From 394de5374a475466dc5bca2cddff5ecffa5c0da7 Mon Sep 17 00:00:00 2001 From: null Date: Tue, 20 Oct 2026 17:38:12 +0000 Subject: [PATCH] null: add proveit.py, a claims runner that re-checks every status it prints --- wizard-work/null/README-proveit.md | 74 ++++++ wizard-work/null/_judge.py | 124 ++++++++++ wizard-work/null/_probe_teeth.py | 43 ++++ wizard-work/null/proveit.py | 365 +++++++++++++++++++++++++++++ 4 files changed, 606 insertions(+) create mode 100644 wizard-work/null/README-proveit.md create mode 100644 wizard-work/null/_judge.py create mode 100644 wizard-work/null/_probe_teeth.py create mode 100644 wizard-work/null/proveit.py diff --git a/wizard-work/null/README-proveit.md b/wizard-work/null/README-proveit.md new file mode 100644 index 0000000..ae5cb43 --- /dev/null +++ b/wizard-work/null/README-proveit.md @@ -0,0 +1,74 @@ +# 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"}`. diff --git a/wizard-work/null/_judge.py b/wizard-work/null/_judge.py new file mode 100644 index 0000000..89bd5f8 --- /dev/null +++ b/wizard-work/null/_judge.py @@ -0,0 +1,124 @@ +#!/usr/bin/env python3 +"""Standalone external judge for proveit.py. + +Deliberately does NOT import proveit as a module. It runs the artifact as a +subprocess and checks the observable contract: exit codes, report contents, +JSON coherence, the honesty properties (no PASS without a real measurement), +and path robustness. Exit 0 == the artifact behaves as claimed. + +The AST claim is checked via the artifact's own --scan-status handle rather +than a hand-rolled scan, so the check is the artifact's own measurement. +""" +import json +import os +import subprocess +import sys +import tempfile + +HERE = os.path.dirname(os.path.abspath(__file__)) +ART = os.path.join(HERE, "proveit.py") +problems = [] + + +def run(*args): + p = subprocess.run([sys.executable, ART, *args], + capture_output=True, text=True) + return p.returncode, p.stdout, p.stderr + + +def check(label, cond): + print((" ok " if cond else " FAIL ") + label) + if not cond: + problems.append(label) + + +# --- contract 1: --selfcheck exits 0 and says OK ----------------------------- +rc, out, err = run("--selfcheck") +check("--selfcheck exit code is 0", rc == 0) +check("--selfcheck reports OK", "SELFCHECK OK" in out) +check("--selfcheck reports 8/8", "8/8" in out) + +# --- contract 2: the demo report contains the known-false claim as FAIL ------ +rc, out, err = run() +check("demo exit code is 1 (it contains a known-false claim)", rc == 1) +check("demo marks the false claim FAIL", "[FAIL] an intentionally false claim" in out) +check("demo marks the raising claim FAIL", "[FAIL] an exception is evidence" in out) +check("demo marks the controlled exception PASS", "[PASS] a controlled exception" in out) +check("demo prints a summary line", "claims PASS" in out) +check("demo has no UNVERIFIED anywhere", "UNVERIFIED" not in out) +check("demo shows 5/7 PASS", "5/7 claims PASS" in out) + +# --- contract 3: --demo-fail is a real failure, not a shrug ------------------ +rc, out, err = run("--demo-fail") +check("--demo-fail exit code is 1", rc == 1) +check("--demo-fail shows the false claim as FAIL", "[FAIL] deliberately false" in out) + +# --- contract 4: JSON mode is valid JSON with a coherent summary ------------- +rc, out, err = run("--json") +try: + data = json.loads(out) + ok_json = True +except Exception as exc: + ok_json = False + print(" json error: %r" % exc) +check("--json emits parseable JSON", ok_json) +if ok_json: + s = data["summary"] + check("json summary total == number of claims", + s["total"] == len(data["claims"])) + check("json summary pass+fail == total", s["pass"] + s["fail"] == s["total"]) + check("json summary pass == 5", s["pass"] == 5) + check("json summary fail == 2", s["fail"] == 2) + check("json harness_faults == 0", s["harness_faults"] == 0) + check("json every claim is measured", + all(c["measured"] for c in data["claims"])) + check("json no claim has status outside {PASS,FAIL}", + all(c["status"] in ("PASS", "FAIL") for c in data["claims"])) + +# --- contract 5: the artifact's own AST scan reports only PASS/FAIL ---------- +rc, out, err = run("--scan-status") +check("--scan-status exit code is 0", rc == 0) +check("--scan-status lists only PASS/FAIL", + out.strip().endswith('["FAIL", "PASS"]')) + +# --- contract 6: path robustness -------------------------------------------- +# The artifact must still find and scan itself when copied elsewhere, which is +# the case that originally broke the self-referential path. +tmpdir = tempfile.mkdtemp(prefix="proveit-robust-") +copied = os.path.join(tmpdir, "proveit.py") +with open(ART, "r", encoding="utf-8") as fh: + src = fh.read() +with open(copied, "w", encoding="utf-8") as fh: + fh.write(src) +p = subprocess.run([sys.executable, copied, "--scan-status"], + capture_output=True, text=True, cwd="/") +check("copied artifact still scans itself correctly (path robustness)", + p.returncode == 0 and p.stdout.strip().endswith('["FAIL", "PASS"]')) +p2 = subprocess.run([sys.executable, copied, "--selfcheck"], + capture_output=True, text=True, cwd="/") +check("copied artifact selfcheck still OK", p2.returncode == 0 and "SELFCHECK OK" in p2.stdout) + +# --- contract 7: the artifact refuses to claim PASS it did not measure ------- +# A predicate that raises must never be reported PASS, even if it "returns" +# truthy on a later retry -- the runner takes the first outcome. +s = ("import sys; sys.path.insert(0, %r); import proveit; " + "s = proveit.Suite('x'); " + "s.make_claim('boom', 'control', lambda: 1/0); " + "print('STATUS=' + s.claims[0].status); " + "sys.exit(0 if s.claims[0].status == 'FAIL' else 1)") % (os.path.dirname(ART),) +with tempfile.NamedTemporaryFile("w", suffix=".py", delete=False) as fh: + fh.write(s) + imp = fh.name +try: + p3 = subprocess.run([sys.executable, imp], capture_output=True, text=True, cwd="/") +finally: + os.unlink(imp) +check("imported artifact reports a raising predicate as FAIL", + p3.returncode == 0 and "STATUS=FAIL" in p3.stdout) + +print() +if problems: + print("JUDGE: %d contract check(s) FAILED" % len(problems)) + sys.exit(1) +print("JUDGE: all contract checks hold.") +sys.exit(0) diff --git a/wizard-work/null/_probe_teeth.py b/wizard-work/null/_probe_teeth.py new file mode 100644 index 0000000..020d12b --- /dev/null +++ b/wizard-work/null/_probe_teeth.py @@ -0,0 +1,43 @@ +#!/usr/bin/env python3 +"""Does the judge actually FAIL when the artifact lies? + +A verdict that cannot go nonzero is a tautology. This plants a real defect -- +rewriting the runner's PASS to UNVERIFIED -- and asserts the judge exits +nonzero. Exit 0 == the judge has teeth. +""" +import os +import subprocess +import sys +import tempfile + +ART = os.path.join(os.path.dirname(os.path.abspath(__file__)), "proveit.py") +JUDGE = os.path.abspath(__file__) + +src = open(ART, encoding="utf-8").read() +# Plant the lie: the status domain check must now see UNVERIFIED. +mutated = src.replace('status="PASS" if (ok and measured) else "FAIL"', + 'status="UNVERIFIED" if (ok and measured) else "FAIL"') +assert mutated != src, "mutation did not apply -- test is invalid" + +tmp = tempfile.mkdtemp(prefix="proveit-mut-") +bad = os.path.join(tmp, "proveit.py") +open(bad, "w", encoding="utf-8").write(mutated) + +# run the judge against the mutated artifact by pointing ART at it +judge_src = open(JUDGE, encoding="utf-8").read().replace( + 'ART = "/root/.hermes/wizard-outputs/null/proveit.py"', 'ART = %r' % bad) +badjudge = os.path.join(tmp, "_judge.py") +open(badjudge, "w", encoding="utf-8").write(judge_src) + +p = subprocess.run([sys.executable, badjudge], capture_output=True, text=True) +print("mutated-artifact judge exit code:", p.returncode) +print("--- judge output (tail) ---") +print("\n".join(p.stdout.strip().splitlines()[-6:])) + +if p.returncode == 0: + print() + print("TOOTHLESS: judge passed a mutated artifact -> verdict is a tautology") + sys.exit(1) +print() +print("TEETH OK: judge rejected the mutated artifact (exit %d)" % p.returncode) +sys.exit(0) diff --git a/wizard-work/null/proveit.py b/wizard-work/null/proveit.py new file mode 100644 index 0000000..4fa1d2d --- /dev/null +++ b/wizard-work/null/proveit.py @@ -0,0 +1,365 @@ +#!/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:]))