"""compare.py: check a run of this supplement against expected/ and against the numbers stated in the paper.

Usage: python3 compare.py <expected_dir> <out_dir>
Text outputs are compared line by line, ignoring blank lines and lines that start with '#' (environment headers).
JSON outputs are compared as parsed JSON, value for value. Then every numerical statement of the paper is checked in the FRESH outputs,
by parsing the printed enclosures and comparing them with the paper's displayed bounds as exact decimals. Exit status 0 only if all pass.
"""
import json, math, re, sys
from fractions import Fraction as F
from pathlib import Path

exp_dir, out_dir = Path(sys.argv[1]), Path(sys.argv[2])
ok_all = True

def lines(p):
    return [l.rstrip() for l in p.read_text(errors='replace').splitlines() if l.strip() and not l.startswith('#')]

def jnorm(v):
    """Parsed JSON without timing fields (audit/t2v6/audit_v6.json records its own elapsed_seconds)."""
    if isinstance(v, dict):
        return {k: jnorm(x) for k, x in v.items() if k != 'elapsed_seconds'}
    if isinstance(v, list):
        return [jnorm(x) for x in v]
    return v

print('== exact comparison with expected/')
for e in sorted(p for p in exp_dir.rglob('*') if p.is_file()):
    rel = e.relative_to(exp_dir)
    o = out_dir / (rel.with_suffix('') if rel.name.endswith('.out.txt') else rel)  # stored text outputs carry an extra .txt
    if not o.exists():
        print(f'MISSING   {rel}'); ok_all = False; continue
    same = (jnorm(json.loads(e.read_text())) == jnorm(json.loads(o.read_text()))) if e.suffix == '.json' else (lines(e) == lines(o))
    print(f"{'SAME     ' if same else 'DIFFERS  '} {rel}")
    ok_all &= same

print('== the paper\'s numerical statements, read from the fresh outputs')

def text(path):
    p = out_dir / path
    return p.read_text(errors='replace') if p.exists() else ''

def line_with(path, *needles):
    for l in text(path).splitlines():
        if all(n in l for n in needles):
            return l
    return None

def ball(s):
    """[m +/- r] -> (m - r, m + r); [a, b] -> (a, b); exact Fractions."""
    t = s.strip().strip('[]')
    if '+/-' in t:
        m, r = (x.strip() for x in t.split('+/-'))
        return F(m) - F(r), F(m) + F(r)
    a, b = (x.strip() for x in t.split(','))
    return F(a), F(b)

def enclosure_after(l, label):
    m = re.search(re.escape(label) + r'\s*(\[[^\]]*\])', l)
    return ball(m.group(1)) if m else None

def check(what, cond):
    global ok_all
    print(f"{'PASS     ' if cond else 'FAIL     '} {what}")
    ok_all &= bool(cond)

def safe(fn, what):
    try:
        check(what, fn())
    except Exception as ex:
        check(f'{what}  [error: {ex}]', False)

# Lemma 7 (C3num), delta = 1/5: the author's enclosures of the left side, and the second implementation's majorants
def c3s(LX, K):
    l = line_with('author/cert_C3s_v7.out', f'exp({LX})], K = {K}:')
    a, b = re.search(r'left side in \[([0-9.]+), ([0-9.]+)\]', l).groups()
    return F(a), F(b), l
G0p = F('0.2774978')
safe(lambda: c3s(1800, 18)[1] <= F('0.209801') and 'HOLDS' in c3s(1800, 18)[2], "Lemma 7: (e^1800, 18) < 0.209801 [author]")
safe(lambda: c3s(1800, 17)[0] > F('0.5646') and 'FAILS' in c3s(1800, 17)[2], "Lemma 7: (e^1800, 17) > 0.5646 [author, lower end]")
safe(lambda: c3s(350, 14)[1] <= F('0.149761') and 'HOLDS' in c3s(350, 14)[2], "Lemma 7: (e^350, 14) < 0.149761 [author]")
safe(lambda: c3s(62, 9)[1] < G0p and 'HOLDS' in c3s(62, 9)[2], "Lemma 7: (e^62, 9) holds [author]")
# The remark after the proof of Theorem 1: at (X_2', 18), delta = 1/5, the left side is > 0.628287, so the k-sum (1 - delta)(left side
# - L_low e^{-delta L_low}) exceeds 0.4961; 0.0081538878 > L_low e^{-L_low/5} = 0.00815388779878..., L_low = log(4e18)
safe(lambda: c3s('2736.86', 18)[0] >= F('0.628287') and 'FAILS' in c3s('2736.86', 18)[2] and F(4, 5) * (c3s('2736.86', 18)[0] - F('0.0081538878')) > F('0.4961'), "Remark 17: (X2', 18) printed lower enclosure >= 0.628287, k-sum > 0.4961 [author]")
# Remark 26: plain (C3) at (e^73, 8), delta = 1/5
safe(lambda: c3s(73, 8)[0] > F('1.0035') and c3s(73, 8)[1] < F('1.0045'), "Remark 26: plain (C3) at (e^73, 8), delta = 1/5, rounds to 1.004 [author]")
def c3b(path, K):
    l = line_with(path, f'K = {K}:', 'CERTIFIED')
    return enclosure_after(l, 'majorant enclosure')[1]
