From 845401ab880929e3e644aa217853ad931b63ecfa Mon Sep 17 00:00:00 2001 From: null Date: Tue, 20 Oct 2026 20:40:15 +0000 Subject: [PATCH] null: close 4 judge blind spots found by a blind-spot hunt (contracts 12-15, 19/19 mutations, 5-stage battery) --- wizard-work/null/README-proveit.md | 70 ++++++++++++---- wizard-work/null/_hunt_blindspots.py | 114 +++++++++++++++++++++++++++ wizard-work/null/_judge.py | 107 +++++++++++++++++++++++++ wizard-work/null/_probe_mutations.py | 16 ++++ wizard-work/null/verify.py | 19 +++-- 5 files changed, 305 insertions(+), 21 deletions(-) create mode 100644 wizard-work/null/_hunt_blindspots.py diff --git a/wizard-work/null/README-proveit.md b/wizard-work/null/README-proveit.md index b59131c..990c236 100644 --- a/wizard-work/null/README-proveit.md +++ b/wizard-work/null/README-proveit.md @@ -21,6 +21,10 @@ structurally (AST), not by substring. | a false claim is reported FAIL | negative control, `2+2==5` | | a raising predicate is FAIL | negative control, `ZeroDivisionError` | | a controlled exception is PASS | `expect_exception=` | +| a truthy non-bool is NOT a pass | contract 12, `lambda: "yes"` | +| a raise outside `expect_exception` stays FAIL | contract 13 | +| a subclass of the expected exception is expected | contract 14 | +| an incomplete run is harness-fault exit 2 | contract 15 | ## Commands @@ -36,12 +40,15 @@ 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 29 observable contracts: -exit codes, report contents, JSON coherence, the honesty properties, path -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`. +`_judge.py` runs the artifact as a subprocess and checks 33 observable checks +across 15 contracts: exit codes, report contents, JSON coherence, the honesty +properties, path 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, that an *incomplete* run (a +predicate that raises before `repeat` is met) reports `measured=False` rather than +`True`, that only a strict `True` is a PASS, that `expect_exception` is not a blanket +pass, that a subclass of the expected exception still counts as expected, and that a +harness fault is exit 2 rather than a silently downgraded 1. ``` python3 _judge.py @@ -52,25 +59,45 @@ python3 _judge.py `_probe_teeth.py` plants a real defect — rewriting the runner's `PASS` to `UNVERIFIED` — and asserts the judge exits nonzero. -`_probe_mutations.py` is the stronger check: it plants **15** plausible regressions +`_probe_mutations.py` is the stronger check: it plants **19** 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. +a lying summary count, a capped `repeat`, a truthy non-bool accepted as PASS, ...) +and requires the judge to exit nonzero on every one. A judge that always exits 0 +cannot pass it. ``` python3 _probe_mutations.py ``` +## The hunt (the open question) + +`_hunt_blindspots.py` asks what the mutation list does *not* contain: it applies +further candidate regressions to a throwaway copy and reports which ones the judge +cannot see. Four in-scope holes were found this way (see bugs 6-9 below) and are now +pinned by contracts 12-15 and by matching mutation entries. Four candidates remain +unpinned and are reported honestly rather than faked: + +| candidate | why it is not pinned | +|---|---| +| `detail` drops the error text | `detail` is not a documented claim; no contract asserts it | +| `seconds` always zero | timing is not a documented claim | +| `status` ignores `measured` | equivalent: `measured` is False only when a raise already set `ok=False` | +| selfcheck always returns OK | unmeasurable from outside — it is the meta-test's own verdict | + +``` +python3 _hunt_blindspots.py +``` + ## The battery (one command, one exit code) -`verify.py` runs all four stages and exits 0 only if each passed *and* the judge +`verify.py` runs all five 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 +Its stage 3 success token pins the count ("19/19"), so a newly planted defect that slips past the judge fails the battery instead of silently widening the blind spot. ## Measured result @@ -78,10 +105,11 @@ slips past the judge fails the battery instead of silently widening the blind sp - `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, 29/29 contract checks hold -- `_probe_mutations.py` → exit 0, 15/15 planted defects caught +- `_judge.py` → exit 0, 33/33 observable checks hold (15 contracts) +- `_probe_mutations.py` → exit 0, 19/19 planted defects caught - `_probe_teeth.py` → exit 0, mutated artifact rejected with judge exit 1 -- `verify.py` → exit 0, 4/4 stages passed +- `_hunt_blindspots.py` → exit 0, every in-scope candidate caught +- `verify.py` → exit 0, 5/5 stages passed ## Bugs this process actually caught (evidence, not narrative) @@ -108,3 +136,17 @@ slips past the judge fails the battery instead of silently widening the blind sp `_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. +6. `ok = bool(value)` — a predicate returning a truthy non-bool (`"yes"`, `1`, `[1]`) + was reported PASS. The runner's whole claim is that PASS means an observed `True`, + so this is a real lie, and no contract ever handed the runner a non-bool. + Measured before the fix: judge exit 0 on the mutated tree. Contract 12 pins it. +7. `ok = True if expect_exception else False` — naming an expected exception excused + *any* raise. A `ZeroDivisionError` with `expect_exception=ValueError` was PASS. + Measured before the fix: judge exit 0. Contract 13 pins it. +8. `ok = type(exc) is expect_exception` — stricter-looking and wrong: a *subclass* of + the named exception was no longer treated as expected. Measured before the fix: + judge exit 0. Contract 14 pins it. +9. Removing `FAILURES += 1` — the artifact documents "2 == harness broke" and claims a + broken harness cannot silently pass, but every claim-level contract looks only at + `status`/`measured`, so the fault was downgraded to exit 1 unnoticed. Measured + before the fix: judge exit 0. Contract 15 pins it, and sensitivity went to 19/19. diff --git a/wizard-work/null/_hunt_blindspots.py b/wizard-work/null/_hunt_blindspots.py new file mode 100644 index 0000000..213a283 --- /dev/null +++ b/wizard-work/null/_hunt_blindspots.py @@ -0,0 +1,114 @@ +#!/usr/bin/env python3 +"""_hunt_blindspots.py -- find regressions the judge cannot see. + +The mutation battery in _probe_mutations.py proves the judge catches a *known* +set of defects. This file asks the open question: what plausible regressions +slip past the judge entirely? It applies each candidate to a throwaway copy of +proveit.py, runs the judge against that copy, and prints which ones were MISSED. + +Measured on 2026-10-20 (before contracts 12-15 were added), the judge exit code +was 0 -- i.e. the defect was invisible -- for each of these: + + truthy non-bool accepted as PASS (contract 12) + unrelated raise counts as controlled (contract 13) + controlled-exception check uses type() not isinstance()(contract 14) + harness fault counter never incremented (contract 15) + claim drops the error text from detail (no contract; detail + is not a documented + claim -- out of scope) + seconds always zero (no contract; timing is + not a documented + claim -- out of scope) + status ignores measured (equivalent: measured + is False only when a + raise set ok=False) + selfcheck always returns OK (unmeasurable from + outside: it is the + meta-test's own + verdict; reported, not + faked) + +The four in-scope holes are now pinned by contracts 12-15 and by four matching +entries in _probe_mutations.py. Exit code: 0 == no in-scope hole remains +unpinned; 1 == a hole listed as pinned is still being missed (the pin broke). +""" +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") + +# (name, old, new, in_scope) +CANDIDATES = [ + ("truthy non-bool accepted as PASS", + "ok = isinstance(value, bool) and value is True", + "ok = bool(value)", True), + ("unrelated raise counts as controlled", + "ok = isinstance(exc, expect_exception) if expect_exception else False", + "ok = True if expect_exception else False", True), + ("controlled-exception check uses type() not isinstance()", + "ok = isinstance(exc, expect_exception) if expect_exception else False", + "ok = type(exc) is expect_exception if expect_exception else False", True), + ("harness fault counter never incremented", + " FAILURES += 1", + " pass # mutation", True), + ("claim drops the error text from detail", + "detail=last_error or repr(value),", + "detail=repr(value),", False), + ("seconds always zero", + "seconds=elapsed,", + "seconds=0.0,", False), + ("status ignores measured", + 'status="PASS" if (ok and measured) else "FAIL"', + 'status="PASS" if ok else "FAIL"', False), + ("selfcheck always returns OK", + " if problems:\n print(\"SELFCHECK FAILED:\")", + " if False:\n print(\"SELFCHECK FAILED:\")", False), +] + + +def run(cmd, cwd=None): + p = subprocess.run(cmd, capture_output=True, text=True, cwd=cwd) + return p.returncode, p.stdout, p.stderr + + +def main(): + with open(ART, "r", encoding="utf-8") as fh: + src = fh.read() + broken_pins = [] + for name, old, new, in_scope in CANDIDATES: + if src.count(old) != 1: + print(" ANCHOR? %-52s count=%d" % (name, src.count(old))) + if in_scope: + broken_pins.append(name + " (anchor not unique)") + continue + d = tempfile.mkdtemp(prefix="hunt-") + try: + with open(os.path.join(d, "proveit.py"), "w", encoding="utf-8") as fh: + fh.write(src.replace(old, new, 1)) + shutil.copy2(JUDGE, os.path.join(d, "_judge.py")) + rc, out, _ = run([sys.executable, os.path.join(d, "_judge.py")], cwd=d) + finally: + shutil.rmtree(d, ignore_errors=True) + if rc == 0: + tag = "MISSED (hole)" if in_scope else "slips (out of scope)" + print(" %-18s %s" % (tag, name)) + if in_scope: + broken_pins.append(name) + else: + print(" %-18s %s" % ("caught", name)) + print() + if broken_pins: + print("HUNT: %d pinned defect(s) still slip past the judge: %s" + % (len(broken_pins), ", ".join(broken_pins))) + return 1 + print("HUNT OK: every in-scope candidate regression is caught by the judge.") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/wizard-work/null/_judge.py b/wizard-work/null/_judge.py index 3fc3031..6409a9b 100644 --- a/wizard-work/null/_judge.py +++ b/wizard-work/null/_judge.py @@ -228,6 +228,113 @@ finally: check("an incomplete run (raise before repeat is met) is measured=False, not True", p7.returncode == 0 and "MEASURED=False" in p7.stdout) +# --- contract 12: only a strict True counts as a measurement --------------- +# `ok = bool(value)` looks equivalent at a glance and is not: a predicate that +# returns a truthy non-bool ("yes", 1, [1]) is not returning True, so calling it +# PASS is the exact lie this artifact exists to forbid. No earlier contract ever +# handed the runner a non-bool, so this regression slipped past all 15 planted +# defects (measured: judge exit 0 on the mutated tree). +PROBE_BOOL = os.path.join(HERE, "_probe_bool.py") +with open(PROBE_BOOL, "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('truthy string', 'control', lambda: 'yes')\n" + "b = s.make_claim('truthy int', 'control', lambda: 1)\n" + "c = s.make_claim('real True', 'control', lambda: True)\n" + "d = s.make_claim('falsy int', 'control', lambda: 0)\n" + "ok = (a.status == 'FAIL' and b.status == 'FAIL'\n" + " and c.status == 'PASS' and d.status == 'FAIL')\n" + "print('A=' + a.status + ' B=' + b.status + ' C=' + c.status + ' D=' + d.status)\n" + "sys.exit(0 if ok else 1)\n" % (os.path.dirname(ART),)) +try: + p8 = subprocess.run([sys.executable, PROBE_BOOL], capture_output=True, + text=True, cwd="/") +finally: + os.unlink(PROBE_BOOL) +check("only a strict True is PASS; truthy non-bools and falsy values are FAIL", + p8.returncode == 0 and "A=FAIL B=FAIL C=PASS D=FAIL" in p8.stdout) + +# --- contract 13: expect_exception does not excuse an unrelated raise ------- +# `ok = True if expect_exception else False` makes ANY raise count as controlled +# the moment a caller names an expected type. A ZeroDivisionError is not a +# ValueError, so it must stay FAIL. Measured hole: judge exit 0 when mutated. +PROBE_UNRELATED = os.path.join(HERE, "_probe_unrelated.py") +with open(PROBE_UNRELATED, "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('unrelated raise', 'control', lambda: 1/0,\n" + " expect_exception=ValueError)\n" + "b = s.make_claim('expected raise', 'control', lambda: 1/0,\n" + " expect_exception=ZeroDivisionError)\n" + "ok = (a.status == 'FAIL' and b.status == 'PASS')\n" + "print('A=' + a.status + ' B=' + b.status)\n" + "sys.exit(0 if ok else 1)\n" % (os.path.dirname(ART),)) +try: + p9 = subprocess.run([sys.executable, PROBE_UNRELATED], capture_output=True, + text=True, cwd="/") +finally: + os.unlink(PROBE_UNRELATED) +check("a raise outside expect_exception stays FAIL (expect_exception is not a blanket pass)", + p9.returncode == 0 and "A=FAIL B=PASS" in p9.stdout) + +# --- contract 14: a subclass of the expected exception is still expected --- +# `type(exc) is expect_exception` looks stricter and is wrong: isinstance is the +# correct semantic, so a subclass of the named exception must count as +# controlled. Measured hole: judge exit 0 when mutated. +PROBE_SUBCLASS = os.path.join(HERE, "_probe_subclass.py") +with open(PROBE_SUBCLASS, "w", encoding="utf-8") as fh: + fh.write( + "import sys\n" + "sys.path.insert(0, %r)\n" + "import proveit\n" + "class MyZero(ZeroDivisionError):\n" + " pass\n" + "s = proveit.Suite('x')\n" + "a = s.make_claim('subclass raise', 'control',\n" + " lambda: (_ for _ in ()).throw(MyZero('x')),\n" + " expect_exception=ZeroDivisionError)\n" + "ok = (a.status == 'PASS')\n" + "print('A=' + a.status)\n" + "sys.exit(0 if ok else 1)\n" % (os.path.dirname(ART),)) +try: + p10 = subprocess.run([sys.executable, PROBE_SUBCLASS], capture_output=True, + text=True, cwd="/") +finally: + os.unlink(PROBE_SUBCLASS) +check("a subclass of the expected exception is treated as expected (isinstance, not type)", + p10.returncode == 0 and "A=PASS" in p10.stdout) + +# --- contract 15: a harness fault is exit 2, never silently downgraded ------ +# The artifact documents "2 == harness broke" and claims a broken harness cannot +# silently pass. Removing `FAILURES += 1` is invisible to every claim-level +# contract (all of them look at status/measured), so only the exit code can see +# it. Measured hole: judge exit 0 when the counter never increments. +PROBE_FAULT = os.path.join(HERE, "_probe_fault.py") +with open(PROBE_FAULT, "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" + "s.make_claim('raises on the first of 3', 'control', lambda: 1/0, repeat=3)\n" + "rc = proveit.report(s)\n" + "print('RC=' + str(rc) + ' FAULTS=' + str(proveit.FAILURES))\n" + "sys.exit(0 if (rc == 2 and proveit.FAILURES >= 1) else 1)\n" + % (os.path.dirname(ART),)) +try: + p11 = subprocess.run([sys.executable, PROBE_FAULT], capture_output=True, + text=True, cwd="/") +finally: + os.unlink(PROBE_FAULT) +check("an incomplete run raises the harness-fault count and exits 2, not 1", + p11.returncode == 0 and "RC=2" in p11.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 index fcc2f90..fbf0880 100644 --- a/wizard-work/null/_probe_mutations.py +++ b/wizard-work/null/_probe_mutations.py @@ -75,6 +75,22 @@ MUTATIONS = [ ("drop the traceback from the claim", "error=last_error,", "error=\"\","), + # --- the four defects found by _hunt_blindspots.py ----------------------- + # Each was measured to slip past the judge BEFORE the matching contract + # (12-15) existed: judge exit 0 on the mutated tree. They are now pinned + # here so a regression re-introducing any of them fails the battery. + ("truthy non-bool accepted as PASS", + "ok = isinstance(value, bool) and value is True", + "ok = bool(value)"), + ("unrelated raise counts as controlled", + "ok = isinstance(exc, expect_exception) if expect_exception else False", + "ok = True if expect_exception else False"), + ("controlled-exception check uses type() not isinstance()", + "ok = isinstance(exc, expect_exception) if expect_exception else False", + "ok = type(exc) is expect_exception if expect_exception else False"), + ("harness fault counter never incremented", + " FAILURES += 1", + " pass # mutation: harness fault silently uncounted"), ] diff --git a/wizard-work/null/verify.py b/wizard-work/null/verify.py index 54f380d..67e6ebe 100644 --- a/wizard-work/null/verify.py +++ b/wizard-work/null/verify.py @@ -1,21 +1,22 @@ #!/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 0 == every stage passed, and the judge demonstrated teeth on 19 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 + 2. _judge.py external contract judge (15 contracts) + 3. _probe_mutations.py judge sensitivity: 19 planted defects, all caught 4. _probe_teeth.py the judge rejects a deliberately lying artifact + 5. _hunt_blindspots.py the open question: no in-scope regression slips 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 +("19/19"), so a new planted defect that slips past the judge fails here rather than silently widening the blind spot. """ import os @@ -33,10 +34,13 @@ STAGES = [ "all contract checks hold"), ("_probe_mutations.py", [sys.executable, os.path.join(HERE, "_probe_mutations.py")], - "15/15 planted defects caught"), + "19/19 planted defects caught"), ("_probe_teeth.py", [sys.executable, os.path.join(HERE, "_probe_teeth.py")], "TEETH OK"), + ("_hunt_blindspots.py", + [sys.executable, os.path.join(HERE, "_hunt_blindspots.py")], + "HUNT OK"), ] @@ -60,8 +64,9 @@ def main() -> int: 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).") + print("VERIFY: 5/5 stages passed " + "(selfcheck 8/8, judge 15 contracts, 19/19 mutation sensitivity, " + "teeth, blind-spot hunt).") return 0