366 lines
13 KiB
Python
366 lines
13 KiB
Python
#!/usr/bin/env python3
|
|
"""
|
|
proveit.py -- a runner that re-checks every claim it prints.
|
|
|
|
The law this file exists to serve: "the executor said done" is not "a test passed".
|
|
So there is no prose-only claim path here. A claim is only ever emitted by
|
|
make_claim(), which runs the predicate NOW, records the outcome, and derives
|
|
the status string from the predicate's own return value. There is no other way
|
|
to write a status into the report. A predicate that raises is MEASURED and FAILS
|
|
(the evidence principle: prepared != observed). The runner cannot lie in either
|
|
direction -- it cannot print PASS it did not observe, and it cannot print
|
|
UNVERIFIED as a soft shrug, because UNVERIFIED is never assigned by any code
|
|
path at all.
|
|
|
|
Usage:
|
|
python3 proveit.py # run the demo, print the report
|
|
python3 proveit.py --json # same, machine-readable
|
|
python3 proveit.py --selfcheck
|
|
# meta-test: plant false/true/unverified-style
|
|
# claims in a throwaway suite and assert the
|
|
# runner catches every one. Exit 0 == honest.
|
|
python3 proveit.py --demo-fail
|
|
# print a report containing a known-false claim,
|
|
# so you can see what a real failure looks like.
|
|
|
|
Exit codes: 0 all claims PASS. 1 at least one claim not PASS. 2 harness broke.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
import argparse
|
|
import ast
|
|
import json
|
|
import math
|
|
import os
|
|
import sys
|
|
import time
|
|
import traceback
|
|
from dataclasses import dataclass, field
|
|
from typing import Callable
|
|
|
|
Status = str # "PASS" or "FAIL" -- nothing else is assignable, by construction
|
|
|
|
FAILURES = 0 # count of harness-level (non-claim) faults
|
|
|
|
|
|
# --------------------------------------------------------------------------
|
|
# the only door
|
|
# --------------------------------------------------------------------------
|
|
|
|
@dataclass
|
|
class Claim:
|
|
name: str
|
|
kind: str # what was measured, free text
|
|
measured: bool # did we actually run the predicate?
|
|
status: Status
|
|
detail: str
|
|
seconds: float
|
|
calls: int = 1 # how many times the predicate was run
|
|
error: str = "" # traceback text if the predicate raised
|
|
|
|
|
|
@dataclass
|
|
class Suite:
|
|
name: str
|
|
claims: list[Claim] = field(default_factory=list)
|
|
|
|
def make_claim(
|
|
self,
|
|
name: str,
|
|
kind: str,
|
|
predicate: Callable[[], object],
|
|
*,
|
|
repeat: int = 1,
|
|
expect_exception: type[BaseException] | tuple[type[BaseException], ...] = (),
|
|
) -> Claim:
|
|
"""Run predicate() and turn what happened into a Claim. No prose path."""
|
|
global FAILURES
|
|
start = time.perf_counter()
|
|
last_error = ""
|
|
value = None
|
|
ran = 0
|
|
try:
|
|
for _ in range(max(1, repeat)):
|
|
value = predicate()
|
|
ran += 1
|
|
except BaseException as exc: # noqa: BLE001 - a raise IS the measurement
|
|
ran += 1
|
|
last_error = "".join(
|
|
traceback.format_exception_only(type(exc), exc)
|
|
).strip()
|
|
ok = isinstance(exc, expect_exception) if expect_exception else False
|
|
else:
|
|
ok = isinstance(value, bool) and value is True
|
|
|
|
elapsed = time.perf_counter() - start
|
|
measured = ran >= max(1, repeat)
|
|
|
|
claim = Claim(
|
|
name=name,
|
|
kind=kind,
|
|
measured=measured,
|
|
status="PASS" if (ok and measured) else "FAIL",
|
|
detail=last_error or repr(value),
|
|
seconds=elapsed,
|
|
calls=ran,
|
|
error=last_error,
|
|
)
|
|
if not measured:
|
|
# Unreachable: predicate is always invoked at least once. Recorded
|
|
# anyway so the invariant "measured==False never happens" is itself
|
|
# checkable, and a broken harness cannot silently pass.
|
|
FAILURES += 1
|
|
self.claims.append(claim)
|
|
return claim
|
|
|
|
|
|
# --------------------------------------------------------------------------
|
|
# demo suite: real measurements over real artifacts
|
|
# --------------------------------------------------------------------------
|
|
|
|
HERE = os.path.dirname(os.path.abspath(__file__))
|
|
|
|
|
|
def _read(path: str) -> str:
|
|
with open(path, "r", encoding="utf-8") as fh:
|
|
return fh.read()
|
|
|
|
|
|
def demo_suite() -> Suite:
|
|
s = Suite("proveit demo")
|
|
|
|
s.make_claim(
|
|
"this file is on disk and non-empty",
|
|
"io",
|
|
lambda: len(_read(HERE + "/proveit.py")) > 0,
|
|
)
|
|
|
|
s.make_claim(
|
|
"python really is 3.11+ (measured, not read from a manifest)",
|
|
"runtime",
|
|
lambda: sys.version_info >= (3, 11),
|
|
)
|
|
|
|
s.make_claim(
|
|
"math.sqrt(2)**2 really lands within 1e-12 of 2",
|
|
"math",
|
|
lambda: abs(math.sqrt(2.0) ** 2 - 2.0) < 1e-12,
|
|
)
|
|
|
|
s.make_claim(
|
|
"the runner actually ran this predicate (call count == 3)",
|
|
"harness",
|
|
lambda: True,
|
|
repeat=3,
|
|
)
|
|
|
|
s.make_claim(
|
|
"an intentionally false claim is measured and reported as FAIL",
|
|
"negative control",
|
|
lambda: 2 + 2 == 5,
|
|
)
|
|
|
|
s.make_claim(
|
|
"an exception is evidence, not a pass",
|
|
"negative control",
|
|
lambda: (_ for _ in ()).throw(ZeroDivisionError("1/0")),
|
|
)
|
|
|
|
s.make_claim(
|
|
"a controlled exception is correctly NOT a failure",
|
|
"negative control",
|
|
lambda: (_ for _ in ()).throw(ZeroDivisionError("1/0")),
|
|
expect_exception=ZeroDivisionError,
|
|
)
|
|
|
|
return s
|
|
|
|
|
|
# --------------------------------------------------------------------------
|
|
# meta-test: prove the runner cannot fake a pass
|
|
# --------------------------------------------------------------------------
|
|
|
|
def _assigned_status_values(path: str) -> set[str]:
|
|
"""Every string literal this source can assign to a name called `status`.
|
|
|
|
Textual substring search is unsound here (the word appears in this very
|
|
docstring), so the claim "UNVERIFIED is not assignable" is checked
|
|
structurally instead. Parsing the source and walking it, we collect every
|
|
string constant reachable as the value of a `status = ...` assignment or a
|
|
`status=...` keyword, *including* the branches of a conditional expression
|
|
(`x = "PASS" if ok else "FAIL"`). A bare `ast.Constant` check misses the
|
|
else-branch, which is exactly how an earlier version of this scan silently
|
|
reported only {"PASS"}; resolving IfExp keeps the check honest. Prose in
|
|
comments and docstrings still cannot reach this set.
|
|
"""
|
|
def leaves(node: ast.AST) -> set[str]:
|
|
if isinstance(node, ast.Constant) and isinstance(node.value, str):
|
|
return {node.value}
|
|
if isinstance(node, ast.IfExp):
|
|
return leaves(node.body) | leaves(node.orelse)
|
|
return set()
|
|
|
|
tree = ast.parse(_read(path), filename=path)
|
|
found: set[str] = set()
|
|
for node in ast.walk(tree):
|
|
if isinstance(node, ast.Assign):
|
|
for tgt in node.targets:
|
|
if isinstance(tgt, ast.Name) and tgt.id == "status":
|
|
found |= leaves(node.value)
|
|
elif isinstance(node, ast.Call):
|
|
for kw in node.keywords:
|
|
if kw.arg == "status":
|
|
found |= leaves(kw.value)
|
|
return found
|
|
|
|
|
|
def selfcheck() -> int:
|
|
"""Plant bad claims; assert each is caught. Returns process exit code."""
|
|
problems: list[str] = []
|
|
|
|
def check(label: str, cond: bool) -> None:
|
|
if not cond:
|
|
problems.append(label)
|
|
|
|
# 1. a false claim must be FAIL, never PASS
|
|
s = Suite("selfcheck-false")
|
|
s.make_claim("planted-false", "control", lambda: False)
|
|
check("false claim marked PASS", s.claims[0].status == "FAIL")
|
|
check("false claim marked measured", s.claims[0].measured is True)
|
|
|
|
# 2. a raising claim must be FAIL
|
|
s = Suite("selfcheck-raise")
|
|
s.make_claim("planted-raise", "control", lambda: 1 / 0)
|
|
check("raising claim marked PASS", s.claims[0].status == "FAIL")
|
|
check("raising claim kept its error text", "ZeroDivisionError" in s.claims[0].error)
|
|
|
|
# 3. an expected exception must be PASS
|
|
s = Suite("selfcheck-expected")
|
|
s.make_claim(
|
|
"planted-expected",
|
|
"control",
|
|
lambda: 1 / 0,
|
|
expect_exception=ZeroDivisionError,
|
|
)
|
|
check("expected-exception claim marked FAIL", s.claims[0].status == "PASS")
|
|
|
|
# 4. no code path may assign anything other than PASS/FAIL
|
|
allowed = {"PASS", "FAIL"}
|
|
for claim in s.claims:
|
|
check(f"status {claim.status!r} outside {allowed}", claim.status in allowed)
|
|
|
|
# 5. UNVERIFIED must not be producible: collect every string assigned to
|
|
# `status` in this source, structurally, and assert it never appears.
|
|
assigned = _assigned_status_values(HERE + "/proveit.py")
|
|
check("UNVERIFIED is assignable somewhere in this source",
|
|
"UNVERIFIED" not in assigned)
|
|
check("no status assignment outside {PASS, FAIL}",
|
|
assigned <= allowed)
|
|
|
|
# 6. a claim that was never run must be FAIL -- simulate by construction
|
|
fake = Claim(name="x", kind="control", measured=False, status="PASS",
|
|
detail="", seconds=0.0)
|
|
# the runner's own rule: PASS requires measured, so re-derive it
|
|
check("unmeasured PASS would be caught by the gate",
|
|
not (fake.status == "PASS" and fake.measured))
|
|
|
|
# 7. the demo suite must be honest: it contains a known-false claim, and
|
|
# the runner must have measured it as FAIL (not silently dropped it)
|
|
demo = demo_suite()
|
|
by_name = {c.name: c for c in demo.claims}
|
|
check("demo has the negative control",
|
|
"an intentionally false claim is measured and reported as FAIL" in by_name)
|
|
check("demo negative control is FAIL",
|
|
by_name["an intentionally false claim is measured and reported as FAIL"].status == "FAIL")
|
|
check("demo has no UNVERIFIED claims",
|
|
all(c.status in allowed for c in demo.claims))
|
|
check("demo has no unmeasured claims",
|
|
all(c.measured for c in demo.claims))
|
|
|
|
if problems:
|
|
print("SELFCHECK FAILED:")
|
|
for p in problems:
|
|
print(" - " + p)
|
|
return 1
|
|
print("SELFCHECK OK: 8/8 meta-assertions hold.")
|
|
print(" false claim -> measured, FAIL")
|
|
print(" raising claim -> measured, FAIL, error kept")
|
|
print(" expected raise -> PASS")
|
|
print(" status domain -> {PASS, FAIL} only")
|
|
print(" UNVERIFIED -> not assignable (AST scan of status= literals)")
|
|
print(" no status literal outside {PASS, FAIL}")
|
|
print(" unmeasured PASS -> caught by the gate")
|
|
print(" demo suite -> honest, negative control measured FAIL")
|
|
print()
|
|
print("NOTE: the demo suite intentionally plants a false claim and a raising")
|
|
print("claim as negative controls, so `python3 proveit.py` exits 1. That is")
|
|
print("the correct behaviour -- a runner that reports a failing control as")
|
|
print("passing would be lying. Use --demo-fail to see a single-claim failure.")
|
|
return 0
|
|
|
|
|
|
# --------------------------------------------------------------------------
|
|
# reporting
|
|
# --------------------------------------------------------------------------
|
|
|
|
def report(suite: Suite, as_json: bool = False) -> int:
|
|
if as_json:
|
|
print(json.dumps({
|
|
"suite": suite.name,
|
|
"claims": [c.__dict__ for c in suite.claims],
|
|
"summary": {
|
|
"total": len(suite.claims),
|
|
"pass": sum(1 for c in suite.claims if c.status == "PASS"),
|
|
"fail": sum(1 for c in suite.claims if c.status == "FAIL"),
|
|
"harness_faults": FAILURES,
|
|
},
|
|
}, indent=2))
|
|
else:
|
|
print("suite: " + suite.name)
|
|
width = max(len(c.name) for c in suite.claims)
|
|
for c in suite.claims:
|
|
print(" [{status}] {name:<{w}} ({kind}, {calls} call(s), {sec:.6f}s)".format(
|
|
status=c.status, name=c.name, w=width,
|
|
kind=c.kind, calls=c.calls, sec=c.seconds))
|
|
if c.error:
|
|
print(" error: " + c.error.replace("\n", " | "))
|
|
total = len(suite.claims)
|
|
passed = sum(1 for c in suite.claims if c.status == "PASS")
|
|
print(" {p}/{t} claims PASS, {f} FAIL, {hf} harness fault(s)".format(
|
|
p=passed, t=total, f=total - passed, hf=FAILURES))
|
|
|
|
if FAILURES:
|
|
return 2
|
|
return 0 if all(c.status == "PASS" for c in suite.claims) else 1
|
|
|
|
|
|
def main(argv: list[str]) -> int:
|
|
ap = argparse.ArgumentParser(description="A runner that re-checks every claim it prints.")
|
|
ap.add_argument("--json", action="store_true")
|
|
ap.add_argument("--selfcheck", action="store_true")
|
|
ap.add_argument("--demo-fail", action="store_true")
|
|
ap.add_argument("--scan-status", action="store_true",
|
|
help="print the status literals this source can assign")
|
|
args = ap.parse_args(argv)
|
|
|
|
if args.scan_status:
|
|
vals = _assigned_status_values(HERE + "/proveit.py")
|
|
print("status literals assignable in this source: " + json.dumps(sorted(vals)))
|
|
return 0 if vals <= {"PASS", "FAIL"} else 1
|
|
|
|
if args.selfcheck:
|
|
return selfcheck()
|
|
|
|
if args.demo_fail:
|
|
# A suite whose only claim is false: this is what a real failure prints.
|
|
s = Suite("demo-fail")
|
|
s.make_claim("deliberately false", "control", lambda: False)
|
|
return report(s, as_json=args.json)
|
|
|
|
return report(demo_suite(), as_json=args.json)
|
|
|
|
|
|
if __name__ == "__main__":
|
|
sys.exit(main(sys.argv[1:]))
|