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

.github/workflows/ci.yml

@@ -1636,23 +1636,33 @@ jobs:
 
   vcr-ra-003-alloc-validator-gate:
     name: "VCR-RA-003 register-allocation validator (red-first + frozen)"
-    # VCR-RA-003 (#242): the UNCONDITIONAL, single-stream backward-dataflow
-    # register-allocation validator (synth_synthesis::liveness::
-    # validate_final_allocation) runs on every ARM compile in the default build
-    # and hard-errors on a callee-saved-preservation (#490) or spill-slot
-    # non-aliasing (#331) violation. This job pins the gate's TWO halves as an
-    # explicit, self-describing red so a regression is visible on its own name:
+    # VCR-RA-003 (#242): the UNCONDITIONAL register-allocation validator
+    # (synth_synthesis::liveness::validate_final_allocation) runs on every ARM
+    # compile in the default build and hard-errors on a violation of FOUR
+    # invariants: (1) callee-saved preservation (#490), (2) spill-slot
+    # non-aliasing (#331), and — PHASE 2 (#49), whole-function past straight-line
+    # — (3) caller-saved preservation across a call and (4) value availability
+    # across a control-flow join. This job pins the gate's halves as an explicit,
+    # self-describing red so a regression is visible on its own name:
     #   (1) RED-FIRST non-vacuity: the ra003_red_* unit tests synthetically
-    #       revert a known-fixed clobber and assert the validator CATCHES it
-    #       (revert #490 prologue -> CalleeSavedNotSaved; drop epilogue restore
+    #       revert / construct a known clobber and assert the validator CATCHES
+    #       it (revert #490 prologue -> CalleeSavedNotSaved; drop epilogue restore
     #       -> CalleeSavedNotRestored; alias two live values on one slot ->
-    #       SpillSlotAliased). The ra003_green_* tests assert it is SILENT on
-    #       correct code (the Consistent half).
+    #       SpillSlotAliased; a caller-saved value live across a bl ->
+    #       CallerSavedLiveAcrossCall; a value in R4 on one join path but not the
+    #       other -> JoinValueNotAvailable; a BrTable -> NotAttempted loud
+    #       decline). The ra003_green_* tests assert it is SILENT on correct code.
     #   (2) SILENT-ON-REAL-CODEGEN: the frozen suite compiles the whole ARM
     #       fixture set THROUGH the unconditional validator; if it false-positived
     #       on any real function that fixture would fail to compile, so 10/10 green
     #       (control_step 0x00210A55, flight_algo 0x07FDF307 byte-identical) is the
     #       validator's "Consistent on every real function" proof.
+    #   (3) PHASE-2 SILENT + FIRES ON REAL BRANCHY CODEGEN: the phase-2 repro
+    #       compiles branchy / memory-touching / call-bearing fixtures (real CF
+    #       joins the availability check reasons about) and asserts ZERO false
+    #       positives — the guard against the R11-linmem-base regression this lane
+    #       found (a join reading the reserved base register, defined nowhere in
+    #       the stream, must be seeded available not flagged).
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v7
@@ -1671,6 +1681,10 @@ jobs:
         run: cargo test -p synth-synthesis --lib ra003_
       - name: Silent-on-real-codegen (frozen suite through the unconditional gate)
         run: cargo test -p synth-cli --test frozen_codegen_bytes
+      - name: PHASE-2 silent-on-real-branchy-codegen (across-CALL + across-JOIN)
+        run: |
+          cargo build -p synth-cli
+          python3 scripts/repro/vcr_ra_003_phase2_join_call.py ./target/debug/synth
 
   vcr-sel-005-cross-backend-op-parity-gate:
     name: "VCR-SEL-005 cross-backend op-parity (universe-complete + red-first)"

artifacts/verified-codegen-roadmap.yaml

@@ -1955,7 +1955,66 @@ artifacts:
         in synth-synthesis (not synth-core) because ArmOp/Reg live there and the
         register-assigned stream is consumed in arm_backend before main.rs.
         ARM-scoped this increment; RV32 / AArch64 get their own arms later
