Bounds-check elision for synth: export proven-safe access sites + close the br_if precision gap

[avrabe]

Context and credit

WasmBounds (Emma Sudo & Keith Winstein, Stanford — paper) applies abstract interpretation to elide Wasm memory bounds checks, and reports a measured 1.21× speedup on a dot-product microbenchmark. It is an early-stage project (their words), but it does two things we have not: it states the motivation crisply and it measures the payoff end to end.

Their motivation section is the clearest statement I've seen of why this matters for our embedded target: hardware guard pages need virtual memory, so on no-MMU embedded — and, increasingly, under the Memory64 and Custom Page Sizes proposals — runtimes fall back to a software bounds check on every memory access. synth's own SoftwareBoundsChecker documents that cost as "~25-40% overhead".

scry already computes the verdict (TrapCheck{kind: OutOfBounds, verdict: ProvenSafe} via region_in_bounds). What's missing is an export a compiler can consume, and one guard idiom that matters for real loop code.

1. Export: safe-accesses.json (schema v1)

Keyed on the wasmparser operator index space — the same space synth's frontend consumes, so no source re-mapping step.

{
  "schema": "scry/safe-accesses/v1",
  "scry_version": "3.2.4",
  "module_sha256": "<hex>",
  "memory_min_bytes": 65536,
  "premises": { "bounded_memory": true },
  "proven_safe": [ { "func": 4, "pc": 41, "op": "i32.load", "width": 4 } ],
  "counts": { "access_sites": 0, "proven_safe": 0 }
}

Soundness contract (belongs in the schema doc):

• module_sha256 binds the verdicts to one exact module; the consumer fails closed on mismatch. Eliding on a stale analysis is a memory-safety hole, not a stale optimisation.
• Verdicts are proven against memory_min_bytes, the guaranteed floor. Wasm memory only grows, so a site proven in-bounds against the floor stays in-bounds under memory.grow.
• Absence from proven_safe means "not proven", never "unsafe".

This mirrors WasmBounds' output contract — "a non-exhaustive list of provably safe memory instruction offsets" that any runtime can consume — which is a good, simple interface worth copying.

2. Precision: br_if on a bare value

Our guard refinement recognises local.get X; i32.const c; <cmp>; br_if, local.get X; i32.eqz; br_if, and the two-local compare (try_guard_brif / try_guard_brif_rel). It does not yet handle local.tee $x; br_if — a branch on the raw value's truthiness (implicit ≠ 0), which is what LLVM emits for count-to-zero loops.

WasmBounds' BrIf rule covers this case: the fall-through edge gets the local = {0}, the taken edge gets ≠ 0. It's the dual of the i32.eqz shape we already support, and it's worth adding.

Their mechanism for it generalises better than ours, too: they pair each operand-stack entry with the expression that produced it, so br_if knows the popped value is local $x. Ours is a syntactic peephole over ops[pc..pc+4]. A light provenance tag (Local(i) | Const | Mem | Other) on the abstract stack would make refinement general rather than idiom-matched.

3. Domain choice: keep intervals + congruence

WasmBounds tracks sets of intervals, which keeps branch-disjointness precise and supports their fixpoint without a widening heuristic (they note widening as future work).

For scry we should keep our current stack, for a specific reason: for the in-bounds decision a disjunctive set and its hull are equivalent — proving every element in bounds is the same as proving the hull in bounds, since the hull's endpoints are attained by elements. So our single interval already answers this question as precisely, and our threshold widening + narrowing (FEAT-016/042) reaches the fixpoint without unrolling. Where a set would otherwise help — stride/alignment — we have the known-bits congruence domain (FEAT-037).

Worth revisiting if we find a case where branch-disjointness matters for a decision other than in-bounds.

4. Measure it

We have never published "% of i32.load/i32.store sites proven safe". That's the number that makes the capability legible, and the input to the synth-side benchmark.

Related: pulseengine/synth#901 (consumer side), FEAT-046 (OOB verdicts), FEAT-061 (loop-range memory content), REQ-004 (invariants for consumers).

[avrabe]

Consumer side landed — pulseengine/synth#915 (synth VCR-MEM-004, #901)

synth now consumes safe-accesses.json behind synth compile --proven-safe. Two things to confirm on the producer side, plus one number you asked for.

1. pc — I read it as the 0-based OPERATOR index, and made the guess self-checking

The schema says "wasmparser operator index space", and §2 here describes the refinement as a peephole over ops[pc..pc+4], so I took pc to be the 0-based index of the operator within the function body — not a wasm byte offset. That drops straight onto synth's op_offsets side-table and onto the existing #494 per-site elision marks, so there is no source-mapping step, which is what the schema was aiming for.

Since the producer isn't shipping yet, synth does not bet on that reading. Ingestion validates every entry against the decoded stream:

• func must exist and pc must be in range for that function's operator count;
• the operator at pc must be a linear-memory access;
• its access width must equal the declared width (bytes touched, so i32.load8_u is 1 and i64.load32_u is 4).

An entry that fails any of these is dropped with a counted diagnostic. So if scry emits byte offsets instead, essentially every entry falls out of range and synth elides nothing, loudly — rather than stripping a bounds check off the wrong access. Please confirm the operator-index reading so we can both write it down normatively; if you'd rather emit byte offsets, say so and I'll key on op_offsets instead (same table, different column).

2. Fields synth treats as load-bearing

module_sha256, memory_min_bytes, and each entry's width are all fail-closed inputs — the first two refuse the whole document on mismatch, the third drops the entry:

• module_sha256 is verified against the exact bytes synth hands its decoder (post-.wat-parse, post-loom, post-arena-bind). That is deliberate: a pre-compile rewrite that shifts function/operator indices also changes those bytes, so index skew and byte skew collapse into one gate. Please hash the module you analysed, byte for byte.
• memory_min_bytes must equal synth's own declared linear-memory minimum for that module. A matching hash implies they agree, so a disagreement means one of us is broken and synth refuses rather than trusting it.
• scry_version is recorded in synth's attestation sidecar and is not used for gating. premises and counts are currently ignored (tolerated, forward-compatible) — tell me if premises.bounded_memory: false should be a refusal and I'll wire it.

3. The number from §4, from the consumer end

On synth's fixture (Cortex-M4, --safety-bounds software, 8 guarded i32 accesses, 5 of them provable by exactly the interval + known-bits reasoning you describe): eliding those 5 takes the function from 232 B → 152 B (80 B, 58 % of the 138 B bounds-guard tax) and 70 → 45 executed instructions. Proving all 8 lands byte-identical to the unguarded build — under proof, the sandbox tax is exactly zero.

So the "% of i32.load/i32.store sites proven safe" metric you propose in §4 is the right one: on this shape the payoff is close to linear in it, and it is the number that makes the capability legible on both sides.

4. Also worth knowing

Absence from proven_safe is treated as "not proven", never "unsafe" — a partial list produces a partially-guarded binary, so a non-exhaustive export is entirely safe to ship. And synth writes a synth-proven-safe-elisions-v1 attestation naming scry as the authority for each elided site (emitted on refusal too), so the chain from your verdict to the emitted bytes is auditable end to end.