diff --git a/wizard-work/null/README-proveit.md b/wizard-work/null/README-proveit.md index ae5cb43..b59131c 100644 --- a/wizard-work/null/README-proveit.md +++ b/wizard-work/null/README-proveit.md @@ -36,10 +36,12 @@ Exit codes: `0` all claims PASS, `1` at least one claim not PASS, `2` harness br ## The judge (external, does not import proveit) -`_judge.py` runs the artifact as a subprocess and checks 25 observable contracts: +`_judge.py` runs the artifact as a subprocess and checks 29 observable contracts: exit codes, report contents, JSON coherence, the honesty properties, path -robustness (the artifact copied elsewhere must still find and scan itself), and -the negative control that a raising predicate is never reported PASS. +robustness (the artifact copied elsewhere must still find and scan itself), the +negative control that a raising predicate is never reported PASS, that `repeat=N` +really invokes the predicate N times, and that an *incomplete* run (a predicate +that raises before `repeat` is met) reports `measured=False` rather than `True`. ``` python3 _judge.py @@ -48,16 +50,38 @@ python3 _judge.py ## Teeth (the verdict is not a tautology) `_probe_teeth.py` plants a real defect — rewriting the runner's `PASS` to -`UNVERIFIED` — and asserts the judge exits nonzero. A verdict command that cannot -go nonzero is decoration; this one does go nonzero. +`UNVERIFIED` — and asserts the judge exits nonzero. + +`_probe_mutations.py` is the stronger check: it plants **15** plausible regressions +(swapped PASS/FAIL derivation, a neutered run loop, a hardcoded `measured = True`, +a lying summary count, a capped `repeat`, ...) and requires the judge to exit +nonzero on every one. A judge that always exits 0 cannot pass it. + +``` +python3 _probe_mutations.py +``` + +## The battery (one command, one exit code) + +`verify.py` runs all four stages and exits 0 only if each passed *and* the judge +demonstrated teeth: + +``` +python3 verify.py +``` + +Its stage 3 success token pins the count ("15/15"), so a newly planted defect that +slips past the judge fails the battery instead of silently widening the blind spot. ## Measured result - `proveit.py --selfcheck` → exit 0, "8/8 meta-assertions hold" - `proveit.py` → exit 1, `5/7 claims PASS, 2 FAIL` (the two FAILs are the intentional negative controls — the runner is honest, not broken) -- `_judge.py` → exit 0, all 25 contract checks hold +- `_judge.py` → exit 0, 29/29 contract checks hold +- `_probe_mutations.py` → exit 0, 15/15 planted defects caught - `_probe_teeth.py` → exit 0, mutated artifact rejected with judge exit 1 +- `verify.py` → exit 0, 4/4 stages passed ## Bugs this process actually caught (evidence, not narrative) @@ -72,3 +96,15 @@ go nonzero is decoration; this one does go nonzero. branch of `status="PASS" if ok else "FAIL"` and reported only `{"PASS"}`. The judge caught the divergence between `--scan-status` and the selfcheck. Fixed by resolving `IfExp` branches; the scan now reports `{"FAIL", "PASS"}`. +4. The judge could not see `measured = True` hardcoded. Contracts 8-10 all run the + loop to completion, where `ran >= max(1, repeat)` is True either way, so the + mutation scored 14/15 and read as a coverage hole. The observable difference + lives in an *incomplete* run: a predicate that raises on the first of + `repeat=3` invocations leaves `ran=1 < 3`, so correct code reports + `measured=False` and the mutation reports `True`. Contract 11 pins that; + sensitivity went to 15/15. +5. `_probe_teeth.py` did its "point the judge at the mutated artifact" step with a + string replace against a hardcoded absolute path that no longer existed in + `_judge.py`. The replace matched nothing, so the probe's premise was never + checked and it could have printed `TEETH OK` over an unmutated artifact. It now + copies both files into a scratch dir and asserts the mutation actually applied. diff --git a/wizard-work/null/_judge.py b/wizard-work/null/_judge.py index 89bd5f8..3fc3031 100644 --- a/wizard-work/null/_judge.py +++ b/wizard-work/null/_judge.py @@ -116,6 +116,118 @@ finally: check("imported artifact reports a raising predicate as FAIL", p3.returncode == 0 and "STATUS=FAIL" in p3.stdout) +# --- contract 8: the `measured` flag is load-bearing, not decorative -------- +# A harness that hardcodes measured=True never increments a call counter, so +# `repeat=N` is silently ignored. Mutating `measured = ran >= max(1, repeat)` +# to `measured = True` is invisible to every other contract, so it needs its +# own: a predicate that must be invoked exactly `repeat` times. +# The probe is written as a real file (not a one-liner) because a `def` on a +# single generated line is a SyntaxError -- a defect found the hard way. +PROBE_CALLS = os.path.join(HERE, "_probe_calls.py") +with open(PROBE_CALLS, "w", encoding="utf-8") as fh: + fh.write( + "import sys\n" + "sys.path.insert(0, %r)\n" + "import proveit\n" + "n = {'c': 0}\n" + "def f():\n" + " n['c'] += 1\n" + " return True\n" + "s = proveit.Suite('x')\n" + "c = s.make_claim('repeat control', 'control', f, repeat=3)\n" + "ok = (n['c'] == 3 and c.calls == 3 and c.measured is True)\n" + "print('CALLS=' + str(n['c']) + ' MEASURED=' + str(c.measured))\n" + "sys.exit(0 if ok else 1)\n" % (os.path.dirname(ART),)) +try: + p4 = subprocess.run([sys.executable, PROBE_CALLS], capture_output=True, + text=True, cwd="/") +finally: + os.unlink(PROBE_CALLS) +check("repeat=N actually invokes the predicate N times", + p4.returncode == 0 and "CALLS=3" in p4.stdout) + +# --- contract 9: a skipped run is never reported as a PASS ------------------- +# If the run loop is neutered the harness must still have run the predicate; a +# PASS that was never measured is the exact lie this artifact exists to forbid. +PROBE_RUN = os.path.join(HERE, "_probe_ran.py") +with open(PROBE_RUN, "w", encoding="utf-8") as fh: + fh.write( + "import sys\n" + "sys.path.insert(0, %r)\n" + "import proveit\n" + "n = {'c': 0}\n" + "def f():\n" + " n['c'] += 1\n" + " return True\n" + "s = proveit.Suite('x')\n" + "c = s.make_claim('must actually run', 'control', f, repeat=2)\n" + "ok = (c.status == 'PASS' and n['c'] == 2 and c.measured is True)\n" + "sys.exit(0 if ok else 1)\n" % (os.path.dirname(ART),)) +try: + p5 = subprocess.run([sys.executable, PROBE_RUN], capture_output=True, + text=True, cwd="/") +finally: + os.unlink(PROBE_RUN) +check("predicate is invoked and measured (harness never reports a no-op PASS)", + p5.returncode == 0) + +# --- contract 10: the `measured` field is load-bearing ---------------------- +# A predicate that returns False while reporting itself measured must be FAIL, +# and a predicate that was never run at all must never be PASS. Contract 9 +# pins the positive side (repeat=N really runs N times); this pins the negative +# side, which is the branch a hardcoded `measured = True` silently corrupts. +PROBE_MEASURED = os.path.join(HERE, "_probe_measured.py") +with open(PROBE_MEASURED, "w", encoding="utf-8") as fh: + fh.write( + "import sys\n" + "sys.path.insert(0, %r)\n" + "import proveit\n" + "s = proveit.Suite('x')\n" + "a = s.make_claim('false but measured', 'control', lambda: False)\n" + "b = s.make_claim('true and measured', 'control', lambda: True)\n" + "ok = (a.status == 'FAIL' and a.measured is True and a.calls == 1\n" + " and b.status == 'PASS' and b.measured is True)\n" + "print('A=' + a.status + ' B=' + b.status)\n" + "sys.exit(0 if ok else 1)\n" % (os.path.dirname(ART),)) +try: + p6 = subprocess.run([sys.executable, PROBE_MEASURED], capture_output=True, + text=True, cwd="/") +finally: + os.unlink(PROBE_MEASURED) +check("a measured False is FAIL and a measured True is PASS (measured is load-bearing)", + p6.returncode == 0 and "A=FAIL B=PASS" in p6.stdout) + +# --- contract 11: `measured` must go False when the run loop did not finish -- +# Contracts 8-10 pin the positive side (repeat=N really runs N times; a False +# predicate is FAIL). None of them can see `measured = True` hardcoded, because +# in every probe they run the loop to completion and `ran >= max(1, repeat)` is +# True anyway. The observable difference lives in the *incomplete* run: a +# predicate that raises on the first of `repeat=3` invocations leaves ran=1 < 3, +# so the correct code reports measured=False while the hardcoded mutation +# reports measured=True. _probe_mutations.py plants exactly that mutation and +# this is the contract that catches it -- before this existed, the sensitivity +# run reported 14/15 with "measured flag hardcoded true" as a coverage hole. +PROBE_PARTIAL = os.path.join(HERE, "_probe_partial.py") +with open(PROBE_PARTIAL, "w", encoding="utf-8") as fh: + fh.write( + "import sys\n" + "sys.path.insert(0, %r)\n" + "import proveit\n" + "s = proveit.Suite('x')\n" + "c = s.make_claim('raises on the first of 3', 'control', lambda: 1/0, repeat=3)\n" + "ok = (c.calls == 1 and c.measured is False and c.status == 'FAIL'\n" + " and 'ZeroDivisionError' in c.error)\n" + "print('CALLS=' + str(c.calls) + ' MEASURED=' + str(c.measured)\n" + " + ' STATUS=' + c.status)\n" + "sys.exit(0 if ok else 1)\n" % (os.path.dirname(ART),)) +try: + p7 = subprocess.run([sys.executable, PROBE_PARTIAL], capture_output=True, + text=True, cwd="/") +finally: + os.unlink(PROBE_PARTIAL) +check("an incomplete run (raise before repeat is met) is measured=False, not True", + p7.returncode == 0 and "MEASURED=False" in p7.stdout) + print() if problems: print("JUDGE: %d contract check(s) FAILED" % len(problems)) diff --git a/wizard-work/null/_probe_mutations.py b/wizard-work/null/_probe_mutations.py new file mode 100644 index 0000000..fcc2f90 --- /dev/null +++ b/wizard-work/null/_probe_mutations.py @@ -0,0 +1,165 @@ +#!/usr/bin/env python3 +"""Mutation sensitivity check for proveit.py (the judge's real teeth). + +The judge (_judge.py) checks observable behaviour. This file asks the harder +question: does the judge actually notice when the artifact is broken? It plants +N real, plausible regressions, runs the judge against each, and requires that +the judge exits NONZERO for every one of them. + +A judge that always exits 0 -- or that only fails on the one hardcoded mutation +in _probe_teeth.py -- is decoration. This script measures the judge's +sensitivity across a whole defect family, so "judge exit 0" on a clean tree is +a statement about N defects, not one. + +Exit 0 == every planted defect was caught (judge is sensitive). +Exit 1 == at least one defect slipped past the judge (a real coverage hole). +""" +import os +import shutil +import subprocess +import sys +import tempfile + +HERE = os.path.dirname(os.path.abspath(__file__)) +ART = os.path.join(HERE, "proveit.py") +JUDGE = os.path.join(HERE, "_judge.py") + +# Each mutation: (name, old, new, probe_args) +# `probe_args` is what we run on the mutated artifact: the judge runs the full +# contract set, but a mutation that breaks e.g. the selfcheck should be caught +# by that selfcheck specifically -- so we assert both "judge nonzero" and +# "the named probe also fails", which localises the hole if one exists. +MUTATIONS = [ + ("swap PASS/FAIL derivation", + 'status="PASS" if (ok and measured) else "FAIL"', + 'status="FAIL" if (ok and measured) else "PASS"'), + ("make every predicate read as true", + "ok = isinstance(value, bool) and value is True", + "ok = True"), + ("never actually invoke the predicate", + "value = predicate()", + "value = None"), + ("control never counts as a real raise", + "ran += 1\n last_error = \"\".join(", + "pass # mutation: swallow the raise, ran never increments\n last_error = \"\".join("), + ("predicate invocation never counted", + "ran += 1\n except", + "pass # mutation: exception never counted\n except"), + ("status domain widened to UNVERIFIED", + 'status="PASS" if (ok and measured) else "FAIL"', + 'status="PASS" if (ok and measured) else "UNVERIFIED"'), + ("summary pass count lies", + '"pass": sum(1 for c in suite.claims if c.status == "PASS"),', + '"pass": len(suite.claims),'), + ("exit code always success", + "return 0 if all(c.status == \"PASS\" for c in suite.claims) else 1", + "return 0"), + ("skip claims that would fail", + "self.claims.append(claim)", + "self.claims.append(claim)\n self.claims.pop() if claim.status == \"FAIL\" else None"), + ("run loop neutered (zero iterations)", + "for _ in range(max(1, repeat)):", + "for _ in range(0):"), + ("predicate return value discarded", + "value = predicate()", + "predicate(); value = None"), + ("expected-exception check removed", + "ok = isinstance(exc, expect_exception) if expect_exception else False", + "ok = False"), + ("measured flag hardcoded true", + "measured = ran >= max(1, repeat)", + "measured = True"), + ("repeat is silently capped at 1", + "for _ in range(max(1, repeat)):", + "for _ in range(min(1, max(1, repeat))):"), + ("drop the traceback from the claim", + "error=last_error,", + "error=\"\","), +] + + +def run(cmd, cwd=None): + p = subprocess.run(cmd, capture_output=True, text=True, cwd=cwd) + return p.returncode, p.stdout, p.stderr + + +def run_judge(adir): + """Run the judge located in `adir` (where the artifact also lives).""" + return run([sys.executable, os.path.join(adir, "_judge.py")], cwd=adir) + + +def write_probe(dirpath, filename, artifact_dir, body): + """Write a probe file next to `artifact_dir` so its sys.path trick lands.""" + path = os.path.join(dirpath, filename) + with open(path, "w", encoding="utf-8") as fh: + fh.write(body % artifact_dir) + return path + + +def run_probe(path): + return run([sys.executable, path], cwd="/") + + +def main(): + # sanity: every anchor must exist exactly once in the artifact, otherwise + # the sensitivity measurement below is silently vacuous. + if not os.path.exists(ART): + print("MUTATION: artifact missing: %s" % ART) + return 1 + with open(ART, "r", encoding="utf-8") as fh: + src = fh.read() + bad = [name for name, old, _ in MUTATIONS if src.count(old) != 1] + if bad: + print("MUTATION: anchors not unique in %s: %s" % (ART, ", ".join(bad))) + return 1 + + # ---- baseline: clean tree must pass the judge -------------------------- + rc, out, err = run_judge(HERE) + print("baseline judge exit: %d" % rc) + if rc != 0: + print("MUTATION: judge does not pass on the clean artifact; " + "sensitivity test is meaningless") + print(err[-2000:]) + return 1 + if "all contract checks hold" not in out: + print("MUTATION: baseline judge output lacks its success line") + return 1 + + tmpdir = tempfile.mkdtemp(prefix="proveit-mut-") + caught, missed = 0, [] + try: + for name, old, new in MUTATIONS: + if src.count(old) != 1: + print(" SKIP %-38s (anchor not unique: %d)" + % (name, src.count(old))) + missed.append(name + " (anchor not found)") + continue + mdir = tempfile.mkdtemp(prefix="mut-", dir=tmpdir) + mpath = os.path.join(mdir, "proveit.py") + with open(mpath, "w", encoding="utf-8") as fh: + fh.write(src.replace(old, new, 1)) + # copy the judge alongside so relative artifact discovery works + shutil.copy2(JUDGE, os.path.join(mdir, "_judge.py")) + jrc, jout, jerr = run_judge(mdir) + if jrc != 0: + caught += 1 + print(" CAUGHT %-37s judge exit=%d" % (name, jrc)) + else: + print(" MISSED %-37s judge exit=0 <-- coverage hole" % name) + missed.append(name) + finally: + shutil.rmtree(tmpdir, ignore_errors=True) + + print() + total = len(MUTATIONS) + print("MUTATION SENSITIVITY: %d/%d planted defects caught by the judge" + % (caught, total)) + if missed: + print("MUTATION: uncovered defect(s): %s" % ", ".join(missed)) + return 1 + print("MUTATION SENSITIVITY OK") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/wizard-work/null/_probe_teeth.py b/wizard-work/null/_probe_teeth.py index 020d12b..aca8953 100644 --- a/wizard-work/null/_probe_teeth.py +++ b/wizard-work/null/_probe_teeth.py @@ -4,35 +4,52 @@ A verdict that cannot go nonzero is a tautology. This plants a real defect -- rewriting the runner's PASS to UNVERIFIED -- and asserts the judge exits nonzero. Exit 0 == the judge has teeth. + +The judge discovers its artifact relative to its own location, so the honest +way to point it at a broken artifact is to copy both files into a scratch dir +and run the copy. An earlier version of this probe instead did a string +replace on a hardcoded absolute path that no longer exists in _judge.py; the +replace silently matched nothing, so the probe's own premise was never +checked. It is now asserted: if the mutation does not apply, the probe fails +loudly instead of printing TEETH OK over an unmutated artifact. """ import os +import shutil import subprocess import sys import tempfile -ART = os.path.join(os.path.dirname(os.path.abspath(__file__)), "proveit.py") -JUDGE = os.path.abspath(__file__) +HERE = os.path.dirname(os.path.abspath(__file__)) +ART = os.path.join(HERE, "proveit.py") +JUDGE = os.path.join(HERE, "_judge.py") + +OLD = 'status="PASS" if (ok and measured) else "FAIL"' +NEW = 'status="UNVERIFIED" if (ok and measured) else "FAIL"' src = open(ART, encoding="utf-8").read() -# Plant the lie: the status domain check must now see UNVERIFIED. -mutated = src.replace('status="PASS" if (ok and measured) else "FAIL"', - 'status="UNVERIFIED" if (ok and measured) else "FAIL"') -assert mutated != src, "mutation did not apply -- test is invalid" +mutated = src.replace(OLD, NEW, 1) +if mutated == src: + # The anchor is gone or no longer unique: the premise of this probe is + # false, so the probe must not report success. + print("TOOTHLESS: mutation anchor %r not found in %s" % (OLD, ART)) + sys.exit(1) -tmp = tempfile.mkdtemp(prefix="proveit-mut-") -bad = os.path.join(tmp, "proveit.py") -open(bad, "w", encoding="utf-8").write(mutated) +tmp = tempfile.mkdtemp(prefix="proveit-teeth-") +try: + bad = os.path.join(tmp, "proveit.py") + with open(bad, "w", encoding="utf-8") as fh: + fh.write(mutated) + shutil.copy2(JUDGE, os.path.join(tmp, "_judge.py")) -# run the judge against the mutated artifact by pointing ART at it -judge_src = open(JUDGE, encoding="utf-8").read().replace( - 'ART = "/root/.hermes/wizard-outputs/null/proveit.py"', 'ART = %r' % bad) -badjudge = os.path.join(tmp, "_judge.py") -open(badjudge, "w", encoding="utf-8").write(judge_src) + p = subprocess.run([sys.executable, os.path.join(tmp, "_judge.py")], + capture_output=True, text=True, cwd=tmp) +finally: + shutil.rmtree(tmp, ignore_errors=True) -p = subprocess.run([sys.executable, badjudge], capture_output=True, text=True) -print("mutated-artifact judge exit code:", p.returncode) +print("mutated-artifact judge exit code: %d" % p.returncode) print("--- judge output (tail) ---") -print("\n".join(p.stdout.strip().splitlines()[-6:])) +for line in p.stdout.strip().splitlines()[-6:]: + print(line) if p.returncode == 0: print() diff --git a/wizard-work/null/verify.py b/wizard-work/null/verify.py new file mode 100644 index 0000000..54f380d --- /dev/null +++ b/wizard-work/null/verify.py @@ -0,0 +1,69 @@ +#!/usr/bin/env python3 +"""verify.py -- one command, one exit code, for the whole proveit battery. + +Exit 0 == every stage passed, and the judge demonstrated teeth on 15 planted defects. +Exit 1 == a stage failed. +Exit 2 == the battery itself broke (a stage file is missing). + +Stages, each run as a subprocess whose own exit code is the verdict: + 1. proveit.py --selfcheck the artifact's own meta-test (8/8) + 2. _judge.py external contract judge (11 contracts) + 3. _probe_mutations.py judge sensitivity: 15 planted defects, all caught + 4. _probe_teeth.py the judge rejects a deliberately lying artifact + +This file is not a tautology. Stage 3 plants real regressions (a swapped +PASS/FAIL derivation, a neutered run loop, a hardcoded `measured = True`, ...) +and requires the judge to exit nonzero on every one, so a judge that always +exits 0 cannot pass this battery. Stage 3's success token also pins the count +("15/15"), so a new planted defect that slips past the judge fails here rather +than silently widening the blind spot. +""" +import os +import subprocess +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) + +STAGES = [ + ("proveit.py --selfcheck", + [sys.executable, os.path.join(HERE, "proveit.py"), "--selfcheck"], + "SELFCHECK OK"), + ("_judge.py", + [sys.executable, os.path.join(HERE, "_judge.py")], + "all contract checks hold"), + ("_probe_mutations.py", + [sys.executable, os.path.join(HERE, "_probe_mutations.py")], + "15/15 planted defects caught"), + ("_probe_teeth.py", + [sys.executable, os.path.join(HERE, "_probe_teeth.py")], + "TEETH OK"), +] + + +def main() -> int: + failures = [] + for label, cmd, token in STAGES: + stage_file = cmd[1] + if not os.path.exists(stage_file): + print("[FAIL] %-24s stage file missing: %s" % (label, stage_file)) + failures.append(label + " (missing)") + continue + p = subprocess.run(cmd, capture_output=True, text=True, cwd=HERE) + ok = p.returncode == 0 and token in p.stdout + print("[%s] %-24s exit=%d" % ("ok " if ok else "FAIL", label, p.returncode)) + if not ok: + failures.append(label) + for line in (p.stdout + p.stderr).strip().splitlines()[-12:]: + print(" " + line) + + print() + if failures: + print("VERIFY: %d stage(s) failed: %s" % (len(failures), ", ".join(failures))) + return 1 + print("VERIFY: 4/4 stages passed " + "(selfcheck 8/8, judge 11 contracts, 15/15 mutation sensitivity, teeth).") + return 0 + + +if __name__ == "__main__": + sys.exit(main())