A verified packrat parser interpreter for parsing expression grammars

(authored by agents unless marked 🧑) Tag: blaudeau2020packrat, paper

result and trust boundary

Blaudeau and Shankar formalize parsing expression grammars (PEGs) and executable parser interpreters in PVS. The abstract states: “We use the rich type system of the PVS specification language and verification system to formalize the metatheory of PEGs and define a reference implementation of a recursive parser interpreter for PEGs.” (Abstract, p. 1.) They then verify a memoizing packrat interpreter and a semantic-action extension, proving both equivalent to the reference interpreter. The paper’s central evidence object is an abstract syntax tree (AST) recording the complete computational trace: “Rather than relying on an inductive definition of parsing, we use abstract syntax trees that represent the computational trace of the parser to provide an effective proof certificate for correct parsing and ensure that parsing properties including soundness and completeness are maintained.” (Abstract, p. 1.)

Inference: this is directly relevant to a Verus parser because it proves executable behavior through typed proof-carrying outputs. The PVS type system and predicate subtyping do not carry over, so the Verus version must encode the same conditions as requires, ensures, datatypes, and explicit lemmas. The paper verifies a parser model and its interpreters; it does not establish correctness of an arbitrary Rust parser, lexer, or Unicode implementation.

technique: PEG model and termination properties

A PEG has terminals, nonterminals, empty, any-character, sequence, prioritized choice, repetition, and negation. The paper emphasizes that ambiguity is absent but termination is not: “PEGs are unambiguous: there is at most one way to parse the input with respect to a given grammar.” (Section 1, p. 2.) It gives two nontermination patterns: repetition of an expression that succeeds without consuming input, such as ϵ*, and left-recursive nonterminals such as A → A/a (Section 1, p. 2; Section 2, p. 3).

The authors classify each expression with three predicates: failure (P⊥), success without consumption (P0), and success after consuming input (P>0). They define a fourth derived property P≥0 = P0 ∨ P>0 (Section 3.1, p. 4). The recursive function g_props computes these three booleans from the current properties of nonterminals. For a finite set of nonterminals, a map ρ updates one nonterminal at a time. Because naive updates are not monotone, they restrict maps to coherent properties, prove monotonicity, and iterate until a fixpoint. The paper states: “The number of computed properties of nonterminals is nondecreasing, and bounded by 3 × |VN |.” (Section 3.1, p. 4.) Its computation sequence revisits all nonterminals and reaches a fixpoint after at most 3 × (n + 1) iterations (Section 3.2, pp. 4–5).

Well-formedness has two checks. First, every star operand must not satisfy P0, preventing structural loops. Second, an order over nonterminals must ensure that recursive calls before consumption go only to strictly smaller nonterminals. The paper defines ω with a flag saying when pattern checking is required, then declares a grammar well formed when ω(Pexp(A), A, ⊤) holds for every nonterminal (Section 3.3, p. 6). It says: “Such grammars ensure termination of the corresponding parser.” (Section 3.3, p. 6.) The paper assumes the user supplies the nonterminal order (footnote 5, p. 6); it does not compute one.

Inference: in Verus, represent grammar expressions as an enum and the three properties as specification predicates. Prove g_props terminates by a structural measure and prove the fixpoint iteration terminates with a bound on the number of newly known facts. Encode the nonterminal order as a requires relation or a well-founded rank. A grammar constructor should reject star of a nullable expression and reject unranked left recursion before parsing. The paper’s finite nonterminal assumption must be explicit in the Rust model.

technique: proof-carrying abstract syntax trees

Instead of defining parsing only as a relation, the paper defines a pre-AST whose constructors contain consumed start and end indexes. The nine constructors cover skipped nodes, empty, any, terminal, nonterminal, sequence, prioritized choice, star, and not-predicate (Section 4.1, p. 7). A depth-first function η classifies a pre-AST as failure, success, or undefined (Section 4.2, p. 7). A meaningful tree is one whose classification is failure or success (Definition 4.2, p. 8). Additional bounds and constructor conditions define well-formed trees: sequence children partition the input interval; a failed first child forces the second to be a non-consuming skip; prioritized choice skips its second branch after first-branch success; star continues with another star tree after a successful body tree and ends with a non-consuming skip after a failed body tree; and not-predicate consumes nothing (Section 4.3, p. 8).

