verify(vcr): VCR-VER-001 program gate DEMONSTRATED — patch-accretion reverses (#242)

CLAUDE.md

@@ -120,8 +120,13 @@ frozen and oracle-gated every step:
 - **Track C (validation):** the differential oracles are CI-gated jobs
   (cmp-select, RV32 shift-fold/const-addr-fold, callee-saved, spill-frame,
   symtab-based frozen-fixture differentials).
-- **Gate `VCR-VER-001`:** a previously load-bearing greedy-fix becomes
-  revertable, full differential bit-identical, cycles equal-or-better.
+- **Gate `VCR-VER-001`:** DEMONSTRATED (implemented, evidence in
+  `scripts/repro/vcr_ver_001_gate.md`) — the v0.11.20 reciprocal-mult
+  cost-gate was deleted outright (PR #322, differential bit-identical); the
+  #496 exhaustion decline is revertable behind `SYNTH_SPILL_ON_EXHAUST`
+  (red case green, anchors byte-identical, declines 14→8) with the flip
+  held on a measured i32-shape cycle regression (missing capability:
+  post-exhaustion code quality on the optimized path).
 
 Shipped default-on levers (v0.13–v0.30, each evidence-gated with a CI-pinned
 opt-out): cmp→select fusion (ARM+RV32), i32 local promotion, immediate-shift

README.md

@@ -260,7 +260,7 @@ The one-sentence version: moving synth's correctness from *"we patched every bug
 | | `SYNTH_SPILL_ON_EXHAUST` | Replace the register-exhaustion decline with allocation-time Belady spilling (#580) — the last piece of the exhaustion hard-fail | built, flag-off; default-on held for silicon cycle numbers |
 | **B — authoritative semantics** | `VCR-ISA-001` | Re-base ARM/RISC-V semantics on Sail-generated Rocq (the official ISA spec) | proposed |
 | | `VCR-WASM-001` | Anchor WASM source semantics on WasmCert-Coq | proposed |
-| **Gate** | `VCR-VER-001` | Success = a previously load-bearing greedy-fix becomes *revertable*, with the full differential bit-identical and cycles equal-or-better | proposed |
+| **Gate** | `VCR-VER-001` | Success = a previously load-bearing greedy-fix becomes *revertable*, with the full differential bit-identical and cycles equal-or-better | **demonstrated** (implemented; [evidence](scripts/repro/vcr_ver_001_gate.md)): the v0.11.20 reciprocal-mult cost-gate deleted outright (PR #322, bit-identical); the #496 exhaustion decline revertable behind `SYNTH_SPILL_ON_EXHAUST` — red case green, anchors byte-identical, declines 14→8; flip held on a measured i32-shape cycle regression |
 
 Honest open items: the RV32 local-promotion flip is held on a failed no-grow gate (#601); f32/f64 remain loud-reject (#369); SIMD/Helium is untested on hardware.
 

artifacts/verified-codegen-roadmap.yaml

@@ -919,7 +919,32 @@ artifacts:
       form with the full differential staying bit-identical and cycles
       equal-or-better — the exact condition the audit checks each cycle. Success
       is measured by those reversions becoming possible, not by new patches.
-    status: proposed
+
+      GATE DEMONSTRATED (2026-07-08, evidence: scripts/repro/vcr_ver_001_gate.md).
+      TWO reversals, one complete and one revertable-behind-flag:
+      (1) the v0.11.20 reciprocal-mult COST-GATE — load-bearing when added
+      (v0.11.19 hard-failed control_step's 4x const div_u) — was DELETED
+      outright in PR #322 once the #320 spill retry covered its case: full
+      differential bit-identical (+-0 B, the fallback was dead on the whole
+      frozen suite), cycles trivially equal, no new cost-gate since — the
+      pass-criteria met literally.
+      (2) the #496 exhaustion hard-DECLINE is revertable behind
+      SYNTH_SPILL_ON_EXHAUST (#580, default off = fix stays): flag-on the
+      original red case stays green (r12_spill_496 differential PASS incl.
+      0x00210A55/0x07FDF307; all five pressure differentials PASS on the
+      reversal bytes), frozen pinned goldens 10/10 in BOTH flag states, the
+      three result anchors' default-path bytes byte-identical flag-on (locked
+      by vcr_ver_001_gate_242.rs), declines 14->8 across the corpus. HONEST
+      HOLD: the weighted cycle proxy REGRESSES on i32 shapes (+30.4%
+      spill_on_exhaust_242, +32.4% spill_rung_581, +8.0% high_pressure_i32,
+      +120% signed_div_const whose 34-B direct lowering becomes a 76-B
+      optimized-path compile; i64 shapes improve -5.5%/-1.4%) — the decline
+      remains load-bearing FOR CYCLES, not correctness. Missing capability
+      (VCR-RA follow-on): post-exhaustion code quality on the optimized path
+      (allocation-time spill placement/coalescing; frame-slot-DCE/stack-fwd
+      do not reach allocation-time slots). The default-on flip stays a
+      separate later PR gated on closing that gap + gale G474RE cycles (#580).
+    status: implemented
     tags: [verification, audit, regression, frozen-fixtures]
     links:
       - type: verifies

crates/synth-cli/tests/vcr_ver_001_gate_242.rs

@@ -0,0 +1,101 @@
+//! VCR-VER-001 (#242) — program-gate lock: the greedy-fix reversal flag must
+//! not disturb the frozen result anchors.
+//!
+//! The gate's second demonstration (see `scripts/repro/vcr_ver_001_gate.md`)
+//! reverts the #496 register-exhaustion hard-decline behind
+//! `SYNTH_SPILL_ON_EXHAUST` (#580): flag-on, a function whose optimized-path
+//! allocation exhausts the R4-R8 scratch/pair pool spills at allocation time
+//! (Belady) instead of declining to the direct selector. The reversal's blast
+//! radius must be exactly the formerly-declining functions:
+//!
+//! * The three frozen result-anchor fixtures (`control_step` `0x00210A55`,
+//!   `flight_seam`/`flight_seam_flat` `0x07FDF307`) decline for reasons the
+//!   flag does NOT address (rung=spill via a non-exhaustion optimized-path
+//!   Err; rung=base), so their DEFAULT-path bytes must be BIT-IDENTICAL with
+//!   the flag on — asserted here. If this ever fails, the reversal grew a new
+//!   blast radius and the gate evidence must be re-derived (differentials
+//!   re-run on the new bytes) before any flip.
+//! * `signed_div_const` is deliberately NOT pinned: it IS flag-sensitive
+//!   (its rung=base decline is recovered into an optimized-path compile at
+//!   34→76 B, execution-verified) — the measured reason the default-on flip
+//!   is held. Pinning its sensitivity would be a speculative tripwire; the
+//!   sensitivity is documented in the gate note instead.
+//!
+//! Execution equivalence of the changed (unpinned) pressure-fixture bytes is
+//! gated by `scripts/repro/spill_on_exhaust_242_differential.py`,
+//! `i64_pair_exhaust_587_differential.py`, `i64_spill_pool_587_differential.py`,
+//! `spill_rung_581_differential.py` and `r12_spill_496_differential.py`.
+
+use std::process::Command;
+
+use object::{Object, ObjectSection};
+
+fn synth() -> &'static str {
+    env!("CARGO_BIN_EXE_synth")
+}
+
+fn fixture(name: &str) -> std::path::PathBuf {
+    std::path::Path::new(env!("CARGO_MANIFEST_DIR"))
+        .join("../..")
+        .join("scripts/repro")
+        .join(name)
+}
+
+/// Compile `wasm` on the DEFAULT path (no `--relocatable` — the optimized
+/// path is eligible, the one the #496 decline and its reversal act on) and
+/// return the `.text` bytes.
+fn default_path_text(wasm: &str, spill_on_exhaust: bool) -> Vec<u8> {
+    let elf = format!(
+        "/tmp/vcr_ver_001_{}_{wasm}.elf",
+        if spill_on_exhaust { "on" } else { "off" }
+    );
+    let mut cmd = Command::new(synth());
+    if spill_on_exhaust {
+        cmd.env("SYNTH_SPILL_ON_EXHAUST", "1");
+    } else {
+        cmd.env_remove("SYNTH_SPILL_ON_EXHAUST");
+    }
+    let out = cmd
+        .args([
+            "compile",
+            fixture(wasm).to_str().unwrap(),
+            "-o",
+            &elf,
+            "--target",
+            "cortex-m4",
+            "--all-exports",
+        ])
+        .output()
+        .expect("run synth");
+    assert!(
+        out.status.success(),
+        "synth compile failed for {wasm}: {}",
+        String::from_utf8_lossy(&out.stderr)
+    );
+    let bin = std::fs::read(&elf).expect("read ELF");
+    let obj = object::File::parse(&*bin).expect("parse ELF");
+    obj.section_by_name(".text")
+        .expect(".text")
+        .data()
+        .expect("section data")
+        .to_vec()
+}
+
+#[test]
+fn vcr_ver_001_reversal_flag_leaves_frozen_anchors_byte_identical() {
+    for wasm in [
+        "control_step.wasm",
+        "flight_seam.wasm",
+        "flight_seam_flat.wasm",
+    ] {
+        let off = default_path_text(wasm, false);
+        let on = default_path_text(wasm, true);
+        assert_eq!(
+            off, on,
+            "{wasm}: SYNTH_SPILL_ON_EXHAUST changed a frozen result anchor's \
+             default-path bytes — the VCR-VER-001 reversal's blast radius grew \
+             beyond the formerly-declining functions; re-derive the gate \
+             evidence (scripts/repro/vcr_ver_001_gate.md) before any flip"
+        );
+    }
+}

scripts/repro/vcr_ver_001_gate.md

@@ -0,0 +1,128 @@
+# VCR-VER-001 — the program gate, attempted and measured
+
+**Epic:** #242 · **Artifact:** `artifacts/verified-codegen-roadmap.yaml` `VCR-VER-001`
+· **Status:** GATE DEMONSTRATED (status → `implemented`); the #496 flip stays HELD
+· **Derived:** 2026-07-08 at `f8c6826`, frozen anchors 10/10 green at baseline.
+
+The gate is the North-Star program's falsification test: *a previously
+load-bearing greedy fix becomes revertable — patch-accretion reverses.*
+Pass-criteria (roadmap): at least one previously load-bearing greedy-fix removed
+with the full differential bit-identical and cycles equal-or-better; no new
+cost-gate introduced.
+
+## Candidate survey
+
+| # | Greedy fix | What it protected | Verdict |
+|---|-----------|-------------------|---------|
+| 1 | v0.11.20 reciprocal-mult **cost-gate** (UDIV fallback when UMULL scratch could not be allocated) | v0.11.19 hard-fail: gale's `control_step` 4× const `div_u` exhausted the R0-R8 pool → compile error | **REVERSED — deleted outright (PR #322)**; meets the pass-criteria literally (below) |
+| 2 | #496 **decline-on-exhaustion** (optimized path hard-declines to the direct selector when its R4-R8 scratch / i64-pair pool exhausts) | #496 silent miscompile: the pre-fix R12/IP last-resort borrow collided with the encoder's indexed-load scratch (#212 class) — `control_step` execution-faulted, `flight_seam_flat` computed wrong values | **REVERTABLE, flag-off** via `SYNTH_SPILL_ON_EXHAUST` (#580); correctness criteria all hold; **cycles criterion FAILS on i32 shapes** → flip stays held (missing capability named below) |
+| 3 | `// #NNN` guards in `optimizer_bridge.rs` (#377/#382/#483/#543 …) | Encoding-range, bounds-guard and volatile-window soundness — not allocation greediness | Not candidates: these are correctness features with their own oracles, not pressure heuristics the allocator subsumes |
+
+## Demonstration 1 — the cost-gate deletion (PR #322) meets the pass-criteria
+
+The v0.11.20 UDIV fallback was load-bearing when added (without it v0.11.19
+failed to compile `control_step`). Two things made it removable, both verified
+in #322 and re-verified today:
+
+1. **The case it guarded is covered by Track-A machinery**: the #320
+   spill-on-exhaustion retry recovers UMULL-scratch exhaustion
+   (`alloc_temp_or_spill` in `instruction_selector.rs`); the original red case
+   is pinned green by `test_209_multi_const_div_does_not_exhaust`.
+2. **Full differential bit-identical**: the fallback was dead on the entire
+   frozen suite — deletion was byte-identical (±0 B), hence cycles trivially
+   equal. No new cost-gate has been introduced since (the reciprocal-multiply
+   path at `instruction_selector.rs:~7412` has no profitability guard).
+
+That is the roadmap's pass-criteria, satisfied exactly: removed (not
+flag-gated), differential bit-identical, cycles equal, no new cost-gate.
+
+## Demonstration 2 — the #496 decline is revertable; the flip is held on measured cycles
+
+Reversal flag: `SYNTH_SPILL_ON_EXHAUST` (#580; default **off** = the greedy fix
+stays). Flag-on, exhaustion routes through the allocation-time Belady spill
+(pair-aware since #587) instead of declining — strictly more capable: fewer
+functions leave the optimized path, and the exhaustion class that #496 turned
+from silent-miscompile into loud-decline becomes "spill and continue".
+
+All numbers derived on `f8c6826`, default path (`--target cortex-m4
+--all-exports`, no `--relocatable`), synth debug build.
+
+### (a) The original red case stays green with the reversal active
+
+* `r12_spill_496_differential.py` with `SYNTH_SPILL_ON_EXHAUST=1`: **PASS** —
+  the two original silicon victims execute bit-for-bit like wasmtime,
+  including the frozen result anchors `control_step(3000,50,40,0) =
+  0x00210A55` and `flight_algo = 0x07FDF307` (13 + 1 vectors).
+* `spill_on_exhaust_242_differential.py` on the flag-on bytes: **PASS** (8/8).
+* `i64_pair_exhaust_587_differential.py` on the flag-on bytes: **PASS** (8/8).
+* `i64_spill_pool_587_differential.py`, `spill_rung_581_differential.py`
+  flag-on: **PASS**.
+* `signed_div_const` + `high_pressure_i32` flag-on bytes execution-verified
+  vs wasmtime under unicorn (6 and 8 vectors): **OK**.
+
+### (b) Differential suite + per-function bytes/declines
+
+Frozen pinned goldens (`frozen_codegen_bytes.rs`, `--relocatable`): the flag
+acts on the optimized path only — **10/10 green in both flag states**.
+Default-path anchor fixtures are byte-identical flag-on (locked by the new
+`vcr_ver_001_gate_242.rs`). Per-function measurement over the pressure corpus:
+
+| fixture (default path) | declines off→on | .text B off→on | weighted cycle proxy* off→on |
+|---|---|---|---|
+| `control_step.wasm` | 1 → 1 (rung=spill, non-exhaustion Err) | 474 = 474 | identical bytes |
+| `flight_seam.wasm` | 3 → 3 (rung=base) | 886 = 886 | identical bytes |
+| `flight_seam_flat.wasm` | 3 → 3 (rung=base) | 1026 = 1026 | identical bytes |
+| `spill_on_exhaust_242.wat` | 1 → **0** | 264 → 296 | 368 → 480 (**+30.4 %**) |
+| `i64_pair_exhaust_587.wat` | 1 → **0** | 348 = 348 | 584 → 552 (**−5.5 %**) |
+| `i64_spill_pool_587.wat` | 1 → **0** | 912 → 930 | 2208 → 2176 (**−1.4 %**) |
+| `spill_rung_581.wat` | 1 → **0** | 228 → 254 | 272 → 360 (**+32.4 %**) |
+| `high_pressure_i32.wat` | 1 → **0** | 274 → 272 | 400 → 432 (**+8.0 %**) |
+| `signed_div_const.wasm` | 1 → **0** | 194 → 236 (fn 34 → 76) | 90 → 198 (**+120 %**) |
+| `high_pressure_i64.wat` | 1 → 1 (rung=param-backing, out of scope) | 350 = 350 | identical bytes |
+
+\* dynamic instructions + data-memory accesses under unicorn (first-order M4:
+LDR/STR ≈ 2 cyc), summed over the differential vectors; every run
+execution-matched wasmtime.
+
+Total declines across the corpus: **14 → 8**. Everything pinned is
+bit-identical; every changed function is execution-proven.
+
+### (c) Frozen anchors + refreeze ritual
+
+Flag OFF (the default this state ships in): frozen byte gate **10/10**, no code
+change — trivially bit-identical. Flag ON changes bytes **only** on unpinned
+pressure fixtures; per the refreeze ritual the result differentials were re-run
+on the new bytes (all PASS, above) and the goldens were **not** re-pinned — the
+flip is a separate later PR.
+
+### The verdict on criterion "cycles equal-or-better" — and the missing capability
+
+The reversal is **correctness-complete but performance-regressive on i32
+shapes**: +8 % to +120 % on the weighted proxy, improving only the i64-pair
+shapes. The #496 decline therefore remains load-bearing *for cycles, not for
+correctness*. The named missing capability (`VCR-RA` follow-on):
+
+> **Post-exhaustion code quality on the optimized path.** The allocation-time
+> Belady spill emits more stack traffic than the direct selector's
+> operand-stack spill on i32-dense shapes (`spill_on_exhaust_242`: 16 → 22
+> memory accesses per call), and an optimized-path function that only compiles
+> *because* of the spill lever can be worse than the direct lowering of the
+> same function (`signed_div_const`: 34 → 76 B, 90 → 198 weighted — the
+> optimized path's const-div lowering under pressure loses to the direct
+> selector's strength-reduced form). Until spill placement/coalescing (or
+> running the frame-slot-DCE/stack-fwd family over allocation-time slots)
+> closes that gap — measured on gale's G474RE per the #580 hold — the flip
+> would trade declines for cycles.
+
+## Reproduce
+
+```sh
+cargo test -p synth-cli --test frozen_codegen_bytes --test vcr_ver_001_gate_242 \
+    --test spill_on_exhaust_242 --test i64_pair_exhaust_587
+# execution evidence (needs wasmtime + unicorn + pyelftools):
+SYNTH=target/debug/synth SYNTH_SPILL_ON_EXHAUST=1 \
+    python scripts/repro/r12_spill_496_differential.py
+SYNTH_SPILL_ON_EXHAUST=1 target/debug/synth compile \
+    scripts/repro/spill_on_exhaust_242.wat -o /tmp/soe.elf --target cortex-m4
+python scripts/repro/spill_on_exhaust_242_differential.py /tmp/soe.elf
+```