From dbe2d7c26955edd13f63d6e1eb48b229d181c139 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 8 Jul 2026 19:16:58 +0200 Subject: [PATCH] =?UTF-8?q?verify(vcr):=20VCR-VER-001=20program=20gate=20D?= =?UTF-8?q?EMONSTRATED=20=E2=80=94=20patch-accretion=20reverses=20(#242)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The North-Star program's falsification test, attempted and measured (evidence: scripts/repro/vcr_ver_001_gate.md): 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, cycles trivially equal, no new cost-gate since. The roadmap's pass-criteria met literally; the artifact goes proposed -> implemented. 2. The #496 register-exhaustion hard-decline is REVERTABLE behind SYNTH_SPILL_ON_EXHAUST (#580, default off = fix stays): - red case green: r12_spill_496 differential PASS flag-on (incl. the 0x00210A55 / 0x07FDF307 silicon anchors); 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 are byte-identical flag-on (new lock: vcr_ver_001_gate_242.rs); declines 14 -> 8 across the corpus - HONEST HOLD: 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 34->76 B; i64 shapes improve -5.5%/-1.4%) — the decline remains load-bearing FOR CYCLES, not correctness. Missing capability named: post-exhaustion code quality on the optimized path (allocation-time spill placement/coalescing). The default-on flip stays a separate later PR (#580 silicon hold). Flag-off this change is docs + roadmap + one additive test: no codegen bytes move; frozen gate green; goldens NOT re-pinned. Co-Authored-By: Claude Fable 5 --- CLAUDE.md | 9 +- README.md | 2 +- artifacts/verified-codegen-roadmap.yaml | 27 +++- .../synth-cli/tests/vcr_ver_001_gate_242.rs | 101 ++++++++++++++ scripts/repro/vcr_ver_001_gate.md | 128 ++++++++++++++++++ 5 files changed, 263 insertions(+), 4 deletions(-) create mode 100644 crates/synth-cli/tests/vcr_ver_001_gate_242.rs create mode 100644 scripts/repro/vcr_ver_001_gate.md diff --git a/CLAUDE.md b/CLAUDE.md index 70e7ba1b..6ec80b49 100644 --- a/CLAUDE.md +++ b/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 diff --git a/README.md b/README.md index 185bd2e1..89bd8add 100644 --- a/README.md +++ b/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. diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 9988d55a..39f6745a 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/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 diff --git a/crates/synth-cli/tests/vcr_ver_001_gate_242.rs b/crates/synth-cli/tests/vcr_ver_001_gate_242.rs new file mode 100644 index 00000000..82d17448 --- /dev/null +++ b/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 { + 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" + ); + } +} diff --git a/scripts/repro/vcr_ver_001_gate.md b/scripts/repro/vcr_ver_001_gate.md new file mode 100644 index 00000000..07d19660 --- /dev/null +++ b/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 +```