feat(#815): VCR-RA-003 RV32 register-allocation validator (RV32 analogue of the ARM gate)

.github/workflows/ci.yml

@@ -1686,6 +1686,62 @@ jobs:
           cargo build -p synth-cli
           python3 scripts/repro/vcr_ra_003_phase2_join_call.py ./target/debug/synth
 
+  vcr-ra-003-rv32-alloc-validator-gate:
+    name: "VCR-RA-003 RV32 register-allocation validator (red-first + frozen)"
+    # VCR-RA-003 for RISC-V (#815, epic #242): the RV32 analogue of the ARM
+    # register-allocation validator. A PARALLEL re-implementation
+    # (synth_backend_riscv::alloc_validator::validate_final_allocation_rv32) keyed
+    # on the RV32 calling convention — NOT a reuse of the ARM-coupled
+    # validate_final_allocation. It runs UNCONDITIONALLY on every RV32 compile in
+    # the default `--features riscv` build (wired in backend.rs
+    # compile_function_with_opts, on the selector's `selection.ops`) and
+    # hard-errors on a violation of the two STRAIGHT-LINE invariants #815 names:
+    #   (1) CALLEE-SAVED PRESERVATION — a body write of an s-register the pass
+    #       saves (s1, s2..s10, mirroring `preserve_callee_saved`; the reserved
+    #       s0/fp + s11/linmem-base excluded) must be saved by the prologue
+    #       `sw s_k, off(sp)` + restored by every epilogue `lw s_k, off(sp)` ->
+    #       CalleeSavedNotSaved / CalleeSavedNotRestored.
+    #   (2) SPILL-SLOT NON-ALIASING — a frame slot `off(sp)` overwritten by a
+    #       second `sw` while its value is still reloaded downstream, per
+    #       straight-line segment (an `addi sp` frame adjust resets the map) ->
+    #       SpillSlotAliased.
+    # A `Call` (the ARM phase-2 across-call/across-join frontier, no RV CFG yet)
+    # is a NON-FATAL NotAttempted (decline > guess). This job pins the gate:
+    #   (a) RED-FIRST non-vacuity: the ra003rv_red_* unit tests synthetically
+    #       revert a known-fixed clobber (drop the prologue save -> CalleeSavedNotSaved;
+    #       drop the epilogue restore -> CalleeSavedNotRestored; alias two live
+    #       values on one slot -> SpillSlotAliased) and assert the validator
+    #       CATCHES it. The ra003rv_green_* tests assert it is SILENT on correct
+    #       code + a Call -> NotAttempted.
+    #   (b) SILENT-ON-REAL-CODEGEN: the frozen RV32 oracle compiles the RV32
+    #       fixtures THROUGH the unconditional validator; if it false-positived on
+    #       a real function that fixture would fail to compile, so 10/10 green
+    #       (control_step 0x00210A55 byte-identical) is the "Consistent on every
+    #       real RV32 function" proof — PLUS a dedicated repro sweeping 9 fixtures
+    #       × {relocatable, default} = 18 pairs asserting ZERO false positives.
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v7
+      - uses: dtolnay/rust-toolchain@stable
+      - name: Cache Cargo dependencies
+        uses: actions/cache@v6
+        with:
+          path: |
+            ~/.cargo/registry
+            ~/.cargo/git
+            target/
+          key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
+          restore-keys: |
+            ${{ runner.os }}-cargo-
+      - name: RED-FIRST non-vacuity + silent-on-correct (RV32 validator unit tests)
+        run: cargo test -p synth-backend-riscv --lib ra003rv
+      - name: Silent-on-real-codegen (frozen suite through the unconditional gate)
+        run: cargo test -p synth-cli --test frozen_codegen_bytes
+      - name: Silent-on-real-codegen (RV32 fixture sweep, both paths)
+        run: |
+          cargo build -p synth-cli
+          python3 scripts/repro/vcr_ra_003_rv32_alloc_validator.py ./target/debug/synth
+
   vcr-sel-005-cross-backend-op-parity-gate:
     name: "VCR-SEL-005 cross-backend op-parity (universe-complete + red-first)"
     # VCR-SEL-005 (#242, #223, #232): the "selector missed an op" class was never

artifacts/verified-codegen-roadmap.yaml

@@ -2016,6 +2016,53 @@ artifacts:
         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.
+        RV32 ARM LANDED (v0.50, #815) — the per-backend RV32 analogue promised at
+        "RV32 / AArch64 get their own arms later" now ships: a PARALLEL
+        re-implementation `synth_backend_riscv::alloc_validator::
+        validate_final_allocation_rv32` (RaFinalVerdict / RaFinalViolation in that
+        crate), keyed on the RV32 calling convention — NOT a reuse of the
+        ARM-coupled `validate_final_allocation` (different instruction enum
+        RiscVOp, different callee-saved set, different `addi sp,-N` + `sw s_k`
+        prologue shape). Wired UNCONDITIONALLY in `backend.rs`
+        (`compile_function_with_opts`, on `selection.ops` immediately after the
+        selector) on EVERY RV32 compile in the default `--features riscv` build
+        (both `compile_module` — the ELF path — and `compile_function` reach it),
+        hard-erroring on a Violation. Two STRAIGHT-LINE invariants (the two #815
+        names): (1) CALLEE-SAVED PRESERVATION — a body write (op_dest) of an
+        s-register the pass saves (s1, s2..s10 = `is_callee_saved_temp`, mirroring
+        `preserve_callee_saved` EXACTLY; the reserved s0/fp + s11/linmem-base are
+        excluded so the checker never false-positives on the pass's own output)
+        must be saved by a prologue `sw s_k, off(sp)` and restored by every
+        epilogue `lw s_k, off(sp)` before a `ret` (jalr x0,0(ra)) ->
+        CalleeSavedNotSaved / CalleeSavedNotRestored; (2) SPILL-SLOT NON-ALIASING
+        — the same holder model as the ARM validator, per straight-line segment,
+        an `addi sp` frame adjust resetting the slot map (the RV analogue of ARM's
+        `ldr sp,[sp,#N]` clear) -> SpillSlotAliased. A `Call` is the ARM
+        phase-2 across-call/across-join frontier (no RV `cfg_liveness` yet) ->
+        NON-FATAL NotAttempted { reason: "rv32-call-boundary" } (decline > guess;
+        the two straight-line invariants still ran). DELIBERATELY NO
+        "unmodeled-op → force-prologue" fail-safe (unlike ARM): on RV every
+        op_dest==None op is CF/system/label/call and writes no s-register, so the
+        fail-safe would be vacuous AND disagree with the pass -> a false-positive;
+        omitting it keeps validator↔pass agreement. RED-FIRST non-vacuity (8
+        `ra003rv_*` unit tests in alloc_validator.rs): 3 RED synthetically revert a
+        known-fixed clobber and assert the CATCH (drop the prologue save of a used
+        s2 -> CalleeSavedNotSaved; drop the epilogue restore -> CalleeSavedNotRestored;
+        alias two live values on one slot -> SpillSlotAliased) + 4 GREEN assert
+        SILENT (the balanced save/use/restore leaf; a pure-scratch t0/a0 leaf;
+        sequential single-slot reuse; a Call -> NotAttempted) + 1 asserting a
+        straight-line Violation BEFORE a Call still fires (the Call does not mask
+        it). SILENT-ON-REAL-CODEGEN: the frozen RV32 oracle
+        (`frozen_fixtures_rv32_text_is_bit_identical_oracle_001`, control_step
+        0x00210A55) compiles through the unconditional validator — 0 false
+        positives, byte-identical — PLUS a dedicated repro
+        (`scripts/repro/vcr_ra_003_rv32_alloc_validator.py`) sweeps 9 RV32 fixtures
+        × {relocatable, default} = 18 pairs (callee-saved-heavy control_step /
+        controller_step, spill-heavy gust_kernel, branchy flight_seam, call-bearing
+        reachable_helper) with 0 validator false-positives. CI-gated:
+        `vcr-ra-003-rv32-alloc-validator-gate` in ci.yml (red-first unit tests +
+        frozen RV32 oracle + the silent-on-real repro). AArch64 arm still open (the
+        integer subset has minimal spill traffic; a NAMED follow-up).
 
   - id: VCR-RA-004
     type: sw-req