#!/usr/bin/env python3
"""check_proof.py: simulation evidence for the DELTA proof of twin #25 (1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---).

The parent is kill #3, 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB--- (KILLED_NONHALT). This script imports the
parent's check_proof.py read-only, for its abstract map (the rules of the parent's proof.md section 2), its
INV+(e) checker and its cycle-pair checker. Everything that depends on the machine or on the start is re-run here
on the twin: the twin's own transition table is simulated directly, and the twin's own orbit is checked.

Nothing here is a proof. Every claim it checks is a hypothesis until Rocq accepts it.

Sections (each prints PASS/FAIL lines; the SUMMARY is the conjunction of all of them):
  S  the relation: sigma = (A C)(B D) is the only state renaming, with or without mirroring, that takes the
     parent's table to the twin's, and sigma(A) = C; so the twin's blank-tape run is the parent's run from
     0^inf C> 0^inf, relabelled (checked step by step), not the parent's own run (which has 11 C> at step 2)
  A  every macro rule of the parent's proof.md section 2, from random instances, simulated on the TWIN's table
     (canonical head state C = sigma(A)), against the parent's abstract map
  C  the twin's initial segment: blank tape -> K(2; (11,13,0); -) at step 1,088
  D  the twin's direct simulation from blank vs the abstract map, transition by transition; the step of
     overflow 6 and the base E-start K(2; (95,68,0),(34,33,1),(10,15,1),(1,26,1); -)
  B  the base: INV+(e) clause by clause (parent's inv_violations), and the Rocq J_base clauses (PC E1 of the
     parent's .v, transcribed) at the twin's base
  G  the twin's orbit from its base: parent's section G2 (every lemma of proof.md 3.8 at every cycle pair) and
     section F (every clause of INV at every cycle), to L* > lmax; the parent's rocq/jcheck.py invariant J,
     macro step by macro step, for a number of re-pairings
  X  the coupling: twin and parent abstract orbits, compared at every macro step (L <= lx) and at every
     re-pairing (L <= lmax): same rule sequence, and exactly one block differs, by +2, and it is the far block
Usage: python3 -B check_proof.py [--quick] [--seed N] [--steps N] [--lmax N] [--lx N] [--jcyc N]
"""
import os, sys, random, argparse, itertools, importlib.util
from collections import Counter
sys.dont_write_bytecode = True

TM = '1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---'
PARENT = '1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---'
HERE = os.path.dirname(os.path.abspath(__file__))
PDIR = os.path.join(os.path.dirname(HERE), PARENT)

def load(name, path):
    spec = importlib.util.spec_from_file_location(name, path)
    mod = importlib.util.module_from_spec(spec); spec.loader.exec_module(mod)
    return mod

cp = load('parent_check_proof', os.path.join(PDIR, 'check_proof.py'))   # parent's checks (read-only)
assert cp.TM == PARENT

ST = 'ABCDEF'
SIGMA = {'A': 'C', 'B': 'D', 'C': 'A', 'D': 'B', 'E': 'E', 'F': 'F'}      # parent state -> twin state
TAB = cp.parse_tm(TM)                                                    # (state index, read) -> (write, move, next) | None
CANON = ST.index(SIGMA['A'])                                             # the twin's K head state: C

INIT_STEP = 1088
INIT_K = (2, [(11, 13, 0)], None)
BASE_K = (2, [(95, 68, 0), (34, 33, 1), (10, 15, 1), (1, 26, 1)], None)
BASE_STEP = 79114          # checked in section D (parent: 78,710)
PARENT_BASE_K = (2, [(95, 68, 0), (34, 33, 1), (10, 15, 1), (1, 24, 1)], None)

def letters(s):
    t = {}
    for i, blk in enumerate(s.split('_')):
        for r in (0, 1):
            x = blk[3*r:3*r+3]
            t[(ST[i], r)] = None if x == '---' else (int(x[0]), x[1], x[2])
    return t

