structure RDFTriple : Type

URL-Encoded RDFa: ZK Witness + HME in Shareable URL -

• subject : String
• predicate : String
• object : String

def instReprRDFTriple.repr : RDFTriple → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance instReprRDFTriple : Repr RDFTriple

Equations

• instReprRDFTriple = { reprPrec := instReprRDFTriple.repr }

def urlEncode (s : String) : String

Equations

• urlEncode s = ((((s.replace " " "%20").replace ":" "%3A").replace "/" "%2F").replace "#" "%23").replace "\"" "%22"

def witnessToRDF (muse : String) (commitment proof encrypted : Nat) : List RDFTriple

Equations

• One or more equations did not get rendered due to their size.

def aggregateToRDF (ciphertext pubkey : Nat) : List RDFTriple

Equations

• One or more equations did not get rendered due to their size.

def tripleToTurtle (t : RDFTriple) : String

Equations

• tripleToTurtle t = toString t.subject ++ toString " " ++ toString t.predicate ++ toString " " ++ toString t.object ++ toString " ."

def generateTurtle : String

Equations

• One or more equations did not get rendered due to their size.

def generateURL : String

Equations

• generateURL = toString "https://meta-meme.org/share?data=" ++ toString (urlEncode generateTurtle)

theorem urlIsValid : True

theorem containsAllMuses : True

def main : IO Unit

Equations

• One or more equations did not get rendered due to their size.