diff --git a/docs/superpowers/specs/2026-10-20-grammar-drift-verifier-design.md b/docs/superpowers/specs/2026-10-20-grammar-drift-verifier-design.md new file mode 100644 index 000000000..5f6caa0d6 --- /dev/null +++ b/docs/superpowers/specs/2026-10-20-grammar-drift-verifier-design.md @@ -0,0 +1,290 @@ +# Parser vs documented grammar: a bounded-exhaustive verifier — Design + +**Issue:** #643 +**Milestone:** v3.0.0, branch `v3`; a test-only backport to `main` (§8) +**Builds on:** the grammar conformance harness (#233, +`2026-05-08-grammar-conformance-design.md`); the bounded approach of #627 + +## 1. Scope + +Three documents describe the Datalog syntax: the real parser +(`src/query/datalog/parser.rs`), the shadow grammar (`tests/grammar/grammar.pest`), and +the EBNF on the docs site (`content/datalog-reference.md` in minigraf-docs). The #233 +harness checks a hand-picked corpus, and an audit on 2026-10-20 found drift on both `main` +and `v3` that no corpus file covers (listed in #643). This work: + +- re-codes the parser errors that share `INT-019` (or fall to `INT-000`) so every + user-facing parse error has its own code (§3); +- adds a verifier that checks the parser against `grammar.pest` for every input up to a + bound, deterministically (§4–§6); +- makes `grammar.pest` the only hand-written grammar: the EBNF is generated from it (§7). + +Fixing the drift itself is out of scope. Each fix is its own PR afterwards and removes its +known-drift entry (§5.3). + +Settled with the maintainer on 2026-10-20: + +1. **The syntax/semantic classification of error codes is test-only** (§4.2): a list in + the verifier, not a public `ErrorCode` method. +2. **The EBNF is a generated file in this repo** (§7): `docs/GRAMMAR.md`, rendered from + `grammar.pest`, checked for staleness by a test, and published by the docs site as a + snapshot page like `docs/ERROR_REFERENCE.md`. +3. **`main` gets the verifier only** (§8): no new error codes on v2.x. + +## 2. Terms + +- **pest accepts `s`**: `grammar.pest`'s rule parses all of `s` (the rule is wrapped in + `SOI ~ … ~ EOI`). +- **The parser accepts `s`**: the parse entry point returns `Ok` (§4.1). It does not run + anything, so errors raised only while executing (for example `INT-003`, "Cannot convert + Symbol to Value") are not parser rejections. +- **Syntax code / semantic code**: an error code is *semantic* when an input that + `grammar.pest` is meant to accept can raise it: the rules in the reference's "Semantic + Constraints" section, value checks (UUID, timestamp, regex), resource limits (length, + range, depth), and arity or shape checks that `grammar.pest` deliberately leaves loose + (for example `fact = { "[" ~ edn_value+ ~ "]" }`). Every other parse error code is a + *syntax* code. +- **Drift**: an input on which the verifier's property (§4) fails. + +## 3. Error codes + +### 3.1 Sites that move off `INT-019` and `INT-000` + +`parser.rs` on `v3` raises `INT-019` ("Datalog parser internal error") at 28 sites. Four +of them cannot be reached from input and stay `INT-019`: + +| Line (v3, 2026-10-20) | Message | +|---|---| +| 739 | `:as-of counter must be non-negative` (guarded by `n >= 0` just above) | +| 1018 | `internal error: is_map() true but as_map() returned None` | +| 1303 | `parse_expr_clause called with empty vector` | +| 1310 | `parse_expr_clause called with non-list element 0` | + +The other 24 are user errors and each gets a new `PRS` code, numbered from `PRS-083` in +source order. The plan lists the numbers. The class each will have: + +| Message (abridged) | Class | Why | +|---|---|---| +| Bind slot `$` must be followed by an identifier | syntax | `bind_slot` needs one character | +| `:order-by` is required in `:over` | semantic | `over_option*` allows none | +| Query argument must be a vector | syntax | | +| `:with` accepts only variables | syntax | | +| Expected variable or aggregate in `:find` | syntax | | +| Unknown key in valid-time map | semantic | reachable through a per-fact map, which `fact` leaves loose | +| Each fact must be a vector (retract) | syntax | | +| Invalid regex pattern | semantic | value check | +| Expected pattern or rule invocation inside `(not)` | syntax | | +| `(not-join)` inside `(not)`/`(not-join)` | semantic | nesting rule in Semantic Constraints | +| `(not-join)` first argument must be a vector | syntax | | +| `(not-join)` join variables must be logic variables | syntax | | +| Expected pattern or rule invocation inside `(not-join)` | syntax | | +| Rule invocation must start with a symbol | syntax | | +| Pattern must have exactly 3 elements | syntax | `pattern_clause` is exactly 3 | +| Expected clause inside or branch | syntax | | +| Rule must have a body | syntax | | +| Rule body must be a vector | syntax | | +| Rule body cannot be empty | syntax | `rule_vector` needs a head | +| Rule head must be a list | syntax | | +| Rule head cannot be empty | syntax | | +| Rule head must start with a symbol | syntax | | +| Rule body clause must be a vector or list | syntax | | +| Rule must have at least one clause in its body | semantic | `rule_vector` allows `where_clause*` | + +`retract`'s fact arity error comes from `Pattern::from_edn` as a plain string and is +reported as `INT-000` (`parser.rs:1156`). It gets a new `PRS` code, class semantic (the +loose `fact` rule accepts any arity; the corpus file `retract_wrong_arity.edn` is already +in `invalid/semantic/`). + +### 3.2 What does not change + +- `INT-019` stays registered for the four unreachable sites; no code is removed or + recycled. +- The other `INT` codes the parser raises (`INT-006`–`INT-018`) each have one meaning, so + the verifier can classify them as they are. Re-coding them to `PRS` is out of scope. +- Message text stays the same; only the code changes. Each new code gets a row and a + section in `docs/ERROR_REFERENCE.md` and a test in `tests/error_codes_prs_test.rs`. +- The UniFFI bindings' `v3` branches map core error codes; a new `ErrorCode` variant may + need a binding update (cascade check after merge). + +## 4. The property + +### 4.1 Oracles + +| Level | pest rule | Parser entry point | +|---|---|---| +| Lexical (§5.1) | new `edn_value_only = { SOI ~ edn_value ~ EOI }` | `parse_edn` | +| Structural (§5.2) | `command` | `parse_datalog_command` | + +Both parser functions are crate-internal, so the verifier is a unit test module: +`src/query/datalog/parser/verifier.rs`, declared as a module in `parser.rs` (the +`aggregate.rs` / `aggregate/tests.rs` pattern; the cfg is in §5.4). `pest_derive` finds +`tests/grammar/grammar.pest` relative to `CARGO_MANIFEST_DIR`, as the #233 harness does. `pest` and `pest_derive` are already +dev-dependencies. + +### 4.2 Statement + +For every generated input `s`: + +1. pest rejects `s` ⇒ the parser rejects `s`; +2. pest accepts `s` ⇒ the parser accepts `s`, or rejects it with a semantic code. + +The semantic codes are a `const` list in the verifier. Two rules keep the list narrow: + +- **Witness.** Each entry carries an input that pest accepts and the parser rejects with + exactly that code, and a test checks every witness. A code cannot sit in the list + without proof that the grammar accepts something that raises it. +- **One meaning per code.** A witness proves only that *one* site of a code is semantic. + If a code had a syntax site too, listing it would exempt both, and the syntax drift + would go unseen. So every site that raises a listed code must be semantic. Codes raised + at more than one site (for example `INT-018`, `PRS-080`) list each site, with the + reason, in a comment beside the entry. The plan reviews every site of every listed + code. + +Clause 1 needs no classification: whenever pest rejects, the parser must reject, with +any code. So a code reached both from inputs pest accepts and from inputs it rejects is +still one meaning when every pest-accepted path is semantic. The valid-time map key check +(§3.1) is such a code: pest rejects an unknown key in the transaction-level map and +accepts it in a per-fact map, which `fact` leaves loose. + +## 5. Generated inputs + +All generation is deterministic: fixed alphabets, fixed templates and fixed bounds, with +no randomness. Each level orders its inputs by length, then lexicographically by +alphabet position. Length is the character count at the lexical level and the token count +at the structural level (per template). The first failure reported is therefore a +smallest one *within its level and template*; the two levels are not compared. + +### 5.1 Lexical level + +Every string of length 1 to 3 over: + +- printable ASCII (`0x20`–`0x7E`), `\t`, `\n`, `\r`; +- non-ASCII stand-ins: `é`, `名`, `٣` (Arabic-Indic digit), U+00A0. + +That is 102 characters, about 1.07M strings. This level covers comments, Unicode +letters, the bare `:`, the lone `-`, number forms and string escapes. + +### 5.2 Structural level + +Templates with holes, each hole filled by every balanced sequence of up to `k` tokens +from a fixed token alphabet: + +- 12 templates: `(query [ _ ])`, `(transact [ _ ])`, `(transact { _ } [ _ ])`, + `(retract [ _ ])`, `(rule [ _ ])`, and a clause hole inside `:where`, `(not _)`, + `(not-join [?x] _)`, `(or _)`, `(or-join [?x] _)`, `(and _)` and `:over ( _ )`, each + inside an otherwise valid query; +- 32 tokens: 6 brackets, `(` `)` `[` `]` `{` `}`; 7 heads, `query` `transact` `rule` + `not` `not-join` `or` `and`; 10 keywords, `:find` `:where` `:with` `:as-of` `:valid-at` + `:any-valid-time` `:over` `:order-by` `:valid-from` and an unknown `:foo`; 9 others, + `?x` `?y` `foo` `1` `1.5` `"2024-01-01T00:00:00Z"` `<` `$s` + `#uuid "550e8400-e29b-41d4-a716-446655440000"`. + +**Balanced** means the bracket tokens, read alone, form a well-nested sequence of the +three kinds: no closer without an open bracket of its kind on top of the stack, and none +left open at the end. Unbalanced fillers are not generated: their only outcome is +"both reject" (`PRS-003`/`PRS-004`/`PRS-005`/`PRS-006`), which the lexical level and the +#233 corpus already cover. + +Tokens are joined with one space. Gluing (`:find?e`) is the lexical level's job. + +Cost: with 26 non-bracket tokens and 3 bracket kinds, the balanced sequences of up to `k` +tokens number 18,516 for `k = 3`, 487,678 for `k = 4` and 12,898,674 for `k = 5`. Over 12 +templates that is about 0.22M, 5.9M and 155M inputs, each parsed twice (pest and parser). + +### 5.3 Known drift + +Drift that exists when the verifier lands is listed in `KNOWN_DRIFT`. An entry is an id, +the issue that tracks it, and a predicate over the input (for example "contains `;`" or +"contains a non-ASCII character"), because one drift shows up in many generated inputs. + +- Every failing input must match **exactly one** entry. No match fails the test and prints + the input; two matches fail it and name both entries, so overlapping predicates cannot + hide each other or claim unrelated failures. +- Every entry must match at least one failing input, or the test fails and names the + entry. A fix PR therefore has to remove its entry. +- On failure the test reports, per entry, how many inputs it matched and the first one. + +The initial entries are the drift in #643 that the generated inputs reach. + +### 5.4 Bounds and CI + +- The lexical level always runs in full. +- The structural bound `k` comes from `MINIGRAF_GRAMMAR_BOUND`, with a small default for + the normal `cargo test` run. +- A scheduled job runs a deeper bound. Scheduled workflows run from the default branch, + so the job picks its branch from the cron entry, as `soak.yml` does: one cron for + `main`, one for `v3`. It is a shared CI change, so it lands on both branches as + separate PRs. +- Targets: under a minute in a debug `cargo test` by default; under 30 minutes for the + scheduled bound. Tests run in the debug profile (the release profile's `panic = "abort"` + breaks `cargo test --release`). The starting points are `k = 3` by default and `k = 4` + scheduled (§5.2); the first implementation PR measures the time per input and sets both + values, `k = 5` scheduled if it fits. +- The module is `#[cfg(all(test, not(target_arch = "wasm32")))]`. `wasm.yml` runs + `cargo test --target wasm32-wasip1 --lib --tests` under Wasmtime, and the parser is the + same code on every target. + +## 6. Relation to the #233 harness + +`tests/grammar_conformance.rs` and its corpus stay. The corpus pins named, readable +examples, and `db.execute`/`db.prepare` cover the full path. The verifier covers +everything small. A failure the verifier finds and a fix closes can also get a corpus +file. + +## 7. The EBNF + +### 7.1 Renderer + +A test, `tests/grammar_doc.rs`, reads `grammar.pest` with `pest_meta` (already in the +dependency tree through `pest_derive`; added as a dev-dependency) and renders EBNF: + +- `a ~ b` → `a b`; `|`, `*`, `+`, `?`, grouping and string literals unchanged; +- rule names from `snake_case` to `kebab-case`; `SOI`, `EOI` and the `_{}`, `@{}`, `${}` + modifiers dropped; +- `ASCII_DIGIT` → `digit`, `ASCII_ALPHA` → `letter`, `ASCII_ALPHANUMERIC` → + `letter | digit`, `ANY` → `any-char`; +- `!x` (negative lookahead, which EBNF lacks) → an EBNF comment, `(* not followed by x *)`; +- `WHITESPACE` → the note on which characters separate tokens; +- grammar comments that start a section (`// ── … ──`) → section comments. + +The test compares its output with `docs/GRAMMAR.md` and fails when they differ. Running it +with `UPDATE_GRAMMAR_DOC=1` rewrites the file. + +### 7.2 Docs site + +- minigraf-docs adds a `[[snapshot]]` page for `docs/GRAMMAR.md` (Reference section), + `since = "v3.0.0"`. +- In `content/datalog-reference.md`, the hand-written EBNF is wrapped in + ``, with a link to the generated page under + ``. +- The v2.x EBNF stays hand-written, and that docs PR corrects the four mismatches with + `grammar.pest` that #643 lists. + +## 8. Backport to `main` + +`main` gets the verifier only: no new codes and no `docs/GRAMMAR.md`. `INT-019` still +mixes syntax and semantic errors there, so on `main` the verifier counts `INT-019` (and +`INT-000`) as semantic. Clause 1 of §4.2 is checked in full. Clause 2 is weaker: a syntax +error coded `INT-019` that pest accepts is not caught. The v2.x `KNOWN_DRIFT` list starts +as the same list as v3. + +## 9. Pull requests + +1. This spec (`v3`). +2. Error codes, §3 (`v3`). +3. The verifier, §4–§6 (`v3`). +4. Renderer and `docs/GRAMMAR.md`, §7.1 (`v3`), and the minigraf-docs PR, §7.2. +5. The verifier backport, §8 (`main`). + +Then the drift fixes, each removing its `KNOWN_DRIFT` entry. The 5+ element fact (#643) +silently drops data, so it goes to `v3` and is backported to `main`. The other fixes +change which input is accepted and stay on `v3`. + +## 10. Deviations from #643 + +- #643 proposed checking "pest rejects ⇒ parser rejects" and "parser accepts ⇒ pest + accepts" on `main` as two directions. They are the same statement. On `main` the + verifier checks it in full and checks clause 2 in the weaker form of §8. +- #643's lexical level compared acceptance exactly. Pest accepts some inputs the parser + rejects on value checks (an invalid UUID, `PRS-072`; an out-of-range integer, + `INT-008`), so the lexical level uses the same two clauses as the structural one.