VCR-DEC-001: whole-function graph-colouring allocator spike (flag-off, #242)#843
Merged
Conversation
…olour-interfering assignment Settles the load-bearing acceptance-oracle claim for the SYNTH_GRAPH_ALLOC graph-colouring spike: the allocator's own graph self-check (verify_allocation against the interference graph) catches the generic colouring bug (two interfering values sharing a colour) and passes a valid colouring. VCR-RA-003 (validate_final_allocation) remains the unconditional backstop for the structural classes (callee-saved #490, spill aliasing #331). Refs #242, VCR-DEC-001. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… (the real gate) The value-range graph allocator's acceptance oracle is validate_segment_rewrite (Rideau/Leroy pairwise trace-equality — the check reallocate_function already runs), NOT verify_allocation on the physical-Reg graph (which the value-range path never calls). Re-aimed: a colouring bug that merges two interfering live ranges onto one register is rejected by validate_segment_rewrite; the identity rewrite passes. This certifies the gate the shipped allocator actually invokes. Refs #242, VCR-DEC-001. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…locator core (flag-off) The North Star's first foothold: a Chaitin/Briggs graph-colouring register allocator built AGAINST the acceptance oracle the verified path already runs (validate_segment_rewrite trace-equality). Reuses the shared liveness dataflow — straight_line_value_ranges -> range_interference -> color_ranges (R0-R8 pool, inputs/live-outs pinned, reserved R9-R12 identity) -> apply_range_coloring -> validate_segment_rewrite. A rewrite the validator rejects is dropped and the function declines. Bounded scope (increment 1): WHOLE straight-line functions only. Declines to the shipping reallocate_function on ANY control flow, spill, or unmodeled op — never hard-fails. Increment 2 (named): whole-function webs across joins via cfg_liveness. Nothing is wired yet (no caller); this commit adds the module + its 4 unit tests + makes is_straight_line pub for shared use. Flag-off is byte-identical (no call site). Refs #242, VCR-DEC-001. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…03 Consistent on applied output) - arm_backend.rs: SYNTH_GRAPH_ALLOC hook branches around ONLY step 1 (reallocate_function); the later dead-frame/callee-saved-prologue/shrink passes run on graph_alloc's output unchanged, so an R4-R8 home still gets its push (the invariant VCR-RA-003 guards). Decline → shipping path, never hard-fail. Flag-off never enters the branch (byte-identical). - Added SYNTH_RA003_VERBOSE print in the Consistent arm (byte-invisible, opt-in) so 'RA-003 Consistent on the applied output' is OBSERVED fact, not inferred from returncode (NotAttempted also returns 0). - graph_alloc.rs: reverted an ill-advised fault-injection/bypass seam (a soundness footgun in the soundness module) — the red-first teeth are the unit probe in liveness.rs (validate_segment_rewrite rejects a merge-rename). - vcr_dec_001_graph_alloc_differential.py: reframed to the three REAL properties — (1) flag-off ≡ frozen goldens, (2) flag-on applies on ≥2 fixtures with RA-003 Consistent on every applied function, (3) flag-on ≡ flag-off (a DESIGNED property: on a straight-line function graph_alloc and reallocate_function share pins+chaitin_core+scope, so byte-identity is by construction; execution correctness follows transitively via the frozen wasmtime differentials). Result: flag-off frozen; flag-on applies on 6/10 corpus fixtures, RA-003 Consistent on every applied function, byte-identical everywhere. Refs #242, VCR-DEC-001. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…mantics-oracle Byte-only differential (pyelftools only, no unicorn/wasmtime): gates flag-off ≡ frozen goldens, flag-on applies on ≥2 fixtures with VCR-RA-003 Consistent on every applied function, and flag-on ≡ flag-off corpus-wide. ci.yml parses (PyYAML-checked). Static run: line, no untrusted-input interpolation. Refs #242, VCR-DEC-001. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Addresses the vacuity risk 'does the graph allocator ever place a free node, or do the pins determine everything': - Unit test simplify_select_places_a_free_interior_range: a register defined, used, redefined has an interior range that is neither a segment input nor the register's live-out — genuinely UNPINNED. reallocate() must place it (Chaitin simplify/select runs) and the result passes validate_segment_rewrite. - Differential deeper non-vacuity: signed_div_const raw selector = 40B, shipping reallocation = 34B (register work happened), graph_alloc = 34B (reproduced it). So graph_alloc's byte-identity to the shipping path is the from-construction pipeline REPRODUCING real reallocation, NOT returning its input unchanged. Refs #242, VCR-DEC-001. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
enabled auto-merge (squash)
July 22, 2026 19:07
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
VCR-DEC-001 — whole-function graph-colouring register allocator SPIKE (flag-off)
The North Star's first foothold (epic #242, decision VCR-DEC-001): synth's
greedy single-pass allocator is the patch-accreting component the whole VCR program
exists to replace. This spike lands a Chaitin/Briggs graph-colouring allocator
in its own module (
crates/synth-synthesis/src/graph_alloc.rs), gated flag-offbehind
SYNTH_GRAPH_ALLOC, built against the acceptance oracle the verified pathalready runs — so any code it emits is provably allocation-sound.
What it does (bounded increment 1)
Whole straight-line functions only. Reuses the shared liveness dataflow —
straight_line_value_ranges→range_interference→color_ranges(R0-R8 pool,inputs + last-opened live-outs pinned, reserved R9-R12 identity) →
apply_range_coloring→
validate_segment_rewrite(the Rideau/Leroy trace-equality gate — the SAMEacceptance oracle
reallocate_functionuses). A rewrite the validator rejects isdropped and the function declines to the shipping
reallocate_function— never ahard-fail. Declines on ANY control flow, spill, or unmodeled op.
Surgical hook: branches around ONLY step 1 (
reallocate_function_post_exhaust) inarm_backend.rs; the laterelide_dead_frame/ensure_callee_saved_prologue/shrink_callee_saved_savespasses run on graph_alloc's output unchanged (so a value ithomes in R4-R8 still gets its callee-saved push — the invariant VCR-RA-003 guards). No
edits to the shared selector/optimizer_bridge the #837 sibling lane touches.
Evidence
Flag-off byte-identical (the GOLDEN trick). The flag-off path never enters the
graph_alloc branch. All 10 frozen-fixture gates green; the differential re-pins
control_step
b365a29e…/308, flight_seam28642d60…/870, flight_seam_flat7d3145c4…/1010,signed_div_const
b277453b…/34 — byte-for-byte the shipping goldens.VCR-RA-003 validates the new allocator's REAL output. With
SYNTH_GRAPH_ALLOC=1theallocator APPLIES on 6/10 corpus fixtures (signed_div_const, filter_axis, flight_seam,
flight_seam_flat, sret_decide, reachable_helper), and the unconditional
validate_final_allocationreturns Consistent on every applied function — observedvia
SYNTH_RA003_VERBOSE(not inferred from returncode;NotAttemptedalso returns 0).The internal
validate_segment_rewriteis the gate that provably ran (else the functionwould have declined); RA-003 is the whole-function backstop, Consistent here because the
applied functions are straight-line.
Red-first (the oracle has teeth). Unit probe
graph_alloc_bad_rename_rejected_by_segment_validator:validate_segment_rewriterejectsa value-flow-breaking merge-rename (two interfering ranges → one register) and accepts the
identity.
reallocate'sErr → Noneroutes that rejection to a safe decline.Differential vs wasmtime. No direct flag-on-vs-wasmtime run — and this is a designed
ceiling, not a dropped deliverable: on a straight-line function graph_alloc and the
shipping
reallocate_functionshare pins +chaitin_core+ single-segment scope, sograph_alloc's output ⊆ {shipping bytes, decline} and divergence is impossible in increment
all 6), and the shipping bytes are already wasmtime-gated by the frozen execution
differentials — so execution correctness follows transitively.
Non-vacuity (the colourer makes REAL choices). Byte-identity is not a trivial identity
transform: signed_div_const raw selector = 40 B, shipping reallocation = 34 B (real
register work), graph_alloc = 34 B (reproduced it). Plus a unit test
(
simplify_select_places_a_free_interior_range) exercising an unpinned interior rangethrough Chaitin simplify/select.
What declines to greedy
Any control flow / call /
BrTable/ i64-pair / FP op / spill / duplicate label →None→ shippingreallocate_function(which HAS spill + multi-segment support).Not in this spike (named next increment)
Increment 2: whole-function webs across control-flow joins via
cfg_liveness—where "the allocator and validator share the dataflow" fully lands. Needs SSA-style web
construction across joins that does not exist yet.
Frozen + claims
Frozen-safe (flag-off byte-identical, 10/10 gates). No proof-count / claims.yaml / roadmap
change (25/25 claims hold; VCR-DEC-001 left as its approved decision record — it is a
decision constraint whose verification-criteria is the revisit-trigger, not an
implementation requirement).
rivet validateclean of non-cross-repo errors; ci.ymlPyYAML-parses. Cover targets only (cortex-m4 / qemu).
🤖 Generated with Claude Code
https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L