VFP register-file spilling — the GI-FPU-002 exhaustion rung (#881, VCR-RA-004, epic #242) - #885
Merged
Conversation
Codecov Report❌ Patch coverage is 📢 Thoughts on this report? Let us know! |
… the #869 mixed shape deep_s: >16 live f32 (phase-1 S-file), deep_d: >8 live f64 (phase-2 D-file), deep_mix: i64->f32 converts under a live f32 stack (the v0.52 falcon rate/ekf D-pressure in f32-only-by-policy code). All three currently loud-decline on -t cortex-m7dp --relocatable with the exact messages the falcon v1.128 entry points report. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ng (VCR-RA-004, epic #242) StackVal::{Float,Double}Spilled + spill_deepest_vfp (deepest segment-local = farthest next use under LIFO discipline, the Belady criterion) + vfp_reload_spilled + vfp_ensure_headroom, driven by a pre-op VFP pressure guard active ONLY under the new vfp_spill_on_exhaustion retry rung (the backend re-runs the full recovery ladder with it after a first pass ends in a GI-FPU-002 exhaustion Err, composing with the #587 pool-grow rung). Soundness rails: - straight-line floor: entries pushed before the last control-flow boundary are never victims (a conditional spill store would not dominate its reload on the untaken path) - S/D aliasing: victims/holes tracked through the ONE shared 16-slot vfp_used map (D-alloc marks both S halves; the D-headroom loop spills until a FULL aligned pair frees) - pinned f32/f64 param+local homes are never victims (freeing relieves nothing) - VSTR/VLDR imm8*4 range (>1020 declines loudly, #180/#185) - spilled entries reaching any integer/float consumer un-reloaded is a loud decline, never a stale register read All three #881 repro shapes (deep_s S-file, deep_d D-file, deep_mix = the v0.52 #869 D-pressure-in-f32-only-code) now emit T symbols on -t cortex-m7dp --relocatable. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…al vs wasmtime Falcon flags (-t cortex-m7dp --relocatable), internal bl resolved by a real arm-none-eabi-ld link (hard-fail on any diagnostic — no reloc ever silently skipped), 109 rows incl. NaN/inf/subnormal operands, both select arms, spilled-across-call, pinned-home, and S/D-aliasing-churn shapes. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ed-across-call twins Invariant 5: per-straight-line-segment VFP spill-slot non-aliasing at 4-byte-half granularity (an F32Store clobbering half of a live F64Store's slot is caught; a provably-same-value re-store — same source S-word, no redefinition, the legal preserve-then-arg-stage overlap — is benign). Invariant 6: an S-word (2..16) defined before a bl and read after with no redefinition crossed the AAPCS-VFP caller-saved boundary; words 0/1 (S0/D0 return) excluded, the documented R0/R1-twin false-negative boundary. Both driven by vfp_word_effect: precise word-level defs/uses for the simple VFP ops, loud None for encoder-expanded compounds (decline > guess applied to the checker), Some(empty) for provably-VFP-free integer ops. All 8 float differentials re-run green against the now-stricter unconditional validator (no false positives on shipped patterns): 619 84/84, 708/709 48/48, 719 238/238, 369 339/339, 869 96296, 782 192686, 782b 702, 881 109. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Live-fixture red evidence (both reverted): dropping S2 preservation in
preserve_vfp_caller_saved fired VfpCallerSavedLiveAcrossCall{word:2,
call_index:32} on spill_call; forcing every VFP spill onto slot 0 fired
VfpSpillSlotAliased on deep_s/deep_d/spill_call — compiles REFUSED, not
miscompiled. Unit pins: two-live-values aliasing, F32-over-F64-half (S/D
aliasing), same-value refresh benign, refresh-after-redef caught,
live-across-bl caught, preserve/restore green, S0/S1 return exclusion.
Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…othing ran it vfp_spill_881_differential.py is the oracle behind this lane's headline claim (7 falcon-shaped exports reaching nm -> T, execution rows bit-identical to wasmtime on cortex-m7dp). It was written, committed, and referenced NOWHERE -- `git grep` found no ci.yml entry and no other caller. The PR board was green with its central gate inert, so the claim was hand-checked only. That is the #879 shelfware class recurring inside the very release whose audit found and fixed two other instances of it (gpio-thin, rv32-boot). Writing an oracle and wiring an oracle are separate steps, and the second is the one that gets dropped when a lane runs out of budget -- which is exactly what happened here: the lane died on a session limit. Wired with the anti-vacuity discipline the #879 fix established: set -o pipefail (a bare `| tee` would report tee's exit status), plus greps on BOTH halves of the claim -- the full export count, so a silent decline cannot read as success, and a non-zero execution-row count. Exit 0 alone is not trusted. Verified red-first by mutation: rewriting the summary to 0 execution rows fails the row grep, and to "all 6 exports" fails the export grep. The committed branch state passes on its own (7 exports, 109 rows) with the lane's uncommitted work-in-progress excluded. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… install ld Wiring the oracle (previous commit) immediately earned its keep: it failed on the CI runner with FileNotFoundError 'arm-none-eabi-nm' while passing locally. A host dependency is exactly what a local run cannot detect -- the #850 class, where an oracle that only works on the author's machine is a local check, not a gate. Two host dependencies, handled differently because they are not the same: 1. `arm-none-eabi-nm` -- REMOVED. Symbols now come from the ELF symbol table via pyelftools (already a dependency of this job). Note this file's own `load()` already did it that way, citing #489 "symtab, not disasm text"; only main() still shelled out. The port must look the table up by TYPE (SHT_SYMTAB), not by name: synth's relocatable objects emit their symtab with an EMPTY sh_name, so get_section_by_name(".symtab") returns None on a file that has one. `nm` searches by type, which is why the shell-out worked and a naive by-name port reported "no .symtab" -- a false failure that would have looked like a miscompile. 2. `arm-none-eabi-ld` -- INSTALLED (binutils only, not the full gcc). The link step is load-bearing: it proves the internal `bl` relocation actually resolves, and skipping it would make that half of the gate vacuous. When a dependency backs a real check, install the dependency; do not delete the check. Verified: 7 exports emitted, 109 execution rows bit-identical to wasmtime. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
force-pushed
the
feat/vfp-spilling-881
branch
from
July 29, 2026 19:13
fe09859 to
b4e833d
Compare
avrabe
added a commit
that referenced
this pull request
Jul 30, 2026
…CLOSED Cold review found the v0.53 assembly was about to ship the SAME defect class as v0.51 and v0.52, with a new twist: the ledger was defending it. F1 (BLOCK) — the FEATURE_MATRIX "Honest Summary" cited #881, #882 and #872 as open residuals. All three were CLOSED by lanes in THIS release. Root cause is a lane-ordering race: L6's doc-honesty commit landed 2026-07-29 15:28 and said "honest-summary residual examples now cite the actually-open issues (#881/#882/#872)" -- true when written; L1 closed #881 fourteen hours later. The doc-honesty lane ran FIRST and nobody re-swept after the fixes landed. The document had become self-contradictory: the summary said RV32 br_table still declines while the backend row three sections up said it lowers. Re-pointed at genuinely-open issues (#890, #851, #846), verified against `gh issue view`. F2 (BLOCK) — claims.yaml PINNED the stale "#881" verbatim, so `claim_check` reported 34/34 while green-confirming a false residual, and correcting the prose would have turned the gate RED. CLAUDE.md says never fix a red gate by loosening the ledger; this was the inverse -- a ledger entry that had gone false, so the gate protected the defect instead of catching it. The fix is structural, not a re-point: an ISSUE-NUMBER pin goes stale the moment the issue is fixed, because `verbatim` only asserts the phrase is PRESENT. This pin has now been wrong twice for exactly that reason (#782, then #881). It now pins the CAPABILITY GAP -- "single-precision FPUs", the i64-from-f32 decline that genuinely remains -- which becomes false precisely when the gap closes. Red-first verified: replacing the phrase reddens SYNTH-F32-F64-VFP (exit 1), restoring it returns green. F3 -- three of seven lanes had NO changelog entry, including L4/#872: a default-on soundness fix that MOVED SHIPPED BYTES (gust_poll 692->696, fact-spec 132->140). A user diffing v0.52->v0.53 output would have found no explanation. Added L1 (#885), L4 (#888) and L7 (#889) entries, and collapsed a duplicate `### Added` section that violated the Keep-a-Changelog structure the release process mandates. F4 -- README declared "No multi-memory" while the matrix (corrected this release) says P with a CI-wired differential. Multi-memory phase 1 shipped in v0.43 (#749); the README line was ~10 releases stale, so v0.53 would have shipped two documents disagreeing about a capability. F5 -- the #880 changelog entry claimed every pinned phrase is bound to its oracle AND that oracle's CI wiring. SYNTH-MATRIX-WCET-COMPOSITION has neither -- the sound-WCET-bound row, one of the most safety-load-bearing claims in the matrix, is the single exception. Named it rather than softening it away. F6 -- #872's real remaining hole (a mid-segment `Pop {…,PC}` the segment-local validator misses) and VCR-DEC-001's (a wrong-return-register rewrite accepted by `validate_cfg_rewrite` AND VCR-RA-003 both, caught only by execution) existed only in Rust doc-comments. Both now stated in the matrix and CHANGELOG: the release was simultaneously OVERSTATING what is open and OMITTING what is. claim_check 34/34, docs regenerated, render byte-fresh. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Jul 30, 2026
* chore(release): v0.53.0 — "The last mile" (7 lanes) Version sweep: workspace + all 13 intra-workspace path-dep pins + MODULE.bazel + status.json, Cargo.lock refreshed to 0.53.0 (v0.52's cold review caught a stale lock; no CI job builds --locked, so this one is on the release process). Docs regenerated once at assembly per #805 -- lanes do not hand-edit generated artifacts. claim_check 34/34, check_version_pins OK. CHANGELOG headline added by the coordinator over the 8 lane-written entries. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(release): cold-review blockers — stop citing issues this release CLOSED Cold review found the v0.53 assembly was about to ship the SAME defect class as v0.51 and v0.52, with a new twist: the ledger was defending it. F1 (BLOCK) — the FEATURE_MATRIX "Honest Summary" cited #881, #882 and #872 as open residuals. All three were CLOSED by lanes in THIS release. Root cause is a lane-ordering race: L6's doc-honesty commit landed 2026-07-29 15:28 and said "honest-summary residual examples now cite the actually-open issues (#881/#882/#872)" -- true when written; L1 closed #881 fourteen hours later. The doc-honesty lane ran FIRST and nobody re-swept after the fixes landed. The document had become self-contradictory: the summary said RV32 br_table still declines while the backend row three sections up said it lowers. Re-pointed at genuinely-open issues (#890, #851, #846), verified against `gh issue view`. F2 (BLOCK) — claims.yaml PINNED the stale "#881" verbatim, so `claim_check` reported 34/34 while green-confirming a false residual, and correcting the prose would have turned the gate RED. CLAUDE.md says never fix a red gate by loosening the ledger; this was the inverse -- a ledger entry that had gone false, so the gate protected the defect instead of catching it. The fix is structural, not a re-point: an ISSUE-NUMBER pin goes stale the moment the issue is fixed, because `verbatim` only asserts the phrase is PRESENT. This pin has now been wrong twice for exactly that reason (#782, then #881). It now pins the CAPABILITY GAP -- "single-precision FPUs", the i64-from-f32 decline that genuinely remains -- which becomes false precisely when the gap closes. Red-first verified: replacing the phrase reddens SYNTH-F32-F64-VFP (exit 1), restoring it returns green. F3 -- three of seven lanes had NO changelog entry, including L4/#872: a default-on soundness fix that MOVED SHIPPED BYTES (gust_poll 692->696, fact-spec 132->140). A user diffing v0.52->v0.53 output would have found no explanation. Added L1 (#885), L4 (#888) and L7 (#889) entries, and collapsed a duplicate `### Added` section that violated the Keep-a-Changelog structure the release process mandates. F4 -- README declared "No multi-memory" while the matrix (corrected this release) says P with a CI-wired differential. Multi-memory phase 1 shipped in v0.43 (#749); the README line was ~10 releases stale, so v0.53 would have shipped two documents disagreeing about a capability. F5 -- the #880 changelog entry claimed every pinned phrase is bound to its oracle AND that oracle's CI wiring. SYNTH-MATRIX-WCET-COMPOSITION has neither -- the sound-WCET-bound row, one of the most safety-load-bearing claims in the matrix, is the single exception. Named it rather than softening it away. F6 -- #872's real remaining hole (a mid-segment `Pop {…,PC}` the segment-local validator misses) and VCR-DEC-001's (a wrong-return-register rewrite accepted by `validate_cfg_rewrite` AND VCR-RA-003 both, caught only by execution) existed only in Rust doc-comments. Both now stated in the matrix and CHANGELOG: the release was simultaneously OVERSTATING what is open and OMITTING what is. claim_check 34/34, docs regenerated, render byte-fresh. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude <noreply@anthropic.com>
This was referenced Jul 30, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
v0.53 lane L1. Gives the VFP register file the spill path the integer file has had since VCR-RA-001, closing the GI-FPU-002 exhaustion rungs (phase 1 S0..S15, phase 2 D0..D7) that block five falcon entry points.
Closes #881. Lane hit the session limit before final self-report; coordinator gating on CI.