Repository navigation
plan(v0.60): scope the release — "Derive what you check against", 8 artifacts - #1070
Merged
Merged
Conversation
Five artifacts. Both halves of the theme were EARNED during v0.59 rather than asserted, which is why this file leads with the evidence: RQ-60-CANARY VCR-TIER-001 increment 1 (delivered, PR #1061). Its immediate finding is the theme's best argument: the census's OWN hand-maintained `declared_temps` column declared the #1048 miscompile LEGAL — `&[R5]` (rm_hi) for the i64 shifts, `&[R3]` (rnhi) for the bit-counts, exactly the registers the defect clobbered. A checker that mirrors the defect it exists to catch. RQ-60-CFOBLIG #1057 (gale). 48% of a real object is covered by NEITHER proof half, and the cause is one level deeper than the issue could see: `Inductive wasm_instr` has NO control-flow constructor at all. There is no obligation for `BrIf` because the model has no `BrIf`. Verified before scoping — gale asked to be corrected and was right to. RQ-60-A64IMPORT VCR-REACH-002. AArch64 accepts 13/805 real modules (1.6%). Import dispatch (~121 modules) is synth's OWN ARM `--relocatable` undefined-symbol design ported, so it is a port of a shipped pattern, not a design question. RQ-60-RACOST VCR-RA-011. Cost model + tied operands, NOT a better search — with the ruled-out alternatives recorded so they are not re-litigated. RQ-60-ARTIFACTSPLIT #1059. The single-file artifact write surface that silently dropped a trace link during the v0.59 wave. Validated with the TYPED oracle, not a permissive one — the lesson from the v0.59 corruption this file's last artifact is about: rivet validate: OURS=0 (main baseline 0; rivet FAILs on main by construction) duplicate-key-STRICT loader: 5 artifacts, no duplicate ids structural: every artifact carries its own links: and a non-empty issue: release field consistent: {v0.60} The structural check is the mitigation RQ-60-ARTIFACTSPLIT proposes, run here by hand against this file. Refs #1021, Refs #1057, Refs #1017, Refs #242, Refs #1059 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
I wrote release-v0.60.yaml by copying v0.59's shape, so it carried the exact defect #1064 is about: top-level `metadata:` + `requirements:` instead of `artifacts:`. rivet's generic-yaml DENIES unknown top-level fields, so the whole file was skipped with a WARN carrying no `ERROR:` prefix. Which means my own validation of this file was VACUOUS. I ran `rivet validate`, got OURS=0, and reported it clean — but rivet had skipped the file entirely. Zero errors from a file that never loaded is not zero errors. Same shape as #1012 one level up, and the reason #1064's fix pins a FLOOR on artifacts loaded rather than only grepping for errors: a validator doing LESS work must fail, not pass quietly. Converted metadata: -> comments (v0.58's shape), requirements: -> artifacts:. Verified BY ID rather than by absence of an error — the distinction that hid this in the first place: RQ-60-CANARY -> RQ-60-CANARY (system-req) [proposed] RQ-60-CFOBLIG -> RQ-60-CFOBLIG (system-req) [proposed] RQ-60-A64IMPORT -> RQ-60-A64IMPORT (system-req) [proposed] RQ-60-RACOST -> RQ-60-RACOST (system-req) [proposed] RQ-60-ARTIFACTSPLIT -> RQ-60-ARTIFACTSPLIT (system-req) [proposed] CI-filter OURS = 0. Artifact count on this branch 447 -> 452 (+5); once #1065 lands the v0.59 fix the same 5 lift 463 -> 468, so this PR must raise ARTIFACT_FLOOR to 468 when it rebases onto #1065. All 5 already derive-from BR-001 (the correct stakeholder-req type), so unlike v0.59 no link retargeting is needed. Refs #1064 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… for internal functions gale (fathom) measured it on the E2 dissolved gust:os composite: synth-wcet-v1 takes its `name` from the EXPORT SECTION and falls back to `func_<index>` for every internal function, so 7 of 13 `loop` declines cannot be hinted at all — and `loop` is 13 of 28 declines with 11 `callee-unbounded` cascades behind it. WORSE THAN "NOT HINTABLE": a hint keyed on `func_22` SILENTLY RETARGETS when an edit shifts the index space. It still parses and still keys onto a function — just not the one the author verified. synth always emits its own DERIVED ceiling rather than the raw hint, so the bound stays synth-derived; what a mis-keyed hint corrupts is the OPT-IN, converting a decline for a function whose shape nobody looked at. An index is not an identity. gale pre-empted the obvious dismissal: rebuilding with `meld fuse --preserve-names` yields a BYTE-IDENTICAL .wcet.json while populating the name section 0 -> 59 of 68. synth carries the names and ignores them. Recorded with the caveat they volunteered, because it must shape the design: the names are v2 Rust mangling carrying a NON-content-derived crate disambiguator, and scry measured 43-45% of their function identities churning per build for exactly that reason (scry#123/#137). Better than an index, still not stable — fixing the blocker with a key that churns every build would trade an unaddressable decline for an unreliable one. Their kill-criterion adopted verbatim: a hints file keyed on the name-section name of one of those seven converts its `loop` decline to `hint-verified`, or is rejected with a NAMED reason. Being ignored because the key never matches is the failure. Validated the way #1064 taught — BY ID, not by absence of an error: all 6 v0.60 artifacts resolve via `rivet validate --explain`; CI-filter OURS=0; duplicate-key-strict loader clean; every artifact carries its own links: and issue:. Refs #1063 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…pervised release Measured on v0.59, in a release where I was EXPLICITLY watching for this class because v0.58 had been burned by it: RQ-59-TIERCENSUS #1047 merged; no open PR flipped it RQ-59-GLOBALINIT #1058 merged; no open PR flipped it RQ-59-PARTIALCENSUS #1051 merged and did not flip its OWN status All three caught by hand and folded into unrelated PRs. Three misses in one supervised release is a coupling problem, not an attention problem: nothing mechanically ties "the code landed" to "the artifact says so". It fails SILENTLY and in the direction that looks like LESS work — a stale `proposed` makes v0.58's release-readiness query under-report scope at the cut, so a shipped artifact can be omitted from the notes and the evidence package. The compounding factor is why this is not just "add a checklist": #1064 showed the v0.59 file was never LOADED by rivet, so for most of the release the readiness query could not have caught a stale status even if run. The two defects hid each other — the file was invisible, so the statuses inside it were unfalsifiable. Three candidate fixes recorded with their tradeoffs rather than one asserted; deriving status from evidence is most in keeping with this release's theme, a CI check that a MERGED-PR artifact is not still `proposed` is the cheapest thing that would have caught all three. Kill-criterion: replay v0.59's three misses — a fix that would not have caught all three has not addressed the measurement. Validated BY ID: RQ-60-FLIPCOUPLE resolves; CI-filter OURS=0. Refs #1064 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…a complete falcon M7 cascade
jess filed it with a fully public repro and measured it on a real RT1176 Renode
model (memory byte-exact, 214,696 instructions retired). 2 of 5 cascade stages
export; the loop cannot close on target without the other three.
VERIFIED ALL THREE CLAIMS against current code before scoping — they measured
0.55.0, we shipped 0.59.0:
* the S pool IS `[bool; 16]` = S0..S15; callee-saved S16..S31 / D8..D15 are
absent and would roughly double it
* NO __aeabi_ul2f/l2f/ul2d/l2d routing exists anywhere; #869's acceptance
comment described exactly that route and inline-f64 shipped instead
* has_double_fpu() gates f64 on FPUPrecision::Double, i.e. m7dp only
REPRODUCED ON 0.59.0, minimal case sharper than the cascade:
(func (param i64) (result f32) (f32.convert_i64_u (local.get 0)))
m4f -> DECLINED "scalar f64 requires a double-precision FPU target"
m7dp -> compiles
A function with NO f64 in its signature is refused for needing f64, because our
own lowering introduces it. A reach failure of our own making.
HONEST RESIDUAL IN MY OWN VERIFICATION, recorded so a lane does not inherit a
false premise: sub-problem 1 (S-exhaustion) is confirmed by CODE INSPECTION
ONLY. My deep-f32 fixture compiled fine at 60 bytes — not deep enough to exhaust
S0..S15. A lane must build a fixture that actually reddens phase 1 before
claiming to fix it.
Refs #1069, Refs #869
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
The gate's own rule: a PR that ADDS artifacts raises the floor in the SAME PR, so every movement is a visible diff. 464 (main) + 8 (release-v0.60.yaml) = 472, measured under the job's own conditions rather than assumed. Re-verified the guard is still POTENT at the new value rather than assuming potency carried over — a raised gate that no longer fires is worse than the omission it was raised for: GREEN: measured=472 floor=472 RED : reintroduce the #1064 metadata:/requirements: schema defect -> measured drops below 472 -> FIRES Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
v0.59.0 shipped today. This scopes v0.60.
Theme: derive what you check against, and reach is part of correctness. Both halves were earned during v0.59 rather than asserted, which is why the file leads with the evidence.
The 8 artifacts
RQ-60-CANARYdeclared_tempscolumn declared the #1048 miscompile legal (&[R5],&[R3]— exactly the clobbered registers). A checker that mirrored the defect it existed to catch.RQ-60-VFPPRESSURE__aeabi_*conversion routing exists, and a function with no f64 in its signature is refused for needing f64 because our own lowering introduces it.RQ-60-A64IMPORT--relocatablepattern ported.RQ-60-CFOBLIGwasm_instrhas no control-flow constructor at all, so it's a model extension, not a proof effort.RQ-60-WCETKEY--wcet-hintshas no key for internal functions; a hint keyed onfunc_22silently retargets when indices shift.RQ-60-RACOSTRQ-60-ARTIFACTSPLITRQ-60-FLIPCOUPLEThree came from siblings (jess, gale) with public repros and measured numbers; each was verified against current code before scoping, and where my verification fell short I said so in the artifact rather than inheriting a false premise.
Floor raised in the same PR
ARTIFACT_FLOOR464 → 472 — the gate's own rule is that a PR adding artifacts raises the floor in that PR, so every movement is a visible diff. Measured under the job's own conditions, not assumed.Re-verified the guard is still potent at the new value rather than assuming potency carried over:
Validated the way #1064 taught
All 8 artifacts resolve by id via
rivet validate --explain, not by absence of an error — the distinction that hid an entire release's scope from the readiness query.CI-filter OURS=0, duplicate-key-strict loader clean, every artifact carries its ownlinks:andissue:.