adityamukho · Oct 29, 2026 · Oct 29, 2026 · Oct 29, 2026 · Oct 29, 2026
@@ -10,10 +10,11 @@ run-name: >-
   || github.event_name == 'workflow_dispatch' && inputs.ref
   || (github.event.schedule == '0 18 * * *' && 'v3' || 'main') }})
 
-# #627: proves the byte encoders that order index keys (src/storage/keys/
-# verification.rs, src/storage/index/verification.rs). The whole set takes
-# about 30 seconds of proof time and ~1 GB of memory. Kani upgrades are
-# deliberate PRs that re-run the set.
+# #627/#693: 12 encoder and 17 pure scalar-decoder harnesses in
+# src/storage/keys/verification.rs and src/storage/index/verification.rs.
+# On the bench machine with -j 4, 29 proofs passed in about 2 minutes warm;
+# aggregate CBMC peak RSS was 7.6 GiB. Keep concurrency capped at the measured
+# value for the 16 GiB runner. Kani upgrades are deliberate PRs that re-run all.
 
 on:
   pull_request:
@@ -61,7 +62,7 @@ jobs:
         uses: model-checking/kani-github-action@v1.1
         with:
           kani-version: 0.68.0
-          args: --lib -j --output-format terse -Z unstable-options --harness-timeout 10m
+          args: --lib -j 4 --output-format terse -Z unstable-options --harness-timeout 10m
 
       - name: Record Kani failure
         if: ${{ failure() && github.event_name == 'schedule' }}
@@ -76,7 +77,7 @@ jobs:
             echo
             echo "- Run: $GITHUB_SERVER_URL/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID"
             echo "- Commit: $(git rev-parse HEAD)"
            echo "- Reproduce: \`cargo kani --lib -j --output-format terse -Z unstable-options --harness-timeout 10m\` (Kani 0.68.0)"
+            echo "- Reproduce: \`cargo kani --lib -j 4 --output-format terse -Z unstable-options --harness-timeout 10m\` (Kani 0.68.0)"
             echo
             echo "The failing harness and its counterexample are in the run log."
           } > "$report_file"

@@ -140,6 +140,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Tests
 
