troupe-standup/wizard-work/null/README-proveit.md

proveit.py — a runner that re-checks every claim it prints

Lane: Codeforge. Purpose: make the evidence law mechanical instead of rhetorical.

The law this artifact serves: "the executor said done" is not "a test passed", and "prepared" is not "observed". So this runner has no prose-only claim path. A status string is only ever written by Suite.make_claim(), which invokes the predicate, records the outcome, and derives PASS/FAIL from what actually happened. There is no other place in the source that assigns to status, and no code path that can emit UNVERIFIED — that word is not assignable anywhere, which is checked structurally (AST), not by substring.

What is measured, not asserted

claim	how it is measured
file exists and is non-empty	open().read() length
interpreter is 3.11+	sys.version_info at runtime
sqrt(2)**2 is 2 to 1e-12	math
predicate really ran 3 times	repeat=3, call counter
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

python3 proveit.py            # demo report; exits 1 (contains known-false controls)
python3 proveit.py --json     # same report, machine-readable
python3 proveit.py --demo-fail# a single-claim failure, so you see what failure prints
python3 proveit.py --selfcheck# meta-test: plants bad claims, asserts each is caught
python3 proveit.py --scan-status  # the status literals this source can assign

Exit codes: 0 all claims PASS, 1 at least one claim not PASS, 2 harness broke.

The judge (external, does not import proveit)

_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

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.

_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, 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 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 ("19/19"), 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, 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
• _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)

1. The first self-check asserted "no status="UNVERIFIED" substring" — but that literal appears in the file's own docstring. The check was unsound; it was rewritten as a structural AST scan.
2. HERE = __file__.rsplit("/", 1)[0] broke when the artifact was imported from another directory, so the self-scan silently found nothing. Fixed to os.path.dirname(os.path.abspath(__file__)); the judge now covers this with a copy-elsewhere test.
3. The AST scan only looked for bare ast.Constant, so it missed the FAIL 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.
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.