"""Independent check of a Claude run: each proof recompiles, proves exactly the task statement,
assumes nothing beyond excluded middle, and no prompt contains a line of the published proofs.
Usage: python3 verify20.py proofs_dir runs_dir [rocq-compile-command]"""
import json, re, subprocess, tempfile, sys, glob, os
sys.path.insert(0, '../htps'); import heldout20
pdir, rdir = sys.argv[1], sys.argv[2]
hammer = len(sys.argv) > 3
from rocq_env import HAMMER_BIN, HAMMER_ENV
bad, rows = [], []
for t, stmt in heldout20.TASKS.items():
    f = f'{pdir}/{t}.v'
    if not os.path.exists(f): bad.append((t, 'no proof')); continue
    src = open(f).read()
    body = src[src.index('Definition MP012'):]; body = body[body.index('\n', body.index('a giver exists')):]
    if re.search(r'\b(Admitted|admit|Axiom|Parameter|Hypothesis|Variable|Conjecture|give_up)\b', body): bad.append((t, 'forbidden'))
    top = re.search(r'Print Assumptions (\w+)\.', body).group(1)
    m = re.search(rf'Lemma {top} : (.*?)\.\nProof\.', body, re.S)
    if ' '.join(m.group(1).split()) != ' '.join(stmt.split()): bad.append((t, 'statement differs'))
    with tempfile.TemporaryDirectory() as d:
        open(f'{d}/F.v', 'w').write(src)
        cmd = [HAMMER_BIN + '/rocq', 'compile', '-q', 'F.v'] if hammer else ['coqc', '-q', 'F.v']
        r = subprocess.run(cmd, cwd=d, capture_output=True, text=True, timeout=900, env=HAMMER_ENV if hammer else None)
    out = r.stdout + r.stderr
    ax = re.findall(r'^(\S+) :', out.split('Axioms:')[-1], re.M) if 'Axioms:' in out else []
    if r.returncode != 0 or not set(ax) <= {'classic'}: bad.append((t, 'compile/axioms', r.returncode, ax))
    rows.append((t, r.returncode == 0, ax, body.count('\nLemma ')))
pub = set()
for f in glob.glob('../../app/static/research/dalil-al-*/**/rocq/*.v', recursive=True):
    for blk in re.findall(r'Proof\.(.*?)(?:Qed|Defined)\.', open(f).read(), re.S):
        pub |= {l.strip() for l in blk.split('\n') if len(l.strip()) > 25}
calls, leaks, models = 0, 0, set()
for f in glob.glob(f'{rdir}/*.jsonl'):
    for l in open(f):
        d = json.loads(l)
        if d.get('kind') == 'model_call':
            calls += 1; models.update(d.get('model') or [])
            leaks += sum(1 for line in pub if line in d['prompt'])
for r in rows: print(f'{r[0]:40s} compiles={r[1]} axioms={r[2] or "none"} lemmas={r[3]}')
print('PROBLEMS:', bad); print('model calls', calls, 'models', models, 'published proof lines', len(pub), 'leaks', leaks)