VCR-DEC-001: whole-function graph-colouring allocator spike (flag-off, #242)

.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)

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