# ---------------------------------------------------------------- S: the relation
def image(tp, sig, mirror):
    out = {}
    for (q, r), v in tp.items():
        out[(sig[q], r)] = None if v is None else (v[0], {'L': 'R', 'R': 'L'}[v[1]] if mirror else v[1], sig[v[2]])
    return out

def lockstep(n):
    """Twin from 0^inf A> 0^inf vs parent from 0^inf C> 0^inf: same tape, same position, twin state = sigma(parent state)."""
    tp, tt = cp.TAB, TAB
    sg = [ST.index(SIGMA[c]) for c in ST]
    size = 2*n + 16
    a = bytearray(size); b = bytearray(size); pa = pb = n + 8
    sa, sb = 0, ST.index('C')                          # twin starts in A, parent in C
    for step in range(n):
        if sa != sg[sb] or pa != pb or a[pa] != b[pb]: return step
        ta, tb = tt[(sa, a[pa])], tp[(sb, b[pb])]
        if (ta is None) != (tb is None): return step
        if ta is None: return None
        a[pa] = ta[0]; pa += ta[1]; sa = ta[2]
        b[pb] = tb[0]; pb += tb[1]; sb = tb[2]
    return None if a == b else -1

def section_S(n):
    print('== S. relation to the parent: renaming / mirror search, start state, lockstep')
    tp, tt = letters(PARENT), letters(TM)
    sols = [(dict(zip(ST, perm)), mir) for perm in itertools.permutations(ST) for mir in (False, True)
            if image(tp, dict(zip(ST, perm)), mir) == tt]
    uniq = len(sols) == 1 and sols[0] == (SIGMA, False)
    print('  maps phi with twin = phi(parent) among 720 renamings x {plain, mirror}: %s' %
          [(''.join(s[c] for c in ST), 'mirror' if m else 'plain') for s, m in sols])
    print('  unique, no mirror, sigma = (A C)(B D) (A->C B->D C->A D->B, E, F fixed) ->', 'PASS' if uniq else 'FAIL')
    inv = all(SIGMA[SIGMA[c]] == c for c in ST)
    print('  sigma is an involution (sigma^-1 = sigma) ->', 'PASS' if inv else 'FAIL')
    st = SIGMA['A']
    print('  twin start state A = sigma(%s): the twin from blank is sigma(parent from 0^inf C> 0^inf)' % [c for c in ST if SIGMA[c] == 'A'][0])
    r = lockstep(n)
    okl = r is None
    print('  lockstep %d steps, twin from blank vs relabelled parent from 0^inf C> 0^inf: %s -> %s' % (
        n, 'identical at every step' if okl else 'differ at step %s' % r, 'PASS' if okl else 'FAIL'))
    # the parent's own run: A0 = 1RB, B0 = 1RC, so step 2 is 0^inf 1 1 C> 0^inf (not 0^inf C> 0^inf)
    t1, t2 = cp.TAB[(0, 0)], cp.TAB[(1, 0)]
    own = t1 == (1, 1, 1) and t2 == (1, 1, 2)
    print('  parent from its own blank start: A0=1RB, B0=1RC, so step 2 is 0^inf 1 1 C> 0^inf; the twin lacks that 11 ->',
          'PASS' if own else 'FAIL')
    return uniq and inv and okl and own and st == 'C'

# ---------------------------------------------------------------- A: the parent's rules on the twin's table
def run_macro(h, P, T, cap=None):
    """Parent's run_macro, on the twin's table, with the twin's canonical head state C (= sigma(A))."""
    w = cp.build(h, P, T); n = len(w)
    if cap is None: cap = 400*n*n + 100000
    pad = 4*n + 64
    tape = bytearray(pad) + bytearray(int(c) for c in w) + bytearray(pad)
    pos = pad - 1; st = CANON; lo = pos; steps = 0
    while steps < cap:
        tr = TAB[(st, tape[pos])]
        if tr is None: return ('HALT', steps, st)
        tape[pos] = tr[0]; pos += tr[1]; st = tr[2]; steps += 1
        if pos < 0 or pos >= len(tape):
            ext = bytearray(len(tape))
            if pos < 0: tape = ext + tape; pos += len(ext); lo += len(ext)
            else: tape = tape + ext
        if pos < lo: lo = pos
        if st == CANON and pos <= lo + 1 and tape[pos] == 0 and not any(tape[lo:pos]):
            r = cp.parse(''.join('1' if b else '0' for b in tape[pos+1:]))
            if r is not None and r[0] != '?': return (r, steps)
    return ('CAP', steps)

