adityamukho · Oct 20, 2026 · Oct 20, 2026 · Oct 20, 2026
@@ -0,0 +1,99 @@
+name: Grammar verifier (nightly)
+
+# Two branches, 12 hours apart: main at 05:30 UTC, v3 at 17:30 UTC.
+# Scheduled runs always use this file from the default branch, so the branch
+# under test is chosen from the cron string that fired (as in soak.yml). Keep
+# the cron strings here and in VERIFIER_REF/run-name identical.
+run-name: >-
+  Grammar verifier (${{ github.event_name == 'workflow_dispatch' && inputs.ref
+  || (github.event.schedule == '30 17 * * *' && 'v3' || 'main') }})
+
+# #643: checks the parser against tests/grammar/grammar.pest on every input up
+# to a bound (src/query/datalog/parser/verifier.rs). `cargo test` runs the
+# structural level at k = 3; this job runs k = 4 (~22 CPU-minutes, ~6 minutes
+# on 4 cores).
+
+on:
+  schedule:
+    - cron: "30 5 * * *"   # main
+    - cron: "30 17 * * *"  # v3
+  workflow_dispatch:
+    inputs:
+      ref:
+        description: Branch to test
+        required: true
+        default: main
+      bound:
+        description: Structural bound k (MINIGRAF_GRAMMAR_BOUND)
+        required: true
+        default: "4"
+
+permissions:
+  contents: read
+  issues: write
+
+env:
+  VERIFIER_REF: ${{ github.event_name == 'workflow_dispatch' && inputs.ref || (github.event.schedule == '30 17 * * *' && 'v3' || 'main') }}
+  MINIGRAF_GRAMMAR_BOUND: ${{ github.event_name == 'workflow_dispatch' && inputs.bound || '4' }}
+
+jobs:
+  verifier:
+    name: Grammar verifier
+    runs-on: ubuntu-latest
+    timeout-minutes: 60
+
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          ref: ${{ env.VERIFIER_REF }}
+
+      - name: Install Rust stable
+        uses: dtolnay/rust-toolchain@stable
+
+      - name: Build
+        run: cargo test --lib --no-run
+
+      - name: Run the verifier
+        shell: bash
+        env:
+          RUST_BACKTRACE: 1
+        run: |
+          set -o pipefail
+          cargo test --lib query::datalog::parser::verifier -- --nocapture 2>&1 | tee verifier-output.txt
+
+      - name: Record verifier failure
+        if: ${{ failure() }}
+        shell: bash
+        env:
+          GH_TOKEN: ${{ github.token }}
+          ISSUE_TITLE: "Nightly grammar verifier failure (${{ env.VERIFIER_REF }})"
+        run: |
+          report_file="verifier-failure.md"
+          {
+            echo "The nightly grammar verifier failed on ${{ env.VERIFIER_REF }}."
+            echo
+            echo "- Run: $GITHUB_SERVER_URL/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID"
+            echo "- Commit: $(git rev-parse HEAD)"
+            echo "- Reproduce: \`MINIGRAF_GRAMMAR_BOUND=$MINIGRAF_GRAMMAR_BOUND cargo test --lib query::datalog::parser::verifier -- --nocapture\`"
+            echo
+            echo "## Test output"
+            echo
+            echo '```text'
+            tail -n 300 verifier-output.txt 2>/dev/null || echo "(no output: the run failed before the test started)"
+            echo '```'
+          } > "$report_file"
+
+          existing_issue="$(gh issue list \
+            --repo "$GITHUB_REPOSITORY" \
+            --state open \
+            --search "$ISSUE_TITLE in:title" \
+            --json number,title \
+            --limit 100 \
+            --jq ".[] | select(.title == \"$ISSUE_TITLE\") | .number" \
+            | head -n 1)"
+
+          if [ -n "$existing_issue" ]; then
+            gh issue comment "$existing_issue" --repo "$GITHUB_REPOSITORY" --body-file "$report_file"
+          else
+            gh issue create --repo "$GITHUB_REPOSITORY" --title "$ISSUE_TITLE" --body-file "$report_file"
+          fi
@@ -11,6 +11,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 - **A fact with more than four elements is rejected** (#649). `transact` read a fact's 4th element as its optional valid-time map and ignored everything after it, so `[[:alice :person/age 1 {} 99 :junk]]` stored `[:alice :person/age 1]` and dropped the rest without an error; two facts run together by a misplaced bracket lost one. A fact of more than four elements now fails with the new `PRS-108`, numbered as in v3.0.0, and the transaction writes nothing. A fact of five or more elements whose 4th is not a map now gets `PRS-108` instead of `PRS-047`. Present since v0.4.0.
 
+### Tests
+
+- **Parser vs grammar verifier (#643), backported from v3.0.0.** `src/query/datalog/parser/verifier.rs` checks, for every generated input, that the parser rejects what `tests/grammar/grammar.pest` rejects, and accepts what it accepts unless the error code is semantic (a listed code with a witness pest accepts). It runs every string of 1 to 3 characters over 102 characters (ASCII, `\t \n \r`, four non-ASCII stand-ins) through `parse_edn`, and every bracket-balanced sequence of up to `MINIGRAF_GRAMMAR_BOUND` (default 3) of 32 tokens in 15 command templates through `parse_datalog_command`, also with no separators up to 3 tokens. Deterministic; about 40 s by default in a debug build. On v2.x `INT-019` still mixes syntax and semantic parse errors (v3.0.0 splits it into `PRS-083`–`PRS-107`), so it counts as semantic here, and a syntax error coded `INT-019` that pest accepts is not caught (v3.0.0 checks that too). The drift it found is the same as on v3 and is listed in `KNOWN_DRIFT` by cause (comments and non-ASCII letters #650; empty sections, ignored keywords, rule and call heads, a lone `:` or `-`, unterminated strings #651; a fact of more than four elements, #649, is fixed above). `grammar.pest` now says what the parser means: a fact is exactly `[e a v]` plus an optional valid-time map and a retracted fact exactly `[e a v]`; `not`, `not-join`, `or`, `or-join` (and `and` inside an `or`) are never rule names; literal keywords end at a word boundary (`:find?x` is one keyword). A nightly workflow, `grammar-verifier.yml`, runs it at bound 4 on `main` and on `v3`, and opens or comments on an issue when it fails.
+
 ## v2.0.8 — 2026-10-20
 
 Patch release on the v2.x line under the [support policy](PHILOSOPHY.md#support-policy): seven data-integrity fixes for queries that silently returned too few or too many rows — `:db/valid-at` in `not-join` bodies (#615) and rule definitions (#617), `or` / `or-join` branches (#620, #625, #637), and rules that call or recurse through a rule with `not`, `not-join`, `or` or `or-join` (#628, #633). File format is unchanged (v7). No API changes. Stored data was never affected. Upgrading is recommended for every v2.x user who uses `or`, `not-join`, `:db/valid-at` or rules with negation or disjunction.

@@ -118,6 +118,7 @@ cargo run < demos/demo_negation.txt
 
 3. **`src/query/datalog/`** — Datalog engine
    - `parser.rs`: EDN/Datalog parser — `transact`, `retract`, `query`, `rule`, `:as-of`, `:valid-at`, `not`, `not-join`
+   - `parser/verifier.rs`: test-only (not wasm32) bounded-exhaustive check of the parser against `tests/grammar/grammar.pest` (#643): every 1–3 character string (`parse_edn`) and every balanced token filler up to `MINIGRAF_GRAMMAR_BOUND` (default 3) in 15 command templates (`parse_datalog_command`); pest rejects ⇒ parser rejects, pest accepts ⇒ parser accepts or raises a `SEMANTIC` code (`INT-019` counts as semantic on v2.x); today's drift is `KNOWN_DRIFT`, one entry per cause, removed by its fix (#650, #651); `grammar-verifier.yml` runs bound 4 nightly
    - `executor.rs`: Query executor — temporal filter (tx-time → net-assert → valid-time), not/not-join post-filter
    - `matcher.rs`: Pattern matching with variable unification; `edn_to_value`, `edn_to_entity_id`
    - `evaluator.rs`: `RecursiveEvaluator` (semi-naive), `StratifiedEvaluator` (repeats a stratum whose rules recurse through a `not`/`or` rule until it derives nothing new, #633), `evaluate_not_join`
@@ -174,7 +175,7 @@ Auto-migrates v1/v2/v3/v4/v5/v6 → v7 on open/checkpoint.
 
 ## Test Coverage
 
-**1313 tests** (1304 passing, 9 ignored; unit + integration + doc).
+**1317 tests** (1308 passing, 9 ignored; unit + integration + doc).
 See `docs/TEST_COVERAGE.md` for the full per-file breakdown.
 
 **Testing conventions** — see the Testing Conventions section below before writing any tests.

@@ -105,7 +105,7 @@ let r2 = pq.execute(&[("tx", BindValue::TxCount(2)), ("entity", BindValue::Entit
 
 ```bash
 cargo run          # interactive Datalog REPL
-cargo test         # run 1313 tests
+cargo test         # run 1317 tests
 cargo run < demos/demo_recursive.txt   # recursive rules demo
 ```
 

@@ -4,7 +4,7 @@
 
 **Verified**: 2026-10-20 with `cargo test`
 
-**Result**: 1,304 passing tests and 9 ignored tests (1,313 total), including the golden-file corpus (#391)
+**Result**: 1,308 passing tests and 9 ignored tests (1,317 total), including the golden-file corpus (#391)
 
 For v2.0.5, `tests/edge_cases_test.rs` checks that a file of 1 to 4,095 bytes is `STG-045`, unchanged and with no WAL, when it is a database cut below one page or foreign bytes, and opens as a new database that takes a write and reads it back after reopen when it is a prefix of the initial header or all zeros (#506). Rule-body tests in `tests/recursive_rules_test.rs` check that a `:db/valid-at` pattern in a rule definition, in its `not` and `not-join` bodies and in its `or` branches binds the query's valid time, on the semi-naive, stratified and magic-sets paths (#617).
 
@@ -22,6 +22,8 @@ For v2.0.5, torn-WAL-tail tests (#513) check that opening a WAL writer cuts off
 
 `tests/error_codes_prs_test.rs` checks that a fact of five or six elements, with or without a map 4th, fails with `PRS-108`, and that a transaction holding one stores none of its facts (#649).
 
+Since v2.0.8, `src/query/datalog/parser/verifier.rs` (4 tests, backported from v3.0.0; #643) checks the parser against `tests/grammar/grammar.pest` on about 1.07M lexical strings and 555K structural inputs at the default bound (7.6M at `MINIGRAF_GRAMMAR_BOUND=4`, run nightly by `grammar-verifier.yml`): pest rejects ⇒ the parser rejects, pest accepts ⇒ the parser accepts or raises a `SEMANTIC` code with a witness (`INT-019` counts as semantic on v2.x). Known drift is listed by cause in `KNOWN_DRIFT` (#650, #651). `tests/grammar_conformance.rs` now classes a fact with too few elements and a retract of the wrong arity as syntax errors, since `grammar.pest`'s fact is exact.
+
 Not counted above: the `BrowserDb` tests run only on wasm32 with `wasm-bindgen-test` in a browser. Two of them check that the IndexedDB flush returns every page a write dirtied, and that a dirty page that cannot be read is an error rather than left out.
 
 The v2.0.8 suite covers the public database API, the Datalog engine, storage and recovery paths, and the v2.0.0 locking and structured-error-code changes, plus v2.0.1's regression test for rebuilding indexes on open after several checkpoints (#370). Since v2.0.1, `tests/point_query_history_test.rs` and new storage unit tests check that attribute-narrowed bound-entity lookups return exactly what a full scan returns, and that `net_asserted_facts` matches its previous implementation on randomized histories (#323). Attribute-scan tests check that the AEVT range covers exactly the queried attribute, including non-ASCII names such as `:丿` and prefix siblings such as `:ab` for `:a` (#381). Incremental B+tree rebuild tests check that checkpoints which copy untouched index leaves produce exactly the entries and file checksum a full rebuild would, including over repeated checkpoints, that single-fact checkpoints do not fragment the index, and that a cyclic leaf chain or damaged slot directory is rejected rather than copied (#315). Directory-sync unit tests check that creating the `.graph` file or the WAL, and deleting the WAL, fsync the parent directory after the file operation, and that reopening an existing file does not (#389). Disjunction tests check that `or-join` returns an empty result, not INT-031, when no rows reach it: on an empty database, after a pattern that matches nothing, after a `not` that removes every row, and in a rule body (#405). A stratification unit test builds the same two-rule negative cycle 64 times and checks that the INT-054 message names the same predicate pair every time (#410). Magic-sets tests check that a recursive rule with a literal start that recurses through another rule returns the same results as without the literal (#297). API tests check that `execute()` and `WriteTransaction::execute()` reject `$slot` bind tokens in every position with API-010 (#407). The REPL `run()` test now runs in a child process with null stdin, so it no longer hangs when the test runner's stdin is an open non-TTY stream (#415). A fault-injection test crashes `save()` at each of its 47 page writes and syncs and checks that every reopen finds exactly the old or the new checkpointed facts (#374). For v2.0.3, storage unit tests and two `edge_cases_test.rs` tests check that more than 65,535 uncheckpointed facts each resolve to their own fact through entity lookups and attribute scans, in memory and file-backed, before and after a checkpoint, and that the widened `FactRef` encodes to the same bytes as before (#445). A WAL test reopens a database next to a WAL whose entries are all checkpointed, writes again, and checks that `:as-of` history is unchanged before and after another reopen; a unit test checks that restoring the transaction counter never lowers it (#447). Since v2.0.3, `tests/golden_corpus_test.rs` opens a copy of each committed golden file in `tests/golden/` (v7 files written by minigraf 2.0.3: one checkpoint, several checkpoints, indexes rebuilt on open, a crash-left WAL, an already-checkpointed WAL, same-transaction multi-values) and checks its manifest's CRC32, `tx_count` and query results after open, after a checkpoint and reopen, and after one more write; a second test checks that every golden file has a manifest (#391). A recursive-rules test runs rule queries on a database with more live facts than `max_results` and checks that they answer, and that the limit still stops a rule that derives more facts than it allows (#528). A WAL test restores a WAL whose entries are all checkpointed and checks that an explicit `checkpoint()` removes it, keeps the fact, and that the next write does not reuse tx 1; the golden-corpus test now requires `v7_stale_wal` to have no WAL after a checkpoint too (#457). A WAL test checks that dropping a handle opened with `wal_checkpoint_threshold(usize::MAX)` leaves the `.graph` file byte for byte unchanged under `Full` and `Normal` sync, keeps the WAL, and that a reopen replays it (#476).

@@ -1901,6 +1901,9 @@ fn parse_rule(elements: &[EdnValue]) -> Result<DatalogCommand> {
     }))
 }
 
+#[cfg(all(test, not(target_arch = "wasm32")))]
+mod verifier;
+
 #[cfg(test)]
 mod tests {
     use super::*;