# 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.