Repository navigation
RQ-61-R4BLIND (#1119): R4-issue scope resolution + R10 window attribution floor — red-first on b4860e4e/eefa19ef (+ RQ-61-EXTRACT flip) - #1124
Merged
Conversation
…tion 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
…-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
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 4, 2026
…ommit exactly as designed (#1147) Merging #1144 turned main red on R10: FAIL R10: delivery-shaped commit in the release window is attributable to NO release artifact: 'fix(ci): authenticate the federated externals sync ...' — no known artifact id or issue number in the subject, and no artifact's `landed:`/`verified-by:` names its PR (#1119: work landed, every artifact silent). That rule shipped ten commits ago in #1124, and this is the first time it has fired on real work. It fired on MINE, which is the right direction: I merged a CI fix with no artifact, and the gate refused to let the release plan stay silent about it. Fixed by creating the artifact, not by exempting the commit. RQ-62-FEDAUTH records the finding, which is worth more than the fix: THE ERROR MESSAGE ACTIVELY MISLEADS. "could not read Username for https://github.com" reads as a permissions failure. All seven siblings are PUBLIC, so an anonymous clone needs no credentials — git only prompts AFTER the transport refuses, and a throttled anonymous response on a tty-less runner surfaces as "No such device or address". The cause is a rate limiter on unauthenticated traffic, hardest from datacenter address space, which is where the self-hosted fleet lives. THE PASSES DO NOT PROVE THE FIX, recorded so nobody later claims they did. #1141 and #1142 passed WITHOUT it at 21:25; #1140 failed without it at 06:14; #1144 passed with it at 21:29. Every failure sits in one contiguous window and everything outside succeeds — the limiter eased on its own. The fix is still right for a reason those passes do not show: it removes the dependence on which side of a window a run lands. AN INTERMITTENT LIMITER IS WORSE FOR SIGNAL THAN A PERMANENT ONE. A job that flaps teaches maintainers to stop reading it — which is precisely what happened: I described this job's failure from memory twice in the org-wide review and was wrong both times. What the job got right and keeps: advisory so nothing was blocked, and it FAILS CLOSED — the non-vacuity guard was skipped rather than passing vacuously, the #1012 lesson working as designed. ARTIFACT_FLOOR re-derived at 519 with `rivet list`. Refs #1143, #1119, #1062 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Sep 6, 2026
…ced 1,892 below what it declared Found while cutting v0.62, on THIS RELEASE'S OWN NEW ORACLE, and confirmed independently by the release's cold review. THE DEFECT. `oracle_wiring_check.py --min-emulation-floor N` is the #910 ratchet; its own failure text states its purpose — "An oracle lost execution, or a floor was lowered." It enforced 322754 against a DECLARED total of 324640 at v0.61.0 and 324646 here: 1,892 emulations of slack, more than most single oracles declare. So an oracle could stay present, stay wired, stay referenced, and drop to ZERO executions while the gate built to notice exactly that reported green. DEMONSTRATED in an isolated worktree, not reasoned about: mutation 1 delete mem_isolation_red_1145.py whole -> exit 1, but by the DANGLING-CI-REFERENCE check, NOT the floor (total fell only to 324640, still above 322754). Two mechanisms, two different failures; only one is the ratchet's job and it was the one that could not fire. mutation 2 oracle stays wired, declares `emulations >= 0` -> exit 0. GREEN. The ratchet's stated failure mode, blind. after fix same mutation -> exit 1, "RATCHET BROKEN: summed floors 324640 < recorded minimum 324646"; unmutated tree exit 0, so the floor is CORRECT, not merely stricter. This is #1113 one level up: that was INTRA-oracle (a decline half contributing zero to its own floor, fixed per-oracle in #1112); this is INTER-oracle (the summed ratchet below the summed declarations). Same sentence — the floor cannot see part of what it asserts — at two scales, one release apart. The per-oracle fix was correct and did not imply the aggregate was tight; nobody checked, because every gate reporting on this floor reports it PRESENT AND WIRED, never TIGHT. The slack was INHERITED, never introduced — so the fix is an INVARIANT, not a number: enforced floor EQUALS declared total, pinned verbatim, a landing oracle bumps both in the same PR. claims.yaml's SYNTH-ORACLE-CHECK-FLOORS-910-CI pin caught the edit at 57/58 before it could ship silently. ALSO IN THIS COMMIT — two cold-review corrections: 1. A FALSE CLAIM I WROTE, propagated to three files. Release prose said the dynamic index in the #1102-residual fixture was load-bearing because "a constant index devirtualizes and the table never materializes." FALSE. Compiling a const-index call_indirect on ARM --relocatable emits `movw r2, #0` / bounds check / `ldr.w ip, [fp, ip]` / `blx ip` — a runtime table load and an indirect call, same shape as the dynamic case; synth has NO devirtualization pass at all (verified against emitted bytes, and no such code exists in the tree). The guard is index-insensitive and refuses the const-index dangling shape too, so the fix and its red-first evidence are UNAFFECTED — what was wrong is the RATIONALE, which is what a future contributor reasons from. Corrected in CHANGELOG.md, RQ-62-TABLEDANGLE.yaml and tabledangle_1102_elem.rs, each stating the correction rather than quietly deleting the sentence. 2. R10 ATTRIBUTION. The floor fix first landed with no artifact or issue anchor in its subject, and status_evidence_check R10 — the gate added in #1124 for exactly this — failed it: "delivery-shaped commit in the release window is attributable to NO release artifact." It was right. Fixed properly rather than by loosening: RQ-62-FLOORTIGHT is now a real v0.62 artifact carrying the finding, and this subject names it. Refs #910, #1102, #1113, #1124, #1145 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Sep 6, 2026
… and apply its four prose corrections The clean-room review record loop_conformance_check step 7 requires, written by an independent reviewer with no inherited framing, dispatched against 0a8c1e1. Its text is committed UNEDITED; the disposition table is additive. WHAT IT FOUND: 1 MUST-FIX, 1 SHOULD-FIX, 5 NOTEs, 4 unverifiable-as-stated, ~20 claims independently verified by execution — including a full re-run of the acceptance census from a freshly built binary (27/243, 40/243, 46/243 and every ranked blocker reproduced exactly), and a rebuild of the PRE-FIX compiler at 858ff8d^ to reproduce the #1102-residual hole end-to-end (object ships exit 0, links clean, zero UNDEF symbols). BOTH ACTIONABLE FINDINGS WERE MINE, AND BOTH ARE FIXED: MUST-FIX 1 the tip failed its own required Claim Check (R10, the rule added in #1124 for exactly this shape). Fixed by giving the work the artifact it deserved — RQ-62-FLOORTIGHT — not by loosening the rule. Now exit 0, 2 delivery commits, 2 attributed. SHOULD-FIX 1 a FALSE claim I wrote, propagated to three files: that a constant call_indirect index devirtualizes so the table never materializes. Re-verified against emitted bytes before acting rather than taking the review's word — `movw r2,#0` / bounds check / `ldr.w ip,[fp,ip]` / `blx ip`. It does not devirtualize; synth has no such pass. Corrected in all three places AS A STATED CORRECTION, so the wrong rationale cannot be re-derived from history. The fix and its red-first evidence are unaffected — only the rationale was wrong, which is the dangerous shape: a correct artifact resting on a reason a future contributor would reason from. NOTES 1, 3, 4 applied to the CHANGELOG, each narrowing a sentence that claimed more than the code or the data supports: - the diff-stat's scope is now stated (feature merges; release commit +213/-51 named separately) - the 81%->11% comparison now says the denominator differs (307 vs 243), that the subcounts come from the v0.59 artifact rather than this release, that per-module records were not preserved, and that the two subcounts may overlap - "fail-closed on unknown mnemonics" now says what the code does: undecodable instructions and zero-instruction scans always refuse; an unknown MNEMONIC refuses only when its operand text names a reserved register NOTE 5 (census hex-immediate collapse) is deliberately NOT fixed here and the disposition says why: no number in the release is wrong, and changing a measurement script mid-cut, under the oracle it feeds, risks the census for no gain. Carried to v0.63, where re-measurement is increment 1. Step 8's PR-head-vs-merge attestation slot is stubbed in the record with its rationale; it is filled at merge time. The gate labels it ATTESTED in both modes, so filling it is a deliberate act — an attestation with nothing behind it is the vacuity this release spent its scope finding. Refs #910, #1102, #1124, #1136 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Sep 6, 2026
…lemented (#1158) * release(v0.62.0): version bump, pin sweep, and release notes derived from merged code Theme: "Reach is part of correctness." Version 0.61.0 -> 0.62.0 across Cargo.toml (workspace + 10 path-dep pins), MODULE.bazel, npm/package.json, artifacts/status.json and Cargo.lock. Pin sweep green. CHANGELOG [0.62.0] written against MERGED CODE and claims.yaml ON THE TREE, not against PR bodies — the v0.57 cold review found four errors in same-author release prose derived the other way. Every load-bearing number re-derived in this session: - census table + ranked blockers: artifacts/release-v0.62/RQ-62-REACH.yaml - ratchet deltas: claims.yaml at v0.61.0 tag vs HEAD (selector_lines_code 19213 -> 19227, +14, one new waiver bound to the exact value; every other pin flat) - 630 Qed / 2 Admitted: coq/STATUS.md - 324,646 emulations / 158 wired scripts: oracle_wiring_check.py - MIN_DERIVED_SLOTS=4, MIN_ONLINE=2, 30 loop-conformance unit tests, `runs-on: [self-hosted, linux, x64, light]`: read out of the shipped scripts and ci.yml, not from the commit prose that claimed them The notes state two things the release would rather not say: it SUBTRACTED NOTHING (6,871 insertions / 22 deletions) and the subtraction ratchet moved the wrong way, waived, with the reason printed. A reach-and-gates release should look like one in the metric that exists to detect it. docs/status/FEATURE_MATRIX.md + artifacts/status.json regenerated via `claim_check.py claims.yaml --emit-status`; claim gate 58/58. Refs #242, #1017, #1062, #1102, #1131, #1132, #1133, #1136, #1143, #1145 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(ci): RQ-62-FLOORTIGHT (#910) — the summed emulation ratchet enforced 1,892 below what it declared Found while cutting v0.62, on THIS RELEASE'S OWN NEW ORACLE, and confirmed independently by the release's cold review. THE DEFECT. `oracle_wiring_check.py --min-emulation-floor N` is the #910 ratchet; its own failure text states its purpose — "An oracle lost execution, or a floor was lowered." It enforced 322754 against a DECLARED total of 324640 at v0.61.0 and 324646 here: 1,892 emulations of slack, more than most single oracles declare. So an oracle could stay present, stay wired, stay referenced, and drop to ZERO executions while the gate built to notice exactly that reported green. DEMONSTRATED in an isolated worktree, not reasoned about: mutation 1 delete mem_isolation_red_1145.py whole -> exit 1, but by the DANGLING-CI-REFERENCE check, NOT the floor (total fell only to 324640, still above 322754). Two mechanisms, two different failures; only one is the ratchet's job and it was the one that could not fire. mutation 2 oracle stays wired, declares `emulations >= 0` -> exit 0. GREEN. The ratchet's stated failure mode, blind. after fix same mutation -> exit 1, "RATCHET BROKEN: summed floors 324640 < recorded minimum 324646"; unmutated tree exit 0, so the floor is CORRECT, not merely stricter. This is #1113 one level up: that was INTRA-oracle (a decline half contributing zero to its own floor, fixed per-oracle in #1112); this is INTER-oracle (the summed ratchet below the summed declarations). Same sentence — the floor cannot see part of what it asserts — at two scales, one release apart. The per-oracle fix was correct and did not imply the aggregate was tight; nobody checked, because every gate reporting on this floor reports it PRESENT AND WIRED, never TIGHT. The slack was INHERITED, never introduced — so the fix is an INVARIANT, not a number: enforced floor EQUALS declared total, pinned verbatim, a landing oracle bumps both in the same PR. claims.yaml's SYNTH-ORACLE-CHECK-FLOORS-910-CI pin caught the edit at 57/58 before it could ship silently. ALSO IN THIS COMMIT — two cold-review corrections: 1. A FALSE CLAIM I WROTE, propagated to three files. Release prose said the dynamic index in the #1102-residual fixture was load-bearing because "a constant index devirtualizes and the table never materializes." FALSE. Compiling a const-index call_indirect on ARM --relocatable emits `movw r2, #0` / bounds check / `ldr.w ip, [fp, ip]` / `blx ip` — a runtime table load and an indirect call, same shape as the dynamic case; synth has NO devirtualization pass at all (verified against emitted bytes, and no such code exists in the tree). The guard is index-insensitive and refuses the const-index dangling shape too, so the fix and its red-first evidence are UNAFFECTED — what was wrong is the RATIONALE, which is what a future contributor reasons from. Corrected in CHANGELOG.md, RQ-62-TABLEDANGLE.yaml and tabledangle_1102_elem.rs, each stating the correction rather than quietly deleting the sentence. 2. R10 ATTRIBUTION. The floor fix first landed with no artifact or issue anchor in its subject, and status_evidence_check R10 — the gate added in #1124 for exactly this — failed it: "delivery-shaped commit in the release window is attributable to NO release artifact." It was right. Fixed properly rather than by loosening: RQ-62-FLOORTIGHT is now a real v0.62 artifact carrying the finding, and this subject names it. Refs #910, #1102, #1113, #1124, #1145 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs(review): commit the v0.62 independent cold review + disposition, and apply its four prose corrections The clean-room review record loop_conformance_check step 7 requires, written by an independent reviewer with no inherited framing, dispatched against 0a8c1e1. Its text is committed UNEDITED; the disposition table is additive. WHAT IT FOUND: 1 MUST-FIX, 1 SHOULD-FIX, 5 NOTEs, 4 unverifiable-as-stated, ~20 claims independently verified by execution — including a full re-run of the acceptance census from a freshly built binary (27/243, 40/243, 46/243 and every ranked blocker reproduced exactly), and a rebuild of the PRE-FIX compiler at 858ff8d^ to reproduce the #1102-residual hole end-to-end (object ships exit 0, links clean, zero UNDEF symbols). BOTH ACTIONABLE FINDINGS WERE MINE, AND BOTH ARE FIXED: MUST-FIX 1 the tip failed its own required Claim Check (R10, the rule added in #1124 for exactly this shape). Fixed by giving the work the artifact it deserved — RQ-62-FLOORTIGHT — not by loosening the rule. Now exit 0, 2 delivery commits, 2 attributed. SHOULD-FIX 1 a FALSE claim I wrote, propagated to three files: that a constant call_indirect index devirtualizes so the table never materializes. Re-verified against emitted bytes before acting rather than taking the review's word — `movw r2,#0` / bounds check / `ldr.w ip,[fp,ip]` / `blx ip`. It does not devirtualize; synth has no such pass. Corrected in all three places AS A STATED CORRECTION, so the wrong rationale cannot be re-derived from history. The fix and its red-first evidence are unaffected — only the rationale was wrong, which is the dangerous shape: a correct artifact resting on a reason a future contributor would reason from. NOTES 1, 3, 4 applied to the CHANGELOG, each narrowing a sentence that claimed more than the code or the data supports: - the diff-stat's scope is now stated (feature merges; release commit +213/-51 named separately) - the 81%->11% comparison now says the denominator differs (307 vs 243), that the subcounts come from the v0.59 artifact rather than this release, that per-module records were not preserved, and that the two subcounts may overlap - "fail-closed on unknown mnemonics" now says what the code does: undecodable instructions and zero-instruction scans always refuse; an unknown MNEMONIC refuses only when its operand text names a reserved register NOTE 5 (census hex-immediate collapse) is deliberately NOT fixed here and the disposition says why: no number in the release is wrong, and changing a measurement script mid-cut, under the oracle it feeds, risks the census for no gain. Carried to v0.63, where re-measurement is increment 1. Step 8's PR-head-vs-merge attestation slot is stubbed in the record with its rationale; it is filled at merge time. The gate labels it ATTESTED in both modes, so filling it is a deliberate act — an attestation with nothing behind it is the vacuity this release spent its scope finding. Refs #910, #1102, #1124, #1136 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs: attribute the one release-notes number that is not re-derivable, and make the NOTE 5 carry a reference Two consistency fixes, both prompted by the cold review's "unverifiable as stated" section rather than by a finding. 1. THE 17-HOUR FIGURE. The review correctly listed "the federated-graph job validated nothing for 17 hours" as a CI-history claim not derivable from the repo. I went looking: ci.yml run history shows the 09-03 main runs and the fix landing, but the federated job is ADVISORY, so per-job validation history is not reconstructable from run conclusions. The figure is my own contemporaneous observation recorded on #1143 — real, but not checkable by a later reader. That is the SAME epistemic status as the v0.59 partial/silent-drop subcounts, which this release already handles by ATTRIBUTING them rather than asserting them (NOTE 3). Treating the two differently would be arbitrary, so the federated claim is now attributed the same way: the window is named as something #1143 recorded, not as something the notes assert. The FIX itself is verified and unchanged — only the duration was ever taken on faith. 2. NOTE 5's CARRY IS NOW A REFERENCE, NOT A PROMISE. Filed as #1159. The disposition previously said "carried to v0.63", which is exactly the kind of claim this project does not accept from anyone else. The issue also records why it is more than cosmetic: the histogram's job is RANKING, and a cause fragmented across N buckets is systematically under-ranked against a cause with no varying payload — which is the input v0.63 plans to prioritise from. Refs #1143, #1156, #1159 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.
Task A — RQ-61-R4BLIND (#1119): R4 could not see conventional-commit delivery subjects
Two rules, because the measured corpus itself refutes half of option 2 as filed in #1119:
R4-issue — scope-position resolution through
fields.issuefix(#1040): ...resolves through the issue map to RQ-61-A32RELOC and gets R4's existing acknowledgment demand (claiming status, or the PR inlanded:). The marker discipline is the scope position only: eefa19e's own subject proves the description position names a cause, not a target — its#1104is the PR that introduced the defect, and resolving it would have misattributed the commit. Scoped to the release window (first-parent commits since the previous minor's tag), becausefix(#1085): ... (#1090)is v0.60-era work on the issue RQ-61-EVIDENCE now holds — matching frozen history against the current issue map would misattribute it.R10 — window attribution floor (what actually catches eefa19e)
Correction to the issue's premise:
fields.issueresolution alone cannot catch eefa19e — its subject names neither RQ-61-ORACLEFLOOR nor its issue (#1113). No resolver can attribute it; but its silence can be noticed. R10: every delivery-typed (feat|fix|perf|proof|test) first-parent commit in the release window must be attributable to some release artifact — a known id anywhere in the subject, a known issue number anywhere, or its PR named in any artifact'slanded:/verified-by:. Unattributable is red, and the red forces exactly thelanded: PR #1112line that #1120 had to write by hand. Attribution errs toward green (a mention suffices) because R10 demands non-silence, not a status flip — so the passing-mention rule the artifact protects is intact.Red-first transcript (measured corpus, live repo)
At
331bbd8b— the last commit before the #1120 hand-flip; both delivery commits in first-parent history, both artifacts stillproposed:On current main (post-#1120 statuses): 0 failures,
status-evidence-window: 3 delivery-shaped commits since v0.60.0 — 3 attributed, 1 issue-anchored delivery claims.Negative direction (required by the artifact)
0cb36bc7(fix(rivet): un-red main's R4 — RQ-61-VCLOSURE's ...) stays green — the id mention attributes it under R10, and no acknowledgment is demanded of VCLOSURE.R4BlindSpot1119, 9 tests): description-position#Nnever becomes a delivery claim even when N is a known issue;Revert "fix(#1040): ..."is not delivery-shaped; an ambiguous issue (two holders at the highest release) warns and never guesses; process types (chore/plan/docs) are exempt; an underivable window skips loudly (WINDOW-SKIP) and the newstatus-evidence-window:CI grep turns that skip into a red.SCOPE_ISSUEkills the b4860e4 replay + ambiguity control; emptyingDELIVERY_TYPESkills the eefa19e replay.What the fix preserves, per the artifact: the id-prefix anchor and its
DELIVERY_FLOORare untouched; R4 stays first-parent; no "id anywhere in the subject" delivery claims.RQ-61-R4BLIND flipped to
implementedwith averified-byrecording the above (including the eefa19e correction).Task B — RQ-61-EXTRACT flipped to implemented (batched to save a CI cycle)
Every
done-whenclause re-verified independently on main, not taken from the PR body:coq/*.ml,coq/*.mli,extracted/,validation/,compiler/*.ml, the dune tree and rootdune-projectall absent; the delivery diff ofa5c75caf(RQ-61-EXTRACT (#1080): delete 98 stale extraction snapshot files + the dune tree nothing runs; docs stop contradicting their own headers #1121) deletes exactly 98.ml/.mlifiles, matchinglanded:.docs/validation/VALIDATION_STATUS.mdopens with the historical note and greps clean of "Successfully implemented" / "Complete and ready for use" / "40 files total"..vtarget untouched; CI'sBazel Build & Proofspassed on PR RQ-61-EXTRACT (#1080): delete 98 stale extraction snapshot files + the dune tree nothing runs; docs stop contradicting their own headers #1121; main green at the merge.Task A cross-check the brief asked for:
a5c75cafwas never in the R4 blind class — its subject is id-first andlanded:names PR #1121, so old and fixed R4 both see and accept it.Gates run locally
status_evidence_check.py: 0 failures, window line present, on this treetest_status_evidence_check.py: 51/51 (42 pre-existing + 9 new)test_claim_check.py: 50/50;claim_check.py claims.yaml: exit 0rivet validate: FAIL (40 errors) — byte-identical to main HEAD465f23a2under the same local rivet (older than CI's); nothing introduced.rstouchedRefs #1119, #1080
🤖 Generated with Claude Code
https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L