{"name":"ep414-lean-proof-verifier","lang":"python3","entry":"spec-ep414-proof.py","script":"#!/usr/bin/env python3\n\"\"\"Verifier for EP-414 proof campaign.\nInput: submission directory containing proof.lean (self-contained Lean 4 or mathlib-backed).\nOutput verdict: pass | fail | invalid (printed as JSON {\"verdict\":...,\"reason\":...}).\nChecks:\n 1. proof.lean exists and is valid UTF-8 (else invalid).\n 2. Statement fidelity: the canonical theorem signature must appear verbatim.\n 3. No sorry / admit / native_decide / `axiom ` declarations (else fail).\n 4. Compile with Lean 4 if toolchain available (lean or elan); compile error => fail.\n 5. On success, append `#print axioms ep414` harness and require output axioms subset of standard (propext, Classical.choice, Quot.sound) (else fail).\nEnvironment without any Lean toolchain => invalid (cannot judge).\n\"\"\"\nimport json, os, re, shutil, subprocess, sys, tempfile\n\nCANON_SIG = \"theorem ep414 : ∀ (m n : ℕ), ∃ (i j : ℕ), iterH i m = iterH j n\"\nFORBIDDEN = [r\"\\bsorry\\b\", r\"\\badmit\\b\", r\"\\bnative_decide\\b\", r\"^\\s*axiom\\s\"]\nSTANDARD_AX = {\"propext\", \"Classical.choice\", \"Quot.sound\"}\n\ndef emit(v, r):\n    print(json.dumps({\"verdict\": v, \"reason\": r}, ensure_ascii=False))\n    sys.exit(0 if v == \"pass\" else 1)\n\ndef find_lean():\n    for name in (\"lean\",):\n        p = shutil.which(name)\n        if p: return p\n    elan = shutil.which(\"elan\")\n    if elan:\n        try:\n            out = subprocess.run([elan, \"which\", \"lean\"], capture_output=True, text=True, timeout=60)\n            if out.returncode == 0 and out.stdout.strip(): return out.stdout.strip()\n        except Exception: pass\n    return None\n\ndef main():\n    args = sys.argv[1:]\n    if not args: emit(\"invalid\", \"no submission path given\")\n    sub = args[0]\n    f = os.path.join(sub, \"proof.lean\")\n    if not os.path.isfile(f): emit(\"invalid\", \"proof.lean missing\")\n    try:\n        src = open(f, encoding=\"utf-8\").read()\n    except Exception as e:\n        emit(\"invalid\", f\"unreadable: {e}\")\n    if CANON_SIG not in src:\n        emit(\"fail\", \"statement fidelity: canonical `theorem ep414` signature not found verbatim\")\n    for pat in FORBIDDEN:\n        if re.search(pat, src, flags=re.M):\n            emit(\"fail\", f\"forbidden token matches /{pat}/\")\n    lean = find_lean()\n    if not lean:\n        emit(\"invalid\", \"no Lean 4 toolchain in verifier environment\")\n    with tempfile.TemporaryDirectory() as td:\n        work = os.path.join(td, \"proof.lean\")\n        open(work, \"w\", encoding=\"utf-8\").write(src + \"\\n#print axioms ep414\\n\")\n        try:\n            r = subprocess.run([lean, work], capture_output=True, text=True, timeout=1800)\n        except subprocess.TimeoutExpired:\n            emit(\"fail\", \"lean compile timeout (>1800s)\")\n        out = (r.stdout or \"\") + (r.stderr or \"\")\n        if r.returncode != 0:\n            emit(\"fail\", \"lean compile error: \" + out[-800:])\n        m = re.search(r\"'ep414' does not depend on any axioms\", out)\n        if m:\n            emit(\"pass\", \"compiled; no axioms used\")\n        am = re.search(r\"axioms? ([^.]+)\", out)\n        if am:\n            used = {a.strip().rstrip(\",\") for a in am.group(1).split(\",\")}\n            bad = used - STANDARD_AX\n            if bad:\n                emit(\"fail\", f\"non-standard axioms: {sorted(bad)}\")\n            emit(\"pass\", f\"compiled; axioms={sorted(used & STANDARD_AX)}\")\n        emit(\"fail\", \"compile ok but axioms report unparsable: \" + out[-300:])\n\nif __name__ == \"__main__\":\n    main()\n","input":"A submission directory containing proof.lean (self-contained Lean 4 proving theorem ep414 as defined in proposition pin pin://429f3fd5c14f9f815db39491ea4625436570f7caf9ac5c51ba3ea2f548f1d06bi0)","output":"JSON {verdict: pass|fail|invalid, reason} printed to stdout; exit 0 iff pass","validation":{"null_tolerance":true,"enumeration_closure":{"closure":"harness self-check fixtures: (a) a valid trivial Lean file `theorem ep414 : ∀ (m n : ℕ), ∃ (i j : ℕ), iterH i m = iterH j n := by simp` style stub that compiles-with-sorry is expected FAIL; (b) fixture pipeline exercised on the two failure classes (missing signature, sorry token) with deterministic verdicts","selfCheckCount":3},"proposition_fidelity":{"artifact":"pin://429f3fd5c14f9f815db39491ea4625436570f7caf9ac5c51ba3ea2f548f1d06bi0","role":"correspondence artifact: canonical natural-language statement, source citations, and the normative Lean signature of theorem ep414 that submissions must preserve verbatim","independence":"authored and pinned separately from this spec before spec publication; spec references it read-only"}}}