Bounded-exhaustive verifier for parser vs documented grammar (pest + EBNF) drift #643

Summary

Add a deterministic, bounded-exhaustive verifier that catches drift between the real Datalog parser (src/query/datalog/parser.rs) and the documented grammar (tests/grammar/grammar.pest and the EBNF in the docs site's content/datalog-reference.md).

This follows the idea in #627 (check a property for every input up to a bound, run the deeper bound on a schedule), but as a plain cargo test that enumerates inputs, not Kani: model-checking pest's generated parser over symbolic strings is not practical.

It extends the grammar conformance harness from #233. That harness checks a hand-picked .edn corpus. It passes on main (v2.0.8) and v3, yet an audit on 2026-10-20 found the drift listed below on both branches, because no corpus file covers those inputs.

Property

For every input up to the bound:

• pest rejects ⇒ the parser rejects.
• pest accepts ⇒ the parser accepts, or rejects with a semantic error code (one listed in the reference's "Semantic Constraints" section).

Design

Layer 1: lexical (exact agreement)

• Every string of up to 3 characters over: printable ASCII, \t, \n, \r, and a few non-ASCII stand-ins (é, 名, ٣, U+00A0). About 1M strings.
• Each goes through pest's edn_value rule and the parser's parse_edn; acceptance must match exactly.
• Lives as a #[cfg(test)] unit test beside parser.rs (pest is already a dev-dependency), so it reaches parse_edn directly with no semantic layer in the way.

Layer 2: structural (token sequences)

• Token sequences placed into fixed templates: (query [ _ ]), (transact [[ _ ]]), (transact { _ } [[ _ ]]), (retract [[ _ ]]), (rule [( _ ) _ ]), and clause holes inside :where, not, not-join, or, or-join, and, :over.
• About 25 token stand-ins: brackets, command and clause heads, :find :where :with :as-of :valid-at :any-valid-time :over :partition-by :order-by, an unknown keyword :foo, ?x, foo, 1, 1.5, "s", <, -, $s, #uuid "…", { }.
• Only bracket-balanced sequences are generated, shortest first, so the first reported failure is minimal.
• Deterministic: fixed alphabet, fixed bound, fixed order, no randomness.

Bounds and CI

• Small bound in the normal test run (target: under a minute).
• Deeper bound in a scheduled workflow, alongside soak.yml.
• The first PR measures run time and sets both bounds from the numbers. The sizes above are estimates.

EBNF: generate, don't verify

Make grammar.pest the single source of truth:

• A small renderer turns grammar.pest into the EBNF text.
• The docs site renders the EBNF from each tag's grammar.pest, the same way it already reads CHANGELOG.md and docs/ERROR_REFERENCE.md per tag (minigraf-docs PR).

Translating a hand-written EBNF back to a PEG for comparison isn't exact (EBNF choice is unordered), so it isn't planned.

Prerequisites

1. Classify parser errors as syntax vs semantic. parser.rs has 28 INT-019 call sites on both main and v3, used for both kinds of error (for example "Rule head must be a list" vs "':order-by' is required in the ':over' clause"). Give them their own PRS codes so the classification isn't guesswork. INT-019 stays registered (codes are never removed or recycled).
2. Known-drift list. The verifier fails on both branches today. Land it with an explicit KNOWN_DRIFT list of inputs that must keep disagreeing. Each fix PR removes its entries, so fixes and the list can't silently disagree.

Initial known drift (both main and v3)

Parser accepts, pest and EBNF reject

Parser bug the grammar doesn't catch

A fact [e a v {map} extra…] is accepted and everything after the 4th element is silently dropped (parse_transact only checks fact_vec.get(3)). (transact [[:alice :a 1 {…} 99 :junk]]) succeeds. The EBNF says 3 elements plus an optional map; pest's fact = edn_value+ is deliberately loose. Silent data loss, so this should be fixed as a bug with its own PRS code.

EBNF vs grammar.pest

• pest allows op_sym (<, +, …) as a value, an aggregate name ((+ ?x), which the parser accepts) and a one-argument function name; the EBNF's symbol excludes operators.
• pest and the parser accept any character after \ in strings ("\q" → q); the EBNF lists only \n \t \r \" \\.
• The EBNF whitespace note omits \r; neither grammar mentions comments.
• The EBNF has no word boundary after true/false/nil (pest uses !word_cont), so trueish is ambiguous.

Word boundaries on literal keywords in grammar.pest

pest matches literal keywords such as ":find" with no end-of-word check, so [:find?e …] parses in pest as :find ?e. The tokenizer reads it as one unknown keyword :find?e followed by an empty :find. Both accept only by coincidence. Same for ":where", ":with", etc.

Suggested plan

• Split the INT-019 sites in parser.rs into syntax / semantic PRS codes (v3 first, backport to main).
• Add the verifier with the KNOWN_DRIFT list (v3 first, then main); measure and set PR / scheduled bounds.
• Add the pest → EBNF renderer; switch minigraf-docs to render the EBNF per tag.
• Fix the drift, each PR removing its KNOWN_DRIFT entries. The 5+ element fact is the data-integrity one (v3 first, backport to main); the other parser tightenings change accepted input, so they belong in v3.

Related

• Explore formal verification of storage encoding with Kani #627: Kani bounded verification of storage encoding (same bounded-exhaustive approach)
• [FEATURE] EBNF grammar specification and semantics documentation #233: EBNF grammar specification and the grammar conformance harness

🤖 Generated with Claude Code

https://claude.ai/code/session_019kY61Y11gcRD91Y6b7jbGT