chore(rivet): flip RQ-61-A32RELOC and RQ-61-ORACLEFLOOR to implemented — their work shipped in #1116 and #1112 - #1120
Merged
Merged
Conversation
…d — their work shipped in #1116 and #1112 Both artifacts' `done-when` conditions are fully met by merged code, and both still read `proposed`. Caught by reading the release status, NOT by a gate. WHY NO GATE CAUGHT IT, which is the more interesting half. R4 fires on a first-parent commit whose SUBJECT STARTS WITH a known artifact id. Every lane PR in this release names its artifact first ("RQ-61-VCLOSURE (#1091): ..."), so R4 sees them. My own two commits used conventional-commit prefixes — "fix(oracle): ..." and "fix(#1040): ..." — so the subjects never matched, the artifacts stayed `proposed`, and status_evidence_check reported 0 failures the whole time. The gate is not wrong; it is blind to a delivery-commit shape that this repo also uses, and the blindness is silent in the direction that matters (work landed, artifact says nothing). This is the v0.59 "orphaned status flips" class recurring, and the same family as everything else in v0.61: a check that exists, is wired, and cannot see part of what it is for. Filed separately rather than fixed here. RQ-61-A32RELOC (#1040, PR #1116): A32 BL sites emit R_ARM_CALL (28), Thumb sites keep type 10, the #1021 harness's execution-mode workaround is removed — all three clauses. `verified-by` records the unfiled SECOND defect (the `eb000000` vs `ebfffffe` addend) and the real-linker evidence that the pre-fix object linked to `eaca0000` with the opcode corrupted from BL to B. RQ-61-ORACLEFLOOR (#1113, PR #1112): both oracles print `refusals: N`, return non-zero at zero, and ci.yml greps it; each proven red-first. `landed` records that the published count was corrected 4 -> 2 because two matches were toolchain probes, not decline assertions. status_evidence_check: 0 failures. claim_check: 54/54. Refs #1040, #1113 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… subjects (14 -> 15) Found while flipping the two artifacts in the previous commit: the reason nothing caught them is itself a gate blind spot, so it gets an artifact rather than a footnote. R4 anchors on the subject PREFIX. Lane PRs name their artifact first and are seen; conventional-commit subjects are not: RQ-61-A32RELOC #1116 "fix(#1040): A32 BL sites carry ..." unseen RQ-61-ORACLEFLOOR #1112 "fix(oracle): #1104 shadowed the ..." unseen Both shipped complete while status_evidence_check reported 0 failures. The artifact records what the fix must NOT break, so it is not re-litigated: the prefix anchor is what stops a passing cross-reference from reading as a delivery claim, and R4 must stay first-parent so a merged branch's internal commits do not each count as a delivery. Resolving through `fields.issue` is the only option that would have caught both instances, and it needs a marker discipline to avoid false positives on reverts and partial fixes. RED-FIRST IS FREE and required: b4860e4 and eefa19e are an already-measured regression corpus, and a fix that does not flag both has not fixed the reported thing. The done-when says so, and also requires the negative direction — it must NOT fire on a subject that merely cross-references an id. ARTIFACT_FLOOR 495 -> 496, re-derived with `rivet list`, not computed. Refs #1119 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
Sep 2, 2026
…tion floor — red-first on b4860e4/eefa19ef (+ RQ-61-EXTRACT flip) (#1124) * RQ-61-R4BLIND (#1119): R4-issue scope resolution + R10 window attribution floor — red-first on b4860e4 and eefa19e R4 only saw delivery commits whose subject STARTS with an artifact id, so two v0.61 artifacts shipped via conventional-commit subjects and stayed proposed with the gate green (#1119). Two rules, because the measured corpus refutes half of option 2 as filed: - R4-issue: a conventional-commit subject whose SCOPE names a fields.issue (fix(#1040): ...) resolves to that issue's highest-release holder and gets R4's acknowledgment demand. Scope-position ONLY — the description position is measured to name a CAUSE (eefa19e's #1104 is the PR that introduced the defect; resolving it would misattribute). Windowed to commits since the previous minor's tag, because fix(#1085) (#1090) is v0.60-era work on the issue RQ-61-EVIDENCE now holds — frozen history must not match the current issue map. - R10: eefa19e names neither its artifact nor its issue, so NO resolver can attribute it — but its silence can be NOTICED. Every delivery-typed (feat/fix/perf/proof/test) first-parent commit in the release window must be attributable to SOME artifact: a known id anywhere in the subject, a known issue anywhere, or its PR in any landed:/verified-by:. The red forces exactly the landed: line #1120 wrote by hand. RED-FIRST at 331bbd8 (last pre-flip commit, old gate 0 failures): the fixed gate reports exactly 2 failures — R4 RQ-61-A32RELOC (fix(#1040) / PR #1116) and R10 on 'fix(oracle): #1104 shadowed ...' (#1112) — and 0 on main after the flip. Negative direction: 0cb36bc (fix(rivet): ... RQ-61-VCLOSURE's ...) stays green — a mention is attribution, never a delivery claim; Revert / description-position / ambiguous-issue shapes all green (R4BlindSpot1119, 9 tests, mutation-verified: neutering SCOPE_ISSUE or DELIVERY_TYPES each kills tests). ci.yml greps the new status-evidence-window line so an underivable window is a CI red, not a quiet skip. Refs #1119 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * chore(rivet): flip RQ-61-EXTRACT to implemented — #1121's delivery re-verified clause by clause on main All three done-when clauses verified independently rather than from the PR body: the 98 snapshot .ml/.mli files across coq/, extracted/, validation/, compiler/ are gone from the tree (delivery diff deletes exactly 98); VALIDATION_STATUS.md is rewritten and no longer contradicts its own header (the 'Successfully implemented' / 'Complete and ready' body claims grep to nothing); the .v extraction target is untouched and CI's 'Bazel Build & Proofs' passed on PR #1121, with main green at the merge. Note for #1119: a5c75ca was never in the R4 blind class — its subject is id-first and its landed: names PR #1121, so old and fixed R4 both see and accept it. Refs #1080, #1121 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> 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.
Two artifacts shipped and still read
proposedBoth
done-whenconditions are fully met by merged code:done-whenRQ-61-A32RELOCRQ-61-ORACLEFLOORrefusals: N✓, return non-zero at zero ✓, ci.yml greps it ✓, each red-first proven ✓Why no gate caught it — the more interesting half
R4 fires on a first-parent commit whose subject starts with a known
artifact id. Every lane PR this release names its artifact first
(
RQ-61-VCLOSURE (#1091): …), so R4 sees them. My own two commits usedconventional-commit prefixes —
fix(oracle): …andfix(#1040): …— so thesubjects never matched, both artifacts stayed
proposed, andstatus_evidence_checkreported 0 failures the whole time.The gate is not wrong; it is blind to a delivery-commit shape this repo also
uses, and the blindness is silent in the direction that matters: work landed,
artifact says nothing, gate says green. Same family as #1085, #1091 and #1113.
Filed as #1119 rather than fixed here — it needs a red-first fix against
these two exact commits (
b4860e4e,eefa19ef), which are now a free,already-measured regression corpus.
What the flips record
RQ-61-A32RELOC'sverified-bykeeps the part that would otherwise be lost:the unfiled second defect (
eb000000vs gas'sebfffffe— a 0 addendresolves two instructions past the callee entry) and the real-linker evidence
that the pre-fix object linked to
eaca0000, opcode corrupted fromeb(BL)to
ea(B), so the link register was never set.RQ-61-ORACLEFLOOR'slandedrecords that the published count was corrected4 → 2, because two of the four matches were toolchain probes ("does this
clang accept rv32imac?"), not decline assertions.
Gates
status_evidence_check.py: 0 failures.claim_check.py: 54/54.Refs #1040, #1113, #1119