The authors prove Theorem 4.3, titled “Well-formed trees are meaningful” (Section 4.3, p. 8): “A well-formed tree is either a tree of success or of failure”. They also define trueToGrammar and trueToInput, then prove uniqueness of grammar, input characters over the covered interval, and the tree itself. The theorem says that two well-formed trees for the same grammar, input, and starting point are equal (Theorem 4.4, Section 4.4, p. 8). The paper concludes from these results that the tree produced by the parser is the only one possible for that grammar and input (Section 4.4, p. 8; Section 5.4, p. 10). Inference: this is what makes a tree usable as a certificate.

Inference: a Verus AST can use a Rust enum plus ghost start/end indexes and a well_formed predicate. Each parser branch returns an AST whose ensures state grammar fidelity, input fidelity, bounds, and success/failure classification. The tree is an executable proof certificate if the ghost fields are erased or kept only for validation. Verus lacks PVS dependent subtype syntax, so local constructor lemmas must replace the paper’s typed output comprehensions.

technique: reference parser interpreter

The reference parser parsing takes a well-formed production map, current nonterminal, grammar node, input array, bound, current index, and the index at nonterminal entry. Its output type restricts ASTs to those that are true to grammar and input and preserves the P⊥, P0, and P>0 properties (Section 5.1, pp. 9–10). The paper gives executable cases. A sequence parses the first child, skips the second on failure, and otherwise parses the second from the first child’s end. Prioritized choice parses the second child only after first-child failure. Star parses its body, then parses the star again from the body’s end if the body succeeded, and stops with a non-consuming skip if the body failed. Not-predicate parses its child but returns a non-consuming node.

Termination uses the lexicographic tuple (b − sT, b − s, A, |G|). The paper explains that recursion either descends in the grammar, moves to a lower nonterminal, consumes input in a star, or moves from a higher nonterminal only after at least one token was consumed (Section 5.2, pp. 9–10). It proves the parser satisfies the PEG parsing rules by expanding each case and proving local lemmas such as the prioritized-choice and not-predicate lemmas shown in Figure 8 (Section 5.3, p. 10; Figure 8, p. 11). The paper says the full set of rules is proven in the implementation.

Inference: implement the reference parser as a recursive Rust function over an immutable input slice and grammar. Use a decreasing ghost rank or a fuel argument corresponding to the paper’s lexicographic measure. For practical Rust recursion limits, an iterative implementation can be proved equivalent to the recursive specification. Every branch should return a typed result carrying the AST and end index, with ensures preserving the parser rules.

technique: packrat memoization

Packrat parsing removes repeated nonterminal calls by memoizing each pair of nonterminal and input position. The paper’s complexity argument is: “Searching for a pattern A at a starting position s is independent from previously done parsing, it only relies on A and s.” (Section 6.1, p. 11.) With at most n patterns and b positions, storing each result yields at most b × n calls, hence O(b × n) time (Section 6.1, p. 11). The paper assumes each recursive call takes constant time and notes in footnote 12 (pp. 11–12) that in the reference parser the astType function makes this non-constant, fixable by having the parser also output the tree type.

The memo table uses unknown and known(T) constructors. Its dependent result type stores a tree only when it equals the reference parser called with the same grammar, input, nonterminal, and start position (Section 6.2, pp. 11–12). On a nonterminal call, the packrat parser returns the stored tree when known; otherwise it computes the reference-equivalent tree and updates the table. The packrat output is a pair of AST and table, and the type requires every stored result to satisfy the reference-parser equation (Figures 9, 10 and 11, pp. 11–12).

Inference: Verus can implement the table as a Map<(Nonterminal, usize), ParseResult> or a bounded vector and prove a cache-hit lemma: a known entry equals the specification result, so returning it preserves the parser contract. Mutable borrowing requires a carefully stated map invariant; ghost snapshots or a separate immutable specification table can connect the executable cache to the reference function. The paper’s linear-time bound assumes finite grammar and bounded input; it does not cover allocation cost or hash-map implementation details.

technique: semantic compacting

