Epic: verified-codegen infrastructure (VCR-*) — replace the patch-accreting selector + allocator

[avrabe]

Tracking epic for the verified-codegen roadmap filed as rivet requirements in artifacts/verified-codegen-roadmap.yaml (PR #241).

Thesis

The recurring greedy-fixes — reciprocal-mult cost-gate (v0.11.20), register-exhaustion hard-fail (instruction_selector.rs:330/356/577/4667), "selector missed an op" (#223/#226/#232) — are symptoms of the single-pass hand-written selector + allocator. We build the structural cure incrementally, in parallel with the gale per-issue cadence. Behavior frozen at every step (fixtures bit-identical, oracle-gated).

Work items (rivet IDs ↔ future PRs)

Track A — codegen core (sequential):

• VCR-RA-001 — SSA allocator with spilling (removes the hard-fail that forces cost-gates). Do first.
• VCR-SEL-001 — Rocq-discharged verified selector DSL. Kill-criterion: ≥70% of a pilot op-class auto-discharged by existing tactics.

Track B — authoritative semantics (parallel):

• VCR-ISA-001 — Sail-generated Rocq ARM/RISC-V semantics.
• VCR-WASM-001 — WasmCert-Coq source semantics.

Track C — validation (start now):

• VCR-ORACLE-001 — coverage-guided, theorem-linked differential oracle.

Gate:

• VCR-VER-001 — the cleanup audit confirms a previously load-bearing greedy-fix becomes revert-able, fixtures bit-identical, cycles equal-or-better.

Suggested first step

VCR-RA-001 (allocator) — it unblocks reverting the cost-gates and is the prerequisite for VCR-SEL-001 (a verified rule that can't be allocated isn't yet correct end-to-end). Track C (VCR-ORACLE-001) can begin in parallel immediately.

Related: #209 (perf lever), #181 (native-pointer ABI / #237), #166/#73 (v0.12 control-flow proofs).

[avrabe]

VCR-RA-001 — step 1 landed as PR #243. Register def/use + liveness foundation (crates/synth-synthesis/src/liveness.rs): reg_effect(&ArmOp) (precise scalar def/use) + local_dead_defs() (sound dead-store detection, the generic form of #221). Pure analysis, not wired into codegen → fixtures bit-identical (control_step ORACLE PASS), 269 lib tests + 7 new. Next on VCR-RA-001: CFG-aware liveness → interference graph over virtual registers (pre-allocation pressure) → spill-under-pressure (removes the exhaustion hard-fail that forces the cost-gates).

[avrabe]

VCR-RA-001 — step 2 (PR #245): redundant-constant detection (const-CSE analysis). redundant_const_defs() — the forward dual of local_dead_defs; flags constant materializations whose value is already resident. Reproduces gale's measured flat_flight waste (#209): the 6× #0x7e clamp → 5 redundant. Pure detection, not wired in; 274 lib tests, control_step ORACLE PASS. The two halves of gale's #1 lever are now both detectable (dead-store + redundant-const); the transform (keep clamp bounds resident) migrates in with the allocator.