fix(881): a GREEN claim is only readable if its proof REACHES the clause
Round three found the one half of the new mechanism with no relevance gate. `verify_claim`'s GREEN path read exactly two things — the run exited 0, and something PASSED — and both are satisfied by a proof that never touches the mutated file at all. Reproduced before fixing: retargeting the shipped GREEN entry's proof from `test_check_doc_narrative.py` to `test_bom_guard_detection.py` changed nothing, and the entry still reported verified. The RED direction never had this hole, because a proof that ignores the mutation stays green and is refused as "the clause is not load-bearing". So a GREEN entry now declares a `reach_replacement` and its `reach_expect`: a SECOND mutation of the SAME clause, required to REDDEN the same proof, executed through `verify_mutation` so its red is read through the diagnostic gate rather than on exit status. The shipped entry declares `path = p` — dropping the `b/` stripping every scanned diff header goes through — and the run then scans NOTHING, which is what the declared diagnostic reads. The same retarget now fails, naming the reach verdict. The gate runs LAST of the three: run first it would refuse before the status and vacuity gates were read and neither could be witnessed failing alone (#685), and the sandbox is reset between a claim's two proof runs for the reason it is reset between mutations. It has its own disarm proof, and the two synthetic claim sandboxes are now real git repositories so `reset_sandbox` has a baseline; `_lib_with` shares the baseline registry, since a copied module's own starts empty. Also from that round: - The record no longer counts the mutation-outcome claims in the pinned proposal-3 scan. A third of the same shape sits in the same result set (`test_a_verdict_BEYOND_A_SHORT_PAGE_is_still_found`), and which side of the line a sentence falls on is a judgement, so an exact count is a figure the next reader re-derives differently — the failure this record is about. - The calibration paragraph no longer restates the post-review-verdict outcome as a dated witnessing. It points at the `CLAIMS` entry that executes it, which is the form the rewritten shell comment beside it demands. - The comment in `check-doc-narrative.py` claimed a universal ("reddens no test") while one file is executed. It now names that file, so the quote binds an outcome no wider than what is checked. - Proposal 4 from the issue is dispositioned explicitly: rejected as a rule here, on the issue's own argument that an exhortation does not fire at the moment of least slack. - `docs/README.md`'s task-signal parenthetical now names the `CLAIMS` population; the file was owned by another slot when this branch started. Cost re-measured 2026-09-05, three baseline/branch pairs: the `CLAIMS` half adds 31.7-43.6%, up from the 12.7-16.6% measured before the gate existed. The old figure is retired rather than scaled — growing the population invalidates the measurement that described it. Refs #881 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015QqCpYFsKgnAnx6jVwrKiV
This commit is contained in:
Claude Fable 5.1
+1
-1
@@ -28,7 +28,7 @@ doc below, or that changes which sections a task signal points to.**
|
||||
| Concurrency / optimistic-locking work | `docs/api-conventions.md` §7a/b/c + `docs/decisions/optimistic-concurrency.md` |
|
||||
| Auth / security-surface work | `docs/decisions/api-auth-security.md` |
|
||||
| CI / release pipeline work | `docs/ci-cd.md` + `docs/decisions/release-ci-governance.md` |
|
||||
| Proposing a new guard / CI check / regression test convention | `docs/defect-shapes-773.md` §4 (detector menu + the classes where no detector is plausible), then the rules every guard must satisfy: `docs/decisions/records/testing/guard-derives-population-from-source.md`, `…/guard-ships-with-mutation-proof.md` and `…/mutation-claims-are-executed.md` (a `MUTATION` grade carries a DECLARED clause mutation that is re-run every suite) — plus `…/verification-code-needs-its-own-proof.md`, which extends the same obligation BEYOND guards to the harness, wrapper or checker doing the checking, and says where its proof lives when the checker holds no row |
|
||||
| Proposing a new guard / CI check / regression test convention | `docs/defect-shapes-773.md` §4 (detector menu + the classes where no detector is plausible), then the rules every guard must satisfy: `docs/decisions/records/testing/guard-derives-population-from-source.md`, `…/guard-ships-with-mutation-proof.md` and `…/mutation-claims-are-executed.md` (a `MUTATION` grade carries a DECLARED clause mutation that is re-run every suite — and so does a PROSE claim that some mutation reddens, or does not redden, a named test, wherever it is written: it is a `CLAIMS` entry in the same manifest, bound to its site and verbatim quote, or it is not written) — plus `…/verification-code-needs-its-own-proof.md`, which extends the same obligation BEYOND guards to the harness, wrapper or checker doing the checking, and says where its proof lives when the checker holds no row |
|
||||
| Adding or bounding a consequential numeric config field (an FFmpeg profile tunable, a pipeline knob) | `docs/api-conventions.md` §3d — reject out of range with a 422 naming the bound and its consequence, never accept-then-rewrite; validate against the constants the renderer reads, keep the render-time clamp for pre-existing rows, and let an UNCHANGED legacy value through on update. Then `api.ffmpeg-profile-numeric-bounds` |
|
||||
| Testing a surface gated by config / an env var / a credential | `docs/decisions/records/testing/deny-path-at-production-config-value.md` — cover the setting absent, at its production value, and each opt-out, and assert the DENY branch |
|
||||
| Touching a full-replace write path or a hand-built request object | `docs/decisions/records/testing/full-replace-asserts-field-list.md` — derive the field list from the DTO and assert set equality; reconcile by id where child state exists. In the SPA the same rule is enforced by the type system: `docs/spa-conventions.md` §4b — build the body as `Complete<T>`, annotating BOTH the wrapper parameter and every construction site |
|
||||
|
||||
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
@@ -374,8 +374,11 @@ graded `MUTATION` without declaring its clause fails the suite. Full contract an
|
||||
docstring or a decision record asserting that some mutation reddens, or does not redden, a named
|
||||
test — to the file and the sentence that make them (ersatztv#881). Those entries carry a `site` and
|
||||
a verbatim `quote` instead of a guard, so a rewritten sentence reports as a retarget; and they may
|
||||
declare a GREEN outcome, which no row here can. A guard's row says nothing about whether a claim
|
||||
about that guard has been declared, and the two populations are derived differently on purpose.
|
||||
declare a GREEN outcome, which no row here can — one that also declares a REACH mutation of the same
|
||||
clause required to redden the same proof, because a green from a proof that never touches the mutated
|
||||
file is indistinguishable from the green the sentence claims. A guard's row says nothing about
|
||||
whether a claim about that guard has been declared, and the two populations are derived differently
|
||||
on purpose.
|
||||
|
||||
One thing that column still does not say: it does not say the declared clause is the ONLY thing the
|
||||
guard hangs on — for three rows (measured 2026-08-22) the redness arrives through the
|
||||
|
||||
@@ -186,7 +186,11 @@ def added_lines(diff: str):
|
||||
p = raw[4:]
|
||||
# `/dev/null` on the new side means the file was DELETED. Stated honestly: this arm
|
||||
# is DEFENSIVE, not load-bearing — a deletion contributes no `+` lines, so nothing is
|
||||
# yielded for it either way, and removing this arm reddens no test. It is kept because
|
||||
# yielded for it either way. Measured rather than asserted, and re-measured on every
|
||||
# run: `test_check_doc_narrative.py` stays green with this arm removed, a declared
|
||||
# claim in `scripts/tests/mutation_manifest.py` (ersatztv#881). The named file is the
|
||||
# scope that is actually executed — a claim over every test in the repository would
|
||||
# be wider than anything re-taking it. The arm is kept because
|
||||
# `path` should never name a file the added lines do not belong to. A
|
||||
# `--diff-filter=d` on the git call was removed rather than kept beside it: a second
|
||||
# mechanism nobody can witness failing is how a duplicate guard hides its twin.
|
||||
|
||||
@@ -130,8 +130,20 @@ class Claim:
|
||||
dead branch left that branch's own test green. Each is a claim that a mutation is NOT noticed,
|
||||
and the rule "declare it or do not write it" is unsatisfiable for them unless the harness can
|
||||
execute a negative. A GREEN entry therefore carries NO `expect`: there is no failing run to read a
|
||||
diagnostic out of, and the two things that could make a green vacuous — a run that errored, and a
|
||||
run in which nothing passed — are checked in `verify_claim` instead.
|
||||
diagnostic out of, and the three things that could make a green vacuous — a run that errored, a
|
||||
run in which nothing passed, and a proof that never reaches the mutated clause at all — are
|
||||
checked in `verify_claim` instead.
|
||||
|
||||
THE THIRD OF THOSE IS WHAT MAKES A GREEN READABLE, and it needs its own declaration. A red is
|
||||
self-checking: a proof that ignores the mutated file stays green and `verify_mutation` refuses it,
|
||||
naming the clause as not load-bearing. A green has no such property — an unrelated proof produces
|
||||
exactly the green the sentence claims, so exit status and "something passed" together still
|
||||
certify a run that never executed the clause. `reach_replacement` closes that: a SECOND mutation
|
||||
of the SAME clause, declared to REDDEN the same proof with the diagnostic in `reach_expect`, and
|
||||
executed through `verify_mutation` so the red is read exactly as a `MUTATION` row's is. Passing it
|
||||
means the proof reaches this clause and its value changes what the proof observes; only then does
|
||||
the declared green say anything. RED entries leave both fields empty — there is nothing there for
|
||||
them to add.
|
||||
|
||||
What a GREEN claim is worth is exactly what the retired `DETECTOR` survivor was worth: it is
|
||||
re-run and required to KEEP surviving, so the day the mutation starts being noticed the entry
|
||||
@@ -151,6 +163,8 @@ class Claim:
|
||||
outcome: str
|
||||
expect: str
|
||||
why: str
|
||||
reach_replacement: str = ""
|
||||
reach_expect: str = ""
|
||||
|
||||
@property
|
||||
def node_id(self) -> str:
|
||||
@@ -404,12 +418,21 @@ def verify_claim(sandbox: Path, claim: Claim) -> Verdict:
|
||||
how the two would come to disagree about what a red is worth (exit status, diagnostic, an
|
||||
already-red proof).
|
||||
|
||||
GREEN is the direction that has no equivalent above, and it is checked by TWO separate clauses
|
||||
because either alone is satisfiable by a run that proves nothing. Exit status alone accepts a run
|
||||
in which every test SKIPPED — pytest exits 0 for that — and "something passed" alone accepts a
|
||||
file that also failed. They are kept apart rather than combined into one condition so each can be
|
||||
disarmed on its own and seen to matter; a single clause covering both would be a guard nothing
|
||||
can witness failing.
|
||||
GREEN is the direction that has no equivalent above, and it is checked by THREE separate clauses
|
||||
because each alone is satisfiable by a run that proves nothing. Exit status alone accepts a run
|
||||
in which every test SKIPPED — pytest exits 0 for that — "something passed" alone accepts a file
|
||||
that also failed, and both together still accept a proof that never touches the mutated file:
|
||||
an unrelated test run produces the same green as the claimed one. That last one is answered by
|
||||
the entry's declared `reach_replacement`, a second mutation of the SAME clause required to REDDEN
|
||||
the same proof. They are kept apart rather than combined into one condition so each can be
|
||||
disarmed on its own and seen to matter; a single clause covering all three would be a guard
|
||||
nothing can witness failing.
|
||||
|
||||
THE RELEVANCE GATE RUNS LAST, and the order is load-bearing rather than incidental. Run first, it
|
||||
would refuse before the status and vacuity gates were ever read, and neither could then be
|
||||
witnessed failing on its own — two gates that mask each other are worth one (#685). The sandbox is
|
||||
reset between the two runs because the first proof run can dirty the tree, and a second result
|
||||
that is a function of the first's is what `reset_sandbox` exists to prevent.
|
||||
"""
|
||||
if claim.outcome == Claim.RED:
|
||||
return verify_mutation(
|
||||
@@ -454,4 +477,33 @@ def verify_claim(sandbox: Path, claim: Claim) -> Verdict:
|
||||
"deselected or absent. A green nothing ran is not evidence that the mutation went "
|
||||
f"unnoticed.\n--- inner pytest output ---\n{output[-3000:]}",
|
||||
)
|
||||
return Verdict(True, "the named proof stayed green under the declared mutation, with tests actually run")
|
||||
|
||||
reset_sandbox(sandbox)
|
||||
reach = verify_mutation(
|
||||
sandbox,
|
||||
Mutation(
|
||||
guard=claim.site,
|
||||
target=claim.target,
|
||||
clause=claim.clause,
|
||||
replacement=claim.reach_replacement,
|
||||
proof=claim.proof,
|
||||
granularity=Mutation.CLAUSE,
|
||||
expect=claim.reach_expect,
|
||||
why=claim.why,
|
||||
),
|
||||
)
|
||||
if not reach.ok:
|
||||
return Verdict(
|
||||
False,
|
||||
f"{claim.proof} stayed green under the declared mutation, but the DECLARED REACH "
|
||||
"mutation of the same clause did not redden it, so that green is not evidence about "
|
||||
"this clause: a proof that never executes it produces exactly the same result. Either "
|
||||
"the proof no longer reaches the clause — in which case the sentence at "
|
||||
f"{claim.site} is about something this proof cannot see — or the reach mutation itself "
|
||||
f"needs re-declaring.\n--- the reach verdict ---\n{reach.reason}",
|
||||
)
|
||||
return Verdict(
|
||||
True,
|
||||
"the named proof stayed green under the declared mutation, with tests actually run, and "
|
||||
"reddened under the declared reach mutation of the same clause",
|
||||
)
|
||||
|
||||
@@ -326,7 +326,8 @@ MUTATIONS: tuple[Mutation, ...] = (
|
||||
"INVENTORY HOLDS ONE REF PER ROW, so this entry names the gate verified rows hang on most "
|
||||
"directly, and the gates that read a proof RUN carry disarm proofs of their own: "
|
||||
"`test_MUTATION_disarming_the_EXIT_STATUS_gate_accepts_a_run_that_NEVER_RAN_A_TEST` for the "
|
||||
"exit-status gate and, on the GREEN direction `CLAIMS` uses, the status and vacuity gates. "
|
||||
"exit-status gate and, on the GREEN direction `CLAIMS` uses, the status, vacuity and "
|
||||
"relevance gates. "
|
||||
"So does the PRE-FLIGHT refusal that no later gate can stand in for — a replacement "
|
||||
"identical to its clause mutates nothing, so the proof runs against the original tree and "
|
||||
"an already-red one reddens exactly like a detection: "
|
||||
@@ -596,6 +597,15 @@ UNDECLARED: dict[str, str] = {
|
||||
# exactly what the retired `DETECTOR` survivor was worth: it is required to KEEP surviving, and the
|
||||
# day the mutation starts being noticed the entry reddens and the sentence has to be rewritten.
|
||||
#
|
||||
# A GREEN ENTRY ALSO DECLARES ITS `reach_replacement`, AND IS WORTHLESS WITHOUT IT. The two
|
||||
# directions are not symmetric: a RED claim checks itself, because a proof that never executes the
|
||||
# mutated file stays green and the harness refuses it in the same words it refuses a clause that has
|
||||
# stopped being load-bearing. A GREEN claim has no such property — an unrelated proof produces
|
||||
# exactly the green the sentence asserts, so a green certifies nothing until the proof is shown to
|
||||
# reach the clause. `reach_replacement` is a SECOND mutation of the SAME clause, declared to redden
|
||||
# the same proof with `reach_expect`, and it is executed through the same `verify_mutation` the rows
|
||||
# above use, so its red is read exactly as theirs is rather than on exit status.
|
||||
#
|
||||
# No count is kept here either, for the reason stated at the top of this file.
|
||||
|
||||
CLAIMS: tuple[Claim, ...] = (
|
||||
@@ -628,19 +638,30 @@ CLAIMS: tuple[Claim, ...] = (
|
||||
),
|
||||
Claim(
|
||||
site="scripts/check-doc-narrative.py",
|
||||
quote="removing this arm reddens no test",
|
||||
quote="`test_check_doc_narrative.py` stays green with this arm removed",
|
||||
target="scripts/check-doc-narrative.py",
|
||||
clause=' path = None if p == "/dev/null" else (p[2:] if p.startswith("b/") else p)',
|
||||
replacement=' path = p[2:] if p.startswith("b/") else p',
|
||||
proof="test_check_doc_narrative.py",
|
||||
outcome=GREEN,
|
||||
expect="",
|
||||
# THE RELEVANCE GATE, and without it this entry certifies nothing: a proof that never
|
||||
# executes this line produces exactly the green the sentence predicts. The reach mutation
|
||||
# drops the `b/` stripping the same expression performs, so every `+++ b/<path>` header
|
||||
# resolves to a path `is_scanned_path` rejects and the run scans NOTHING — which is what the
|
||||
# declared diagnostic reads, from the ACTUAL half of the comparison rather than the expected
|
||||
# one. Passing it means the proof reaches this clause and what the clause computes changes
|
||||
# what the proof observes, which is the precondition the green half needs and cannot supply.
|
||||
reach_replacement=" path = p",
|
||||
reach_expect="scanned 0 file(s); 0 advisory warning(s)",
|
||||
why="The `/dev/null` arm is declared DEFENSIVE in its own comment — a deleted file "
|
||||
"contributes no `+` lines, so nothing is yielded for it either way. The comment says so and "
|
||||
"then says removing the arm reddens no test, which is a measurement, and until this entry "
|
||||
"nothing re-took it. The mutation removes exactly the arm the comment is about, leaving the "
|
||||
"`b/` stripping it is wrapped around, so a red here would mean the arm has become "
|
||||
"load-bearing and the comment is now wrong.",
|
||||
"then names an outcome, which is a measurement, and until this entry nothing re-took it. The "
|
||||
"mutation removes exactly the arm the comment is about, leaving the `b/` stripping it is "
|
||||
"wrapped around, so a red here would mean the arm has become load-bearing and the comment is "
|
||||
"now wrong. The quote names the proof FILE rather than every test in the repository, because "
|
||||
"the file is what the harness runs: an outcome half broader than the executed scope is the "
|
||||
"same drift in miniature.",
|
||||
),
|
||||
Claim(
|
||||
site="docs/decisions/records/docs/record-wing-parse-guard.md",
|
||||
|
||||
@@ -267,7 +267,7 @@ def test_every_CLAIM_is_BOUND_to_the_PROSE_it_justifies():
|
||||
)
|
||||
|
||||
|
||||
def test_every_CLAIM_declares_a_DIRECTION_and_only_a_RED_carries_a_DIAGNOSTIC():
|
||||
def test_every_CLAIM_declares_a_DIRECTION_and_the_FIELDS_THAT_DIRECTION_NEEDS():
|
||||
"""RED and GREEN are read differently, and the shape has to say which before anything runs.
|
||||
|
||||
A RED claim is the assertion a `MUTATION` row makes and needs the same specific diagnostic: exit
|
||||
@@ -275,6 +275,14 @@ def test_every_CLAIM_declares_a_DIRECTION_and_only_a_RED_carries_a_DIAGNOSTIC():
|
||||
out of, so an `expect` on one could only be dead text — and dead text beside a live field is how
|
||||
a reader comes to believe something is checked. `verify_claim` owns the unknown-outcome case, so
|
||||
it is deliberately not re-asserted here; two copies of one rule is how they come to disagree.
|
||||
|
||||
THE REACH FIELDS ARE REQUIRED ON A GREEN AND FORBIDDEN ON A RED, and that asymmetry is the whole
|
||||
difference between the two directions. A red is self-checking: a proof that never executes the
|
||||
mutated file stays green and the harness refuses the entry. A green is not — an unrelated proof
|
||||
produces the same green the sentence claims — so a GREEN entry must declare a second mutation of
|
||||
the same clause that DOES redden its proof, with its own specific diagnostic, or the entry is
|
||||
unreadable. A RED entry declaring them would be dead text of exactly the kind the `expect` rule
|
||||
above rejects.
|
||||
"""
|
||||
for claim in CLAIMS:
|
||||
if claim.outcome == Claim.RED:
|
||||
@@ -282,11 +290,27 @@ def test_every_CLAIM_declares_a_DIRECTION_and_only_a_RED_carries_a_DIAGNOSTIC():
|
||||
f"{claim.site}: a RED claim needs a specific diagnostic, not {claim.expect!r} — "
|
||||
"otherwise any red at all satisfies it, including a crash."
|
||||
)
|
||||
assert claim.reach_replacement == "" and claim.reach_expect == "", (
|
||||
f"{claim.site}: a RED claim must declare no reach mutation. Its own mutation already "
|
||||
"proves the proof reaches the clause — a green there is what the harness refuses — "
|
||||
"so these fields would be read by nothing."
|
||||
)
|
||||
elif claim.outcome == Claim.GREEN:
|
||||
assert claim.expect == "", (
|
||||
f"{claim.site}: a GREEN claim must carry no `expect` ({claim.expect!r}). There is no "
|
||||
"failing run to match it against, so it would read as a check and be none."
|
||||
)
|
||||
assert claim.reach_replacement and claim.reach_replacement != claim.replacement, (
|
||||
f"{claim.site}: a GREEN claim must declare a `reach_replacement` distinct from the "
|
||||
"mutation it claims is unnoticed. Without one, a proof that never executes this "
|
||||
"clause produces exactly the green the sentence asserts and the entry certifies "
|
||||
"nothing."
|
||||
)
|
||||
assert len(claim.reach_expect.strip()) >= 20, (
|
||||
f"{claim.site}: the reach mutation's diagnostic is {claim.reach_expect!r}. It is read "
|
||||
"by the same gate a RED claim's is, and for the same reason: a red for an unrelated "
|
||||
"reason would certify reach the proof does not have."
|
||||
)
|
||||
assert claim.why.strip(), f"{claim.site}: every claim must say what its mutation does"
|
||||
assert claim.target and claim.clause and claim.replacement, f"{claim.site}: incomplete mutation"
|
||||
|
||||
@@ -321,11 +345,15 @@ def sandbox(tmp_path_factory):
|
||||
# directions: over a proof that was ALREADY red, a RED claim is satisfied by redness its mutation
|
||||
# did not cause, and a GREEN claim is refused for a reason that has nothing to do with its
|
||||
# mutation — reported as a wrong sentence when what is wrong is the proof.
|
||||
# WHAT THIS CONTROL CANNOT DO, so it is not read as more: it cannot see a single ref that
|
||||
# collects nothing. Both assertions below are over the AGGREGATE of every ref, so the word
|
||||
# `passed` is supplied by the others. That discrimination is per-claim and lives in
|
||||
# `verify_claim`'s own vacuity gate, disarmed and witnessed in
|
||||
# `test_MUTATION_disarming_the_GREEN_VACUITY_gate_accepts_a_run_in_which_NOTHING_PASSED`.
|
||||
# WHAT THIS CONTROL CANNOT DO, so it is not read as more. It cannot see a single ref that
|
||||
# collects nothing — both assertions below are over the AGGREGATE of every ref, so the word
|
||||
# `passed` is supplied by the others. Nor can it see a ref that collects plenty and reaches
|
||||
# NOTHING the claim mutates, which is the larger of the two: such a proof is green here and green
|
||||
# under the mutation, and a GREEN claim would read as verified on a run that never executed its
|
||||
# clause. Both discriminations are per-claim and live in `verify_claim` — its vacuity gate and
|
||||
# its relevance gate — each disarmed and witnessed in
|
||||
# `test_MUTATION_disarming_the_GREEN_VACUITY_gate_accepts_a_run_in_which_NOTHING_PASSED` and
|
||||
# `test_MUTATION_disarming_the_GREEN_RELEVANCE_gate_accepts_a_proof_that_NEVER_REACHES_THE_CLAUSE`.
|
||||
result = run_pytest(sb, node_ids)
|
||||
assert result.returncode == 0, (
|
||||
"the proof tests named by the inventory are NOT green on an unmutated copy of this "
|
||||
@@ -461,11 +489,13 @@ def test_every_SURVIVING_clause_mutation_still_does(sandbox, mutation):
|
||||
|
||||
EXIT_STATUS_CLAUSE = " if result.returncode != 1:"
|
||||
DIAGNOSTIC_CLAUSE = " if mutation.expect not in diagnostic:"
|
||||
# The GREEN direction's two gates (#881). They are separate clauses precisely so each can be
|
||||
# disarmed alone: a run that ERRORED and a run in which NOTHING PASSED are different ways for a
|
||||
# green to be worthless, and a single condition covering both is a guard nothing can witness failing.
|
||||
# The GREEN direction's three gates (#881). They are separate clauses precisely so each can be
|
||||
# disarmed alone: a run that ERRORED, a run in which NOTHING PASSED and a proof that never reaches
|
||||
# the mutated clause are different ways for a green to be worthless, and a single condition covering
|
||||
# them is a guard nothing can witness failing.
|
||||
GREEN_STATUS_CLAUSE = " if result.returncode != 0:"
|
||||
GREEN_VACUITY_CLAUSE = ' if "passed" not in output:'
|
||||
GREEN_RELEVANCE_CLAUSE = " if not reach.ok:"
|
||||
# The PRE-FLIGHT refusal that decides before any proof runs and still needs a disarm proof: a
|
||||
# replacement equal to its clause writes the target back unchanged, so what the proof ref then runs
|
||||
# against is the ORIGINAL tree.
|
||||
@@ -519,6 +549,11 @@ def _lib_with(tmp_path: Path, clause: str, replacement: str, label: str):
|
||||
spec.loader.exec_module(mutant)
|
||||
finally:
|
||||
sys.modules.pop(spec.name, None)
|
||||
# The copy's `_BASELINES` starts EMPTY — it is a fresh module object — so a sandbox registered
|
||||
# with the real library is invisible to it and its `reset_sandbox` would refuse a tree it has no
|
||||
# baseline for. Share the registry rather than rebuilding the sandbox for the mutant: the subject
|
||||
# of every proof below is one clause of this copy, not where its sandbox came from.
|
||||
mutant._BASELINES.update(_BASELINES)
|
||||
return mutant
|
||||
|
||||
|
||||
@@ -646,21 +681,39 @@ def test_the_sandbox_is_left_UNCHANGED_by_a_verdict(tmp_path):
|
||||
|
||||
|
||||
# ------------------------------------------------------------------------------------------------
|
||||
# THE GREEN DIRECTION'S OWN PROOFS — two gates, each disarmed ALONE (ersatztv#881)
|
||||
# THE GREEN DIRECTION'S OWN PROOFS — three gates, each disarmed ALONE (ersatztv#881)
|
||||
# ------------------------------------------------------------------------------------------------
|
||||
|
||||
# The reach mutation these fixtures declare: it replaces the marker with a test that FAILS, so the
|
||||
# proof reddens with a diagnostic nothing else in the fixture produces. That is what a real reach
|
||||
# declaration does — a second mutation of the same clause whose red is read through the diagnostic
|
||||
# gate, not through exit status.
|
||||
_REACH_DIAGNOSTIC = "a deliberate failure the reach mutation injects"
|
||||
_REACH_REPLACEMENT = f'def test_reach_red():\n assert False, "{_REACH_DIAGNOSTIC}"'
|
||||
|
||||
def _inert_claim_sandbox(tmp_path: Path, body: str) -> tuple[Path, Claim]:
|
||||
|
||||
def _inert_claim_sandbox(tmp_path: Path, body: str, reach_replacement: str = _REACH_REPLACEMENT) -> tuple[Path, Claim]:
|
||||
"""A synthetic sandbox holding one test file, and a GREEN claim over it.
|
||||
|
||||
The claim's mutation is an inert comment edit, so whatever the file's tests do under it is what
|
||||
they do without it — which is what isolates the VERDICT's reading of the result from the
|
||||
mutation's effect. `body` decides the outcome each proof below needs.
|
||||
mutation's effect. `body` decides the outcome each proof below needs, and `reach_replacement`
|
||||
decides what the relevance gate sees; the default reddens, so a caller testing an EARLIER gate
|
||||
is not stopped by this one.
|
||||
|
||||
It is a REAL git repository, unlike `_inert_sandbox` above, because `verify_claim` resets between
|
||||
its two runs and `reset_sandbox` refuses a tree it has no recorded baseline for. Registering the
|
||||
baseline is what `build_sandbox` does for the repo-sized one; here it is three git calls.
|
||||
"""
|
||||
tests = tmp_path / "scripts" / "tests"
|
||||
sb = tmp_path / "sb"
|
||||
tests = sb / "scripts" / "tests"
|
||||
tests.mkdir(parents=True)
|
||||
(tests / "test_inert.py").write_text(f"# INERT MARKER\n{body}")
|
||||
return tmp_path, Claim(
|
||||
_git(sb, "init", "-q", ".")
|
||||
_git(sb, "add", "-A", "-f", ".")
|
||||
_git(sb, "commit", "-qm", "inert claim sandbox")
|
||||
_BASELINES[str(sb.resolve())] = _git(sb, "rev-parse", "HEAD").stdout.decode().strip()
|
||||
return sb, Claim(
|
||||
site="scripts/tests/test_inert.py",
|
||||
quote="a sentence this fixture does not have to contain, since the binding is checked elsewhere",
|
||||
target="scripts/tests/test_inert.py",
|
||||
@@ -670,6 +723,8 @@ def _inert_claim_sandbox(tmp_path: Path, body: str) -> tuple[Path, Claim]:
|
||||
outcome=Claim.GREEN,
|
||||
expect="",
|
||||
why="an inert mutation over a file whose outcome the fixture fixes",
|
||||
reach_replacement=reach_replacement,
|
||||
reach_expect=_REACH_DIAGNOSTIC,
|
||||
)
|
||||
|
||||
|
||||
@@ -722,3 +777,34 @@ def test_MUTATION_disarming_the_GREEN_VACUITY_gate_accepts_a_run_in_which_NOTHIN
|
||||
"the green-direction vacuity gate was replaced with a constant and a run in which no test "
|
||||
"passed was still rejected, so the verdict does not hang on the clause that reads it"
|
||||
)
|
||||
|
||||
|
||||
def test_MUTATION_disarming_the_GREEN_RELEVANCE_gate_accepts_a_proof_that_NEVER_REACHES_THE_CLAUSE(tmp_path):
|
||||
"""The third gate, and the one the other two cannot stand in for.
|
||||
|
||||
This is the hole in the shape: a proof that never executes the mutated clause exits 0 with tests
|
||||
genuinely passing, so the status gate and the vacuity gate both accept, and the run is
|
||||
indistinguishable from the green the sentence claims. Only the declared reach mutation separates
|
||||
them — and here it does not redden either, which is exactly what a proof that reads a different
|
||||
file looks like.
|
||||
|
||||
The fixture makes the reach mutation inert too, rather than pointing the proof at a second file:
|
||||
"the proof does not depend on this clause" is the property under test, and an inert mutation of
|
||||
the clause is that property in its smallest form. `verify_mutation` refuses it in the words it
|
||||
uses for a clause that has stopped being load-bearing, which is the same fact from the other end.
|
||||
"""
|
||||
sb, claim = _inert_claim_sandbox(
|
||||
tmp_path,
|
||||
"\n\ndef test_ok():\n assert True\n",
|
||||
reach_replacement="# INERT MARKER, ALSO CHANGED",
|
||||
)
|
||||
|
||||
verdict = verify_claim(sb, claim)
|
||||
assert not verdict.ok, "a green produced by a proof that never reaches the clause was accepted"
|
||||
assert "DECLARED REACH" in verdict.reason, verdict.reason
|
||||
|
||||
mutant = _lib_with(tmp_path, GREEN_RELEVANCE_CLAUSE, " if False:", "green relevance gate")
|
||||
assert mutant.verify_claim(sb, claim).ok, (
|
||||
"the relevance gate was replaced with a constant and a green from a proof that does not "
|
||||
"depend on the clause was still rejected, so the verdict does not hang on the reach mutation"
|
||||
)
|
||||
|
||||
Reference in New Issue
Block a user