From cbb1b66a0df52f94dba565180eb72d41151443e1 Mon Sep 17 00:00:00 2001 From: Benjamin Lipp Date: Tue, 7 Jul 2026 16:23:03 +0200 Subject: [PATCH] WIP: pretty printer Co-authored-by: Anja Rabich --- marzipan/TODO.md | 17 ++ marzipan/src/__init__.py | 3 +- marzipan/src/letfuncdecl.py | 425 +++++++++++++++++++----------------- marzipan/src/sample.pv | 2 +- 4 files changed, 247 insertions(+), 200 deletions(-) diff --git a/marzipan/TODO.md b/marzipan/TODO.md index 98bae1a7..a3602b54 100644 --- a/marzipan/TODO.md +++ b/marzipan/TODO.md @@ -45,7 +45,24 @@ ## Next Steps +* refactor letfundecl.py into separate modules, shorter functions, … +* write a test framework + * file in, test succeeds if parsing succeeds + * file in, test succeeds if parsing and pretty printing succeeds and matches input up to whitespace, and opinionated things like empty square brackets. * 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 + * 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 + * 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 + * 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) * complete with CryptoVerif options * do not assume that the repo path has subdir marzipan diff --git a/marzipan/src/__init__.py b/marzipan/src/__init__.py index 9d89286f..c2fc1f58 100644 --- a/marzipan/src/__init__.py +++ b/marzipan/src/__init__.py @@ -1,7 +1,8 @@ # from rich.console import Console import click -from .parser import * +import .parser as parser + from .util import export, pkgs, rename, setup_exports target_subdir = "target/proverif" diff --git a/marzipan/src/letfuncdecl.py b/marzipan/src/letfuncdecl.py index 771d37fe..e7b5c955 100644 --- a/marzipan/src/letfuncdecl.py +++ b/marzipan/src/letfuncdecl.py @@ -19,6 +19,7 @@ from lark import Lark, Token, Transformer, Tree, ast_utils, tree, v_args from lark.tree import Meta from typing_extensions import Type +from proverif.ast.attributemap import AttrMap from util import T this_module = sys.modules[__name__] @@ -27,22 +28,18 @@ pp = pprint.PrettyPrinter(indent=4, width=50) DEBUG = False +PTERM_LIST_CONFIG = { + "list_separator": ", ", + "left_bracket": "(", + "right_bracket": ")", + "empty_brackets": True, + "none_representation": "", +} + CONFIG = { "space": " ", - "list.pterm": { - "list_separator": ", ", - "left_bracket": "(", - "right_bracket": ")", - "empty_brackets": True, - "none_representation": "", - }, - "list.default": { - "list_separator": ", ", - "left_bracket": "(", - "right_bracket": ")", - "empty_brackets": True, - "none_representation": "", - }, + "list.pterm": PTERM_LIST_CONFIG, + "list.default": PTERM_LIST_CONFIG, "list.gterm": { "list_separator": ", ", "left_bracket": "", @@ -58,37 +55,6 @@ CONFIG = { } -class AttrMap(Mapping): - """ - Small wrapper so that dict values can be accessed as {ctx.foo} - instead of only {ctx["foo"]} inside our custom format strings. - """ - - def __init__(self, mapping: Mapping[str, Any]): - self._mapping = mapping - - def __getattr__(self, name: str) -> Any: - try: - return self._mapping[name] - except KeyError: - raise AttributeError(name) from None - - def __getitem__(self, name: str) -> Any: - return self._mapping[name] - - def __contains__(self, key: object) -> bool: - return key in self._mapping - - def __str__(self) -> str: - return str(self._mapping) - - def __iter__(self) -> Iterator[Any]: - return self._mapping.__iter__() - - def __len__(self) -> int: - return len(self._mapping) - - def get_list_config(format_spec: str, ctx: Mapping[str, Any] | None = None): if ctx: if format_spec not in ctx: @@ -108,6 +74,25 @@ def get_list_config(format_spec: str, ctx: Mapping[str, Any] | None = None): ) +format_spec_parser = Lark(""" +start: list_config | linebreaks + +LIST_PREFIX: "list" +LIST_TYPES: "pterm" | "gterm" | "default" +list_config: LIST_PREFIX "." LIST_TYPES + +linebreaks: "indentline" | "newline" +""") + + +def check_format_spec(format_spec: str): + if not format_spec == "": + # This raises an error in case the format spec string + # does not match the grammar + format_spec_parser.parse(format_spec) + return True + + def pretty( value: Any, column: int, format_spec: str, ctx: Mapping[str, Any] | None = None ) -> str: @@ -228,6 +213,8 @@ class PrettyFormatter(Formatter): def format_field(self, value: Any, format_spec: str) -> str: """This function override injects the column and configuration context""" + if not check_format_spec(format_spec): + raise ValueError(f"invalid format spec {format_spec}") return pretty(value, column=self.column, format_spec=format_spec, ctx=self.ctx) @@ -247,7 +234,7 @@ class MarzipanAST(ast_utils.Ast, ABC): @dataclass class TypeDecl(MarzipanAST): - ident: Token + ident: Ident def pretty_print(self, column: int = 0) -> str: template = "type {ident}." @@ -256,7 +243,7 @@ class TypeDecl(MarzipanAST): @dataclass class Typeid(MarzipanAST): - ident: Token + ident: Ident def pretty_print(self, column: int = 0) -> str: template = "{ident}" @@ -273,22 +260,39 @@ class Pterm(MarzipanAST, ast_utils.AsList): @dataclass -class Gbinding(MarzipanAST): - value: int | Ident +class GbindingNat(MarzipanAST): + value: int gterm: Gterm gbinding: Optional[Gbinding] = None def pretty_print(self, column: int = 0) -> str: - result = "" - if type(self.value) is int: - result = pretty_format(self, "!{value}={gterm}", column=column) - else: - result = pretty_format(self, "{value}={gterm}", column=column) + return pretty_format( + self, + "!{value}={gterm}" + (";{gbinding}" if self.gbinding else ""), + column=column, + ) - if self.gbinding is not None: - result += pretty_format(self, ";{gbinding}", column=column) - return result +@dataclass +class GbindingIdent(MarzipanAST): + value: Ident + gterm: Gterm + gbinding: Optional[Gbinding] = None + + def pretty_print(self, column: int = 0) -> str: + return pretty_format( + self, + "{value}={gterm}" + (";{gbinding}" if self.gbinding else ""), + column=column, + ) + + +@dataclass +class Gbinding(MarzipanAST): + gbinding: GbindingNat | GbindingIdent + + def pretty_print(self, column: int = 0) -> str: + return pretty_format(self, "{gbinding}", column=column) @dataclass @@ -318,8 +322,10 @@ class FunGterm(MarzipanAST): return pretty_format( self, "{fun_gterm}({gterm_list})" + # phase is an int, so we need to check for None explicitly, + # because the int might be 0, and 0 would be interpreted as false. + (" phase {phase}" if self.phase is not None else "") - + (" @ {at}" if self.at is not None else ""), + + (" @ {at}" if self.at else ""), column=column, ) @@ -332,17 +338,17 @@ class InfixGterm(MarzipanAST): def pretty_print(self, column: int = 0) -> str: return pretty_format( - self, "{first_infix_gterm} {self.infix} {second_infix_gterm}", column=column + self, "{first_infix_gterm} {infix} {second_infix_gterm}", column=column ) @dataclass class ChoiceGterm(MarzipanAST): - choice_gterm: Tuple[Gterm, Gterm] + left: Gterm + right: Gterm def pretty_print(self, column: int = 0) -> str: - left, right = self.choice_gterm - return f"choice [ {left.pretty_print()}, {right.pretty_print()} ]" + return pretty_format(self, "choice [{left}, {right}]", column=column) @dataclass @@ -352,7 +358,7 @@ class ArithGterm(MarzipanAST): value: int def pretty_print(self, column: int = 0) -> str: - return f"{self.arith_gterm.pretty_print()} {self.operand} {self.value}" + return pretty_format(self, "{arith_gterm} {operand} {value}", column=column) @dataclass @@ -361,7 +367,7 @@ class Arith2Gterm(MarzipanAST): arith_gterm: Gterm def pretty_print(self, column: int = 0) -> str: - return f"{self.value} + {self.arith_gterm.pretty_print()}" + return pretty_format(self, "{value} + {arith_gterm}", column=column) @dataclass @@ -370,10 +376,11 @@ class InjeventGterm(MarzipanAST): at: Optional[Ident] = None def pretty_print(self, column: int = 0) -> str: - result = f"inj-event ( {self.event_gterms.pretty_print()} )" - if self.at is not None: - result += f"@ {self.at}" - return result + return pretty_format( + self, + "inj-event ( {event_gterms} )" + ("@ {at}" if self.at else ""), + column=column, + ) @dataclass @@ -382,7 +389,7 @@ class ImpliesGterm(MarzipanAST): right: Gterm def pretty_print(self, column: int = 0) -> str: - return f"{self.left.pretty_print()} ==> {self.right.pretty_print()}" + return pretty_format(self, "{left} ==> {right}", column=column) @dataclass @@ -393,8 +400,7 @@ class EventGterm(MarzipanAST): def pretty_print(self, column: int = 0) -> str: return pretty_format( self, - "event ({event_gterms:list.gterm})" - + ("@{at}" if self.at is not None else ""), + "event ({event_gterms:list.gterm})" + ("@{at}" if self.at else ""), column=column, ) @@ -428,15 +434,16 @@ class LetGterm(MarzipanAST): @dataclass class SampleGterm(MarzipanAST): ident: Ident + # The implementation here does not allow to reproduce empty square brackets. + # Empty square brackets in the input will result in no square brackets in the output. gbinding: Optional[Gbinding] = None def pretty_print(self, column: int = 0) -> str: - str = f"new {self.ident.value}" - if self.gbinding is not None: - str += "[" - str += self.gbinding.pretty_print() - str += "]" - return str + return pretty_format( + self, + "new {ident}" + ("[{gbinding}]" if self.gbinding else ""), + column=column, + ) @dataclass @@ -484,24 +491,17 @@ class Gterm(MarzipanAST): @dataclass class Typedecl(MarzipanAST): - type_list: List[Ident] + type_list: IdentList typeid: Typeid optional_typedecl: Optional[Typedecl] = None - # _non_empty_seq{IDENT} ":" typeid [ "," typedecl ] def pretty_print(self, column: int = 0) -> str: - str = "" - # str += ", ".join([t.pretty_print() for t in self.type_list]) - if isinstance(self.type_list, List): - str += ", ".join([t for t in self.type_list]) - elif isinstance(self.type_list, Token): - str += self.type_list.value - str += ": " - str += self.typeid.pretty_print() - if self.optional_typedecl is not None: - str += ", " - str += self.optional_typedecl.pretty_print() - return str + return pretty_format( + self, + "{type_list:list.gterm}: {typeid}" + + (", {optional_typedecl}" if self.optional_typedecl else ""), + column=column, + ) @dataclass @@ -514,7 +514,7 @@ class LetfunDecl(MarzipanAST): return pretty_format( self, "letfun {ident}" - + ("({typedecl})" if self.typedecl is not None else "") + + ("({typedecl})" if self.typedecl else "") + " =\n{pterm:indentline}." + "{ctx.empty_lines_after_decl}", column=column, @@ -529,53 +529,50 @@ class LemmaGterm(MarzipanAST): def pretty_print(self, column: int = 0) -> str: return pretty_format( self, - "{gterm}" + ("; {lemma}" if self.lemma is not None else ""), + "{gterm}" + ("; {lemma}" if self.lemma else ""), column=column, ) +@dataclass +class IdentList(MarzipanAST, ast_utils.AsList): + idents: List[Ident] + + def pretty_print(self, column: int = 0) -> str: + return pretty_format(self, "{idents:list.gterm}", column=column) + + @dataclass class LemmaPublicVars(MarzipanAST): gterm: Gterm - public_vars: List + public_vars: IdentList lemma: Optional[Lemma] = None def pretty_print(self, column: int = 0) -> str: - str = self.gterm.pretty_print() - str += "for { public_vars" - str += ",".join( - [ - v.pretty_print() if hasattr(v, "pretty_print") else str(v) - for v in self.public_vars - ] + return pretty_format( + self, + "{gterm} for {{ public_vars {public_vars} }}" + + ("; {lemma}" if self.lemma else ""), + column=column, ) - str += "}" - if self.lemma is not None: - str += ";" + self.lemma.pretty_print() - return str @dataclass class LemmaPublicVarsSecret(MarzipanAST): gterm: Gterm secret: Ident - public_vars: List + public_vars: Optional[IdentList] lemma: Optional[Lemma] = None def pretty_print(self, column: int = 0) -> str: - str = self.gterm.pretty_print() - str += "for { secret" - str += self.secret.value - str += ",".join( - [ - v.pretty_print() if hasattr(v, "pretty_print") else str(v) - for v in self.public_vars - ] + return pretty_format( + self, + "{gterm} for {{ secret {secret}" + + ("public_vars {public_vars}" if self.public_vars else "") + + "[real_or_random] }}" + + ("; {lemma}" if self.lemma else ""), + column=column, ) - str += "[real_or_random] }" - if self.lemma is not None: - str += ";" + self.lemma.pretty_print() - return str @dataclass @@ -608,7 +605,7 @@ class LemmaDeclCore(MarzipanAST): return pretty_format( self, "lemma " - + ("{typedecl};" if self.typedecl is not None else "") + + ("{typedecl};" if self.typedecl else "") + "\n" + "{lemma:indentline}." + "{ctx.empty_lines_after_decl}", @@ -621,9 +618,7 @@ class LemmaAnnotation(MarzipanAST): annotation: str def pretty_print(self, column: int = 0) -> str: - str = "" - str += self.annotation - return str + return pretty_format(self, "{annotation}", column=column) @dataclass @@ -632,21 +627,22 @@ class LemmaDecl(MarzipanAST): lemma_decl_core: LemmaDeclCore def pretty_print(self, column: int = 0) -> str: - str = "" - if self.lemma_decl_annotation is not None: - str += f"@lemma {self.lemma_decl_annotation}\n" - str += f"{self.lemma_decl_core.pretty_print()}" - return str + return pretty_format( + self, + ("@lemma {lemma_decl_annotation}" if self.lemma_decl_annotation else "") + + "{lemma_decl_core}", + column=column, + ) # "{% if lemma_decl_annotation %}@lemma {{lemma_decl_annotation}}{% endif %}{{lemma_decl_core}}" # def pretty_print(self, column=0, indent=2): - # return f"{'@lemma' + a if a is not None else ''}{l}" + # return f"{'@lemma' + a if a else ''}{l}" # def pretty_print(self, column=0, indent=2): # a = self.lemma_decl_annotation # l = self.lemma_decl_core - # return f"{'@lemma' + a.pretty_print(column, indent) if a is not None else ''}{l.pretty_print(column, indent)}" + # return f"{'@lemma' + a.pretty_print(column, indent) if a else ''}{l.pretty_print(column, indent)}" @dataclass @@ -654,7 +650,7 @@ class Query(MarzipanAST): query: QueryGterm | QuerySecret | QueryPutBegin def pretty_print(self, column: int = 0) -> str: - return self.query.pretty_print() + return pretty_format(self, "{query}", column=column) @dataclass @@ -662,7 +658,7 @@ class QueryAnnotation(MarzipanAST): annotation: str def pretty_print(self, column: int = 0) -> str: - return self.annotation + return pretty_format(self, "{annotation}", column=column) @dataclass @@ -670,7 +666,7 @@ class ReachableAnnotation(MarzipanAST): annotation: str def pretty_print(self, column: int = 0) -> str: - return self.annotation + return pretty_format(self, "{annotation}", column=column) @dataclass @@ -682,9 +678,9 @@ class QueryDeclCore(MarzipanAST): return pretty_format( self, "query " - + ("{typedecl};" if self.typedecl is not None else "") + + ("{typedecl};" if self.typedecl else "") + "\n" - + "{query:newline}." + + "{query:indentline}." + "{ctx.empty_lines_after_decl}", column=column, ) @@ -692,101 +688,117 @@ class QueryDeclCore(MarzipanAST): @dataclass class QueryDecl(MarzipanAST): - query_decl_annotation: Optional[QueryAnnotation | ReachableAnnotation] + annotation: Optional[QueryAnnotation] query_decl_core: QueryDeclCore def pretty_print(self, column: int = 0) -> str: - str = "" - if self.query_decl_annotation is not None: - if isinstance(self.query_decl_annotation, QueryAnnotation): - str += f"@query {self.query_decl_annotation.pretty_print()}\n" - elif isinstance(self.query_decl_annotation, ReachableAnnotation): - str += f"@reachable {self.query_decl_annotation.pretty_print()}\n" - str += self.query_decl_core.pretty_print() - return str + return pretty_format( + self, + ("@query {annotation}" if self.annotation else "") + "{query_decl_core}", + column=column, + ) + + +@dataclass +class ReachableDecl(MarzipanAST): + annotation: Optional[ReachableAnnotation] + query_decl_core: QueryDeclCore + + def pretty_print(self, column: int = 0) -> str: + return pretty_format( + self, + ("@reachable {annotation}" if self.annotation else "") + + "{query_decl_core}", + column=column, + ) @dataclass class QueryGterm(MarzipanAST): gterm: Gterm - public_vars: Optional[List[Ident]] = None + public_vars: Optional[IdentList] = None query: Optional[Query] = None def pretty_print(self, column: int = 0) -> str: - str = self.gterm.pretty_print() - if self.public_vars is not None: - str += "public_vars " - str += ", ".join( - [ - v.pretty_print() if hasattr(v, "pretty_print") else str(v) - for v in self.public_vars - ] - ) - if self.query is not None: - str += ";" + self.query.pretty_print() - return str + return pretty_format( + self, + "{gterm}" + + ("public_vars {public_vars:list.gterm}" if self.public_vars else "") + + ("; {query}" if self.query else ""), + column=column, + ) @dataclass class QuerySecret(MarzipanAST): ident: Ident - public_vars: Optional[List[Ident]] = None + public_vars: Optional[IdentList] = None query: Optional[Query] = None def pretty_print(self, column: int = 0) -> str: - str = "secret" - str += self.ident.pretty_print() - if self.public_vars is not None: - str += "public_vars " - str += ", ".join( - [ - v.pretty_print() if hasattr(v, "pretty_print") else str(v) - for v in self.public_vars - ] - ) - if self.query is not None: - str += ";" + self.query.pretty_print() - return str + return pretty_format( + self, + "secret {ident}" + + ("public_vars {public_vars:list.gterm}" if self.public_vars else "") + + ("; {query}" if self.query else ""), + column=column, + ) @dataclass class QueryPutBegin(MarzipanAST): - event_list: List[Ident] + event_list: IdentList query: Optional[Query] = None def pretty_print(self, column: int = 0) -> str: - str = "putbegin event :" - str += ", ".join( - [ - e.pretty_print() if hasattr(e, "pretty_print") else str(e) - for e in self.event_list - ] + return pretty_format( + self, + "putbegin event :" + + ("{event_list:list.gterm}" if self.event_list else "") + + ("; {query}" if self.query else ""), + column=column, + ) + + +@dataclass +class QueryPutBeginInj(MarzipanAST): + event_list: IdentList + query: Optional[Query] = None + + def pretty_print(self, column: int = 0) -> str: + return pretty_format( + self, + "putbegin inj-event :" + + ("{event_list:list.gterm}" if self.event_list else "") + + ("; {query}" if self.query else ""), + column=column, ) - if self.query is not None: - str += ";" + self.query.pretty_print() - return str @dataclass class Decl(MarzipanAST): - decl: LemmaDecl | QueryDecl | TypeDecl | LetfunDecl + decl: LemmaDecl | QueryDecl | ReachableDecl | TypeDecl | LetfunDecl def pretty_print(self, column: int = 0) -> str: - return self.decl.pretty_print() + return pretty_format( + self, + "{decl}", + column=column, + ) parser = Lark(""" start: decl* -decl: lemma_decl | query_decl | type_decl | letfun_decl +decl: lemma_decl | query_decl | reachable_decl | type_decl | letfun_decl _non_empty_seq{x}: x ("," x)* _maybe_empty_seq{x}: [ _non_empty_seq{x} ] IDENT: /[a-zA-Z][a-zA-Z0-9À-ÿ'_]*/ -NAT: DIGIT+ +NAT: DIGIT+ // ProVerif Manual 4.1.3: 0 is considered as natural number typeid: IDENT type_decl: "type" IDENT "." -typedecl: _non_empty_seq{IDENT} ":" typeid [ "," typedecl ] +typedecl: ident_list ":" typeid [ "," typedecl ] pterm: IDENT | NAT | "(" _maybe_empty_seq{pterm} ")" letfun_decl: "letfun" IDENT [ "(" [ typedecl ] ")" ] "=" pterm "." _QUERY: "@query" @@ -827,12 +839,16 @@ paren_gterm: "(" gterm_list ")" sample_gterm: "new" IDENT [ "[" [ gbinding ] "]" ] let_gterm: "let" IDENT "=" gterm "in" gterm -gbinding: "!" NAT "=" gterm [";" gbinding] - | IDENT "=" gterm [";" gbinding] +gbinding_nat: "!" NAT "=" gterm [";" gbinding] +gbinding_ident: IDENT "=" gterm [";" gbinding] +gbinding: gbinding_nat + | gbinding_ident + +ident_list: _non_empty_seq{IDENT} lemma_gterm: gterm [";" lemma] -lemma_public_vars: gterm "for" "{" "public_vars" _non_empty_seq{IDENT} "}" [";" lemma] -lemma_public_vars_secret: gterm "for" "{" "secret" IDENT [ "public_vars" _non_empty_seq{IDENT}] "[real_or_random]" "}" [";" lemma] +lemma_public_vars: gterm "for" "{" "public_vars" ident_list "}" [";" lemma] +lemma_public_vars_secret: gterm "for" "{" "secret" IDENT [ "public_vars" ident_list] "[real_or_random]" "}" [";" lemma] lemma: lemma_gterm | lemma_public_vars | lemma_public_vars_secret @@ -840,16 +856,20 @@ lemma_annotation: _LEMMA ESCAPED_STRING lemma_decl: [lemma_annotation] lemma_decl_core lemma_decl_core: "lemma" [ typedecl ";"] lemma "." -query_gterm: gterm ["public_vars" _non_empty_seq{IDENT}] [";" query] -query_secret: "secret" IDENT ["public_vars" _non_empty_seq{IDENT}] [";" query] -query_putbegin: "putbegin" "event" ":" _non_empty_seq{IDENT} [";" query] // Opportunistically left a space between "event" and ":", ProVerif might not accept it with spaces. -| "putbegin" "inj-event" ":" _non_empty_seq{IDENT} [";" query] +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_annotation: _QUERY ESCAPED_STRING reachable_annotation: _REACHABLE ESCAPED_STRING -query_decl: [ query_annotation | reachable_annotation] query_decl_core + +query_decl: [query_annotation] query_decl_core +reachable_decl: [reachable_annotation] query_decl_core query_decl_core: "query" [ typedecl ";"] query "." %import common (DIGIT, WS, ESCAPED_STRING) @@ -858,14 +878,22 @@ query_decl_core: "query" [ typedecl ";"] query "." class ToAst(Transformer): - def IDENT(self, str): - return str + def IDENT(self, token: Token) -> str: + return str(token.value) - def NAT(self, n): - n = int(n) + def INFIX(self, token: Token) -> str: + return str(token.value) + + def NAT(self, token: Token) -> int: + n = int(token.value) assert n >= 0, "NAT must be an integer >= 0" return n + # This captures all tokens that are not explicitly handled by other methods, + # like ESCAPED_STRING, etc, that we import in our grammar. + def __default_token__(self, token: Token) -> Any: + return token.value + # @v_args(inline=True) def start(self, x): return x @@ -1019,6 +1047,7 @@ def parse(input: str): # print("=" * 100) # print("print parsetree") # print(parsetree.pretty()) + # print(parsetree) ast = transformer.transform(parsetree) # print("=" * 100) # print("print_tree ast") diff --git a/marzipan/src/sample.pv b/marzipan/src/sample.pv index 669d8fbf..87bb83b7 100644 --- a/marzipan/src/sample.pv +++ b/marzipan/src/sample.pv @@ -28,7 +28,7 @@ query k:key; @lemma "secrecy: The adversary can learn a trusted kem pk only by using the reveal oracle" lemma skp:kem_sk_prec; attacker(kem_pub(trusted_kem_sk(skp))) - ==> event(RevealPk(kem_pub(trusted_kem_sk(skp)))). + ==> event(RevealPk(kem_pub(trusted_kem_sk(skp)))) for { public_vars a, b}. @lemma "secrecy: Attacker knowledge of a kem sk implies the key is not trusted" lemma k:kem_sk, kp:kem_sk_prec;