fix(vcr-ra): spill passes honor resolved branch geometry (#606)

[avrabe]

Adversarial fixture verdict — SAFE today, by accident

Every adversarial shape executes bit-identical to wasmtime on current main defaults (unicorn Thumb vs wasmtime, linear-memory window compare, both branch directions):

OK spill_branch::spill_arm(0,)/(1,)   12-deep operand stack -> spills INSIDE a block/br_if/br arm
OK spill_branch3::spill_arm(0,)/(1,)  pressure burst spills $v, two reloads in the arm (stack-fwd + spill-realloc FIRE, direct path)
OK spill_branch4::spill_arm(0,)/(1,)  const evicted before the branch, reused twice in the arm
OK sel_arm::sel_arm / shl_arm         select / const-shift inside the arm (fuse + shift-fold probes)
VERDICT: ALL MATCH   (identical result with the main binary and the fixed binary)

So no shipped miscompile, no patch release needed. But the audit shows the safety is FIVE unrelated accidents, not a design property:

1. bridge reload_spill targets reserved R12, which stages 1–2 (spill_forward_segment, collect_spill_pairs) exclude;
2. eviction spill slots are fresh-monotonic (next_spill_offset only grows) — no same-slot overwrite for the frame-slot DCE to prove dead;
3. stage 3 (eliminate_unread_frame_stores) declines wholesale on any numeric branch via its admission scan — the only designed barrier of the five;
4. spill_on_exhaust's scope gate excludes Branch/CondBranch, so i64 pair reloads (non-reserved regs, stages 1–2 visible) never coexist with real control flow — only with fixed-content bne+0; udf trap-guard spans;
5. non-const pressure under control flow declines to the direct selector (Optimized path silently miscompiles register-exhausting i32 folds (no spill, no decline) #496), whose label-form branches re-resolve after the passes (verified: the b.n displacement adapts, e010→e00f, on the firing spill_branch3 shape).

Change any one of those (e.g. reload into an allocated register instead of R12 — the obvious next perf lever) and the #604 class comes back silently, default-on.

The fix — #604's rule, adopted structurally

resolved_branch_geometry (targets = barriers, span byte-freeze, decline-on-unmappable) is now enforced in all five rewriting passes on the shared stream, not just const-CSE:

pass	barrier at resolved targets	span byte-freeze
apply_spill_realloc stages 1–2	segment split	segment rewrite must be exactly size-neutral
eliminate_dead_frame_stores	forward scan stops	frozen candidate stores kept
forward_stack_reloads (#390)	forward scan stops (loop back-edge join)	4-byte ldr→2-byte mov declined in-span
eliminate_unread_frame_stores	already structurally safe — now pinned by test	(wholesale decline)
reallocate_function	segment split (a rename valid on the fall-through edge is unproven on a taken edge entering mid-segment)	width-flipping (R8↔low, 16↔32-bit) recolours declined in-span

New resolved_branch_geometry_labels_as_zero: the direct selector emits mixed streams (label-form CF + numeric trap guards). The #604 helper declines those — which gave back real forwarding wins on msgq_put_359. The variant maps Label as 0 bytes (exactly what resolve_label_branches encodes), keeping every direct-path win. const-CSE keeps its #604 decline stance byte-for-byte.

Evidence

• 7 new pass-level adversarial tests, each paired with a branch-free non-vacuity control that proves the same shape still fires outside spans.
• Frozen anchors bit-identical: frozen_codegen_bytes + both escape-hatch gates green, no re-pins.
• Corpus (148 repro fixtures × default / --relocatable / SYNTH_BASE_CSE=0, new vs main): 229/231 .text-identical. The 2 deltas (msgq_put_359 default+basecse0) are one instruction-count- and byte-size-neutral recolour (udiv r1,r0,r1; mov r1,r1 → udiv r2,r0,r1; mov r1,r2) where the trap-guard join now correctly splits a realloc segment; accepted by the VCR-RA-003 backward-dataflow validator. Give-back: zero (the labels-as-zero variant restored all of msgq's forwarding wins; only the recolour choice differs).
• Differential sweep: 52 pass / 0 regressions. sret_decide_differential fails identically with the main binary — its compiled .o is bit-identical old-vs-new (cmp clean), so it is a harness-environment issue, not this PR. Skipped (external fixtures not in repo): call_indirect_594 (/tmp/ci594.o), call_indirect_597 (/tmp/ci597.o), wake_path (/tmp/merged.wat).
• cargo test -p synth-synthesis -p synth-cli green (exit 0); cargo fmt --check + cargo clippy -D warnings clean.

Also adds SYNTH_PATH_DEBUG=1 (env-gated) exposing which selector path compiled each function — this audit was impossible to do honestly without it.

Closes #606

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 97.92899% with 7 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-synthesis/src/liveness.rs	98.74%	4 Missing ⚠️
crates/synth-backend/src/arm_backend.rs	84.21%	3 Missing ⚠️

📢 Thoughts on this report? Let us know!