Context
The VCR-RA-003 register-allocation validator (synth_synthesis::liveness::validate_final_allocation, #808) is ARM-only today. It runs unconditionally on every ARM compile and hard-errors on:
It is deeply coupled to the ARM backend:
- signature is
validate_final_allocation(instrs: &[ArmInstruction])
- callee-saved set hard-coded
[R4, R5, R6, R7, R8]
- prologue/epilogue detected via ARM
Push { regs } (LR-containing) / Pop
- def/use classification via
reg_effect(op: &ArmOp) (ArmOp-specific)
Why RV32 is a separate lane, not "also run it"
RV32 needs a parallel re-implementation, not a target parameter:
- a different instruction enum (
synth_backend_riscv::riscv_op::RiscVOp, not ArmInstruction)
- a different callee-saved set — RV psABI
s0–s11 (x8–x9, x18–x27)
- a different prologue/epilogue shape (
addi sp, sp, -N + sw ra, …(sp), not a reg-list push)
- no
reg_effect def/use classifier exists for RiscVOp — one must be written (the RV analogue of the ARM reg_effect "bail-on-unmodeled → None" contract, so the fail-safe direction is preserved)
This was scoped honestly during the VCR-SEL-005 universe-complete cross-backend op-parity lane (#49): landing the parity gate solidly was preferred over half-implementing a soundness checker on a second backend.
Deliverable
validate_final_allocation_rv32(instrs: &[RiscVOp]) -> RaFinalVerdict (or a shared trait), with an RV32 reg_effect- red-first non-vacuity unit tests mirroring
ra003_red_* / ra003_green_*: synthetically revert a known-fixed RV32 clobber → the validator CATCHES it; assert SILENT on correct RV32 codegen
- wire it unconditionally on the RV32 compile path (mirroring the ARM wiring), frozen-safe (checker emits nothing — RV32
.text byte-identical, the frozen RV32 oracle unchanged)
- a named CI job (sibling of
vcr-ra-003-alloc-validator-gate)
Refs
Epic #242 (VCR-*). ARM validator: #808 / #490 / #331. Parity lane that scoped this out: #49.
Context
The VCR-RA-003 register-allocation validator (
synth_synthesis::liveness::validate_final_allocation, #808) is ARM-only today. It runs unconditionally on every ARM compile and hard-errors on:It is deeply coupled to the ARM backend:
validate_final_allocation(instrs: &[ArmInstruction])[R4, R5, R6, R7, R8]Push { regs }(LR-containing) /Popreg_effect(op: &ArmOp)(ArmOp-specific)Why RV32 is a separate lane, not "also run it"
RV32 needs a parallel re-implementation, not a target parameter:
synth_backend_riscv::riscv_op::RiscVOp, notArmInstruction)s0–s11(x8–x9,x18–x27)addi sp, sp, -N+sw ra, …(sp), not a reg-list push)reg_effectdef/use classifier exists forRiscVOp— one must be written (the RV analogue of the ARMreg_effect"bail-on-unmodeled → None" contract, so the fail-safe direction is preserved)This was scoped honestly during the VCR-SEL-005 universe-complete cross-backend op-parity lane (#49): landing the parity gate solidly was preferred over half-implementing a soundness checker on a second backend.
Deliverable
validate_final_allocation_rv32(instrs: &[RiscVOp]) -> RaFinalVerdict(or a shared trait), with an RV32reg_effectra003_red_*/ra003_green_*: synthetically revert a known-fixed RV32 clobber → the validator CATCHES it; assert SILENT on correct RV32 codegen.textbyte-identical, the frozen RV32 oracle unchanged)vcr-ra-003-alloc-validator-gate)Refs
Epic #242 (VCR-*). ARM validator: #808 / #490 / #331. Parity lane that scoped this out: #49.