From 90f49eb7727ff83b730928ecc68c3f7abe431ce2 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 14 Aug 2026 22:48:01 +0200 Subject: [PATCH] =?UTF-8?q?plan(v0.58):=20"Delete=20the=20thing=20you=20re?= =?UTF-8?q?placed"=20=E2=80=94=20the=20North=20Star,=20corrected=20by=20me?= =?UTF-8?q?asurement?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The user asked for an honest review of whether the codebase needs a new north star. Measured rather than opined, v0.42.0 -> v0.57.0 (15 releases): workspace source 130,658 -> 174,578 lines (+34%) instruction_selector.rs 24,909 -> 29,616 lines (+19%) code (pre-test-module) 18,481 wildcard `_ =>` arms 105 selector churn since v0.42 5,515 added / 808 deleted (6.8 : 1) VCR-SEL-001 verified rules 40 -> 50 FLAT since v0.50 files saying "mirror" 57 files saying "hand-maintained" 11 files saying "single source of truth" 1 The finding: epic #242's GOAL is right and its STRATEGY is not working. The thing it exists to replace grew 4,707 lines while the replacement gained ten rules and then stalled for seven releases. We are not replacing the patch-accreting selector — we are building a verified path ALONGSIDE it, and the unverified one is winning on volume. The mechanism is visible in v0.57. VCR-SEL-001 made 50 ops Rocq-proved via a BYTE-INVISIBLE FLIP: the proofs are real, the shipped path did change, and the hand-written arms STAYED. So each release adds a proof, a checker for it, a doc claim about the checker, and a ledger pin for the doc — every one hand-maintained. v0.57 found 5 of its 10 defects were in CHECKERS and three doc claims had rotted behind a green 43/43. The verification machinery is now its own defect surface, and it grows because nothing is retired. CORRECTION, not replacement (recorded in CLAUDE.md's North Star): A rule is not done when it is proven. It is done when the hand-written arm it replaces is DELETED. That makes the epic's thesis a metric that CAN GO THE WRONG WAY — this repo's own standard for whether a gate is worth anything. It is currently going the wrong way and nothing notices, because nothing measures it. v0.58 — ten artifacts, subtraction-first: RQ-58-METRIC pin the numbers (ceilings that must FALL, floor that must RISE); adding an arm without deleting one must red the gate RQ-58-RETIRE delete the hand-written arms for the 50 DSL-covered ops — must be BYTE-IDENTICAL, since the DSL already emits them RQ-58-WILDCARD the selector's 105 `_ =>` arms, same class as #946 but with miscompile consequence; rank, convert, state the denominator RQ-58-MIRRORS generate-don't-mirror over the 57; fixing the FEATURE_MATRIX freshness gate (render-vs-template, never template-vs-code) is the highest-leverage item because it hid three others RQ-58-SELDSL un-stall 50 -> 70 rules, each landing WITH its deletion RQ-58-SPLIT split the 29,616-line file along the #197 seam, byte-identical RQ-58-SELECT973 #973 ARM select miscompile AND the CI gap that hid it RQ-58-VERIFYWIRE #981 shift-decline wiring RQ-58-OBJECT #938 breaking 0.x-minor on the crate differentials depend on RQ-58-FLAKE #977, whose silent direction is reading a STALE ELF and passing Explicitly NOT "clean up the codebase": refactoring 29k lines of selector with no per-step execution oracle is how you inject the miscompiles this project exists to prevent — and v0.57 supplies the cautionary case, since the gpio differential could not have caught its own miscompile. Every subtraction lane is gated on byte-identity or an execution differential. rivet: 50 errors before AND after (unchanged); warnings +20, the standard pair every artifact carries × 10. claim_check 43/43. Refs #242 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- CLAUDE.md | 29 ++- artifacts/release-v0.58.yaml | 399 +++++++++++++++++++++++++++++++++++ 2 files changed, 427 insertions(+), 1 deletion(-) create mode 100644 artifacts/release-v0.58.yaml diff --git a/CLAUDE.md b/CLAUDE.md index c0b16ada..bcaae728 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -123,7 +123,34 @@ public claim; when a proof/rule landed, bump doc + ledger together. **Replace synth's patch-accreting code generator with foundationally-verified, allocator-robust infrastructure — correctness from construction, not an -ever-growing pile of locally-correct patches.** The recurring greedy fixes +ever-growing pile of locally-correct patches.** + +> **CORRECTION (v0.58, measured — the goal is right, the strategy was not).** +> A rule is NOT done when it is proven. It is done when the hand-written arm it +> replaces is **DELETED**. Measured v0.42.0 → v0.57.0: `instruction_selector.rs` +> grew **24,909 → 29,616** lines (churn **5,515 added / 808 deleted**, 6.8:1) +> while VCR-SEL-001's verified rules went **40 → 50 and then sat flat for seven +> releases**; the workspace grew 130,658 → 174,578 lines. We were building the +> verified path ALONGSIDE the unverified one, and the unverified one was winning +> on volume — because "replace" was never measured, only asserted. +> +> The compounding cost: each release added a proof, a checker for the proof, a +> doc claim about the checker and a ledger pin for the doc — all hand-maintained +> (57 files say "mirror", 11 "hand-maintained", exactly **1** "single source of +> truth"). v0.57 then found **5 of its 10** defects were in checkers, and three +> doc claims had rotted behind a green gate. Verification machinery became its +> own defect surface because nothing was ever retired. +> +> So the metric is now **subtraction**, CI-pinned so it can go the wrong way +> (RQ-58-METRIC): selector line count and wildcard count are CEILINGS that must +> fall; the rule count is a FLOOR that must rise. Adding a hand-written lowering +> without deleting one must turn the gate red. +> +> This is NOT "clean up the codebase" — refactoring 29k lines of selector +> without a per-step execution oracle is how you inject the miscompiles this +> project exists to prevent. Every subtraction is gated on byte-identity or an +> execution differential; a deletion that moves emitted bytes without an oracle +> proving the new bytes correct is REFUSED, not explained. The recurring greedy fixes (reciprocal-mult cost-gate, register-exhaustion hard-fail, the "selector missed an op" class #223/#226/#232) are symptoms of two single-pass hand-written components: the instruction selector and the register allocator. Filed as the diff --git a/artifacts/release-v0.58.yaml b/artifacts/release-v0.58.yaml new file mode 100644 index 00000000..9cadcfa2 --- /dev/null +++ b/artifacts/release-v0.58.yaml @@ -0,0 +1,399 @@ +# ============================================================================= +# v0.58 — "Delete the thing you replaced" +# ============================================================================= +# +# THE THEME, and it is a CORRECTION to the North Star rather than a new one. +# +# Epic #242 says: replace the patch-accreting code generator — correctness from +# construction, not an ever-growing pile of locally-correct patches. +# +# The goal is right. The strategy is not working, and the numbers say so. +# Measured across v0.42.0 -> v0.57.0 (15 releases, 2026-08-14): +# +# workspace source 130,658 -> 174,578 lines (+34%) +# instruction_selector.rs 24,909 -> 29,616 lines (+19%) +# of which code (pre-test-module) 18,481 +# wildcard `_ =>` arms 105 +# selector churn since v0.42 5,515 added / 808 deleted (6.8 : 1) +# VCR-SEL-001 verified rules 40 -> 50 (FLAT since v0.50) +# files saying "mirror" 57 +# files saying "hand-maintained" 11 +# files saying "single source of truth" 1 +# +# Read those together. The thing the epic exists to REPLACE grew by 4,707 lines +# while the replacement gained ten rules and then stalled for seven releases. +# We are not replacing the patch-accreting selector. We are building a verified +# path ALONGSIDE it, and the unverified one is winning on volume. +# +# The mechanism is visible in v0.57. VCR-SEL-001 made 50 ops' lowering +# Rocq-proved through a BYTE-INVISIBLE FLIP — the proofs are real and the +# shipped path did change, but the hand-written arms STAYED. So each release +# adds a proof, plus a checker for the proof, plus a doc claim about the +# checker, plus a ledger pin for the doc — every one of them hand-maintained. +# v0.57 then found three of those had rotted while the gate showed green, and +# five of its ten artifacts were defects in checkers rather than in compiled +# code. Verification machinery has become a defect surface of its own, and it +# is growing because nothing is ever retired. +# +# THE CORRECTION, one sentence: +# +# A rule is not done when it is proven. It is done when the hand-written +# arm it replaces is DELETED. +# +# That turns the North Star into a metric that CAN GO THE WRONG WAY — which is +# this repo's own standard for whether a gate is worth anything. Right now it +# is going the wrong way and nothing notices, because nothing measures it. +# +# WHAT THIS RELEASE IS NOT. It is not "clean up the codebase". Refactoring +# 29,616 lines of instruction selector without a per-step execution oracle is +# exactly how you inject the miscompiles this project exists to prevent — and +# v0.57 supplies the cautionary case: the gpio differential could not have +# caught its own miscompile, so "the tests pass" would have been meaningless. +# Every subtraction lane below is gated on byte-identity or an execution +# differential. A deletion that changes emitted bytes without an oracle proving +# the new bytes correct is REFUSED, not explained. +# +# HONEST RISK, stated up front: byte-identity is the strong gate but it only +# proves we did not change behaviour on the inputs we HAVE. For the covered-op +# retirement that is sufficient (the DSL path already ships those bytes). For +# the wildcard and split lanes it is not, and those carry differentials. +# ============================================================================= + +artifacts: + - id: RQ-58-METRIC + type: system-req + title: "Make subtraction measurable — pin the numbers that are currently going the wrong way" + description: > + FIRST, because without it every other lane in this release is a vibe. + Nothing in CI currently measures whether the patch pile is growing. The + epic's own thesis is therefore unfalsifiable in practice, which is how it + drifted for seven releases without anyone noticing. + Pin, in claims.yaml and a CI step: instruction_selector.rs line count + (29,616 at v0.57.0), its wildcard-arm count (105), the VCR-SEL-001 rule + count (50), and the count of hand-maintained-mirror markers (57 files). + Direction matters and differs per number: the selector count and the + wildcard count are CEILINGS that must fall; the rule count is a FLOOR + that must rise. + RED-FIRST: adding a hand-written lowering arm without deleting one must + turn the gate red. Demonstrate it by adding one, watching it red, and + reverting — do not assert it. A ceiling set at "current + slack" would be + the vacuous version and is explicitly out of scope. + NOT a code-golf gate: the point is not fewer characters, it is fewer + hand-maintained decisions. If a lane legitimately needs to grow the file, + the ceiling moves WITH a stated reason in the same PR — the #911 rule + applied to size. + status: proposed + release: v0.58 + tags: [north-star, metric, falsifiability, vcr-sel-001] + links: + - type: derives-from + target: BR-001 + - type: refines + target: NFR-002 + fields: + req-type: functional + priority: must + verification-track: static-analysis + issue: "#242" + + - id: RQ-58-RETIRE + type: system-req + title: "Retire the hand-written arms for the 50 DSL-covered ops — the first deletion" + description: > + THE HEADLINE. VCR-SEL-001's 50 rules are the SHIPPED lowering path for + their covered ops (CLAUDE.md, byte-invisible flip). The hand-written arms + they replaced are still in instruction_selector.rs. Delete them. + This is the safest possible deletion and that is precisely why it goes + first: the DSL path ALREADY emits these bytes on main, so removing the + superseded arm must be BYTE-IDENTICAL across every frozen anchor and every + differential. If it is not byte-identical, that is a finding — it means + the flip did not cover what it claims, and the finding outranks the + deletion. + METHOD: one op per commit, anchors + differentials green per commit, so a + bisect lands on a single op. Report lines deleted per op and the running + selector total. + EXPECTED RESIDUAL, named in advance: some arms will be reachable from the + OTHER selector (#197 — `--relocatable` forces the direct path, + `select_with_stack`). An arm that is dead on one path and live on the + other is NOT deletable yet; say which those are rather than deleting them + and discovering it downstream. That set is the input to RQ-58-SPLIT. + status: proposed + release: v0.58 + tags: [north-star, subtraction, vcr-sel-001, byte-identical] + links: + - type: derives-from + target: BR-001 + - type: refines + target: NFR-002 + fields: + req-type: functional + priority: must + verification-track: frozen-anchor + issue: "#242" + + - id: RQ-58-WILDCARD + type: system-req + title: "105 wildcard arms in the instruction selector — the same class as #946, unmeasured" + description: > + instruction_selector.rs carries 105 `_ =>` arms. v0.57 fixed exactly one + instance of this class (writes_sp, 175 of 222 variants absorbed, #969) and + found it was LIVE — three priced ops reached it — while the numbers + happened to be right for a reason nothing checked. + The selector's wildcards are the same shape with a worse consequence: a + missed op there is a MISCOMPILE or a silent decline, not a loose bound. + #615 (the A32 silent-NOP class) is the precedent and the pattern to reuse: + expand-or-loud-reject, plus a no-wildcard tripwire that fails to COMPILE + when a new variant appears. + DO NOT sweep all 105 blindly. Rank them first: which absorb WasmOp + variants (miscompile risk), which absorb internal enums (lower risk), + which are genuinely total. Convert the miscompile-risk set; state the + count converted and the count deliberately left with a reason. A partial + conversion with an honest denominator beats a claimed sweep — that is the + #935 lesson applied to refactoring. + EXPECT to find live holes. v0.57's writes_sp lane expected latent and + found live. + status: proposed + release: v0.58 + tags: [soundness, exhaustiveness, tripwire, wildcard, selector] + links: + - type: derives-from + target: BR-001 + - type: refines + target: NFR-002 + fields: + req-type: functional + priority: must + verification-track: execution-differential + issue: "#946" + + - id: RQ-58-MIRRORS + type: system-req + title: "57 files say 'mirror', 1 says 'single source of truth' — generate, don't mirror" + description: > + The rot class this repo keeps paying for, now counted. 57 source files + mention a mirror, 11 a hand-maintained list, exactly ONE claims a single + source of truth. + v0.57 alone: the aarch64 decline list went stale TWICE and still named a + capability that release SHIPPED; exec_trap_subset_op's allowlist drifted + so three ops delegated to a model that did not implement them; + `referenced_locals` existed in THREE backend copies until #974 collapsed + it; and the FEATURE_MATRIX template carried three stale numbers behind a + green 43/43 because the freshness gate compares the RENDER to the + TEMPLATE and never the template to the CODE. + VCR-ISA-001 already proved the fix works — #667 made the shipped + sel_dsl::RULES table EMIT the Rocq model, so selector/model drift became + unrepresentable rather than merely tested-for. + DO: inventory all 57, rank by rot-risk (does a stale copy cause a wrong + ANSWER, or only a wrong doc?), and convert the top-ranked ones to + generated-from-one-source. Fixing the FEATURE_MATRIX freshness gate so it + can see template-vs-code drift is in scope and is the highest-leverage + single item, because it is the gate that hid three of the others. + Report the inventory even for the ones not converted — an unconverted + mirror that is NAMED is a known risk; an unnamed one is the next #975. + status: proposed + release: v0.58 + tags: [north-star, generate-dont-mirror, doc-rot, vcr-isa-001] + links: + - type: derives-from + target: BR-001 + - type: refines + target: NFR-002 + fields: + req-type: functional + priority: must + verification-track: static-analysis + issue: "#242" + + - id: RQ-58-SELDSL + type: system-req + title: "Un-stall VCR-SEL-001: 50 -> 70 rules, and each one DELETES its arm" + description: > + The rule count has been 50 since v0.50 — seven releases flat — while the + selector it replaces grew 1,197 lines. Restart it, under the new + definition of done. + Each new rule must land WITH the deletion of the hand-written arm it + supersedes, in the same PR. A rule that ships without its deletion is the + pattern that produced the current state and is not accepted here. + Pick the next 20 ops by SUBTRACTION VALUE, not by ease: prefer ops whose + hand-written arm is large, wildcard-adjacent, or duplicated across the two + selectors. State the selection criterion and the lines deleted per rule. + HONEST CONSTRAINT: some ops will not be expressible in the DSL as it + stands. That is a real finding about the DSL's expressiveness and should + be reported as such — with the specific construct that defeats it — + rather than quietly reducing the target from 20. + status: proposed + release: v0.58 + tags: [north-star, vcr-sel-001, rocq, subtraction] + links: + - type: derives-from + target: BR-001 + - type: refines + target: NFR-002 + fields: + req-type: functional + priority: should + verification-track: proof + issue: "#242" + + - id: RQ-58-SPLIT + type: system-req + title: "instruction_selector.rs is 29,616 lines — split it along the seam that already exists" + description: > + 18,481 lines of code plus 11,135 of tests in ONE file. Nobody can hold it, + which is why wildcards accumulate in it and why two selectors could + diverge inside it unnoticed (#946's own scanner got this wrong: it claimed + `--relocatable` forces `select_default`, when it forces the DIRECT + selector, which IS `select_with_stack` — direct is not default). + The seam is not invented, it is already there: the two-selector split + (#197). Separate the shared lowering core from the two path-specific + layers so the difference between them is READABLE rather than + archaeological. + GATE: byte-identical output across all frozen anchors and differentials. + A pure move must not change a single emitted byte, and if it does the + move is wrong. Commit per moved unit so a bisect is meaningful. + SEQUENCING: runs AFTER RQ-58-RETIRE, so the file is smaller and the + dual-path residual it names is known before anything moves. + SCOPE HONESTY: this is the lane most likely to be partially completed. A + half-finished split with a stated boundary is acceptable; an unstated one + is not. + status: proposed + release: v0.58 + tags: [structure, two-selector, byte-identical, readability] + links: + - type: derives-from + target: BR-001 + - type: refines + target: NFR-002 + fields: + req-type: functional + priority: should + verification-track: frozen-anchor + issue: "#197" + + - id: RQ-58-SELECT973 + type: system-req + title: "ARM select on an i64-comparison with computed arms returns the then-arm — and CI never compiles ARM fixtures" + description: > + #973, found in v0.57 only because a lane compiled the repro corpus for + ARM. The miscompile: `select` on an i64-comparison condition with COMPUTED + arms always returns the then-arm — the spill reload puts the then-value + into the live else-arm register and both `it` arms move the same one. + Proven independent of #974 (identical 44/49 on binaries built before and + after that fix). + THE BIGGER FINDING IS THE SECOND HALF: it surfaced only because someone + compiled ARM fixtures, WHICH CI NEVER DOES. A whole backend's fixture + surface is uncompiled in CI. Fixing the miscompile without closing that + gap leaves the next one equally invisible, so BOTH are in scope: the fix, + red-first with an execution differential, AND an ARM leg for the corpus + sweep with a declared floor. + status: proposed + release: v0.58 + tags: [soundness, miscompile, arm, ci-gap, select] + links: + - type: derives-from + target: BR-001 + - type: refines + target: NFR-002 + fields: + req-type: functional + priority: must + verification-track: execution-differential + issue: "#973" + + - id: RQ-58-VERIFYWIRE + type: system-req + title: "synth verify still declines shift rules for a gap #975 closed" + description: > + #981. `i32.shl` reports `declined immediate-shift-encoding`, and the + stated reason — "SMT modeling of the variable-shift register encoding is + an open gap" — became false in v0.57: #975 modelled LslReg/LsrReg/AsrReg/ + RorReg faithfully as Rm<7:0> (ARMv7-M A7.7.68/70/12/117) and moved five + lowerings Invalid -> Verified. The comments were corrected at release + assembly; the WIRING was deliberately left, because rewiring the rule + table is a verification-surface change and not release work. + Route the shift rules to the modelled ops and remove the decline, or + narrow it to whatever sub-case genuinely remains and state THAT reason. + RED-FIRST, and the trap is specific: "verify still passes" is not the + evidence. The evidence is the DECLINED COUNT dropping and the newly + checked rules returning Verified FOR THE RIGHT REASON — #975's own + measurement is the template, since it found i32.add returning Verified + when it should not have. + Worth stating because it is the general lesson: a decline that is too + conservative is INVISIBLE. Nothing reds, no test fails, the tool quietly + checks less than it could while its stated reason drifts from the truth. + status: proposed + release: v0.58 + tags: [verification, decline-honesty, wiring, arm-semantics] + links: + - type: derives-from + target: BR-001 + - type: refines + target: NFR-002 + fields: + req-type: functional + priority: should + verification-track: static-analysis + issue: "#981" + + - id: RQ-58-OBJECT + type: system-req + title: "object 0.39 -> 0.40 is a breaking 0.x-minor on the crate the differentials depend on" + description: > + #938. Currently failing Test AND Clippy, with auto-merge disabled by hand + during v0.57 — because the 0.x-minor hold COMMENTED but did not ENFORCE + (filed as #965, and it is a gate-that-cannot-fail instance in its own + right). + `object` is not incidental: it is what the execution differentials read + ELF symtabs with, and what #959 moved `disasm_words` onto to kill a + host-dependent `synth disasm` parse. A breaking bump landing unverified + would surface as oracle failures far from their cause. + Per the 0.x-minor rule this needs a FULL suite green — including the + feature-gated paths (`--features z3-solver`), since a feature-gated build + hides unhandled match sites. Either land it with that evidence or pin + `object` with a stated reason. #965 (make the hold enforce) is the + companion and should land first or alongside. + status: proposed + release: v0.58 + tags: [dependencies, breaking, 0x-minor, differentials] + links: + - type: derives-from + target: BR-001 + - type: refines + target: NFR-002 + fields: + req-type: functional + priority: should + verification-track: static-analysis + issue: "#938" + + - id: RQ-58-FLAKE + type: system-req + title: "shift_mask_elide_686 reads a non-ELF — and the silent direction is reading a STALE one" + description: > + #977, second sighting (#960 and #974, both in files those PRs never + touched, and on #974 the SAME test passed in the required Test job while + failing in the coverage job on the identical commit — which points at the + environment, not the assertion). + Why it outranks an ordinary flake: `parse elf: Could not read file magic` + means the harness read something that is empty or not an ELF. That is one + step from reading a STALE ELF and PASSING — the silent direction, and + exactly the v0.56 trap where a failed compile wrote nothing and the + previous run's object got executed. + FIX SHAPE: assert the compile's exit status and the file's non-zero size + BEFORE parsing, so a bad compile reports as a bad compile; and give the + fixture a process-scoped temp path if the collision hypothesis holds. + That converts a confusing flake into a precise message and closes the + silent direction at the same time. + status: proposed + release: v0.58 + tags: [flake, stale-artifact, harness, silent-direction] + links: + - type: derives-from + target: BR-001 + - type: refines + target: NFR-002 + fields: + req-type: functional + priority: should + verification-track: static-analysis + issue: "#977"