Historical report imported 2026-10-10 from docs/experiments/ablation/coverage-e1-run-01.md. Original SHA-256: c810f7e3baf70d524a6c21bde9a4804ad953a0c42e681fde46c04199f2e2b1e7. Measurements and outcomes retain their stated revisions. Links and local environment labels are normalized; $FABRIC_DATA is the mounted experiment drive. See evidence policy.

E1R: authenticated coverage correctness

Outcome and boundary

The registered protocol passed its finite correctness corpus: 1,536 complete query results exactly matched an independent positional full scan, 1,536 all-unavailable cases returned the expected complete/incomplete status, and 8,832 injected metadata faults were rejected. There were zero observed contract violations. This supports a research prototype under the stated trust assumptions, not application adoption or a performance claim.

The new coverage module is separate from S1 and FOL2. It owns generated rows in memory, validates exact-set summaries, authenticates full-event block commitments with SHA-256, and verifies query-bound receipts against an independently retained anchor. It does not replay or change the application log. ADR-0007 and the query view explain the contract and diagram.

Oracle, selection and non-vacuity

An independent oracle author wrote the eight contract tests and the fixed corpus before either candidate existed. The freeze record (local evidence omitted from stage) pins protocol, interface and oracle hashes. The preimplementation command exited 101 because the coverage module did not exist; that was not a passing test run. The preservation runner independently propagated the same expected failure.

Two isolated Luna candidates each passed the frozen tests. Three further selection probes checked empty roots, excess proof nodes, canonical field boundaries, attribute order, signed zero and the self-authentication counterexample. Both passed: N=2, observed pass fraction 2/2, with no escalation. This is not a model reliability estimate. The selection decision (local evidence omitted from stage) retains candidate B: it validates generated and supplied summaries through one path and constructs roots and paths from one tree. Candidate A relies on summary construction for generated summaries. No performance metric selected a candidate. Full command outputs and source hashes remain in A (local evidence omitted from stage) and B (local evidence omitted from stage).

Two source mutations in a separate worktree established that the checks can fail:

Deliberate defect	Expected failing check	Actual exit
Bypass the nonempty receipt's independently retained root comparison	receipt_authentication_binding_and_layout_errors	101
Remove summary validation before sealing	builder_rejects_omissions_and_accepts_conservative_summaries	101

The root-binding record (local evidence omitted from stage) and builder-validation record (local evidence omitted from stage) include mutation diffs, commands, and assertion failures. Neither defect entered the selected source. The deliberately faulty self-authentication baseline also accepts a response-derived root when checking against the independently retained root correctly fails.

Reproduction and preserved evidence

From the repository root, using a fresh output directory:

cargo test --offline --locked --manifest-path tools/storage-probe/Cargo.toml
python3 -B tools/bench/run_coverage_e1.py target/coverage-e1/run-02

Run 01 executed the runner with target/coverage-e1/run-01, exit 0, from 10:35:04 to 10:35:33 UTC on 2026-09-27. The host was WSL2 Linux/x86_64, Rust/Cargo 1.98.0; this was the unoptimized test profile. The metadata (local evidence omitted from stage) records the exact cargo command, toolchain, starting revision, working-tree state and source hashes. Raw test/compiler output and tracked diff (local evidence omitted from stage), summary (local evidence omitted from stage) and frozen protocol (local evidence omitted from stage) are preserved. JSON strings retain the original output and diff bytes, including blank lines and diff context spaces; their initial plain-text archive triggered Git whitespace checks, so the archive uses this lossless container. New source files are pinned by hashes and retained in this change; the tracked diff alone does not include files that were untracked at run time.

The four S1-shaped workloads use seeds 101, 102, 103, 2,048 rows each, 64-row blocks, and 128 queries generated by the frozen SplitMix64 seed-7 fixture. Total input is 24,576 generated events in 12 snapshots. The scalar oracle reads original rows, not candidate summaries or receipts. Every full result compares ordered positions.

Check	Cases	Observed outcome
Clean complete query versus full scan	1,536	Exact positional equality
All raw blocks modeled unavailable	1,536	Expected candidate ordinals; safe exclusions remain possible
Missing block ordinal	1,536	Rejected
Substituted summary bytes	1,152	Rejected
Swapped ordinal order	1,536	Rejected
Replaced anchor root	1,536	Rejected
Mismatched snapshot identity	1,536	Rejected
Truncated trusted block count	1,536	Rejected

Summary substitution is injected only where a query actually has an excluded block; the raw counters preserve that denominator. This models a stale or changed summary by changing its bytes, not a real metadata cache or disk-generation swap. The eight smaller contract tests separately cover builder omissions, conservative supersets, empty and odd trees, malformed authenticated layouts, overflow, query binding, Unicode tokens, duplicate IDs and full-event bit-sensitive hashing.

Trust-boundary negative control

The test intentionally authenticates row=rare, summary=common through the low-level commitment utility, bypassing the builder. Receipt verification accepts the exclusion while the independent row oracle finds a match. Conversely, the normal builder rejects that invalid summary. This expected counterexample is why hash binding cannot replace semantic validation. Likewise, a Scanned marker depends on an honest exact evaluator; it is not a cryptographic execution proof.

The verifier's signature accepts only metadata and the expected query. Source inspection confirms no row-loading path. This is a type/API boundary, not a measured physical-bytes-read counter. The partition argument and assumptions are recorded in the protocol and ADR.

Review and next decision

The GPT verifier (local evidence omitted from stage) ran the full 19-test research suite and an independent 11,142-case scratch probe, both exit 0. Its probe covered lengths 0–17, five block sizes, six predicates, availability masks and digest tampering. The Claude Sonnet reviewer (local evidence omitted from stage) ran the 11 small coverage/selection tests and six additional adversarial tests, both exit 0. Those probes exercised all proof depths in a 13-leaf tree, odd-node duplication, 1–32 block proof lengths, empty anchors, token encoding boundaries and invalid exclusions. Both approved the same unchanged implementation hash. Neither approval establishes an unbounded proof.

Claude's initial piped test command was denied by its CLI allowlist; the plain already-authorized command subsequently ran. A scratch-directory shell command was also denied; its authorized file-writing tool created the probe files. These denials, successful test outcomes and session identity are preserved in the review record. The parent also reproduced both reviewers' standalone probes. The final artifact verification (local evidence omitted from stage) matched all 19 measured source hashes and four frozen hashes, and recomputed the summary. Documentation, research-package formatting and diff checks exited 0.

The finite checks justify proceeding to the separately scoped snapshot-bound residual-answer experiment. They do not justify a storage migration or removing a durability sync.

There is no malicious-server proof, durable anchor publication, wire parser, concurrent append, compaction, partial-result merge, physical failure detection, latency comparison or memory-cost result. Query completeness may rely on validated metadata for unreadable excluded blocks and therefore does not prove raw retention. Exact summary sets deliberately differ from S1's Bloom representation. Overhead, anchor lifecycle and resumability remain future experiments; append-phase attribution remains an independent Stage 6 question.