#!/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:]))