def section_A(n, rng):
    print('== A. the parent\'s macro rules (proof.md section 2 of the parent) on the TWIN\'s table, head state C')
    allok = True; tot = 0
    for rule in cp.RULES:
        ok = 0; fails = []
        for i in range(n):
            h, P, T = cp.gen(rule, rng, i)
            exp = cp.astep(h, P, T)
            assert exp[3] == rule, (rule, exp[3], h, P, T)
            got = run_macro(h, P, T)
            good = got[0] not in ('HALT', 'CAP') and got[0] == (exp[0], exp[1], exp[2]) and got[1] >= 1
            ok += good
            if not good: fails.append((h, P, T, str(got)[:120]))
        tot += n; allok &= (ok == n)
        print('  %-14s %3d/%d %s' % (rule, ok, n, 'PASS' if ok == n else 'FAIL ' + str(fails[:2])))
    # the halting cell, relabelled: parent halts on F1, entered only from C1 (=1RF), entered only from B0;
    # twin: F1 is ---, F is entered only from A1 (=1RF), A is entered only from D0 (=1RA)
    entF = sorted(ST[q] + str(r) for (q, r), v in TAB.items() if v and v[2] == 5)
    entA = sorted(ST[q] + str(r) for (q, r), v in TAB.items() if v and v[2] == 0)
    okh = TAB[(5, 1)] is None and entF == ['A1'] and entA == ['D0']
    print('  halting transition: F1 undefined; F entered only from %s, A only from %s; so the twin halts exactly at D> 0 1 1 ->'
          % (entF, entA), 'PASS' if okh else 'FAIL')
    print('  A total: %s (%d instances)' % ('PASS' if allok and okh else 'FAIL', tot))
    return allok and okh

# ---------------------------------------------------------------- C, D: the twin's initial segment, direct cross-check
def stream_canonical(max_steps):
    """Direct simulation of the twin from the blank tape; yields (step, K) at every canonical record config
    (state C on a new leftmost cell, tape to its right parses as some K)."""
    size = 1 << 16
    tape = bytearray(size); pos = size//2; st = 0; lo = pos; hi = pos; steps = 0
    while steps < max_steps:
        tr = TAB[(st, tape[pos])]
        if tr is None: yield (steps, 'HALT'); return
        tape[pos] = tr[0]; pos += tr[1]; st = tr[2]; steps += 1
        if pos < 0 or pos >= len(tape):
            ext = bytearray(len(tape))
            if pos < 0: tape = ext + tape; pos += len(ext); lo += len(ext); hi += len(ext)
            else: tape = tape + ext
        if pos > hi: hi = pos
        if pos < lo:
            lo = pos
            if st == CANON:
                r = cp.parse(tape[pos+1:hi+1].translate(cp.BITS).decode())
                if r is not None and r[0] != '?': yield (steps, r)

