A negative control written from the guard confirms the guard, not the claim - #822
Merged
Conversation
… claim
Five times in this session a guard was written, its negative control was run, the control
failed as expected, and the guard still proved nothing.
the isolation suite asserted the docker run argv; mutating the argv failed the test,
while no probe had ever executed inside the container
three refusal tests passed while the attack could not run at all, so the control
"make the attack succeed" was impossible to construct and nobody wrote that down
a schema was widened to accept placeholder strings so a template would validate;
removing a required field still failed, so the control passed for the wrong property
a path scan covered all of bench/, which forced four historical run logs to be
rewritten; adding a path still failed the test
the exclusion index matched only entry.value; kind was never read, so a record-id row
excluded correctly and the other fourteen kinds were inert with no control at all
Each control was built from the guard's implementation, in the guard's vocabulary. That
confirms the mechanism runs. It cannot confirm the claim, because the claim was never
written down anywhere a control could be derived from it.
So the registry indexes claims, not functions, and the claim must be a sentence about the
study rather than about the code. If it cannot be stated without naming a function it is
describing a mechanism and gets rewritten. Each claim carries mutations that should break
it, and the runner reports four outcomes rather than pass and fail:
mutation applied, test failed the guard binds this claim
mutation applied, test passed the guard is inert for it
mutation cannot be applied the claim has no expressible control
zero mutations nothing was ever attempted
The last two are the ones that used to disappear. A property nobody could write a control
for and a property nobody tried to write one for both looked exactly like a property that
passed.
The first run is red, and that is the runner working. Thirteen claims bind. One is inert:
the personal-path scan passes with its own check bypassed, because a clean tree satisfies
it either way and nothing constructs a violating file. One is unavailable. Thirteen
exclusion-index kinds have no expressible control, which is the same finding an adversarial
review reached from the other direction by reading the code -- two methods, one conclusion,
and only record-id actually excludes anything.
Nothing here fixes those. Surfacing them is the deliverable; a mutation runner whose first
run is green on a tree with a known inert guard is itself inert.
Record-Id: r-guardmutation
Provenance: authored
Certainty: firm
Blast: system
Undo: easy
Ruled-out: fixing the inert guards in the same change | a runner that has never reported a real failure is not known to report one, and the red run is the evidence that it can
Ruled-out: indexing guard functions instead of claims | that reproduces the exact failure this exists to stop, because the control comes back out of the implementation it is meant to test
Ruled-out: treating an unexpressible control as a skip | it is indistinguishable from a control nobody attempted, and both were silently green before
Ruled-out: folding this into the check job | it runs vitest once per mutation, so it belongs in its own job where its cost is visible
Limit: a mutation proves a guard reacts to one specific edit. A guard can bind its claim for that edit and miss a different violation of the same claim, so coverage here is a floor and not a proof
Limit: the claims were written by the same author as the guards, so a claim stated too narrowly produces a control that passes for a property nobody wanted
Limit: thirteen exclusion-index kinds remain inert; this change makes that visible and does not repair it
Verified: 15 mutations run against the real suites, producing 13 bound, 1 inert, 1 unavailable and 13 uncovered. Both typechecks clean and the CI gate suite passes at 7. The inert result was checked by hand: bypassing the personal-path scan leaves the suite green
CommitLore-Version: 2.0.0
…ument with it
The mutation runner's first honest run is red: thirteen exclusion-index kinds have no
expressible control, one path scan is inert, one control is unavailable. Wiring that into
the gate's `needs` made the branch unmergeable, and a gate nobody can pass is removed
rather than fixed. I made this mistake earlier in this session with a CI-must-run
assertion no runner could satisfy, so the same shape twice.
So the job fails on regression against a recorded baseline instead of on the backlog.
Four directions, and the fourth is the one that keeps the file honest:
a bound property degrades FAIL
a new property arrives with no mutations FAIL
a recorded gap stays a gap reported, exit 0
a recorded gap becomes bound FAIL, tighten the baseline
Without the fourth a ratchet rots: improvements accumulate while the record still claims
the old gaps, and a reader cannot tell which gaps are real. Making repair fail until the
baseline moves keeps measurement and record in step.
Every gap carries its reason in the claim's own words -- "the census matches exclusion rows
by value only, so this task identity is not represented in the candidate values the claim
would need to make ineligible" -- because a missing test and a missing feature need
different work and the outcome alone cannot tell them apart. Twelve of the thirteen gaps
are the second kind.
The runner also caught a real regression while this was being built: the tampered-bundle
mutation had been deleted during a negative control and not restored, so a property the
baseline recorded as bound measured uncovered. The tool found its own author's mistake on
its first live use, which is the most useful thing it could have done.
Record-Id: r-guardratchet
Provenance: authored
Certainty: firm
Blast: system
Undo: easy
Ruled-out: leaving the job in the gate while it is red | branch protection would block every merge until someone deleted the job, and deleting it removes the only thing that can see these gaps
Ruled-out: allowing an improvement without updating the baseline | the record would drift below the measurement, and a baseline that overstates the gaps is as useless as one that understates them
Ruled-out: recording gaps as a count instead of per property with a reason | a count cannot distinguish a control nobody wrote from one that cannot exist, and those need different work
Limit: the baseline is a floor. A guard can bind its claim against the one mutation recorded for it and still miss a different violation of the same claim
Limit: the reasons are written by the same author as the claims, so a gap reasoned narrowly can look more settled than it is
Limit: thirteen exclusion kinds remain uncovered and one scan inert; this records them and repairs neither
Verified: the runner exits 0 against the current tree, prints all four outcome classes with per-property reasons, and the summary is 13 bound, 1 inert, 1 unavailable, 13 uncovered across 15 mutations. Three negative controls observed and restored -- a mutation removed from a bound property, a property added with an empty mutation list, and a baseline gap marked bound without repair -- each failing as a distinct named reason. Both typechecks clean, ci-gate suite green
CommitLore-Version: 2.0.0
CommitLore — record lintTrailers: clean — 3 commits in Active constraints for the paths this PR touchesLimits (67)
Ruled out (128)
Warnings (15)
Trailer violations fail this check. Active constraints are informational — they are what the repository already decided, not a verdict on this PR. |
…list of eleven
`REQUIRED_CHECKS` names the jobs a release must see. The release-gate suites built their
job fixtures from a hand-written copy of that list, so adding `guard-mutations` made the
two disagree: the verifier reported the missing job first, and every test asserting a
specific downstream message never reached it.
× refuses a required job that failed
→ expected 'ERROR: exact-head CI did not pass for…' to contain 'conclusion "failure"'
A list written beside the thing it checks agrees with itself by construction. That is the
shape already recorded in this repository from `check (22.23.2)` and from `lint`'s
pull_request trigger, and it is why a one-line addition took twenty tests down.
The fixtures derive their job lists from `REQUIRED_CHECKS` now, mutating only the single
job each case is about. A thirteenth required job will not touch them.
Record-Id: r-reqchecksfixture
Provenance: authored
Certainty: firm
Blast: local
Undo: easy
Ruled-out: adding guard-mutations to each fixture's copy of the list | it fixes today and leaves the next addition to break the same twenty tests
Ruled-out: dropping guard-mutations from REQUIRED_CHECKS so the suites pass | the job exists to be required, and a required check the release gate does not know about is the gap this list closes
Limit: the fixtures now agree with REQUIRED_CHECKS by construction, so a job that should be required but was never added to that list is still invisible here; the list itself remains the single named site
Verified: 36 cases across the ci-gate and release-prerequisite suites, both typechecks clean, and the mutation ratchet still exits 0 at 13 bound, 1 inert, 1 unavailable, 13 uncovered. Negative control observed and restored -- an unknown name added to REQUIRED_CHECKS leaves 19 exact-head cases and the tag-binding case passing, which is the property being bought
CommitLore-Version: 2.0.0
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
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.
Five times in this session a guard was written, its negative control ran, the control failed as expected, and the guard still proved nothing.
Every control was derived from the guard's implementation, in the guard's vocabulary. That confirms the mechanism runs. It cannot confirm the claim, because the claim was never written anywhere a control could come from.
Claims, not functions
bench/cdeb/guards/registry.jsonindexes 21 claims — sentences about the study, not about the code. If a claim cannot be stated without naming a function, it is describing a mechanism and gets rewritten.The runner reports four outcomes instead of pass/fail:
The last two used to disappear. A property nobody could write a control for, and one nobody tried to, both looked identical to one that passed.
A ratchet, not a wall
The first honest run is red. Putting that in
gate'sneedsmakes the branch unmergeable, and a gate nobody can pass gets deleted — taking the instrument with it. (I made exactly this mistake earlier in this session with a CI-must-run assertion no runner could satisfy.)So the job fails on regression against a baseline:
Without the fourth direction a ratchet rots: improvements accumulate while the record still claims the old gaps. Making repair fail until the baseline moves keeps measurement and record in step.
Current state, recorded per property with its reason
Each gap carries its reason in the claim's own words — "the census matches exclusion rows by value only, so this task identity is not represented in the candidate values the claim would need to make ineligible" — because a missing test and a missing feature need different work. Twelve of thirteen gaps are the second kind, which is the same conclusion an adversarial review reached independently by reading the code.
It caught its author on first use
While this was being built, a negative control removed the tampered-bundle mutation and did not restore it. A property the baseline recorded as
boundmeasureduncovered, and the ratchet failed with exactly that sentence. Restored and re-verified.Verification
Runner exits 0 on the current tree. Three negative controls observed and restored — a mutation removed from a bound property, a property added with an empty mutation list, and a baseline gap marked bound without repair — each failing with a distinct named reason. Both typechecks clean,
ci-gatesuite green.Limits, in the commit
The baseline is a floor: a guard can bind against its one recorded mutation and still miss a different violation of the same claim. Reasons are written by the same author as the claims. Thirteen exclusion kinds remain uncovered and one scan inert — this records them and repairs neither.