neuwirth
/
epiphany
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

P13-S22 contract: M2's whole-test alternative was false 

§3 offered "delete the new table's row loop (or the whole new test)" as
interchangeable forms of the paired control. They are not. Deleting the
test drops the suite to 1557, contradicting the 1558/0 result required
in the same sentence; only loop-deletion holds the test count fixed so
the passing count is comparable to the baseline.

Found by the executing agent, which took the loop reading — the only one
satisfying both conditions — and reported the tension rather than
silently picking. Corrected here as a forward commit: 6e4e455 already
sits on the contract, and the evidence chain reads better with the
defect and its repair both visible.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QjsEnYhm1gPpf6ii2iFxFV
This commit is contained in:
Levi Neuwirth 2026-07-31 19:30:21 -04:00
parent 6e4e45587f
commit a4d78471bb
1 changed files with 15 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
spec/CONTRACT_P13S22_TAGLOCK.md
View File

@ -305,11 +305,21 @@ fail signs nothing.
variant does not satisfy pin 4 and does not sign this rung.
**M2 — the paired control, which is what makes M1 mean anything.** With M1's
mutation **still applied**, delete the new table's row loop (or the whole new
test) and run `cargo test --workspace`. **Must pass 1558/0** — reproducing
P13-S22 itself in the tree rather than arguing for it, exactly as P13-S15's
`&table[..30]` control did. Then restore the test, leaving M1 applied, confirm
the failure returns, and restore M1.
mutation **still applied**, delete the new test's **row/assertion loop only**,
**retaining the test function itself** (and its coverage block), then run
`cargo test --workspace`. **Must pass 1558/0** — reproducing P13-S22 itself in
the tree rather than arguing for it, exactly as P13-S15's `&table[..30]`
control did. Then restore the loop, leaving M1 applied, confirm the failure
returns, and restore M1.
> **Deleting the whole test is NOT an equivalent alternative, and an earlier
> draft of this contract wrongly offered it as one.** The suite would then
> report **1557**, contradicting the 1558/0 requirement stated in the same
> breath — the two forms are not interchangeable, and only loop-deletion
> satisfies both conditions at once. The point of M2 is to remove *the
> association assertion* while leaving the test count fixed, so that the
> passing 1558 is comparable to the baseline 1558 rather than to a different
> number.
> Without M2, M1 shows only that some test fails under some mutation. The whole
> claim of this rung is that **nothing else** sees it.