Repository navigation
fix(selector): spill i64 register pairs + call results under pressure (#171) - #198
Merged
Merged
Conversation
…#171) i64-heavy functions that kept more i64 values live than the 5 consecutive register pairs hold hit "no consecutive pair" exhaustion and were dropped by the #168 skip-and-continue net. #188's caller-saved preservation added pressure that pushed z_impl_k_sem_give over the edge (it compiled on v0.11.6, was skipped on v0.11.8). This implements the real spill. - Operand stack `Vec<Reg>` → `Vec<StackVal>` (`Reg | Spilled { lo_slot }`). `stack_live_regs` counts only register-resident entries. - `alloc_consecutive_pair` spills the deepest register-resident entry to a frame slot (STR lo/hi) when no pair is free, freeing it, and retries. `pop_operand` / `peek_operand` reload a spilled value into a fresh pair (LDR lo/hi) on consume. - `LocalLayout` reserves an 8-slot i64 spill area (`i64_spill_base`), only when the function has i64 ops (keeps i32-only frames unchanged); slots are reused. - Call path under pressure: `restore_caller_saved` spills the call result to the frame (returns `StackVal::Spilled`) when no callee-saved reg is free to park it; `emit_arg_moves` acquires its cycle-break scratch lazily (only for a genuine cycle), so an acyclic arg move needs no free reg. Acceptance: the 6-live-i64 case now compiles via spill (was Err); a z_impl-shaped i64+calls function compiles end-to-end (was skipped). 1292 workspace tests pass, fmt + clippy clean; #188/#195/#170 non-regression confirmed. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Aug 21, 2026
…truction, not a lost condition; pin the STABLE branch population, re-state the reconstruction floors with the evidence THE DIAGNOSIS (coordinator asked for the inventory, not the counts). The #990 fix added ~100 lines of UNSCORED code (the zero-init classifier) to a crate linked into the MC/DC harness wasm. Zero scored-function source changed, the 56 rows unchanged — yet CI's scored table went 26 dec/6 full -> 21/3: validate_final_allocation_rv32 7->4, validate_served_image 2->0, count_params_heuristic::{closure} 1->0, validate_reloc_resolutions 2->1 (its full-MC/DC credit is one of the two lost; build_options' the other), sp_slot_load swapped for sp_slot_store, while validate_reloc_resolutions_spanned GAINED 2. A (file,line,shape) multiset diff of the two CI reports' scored files shares 3 of ~20 records. THE DISCRIMINATING EVIDENCE, four-way: - same host+toolchain A/B (rustc 1.96.1, witness 0.42.0): the instrument-side manifests of base and branch carry an IDENTICAL branch population for every scored function — 175 branches, per-function byte-for-byte (validate_ final_allocation_rv32 47 both sides, validate_served_image 5+1 both sides). No condition was deleted; none became unreachable. - cross-host, same source pair, same pinned versions: ubuntu 26/6 -> 21/3 (-5/-3) but macOS 17/7 -> 22/7 (+5/0). A source-caused deletion cannot change sign with the host. So: NOT (a) — no decision legitimately disappeared (the classifier is not in the scored population at all); NOT repo-side (b) — nothing became unreachable or gated; it is the CHECKER: witness's report-side decision RECONSTRUCTION (grouping branches into decisions) is a function of binary layout. Filed upstream with the artifacts: pulseengine/witness#208 (family #198/#179). THE GATE ACTION (stronger, not weaker): - NEW deletion-sensitive check on the surface the A/B proved stable: BRANCH_POPULATION pins the instrument-side branch count of all 20 scored functions EXACTLY (175 total; claims.yaml value-must-EQUAL spirit; REPIN block printed on mismatch, with the rule that an unmoved source means witness#208, not a repin). Negative control run: deleting one validate_served_image branch from a manifest copy reds the gate NAMING the function. - The reconstruction floors are RE-STATED from the #990 branch's own ubuntu measurement (21 dec / 3 full; conditions 139>=130, proved 62>=57, dead 48<=50 unchanged) with the full evidence written at the site — a re-statement WITH the discriminating measurement, not a floor lowered to go green: the new population pins are what now answers 'was anything real lost' when reconstruction moves again. - ci.yml uploads the manifest in mcdc-evidence: this diagnosis required the attribution map and the artifact did not carry it. If ubuntu's branch population differs from the macOS-derived pins, the gate prints the measured REPIN table — re-derive from that run's artifact (now uploaded) rather than guessing. Refs #990 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Aug 21, 2026
…s the wasm-mandated 0 — domination-precise zero-init classification, ARM + RV32 (#1016) * test(#990): RED-FIRST executed differential — br_if-skipped local write leaks poisoned stack on ARM AND RV32 Measured on 32c7e19 (unfixed v0.58 tree), unicorn vs wasmtime, every stack word below the entry SP poisoned 0xDEADBEEF: ARM (cortex-m4, --relocatable): 22/34, 9 explicit poison leaks RV32 (riscv32imac, --relocatable): 22/34, 9 explicit poison leaks The same 12 vectors fail on BOTH backends because the classifier is shared: `synth_synthesis::read_before_write_locals` walks the op stream in LINEAR order, so a `local.set` on a conditionally-skipped path (br_if / if-without- else / one br_table arm) suppresses the #457 zero-init even though it does not dominate the merge-point read. The skipping path returns previous-frame stack bytes — information disclosure, e.g.: BUG bl_brif(0xffffffff): want=0x00000000 got=0xdeadbeef <- POISON BUG bl_brif_i64(0xffffffff): want=0 got=0xdeadbeefdeadbeef (BOTH words) BUG bl_if_else_one_arm(0x1): want=0x00000007 got=0xdeadbef6 Guards all green on the unfixed tree (straight-line write-then-read, #457 read-before-write, both-arms write, same-block dominated write, #970's conditionally-written-param shape, loop accumulator) — the red is the class, not the harness. #970's own oracles: 38/38 ARM, 38/38 RV32 on this commit (baseline banked before the fix). Refs #990 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(#990): zero-init classification is now DOMINATION, not linear op order — a br_if-skipped local.set no longer suppresses the wasm-mandated zero (ARM + RV32) ROOT CAUSE. `synth_synthesis::read_before_write_locals` (the shared #457 zero-init classifier, driving BOTH the ARM select_with_stack prologue and the RV32 frame-slot zero-init) walked the op stream in LINEAR order: any `local.set`/`local.tee` seen before the first `local.get` suppressed the entry zero-init. A write on one arm of a `br_if` (or an `if` without else, or one `br_table` arm) precedes the merge-point read linearly while the branch jumps PAST it — the slot is never written on the skipping path, and the read returns previous-frame stack bytes. Information disclosure, executed and measured (0xDEADBEEF poison returned on both backends). Why #970/#457 did not rescue it: #970 fixed the PARAM half (count_params); access is the (conditional) WRITE, so the gate never fired. THE FIX. The classifier now tracks domination with a scope stack plus a branch-target pre-scan: a write dominates later ops in its own scope and nested scopes; at End the writes survive into the parent exactly when fall-through is the only way past them (untargeted block/if, loop bottom, if/else both-arms INTERSECTION). Precision is load-bearing, not cosmetic: the coarse discard-at-End draft emitted a zero-init that was a dead store in the same straight-line segment as the dominating store, and RV32's VCR-RA-003 holder model correctly REFUSED it (SpillSlotAliased on guard_same_block) — the validator stayed strict; the classifier got precise. Where the walk still over-approximates, zeroing a non-param local at entry is exactly wasm's mandated initial state (a false positive costs bytes, a false negative is #990). ORACLES (red-first differential landed in the previous commit at 22/34 per backend, 9 poison leaks each): - brif_local_zeroinit_990_arm_differential.py: 22/34 -> 34/34, 0 leaks - brif_local_zeroinit_990_riscv_differential.py: 22/34 -> 34/34, 0 leaks - cond_write_param_970_{arm,riscv}: 38/38 BOTH before AND after (the #970 param half is not regressed; banked baselines before touching the code) - arm_corpus_sweep_973.py: PASS — provenance_branches_396.wat:decide now matches wasmtime, its KNOWN_ARM_MISMATCHES ratchet line DELETED (the both-direction contract); only the sibling lane's 4 #989 entries remain - frozen_codegen_bytes: 10/10 anchors byte-IDENTICAL (no frozen fixture carries the conditional-write shape) - gust_spill_fwd_390_differential.py: PASS on the new gust_poll bytes (return + post-call state struct vs wasmtime, default + both lever opt-outs) BYTE DELTA, banked deliberately: gust_poll 696 -> 700 (+4). Capstone diff shows the ONLY content change is the prologue zero-init `movs r2,#0; str.w r2,[sp,#0x24]` for gust_poll's conditionally-written local; the rest is branch renumbering. size_attribution_390 repinned + report regenerated. cargo test --workspace: 146 suites, all green after the repin (the one red was the size gate doing its job). LEDGER: claims.yaml selector ratchets moved (+157 code lines, +1 wildcard arm net) — waivers with reasons in the same PR per the RQ-58-METRIC contract; status.json regenerated; oracle wiring check green (new job brif-local-zeroinit-990-oracle mirrors the #970 two-leg precedent). Refs #990 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * chore(#990): rebase onto RQ-59-WARALIAS — re-derive the composed ratchet, don't inherit either branch's #1015 (RQ-59-WARALIAS, #989) landed first and both lanes touch ARM local handling, so this rebase had three conflicts. Resolved by re-deriving from the MERGED tree rather than picking a side: 1. `scripts/repro/arm_corpus_sweep_973.py` — #1015 deleted the four KNOWN_ARM_MISMATCHES entries tagged 989 (its own ratchet, now fixed); this branch still carried them from the older base. Took the deletion. Verified by COUNTING what should remain: 0 entries tagged 989, the single 990 entry intact, 0 leftover conflict markers. (`git checkout --theirs` takes the WHOLE FILE and has silently deleted a lane's implementation before — counting the symbols is the check that catches it.) 2. `claims.yaml` ratchet values — THE STALE-BASE COMPOSE TRAP. #989 measured 17,961 -> 18,134 (+173); #990 measured 17,961 -> 18,118 (+157). Both correct against the v0.58 base, NEITHER correct once both land. Re-derived on the merged tree: 17,961 + 173 + 157 = 18,291 code / 28,912 total, and the deltas compose exactly. Also selector_wildcard_arms 56/91. 3. `artifacts/status.json` — generated; regenerated with --emit-status. THE GATE CAUGHT THE COMPOSE CASE, which is the point of it. Each lane had waived its OWN value, but a waiver is bound to its value, so two waived growths do not silently authorise their sum — the ratchet went red on 18,291 with NO waiver until one was written naming both lanes. That is the mechanism working: per-growth permission, never standing. Verified on the merged tree, exit codes captured directly: rustc 1.98.0 clippy -D warnings: 0 cargo test --workspace: 0 (146 result blocks, 0 failed) claim_check.py: 49/49 model_coverage_audit.py --check: 0 Refs #990, #989, #242. * fix(#990): remove the KNOWN_ARM_MISMATCHES entry this PR fixes — my rebase restored it MY CONFLICT-RESOLUTION ERROR, caught by the ratchet's other direction. Rebasing onto #1015 conflicted in this file: #1015 had deleted its four entries tagged 989, this branch's older base still carried them. I resolved by taking HEAD's deletion — correct for the 989 entries — and then 'verified what should remain' against the WRONG expectation, keeping the 990 entry that this PR's own fix retires. The gate is bidirectional and said so exactly: FAIL PHASE B RATCHET: provenance_branches_396.wat:decide is on KNOWN_ARM_MISMATCHES (#990) but produced NO mismatch this run — either it was fixed (remove the entry) That is the ratchet working in the direction that is easy to forget: it refuses a stale entry claiming a defect that no longer reproduces, not just a new mismatch. Counting what should remain only helps when the expected count is right; here the correct expectation was ZERO entries for both issues, because both are now fixed on this branch. Sweep after removal: compiled 147/159, executed 2490/2490, mismatches 0, PASS. Refs #990. * gate(#990): MC/DC red diagnosed — witness#208 layout-sensitive reconstruction, not a lost condition; pin the STABLE branch population, re-state the reconstruction floors with the evidence THE DIAGNOSIS (coordinator asked for the inventory, not the counts). The #990 fix added ~100 lines of UNSCORED code (the zero-init classifier) to a crate linked into the MC/DC harness wasm. Zero scored-function source changed, the 56 rows unchanged — yet CI's scored table went 26 dec/6 full -> 21/3: validate_final_allocation_rv32 7->4, validate_served_image 2->0, count_params_heuristic::{closure} 1->0, validate_reloc_resolutions 2->1 (its full-MC/DC credit is one of the two lost; build_options' the other), sp_slot_load swapped for sp_slot_store, while validate_reloc_resolutions_spanned GAINED 2. A (file,line,shape) multiset diff of the two CI reports' scored files shares 3 of ~20 records. THE DISCRIMINATING EVIDENCE, four-way: - same host+toolchain A/B (rustc 1.96.1, witness 0.42.0): the instrument-side manifests of base and branch carry an IDENTICAL branch population for every scored function — 175 branches, per-function byte-for-byte (validate_ final_allocation_rv32 47 both sides, validate_served_image 5+1 both sides). No condition was deleted; none became unreachable. - cross-host, same source pair, same pinned versions: ubuntu 26/6 -> 21/3 (-5/-3) but macOS 17/7 -> 22/7 (+5/0). A source-caused deletion cannot change sign with the host. So: NOT (a) — no decision legitimately disappeared (the classifier is not in the scored population at all); NOT repo-side (b) — nothing became unreachable or gated; it is the CHECKER: witness's report-side decision RECONSTRUCTION (grouping branches into decisions) is a function of binary layout. Filed upstream with the artifacts: pulseengine/witness#208 (family #198/#179). THE GATE ACTION (stronger, not weaker): - NEW deletion-sensitive check on the surface the A/B proved stable: BRANCH_POPULATION pins the instrument-side branch count of all 20 scored functions EXACTLY (175 total; claims.yaml value-must-EQUAL spirit; REPIN block printed on mismatch, with the rule that an unmoved source means witness#208, not a repin). Negative control run: deleting one validate_served_image branch from a manifest copy reds the gate NAMING the function. - The reconstruction floors are RE-STATED from the #990 branch's own ubuntu measurement (21 dec / 3 full; conditions 139>=130, proved 62>=57, dead 48<=50 unchanged) with the full evidence written at the site — a re-statement WITH the discriminating measurement, not a floor lowered to go green: the new population pins are what now answers 'was anything real lost' when reconstruction moves again. - ci.yml uploads the manifest in mcdc-evidence: this diagnosis required the attribution map and the artifact did not carry it. If ubuntu's branch population differs from the macOS-derived pins, the gate prints the measured REPIN table — re-derive from that run's artifact (now uploaded) rather than guessing. Refs #990 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * test(#990): committed potency tests for the BRANCH_POPULATION checker — a new checker born of a checker defect ships with its own negative controls The coordinator's point is the repo's own standard (claims.yaml on the RQ-58-METRIC ratchet, enforced by scripts/test_claim_check.py): a new checker whose only validation is a demonstration run once in the PR that added it is the next entry on the checkers-are-the-defects list. scripts/test_mcdc_gate.py drives the REAL gate end-to-end on synthetic (manifest, report) fixtures — witness never runs — generated consistently from one population map so the report-side floors hold in every case and a mutated population is the ONLY thing that can red the gate (clean failure attribution): RED, each naming the function: - dropped branch (THE deletion case): validate_served_image 5->4 -> 'branch population moved: ... = 4 (pinned 5)' - grown branch (added condition needs rows): count_params_heuristic 5->6 - UNPINNED scored function appearing in the manifest - mismatch emits the REPIN block WITH its guard sentence ('witness#208, not a repin') and in paste-able pin-table syntax — the sentence standing between the block and someone pasting it to go green is now asserted verbatim, so a refactor cannot silently drop it GREEN (a gate that only ever fails is as useless as one that only passes): - populations exactly matching pins -> exit 0 - branches in UNSCORED functions (the witness#208 layout-noise population) are ignored — a dep bump must not red the population check Wired into the mcdc CI job next to the row-driver sanity gate. 6/6 locally. Refs #990 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
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.
Summary
Closes #171 — the real i64 register-pair spill. i64-heavy functions exceeding the 5 consecutive register pairs hit "no consecutive pair" exhaustion and were dropped by the #168 skip net. #188's caller-saved preservation added pressure that regressed
z_impl_k_sem_givefrom compiling (v0.11.6) to skipped (v0.11.8). This implements the spill so they compile.Design
Vec<Reg>→Vec<StackVal>(Reg | Spilled { lo_slot });stack_live_regscounts only register-resident entries (~200 sites converted, every handler's logic preserved).alloc_consecutive_pairspills the deepest register-resident entry to a frame slot (STR lo/hi) when no pair is free, then retries;pop_operand/peek_operandreload a spilled value into a fresh pair (LDR lo/hi) on consume.LocalLayoutreserves an 8-slot i64 spill area (i64_spill_base) only when the function has i64 ops (i32-only frames unchanged); slots reused.restore_caller_savedspills the call result to the frame (returnsSpilled) when no callee-saved reg is free;emit_arg_movesacquires its cycle-break scratch lazily (only a genuine cycle needs it).Verification
Err), asserts STR/LDR frame traffic.Note
Three background agents failed on this all-or-nothing refactor (each crashed mid-pass leaving the i64-critical selector non-compiling); it was completed directly. The related #197 (the optimized path doesn't preserve caller-saved across import calls — gale's
z_impluses that path) is a distinct fix tracked separately.Closes #171.
🤖 Generated with Claude Code