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.