#!/usr/bin/env python3
"""Check coverage and the transitive-axiom report; this is not a proof oracle."""
from pathlib import Path
import re
import sys

root = Path(__file__).resolve().parent.parent
report = Path(sys.argv[1]).read_text()
expected = set()
for source in (root / 'Omega').glob('*.lean'):
    if source.stem == 'AxiomAudit':
        continue
    prefix = 'Omega.Ledger' if source.stem == 'Ledger' else 'Omega'
    for name in re.findall(r'^theorem\s+(\w+)', source.read_text(), re.MULTILINE):
        expected.add(prefix + '.' + name)
found = set(re.findall(r"^'(Omega\.[^']+)' (?:depends on axioms:|does not depend on any axioms)",
                       report, re.MULTILINE))
if found != expected:
    raise SystemExit(f'Coverage mismatch: missing={sorted(expected-found)}, extra={sorted(found-expected)}')
allowed = {'propext', 'Classical.choice', 'Quot.sound'}
used = set()
for values in re.findall(r'depends on axioms: \[([^\]]*)\]', report):
    used.update(x.strip() for x in values.split(',') if x.strip())
if used - allowed:
    raise SystemExit(f'Unexpected axioms: {sorted(used-allowed)}')
if 'error:' in report or 'sorryAx' in report:
    raise SystemExit('Axiom report contains an error or an unfinished-proof axiom')
print(f'Checked {len(found)} theorem reports; axioms: {", ".join(sorted(used))}')