diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1cc665e9..d253412e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -688,6 +688,23 @@ jobs: run: SYNTH=./target/debug/synth python scripts/repro/mem761_linmem_r9_overlap_differential.py - name: Run #761 linmem<->globals overlap oracle (cortex-m4, low layout) run: EXTRA_SYNTH_FLAGS="--stack-layout low" SYNTH=./target/debug/synth python scripts/repro/mem761_linmem_r9_overlap_differential.py + # VCR-DEC-001 (epic #242, the North Star's first foothold): the + # SYNTH_GRAPH_ALLOC whole-function graph-colouring allocator SPIKE. Gates + # three properties on the ARM corpus: (1) flag-OFF ≡ the frozen goldens + # (the GOLDEN trick — the spike is byte-invisible when off), (2) flag-ON + # APPLIES on ≥2 fixtures and the UNCONDITIONAL VCR-RA-003 validator returns + # Consistent on every applied function (observed via SYNTH_RA003_VERBOSE — + # the acceptance oracle validating the new allocator's REAL output), and + # (3) flag-ON ≡ flag-OFF corpus-wide (a DESIGNED property: on a + # straight-line function graph_alloc and the shipping reallocate_function + # share pins + chaitin_core + single-segment scope, so byte-identity is by + # construction; execution correctness follows transitively via the frozen + # wasmtime differentials above). The red-first teeth are the unit probe + # graph_alloc_bad_rename_rejected_by_segment_validator (validate_segment_ + # rewrite rejects a value-flow-breaking merge-rename). Byte-only compare — + # needs pyelftools ONLY (no unicorn/wasmtime). + - name: Run VCR-DEC-001 graph-alloc spike differential (#242, thumb2) + run: python scripts/repro/vcr_dec_001_graph_alloc_differential.py ./target/debug/synth fact-spec-oracle: name: fact-spec elision oracle (#494 phases 2 + 2b + 3+ + bounds) diff --git a/crates/synth-backend/src/arm_backend.rs b/crates/synth-backend/src/arm_backend.rs index 3bcb4871..1ede0c7d 100644 --- a/crates/synth-backend/src/arm_backend.rs +++ b/crates/synth-backend/src/arm_backend.rs @@ -929,17 +929,54 @@ fn compile_wasm_to_arm( Reg::R7, Reg::R8, ]; + // VCR-DEC-001 (epic #242, the North Star's first foothold): the + // SYNTH_GRAPH_ALLOC graph-colouring allocator SPIKE. When enabled it + // replaces STEP 1 of the re-allocation (the segment-based + // `reallocate_function`) with a whole-function Chaitin/Briggs colouring + // (`graph_alloc::reallocate`) built against the SAME acceptance oracle + // (`validate_segment_rewrite` trace-equality); the later dead-frame / + // callee-saved-prologue / shrink passes still run on its output, so a + // value it homes in R4-R8 still gets its callee-saved push (the + // invariant the unconditional VCR-RA-003 validator guards). It is + // BOUNDED to whole straight-line functions and DECLINES (returns None) + // to the shipping `reallocate_function` on any control flow, spill, or + // unmodeled op — never a hard-fail. Flag-OFF (`SYNTH_GRAPH_ALLOC` unset) + // never enters this branch, so the shipping bytes are byte-identical + // (the GOLDEN trick — frozen fixtures unchanged). NO default flip: the + // spike ships flag-off; the flip is a later, evidence-gated step. + // // VCR-VER-001 (#242): on a function the spill-on-exhaustion machinery // shaped, the terminal segment gets relaxed live-out pinning (only // R0/R1 are observable past `bx lr` at this pre-prologue position) so // the colourer can lower R4-R8-homed tails into caller-saved R0-R3 — // shrinking the `push {r4-r8,lr}` the #580 exhaustion shapes pay for. // `post_exhaust == false` selects the shipping pass bit for bit. - let (out, stats) = synth_synthesis::liveness::reallocate_function_post_exhaust( - &arm_instrs, - &POOL, - post_exhaust, - ); + let (out, stats) = if synth_synthesis::graph_alloc::enabled() { + match synth_synthesis::graph_alloc::reallocate(&arm_instrs, &POOL) { + Some(new) => { + if std::env::var("SYNTH_GRAPH_ALLOC_STATS").is_ok() { + eprintln!("[graph-alloc] whole-function colouring APPLIED (validated)"); + } + (new, synth_synthesis::liveness::ReallocStats::default()) + } + None => { + if std::env::var("SYNTH_GRAPH_ALLOC_STATS").is_ok() { + eprintln!("[graph-alloc] DECLINED → shipping reallocate_function"); + } + synth_synthesis::liveness::reallocate_function_post_exhaust( + &arm_instrs, + &POOL, + post_exhaust, + ) + } + } + } else { + synth_synthesis::liveness::reallocate_function_post_exhaust( + &arm_instrs, + &POOL, + post_exhaust, + ) + }; if std::env::var("SYNTH_REALLOC_STATS").is_ok() { eprintln!( "[range-realloc] {} segments: {} reallocated, {} declined ({} validator-rejected), {} need spill (step 4)", @@ -1408,7 +1445,11 @@ fn compile_wasm_to_arm( ); } } - synth_synthesis::liveness::RaFinalVerdict::Consistent => {} + synth_synthesis::liveness::RaFinalVerdict::Consistent => { + if std::env::var_os("SYNTH_RA003_VERBOSE").is_some() { + eprintln!("VCR-RA-003: Consistent"); + } + } } // Encode to binary — use Thumb-2 for Cortex-M targets diff --git a/crates/synth-synthesis/src/graph_alloc.rs b/crates/synth-synthesis/src/graph_alloc.rs new file mode 100644 index 00000000..c56c6f19 --- /dev/null +++ b/crates/synth-synthesis/src/graph_alloc.rs @@ -0,0 +1,362 @@ +//! VCR-DEC-001 — whole-function graph-colouring register allocator SPIKE. +//! +//! **The North Star, first foothold.** synth's shipping register allocator is a +//! greedy single-pass component (`optimizer_bridge::ir_to_arm_impl`) plus the +//! verified segment-based re-allocation pass (`liveness::reallocate_function`). +//! The whole VCR program (epic #242) exists to REPLACE the greedy allocator with +//! a from-construction-correct one. This module is the bounded first increment of +//! that replacement: a Chaitin/Briggs graph-colouring allocator built AGAINST the +//! acceptance oracles the verified path already runs, so any code it emits is +//! provably allocation-sound. +//! +//! **Flag-gated, decline-to-shipping.** Everything here fires only under +//! `SYNTH_GRAPH_ALLOC=1`. With the flag unset the shipping path is byte-for-byte +//! untouched (the caller never calls into this module) — the GOLDEN trick: the +//! frozen fixtures stay bit-identical. When the flag is set and this allocator +//! cannot handle a function within its bounded scope, it returns `None` and the +//! caller falls back to the shipping `reallocate_function` — never a hard-fail. +//! +//! **Bounded scope (increment 1).** WHOLE straight-line functions only: a +//! function whose entire body is one straight-line segment (no branches, no +//! calls, no i64-pair / FP ops — anything [`crate::liveness::straight_line_value_ranges`] +//! or [`crate::liveness::reg_effect`] declines). Such a function is coloured as a +//! SINGLE whole-function interference graph over the R0-R8 pool, with segment +//! inputs and live-outs pinned to their incoming/outgoing registers and reserved +//! registers (R9-R12) identity-assigned. On ANY control flow, spill, or unmodeled +//! op, it declines to the shipping path. +//! +//! Increment 2 (NAMED, NOT in this spike): whole-function *webs* built from +//! [`crate::liveness::cfg_liveness`] — colouring value ranges ACROSS control-flow +//! joins, where "the allocator and validator share the dataflow" fully lands. +//! That needs SSA-style web construction across joins that does not exist yet; +//! it is honestly beyond a bounded first slice. +//! +//! **The oracle IS the point (red-first).** Every rewrite this module produces is +//! proven semantics-preserving by [`crate::liveness::validate_segment_rewrite`] +//! (the Rideau/Leroy pairwise trace-equality validator — the SAME acceptance gate +//! `reallocate_function` uses); a rewrite the validator rejects is dropped and the +//! function declines. Downstream, the unconditional VCR-RA-003 +//! [`crate::liveness::validate_final_allocation`] re-checks the final stream, and +//! the wasmtime execution differential is the runtime backstop. + +use crate::instruction_selector::ArmInstruction; +use crate::liveness::{ + apply_range_coloring, color_ranges, is_straight_line, range_interference, reg_effect, + straight_line_value_ranges, validate_segment_rewrite, +}; +use crate::rules::Reg; +use std::collections::{BTreeMap, BTreeSet}; + +/// Is `SYNTH_GRAPH_ALLOC` enabled? Any value other than `0` turns the spike on; +/// unset or `0` keeps the shipping path (byte-identical). +pub fn enabled() -> bool { + std::env::var("SYNTH_GRAPH_ALLOC").is_ok_and(|v| v != "0") +} + +/// Whole-function graph-colouring re-allocation of `instrs` over `pool` +/// (the R0-R8 allocatable set), or `None` to DECLINE (the caller keeps the +/// shipping path). Declines whenever the function is not a single whole-function +/// straight-line segment, the colouring spills, the independent edge re-check +/// fails, or the trace-equality validator rejects the rewrite. A `Some` result is +/// a rewrite PROVEN to preserve the function's dataflow. +/// +/// This is the surgical entry point the flag-gated hook calls in place of +/// `reallocate_function` step 1; the caller's later prologue / dead-frame passes +/// run on the output unchanged (so a value homed in R4-R8 still gets its +/// callee-saved push — the invariant VCR-RA-003 guards). +pub fn reallocate(instrs: &[ArmInstruction], pool: &[Reg]) -> Option> { + // BOUNDED SCOPE: the whole function must be ONE straight-line segment. Any + // control-flow / call / unmodeled op → decline (shipping path segments such + // functions; this spike does not, by design — increment 2 is the whole- + // function webs across joins). + if instrs.is_empty() { + return None; + } + for ins in instrs { + if !is_straight_line(&ins.op) || reg_effect(&ins.op).is_none() { + return None; + } + } + + let ranges = straight_line_value_ranges(instrs)?; + if ranges.is_empty() { + return None; + } + + let pool_index: BTreeMap = pool.iter().enumerate().map(|(i, r)| (*r, i)).collect(); + let adj = range_interference(&ranges); + + // Pins: segment inputs (def == 0) and each register's LAST-opened range + // (the whole-function live-out) keep their original register — the function + // must return its result registers unchanged. Reserved registers (R9-R12, + // SP, LR, PC) are identity-assigned outside the colouring. + let mut last_opened: BTreeMap = BTreeMap::new(); + for r in &ranges { + last_opened.insert(r.reg, r.vreg); // ranges are in creation order + } + let mut pins: BTreeMap = BTreeMap::new(); + let mut assignment: BTreeMap = BTreeMap::new(); + let mut pool_nodes: BTreeSet = BTreeSet::new(); + for r in &ranges { + match pool_index.get(&r.reg) { + None => { + // Reserved register: identity, never coloured. + assignment.insert(r.vreg, r.reg); + } + Some(&idx) => { + pool_nodes.insert(r.vreg); + let exit_pinned = last_opened.get(&r.reg) == Some(&r.vreg); + if r.def == 0 || exit_pinned { + pins.insert(r.vreg, idx); + } + } + } + } + + // Colouring input: pool ranges only (reserved registers cannot collide with + // pool colours, so their edges are irrelevant to the pool colouring). + let mut pool_adj: BTreeMap> = adj + .iter() + .filter(|(n, _)| pool_nodes.contains(n)) + .map(|(n, nbrs)| (*n, nbrs.intersection(&pool_nodes).copied().collect())) + .collect(); + + // #677 soundness: a pool register with NO range in this function is not + // thereby FREE for a rename target — but for a WHOLE-FUNCTION straight-line + // segment there is nothing "outside" it, so an absent pool register is + // genuinely free. We still block absent colours defensively (an + // identity-shaped colouring within the present registers always exists, so + // this never costs a recoloring the original had), matching the shipping + // pass's #677 discipline exactly. + let present: BTreeSet = ranges.iter().map(|r| r.reg).collect(); + let mut next_blocker = ranges.len(); + for (idx, reg) in pool.iter().enumerate() { + if present.contains(reg) { + continue; + } + let blocker = next_blocker; + next_blocker += 1; + pins.insert(blocker, idx); + for nbrs in pool_adj.values_mut() { + nbrs.insert(blocker); + } + pool_adj.insert(blocker, pool_nodes.iter().copied().collect()); + } + + // Spill cost: occurrence count per range (1 per def + 1 per use event), + // replayed with the same vreg numbering `straight_line_value_ranges` uses. + let costs = occurrence_costs(instrs)?; + + let (coloring, spilled) = color_ranges(&pool_adj, pool.len(), &pins, &costs); + if !spilled.is_empty() { + // Spill code insertion is increment 2+ (reuse the Belady machinery). + // For now a function that does not fit the pool declines to the shipping + // path — which HAS spill support. + return None; + } + for (v, c) in &coloring { + assignment.insert(*v, pool[*c]); + } + + // Defense-in-depth: independently of the colourer, re-check every + // interference edge against the final assignment (cf. + // `liveness::verify_allocation`, but keyed on value ranges). + for (n, nbrs) in &adj { + for m in nbrs { + match (assignment.get(n), assignment.get(m)) { + (Some(a), Some(b)) if a != b => {} + _ => return None, + } + } + } + + // Apply the colouring, then PROVE it preserves the function's dataflow with + // the trace-equality validator (whole-function live-outs + entry inputs + // pinned; no exemptions — a whole straight-line function's exit registers are + // all observable). This is the acceptance oracle; a reject → decline (the + // red-first teeth are the unit probe `graph_alloc_bad_rename_rejected_by_\ + // segment_validator` in liveness.rs: it shows validate_segment_rewrite + // rejects a value-flow-breaking merge-rename and accepts the identity — the + // exact Err/Ok this match discharges to decline/accept). + let new = apply_range_coloring(instrs, &assignment)?; + match validate_segment_rewrite(instrs, &new) { + Ok(()) => Some(new), + Err(_) => None, + } +} + +/// Per-range occurrence cost (Chaitin spill metric input): 1 per def + 1 per use, +/// replayed with the SAME vreg numbering as [`straight_line_value_ranges`] so the +/// costs align with the range ids `range_interference` / `color_ranges` use. +/// `None` on an unmodeled op (already excluded by the caller's pre-scan, but kept +/// total). +fn occurrence_costs(instrs: &[ArmInstruction]) -> Option> { + let mut costs: BTreeMap = BTreeMap::new(); + let mut current: BTreeMap = BTreeMap::new(); + let mut next = 0usize; + for ins in instrs { + let e = reg_effect(&ins.op)?; + for u in &e.uses { + let v = *current.entry(*u).or_insert_with(|| { + let v = next; + next += 1; + v + }); + *costs.entry(v).or_insert(0) += 1; + } + for d in &e.defs { + current.insert(*d, next); + *costs.entry(next).or_insert(0) += 1; + next += 1; + } + } + Some(costs) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::rules::{ArmOp, Operand2}; + + fn ins(op: ArmOp) -> ArmInstruction { + ArmInstruction { + op, + source_line: None, + } + } + + const POOL: [Reg; 9] = [ + Reg::R0, + Reg::R1, + Reg::R2, + Reg::R3, + Reg::R4, + Reg::R5, + Reg::R6, + Reg::R7, + Reg::R8, + ]; + + #[test] + fn colours_a_straight_line_function_and_validates() { + // r2 = r0 + r1 ; r0 = r2 + r1 (all straight-line, fits the pool) + let body = vec![ + ins(ArmOp::Add { + rd: Reg::R2, + rn: Reg::R0, + op2: Operand2::Reg(Reg::R1), + }), + ins(ArmOp::Add { + rd: Reg::R0, + rn: Reg::R2, + op2: Operand2::Reg(Reg::R1), + }), + ]; + let out = reallocate(&body, &POOL).expect("straight-line function colours"); + // The rewrite must pass the trace-equality validator (it did, or + // reallocate would have returned None) — and it preserves length. + assert_eq!(out.len(), body.len()); + assert_eq!(validate_segment_rewrite(&body, &out), Ok(())); + } + + /// NON-VACUITY: prove the Chaitin/Briggs simplify/select core actually PLACES + /// a FREE (unpinned) node — not that the pins alone determine everything. A + /// register defined, used, then REDEFINED has an EARLIER range that is + /// neither a segment input (def != 0) nor the register's last-opened range + /// (live-out) — so it is unpinned, and the colourer must choose its register. + /// We give a SMALL pool so a valid colouring requires reusing a colour the + /// pins do not force: only the select phase can find it. + #[test] + fn simplify_select_places_a_free_interior_range() { + // Pool = {R0, R1} — only two colours. Body (all in-pool registers): + // r0 = r0 + r1 ; A: r0 redefined — its INPUT range (def 0) is pinned, + // this new r0 range is last-opened → pinned to colour 0 + // r1 = r0 + r1 ; r1 redefined: its input range pinned, new one + // last-opened → pinned to colour 1 + // Every range here is input-or-last-opened, so to get a genuinely FREE + // interior range we need a THIRD def of some register that is later + // overwritten. Use r0 defined, consumed, then r0 overwritten: + // 0: r0 = r0 + r1 (r0 range A: def=0? no, def=0 is the INPUT range; + // this DEF opens range A' — def=0 is instr 0's def, + // which IS index 0 → treated as input-pinned. avoid.) + // Cleaner: start the free range at a NON-zero instruction. + // 0: r1 = r0 + r0 ; opens r1 range (def=0 index → but this is the + // FIRST def of r1, at instr 0). To keep it + // unpinned we must redefine r1 later AND it must + // not be def==0. `straight_line_value_ranges` + // marks def with the instruction INDEX, and the + // input pin is `def == 0` meaning the range opened + // at index 0. So a def at index 0 is input-pinned. + // Use three instructions so the middle def is at index 1 (not 0) and is + // overwritten at index 2 (so not last-opened): + // 0: r1 = r0 + r0 ; r1 def@0 (input-pinned), r0 input (pinned) + // 1: r1 = r0 + r0 ; r1 def@1 — NOT index 0, and OVERWRITTEN next → + // neither input nor last-opened ⇒ FREE + // 2: r1 = r0 + r0 ; r1 def@2 last-opened (live-out) → pinned + let small_pool = [Reg::R0, Reg::R1]; + let body = vec![ + ins(ArmOp::Add { + rd: Reg::R1, + rn: Reg::R0, + op2: Operand2::Reg(Reg::R0), + }), + ins(ArmOp::Add { + rd: Reg::R1, + rn: Reg::R0, + op2: Operand2::Reg(Reg::R0), + }), + ins(ArmOp::Add { + rd: Reg::R1, + rn: Reg::R0, + op2: Operand2::Reg(Reg::R0), + }), + ]; + // The r1 range opened at instruction 1 is free (def index 1, overwritten + // at 2). It is dead-on-arrival (defined, immediately overwritten), so it + // does not interfere with the pinned r0/r1 ranges beyond r0; the colourer + // simplifies+selects a colour for it. A `Some` result that PASSES the + // trace-equality validator proves the free-placement path ran soundly. + let out = reallocate(&body, &small_pool).expect("free interior range colours"); + assert_eq!(out.len(), body.len()); + assert_eq!( + validate_segment_rewrite(&body, &out), + Ok(()), + "the colouring of the free interior range must preserve dataflow" + ); + } + + #[test] + fn declines_on_control_flow() { + // A branch makes it non-straight-line → decline (None). + let body = vec![ + ins(ArmOp::Add { + rd: Reg::R2, + rn: Reg::R0, + op2: Operand2::Reg(Reg::R1), + }), + ins(ArmOp::B { + label: ".exit".into(), + }), + ]; + assert!( + reallocate(&body, &POOL).is_none(), + "control flow is outside the bounded whole-straight-line scope" + ); + } + + #[test] + fn declines_on_call() { + let body = vec![ins(ArmOp::Bl { + label: "func_1".into(), + })]; + assert!( + reallocate(&body, &POOL).is_none(), + "a call is unmodeled — decline to the shipping path" + ); + } + + #[test] + fn declines_on_empty() { + assert!(reallocate(&[], &POOL).is_none()); + } +} diff --git a/crates/synth-synthesis/src/lib.rs b/crates/synth-synthesis/src/lib.rs index a23e086e..450c9863 100644 --- a/crates/synth-synthesis/src/lib.rs +++ b/crates/synth-synthesis/src/lib.rs @@ -2,6 +2,7 @@ pub mod contracts; pub mod control_flow; +pub mod graph_alloc; pub mod instruction_selector; pub mod liveness; pub mod optimizer_bridge; diff --git a/crates/synth-synthesis/src/liveness.rs b/crates/synth-synthesis/src/liveness.rs index 7daf4992..6ae9a9fb 100644 --- a/crates/synth-synthesis/src/liveness.rs +++ b/crates/synth-synthesis/src/liveness.rs @@ -172,8 +172,10 @@ pub fn reg_effect(op: &ArmOp) -> Option { } /// True if `op` is straight-line (no branch / label / call) and therefore safe -/// to include in a local, single-block analysis. -fn is_straight_line(op: &ArmOp) -> bool { +/// to include in a local, single-block analysis. `pub` so the VCR-DEC-001 +/// graph-colouring allocator ([`crate::graph_alloc`]) can share the exact +/// straight-line predicate this module's analyses use. +pub fn is_straight_line(op: &ArmOp) -> bool { use ArmOp::*; !matches!( op, @@ -14478,4 +14480,82 @@ mod tests { available (the universe-init correctness case) — got a false positive" ); } + + // ---- VCR-DEC-001 graph-allocator RED-FIRST probe (SYNTH_GRAPH_ALLOC) ---- + // Settles the load-bearing claim "the acceptance oracle gates the new + // allocator". The value-range graph allocator (crate::graph_alloc) rewrites + // each straight-line segment via a colouring and PROVES the rewrite preserves + // execution semantics with `validate_segment_rewrite` (the Rideau/Leroy + // pairwise trace-equality gate — STRONGER than "no interfering ranges share a + // register": it is exactly the check reallocate_function already runs, so the + // spike reuses the verified path's own acceptance oracle). VCR-RA-003 + // (validate_final_allocation) is the unconditional whole-function backstop on + // the final stream; wasmtime is the execution backstop. + // + // Red-first: a colouring bug that MERGES two simultaneously-live ranges onto + // one register breaks value flow — validate_segment_rewrite must reject it. + #[test] + fn graph_alloc_bad_rename_rejected_by_segment_validator() { + // Original straight-line segment (r2 = r0 + r1, then r0 is redefined and + // read — so r0's first value and r1 are both live at the add): + // movw r0,#1 ; movw r1,#2 ; add r2,r0,r1 ; add r3,r0,r2 + // r0 is live across the `add r2` (read again at `add r3`), and r1 is live + // there too — they interfere. + let orig = vec![ + ins(ArmOp::Movw { + rd: Reg::R0, + imm16: 1, + }), + ins(ArmOp::Movw { + rd: Reg::R1, + imm16: 2, + }), + ins(ArmOp::Add { + rd: Reg::R2, + rn: Reg::R0, + op2: Operand2::Reg(Reg::R1), + }), + ins(ArmOp::Add { + rd: Reg::R3, + rn: Reg::R0, + op2: Operand2::Reg(Reg::R2), + }), + ]; + // A DELIBERATELY BROKEN rewrite: rename r1's def+use to r0 — collapsing + // two interfering live values onto one register. `add r2,r0,r1` becomes + // `add r2,r0,r0`, changing the computed value: a real miscompile. + let broken = vec![ + ins(ArmOp::Movw { + rd: Reg::R0, + imm16: 1, + }), + ins(ArmOp::Movw { + rd: Reg::R0, // was r1 — clobbers r0's live value + imm16: 2, + }), + ins(ArmOp::Add { + rd: Reg::R2, + rn: Reg::R0, + op2: Operand2::Reg(Reg::R0), // was r1 + }), + ins(ArmOp::Add { + rd: Reg::R3, + rn: Reg::R0, + op2: Operand2::Reg(Reg::R2), + }), + ]; + assert!( + validate_segment_rewrite(&orig, &broken).is_err(), + "the segment trace-equality validator MUST reject a rename that \ + merges two interfering live ranges onto one register — this is the \ + red-first acceptance gate for the graph allocator's rewrite" + ); + // The identity rewrite (a no-op colouring) is accepted — the gate is not + // vacuously rejecting. + assert_eq!( + validate_segment_rewrite(&orig, &orig), + Ok(()), + "the identity rewrite must pass — the gate is non-vacuous" + ); + } } diff --git a/scripts/repro/vcr_dec_001_graph_alloc_differential.py b/scripts/repro/vcr_dec_001_graph_alloc_differential.py new file mode 100644 index 00000000..874cd556 --- /dev/null +++ b/scripts/repro/vcr_dec_001_graph_alloc_differential.py @@ -0,0 +1,225 @@ +#!/usr/bin/env python3 +"""VCR-DEC-001 graph-colouring allocator SPIKE differential (SYNTH_GRAPH_ALLOC). + +The North Star's first foothold: a whole-function Chaitin/Briggs graph-colouring +register allocator (crate `synth_synthesis::graph_alloc`), flag-gated behind +`SYNTH_GRAPH_ALLOC`, built AGAINST the acceptance oracles the verified path +already runs. This differential asserts the three properties that make the spike +sound, on the ARM fixture corpus (arm / cortex-m4, --all-exports --relocatable): + + (1) FLAG-OFF ≡ SHIPPING (the GOLDEN trick). `SYNTH_GRAPH_ALLOC` unset must + produce EXACTLY the shipping bytes — the flag-off path never enters the + graph_alloc branch. Pinned against the frozen goldens for the four canonical + fixtures (control_step, flight_seam, flight_seam_flat, signed_div_const). + + (2) FLAG-ON APPLIES on ≥1 named function per applying fixture, and on every + applied function the UNCONDITIONAL VCR-RA-003 validator + (validate_final_allocation) returns **Consistent** — the acceptance oracle + validating the new allocator's REAL output (observed via + SYNTH_RA003_VERBOSE, not inferred from returncode). + + (3) FLAG-ON ≡ FLAG-OFF on the whole corpus. This is a DESIGNED PROPERTY, not a + null result: on a straight-line function graph_alloc and the shipping + `reallocate_function` use the same pins (inputs + last-opened live-outs), + the same chaitin_core, and the same single-segment scope, so their outputs + are byte-identical BY CONSTRUCTION; everywhere else graph_alloc declines. + graph_alloc's output ⊆ {shipping bytes, decline}, so divergence is + impossible in increment 1. Execution correctness therefore follows + TRANSITIVELY: flag-on bytes = shipping bytes on applied functions, and the + shipping bytes are already wasmtime-gated by the frozen execution + differentials. (A passive flag-on-vs-wasmtime corpus would merely re-test + the shipping compiler, so it is deliberately NOT built here.) + +The red-first teeth — "a colouring bug → the acceptance oracle catches it" — are +the unit probe `graph_alloc_bad_rename_rejected_by_segment_validator` in +liveness.rs: validate_segment_rewrite (the trace-equality gate graph_alloc +invokes) rejects a value-flow-breaking merge-rename and accepts the identity. + +Usage: python3 vcr_dec_001_graph_alloc_differential.py +Exit 0 = all three properties hold; nonzero = a violation. +""" +import hashlib +import os +import subprocess +import sys +import tempfile +from pathlib import Path + +REPRO = Path(__file__).resolve().parent + +# Canonical frozen fixtures (fixture, golden .text sha256, golden len) — the exact +# pins from crates/synth-cli/tests/frozen_codegen_bytes.rs oracle_001. +FROZEN = [ + ("control_step.wasm", + "b365a29ef47ddd3e5ef8755d54cbd0d46c504af64dd24d08e9500385f674d892", 308), + ("flight_seam.wasm", + "28642d60533c3fc154dfc7ab27e6a9f4ffe5b0a81adfe4c0fba493d490fc8d2c", 870), + ("flight_seam_flat.wasm", + "7d3145c4ed0493cd326f867ab068930a64f3813bce60d031b19f535d0f800998", 1010), + ("signed_div_const.wasm", + "b277453b7829a5b2c64527131298d89fa63f5641231b1d4c7336675e8cdab9b0", 34), +] + +# Full corpus for the flag-on ≡ flag-off + RA-003 checks. +CORPUS = [ + "control_step.wasm", "flight_seam.wasm", "flight_seam_flat.wasm", + "signed_div_const.wasm", "controller_step.wasm", "filter_axis.wasm", + "gust_kernel.wasm", "sret_decide.wasm", "reachable_helper.wasm", + "msgq_put_359.wasm", +] + +# Flags the frozen gate removes so an ambient env var can't re-freeze the result. +CLEAR = [ + "SYNTH_NO_CMP_SELECT_FUSE", "SYNTH_NO_LOCAL_PROMOTE", "SYNTH_NO_IMM_SHIFT_FOLD", + "SYNTH_NO_STACK_FWD", "SYNTH_SPILL_REALLOC", "SYNTH_CONST_CSE", "SYNTH_BASE_CSE", + "SYNTH_DEAD_FRAME_ELIM", "SYNTH_UXTH_FOLD", "SYNTH_GRAPH_ALLOC", +] + + +def compile_arm(synth, wasm, extra_env): + env = dict(os.environ) + for k in CLEAR: + env.pop(k, None) + env.update(extra_env) + td = tempfile.mkdtemp() + elf = Path(td) / (wasm + ".elf") + r = subprocess.run( + [synth, "compile", str(REPRO / wasm), "-o", str(elf), + "-b", "arm", "--target", "cortex-m4", "--all-exports", "--relocatable"], + capture_output=True, env=env, + ) + return r, elf + + +def text_of(elf): + data = Path(elf).read_bytes() + return _extract_text(data) + + +def _extract_text(elf_bytes): + import struct + assert elf_bytes[:4] == b"\x7fELF", "not an ELF" + e_shoff = struct.unpack_from(" 0, at least one Consistent appears and NO Violation. + consistent = on_stderr.count("VCR-RA-003: Consistent") + violation = "register-allocation validation FAILED" in on_stderr + # Byte-identity flag-on ≡ flag-off (the designed property). + ident = text_of(off_elf) == text_of(on_elf) + if applied > 0: + applied_fixtures += 1 + ok = ident and not violation and (applied == 0 or consistent > 0) + tag = [] + tag.append(f"applied={applied}") + tag.append(f"RA003-consistent={consistent}") + tag.append("bytes≡" if ident else "BYTES-DIFFER<--") + if violation: + tag.append("RA003-VIOLATION<--") + print(f" {wasm:<24} {' '.join(tag)} {'OK' if ok else 'FAIL <--'}") + fails += 0 if ok else 1 + + # Non-vacuity: the allocator must ACTUALLY fire on at least a few fixtures, + # else the "≡ flag-off" property is trivially satisfied by never running. + print(f"== applying fixtures: {applied_fixtures} (must be ≥ 2 for non-vacuity) ==") + if applied_fixtures < 2: + print(" VACUOUS: graph_alloc never applied — increment-1 scope regressed.") + fails += 1 + + # DEEPER non-vacuity: prove graph_alloc's byte-match is NOT a trivial identity + # transform. Compile a known-applying fixture with the shipping re-allocation + # DISABLED (SYNTH_RANGE_REALLOC=0 = the raw selector stream): if the shipping + # reallocated bytes DIFFER from the raw stream, reallocation did real register + # work — and graph_alloc reproduced THOSE bytes (property 3), so graph_alloc + # is making the same non-trivial choices, not returning its input unchanged. + print("== (deeper non-vacuity) graph_alloc reproduces REAL reallocation ==") + r_raw, raw_elf = compile_arm(synth, "signed_div_const.wasm", + {"SYNTH_RANGE_REALLOC": "0"}) + r_realloc, realloc_elf = compile_arm(synth, "signed_div_const.wasm", {}) + r_ga, ga_elf = compile_arm(synth, "signed_div_const.wasm", + {"SYNTH_GRAPH_ALLOC": "1"}) + if all(x.returncode == 0 for x in (r_raw, r_realloc, r_ga)): + raw_t, realloc_t, ga_t = (text_of(raw_elf), text_of(realloc_elf), + text_of(ga_elf)) + did_work = raw_t != realloc_t + ga_matches = ga_t == realloc_t + ok = did_work and ga_matches + print(f" signed_div_const: raw={len(raw_t)}B realloc={len(realloc_t)}B " + f"graph_alloc={len(ga_t)}B realloc-did-work={did_work} " + f"graph_alloc≡realloc={ga_matches} {'OK' if ok else 'FAIL <--'}") + if not ok: + fails += 1 + else: + print(" signed_div_const: COMPILE FAIL") + fails += 1 + + print("-" * 60) + if fails: + print(f"VIOLATION: {fails} check(s) failed.") + return 1 + print("OK: flag-off frozen, flag-on applies + RA-003 Consistent + ≡ flag-off.") + return 0 + + +if __name__ == "__main__": + sys.exit(main())