verus: parser idempotence (parse ∘ print ∘ parse == parse), three phases

[kiranandcode]

Stacked on #15. This proves parser idempotence at the token level: re-printing what you parsed and parsing that again lands exactly where the first parse did.

The roundtrip work in #15 fixes one direction, parse(print(a)) == a for a printable AST a. This branch adds the complementary, input-driven property:

for every token sequence toks,
if parse(toks) = Some(a) then parse(print(a)) = parse(toks).

i.e. parse ∘ print ∘ parse == parse, over both the expression grammar and the full statement grammar, axiom-free.

Three phases

The proof composes three phases, all in src/sql/parser/verified_idempotence.rs:

• Phase 1, the parse image is printable. A successful parse yields a printable AST. This is the new work: bottom-up image lemmas over every sub-parser (columns, the FROM join tree, assignments, select items, rows, order lists, the SELECT clauses), each recovering the parser's own structural guarantees (is_stable right children, CROSS/predicate coupling, list len >= 1) from the parse itself. Embedded expressions reuse the expression-level image lemma.
• Phase 2, the printer right-inverts. printable(a) ==> parse(print(a)) = (Some(a), []). This is the existing roundtrip lemma, reused verbatim.
• Phase 3, idempotence. Compose the two.

The finite-float fragment

Phase 1 is not universally true, and the reason is worth stating plainly. The headlines carry a guard, finite_floats / finite_floats_stmt, and it is the tightest honest precondition rather than a proof convenience. Two things carve it out, and they are different in kind.

Overflow floats are a genuine non-printability. A number token like 1e400 parses to Float(inf), and literal_views(Float(inf)) is None. An infinite float has no canonical print, so there is nothing to reparse.

Aliased * is a domain guard, not a printer limitation. SELECT * AS a parses to (All, Some("a")), which printable_select_item rejects. But * AS a prints and reparses back to itself, so it roundtrips. The clause sits in the printable predicate because the canonical select grammar does not alias *, as SQL does not, and it is load-bearing here only because Phase 3 routes through printable_stmt.

On the finite-float fragment, which is all real SQL, the guard is discharged and idempotence holds unconditionally.

Result

lemma_parse_idempotent_expr_finite and lemma_parse_idempotent_stmt_finite state the headline: parse(print(a)) == parse(toks) with the natural finite_floats guard in place of the opaque printable. verify.sh stays green across all 19 modules; the idempotence module is 53 verified, 0 errors. No assume, admit, or external_body; the trust surface is unchanged.

🤖 Generated with Claude Code