gitea-mirror/rosenpass
1
0
Fork 0
mirror of https://github.com/rosenpass/rosenpass.git synced 2026-02-28 14:33:37 -08:00
Code Issues Packages Projects Releases Wiki Activity

feat: module declaration, WIP: missing ProVerif option terms

Browse Source 
Co-authored-by: Anja Rabich <a.rabich@uni-luebeck.de>
This commit is contained in:
Benjamin Lipp
2025-10-14 18:01:13 +02:00
parent 3ce0d262d9
commit f20fd1acc3
2 changed files with 13 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
marzipan/TODO.md
View File

@@ -33,11 +33,12 @@
* ~~exception handling in analyze() and in run_proverif()~~ * ~~exception handling in analyze() and in run_proverif()~~
* ~~refactor filtering in run_proverif (see karo's comment)~~ * ~~refactor filtering in run_proverif (see karo's comment)~~
* ~configurable target directory~ * ~configurable target directory~
* ~lark parser: multiline comments, how???~
## Next Steps ## Next Steps
* integrate marzipan.awk into Python, somehow * integrate marzipan.awk into Python, somehow
* lark parser: multiline comments, how??? * options term special cases (c.f. manual page 133, starting with "fun" term)
* rewrite marzipan.awk into Python/LARK * rewrite marzipan.awk into Python/LARK
* define a LARK grammar for marzipan.awk rules * define a LARK grammar for marzipan.awk rules
* write python code for processing marzipan rules, e.g. alias replacement (step: i.pv->o.pv) * write python code for processing marzipan rules, e.g. alias replacement (step: i.pv->o.pv)
@@ -54,6 +55,6 @@
* and rewrite the AST within Python * and rewrite the AST within Python
* reconstruct ProVerif input file for ProVerif * reconstruct ProVerif input file for ProVerif
* rewrite our CPP usages into Python/…? * rewrite our CPP usages into Python/…?
* low priority: nested comments in ProVerif code
“it replaces the Bash script and is idiomatic Python code” “it replaces the Bash script and is idiomatic Python code”

11
marzipan/src/parser.py
View File

@@ -33,7 +33,13 @@ proverif_grammar = Lark(
_non_empty_seq{x}: x ("," x)* _non_empty_seq{x}: x ("," x)*
_maybe_empty_seq{x}: [ _non_empty_seq{x} ] _maybe_empty_seq{x}: [ _non_empty_seq{x} ]
IDENT_FUN_CONST: "data" | "private" | "typeConverter"
IDENT_FREE_REDUC: "private"
IDENT_PRED: "memberOptim" | "block"
IDENT_PROCESS: "precise"
IDENT_QUERY_LEMMA_AXIOM: "noneSat" | "discardSat" | "instantiateSat" | "fullSat" | "noneVerif" | "discardVerif" | "instantiateVerif" | "fullVerif"
options: [ "[" _non_empty_seq{IDENT} "]" ] options: [ "[" _non_empty_seq{IDENT} "]" ]
options{idents}: [ "[" _non_empty_seq{idents} "]" ]
process: ZERO process: ZERO
| YIELD | YIELD
| IDENT [ "(" _maybe_empty_seq{pterm} ")" ] | IDENT [ "(" _maybe_empty_seq{pterm} ")" ]
@@ -193,6 +199,7 @@ proverif_grammar = Lark(
| nounif_decl | nounif_decl
| elimtrue_decl | elimtrue_decl
| clauses_decl | clauses_decl
| module_decl
#| param_decl #| param_decl
#| proba_decl #| proba_decl
#| letproba_decl #| letproba_decl
@@ -204,7 +211,7 @@ proverif_grammar = Lark(
channel_decl: "channel" _non_empty_seq{IDENT} "." channel_decl: "channel" _non_empty_seq{IDENT} "."
free_decl: "free" _non_empty_seq{IDENT} ":" typeid options "." free_decl: "free" _non_empty_seq{IDENT} ":" typeid options "."
const_decl: "const" _non_empty_seq{IDENT} ":" typeid options "." const_decl: "const" _non_empty_seq{IDENT} ":" typeid options "."
fun_decl: "fun" IDENT "(" _maybe_empty_seq{typeid} ")" ":" typeid options "." fun_decl: "fun" IDENT "(" _maybe_empty_seq{typeid} ")" ":" typeid options{IDENT_FUN_CONST} "."
letfun_decl: "letfun" IDENT [ "(" [ typedecl ] ")" ] "=" pterm "." letfun_decl: "letfun" IDENT [ "(" [ typedecl ] ")" ] "=" pterm "."
reduc_decl: "reduc" eqlist options "." reduc_decl: "reduc" eqlist options "."
fun_reduc_decl: "fun" IDENT "(" _maybe_empty_seq{typeid} ")" ":" typeid "reduc" mayfailreduc options "." fun_reduc_decl: "fun" IDENT "(" _maybe_empty_seq{typeid} ")" ":" typeid "reduc" mayfailreduc options "."
@@ -328,6 +335,8 @@ proverif_grammar = Lark(
elimtrue_decl: "elimtrue" [ failtypedecl ";" ] term "." elimtrue_decl: "elimtrue" [ failtypedecl ";" ] term "."
clauses_decl: "clauses" clauses "." clauses_decl: "clauses" clauses "."
module_decl: "@module" " " IDENT
# TODO: finish defining these (comes from Cryptoverif) # TODO: finish defining these (comes from Cryptoverif)
#param_decl: "param" _non_empty_seq{IDENT} options "." #param_decl: "param" _non_empty_seq{IDENT} options "."
#proba_decl: "proba" IDENT ["(...)"] options "." #proba_decl: "proba" IDENT ["(...)"] options "."