#!/usr/bin/env python3
"""Check every rule and claim in proof.md for 1RB0RA_1RC1RF_1LD0LC_1RA1LE_1RA0LC_---0RD (stdlib only).

usage: python3 -B check_proof.py [--long] [--seed S] [--quick]
  default: about 6 minutes of pure Python (--quick: about 2.5 minutes).
  --long : also recompile and rerun the C trackers (scripts/proof/rle2.c to 1.3e10 steps, about 60 s;
           scripts/funded/cfgdump.c to 3e8 steps) and compare with the stored files.
  --quick: fewer random instances (smoke test).

Checks (names as in proof.md):
  HALT     the only undefined transition is F0, and F is entered only by B1.
  FULLPY   independent Python run from blank to 1.6e7 steps: visit runs at b18 and b618 equal the stored C file.
  IFACE    stored run to 1.3e10 (data/proof/rle_b18_b618_1.3e10.txt): b18 visits are only AC/DC, b618 only AE/BE;
           b18 runs alternate A/D (one D-run per epoch); the epoch table N_m, c_m, j_m.
  INIT     the rest point S0 (step 300,032,133): M clean, T canonical T(P,PP;e=5521).
  ZM       zone M (cells 18..617): per-visit rules MD/MA (and the top carry -> B visits), exact on random words.
  GMAP     the value map g: every v ends at 0 or 5; visit bound.
  TA       zone T: A visit = throttle increment (exact), including K = -1.
  TB       zone T: the first B visits after an A-run follow the throttle frontier rule (exact, throttle part).
  TBURST5  [flagged F2] all 40 canonical throttles with K <= 2: B^5 then A^2600 -> canonical, K' in {K, K-1}
           (INFO line: K = 3, where 3 of 81 throttles end with a dead slot).
  TBURSTJ  [flagged F3] random canonical throttles, B^j (j up to 3000) then A^2600: no halt, all answers E
           (INFO line: how many end canonical; the rest end with a dead slot or big-region leftovers).
  TNEG     zone T is NOT safe for arbitrary visit words: T(R,R) on B A^7 B A^8 B answers C. (Expected PASS = the
           counterexample reproduces; it is why the burst shape in IFACE matters.)
"""
import os, sys, random, json, subprocess, math, itertools, time
HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, os.path.join(HERE, 'scripts', 'proof'))
from zones import TR, Halt, visit, load_cfg, win, set_cells, to_b18_rest

ARGS = sys.argv[1:]
LONG = '--long' in ARGS; QUICK = '--quick' in ARGS
SEED = int(ARGS[ARGS.index('--seed') + 1]) if '--seed' in ARGS else 1
rng = random.Random(SEED)
fails = []
def check(name, ok, info=''):
    print(('PASS ' if ok else 'FAIL ') + name + (('  ' + info) if info else '')); sys.stdout.flush()
    if not ok: fails.append(name)
T0 = time.time()

# ---------------- HALT ----------------
undef = [k for k, v in TR.items() if v is None]
into_F = [k for k, v in TR.items() if v is not None and v[2] == 'F']
check('HALT', undef == [('F', 0)] and into_F == [('B', 1)] and TR[('B', 1)] == (1, 1, 'F') and TR[('F', 1)] == (0, 1, 'D'),
      f'undefined {undef}, into F {into_F}: halts iff B reads 1 with a 0 right of it ("B> 1 0")')

# ---------------- FULLPY + IFACE ----------------
RLE = os.path.join(HERE, 'data', 'proof', 'rle_b18_b618_1.3e10.txt')
def parse_rle(lines):
    runs = {18: [], 618: []}
    for l in lines:
        p = l.split()
        if p and p[0] in ('b18', 'b618'): runs[int(p[0][1:])].append((p[1], int(p[2]), int(p[3])))
    return runs
stored = parse_rle(open(RLE).read().split('\n'))

