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
811 lines
46 KiB
Python
811 lines
46 KiB
Python
"""Every `MUTATION` row of `docs/guard-inventory.md` is EXECUTED, not asserted (ersatztv#790).
|
|
|
|
The `MUTATION` grade means "a clause-level mutation was executed and this named test was witnessed
|
|
red". Witnessed once, by hand, that is evidence about the day the row was written and nothing else:
|
|
it decays as soon as the guard is edited, and a wrong grade has no way to announce itself.
|
|
|
|
So this file re-runs every one of them: for each declared mutation in `mutation_manifest.py`, apply
|
|
it to an isolated copy of this repository and require the row's OWN named test to go red.
|
|
|
|
WHAT A GREEN RUN HERE DOES AND DOES NOT PROVE — stated because a mutation harness that overclaims is
|
|
the same defect one level up:
|
|
|
|
* It proves the recorded proof ref names a test that EXISTS, still collects, and still reacts to
|
|
the declared clause. That is precisely the decay #790 was filed about.
|
|
* It proves the declared clause still occurs, exactly once, in the entry's declared `target` —
|
|
which is not always the guard's own file. A clause that has been reworded fails here rather than
|
|
silently mutating nothing.
|
|
* Combined with the positive control below, it proves every named proof test is GREEN on the
|
|
unmutated sandbox — so "the mutation was noticed" cannot be confused with "the test was already
|
|
red". For the proof tests that perform a disarm of their own, that control also runs the disarm;
|
|
the two named tests that are plain production set-equality checks have no disarm of their own,
|
|
and this harness supplies theirs.
|
|
* It does NOT prove the declared clause is the ONLY thing the guard hangs on. Some entries redden
|
|
through the proof test's own "the clause has moved, RETARGET this" assertion rather than through
|
|
changed behaviour. That is the intended reading, not a hole: those tests perform their
|
|
behavioural disarm themselves on every green run, and what they could not do is notice their own
|
|
clause reference going stale. Which entries those are is a dated measurement and lives in
|
|
`docs/decisions/records/testing/mutation-claims-are-executed.md`, not here.
|
|
|
|
The `granularity` column is where this file refuses to flatter itself. See `Mutation` in
|
|
`mutation_harness_lib.py`: a `DETECTOR` entry — one whose detector accumulates faults from arms that
|
|
a single mutation trips several of at once — must CARRY the finer mutation that survived, re-run
|
|
every suite and required to keep surviving. EVERY entry is `CLAUSE` today and the survivor set is
|
|
EMPTY, so that machinery is currently unexercised; `test_the_DETECTOR_survivor_set_is_empty_ON_PURPOSE`
|
|
says so out loud rather than leaving it as a lone SKIPPED placeholder nobody reads.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
import importlib.util
|
|
import re
|
|
import shutil
|
|
import sys
|
|
from dataclasses import replace
|
|
from pathlib import Path
|
|
|
|
import pytest
|
|
|
|
from scripts.tests.mutation_harness_lib import (
|
|
_BASELINES,
|
|
Claim,
|
|
Mutation,
|
|
_git,
|
|
build_sandbox,
|
|
reset_sandbox,
|
|
run_pytest,
|
|
verify_claim,
|
|
verify_mutation,
|
|
)
|
|
from scripts.tests.mutation_manifest import CLAIMS, MUTATIONS, UNDECLARED
|
|
from scripts.tests.tracked_files import tracked_file_set
|
|
|
|
REPO_ROOT = Path(__file__).resolve().parents[2]
|
|
INVENTORY = REPO_ROOT / "docs" / "guard-inventory.md"
|
|
|
|
# `| `guard` | blocks | kind | proof | proof ref |` — the five-column inventory row. The column
|
|
# count is what excludes the two-column tables elsewhere in the file; `test_the_inventory_rows_parse`
|
|
# below is the floor that catches the shape changing under it.
|
|
_ROW = re.compile(r"^\|\s*`([^`]+)`\s*\|([^|]*)\|\s*(\w[\w-]*)\s*\|\s*([A-Z-]+)\s*\|\s*(.*?)\s*\|\s*$", re.M)
|
|
|
|
|
|
def _inventory_rows() -> list[tuple[str, str, str, str]]:
|
|
"""(guard, kind, proof grade, proof ref) for every inventory row.
|
|
|
|
Derived from the document the grades live in, never hand-listed: the whole point is that a row
|
|
cannot change its grade without this file noticing.
|
|
"""
|
|
rows = [(m.group(1), m.group(3), m.group(4), m.group(5).strip("`")) for m in _ROW.finditer(INVENTORY.read_text())]
|
|
guards = [g for g, _k, _p, _r in rows]
|
|
duplicates = sorted({g for g in guards if guards.count(g) > 1})
|
|
assert not duplicates, (
|
|
f"the inventory lists {duplicates} more than once. Every comparison below reduces rows "
|
|
"through a set or a dict, so a duplicate row is INVISIBLE to this file — it would report all "
|
|
"entries verified over a table that contradicts itself. `test_guard_inventory.py` catches "
|
|
"this too, but only when the whole suite runs, and this file is routinely run alone."
|
|
)
|
|
assert len(rows) >= 50, (
|
|
f"only parsed {len(rows)} inventory rows — the table's shape has changed and this regex now "
|
|
"reads a fraction of it. Every set comparison below would then pass over a population that "
|
|
"is mostly missing, which is the vacuous-completeness failure the inventory itself exists to "
|
|
"prevent."
|
|
)
|
|
return rows
|
|
|
|
|
|
# ------------------------------------------------------------------------------------------------
|
|
# THE MANIFEST IS PINNED TO THE INVENTORY — a grade cannot change without this file changing
|
|
# ------------------------------------------------------------------------------------------------
|
|
|
|
|
|
def test_the_manifest_covers_exactly_the_MUTATION_rows():
|
|
"""Set equality, both directions, because they are different defects.
|
|
|
|
A `MUTATION` row with no manifest entry is a claim nothing checks — the state #790 was filed
|
|
about. A manifest entry for a row that is no longer graded `MUTATION` is a check whose subject
|
|
has moved out from under it, and it would keep passing.
|
|
"""
|
|
graded = {guard for guard, _kind, grade, _ref in _inventory_rows() if grade == "MUTATION"}
|
|
declared = {m.guard for m in MUTATIONS}
|
|
assert graded, "no row in the inventory is graded MUTATION, so this whole file would prove nothing"
|
|
assert declared - graded == set(), (
|
|
f"declared mutations for rows that are not graded MUTATION: {sorted(declared - graded)}"
|
|
)
|
|
assert graded - declared == set(), (
|
|
f"these rows claim a MUTATION proof with nothing executing it: {sorted(graded - declared)}. "
|
|
"Declare the clause in mutation_manifest.py, or regrade the row."
|
|
)
|
|
assert len(MUTATIONS) == len(declared), "two manifest entries name the same guard"
|
|
|
|
|
|
def test_every_declared_mutation_names_the_row_s_OWN_proof_ref():
|
|
"""The manifest may not point at a different test than the row does.
|
|
|
|
Without this, the inventory could keep citing a stale proof while the harness quietly exercised
|
|
a healthier one, and the row would read as verified.
|
|
"""
|
|
refs = {guard: ref for guard, _kind, grade, ref in _inventory_rows() if grade == "MUTATION"}
|
|
wrong = [(m.guard, m.proof, refs.get(m.guard)) for m in MUTATIONS if refs.get(m.guard) != m.proof]
|
|
assert not wrong, f"manifest proof ref disagrees with the inventory row: {wrong}"
|
|
|
|
|
|
def test_every_GUARD_row_is_either_DECLARED_or_STATED_here():
|
|
"""`Done-when`: guards whose mutation cannot be declared are STATED, not silently skipped.
|
|
|
|
Set equality against the inventory's GUARD rows, both directions, keyed on the guard. Keying on
|
|
the row's GRADE instead would be cheaper and tautological — a new guard graded NONE would inherit
|
|
a reason automatically and nobody would look at it — and a COUNT moves only on net change, so one
|
|
guard arriving as another is promoted leaves it unchanged. This is the same hand-maintained,
|
|
machine-checked shape as `docs/guard-inventory.md` itself, which is what makes it safe.
|
|
|
|
The partition covers `Kind == GUARD` rows only. `TOOLING` asserts nothing and `PROOF` files exist
|
|
to prove other guards, so neither carries a mutation claim to verify — a rule about the Kind
|
|
column rather than a list anyone maintains.
|
|
"""
|
|
guards = {guard for guard, kind, _grade, _ref in _inventory_rows() if kind == "GUARD"}
|
|
declared = {m.guard for m in MUTATIONS}
|
|
stated = set(UNDECLARED)
|
|
|
|
assert not (declared & stated), (
|
|
f"these guards are both declared and stated as undeclared: {sorted(declared & stated)}"
|
|
)
|
|
unaccounted = sorted(guards - declared - stated)
|
|
assert not unaccounted, (
|
|
f"these guards are neither declared nor stated: {unaccounted}. Declare the clause in "
|
|
"mutation_manifest.py, or write a line in UNDECLARED saying what a proof would need — "
|
|
"silence is the one option that is not available."
|
|
)
|
|
orphaned = sorted(stated - guards)
|
|
assert not orphaned, (
|
|
f"UNDECLARED names rows that are not GUARD-kind rows any more: {orphaned}. A reason for a "
|
|
"guard that no longer exists reads as coverage."
|
|
)
|
|
thin = [g for g, reason in UNDECLARED.items() if len(reason.strip()) < 60]
|
|
assert not thin, f"these UNDECLARED entries say nothing a reader could act on: {thin}"
|
|
|
|
|
|
def test_every_entry_declares_a_known_granularity_and_DETECTOR_entries_CARRY_their_survivor():
|
|
"""`DETECTOR` is an admission, and an unevidenced one would be a grading curve.
|
|
|
|
#790's complaint about `pin_population_faults` — that neutering a whole helper is "coarse enough
|
|
that a single surviving clause would not be noticed" — applies to every entry graded here. So an
|
|
entry may only claim `DETECTOR` while carrying the finer mutation that was tried, as data rather
|
|
than as a sentence: `test_every_SURVIVING_clause_mutation_still_does` then runs it.
|
|
"""
|
|
bad = [m.guard for m in MUTATIONS if m.granularity not in (Mutation.CLAUSE, Mutation.DETECTOR)]
|
|
assert not bad, f"unknown granularity on {bad}; allowed: CLAUSE, DETECTOR"
|
|
assert all(m.why.strip() for m in MUTATIONS), "every declared mutation must say what its clause does"
|
|
|
|
unevidenced = [m.guard for m in MUTATIONS if m.granularity == Mutation.DETECTOR and not m.survived_clause]
|
|
assert not unevidenced, (
|
|
f"these entries claim DETECTOR granularity while naming no finer mutation that was tried: "
|
|
f"{unevidenced}. Carry the survivor, or declare the finer clause instead."
|
|
)
|
|
misplaced = [m.guard for m in MUTATIONS if m.granularity == Mutation.CLAUSE and m.survived_clause]
|
|
assert not misplaced, (
|
|
f"these entries are graded CLAUSE but carry a surviving finer mutation: {misplaced}. If a "
|
|
"finer clause exists and survives, the grade is DETECTOR."
|
|
)
|
|
half = [m.guard for m in MUTATIONS if bool(m.survived_clause) != bool(m.survived_replacement)]
|
|
assert not half, f"a survivor needs both a clause and a replacement: {half}"
|
|
|
|
|
|
def test_every_entry_declares_a_SPECIFIC_diagnostic_it_must_redden_with():
|
|
"""`expect` is what stops exit code 1 from being the whole verdict, so it cannot be a token.
|
|
|
|
An empty or near-empty expectation matches any output and hands the verdict straight back to the
|
|
exit status — the state this field exists to leave. It must also be a substring of no other
|
|
entry's, or two rows could be satisfied by one another's diagnostic.
|
|
"""
|
|
vague = [(m.guard, m.expect) for m in MUTATIONS if len(m.expect.strip()) < 20]
|
|
assert not vague, f"these expectations are too weak to distinguish one red from another: {vague}"
|
|
for m in MUTATIONS:
|
|
clashes = [o.guard for o in MUTATIONS if o is not m and m.expect in o.expect]
|
|
assert not clashes, f"{m.guard}'s expectation is contained in {clashes}'s — neither is specific"
|
|
|
|
|
|
# ------------------------------------------------------------------------------------------------
|
|
# THE PROSE CLAIMS — the same rule over a population that is not the inventory (ersatztv#881)
|
|
# ------------------------------------------------------------------------------------------------
|
|
|
|
|
|
def test_the_CLAIM_population_is_NOT_EMPTY():
|
|
"""ANTI-VACUITY for everything below, which is parametrized over `CLAIMS`.
|
|
|
|
`@parametrize` over an empty tuple collects one placeholder reported as SKIPPED, not a failure,
|
|
so an emptied `CLAIMS` would leave the whole prose half of this file passing over nothing while
|
|
reading exactly like coverage. That is the same reason
|
|
`test_the_DETECTOR_survivor_set_is_empty_ON_PURPOSE` exists — with the opposite expectation,
|
|
because an empty survivor set is a recorded decision and an empty claim set is a mechanism that
|
|
has quietly stopped being used.
|
|
"""
|
|
assert CLAIMS, (
|
|
"CLAIMS is empty, so every check below passes over nothing. An opt-in binding nobody uses is "
|
|
"indistinguishable from no binding at all — declare the claims, or retire the mechanism "
|
|
"deliberately and say so in testing.mutation-claims-are-executed."
|
|
)
|
|
|
|
|
|
def test_every_CLAIM_is_BOUND_to_the_PROSE_it_justifies():
|
|
"""The binding, both halves, because a claim entry unbound from its sentence proves nothing.
|
|
|
|
A claim is an assertion ABOUT a sentence in another file. If the sentence is reworded, moved or
|
|
deleted, the entry keeps executing a mutation nobody is claiming anything about and reports it as
|
|
verified — which is precisely the decay `MUTATION` rows were suffering before #790, one level up.
|
|
|
|
MEMBERSHIP is answered by the git INDEX, never by the disk
|
|
(`testing.guard-derives-population-from-source`): a claim pointing at an untracked scratch file
|
|
would otherwise pass here on the author's machine and be absent in the sandbox and in CI.
|
|
EXISTENCE on disk is a separate assertion below, because a tracked path with no file is a tree
|
|
mid-edit and should be reported, not read as an absent site.
|
|
"""
|
|
tracked = tracked_file_set()
|
|
untracked = sorted({c.site for c in CLAIMS if c.site not in tracked})
|
|
assert not untracked, (
|
|
f"these claim sites are not tracked by git: {untracked}. The prose has to live in the "
|
|
"repository for the binding to mean anything."
|
|
)
|
|
for claim in CLAIMS:
|
|
# Existence ASSERTED, not filtered, per `tracked_files.py`'s own contract: a path in the
|
|
# index with no file on disk means the tree is mid-edit, and a bare `FileNotFoundError`
|
|
# from the read below would name the path without saying why this file cares.
|
|
site = REPO_ROOT / claim.site
|
|
assert site.is_file(), (
|
|
f"git tracks {claim.site} but there is no file there, so the sentence this entry is "
|
|
"bound to cannot be read. The tree is mid-edit; this is reported rather than skipped."
|
|
)
|
|
text = site.read_text(encoding="utf-8")
|
|
occurrences = text.count(claim.quote)
|
|
assert occurrences == 1, (
|
|
f"{claim.site}: the declared quote occurs {occurrences} times, not once — "
|
|
f"{claim.quote!r}. RETARGET the entry rather than loosening the match. If the sentence "
|
|
"was deleted, delete this entry; if it was reworded, re-read it and re-declare, because "
|
|
"a reworded claim is a NEW claim and this harness has never executed it."
|
|
)
|
|
assert claim.quote.strip() == claim.quote and len(claim.quote) >= 20, (
|
|
f"{claim.site}: the quote is too short or padded to identify a sentence: {claim.quote!r}"
|
|
)
|
|
|
|
|
|
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
|
|
status alone would let a crash certify it. A GREEN claim has no failing run to read 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:
|
|
assert len(claim.expect.strip()) >= 20, (
|
|
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"
|
|
|
|
|
|
# ------------------------------------------------------------------------------------------------
|
|
# THE EXECUTION — one isolated repository, reused, reset between mutations
|
|
# ------------------------------------------------------------------------------------------------
|
|
|
|
|
|
@pytest.fixture(scope="session")
|
|
def sandbox(tmp_path_factory):
|
|
"""An isolated copy of this repository, with the POSITIVE CONTROL already run in it.
|
|
|
|
The control is inside the fixture rather than in a test of its own so ordering is a dependency
|
|
rather than a convention: no mutation can be judged before every proof test has been shown green
|
|
on the unmutated tree. Without it, "the named test went red" is satisfied just as well by a proof
|
|
test that was already broken, and reporting that as a verified mutation is the failure mode this
|
|
whole file exists to remove.
|
|
"""
|
|
sb = build_sandbox(tmp_path_factory.mktemp("mutation-sandbox"))
|
|
# The sandbox holds what GIT TRACKS, so a proof test in a file that has never been `git add`ed is
|
|
# simply absent there and the run below reports "file or directory not found" — accurate, and
|
|
# unreadable as a diagnosis. Named here instead, because this is what a developer adding a guard
|
|
# hits first.
|
|
node_ids = [m.node_id for m in MUTATIONS] + [c.node_id for c in CLAIMS]
|
|
missing = sorted({n.split("::")[0] for n in node_ids if not (sb / n.split("::")[0]).is_file()})
|
|
assert not missing, (
|
|
f"these proof files are not in the sandbox: {missing}. The sandbox is derived from "
|
|
"`git ls-files`, so an unstaged new file is not in it — `git add` it and re-run."
|
|
)
|
|
# The claim proofs join the control for the reason the row proofs do, and it holds in BOTH
|
|
# 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. 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 "
|
|
"repository, so nothing below can distinguish 'the mutation was noticed' from 'the test was "
|
|
f"already red'. Fix them first.\n{result.stdout[-4000:]}{result.stderr[-2000:]}"
|
|
)
|
|
assert "passed" in result.stdout, f"the control run collected nothing: {result.stdout!r}"
|
|
try:
|
|
yield sb
|
|
finally:
|
|
# ~115 MiB of tracked files plus its own git objects. pytest keeps the last three sessions'
|
|
# tmp dirs by default, so leaving it costs a third of a gigabyte on a developer machine that
|
|
# runs this a few times.
|
|
shutil.rmtree(sb, ignore_errors=True)
|
|
|
|
|
|
def test_the_reset_restores_the_BASELINE_even_after_a_proof_COMMITS(sandbox):
|
|
"""One sandbox serves every mutation, so the reset has to be a reset to a fixed point.
|
|
|
|
`git reset --hard` with no argument resets to whatever HEAD currently is. A proof test that
|
|
commits inside the sandbox — several drive `git commit` for real — moves HEAD onto a commit
|
|
carrying whatever was in the tree at the time, and every later reset would faithfully restore
|
|
THAT. The contamination surfaces as an unrelated red several mutations further on, which is the
|
|
hardest kind of harness defect to attribute.
|
|
"""
|
|
subject = sandbox / "docs" / "guard-inventory.md"
|
|
baseline = subject.read_text()
|
|
|
|
subject.write_text(baseline + "\n<!-- planted, then COMMITTED -->\n")
|
|
_git(sandbox, "add", "-A")
|
|
_git(sandbox, "commit", "-qm", "a proof test committing inside the sandbox")
|
|
assert subject.read_text() != baseline, "the planted change did not land, so this proves nothing"
|
|
|
|
reset_sandbox(sandbox)
|
|
|
|
assert subject.read_text() == baseline, (
|
|
"the reset restored the sandbox to a commit made DURING a mutation rather than to the "
|
|
"pristine baseline, so every later verdict is computed against a contaminated tree"
|
|
)
|
|
# Through `_git`, not a raw `subprocess.run`: an ambient `GIT_DIR` — which a git hook exports,
|
|
# and this suite runs from one — would resolve this against the REAL repository and compare two
|
|
# commits that have nothing to do with the sandbox. Asserting isolation with an unisolated call
|
|
# is the defect this harness exists to catch, one level up.
|
|
head = _git(sandbox, "rev-parse", "HEAD").stdout.decode().strip()
|
|
assert head == _BASELINES[str(sandbox.resolve())], f"HEAD was left off the recorded baseline commit: {head}"
|
|
|
|
|
|
@pytest.mark.parametrize("mutation", MUTATIONS, ids=lambda m: m.guard)
|
|
def test_MUTATION_the_declared_clause_reddens_the_named_proof(sandbox, mutation):
|
|
reset_sandbox(sandbox)
|
|
verdict = verify_mutation(sandbox, mutation)
|
|
assert verdict.ok, f"{mutation.guard}: {verdict.reason}"
|
|
|
|
|
|
@pytest.mark.parametrize("claim", CLAIMS, ids=lambda c: f"{c.site}:{c.outcome}")
|
|
def test_CLAIM_the_declared_mutation_produces_the_DECLARED_OUTCOME(sandbox, claim):
|
|
"""The prose, executed. A red here is not necessarily a defect in the code — for a GREEN claim it
|
|
usually means the mutation is noticed NOW, which is good news about the code and a sentence that
|
|
has to be rewritten. Either way the claim has stopped being true, which is the whole point."""
|
|
reset_sandbox(sandbox)
|
|
verdict = verify_claim(sandbox, claim)
|
|
assert verdict.ok, f"{claim.site} — {claim.quote!r}: {verdict.reason}"
|
|
|
|
|
|
_SURVIVORS = tuple(m for m in MUTATIONS if m.granularity == Mutation.DETECTOR)
|
|
|
|
|
|
def test_the_DETECTOR_survivor_set_is_empty_ON_PURPOSE():
|
|
"""ANTI-VACUITY for the parametrized proof below, which currently runs over NOTHING.
|
|
|
|
`@parametrize` over an empty tuple does not fail and does not collect a real case: with pytest's
|
|
default `empty_parameter_set_mark=skip` (and this repo sets no ini), it collects ONE placeholder
|
|
reported as `SKIPPED … got empty parameter set`. Measured. In a 1500-test run that is one `s`
|
|
among the dots — not a false green, but indistinguishable from coverage unless someone reads the
|
|
skip list, which is the same reason `test_the_husky_launched_population_is_not_empty` exists in
|
|
`test_hook_fire_log.py`.
|
|
|
|
`_SURVIVORS` went empty when ersatztv#891 regraded the last `DETECTOR` row to `CLAUSE`. TWO
|
|
things are consequently unexercised, enumerated rather than counted:
|
|
|
|
1. the survivor runner below, `test_every_SURVIVING_clause_mutation_still_does`; and
|
|
2. the `unevidenced` arm of
|
|
`test_every_entry_declares_a_known_granularity_and_DETECTOR_entries_CARRY_their_survivor`,
|
|
which filters on `granularity == DETECTOR`.
|
|
|
|
Both self-arm the moment an entry is graded `DETECTOR`. `verify_mutation`'s "still PASSED"
|
|
verdict path is NOT in this list: it is not DETECTOR-gated and fires for any declared mutation
|
|
that fails to redden, and
|
|
`test_an_INERT_mutation_is_REPORTED_rather_than_passed` drives it every run — measured by
|
|
retargeting its diagnostic string and watching that test go red.
|
|
|
|
This test states the expected size, so the day someone adds a `DETECTOR` entry it goes red and
|
|
names the lines to update; the empty set becomes a decision rather than a skip nobody reads.
|
|
"""
|
|
assert len(_SURVIVORS) == 0, (
|
|
f"a DETECTOR entry exists again ({[m.guard for m in _SURVIVORS]}), so the survivor runner "
|
|
"below is no longer unexercised. Update this expectation — and note that the machinery it "
|
|
"drives has had no coverage since ersatztv#891, so exercise it deliberately rather than "
|
|
"assuming it still works."
|
|
)
|
|
|
|
|
|
@pytest.mark.parametrize("mutation", _SURVIVORS, ids=lambda m: m.guard)
|
|
def test_every_SURVIVING_clause_mutation_still_does(sandbox, mutation):
|
|
"""The DETECTOR grade, executed rather than recited.
|
|
|
|
A finer mutation that has since STARTED reddening the proof test means the guard now admits
|
|
clause-level proof and the entry should be regraded — the coarse grade would otherwise persist as
|
|
an excuse long after the reason for it went away. Failing here is therefore good news; it just
|
|
has to be acted on.
|
|
"""
|
|
reset_sandbox(sandbox)
|
|
finer = replace(
|
|
mutation,
|
|
clause=mutation.survived_clause,
|
|
replacement=mutation.survived_replacement,
|
|
survived_clause="",
|
|
survived_replacement="",
|
|
)
|
|
verdict = verify_mutation(sandbox, finer)
|
|
assert not verdict.ok, (
|
|
f"{mutation.guard} is graded DETECTOR because {mutation.survived_clause!r} was tried and left "
|
|
"the proof test green — but it reddens it now. Regrade the entry to CLAUSE with that mutation."
|
|
)
|
|
assert "still PASSED" in verdict.reason, (
|
|
f"the survivor did not survive for the recorded reason — it failed with: {verdict.reason}"
|
|
)
|
|
|
|
|
|
# ------------------------------------------------------------------------------------------------
|
|
# THIS GUARD'S OWN MUTATION PROOF — the redness clause, disarmed, on a sandbox of two files
|
|
# ------------------------------------------------------------------------------------------------
|
|
|
|
EXIT_STATUS_CLAUSE = " if result.returncode != 1:"
|
|
DIAGNOSTIC_CLAUSE = " if mutation.expect not in diagnostic:"
|
|
# 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.
|
|
IDENTICAL_REPLACEMENT_CLAUSE = " if mutated == original:"
|
|
LIB = REPO_ROOT / "scripts" / "tests" / "mutation_harness_lib.py"
|
|
|
|
|
|
def _inert_sandbox(tmp_path: Path, body: str = " assert True\n") -> tuple[Path, Mutation]:
|
|
"""A minimal synthetic sandbox holding one test file, whose outcome is fixed by `body`.
|
|
|
|
Deliberately not a copy of the repo: the subject here is `verify_mutation`'s verdict, and a real
|
|
sandbox would cost four seconds to prove something about two lines of control flow.
|
|
"""
|
|
tests = tmp_path / "scripts" / "tests"
|
|
tests.mkdir(parents=True)
|
|
(tests / "test_inert.py").write_text(f"# INERT MARKER\n\n\ndef test_ok():\n{body}")
|
|
return tmp_path, Mutation(
|
|
guard="inert",
|
|
target="scripts/tests/test_inert.py",
|
|
clause="# INERT MARKER",
|
|
replacement="# INERT MARKER, CHANGED",
|
|
proof="test_inert.py::test_ok",
|
|
granularity=Mutation.CLAUSE,
|
|
# A legal expectation, not the empty string: an empty one is a shape the manifest forbids,
|
|
# so a fixture relying on it would be proving something about a configuration that cannot
|
|
# ship. Each caller that needs a different one passes it through `replace`.
|
|
expect="a diagnostic no run of this fixture produces",
|
|
why="an inert mutation: the named test cannot notice it",
|
|
)
|
|
|
|
|
|
def _lib_with(tmp_path: Path, clause: str, replacement: str, label: str):
|
|
"""Import a copy of the library with one clause replaced.
|
|
|
|
The copy is registered in `sys.modules` before execution: `@dataclass` resolves a string
|
|
annotation through `sys.modules[cls.__module__]`, so an unregistered module raises AttributeError
|
|
on the first dataclass it defines rather than on anything to do with the clause.
|
|
"""
|
|
source = LIB.read_text()
|
|
assert source.count(clause) == 1, (
|
|
f"the {label} has moved or been reworded; RETARGET this mutation rather than loosening the "
|
|
"match — and update the mutation_manifest entry for this file, which names the same string"
|
|
)
|
|
path = tmp_path / f"mutant_{label.replace(' ', '_')}.py"
|
|
path.write_text(source.replace(clause, replacement, 1))
|
|
|
|
spec = importlib.util.spec_from_file_location(path.stem, path)
|
|
mutant = importlib.util.module_from_spec(spec)
|
|
sys.modules[spec.name] = mutant
|
|
try:
|
|
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
|
|
|
|
|
|
def test_an_INERT_mutation_is_REPORTED_rather_than_passed(tmp_path):
|
|
"""The behavioural half. A harness that cannot tell a real disarm from a comment edit would
|
|
report every row verified on any tree at all."""
|
|
sb, inert = _inert_sandbox(tmp_path)
|
|
verdict = verify_mutation(sb, inert)
|
|
assert not verdict.ok, "a mutation the named test cannot possibly notice was reported as verified"
|
|
assert "still PASSED" in verdict.reason, verdict.reason
|
|
|
|
|
|
def test_a_red_for_the_WRONG_REASON_is_not_accepted(tmp_path):
|
|
"""The gate `expect` exists for. Pytest reports an ordinary exception exactly as it reports a
|
|
failed assertion, so a mutation that CRASHES the proof test looks identical to one it detected.
|
|
A verdict that cannot tell those apart certifies rows on evidence about nothing."""
|
|
sb, inert = _inert_sandbox(tmp_path, " raise RuntimeError('an unrelated crash')\n")
|
|
crashing = replace(inert, expect="the diagnostic this row is supposed to produce")
|
|
verdict = verify_mutation(sb, crashing)
|
|
assert not verdict.ok, "a red with nothing to do with the declared diagnostic was accepted"
|
|
assert "NOT with the declared diagnostic" in verdict.reason, verdict.reason
|
|
|
|
|
|
def test_MUTATION_disarming_the_DIAGNOSTIC_gate_accepts_a_red_for_the_wrong_reason(tmp_path):
|
|
"""The clause-level proof, on the newer of the two gates every verdict passes through.
|
|
|
|
Disarm the check that the failure carries the declared diagnostic, and the crashing case above
|
|
must start reporting as verified. If it does not, that rejection is coming from somewhere other
|
|
than the clause, and the test above proves nothing about it.
|
|
"""
|
|
sb, inert = _inert_sandbox(tmp_path, " raise RuntimeError('an unrelated crash')\n")
|
|
crashing = replace(inert, expect="the diagnostic this row is supposed to produce")
|
|
assert not verify_mutation(sb, crashing).ok, (
|
|
"the UNMUTATED verdict already accepted it, so the mutant proves nothing"
|
|
)
|
|
|
|
mutant = _lib_with(tmp_path, DIAGNOSTIC_CLAUSE, " if False:", "diagnostic gate")
|
|
assert mutant.verify_mutation(sb, crashing).ok, (
|
|
"the diagnostic gate was replaced with a constant and a red for an unrelated reason was "
|
|
"STILL rejected, so the verdict does not hang on the clause that reads it"
|
|
)
|
|
|
|
|
|
def test_MUTATION_disarming_the_EXIT_STATUS_gate_accepts_a_run_that_NEVER_RAN_A_TEST(tmp_path):
|
|
"""The same proof for the older gate, and it has to be built carefully to isolate it.
|
|
|
|
A GREEN run cannot serve: it produces no exception output, so only an EMPTY expectation would
|
|
reach the status gate — and an empty expectation is a shape the manifest forbids, which would
|
|
make this a proof about a configuration that cannot ship. Instead the sandbox's test file fails
|
|
at IMPORT: pytest exits non-1 (nothing was collected, so nothing ran) while still printing the
|
|
exception, so a legal non-empty expectation matches and the exit status is the ONLY thing
|
|
rejecting it. That is the case this gate exists for — a proof ref that no longer names a
|
|
collectable test must not read as a guard going red.
|
|
"""
|
|
boom = "a deliberate import-time failure, which is not a test result"
|
|
sb, inert = _inert_sandbox(tmp_path)
|
|
(sb / "scripts" / "tests" / "test_inert.py").write_text(f"# INERT MARKER\nraise RuntimeError({boom!r})\n")
|
|
uncollectable = replace(inert, expect=boom)
|
|
|
|
verdict = verify_mutation(sb, uncollectable)
|
|
assert not verdict.ok, "a run in which no test executed was accepted as a guard going red"
|
|
assert len(uncollectable.expect) >= 20, "the expectation must be one the manifest would accept"
|
|
|
|
mutant = _lib_with(tmp_path, EXIT_STATUS_CLAUSE, " if False:", "exit status gate")
|
|
assert mutant.verify_mutation(sb, uncollectable).ok, (
|
|
"the exit-status gate was replaced with a constant and a run that never executed a test was "
|
|
"still rejected, so the verdict does not hang on the status it reads"
|
|
)
|
|
|
|
|
|
def test_MUTATION_disarming_the_IDENTICAL_REPLACEMENT_gate_CERTIFIES_A_ROW_THAT_MUTATED_NOTHING(tmp_path):
|
|
"""The pre-flight refusal, isolated the same way, and it is the one no later gate can stand in for.
|
|
|
|
A replacement equal to its clause leaves the file byte-identical, so the proof ref runs against an
|
|
UNMUTATED tree. Over a proof that is already red for its own reasons, that is indistinguishable
|
|
from a detection — exit 1, carrying the declared diagnostic — so the exit-status and diagnostic
|
|
gates both accept and this one is what refuses. Which is why the fixture fails on its own: a green
|
|
fixture would be rejected by the status gate instead and the two would mask each other (#685).
|
|
"""
|
|
boom = "a failure this fixture produces with no mutation applied at all"
|
|
sb, inert = _inert_sandbox(tmp_path, f" raise RuntimeError({boom!r})\n")
|
|
no_op = replace(inert, replacement=inert.clause, expect=boom)
|
|
|
|
verdict = verify_mutation(sb, no_op)
|
|
assert not verdict.ok, "a replacement identical to its clause was accepted as a mutation"
|
|
assert "nothing was mutated" in verdict.reason, verdict.reason
|
|
|
|
mutant = _lib_with(tmp_path, IDENTICAL_REPLACEMENT_CLAUSE, " if False:", "identical replacement gate")
|
|
assert mutant.verify_mutation(sb, no_op).ok, (
|
|
"the identical-replacement gate was replaced with a constant and a row that mutated NOTHING "
|
|
"was still rejected, so the verdict does not hang on the clause that compares the two texts"
|
|
)
|
|
|
|
|
|
def test_a_clause_that_no_longer_OCCURS_ONCE_is_reported_rather_than_applied(tmp_path):
|
|
"""The failure paths, driven directly, because this is where a harness quietly stops harnessing.
|
|
|
|
A clause that has been reworded away, or that now matches a second site, must produce a verdict
|
|
naming the problem. Silently replacing nothing — or replacing the wrong site — would leave every
|
|
row in this file reporting verified while mutating something nobody declared.
|
|
"""
|
|
sb, inert = _inert_sandbox(tmp_path)
|
|
|
|
gone = replace(inert, clause="# A CLAUSE THAT IS NOT THERE")
|
|
assert not verify_mutation(sb, gone).ok
|
|
assert "occurs 0 times" in verify_mutation(sb, gone).reason
|
|
|
|
(sb / "scripts" / "tests" / "test_inert.py").write_text(
|
|
"# INERT MARKER\n# INERT MARKER\n\n\ndef test_ok():\n assert True\n"
|
|
)
|
|
assert "occurs 2 times" in verify_mutation(sb, inert).reason
|
|
|
|
absent = replace(inert, target="scripts/tests/no_such_file.py")
|
|
assert "does not exist in the sandbox" in verify_mutation(sb, absent).reason
|
|
|
|
|
|
def test_the_sandbox_is_left_UNCHANGED_by_a_verdict(tmp_path):
|
|
"""One sandbox serves every mutation, so a verdict that leaves its edit behind would make each
|
|
result a function of the ones before it."""
|
|
sb, inert = _inert_sandbox(tmp_path)
|
|
subject = sb / "scripts" / "tests" / "test_inert.py"
|
|
before = subject.read_text()
|
|
verify_mutation(sb, inert)
|
|
assert subject.read_text() == before, "verify_mutation left its mutation in the sandbox"
|
|
|
|
|
|
# ------------------------------------------------------------------------------------------------
|
|
# 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, 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, 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.
|
|
"""
|
|
sb = tmp_path / "sb"
|
|
tests = sb / "scripts" / "tests"
|
|
tests.mkdir(parents=True)
|
|
(tests / "test_inert.py").write_text(f"# INERT MARKER\n{body}")
|
|
_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",
|
|
clause="# INERT MARKER",
|
|
replacement="# INERT MARKER, CHANGED",
|
|
proof="test_inert.py",
|
|
outcome=Claim.GREEN,
|
|
expect="",
|
|
why="an inert mutation over a file whose outcome the fixture fixes",
|
|
reach_replacement=reach_replacement,
|
|
reach_expect=_REACH_DIAGNOSTIC,
|
|
)
|
|
|
|
|
|
def test_an_UNKNOWN_outcome_is_REFUSED_rather_than_read_as_either(tmp_path):
|
|
"""`verify_claim` branches on the outcome, so a value it does not recognise must not fall through
|
|
to a verdict. A typo'd direction reading as verified is the shape this whole file exists to
|
|
remove, one level up from the claims themselves."""
|
|
sb, claim = _inert_claim_sandbox(tmp_path, "\n\ndef test_ok():\n assert True\n")
|
|
verdict = verify_claim(sb, replace(claim, outcome="green"))
|
|
assert not verdict.ok, "an unrecognised outcome was accepted"
|
|
assert "unknown outcome" in verdict.reason, verdict.reason
|
|
|
|
|
|
def test_MUTATION_disarming_the_GREEN_EXIT_STATUS_gate_accepts_a_proof_that_WENT_RED(tmp_path):
|
|
"""Disarm the status gate alone and a GREEN claim whose proof FAILED must start reporting verified.
|
|
|
|
The fixture's file both fails and passes a test, deliberately: a file that only failed would also
|
|
be rejected by the vacuity gate below, and the two would mask each other — a mutant that reddens
|
|
because a SECOND clause is doing the work proves nothing about the one under test (#685).
|
|
"""
|
|
body = "\n\ndef test_ok():\n assert True\n\n\ndef test_red():\n assert False\n"
|
|
sb, claim = _inert_claim_sandbox(tmp_path, body)
|
|
|
|
verdict = verify_claim(sb, claim)
|
|
assert not verdict.ok, "a proof that went RED was accepted as a verified GREEN claim"
|
|
assert "exited 1" in verdict.reason, verdict.reason
|
|
|
|
mutant = _lib_with(tmp_path, GREEN_STATUS_CLAUSE, " if False:", "green status gate")
|
|
assert mutant.verify_claim(sb, claim).ok, (
|
|
"the green-direction status gate was replaced with a constant and a proof that FAILED was "
|
|
"still rejected, so the verdict does not hang on the status it reads"
|
|
)
|
|
|
|
|
|
def test_MUTATION_disarming_the_GREEN_VACUITY_gate_accepts_a_run_in_which_NOTHING_PASSED(tmp_path):
|
|
"""The second gate, isolated the same way. Pytest exits 0 when every test SKIPS, so exit status
|
|
alone certifies a green in which nothing was given the chance to notice the mutation — which is
|
|
exactly the vacuous-completeness failure the inventory itself exists to prevent."""
|
|
body = (
|
|
"\n\nimport pytest\n\n\n@pytest.mark.skip(reason='nothing runs here')\ndef test_skipped():\n assert True\n"
|
|
)
|
|
sb, claim = _inert_claim_sandbox(tmp_path, body)
|
|
|
|
verdict = verify_claim(sb, claim)
|
|
assert not verdict.ok, "a run in which every test skipped was accepted as a verified GREEN claim"
|
|
assert "NOTHING PASSED" in verdict.reason, verdict.reason
|
|
|
|
mutant = _lib_with(tmp_path, GREEN_VACUITY_CLAUSE, " if False:", "green vacuity gate")
|
|
assert mutant.verify_claim(sb, claim).ok, (
|
|
"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"
|
|
)
|