Arc: verify what ships (close #73) — v0.12 control-flow model + division traps

[avrabe]

The arc: "Verify what ships, not a model of it"

The i64-T1 arc (v0.8.0→v0.11.0) gave every i32/i64 op a T1 result-correspondence proof. But #73 names the gap at the center of the project: compile_wasm_to_arm (the proven function) still diverges from instruction_selector.rs (the shipped code), so — in #73's own words — "the proofs are internally valid but do not establish correctness of the shipped binary." For a project whose mission is "AI writes the code — who proves it's safe?", closing this is the 1.0-grade move.

This umbrella tracks the multi-release campaign to close that gap end-to-end.

Roadmap

• v0.12 — control-flow execution model + division trap-guard verification (this milestone, scoped below)
• v0.13 — codegen alignment: register allocation + constant materialization (MOVW/MVN/MOVW+MOVT) + comparison flag-semantics, so Compilation.v is what Rust emits (closes proof: Rocq compile_wasm_to_arm diverges from Rust instruction selector #73 items 2–4)
• v0.14 — whole-function verification: block/loop/br/br_if control flow + AAPCS calls (verified compiler, not verified instruction selection)
• v1.0 — certification-grade safety case: fuse Rocq ⊗ witness (MC/DC) ⊗ sigil (attestation) ⊗ rivet (traceability) into one auditable artifact mapped to a functional-safety standard

---

v0.12 milestone — control-flow exec_program + division traps

The blocker

exec_program (ArmSemantics.v) is a flat sequential fixpoint with no program counter; BCondOffset is modeled as Some s (a no-op). The shipped division code is CMP Rm,#0 / BNE skip / UDF / SDIV — a trap guard that is safety-critical (ARMv7-M SDIV by zero silently returns 0; it does not fault). The current model cannot represent "branch taken skips the UDF," which is exactly why the 4 i32-division theorems are Admitted ("requires PC-relative branching model to skip UDF trap guard").

Design (non-invasive)

1. Add exec_indexed to ArmSemantics.v: PC-indexed, fuel-bounded execution over the instruction vector. BCondOffset cond offset gets real semantics — fall through (pc+1) or jump (pc+offset) based on whether cond holds in the flags; UDF returns None (trap).
2. Bridge lemma: exec_indexed agrees with exec_program on branch-free (straight-line) programs. This keeps every existing T1 proof untouched — they're all straight-line and continue to use exec_program; only branching code uses the new model.
3. Align Compilation.v division clauses (I32DivS/U, I32RemS/U) to emit the real CMP/BNE/UDF/SDIV trap-guard sequence (not the bare SDIV they model today).
4. Re-prove the 4 division theorems as T1 against exec_indexed, case-splitting on the divisor:
   • divisor ≠ 0 → branch taken → UDF skipped → SDIV computes the quotient (the existing I32.divs v1 v2 = Some result hypothesis);
   • divisor = 0 → branch not taken → UDF traps (exec_indexed = None), matching the WASM trap semantics.

Outcome

• Closes the 4 i32-division admits as proofs about the shipped trap-guarded code, not a bare-SDIV model. Tree-wide admits 9 → 5.
• Establishes the trap-verification capability (the div-by-zero trap is now proven), which generalizes to memory-bounds and overflow traps later.
• First concrete dent in proof: Rocq compile_wasm_to_arm diverges from Rust instruction selector #73 (item 1).

Falsification statement

v0.12 is wrong if: (a) any of i32_divs/divu/rems/remu_correct is not Qed against the trap-guarded Compilation.v clause; (b) the division clause in Compilation.v does not match the CMP/BNE/UDF/SDIV shape instruction_selector.rs emits (cross-checked); (c) exec_indexed and exec_program disagree on any branch-free program (the bridge lemma must be Qed); (d) a new Axiom is introduced; or (e) bazel test //coq:verify_proofs goes red on a clean v0.12 checkout.

Why non-invasive matters

Rewriting exec_program in place would break all ~40 existing T1 proofs (they pattern-match the sequential fixpoint). The add-exec_indexed-plus-bridge-lemma design isolates the change to division, keeps the green proofs green, and is itself a verified refinement (the bridge lemma proves the two models agree where they overlap).

Partially addresses #73 (item 1). Items 2–4 follow in v0.13.

[avrabe]

Status (issue-hygiene pass): the v0.12 arc is mid-flight. Done: the indexed-PC execution model (exec_indexed + BCondOffset/UDF semantics) and the Compilation.v division clauses aligned with the real trap-guard codegen. In progress: re-proving the 4 division theorems as T1 against exec_indexed. Remaining: the branch-free bridge lemma (exec_indexed ≡ exec_program) + clean-room verify + ship v0.12. v0.12's scope also gained the tool-qualification roots (VCR-TQ-001/002, #284) — the proofs are pillar 1 of that argument. #73 closes when this arc lands.

[avrabe]

Cross-repo note from ordeal — offering a shared trap-semantics library, and checking whether synth wants it.

loom traced its trap-elimination miscompiles to one root cause: the verifier proves value equivalence over a model in which operations are total, so traps don't exist in the model and "drop the trapping op" looks value-equal. synth's shipped cluster looks like the same class from here — #633 (i64 div_s overflow silently wrong), #666 (rem_s spurious trap), #709 (trunc_f32 saturates instead of trapping), #665 (unreachable→no-op), #642 (call_indirect no bounds/type check). The per-op guard approach is whack-a-mole; the systematic fix is to verify trap-equivalence, not value-equivalence.

ordeal#59 builds this as a shared, thin QF_BV library (targeting ordeal v0.9.0, no new solver theory — every trap condition is already in the fragment):

• trap_condition(op) for div_s/div_u/rem_s/rem_u (zero + signed-overflow) and load/store (OOB given a mem_bound);
• a (value, may_trap) wrapper + a VC helper: (orig.trap ⇔ opt.trap) ∧ (¬orig.trap ⇒ orig.value == opt.value).

loom is the first consumer (loom#279). The question for synth: does synth-verify's translation validator want to consume the same library and make trap-preservation a mandatory gate, so value-only equivalence can't pass a lowering that drops a WASM trap? The WASM↔ARM angle makes this sharper than loom's: ARM SDIV/UDIV do not trap on divide-by-zero (they return 0), so a value-only VC structurally cannot catch a div_s(x,0) lowering that omits the guard — exactly the shape of #633/#666. Memory faults (OOB load/store) are the same story.

If that's useful, synth becomes the second adopter and the library's mem_bound/signature needs get shaped by both consumers at once. If synth already models this end-to-end and gates on it, tell me and I'll scope ordeal#59 to loom's needs only. No action needed on your side yet — just want to know if the shared piece is wanted before it hardens.

Refs: ordeal#59, loom#279, loom#273/#274/#276/#278 (the loom cluster).

[avrabe]

Yes — synth wants the shared trap-semantics library; replied on ordeal#59 with our requirements. This is the systematic closure of the trap-elimination cluster this arc (#73/#166) has been chasing op-by-op.

Confirmed from the code: synth-verify's translation_validator proves value-equivalence over total ops; trap reasoning lives only in fact_spec.rs (the #494/#633 div-guard elision obligation), not as a gate on the general lowering path. So the default VC can't catch a dropped WASM trap — ordeal's diagnosis is exact.

The WASM→ARM angle makes it mandatory, not just nice: ARM SDIV/UDIV return 0 on ÷0, and float→int VCVT saturates — the ARM model is more total than WASM, so a value-only VC structurally cannot see a lowering that omits our UDF guard (#633/#666 div, #709 trunc_f32). We've been closing these one at a time with a hand-written guard + a unicorn differential each (#709 and #275 landed in v0.40.0, #665/#666/#642 earlier); trap-equivalence as a mandatory VC ends the whack-a-mole.

Filed synth-side as VCR-VER-002 (consume ordeal's trap_condition library → mandatory trap-preservation gate in translation_validator), gated on ordeal#59 landing in ordeal v0.9.0. synth requirements added to ordeal#59: float-trunc trap conditions, unreachable, call_indirect bounds+type, and a caller-supplied symbolic mem_bound (our native-pointer linmem extent, which interacts with the #383/#678 shadow-stack shrink). Thanks for looping us in before it hardened — second adopter shapes the mem_bound/trunc signatures alongside loom.