def py_rle(nsteps):
    W = {}; D = {}; N = {}
    S = 'ABCDEF'
    for (q, s), v in TR.items():
        if v is not None: W[(S.index(q), s)] = v[0]; D[(S.index(q), s)] = v[1]; N[(S.index(q), s)] = S.index(v[2])
    size = 1 << 16; off = 1 << 12; t = bytearray(size); pos = 0; q = 0
    wt = [[W.get((a, b), 0) for b in (0, 1)] for a in range(6)]; dt = [[D.get((a, b), 0) for b in (0, 1)] for a in range(6)]
    nt = [[N.get((a, b), -1) for b in (0, 1)] for a in range(6)]
    runs = {18: [], 618: []}; inv = {18: -1, 618: -1}; last = {18: None, 618: None}
    step = 0
    while step < nsteps:
        i = pos + off; s = t[i]
        if q == 5 and s == 0: return None, step
        t[i] = wt[q][s]; old = pos; pos += dt[q][s]; q = nt[q][s]; step += 1
        if old == 17 or old == 18 or old == 617 or old == 618:
            for b in (18, 618):
                if old == b - 1 and pos == b: inv[b] = q
                elif old == b and pos == b - 1:
                    ty = S[inv[b]] + S[q]; r = runs[b]
                    if r and r[-1][0] == ty: r[-1][1] += 1
                    else: r.append([ty, 1, step])
    return runs, step
NPY = 6_000_000 if QUICK else 16_000_000
pr, _ = py_rle(NPY)
ok = pr is not None
for b in (18, 618):
    got = [tuple(x) for x in pr[b][:-1]]          # last run may be cut by the horizon
    ref = [x for x in stored[b] if x[2] < NPY][:len(got)]
    ok = ok and got == ref and len(got) > 0
check('FULLPY', ok, f'Python run to {NPY:,} steps: {len(pr[18]) - 1} closed b18 runs and {len(pr[618]) - 1} b618 runs equal the stored C runs')

if LONG:
    src = os.path.join(HERE, 'scripts', 'proof', 'rle2.c'); exe = os.path.join('/tmp', 'r8_rle2_check')
    subprocess.run(['gcc', '-O2', '-o', exe, src], check=True)
    out = subprocess.run(['nice', '-n', '10', exe, '1.3e10'], capture_output=True, text=True).stdout
    check('FULLC', out.strip() == open(RLE).read().strip(), 'C rerun to 1.3e10 equals the stored run file')

ty18 = sorted({x[0] for x in stored[18]}); ty618 = sorted({x[0] for x in stored[618]})
alt = all(stored[18][i][0] != stored[18][i + 1][0] for i in range(len(stored[18]) - 1))
check('IFACE-types', ty18 == ['AC', 'DC'] and ty618 == ['AE', 'BE'],
      f'b18 {ty18} ({sum(x[1] for x in stored[18]):,} visits), b618 {ty618} ({sum(x[1] for x in stored[618]):,} visits), 0 halts to 1.3e10')
check('IFACE-alternation', alt and stored[18][0][0] == 'AC', 'b18 visit word = A^N1 D^c1 A^N2 D^c2 ... (one D-run per epoch)')
# epoch table: D-run k (from 0) is the pause of epoch m = k + 3: D-run 117 at 7,565,813 is m = 10
D = [x for x in stored[18] if x[0] == 'DC']; A = [x for x in stored[18] if x[0] == 'AC']
tab = []
for k, d in enumerate(D):
    m = k + 3
    nA = next((a[1] for a in A if a[2] > d[2]), None)
    nxt = D[k + 1][2] if k + 1 < len(D) else 10 ** 13
    j = sum(b[1] for b in stored[618] if b[0] == 'BE' and d[2] < b[2] < nxt)
    tab.append((m, d[2], d[1], nA, j))
