ersatztv/docs/decisions/records/testing/verification-code-needs-its-own-proof.md

key, title, status, since, supersedes, superseded-by, rule, signals, mechanics

key	title	status	since	supersedes	superseded-by	rule	signals	mechanics
testing.verification-code-needs-its-own-proof	2026-08-28 — verification code is code under test: the obligation follows the VERDICT, and the exempt branch is what no proof test can drive hermetically (#796)	active	2026-08-28	none	none	VERIFICATION CODE IS CODE UNDER TEST. The obligation in `testing.guard-ships-with-mutation-proof` attaches to whatever emits a PASS/FAIL somebody acts on — a smoke test, a timeout wrapper, an operator-run checker, the harness that applies the mutations — and NOT only to files sitting in the guard population or named like guards; every one of the five defects measured below was in code nobody had counted as a guard. THE DISCRIMINATOR IS WHETHER A PROOF TEST CAN DRIVE THE CONSTRUCT HERMETICALLY, NOT WHETHER CI RUNS IT, and the difference is load-bearing rather than pedantic: `.claude/hooks/*.sh` and `.husky/pre-push` are operator-run and CI never fires them AS HOOKS, yet FOUR of them carry `MUTATION` rows — `posttooluse-worktree-marker.sh`, `pretooluse-bom-guard.sh`, `pretooluse-worktree-guard.sh` and `.husky/pre-push` — because a pytest proof drives them in a sandbox. A does-CI-run-it test would sort those four already-proven guards into the exempt branch. (Most of the remaining hooks are graded `NONE`; that is unproven debt, not evidence for the other discriminator.) "IT NEEDS A REAL SERVER" IS AN EXEMPTION CLAIM AND IT IS USUALLY FALSE: `scripts/mcp_smoke.py` takes its config path and server name as POSITIONAL ARGUMENTS, so a test hands it a synthetic config in a tmpdir pointing at a stub responder and drives FIVE of its refusal paths plus the success path — no gitignored `.mcp.json`, no language server — and it is proven that way in `scripts/tests/test_mcp_smoke.py`. That is a subset, not every branch: the config, command-resolution and spawn stages are not driven, and the test file lists what it covers rather than implying the rest. A checker is never excused because its CALLER cannot run in CI. WHERE THE PROOF LIVES: the checker itself needs NO `docs/guard-inventory.md` row, because that population is derived from workflow and hook call sites and a transitively-reached script is rejected as a phantom; the proof goes in an ordinary `scripts/tests/test_*.py`, which joins the population automatically and carries the row, while the manifest entry names THAT test as `guard` and the checker as `target`. That shape already exists for `mutation_harness_lib.py` and needs no change to any population. ONLY WHAT NO PROOF TEST CAN DRIVE HERMETICALLY falls back to a WITNESSED NEGATIVE CONTROL — the failure path executed once, the false-green form reproduced, both recorded in the PR, and its decay stated because nothing re-runs it. `scripts/check-local-lsp.sh` is the genuine case: it asserts developer-machine installs (a global `csharp-ls`, a `host/fxr` under `DOTNET_ROOT`, a root `node_modules`) that no runner has. STOP-AND-SUBTRACT, adopted here as this record's own threshold: when a review round's finding was CREATED by the previous round's fix and that happens TWICE CONSECUTIVELY, delete the layer generating them rather than guarding it. READING THE CONSTRUCT IS NOT EXECUTING IT: ShellCheck 0.11.0 flagged NEITHER of the two shell defects below, and each is indistinguishable from correct by reading.	the verification harness is itself unproven code · a false green in the checker rather than the checked · `[ -x "$cmd" ]` is true for a DIRECTORY · perl alarm/exec exits 0 without `or die` · macOS has no `timeout` and no `gtimeout` · smoke test accepts an impostor server · a server that pre-answers a guessable id · each fix created the next round's defect · stop and subtract rather than add a layer · hermetically drivable is the test, not does-CI-run-it · a checker is not exempt because its CALLER cannot run in CI · the checker needs no inventory row — name the proof test as `guard` and the checker as `target` · a transitively-reached script is rejected as a PHANTOM · witnessed negative control for what cannot be driven · paths: `scripts/mcp_smoke.py`, `scripts/tests/test_mcp_smoke.py`, `scripts/check-local-lsp.sh`, `scripts/tests/mutation_manifest.py`, `docs/guard-inventory.md` · issues: #796, #793, #790, #785, #777, #776	THE macOS TIMEOUT RECIPE, recorded here because the WRONG form was the recommended one and a session that followed it verbatim produced a false green (#793): `perl -e 'alarm shift; exec @ARGV or die "exec failed: $!\n"' <secs> <cmd...>`. The `or die` is load-bearing — without it perl exits 0 when `exec` fails, so a missing or misspelt binary reports SUCCESS having run nothing (measured 2026-08-28: `perl -e 'alarm shift; exec @ARGV' 5 /nope` exits 0; the `or die` form exits 2 and says why). macOS has neither `timeout` (GNU coreutils) nor `gtimeout` on this fleet, and an absent `gtimeout` exits 127 with empty output, which reads as a clean pass to any caller grepping stdout for a failure string. Two traps travel with it: `[ -x "$cmd" ]` does not establish that a command is runnable, because a directory satisfies `-x` (`[ -x /bin ]` is true); and whatever wrapper is used, its EXIT CODE must be checked rather than its stdout. `scripts/check-local-lsp.sh` is the single in-repo site carrying the perl recipe and the check-the-exit-code discipline; the `-x` trap appears there only in a comment recording what it deliberately does not do.

The measurement. #793 added one small operator-run check — a smoke test that starts the csharp-lsp MCP server and lists its tools. Five independent cold-review rounds found five false greens in the verification code itself, each introduced by the fix for the previous one and each reproduced with a control before being fixed:

#	The check	Why it reported success without checking
1	[ -x "$cmd" ]	a directory satisfies -x; [ -x /bin ] is true
2	smoke test accepts any id-matching reply	an impostor server, and {"id":1}, both passed
3	perl -e 'alarm shift; exec @ARGV' wrapper	perl exits 0 when exec fails → prints PASS having run nothing
4	message/line caps added to bound #3's replacement	an over-long line had its suffix re-parsed as a fresh message
5	pending-id registered before send	a server could pre-answer an id it could predict

Why this is a separate rule and not an application of #775. testing.guard-ships-with-mutation- proof is scoped by a population — the guard files docs/guard-inventory.md derives and grades. Defects 1 and 3 are a [ -x ] test and a perl wrapper inside scripts/check-local-lsp.sh, which no workflow or hook invokes; 2, 4 and 5 live in scripts/mcp_smoke.py, reached only through that script and so excluded by scope limit item 6. Neither file is in the population. That scoping is what keeps the inventory from becoming a chore that gets rubber-stamped; what was missing is the claim that the obligation follows the verdict, not the file.

The discriminator, stated precisely because the obvious one is wrong. It is not "does CI run this": CI never fires .claude/hooks/*.sh or .husky/pre-push as hooks either, yet four of them are graded MUTATION, because a pytest proof drives them in a sandbox. The question is whether a proof test can drive the construct hermetically, and "it needs a live server" usually fails that test rather than passing it. mcp_smoke.py takes its config path and server name as positional arguments, so scripts/tests/test_mcp_smoke.py hands it a synthetic config pointing at a stub responder and drives five of its refusal paths plus the success path — identity mismatch, a body carrying only an id, a missing tool, a pre-answered initialize, a pre-answered tools/list — with no server to start. That is a subset and the file says so. check-local-lsp.sh genuinely cannot be driven that way: it asserts a global csharp-ls on PATH, a host/fxr under DOTNET_ROOT, and a root node_modules, which is developer-machine state no runner has. That, and not "it is operator-run", is what puts it in the exempt branch. Note what that concedes: two of the five defects below (the -x test and the perl wrapper) were in check-local-lsp.sh itself, so the exempt branch is not defect-free — it is the part where a recorded control is the best available proof. Three of the five were in mcp_smoke.py, and those are the ones now pinned.

Where the proof lives, and why the checker needs no row. docs/guard-inventory.md's population is derived from workflow and hook call sites, so a row for mcp_smoke.py is rejected outright — measured, not assumed:

AssertionError: guard-inventory.md lists ['scripts/mcp_smoke.py'], which no longer exist or are
no longer invoked by any workflow or hook. A row for a guard that does not run reads as coverage
and is not.

The row is therefore never the route. The proof goes in scripts/tests/test_*.py, which joins the population automatically and carries the row, and the manifest entry names that test as guard with the checker as target — the shape test_mutation_harness.py already uses for mutation_harness_lib.py, itself outside the population under scope limit item 7. No population derivation changes; the declared clause is re-applied every run like any other.

The residual, for the exempt branch only. A witnessed negative control recorded in a PR is weaker than a mutation re-run every suite: nothing re-executes it, and a later edit can silently undo what it proved. The alternative there is not a stronger check but a green one that runs nowhere — this repo's most expensive recurring failure (#631, #719, #751).

Stop-and-subtract. Rounds 3→4 are the clearest case: round 3 replaced the broken wrapper, round 4 found that the caps round 3 added re-parsed an over-long line's suffix, and the fix was deleting those caps — three defects with one cause. Round 5 likewise replaced lock-based ordering with unguessable random ids: strictly less code, and it removed the race rather than policing it. Two consecutive rounds of fix-creates-the-next-defect is adopted here as the threshold; the six-round text-comparison case behind release.verdict-vocabulary-shared is precedent for the shape, not its source, and it concluded in a categorical ban rather than a count.

Read-the-construct fails; execute-it works. Defect 3 is indistinguishable from correct by reading. ShellCheck 0.11.0 over reconstructed forms of the two shell defects returns only style nits (SC2292, SC2250) and an unused-variable warning — nothing about either; the remaining three are Python and outside its reach, so the honest figure is two of two, not zero of five. #776 reached the same conclusion the same week from a different subsystem, with no shared code: exec … 2>/dev/null silences the shell, and a trap's exit "$?" invents a status. The idiom behind defect 3 came from written project memory recommending the form without or die — correct advice, written down, was still a single point of failure, because the recipe had never had its own failure path executed.