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