Repository navigation
feat(vcr-ra): backward-dataflow allocation validator v1 — the assurance carrier (VCR-RA-003, v0.11.39) - #323
Merged
Merged
Conversation
…-003)
Rideau/Leroy CC'10 translation validation, adapted to synth's phys-to-phys
renames-only re-allocation class, wired as the acceptance gate the range
re-allocation pass (default-ON since v0.11.36) cannot bypass.
Algorithm (validate_segment_rewrite): walk (original, rewritten) in
backward lockstep (same length + register-erased opcode shapes verified
first) maintaining equations orig_reg ~ rewritten_reg. Exit seed = the
original's per-register last-written set as identity (the pass's live-out
pinning), with AAPCS scratch (R2/R3/R12/LR) exempted when the segment ends
in `pop {...,pc}` (a return: scratch is dead-out by convention). Defs
discharge positional pairs and reject any equation touching a defined
register under a different pairing; uses add positional equations
UNCONDITIONALLY (covers flags and memory: every operand feeding a
flag-setter or store is forced equal). Entry: all surviving equations must
be identity (input pinning). RMW ops (Movt/SelectMove) need no special
case: reg_effect lists rd as both def and use, so the def discharges and
the use re-imposes the prior-value pairing.
The validator immediately caught a real latent hole in the pass: pinning
the per-register LAST range does not pin the register's EXIT VALUE — the
colourer can relocate a later range onto a pinned register after its last
use (dies-at-birth non-interference), changing exit state (seen on the
flight_seam_flat whole-leaf segment, benign there because the segment ends
in a return; a miscompile waiting to happen on a mid-function segment).
Return segments are accepted via the AAPCS exemption; the mid-function
shape is now REJECTED and falls back to the original bytes (test
reallocate_function_is_sound_and_near_identity_on_packed_greedy_code
updated to pin the gated truth).
Evidence (rivet verification-criteria for VCR-RA-003 v1):
- accepts everything the pass produces: real fixture compiles show
0 validator rejects (control_step 5 seg/2 realloc, div_const 1/1,
flight_seam_flat fires across all functions); new ReallocStats
field validator_rejects pinned to 0 by
realloc_on_repro_fixture_streams_has_zero_validator_rejects
(criterion allows <5%; current truth 0).
- mutation campaign: 196/200 seeded mutants killed (98.0%, >=95%
criterion); 4 survivors are the documented dead-def /
pass-through-register class, equivalent under the validated contract.
- fixtures BIT-IDENTICAL vs origin/main (sha256: control_step
824884c4..., div_const cada05fe..., flight_seam_flat 03ce9019...);
differentials PASS: control_step 13/13, div_const 338/338,
flight_seam_flat 0x07FDF307 == wasmtime.
- cargo test -p synth-synthesis: 377 passed; synth-backend: green;
clippy -D warnings clean; fmt clean.
Honest v1 bounds (vs the full Rideau/Leroy class): renames-only (no
spill/reload, coalescing, or live-range splitting validation yet — the
pass does not produce them); no copy-aware equation transfer through Mov;
rewritten-side writes to registers the original never defines are
unchecked when segment-dead (the pass's own pass-through contract, closed
by cross-segment liveness in step 5); unverified Rust (v2 = Rocq
soundness proof against exec_indexed).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
This was referenced Jun 11, 2026
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.
What
VCR-RA-003 v1 — the Rideau/Leroy-style backward-dataflow translation validator, now the acceptance gate guarding the default-ON re-allocation pass: every segment rewrite must prove dataflow preservation (equation sets walked backward in lockstep, defs discharge, uses impose, entry must be identity) or the segment falls back to original bytes.
It earned its keep before merging
On first contact with production output the validator rejected a genuine latent hole: the pass's live-out pinning pins the last range, not the register's exit value — benign at function returns (principled AAPCS scratch exemption added: R2/R3/R12/LR dead-out by convention) but a real cross-segment hazard mid-function, now mechanically guarded (rejected → safe fallback) until step-5's cross-segment liveness closes it properly.
Evidence (rivet criteria, met)
reallocated > 0 && validator_rejects == 0cmp-bit-identical to main ×3; differentials PASS (13/13, 338/338,0x07FDF307)Honest limits
Renames-only class (no spill/coalesce/split validation yet — widens with VCR-RA-004's consumers); flags/memory soundness via unconditional use-equations rather than modeling; unverified Rust — v2 is the Rocq soundness proof (v0.12.0 scope), at which point the validator (350-line class, per the literature) carries the tool-qualification assurance instead of the allocator.
Traceability: VCR-RA-003 (
release-v0.11.39, epic #242).🤖 Generated with Claude Code