plan(v0.57): close RQ-57-BACKFILL by disproving its method, + re-grade 4 shipped artifacts - #979
Merged
Merged
Conversation
…e 4 shipped Two things. The re-grades are bookkeeping; the back-fill is a finding. RE-GRADED to `implemented` (work merged on main): RQ-57-COUNTPARAMS #970 (#974) ARM+RV32 conditional-param miscompile RQ-57-GPIO #846 (#976) gpio-thin 502 -> 494 B RQ-57-ARMSEM #923 (#975) ArmSemantics no-oped 87 of 222 ops RQ-57-MCDC #912 (#978) MC/DC over synth's own decision logic RQ-57-BACKFILL: the back-fill was NOT performed, on evidence. 263 of 288 artifacts carry no `release:`. The prescribed derivation — "the first tag containing the artifact" — RUNS FINE (0 undecidable, 24 distinct tags) and answers the WRONG QUESTION. It yields when an artifact ENTERED THE PLAN; `release:` means the release the work is TARGETED AT or SHIPPED IN. The file supplied its own control case, which is what settles it: VCR-RA-001, hand-set release: v0.24.0 <- when the work shipped VCR-RA-001, mechanical rule v0.11.30 <- introducing commit's tag It is the ONLY artifact in verified-codegen-roadmap.yaml that already carried a `release:`, and the rule contradicts it. Sweeping the other 32 would have written 32 false values with the one correct value sitting beside them as the disproof. Scale, had it been applied blindly: 190 of the 263 resolve to v0.1.1 — the initial import, i.e. the standing requirement base (architecture, stakeholder and system requirements, component model, target platforms). Tagging those v0.1.1 asserts the whole foundational base was targeted at the first tag, and makes "what is in v0.1.1?" return 190 artifacts including work that shipped forty releases later. That is the corruption of the readiness query this artifact exists to prevent — so the artifact's own guardrail ("stays unassigned rather than guessed", the #911 lesson applied to planning data) decides it. CONVENTION, now documented in docs/release-process.md so the absence stops being re-filed as an unfinished chore: * per-release plan artifacts carry `release:` (they are work items; they do) * standing artifacts carry it ONLY where the shipping release is known, as VCR-RA-001 does * setting it on a standing artifact is a per-artifact judgement with CHANGELOG evidence, never a sweep A missing `release:` is a justified state. A wrong one is worse than a missing one. rivet: 50 errors / 166 warnings before AND after — unchanged. claim_check 43/43. Refs #912 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! |
avrabe
added a commit
that referenced
this pull request
Aug 14, 2026
* chore(release): v0.57.0 assembly — "the checkers were the defects" Nine artifacts. In five of them the bug was in the machinery that checks the compiled code, not in the compiled code: #975 ArmSemantics silently no-oped 87 of 222 ops — a Rocq-proved, default-on rotl rule was "validated" by a model that executed neither of its instructions #976 the gpio differential CANNOT discriminate the miscompile it guards — complementary conditions, so no input to that driver can #969 writes_sp claimed exhaustiveness over a wildcard absorbing 175 of 222 #967 the "9 unattributed branches" were manufactured by witness's own hardcoded divergence text #979 the prescribed release: back-fill would have written 32 false entries, with the one correct pre-existing value beside them as the disproof The unifying property is that each of those checks COULD NOT FAIL. This release makes them able to fail and proves it by making them fail on purpose. Also fixed, and the most severe item: #974 — a conditionally-written parameter was demoted to a zero-init local on ARM and RISC-V. Exit 0, no decline, wrong code; on RISC-V it reads an UNINITIALISED stack slot (0xDEADBEEF under a poisoned stack), an information-disclosure shape. ARM behaves identically — which the issue predicted otherwise, and only execution settled. Release surfaces, all four swept and checker-confirmed at 0.57.0: Cargo.toml [workspace.package] + 10 path-dep pins MODULE.bazel, npm/package.json, Cargo.lock (cargo metadata) scripts/check_version_pins.py: OK Derived artifacts regenerated (--emit-status): artifacts/status.json, docs/status/FEATURE_MATRIX.md. Claim gate: 43/43. Open by design, named not hidden: #973 (ARM select miscompile, found only because a lane compiled ARM fixtures — which CI never does), #977 (ELF-magic flake, second sighting), #938 (breaking object 0.x-minor bump, auto-merge disabled), #912 (open with four remaining: items). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(release): act on the v0.57.0 cold review — 8 accuracy defects, 4 of them mine Cold review of the assembled release. Nothing blocked the tag; everything below is accuracy. Four of the eight were errors in the CHANGELOG I had just written, which is the reason the review exists. THE GENERALIZABLE FINDING, and it is pointed given this release's theme: `check_generated_fresh` byte-compares the RENDERED FEATURE_MATRIX against the TEMPLATE. `render_feature_matrix` only substitutes `{{...}}` fields, so the gate proves the render is faithful to the template — and NEVER that the template is faithful to the code. Every stale number below lives in template prose no substitution touches. In a release titled "the checkers were the defects", that is the checker that cannot fail. Three independent stale numbers survived a green 43/43. USER-FACING FALSE, verified by compiling rather than by reading: FEATURE_MATRIX listed "writing a PARAM local in a LEAF function" as a LOUD DECLINE on aarch64. #971 shipped exactly that. A leaf `local.set` on a param compiles: 32 bytes of machine code, exit 0. Also corrected in the same row: homing is no longer non-leaf-only, and the float-param decline widened with it. Fixed in the TEMPLATE (the render is generated) + regen. MY CHANGELOG ERRORS: * "145 of the 175 pre-declined / 30 reachable" matched no partition. The shipped source (wcet_loops.rs:1232) says 142 give up with `true`, leaving 33. Re-derived: 142/33. Corrected. * "demoted to a zero-initialised local" is wrong for the two backends the entry is about — zero-init is gated on first-access-being-a-READ, and in the cond-write shape the first access IS the write, so nothing initialises the slot. That is WHY it reads poison; the old wording made an information-disclosure bug sound like a benign wrong value, and contradicted the entry's own next sentence. * "Nine artifacts" — there are ten, and RQ-57-DOCSWEEP (#946/#968) had NO CHANGELOG entry at all despite touching CLAUDE.md, coq/STATUS.md, PROJECT_STATUS.md, the matrix template and eight source files. Added. * "Five in-tree oracles took that opt-in" — eight scripts plus three Rust tests. All eight carry floors, but `i64_param_518_riscv_loudskip`'s is `compiles >= 1`, which is a floor and NOT the "tight" one the paragraph claimed for the set. Named rather than folded into the claim. STALE COUNTS (the template-prose class above): ORACLE_WIRING.md, the matrix template and claims.yaml all said "137 oracles / 295,621 emulator entries". Re-derived independently — and the reviewer's number and mine agree exactly: 144 oracles / 296,059. Both `count-min` pins moved 137 -> 144 with them (same `emulations >=` pattern, two sibling claims); the pinned verbatim texts moved too, or the ledger would have gone red against its own corrected doc. REVERSE STALENESS (a doc calling SHIPPED work missing): `synth verify` declines shift rules citing "SMT modeling of the variable-shift register encoding is an open gap". #975 CLOSED that gap — it modelled LslReg/LsrReg/AsrReg/RorReg as Rm<7:0> (ARMv7-M A7.7.68/70/12/117) and moved five lowerings Invalid -> Verified. Both comments corrected to say what is true: the modelling gap is closed, the remaining decline is a WIRING residual. Behaviour deliberately unchanged — rewiring the rule table is a verification-surface change, not release assembly. Filed as #981. ARTIFACT: RQ-57-PROVGAP still asserted "9 object branches with no WASM origin" as fact while its own PR disproved it. Outcome recorded, as RQ-57-BACKFILL already did. docs/architecture/CRATE_STRUCTURE.md said 18 crates; there are 19. A RECURRENCE — PROJECT_STATUS.md cites this exact drift as why it was gutted in the #946 sweep, and one file over it was live again. Gates after: claim_check 43/43, check_version_pins OK at 0.57.0, cargo check -p synth-cli rc=0. Refs #980, #981 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * style: rustfmt the #975 decline-reason comment (indent 14 -> 12) My own miss: I ran cargo check on the edited file but not cargo fmt, and Format is a required context. The comment content is unchanged — only the indentation rustfmt wanted. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Re-grades are bookkeeping. The back-fill is a finding.
Re-graded to
implementedRQ-57-BACKFILL — not performed, on evidence
263 of 288 artifacts carry no
release:. The prescribed derivation — "the first tag containing the artifact" — runs fine (0 undecidable, 24 distinct tags) and answers the wrong question: it yields when an artifact entered the plan, whilerelease:means the release the work is targeted at or shipped in.The file supplied its own control case:
VCR-RA-001release:set by handIt is the only artifact in
verified-codegen-roadmap.yamlthat already carried arelease:, and the mechanical rule contradicts it. Sweeping the other 32 would have written 32 false values — with the one correct pre-existing value sitting beside them as the disproof.At scale it is worse: 190 of the 263 resolve to
v0.1.1, the initial import — the standing requirement base (architecture, stakeholder/system requirements, component model, target platforms). Tagging thoserelease: v0.1.1asserts the entire foundational base was targeted at the first tag, and makes "what is in v0.1.1?" return 190 artifacts including work that shipped forty releases later. That is precisely the corruption of the readiness query the artifact exists to prevent — so its own guardrail ("stays unassigned rather than guessed", the #911 lesson applied to planning data) decides it.Convention, now documented
In
docs/release-process.md, so the absence stops being re-filed as an unfinished chore:release:— work items by construction, and already do;VCR-RA-001does;A missing
release:is a justified state. A wrong one is worse than a missing one.Gates
rivet 50 errors / 166 warnings before and after — unchanged.
claim_check43/43.Refs #912
🤖 Generated with Claude Code
https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L