safe(lambda: c3b('second/cert_C3_e1800.out', 18) < F('0.209801'), "Lemma 7: (e^1800, 18) < 0.209801 [second, Arb]")
safe(lambda: c3b('second/cert_C3_e350.out', 14) < F('0.149761'), "Lemma 7: (e^350, 14) < 0.149761 [second, Arb]")
safe(lambda: c3b('second/cert_C3_e62.out', 9) < G0p, "Lemma 7: (e^62, 9) holds [second, Arb]")
def grh(w, K):
    l = line_with('third/t2_check/c3_grh.out', f'w={w},', f'K={K},')
    return enclosure_after(l, 'left-side enclosure'), enclosure_after(l, 'right-side enclosure'), l
safe(lambda: grh(11, 9)[0][1] <= F('0.241386') and 'CERTIFIED' in grh(11, 9)[2], "Lemma 7: (e^62, 9) < 0.241386 [third, c3_grh w = 11]")
# Lemma 10 (C4num) and the K = 17 remark
def c4(K):
    l = line_with('second/cert_C4.out', f'K={K}:')
    return enclosure_after(l, 'upper-majorant enclosure'), enclosure_after(l, 'target enclosure'), l
safe(lambda: c4(18)[0][1] < F('0.406804') and c4(18)[1][0] > F('0.986659'), "Lemma 10: C4 at K = 18 < 0.406804 vs > 0.986659")
safe(lambda: abs(c4(17)[0][1] - F('1.07')) < F('0.01'), "Remark 17: C4 at K = 17 about 1.07 (not established)")
# Lemma 16 (S4num): the certificate of record (third) and the second implementation; the K = 17 remark
def s3p():
    l = line_with('third/t2_check/cert_S3P_K18.out', 'H=400:')
    return enclosure_after(l, 'low-piece upper-majorant enclosure'), enclosure_after(l, 'high-piece upper-majorant enclosure'), l
safe(lambda: s3p()[0][1] < F('1.34e-6') and s3p()[1][1] < F('0.4481') and 'CERTIFIED' in s3p()[2], "Lemma 16: < 1.34e-6 and < 0.4481 [third, record, H = 400]")
def s4(K, piece):
    l = line_with('second/cert_S4_H400.out', f'K={K} on {piece}')
    return enclosure_after(l, 'upper-majorant enclosure'), l
safe(lambda: s4(18, '[L0, 3000]')[0][1] < F('1.34e-6') and s4(18, '[3000, L3]')[0][1] < 1, "Lemma 16: K = 18 both pieces < 1 [second]")
safe(lambda: abs(s4(17, '[3000, L3]')[0][1] - F('14.3')) < F('0.1'), "Remark 17: S4 at K = 17, second piece about 14.3 (not established)")
# Theorem 2 grids
def grid(path, n):
    l = line_with(path, f'{n} intervals, failures 0; coverage asserted; least relative margin')
    return F(l.rsplit(' ', 1)[1]) if l else None
safe(lambda: grid('second/cert_qrhB3_K14_low.out', 501) > F('0.9030'), "Theorem 2: [350, 51046], 501 intervals, margin 0.9030...")
safe(lambda: grid('second/cert_qrhB3p_K14_top.out', 449) > F('0.4237'), "Theorem 2: [51046, 159011874857757], 449 intervals, margin 0.4237...")
def gridrows(path):
    return json.loads((out_dir / path).read_text())['rows']   # rows [L1, L2, M, lambda, margin, ok]; z1 = exp(L1/M)
LOW, TOP = 'second/cert_qrhB3_K14_350_51046.json', 'second/cert_qrhB3p_K14_51046_159011874857757.json'
safe(lambda: len(gridrows(LOW)) == 501 and max(r[2] for r in gridrows(LOW)) <= 48 and min(r[0] / r[2] for r in gridrows(LOW)) > math.log(10493), "Theorem 2: low grid z1 > 10493 with M <= 48 (a descriptive minimum, in binary64; the certificate asserts z1 > 10372 in Arb)")
safe(lambda: len(gridrows(TOP)) == 449 and max(r[2] for r in gridrows(TOP)) <= 32 and min(F(r[0]) / r[2] for r in gridrows(TOP)) >= F('1595.1875'), "Theorem 2: top grid log z1 >= 1595.1875 with M <= 32")
# Lemma 23 (C3GRHnum) and Remark 26
safe(lambda: grh(19, 9)[0][1] <= F('0.147535') and grh(19, 9)[1][0] > F('0.2281295') and 'CERTIFIED' in grh(19, 9)[2], "Lemma 23: w = 19 < 0.147535 vs > 0.2281295")
safe(lambda: grh(23, 9)[0][1] <= F('0.139061') and grh(23, 9)[1][0] > F('0.2171299') and 'CERTIFIED' in grh(23, 9)[2], "Lemma 23: w = 23 < 0.139061 vs > 0.2171299")
safe(lambda: grh(29, 8)[0][0] > F('0.363') and grh(29, 8)[1][1] < F('0.189'), "Remark 26: w = 29, K = 8: > 0.363 vs < 0.189")
# Lemma 25 (GRHsievenum) and Remark 26
def sieve(K, P):
    l = line_with('third/t2_check/cert_grh_sieve.out', f'K={K}, presieve={P}:')
    return enclosure_after(l, 'computed upper-bound enclosure'), l
