237 lines
11 KiB
Python
237 lines
11 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)
|
|
|
|
print()
|
|
if problems:
|
|
print("JUDGE: %d contract check(s) FAILED" % len(problems))
|
|
sys.exit(1)
|
|
print("JUDGE: all contract checks hold.")
|
|
sys.exit(0)
|