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

.github/workflows/ci.yml

@@ -1207,6 +1207,68 @@ jobs:
           SYNTH: ./target/debug/synth
         run: python scripts/repro/fact_spec_rem_494_differential.py
 
+  proven-safe-oracle:
+    name: proven-safe bounds-elision oracle (VCR-MEM-004, #901)
+    # VCR-MEM-004 (#901): `--proven-safe` consumes scry's safe-accesses.json
+    # (schema scry/safe-accesses/v1, scry#114) and elides the
+    # `--safety-bounds software` inline guard at the access sites scry PROVED
+    # in-bounds. This job gates the three safety properties, not the speedup:
+    #   (1) FAIL CLOSED on module_sha256 / memory_min_bytes / malformed input;
+    #   (2) ABSENCE MEANS "NOT PROVEN" — a partial verdict list leaves exactly
+    #       the unproven guards standing, and their out-of-bounds accesses
+    #       still TRAP under execution;
+    #   (3) a genuine elision that is result-identical to wasmtime.
+    # The differential's fail-closed leg is a permanent regression gate: it
+    # applies one module's verdicts to a MUTATED module whose keys all still
+    # validate, so deleting the hash comparison turns it RED with a real
+    # UC_ERR_READ_UNMAPPED (verified by mutation when #901 landed).
+    # Isolated job: emulation deps pip-installed here ONLY.
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v7
+      - uses: dtolnay/rust-toolchain@stable
+      - name: Cache Cargo dependencies
+        uses: actions/cache@v6
+        with:
+          path: |
+            ~/.cargo/registry
+            ~/.cargo/git
+            target/
+          key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
+          restore-keys: |
+            ${{ runner.os }}-cargo-
+      # Unit level: the fail-closed ingestion gates (synth-core) and the
+      # dep-free ProvenSafeBoundsChecker trait semantics (synth-memory).
+      - name: Run ingestion + BoundsChecker unit gates
+        run: cargo test -p synth-core --lib proven_safe && cargo test -p synth-memory --lib
+      # Byte evidence: the partial-list partition, the refusals, the key-space
+      # canary, and the attestation contents.
+      - name: Run --proven-safe byte gates (#901)
+        run: cargo test -p synth-cli --test proven_safe_bounds_901
+      # The fact-spec combination refusal needs the solver-carrying build (the
+      # pass is inert without it), so it is a separate feature-gated run.
+      - name: Run the fact-spec-combination refusal gate (verify feature)
+        run: cargo test -p synth-cli --features verify --test proven_safe_bounds_901
+      - name: Build synth
+        run: cargo build -p synth-cli
+      - uses: actions/setup-python@v7
+        with:
+          python-version: "3.x"
+      - name: Install emulation deps
+        run: pip install wasmtime unicorn pyelftools
+      - name: Run --proven-safe execution differential (#901)
+        env:
+          SYNTH: ./target/debug/synth
+        run: |
+          set -euo pipefail
+          python scripts/repro/proven_safe_bounds_901_differential.py \
+            | tee /tmp/proven_safe_901.log
+          grep -q '^RESULT: PASS' /tmp/proven_safe_901.log
+          # Non-vacuity: a differential that checked nothing must not pass.
+          grep -qE '^#901 CHECKS=[1-9][0-9]*/[1-9][0-9]*$' /tmp/proven_safe_901.log
+          grep -q 'absence-is-not-safety: [1-9]' /tmp/proven_safe_901.log
+          grep -q 'fail-closed: stale verdicts REFUSED' /tmp/proven_safe_901.log
+
   rv32-shift-fold-oracle:
     name: rv32 immediate-shift-fold execution oracle
     # VCR-ORACLE-001 (#242, #472): EXECUTE the RV32 immediate-shift-fold lever

CHANGELOG.md

@@ -7,6 +7,85 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Added
+
+- **`--proven-safe`: bounds-check elision on scry's proof, fail-closed and
+  attested (VCR-MEM-004, #901).** `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 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`. New `synth_memory::ProvenSafeBoundsChecker` (the fifth
+  `BoundsChecker` strategy, and the first proof-informed one) and
+  `synth_core::proven_safe` (ingestion + attestation).
+
+  **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:
+
+  - a `module_sha256` that does not match **the exact bytes handed to the
+    decoder** (after `.wat` parsing, after loom, after the #418 arena-bind
+    rewrite). Binding the hash there is deliberate: a pre-compile rewrite that
+    shifts function/operator indices also breaks the hash, so index skew and
+    byte skew are ONE gate. Eliding on a stale analysis is a memory-safety
+    hole, not a stale optimization;
+  - a `memory_min_bytes` that disagrees with this module's declared floor (a
+    matching hash implies they are equal, so a disagreement means the producer
+    is broken — and a broken prover is not trusted);
+  - a malformed, missing, or wrong-schema file — the `wsc.facts` fail-safe skew
+    rule applied to a JSON carrier. No input can turn a good compile into a
+    failed one;
+  - a `(func, pc)` key that does not validate against the DECODED operator
+    (must exist, must be a linear-memory access, must have the declared access
+    width). scry#114's `pc` is the 0-based **wasmparser operator index**; if a
+    producer ever emitted wasm byte offsets instead, nearly every entry fails
+    this check and the build elides nothing **loudly** rather than stripping
+    the guard off the wrong access;
+  - a function that `SYNTH_FACT_SPEC` specialized, which renumbers the index
+    space the verdicts are keyed in — refused per function, never silently
+    remapped.
+
+  **Absence from the list means "not proven", never "unsafe":** an unlisted
+  site keeps its guard, so a partial verdict list yields a partially-guarded
+  binary. "Flag given, file accepted, nothing elided" is diagnosed by name
+  rather than reported as success.
+
+  **The flag never silently does nothing.** Guards are stripped on the ARM
+  backend under `--safety-bounds software`; under any other backend or bounds
+  mode the verdicts are still ingested and verified, but the attestation
+  records ZERO elisions and names the reason, so it can never claim an elision
+  that did not happen. On the single-function path (`--func-index` /
+  `--func-name`), which builds no marks and has no attestation surface, the
+  flag is REFUSED loudly rather than ignored (the #865 silent-no-op shape).
+
+  **Attestation (sigil):** every `--proven-safe` compile writes
+  `<output>.proven-safe-elisions.json` (`synth-proven-safe-elisions-v1`) with
+  the elision set, each site's authority, the scry version, both module hashes
+  and both memory floors — **emitted on refusal too**, so sigil can tell
+  "nothing to elide" from "file rejected".
+
+  **Measured** on `scripts/repro/proven_safe_bounds_901.wat` (Cortex-M4, 8
+  guarded accesses, 5 proven): `probe` **232 → 152 B** (80 B, 58 % of the
+  138 B guard tax, 34.5 % of the function) and **70 → 45 executed
+  instructions** (36 %). Proving all 8 lands byte-identical to the
+  `--safety-bounds`-off floor. The per-site win is the same magnitude #494
+  publishes because it is the same guard strip — what is new is the authority
+  and the fail-closed binding, not the byte. 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), pinned in `claims.yaml`.
+
+  Gated by `crates/synth-cli/tests/proven_safe_bounds_901.rs` (11 byte gates)
+  and `scripts/repro/proven_safe_bounds_901_differential.py` (207 checks,
+  unicorn vs wasmtime, CI-wired in the new `proven-safe-oracle` job): an
+  in-bounds sweep where elided ≡ guarded ≡ wasmtime on return value AND the
+  full 64 KiB memory image, out-of-bounds accesses at NOT-PROVEN sites that
+  still trap, and a fail-closed leg that applies one module's verdicts to a
+  mutated module whose keys all still validate — deleting the hash comparison
+  turns it RED with a real `UC_ERR_READ_UNMAPPED`. Opt-in; frozen anchors
+  10/10 (the mark vector defaults empty).
+
 ## [0.54.0] - 2026-08-05
 
 **"Close what we measured."** v0.53 built the instruments; this release acts on

artifacts/verified-codegen-roadmap.yaml

@@ -3102,6 +3102,131 @@ artifacts:
         on stack_canary_687 / i64_global_init_649 / control_step self-contained
         images.
 
+  - id: VCR-MEM-004
+    type: sw-req
+    title: "ProvenSafeBoundsChecker: fail-closed elision of software bounds guards from scry's proven-safe verdicts (synth #901, scry #114)"
+    description: >
+      WasmBounds (Sudo & Winstein, Stanford CS191 Spring 2026) shows the payoff
+      end to end: abstract interpretation identifies provably in-bounds wasm
+      memory accesses, their bounds checks are elided, and they measure 1.21x.
+      Their motivation IS synth's target — hardware guard pages need virtual
+      memory, so on no-MMU embedded (and under Memory64 / Custom Page Sizes)
+      every access falls back to a SOFTWARE bounds check. synth's own
+      `synth_memory::SoftwareBoundsChecker` documents that cost as
+      "~25-40% overhead", and `--safety-bounds software` emits the #752
+      wraparound-safe SUB/CMP/BHS/UDF/CMP/BLS/UDF guard (16 B) at every i32
+      access site.
+
+      Difference from WasmBounds: we own BOTH halves. scry proves the access
+      in-bounds (sound AI, admit-free Rocq) and synth proves the codegen
+      correct (Rocq), so the elision is PROOF-CARRYING and ATTESTED rather than
+      a trusted optimizer flag. This artifact is the CONSUMER side; the producer
+      is scry #114 (`safe-accesses.json`, schema `scry/safe-accesses/v1`,
+      FEAT-046 OOB verdicts). Relation to VCR-PERF-002 (#494): #494 already
+      strips this exact guard, but its authority is a PER-SITE ordeal obligation
+      discharged inside synth from loom's `wsc.facts` premises. VCR-MEM-004
+      reuses the SAME per-site strip mechanism
+      (`InstructionSelector::apply_mem_bounds_elision`) under a DIFFERENT
+      authority: a whole-module external abstract interpretation, hash-bound to
+      one exact module. The two are independent evidence channels for one
+      mechanism, and the sidecar records WHICH one authorized each site.
+
+      SAFETY PROPERTIES — these are the deliverable, not the speedup:
+        (1) FAIL CLOSED on `module_sha256` mismatch. The hash is verified
+            against the EXACT bytes handed to the decoder (post-WAT-parse,
+            post-loom, post-#418 arena-bind), so any pre-compile module rewrite
+            that shifts function/op indices ALSO breaks the hash and refuses —
+            index skew and byte skew collapse into one gate. Eliding on a stale
+            analysis is a memory-safety hole, not a stale optimization.
+        (2) ABSENCE MEANS "NOT PROVEN", NEVER "UNSAFE". A site not listed in
+            `proven_safe` delegates to `SoftwareBoundsChecker` unchanged. The
+            verdict list is non-exhaustive by contract (WasmBounds' own output
+            contract), so a partial list must yield a partially-guarded binary.
+        (3) FAIL CLOSED on `memory_min_bytes` disagreement. Verdicts are proven
+            against scry's declared floor; if it differs from synth's declared
+            minimum for this module, every verdict is unsound HERE — refuse and
+            name both values. (A matching hash implies they agree, so a
+            mismatch means the producer is broken, and trusting a broken prover
+            is the hole this artifact closes.)
+        (4) SELF-CHECKING KEY. `(func, pc)` is the wasmparser operator index
+            space — `pc` is the 0-based op index within the function body (the
+            space scry's own guard refinement walks as `ops[pc..pc+4]`, and the
+            space synth's `op_offsets` side-table and #494's elision marks are
+            indexed by). Ingestion VALIDATES each entry against the decoded
+            stream: `func` must exist, `pc` must be in range, and the op at
+            `pc` must be a memory access whose access width matches the
+            declared `width`. A mismatch DROPS that entry with a counted
+            diagnostic — so if the producer ever emits byte offsets instead of
+            op indices, essentially every entry fails validation and the build
+            elides NOTHING loudly, instead of stripping the guard off the wrong
+            access silently.
+        (5) MALFORMED / MISSING / UNPARSEABLE ⇒ no elisions WITH a diagnostic,
+            never an error and never partial trust — the `wsc.facts` fail-safe
+            skew rule (`synth_core::wsc_facts`, loom#231 Q4) applied to a JSON
+            carrier.
+        (6) FACT-SPEC COMBINATION REFUSED. `SYNTH_FACT_SPEC` may REWRITE the op
+            stream before selection (`SpecializedFn::kept`), which renumbers the
+            index space `pc` is stated in. When a function was specialized, its
+            scry marks are DROPPED with a loud per-function diagnostic rather
+            than remapped — a remap is a future increment that must be gated on
+            its own differential, not assumed.
+        (7) ZERO-ELISION IS LOUD. `--proven-safe` accepted but nothing stripped
+            is the failure mode that looks like success. Every reason is named:
+            file refused, no site validated, `--safety-bounds` not `software`,
+            or the function took the optimized path (`optimizer_bridge`'s
+            `push_software_bounds_guard` sites are NOT mark-driven — the same
+            boundary #494 has).
+
+      ATTESTATION (loop step 6, sigil): every `--proven-safe` compile writes
+      `<out>.proven-safe-elisions.json` (schema
+      `synth-proven-safe-elisions-v1`) carrying the accepted/refused verdict
+      and its reason, `scry_version`, `module_sha256`, `memory_min_bytes`, the
+      `--safety-bounds` mode, and the per-site elision set (func, pc, op,
+      width) — emitted ON REFUSAL TOO, so sigil can distinguish "nothing to
+      elide" from "file rejected" instead of reading a brag sheet.
+
+      CRATE GRAPH (the `shadow_budget.rs` shape, deliberately): ingestion, hash
+      verification and attestation live in `synth-core` (which already carries
+      `sha2`/`serde_json`); the named `ProvenSafeBoundsChecker` lives in
+      `synth-memory/src/bounds.rs` beside the `BoundsChecker` trait and is
+      DEP-FREE (its whole dep list is `bitflags` and it supports no_std). synth-
+      memory is `publish = false` and nothing depends on it, so a CLI path dep
+      is impossible without changing the published surface; the two halves are
+      joined by this documented contract, not a compile-time link. Named
+      residual, not hidden.
+    status: implemented
+    tags: [codegen, memory, bounds-elision, scry, proof-carrying, attestation, sigil, track-c, synth-901, scry-114]
+    links:
+      - type: derives-from
+        target: VCR-001
+      - type: traces-to
+        target: VCR-MEM-001
+      - type: traces-to
+        target: VCR-PERF-002
+    fields:
+      req-type: functional
+      priority: should
+      verification-criteria: >
+        RED-FIRST, one per safety property, all three failing before the change
+        (crates/synth-cli/tests/proven_safe_bounds_901.rs, plus dep-free trait
+        unit tests in synth-memory): (1) a `safe-accesses.json` whose
+        `module_sha256` is one nibble off elides NOTHING and warns — and the
+        MUTATION that inverts the hash comparison turns the differential's
+        out-of-bounds leg RED (a silent OOB access), which is the evidence the
+        gate is load-bearing rather than decorative; (2) a list covering 5 of
+        the fixture's 8 access sites leaves EXACTLY 3 guards standing (byte
+        delta = 5 x 16 B) and an unlisted site still TRAPS under execution;
+        (3) a full list strips all 8 and the compile stays result-identical to
+        wasmtime across an in-bounds sweep. Malformed/missing/wrong-schema/
+        wrong-`memory_min_bytes` files each elide nothing with a NAMED
+        diagnostic and exit 0. Execution differential
+        (scripts/repro/proven_safe_bounds_901_differential.py, unicorn +
+        wasmtime, CI-wired in the same commit): elided ≡ checked ≡ wasmtime on
+        every in-bounds case (return value AND full final memory image), and
+        the not-proven OOB case still traps. Flag-off is byte-identical by
+        construction (the mark vector defaults empty) and locked by the frozen
+        anchors 10/10.
+
   # ---------------------------------------------------------------------------
   # Toolchain completeness — debuggability (not a VCR correctness item, but
   # Tier-2 depends on the VCR-RA value→location mapping)

claims.yaml

@@ -965,6 +965,47 @@ claims:
       - kind: verbatim
         text: 'grep -q "^#846 CHECKS=75/75" gpio846.out'
 
+  # ---------------------------------------------------------------------------
+  # VCR-MEM-004 / #901 — the SoftwareBoundsChecker cost claim.
+  #
+  # `synth-memory/src/bounds.rs` carried "~25-40% overhead" as a bare assertion
+  # for its whole life, and #901's whole premise is that verification pays for
+  # itself against exactly that number. So the doc now states a MEASURED cost,
+  # and this entry pins the doc's numbers to the constants the byte gate
+  # asserts against real compiled bytes. Change the lowering and the gate's
+  # constants move; move them without updating the doc and this reddens.
+  #
+  # What is pinned is the CAPABILITY (a measured guard tax and a measured
+  # recovery on a named fixture), never an issue number — a closed issue would
+  # let the ledger green-confirm a false residual (the v0.53 lesson).
+  # ---------------------------------------------------------------------------
+  - id: SYNTH-PROVEN-SAFE-901-MEASURED
+    doc: crates/synth-memory/src/bounds.rs
+    text: "138 B (+147 %) and 40 instructions"
+    evidence:
+      - kind: verbatim
+        text: "recovers 80 B (58 % of the tax)"
+      - kind: file-exists
+        path: crates/synth-cli/tests/proven_safe_bounds_901.rs
+      - kind: file-exists
+        path: scripts/repro/proven_safe_bounds_901_differential.py
+      - kind: file-exists
+        path: scripts/repro/proven_safe_bounds_901.wat
+      # The doc's 138 B tax and 80 B recovery ARE the gate's constants.
+      - kind: count-eq
+        pattern: "const TAX_ALL_8: usize = 138;"
+        glob: "crates/synth-cli/tests/proven_safe_bounds_901.rs"
+        expect: 1
+      - kind: count-eq
+        pattern: "const SAVED_PROVEN_5: usize = 80;"
+        glob: "crates/synth-cli/tests/proven_safe_bounds_901.rs"
+        expect: 1
+      # Fail-closed is the deliverable: the refusal must stay in the ingestion.
+      - kind: count-eq
+        pattern: "REFUSED — module_sha256 mismatch"
+        glob: "crates/synth-core/src/proven_safe.rs"
+        expect: 1
+
   # ---------------------------------------------------------------------------
   # #890 — the ORACLE-WIRING surface, generalized. SYNTH-GPIO-846-ORACLE-CI-WIRED
   # above pins ONE script's CI wiring by hand; that is the instance-at-a-time