BL-058: fix the side-consistency reading, and require mutant audits to be interpretable - #57
Merged
Merged
Conversation
…o be interpretable Verified against IND-v4-RESULTS.json directly rather than against FINDING-BL057's summary of it, which turned out to matter. AMENDMENT 1. v0.4 registers the side-consistency reading as free -- 'either may be implemented'. For a correct implementation the two readings agree exactly. Under two of the mutations the eligible population differs: 5,912 against 50,362, and 5,912 against 1,746. The choice is free where it does not matter and not free where it does, and the ablations are how this experiment measures checker power. The parent-local reading becomes normative for reported results, with every ablation additionally run under the root-based reading and its population and firing count reported separately. AMENDMENT 2, which the finding did not carry. FINDING-BL057 describes five broken root() implementations; the data has seven. The two omitted, minIndexInChain and grandparentSkip, are exactly the two firing zero under both readings, and they appear in no finding -- only in the raw results. A zero has two opposite meanings. Equivalent: the mutation cannot change behaviour, so nothing could fire, and it says nothing about the checker. Undetected: the mutation changes behaviour and the checker misses it, which is the most serious result this experiment can produce. IND-v4-RESULTS.json records name and firing count only -- it contains none of 'equivalent', 'fingerprint', 'description' or 'semantics' -- so no reader can tell which applies. An audit whose zeros cannot be interpreted is not falsifiable, and BL-056 had already established behavioural fingerprinting as the method. classify_survivors.py reconstructs both from their names and finds both EQUIVALENT: 0 differing calls of 297,378 across all 50,362 exhaustive worlds. Deliberately a weak claim -- it establishes what these reconstructions do to this implementation, the same names admit others, and the independent code is not in this repository. It does not show the originals were harmless. It shows the question cannot be settled from the published artefact, which is the finding. The classifier carries a positive control that differs on 174,812 of 297,378 calls. Without it, a classifier returning EQUIVALENT unconditionally would have printed the same two lines and 'proved' both mutants harmless. The second class is named BEHAVIOUR_CHANGING rather than UNDETECTED because this tool does not run the checker and cannot say whether it fires. Calling it undetected would assert a result never measured. 323 tests pass.
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.
Verified against
IND-v4-RESULTS.jsondirectly rather than againstFINDING-BL057’s summary of it — which turned out to matter.Amendment 1 — the reading is not free where it counts
v0.4 registers it as free: "either may be implemented."
Correct implementations agree exactly. Under two mutations the eligible population differs. The choice is free where it does not matter and not free where it does — and the ablations are how this experiment measures checker power.
→ parent-local becomes normative for reported results; every ablation additionally run under root-based, populations and firing counts reported separately.
Amendment 2 — the part the finding did not carry
FINDING-BL057describes five brokenroot()implementations. The data has seven. The two omitted —minIndexInChain,grandparentSkip— are exactly the two firing zero under both readings, and appear in no finding at all.A zero has two opposite meanings:
The results file records name + count only. It contains none of
equivalent,fingerprint,description,semantics. An audit whose zeros cannot be interpreted is not falsifiable — and BL-056 had already established fingerprinting as the method.classify_survivors.pyreconstructs both from their names: both EQUIVALENT, 0 differing calls of 297,378 across all 50,362 worlds.Deliberately a weak claim. It establishes what these reconstructions do to this implementation; the same names admit others and the independent code is not here. It does not show the originals were harmless — it shows the question cannot be settled from the published artefact. That is the finding.
The classifier is trapped too
Positive control
control:offByOneStopdiffers on 174,812 of 297,378 calls. Without it, a classifier returning EQUIVALENT unconditionally would have printed the same two lines and "proved" both mutants harmless.The second class is named
BEHAVIOUR_CHANGING, notUNDETECTED, because this tool never runs the checker and cannot say whether it fires. Calling it undetected would assert a result never measured.323 tests pass.