The `Claim` docstring motivated the GREEN direction by enumerating three corpus
sites and restating what each asserts. The middle restatement said
`scripts/check-doc-narrative.py` "says removing its `/dev/null` arm reddens no
test" — the universal a9341d841 removed from that file when it narrowed the
comment to the scope the harness actually executes
("`test_check_doc_narrative.py` stays green with this arm removed"). The
docstring was written before that narrowing and kept re-asserting the wider
claim, attributed to a file that no longer makes it: `git grep -F "reddens no
test"` returned exactly one hit, the line asserting it. That is #881's own
defect #2 reproduced inside the fix.
Restating an outcome is what makes it drift, so the enumeration now names the
three sites and the mutation each describes, states the shape they share, and
says why the outcome wording is not repeated. The only two copies of that
outcome left in the tree are the site comment and the `CLAIMS` quote bound to
it, which is the binding by construction. Both other members were re-checked
today and hold: `.gitea/workflows/review-verdict.yml:2411` and
`scripts/tests/hook_fire_isolation.py:82`.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015QqCpYFsKgnAnx6jVwrKiV
512 lines
26 KiB
Python
512 lines
26 KiB
Python
"""Machinery for the clause-level mutation harness (ersatztv#790).
|
|
|
|
`docs/guard-inventory.md` grades each guard's proof `MUTATION`, `BEHAVIOUR-ONLY` or `NONE`, and
|
|
`MUTATION` means "a clause-level mutation was executed and this named test was witnessed red". A
|
|
witnessing performed once, by hand, decays the moment anyone edits the guard, and a grade nothing
|
|
re-checks can simply be wrong.
|
|
|
|
This module turns each such row from an assertion into a check: apply the guard's **declared**
|
|
clause mutation to an isolated copy of the repo and require the row's own named test to go RED.
|
|
|
|
WHAT IS DELIBERATELY NOT DONE. The mutation is declared per guard in `mutation_manifest.py`, never
|
|
inferred. A harness that guessed which clause of a 90-line hook is *the* guard would manufacture
|
|
exactly the confident-but-empty coverage this exists to prevent — the reason
|
|
`testing.guard-ships-with-mutation-proof` rejects a generic runner. Guessing is also unnecessary:
|
|
most of the proof tests already name their clause in source (the BOM test's `= "efbbbf" ]; then`,
|
|
`UNSET_CLAUSE`, `prove-fix.sh`'s `if [ "$RC" -eq 0 ]; then`), and the manifest reuses that same
|
|
string rather than inventing a second one.
|
|
|
|
THE SANDBOX IS A REAL GIT REPOSITORY, not a directory of copied files. Several guards derive their
|
|
population from `git ls-files` and one drives `git worktree add`, so a plain copy would send them
|
|
down their degraded paths and every mutation would "redden" for a reason having nothing to do with
|
|
the clause. Its contents are the TRACKED files with WORKING-TREE content — `git ls-files -s`, not a
|
|
filesystem walk (`testing.guard-derives-population-from-source`, and the reason #778's guard was red
|
|
on every developer checkout and green in CI: `.husky/_/` is generated by `npm ci` and untracked).
|
|
|
|
Two index entries are not regular files and are handled explicitly rather than by an exception:
|
|
the `.claude/skills/jellyfin` symlink is recreated as a symlink (it dangles outside `~/ersatztv`,
|
|
which is inherent to the cross-repo symlink pattern and not this harness's problem), and the
|
|
`ErsatzTV-macOS` gitlink is SKIPPED — no guard reads the submodule, and materialising one would
|
|
cost a fetch per run.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
import os
|
|
import shutil
|
|
import subprocess
|
|
import sys
|
|
from dataclasses import dataclass
|
|
from pathlib import Path
|
|
|
|
REPO_ROOT = Path(__file__).resolve().parents[2]
|
|
|
|
# Long enough that a slow shared runner is not mistaken for a hang, short enough that a genuinely
|
|
# stuck inner pytest fails the job rather than burning the whole CI budget. The full set of proof
|
|
# tests runs in ~7s locally.
|
|
PYTEST_TIMEOUT = 300
|
|
|
|
# Every git call here is local and confined to the sandbox; anything slower is stuck, not slow.
|
|
GIT_TIMEOUT = 120
|
|
|
|
# The pristine commit of each sandbox, held OUT OF THE REPOSITORY the proof tests drive. A ref inside
|
|
# it would be one more thing a proof can move: `git branch -f` fails on a checked-out branch, a
|
|
# global `init.defaultBranch` can collide with the name, and any `git update-ref`/`git checkout -B` a
|
|
# proof runs could retarget it. An object id kept here cannot be reached from inside the sandbox at
|
|
# all, and `git reset --hard <oid>` needs no ref to exist.
|
|
_BASELINES: dict[str, str] = {}
|
|
|
|
|
|
@dataclass(frozen=True)
|
|
class Mutation:
|
|
"""One declared clause mutation and the test that must notice it.
|
|
|
|
`guard` is the `Guard` column of `docs/guard-inventory.md` — the thing being graded.
|
|
`target` is the file actually edited. They are usually the same; where they differ, `why` says
|
|
why, and `test_a_cross_file_mutation_states_why` requires it.
|
|
`clause` must occur EXACTLY ONCE in `target`: a mutation that lands on an unintended second site
|
|
proves something about a clause nobody declared.
|
|
`expect` is a substring the FAILING run's output must contain, and it is what stops exit code 1
|
|
from being the whole verdict. Pytest reports an ordinary exception the same way it reports a
|
|
failed assertion, so a mutation that merely CRASHES the proof test — an emptied population
|
|
reaching an `IndexError`, a syntax error, an unrelated parametrisation — would otherwise be
|
|
accepted as "the guard noticed". Naming the diagnostic the mutation is supposed to produce makes
|
|
each row's evidence specific: a red for a different reason fails here and has to be re-declared.
|
|
|
|
`granularity` is `CLAUSE` or `DETECTOR`, and it is the honest half of this harness. #790 opened
|
|
on the observation that neutering `pin_population_faults` wholesale is "coarser than disarming
|
|
one clause at a time — coarse enough that a single surviving clause would not be noticed". That
|
|
is true, and it is also not always avoidable: a detector that accumulates faults from several
|
|
independent arms answers on ANY of them, so disarming one arm leaves its proof test green and
|
|
the only mutation that reddens is the whole detector. Recording which grade each guard actually
|
|
admits turns that from an unstated weakness into a measured property.
|
|
|
|
A `DETECTOR` entry does not merely SAY a finer mutation was tried; it carries that mutation in
|
|
`survived_clause`/`survived_replacement`, and `test_every_SURVIVING_clause_mutation_still_does`
|
|
re-runs it and requires the proof test to stay GREEN. WHERE SUCH AN ENTRY EXISTS, the
|
|
justification for the coarse grade is therefore executed on every run, exactly like the grade it
|
|
justifies — a prose claim would decay the same way the hand-run witnessing this harness replaces
|
|
did. No entry is graded `DETECTOR` since ersatztv#891, so that runner currently executes nothing;
|
|
`test_the_DETECTOR_survivor_set_is_empty_ON_PURPOSE` asserts the emptiness so it stays a recorded
|
|
decision rather than an unread skip.
|
|
"""
|
|
|
|
CLAUSE = "CLAUSE"
|
|
DETECTOR = "DETECTOR"
|
|
|
|
guard: str
|
|
target: str
|
|
clause: str
|
|
replacement: str
|
|
proof: str
|
|
granularity: str
|
|
expect: str
|
|
why: str
|
|
survived_clause: str = ""
|
|
survived_replacement: str = ""
|
|
|
|
@property
|
|
def node_id(self) -> str:
|
|
"""The inventory records proof refs as `file.py::test`; pytest wants a path."""
|
|
return f"scripts/tests/{self.proof}"
|
|
|
|
|
|
@dataclass(frozen=True)
|
|
class Claim:
|
|
"""One PROSE claim about a mutation's outcome, bound to the sentence that makes it.
|
|
|
|
A `Mutation` above is keyed on a GUARD, because its population is the `MUTATION`-graded rows of
|
|
`docs/guard-inventory.md`. A claim is keyed on the PROSE instead: `site` names the tracked file
|
|
whose text makes the claim and `quote` is that text, verbatim. Both halves are checked every run
|
|
— the quote must occur exactly once in the site — so a reworded sentence reports as a retarget
|
|
rather than drifting away from the entry that justifies it. That binding is the thing #812's four
|
|
defects were missing; each was a sentence with nothing tying it to what it asserted.
|
|
|
|
`outcome` is `RED` or `GREEN`, and the GREEN direction is why this is not just another `Mutation`.
|
|
A `MUTATION` row always claims a red, so the harness only ever had to recognise one. Prose does
|
|
not, and the corpus carries the other direction too: `.gitea/workflows/review-verdict.yml`,
|
|
`scripts/check-doc-narrative.py` and `scripts/tests/hook_fire_isolation.py` each name a mutation —
|
|
an arm disarmed on its own, an arm removed, a dead branch deleted — and assert that nothing
|
|
notices it. How each of those sentences words its outcome is deliberately not repeated here: a
|
|
restatement is a second copy of an outcome, free to drift from the site while the entry that
|
|
executes it stays green, which is the drift a `Claim` exists to close. What they share is the
|
|
shape — a claim that a mutation is NOT noticed — and for that shape the rule "declare it or do
|
|
not write it" is unsatisfiable 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 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
|
|
goes red and the sentence has to be rewritten. `testing.mutation-claims-are-executed` records the
|
|
direction that matters — a claim that can no longer decay is a tautology reading like a proof.
|
|
"""
|
|
|
|
RED = "RED"
|
|
GREEN = "GREEN"
|
|
|
|
site: str
|
|
quote: str
|
|
target: str
|
|
clause: str
|
|
replacement: str
|
|
proof: str
|
|
outcome: str
|
|
expect: str
|
|
why: str
|
|
reach_replacement: str = ""
|
|
reach_expect: str = ""
|
|
|
|
@property
|
|
def node_id(self) -> str:
|
|
"""A claim may name a whole proof FILE, where the prose says "leaves the suite green"."""
|
|
return f"scripts/tests/{self.proof}"
|
|
|
|
|
|
@dataclass(frozen=True)
|
|
class Verdict:
|
|
ok: bool
|
|
reason: str
|
|
|
|
|
|
def _clean_env(**extra: str) -> dict[str, str]:
|
|
"""The environment every subprocess here runs in, with git's ambient state REMOVED.
|
|
|
|
Exported `GIT_*` variables override `-C` and `cwd`. `GIT_DIR`, `GIT_WORK_TREE`,
|
|
`GIT_INDEX_FILE`, `GIT_COMMON_DIR` and `GIT_OBJECT_DIRECTORY` each redirect part of a repository;
|
|
`GIT_CONFIG_COUNT`/`GIT_CONFIG_KEY_n`/`GIT_CONFIG_VALUE_n` inject arbitrary settings, `core.worktree`
|
|
among them. Any of those reaching this module's `git init`/`add`/`commit`/`reset --hard` points
|
|
them at the REAL repository, and the "sandbox" would then write through the tree it exists to
|
|
stay out of. A git hook exports several of them, and this suite runs from one.
|
|
|
|
So this is a DENY-BY-DEFAULT boundary rather than a list of the variables anyone has thought of:
|
|
every `GIT_*` is dropped and only the identity this module sets itself is put back. An enumeration
|
|
of the dangerous ones shipped here once, covering three of them — a list is what this replaces.
|
|
"""
|
|
env = {k: v for k, v in os.environ.items() if not k.startswith("GIT_")}
|
|
env.update(extra)
|
|
return env
|
|
|
|
|
|
def _git(cwd: Path, *args: str) -> subprocess.CompletedProcess:
|
|
# `-c` rather than the ambient configuration, because the sandbox must not inherit the
|
|
# developer's machine: a global `core.hooksPath` would fire this repo's husky hooks against a
|
|
# throwaway tree, and `commit.gpgsign` would block the commit on a signing key CI does not have —
|
|
# indefinitely, at a pinentry prompt, which no pytest timeout is watching.
|
|
return subprocess.run(
|
|
# `core.worktree` is pinned along with the rest: a proof that plants one in the sandbox's own
|
|
# config would otherwise redirect `reset --hard` and `clean -qffdx` at a tree outside it.
|
|
[
|
|
"git",
|
|
"-c",
|
|
"core.hooksPath=/dev/null",
|
|
"-c",
|
|
"commit.gpgsign=false",
|
|
"-c",
|
|
f"core.worktree={cwd}",
|
|
*args,
|
|
],
|
|
cwd=str(cwd),
|
|
check=True,
|
|
capture_output=True,
|
|
timeout=GIT_TIMEOUT,
|
|
env=_clean_env(
|
|
GIT_AUTHOR_NAME="mutation-harness",
|
|
GIT_AUTHOR_EMAIL="harness@example.invalid",
|
|
GIT_COMMITTER_NAME="mutation-harness",
|
|
GIT_COMMITTER_EMAIL="harness@example.invalid",
|
|
),
|
|
)
|
|
|
|
|
|
def build_sandbox(dest: Path, root: Path = REPO_ROOT) -> Path:
|
|
"""Materialise `root`'s tracked files at `dest` and make it a git repository."""
|
|
entries = subprocess.run(
|
|
["git", "-C", str(root), "ls-files", "-s", "-z"],
|
|
capture_output=True,
|
|
check=True,
|
|
timeout=GIT_TIMEOUT,
|
|
env=_clean_env(),
|
|
).stdout.decode()
|
|
|
|
copied = 0
|
|
for entry in entries.split("\0"):
|
|
if not entry:
|
|
continue
|
|
meta, path = entry.split("\t", 1)
|
|
mode = meta.split()[0]
|
|
if mode == "160000": # gitlink — see the module docstring
|
|
continue
|
|
src = root / path
|
|
dst = dest / path
|
|
dst.parent.mkdir(parents=True, exist_ok=True)
|
|
if src.is_symlink():
|
|
os.symlink(os.readlink(src), dst)
|
|
else:
|
|
shutil.copy2(src, dst)
|
|
copied += 1
|
|
|
|
if copied == 0:
|
|
raise RuntimeError(
|
|
"the sandbox population is EMPTY — `git ls-files` returned nothing, so every mutation "
|
|
"below would run against an empty tree and report success. Anti-vacuity, not paranoia."
|
|
)
|
|
|
|
_git(dest, "init", "-q", ".")
|
|
# `-f` because some tracked files are also gitignored; without it they would be dropped from the
|
|
# sandbox's index and a guard deriving its population from `git ls-files` would see less than the
|
|
# real repo does.
|
|
_git(dest, "add", "-A", "-f", ".")
|
|
_git(dest, "commit", "-qm", "mutation-harness sandbox")
|
|
_BASELINES[str(dest.resolve())] = _git(dest, "rev-parse", "HEAD").stdout.decode().strip()
|
|
return dest
|
|
|
|
|
|
def reset_sandbox(sandbox: Path) -> None:
|
|
"""Return the sandbox to its committed state between mutations.
|
|
|
|
The proof tests write into `tmp_path`, but a guard driven through its real entry point can leave
|
|
artifacts in the tree it is pointed at, and one mutation's residue reaching the next would make
|
|
the second result a function of the first's.
|
|
"""
|
|
# RESET TO THE RECORDED BASELINE COMMIT, never to bare HEAD. `git reset --hard` with no argument
|
|
# resets to whatever HEAD currently is — so a proof test that COMMITS inside the sandbox moves
|
|
# HEAD onto a commit containing the mutant, and every later "reset" would then faithfully restore
|
|
# it. The `finally` in `verify_mutation` puts the file back, but nothing would put HEAD back, and
|
|
# the contamination would surface as an unrelated red several mutations later.
|
|
#
|
|
# `-ff` rather than `-f` because a single `-f` refuses to delete a nested git repository, which is
|
|
# precisely what a proof driving `git init` or `git worktree add` into the sandbox leaves behind.
|
|
baseline = _BASELINES.get(str(sandbox.resolve()))
|
|
if baseline is None:
|
|
raise RuntimeError(
|
|
f"no recorded baseline for {sandbox} — it was not built by build_sandbox, so there is "
|
|
"nothing to reset TO and a reset here would pin whatever state the tree is in now"
|
|
)
|
|
_git(sandbox, "reset", "-q", "--hard", baseline)
|
|
_git(sandbox, "clean", "-qffdx")
|
|
|
|
|
|
def run_pytest(sandbox: Path, node_ids: list[str]) -> subprocess.CompletedProcess:
|
|
return subprocess.run(
|
|
[
|
|
sys.executable,
|
|
"-m",
|
|
"pytest",
|
|
"-q",
|
|
"--no-header",
|
|
"--tb=short", # the assertion MESSAGE, which `expect` is matched against
|
|
"-p",
|
|
"no:cacheprovider", # keeps `git status` in the sandbox clean between mutations
|
|
*node_ids,
|
|
],
|
|
cwd=str(sandbox),
|
|
capture_output=True,
|
|
text=True,
|
|
env=_clean_env(PYTHONPATH="."),
|
|
timeout=PYTEST_TIMEOUT,
|
|
)
|
|
|
|
|
|
# Only exit code 1 means "a test ran and failed", and it is the only status accepted here. Everything
|
|
# else is rejected, which matters most for the two ways a proof ref goes stale — measured, because
|
|
# they are easy to get the wrong way round: with an explicit `file.py::function` node id, a missing
|
|
# FILE and a missing FUNCTION both exit 4 ("ERROR: not found"), while 5 needs a successful collection
|
|
# that selected nothing — a deselection. Reading either as a guard going red is how a harness reports
|
|
# coverage it does not have.
|
|
_PYTEST_RED_MEANINGS = {
|
|
0: "the named test still PASSED with the clause mutated, so the clause is not load-bearing for it",
|
|
2: "the inner pytest was interrupted",
|
|
3: "the inner pytest hit an internal error",
|
|
4: "the inner pytest could not resolve the node id — the proof ref names a file or a test that does not exist",
|
|
5: "the inner pytest collected successfully but selected NOTHING — the proof ref was deselected",
|
|
}
|
|
|
|
|
|
def _mutate_and_run(
|
|
sandbox: Path, target_path: str, clause: str, replacement: str, node_id: str
|
|
) -> tuple[Verdict | None, subprocess.CompletedProcess | None]:
|
|
"""Apply one declared clause mutation and run one proof ref under it.
|
|
|
|
Split out of `verify_mutation` so the RED and GREEN directions share ONE application path rather
|
|
than two copies of it. Everything that can go wrong BEFORE the proof runs — an absent target, a
|
|
clause that has moved or acquired a second site, a replacement identical to the clause — is the
|
|
same question in both directions and is answered here; each direction then reads the result its
|
|
own way. A `Verdict` comes back only when the mutation could not be applied at all.
|
|
"""
|
|
target = sandbox / target_path
|
|
if not target.is_file():
|
|
return Verdict(False, f"the mutation target {target_path} does not exist in the sandbox"), None
|
|
|
|
original = target.read_text(encoding="utf-8")
|
|
occurrences = original.count(clause)
|
|
if occurrences != 1:
|
|
return (
|
|
Verdict(
|
|
False,
|
|
f"the declared clause occurs {occurrences} times in {target_path}, not once. "
|
|
"RETARGET it rather than loosening the match — a clause that has moved, or that now "
|
|
"matches a second site, means the recorded proof no longer points at what it claims to.",
|
|
),
|
|
None,
|
|
)
|
|
|
|
mutated = original.replace(clause, replacement, 1)
|
|
if mutated == original:
|
|
return Verdict(False, "the replacement is identical to the clause, so nothing was mutated"), None
|
|
|
|
target.write_text(mutated, encoding="utf-8")
|
|
try:
|
|
return None, run_pytest(sandbox, [node_id])
|
|
finally:
|
|
target.write_text(original, encoding="utf-8")
|
|
|
|
|
|
def verify_mutation(sandbox: Path, mutation: Mutation) -> Verdict:
|
|
"""Apply one declared mutation in `sandbox` and require its named test to go red.
|
|
|
|
The sandbox is left as it was found; callers still `reset_sandbox` between mutations because a
|
|
driven guard can dirty the tree in ways this function does not know about.
|
|
"""
|
|
refusal, result = _mutate_and_run(sandbox, mutation.target, mutation.clause, mutation.replacement, mutation.node_id)
|
|
if refusal is not None:
|
|
return refusal
|
|
assert result is not None # `_mutate_and_run` returns exactly one of the two
|
|
|
|
output = result.stdout + result.stderr
|
|
if result.returncode != 1:
|
|
meaning = _PYTEST_RED_MEANINGS.get(result.returncode, f"unexpected pytest exit code {result.returncode}")
|
|
return Verdict(False, f"{meaning}\n--- inner pytest output ---\n{output[-3000:]}")
|
|
# MATCHED AGAINST THE EXCEPTION OUTPUT ALONE, not the whole run. `--tb=short` echoes the failing
|
|
# SOURCE as well as the message, and every one of these assertions carries its message as a
|
|
# string literal a line or two above — so matching the full output would let a red at assertion A
|
|
# be certified by assertion B's text merely being on screen. Pytest prefixes exception lines with
|
|
# `E `, and that is the only part that reports what actually failed.
|
|
diagnostic = "\n".join(line[2:] for line in output.splitlines() if line.startswith("E "))
|
|
# This couples the harness to pytest's traceback FORMAT, and pytest is deliberately unpinned in
|
|
# `script-tests`. The coupling is fail-CLOSED: a release that stopped prefixing exception lines
|
|
# with `E ` would empty `diagnostic` and every row would fail here naming its own expectation,
|
|
# which is loud and instantly diagnosable. The alternative — matching the whole run — fails
|
|
# silently in the direction that certifies rows on the wrong red. Note the join: a multi-line
|
|
# assertion message arrives as several `E ` lines, so an expectation must not span a newline.
|
|
if mutation.expect not in diagnostic:
|
|
return Verdict(
|
|
False,
|
|
f"the named test went red, but NOT with the declared diagnostic {mutation.expect!r}. A red "
|
|
"for a reason other than the one this row records is not evidence about the clause — a "
|
|
"crash, a syntax error or an unrelated parametrisation all look like this. Re-declare "
|
|
f"`expect` once you know what the mutation now produces.\n--- inner pytest output ---\n"
|
|
f"{output[-3000:]}",
|
|
)
|
|
return Verdict(True, "the named test went red under the declared mutation, with the declared diagnostic")
|
|
|
|
|
|
def verify_claim(sandbox: Path, claim: Claim) -> Verdict:
|
|
"""Execute one declared prose claim: apply its mutation and require its DECLARED direction.
|
|
|
|
RED delegates to `verify_mutation`, deliberately and not for brevity: a claim that a mutation IS
|
|
noticed is the same assertion a `MUTATION` row makes, and giving it a second implementation is
|
|
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 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(
|
|
sandbox,
|
|
Mutation(
|
|
guard=claim.site,
|
|
target=claim.target,
|
|
clause=claim.clause,
|
|
replacement=claim.replacement,
|
|
proof=claim.proof,
|
|
granularity=Mutation.CLAUSE,
|
|
expect=claim.expect,
|
|
why=claim.why,
|
|
),
|
|
)
|
|
if claim.outcome != Claim.GREEN:
|
|
return Verdict(
|
|
False,
|
|
f"unknown outcome {claim.outcome!r} on the claim at {claim.site} — declare RED (the "
|
|
"mutation is noticed) or GREEN (it is not). An outcome this function does not recognise "
|
|
"must not read as a verified claim.",
|
|
)
|
|
|
|
refusal, result = _mutate_and_run(sandbox, claim.target, claim.clause, claim.replacement, claim.node_id)
|
|
if refusal is not None:
|
|
return refusal
|
|
assert result is not None # `_mutate_and_run` returns exactly one of the two
|
|
|
|
output = result.stdout + result.stderr
|
|
if result.returncode != 0:
|
|
return Verdict(
|
|
False,
|
|
f"the prose at {claim.site} says this mutation leaves {claim.proof} GREEN, but the run "
|
|
f"exited {result.returncode}. If the mutation is now noticed that is good news about the "
|
|
"code and bad news about the sentence: rewrite the sentence, and regrade this entry RED "
|
|
f"with the diagnostic it produces.\n--- inner pytest output ---\n{output[-3000:]}",
|
|
)
|
|
if "passed" not in output:
|
|
return Verdict(
|
|
False,
|
|
f"the run of {claim.proof} exited 0 but NOTHING PASSED — every test was skipped, "
|
|
"deselected or absent. A green nothing ran is not evidence that the mutation went "
|
|
f"unnoticed.\n--- inner pytest output ---\n{output[-3000:]}",
|
|
)
|
|
|
|
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",
|
|
)
|