fix(#1085): two v0.60 artifacts pinned evidence that could not fail on the failure they define - #1090
Merged
Merged
Conversation
…n the failure they define Both `done-when` predicates certified that code EXISTS. Neither artifact's claim is that code exists. RQ-60-A64IMPORT. Its description says, in capitals: "HONESTY REQUIREMENT: the acceptance number is the deliverable ... A change that adds a code path without moving the census has not delivered." Its signature was `contains:crates/synth-backend-aarch64/src/elf.rs:undefined_externals` — a code-existence check, i.e. precisely what the description says is NOT the deliverable. A predicate that cannot fail on the failure the artifact defines for itself is not a predicate. The status stays `implemented` — #1071's code is on main and EXECUTES (ld.lld links the objects against assembled definitions; unicorn runs the linked images: run(37)=42 through the import, table dispatch slot0 41->42 and slot1 21->42) — but the BASIS is now written where the release- readiness query's reader sees it, and it states the negative too: the AArch64 ACCEPTANCE RATE IS UNMEASURED since #1071. The 805-module corpus is not synth-local; the re-run is requested at #1017 and is named as increment 2 rather than quietly dropped. The v0.60 release notes assert no reach improvement. RQ-60-CANARY. Signature moves from `arm_encoder.rs:expansion_scratch_contract` (a function name) to the canary gate's own NON-VACUITY FLOOR, `scripts/repro/expansion_canary_gate_1021.py:emulations >= 1200`. The artifact's claim is that every rule-emitted expansion is EXECUTED with non-contract registers canaried; the old predicate would still hold with the gate deleted, and could never see the gate quietly emptied — the vacuity shape #910 exists for. SENSITIVITY PROVEN, not assumed: dropping the gate's floor from 1200 to 0 (needle counted == 1 before mutating) takes status-evidence from 0 failures to 1, naming RQ-60-CANARY. Restoring it returns 0. Also records `shipped-in: v0.59.0` on CANARY. Measured: the canary gate merged as #1061 at 08:50 on 2026-08-26, v0.59.0 was tagged at 15:19 the same day (so the gate is an ANCESTOR of that tag, and v0.59.0's notes already credit it), and the v0.60 plan was written at 18:56 — AFTER the tag — scoping as future work something already released. v0.60 carries this artifact's traceability closure, NOT the capability, and the notes say so. Every gate passed throughout, because each asks whether the declared evidence EXISTS and none asks which release it arrived in. Found by auditing all eight v0.60 artifacts against the bar each one's own description sets; three of eight pinned a `contains:` on an implementation path where the stated bar was measured or executed (the third, RQ-60-ARTIFACTSPLIT, was fixed in #1084). The proposed rules are R7 (evidence must belong to the release) and R9 (a `contains:` into `crates/**` is weaker than one pointing at the gate that exercises it) — both in #1085, neither implemented here. Gates: status-evidence 0 failures (60 artifacts / 5 files / 8 predicates), claim_check 51/51, 24 tests OK. Refs #1085, refs #1017, refs #1021. 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 Aug 27, 2026
avrabe
added a commit
that referenced
this pull request
Aug 27, 2026
…e, the release field must match the file, code-existence is not a predicate Three rules, all found by USING the v0.60 status-evidence gate rather than reasoning about it. Red-first each: all three defective fixtures pass the pre-change checker with 0 failures, then fail on exactly the rule under test and no other. R7 — EVIDENCE MUST BELONG TO THE RELEASE. For every contains:/file: done-when that HOLDS, the oldest first-parent commit introducing the signature (git log -S for contains:, --diff-filter=A for file:) must not be an ancestor of the previous minor's HIGHEST tag (so evidence shipped in a previous PATCH is caught too). The RQ-60-CANARY shape — gate merged 08:50, v0.59.0 tagged 15:19, v0.60 plan written 18:56 — is replayed in a real git fixture; the shipped-in: escape hatch (per-case, version-shaped, reason written beside it, #1090) is the green control exactly as it stands on main. Reliability stated, not silent: no-git/shallow/missing-tag/ uncommitted-signature SKIPS LOUDLY (R7-SKIP warning + a skip count in the machine-read summary), and the CI grep pins '(0 skipped)' with >= 1 archaeology check — a shallow CI checkout already reds the R4 delivery floor before R7 is reached. Live: 4 checks performed, 0 skipped. R8 — THE release: FIELD MUST EQUAL THE FILE'S VERSION. The checker version-gates by PATH; rivet's readiness query reads the FIELD; nothing asserted agreement. The harmful never-hit direction (release: v0.60 parked in a pre-v0.60 file, exempt from every >= v0.60 rule while rivet counts it in v0.60's scope) is the red fixture. THE 6 MEASURED MISMATCHES ARE KEPT under the one now-STATED allowance: a field naming a PATCH of the file's previous minor (vX.(Y-1).Z, Z >= 1) is the parked-patch practice (v0.56.1/v0.56.2 in release-v0.57.yaml) and green; missing, unparseable, ahead-of-path, or behind-without-patch fields are red. No historical release file needed edits. R9 — A contains: INTO CRATE SOURCE IS WEAKER THAN THE GATE. Under a CLAIMING status, a signature whose path is crates/** excluding /tests/ components (crate integration-test dirs are executed by the required Test job and are gate-shaped, like scripts/, coq/ and workflows — measured, every honest live signature already points at one of those) requires a written verified-by saying why code-existence IS the outcome; the better fix is re-pointing at the gate, which is what both #1090 corrections did. The RQ-60-A64IMPORT specimen is the red fixture; both correction forms are green controls. test_4's green control updated to the #1090 corrected done-when — the old fixture carried the exact shape R9 now reds, and R9 caught it. Gates: 42 unit tests OK (7-instance replay intact); live tree 66 artifacts / 0 failures / 4 archaeology checks (0 skipped); 5 mutations each kill >= 1 test with needle counts asserted before mutating (R7 ancestor check, R8 loop, R8 allowance, R9 trigger, R7 skip accounting) and byte-identical restore; claim_check 52/52; test_claim_check 50 OK; ci.yml summary grep extended in the same PR. Artifact flipped implemented with done-when pointing at the R7 replay class in the unit suite (R9 applied to itself) and a written verified-by. Refs #1085, #1090, #1064, #242. 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
Aug 27, 2026
…e, the release field must match the file, code-existence is not a predicate (#1099) Three rules, all found by USING the v0.60 status-evidence gate rather than reasoning about it. Red-first each: all three defective fixtures pass the pre-change checker with 0 failures, then fail on exactly the rule under test and no other. R7 — EVIDENCE MUST BELONG TO THE RELEASE. For every contains:/file: done-when that HOLDS, the oldest first-parent commit introducing the signature (git log -S for contains:, --diff-filter=A for file:) must not be an ancestor of the previous minor's HIGHEST tag (so evidence shipped in a previous PATCH is caught too). The RQ-60-CANARY shape — gate merged 08:50, v0.59.0 tagged 15:19, v0.60 plan written 18:56 — is replayed in a real git fixture; the shipped-in: escape hatch (per-case, version-shaped, reason written beside it, #1090) is the green control exactly as it stands on main. Reliability stated, not silent: no-git/shallow/missing-tag/ uncommitted-signature SKIPS LOUDLY (R7-SKIP warning + a skip count in the machine-read summary), and the CI grep pins '(0 skipped)' with >= 1 archaeology check — a shallow CI checkout already reds the R4 delivery floor before R7 is reached. Live: 4 checks performed, 0 skipped. R8 — THE release: FIELD MUST EQUAL THE FILE'S VERSION. The checker version-gates by PATH; rivet's readiness query reads the FIELD; nothing asserted agreement. The harmful never-hit direction (release: v0.60 parked in a pre-v0.60 file, exempt from every >= v0.60 rule while rivet counts it in v0.60's scope) is the red fixture. THE 6 MEASURED MISMATCHES ARE KEPT under the one now-STATED allowance: a field naming a PATCH of the file's previous minor (vX.(Y-1).Z, Z >= 1) is the parked-patch practice (v0.56.1/v0.56.2 in release-v0.57.yaml) and green; missing, unparseable, ahead-of-path, or behind-without-patch fields are red. No historical release file needed edits. R9 — A contains: INTO CRATE SOURCE IS WEAKER THAN THE GATE. Under a CLAIMING status, a signature whose path is crates/** excluding /tests/ components (crate integration-test dirs are executed by the required Test job and are gate-shaped, like scripts/, coq/ and workflows — measured, every honest live signature already points at one of those) requires a written verified-by saying why code-existence IS the outcome; the better fix is re-pointing at the gate, which is what both #1090 corrections did. The RQ-60-A64IMPORT specimen is the red fixture; both correction forms are green controls. test_4's green control updated to the #1090 corrected done-when — the old fixture carried the exact shape R9 now reds, and R9 caught it. Gates: 42 unit tests OK (7-instance replay intact); live tree 66 artifacts / 0 failures / 4 archaeology checks (0 skipped); 5 mutations each kill >= 1 test with needle counts asserted before mutating (R7 ancestor check, R8 loop, R8 allowance, R9 trigger, R7 skip accounting) and byte-identical restore; claim_check 52/52; test_claim_check 50 OK; ci.yml summary grep extended in the same PR. Artifact flipped implemented with done-when pointing at the R7 replay class in the unit suite (R9 applied to itself) and a written verified-by. Refs #1085, #1090, #1064, #242. 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.
Refs #1085, #1017, #1021.
Both
done-whenpredicates certified that code exists. Neither artifact's claim is that code exists.RQ-60-A64IMPORTIts own description says, in capitals:
and its signature was
contains:crates/synth-backend-aarch64/src/elf.rs:undefined_externals— a code-existence check, i.e. exactly what the description says is not the deliverable. A predicate that cannot fail on the failure the artifact defines for itself is not a predicate.Status stays
implemented— #1071's code is on main and executes (ld.lldlinks the objects against assembled definitions; unicorn runs the linked images:run(37)=42through the import, table dispatch slot0 41→42 / slot1 21→42). What changes is that the basis is written where the release-readiness query's reader sees it, including the negative: the AArch64 acceptance rate is UNMEASURED since #1071. The 805-module corpus is not synth-local; the re-run is requested at #1017 and named as increment 2 rather than quietly dropped. The v0.60 release notes assert no reach improvement.RQ-60-CANARYSignature moves from a function name in
arm_encoder.rsto the canary gate's own non-vacuity floor,scripts/repro/expansion_canary_gate_1021.py:emulations >= 1200. The claim is that every rule-emitted expansion is executed with non-contract registers canaried; the old predicate would still hold with the gate deleted, and could never see the gate quietly emptied — the vacuity shape #910 exists for.Sensitivity proven, not assumed: dropping the floor from 1200 to 0 (needle counted
== 1before mutating) takes status-evidence from0 failuresto1, namingRQ-60-CANARY. Restoring returns 0.Also records
shipped-in: v0.59.0. Measured:v0.59.0's notes already credit it ("VCR-TIER-001 increment 1 — the pseudo-op expansion canary gate"). v0.60 carries this artifact's traceability closure, not the capability, and the release notes say so.
Why both slipped through
Every gate passed throughout, because each asks whether the declared evidence exists and none asks which release it arrived in, or whether the evidence proves the stated claim. Found by auditing all eight v0.60 artifacts against the bar each description sets — three of eight pinned a
contains:on an implementation path where the stated bar was measured or executed (the third,RQ-60-ARTIFACTSPLIT, was fixed in #1084).The proposed rules — R7 (evidence must belong to the release) and R9 (a
contains:intocrates/**is weaker than one pointing at the gate that exercises it) — are written up in #1085 and not implemented here; this PR corrects the two live instances.Gates: status-evidence
0 failures(60 artifacts / 5 files / 8 predicates), claim_check51/51, 24 tests OK.🤖 Generated with Claude Code
https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L