Build ErsatzTV Image / CI toolchain image resolves (pull_request) Successful in 6s
Build ErsatzTV Image / Delimiter ban (release path) (pull_request) Successful in 20s
PR Gates / CI image pin matches docker/ci (pull_request) Successful in 17s
PR Gates / decisions lifecycle (pull_request) Successful in 23s
PR Gates / Docs update reminder (pull_request) Successful in 14s
PR Gates / Fix proofs (Proves trailers) (pull_request) Successful in 11s
Review verdict / Set review-verdict status (pull_request_target) Successful in 37s
review-verdict/h10 Review-verdict: MERGEABLE @ 0f8e73a (base: main)
Build ErsatzTV Image / Build & test (.NET) (pull_request) Successful in 8m47s
Build ErsatzTV Image / EF migration integrity (SQLite + MySql) (pull_request) Successful in 6m3s
Build ErsatzTV Image / Build & push image (amd64) (pull_request) Skipped
PR Gates / Script lint and tests (ruff + pytest) (pull_request) Successful in 19m41s
Build ErsatzTV Image / Functional E2E (curl + UI contracts) (pull_request) Successful in 5m47s
Build ErsatzTV Image / API docs in sync (OpenAPI + endpoint index) (pull_request) Successful in 8s
Build ErsatzTV Image / Formatting (changed .cs conform to .editorconfig) (pull_request) Successful in 6s
The previous commit replaced "the order is load-bearing" with "and that is the whole of what the order buys". What was measured is narrower: with the relevance gate moved first, the three gates are each still witnessed refusing alone. That does not establish the order buys nothing else - the reset placement is a second candidate, unmeasured either way - so the absolute is gone from both sites and what stays is the cost reason, which is readable from the control flow. refs #881 Decisions-Edit: yes Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015QqCpYFsKgnAnx6jVwrKiV
514 lines
26 KiB
Python
514 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 BECAUSE IT IS THE EXPENSIVE ONE: it is the only one of the three
|
|
that costs a second full run of the proof — under the reach mutation, with a sandbox reset in
|
|
between — so an entry the status or the vacuity gate has already refused never pays for it. What
|
|
keeps the three worth three is that each carries its own disarm proof, rather than the position
|
|
it sits in. 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",
|
|
)
|