BL-058b: the immunity ablation is blind to the worst mutations - #59
Merged
Conversation
Adversary preparation. Built the programme's first mutant audit meeting Amendment 2 of BL-058 -- every mutant implementation published, every mutant classified equivalent or behaviour-changing, and the unit of counting stated -- then ran it and found something. depth0 and alwaysZero change root_of and are NEVER CAUGHT, under either reading. They are not equivalent mutants, so their zeros are not forced: this is a blind spot rather than a harmless result. Both make root_of ignore lineage entirely -- depth0 returns each claim as its own root, alwaysZero returns claim 0 for everything. Under either, the verdict collapses to a function of the multiset of sides, and rewiring preserves sides by construction, so the verdict is trivially invariant and immunity trivially holds. The immunity ablation tests INVARIANCE UNDER REWIRING, NOT CORRECTNESS OF root_of. A uniformly wrong mutation preserves invariance and is invisible; a partly wrong one breaks it and is caught. That ordering is backwards: the ablation catches subtle errors and misses gross ones, and 'the ablation fired on 3,940 worlds' has been read as evidence of checker power when it is evidence of a particular kind that excludes the most severe defects. This does NOT say Theorem 1 is wrong. Immunity holds for the correct implementation at 116,032 eligible pairs with zero violations, and the control firing zero is what makes every other row readable. It says the immunity ablation is not a test of root_of and must not be counted as one. Amendment 1 also reproduced independently from our own implementation: three mutants have divergent populations between readings, and offByOneStop diverges in firing too, 1,720 against 118,968 -- so the divergence is not confined to eligibility. Not a replication of IND-v4: their unit of counting is unstated, so no correspondence is claimed. The two agree on the facts that matter and this one adds the classification that makes the zeros interpretable. Also marks FINDING-KL001-v0.2 and v0.3 superseded in framing, not withdrawn. Their numbers stand; a reader stopping at v0.3 comes away with 'reduces false cleans', which DESIGN-v0.4 exists to prevent. 105s at max-claims 6, so it is a deliberate audit rather than a suite test; run and committed with its output. 323 tests pass.
Six numbered claims, each stated as narrowly as the evidence supports and paired with what would falsify it. Three things measured that do NOT support the claim a reader would expect. Six known weaknesses, listed so an adversary does not spend their time rediscovering them. Written because the claims were spread across fifteen findings with careful hedges in each. Without a target an adversary attacks strawmen or burns effort reconstructing what is actually asserted, and we learn less from either. Section C is the part worth reading. C4 in particular: every mistake made while building this was caught by a check -- a vacuous boundary run, an invented ladder rung, a stale status file, a probe that would have passed by printing a constant. Not one design error was caught by tooling. The deepest problem in KL-001 was found by a human asking one question. One narrow form of it is now checkable and I have no account of the rest. Also verified for this pass and unchanged: Gate and Border suites pass, 72 and 50 tests; both state the two attack prices and the odd-margin parity gap identically; Border's conformance contract already says its check is strictly weaker than Theorem 1 and does not test it, which BL-058b supports rather than undercuts.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adversary preparation. Built the first mutant audit meeting Amendment 2 of BL-058 — implementations published, every mutant classified, unit of counting stated — then ran it and found something.
The finding
depth0andalwaysZerochangeroot_ofand are never caught, under either reading. Not equivalent mutants — their zeros are not forced. Blind spot, not a harmless result.Both make
root_ofignore lineage entirely. The verdict collapses to a function of the multiset of sides; rewiring preserves sides by construction; so invariance is trivial and immunity trivially holds.That ordering is backwards — it catches subtle errors and misses gross ones. "The ablation fired on 3,940 worlds" has been read as evidence of checker power when it is evidence of a particular kind that excludes the most severe defects.
What it does not say
Theorem 1 is not wrong. Immunity holds for the correct implementation at 116,032 eligible pairs, zero violations — and the control firing zero is what makes every other row readable. The claim is that the immunity ablation is not a test of
root_ofand must not be counted as one.Amendment 1, reproduced independently
Three mutants diverge in population between readings;
offByOneStopalso diverges in firing (1,720 vs 118,968), so it is not confined to eligibility. BL-058 was raised from the independent audit — this reproduces it from our own implementation with published semantics.Not a replication: IND-v4’s unit of counting is unstated, so no number-for-number correspondence is claimed.
Also
FINDING-KL001-v0.2/v0.3marked superseded in framing, not withdrawn — numbers stand, but a reader stopping at v0.3 comes away with "reduces false cleans."105s at max-claims 6, so it is a deliberate audit rather than a suite test. 323 tests pass.