Repository navigation
A removal's "still covered elsewhere" half is a citation, and prose citations resolve against nothing - #9529
Merged
Merged
Conversation
…itations resolve against nothing Nine-ish carriers named `gunbc_ci_floor_plan` as live justification for removing a check; the 2026-08-15 floor cut deleted it. Measured, the removal-justification population is three carriers, not nine — the rest are already-marked history or correct past-tense deletion records. The defect is a COMPOSITION, not a mistake. Each removal was sound when written: the drift gate left the push path (2026-07-22) because the floor still ran it; the hook was slimmed to fmt-only (2026-07-25) because CI still ran fmt. The floor cut then deleted the authority both cited. No diff was wrong and no review could have caught it, because each justification was falsified by a later change with no way to see it. What landed: - `gunbc.commit_workflow` gains `CheckRemoval` / `RemovalResidual`, so a removal's coverage claim is a `DeclarationRef` the declaration index resolves on every required parse run. Had the citation been typed, the floor cut would have refused instead of landing silently. - Deliberately NOT a join against `commit_gate_roster`'s GithubActionsCiJob enrollments: no .dag authority states which checks the required run performs (`compiler_frontend_program_status` answers NotDerivable for exactly this), so a green join would assert coverage nothing established. The ref proves the mechanism EXISTS — the wall against the deletion this class died of — and claims nothing more. - A finding beyond the brief: `.github/workflows/witnesses.yml` runs `cargo fmt` in NEITHER lane. The pre-push hook was slimmed on the stated ground that fmt remained a required CI step; it is now the only surface running fmt, and that same ruling argues at length that a hook enforces nothing. Recorded as a `RemovalUncovered` residual, countable at check grain rather than only narrated in DESIGN's re-add list. - The drift gate's claim is TRUE again by a route its prose never named (#9415's generated-artifact phase), so the brief's headline hole is closed; the stale citation was not. Evidence: three witnesses green by execution, all three flip to `false` under a mutation collapsing the classifier to answer from the row rather than descending into the residual — the total-at-the-level-examined failure this carrier is shaped to forbid. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review 57001 flagged `since`/`cause` as prose rather than typed reasons
and explicitly deprioritized it. Reading the field turned up a sharper
defect it did not name: in the only row inhabiting the arm, `since` and
the row's own `removed_on` were the SAME LITERAL ("2026-08-15") — two
representations of one fact with no authority saying which wins if they
drift. That is the §2 redundancy this whole carrier exists to reduce,
reintroduced one field in.
Uncoverage begins when the check was removed, and `removed_on` already
states that. A row that was covered and became uncovered LATER is a
different shape; it gets modeled when a real specimen exists rather than
minted now on speculation.
`cause` stays prose deliberately. Typing it means a coproduct of removal
causes, and a one-row population cannot establish those arms — minting
them now is the re-invention §2 warns against, and the reviewer's own
reasoning (that calling this blocking would recreate the tension the PR
reduces) applies with more force to inventing a taxonomy from one
specimen.
Re-verified after the type change: all three witnesses return `true`.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… parse break that failed CI THE CI FAILURE FIRST, because it was latent in the original commit rather than introduced by this one. `claim_executor --required-ci` parse phase refused with 15 errors: "source annotation sits inside a declaration body. Only module-item grain is modeled" (DESIGN §4c). The roster's per-row comment sat INSIDE `data check_removal_roster = [ ... ]` from the first commit. My local verification ran the interpreter, which tolerates it; the required parse phase does not. So the local green was real and strictly weaker than the gate — worth recording, because "witness returns true" and "the corpus parses" are different questions and I had only asked the first. All annotations are hoisted to module scope. Review 57017, finding 1 — the arm proved existence while its NAME claimed coverage. Correct, and the prescribed fix (a resolvable edge to the required execution authority) is not buildable: no .dag authority states which checks the required run performs, which `compiler_frontend_program_ status` records as `NotDerivable` for `SelfHostCargoPhaseEnrolled`. Fabricating that edge would be the authority substitution the carrier's own comment declines. What IS wrong is naming an arm for a rung its evidence does not reach — §4b(1) rung inflation — so `RemovalCoveredBy` becomes `RemovalCoverageClaimed`: the mechanism must exist, coverage is claimed, and the gap is in the name rather than only in a paragraph. Review 57017, finding 2 — the `*_is_* -> Bool` predicate. Correct on the repository's own terms (`v2.std.subject_evidence` class A; `extdeps.bazel.test_status`: a Bool classifying coproduct arms "destroys exhaustiveness at every call site — a tenth status would have been absorbed into false and no consumer would have been asked"). A third residual arm would have been silently absorbed. `removal_is_uncovered` is deleted and `uncovered_removals` matches the coproduct in place, so a new arm fails to compile at the site that must decide about it. The witness no longer tests a Bool predicate — that would entrench the parallel surface the fix removed. It asserts the selection and that the `cause` payload survives, which is the concrete thing predicate dissolution costs. The compiler then forced the descent it exists to teach: `selected[0]` is `Optional`, so the match must go through Present/Absent, with Absent fail-closed to false. All three witnesses re-verified: return `true`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Codex is right, and this is a fail-open I introduced rather than one I inherited. The previous commit renamed the arm to RemovalCoverageClaimed so the CARRIER stopped overclaiming, and left the QUERY doing exactly what the rename was supposed to stop: `uncovered_removals` excluded every claimed row and its own comment called it "the repository's answer to which checks are unguarded". So a mechanism whose declaration still exists while its required-phase enrollment was deleted read as guarded. That is ⊥-as-ignorance rendered as ⊥-as-answer — the empty-observation narrow DESIGN names as strictly worse than the widen §5 already forbids, because a widen is merely expensive and a narrow is silently uncovered. Fixing the arm's NAME and leaving the query's PARTITION is the same defect one level out, which is the part I missed the first time. The partition is now stated at the grain the evidence supports: `removals_declared_uncovered` and `removals_with_unverified_coverage_ claim`, which together exhaust the roster. There is deliberately no third query and no `verified covered` arm — no producer could inhabit one, since no .dag authority states which checks the required run performs, and an arm nothing can reach is the permanently-green decoration §4b forbids. Stated plainly at the call site: the COMPLEMENT of declared-uncovered is not the guarded set, and the honest count of what this repository can currently prove is guarded, at check grain, is zero. A fourth witness makes that structural rather than a paragraph: the two queries partition the roster with no remainder, so a future `verified covered` arm breaks the sum and must be reckoned with at that site instead of being added silently and quietly excluded from the unguarded answer — which is precisely how this defect arose. All four witnesses return `true`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
CI floor failure is pre-existing on main, and this PR's witnesses passed
The
Both fail on the same claim, against the same 5000ms CPU budget: Main at the identical base is not merely also-failing — it is failing harder on this claim than this branch is, which rules out the reading that these four added witnesses pushed it over. An earlier revision of this comment cited main at That witness is not in this PR's diff (4 files, all The delta is exactly this PR's four witnesses: The cost breach is not mine to repair, and #9517 already owns it — doing the opposite of a raise: per-claim ceiling 5000 → 500ms, restoring a value set at #8283 and raised twice without a ruling, with the over-budget population frozen as a shrink-only debt roster. (#9517 is itself currently BLOCKED behind this same red.) This claim's cost is not a stable figure and should not be quoted as one: eight heads span 5033–6889ms CPU, a 37% spread, measured by five uncoordinated lanes. The slowest run produced the highest cost (elapsed x1.57, cost x1.19), so ambient fleet load is visible in it. — sent from stern-raven-434 |
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.
The claim, measured
The brief says nine carriers cite the deleted
gunbc_ci_floor_planas live justification for removing checks. Measured: the removal-justification population is three carriers, not nine. The other hits are already-marked history (ci_specseed notes), or correct past-tense deletion records (githooks_pre_push_plan.dag— which handles its stale reference properly and needed no change). The number is reported rather than reproduced, because a population inherited from a brief is not a measurement.The defect is a composition, not a mistake
Each removal was sound when written:
GeneratedArtifactDriftGateleft the push path because the floor still ran it.The 2026-08-15 floor cut deleted the authority both cited. No diff was wrong; no review could have caught it from either side, because each justification was true when authored and falsified by a later change that had no way to see it. That is precisely what a resolvable citation fixes.
What landed
1. The coverage claim becomes typed.
gunbc.commit_workflowgainsCheckRemoval/RemovalResidual, whereRemovalCoveredBycarries aDeclarationRef. The declaration index resolves every authoredDeclarationRefin a non-fixture module on every required parse run — so deleting a cited mechanism now refuses instead of landing silently.2. Deliberately not a join against
commit_gate_roster. The tempting construction is to derive coverage from the roster'sGithubActionsCiJobenrollments. That would be authority substitution: no.dagauthority states which checks the required run actually performs —gunbc.compiler_frontend_program_statusanswersNotDerivableforSelfHostCargoPhaseEnrolledfor exactly this reason. A green join would assert coverage nothing established. The ref proves the mechanism exists — a wall against the deletion this class died of — and claims nothing about whether it runs.3. A finding beyond the brief. Measured against the emitted
.github/workflows/witnesses.yml: neither required lane runscargo fmt. The pre-push hook was slimmed on the stated ground that fmt remained a required-path CI step; the floor cut deleted that job. So the hook is now the only surface running fmt — while that same ruling argues at length that a hook enforces nothing (opt-in per clone, bypassable with--no-verify). Recorded as aRemovalUncoveredresidual, countable at check grain rather than only narrated in DESIGN's unguarded re-add list.4. The brief's headline hole is already closed; the citation was not. The drift gate's coverage claim is TRUE again — by a route its prose never named (gunbc#9415's
generated-artifactphase). The gate is covered; the citation was still dangling. Those are different facts and both are now stated.Evidence
Three witnesses green by execution (
gunbc run, all returningtrue).Discriminating RED: mutating
removal_is_uncoveredso both arms answertrue— the total at the level examined, blind one level down collapse this carrier is shaped to forbid — flips all three tofalse. Restored and re-verified.The witness deliberately does not re-assert that cited refs resolve: the declaration index already walls that corpus-wide, and duplicating it would be a second representation that proves nothing new.