plan(v0.67): scope the release — "One root cause, not five symptoms" (7 artifacts)

[avrabe]

Scopes v0.67 and moves the release anchor to v0.66.0. Seven artifacts, no code changes.

Why this theme

v0.66 built oracles that had never existed and ran them on code that had never been executed — the self-contained corpus images were compiled roughly 400 times per survey run and never once booted, and the boot sweep's first run found two silent miscompiles. It closed 77 of 103 pinned parity entries and still ended with known_open_pins at 127, because the instruments kept finding things faster than the fixes closed them.

The residue is a cluster that reads as separate defects and is not. #1204, #1241 and a run of optimized-path wrong answers all report R9/R10/R11 clobbered. #1241 asks the question in its own title — "(#1204's pair class?)". #1204 already names the mechanism:

register	role in a self-contained image
R11	the direct selector's linear-memory base, seeded 0x2000_0100 by the generated startup
R10	the register the software bounds guard compares against
R9	allocatable, observed clobbered alongside the other two

liveness::ensure_callee_saved_prologue (#490) saves R4-R8. The optimized path's allocator hands out R9-R11. The return values are correct; it is the next function that breaks.

Artifacts

id	pri	issue	one line
RQ-67-CALLEESAVE	must	#1204	fix the callee-saved set, then measure which issues closed
RQ-67-VFPREACH	must	#1267	synth allocates from half the VFP register file
RQ-67-HIGHWORD	must	#1240	i64 clz/ctz/popcnt high word — the #916 class on the other selector
RQ-67-SUBTRACT	must	#242	make selector_lines_code fall for the first time
RQ-67-PINDOWN	should	#242	known_open_pins must end below 127
RQ-67-NOTESGATE	should	#1259	give the release notes a gate
RQ-67-ARCHMODEL	carried	#1136	seventh consecutive N/A, re-verified at cut

Added after the plan was written, from a user report (#1267)

Filed by gale against shipped v0.66.0 while this PR was in CI. The falcon flight cascade lowers 21 of 22 functions on --target cortex-m7dp and declines exactly one — the tick — with VFP register file exhausted (S0..S15 all live).

Reading the source rather than the message: the selector allocates inside S0-S15/D0-D7 (vfp_home: &[bool; 16]), the encoder already encodes VfpReg::S0 through S31, VPUSH/VPOP appear nowhere, and liveness.rs:5977 says in so many words that D8-D15 are callee-saved and out of scope. Every FPU target synth supports has S0-S31. The file is not exhausted when that error fires — half of it is unused, because using it needs a prologue that cannot be emitted.

That makes the release more coherent, not less. It is RQ-67-CALLEESAVE's shape one register file over:

	integer	float
prologue saves	R4-R8	nothing
allocator wants	R9-R11	D8-D15
failure	clobbers it — silent wrong answer (#1204)	refuses to use it — loud decline (#1267)

One root shape — the callee-saved contract and the allocator disagreeing about which registers exist — failing in opposite directions.

The reporter asked which of two remedies was intended. Neither: they already tried guest-side #[inline(never)] and the decline moved with the body (#952, then #1102), and VFP spilling was never going to cover a tick this size against half a register file. Answered on the issue.

Two things deliberately fixed in the plan rather than discovered during it

The attribution is a measurement, not a prediction. CALLEESAVE's done-when requires re-running the boot sweep and the parity oracle over the whole cluster and naming which issues closed. v0.66's five both-selectors-wrong classes turned out to be four root causes — two issues were one defect, one issue was two independent causes. Five fixes for one bug is worse than one honestly attributed, and so is one fix claimed to have closed five things it never touched. HIGHWORD stays a separate artifact as the negative control: it is explicitly a different mechanism, so if it closes as a side effect the attribution is wrong somewhere and the release says so.

The subtraction lever is named before the work starts. "Find something to delete" is the instruction that produced eight consecutive rises. v0.66 killed the previous lever honestly — all four "DEAD" sites were reachable, and all four sat outside the ratchet's population anyway, so deleting every one would have moved the metric by zero. What remains is v0.58's own correction, which makes sel_dsl_rules rising the precondition for selector_lines_code falling: one artifact, not two. The candidate is the i64 immediate family — i32 carries sixteen proven _imm rules, i64 carries zero of the 80, the hand-written arms exist in select_with_stack.rs, and the Rocq proofs follow a pattern already discharged.

The anchor move, and the gate that caught it

status_evidence_check reported ANCHOR-LAG 1 and named the values it needed (v0.66.0, delivery 69, programme 417). Moving the constant without the matching ledger pin reddened Claim Check on the first attempt here — the gate working exactly as designed, since the anchor is pinned in claims.yaml precisely so it cannot drift silently. Both move in this PR.

Gates

claim_check 0 · status_evidence 0 · oracle_wiring 0 · version_pins 0

rivet validate reports 40 errors, unchanged from the pre-existing baseline. The six new artifacts add only the same two WARN classes every v0.66 artifact already produces (req-type: process and the commit-trailer id shape).

Refs #1204 #1240 #1259 #1267 #1136 #242

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!