LeanMenhir

A formally verified LR(1) parser interpreter + validator for Lean 4, ported from coq-menhirlib (the verified parser library Menhir emits for Coq/CompCert), plus a self-contained, untrusted native LR(1)/SLR(1) table generator.

The key idea

The LR table generator is untrusted. Separate verified validators (isSafe for soundness, isComplete for completeness) check that generated tables are consistent with a grammar, and a verified interpreter runs validated tables. Soundness, completeness, and unambiguity all hold whenever the validators accept — regardless of bugs in the generator — so nobody has to verify the large, fiddly LR table-construction algorithm itself.

Guarantees

All stated and axiom-guarded in LeanMenhir/Guarantees.lean (see docs/AUDIT.md for the full reviewer's guide):

• Soundness (parser_sound) — if parse returns Parsed, the consumed input really is a word of the language, and the returned value is the semantics of a real derivation.
• Completeness (parser_complete, parser_accepts, parser_never_rejects_valid) — every derivation of the grammar is found by the parser (given enough fuel), and a word of the language is never rejected.
• Unambiguity (grammar_unambiguous) — any two derivations of the same word have the same semantic value.
• Exact consumption / EOF anchoring (parser_consumes_exactly) — for an EOF-anchored grammar and an EOF-free lexer, acceptance means the whole input was parsed, nothing else.
• runtime_sound / runtime_complete / runtime_consumes_exactly transfer all of the above to the executable driver Runtime.parseList.

Every one of these theorems is followed by a #guard_msgs-checked #print axioms call, so a sorry or a stray axiom is a build failure, not a silent regression.

Directory layout

LeanMenhir/
  Spec/          grammar/language/input definitions
    Alphabet.lean    Alphabet / Enumerable typeclasses (core `Ord` + `Std.TransOrd`/`Std.LawfulEqOrd`)
    Grammar.lean     symbols, the Grammar interface, dependently-typed ParseTree
    Language.lean    Derives / `word ∈ language nt` (existence of a derivation)
    Buffer.lean      O(1) head/tail token buffer and its denotation `get`
  Machine/       the LR automaton and interpreter
    Automaton.lean   the LR automaton table interface (states, actions, tables)
    Interpreter.lean pop / reduceStep / step / parse (fuel-based), no `sorry`
  Correctness/   the ported/extended proofs
    Classes.lean     validator boolean/Prop plumbing
    Safe.lean        safety validator `isSafe` + soundness lemma
    Complete.lean    completeness validator `isComplete` + soundness lemma
    Sound.lean       soundness proof of the interpreter
    CompleteProof.lean completeness proof of the interpreter
    Congr.lean       interpreter extensionality in the input buffer
    Anchored.lean    EOF-anchoring and exact-consumption
  Generator/     the untrusted native LR(1)/SLR(1) generator
    FinAlphabet.lean Alphabet instances for Fin n (generator index types)
    Tables.lean      bridge from untrusted GenTables to a genuine Automaton
    Grammar0.lean    the human-written grammar and its definitional Grammar
    Derives0.lean    the textbook Grammar0.Derives spec + transport theorem
    LR1.lean         canonical LR(1) / SLR(1) table construction
    BuildTables.lean the `build_tables%` elaborator (builds tables at elab time)
    BTree.lean       balanced BST for kernel-reducible O(log n) table lookups
  Examples/      end-to-end example grammars (see below)
  Main.lean      user-facing entry points: `parse`, `parse_correct`,
                 `parse_complete`, `unambiguity`
  Runtime.lean   grammar-agnostic executable driver: pads a token list into a
                 buffer, runs `Main.parse`, maps the result into `Except`
  Guarantees.lean  the review surface: every end-to-end theorem restated with
                   an informal reading, its caveats, and an axiom guard

Building

lake build

Toolchain: leanprover/lean4:v4.31.0 (see lean-toolchain).

Examples

LeanMenhir/Examples/ is a three-part tutorial, meant to be read in order, plus one regression test:

Example	What it shows	Certificates
CoreDatatypes.lean	the specification layer. A Grammar written by hand, field by field; why a ParseTree is correct by construction (an ill-formed tree fails to elaborate — checked with #guard_msgs); why nothing at this layer prevents ambiguity; ptSem; and Derives / word ∈ G.language nt. Mentions no automaton, table, or certificate.	none needed
ByHand.lean	the machine layer, no generator. An Automaton for that same grammar written out by hand — six states, action/goto tables, and all three validator annotations — with Safe/Complete discharged by kernel decide. The guarantees therefore become unconditional theorems about a parser you can run.	kernel decide
Generated.lean	how a frontend uses the generator. Laid out in the order BNFC's --leanmenhir backend emits its four modules. Two distinct AST categories (Stm/Exp) exercise the heterogeneous semantic bridge; build_tables% supplies untrusted tables; and a review surface presents the productions readably and proves the presentation equals prod_lhs/prod_rhs_rev, so the generator, the table blob, and the lifting functions need not be trusted or even read.	kernel rfl + decide
ScaleTest.lean	a 21-production regression test for the dependent-action-dispatcher scaling wall (O(log n) BTree lookups, the Fin-literal exhaustiveness workaround). Not a tutorial.	kernel rfl

Generated also proves that its verified language is exactly the textbook Grammar0.Derives relation on the grammar you wrote (language_eq), and that the grammar is EOF-anchored (eof_anchored).

Dependencies

Core Lean 4 and Std only — no Mathlib.

Trust and axioms

The end-to-end guarantees depend on at most Lean's three standard axioms, propext, Classical.choice, and Quot.sound — no sorry, no custom axioms. Every theorem in Guarantees.lean carries a #guard_msgs-checked #print axioms call enforcing this at build time.

A grammar's own safety/completeness certificates can be discharged either way:

• kernel decide/rfl on concrete tables — the Lean kernel is the only trusted component; every example in this repository takes this path;
• native_decide — compiles the validator and tables to machine code and runs them, which scales to much larger grammars but adds Lean.ofReduceBool (trust in the compiler) to that certificate's axiom list. BNFC's generated parsers use this by default and take the kernel path under --leanmenhir-kernel-certs.

Note that a grammar never rests on compiler trust either way: the proof tying the verified grammar to the productions you wrote is always kernel rfl, so only the automaton's safety/completeness certificates are affected by the choice.

License

LGPL-3.0-or-later (derivative of coq-menhirlib, © Inria/CNRS).