feat(#901): ProvenSafeBoundsChecker — fail-closed, attested bounds-check elision from scry's proofs (VCR-MEM-004) by avrabe · Pull Request #915 · pulseengine/synth

avrabe · 2026-08-05T16:39:53Z

What

synth compile --proven-safe safe-accesses.json consumes scry's scry/safe-accesses/v1 verdict list (producer: pulseengine/scry#114) and drops the --safety-bounds software inline bounds guard at exactly the access sites scry's sound abstract interpretation proved in-bounds against the memory's guaranteed minimum size — a floor wasm memory can only grow away from, so the verdict survives memory.grow.

Closes #901. Typed as VCR-MEM-004 in artifacts/verified-codegen-roadmap.yaml (added before the implementation, next to VCR-MEM-001, the sibling scry consumption channel).

The deliverable is the refusal logic, not the speedup

Every question the ingestion can ask is answered fail-closed, and fail-closed always means the same thing — elide nothing, warn, exit 0:

Condition	Behaviour
`module_sha256` ≠ the bytes handed to the decoder	REFUSE, both hashes named
`memory_min_bytes` ≠ this module's declared floor	REFUSE, both values named
malformed / missing / wrong-schema file	REFUSE, diagnosed, never an error
`(func, pc)` key fails validation against the decoded operator	DROP that entry, counted
the function was specialized by `SYNTH_FACT_SPEC`	REFUSE that function's marks
non-ARM backend, or bounds mode ≠ `software`	no marks, attestation records 0
single-function path (`--func-index`/`--func-name`)	hard error, names what works

The hash is taken over the post-.wat-parse, post-loom, post-#418-arena-bind bytes. That is deliberate: those rewrites shift function/operator indices, so binding the hash there makes index skew and byte skew one gate.

The key is self-checking. scry#114's pc is the 0-based wasmparser operator index — an open producer question. Rather than bet on the reading, each entry is re-validated against the decoded operator (must exist, must be a linear-memory access, must have the declared access width). If a producer ever emits byte offsets, essentially every entry fails and the build elides nothing loudly instead of stripping the guard off the wrong access.

Absence means "not proven", never "unsafe": an unlisted site keeps its guard, so a partial verdict list yields a partially-guarded binary.

Measured

scripts/repro/proven_safe_bounds_901.wat, Cortex-M4, 8 guarded accesses, 5 proven:

build	`probe`	executed insns
no bounds checking (floor)	94 B	30
`--safety-bounds software`	232 B	70
5 of 8 sites proven	152 B	45

80 B saved = 58 % of the 138 B guard tax, 34.5 % of the function; 25 fewer instructions (36 %). Proving all 8 lands byte-identical to the floor.

Honest framing: the per-site win is the same magnitude #494 already publishes, because it is the same guard strip. What is new is the authority — a whole-module external AI, hash-bound and attested — not the byte. The guard is also not a uniform 16 B per site, and the two partitions' savings sum to 130 < 138 (8 B of address materialization only collapses once no guard remains); both recorded rather than smoothed.

This also converts SoftwareBoundsChecker's long-standing "~25-40 % overhead" doc comment from an assertion into a measurement — the real tax on this access-dense kernel is +147 % bytes / +133 % instructions, worse than the old guess, with the small denominator named.

Attestation (loop step 6 — breaks a 3-release N/A streak)

Every --proven-safe compile writes <output>.proven-safe-elisions.json (synth-proven-safe-elisions-v1): the elision set with each site's authority, the scry version, both module hashes, both memory floors, the bounds mode, and every diagnostic — emitted on refusal too, so sigil can tell "nothing to elide" from "file rejected". A sidecar that only appears on success is a brag sheet, not an attestation.

Red-first evidence

Each safety property has a mutation that turns a gate red, not just a new-code test:

Mutation	Result
`for_site` returns `proven: true` (absence ⇒ safe)	2 synth-memory unit gates RED
delete the `module_sha256` + memory-floor comparisons	3 synth-core gates RED
delete the `module_sha256` comparison	byte gate RED (10/1)
…same, against the differential	207 → 199, `UC_ERR_READ_UNMAPPED` — a real OOB read
force `proven_safe_backend_supported = true`	backend gate RED (12/1)
change `SAVED_PROVEN_5` 80 → 96	`claim_check` RED (37/38)

The differential's fail-closed leg is a permanent regression gate: it applies one module's verdicts to a mutated module (i32.const 63 → i32.const -1, so the five formerly-proven accesses become unbounded) whose every key still validates. module_sha256 is the only thing between stale verdicts and a silent OOB.

Defects the gates found mid-flight

False attestation outside software mode — marks were set, the strip was a no-op, the sidecar claimed elisions that never happened.
False attestation on -b riscv / -b aarch64 — same shape one axis over: sites_elided: 5 with an ELF byte-identical to the baseline. The first fix closed the instance, not the mechanism; every test path went through --all-exports -b arm.
Silent no-op on --func-index/--func-name — the aarch64: linear-memory load/store emit NO bounds check and --safety-bounds is a no-op (all modes byte-identical) — OOB reads/writes up to 4GiB past the guest memory instead of trapping #865 shape. Now a loud error.
A vacuous gate of my own — the fact-spec combination test asserted only inside a conditional. Verified the pass does specialize the fixture (38 → 36 ops), then made the gate assert the specialization, the renumbering, the refusal and the attestation.

Gates

13 byte gates (14 with --features verify) · differential 207/207 · synth-core 15 · synth-memory 26
New CI job proven-safe-oracle, wired in the same commit as the differential: set -euo pipefail, RESULT: PASS grep, and a non-zero #901 CHECKS=n/n grep so a differential that checked nothing cannot pass
oracle_wiring_check: 158 scripts, 151 wired, 0 undeclared · claim_check: 38/38 (new SYNTH-PROVEN-SAFE-901-MEASURED pins the doc's numbers to the byte gate's constants — a capability gap, never an issue number)
Frozen anchors 10/10 (opt-in; the mark vector defaults empty) · clippy --workspace --all-targets -D warnings exit 0 · cargo fmt --check exit 0

Residuals, named not hidden

The two halves are joined by a documented contract, not a compile-time link. synth-memory is publish = false and synth-cli is published, so a path dep would change the published surface. Ingestion lives in synth-core; the named ProvenSafeBoundsChecker lives beside the trait in synth-memory, dep-free — the shadow_budget.rs split, forced here rather than chosen.
Elision is ARM-only. RISC-V/aarch64 ingest and verify but strip nothing (attested as 0).
The fact-spec combination is refused, not remapped. Remapping through SpecializedFn::kept needs its own differential.
Multi-memory (pre-existing, not created here): memory_min_bytes is compared against all_memories.first() and the IR still drops memory_index (VCR-MEM-002), so a verdict list for a multi-memory module would concern accesses whose target memory synth does not track.
synth-memory --no-default-features (no_std) does not build — and did not before this change (codegen uses Vec unconditionally). Not made worse, not papered over.

Note for assembly

docs/status/FEATURE_MATRIX.md was regenerated with scripts/claim_check.py --emit-status (never hand-edited) because the generated-file freshness gate is part of the required Claim Check. The template scripts/templates/feature_matrix.md.tmpl is the source edit; the coordinator's #805 regen at assembly still owns the final word.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…ry verdicts Traceability leads (pulseengine-feature-loop step 1): the typed sw-req for the #901 capability lands BEFORE the implementation, next to VCR-MEM-001 (the sibling scry consumption channel) and linked to VCR-PERF-002 (#494), whose per-site guard-strip mechanism VCR-MEM-004 reuses under a DIFFERENT authority — a whole-module external abstract interpretation hash-bound to one exact module, instead of a per-site ordeal obligation. The seven safety properties (fail-closed hash, absence != safety, fail-closed memory_min_bytes, self-checking (func,pc) key, fail-safe malformed handling, refused fact-spec combination, loud zero-elision) are stated as the deliverable; the speedup is not. status: proposed until the implementation and its oracles land. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

… strategy synth-memory/src/bounds.rs had a pluggable BoundsChecker trait and four strategies, none of them proof-informed. Adds the fifth: ProvenSafeSites — the (func_index, pc) verdict set, keyed on the wasmparser OPERATOR INDEX (same space as op_offsets and #494's elision marks). Sorted Vec + binary search so the attestation's iteration order is deterministic. ProvenSafeBoundsChecker — one decision per access site. Proven => no check at all + BoundsCheckOverhead::Zero; every other site DELEGATES to SoftwareBoundsChecker unchanged. Deliberately dep-free (this crate's dep list is bitflags alone): JSON ingestion, module_sha256 verification and attestation land next in synth-core. synth-memory is publish=false and synth-cli is published, so a path dep is impossible without changing the published surface — the shadow_budget.rs split, forced here rather than chosen. The two halves are joined by a documented contract, NOT a compile-time link; that is a named residual. The empty set is the FAIL-CLOSED value: every refusal path (hash mismatch, malformed file, missing file, memory_min_bytes disagreement) yields it, and it degrades the module to SoftwareBoundsChecker — never to no checking. There is no constructor that marks a site proven without a ProvenSafeSites lookup. RED-FIRST (mutation, not a shipped lever): making for_site return proven: true unconditionally — i.e. 'absence means safe' — turns absent_site_is_indistinguishable_from_the_software_checker_901 and empty_site_set_checks_everything_901 RED (24 passed / 2 failed). Reverted. Note: --no-default-features (no_std) does not build for this crate and did not before this change — the codegen module uses Vec unconditionally. Not made worse, not papered over. Implements: VCR-MEM-004 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…ingestion + sigil attestation Ingests scry's safe-accesses.json (schema scry/safe-accesses/v1, scry#114) and emits the synth-proven-safe-elisions-v1 attestation sidecar. TOTAL by design — no Result in ingest()'s signature, mirroring parse_wsc_facts: the verdicts are an optional accelerator, so no input may turn a successful compile into a failed one. FOUR FAIL-CLOSED GATES, each meaning the same thing (elide NOTHING, warn, exit 0): 1. module_sha256 mismatch. Verified against the EXACT bytes handed to the decoder — after .wat parsing, after loom, after the #418 arena-bind rewrite. Deliberate: those rewrites shift function/operator indices, so binding to the post-rewrite bytes collapses INDEX skew and BYTE skew into one gate. A file produced for the pre-rewrite module fails the hash. The diagnostic names BOTH hashes. 2. memory_min_bytes disagreement. Verdicts are proven against scry's declared floor; a matching hash implies it equals synth's declared minimum, so a mismatch means the producer is BROKEN — and a broken prover is not trusted. Names both values. 3. Wrong schema / malformed JSON / unreadable file. The wsc.facts fail-safe skew rule applied to a JSON carrier. Unknown JSON fields are tolerated (a newer scry must not break an older synth). 4. THE KEY IS SELF-CHECKING. validate_function() checks every entry against the DECODED op stream: pc in range, the op there IS a linear-memory access, and its access width EQUALS the declared width. Failures are dropped per-entry with a counted diagnostic. So if a producer ever emits wasm BYTE OFFSETS instead of operator indices, essentially every entry falls out of range and the build elides NOTHING loudly — instead of stripping the guard off the wrong access silently. That is what makes the open scry#114 'pc' reading safe to bet on. A refused document is NOT trusted piecemeal: offered is emptied wholesale. ATTESTATION: ElisionAttestation is emitted ON REFUSAL TOO, carrying accepted:false + the reason + sites_offered/sites_elided/sites_not_elided, so sigil can distinguish 'nothing to elide' from 'file rejected'. A sidecar that only appears on success is a brag sheet, not an attestation. Each elision carries an 'authority' field so a site elided under a different authority (#494's per-site ordeal certificate) stays distinguishable. RED-FIRST (mutation): deleting the hash gate and the memory-floor gate turns hash_mismatch_refuses_everything_901, one_flipped_module_byte_refuses_901 and memory_min_bytes_disagreement_refuses_901 RED (12 passed / 3 failed). Reverted. 15/15 green, clippy -D warnings clean. Implements: VCR-MEM-004 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…on sidecar New `--proven-safe <PATH>` on `synth compile` (--all-exports module path). Ingests scry's safe-accesses.json, validates every (func, pc) key against the decoded operator stream, and strips the --safety-bounds software inline guard at exactly the sites that survive. WIRING — one consumption point, two authorities: CompileConfig::proven_safe_mem_elide is kept SEPARATE from #494's fact_mem_bounds_elide (different authorities: whole-module external AI vs per-site ordeal certificate; the attestation records which covered each site). arm_backend unions them into the existing mark vector, so the scry marks inherit all three of #494's defensive gates for free: - the memory.grow(0) fold index-shift drop (with its own named decline); - direct-selector routing (a marked function never takes the optimized path, which is why optimizer_bridge's push_software_bounds_guard sites need no mark plumbing); - the strip is a no-op unless the mode is actually Software. REFUSALS, all loud, none fatal: - every synth_core::proven_safe gate (hash, memory floor, schema, malformed); - per-function: SYNTH_FACT_SPEC specialized this function, renumbering the index space pc is stated in => marks DROPPED, guards retained. Remapping through SpecializedFn::kept is a future increment that needs its own differential; assuming it would be a silent wrong-site strip; - ZERO-ELISION IS LOUD: flag given + file accepted + nothing stripped names the reason (vacuous document / --safety-bounds not software / no key survived validation, pointing at the byte-offset-vs-operator-index cause). ATTESTATION: <output>.proven-safe-elisions.json on EVERY --proven-safe compile including refusals. FIXTURE scripts/repro/proven_safe_bounds_901.wat — ONE function carrying both halves: 5 accesses off a provably-bounded base (slot & 63) * 16 + 256, and 3 off an unconstrained i32 param that no analysis can bound. So a single binary demonstrates elision AND absence-is-not-safety. Its pinned operator indices were verified against the real decoder (9/11/14/17/22 proven, 24/29/35 not). MEASURED (cortex-m4, --safety-bounds software, symtab slices): probe 232 B -> 152 B = 80 B saved (34.5%), 16 UDF#0 -> 6 .text 392 B -> 312 B stale-hash build: 232 B / 16 UDF — BYTE-IDENTICAL to the baseline. Unguarded floor is 94 B, so the 8-site guard tax is 138 B and proving 5 of 8 sites recovers 80 B of it. 16 B per site — the SAME magnitude #494 publishes, because it is the same guard strip. What is new is the authority, not the per-site win. clippy::large_enum_variant is allowed on Commands with a rationale: the Compile variant crossed the threshold with this flag, clap wants the fields inline, and the enum is built once per process. Frozen anchors 10/10. clippy --workspace --all-targets -D warnings: exit 0. Implements: VCR-MEM-004 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

11 end-to-end gates on the REAL compiled bytes of the #901 fixture, one per safety property, all symtab-sliced (never disasm text). MEASURED (cortex-m4, --safety-bounds software, 'probe' symbol): floor (no --safety-bounds) 94 B, 0 UDF#0 guarded (all 8 sites) 232 B, 16 UDF#0 => guard tax 138 B 5 proven elided 152 B, 6 UDF#0 => SAVED 80 B (34.5%) 3 unproven elided (mirror) 182 B, 10 UDF#0 => saved 50 B all 8 elided 94 B, 0 UDF#0 => byte-identical to floor Honest notes recorded in the test, not smoothed over: the guard is NOT a uniform 16 B per site (the address form differs), and 80 + 50 = 130 < 138 because 8 B of address materialization only collapses once NO guard remains. DEFECT THE GATES FOUND: with --safety-bounds NOT software, the marks were still set and the attestation recorded '8 elisions' — but the selector's strip is a no-op outside Software mode, so NOTHING was elided. sigil would have attested elisions that never happened. A false attestation is worse than no attestation. Fixed by gating mark-setting on SafetyBounds::Software; the loud zero-elision diagnostic now names the mode as the reason. RED-FIRST (mutation): deleting the module_sha256 comparison turns stale_hash_elides_nothing_and_is_byte_identical_901 RED — the elision fires on a stale analysis and the .text stops matching the guarded baseline (10 passed / 1 failed). Reverted. Covered: full elision reaching the unguarded floor; the PARTIAL 5-of-8 list leaving exactly the 3 unproven guards (plus its mirror image, so the partition is proven disjoint and complete — not the near-vacuous empty-list version); stale hash; memory_min_bytes disagreement; malformed / missing / wrong-schema / garbage-site documents (all exit 0, byte-identical, attested as refused); the key-space canary (byte offsets instead of operator indices elide nothing LOUDLY); width skew dropping only the skewed site; the attestation contents including per-site authority; and the fact-spec combination refusal (verify-gated). Implements: VCR-MEM-004 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

scripts/repro/proven_safe_bounds_901_differential.py — unicorn vs wasmtime, CI-wired in the new proven-safe-oracle job (set -euo pipefail, RESULT: PASS grep, and a non-zero CHECKS=n/n grep so a differential that checked nothing cannot pass). 207/207 checks green. FOUR LEGS: 1. BYTE EVIDENCE + non-vacuity — the run fails unless the compile reported exactly 5 scry-authorized elisions. 2. IN-BOUNDS SWEEP — 180 rows (10 slots x 6 raw addresses x 3 memory seeds): ELIDED == GUARDED == wasmtime on the return value AND the full 64 KiB final memory image (the fixture stores through both address expressions). 3. ABSENCE IS NOT SAFETY, EXECUTABLE — 5 out-of-bounds accesses at the three NOT-PROVEN sites still TRAP in the ELIDED build, exactly like wasmtime. Their guards survived the elision of the five that were proven. 4. FAIL CLOSED, AND LOAD-BEARING — the red leg. It applies the fixture's verdicts to a MUTATED module (i32.const 63 -> i32.const -1, so slot & -1 == slot and the five formerly-proven accesses become UNBOUNDED) whose every (func, pc) key STILL VALIDATES: same operator count, kinds and widths. module_sha256 is the only thing that differs, so it is the only thing standing between stale verdicts and a silent out-of-bounds access. RED-FIRST, and this one is the important one: deleting the module_sha256 comparison makes leg 4 accept the stale verdicts and probe(4096, 0), probe(65536, 0), probe(1048576, 0) return UC_ERR_READ_UNMAPPED — a REAL out-of-bounds read where wasmtime traps. 199/207, RESULT: FAIL. Reverted. This is a permanent regression gate, not a one-time demo. MEASURED, with the honest denominators: probe 232 B -> 152 B: 80 B saved = 58% of the 138 B guard tax, 34.5% of the function. 5 of 8 sites proven. Executed instructions on one in-bounds call: 70 -> 45, i.e. 25 fewer (35.7%); the full 8-site guard cost is 40 instructions (70 -> 30 floor). The per-site win is the same magnitude #494 publishes because it is the same guard strip — what is new is the authority (a whole-module external AI, hash-bound and attested) and the fail-closed binding, not the byte. oracle_wiring_check: 158 scripts, 151 wired, 0 undeclared. claim_check: 37/37. Implements: VCR-MEM-004 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…R-MEM-004 implemented - CHANGELOG [Unreleased]: the --proven-safe entry, led by the refusal logic rather than the speedup, with the measured numbers and their denominators. - scripts/templates/feature_matrix.md.tmpl (a SOURCE file): the validator row and the CLI flag list. docs/status/FEATURE_MATRIX.md was REGENERATED with scripts/claim_check.py --emit-status, never hand-edited — the generated-file freshness gate is part of the required Claim Check, so leaving it stale would redden this PR. The coordinator's #805 regen at assembly still owns the final regeneration; this is only what keeps the lane green. - claims.yaml: SYNTH-PROVEN-SAFE-901-MEASURED pins the doc's measured cost (138 B / 40 insn guard tax, 80 B recovered) to the CONSTANTS the byte gate asserts against real compiled bytes, plus the presence of the fail-closed refusal in the ingestion. Non-vacuity verified: changing SAVED_PROVEN_5 from 80 to 96 turns it FAIL (37/38). It pins a CAPABILITY — a measured tax and a measured recovery on a named fixture — never an issue number, so a closed issue can never green-confirm a false residual (the v0.53 lesson). - synth-memory bounds.rs: SoftwareBoundsChecker's '~25-40% overhead' becomes a MEASURED table. The real tax on this access-dense kernel is +147 % bytes / +133 % instructions — worse than the old guess, stated as such, with the small denominator named ('one fixture on one target, not a headline'). - VCR-MEM-004 status proposed -> implemented. claim_check 38/38; oracle_wiring_check 158 scripts / 151 wired / 0 undeclared. Implements: VCR-MEM-004 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…rface defects) Both are the SAME class as the non-Software false attestation the byte gates already caught. That fix closed the instance, not the mechanism: every test path went through '--all-exports -b arm', so neither axis was observable. DEFECT 1 — FALSE ATTESTATION ON NON-ARM BACKENDS. Only the ARM direct selector consumes the marks (apply_mem_bounds_elision); RISC-V and aarch64 accept --safety-bounds software but emit their own guards from their own selectors and read no mark table. Measured before the fix: synth compile m.wasm -b riscv --target rv32imac ... --proven-safe s.json synth compile m.wasm -b aarch64 --target cortex-a53 ... --proven-safe s.json both wrote 'sites_elided: 5' while the ELF was BYTE-IDENTICAL to the guarded baseline. sigil would have attested five elisions that never happened. Now gated on the arm backend; the loud zero-elision path names the backend, and the attestation records 0 of 5. DEFECT 2 — SILENT NO-OP ON THE SINGLE-FUNCTION PATH. --func-index / --func-name never reach compile_all_exports, so --proven-safe there produced no ingestion, no diagnostic, no attestation, exit 0. That is the #865 shape (the v0.52 headline was a flag that quietly did nothing). Now a hard error naming the invocation that works. Deliberate asymmetry: a stale or malformed verdict FILE never fails a compile (it is data, and fail-closed handles it); an INVOCATION synth cannot honour is refused, matching --stack-layout's precedent. Also fixed: the zero-elision reason said 'none survived key validation' even when the sites were refused for fact-spec renumbering — it now points at the REFUSED/DROP lines and keeps the byte-offset hint conditional. DE-VACUATED the fact-spec combination gate: it asserted only inside a conditional on the stderr containing 'specialized', so a declining pass would have made it check nothing. Verified the pass DOES specialize this fixture — it admits the redundant-mask elision on the slot mask, deleting two operators (38 -> 36) and renumbering every index after them, which is exactly the skew the refusal exists for. The gate now asserts the specialization, the renumbering, the refusal AND the zero-elision attestation. RED-FIRST (mutation): forcing the backend-support flag to true turns non_arm_backends_attest_zero_elisions_901 RED (12 passed / 1 failed). Reverted. 13 byte gates (14 with --features verify), differential 207/207, frozen anchors 10/10, clippy -D warnings exit 0, claim_check 38/38. Bazel needs no change: crates/BUILD.bazel globs synth-core sources and no new external dependency was added. Implements: VCR-MEM-004 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

codecov · 2026-08-05T17:22:38Z

Codecov Report

❌ Patch coverage is 95.83333% with 29 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-cli/src/main.rs	86.61%	17 Missing ⚠️
crates/synth-backend/src/arm_backend.rs	47.36%	10 Missing ⚠️
crates/synth-core/src/proven_safe.rs	99.53%	2 Missing ⚠️

📢 Thoughts on this report? Let us know!

…face (#910) `Claim Check` went red on the lane's OWN gate, correctly. Two oracles reached main AFTER the floors were measured and declare nothing: scripts/repro/i64_high_reg_zero_fill_916_differential.py (via #919) scripts/repro/proven_safe_bounds_901_differential.py (via #915) Both are real unicorn+wasmtime execution differentials, so both get `emulations >= N`. Floors MEASURED through the driver, never guessed — a guessed floor is the vacuous number this lane exists to remove: #916 measured=48 emulations=48 wasmtime_calls=48 #901 measured=371 emulations=371 wasmtime_calls=188 compiles=5 Both steps now route through `scripts/oracle_run.py`, so they report to the per-job ledger like every other wired oracle. This RETRACTS the comment I added in the previous commit claiming the #916 harness could not be bound and that declaring a floor was a follow-up: the gate disagreed, and the gate was right. Its weak-floor table row is dropped for the same reason. Totals move 133 -> 135 oracles, 294,914 -> 295,333 emulator entries. THE FIND: that number lives on THREE surfaces, and only two were pinned. ORACLE_WIRING.md and ci.yml are in `claims.yaml`; the FEATURE_MATRIX template was not — so with the matrix still reading "133 oracles assert 294,914" the ledger reported 42/42 HOLD. A number quotable in a shipped doc and bound to no gate is #880 exactly: the gate checked the matrix against its RENDER, never its CONTENT. Added SYNTH-ORACLE-CHECK-FLOORS-910-MATRIX, pinned on the TEMPLATE rather than the generated file — pinning the render is satisfiable by faithfully regenerating wrong prose. Negative-controlled, not assumed: reverting the template to 133/294,914 yields `FAIL SYNTH-ORACLE-CHECK-FLOORS-910-MATRIX`; restoring gives 43/43. Local: oracle wiring 159 scripts, 0 UNDECLARED, emulations 135 / floor 295333. Refs #910, #918

…sert what the oracles actually execute (#910) (#918) * docs(#910): rivet — VG-009/VG-010, the two evidence-INSTRUMENT gaps Traceability leads the lane. VG-001..VG-008 all say "a property is not yet proven"; these two say something different in kind — an instrument REPORTS something other than what its name implies, and the measurement itself is the defect. VG-009 (#910): `Code Coverage` runs `cargo llvm-cov --workspace`, i.e. the Rust test suite. The execution differentials spawn the compiler as a separate, UNINSTRUMENTED process from different CI jobs, so every one of those executions is invisible to the percentage — it understates real testing AND cannot be read as completeness. Records the v0.54.0 measurement and the decline of #910 option 1 with its reason (instrumenting the binary changes the artifact under test; the differentials exist to execute the SHIPPED bytes). VG-010 (#910 F10): measured — 152 of the 160 workflow steps that run a scripts/repro/ oracle assert nothing beyond the process exit code. Not only the 63 wired by #890; the pre-existing hand-wired steps too. Exactly 8 assert a printed verdict or count. Both carry the RESOLUTION TAKEN so the artifact states the shipped decision, not just the complaint. * docs(#910): the coverage number now says what it measures (option 2) `Code Coverage` -> `Rust-test Line Coverage (unit + integration only)`. The old name implied whole-system coverage; the job runs `cargo llvm-cov --workspace`, i.e. one population — the Rust test suite, in-process. The scope note travels WITH the number in three places, because a caveat that lives somewhere else does not survive being quoted: * the job body, for whoever edits it; * `$GITHUB_STEP_SUMMARY`, so reading the percentage and reading the caveat are the same act; * the README, under the badge. All three say the same two things: the number UNDERSTATES the testing that exists (the differentials run an uninstrumented subprocess from other jobs, so `backend.rs` reads ~42 % while being exercised end-to-end by nearly every differential), and it is NOT a completeness measure. Verified before renaming that `Code Coverage` is NOT among main's 9 required status checks — renaming a required context deadlocks every merge until branch protection is updated, which is a coordinator decision, not a lane one. gh api repos/pulseengine/synth/branches/main/protection/required_status_checks --jq '.contexts' ["Format","Clippy","Test","Z3 Verification","Claim Check", "Version Pin Sweep","Bazel Build & Proofs","Kani Verification", "Rivet Validation"] No emitted byte moves; 37/37 claims still hold. * feat(#910 F10): oracle steps assert EXECUTION, not exit status Measured first, because the premise was understated: not 63 but **152 of the 160 workflow steps** that run a `scripts/repro/` oracle asserted nothing beyond the process exit code. Exactly 8 asserted a printed verdict or count — and the pre-#890 hand-wired steps are mostly in the bare 152 too. Exit 0 does not distinguish "emulated 240 vectors, all bit-identical" from "the fixture list came back empty, printed PASS". That is #890's inert gate one level down: wired, but what it attests is unstated. MECHANISM — `scripts/oracle_run.py`, an in-process driver (runpy) that wraps three entry points and counts them: unicorn.Uc.emu_start -> emulations wasmtime.Func.__call__ -> wasmtime_calls subprocess `synth … compile …` -> compiles The count comes from the emulator, not from the harness's own bookkeeping, so a comparison loop that never runs cannot fake it. Chosen over 152 bespoke greps because it is uniform and needs no edit to any harness; chosen over #910 option 1 (instrumenting the binary) because that changes the artifact under test. DECLARATION — one `# ci-checks:` header per oracle, same locality argument as `# ci-status:`: the floor lives in the file it describes and cannot outlive it. Floors are `>=`, never equality, so adding a fixture cannot redden a step. CALIBRATION, not assumption — every floor below is a MEASURED value, obtained by executing each CI oracle step VERBATIM (parsed out of ci.yml, so there is no transcription drift) with the invocation routed through the driver. Four oracles that self-report a check count agree with the driver 1:1: gpio_thin_846 prints `#846 CHECKS=75/75` driver 75 aarch64_call_indirect_851 prints `35 checks (23 trap, 12 value)` driver 35 aarch64_globals_851 prints `17 checks` driver 17 aarch64_float_completion_851 (the "662 float-boundary checks") driver 662 150 wired oracles now declare: emulations 133 scripts 294,914 emulator entries asserted stdout 7 scripts 458 printed counts asserted compiles 9 scripts 43 compilations asserted none 1 script aarch64_matrix.sh — a POSIX shell oracle the in-process driver cannot instrument; its step already carries its own >= 32 accepted-ops assertion The mode is the STRONGEST that holds on EVERY invocation: several oracles run twice, once executing and once on a decline / byte-identity leg that executes nothing by design, and a floor that only holds for the good leg is not a floor. The weaker floor loses nothing — every counter is still measured and recorded. 159 CI step lines routed. The one deliberately NOT routed is the #275 RED non-vacuity step (`! python …`), which inverts its verdict: routing it would file a below-floor record for a run that is SUPPOSED to fail. No emitted byte moves; no existing assertion removed. * feat(#910): the check-floor ledger — report the population, ratchet the floor Two gates on top of the per-step floors: 1. `oracle_wiring_check.py` now also requires a `# ci-checks:` declaration on every `wired` oracle, and sums the floors PER MODE. It shares the driver's parser by importing it (`_load_oracle_run`) rather than re-implementing the grammar — two hand-maintained copies of one declaration format is the mirror-drift shape this repo keeps paying for. `--min-emulation-floor 294914` is the RATCHET, wired into the existing (required) `Claim Check` job rather than a new job — a brand-new job is not a required context on main and could sit red for weeks, which is the exact failure #890 exists to kill. Anti-vacuity in the gate itself: zero declared emulation floor is a hard failure, not a clean sheet. 2. `scripts/oracle_evidence.py` closes every oracle job with what it MEASURED, from the JSONL the driver appends to ($ORACLE_EVIDENCE_JSONL, set at workflow level so no oracle job can forget it). It asserts every record met its floor AND that the expected number of oracles reported at all — a step deleted, commented out or skipped by an early exit leaves the ledger short, and a short ledger is a red job rather than a quietly smaller number. Wired into 37 oracle jobs with their own `--min-oracles` count. REPORTED PER UNIT, NEVER SUMMED ACROSS UNITS. Emulator entries, wasmtime reference executions and compilations are three different things; one impressive combined figure is precisely the defect #910 is about. Both step summaries say so, and say that none of it is visible to `Rust-test Line Coverage` — the two populations are reported side by side and never added. Both directions exercised locally: --min-oracles 2 green on a 2-record ledger, --min-oracles 3 red on the same ledger with the reason printed. * docs(#910): pin the two populations — ledger, policy doc, CHANGELOG claims.yaml gains four entries, all pinned to CAPABILITY GAPS rather than issue numbers (the v0.53 burn: a ledger pinned to a CLOSED issue green-confirms a false residual, and correcting the prose then turns it RED): SYNTH-ORACLE-CHECK-FLOORS-910 — every wired oracle carries a floor (count-min 150), the execution population does not shrink (count-min 133), and the "nothing can be bound" hatch stays at ONE (count-max 1) SYNTH-ORACLE-CHECK-FLOORS-910-CI — the doc's number and the number the gate ENFORCES cannot drift, and the routing cannot be quietly undone (count-min 159 routed steps, 37 job ledgers) SYNTH-COVERAGE-SCOPE-910 — the scope caveat cannot be dropped while SYNTH-COVERAGE-SCOPE-910-README the percentage stays quotable ORACLE_WIRING.md gains the whole #910 half: the mechanism, why a driver instead of 152 greps, why #910 option 1 was declined, the declaration grammar, the CALIBRATION table (four self-reporting oracles agreeing 1:1), the per-mode floor table, the "this is not the coverage percentage and must never be added to it" section, and the itemized weak-floor list. The FEATURE_MATRIX template (a source file) drops the now-closed "the sweeps assert exit status rather than a per-script check count" residual and states both #910 outcomes; docs/status/FEATURE_MATRIX.md regenerated via --emit-status, never hand-edited. 41/41 claims hold. * test(#910): prove the check-floor gates by MUTATION — 7 legs, all red The mechanism must not become the thing it polices. Each leg runs the step EXTRACTED VERBATIM from ci.yml (yaml.safe_load -> the step's `run:` block -> bash -e), so nothing here is a transcription of what CI does. M1 harness returns before its comparison loop -> driver measured 0, step RED M2 one floor lowered to 0 -> ratchet 294912 < 294914 RED M3 `# ci-checks:` header deleted -> wiring gate RED M4 stdout regex with no capture group -> driver rejects, RED M5 a routed step demoted to a COMMENT -> wiring gate RED M6 oracle steps un-routed -> claims count-min RED M7 job ledger short (1 of 15 oracles) -> ledger RED BASELINE and RESTORED both green; `git status --porcelain` empty afterwards. M1 is the load-bearing leg: the mutated harness STILL prints `ORACLE: PASS` and STILL exits 0. A `grep -q '^ORACLE: PASS'` would have greened it, and so would every one of the 152 exit-status-only steps this replaces. Only the emulator count catches it — because that count does not come from the harness. M5 re-proves the v0.54 comment-stripping fix under this lane's edits rather than assuming it: 159 `run:` bodies were rewritten here, and that is precisely the surface the fix covers. M6's nuance is written down rather than rounded off — the substitution hit both the `python3` and `python` spellings, so it un-routed two lines (159 -> 157), not one. The leg proves the direction. * fix(#918): three red gates, three defects in the instruments (#910) All three failures were this lane's own, and none was the CI-floor calibration the lane predicted. Reading the logs beat predicting them. 1. WCET sweep — "ledger SHORT: 3 oracles, expected >= 4". A TRUE POSITIVE with its root cause in the ledger's own harness. `ORACLE_EVIDENCE_JSONL` is a RELATIVE path and oracles run in-process (runpy), so a harness that chdir's redirects the append into its own scratch directory, which is then deleted. Exactly one of the four WCET phase scripts chdir's (phase2, line 213) and exactly that one's record went missing — 17 emulations recorded of 25 executed. Fixed twice over, because they are different failure modes: - resolve the ledger to an ABSOLUTE path at import, before any oracle can move the cwd; - restore `os.getcwd()` in run_oracle's finally block. It already restored sys.argv and sys.path; the third piece of interpreter state an in-process oracle can move was the one that bit. Red-first: a chdir'ing fixture records 0 ledger lines before, 1 after. No new gate — the --min-oracles assert IS the regression test for this class; it is what caught it. 2. Instrument independence — the failing step is `git diff --exit-code`, the assert that the v0.53 mutation never persists. The oracle steps `tee` into *.out AND those files were COMMITTED, so every fresh run dirties the tree and trips a soundness assert that has nothing to do with the mutation. Untracked all five and ignored them; the steps that produce and consume them at runtime are unchanged. 3. Rivet Validation — VG-009/VG-010 were typed `sys-verification`, a verification MEASURE, which rivet requires to `verifies` a system requirement. They are recorded GAPS and verify nothing. Typed `system-req` as VG-001..VG-008; their links already matched that shape. The species distinction the file draws is real, but it belongs in the prose, not the schema type. Refs #910, #918 * fix: the merge left conflict markers in ci.yml — the workflow could not parse A merge-created defect, present in NEITHER parent. The merge conflicted in TWO files; I read the output through `tail -5` and saw only the CHANGELOG one, then `git add -A` staged ci.yml with its markers intact and the commit succeeded. GitHub reported it as `.github/workflows/ci.yml: failure` with ZERO checks — not a red gate, an ABSENT one, which is the harder failure to notice. Resolved keeping both sides: #599 keeps this lane's oracle_run.py routing, and main's new #916 zero-fill differential is kept verbatim as raw `python` — it carries no `# ci-checks:` header and the driver hard-errors on a script it cannot bind a floor to. Listed in the weak-floor table so the residue stays counted rather than silently unrouted. Also corrects the ORACLE_WIRING.md path in VG-010 and in the new comment: the file is at scripts/repro/, never docs/development/. Post-merge asserts, since resolving one conflict is not resolving the merge: zero conflict markers tree-wide, and both edited YAML files parse. * fix(#918): declare the two undeclared oracles — and pin the third surface (#910) `Claim Check` went red on the lane's OWN gate, correctly. Two oracles reached main AFTER the floors were measured and declare nothing: scripts/repro/i64_high_reg_zero_fill_916_differential.py (via #919) scripts/repro/proven_safe_bounds_901_differential.py (via #915) Both are real unicorn+wasmtime execution differentials, so both get `emulations >= N`. Floors MEASURED through the driver, never guessed — a guessed floor is the vacuous number this lane exists to remove: #916 measured=48 emulations=48 wasmtime_calls=48 #901 measured=371 emulations=371 wasmtime_calls=188 compiles=5 Both steps now route through `scripts/oracle_run.py`, so they report to the per-job ledger like every other wired oracle. This RETRACTS the comment I added in the previous commit claiming the #916 harness could not be bound and that declaring a floor was a follow-up: the gate disagreed, and the gate was right. Its weak-floor table row is dropped for the same reason. Totals move 133 -> 135 oracles, 294,914 -> 295,333 emulator entries. THE FIND: that number lives on THREE surfaces, and only two were pinned. ORACLE_WIRING.md and ci.yml are in `claims.yaml`; the FEATURE_MATRIX template was not — so with the matrix still reading "133 oracles assert 294,914" the ledger reported 42/42 HOLD. A number quotable in a shipped doc and bound to no gate is #880 exactly: the gate checked the matrix against its RENDER, never its CONTENT. Added SYNTH-ORACLE-CHECK-FLOORS-910-MATRIX, pinned on the TEMPLATE rather than the generated file — pinning the render is satisfiable by faithfully regenerating wrong prose. Negative-controlled, not assumed: reverting the template to 133/294,914 yields `FAIL SYNTH-ORACLE-CHECK-FLOORS-910-MATRIX`; restoring gives 43/43. Local: oracle wiring 159 scripts, 0 UNDECLARED, emulations 135 / floor 295333. Refs #910, #918

avrabe and others added 8 commits August 5, 2026 18:04

avrabe mentioned this pull request Aug 5, 2026

Bounds-check elision for synth: export proven-safe access sites + close the br_if precision gap pulseengine/scry#114

Open

avrabe merged commit c1bdb95 into main Aug 5, 2026
57 checks passed

avrabe deleted the feat/901-proven-safe-bounds branch August 5, 2026 17:34

Navigation Menu

Uh oh!

feat(#901): ProvenSafeBoundsChecker — fail-closed, attested bounds-check elision from scry's proofs (VCR-MEM-004) - #915

feat(#901): ProvenSafeBoundsChecker — fail-closed, attested bounds-check elision from scry's proofs (VCR-MEM-004)#915
avrabe merged 8 commits into
mainfrom
feat/901-proven-safe-bounds

avrabe commented Aug 5, 2026

Uh oh!

codecov Bot commented Aug 5, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

avrabe commented Aug 5, 2026

What

The deliverable is the refusal logic, not the speedup

Measured

Attestation (loop step 6 — breaks a 3-release N/A streak)

Red-first evidence

Defects the gates found mid-flight

Gates

Residuals, named not hidden

Note for assembly

Uh oh!

codecov Bot commented Aug 5, 2026

Codecov Report

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant