feat(vcr-ra): spill on register exhaustion — remove the optimized-path hard-fail (#242, VCR-RA-001) by avrabe · Pull Request #580 · pulseengine/synth

avrabe · 2026-07-02T18:21:06Z

The hard-fail history

The optimized path (ir_to_arm) hard-failed on register exhaustion: #496 made alloc_i32_scratch / alloc_i64_pair flag pool exhaustion and decline the whole function to the direct selector — the honest fix that replaced the silent R12-borrow miscompile (R12/IP is the encoder's indexed-load scratch, #212). Honest, but it meant any function exceeding the R4-R8 pool never got the optimized path's benefits — the literal VCR-RA-001 "remove the register-exhaustion hard-fail" claim stayed open.

Why exhaustion hard-failed despite existing spill support: the spill machinery in ir_to_arm was dead flag-off — the Const handler could evict-and-spill, but any pressure that triggers eviction also exhausts the (smaller) scratch pool, which set the decline flag and discarded the body. The reload half was also unsound for real pressure (both operands of one op reload into R12; most handlers never reload at all) — all masked by the decline.

Allocation-time Belady spill (flag: `SYNTH_SPILL_ON_EXHAUST`, default OFF)

A pre-step before each IR instruction (only when the flag is on AND every opcode in the function is modeled):

(a) reinstate spilled sources — reload each into a pool register (LDR rd, [SP,#slot]), put it back in vreg_to_arm, so get_arm_reg never returns the R12 placeholder;
(b) free a dest register — if the handler will allocate a fresh scratch and the pool is full, evict the live vreg with the farthest next use (Belady, linear next-use table over the IR; deterministic tie-breaks) via STR victim, [SP,#slot]. Victims always get a store (the function's final result is read by the epilogue, invisible to the linear table); the epilogue reloads a spilled final result straight into R0.

If no victim is evictable (everything pinned), the pre-step falls through and the #496 decline fires exactly as flag-off — the lever degrades to the status quo, never to a miscompile.

Also fixed under the flag (latent, unreachable flag-off because any spill implied a decline): the appended trailing return missed the ADD SP frame epilogue, and Const-handler exhaustion could hand out reserved R9/R10/R11 (globals base / memsize / base-CSE) or clobber R3 — the pre-step pre-frees a pool register for Const dests too, so its allocator never reaches those fallbacks.

Flag choice

A separate flag, not SYNTH_SPILL_REALLOC: that lever is a post-hoc rewrite of already-allocated code (byte-level, same function set), while this one changes which functions take the optimized path — entangling them would make the realloc flip judge a population change. The flip decision later covers both.

i64 scope (honest)

i64 pair exhaustion keeps declining even flag-on. i64 values are two separate vregs with a pair invariant the v1 spill model does not carry (#518 class); spill_on_exhaust_supported also excludes control flow (a back-edge invalidates the linear next-use table), calls, and non-param locals. One unsupported opcode keeps the whole function on the #496 decline.

Red→green

scripts/repro/spill_on_exhaust_242.wat — 10 param-derived i32 values simultaneously live (const-folding can't collapse them), non-commutative fold:

RED (flag-off): declines; SYNTH_RECOVERY_STATS=1 shows rung=spill (direct selector's ladder produced the code). Pinned by spill_on_exhaust_red_flag_off_declines_to_direct_spill_rung.
GREEN (flag-on): stays on the optimized path (no recovery rung fires), and spill_on_exhaust_242_differential.py matches wasmtime on all 8 vectors under unicorn (incl. vectors where params force asymmetric sub/xor results).

Unit tests: #496 decline pinned; balance invariant (every LDR [SP,#x] preceded by a STR [SP,#x]); no R12 ships flag-on; Belady first victim is the farthest-next-use register (R8), not LRU's oldest (R4); below the pressure edge the lever is a byte-level no-op; scope classifier pinned.

Flag-off proof (STOP condition)

68/68 corpus fixtures byte-identical (full-ELF sha256) vs a main-built (bad0901) binary — both self-contained and --relocatable.
frozen_codegen_bytes 3/3, const-CSE golden, recovery_stats_242, promotion_exhaustion_fallback_474 all green.
cargo test -p synth-synthesis -p synth-cli fully green; cargo fmt --check and cargo clippy -p synth-synthesis -p synth-cli --all-targets -- -D warnings clean.

Flag-on validation

flight_seam_differential.py: seam 0x07FDF307 MATCH.
const_cse_differential.py: PASS (with the flag on top).
r12_spill_496_differential.py (control_step + flight_seam_flat, self-contained): PASS both flag states.
New fixture differential: PASS.
Corpus: 68/68 compile flag-on (zero failures). Ten corpus functions move off recovery rungs onto the optimized path; execution-checked vs wasmtime under unicorn flag-on: high_pressure_i32, filter_axis (.wat+.wasm), signed_div_const, uxth_fold, const_cse_direct, const_cse — all PASS. Residual: gust_kernel (1 of 5 fns moved) is compile-validated only here — its gust_poll needs a globals-base (R9) harness that fails identically flag-off, so no regression evidence; it's gale's silicon fixture family and the flip gate covers it.

Size (honest)

The newly-optimized fixture is larger on the optimized path today: hp = 216 B flag-on vs 98 B on the direct path (flag-off). The greedy linear allocator never frees dead vregs' registers, so at the pressure edge nearly every op evicts (STR/LDR churn). The win of this PR is removing the hard-fail class and keeping such functions on the optimized path where the downstream levers (range-realloc, const-CSE, spill-realloc forwarding/DCE #569/#576/#579) apply — dead-vreg pool release and slot reuse are the follow-on size levers before any flip.

Found while testing (pre-existing, NOT touched here)

The direct selector's spill rung miscompiles this fixture's shape: mul.w r2,r0,r1 clobbers a live spill candidate and a later ldr r0,[sp,#8] reads a slot never stored (disasm of the flag-off build, both --relocatable and self-contained). Flag-off vectors like hp(1,2) return 0xffffd1ce vs wasmtime's 0x2e37. That's instruction_selector.rs (out of scope per this PR's charter) — will file separately with the fixture as repro.

🤖 Generated with Claude Code

…h hard-fail (#242, VCR-RA-001) The optimized path (ir_to_arm) declined every function whose R4-R8 scratch pool exhausted (#496 — the honest fix that replaced the R12-borrow miscompile). Behind SYNTH_SPILL_ON_EXHAUST=1 (default off), a pre-step now spills at ALLOCATION time instead: when the pool is full, the live vreg with the FARTHEST next use (Belady, linear next-use table over the IR) is STRed to a fresh frame slot and its register reused; spilled sources are reloaded into pool registers at their next use (never the flag-off R12 placeholder, which cannot carry two operands and collides with the encoder's IP scratch). Scope (v1, honest): straight-line i32-only functions — no i64 pairs (alloc_i64_pair exhaustion keeps declining), no control flow (a back-edge would invalidate the linear next-use table), no calls, no non-param locals. One unsupported opcode keeps the whole function on the #496 decline. Also fixed under the flag (latent, unreachable flag-off because any spill implied a decline): the appended trailing return missed the ADD SP epilogue, and Const-handler exhaustion could hand out reserved R9/R10/R11 or clobber R3 — the pre-step now pre-frees a pool register for Const dests too. Red→green: scripts/repro/spill_on_exhaust_242.wat (10 param-derived live values) declines flag-off (rung=spill) and compiles on the optimized path flag-on, matching wasmtime on all vectors under unicorn (spill_on_exhaust_242_differential.py). Flag-off proof: 68/68 corpus fixtures byte-identical (full-ELF sha256) vs a main-built binary, both self-contained and --relocatable; frozen bytes 3/3; const-CSE golden green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

codecov · 2026-07-02T18:25:16Z

Codecov Report

❌ Patch coverage is 82.48473% with 86 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-synthesis/src/optimizer_bridge.rs	82.48%	86 Missing ⚠️

📢 Thoughts on this report? Let us know!

…r-stored slot (#581) (#582) The direct selector's #253 add/sub (and bitwise/addr) immediate folds delete the const materialization BY source_line. Under the spill-on-exhaustion retry rung (VCR-RA-001 3b-lite), alloc_temp_or_spill for the const's temp first emits the victim's spill store `STR rX,[sp,#slot]` tagged with the SAME source_line — the fold deleted the store along with the MOVW, leaving the victim's vstack entry marked Spilled with no store. Its later reload read a never-written frame slot: silent wrong value on the shipped --relocatable path (spill_on_exhaust_242.wat hp(1,2) = 0xffffd1ce vs wasmtime 0x2e37). Fix: `is_const_materialization` (MOVW/MOVT/MVN) filters every by-source_line drop — drop_prev_const_materialization, splice_out_addr_const_materialization, and the #209 reciprocal-mult dead-divisor retain — so spill stores survive any fold. Defensive `assert_spill_reloads_have_stores` at the end of select_with_stack (internal-bug panic pattern): a reload from the reserved spill area without a preceding store to that slot can no longer leave the selector silently. Gates: new scripts/repro/spill_rung_581_differential.py (minimal fold-shape fixture + the original #580 discovery fixture, unicorn vs wasmtime, direct path) red on main → 12/12 green; unit fold_preserves_spill_store_581; frozen 3/3 bit-identical; r12_spill_496 + AAPCS oracles green; cargo test -p synth-synthesis -p synth-cli green; clippy -D warnings clean. Closes #581 Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

… Belady spilling default-on (#585) Caps the four-lane arc: slot liveness (#579), exhaustion spill (#580), spill-rung fix (#582), SYNTH_SPILL_REALLOC flip + refreeze (#583). VCR-RA-001 -> verified; rivet release status v0.24.0: cuttable. Pin sweep + lock + CHANGELOG. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

…emainder (#587, #242) (#589) Extend the SYNTH_SPILL_ON_EXHAUST pre-step (#580) from i32 singles to i64 register PAIRS on the optimized path. When an even-aligned pair allocation would fail, the pre-step evicts either (a) a coherent live PAIR or (b) two independent singles freeing a legal even pair — choosing the candidate whose displaced values have the farthest soonest-next-use (pair-aware Belady), deterministic tie-breaks by fixed candidate order. Pair victims get 8-byte-aligned slot couples (lo at off, hi at off+4 — the #171/#325 direct-path convention) and reload as coherent pairs into any legal even pair at next use; a spilled final i64 result reloads straight into R0:R1 in the epilogue. If no sound eviction exists the function falls through to the existing #496 decline — loud skip, never wrong code. Scope stays honest: only the modeled i64 subset is admitted (const/load-param/ add/sub/and/or/xor/mul, comparisons+eqz, i32<->i64 conversions); shifts/ rotates (encoders clobber the amount pair in place), div/rem, clz/ctz/popcnt, non-param i64 locals, and i64+globals/memory.size mixing (R9/R10 conventions collide with the (R8,R9)/(R10,R11) candidates) keep declining. The candidate list is shared with alloc_i64_pair via SPILL_I64_PAIR_CANDIDATES so evictor and allocator cannot drift. Red -> green: scripts/repro/i64_pair_exhaust_587.wat (5 simultaneously-live i64s over 4 candidate pairs) declined on BOTH flag states at v0.24.0; now flag-on it stays on the optimized path (no recovery rung) and matches wasmtime under unicorn on all 8 vectors (flag-off decline pinned + still matches via the direct selector). Flag-off ELF is byte-identical to the pre-change baseline; frozen_codegen_bytes (incl. escape hatches), const_cse golden, spill_on_exhaust_242 (i32) and i64_param_518 differentials all pass. Flag stays default-OFF pending gale silicon, per the #587 triage. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

…reverses (#242) (#659) The North-Star program's falsification test, attempted and measured (evidence: scripts/repro/vcr_ver_001_gate.md): 1. The v0.11.20 reciprocal-mult cost-gate — load-bearing when added (v0.11.19 hard-failed control_step's 4x const div_u) — was DELETED outright in PR #322 once the #320 spill retry covered its case: full differential bit-identical, cycles trivially equal, no new cost-gate since. The roadmap's pass-criteria met literally; the artifact goes proposed -> implemented. 2. The #496 register-exhaustion hard-decline is REVERTABLE behind SYNTH_SPILL_ON_EXHAUST (#580, default off = fix stays): - red case green: r12_spill_496 differential PASS flag-on (incl. the 0x00210A55 / 0x07FDF307 silicon anchors); all five pressure differentials PASS on the reversal bytes - frozen pinned goldens 10/10 in BOTH flag states; the three result anchors' default-path bytes are byte-identical flag-on (new lock: vcr_ver_001_gate_242.rs); declines 14 -> 8 across the corpus - HONEST HOLD: weighted cycle proxy regresses on i32 shapes (+30.4% spill_on_exhaust_242, +32.4% spill_rung_581, +8.0% high_pressure_i32, +120% signed_div_const 34->76 B; i64 shapes improve -5.5%/-1.4%) — the decline remains load-bearing FOR CYCLES, not correctness. Missing capability named: post-exhaustion code quality on the optimized path (allocation-time spill placement/coalescing). The default-on flip stays a separate later PR (#580 silicon hold). Flag-off this change is docs + roadmap + one additive test: no codegen bytes move; frozen gate green; goldens NOT re-pinned. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

…nst-div guards (#242, the PR #659 verdict) (#672) PR #659 held the SYNTH_SPILL_ON_EXHAUST flip on a measured i32-shape cycle regression and named the missing capability: post-exhaustion code quality on the optimized path. Root cause of the unreached allocation-time Belady slots: - fresh-monotonic slots defeat the overwrite-only frame-slot DCE (#515); - the eviction store's source is redefined immediately, defeating forward_stack_reloads; - spill_rechoice's rename deadness proof is segment-local — R2/R3 are never touched again on bridge streams, so "possibly live-out" declined them, and exact SegmentTrace equality rejected any fresh-register rename; - signed_div_const additionally paid for const-divisor trap guards the direct selector elides (#209 Opt 1a). Extensions, ALL scoped to functions the #580 machinery actually shaped (OptimizerBridge::spill_on_exhaust_fired — flag-on leaves every untouched function byte-identical, locked by vcr_ver_001_gate_242 + frozen 10/10 run in both flag states; flag-off is bit-for-bit the shipping pipeline): - scratch_dead_at: function-level R2/R3 exit-deadness (conservative at any branch/call/unmodeled op) feeding rename_kill_def; trace equality modulo provably-dead exit entries; per-pair pressure commit; byte-shrinking count-neutral folds admitted; - constant rematerialization of spilled single-instruction consts in spill_forward_segment (movt RMW kills the shape — the #582 discipline); - bounded fixpoint of the cleanup triple + late elide_dead_frame; - terminal-segment relaxed live-out pinning in range-realloc (only R0/R1 observable past bx lr pre-prologue; VCR-RA-003 validator run with the same exemptions; reload-free segments only); - const-divisor trap-guard elision in DivS/DivU/RemS/RemU (single-def Const scan, total-or-disabled def enumeration; c=0 keeps all, DivS c=-1 keeps the overflow guard). Cycle proxy (scripts/repro/postex_cycle_proxy.py, wasmtime-matched): spill_on_exhaust_242 +30.4%→+17.4%, spill_rung_581 +32.4%→+8.8%, high_pressure_i32 +8.0%→−24.0%, signed_div_const +120%→−33.3%, i64 pair/pool −16.4%/−2.9%. Two fixtures still miss ≤+5%: the residual is alloc_i32_scratch's fixed R4-R8 dest pool vs the direct selector's nine registers — the Track-A allocator replacement itself (see the gate doc's "residual, named" section; a reload-pool widening was tried and reverted, measured strictly worse). The flip stays HELD (#580). Gates: cargo test --workspace green; frozen anchors 10/10 + gate lock in BOTH flag states; r12_spill_496 / spill_on_exhaust_242 / i64_pair_exhaust_587 / i64_spill_pool_587 / spill_rung_581 differentials PASS flag-on; fmt + clippy -D warnings clean. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

…d mask profile Two defects in the #374 memory.copy/memory.fill lowering (select_with_stack), one lane: (dst/src as walking loop pointers, len as the byte buffer). LocalGet of a register-homed local (AAPCS param r0-r3, promoted local r4-r8) pushes the HOME register itself, so a local reused AFTER the op read a wild mem_base+cursor pointer or the last byte copied. Fix, mirroring the #193 reservation discipline: `bulk_mutable_operand` copies a popped operand into a fresh scratch before mutation when it is still live (live param/promoted home, duplicate vstack entry, if/block result reg, or aliased to another popped operand of the same op); a provably-dead temp is used in place, keeping the const-operand shapes byte-identical (#374 differential still 16/16). The red differential also exposed the #663-class range-realloc hole the fix then tripped over: `try_reallocate_segment` treated a pool register with NO range in a segment as free, but such a register can be LIVE-THROUGH (a param home the segment never touches — the memcpy backward path recolored its walking-pointer intermediate onto R0, the still-live dst local). Absent pool colours are now blocked with synthetic pinned interference nodes; identity colouring within the segment's present registers always exists, so no recoloring the original bytes had is lost (frozen anchors stay 10/10 bit-identical). Relaxed-exit terminal segments keep the #580 exemptions (only absent R0/R1 blocked past the bx lr). was emitted byte-identical to `none` while safety-manifest.json still attested "mask" (attestation-integrity hole). The lowering now applies the scalar #651/#654 mask_effective_address wrap-not-trap discipline: dst and src effective addresses fold with AND (size-1) and len clamps to size-dst / size-src so the FINAL byte stays in bounds — every loop access lands in [0, size), wasm-in-bounds ops are unchanged, and the manifest's mask claim is now backed by the emission (mask ≢ none proven by the pure-bulk byte-diff gate). Oracles (all run locally, red on v0.37.1 → green here): - scripts/repro/bulk_local_clobber_677_differential.py — 2/8 → 8/8 vs wasmtime under unicorn (dst/src/len reuse + const control). - scripts/repro/bulk_mask_679_differential.py — pure-bulk byte-diff (identical → differs), manifest coherence, escape/fold/clamp vectors with R10=4096 and out-of-bound containment (raw escaped writes → contained). - scripts/repro/bulk_memory_374_differential.py — 16/16 (unchanged shapes byte-identical; script gains SYNTH env override). - frozen_codegen_bytes 10/10; safety_bounds_377 13/13+13/13; unreachable_665, i32_shift_mask_682 PASS; cargo test --workspace green; fmt + clippy -D clean. - 8 new selector unit tests (677 preservation/aliasing/no-copy-when-dead, 679 fold+clamp presence, mask≠none structural). Both oracles are CI-wired in the trap-semantics job (#489 discipline). Closes #677. Closes #679. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…copy/fill (#695) * fix(bulk-memory): #677 operand-register clobber + #679 silent-unmasked mask profile Two defects in the #374 memory.copy/memory.fill lowering (select_with_stack), one lane: (dst/src as walking loop pointers, len as the byte buffer). LocalGet of a register-homed local (AAPCS param r0-r3, promoted local r4-r8) pushes the HOME register itself, so a local reused AFTER the op read a wild mem_base+cursor pointer or the last byte copied. Fix, mirroring the #193 reservation discipline: `bulk_mutable_operand` copies a popped operand into a fresh scratch before mutation when it is still live (live param/promoted home, duplicate vstack entry, if/block result reg, or aliased to another popped operand of the same op); a provably-dead temp is used in place, keeping the const-operand shapes byte-identical (#374 differential still 16/16). The red differential also exposed the #663-class range-realloc hole the fix then tripped over: `try_reallocate_segment` treated a pool register with NO range in a segment as free, but such a register can be LIVE-THROUGH (a param home the segment never touches — the memcpy backward path recolored its walking-pointer intermediate onto R0, the still-live dst local). Absent pool colours are now blocked with synthetic pinned interference nodes; identity colouring within the segment's present registers always exists, so no recoloring the original bytes had is lost (frozen anchors stay 10/10 bit-identical). Relaxed-exit terminal segments keep the #580 exemptions (only absent R0/R1 blocked past the bx lr). was emitted byte-identical to `none` while safety-manifest.json still attested "mask" (attestation-integrity hole). The lowering now applies the scalar #651/#654 mask_effective_address wrap-not-trap discipline: dst and src effective addresses fold with AND (size-1) and len clamps to size-dst / size-src so the FINAL byte stays in bounds — every loop access lands in [0, size), wasm-in-bounds ops are unchanged, and the manifest's mask claim is now backed by the emission (mask ≢ none proven by the pure-bulk byte-diff gate). Oracles (all run locally, red on v0.37.1 → green here): - scripts/repro/bulk_local_clobber_677_differential.py — 2/8 → 8/8 vs wasmtime under unicorn (dst/src/len reuse + const control). - scripts/repro/bulk_mask_679_differential.py — pure-bulk byte-diff (identical → differs), manifest coherence, escape/fold/clamp vectors with R10=4096 and out-of-bound containment (raw escaped writes → contained). - scripts/repro/bulk_memory_374_differential.py — 16/16 (unchanged shapes byte-identical; script gains SYNTH env override). - frozen_codegen_bytes 10/10; safety_bounds_377 13/13+13/13; unreachable_665, i32_shift_mask_682 PASS; cargo test --workspace green; fmt + clippy -D clean. - 8 new selector unit tests (677 preservation/aliasing/no-copy-when-dead, 679 fold+clamp presence, mask≠none structural). Both oracles are CI-wired in the trap-semantics job (#489 discipline). Closes #677. Closes #679. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * fix: clippy values_mut + harness reads symtab by SHT_SYMTAB type (#489 pattern) - liveness.rs: iter_mut over map → values_mut (rust-1.97 clippy). - The two #677/#679 differential harnesses read .symtab via get_section_by_name, which returns None because synth emits an unnamed SHT_SYMTAB section; switched to iterate by sh_type (the established #489 pattern all other harnesses use). Both oracles PASS locally. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

…all corrected An independent fresh-context pass verified every checkable claim in the CHANGELOG's v0.78 section, all ten artifacts and the six commit messages by RUNNING the refuting command rather than reasoning about plausibility. Ten were false. The conduct question came back clean, and that half was verified in detail rather than asserted (below). THE BEST CATCH — THE RELEASE'S OWN TWO NUMBERS REFUTED EACH OTHER. "The last compiling case moved from 58 to 64 locals" appeared in the CHANGELOG, in WIDEFILE, in PINDEBT6 and in commit f1348d7. But the same artifact says "n=60 emitted 1956 bytes against n=59's 2040" ONE CLAUSE LATER — and n=59's 2040 bytes is a figure from the SHIPPED tree, so 59 compiles and the wall is at 60. The committed test's own docstring already said "the wall for the family moves from 60 to 72". THE CODE WAS RIGHT AND THE PROSE WAS WRONG. The reviewer built an out-of-tree crate with path deps, copied `wide_f32_ops` and `m7dp_config` verbatim, and ran the shipped ladder: 57/58/59 OK at 1968/2004/2040 bytes, 60 and beyond DECLINE. Restated everywhere as the WALL moving 60 -> 72, with 59-compiles-today named so the two figures can no longer disagree. "To 64" was the same defect at the other end: 64 is the largest point tested, not the new wall, which the artifact itself puts at 72. 38 WAS THE WRONG DENOMINATOR. "38 `SYNTH_*` reads in shipped code" — 38 is the FLAG count; there are 61 read sites across them, 6 flags read at more than one site. The census's own output says "38 SYNTH_* flags", and the next clause ("Four are capabilities") only parses over flags. Corrected to name both numbers. A PROVENANCE CITATION POINTING AT AN UNREACHABLE COMMIT. FEATURESET said "MEASURED at this cut, at commit `8f564ad8`". `git merge-base --is-ancestor 8f564ad HEAD` says NO and `git branch -a --contains` is empty: it is the orphaned pre-rename cost-model commit, stranded when its subject was amended off an artifact id — a rename this release made deliberately, for status_evidence R4. The citation exists PRECISELY to supply provenance for a number derived from files the release edits, and it named a commit belonging to a different lane that no longer exists. Now `fac5b463`, verified reachable. A citation that looks checkable and is not is worse than none. THE 5 -> 4 CORRECTION DID NOT PROPAGATE. Commit 078cd88 corrected the headline from five hidden capabilities to four, and three clauses kept the old figure: FEATURESET's held-open comment and its closing paragraph ("three of the five"), and BLOCKERCLASS's "five capabilities ship flag-off". The CHANGELOG had it right at "two of the four", so an artifact disagreed with the notes that summarise it. The breakdown is now stated so it sums: two say only "evidence-gated", one is gated on #494's phasing, one on silicon (#580). 29,616 IS THE v0.57 FIGURE FOR A FILE THAT IS 19,905 LINES. It appeared in the artifact, in commit fac5b46 and in the SHIPPED SCRIPT'S OWN DOCSTRING, twice. `wc -l` is 19905 at HEAD and at v0.77.0; the family total is 30375. The `#[cfg(test)]` sits at line 308, so "1% / 99%" becomes line 308 / 98% — the argument survives, the number did not. AND THE "4 OF 128 FILES CUT EARLY" WAS 3 BY THE SENTENCE'S OWN CRITERION. Three files lose SHIPPED code to a first-marker cut (instruction_selector.rs, expansion_validator.rs, properties.rs). The fourth, optimizer_bridge.rs, merely has more than one `#[cfg(test)]` and its first is at 79.7%, losing nothing shipped. Counting it needs a different predicate than the one the sentence gives. A NARROW EXCEPTION GENERALISED INTO THE RULE. COSTMODEL's description said WCET bounds "are priced from the REAL ENCODER's own byte lengths (`straightline_expansion_real`), not from the estimator". The GENERAL path is `straightline_expansion` at wcet.rs:119, which calls `estimate_arm_byte_size` — the ESTIMATOR, as its own doc says. `straightline_expansion_real` at :142 is consulted from exactly ONE match arm (:342), the #936 i64 family. The soundness argument holds and is a different one: the estimator is pinned to the real encoder by `estimator_encoder_agreement`, which is why using it is provably >= the real cost — and why the same file can call it a "hand-maintained mirror" two paragraphs later without contradiction. Corrected in place, with the refutation recorded rather than the sentence quietly swapped. A LINE NUMBER THAT NAMED THE CONSULT SITE AS THE READ SITE. `optimizer_bridge.rs:3719` does not contain `SYNTH_SPILL_ON_EXHAUST`; the env read is at :784, which is where the census itself reports it, and :3719 is where the flag is consulted. The paired citation (instruction_selector.rs:9238) is exact, which made the mismatch read as equally exact. Both sites now named for what they are. THE CONDUCT QUESTION: NO VIOLATION, verified rather than assumed. Zero comments were posted to #1318 or #1426 by this release — #1318's 13 comments all predate every v0.78 commit, #1426 has none. #1426's `updatedAt` on release day is a BODY edit, not a thread post, and #1426 is authored by avrabe, not the reporter. It is 384 words about his build with no machinery, no ratchet content, no repo citation convention (that text lives in the source comment, not the issue) and no loop trailer. The shipped diagnostic cites the OPEN, correctly-titled #1426. Rule 4 is respected explicitly in three places. Gates: claim_check 75/75, status_evidence 0 failures (223 artifacts, 171 done-when, 72 archaeology checks, 0 skipped). Refs #1437, #1439, #1433, #242 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…e set — derive it, on both axes (#1438) * RQ-78-FEATURESET: derive which capabilities the delivered binary actually has The maintainer asked whether the binary we deliver is our full feature set, or whether capability is hiding behind flags. Answering it meant reading 128 source files, and three hand censuses gave three different answers: 15, then 9, then 5. This derives it. `scripts/shipped_feature_census.py` walks `crates/*/src/**/*.rs`, cuts each file at its `#[cfg(test)]` module, and classifies every `SYNTH_*` read by whether the CAPABILITY is reachable with the variable unset. MEASURED, at this commit: 38 flags in non-test code — 16 diagnostics (no emitted byte changes), 15 opt-outs that ship ON, and FIVE capabilities the delivered binary does not have: SYNTH_FACT_SPEC, SYNTH_GRAPH_ALLOC, SYNTH_RV_ADDR_FOLD, SYNTH_SHADOW_ALLOC, SYNTH_SPILL_ON_EXHAUST. Plus 2 modifiers of those. Zero undetermined. WHY THE HAND COUNTS DISAGREED, and it is one mechanism: the polarity of the BOOLEAN is not the polarity of the FEATURE. Two live sites in arm_backend.rs prove the boolean cannot be the answer — their booleans are OPPOSITE when unset and both capabilities ship ON: 857: let promote = var("SYNTH_NO_LOCAL_PROMOTE").is_err(); // true 1684: let islands_disabled = var_os("SYNTH_NO_LITPOOL_ISLANDS").is_some(); // false What closes the gap is the BINDING NAME, which says what the boolean means. So the rule is one line with no special cases: capability ships ON <=> (boolean when unset) XOR (binding name is negative) A first draft of this script special-cased `SYNTH_NO_*` by name instead, and its own self-test rejected it: keying on the prefix gets every `is_err` site backwards, and it would have been a hand-written mirror of a naming convention rather than a reading of the code. The prefix now carries no weight; the five `SYNTH_NO_*` flags classify correctly because of their BINDINGS. The negative control pins that — a `SYNTH_NO_*` flag that must be SET to enable ships OFF. The 5-vs-7 gap is derived too, not judged: a flag whose name strictly extends another READ flag's name modifies that flag rather than gating its own capability (`SYNTH_GRAPH_ALLOC_FORCE` -> `SYNTH_GRAPH_ALLOC`). Negative control: a `_FORCE` flag whose parent is read nowhere gates its own capability and counts as one. My own hand count of 5 had silently DROPPED these two; the derivation shows them. REFUSALS, so a green cannot be about the empty set or the wrong one: * glob matches nothing -> REFUSE (verified: 128 of 270 `.rs` under crates/ are shipped code; the other 142 are 135 tests, 6 examples, 1 bench, and the two flags read only out there are correctly absent); * zero SYNTH_ reads across a non-empty file set -> REFUSE; * any `crates/*/build.rs` reading a SYNTH_ var -> REFUSE, because a compile-time gate is invisible to a census of runtime reads and would make this script under-report the very thing it measures. Nothing does today. Gated with a POSITIVE control: the same temp tree without a build.rs must classify successfully, or the refusal proves nothing; * an unreadable expression is UNDETERMINED and counted separately, never bucketed as "not shipping off". The self-test is wired into the required Claim Check job with an ARITHMETIC assertion floor inside the script. `grep -qE '[0-9]+ assertions'` is a digit class, not a floor — it accepts zero, so it passes a self-test whose body stopped running. That is the #1435 defect this same job already fixed one layer up, and repeating it in a file about mechanical honesty would be poor. Proven potent both ways with the exit code read WITHOUT a pipe (a pipeline's rc is the last command's, which reported rc=0 over a real refusal on the first attempt): raising the floor reds, and deleting one real assertion reds at 24 < 25. Refs #1433 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * RQ-78-FEATURESET: the census was right by luck — fix the predicate, add axis 2 A cold read of the committed census found three blind spots, all of them in the gap between 25 self-test assertions over synthetic one-line strings and a census that runs over 128 real multi-line files. Two changed nothing about the answer and one would have. (1) THE TEST-MODULE CUT WAS A DOCUMENTED REPEAT. `non_test` truncated at the FIRST `#[cfg(test)]`, which is the v0.77 selector-classifier defect verbatim. Measured: 4 of 128 files cut early, and `instruction_selector.rs` carries a `#[cfg(test)] fn aapcs_param_regs` helper at 1% of its 29,616 lines — so the census discarded 99% of the shipped selector, plus two thirds each of `properties.rs` and `expansion_validator.rs`. NO FLAG WAS LOST at this commit, which is luck and not a predicate: the sole read after any cut (`SYNTH_SEL_DSL_REGEN`) happens to sit in a genuine `mod tests`. One env read added to the selector body would have vanished silently, and vanishing under-reports, which answers the maintainer's question reassuringly and wrongly. Each `#[cfg(test)]` ITEM is now removed by brace balance, line numbers preserved, with a scanner that is not fooled by a `{` inside a string literal. (2) THE BINDING WINDOW WAS FORWARD-ONLY, so rustfmt could flip a verdict. A `lines[i:i+3]` window starting at the read misses a binding wrapped onto the previous line — 13 reads in this tree, including `SYNTH_GRAPH_ALLOC`'s `fn enabled()` and `SYNTH_SPILL_ON_EXHAUST`'s `spill_on_exhaust_enabled`. The wrapped `islands_disabled` shape classifies OFF under a forward-only window and ON in fact. But naively widening BACKWARD is also wrong: two lines above `SYNTH_FUSE_STATS` sits an unrelated `let arm_instrs = ...` that a window adopts as the binding. The search is now scoped to the ENCLOSING STATEMENT, with both shapes pinned as assertions. (3) FIRST-READ-WINS had no agreement check — the `.position()`/`.rposition()` shape. Every read site is now classified and a disagreement REFUSES. Measured: 6 flags are read at more than one site and all 6 agree, so the previous output was correct; it was just unlicensed. THE REFUSAL ITSELF WAS DEAD CODE in the first attempt — `verdicts` was overwritten with a one-element set before its size was tested, so `len(verdicts) > 1` could never be true. Its own red-first fixture was ALSO wrong: it used `let off = ...`, and `off` is a negative binding word, so both sites classified ON and the fixture proved nothing. Both fixed, refusal now fires. AXIS 2 ADDED, because the ask said "hiding behind FEATURES" and in this repo that word also names Cargo features, which no census of runtime reads can see. TWO DIFFERENT BINARIES ARE DELIVERED and they do not carry the same set: `release.yml` builds `-p synth-cli --features verify`; `cargo install synth-cli` takes `default = ["riscv"]` only, so `synth verify` is NOT in the crates.io binary — it loud-declines with "Verification requested but not compiled into this binary", which is correct behaviour that nothing had recorded. `awsm` and `wasker` are in neither; `exports_only_275_probe` is in neither by design. AND THE FEATURE PARSER REPEATED THE CHARACTER-CLASS DEFECT A THIRD TIME. `[a-z][a-z0-9-]*` silently dropped `exports_only_275_probe` for its UNDERSCORES, exactly as `[a-z-]*` misses `synth-backend-aarch64` for its DIGITS and as `[4-9][0-9]*` is not a floor (#1435). A feature this misses reads as "not declared", which is indistinguishable from "not hidden". Widened, and the underscore name is pinned by name in an assertion. TWO BUCKETS RELABELLED for honesty. `DIAG` decides 14 of 38 flags by a regex over NAMES — that is a judgement, not a derivation, and it is now printed as its own bucket rather than folded into the derived counts (the RQ-77-CENSUS convention). And `SYNTH_ORDEAL_DEADLINE_MS` / `SYNTH_ORDEAL_MAX_CONFLICTS` were filed under a bucket label asserting "no emitted byte changes", which is false: `solver.rs` documents that setting the deadline to 0 "re-opens the #849 hang class", and a query that times out answers Unknown, so the budget decides what gets PROVEN and therefore which elisions are admitted. They are named as solver budgets instead. The answer on axis 1 is unchanged at 5 capabilities + 2 modifiers, now for the right reason. Self-test 25 -> 36 assertions, floor raised with it and re-proven potent by deleting one real assertion (35 < 36, rc=1 read without a pipe). Refs #1437 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * RQ-78-FEATURESET + BLOCKERCLASS/LADDER rescope: name what the binary lacks THE FEATURE-SET ARTIFACT records the two-axis census and the three wrong hand counts it replaced. Five capabilities ship flag-off; `synth verify` is absent from the crates.io binary though the GitHub release binary has it. #1437 is HELD OPEN via `issue-scope: outlives` — it carries three asks and this lane delivers one; asks 2 and 3 are maintainer decisions about whether each flip is scheduled and whether the crates.io feature set is intended. Closing on ask 1 would be the v0.71/v0.73 umbrella shape, and the gate those releases built caught it: before the `outlives`, status_evidence authorised #1437 for closure. BLOCKERCLASS WAS A `must` WHOSE PREDICATE COULD NOT BE EVALUATED. Its done-when required re-deriving the NEVER set "from RQ-78-LADDER's fresh ladder", and that ladder is blocked on an unmounted corpus — so the check could never run and would have read as merely undone. Rescoped to the half that is derivable, with the freshness half named as blocked. Its delivered half is a NAMING and a REFUTATION. The top ARM NEVER class is register exhaustion, 70 of 141 modules, half the reach headroom — labelled with its provenance (the RQ-64-HISTOGRAM re-attribution, #1159, v0.64, NOT a v0.78 measurement). And the inference that writes itself is refuted: RQ-78-FEATURESET found that two of the five flag-off capabilities are register-allocation capabilities, so "the fix for half the NEVER set is built and not shipped" is one sentence away — and I was one sentence from writing it. THE TWO "REGISTER EXHAUSTIONS" ARE DIFFERENT SITES. The 70-module decline is raised by `free_callee_saved` at `instruction_selector.rs:9238` over the five-register `CALLEE_SAVED_POOL` on the SELECTOR path. `SYNTH_SPILL_ON_EXHAUST` is consulted at `optimizer_bridge.rs:3719`, gating the OPTIMIZED path's VCR-RA-001 allocator spill (#496). Two files, two code paths, one shared NAME. Whether clearing the allocator's exhaustion prevents the selector's is UNTESTED and needs the corpus. That is this release's own theme landing on the release's PLAN rather than on a gate: a true-sounding sentence about the wrong subject. The obligation is now named — any future reach claim from either flag must show the SELECTOR's decline disappearing on named modules — and v0.63's recorded lesson bounds it independently: RQ-63-ARMI64OFF cleared a 46-module primary blocker and gained ZERO modules, so the honest ceiling on clearing the 70 is UNKNOWN, not 70. LADDER's delivered half is the PROVENANCE DEFECT that made the block so slow to diagnose. The header cited `corpora/wasm-243/MANIFEST.sha256` — a bare relative path that reads as repo-relative. It is not: `corpora/` is absent, tracked by zero files, and not even gitignored, and `partial_census_1017.py` took the corpus as a positional whose help said only ".wasm files or directories". The path the ladder cites was DEFINED NOWHERE IN THE TREE, and this lane was one command from publishing that the corpus was unobtainable. It is not lost, it is unmounted. Both ends now say so: the ladder header carries an explicit external-corpus note with the last known absolute path and the auth failure's date, and the script's `--help` says it where an operator reads it. THE REACH FLOOR IS DELIBERATELY NOT PINNED, and the artifact says so rather than omitting it. Pinning a floor would pin v0.63's figures; pinning a cost ceiling ALONE is the alternating the theme forbids, letting a release buy cost wins with reach losses and stay green. Neither half is pinned and the reason is recorded. Gates on this tree: status_evidence 0 failures (169 done-when predicates, anchor lag 0), claim_check 75/75, census self-test 36 assertions, partial_census self-test 14 assertions. Refs #1437, #1432, #242 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * v0.78 cost-model lane: the model exists, derives from the real encoder, and does not ship The premise SURVIVES its own refuting command — `grep -A1 'prices a 2-byte register copy' CLAUDE.md` still hits at line 168, so nothing has addressed the metric. But scoping the differential meant locating the metric, and locating it showed this lane was about to BUILD A COST MODEL THAT ALREADY EXISTS AND DOES NOT SHIP. THREE COST NOTIONS ON THE ARM PATH, located by file and line: 1. The SHIPPED spill decision prices no bytes at all. The victim is Belady next-use DISTANCE — `spill_evict_farthest` / `spill_evict_pair_farthest`, optimizer_bridge.rs:7522 and :7611, "farthest next use wins". Belady is not wrong; it is optimal for reload COUNT under a known future. It optimizes a different objective than emitted size, so on the byte axis every candidate is priced identically — a STRONGER statement than CLAUDE.md's "a 2-byte register copy and a 4-byte frame reload identically", and the honest one. 2. A byte-size function DOES exist on the shipped path — `estimate_arm_byte_size`, optimizer_bridge.rs:371 — but it serves BRANCH DISPLACEMENT, not allocation, and its own doc comment calls it "a *hand-maintained mirror* of the encoder": the #498 structural cause, and the pattern the North Star forbids. It exists because synth-synthesis cannot depend on synth-backend. 3. The REAL-encoder cost model exists and does not ship. graph_alloc.rs:583 prices each web as `enc(&instrs[*i].op) * weight` — the real encoder's own byte length times the loop weight — normalized `W / (span * degree)`. Behind SYNTH_GRAPH_ALLOC, default OFF. SO THE FINDING IS THE NORTH STAR'S OWN RULE ONE LAYER DOWN. "Derive what you check against from the artifact you ship": of three cost notions, the one that DERIVES from the shipped encoder is the one that is NOT shipped, and the one on the shipped path is a hand mirror serving a different purpose. The allocator that would consume the derived metric is the same flag-off capability RQ-78-FEATURESET derived — so this is not two lanes agreeing, it is one fact seen from two directions. And that the flag ships off is now DERIVED by a committed census whose self-test runs in the required Claim Check job, where the previous claim of this shape rested on prose. WHAT IS HELD BACK, because the adjacent overclaim is the one this release keeps catching: no claim that flipping SYNTH_GRAPH_ALLOC improves emitted code, and no claim that Belady causes any specific regression. RQ-59-MEASURE is cited as the premise's ground, not re-derived. A differential over shapes I construct locally would measure the shapes I chose — the wrong-subject class this release is named after — and the measurement that settles it needs the blocked corpus. THE COST CEILING IS DELIBERATELY NOT PINNED. The done-when required it "paired with RQ-78-LADDER's reach floor so neither can be bought with the other". That floor cannot be pinned — its corpus is unmounted — and pinning the ceiling ALONE is the alternating the theme forbids: a release could buy cost wins with reach losses and stay green. Shipping the reachable half would have inverted the pin's purpose. Refs #1433 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * RQ-78-FEATURESET: the count was FIVE and the answer is FOUR — an OVER-report Every other error in this lane under-reported. This one runs the other way, which is its own kind of wrong: it inflated the answer to the maintainer's question in the alarming direction. `SYNTH_SHADOW_ALLOC` is MEASURE-ONLY, not a capability the delivered binary lacks. Its own source says so at `crates/synth-backend/src/arm_backend.rs:2014` — "the measure-only bridge between the built analysis layer and the eventual virtual-register wiring ... off by default and side-effect-free either way" — and `:1954` groups it WITH the diagnostics: "Diagnostics inside (SYNTH_FUSE_STATS, SYNTH_SHADOW_ALLOC, SYNTH_SPILL_REPORT) ... never a byte change". Its guarded block holds three `eprintln!` and no mutation. It was filed as a capability because it is NAMED like one — no DEBUG/STATS/DUMP suffix for the `DIAG` name rule to catch. Being off is not missing capability for a flag that changes no emitted byte. The other four were re-checked against the source rather than left on the strength of one correction: `SYNTH_RV_ADDR_FOLD` calls `fold_const_addr(&mut ctx.out)` and demonstrably moves bytes; `SYNTH_GRAPH_ALLOC`'s own module header says "any code it emits is provably allocation-sound" and "with the flag unset the shipping path is byte-for-byte untouched"; `SYNTH_SPILL_ON_EXHAUST` converts a decline into a compile; `SYNTH_FACT_SPEC` elides guards. All four stand. Six buckets, 38 flags: 4 capabilities + 2 modifiers + 1 measure-only + 15 opt-outs + 2 solver budgets + 14 instrumentation. A DERIVED DISCRIMINATOR WAS TRIED AND REJECTED WITH ITS MEASUREMENT, recorded so it is not re-tried blind: score each flag's guarded block by print macros versus mutation markers and call a print-only block measure-only. It finds SHADOW_ALLOC — and ALSO flags SYNTH_GRAPH_ALLOC and SYNTH_GRAPH_ALLOC_FORCE, which are real capabilities, because their reads sit inside a tiny `fn enabled()` whose block is the boolean and not the capability's effect. TWO FALSE POSITIVES IN THREE HITS. This repo's ratchet documentation says a gate people cannot move honestly is a gate they route around, so it is not shipped; the classification is an explicit grounded list of one instead of a noisy rule. SO THE CENSUS NOW PRINTS ITS OWN LIMIT on every run rather than leaving it to be discovered: it DERIVES POLARITY — is the capability reachable with the variable unset — and that half is mechanical. Whether a flag CHANGES EMITTED BYTES is a SEPARATE question it decides BY NAME for 17 of 38 flags, and SYNTH_SHADOW_ALLOC is the standing proof that the name rule misses cases. The cost-model lane's commit subject is also renamed off its artifact id. A subject STARTING with an artifact id is a delivery claim to status_evidence R4 (first-parent on HEAD), and COSTMODEL is non-claiming — so an id-first subject asserted more than the artifact does. R4 caught it locally before the push, which is what running the battery first is for. Every previous non-claiming artifact points `landed:` at the release PR and carries no id-first commit; that is the convention. Gates re-run on this tree: claim_check 75/75, status_evidence 0 failures, check_version_pins OK, oracle_wiring OK, artifact_citation OK, stale_pin_check PASS, ci_pool_tripwire 0 failures, census self-test 39 assertions. No Rust touched. Refs #1437 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * RQ-78-WIDEFILE: the reach fix that would have shipped a silent miscompile The recovery ladder's LAST rung is the only one with no pool-grow retry, and giving it one cannot ship, because the wide-file path emits WRONG CODE. The oracle landed first and refused the increment, which is what the gating rule is for. THE ASYMMETRY. In arm_backend.rs, stages 1 and 2 each retry with a GROWN slot pool when their failure is slot exhaustion. Stage 3 (`vfp-wide-file`, #1267) calls `full_sequence(None, true, true, true)` and runs with the DEFAULT 8-slot pool while asking the selector to frame-home locals, with no retry at all. The two halves each fix exactly what the other hits: vfp-frame-locals+pool-grow(N) -> VFP register file exhausted (the wide file fixes) vfp-wide-file (8 slots) -> spill-slot pool exhausted (a grown pool fixes) The combination had never been tried. The externally-reported `controller@0.10.0#step` (#1318/#1426) shows both walls in one ladder. This is the "twin does not inherit the fix" shape already recorded here from v0.71: stage 3 was added after stages 1 and 2 already had their retries. ADDING THE RETRY EXTENDS REACH, measured on a synthetic family of n f32 locals consumed by a RIGHT-leaning product nest so all n stay live at once (the shipped fixtures fold LEFT, two live at a time, which is why none reached stage 3): the last compiling n went 58 -> 64, and the new wall at n=72 is the genuine `[sp,#imm]` 1020-byte VSTR/VLDR ceiling, declined loudly. The cost half moved the right way too — n=60 emitted 1956 bytes against n=59's 2040, because 32 allocatable S-registers instead of 16 means fewer values need a frame slot at all. AND THE NEWLY-ACCEPTED CODE IS WRONG. Through the #1069 execution differential (unicorn vs wasmtime, bit-exact): every NEGATIVE input disagreed, every non-negative agreed, and `got ^ want == 0x8000_0000` on EVERY failing row — precisely the sign bit — for -0.0, -1.0, -0.25, -3.14159265, -1e30 and -inf. All 60 factors share the param's sign, so 60 of them multiply to a POSITIVE result; an odd number of sign contributions means one factor is not the value it should be. Magnitudes agree because this family saturates to ±inf or 0, so the fixture DETECTS the defect and cannot localise it further — said because a reader would otherwise expect a magnitude signal. THE DEFECT IS IN THE WIDE-FILE PATH, NOT POOL GROWTH, and that is derived: `live24` in the same differential exercises `vfp-frame-locals+pool-grow` and is bit-exact, so the delta between a passing case and a failing one is the wide file. WHY IT SURVIVED: #1267 is the ONLY rung with no execution oracle. Nothing in scripts/repro/ covers it. `vfp_wide_file_1267.rs` asserts the VPUSH/VPOP pair, its position relative to the frame `sub sp`, and the #1273 stack-param refusal — real encoding properties — so the ordering hypothesis is already excluded by that file's own assertions and the cause is elsewhere. Filed as #1439 with the repro rather than guessed at. LATENT, NOT ACTIVE, and the distinction is load-bearing: that file records that nothing on this tree reaches the rung, and that on the reporter's module it is "reached TWICE and rescues neither call". Because it rescues nothing, NO SHIPPED BINARY MISCOMPILES THROUGH THIS PATH TODAY. What makes it urgent is that the obvious reach fix would make it live, converting two loud declines in a real customer module into possibly-wrong code — "accept more and check less" by name. SO THE RUNG IS NOT IN THE TREE. What is committed is a test pinning the honest state: the shape declines, the ladder REACHES the wide-file rung and dies there on slot exhaustion, stage 2's grow retry IS present (so "stage 3 lacks one" is a real contrast), and stage 3's is ABSENT. That last assertion is a TRIPWIRE that fails the moment the rung lands, forcing whoever adds it to add the execution coverage in the same change. PROVEN POTENT by applying the ~20-line rung and watching the test go red, with the mutation verified by `git diff --numstat` against a BACKUP COPY (10 lines added) and arm_backend.rs afterwards confirmed restored byte-identical by an empty numstat. THE FIXTURE IS DELIBERATELY NOT IN THE COMMITTED .wat. A declining export makes `synth compile` exit non-zero under #952, so the differential would need `--allow-skipped-exports` — and that flag's own diagnostic says a build gating on `$?` would otherwise accept an object with a silently-missing public entry point. Weakening that gate to host a fixture would trade a real safeguard for test convenience, so the shape lives in the Rust test where it needs no exemption. CONDUCT RULE 4, STATED PLAINLY: the externally reported residual DID NOT MOVE. `controller@0.10.0#step` still declines and this release does not change that. This is not progress on his defect — it is the measurement of why the obvious extension of the ladder cannot be taken yet. It is recorded here and in the release notes, NOT posted to his threads. ONE GATE CAUGHT ONE WORD. claim_check went 75/75 -> 2 failures on this tree, and both had a single cause: my comment said "mirroring stage 2", which is counted by the `mirror_marker_files` ratchet (a ceiling that must FALL, derived 61 vs ledger 60) and which also appears inside artifacts/status.json, so the staleness check fired too. The ledger's own spec warns this metric "over-counts prose", and describing a code shape is not declaring a hand-maintained mirror — so the wording is reworded rather than waived, which keeps the metric about what it means. `--emit-status` was correctly a no-op: status.json was never stale for any other reason, and the artifact count is not in it. Gates on this tree: claim_check 75/75, status_evidence 0 failures, version pins OK, oracle_wiring OK, artifact_citation OK, stale_pin PASS, ci_pool_tripwire 0, census self-test 39 assertions, cargo fmt clean, clippy -D warnings clean, cargo test --workspace 168 suites / 3148 passed / 0 failed. Refs #1439, #1426, #1318, #242 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * v0.78.0: what does it compile, and what does that code cost? Version bump 0.77.0 -> 0.78.0 across 30 pin positions (13 files), Cargo.lock and artifacts/status.json regenerated rather than hand-edited, plus the CHANGELOG section and the three remaining carried artifacts. THE ANCHOR IS DELIBERATELY NOT MOVED. `ANCHOR_TAG` stays v0.77.0 / 133 / 507; moving it at the tag reds A0, and it belongs in the v0.79 PLANNING PR where creating artifacts/release-v0.79/ is what forces it. THE RIVET SECTION IS PASTED UNEDITED from `release_notes_from_rivet.py --base v0.77.0`, and that is asserted rather than trusted: the tool's output was compared as a substring of the committed CHANGELOG. v0.77's first attempt reordered and paraphrased every title while carrying the tool's own "do not hand-edit the lists" comment. THE TRACE-GRAPH DELTA IS VERIFIED, NOT REPEATED. +27 warnings / +0 errors. Previous releases called this "structural"; this one derived it: 27 = 9 artifacts x exactly 3 classes (RQ-* ids not commit-trailer shaped; `req-type: process` outside the loaded schema; each system req wants an incoming `verifies` link), 9 in each class, same three classes and same rivet 0.37.0 as v0.77's +24 over 8 artifacts. A peer session was working on rivet schema-validation warnings; it has NOT landed. THE THREE CARRIED ARTIFACTS, each measured: PINDEBT6 (#1373) — known_open_pins 84, known_open_pinned_cases 157, delta across v0.78 ZERO, derived from `git show v0.77.0:claims.yaml` rather than quoted. The tool's own columns say last-moved v0.74.0, held 5 releases. Ground, derived: `git diff --name-only v0.77.0..HEAD -- '*.rs'` is exactly ONE file and it is under tests/, so no emitted byte can move. Two candidates rejected, one of them ATTEMPTED and reverted (WIDEFILE). VARVE (#1422) — a recorded NON-ACTION on the maintainer's decision. Confirmed rather than asserted: `git log v0.77.0..HEAD -- varve.toml` is EMPTY, layer still 2026.09.2, and `grep -rn VARVE_ROOT .github/` returns nothing. The inversion is restated because it is what makes every local remedy wrong, and the open question is upstream. ARCHMODEL (#1136) — spar#445 OPEN, updatedAt EQUALS createdAt at 2026-09-03T10:57:37Z with zero comments, so untouched for 27 days. SIXTEENTH consecutive N/A, derived BY ARTIFACT IDENTITY (v0.77's tag-keyed census undercounted 15 as 14 because v0.65's filing predates today's tag vocabulary) and confirmed with the gate's OWN find_filed_steps12_decision across every release directory: 16 non-stale filings, v0.63..v0.78, contiguous, v0.78 discharged. The five tags are intact. NEITHER RATCHET IS PINNED, and the CHANGELOG says so rather than omitting it: the reach floor cannot be pinned while the corpus is unmounted, and pinning the cost ceiling ALONE is the alternating the theme forbids. Gates on this tree: claim_check 75/75, status_evidence 0 failures, version pins OK at 0.78.0, oracle_wiring OK, artifact_citation OK, stale_pin PASS, ci_pool_tripwire 0, census self-test 39 assertions, cargo fmt clean, cargo test --workspace 168 suites / 3148 passed / 0 failed. Still outstanding before the tag: the two-round cold review record (docs/reviews/v0.78-cold-review.md, conformance step 7) and CI on the merged commit. Refs #1432, #1433, #1373, #1422, #1136, #242 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * RQ-78-RITUAL: the script every merge goes through had no test, and its wait loop could only fail by hanging `scripts/merge_ritual.sh` runs four checks and performs the merge inside its own && chain. It had NO test, NO CI reference and NO shellcheck anywhere in the tree, and its CHECK3b wait loop was `while :; do ... sleep 60; done` with no bound at all — so its failure mode was a HANG rather than a signal. Three releases have already had to repair it: RQ-72-RITUAL created it, RQ-73-STEP8 added the squash-fidelity call, RQ-77-SUBJECT fixed a loop that counted checks with an EMPTY conclusion and an exit code read through a `| tee`. Every property it relies on was held in place by nothing but the file not being edited. THE LOOP IS NOW BOUNDED. `MAX_WAIT_MIN`, default 180, overridable through `MERGE_RITUAL_MAX_WAIT_MIN` because runner capacity is a fleet property and not a property of this script — synth holds 1-2 of 12 self-hosted slots and a release PR has taken ~2.5h, so 3h is generous rather than tight. On exhaustion it prints TIMEOUT and exits 2: a REFUSAL, never a fall-through to a verdict, because timing out tells you nothing about whether the PR is mergeable. A hang is worse to diagnose than a refusal — there is nothing to read. `scripts/test_merge_ritual.py` is the repo's FIRST test for the ritual: 11 assertions, wired into the required `claim-check` job, hermetic. IT DOES TWO DIFFERENT THINGS AND DOES NOT CONFLATE THEM. EXECUTION: the timeout is tested by EXTRACTING THE SHIPPED LOOP TEXT from merge_ritual.sh and running it against a stub `gh`, so the lines under test are the lines that ship and nothing is mirrored — a re-typed loop would be a hand-written mirror of a shipped thing. With a 1-minute budget and checks that never settle it exits 2 with TIMEOUT; with nothing pending THE SAME loop exits normally, and that POSITIVE CONTROL is load-bearing, because without it "it exits 2" would be equally consistent with a loop that can never succeed. STRUCTURE: the rest are static and each is proven NON-VACUOUS by removing the property from a copy — the merge sits inside an && chain, merge_gate's exit code is read from the PROCESS and not through a pipe, the ritual greps the literal GATEOK, the wait floor is derived from branch protection, the loop is bounded. WHAT A TEST OF A SHELL SCRIPT CANNOT PROVE, stated rather than implied: the ritual's real behaviour needs a live PR, a live branch-protection API and a live merge, and a test that stubbed all of it would be testing the stub. The static half proves a property has not silently DISAPPEARED, which is exactly what the three repairs above were. TWO DEFECTS THE TEST FOUND IN ITSELF, both this release's own class: (1) The merge-chain assertion searched the whole file for `gh pr merge` and matched a COMMENT at line 25 — "`gh pr merge --squash` uses the PR title..." — which carries no `&&`. It reported the SHIPPED merge as unchained while the real statement 20 lines further down is correctly chained. A true statement about the wrong subject, inside the test written to catch that class. Fixed by stripping comment lines, with the reason recorded in the helper. (2) Two mutations used `.replace(old, new, 1)`, so an `in`-style predicate still found a later copy of the token and the mutant was REJECTED BY NOTHING — the assertion looked non-vacuous while proving nothing. Fixed to replace-all. Both surfaced ONLY because the loop requires the mutant to fail, which is the difference between a mutation check and a decoration. NOT CLOSED, and named on #1440 rather than left looking done: shellcheck is ABSENT from this machine, so a CI step for it could not be verified locally, and wiring an unverified step into a required job is how a gate stops being trusted; and the ritual is still untested END TO END. #1440 is therefore held open via `issue-scope: outlives`. THE CHANGELOG'S RIVET BLOCK WAS RE-DERIVED, not hand-patched, because this artifact is the tenth and the block named nine. `release_notes_from_rivet.py --base v0.77.0` re-run and pasted unedited (asserted as a substring, not trusted), and the trace-graph delta re-measured: +30 warnings / +0 errors = 10 artifacts x exactly 3 classes, 10 in each, still the same three classes and the same rivet 0.37.0. A figure derived from files the release edits is true only at a named commit, and this one moved under its own lane. Gates on this tree: claim_check 75/75, status_evidence 0 failures (223 artifacts, 171 done-when predicates), version pins OK at 0.78.0, oracle_wiring OK, artifact_citation OK, stale_pin PASS, ci_pool_tripwire 0, merge-ritual 11 assertions, census self-test 39 assertions. Refs #1440 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * Cold review round 1 (gate potency): 18 gates tested, 2 vacuous, 6 corrections An independent fresh-context pass made every new and changed gate go red on demand, verifying each mutation against a BACKUP COPY and reading every exit code without a pipe. 16 of 18 were POTENT. The two that were not, and four other findings, are corrected here. VACUOUS 1 — ONE MATCHER SERVED ALL FOUR REFUSALS. `_refuses()` checked only that the message started with `REFUSE:`, so the four refusal assertions in shipped_feature_census.py were interchangeable: each asserted "SOME refusal fired", not "THIS one did". MEASURED consequence — deleting the empty-glob refusal outright left the self-test GREEN at 39 assertions / 0 failures, because the DOWNSTREAM zero-reads refusal fired instead and satisfied the matcher. One assertion named a refusal it was not testing, which is a true statement about the wrong subject in the file whose own subject is that class. Every caller now passes a distinctive substring of its own refusal (`matched no files` / `zero SYNTH_* reads` / `reads a SYNTH_* variable` / `classify DIFFERENTLY`) and `_refuses` requires it — plus an assert against an empty needle, which would re-open the same hole. RE-PROVEN: the same deletion now reds the assertion that names it. VACUOUS 2 — THE HEADER'S CLAIM ABOUT ITS OWN WIRING WAS FALSE. It said the census "asserts nothing about the compiler's output, so there is no expected value for CI to fail on beyond the self-test", and only `--self-test` was wired. But `main()` returns 1 when any flag is UNDETERMINED, which IS an expected value. MEASURED: deleting the whole MEASURE_ONLY/DIAG/SOLVER_BUDGET bucketing moved the reported answer from 4 hidden capabilities to 15 with 2 undetermined, and CI stayed GREEN because nothing ran the census. The two MEASURE_ONLY assertions are membership-in-a-constant tautologies; running the census is what exercises the bucketing that consumes them. The census itself is now a required step and the header says what is actually wired. A FALSE NUMBER IN A RELEASE ARTIFACT'S OWN EVIDENCE FIELD, and the review derived that nothing pins it: RQ-78-FEATURESET said the self-test has "(36 assertions)" while the live count is 39 and MIN_ASSERTIONS is 39. Corrected, and the same sentence now names BOTH wired steps rather than one. THE GUARD DID NOT TRANSFER BACK TO THE FILE THAT MOTIVATED IT. `ci_citation_floor.py --self-test` had NO assertion-count floor, even though `shipped_feature_census.py` added exactly that guard in the SAME release citing THIS file's lane (#1435) as its precedent. MEASURED: deleting its `an ABSENT line REFUSES` assertion took the run from 15 printed assertions to 14 with rc=0 and "0 failure(s)". `MIN_ASSERTIONS = 15` added, derived by RUNNING the self-test and counting printed lines rather than regexing `ok(` — a first attempt at that regex returned 9 and its own sanity assertion caught it before anything was written. PROVEN potent: 14 < 15 now exits 1. A FIXTURE THAT CLAIMED TO BE LIVE. `ci_citation_floor.py`'s `live` sample says `7274 test names / 206 artifact files`; the tree emits `7275 / 209`. Rather than re-syncing a figure that moves with the corpus every release — a fixture needing that is a fixture nobody trusts — it is now labelled a FROZEN SAMPLE with its capture date, and the comment says what it pins (the SHAPE) and where a real drift would surface (the ci.yml step that runs the parser against the real log). AN ACTIONABLE MESSAGE ON AN UNREACHABLE PATH. `wide60_declines_...`'s explicit tripwire assert carries the instruction "flip this test AND add wide60 to the execution differential", but in the realistic case — the rung lands and the shape COMPILES — `expect_err` panics FIRST, so the operator sees "must still DECLINE" and never the instruction. The test reds either way; only the useful text was unreachable. The instruction now rides on the `expect_err` message too, naming #1439's sign-wrong result so nobody reads a compile-only green as reach. NOT CHANGED, on the review's own reasoning: the remaining `manual:` done-when predicates are documented as unchecked-by-design, and flipping a `proposed` artifact to `implemented` does red — via R11, because `disposition: partial` contradicts a claiming status. Gates on this tree: claim_check 75/75, status_evidence 0 failures, version pins OK at 0.78.0, oracle_wiring OK, artifact_citation OK, stale_pin PASS, ci_pool_tripwire 0, merge-ritual 11 assertions, citation floor 15 assertions, census self-test 39 assertions, census 0 undetermined, vfp_local_pressure_1069 10 passed, fmt clean. Refs #1435, #1437, #1439 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * Cold review round 1 (prose truth): 109 statements checked, 10 false, all corrected An independent fresh-context pass verified every checkable claim in the CHANGELOG's v0.78 section, all ten artifacts and the six commit messages by RUNNING the refuting command rather than reasoning about plausibility. Ten were false. The conduct question came back clean, and that half was verified in detail rather than asserted (below). THE BEST CATCH — THE RELEASE'S OWN TWO NUMBERS REFUTED EACH OTHER. "The last compiling case moved from 58 to 64 locals" appeared in the CHANGELOG, in WIDEFILE, in PINDEBT6 and in commit f1348d74. But the same artifact says "n=60 emitted 1956 bytes against n=59's 2040" ONE CLAUSE LATER — and n=59's 2040 bytes is a figure from the SHIPPED tree, so 59 compiles and the wall is at 60. The committed test's own docstring already said "the wall for the family moves from 60 to 72". THE CODE WAS RIGHT AND THE PROSE WAS WRONG. The reviewer built an out-of-tree crate with path deps, copied `wide_f32_ops` and `m7dp_config` verbatim, and ran the shipped ladder: 57/58/59 OK at 1968/2004/2040 bytes, 60 and beyond DECLINE. Restated everywhere as the WALL moving 60 -> 72, with 59-compiles-today named so the two figures can no longer disagree. "To 64" was the same defect at the other end: 64 is the largest point tested, not the new wall, which the artifact itself puts at 72. 38 WAS THE WRONG DENOMINATOR. "38 `SYNTH_*` reads in shipped code" — 38 is the FLAG count; there are 61 read sites across them, 6 flags read at more than one site. The census's own output says "38 SYNTH_* flags", and the next clause ("Four are capabilities") only parses over flags. Corrected to name both numbers. A PROVENANCE CITATION POINTING AT AN UNREACHABLE COMMIT. FEATURESET said "MEASURED at this cut, at commit `8f564ad8`". `git merge-base --is-ancestor 8f564ad8 HEAD` says NO and `git branch -a --contains` is empty: it is the orphaned pre-rename cost-model commit, stranded when its subject was amended off an artifact id — a rename this release made deliberately, for status_evidence R4. The citation exists PRECISELY to supply provenance for a number derived from files the release edits, and it named a commit belonging to a different lane that no longer exists. Now `fac5b463`, verified reachable. A citation that looks checkable and is not is worse than none. THE 5 -> 4 CORRECTION DID NOT PROPAGATE. Commit 078cd88a corrected the headline from five hidden capabilities to four, and three clauses kept the old figure: FEATURESET's held-open comment and its closing paragraph ("three of the five"), and BLOCKERCLASS's "five capabilities ship flag-off". The CHANGELOG had it right at "two of the four", so an artifact disagreed with the notes that summarise it. The breakdown is now stated so it sums: two say only "evidence-gated", one is gated on #494's phasing, one on silicon (#580). 29,616 IS THE v0.57 FIGURE FOR A FILE THAT IS 19,905 LINES. It appeared in the artifact, in commit fac5b463 and in the SHIPPED SCRIPT'S OWN DOCSTRING, twice. `wc -l` is 19905 at HEAD and at v0.77.0; the family total is 30375. The `#[cfg(test)]` sits at line 308, so "1% / 99%" becomes line 308 / 98% — the argument survives, the number did not. AND THE "4 OF 128 FILES CUT EARLY" WAS 3 BY THE SENTENCE'S OWN CRITERION. Three files lose SHIPPED code to a first-marker cut (instruction_selector.rs, expansion_validator.rs, properties.rs). The fourth, optimizer_bridge.rs, merely has more than one `#[cfg(test)]` and its first is at 79.7%, losing nothing shipped. Counting it needs a different predicate than the one the sentence gives. A NARROW EXCEPTION GENERALISED INTO THE RULE. COSTMODEL's description said WCET bounds "are priced from the REAL ENCODER's own byte lengths (`straightline_expansion_real`), not from the estimator". The GENERAL path is `straightline_expansion` at wcet.rs:119, which calls `estimate_arm_byte_size` — the ESTIMATOR, as its own doc says. `straightline_expansion_real` at :142 is consulted from exactly ONE match arm (:342), the #936 i64 family. The soundness argument holds and is a different one: the estimator is pinned to the real encoder by `estimator_encoder_agreement`, which is why using it is provably >= the real cost — and why the same file can call it a "hand-maintained mirror" two paragraphs later without contradiction. Corrected in place, with the refutation recorded rather than the sentence quietly swapped. A LINE NUMBER THAT NAMED THE CONSULT SITE AS THE READ SITE. `optimizer_bridge.rs:3719` does not contain `SYNTH_SPILL_ON_EXHAUST`; the env read is at :784, which is where the census itself reports it, and :3719 is where the flag is consulted. The paired citation (instruction_selector.rs:9238) is exact, which made the mismatch read as equally exact. Both sites now named for what they are. THE CONDUCT QUESTION: NO VIOLATION, verified rather than assumed. Zero comments were posted to #1318 or #1426 by this release — #1318's 13 comments all predate every v0.78 commit, #1426 has none. #1426's `updatedAt` on release day is a BODY edit, not a thread post, and #1426 is authored by avrabe, not the reporter. It is 384 words about his build with no machinery, no ratchet content, no repo citation convention (that text lives in the source comment, not the issue) and no loop trailer. The shipped diagnostic cites the OPEN, correctly-titled #1426. Rule 4 is respected explicitly in three places. Gates: claim_check 75/75, status_evidence 0 failures (223 artifacts, 171 done-when, 72 archaeology checks, 0 skipped). Refs #1437, #1439, #1433, #242 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * Cold review record for v0.78, and the round-2 section stated rather than omitted docs/reviews/v0.78-cold-review.md — conformance step 7's artifact, naming both reviewed commits: round 1 examined a4afc445, round 2 examines 0b4a6f13 (the tree AFTER round 1's corrections, because its brief is to attack those corrections rather than re-review the release). Records round 1's two parallel passes: prose truth (109 statements checked, 10 false) and gate potency (18 gates tested, 16 potent, 2 vacuous), each finding tabulated with the true value beside the false one. Includes the conduct question's verification in detail — zero comments posted to either of the reporter's threads, #1426 still 384 words about his build, the shipped diagnostic citing the open correctly-titled issue, and rule 4 respected explicitly in three places. ALSO RECORDS THE PRE-TAG STEP THAT HAS CAUGHT THINGS TWICE: the close set derives as 1 authorised (#1435), 3 held open (#1437, #1439, #1440), with #1319/#1419 attributed to v0.77 by the prior-release scan and cpetig's #1318 correctly NOT authorised because the release did not move his residual. #1435's four asks were then verified ON THE TOOL rather than on the pin — numeric comparison (206 rc=0, 99 rc=1), the offending value printed, an absent summary line REFUSED, and a `--self-test` pinning the old regex in both directions — plus the wiring the issue implies rather than states: the `1[0-9]{2,}` grep is gone from ci.yml and the script runs at both :407 and :470. The issue's OWN refuting command now inverts: 206 ACCEPTs, which the issue says makes it stale. ROUND 2 HAS NOT REPORTED, AND THE RECORD SAYS SO IN THOSE WORDS. An empty section would read as "round 2 found nothing"; this one lists the eleven correction groups it was dispatched to attack and states that it must be filled before the tag. v0.77's round 2 found THREE of five failures inside round 1's own corrections, one having reached reporter-facing text, so an unreported round 2 is not a formality. PUSHED NOW DESPITE THAT, on a measured ground: a4afc445 has had ZERO runner slots for two hours (17 non-advisory queued, 0 in_progress, 59 completed), and it is a tree three commits behind what will ship. Its queued jobs occupy queue positions to test something that is not the candidate. The CI waiter pinned to it exhausted its budget and printed `TIMEOUT after 120 polls` with exit 2 rather than falling through to green — the behaviour RQ-78-RITUAL added to merge_ritual.sh for the same reason, here in the ad-hoc waiter. Gates: claim_check 75/75, status_evidence 0 failures, version pins OK at 0.78.0, oracle_wiring OK, artifact_citation OK, stale_pin PASS, ci_pool_tripwire 0, merge-ritual 11 assertions, citation floor 15 assertions, census self-test 39 assertions, census 0 undetermined. Refs #1435, #1437, #1439, #1440 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * Cold review round 2: 11 corrections attacked, 2 FAILED — both inside round 1's own fixes Round 2's whole job is to attack round 1's corrections, and it earned it again: 9 held, 2 failed, plus 2 false statements round 1 missed entirely. The same shape as v0.77, where three of five round-2 failures were inside round 1's corrections. FAILURE A — THE WALL IS 66, NOT 72, AND 72 WAS NEVER MEASURED. This is the worse of the two, because round 1's correction made the number LESS true. Round 2 built an out-of-tree probe (path deps into the worktree, `wide_f32_ops`/`m7dp_config`/ `ladder_compile` copied verbatim), applied the ~20-line stage-3 retry and swept n=55..80: shipped tree : 57/58/59 OK at 1968/2004/2040 B, 60 DECLINES with retry : 60..65 compile at 1956/1992/2028/2064/2100/2136 B, 66 DECLINES at n=66 : vfp-wide-file+pool-grow(136) -> #881: offset 1024 exceeds the VSTR/VLDR [sp,#imm] range (1020) So the wide file buys SIX locals, not twelve. And the grow formula is NOT the variable — byte-identical at the stage-2 size, at the I64_SPILL_SLOTS_MAX cap of 120, and with the cap lifted to 400 — because ~128 eight-byte slots are the addressable maximum under a 1020-byte offset and this family consumes about two per local. WHERE 72 CAME FROM: the test docstring, never measured. Round 1 promoted an UNTESTED DOCSTRING NUMBER into the CHANGELOG headline and three artifacts, REPLACING `58 -> 64` — where 64 was at least a genuinely compiling measured point. The mechanism it named was right; its subject did not exist. Corrected at the source (the docstring) and in all four places, with the shipped-tree figure and the probe figure now distinguished so they cannot be read as one measurement. SECOND COUNT: THE CORRECTION DID NOT PROPAGATE. `RQ-78-WIDEFILE.yaml`'s `verified-by` still carried "the last compiling n was 58" — the exact sentence round 1 declared false — because round 1's diff touched only the `description`. The evidence field is the one that matters, and it kept the false statement. FAILURE J — A VACUOUS ASSERTION IN THE TEST ROUND 1 HAD JUST WRITTEN. The population-floor assertion in `test_merge_ritual.py` passed `loop.replace("FLOOR","FLOOR")` — A NO-OP — and its predicate `rc == 0 or "TIMEOUT" in out` accepted BOTH outcomes the harness can produce. It held under a break condition replaced by `false`, under the floor removed entirely, and under an unsatisfiable floor. Its own name conceded it ("which is what the positive control above just showed"). Round 1's gate pass recorded "18 gates tested, 2 vacuous" and listed this very file as verified at 11 assertions; there were at least three. Replaced with one that varies the POPULATION — 3 present against a floor of 9 with nothing pending, the #1407 shape where "nothing pending" is also true before CI registers. `run_loop` gained a `present` parameter, because a parameter that cannot vary cannot discriminate. Re-measured, and the honest result is a PAIR: floor removed (-ge 0) -> floor assertion FAILS, positive control passes break condition -> false -> floor assertion passes, POSITIVE CONTROL FAILS floor unsatisfiable -> floor assertion passes, POSITIVE CONTROL FAILS timeout removed -> the loop HANGS; the harness's 120s timeout raises Neither member is sufficient alone, and that pairing is now recorded in the file — claiming the single assertion catches all four would be the same over-claim round 2 had just caught. NEW, MISSED BY ROUND 1: CORRECTION G'S PROPAGATION RE-ASSERTED THE ERROR IT FIXED. `RQ-78-BLOCKERCLASS.yaml:93` read "`SYNTH_SPILL_ON_EXHAUST` is CONSULTED at `optimizer_bridge.rs:784` and CONSULTED at `:3719`" — round 1 inserted `:784` into a sentence whose verb was already "consulted", producing a clause that calls :784 a CONSULT site, precisely the defect its own commit message says it fixed. The CHANGELOG edit was correct; the artifact was not. Now "is READ at :784 and CONSULTED at :3719". AND ROUND 1'S OWN TWO HEADLINES ARE NOW FALSE, corrected in the review record where they are stated rather than quietly dropped: "10 false, ALL CORRECTED" (one survived in the evidence field, and the replacement was itself false) and "2 vacuous" (at least three). THE NINE THAT HELD, each re-derived: 61 read sites and 6 multi-site flags; 19,905 lines / marker at 308 / 98.45% / three files losing shipped code; `fac5b463` reachable and correctly described while `8f564ad8` is not; the 2+1+1 breakdown summing to four with the right gates named; wcet.rs 118/119/142/342 with "exactly one" exact; :784/:3719 both exact; BOTH claimed vacuity fixes — each of the four refusals, deleted in turn, now fails THE ASSERTION THAT NAMES IT and no other; MIN_ASSERTIONS = 15 real and potent; and the conduct findings. THE THIRD QUESTION, ROUND 2: no violation. #1426 0 comments / 384 tokens / updatedAt BEFORE the first v0.78 commit; #1318's 13 comments all predate the release. The comment on #1441 replies to fathom/gale — the body is signed as such — not to cpetig, leads with the decision, corrects no count, and claims no v0.78 progress. One clause is noted as AMBIGUOUS rather than false: "not v0.78, which is at its tag" is true read as "at its tag point" and false read as "already tagged". Recorded so the wording is not reused. Gates: claim_check 75/75, status_evidence 0 failures, version pins OK at 0.78.0, oracle_wiring OK, artifact_citation OK, stale_pin PASS, ci_pool_tripwire 0, merge-ritual 11 assertions, citation floor 15 assertions, census self-test 39 assertions, census 0 undetermined, clippy -D warnings clean, cargo test --workspace 168 suites / 3148 passed / 0 failed, fmt clean. Refs #1435, #1437, #1439, #1440 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>

avrabe mentioned this pull request Jul 2, 2026

Direct selector spill rung miscompiles: ldr reads a never-stored frame slot after mul.w clobbers a live register (shipped path, wrong value) #581

Closed

avrabe merged commit 9474111 into main Jul 2, 2026
24 of 25 checks passed

avrabe deleted the feat/242-exhaustion-spill branch July 2, 2026 18:40

avrabe mentioned this pull request Jul 2, 2026

fix(selector): spill rung stores before clobber — never reload a never-stored slot (#581) #582

Merged

avrabe mentioned this pull request Jul 2, 2026

chore(release): v0.24.0 — the allocator release: VCR-RA-001 verified, Belady spilling default-on #585

Merged

This was referenced Jul 7, 2026

docs: refresh README North-Star + CLAUDE.md to post-v0.30 reality #625

Merged

verify(vcr): VCR-VER-001 program gate DEMONSTRATED — patch-accretion reverses (#242) #659

Merged

avrabe mentioned this pull request Jul 8, 2026

feat(vcr-ra): post-exhaustion code quality — the capability PR #659 named missing (#242) #672

Merged

avrabe mentioned this pull request Jul 10, 2026

fix(bulk-memory): #677 operand clobber + #679 silent-unmasked mask — copy/fill #695

Merged

This was referenced Sep 30, 2026

The delivered binary is not the full feature set: 5 capabilities ship flag-off, and synth verify is absent from the crates.io build #1437

Open

RQ-78-FEATURESET (#1437): the delivered binary is not the full feature set — derive it, on both axes #1438

Merged

Navigation Menu

Repository navigation

feat(vcr-ra): spill on register exhaustion — remove the optimized-path hard-fail (#242, VCR-RA-001) - #580

feat(vcr-ra): spill on register exhaustion — remove the optimized-path hard-fail (#242, VCR-RA-001)#580
avrabe merged 1 commit into
mainfrom
feat/242-exhaustion-spill

avrabe commented Jul 2, 2026

Uh oh!

codecov Bot commented Jul 2, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

avrabe commented Jul 2, 2026

The hard-fail history

Allocation-time Belady spill (flag: SYNTH_SPILL_ON_EXHAUST, default OFF)

Flag choice

i64 scope (honest)

Red→green

Flag-off proof (STOP condition)

Flag-on validation

Size (honest)

Found while testing (pre-existing, NOT touched here)

Uh oh!

codecov Bot commented Jul 2, 2026

Codecov Report

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Allocation-time Belady spill (flag: `SYNTH_SPILL_ON_EXHAUST`, default OFF)