Third review round. Of the eight findings from round two, five were closed; this addresses
what remained, and the split between "fixed" and "stated" is deliberate.
FIXED — the record could not adjudicate. Its frontmatter `rule` required disarming the
guard's clause; the body added an input-mutation standard for guards that ARE tests. Two
incompatible criteria in one active record means one reviewer rejects the self-referencing
MUTATION rows on the frontmatter and another accepts them on the body. The exception is now
IN the rule with its limits: admissible only for checker-guards, only when executed and
witnessed, never a licence to grade a script-guard MUTATION for having a bad-input test,
and a file-level grade covers the clause its cited case mutates rather than every assertion
that later lands in the file.
FIXED — a matrix-templated image bypassed the cross-workflow check. `_PIN.match` requires a
literal tag, so `image: <repo>:${{ matrix.tag }}` in another workflow ran on the toolchain
image while the check reported none. Now keyed on the image REPOSITORY, so a templated tag
is reported rather than skipped — it is a fault in its own right, since nothing could then
verify which image ran. Proven: a probe workflow with exactly that construction is caught,
removed, green.
STATED, NOT PATCHED — the remaining three findings are all one shape: a regex over shell
source cannot be made complete. Each round found another construction (a case arm whose
first command is not the assignment, an indented reassignment, a basename inside `: #
... disabled`), and a fourth round would find a fifth. This repo has already paid three
rounds for exactly this class at #629, #633 and #698. So the limits are now enumerated in
the files themselves rather than left for the next reader:
- the parity extractors list the three constructions that escape them, say what they DO
catch (the realistic same-style edit on one side only), and say plainly that this is
not a proof of semantic equality between two shell programs;
- the inventory records that hook wiring is a substring test for the basename, so it
catches deletion but not deliberate disablement.
Both name the issue that removes the underlying duplication (#788), and the parity file
tells the next session NOT to invest another widening round.
Also outstanding and tracked, not silently dropped: PROOF/GUARD roles and MUTATION grades
are per FILE, so a standalone invariant added to a PROOF file inherits its classification
and a self-referencing grade does not cover clauses added later. That is clause-level
inventory, which is #790.
ruff clean, pyright clean, decisions-validate OK, 580 script-tests pass.
Refs #774
Refs #775
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
10 KiB
key, title, status, since, supersedes, superseded-by, rule, signals, mechanics
| key | title | status | since | supersedes | superseded-by | rule | signals | mechanics |
|---|---|---|---|---|---|---|---|---|
| testing.guard-ships-with-mutation-proof | 2026-08-13 — a guard ships with a proof it can go red: disarm that clause alone and a named test must fail (#775) | active | 2026-08-13 | none | none | A guard is not considered tested because a test involving it passes. It ships with a MUTATION PROOF: remove or disarm THAT GUARD'S CLAUSE ALONE, and a NAMED test must go red. ONE NAMED EXCEPTION, with its limits, because the rule degenerates without it: where the guard IS a test (a checker enforcing a repo invariant, with no separate script behind it), disarming it makes it ABSENT rather than red, so the proof is the contrapositive — INTRODUCE THE DEFECT THE GUARD EXISTS TO CATCH into an isolated copy of the guarded artifact, and the named test must go red. That is a mutation of the guarded SYSTEM rather than of the assertion, and it is admissible ONLY for checker-guards and ONLY when the mutation was executed and witnessed. It is NOT a licence to grade an ordinary script-guard MUTATION for having a bad-input test: feeding a script an input its clause rejects is BEHAVIOUR-ONLY, which is what three rows were regraded for. A file-level grade under this exception covers the clause its cited case actually mutates, not every assertion that later lands in the same file; clause-level grading is tracked in #790. Three things this excludes, each of which has already shipped here as a green suite over a dead check. FIRST, a behavioural test — one that feeds the guard a good input and a bad input and checks it passes and fails — proves the guard REACTS, never that it is LOAD-BEARING; #685 had two guards on one condition where deleting either left the whole suite green while every behavioural test passed. SECOND, mutating the WHOLE FILE does not count (#510): a whole-file revert cannot show that a test reaches a particular clause, so the mutation must target the clause. THIRD, the guard being WIRED is not the guard RUNNING — #631's suite was invoked by no CI job, #751's step was dropped by the runner and the job reported success in 6s against a normal 14-17s, and #719's new logic was never connected to stdin. Every guard also carries an ANTI-VACUITY assertion, because the characteristic failure of a completeness check is reporting that it proved everything while its population was empty. Mechanical enforcement is possible for the BOOKKEEPING and not for the JUDGEMENT, and the split is the decision: `docs/guard-inventory.md` lists every guard file with its Kind, its Proof class (`MUTATION`/`BEHAVIOUR-ONLY`/`NONE`) and a `file::function` ref, and `scripts/tests/test_guard_inventory.py` derives the guard population from the filesystem and the call sites, asserts SET EQUALITY against the rows, and resolves every claimed ref to a real `def`. So a new guard cannot ship unclassified and a renamed test cannot leave a row silently claiming coverage. What stays with review, and is stated rather than papered over: nothing checks that a row claiming `MUTATION` is telling the truth. | mutation proof · delete the guard alone see red · disarm the clause not the file · behaviour-only is not a proof · anti-vacuity assertion · guard wired is not guard running · a green job with no step output · `docs/guard-inventory.md` · set equality against the row set · proof ref resolves to a real def · 21 of 32 guards unproven · PROOF kind stops the regress · hook wiring is not hook existence · paths: `scripts/tests/test_guard_inventory.py`, `scripts/tests/test_ci_dropped_step_guard.py`, `scripts/ci-prove-ban-detects.sh` · issues: #775, #773, #751, #756, #719, #685, #631, #621, #510, #445 | Proof classes are a closed vocabulary enforced by the inventory test; a `TOOLING` row may not claim a proof. `scripts/ci-prove-ban-detects.sh` is the one guard that runs its own mutation at CI time rather than in pytest, because the thing it proves — that the ban test is not deselected — is disarmable from inside pytest configuration. |
Vacuous verification is the single most common recorded failure shape in this corpus — 17 of 69 records (25%), of which about half are not sampling errors at all: the check was simply dead (#773 §3 Family B). The rule already exists in prose, in #685's record and in project memory. It is enforced nowhere, which is why it keeps being relearned. This is a hooks problem wearing a docs problem's clothes.
The six ways a check has already been dead here, because the list is more convincing than the
principle. scripts/tests/ was invoked by no CI job (#631) — a test suite that runs nowhere is not
a safety net, it is a document. Deleting the single line calling record_wing_faults() from
main() left the suite green while a real record vanished (#621). A ${{ }} inside a shell
comment made the runner drop the step, and the job reported success in 6s where the working
version takes 14–17 (#751). New pre-push logic was never wired to receive stdin (#719). if ! cmd; then status=$? reads bash's logical negation, so a failing spec run exited 0 (#445). And two guards
on one condition masked each other, so deleting either left the suite green and the boundary test
pinned nothing (#685).
Note what those have in common: in every case a human had read the guard and believed it worked. The guard was not subtly wrong, it was absent, and absence is invisible from the outside because a dead check and a satisfied check produce the identical green.
Why behavioural coverage is not the same claim. A test that drives the guard with a good input
and a bad input establishes that the guard's logic responds to its argument. It says nothing about
whether that logic is connected — to the runner, to the caller, to the exit code anyone reads.
#719 and #631 would both have passed such a test on the day they shipped dead. This is why
docs/guard-inventory.md grades BEHAVIOUR-ONLY separately from MUTATION rather than counting
them together: they answer different questions, and adding them up is how 19 unproven guards get
reported as covered.
The model, and what makes it the model.
test_ci_dropped_step_guard.py::test_dropping_ANY_single_step_FAILS_the_guard removes each marked
step's marker one at a time and asserts the guard rejects the run — every step, explicitly not a
sample, on the argument that the interesting drop is whichever step someone actually edits. Around
it sit a positive control (the guard passes when every step marked itself), a negative control (a
fired skip gate still requires the always-steps, so the gate is not a blanket off-switch), and an
anti-vacuity check that assert with an empty expectation set REFUSES instead of printing All 0
expected step(s) executed and exiting 0. Four kinds, none substituting for another.
What was mechanised here, and the line it stops at. The bookkeeping half is fully mechanical and
now enforced: the inventory's population is derived, compared for set equality in both directions,
and every Proof ref is resolved to a real def. A new guard cannot be added without being
classified; a renamed test cannot leave a row claiming a proof that evaporated. That closes the two
ways this decays silently. The judgement half — is this row's MUTATION claim true? — is not
mechanical and was not faked. A generic mutation runner for shell hooks was considered and rejected:
it would have to know which clause of a 90-line hook is the guard, and a runner that guesses would
manufacture exactly the confident-but-empty coverage this record exists to prevent.
What "disarm the clause" means when the guard IS a test, because the rule degenerates otherwise.
For a guard implemented as a shell script with a separate test, disarming is literal: delete the
clause, watch the named test redden. For a guard implemented AS a test — test_guard_inventory.py,
test_ci_image_pin_population.py — deleting the guard does not make anything red, it makes the test
absent. The equivalent proof is the contrapositive: introduce the defect the guard exists to
catch, and the named test must go red. This is the named exception in the rule above, not a
second standard sitting beside it — an earlier draft stated it only here, and cold review correctly
objected that a record carrying two incompatible criteria cannot adjudicate a future grade: one
reviewer would reject the self-referencing rows on the frontmatter, another accept them on the body.
It is a real mutation of the guarded system, not of the test, and it is what was executed here — a deleted inventory row, a new unclassified hook, a stale
proof ref, a SHIP* case arm the extractor could not parse, and each of four ways a container job
can lose its pin, applied to every registered job rather than a sample. Cold review pushed back on
calling these mutation proofs; the pushback is right that they mutate INPUT rather than the
assertion, and wrong that this makes them weaker — for a checker, the input IS the system under
guard. Recorded because the distinction will come up again.
Where that review was straightforwardly right: neutering pin_population_faults wholesale (20 of 25
red) is coarser than disarming one clause at a time, and coarse enough that a single surviving
clause would not be noticed. Read it as a floor, not as per-clause coverage.
Applied to itself, which is the only honest test of a rule like this — and it failed twice before
it passed. The population guard's first draft compared two derived sets that shrank together, so
it was blind to a removed container: block: the exact defect testing.guard-derives-population- from-source exists to prevent, in the guard enforcing it. Running the mutations caught that. Then
the inventory's own completeness check shipped with a path pattern that excluded scripts/tests/,
so the three guard files added in that very commit had no rows and the check stayed green — caught
not by running anything, but by a cross-family reviewer. And the summary counts were a hand-kept
mirror of the table that was wrong on arrival, which both reviewers found independently. Three
self-inflicted instances of two rules, in the change introducing them. That is the argument for
mechanising the bookkeeping rather than trusting care, made by the authors of the rules failing to
follow them while writing them down.