Proofload: A Frozen Test That Owned Too Much, and a Hole in the Ledger
Part 7. Intervals on the per-cell difference, the layered report, and a housekeeping pass that found two things nobody was looking for. See Part 6: A Refusal That Offered an Override That Also Refused.
Sep 7: Two measurements before any test was written
The packet was confidence intervals on the per-cell difference, and it opens by saying in its own header that it is the smallest change available and does not close the complaint people actually have.
Two things were measured before a line was written, and both came back against the spec’s guess. The fixture has no censoring at all, on either arm, exactly, which means it cannot serve as a guard for the branch that handles censoring. And a committed fixture producing zero rejections does exist, which the spec said it did not.
The rule that produced those two measurements is worth more than either of them. A spec that names a fixture as a guard has to check that the fixture can actually fail the thing it guards. It bit twice in one packet.
Sep 7: A frozen test that owned the whole stream
One frozen test had to move before a line of implementation, and it is the most portable lesson of the week.
It asserted the entire standard output of the diff verb by exact equality, at both ends. Its own packet was about error visibility, and error visibility is a block inside that stream. But whole-stream equality gave that one packet a veto over every later packet’s right to append anything to the same stream. The next packet that needed to print something collected it.
Narrowed to what it meant: the block’s own content, and its position relative to what precedes it. What follows the block is not that packet’s business. Committed alone, before any implementation.
The general rule, since this will recur: a frozen test asserts the property its packet owned. Whole-stream equality on a stream later packets add to is over-pinning, and it fails the next packet rather than the bug it was aimed at.
Sep 7: Pooling, closed
The pilot said the per-cell view had no resolution at the replicate count it ran. The obvious rescue is to borrow strength across cells rather than testing each one alone, so that got fitted properly against the pilot’s baseline arm rather than argued about.
It came back empty. Not harmful, not a trade-off, just no movement worth the complexity. Closed, with the fit recorded so it does not get re-litigated in three weeks.
One correction to my own reasoning went in the same record. A reliability figure had been used earlier to argue there was nothing to pool. Reliability describes how spread the units are and says nothing about the precision of a within-unit difference, so it was the wrong statistic for the claim. The conclusion is unaffected, because the fit establishes it independently, but the number comes out of the argument and must not appear anywhere.
Sep 7 to 8: The layered report
What shipped instead is a report with levels, where a level is only tested when the level above it rejects. Three packets over two days, each with its own frozen oracle and its own mutation pass.
Two design corrections came out of measuring before writing, which is now the standing order for these. A level that had been described as “a handful of hypotheses, so power stays high” is nothing of the sort on real data. And a bound the plan cited turned out not to be the one the plan named; reading the source paper, there are two, and ours is the other one.
The power gate from the previous part reappears one level down, which is the part I like: a grouping the design cannot resolve is refused with the next one named, rather than silently reported.
The mutation pass on the top level found something worth writing down. Two mutants survive by construction and no test can catch either, because both leave every p-value bit-identical. The property they violate holds because of how the source is shaped, not because anything asserts it. A green suite is not evidence for it, and the entry says so, so nobody reads the suite as covering it later.
Sep 9: The biped
The tool met a system that was not its own fixture or its own pilot. That has its own series, starting at Specimen Sizing and the Initial Sweep.
Sep 10: A hole under the shipped range
Housekeeping only. No feature work, nothing pushed.
The decision ledger holds 58 rows and reads as complete. It is not. Seven numbers in the middle are drafts that live only in two specs and a design record and were never landed, and they are the drafts behind three packets, all three of which are built and shipped. Meanwhile the three numbers above them, which cover something not yet built, were landed properly. So the ledger’s high-water mark sits above a hole its own shipped code depends on, and nothing in the numbering makes that visible.
The other one came from a verification worktree, created detached at the current commit with its own environment and installed the way a user would install it. It collects 216 fewer tests than the working checkout at the same commit. Those 216 are five modules that never collect because the base install omits two optional dependencies, and those five modules are the entire trace-capture and pilot surface. A run performed as installed would pass while seeing none of it.
Neither of those is a bug in the code. Both are bugs in how I would find out about a bug in the code, which is worse.
Nothing here blocks the next packet. Open items are two missing changelog lines, the ledger back-fill, and a decision about which extras the verification environment gets.