344 lines
16 KiB
Python
344 lines
16 KiB
Python
#!/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)
|
|
|
|
# --- contract 8: the `measured` flag is load-bearing, not decorative --------
|
|
# A harness that hardcodes measured=True never increments a call counter, so
|
|
# `repeat=N` is silently ignored. Mutating `measured = ran >= max(1, repeat)`
|
|
# to `measured = True` is invisible to every other contract, so it needs its
|
|
# own: a predicate that must be invoked exactly `repeat` times.
|
|
# The probe is written as a real file (not a one-liner) because a `def` on a
|
|
# single generated line is a SyntaxError -- a defect found the hard way.
|
|
PROBE_CALLS = os.path.join(HERE, "_probe_calls.py")
|
|
with open(PROBE_CALLS, "w", encoding="utf-8") as fh:
|
|
fh.write(
|
|
"import sys\n"
|
|
"sys.path.insert(0, %r)\n"
|
|
"import proveit\n"
|
|
"n = {'c': 0}\n"
|
|
"def f():\n"
|
|
" n['c'] += 1\n"
|
|
" return True\n"
|
|
"s = proveit.Suite('x')\n"
|
|
"c = s.make_claim('repeat control', 'control', f, repeat=3)\n"
|
|
"ok = (n['c'] == 3 and c.calls == 3 and c.measured is True)\n"
|
|
"print('CALLS=' + str(n['c']) + ' MEASURED=' + str(c.measured))\n"
|
|
"sys.exit(0 if ok else 1)\n" % (os.path.dirname(ART),))
|
|
try:
|
|
p4 = subprocess.run([sys.executable, PROBE_CALLS], capture_output=True,
|
|
text=True, cwd="/")
|
|
finally:
|
|
os.unlink(PROBE_CALLS)
|
|
check("repeat=N actually invokes the predicate N times",
|
|
p4.returncode == 0 and "CALLS=3" in p4.stdout)
|
|
|
|
# --- contract 9: a skipped run is never reported as a PASS -------------------
|
|
# If the run loop is neutered the harness must still have run the predicate; a
|
|
# PASS that was never measured is the exact lie this artifact exists to forbid.
|
|
PROBE_RUN = os.path.join(HERE, "_probe_ran.py")
|
|
with open(PROBE_RUN, "w", encoding="utf-8") as fh:
|
|
fh.write(
|
|
"import sys\n"
|
|
"sys.path.insert(0, %r)\n"
|
|
"import proveit\n"
|
|
"n = {'c': 0}\n"
|
|
"def f():\n"
|
|
" n['c'] += 1\n"
|
|
" return True\n"
|
|
"s = proveit.Suite('x')\n"
|
|
"c = s.make_claim('must actually run', 'control', f, repeat=2)\n"
|
|
"ok = (c.status == 'PASS' and n['c'] == 2 and c.measured is True)\n"
|
|
"sys.exit(0 if ok else 1)\n" % (os.path.dirname(ART),))
|
|
try:
|
|
p5 = subprocess.run([sys.executable, PROBE_RUN], capture_output=True,
|
|
text=True, cwd="/")
|
|
finally:
|
|
os.unlink(PROBE_RUN)
|
|
check("predicate is invoked and measured (harness never reports a no-op PASS)",
|
|
p5.returncode == 0)
|
|
|
|
# --- contract 10: the `measured` field is load-bearing ----------------------
|
|
# A predicate that returns False while reporting itself measured must be FAIL,
|
|
# and a predicate that was never run at all must never be PASS. Contract 9
|
|
# pins the positive side (repeat=N really runs N times); this pins the negative
|
|
# side, which is the branch a hardcoded `measured = True` silently corrupts.
|
|
PROBE_MEASURED = os.path.join(HERE, "_probe_measured.py")
|
|
with open(PROBE_MEASURED, "w", encoding="utf-8") as fh:
|
|
fh.write(
|
|
"import sys\n"
|
|
"sys.path.insert(0, %r)\n"
|
|
"import proveit\n"
|
|
"s = proveit.Suite('x')\n"
|
|
"a = s.make_claim('false but measured', 'control', lambda: False)\n"
|
|
"b = s.make_claim('true and measured', 'control', lambda: True)\n"
|
|
"ok = (a.status == 'FAIL' and a.measured is True and a.calls == 1\n"
|
|
" and b.status == 'PASS' and b.measured is True)\n"
|
|
"print('A=' + a.status + ' B=' + b.status)\n"
|
|
"sys.exit(0 if ok else 1)\n" % (os.path.dirname(ART),))
|
|
try:
|
|
p6 = subprocess.run([sys.executable, PROBE_MEASURED], capture_output=True,
|
|
text=True, cwd="/")
|
|
finally:
|
|
os.unlink(PROBE_MEASURED)
|
|
check("a measured False is FAIL and a measured True is PASS (measured is load-bearing)",
|
|
p6.returncode == 0 and "A=FAIL B=PASS" in p6.stdout)
|
|
|
|
# --- contract 11: `measured` must go False when the run loop did not finish --
|
|
# Contracts 8-10 pin the positive side (repeat=N really runs N times; a False
|
|
# predicate is FAIL). None of them can see `measured = True` hardcoded, because
|
|
# in every probe they run the loop to completion and `ran >= max(1, repeat)` is
|
|
# True anyway. The observable difference lives in the *incomplete* run: a
|
|
# predicate that raises on the first of `repeat=3` invocations leaves ran=1 < 3,
|
|
# so the correct code reports measured=False while the hardcoded mutation
|
|
# reports measured=True. _probe_mutations.py plants exactly that mutation and
|
|
# this is the contract that catches it -- before this existed, the sensitivity
|
|
# run reported 14/15 with "measured flag hardcoded true" as a coverage hole.
|
|
PROBE_PARTIAL = os.path.join(HERE, "_probe_partial.py")
|
|
with open(PROBE_PARTIAL, "w", encoding="utf-8") as fh:
|
|
fh.write(
|
|
"import sys\n"
|
|
"sys.path.insert(0, %r)\n"
|
|
"import proveit\n"
|
|
"s = proveit.Suite('x')\n"
|
|
"c = s.make_claim('raises on the first of 3', 'control', lambda: 1/0, repeat=3)\n"
|
|
"ok = (c.calls == 1 and c.measured is False and c.status == 'FAIL'\n"
|
|
" and 'ZeroDivisionError' in c.error)\n"
|
|
"print('CALLS=' + str(c.calls) + ' MEASURED=' + str(c.measured)\n"
|
|
" + ' STATUS=' + c.status)\n"
|
|
"sys.exit(0 if ok else 1)\n" % (os.path.dirname(ART),))
|
|
try:
|
|
p7 = subprocess.run([sys.executable, PROBE_PARTIAL], capture_output=True,
|
|
text=True, cwd="/")
|
|
finally:
|
|
os.unlink(PROBE_PARTIAL)
|
|
check("an incomplete run (raise before repeat is met) is measured=False, not True",
|
|
p7.returncode == 0 and "MEASURED=False" in p7.stdout)
|
|
|
|
# --- contract 12: only a strict True counts as a measurement ---------------
|
|
# `ok = bool(value)` looks equivalent at a glance and is not: a predicate that
|
|
# returns a truthy non-bool ("yes", 1, [1]) is not returning True, so calling it
|
|
# PASS is the exact lie this artifact exists to forbid. No earlier contract ever
|
|
# handed the runner a non-bool, so this regression slipped past all 15 planted
|
|
# defects (measured: judge exit 0 on the mutated tree).
|
|
PROBE_BOOL = os.path.join(HERE, "_probe_bool.py")
|
|
with open(PROBE_BOOL, "w", encoding="utf-8") as fh:
|
|
fh.write(
|
|
"import sys\n"
|
|
"sys.path.insert(0, %r)\n"
|
|
"import proveit\n"
|
|
"s = proveit.Suite('x')\n"
|
|
"a = s.make_claim('truthy string', 'control', lambda: 'yes')\n"
|
|
"b = s.make_claim('truthy int', 'control', lambda: 1)\n"
|
|
"c = s.make_claim('real True', 'control', lambda: True)\n"
|
|
"d = s.make_claim('falsy int', 'control', lambda: 0)\n"
|
|
"ok = (a.status == 'FAIL' and b.status == 'FAIL'\n"
|
|
" and c.status == 'PASS' and d.status == 'FAIL')\n"
|
|
"print('A=' + a.status + ' B=' + b.status + ' C=' + c.status + ' D=' + d.status)\n"
|
|
"sys.exit(0 if ok else 1)\n" % (os.path.dirname(ART),))
|
|
try:
|
|
p8 = subprocess.run([sys.executable, PROBE_BOOL], capture_output=True,
|
|
text=True, cwd="/")
|
|
finally:
|
|
os.unlink(PROBE_BOOL)
|
|
check("only a strict True is PASS; truthy non-bools and falsy values are FAIL",
|
|
p8.returncode == 0 and "A=FAIL B=FAIL C=PASS D=FAIL" in p8.stdout)
|
|
|
|
# --- contract 13: expect_exception does not excuse an unrelated raise -------
|
|
# `ok = True if expect_exception else False` makes ANY raise count as controlled
|
|
# the moment a caller names an expected type. A ZeroDivisionError is not a
|
|
# ValueError, so it must stay FAIL. Measured hole: judge exit 0 when mutated.
|
|
PROBE_UNRELATED = os.path.join(HERE, "_probe_unrelated.py")
|
|
with open(PROBE_UNRELATED, "w", encoding="utf-8") as fh:
|
|
fh.write(
|
|
"import sys\n"
|
|
"sys.path.insert(0, %r)\n"
|
|
"import proveit\n"
|
|
"s = proveit.Suite('x')\n"
|
|
"a = s.make_claim('unrelated raise', 'control', lambda: 1/0,\n"
|
|
" expect_exception=ValueError)\n"
|
|
"b = s.make_claim('expected raise', 'control', lambda: 1/0,\n"
|
|
" expect_exception=ZeroDivisionError)\n"
|
|
"ok = (a.status == 'FAIL' and b.status == 'PASS')\n"
|
|
"print('A=' + a.status + ' B=' + b.status)\n"
|
|
"sys.exit(0 if ok else 1)\n" % (os.path.dirname(ART),))
|
|
try:
|
|
p9 = subprocess.run([sys.executable, PROBE_UNRELATED], capture_output=True,
|
|
text=True, cwd="/")
|
|
finally:
|
|
os.unlink(PROBE_UNRELATED)
|
|
check("a raise outside expect_exception stays FAIL (expect_exception is not a blanket pass)",
|
|
p9.returncode == 0 and "A=FAIL B=PASS" in p9.stdout)
|
|
|
|
# --- contract 14: a subclass of the expected exception is still expected ---
|
|
# `type(exc) is expect_exception` looks stricter and is wrong: isinstance is the
|
|
# correct semantic, so a subclass of the named exception must count as
|
|
# controlled. Measured hole: judge exit 0 when mutated.
|
|
PROBE_SUBCLASS = os.path.join(HERE, "_probe_subclass.py")
|
|
with open(PROBE_SUBCLASS, "w", encoding="utf-8") as fh:
|
|
fh.write(
|
|
"import sys\n"
|
|
"sys.path.insert(0, %r)\n"
|
|
"import proveit\n"
|
|
"class MyZero(ZeroDivisionError):\n"
|
|
" pass\n"
|
|
"s = proveit.Suite('x')\n"
|
|
"a = s.make_claim('subclass raise', 'control',\n"
|
|
" lambda: (_ for _ in ()).throw(MyZero('x')),\n"
|
|
" expect_exception=ZeroDivisionError)\n"
|
|
"ok = (a.status == 'PASS')\n"
|
|
"print('A=' + a.status)\n"
|
|
"sys.exit(0 if ok else 1)\n" % (os.path.dirname(ART),))
|
|
try:
|
|
p10 = subprocess.run([sys.executable, PROBE_SUBCLASS], capture_output=True,
|
|
text=True, cwd="/")
|
|
finally:
|
|
os.unlink(PROBE_SUBCLASS)
|
|
check("a subclass of the expected exception is treated as expected (isinstance, not type)",
|
|
p10.returncode == 0 and "A=PASS" in p10.stdout)
|
|
|
|
# --- contract 15: a harness fault is exit 2, never silently downgraded ------
|
|
# The artifact documents "2 == harness broke" and claims a broken harness cannot
|
|
# silently pass. Removing `FAILURES += 1` is invisible to every claim-level
|
|
# contract (all of them look at status/measured), so only the exit code can see
|
|
# it. Measured hole: judge exit 0 when the counter never increments.
|
|
PROBE_FAULT = os.path.join(HERE, "_probe_fault.py")
|
|
with open(PROBE_FAULT, "w", encoding="utf-8") as fh:
|
|
fh.write(
|
|
"import sys\n"
|
|
"sys.path.insert(0, %r)\n"
|
|
"import proveit\n"
|
|
"s = proveit.Suite('x')\n"
|
|
"s.make_claim('raises on the first of 3', 'control', lambda: 1/0, repeat=3)\n"
|
|
"rc = proveit.report(s)\n"
|
|
"print('RC=' + str(rc) + ' FAULTS=' + str(proveit.FAILURES))\n"
|
|
"sys.exit(0 if (rc == 2 and proveit.FAILURES >= 1) else 1)\n"
|
|
% (os.path.dirname(ART),))
|
|
try:
|
|
p11 = subprocess.run([sys.executable, PROBE_FAULT], capture_output=True,
|
|
text=True, cwd="/")
|
|
finally:
|
|
os.unlink(PROBE_FAULT)
|
|
check("an incomplete run raises the harness-fault count and exits 2, not 1",
|
|
p11.returncode == 0 and "RC=2" in p11.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)
|