def section_CD(max_steps):
    print('== C. the twin\'s initial segment')
    seq = list(stream_canonical(max_steps))
    halted = any(k == 'HALT' for _, k in seq)
    pre = [(s, k) for s, k in seq if s < INIT_STEP]
    first = [x for x in seq if x[0] == INIT_STEP]
    okC = bool(first) and first[0][1] == INIT_K and not halted
    print('  canonical configs before step %d: %s' % (INIT_STEP, pre))
    if len(pre) >= 3:
        try:
            nx = cp.astep(*pre[1][1])
            print('  step %d is in D: %s predicts %s, observed %s at step %d (%s); that successor has L = 0, outside D'
                  % (pre[1][0], nx[3], nx[:3], pre[2][1], pre[2][0], 'match' if nx[:3] == pre[2][1] else 'MISMATCH'))
        except cp.Outside as e:
            print('  step %d: outside (%s)' % (pre[1][0], e))
    print('  step %d: %s -> %s' % (INIT_STEP, first[0][1] if first else None, 'PASS' if okC else 'FAIL'))
    print('== D. the twin\'s direct simulation from blank (%d steps) vs the parent\'s abstract map' % max_steps)
    cnt = Counter(); bad = 0; rep = 0; base = None; reps = []
    post = [x for x in seq if x[0] >= INIT_STEP and x[1] != 'HALT']
    for (s0, k0), (s1, k1) in zip(post, post[1:]):
        try:
            h, P, T, name = cp.astep(*k0)
            if (h, P, T) == (k1[0], k1[1], k1[2]):
                cnt[name] += 1
                if name in ('Ov', 'X1'):
                    rep += 1; reps.append(s1)
                    if rep == 6: base = (s1, k1)
            else: bad += 1; print('  MISMATCH at step', s0, k0, '->', k1, 'predicted', (h, P, T))
        except cp.Outside as e:
            bad += 1; print('  OUTSIDE at step', s0, e)
    okD = bad == 0 and len(post) > 1 and not halted
    print('  %d consecutive canonical transitions, %s; last canonical step %d -> %s' % (
        sum(cnt.values()), dict(cnt), post[-1][0], 'PASS' if okD else 'FAIL'))
    print('  re-pairings (Ov/X1) at steps:', reps[:12], '...' if len(reps) > 12 else '')
    okB = base is not None and base[0] == BASE_STEP and base[1] == BASE_K
    print('  base E-start (after re-pairing 6): step %s, %s -> %s' % (base[0] if base else None, base[1] if base else None,
                                                                   'PASS' if okB else 'FAIL'))
    return okC, okD and okB

# ---------------------------------------------------------------- B: INV+(e) and the Rocq J clauses at the base
def dv(P):
    v = 0
    for (_, _, d) in reversed(P): v = d + 2*v
    return v

def PC_E1(h, i, p, q, n, tv):
    """PC E1 false h i p q n tv of the parent's .v (Definitions PN, PI, PC), transcribed literally."""
    w = 2**n
    pn = (q >= tv + w + 1 and p + tv + w >= 3) if n == 0 else \
         (q >= tv + 3*w + 1 and (p + tv) % 2 == 1 and p + tv + w >= 3*w)
    if i == 1: pi = h % 2 == 0 and 2 <= n and p + tv + w + 3 >= 11*w and h + 4*(tv + w) + 6 >= 12*w
    elif i == 2: pi = p + tv + w + 1 >= 7*w
    else: pi = True
    return 1 <= p and 1 <= q and pn and pi

def J_base(K):
    """J (mkst h P TN E1 false): P <> [], TC E1 false TN (T = TN, c4 = false), AllI (PCx E1 false h) 1 P."""
    h, P, T = K
    if not P or T is not None: return False, []
    res = [PC_E1(h, i+1, p, q, len(P)-1-i, dv(P[i:])) for i, (p, q, d) in enumerate(P)]
    return all(res), res