print('       epoch table: m, first D step, c_m, N_m (A-run after), B visits at b618 in that ending')
for r in tab: print('        ', r)
gl = [r for r in tab if r[4]]
check('IFACE-epochs', [r[0] for r in gl] == [5, 14] and all(r[4] == 5 for r in gl)
      and all((r[3] or 10 ** 9) >= 3000 for r in tab if r[0] >= 9),
      'B-bursts at b618: exactly 5 visits, at m = 5 (start-up) and m = 14 only; every A-run for m >= 9 has N_m >= 3,000')

# ---------------- INIT ----------------
INB = {'P': '1001', 'Q': '1011', 'R': '1000'}; D4 = {'1001': 'P', '1011': 'Q', '1000': 'R', '0011': 's'}
MSB = {'.': '0110', '1': '1110', '2': '0010', '0': '0000'}; MDEC = {v: k for k, v in MSB.items()}
def parseT(T):
    """canonical T(s3, digits; e): cell 618 = 1, groups from 619 in P/Q/R, last one the marker Q, then (0011)^e, then 0s.
    Returns (throttle string incl. s3, without marker; e) or None."""
    if T.get(618, 0) != 1: return None
    hi = max(T); g = []; p = 619
    while True:
        b = win(T, p, p + 3)
        if b == '0011' or b == '0000': break
        if b not in ('1001', '1011', '1000'): return None
        g.append(D4[b]); p += 4
        if len(g) > 40: return None
    if not g or g[-1] != 'Q': return None
    e = 0
    while win(T, p, p + 3) == '0011': e += 1; p += 4
    if any(T.get(c, 0) for c in range(p, hi + 1)): return None
    return ''.join(g[:-1]), e
def buildT(thr, e):
    T = {}; set_cells(T, 618, '1' + ''.join(INB[c] for c in thr) + '1011' + '0011' * e); return T
def mword(M):
    return [MDEC.get(win(M, 2 + 4 * k, 5 + 4 * k), '?') for k in range(4, 154)]
cfg = os.path.join(HERE, 'data', 'funded', 'cfg_3e8.txt')
tape, pos, st, step = load_cfg(cfg)
if LONG:
    exe = '/tmp/r8_cfgdump_check'
    subprocess.run(['gcc', '-O2', '-o', exe, os.path.join(HERE, 'scripts', 'funded', 'cfgdump.c')], check=True)
    out = subprocess.run([exe, '3e8'], capture_output=True, text=True).stdout
    check('INIT-cfg', out.strip() == open(cfg).read().strip(), 'cfgdump rerun from blank to 3e8 equals data/funded/cfg_3e8.txt')
pos, st, n = to_b18_rest(tape, pos, st)
S0 = step + n
Mz = {c: 1 for c in tape if 18 <= c <= 617}; Tz = {c: 1 for c in tape if c >= 618}; Lz = {c: 1 for c in tape if c <= 17}
pt = parseT(Tz)
check('INIT', S0 == 300_032_133 and set(mword(Mz)) == {'.'} and win(Mz, 618 - 4, 617) == '0110' and pt == ('PPP', 5521),
      f'rest point S0 at step {S0:,} (head 17, state {st}): M = 150 blocks ".", T = {pt}')
LEFT0 = win(Lz, -100, 17)

# ---------------- ZM ----------------
VAL = {'.': 0, '2': 1, '1': 2}; DIG = {0: '.', 1: '2', 2: '1'}
def m_add(w, i, c):
    w = list(w); out = 0
    while c:
        if i >= len(w): return w, c          # carry c out of the top block -> c B visits at b618
        v = VAL[w[i]] + c; w[i] = DIG[v % 3]; c = v // 3; i += 1
    return w, 0