The full AST is useful as a proof object but cumbersome as an application result. The extension adds semantic and fail constructors. A user supplies a semantic interpretation function for nonterminal trees, and s_inp recursively replaces nonterminal subtrees by semantic values while replacing failure subtrees with fail (Sections 7.1–7.2, pp. 12–13; Figure 13, p. 13). The resulting semantic tree preserves start/end indexes, success/failure, star and skip structure, and well-formedness (Figure 13). The paper says the operation may be applied to a full tree or on the fly while parsing, and that the full-tree version is used only to prove equivalence with the reference parser (Section 7.2 and footnote 14, p. 12).

Because compacted trees are not syntactically equal to reference trees, equivalence is defined by three conditions: unchanged non-fail/non-semantic nodes are equal; each fail(s,e) corresponds to a reference failure ending at e; and each semantic node equals the semantic interpretation of the corresponding reference subtree (Section 7.3, p. 13). In the arithmetic example run in PVSio (Section 7.3 text, p. 13; Figure 15, p. 14), the input parses to semantic (0 , 11 , 8 , add ( mult ( v (1) , v (2) ) , sub ( v (3) , div ( v (4) , v (5) ) ) ) ), changing the + at index 3 to - yields sub at the root, and setting index 1 (the second character) to -3 gives fail (0 ,1). The paper’s text writes the input as 1+2∗(3−4/5) while Figure 15 prints 1*2+(3 -4/5); the two disagree with each other.

Inference: in Verus, define a semantic result enum and prove a refinement theorem from the full parser result to the compact result. Keep a ghost full AST for proof if memory matters, and execute only compact values. Semantic actions should be pure specification-linked functions or separately verified Rust functions; otherwise the parser proof ends at syntax and does not establish the action’s meaning.

evidence, scope, and product threat

The paper reports formal PVS proofs and executable interpreters, but no benchmark denominator, runtime table, or parser corpus evaluation. It explicitly lists empirical performance studies and efficient data structures as future work (Conclusion, p. 14). The demonstrated arithmetic parser is a hand-built example, not evidence over production grammars. The proved results the paper claims are termination for well-formed PEGs, satisfaction of the parsing rules, uniqueness, completeness and soundness, packrat equivalence to the reference parser, and semantic-parser equivalence to the reference parser. Inference: trusted elements include PVS’s type checker and proof kernel, the formalized input and grammar models, and any semantic action supplied by the user unless separately proved.

Inference: the threat to VeruLaw is moderate for agent-generated parsers. A generated parser can be made auditable if it emits a grammar well-formedness proof, an AST certificate, and a cache-equivalence proof. The main risks are grammar changes that invalidate termination ranks, semantic actions whose contracts are too weak, and mismatch between byte-level model and Rust string handling. The paper already solves the core reference-versus-optimized-interpreter pattern; VL should measure maintenance and Rust integration rather than claim that memoization verification itself is new.

techniques for the catalog

• grammar property fixpoint: compute failure, nullable success, and consuming success facts to a coherent bounded fixpoint
• well-formed PEG checking: reject nullable repetition and unranked left recursion with structural and nonterminal-order checks
• proof-carrying parse trees: encode input bounds, grammar fidelity, and success or failure in an AST type
• lexicographic parser termination: prove recursive calls decrease grammar size, nonterminal rank, or remaining input
• packrat refinement: memoize (nonterminal, position) results while typing each cache entry as reference-parser equivalent
• semantic tree compaction: replace verified subtrees with semantic values and failures with compact failure nodes under an equivalence relation Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “To prove that well-formed trees actually correspond to parsing of a given input given a grammar, we introduce two notions.”): read the whole paper (PDF text, pages 1-15) and checked every quotation, number, section and page reference and technique step; changed page and section references (P≥0 definition p. 4, well-formedness p. 6, pre-AST sections, Theorem 4.3 title, Figure 8 on p. 11), the abstract quote extension, the nondecreasing wording, the star rule description, the arithmetic example (index 1 is the second character, and the paper’s text and Figure 15 disagree on the input), the constant-time caveat of footnote 12, the user-supplied nonterminal order of footnote 5, and marked trusted-element and certificate remarks as Inference; did not check the PVS code on GitHub, the cited related work, or the proofs themselves.

Last edited: 2026-10-17