def section_B():
    print('== B. the base E-start: INV+(e) (parent proof.md 3.8.1) and the Rocq J_base clauses')
    h, P, T = BASE_K
    v = cp.inv_violations(*BASE_K)
    Ls = cp.Lstar(P, T)
    print('  %s: L* = %d; (b) q_1+1=%d >= %d, q_2=%d >= %d, q_3=%d >= %d; (c) p+d = %d, %d, %d odd; far pair (p,q) = (%d,%d), q >= 6;'
          ' (e1) p_1+1=%d >= %d, (e2) p_2=%d >= %d' % (
          BASE_K, Ls, P[0][1]+1, 5*2**(Ls-1), P[1][1], 5*2**(Ls-2), P[2][1], 5*2**(Ls-3), P[0][0]+P[0][2], P[1][0]+P[1][2],
          P[2][0]+P[2][2], P[3][0], P[3][1], P[0][0]+1, 2**(Ls+2), P[1][0], 2**Ls))
    okI = not v
    print('  INV+(e) violations:', v or 'none', '->', 'PASS' if okI else 'FAIL')
    okJ, res = J_base(BASE_K)
    okJp, resp = J_base(PARENT_BASE_K)
    print('  Rocq J (mkst 2 base TN E1 false), PC E1 per pair:', res, '-> twin', 'PASS' if okJ else 'FAIL',
          '| parent base (sanity):', 'PASS' if okJp else 'FAIL')
    # the only difference from the parent's base is the far q (24 -> 26); in J it enters only PN E1 at n = 0
    diff = [(j+1, a, b) for j, (a, b) in enumerate(zip(P, PARENT_BASE_K[1])) if a != b]
    okd = diff == [(4, (1, 26, 1), (1, 24, 1))]
    print('  difference from the parent\'s base: %s (far pair only; J uses it only in q >= tv + 2^0 + 1 = 3) ->' % diff,
          'PASS' if okd else 'FAIL')
    return okI and okJ and okJp and okd

# ---------------------------------------------------------------- G: the twin's orbit through the parent's checks
def section_G(lmax, jcyc):
    print('== G. the twin\'s orbit from its base through the parent\'s checks (G2, F) and the parent\'s jcheck J')
    saved = (cp.INIT_K, cp.BASE_K)
    cp.INIT_K, cp.BASE_K = INIT_K, BASE_K          # the parent's orbit_e/class_invariants read these globals
    try:
        r2 = cp.orbit_e(lmax)
        rF = cp.class_invariants(lmax)
    finally:
        cp.INIT_K, cp.BASE_K = saved
    jc = load('parent_jcheck', os.path.join(PDIR, 'rocq', 'jcheck.py'))
    Pb = [list(x) for x in BASE_K[1]]
    res = jc.run(BASE_K[0], Pb, ('N',), ('E1', False), jcyc)
    okj = res[0] == 'OK'
    print('  jcheck J (parent rocq/jcheck.py) at every macro step from the twin\'s base, %d re-pairings: %s %s rules %s -> %s'
          % (jcyc, res[0], res[1] or '', res[3], 'PASS' if okj else 'FAIL'))
    ok = r2 and rF and okj
    print('  G total:', 'PASS' if ok else 'FAIL')
    return ok

# ---------------------------------------------------------------- X: the coupling with the parent's orbit
def block_diff(ka, kb):
    """Twin K kb vs parent K ka. Returns None if h, L, digits or tail type differ; else the list of
    (kind, index, delta) over all exponents (p_j, q_j, tail parameter) that differ."""
    (ha, Pa, Ta), (hb, Pb, Tb) = ka, kb
    if ha != hb or len(Pa) != len(Pb) or [x[2] for x in Pa] != [x[2] for x in Pb]: return None
    if (Ta is None) != (Tb is None) or (Ta is not None and Ta[0] != Tb[0]): return None
    d = []
    for j, (x, y) in enumerate(zip(Pa, Pb)):
        if x[0] != y[0]: d.append(('p', j+1, y[0]-x[0]))
        if x[1] != y[1]: d.append(('q', j+1, y[1]-x[1]))
    if Ta is not None and Ta[1] != Tb[1]: d.append((Ta[0], 0, Tb[1]-Ta[1]))
    return d

def far_kind(d, K):
    """Name the +2 block relative to the far end: the last pair's p or q, or the tail parameter."""
    kind, j, _ = d
    if j == 0: return kind
    return kind + ('_L' if j == len(K[1]) else '_L-1' if j == len(K[1]) - 1 else '_interior')