def m_pred(w, x):
    """predicted (new word, emitted b618 visits) for one visit x at b18; w = blocks 4..153."""
    if x == 'D':
        w2, c = m_add(w, 1, 2); return w2, 'B' * c
    f = next((i for i, c in enumerate(w) if c != '.'), None)
    if f is None: return list(w), 'A'
    w = list(w); c0 = w[f]
    if c0 == '0': w[f] = '.'; return w, ''
    if c0 == '2': w[f] = '0'; return w, ''
    w[f] = '.'; w2, c = m_add(w, f + 1, 4); return w2, 'B' * c
def zm_instance(w, prog):
    M = dict(Mz)
    for k, c in enumerate(w): set_cells(M, 2 + 4 * (4 + k), MSB[c])
    pred = mword(M); nv = okv = 0; bad = None; emitted = ''
    for x in prog:
        try:
            o, rv, _ = visit(M, 18, x, hi=617, answer='E', cap=10 ** 6)
        except Halt:
            return nv, okv, ('halt', nv), emitted
        pw, pe = m_pred(pred, x); pred = pw; nv += 1; emitted += ''.join(rv)
        if o == 'C' and ''.join(rv) == pe and mword(M) == pred: okv += 1
        elif bad is None: bad = (nv, x, o, ''.join(rv), pe)
        if x == 'A' and emitted.endswith('AA'): break      # ending done: the word is clean and visits pass
    return nv, okv, bad, emitted
NZ = 40 if QUICK else 160
tot = okt = 0; bads = []; gl = cl = mo = 0
for it in range(NZ):
    kind = it % 4
    if kind < 2:     # pause end: clean word, D-run, A-run through the ending
        w = ['.'] * 150; c = rng.randrange(1, 400 if kind == 0 else 60)
        prog = 'D' * c + 'A' * 330
    elif kind == 2:  # random short word (incl. a junk block at the frontier), then A-run
        L = rng.randrange(1, 25); w = [rng.choice('.12') for _ in range(L)] + ['.'] * (150 - L)
        f = next((i for i, c in enumerate(w) if c != '.'), None)
        if f is not None and rng.random() < 0.3: w[f] = '0'
        prog = 'A' * 340
    else:            # MO: nearly full word, D-run with carries out of the top, then A-run
        w = ['.'] + [rng.choice('11112') for _ in range(149)]
        prog = 'D' * rng.randrange(1, 30) + 'A' * 330
    nv, okv, bad, em = zm_instance(w, prog)
    tot += nv; okt += okv
    if bad and len(bads) < 5: bads.append((it, bad))
    gl += em.count('B') >= 5 and kind < 3; mo += kind == 3 and 'B' in em
check('ZM', okt == tot and not bads, f'{NZ} instances, {okt:,}/{tot:,} visits exact (word and b618 output), all answers C; '
      f'{gl} instances with a glider exit (5 B), {mo} MO instances with top carries' + (f' bad {bads}' if bads else ''))

# ---------------- GMAP ----------------
def g_out(v):
    n = 0
    while True:
        if v == 0: return 0, n
        while v % 3 == 0: v //= 3
        if v == 5: return 5, n
        if v % 3 == 1: v = (v - 1) // 3; n += 2
        else: v = (v + 10) // 3; n += 1
res = [g_out(v) for v in range(1, 3 ** 10)]
ends = {r[0] for r in res}; ng = sum(r[0] == 5 for r in res)
def nd(v):
    k = 0
    while v: v //= 3; k += 1
    return k
bound = all(n <= 2 * nd(v) + 3 for v, (_, n) in zip(range(1, 3 ** 10), res))
check('GMAP', ends == {0, 5} and ng == 3 ** 8 and bound,
      f'v in 1..3^10-1: ends in {sorted(ends)}, {ng} = 3^8 gliders, visits <= 2*(ternary digits of v) + 3')

