From 8b5fef2fed32cd09cd442d02ce32829af685e4af Mon Sep 17 00:00:00 2001 From: Benjamin Lipp Date: Tue, 7 Jul 2026 18:02:38 +0200 Subject: [PATCH] chore: add %extend and -> to TODO after having tested them Co-authored-by: Anja Rabich --- marzipan/TODO.md | 15 ++++++++++++--- marzipan/src/letfuncdecl.py | 26 ++++++++++++++++++-------- 2 files changed, 30 insertions(+), 11 deletions(-) diff --git a/marzipan/TODO.md b/marzipan/TODO.md index a3602b54..901b031d 100644 --- a/marzipan/TODO.md +++ b/marzipan/TODO.md @@ -52,15 +52,21 @@ * integrate marzipan.awk into Python, somehow * review letfundecl.py * [X] distill what we learned about grammar style - * cyclic dependencies are problematic if we wanted to split the grammar into multiple files and import within a lark grammar, because Lark would then complain when one file is not self-containing/completely resolvable + * newly discovered Lark features: + * %extend makes it possible to first load the original ProVerif grammar + and then load a small file that adapts it + * -> can be used to give different names to branches of a rule, this + spares us from splitting rules manually + * [Update: do we need to do this?]cyclic dependencies are problematic if we wanted to split the grammar into multiple files and import within a lark grammar, because Lark would then complain when one file is not self-containing/completely resolvable + * maybe this is no longer necessary anyway now that we know about %extend * rules with multiple sub-rules, if the sub-rules have differently long or different "type signatures", or different constants, except if all sub-rules only have one base type and no different constants - * rules that have list values in them together with other values: the list value must be moved into a dedicated rule to not be problematic with the AsList class inheritance + * rules that have multiple parameters from which one is a list: the list value must be moved into a dedicated rule to not be problematic with the AsList class inheritance * in the transformer class, each terminal must have a function that handles it * [X] learnings w.r.t. pretty_format * if an optional attribute is an integer that can be 0, `is not None` must be used explicitly, otherwise 0 will be treated as false; for strings this is fine because we do not want to print empty strings * all rules shall have a test file that touches/uses them * scale letfundecl.py to the entire grammar - * rewrite the grammar in the new style + * rewrite the grammar in the new style, using %extend and -> * generate/write the dataclasses * write a test framework that computes test coverage for rules * options term special cases (c.f. manual page 133, starting with "fun" term) @@ -79,6 +85,9 @@ * reconstruct ProVerif input file for ProVerif * rewrite our CPP usages into Python/…? * low priority: nested comments in ProVerif code +* usability feature: functionality to help modify a grammar, as seen in the modify_decl_rule function + * Lark does not seem to have a pretty printer for the internal grammar representation, + source_grammar is exactly the input string ## Idea diff --git a/marzipan/src/letfuncdecl.py b/marzipan/src/letfuncdecl.py index e7b5c955..2117a899 100644 --- a/marzipan/src/letfuncdecl.py +++ b/marzipan/src/letfuncdecl.py @@ -738,6 +738,7 @@ class QuerySecret(MarzipanAST): def pretty_print(self, column: int = 0) -> str: return pretty_format( self, + # "secret" IDENT ["public_vars" ident_list] [";" query] "secret {ident}" + ("public_vars {public_vars:list.gterm}" if self.public_vars else "") + ("; {query}" if self.query else ""), @@ -852,18 +853,25 @@ lemma_public_vars_secret: gterm "for" "{" "secret" IDENT [ "public_vars" ident_l lemma: lemma_gterm | lemma_public_vars | lemma_public_vars_secret + lemma_annotation: _LEMMA ESCAPED_STRING lemma_decl: [lemma_annotation] lemma_decl_core lemma_decl_core: "lemma" [ typedecl ";"] lemma "." -query_gterm: gterm ["public_vars" ident_list] [";" query] -query_secret: "secret" IDENT ["public_vars" ident_list] [";" query] -query_putbegin: "putbegin" "event" ":" ident_list [";" query] // Opportunistically left a space between "event" and ":", ProVerif might not accept it with spaces. -query_putbegin_inj: "putbegin" "inj-event" ":" ident_list [";" query] -query: query_gterm - | query_secret - | query_putbegin - | query_putbegin_inj +//query_gterm: gterm ["public_vars" ident_list] [";" query] +//query_secret: "secret" IDENT ["public_vars" ident_list] [";" query] +//query_putbegin: "putbegin" "event" ":" ident_list [";" query] // Opportunistically left a space between "event" and ":", ProVerif might not accept it with spaces. +//query_putbegin_inj: "putbegin" "inj-event" ":" ident_list [";" query] +//?query: query_gterm +// | query_secret +// | query_putbegin +// | query_putbegin_inj + +query: gterm ["public_vars" ident_list] [";" query] -> query_gterm + | "secret" IDENT ["public_vars" ident_list] [";" query] -> query_secret + // Opportunistically left a space between "event" and ":", ProVerif might not accept it with spaces. + | "putbegin" "event" ":" ident_list [";" query] -> query_putbegin + | "putbegin" "inj-event" ":" ident_list [";" query] -> query_putbegin_inj query_annotation: _QUERY ESCAPED_STRING reachable_annotation: _REACHABLE ESCAPED_STRING @@ -1043,6 +1051,8 @@ def pretty_print(asttree: list): def parse(input: str): global DEBUG + # print(parser.source_grammar) + parsetree = parser.parse(input) # print("=" * 100) # print("print parsetree")