RQ-60-VFPPRESSURE increment 2: frame-homed overflow VFP locals — the 13->14 homed-local wall falls, 5/5 falcon cascade stages on cortex-m7dp (Refs #1069)

[avrabe]

RQ-60-VFPPRESSURE increment 2 — VFP pressure from homed locals. Refs #1069.

The measurement this is built on (and why the roadmap's fix was wrong)

jess's fixture plus a discriminating variant — same pressure, different residence:

LOCALS (homed)                    OPERAND STACK (#881-rescued)
  13 locals : ok                    30 deep : ok
  14 locals : EXHAUSTED             40 deep : ok
  16 locals : EXHAUSTED             60 deep : ok

Sixty simultaneously-live f32 on the operand stack compile; fourteen in homed locals do not. The 13→14 wall is home residence, not register-file capacity: a home S-register is pinned for the function's extent, and spill_deepest_vfp (correctly) never victims a home. Extending the pool into callee-saved S16..S31 would move the same wall from ~13 to ~29 locals at prologue/epilogue cost on every affected function — re-derived, agreed with the brief, not implemented.

Red first (literal output, commit 7f658f3)

$ synth compile scripts/repro/vfp_local_pressure_1069.wat -t cortex-m7dp --relocatable -o red.o
Compiling function 'live13'...   384 bytes of machine code
warning: skipping function 'live14': ... GI-FPU-002: VFP register file exhausted (S0..S15 all live) —
  ... the backend retries with VFP spilling (#881) and this surfaces only if that also fails
warning: skipping function 'live16': ... VFP register file exhausted ...
warning: skipping function 'live24': ... VFP register file exhausted ...
warning: skipping function 'live8d': ... GI-FPU-002 phase 2: caller-saved VFP D-register file exhausted ...
Error: #952: 4 of 5 requested export(s) were skipped   [exit 1]

After (this branch): all 5 compile; RESULT: PASS, 70/70 emulations bit-identical to wasmtime.

The three design decisions

1. Spill the local, or de-home it? — De-home at birth, never evict. A mid-function eviction must emit a transfer store that dominates every later read; on one arm of a branch it does not (the same dominance hole the stack guard's cf_floor exists to avoid), and the single-pass selector has no dominator analysis. Frame-homing from the first def sidesteps it: local.set is the store, local.get loads — dominance is inherited from wasm's own def-use semantics, since the store sits exactly where wasm writes the local.

2. Choosing the victim — a positional cap, not a next-use heuristic. No pinned local home may sit above S7/D3; a fresh local whose lowest-free grant lands above the cap (or fails) is frame-homed. First-def order decides who keeps a register — honest reason: a single forward pass has no next-use information without a pre-scan, and the cap is what guarantees the invariant that matters for soundness of the rest of the rung: S8..S15 (4 aligned D-pairs) stay reclaimable, which is exactly the worst transient demand in vfp_op_demand (the #869 conversion family, 4 pairs). A furthest-next-use / access-count pre-scan is a named quality follow-up, not a soundness need.

3. Ladder — a separate LAST-resort stage, not a change to the #881 rung. This one was corrected by measurement mid-lane: the first draft gated the cap on vfp_spill_on_exhaustion itself, and the real falcon rate.o moved bytes — rate@0.7.0#tick compiles today via the plain rung with f64 homes above D3. So the cap lives behind a new selector lever (set_vfp_frame_home_locals), and the backend tries it only after the plain #881 rung and its pool-grow composition failed:

base → int rungs → #587 pool-grow
  → plain #881 VFP rung (+ pool-grow)          ← yesterday's path, verbatim
    → #1069 frame-homed locals (+ pool-grow sized depth + distinct-local-targets + 4)   ← NEW, last

plain_rung_stays_yesterdays_path_for_shapes_it_already_rescues pins the class red-first: base red, plain rung green by itself, and the frame lever provably produces different instructions for it — the ordering is load-bearing.

The two traps, handled

• Substring-is-control-flow: the frame-homed slot pool exhaustion message is a pub const (VFP_FRAME_HOME_SLOT_EXHAUSTION) that arm_backend.rs matches directly — one source, no drifting copy. live24 (24 locals > the 8-slot pool) is the test that goes red if the message and the matcher ever separate: it compiles only if the retry fires.
• arm: i64 register-pair + i64 spill-slot-pool exhaustion still skips functions post-Belady (v0.24.0) — the falcon regalloc remainder (#242) #587 scoping: the pool-grow rung grows slots, not registers — correct that it can't help the register wall. But frame-homed locals hold permanent slots outside the operand-stack depth bound, so the frame stage's grow retry is sized depth + distinct local.set/tee targets + 4. The plain rung's grow keeps yesterday's depth + 4 exactly.

Byte-identity evidence (currently-compiling functions)

• Structural: the frame lever is set only on the last-resort retry; base path, plain rung, and grow rung re-run verbatim first. live13 (jess's negative control) compiles on the base path — pinned by test.
• Frozen anchors: cargo test --workspace green (includes the frozen-fixture byte gates).
• Real modules: falcon rate.o and mixer.o (the two stages that fully compile on main) — cmp bit-identical main vs branch. rate is the strong case: it compiles via the plain rung, and it is the module that caught the first draft.
• GI-FPU-002 + RA tail is now the ONLY gate between the falcon cascade and the M7 — 5 entry-point symbols; phase-2 D-register pressure is new in v0.52 (inline-f64 #869 lowering) #881 oracle re-run green: 109/109 execution rows bit-identical (incl. deep_local, the homes-are-never-victims pin).

Execution differential (CI-wired)

scripts/repro/vfp_local_pressure_1069_differential.py — new oracle_run CI step, emulations >= 40, measured 70:

• live13/14/16/24 (f32) and live8d (f64) on -t cortex-m7dp --relocatable, linked with arm-none-eabi-ld (any diagnostic hard-fails), executed under unicorn vs wasmtime bit-exact (NaN==NaN per §4.3.3) across ±0, ±1, denormal-underfow, 1e±30, ±inf, NaN;
• every local's round-tripped value feeds one product tree, so a spill that reloads the wrong slot is a plausible wrong float that flips result bits — the class the comparison exists to catch;
• #973 ARM corpus sweep re-run PASS (154/167 compiled, 2502/2502 vectors; the new fixture's f32 columns compile on the m4f sweep target, live8d declines by f64 precision there, named in EXPECTED_DECLINES).

The falcon cascade, by symbol name, on cortex-m7dp (the target jess ships)

Pulled the published falcon 1.134.1 components from ghcr (the issue's public repro), compiled -t cortex-m7dp --relocatable --all-exports --embedder-data-init --embedder-global-init:

symbol	main (e6a3b27)	this branch
pulseengine:falcon-cascade/attitude@0.7.0#tick	skipped (S-file exhausted)	nm → T
pulseengine:falcon-cascade/ekf@0.7.0#estimate	skipped (S-file exhausted)	nm → T
pulseengine:falcon-cascade/position@0.7.0#tick	skipped (D-file exhausted)	nm → T
pulseengine:falcon-cascade/rate@0.7.0#tick	nm → T	nm → T, bit-identical
pulseengine:falcon-cascade/mixer@0.7.0#mix	nm → T	nm → T, bit-identical

5/5 cascade stages — #1069's definition of done, on the per-stage components. position#tick was not in this increment's assigned scope (phase-2 D-file) but the same mechanism closes it: its D-pressure is inline-conversion temps plus pinned D homes, and capping the homes gives the #869 machinery its 4 pairs back. Bonus: all five also compile on single-precision cortex-m7 (where increment 1 had already cleared position only).

Gates

• cargo fmt --all clean; cargo clippy --workspace --all-targets -- -D warnings clean; cargo test --workspace exit 0, 152 suites, 0 failures (incl. the 8 new tests and the frozen-anchor byte gates), gated on cargo's own exit code, not a pipeline tail's.
• python3 scripts/claim_check.py claims.yaml exit 0: selector_lines_code 18910 → 19199 with a same-commit waiver (to: 19199) — growth, not substitution: every existing path is byte-frozen so nothing could be deleted in exchange. selector_lines_total 29556 → 29845. Wildcard pins unmoved (the guard override is written wildcard-free). artifacts/status.json regenerated.

Honest residuals (named, not hidden)

• Fused-cascade verification is per-stage here, not on the meld-fused image: the local meld (0.9.0) predates fuse --memory shared --pack-rebase (issue used 0.52.0). The per-stage objects are exactly what the issue's step-1 pulls; jess's standing offer in GI-FPU-002: three named cascade entry points are the entire remaining gap to a complete falcon M7 image (attitude#tick, ekf#estimate, position#tick) — everything else in the chain now works #1069 is the right loop for the fused RT1176 image, and the delta above is stated per symbol so it can be checked against it directly.
• The rescued functions' correctness evidence is the fixture differential, not an executed attitude/ekf run — executing the real #tick/#estimate needs the component ABI/memory environment (jess's on-target loop). The mechanism (frame round-trip under pressure) is what the 70-row differential proves bit-exact, on the same code path.
• Quality, not soundness: frame-homed locals pay a load per local.get; first-def order (not next-use) decides who keeps a register; a pre-scan ranking locals is a named follow-up. Functions rescued by this stage previously did not compile at all.
• WCET: a frame-homed local's VLDR/VSTR are straight-line ops on the priced path; nothing new declines, but no new bound claim is made either.
• Params are untouched — AAPCS fixes their homes (possibly above the cap); only fresh non-param locals get the residence decision. A signature whose f32 params alone fill the file still declines, exactly as before.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

❌ Patch coverage is 82.64840% with 38 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-synthesis/src/instruction_selector.rs	76.55%	34 Missing ⚠️
crates/synth-backend/src/arm_backend.rs	93.22%	4 Missing ⚠️

📢 Thoughts on this report? Let us know!