# ---------------- TA ----------------
def t_inc(thr, e):
    if thr == '': return thr, e + 2
    s3 = thr[0]; c = 0 if s3 == 'P' else 1
    s3n = {'P': 'Q', 'Q': 'R', 'R': 'P'}[s3]; d = list(thr[1:]); V = {'P': 0, 'R': 1, 'Q': 2}; IV = 'PRQ'
    for j in range(len(d)):
        if not c: break
        v = V[d[j]] + c; d[j] = IV[v % 3]; c = v // 3
    return s3n + ''.join(d), e + c
NT = 30 if QUICK else 120
tot = okt = 0; bad = None
for it in range(NT):
    K = rng.randrange(-1, 5); thr = '' if K < 0 else ''.join(rng.choice('PQR') for _ in range(K + 1)); e = rng.randrange(6, 30)
    T = buildT(thr, e); pthr, pe = thr, e
    for v in range(40):
        o, rv, _ = visit(T, 618, 'A', cap=10 ** 6); pthr, pe = t_inc(pthr, pe); tot += 1
        if o == 'E' and parseT(T) == (pthr, pe): okt += 1
        elif bad is None: bad = (thr, e, v, o, parseT(T), (pthr, pe))
check('TA', okt == tot, f'{NT} canonical throttles (K = -1..4), {okt:,}/{tot:,} A visits: answer E and T = predicted increment'
      + (f' bad {bad}' if bad else ''))

# ---------------- TB ----------------
JUNK = {'P': '0001', 'R': '0000', 'Q': '0011'}
def t_bvisits(thr, n):
    """throttle part (s3, digits, marker) after each of n B visits (frontier rule; see proof.md TB)."""
    t = list(thr) + ['Q']; pend = None; saved = None; out = []
    V = {'P': 0, 'R': 1, 'Q': 2}; IV = 'PRQ'
    for _ in range(n):
        if pend is not None:
            t[pend] = 'P'; t[pend + 1] = saved; pend = None
        else:
            f = next((i for i in range(len(t) - 1) if t[i] != 'P'), None)
            if f is not None:
                if t[f] == 'Q':
                    t[f] = 'P'; c = 4
                    for j in range(f + 1, len(t) - 1):
                        v = V[t[j]] + c; t[j] = IV[v % 3]; c = v // 3
                else:
                    saved = t[f + 1]; t[f + 1] = JUNK[t[f + 1]]; pend = f
        out.append(list(t))
    return out, pend
def tgroups(T, n):
    return [D4.get(win(T, 619 + 4 * j, 622 + 4 * j), win(T, 619 + 4 * j, 622 + 4 * j)) for j in range(n)]
tot = okt = 0; bad = None
NB = 60 if QUICK else 240
for it in range(NB):
    K = rng.randrange(0, 5); thr = ''.join(rng.choice('PQR') for _ in range(K + 1)); e = 20
    T = buildT(thr, e); pred, _ = t_bvisits(thr, 5)
    for v in range(5):
        o, rv, _ = visit(T, 618, 'B', cap=10 ** 6); tot += 1
        got = [{'s': '0011'}.get(x, x) for x in tgroups(T, K + 2)]
        exp = [x if x in 'PQR' else x for x in pred[v]]
        exp = ['0011' if x == '0011' else x for x in exp]
        if o == 'E' and got == exp: okt += 1
        elif bad is None: bad = (thr, v, o, got, exp)
check('TB', okt == tot, f'{NB} canonical throttles (K = 0..4), {okt:,}/{tot:,} B visits: answer E, throttle part as predicted'
      + (f' bad {bad}' if bad else ''))

# ---------------- TBURST5 / TBURSTJ (flagged lemmas F2 / F3) ----------------
NA = 2600
def burst(thr, e, j, na=NA):
    T = buildT(thr, e); outs = set()
    try:
        for _ in range(j): outs.add(visit(T, 618, 'B', cap=10 ** 7)[0])
        for _ in range(na): outs.add(visit(T, 618, 'A', cap=10 ** 7)[0])
    except Halt:
        return 'halt', None
    return outs, parseT(T)
