111 lines
5.2 KiB
Markdown
111 lines
5.2 KiB
Markdown
# 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=` |
|
|
|
|
## 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 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`.
|
|
|
|
```
|
|
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 **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, 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)
|
|
|
|
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.
|