def section_X(lx, lmax):
    print('== X. the coupling: twin vs parent abstract orbits')
    # X1: every macro step (plain astep, no batching), from the first K at which both orbits have the same h
    a, b = cp.INIT_K, INIT_K
    n = 0; kinds = Counter(); okx = True
    while len(a[1]) <= lx:
        d = block_diff(a, b)
        if d is None or len(d) != 1 or d[0][2] != 2:
            okx = False; print('  X1 FAIL at macro step %d: parent %s, twin %s' % (n, a, b)); break
        kinds[far_kind(d[0], a)] += 1
        ha, Pa, Ta, na = cp.astep(*a); hb, Pb, Tb, nb = cp.astep(*b)
        if na != nb:
            okx = False; print('  X1 FAIL: rule %s vs %s at macro step %d' % (na, nb, n)); break
        a, b = (ha, Pa, Ta), (hb, Pb, Tb); n += 1
    far = all(not k.endswith('_interior') and not k.endswith('_L-1') for k in kinds)
    print('  X1: %d macro steps from K0 (parent K(2;(11,11,0);-), twin K(2;(11,13,0);-)) to L > %d: same rule at every step,'
          ' exactly one exponent differs, by +2: %s; where: %s -> %s' % (n, lx, okx, dict(kinds), 'PASS' if okx and far else 'FAIL'))
    # X2: at every re-pairing (batched map), to L > lmax
    def repairs(K):
        h, P, T = K; P = list(P); names = []; m = 0
        while len(P) <= lmax:
            h, P, T, name, k, mm = cp.mstep(h, P, T)
            m += mm
            if name != 'bulk': names.append(name)
            if name in ('Ov', 'X1'):
                yield (h, list(P), T), tuple(names), m; names = []; m = 0
    cnt = 0; kinds = Counter(); ok2 = True; events = Counter()
    for (ka, na, ma), (kb, nb, mb) in zip(repairs(cp.INIT_K), repairs(INIT_K)):
        cnt += 1
        d = block_diff(ka, kb)
        if d is None or len(d) != 1 or d[0][2] != 2 or ma != mb or [x for x in na if x != 'Dec'] != [x for x in nb if x != 'Dec']:
            ok2 = False; print('  X2 FAIL at re-pairing %d: parent %s, twin %s' % (cnt, str(ka)[:80], str(kb)[:80])); break
        kinds[(far_kind(d[0], ka), na[-1])] += 1
        for x in na:
            if x not in ('Dec', 'End', 'Ov'): events[x] += 1
    far = all('_interior' not in k[0] and '_L-1' not in k[0] for k in kinds)
    print('  X2: %d re-pairings to L > %d: same macro steps (all rules but Dec, and the same number of decrements) in every'
          ' cycle, exactly one exponent differs, by +2, always the far block: %s' % (cnt, lmax, dict(kinds)))
    print('      rare rules seen in both orbits: %s -> %s' % (dict(events), 'PASS' if ok2 and far else 'FAIL'))
    return okx and far and ok2

if __name__ == '__main__':
    ap = argparse.ArgumentParser()
    ap.add_argument('--quick', action='store_true')
    ap.add_argument('--seed', type=int, default=20261010)
    ap.add_argument('--steps', type=int, default=None)
    ap.add_argument('--lmax', type=int, default=None)
    ap.add_argument('--lx', type=int, default=None)
    ap.add_argument('--jcyc', type=int, default=None)
    a = ap.parse_args()
    rng = random.Random(a.seed)
    n = 12 if a.quick else 45
    steps = a.steps or (2*10**6 if a.quick else 3*10**7)
    lmax = a.lmax or (60 if a.quick else 300)
    lx = a.lx or (12 if a.quick else 16)
    jcyc = a.jcyc or (26 if a.quick else 34)
    r = {'S relation': section_S(2*10**5 if a.quick else 2*10**6), 'A rules on twin': section_A(n, rng)}
    okC, okD = section_CD(steps)
    r['C init'] = okC; r['D cross-check+base'] = okD
    r['B base INV+(e), J'] = section_B()
    r['G twin orbit'] = section_G(lmax, jcyc)
    r['X coupling'] = section_X(lx, lmax)
    print('== SUMMARY:', ', '.join('%s %s' % (k, 'PASS' if v else 'FAIL') for k, v in r.items()), '->',
          'PASS' if all(r.values()) else 'FAIL',
          '| Simulation checks the claims of proof.md; the proof is the argument in proof.md (and the parent\'s).')
    sys.exit(0 if all(r.values()) else 1)