From 263967d5f07023002186539df20d3e25fd7dc98e Mon Sep 17 00:00:00 2001 From: Benjamin Lipp Date: Mon, 2 Feb 2026 16:21:36 +0100 Subject: [PATCH] feat: add missing grammar rules for CryptoVerif compat --- marzipan/src/grammar/_cryptoverif.lark | 7 --- marzipan/src/grammar/common.lark | 13 +++-- marzipan/src/grammar/cryptoverif.lark | 76 ++++++++++++++++++++++++++ marzipan/src/grammar/decl.lark | 19 +++++-- marzipan/src/parser.py | 6 +- 5 files changed, 103 insertions(+), 18 deletions(-) delete mode 100644 marzipan/src/grammar/_cryptoverif.lark create mode 100644 marzipan/src/grammar/cryptoverif.lark diff --git a/marzipan/src/grammar/_cryptoverif.lark b/marzipan/src/grammar/_cryptoverif.lark deleted file mode 100644 index b406f4cd..00000000 --- a/marzipan/src/grammar/_cryptoverif.lark +++ /dev/null @@ -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} ")" "." diff --git a/marzipan/src/grammar/common.lark b/marzipan/src/grammar/common.lark index d8f1f152..3d7f03bf 100644 --- a/marzipan/src/grammar/common.lark +++ b/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" diff --git a/marzipan/src/grammar/cryptoverif.lark b/marzipan/src/grammar/cryptoverif.lark new file mode 100644 index 00000000..ce0e6a38 --- /dev/null +++ b/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} ")" "." \ No newline at end of file diff --git a/marzipan/src/grammar/decl.lark b/marzipan/src/grammar/decl.lark index ab739938..2997711e 100644 --- a/marzipan/src/grammar/decl.lark +++ b/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 diff --git a/marzipan/src/parser.py b/marzipan/src/parser.py index fc3271d2..a114c1a9 100644 --- a/marzipan/src/parser.py +++ b/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: /\(\*(\*(?!\))|[^*])*\*\)/