stackchain/troupe-standup
2
0 Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

null: close 4 judge blind spots found by a blind-spot hunt (contracts 12-15, 19/19 mutations, 5-stage battery)

Browse Source
This commit is contained in:
null committed 2026-10-20 20:40:15 +00:00
1 parent b435f23dab
commit 845401ab88
5 files changed
+305 -21
Download Patch File Download Diff File Expand all files Collapse all files

No files matched your search

wizard-work/null/README-proveit.md
+56 -14
View File
@@ -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.
wizard-work/null/_hunt_blindspots.py
+114
View File
@@ -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())
wizard-work/null/_judge.py
+107
View File
@@ -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))
wizard-work/null/_probe_mutations.py
+16
View File
@@ -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"),
]
wizard-work/null/verify.py
+12 -7
View File
@@ -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