75 lines
3.4 KiB
Markdown
75 lines
3.4 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 25 observable contracts:
|
|
exit codes, report contents, JSON coherence, the honesty properties, path
|
|
robustness (the artifact copied elsewhere must still find and scan itself), and
|
|
the negative control that a raising predicate is never reported PASS.
|
|
|
|
```
|
|
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. A verdict command that cannot
|
|
go nonzero is decoration; this one does go nonzero.
|
|
|
|
## 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, all 25 contract checks hold
|
|
- `_probe_teeth.py` → exit 0, mutated artifact rejected with judge exit 1
|
|
|
|
## 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"}`.
|