Repository navigation
plan(v0.70): scope the release — "Evidence you can re-derive" (7 artifacts, every candidate measured against source first) - #1336
Merged
Merged
Conversation
…facts, every candidate measured against source before it was written) Two MUSTs, both cpetig (EXTERNAL reporter), both reproduced on main with their own command lines; five SHOULDs, four of them found by v0.69's clean-room review and verified at source before being written. MUSTs — who is blocked: RQ-70-NPA #1331 --native-pointer-abi cannot lower static-data f32 load/store. MEASURED: 6 of 22 functions skipped, 4 of 6 EXPORTS skipped, rc=1 via #952, NO object emitted. The issue excerpt shows 2 — the same undercount shape as #1318 (2 vs 7). The embedder-init workaround was verified on THIS module (rc=0, 0 skipped, 28409 bytes), so the gap is specific to the ABI. RQ-70-ALIAS #1321 VCR-RA-003 SpillSlotAliased{184,...} is now THE blocker for cpetig's export: v0.69 raised the capacity ceiling (pool-grow(194) -> ok) and the validator refuses the stream. Slot 184 is i32 LOCAL 31, not f32 local 45 — the v0.69 diagnosis was corrected at the cut and the mechanism is store->reload forwarding with DSE blocked by unmodelled F32 ops. SHOULDs — gates that report success about work they did not do: RQ-70-CITEGAP #1333 artifact_citation_check globs artifacts/*.yaml NON- recursively: 30 of 127 files, 0 v0.69 artifacts. It has never scanned a release artifact since v0.61. RQ-70-WINDOWVAC #1334 status_evidence's delivery window matched ZERO commits for two releases. 8 RQ-NN deliveries do not match the shape; the 6 that do are release/chore/plan and not in DELIVERY_TYPES. CI only reds on SKIPPED. RQ-70-DONEWHEN #1335 9/9 done-when are `manual:`, so R3 cannot fire; 100% since v0.66. The conformance gate counts DECLARATION, not evaluation. RQ-70-PAGELIB #1315 the page-size refusal is CLI-only; synth-core decodes page_size_log2 and does not refuse, so a PUBLISHED- library caller still gets it silently ignored — the shape #1317 closed in the same release. RQ-70-FALCONCORPUS #1318 FALCON's headline numbers are not re-derivable from the repo: the reporter's modules were never committed. Two corpus definitions (207x5 and 193x5) were both called "the corpus". THE ANCHOR MOVES IN THIS PR, which is the only place it may move: ANCHOR_TAG v0.68.0 -> v0.69.0, ANCHOR_DELIVERY 80 -> 88, ANCHOR_PROGRAMME 433 -> 442 — all three DERIVED by the checker itself, not remembered — plus the matching claims.yaml pin. status-evidence-anchor now reports lag 0. Gates on this tree: status_evidence 0 (155 artifacts, 0 failures), claim_check 75/75, oracle_wiring 0, check_version_pins 0, artifact_citation 0, and both anchor unit-test suites pass. Refs #1331 #1321 #1333 #1334 #1335 #1315 #1318 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…out a set rivet can diff, and the diff nobody ran reports 22 new warnings
Raised by the maintainer after the v0.69 tag: the release notes should carry a
rivet-DERIVED section. They did not, and running `rivet diff` now shows why that
mattered.
MEASURED with the CI-PINNED rivet 0.37.0, v0.68.0 -> v0.69.0:
9 added, 0 removed, 0 modified, 575 unchanged
0 new errors, 0 resolved errors, 22 NEW WARNINGS, 0 resolved
The nine additions are the release's nine artifacts with their titles — a
derived table of contents no human wrote. The 22 warnings are the finding, in
three classes, none surfaced by any v0.69 gate:
(a) ALL NINE IDs cannot be commit-trailer references — "trailers need an
uppercase-alphanumeric prefix and an all-digit suffix, e.g. REQ-001".
No RQ-NN artifact is traceable through commits at all.
(b) `req-type: process` is not in the schema's allowed set — 4 of v0.69's 9,
53 occurrences repo-wide. A convention the schema never accepted.
(c) all nine lack an incoming `verifies` link, so the right side of the V is
open for every artifact this release shipped.
(a) IS THE SAME ROOT CAUSE AS RQ-70-WINDOWVAC (#1334), FOUND INDEPENDENTLY BY A
SECOND TOOL: status_evidence's window matches zero commits because
"RQ-69-SUBTRACT (#242): ..." does not fit its conventional-commit regex, and
rivet says the same IDs cannot be trailer references. One naming decision, two
traceability mechanisms silently disabled. Scope them together.
A VERSION NOTE THAT IS ITSELF A FINDING: the first run used the `rivet` on PATH
(~/.cargo/bin/rivet, 0.32.0) — exactly the shadow #1236 pins and #1308 reports
on the runners. The maintainer corrected it to the CI-pinned 0.37.0. The
artifact delta is identical, but the versions disagree about validate: 0.32.0
reports "0 broken cross-refs" where 0.37.0 reports "cross-refs NOT CHECKED —
externals failed to load". The older 0 was the vacuous reading; the upgrade
landed in v0.69 (#1324) and made it honest.
v0.70 is now 8 artifacts. Gates on this tree: status_evidence 0, claim_check
75/75; artifacts strict-loaded with a duplicate-key-strict loader.
Refs #1337 #1334 #1308
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 was referenced Sep 22, 2026
avrabe
added a commit
that referenced
this pull request
Sep 22, 2026
…rtifacts, every candidate refuted against source first), and MOVE THE ANCHOR to v0.70.0 (#1350) THE ANCHOR MOVES HERE BECAUSE NOTHING ELSE FORCES IT. ANCHOR_TAG/ANCHOR_DELIVERY/ ANCHOR_PROGRAMME go to v0.70.0 / 90 / 451, all three DERIVED rather than typed: the placeholders were set to 0 and the checker reported the real counts ("90 id-first delivery commits reachable from the tag", "451 artifacts in the tree at the tag"), then those were pinned. The matching claims.yaml pin moves with them — claim_check reds until it does, and it did. The waiver channel (PROGRAMME_DELETED_SINCE_ANCHOR) is already 0. EVERY CANDIDATE HAD ITS REFUTING COMMAND RUN AGAINST SOURCE BEFORE IT WAS WRITTEN, and three were reshaped by the answer: - STACKDEPTH (#1341, cpetig): the reporter's proposed mechanism is UNSOUND AS STATED. "If --emit-wcet already walks the call graph, the same traversal would yield the depth" — the traversal is right, the arithmetic is not. wcet_compose composes `total = own + Σ multiplier × callee_total` where multiplier is the PROVEN EXECUTION COUNT, so a callee invoked 1000× in a loop is charged 1000× the stack it actually uses. Stack depth is a MAX over the call tree, not a trip-weighted sum. Over-reporting is not the safe direction: an embedder told 2 MB for a 2.3 KB requirement stops believing the number. Also measured: `frame_size` appears in NO wcet_*.rs file. - ISLANDS (#345/#1331, cpetig): MISNAMED as filed. arm_backend.rs:1727's `imm12 > 4095` refusal is CORRECT — Thumb-2 LDR(literal) has that range and failing beats miscompiling. What broke is "these function bodies are far smaller" beside a pool APPENDED AT THE END, one per function. The lane is CONSTANT ISLANDS, not a range fix. - VFPALIAS (#881): SHARPENED, not assumed. The VFP twin already tracks src_word + src_version and treats a provably-identical re-store as benign, so it already defends the case the integer check could not. The open question is narrower, and the lane may end in a published REFUTATION. Two candidates were measured during the v0.70 cut by being hit: - MUTANTDRIFT (#1189): a mutant pinned by file:line:col is invalidated by any edit ABOVE it. v0.70's liveness.rs change moved a pinned site 7346 -> 7350 and the gate reddened saying "survivors must reproduce". `reanchor` fixes it; `grep -c reanchor .github/workflows/ci.yml` = 0. - ISSUESCOPE: R11 correctly forbids a `disposition:` beside a claiming status, so an artifact whose scope IS delivered while its ISSUE stays broader can say so only in prose. Comparing field key sets across v0.70's close-set and keep-open set, NO existing field separates them. MUSL (#1349) is recorded with v0.70's own measurement: its shipped Linux asset reports GLIBC_2.39, run through the issue's own two commands on the published tarball. v0.70 ships with the same floor and its report says so. THIS RELEASE DIRECTORY HAS A `_release.yaml`. v0.70's did not — #1336 omitted it, and status_evidence's R0 constrains the file only IF PRESENT, so the gap was invisible. v0.70's cold review found it and deliberately did NOT back-fill one, because it is a plan-time document and writing one at a tag manufactures the evidence. It is written here, at plan time, comments-only as R0 requires. DONE-WHEN: 8 declared, 6 MECHANICALLY EVALUABLE, 2 manual. The first draft was 100% `manual:` — which is exactly the habit RQ-70-DONEWHEN measured and criticised (v0.66-v0.69 each shipped 100%, a rate R3 can never fire on, printed as though it were evaluation). Writing the plan that way would have repeated the finding inside the plan that names it. ARCHMODEL and PAGELIB stay manual because they genuinely are: spar#445 and gale/#1145 are external. ARCHMODEL's TAGS ARE CHECKED, NOT ASSUMED: [process, carried, spar, aadl, feature-loop]. v0.69's equivalent lost `feature-loop` and the deferral became invisible to the conformance gate's steps-1-2 slot, which matches `feature-loop` AND (`aadl`|`spar`). Its description also warns against reintroducing "release artifacts only exist from v0.63", which is FALSE, was retracted in v0.69, and came back in v0.70. claim_check 75/75, status_evidence + check_version_pins + oracle_wiring + artifact_citation all rc=0, and the four gate unit-test suites rc=0. No Rust changed. Refs #1341 Refs #345 Refs #1349 Refs #1189 Refs #881 Refs #1339 Refs #1136 Refs #1250 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L 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.
Scopes v0.70 — "Evidence you can re-derive". Seven artifacts. Every candidate was measured against source before it was written, and the two musts were reproduced with the reporter's own command line.
Musts — ordered by who is blocked
Both are cpetig, a real external reporter.
--native-pointer-abicannot lower static-dataf32.load/f32.store: 6 of 22 functions skipped, 4 of 6 exports, rc=1, no object emitted. The issue excerpt shows 2 — the same undercount shape as #1318 (2 vs 7). The embedder-init workaround was verified on this module (rc=0, 0 skipped, 28409 B), so the gap is specific to the ABI.VCR-RA-003 SpillSlotAliased{184,…}is now the blocker for their export — v0.69 raised the capacity ceiling (pool-grow(194) -> ok) and the validator refuses the stream. Slot 184 is i32 local 31, not f32 local 45; v0.69's diagnosis was corrected at the cut.Shoulds — four are gates that reported success about work they did not do
All four came out of v0.69's clean-room review and were re-verified at source here.
artifact_citation_checkglobsartifacts/*.yamlnon-recursively: 30 of 127 files, 0 v0.69 artifacts. It has never scanned a release artifact since v0.61. The fix must be red-first.release/chore/plan, none a delivery type. CI only reds onSKIPPED, so0is green.manual:, so R3 cannot fire; 100 % since v0.66. The conformance gate prints "9/9 done-when" by counting declaration, not evaluation.synth-coredecodespage_size_log2and doesn't refuse, so a published-library caller still gets it silently ignored — the shape safety-bounds pmp: still an alias in the synth-core library (SafetyBounds::parse), and the AArch64 refusal names mpu #1317 closed in that same release.The anchor moves here — the only place it may
ANCHOR_TAGANCHOR_DELIVERYANCHOR_PROGRAMMEAll three derived by the checker itself (I set a placeholder and let it report the real counts), plus the matching
claims.yamlpin — whichclaim_checkimmediately failed on until it moved, exactly as designed.status-evidence-anchor: v0.69.0 — 88 delivery commits (pinned 88), 442 artifacts (pinned 442), lag 0Gates
status_evidence0 (155 artifacts, 0 failures) ·claim_check75/75 ·oracle_wiring0 ·check_version_pins0 ·artifact_citation0 · both anchor unit-test suites pass · artifacts validated with a duplicate-key-strict YAML loader and everydone-whenchecked well-formed.🤖 Generated with Claude Code
https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L