-        (per-backend, like VCR-VER-003). v2 (Rocq-mechanized soundness of the
+        (per-backend, like VCR-VER-003).
+        PHASE 2 (v0.49, #49) — WHOLE-FUNCTION across CALLS and JOINS: the named
+        phase-2 boundary is now extended past straight-line with two more
+        invariants, each anchored on a reference OUTSIDE inferred value-identity
+        (the v0.48 vacuity lesson: generic GP-liveness on one stream cannot tell
+        a clobber from a redefinition). (3) CALLER-SAVED PRESERVATION ACROSS A
+        CALL: a value in R2/R3/R12 defined before a bl/blx/call and read after it
+        with 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 value. R0/R1 are EXCLUDED (a
+        call DEFINES them: the return value) - a documented false-NEGATIVE
+        boundary (FN < FP). Reasoned locally at the call site; does NOT modify the
+        shared `reg_effect` (whose None-on-call meaning the phase-1 callee-saved
+        fail-safe and `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`. Solved by a forward MUST
+        (intersection) availability fixpoint (UNIVERSE-init, not empty - it is a
+        must-analysis) over a DEDICATED join CFG (`build_join_cfg`) that admits
+        `bx lr` returns (sinks) and calls (fall-through with a caller-saved
+        def-set), so branchy functions with calls/returns remain analyzable
+        instead of wholesale-declining. Entry seed = params R0-R3, SP, LR, AND the
+        RESERVED registers R9/R10/R11/R12 (`contracts::regalloc::RESERVED_REGS` -
+        R11 = linmem base etc., never allocated, resident by construction);
+        seeding them is REQUIRED to avoid a false positive on every
+        memory-touching branchy function (the block_brif_483 `nested` case: a
+        `str [r11,#off]` at a join, R11 defined nowhere in the stream - this lane
+        FOUND + FIXED that regression). RaFinalVerdict gains `NotAttempted {
+        reason }` - a LOUD honest decline when the join CFG cannot be built
+        (numeric branch, BrTable, computed Bx, duplicate label); NON-FATAL at the
+        arm_backend call site (only Violation hard-errors), so a construct the
+        checker cannot model never blocks a correct compile but is also never
+        silently passed. RED-FIRST non-vacuity extended (17 `ra003_*` tests): +2
+        RED assert the SPECIFIC violation (a caller-saved value live across a bl
+        -> CallerSavedLiveAcrossCall; a value in R4 on one join path but not the
+        other -> JoinValueNotAvailable), +4 GREEN (return-value-after-call,
+        callee-saved-across-call, both-paths-define, dominator-defined at a join),
+        +1 NotAttempted (BrTable -> loud decline). Vacuity-in-practice VERIFIED:
+        invariant 4 FIRES on real branchy codegen (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.
+        HONEST PATH SCOPE: invariant 4 FIRES (analyzable label-form CFG) on the
+        RELOCATABLE / direct-selector path; on the DEFAULT optimized path branches
+        are already resolved to NUMERIC offsets (BOffset/BCondOffset) before the
+        validator runs, so the join CFG cannot be built and invariant 4 declines
+        to NotAttempted THERE (invariants 1-3 still run on both paths - a
+        false-positive Violation on either would hard-error the compile). Verified
+        BOTH paths: control_step on the DEFAULT path (the control_step
+        differential's own input) + 7 branchy fixtures × {relocatable, default} =
+        16 pairs, 0 false positives; the full 130-fixture default-path sweep is
+        also 0 violations. The NotAttempted decline is COMMON on the default path
+        (~41/130 fixtures), so its diagnostic eprintln is gated behind
+        `SYNTH_RA003_VERBOSE` (a production compile stays quiet; the verdict is
+        observable on demand). Extending invariant 4 to the numeric-branch
+        optimized path (a resolved-offset CFG builder, the #606 geometry) is a
+        NAMED follow-up. CI-gated: the third `vcr-ra-003-alloc-validator-gate`
+        step runs `scripts/repro/vcr_ra_003_phase2_join_call.py` over
+        branchy/mem/call fixtures on BOTH paths (silent-on-real-branchy-codegen).
+        Frozen-safe (emits nothing; control_step 0x00210A55 / flight_algo
+        0x07FDF307 byte-identical, 10/10). v2 (Rocq-mechanized soundness of the
         straight-line fragment) remains the open step.
 
   - id: VCR-RA-004

crates/synth-backend/src/arm_backend.rs

@@ -1360,28 +1360,55 @@ fn compile_wasm_to_arm(
 
     // VCR-RA-003 (epic #242): UNCONDITIONAL per-compilation register-allocation
     // validation. The register allocator is the last major unverified codegen
-    // component; this single-stream backward-dataflow checker proves — by
-    // construction, on the EXACT emitted stream about to be encoded — that the
-    // allocation preserves the two invariants whose reference lives in the
-    // stream: callee-saved preservation (#490) and spill-slot non-aliasing
-    // (#331). It runs on every ARM compile in the DEFAULT shipping build (NOT
-    // behind `--features verify`; a verify-gated check would be dormant in
-    // exactly the build that ships — the #757 / VCR-VER-003 lesson) and
-    // hard-errors the compile on a violation. Branches / CF joins and unmodeled
-    // ops (calls, i64-pair, FP) are the named PHASE-2 boundary: the spill check
-    // segments at them (never reasoning across a join), so this is honest — it
-    // never claims coherence it cannot prove. Frozen-safe: it emits nothing, so
-    // `.text` is byte-identical (proven by the frozen suite).
-    if let synth_synthesis::liveness::RaFinalVerdict::Violation(v) =
-        synth_synthesis::liveness::validate_final_allocation(&arm_instrs)
-    {
-        return Err(format!(
-            "VCR-RA-003: register-allocation validation FAILED — {v:?}. \
-             The emitted stream violates a register-allocation invariant \
-             (callee-saved preservation #490 / spill-slot non-aliasing #331); \
-             this is a compiler bug, not a program error. Refusing to emit a \
-             miscompiled object."
-        ));
+    // component; this whole-function checker proves — by construction, on the
+    // EXACT emitted stream about to be encoded — that the allocation preserves
+    // FOUR invariants whose reference lives in the stream (or the ABI): (1)
+    // callee-saved preservation (#490), (2) spill-slot non-aliasing (#331), and
+    // — PHASE 2 (#49), extending past straight-line — (3) caller-saved
+    // preservation across calls (a value in R2/R3/R12 live across a `bl` the
+    // AAPCS boundary destroys), and (4) value availability across control-flow
+    // joins (a live-in to a join must be defined on every incoming edge). It runs
+    // on every ARM compile in the DEFAULT shipping build (NOT behind
+    // `--features verify`; a verify-gated check would be dormant in exactly the
+    // build that ships — the #757 / VCR-VER-003 lesson) and hard-errors the
+    // compile on a VIOLATION. A `NotAttempted` verdict (the join check declines
+    // on an unmodeled-CF function: numeric branch, `BrTable`, etc.) is NON-FATAL
+    // — the compile proceeds; the other three invariants were still checked and
+    // held. This is the decline>guess doctrine applied to the checker itself: it
+    // never claims join coherence it cannot prove, but it also never blocks a
+    // correct compile for a construct it simply doesn't model yet. Frozen-safe:
+    // it emits nothing, so `.text` is byte-identical (proven by the frozen suite).
+    match synth_synthesis::liveness::validate_final_allocation(&arm_instrs) {
+        synth_synthesis::liveness::RaFinalVerdict::Violation(v) => {
+            return Err(format!(
+                "VCR-RA-003: register-allocation validation FAILED — {v:?}. \
+                 The emitted stream violates a register-allocation invariant \
+                 (callee-saved preservation #490 / spill-slot non-aliasing #331 \
+                 / caller-saved-across-call / join-value-availability); this is a \
+                 compiler bug, not a program error. Refusing to emit a \
+                 miscompiled object."
+            ));
+        }
+        // Loud honest decline (join reasoning skipped for an unmodeled-CF
+        // function). Non-fatal — the straight-line / callee-saved / across-call
+        // invariants still ran and held; only the across-JOIN availability
+        // reasoning is skipped (the optimized path pre-resolves branches to
+        // NUMERIC offsets, outside the label-form CFG the join check needs, so
+        // this is the COMMON case on the default path — ~41/130 repro fixtures).
+        // Surfaced only under `SYNTH_RA003_VERBOSE` so a production compile stays
+        // quiet: emitting it unconditionally would print on every branchy
+        // optimized-path compile (new stderr noise phase 1 never produced), yet
+        // it must remain observable on demand for the honest-scope audit.
+        synth_synthesis::liveness::RaFinalVerdict::NotAttempted { reason } => {
+            if std::env::var_os("SYNTH_RA003_VERBOSE").is_some() {
+                eprintln!(
+                    "VCR-RA-003: across-join validation NOT ATTEMPTED ({reason}) — \
+                     straight-line / callee-saved / across-call invariants held; \
+                     join-availability reasoning declined on this control-flow shape."
+                );
+            }
+        }
+        synth_synthesis::liveness::RaFinalVerdict::Consistent => {}
     }
 
     // Encode to binary — use Thumb-2 for Cortex-M targets