+- **Format-v8 scalar key decoders are model checked (#693).** Pure inner decoders let Kani prove round trips for signed and unsigned integers, descending transaction counts, valid-to times, floats and six tagged scalar value kinds, plus no panic and bounded cursor consumption on short malformed inputs. The `Reader` still returns the same INT-049 messages and cursor positions; a test-only copy of its old code checks those against exhaustive 0–2 byte and seeded longer inputs. Strings, sets, packed pages and WAL retain fuzz and property coverage. No key bytes or file format change.
 - **Statement bases and large write transactions (#550).** A `WriteTransaction` whose statements repeat, change, retract and re-assert each other's facts across chunks gives every statement the same outcome, and stores the same records, at chunk sizes 1 to 4 as with one chunk; queries after each statement return what a commit of the statements so far would hold; failed and rolled-back statements and transactions leave the file passing `verify`. The fault matrix covers a large `WriteTransaction` at every write and sync, and with `test-hooks` the crash-kill test runs every third transaction of its large variant as one.
 - **Golden-file compatibility corpus (#391).** `tests/golden/` holds v7 files written by minigraf 2.0.3, each with a JSON manifest of its CRC32, `tx_count` and expected query results. They cover one checkpoint, several checkpoints, indexes rebuilt on open, a WAL left by a crash, a WAL whose entries were already checkpointed, and same-transaction multi-values (#371). `tests/golden_corpus_test.rs` opens a copy of each file and checks its manifest after open, after a checkpoint and reopen, and after one more write. Golden files are never regenerated, only added; a new `golden-corpus` job in `policy.yml` fails a pull request that changes one. The generator is a standalone crate pinned to `minigraf = "=2.0.3"` (`tests/golden/gen/v7/`). On `v3`, each v7 file must also carry a v8 meta page after its first open, and seven v8 files are frozen alongside them, written by the `v3` branch at `23aa57c` (`tests/golden/gen/v8/`): one checkpoint, seven copy-on-write checkpoints, a crash-left v2 WAL, an already-checkpointed v2 WAL, same-transaction multi-values, a v7 file migrated in place, and long values (a 4,068-byte string stored twice, the 64/65-byte inline boundary, a 1,000-byte attribute and keyword). All #371 queries now pass.
 - **Model-based storage test (#385).** `tests/model_based_test.rs` runs random sequences of `transact` (multi-valued batches, transaction- and fact-level valid-time windows, a triple repeated with another window), `retract`, write transactions (committed or rolled back, retracting their own assertions), checkpoints, reopens (default, a 4-page cache, auto-checkpoint every 2 writes) and simulated crashes (a copy of the `.graph` file and WAL taken while the handle is open, so the WAL is replayed) against a file in a temp dir. After every step, `current_tx_count`, `verify`, full rows with windows and tx counts, and entity-, entity+attribute-, attribute-, attribute+value-, value-bound and full-scan queries, under `:as-of N` and `:valid-at T`, must match a plain reference model (one valid-time window per triple, #435; API-011 for two windows of one triple in one statement and API-019 for an empty or inverted window, from `execute` and `tx.execute`, #436; the last statement that writes a triple decides it at commit, #477). Reads inside a write transaction are checked against what its commit will hold. Normal CI runs 24 cases; the nightly property-test workflow runs 30,000.
@@ -160,7 +161,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - `tests/snapshot_atomicity_test.rs` races a writer against a reader: a query must see each transaction whole, whether written with `execute` or a `WriteTransaction` (#554), and must read one state for all its patterns (#555), in memory and on file. It also runs the v2.x checkpoint race from #558, which never failed on v3: copy-on-write checkpoints do not overwrite pages a published reader uses.
 - **The `datalog_eval` fuzz guard counts partial bindings** (#597). The guard skipped inputs whose patterns join to more than 50,000 rows, counting only the rows after the last pattern. A `not-join` body still runs on the executor pattern by pattern in text order, so a 120-pattern body built hundreds of thousands of partial bindings before its last pattern matched nothing, and ran past the 60-second timeout. The guard now counts the bindings after every pattern. On the `v3` corpus (4,783 inputs) coverage drops by 7 of 9,719 edges. The input is added as a seed, as is the `btree_page` input of the cursor fix above.
 
-- **Kani proofs of the key and value encoders (#627).** `src/storage/keys/verification.rs` and `src/storage/index/verification.rs` hold 12 Kani harnesses, compiled only under `cfg(kani)`. They prove for every input that the v8 key encoders (`put_int`, `put_uint`, `put_tx_desc`, `put_valid_to`, `float_bits`) and `encode_value` keep the order the indexes rely on, that every NaN encodes to one value, and that `float_bits` round-trips. `.github/workflows/kani.yml` runs them on pull requests that touch the encoders and nightly on `main` and `v3`. Decoders, strings, packed pages and the WAL are not covered: the model checker does not finish on them, and the fuzz and property tests remain their defence. Test-only; `Cargo.toml` declares the `kani` cfg so normal builds do not warn.
+- **Kani proofs of the key and value encoders (#627).** `src/storage/keys/verification.rs` and `src/storage/index/verification.rs` hold 12 Kani encoder harnesses, compiled only under `cfg(kani)`. They prove for every input that the v8 key encoders (`put_int`, `put_uint`, `put_tx_desc`, `put_valid_to`, `float_bits`) and `encode_value` keep the order the indexes rely on, that every NaN encodes to one value, and that `float_bits` round-trips. `.github/workflows/kani.yml` runs them on pull requests that touch the keys and nightly on `main` and `v3`. The original #627 scope left decoders out; #693 above adds scalar decoder proofs. Strings, sets, packed pages, WAL and `Reader`'s error mapping remain under fuzz, property and differential tests. Test-only; `Cargo.toml` declares the `kani` cfg so normal builds do not warn.
 - **Parser vs grammar verifier (#643).** `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 20 s by default and 3.5 min at bound 4 on a 16-thread machine. The drift it found is listed in `KNOWN_DRIFT` by cause (comments and non-ASCII letters #650, since documented: see below; empty sections, ignored keywords, rule and call heads, a lone `:` or `-`, unterminated strings #651, since fixed; a fact of more than four elements losing elements, #649, since fixed); each fix removes its entry. `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).
 - **The grammar documents comments and non-ASCII identifiers** (#650). The parser has always accepted both; `tests/grammar/grammar.pest` and `docs/GRAMMAR.md` now say so. A `;` starts a comment that runs to the end of the line and is skipped like whitespace. Symbols, variables, keywords and bind slots take Unicode letters and numerals (`:person/名前`, `?ñ`), as Rust's `char::is_alphabetic` and `char::is_numeric` define them; a symbol starts with a letter or `_`, and `-` followed by a numeral starts a number, not a symbol. Nothing the parser accepts or rejects changes.
 

@@ -8
8000
4,9 +84,11 @@ cargo test --test complex_queries_test -- --nocapture
 cargo test --test recursive_rules_test -- --nocapture
 cargo test --test concurrency_test
 
-# Kani proofs of the encoders (#627); ~1 GB. Never add decoder/string harnesses
-# without a bench-machine run first: they went past 27 GB without finishing
-cargo kani --lib -j --output-format terse -Z unstable-options --harness-timeout 10m
+# Kani proofs of key encoders and pure scalar decoders (#627, #693):
+# 29 harnesses, ~2 minutes warm and 7.6 GiB peak aggregate CBMC RSS at -j 4.
+# Measure any new harness on the bench machine before adding it to CI.
+# Reader error paths and variable-length strings remain outside Kani's budget.
+cargo kani --lib -j 4 --output-format terse -Z unstable-options --harness-timeout 10m
 
 # Run examples
 cargo run --example embedded
@@ -117,7 +119,7 @@ cargo run < demos/demo_negation.txt
    - `backend/fault_inject.rs`: `FaultInjectingBackend` — injects I/O errors for durability tests (test builds only)
    - `fault.rs`: thread-local fault plan (test builds only, #390) — EIO, torn/short writes, sticky ENOSPC, failed fsync with or without lost writes, at the k-th write or sync of `FileBackend`, the WAL and `sync_parent_dir`; driven by `src/fault_matrix.rs`
    - `index.rs`: pending (uncheckpointed) EAVT/AEVT keys over UUIDs and strings, `encode_value`; `index/verification.rs`: Kani proofs of `encode_value` (`#[cfg(kani)]`, #627)
-   - `keys.rs`: byte-comparable v8 keys (FDB integers, value tags, `tx↓`, FOREVER), DICT keys, `MAX_VALUE_BYTES`, `MAX_IDENT_BYTES`; sets (#316): tag `0x08`, element encoding (`set_elements`: each element's key encoding, sorted) inline up to 64 bytes, else `LongSet` in a value page, `decode_set`, `set_bytes_bound` (the WAL's id-free size bound); `keys/verification.rs`: Kani proofs that the key encoders preserve order (`#[cfg(kani)]`, #627; `kani.yml` runs them on encoder PRs and nightly)
+   - `keys.rs`: byte-comparable v8 keys (FDB integers, value tags, `tx↓`, FOREVER), DICT keys, `MAX_VALUE_BYTES`, `MAX_IDENT_BYTES`; sets (#316): tag `0x08`, element encoding (`set_elements`: each element's key encoding, sorted) inline up to 64 bytes, else `LongSet` in a value page, `decode_set`, `set_bytes_bound` (the WAL's id-free size bound); pure scalar decoders preserve INT-049 errors (#693). `keys/verification.rs` proves encoder order and scalar decoder round trips/malformed bounds with Kani (`#[cfg(kani)]`, #627, #693); `keys/legacy_verification.rs` compares the old and new readers in tests. `kani.yml` runs proofs on key PRs and nightly.
    - `node.rs`: prefix-compressed leaf and shortest-separator internal node codecs
    - `btree.rs`: On-disk B+tree over byte keys (`build_btree`, `cow_update` (copy-on-write inserts and deletes; an emptied leaf or node leaves its parent, an emptied tree is root 0; #550) and `cow_insert`, `LeafCursor` (with `seek`), `prefix_scan`, `get`, `MutexStorageBackend`)
    - `dict.rs`: `DictReader` (id ↔ UUID/ident, tx timestamps, long values; `uuids_of` walks dense id batches with `LeafCursor` and uses exact scalar reads for sparse/small batches, #530) and `Encoder` (checkpoint-time id assignment and key building)
@@ -216,7 +218,7 @@ Auto-migrates v7 → v8 on open (spec §9, with a backup meta page). v1–v6 are
 
 ## Test Coverage
 
-**1996 tests** (1979 passing, 17 ignored; unit + integration + doc). Engine answers once checked by the executor are frozen in `tests/answers/` (#551).
+**2000 tests** (1983 passing, 17 ignored; unit + integration + doc). Engine answers once checked by the executor are frozen in `tests/answers/` (#551).
 See `docs/TEST_COVERAGE.md` for the full per-file breakdown.
 
 **Testing conventions** — see the Testing Conventions section below before writing any tests.
@@ -229,6 +231,7 @@ Current plan (see `ROADMAP.md` and the milestones):
 - **v2.x** (`main`, format v7) now gets only data-integrity and security fixes as patch releases (v2.0.3 is the first); v2.0.2 was the last planned v2.x release.
    - **v3.0.0** (format v8 and data integrity, plus `:limit` #306, optional `:distinct` output #493, `lag`/`lead` #182, sliding row frames #183, query profiler #185, set membership predicates #316 and prepared queries in every binding #181, UDF registration in every binding #180; tracker #383) is developed on the long-lived `v3` branch. All v3 PRs target `v3`; `main` stays untouched. CI runs on PRs to `v3` the same as on PRs to `main`. Do not merge `main` into `v3` routinely: `main` only gets backports of fixes already on `v3`. Shared CI and workflow changes land on both branches as separate PRs. Just before the v3.0.0 cut, merge `main` into `v3` once (merge commit; source conflicts resolved to `v3`, `main`'s v2.0.x CHANGELOG sections brought over) so the cut is a fast-forward. At the first v3 release, the current `main` is copied to `v2` and `v3` becomes the new `main`.
 - **Input order (#641)** targets v3.0.0 in three slices: committed scalar Sort omission, one-group count/count-distinct and partition-at-a-time windows are implemented in the dependent PRs for `v3`. The reviewed design, fallback scope and acceptance gates are in `docs/superpowers/specs/2026-10-28-641-input-order-design.md`.
+- **Scalar key decoder proofs (#693)** target v3.0.0 before the release cut. The pure decoder refactor preserves key bytes and INT-049 behavior; Kani covers round trips and bounded malformed inputs. The approved design and CI limits are in `docs/superpowers/specs/2026-10-29-693-decoder-proofs.md`.
 - **v3.next** (the release after v3.0.0) holds new features (rule persistence #241; OPFS `BrowserDb` #441).
 - Known v2.x data issue: same-transaction multi-valued facts (#371). Fix ships in v3.0.0. All v2.x known issues are listed in pinned issue #421 (`known-issue` label); `data-integrity`/`corruption`/`durability` issues fixed in a v2.x patch stay open until that patch is published; issues fixed on the unreleased `v3` branch close on merge (closing keywords do not fire on `v3`, so close them with `gh issue close`) and stay listed in #421 (CONTRIBUTING.md).
 - Support policy and tiers: PHILOSOPHY.md §7 and §10. v2.x gets data-integrity and security fixes for 12 months after v3.0.0. Tier 1 = Rust + Python + browser WASM (from v3.0.0); other bindings are Tier 2.

@@ -142,6 +142,8 @@ cargo test         # run the test suite
 cargo run < demos/demo_recursive.txt   # recursive rules demo
 ```
 
+Storage key encoding and scalar decoding have Kani proofs; see [test coverage](docs/TEST_COVERAGE.md#kani-proofs-of-key-encoders-and-scalar-decoders-627-693) for their scope and how to run them.
+
 Queries without aggregates return one row per matching binding, including repeated `:find` tuples.
 Add the bare `:distinct` flag to remove repeated
 output tuples: `(query [:find ?name :where [?e :person/name ?name] :distinct])`.

@@ -78,6 +78,7 @@ This was the GitHub milestone named “2.0” before v2.0.0 used that version nu
 Scope — format and storage integrity:
 
 - v8 index keys with value bytes and v7→v8 migration (#371, #287; done on `v3`)
+- Kani proofs that the format-v8 scalar key decoders invert their encoders and reject bounded malformed inputs without panicking (#693; targeted before v3.0.0, with no format change)
 - v8 storage format, done on `v3` in five PRs (#374, #434, #388, #433):
   - per-page CRC32, page id and generation on every page (#388);
   - two alternating meta pages; crash-atomic, copy-on-write checkpoints whose cost follows the change (#374, #434);