safe(lambda: sieve(9, 'False')[0][1] < F('0.000265') and '238 intervals' in sieve(9, 'False')[1] and 'CERTIFIED' in sieve(9, 'False')[1], "Lemma 25: 238 intervals, max < 0.000265")
safe(lambda: 'CERTIFIED' in sieve(8, 'True')[1], "Remark 26: the sieve range passes K = 8 with Lemma 13 (the presieve)")
# (I4'), Appendix B: mpmath iv (third) and Arb (audit)
safe(lambda: line_with('third/js_cert/js_cert.out', 'a-form BJV22', 'covered by 12 boxes', 'case (b) > 9.80368') is not None, "(I4'): [L0, 3000] case (b) > 9.8036 [third, mpmath iv]")
def tail_iv():
    l = line_with('third/js_cert/js_cert.out', 'tail L >= 3000.0 by route A')
    return F(re.search(r'case \(b\) > ([0-9.]+)', l).group(1))
safe(lambda: tail_iv() > F('26.218'), "(I4'): L >= 3000 case (b) > 26.218 [third, mpmath iv]")
def jget(path, *keys):
    v = json.loads((out_dir / path).read_text())
    for k in keys:
        v = v[k]
    return v
safe(lambda: jget('audit/audit_js.json', 'direct_cover_C1_114', 'count') == 12 and ball(jget('audit/audit_js.json', 'direct_cover_C1_114', 'min_lower_b'))[0] > F('9.8036'), "(I4'): [L0, 3000] case (b) > 9.8036 [audit, Arb]")
safe(lambda: ball(jget('audit/audit_js.json', 'tail_at_3000_C1_114', 'case_b'))[0] > F('26.21829064'), "(I4'): L >= 3000 case (b) > 26.21829064 [audit, Arb]")
# The independent audit's bounds quoted in the paper's computations section (Arb)
R6 = 'audit/t2v6/'
safe(lambda: ball(jget(R6 + 'resume1/audit_c4.json', '1800', 'lhs_majorant'))[1] < F('0.2097564'), "Audit: Lemma 7 at (e^1800, 18) < 0.2097564")
safe(lambda: ball(jget(R6 + 'resume1/audit_c4.json', '2736.86', 'lhs_majorant'))[1] < F('0.4067970'), "Audit: Lemma 10 < 0.4067970")
safe(lambda: ball(jget(R6 + 'resume1/audit_s4.json', 'logarithmic', 'high'))[1] < F('0.448050660231') and ball(jget(R6 + 'resume1/audit_s4.json', 'rational', 'high'))[1] < F('0.454079084257'), "Audit: Lemma 16 < 0.448050660231 (log cells), < 0.454079084257 (rational)")
def mid(i):
    return ball(jget(R6 + 'resume1/audit_grh9.json', 'middle')[i]['lhs_majorant'])[1]
safe(lambda: mid(0) < F('0.2413750') and mid(1) < F('0.1475264') and mid(2) < F('0.1390529'), "Audit: Lemma 7 (e^62, 9) < 0.2413750; Lemma 23 < 0.1475264 and < 0.1390529")
safe(lambda: len(jget(R6 + 'resume1/audit_grh9.json', 'sieve', 'rows')) == 238 and max(ball(r['upper'])[1] for r in jget(R6 + 'resume1/audit_grh9.json', 'sieve', 'rows')) < F('0.000265'), "Audit: Lemma 25, all 238 rows < 0.000265")
def gridref(i):
    g = jget(R6 + 'audit_v6.json', 'grids')[i]
    return g['nrows'], ball(g['min_relative_margin'])[0]
safe(lambda: gridref(0)[0] == 501 and gridref(0)[1] > F('0.9030') and gridref(1)[0] == 449 and gridref(1)[1] > F('0.42371750647'), "Audit: Theorem 2, all 950 rows; top margin > 0.42371750647")
safe(lambda: line_with(R6 + 'check_float_cells.out', 'weights verified 11801', 'J values verified 1127') is not None, "Audit: the float cell weights (11801) and J values (1127) checked in Arb")
# Appendix B's f and F
safe(lambda: line_with('author/fF_enclose.out', '1 - f(6) < 1.05e-4: True', 'F(7) - 1 < 5e-6: True') is not None, "Appendix B: 1 - f(6) < 1.05e-4 and F(7) - 1 < 5e-6")

print('== RESULT:', 'ALL REPRODUCED' if ok_all else 'SOMETHING DIFFERS OR FAILS (see above)')
sys.exit(0 if ok_all else 1)