states = [''] + [s + ''.join(d) for K in range(0, 3) for s in 'PQR' for d in itertools.product('PQR', repeat=K)]
# K <= 2 is the reachable range: T(PPP) has K = 2 at S0 and no rule raises K. K = 3 is reported separately below.
if QUICK: states = states[:20]
okc = 0; drops = 0; stays = 0; pred_ok = 0; bad = []
for thr in states:
    outs, pt = burst(thr, 25, 5)
    K = len(thr) - 1
    if outs == {'E'} and pt is not None and len(pt[0]) - 1 in (K, K - 1) and (K >= 0 or len(pt[0]) - 1 == -1) and pt[1] >= 25:
        okc += 1; d = len(pt[0]) - 1 == K - 1; drops += d; stays += not d
        if thr:
            _, pend = t_bvisits(thr, 5); pred_ok += (pend is not None) == d
        else: pred_ok += 1
    elif len(bad) < 4: bad.append((thr, outs, pt))
check('TBURST5', okc == len(states) and pred_ok == len(states),
      f'[flagged F2] {okc}/{len(states)} throttles (K = -1..2, e = 25): B^5 A^{NA} -> canonical, e\' >= e, K\' = K in {stays}, K-1 in {drops}; '
      f'K-drop = "R step half done after the 5th B" in {pred_ok}/{len(states)}' + (f' bad {bad}' if bad else ''))
k3 = [s + ''.join(d) for s in 'PQR' for d in itertools.product('PQR', repeat=3)]
if QUICK: k3 = k3[:9]
k3c = [thr for thr in k3 if (lambda o, p: o == {'E'} and p is not None and len(p[0]) - 1 in (2, 3))(*burst(thr, 25, 5))]
print(f'INFO TBURST5-K3  {len(k3c)}/{len(k3)} K = 3 throttles canonical after B^5 A^{NA}; the others end with a dead slot '
      f'(0011/0000 between the digits and the marker): {sorted(set(k3) - set(k3c))}. K = 3 is not reachable from S0.')
NJ = 10 if QUICK else 40
okc = 0; bad = []; js = []; kd = 0; safe = 0
for it in range(NJ):
    K = rng.randrange(-1, 3); thr = '' if K < 0 else ''.join(rng.choice('PQR') for _ in range(K + 1))
    j = int(math.exp(rng.uniform(0, math.log(3000)))); js.append(j); e = rng.randrange(30, 60)
    outs, pt = burst(thr, e, j)
    safe += outs == {'E'}
    if outs == {'E'} and pt is not None and len(pt[0]) - 1 in ({K, K - 1} if K >= 0 else {-1}) and pt[1] >= e:
        okc += 1; kd += len(pt[0]) - 1 < K
    elif len(bad) < 6: bad.append((thr, e, j))
check('TBURSTJ', safe == NJ, f'[flagged F3] {safe}/{NJ} random throttles (K = -1..2, e = 30..59), B^j with j = {min(js)}..{max(js)} '
      f'then A^{NA}: no halt, every visit answered E')
print(f'INFO TBURSTJ-canonical  only {okc}/{NJ} end canonical (K\' in {{K, K-1}}, {kd} drops); the others end with a dead slot '
      f'or leftover big-region blocks, so F3 needs a wider invariant family: {bad}')

# ---------------- TNEG ----------------
T = buildT('RR', 30); outs = []
for x in 'B' + 'A' * 7 + 'B' + 'A' * 8 + 'B':
    outs.append(visit(T, 618, x, cap=10 ** 6)[0])
check('TNEG', outs[-1] == 'C' and set(outs[:-1]) == {'E'},
      'T(R,R; e=30) on B A^7 B A^8 B answers C on the last visit: T is safe only for the burst shape the run produces')

print(f'\nSUMMARY: {"ALL PASS" if not fails else f"{len(fails)} FAIL: {fails}"}  ({time.time() - T0:.0f} s, seed {SEED})')