Proofload: Nine Modules and One Competing-Risks Bug
Part 2. The executor, the report renderer, the Modal backend, the CLI, and then multi-event reporting, which is where the day’s real bug lived. See Part 1: The Diff Reproduced a Published Result on the First Run.
Sep 3: Two tests that no implementation could pass
The build sessions run against an oracle written first and frozen. Twice today the oracle contained an assertion that is impossible rather than merely failing.
The first: the run id test asserts a regex where the trailing Z sits at position 15, then asserts on the next line that position 14 is Z. yyyymmddThhmmssZ is sixteen characters. The spec said “15-char UTC stamp ending in Z”, a miscount, and the count got copied into the index check while the regex encoded the real shape.
The second: zip(dists, dists[1:], strict=True). A list zipped strictly against its own tail differs in length by one, so it raises for every example the property test draws. That one was mine, added to satisfy a lint rule without noticing that the tail is shorter.
Both halted the build rather than getting worked around, which is the rule and is the right rule. The cost is a round trip; the alternative is an implementation shaped to fit a broken test.
Sep 3: The Modal backend, and what a map cannot give back
Two things the specification asked for turned out not to be available from a real parallel map, and both got decided rather than fudged.
A cap on rollouts is written as “stop after the batch containing the Nth completed episode”. Once a map is running, breaking out of the iterator cannot retrieve work that finishes afterwards. Decision: cap what gets submitted rather than what gets consumed, so nothing in flight is ever wasted and the run is honestly marked partial.
And exceptions coming back from the map arrive with no position, so a failed batch cannot identify itself. Decision: attribution is reconstructed from what did come back rather than guessed at, and the one case that stays unattributed is named in the code as such.
The cost estimate reads from a dated table and returns nothing at all for a machine type it does not know, rather than guessing. A wrong estimate is worse than no estimate here, because it is the number someone decides to spend against.
Sep 3: The competing set is every terminal outcome
Then the multi-event work, and the bug of the day.
Asked for the survived event alone, the first version passed only the requested events to Aalen-Johansen. So fallen robots were treated as censored at their fall time, the risk set at the horizon held only survivors, and the survived incidence read 1.0 in every cell with any survivor at all. The fixture that reads 60 safer came out at 9 worse.
A fallen robot is absorbed. It is not still at risk of surviving. The competing set has to be every terminal outcome present in either run; the event list only selects which curves get compared. On data where every non-null row is terminal that makes incidence at the horizon equal to the terminal rate, so the single-event numbers are unchanged, which is exactly why nobody would have noticed.
Sep 3: The same run, two different rates
An adversarial review pass over the CLI before commit found the same mistake at a second call site. The single-run report passed only the reported events as the competing set, so every outcome the event inference had just removed was treated as censoring rather than as an absorbing risk. A cell of five completed and five violated printed 100% violated instead of 50%.
The consequence is worse than the number. report A B and report A printed contradictory rates for the same run, the same cell and the same event. On a real mock-agent report one cell went from 100.0 to 87.5 once it was fixed.
Two more from the same pass: a horizon flag accepted and silently ignored on the pair form, and an inference-failure message that pooled both arms and reported an eight-row run as sixteen rows, in the same sentence as its own correct table.
Sep 3: An invariant that can be tested and cannot be built
The hardening session that followed was supposed to lock the competing-set rule in place so it cannot come back at a third call site. One invariant would not map.
Making the diff raise on an event absent from the competing set breaks three tests in a frozen oracle, one of them deterministic: it builds a pair whose only outcomes are timeout and completed, then asks for a diff on timeout and violated. Absent by construction. I measured it twice, once with the check where I would put it and once where a reviewer panel proposed putting it. Same three failures both times.
Worth recording, because it will come up again. An adversarial review panel cleared that invariant unanimously. Every reviewer verified that a test for it can be written and passes against a small implementation. None of them ran the existing suite against that implementation. “Can this be tested” and “can this be built here” are different questions, and only the second one decided anything.
The rule ended up split instead: validation lives where the human types a name, and the mathematics stays permissive. An unknown event is refused by the verbs at exit 2, and the diff called directly returns zero counts rather than raising.