feat: add missing grammar rules for CryptoVerif compat

marzipan/src/grammar/_cryptoverif.lark

@@ -1,7 +0,0 @@
-    # TODO: finish defining these (comes from Cryptoverif)
-    #param_decl: "param" _non_empty_seq{IDENT} options "."
-    #proba_decl: "proba" IDENT ["(...)"] options "."
-    #letproba_decl: "letproba" IDENT ["(...)"] "= ..." "."
-    #proof_decl: "proof" "{" proof "}"
-    #def_decl: "def" IDENT "(" _maybe_empty_seq{typeid} ")" "{" decl* "}"
-    #expand_decl: "expand" IDENT "(" _maybe_empty_seq{typeid} ")" "."

marzipan/src/grammar/common.lark

@@ -29,12 +29,17 @@ OPTIONS_AXIOM: OPTIONS_QUERY_LEMMA_AXIOM
 OPTIONS_QUERY_LEMMA: OPTIONS_QUERY_LEMMA_AXIOM | "induction" | "noInduction"
 OPTIONS_LEMMA: OPTIONS_QUERY_LEMMA | "maxSubset"
 OPTIONS_QUERY: OPTIONS_QUERY_LEMMA | "proveAll"
-OPTIONS_QUERY_SECRET: "reachability" | "pv_reachability" | "real_or_random" | "pv_real_or_random" | "/cv_[a-zA-Z0-9À-ÿ'_]*/"
+OPTIONS_QUERY_SECRET: "reachability" | "pv_reachability" | "real_or_random" | "pv_real_or_random" | /cv_[a-zA-Z0-9À-ÿ'_]*/
 OPTIONS_RESTRICTION: "removeEvents" | "keepEvents" | "keep" # transl_option_lemma_query in pitsyntax.ml
-OPTIONS_EQUATION: "convergent" | "linear" # check_equations in pitsyntax.ml
+OPTIONS_EQUATION: "convergent" | "linear" | "manual" # manual is for compatibility with CryptoVerif
 OPTIONS_TYPE: "fixed" | "bounded" | "large" | "nonuniform" | "password" | "size" NAT | "size" NAT "_" NAT | "pcoll" NAT | "small" | "ghost" # from Page 22 in CryptoVerif reference manual
 options{idents}: [ "[" _non_empty_seq{idents} "]" ]
-BOOL : "true" | "false"
+
+# ProVerif manual 6.6.2: ProVerif also accepts no instead of false and yes instead of true.
+FALSE: "false" | "no"
+TRUE: "true" | "yes"
+BOOL : TRUE | FALSE
+
 NONE: "none"
 FULL: "full"
 ALL: "all"
@@ -91,7 +96,7 @@ ignore_types_values: BOOL | "all" | "none" | "attacker"
 simplify_process_values: BOOL | "interactive"
 precise_actions_values: BOOL | "trueWithoutArgsInNames"
 redundant_hyp_elim_values: BOOL | "beginOnly"
-reconstruct_trace_values: BOOL | NAT | "yes" | "no" # TODO(blipp): check whether yes/no is always allowed for BOOL
+reconstruct_trace_values: BOOL | NAT
 attacker_values: "active" | "passive"
 key_compromise_values: "none" | "approx" | "strict"
 predicates_implementable: "check" | "nocheck"

marzipan/src/grammar/cryptoverif.lark

@@ -0,0 +1,76 @@
+# CryptoVerif manual Page 21
+OPTIONS_PARAM: "noninteractive" | "passive" | "default" | "small" | "size" NAT
+param_decl: "param" _non_empty_seq{IDENT} options{OPTIONS_PARAM} "."
+
+dimension: "time" ["^" INT]
+         | "length" ["^" INT]
+         | "number"
+         | dimension "*" dimension
+         | dimension "/" dimension
+var_dimension: IDENT ":" dimension
+probability_estimate: "pest" NAT | "password" | "large"
+proba_decl: "proba" IDENT ["(" _maybe_empty_seq{dimension} ")"] ["[" probability_estimate "]"] "."
+
+simpleterm: IDENT
+          | IDENT "(" _maybe_empty_seq{simpleterm} ")"
+          | "(" _maybe_empty_seq{simpleterm} ")"
+          | IDENT "[" _maybe_empty_seq{simpleterm} "]"
+          | simpleterm "=" simpleterm
+          | simpleterm "<>" simpleterm
+          | simpleterm "||" simpleterm
+          | simpleterm "&&" simpleterm
+proba: "(" proba ")"
+     | proba "+" proba
+     | proba "-" proba
+     | proba "*" proba
+     | proba "/" proba
+     | proba "^" INT
+     | "max" "(" _non_empty_seq{proba} ")"
+     | "min" "(" _non_empty_seq{proba} ")"
+     | IDENT [ "(" _maybe_empty_seq{proba} ")" ]
+     | "|" IDENT "|"
+     | "maxlength" "(" simpleterm ")"
+     | "length" "(" IDENT [ "," _non_empty_seq{proba} ] ")"
+     | "length" "(" "(" _maybe_empty_seq{IDENT} ")" [ "," _non_empty_seq{proba} ] ")"
+     | NAT
+     | "#" IDENT
+     | "#" "(" IDENT "foreach" _non_empty_seq{IDENT} ")"
+     | "eps_find"
+     | "eps_rand" "(" IDENT ")"
+     | "Pcoll1rand" "(" IDENT ")"
+     | "Pcoll2rand" "(" IDENT ")"
+     | "time"
+     | "time" "(" IDENT [ "," _non_empty_seq{proba} ] ")"
+     | "time" "(" "let" IDENT [ "," _non_empty_seq{proba} ] ")"
+     | "time" "(" "(" _maybe_empty_seq{IDENT} ")" [ "," _non_empty_seq{proba} ] ")"
+     | "time" "(" "let" "(" _maybe_empty_seq{IDENT} ")" [ "," _non_empty_seq{proba} ] ")"
+     | "time" "(" "=" IDENT [ "," _non_empty_seq{proba} ] ")"
+     | "time" "(" "!" ")"
+     | "time" "(" "foreach" ")"
+     | "time" "(" "[" NAT "]" ")"
+     | "time" "(" "&&" ")"
+     | "time" "(" "||" ")"
+     | "time" "(" "new" IDENT ")"
+     | "time" "(" "<-R" IDENT ")"
+     | "time" "(" "newOracle" ")"
+     | "time" "(" "if" ")"
+     | "time" "(" "find" NAT ")"
+     | "optim-if" optimcond "then" proba "else" proba
+optimcond: "(" optimcond ")"
+         | "is-cst" "(" proba ")"
+         | proba "=" proba
+         | proba "<=" proba
+         | proba ">=" proba
+         | proba "<" proba
+         | proba ">" proba
+         | optimcond "&&" optimcond
+         | optimcond "||" optimcond
+letproba_decl: "letproba" IDENT ["(" _non_empty_seq{var_dimension} ")"] "=" proba "."
+
+# ProVerif ignores proof blocks, so lazily matching proof blocks and accepts everything as
+# proof content except a closing brace should be enough.
+_no_braces: /[^{}]+/
+proof_decl: "proof" "{" [ _no_braces ] "}"
+
+def_decl: "def" IDENT "(" _maybe_empty_seq{typeid} ")" "{" decl* "}"
+expand_decl: "expand" IDENT "(" _maybe_empty_seq{typeid} ")" "."

marzipan/src/grammar/decl.lark

@@ -25,12 +25,12 @@ decl: type_decl
     | elimtrue_decl
     | clauses_decl
     | module_decl
-    #| param_decl
-    #| proba_decl
-    #| letproba_decl
-    #| proof_decl
-    #| def_decl
-    #| expand_decl
+    | param_decl
+    | proba_decl
+    | letproba_decl
+    | proof_decl
+    | def_decl
+    | expand_decl
 
 type_decl: "type" IDENT options{OPTIONS_TYPE} "."
 channel_decl: "channel" _non_empty_seq{IDENT} "."
@@ -86,10 +86,17 @@ noninterf_decl: "noninterf" [ typedecl ";"] _maybe_empty_seq{nidecl} "."
 weaksecret_decl: "weaksecret" IDENT "."
 
 nidecl: IDENT [ "among" "(" _non_empty_seq{term} ")" ]
+
+# According to the manual page 127, “Compatibility with CryptoVerif”, ProVerif also allows disequations.
+# The ProVerif source code uses the same eqlist for equation and reduc, so we do that, too.
 equality: term "=" term
+        | term "<>" term
         | "let" IDENT "=" term "in" equality
+
 mayfailequality: IDENT mayfailterm_seq "=" mayfailterm
+
 eqlist: [ "forall" typedecl ";" ] equality [ ";" eqlist ]
+
 clause: term
         | term "->" term
         | term "<->" term

marzipan/src/parser.py

@@ -105,6 +105,7 @@ process_rules = Path(parent_dir + "process.lark").read_text()
 query_rules = Path(parent_dir + "query.lark").read_text()
 lemma_rules = Path(parent_dir + "lemma.lark").read_text()
 term_rules = Path(parent_dir + "term.lark").read_text()
+cryptoverif_rules = Path(parent_dir + "cryptoverif.lark").read_text()
 
 # marzipan additives
 common_rules = (
@@ -143,9 +144,12 @@ query_rules = modify_decl_rule(
 lemma_rules = modify_decl_rule(lemma_rules, "lemma_decl", "[LEMMA ESCAPED_STRING]")
 
 grammar = (
-    common_rules + decl_rules + process_rules + query_rules + lemma_rules + term_rules
+    common_rules + decl_rules + process_rules + query_rules + lemma_rules + term_rules + cryptoverif_rules
 )
 
+with open(Path(parent_dir + "generated_grammar.lark"), "w") as f:
+    f.write(grammar)
+
 parser = Lark(grammar)
 
 # COMMENT:  /\(\*(\*(?!\))|[^*])*\*\)/