ProvenSafeBoundsChecker: elide software bounds checks using scry's proven-safe verdicts

[avrabe]

Why now

WasmBounds (Emma Sudo & Keith Winstein, Stanford — paper) uses abstract interpretation to identify provably in-bounds Wasm memory accesses so their bounds checks can be elided, and reports a measured 1.21× speedup. It's an early-stage project, but it demonstrates the payoff end to end — which we haven't done.

Their motivation is precisely synth's target: hardware guard pages need virtual memory, so on no-MMU embedded — and under the Memory64 and Custom Page Sizes proposals — runtimes fall back to a software bounds check on every memory access. synth-memory/src/bounds.rs already documents SoftwareBoundsChecker as "portable, ~25-40% overhead".

WasmBounds is deliberately engine-agnostic: it emits a list of safe offsets that any runtime can consume. Our situation is different in a way we should exploit — we own both halves of the pipeline. scry proves the access in-bounds (admit-free Rocq) and synth proves the codegen correct (Rocq), so we can make the elision proof-carrying and attested on Cortex-M/R and RISC-V.

The seam already exists

synth-memory/src/bounds.rs defines a pluggable BoundsChecker trait with a BoundsCheckOverhead category. There is no scry-informed strategy today (grepped synth-memory/synth-opt/synth-analysis for elide|proven_safe|scry — nothing). scry is already a synth dependency with a live green gate (scry_shadow_stack_budget, VCR-MEM-001/#383, re-verified across scry v2.3→v2.6), so the consumption channel is proven.

Proposal: ProvenSafeBoundsChecker

Consumes scry's safe-accesses.json (schema scry/safe-accesses/v1, specced in pulseengine/scry#114):

{ "schema": "scry/safe-accesses/v1", "module_sha256": "<hex>",
  "memory_min_bytes": 65536,
  "proven_safe": [ { "func": 4, "pc": 41, "op": "i32.load", "width": 4 } ] }

Behaviour:

1. Fail closed on hash mismatch. Verify module_sha256 against the module being compiled; on mismatch elide nothing and warn. Eliding on a stale analysis is a memory-safety hole, not a stale optimisation.
2. Sites in proven_safe emit no check; everything else delegates to SoftwareBoundsChecker (absence means "not proven", never "unsafe").
3. Record the elision count + scry version/module hash so sigil can attest what was elided and on whose authority.

Keying is on the wasmparser operator index (func_index, pc) — the index space synth's frontend already consumes, so there's no source-mapping step and the attestation chain stays intact.

Soundness note: verdicts are proven against the memory's guaranteed minimum size. Wasm memory only grows, so the elision stays valid under memory.grow.

Benchmark

Via synth-qemu on Cortex-M, measure both axes against the SoftwareBoundsChecker baseline:

• .text size delta — on our embedded targets flash footprint is often the binding constraint, and it's an axis our own toolchain is well placed to measure directly.
• cycles/iteration — comparable to the 1.21× WasmBounds reports.

This also converts synth's own "~25-40% overhead" doc comment from an asserted claim into a measured one.

Related: pulseengine/scry#114 (producer side), scry FEAT-046 (OOB verdicts).