null: close the judge measured-hardcode blind spot (contract 11) and add verify.py battery

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.

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))

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())

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()

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())