feat(#242): VCR-RA-003 phase 2 — across-CALL + across-JOIN allocation validation (whole-function)

[avrabe]

VCR-RA-003 phase 2 (epic #242) — make the register-allocation validator WHOLE-FUNCTION

v0.48 (#808) shipped validate_final_allocation — an UNCONDITIONAL per-compilation register-allocation validator (runs on every ARM compile in the default --features riscv build, hard-errors on violation) — but BOUNDED to straight-line segments + spill/reload + callee-saved discipline. This lane extends it past straight-line to control-flow joins and calls.

Two new invariants (each anchored on a reference OUTSIDE inferred value-identity — the v0.48 vacuity lesson)

3. Caller-saved preservation across a CALL. A value in R2/R3/R12 defined before a bl/blx/call and read after it (no intervening redef) crossed a boundary the AAPCS is contractually allowed to clobber → CallerSavedLiveAcrossCall. The reference is the ABI contract at the call, not an inferred redefinition. R0/R1 are excluded (a call DEFINES them: the return value) — a documented false-negative boundary (FN < FP). Reasoned locally; does not modify the shared reg_effect (whose None-on-call meaning the phase-1 callee-saved fail-safe + eliminate_unread_frame_stores both depend on).

4. Value availability across a JOIN. A register live-in to a CF join (≥2 preds) must be AVAILABLE — must-defined on every incoming path, or an entry live-in → else JoinValueNotAvailable. Forward MUST (intersection) availability fixpoint (universe-init, not empty — it is a must-analysis) over a dedicated join CFG that admits bx lr returns (sinks) and calls (fall-through with a caller-saved def-set), so branchy functions with calls/returns stay analyzable. Entry seed = params R0-R3, SP, LR, and the RESERVED registers R9/R10/R11/R12 (contracts::regalloc::RESERVED_REGS — R11 = linmem base, resident by construction).

RaFinalVerdict gains NotAttempted { reason } — a loud honest decline when the join CFG can't be built (numeric branch, BrTable, computed Bx, dup label). NON-FATAL at the arm_backend call site; only Violation hard-errors. Decline>guess applied to the checker itself.

Red-first evidence (non-vacuity proven BEFORE trusting)

cargo test -p synth-synthesis --lib ra003_ — 17 tests. New phase-2:

• RED across-CALL: ra003_red_caller_saved_live_across_call_is_caught — R2 defined, bl, R2 read → asserts the SPECIFIC CallerSavedLiveAcrossCall (never Violation | *).
• RED across-JOIN: ra003_red_across_join_clobber_is_caught — R4 on then-path, R5 (not R4) on else-path, join reads R4 → asserts the SPECIFIC JoinValueNotAvailable{R4}.
• GREEN: return-value-after-call, callee-saved-across-call, both-paths-define, dominator-defined-at-join.
• ra003_join_declines_on_unmodeled_control_flow — BrTable → NotAttempted (never a silent Consistent).

Silent on real codegen + vacuity-in-practice

• Invariant 4 FIRES on real branchy codegen (traced: if_else_result_343 / cf_shapes_500 / block_brif_483 joins all Consistent, incl. a real R11 availability check) — not unit-tested-but-dead-in-shipping.
• Found + fixed a real false positive: block_brif_483's nested — a str [r11,#off] at a join, R11 (linmem base) defined nowhere in the stream → fixed by seeding the reserved registers.
• Sweep: 130 fixtures on --relocatable + control_step & 7 branchy × {relocatable, default} = 16 pairs → 0 false positives.

Path scope (honest)

Invariant 4 fires on the label-form / --relocatable path (analyzable CFG). On the default optimized path branches are pre-resolved to NUMERIC offsets before the validator runs, so invariant 4 declines to NotAttempted there (invariants 1-3 still run on both paths — control_step, the differential's own input, compiles CLEAN on the default path). The NotAttempted decline is common on the default path (~41/130 fixtures), so its diagnostic eprintln is gated behind SYNTH_RA003_VERBOSE (production stays quiet, verdict observable on demand). Numeric-branch CFG = named follow-up.

Frozen / gates

• Frozen 10/10 byte-identical (control_step 0x00210A55, flight_algo 0x07FDF307) — the validator emits nothing.
• Full cargo test --workspace green; clippy -D warnings clean; cargo fmt --check clean.
• claim_check 25/25. rivet: 52 errors / 102 warnings identical to origin/main (pre-existing coverage backlog; this lane adds zero new errors).
• CI: appended a third step to vcr-ra-003-alloc-validator-gate running scripts/repro/vcr_ra_003_phase2_join_call.py over branchy/mem/call fixtures on BOTH paths (existing red-first + frozen steps untouched).

Still loud-flags-unattempted (named follow-ups)

• Optimized-path numeric-branch joins (resolved-offset CFG builder, the AUDIT: spill-realloc passes delete instructions on resolved-offset streams — same branch-overshoot hazard class as the #604 const-CSE miscompile (default-on since v0.24.0) #606 geometry) → NotAttempted.
• RV32 / AArch64 get their own arms later (per-backend, like VCR-VER-003).
• v2 Rocq-mechanized soundness of the straight-line fragment.

Merged origin/main (VCR-SEL-005 #816 + #761 R9/globals base separation); re-verified all gates post-merge.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L