#!/usr/bin/env python3
"""check_twin.py: checks the twin-port analysis of 740 line 64 (P-64) against busycoq's
Sk1like_TC_v1.v Module TM1.  Result: the port is REFUTED.  This script checks every fact the
refutation in notes.md rests on.

  64  = 1RB0LC_0RC0RB_1LD0RE_0LE0LF_1LA0LB_1RA---
  TM1 = 1LB0RC_0LC0LB_1RD0LE_0RE1RF_1RA0RB_1RA---   (upstream, proved nonhalting)
  64f = flip(64) = 1LB0RC_0LC0LB_1RD0LE_0RE0RF_1RA0RB_1LA---   (TM1's frame: same state names)

Sections (each prints PASS/FAIL; SUMMARY is PASS only if all pass):
  M  relation: byte-exact holdout line 64; flip(64) differs from TM1 in exactly D1 and F0;
     line 124 is the same table renamed (TM3's renaming) and started in TM1's C.
  C  every case of RInc_spec / Inc_spec re-derived symbolically (busycoq `es` style: concrete
     steps, shift rules with a travelling context, the IH at the abstract tail):
       TM1's map on TM1: all 42 obligations;  64f: the 39 cases where TM1 never fires D1 derive
       unchanged, the 3 exit cases (the only ones that fire D1) do NOT; the twin map RIncF
       (3 changed exits + Tp3 = [0;1;1;0;0;1] + its 2 callers) derives on 64f: all 44 obligations.
  I  init: both machines reach toC x0 = (1, D0011 14 (D0011 5 D001T)) at step 1699, no D1 before.
  R  the concrete maps (TM1: RInc/Inc; 64f: RIncF/IncF) agree with direct TM simulation on
     random states (every exit case hit).
  S  step anchoring: line 64 itself (unflipped) from the blank tape to 6.5e6 steps: its F entries
     (39,734 / 841,213 / 6,436,652) fall in Inc steps 109 / 607 / 1746 of IncF.
  D  the divergence: from x0, the two abstract orbits give equal tapes except a 3-cell window
     after each of the first 6 exits and reconverge after exits 1-5; after exit 6 (Inc 528,713) they
     never reconverge: at Inc 529,337 TM1 makes D0011101 (its 7th exit fires at Inc 529,462) while
     64f merges the region into one w-block (374,704 cells differ).  TM1 reaches the cycle state S'
     at Inc 1,333,817; 64f does not.  The four critical Inc steps are re-run directly on the list
     strings (line 64 and the mirror of TM1).
  T  line 124 against TM3 (informational, same table): the same divergence, 15 Inc steps later.
  N  negative controls: wrong twin maps must fail C and R.
Usage: python3 -B check_twin.py [--quick]   (about 1-2 minutes; --quick skips S and shortens R)
"""
import os, sys, random, time
HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, HERE)
sys.setrecursionlimit(10000)
import symexec as S

ROOT = os.path.dirname(os.path.dirname(HERE))
L64 = '1RB0LC_0RC0RB_1LD0RE_0LE0LF_1LA0LB_1RA---'
L124 = '1RB0LC_0RC0RF_1RD0RE_1LE0RA_0LA0LE_1LD---'
TM1 = '1LB0RC_0LC0LB_1RD0LE_0RE1RF_1RA0RB_1RA---'
TM3 = '1RB0LC_0RC1RF_1RD0RE_1LE0RA_0LA0LE_1RD---'
T64F = S.flip_str(L64)
QUICK = '--quick' in sys.argv
results = []

def report(sec, ok, msg):
    results.append((sec, ok))
    print('%s %s  %s' % (sec, 'PASS' if ok else 'FAIL', msg), flush=True)

# ------------------------------------------------------------------ M
def sec_M():
    lines = open(os.path.join(ROOT, 'data/holdouts/BB6_holdouts_740.txt')).read().split('\n')
    report('M', lines[63] == L64, 'holdout line 64 is byte-exact %s' % L64)
    a, b = S.parse_tm(T64F), S.parse_tm(TM1)
    diff = sorted(k for k in a if a[k] != b[k])
    report('M', T64F == '1LB0RC_0LC0LB_1RD0LE_0RE0RF_1RA0RB_1LA---' and diff == [('D', 1), ('F', 0)],
           'flip(64) = %s differs from TM1 exactly at %s: D1 %s vs %s, F0 %s vs %s'
           % (T64F, diff, a[('D', 1)], b[('D', 1)], a[('F', 0)], b[('F', 0)]))
    phi = {'A': 'D', 'B': 'E', 'C': 'A', 'D': 'B', 'E': 'C', 'F': 'F'}   # TM1 state -> TM3 state
    def ren(tab):
        return {(phi[q], r): (None if t is None else (t[0], t[1], phi[t[2]])) for (q, r), t in tab.items()}
    ok = ren(S.parse_tm(TM1)) == S.parse_tm(TM3) and ren(S.parse_tm(T64F)) == S.parse_tm(L124) \
        and lines[123] == L124
    report('M', ok, 'TM3 = TM1 renamed (A,B,C,D,E,F -> D,E,A,B,C,F) and line 124 = 64f renamed the same way: '
           'one table, started in TM1-state A (64) and C (124)')

# ------------------------------------------------------------------ C
def derive(tmstr, twin):
    tab = S.parse_tm(tmstr); out = {}
    for lab, x, ih in S.rinc_cases(twin) + S.inc_cases(twin):
        if lab.startswith('Inc'): st, run, exp = S.run_inc_case(tab, x, ih, twin)
        else: st, run, exp = S.run_rinc_case(tab, x, ih, twin)
        d1 = sum(1 for t in run.trans if t == ('D', 1)) if run else 0
        out[lab] = (st.split(':')[0], d1, run)
    return out

EXITS = ['D00101 n=0, r=D00101 n0=1+c0', 'D01 n=1+c', 'D0011101 n=1+c']

def sec_C():
    t1 = derive(TM1, False)
    ok1 = [k for k, v in t1.items() if v[0] == 'ok']
    d1 = sorted(k for k, v in t1.items() if v[1])
    report('C', len(ok1) == 42 and all(v[0] in ('ok', 'skip') for v in t1.values()) and d1 == sorted(EXITS),
           "TM1's map on TM1: %d/%d obligations derive (%d inr cases need none); D1 fires only in %s"
           % (len(ok1), len(ok1), sum(v[0] == 'skip' for v in t1.values()), d1))
    tf = derive(T64F, False)
    same = sorted(k for k, v in tf.items() if v[0] == 'ok')
    bad = sorted(k for k, v in tf.items() if v[0] not in ('ok', 'skip'))
    report('C', len(same) == 39 and bad == sorted(EXITS),
           "TM1's map on 64f: %d obligations derive unchanged; the exit cases fail: %s" % (len(same), bad))
    tw = derive(T64F, True)
    okw = [k for k, v in tw.items() if v[0] == 'ok']
    report('C', len(okw) == 44 and all(v[0] in ('ok', 'skip') for v in tw.values()),
           'twin map RIncF on 64f: %d/%d obligations derive (new: Tp3 from D01, D00111|Tp3, Inc|Tp3)'
           % (len(okw), len(okw)))
    for k in EXITS:
        r1 = t1[k][2]; rf = tw[k][2]
        print('    %-30s TM1: %s %s  (%s steps)' % (k, r1.end[1], S.fmt(r1.end[2]), r1.steps))
        print('    %-30s 64f: %s %s  (%s steps)' % ('', rf.end[1], S.fmt(rf.end[2]), rf.steps))

# ------------------------------------------------------------------ I
def sec_I():
    W = list(S.W)
    tgt = W + [0, 0, 1, 1] + W * 14 + [0, 0, 1, 1] + W * 5 + [0, 0, 1]
    res = []
    for s in (TM1, T64F):
        tab = S.parse_tm(s); tape = {}; pos = 0; q = 'A'; steps = 0; d1 = 0; found = None
        while steps < 5000:
            if q == 'C':
                nz = [p for p, v in tape.items() if v]
                if nz and min(nz) >= pos:
                    seg = [tape.get(p, 0) for p in range(pos, max(max(nz) + 1, pos + len(tgt)))]
                    if seg[:len(tgt)] == tgt and not any(seg[len(tgt):]):
                        found = steps; break
            r = tape.get(pos, 0); t = tab[(q, r)]
            if (q, r) == ('D', 1): d1 += 1
            tape[pos] = t[0]; pos += 1 if t[1] == 'R' else -1; q = t[2]; steps += 1
        res.append((found, d1))
    report('I', res == [(1699, 0), (1699, 0)], 'toC x0 reached at step %s (TM1) and %s (64f); D1 firings before: %s, %s'
           % (res[0][0], res[1][0], res[0][1], res[1][1]))

# ------------------------------------------------------------------ R
W4 = [0, 0, 0, 1]
def tape_of(x):
    n, st = x
    out = W4 * n
    for d in st[::-1]:
        out += [0, 0, 1] if d == 'T' else S.RD[d[0]] + W4 * d[1]
    return out

def run_to(tab, start, target, cap=200000):
    tape = {i: v for i, v in enumerate(start)}; pos = 0; q = 'C'; steps = 0; tl = len(target)
    while steps < cap:
        r = tape.get(pos, 0); t = tab[(q, r)]
        if t is None: return 'halt'
        tape[pos] = t[0]; pos += 1 if t[1] == 'R' else -1; q = t[2]; steps += 1
        if q == 'C' and all(v == 0 or p >= pos for p, v in tape.items()):
            if [tape.get(p, 0) for p in range(pos, pos + tl)] == target and \
                    all(v == 0 or p < pos + tl for p, v in tape.items()):
                return 'ok'
    return 'cap'

def model_check(tmstr, twin, n, seed, inc=None):
    inc = inc or S.inc_c
    random.seed(seed); tab = S.parse_tm(tmstr); names = list(S.RD)
    ok = bad = 0; hits = {}
    for _ in range(n):
        st = ['T'] + [(random.choice(names), random.choice([0, 0, 1, 1, 2, 3, 5])) for _ in range(random.randint(1, 5))]
        x = [random.choice([0, 1, 1, 2, 3]), st]; x2 = [x[0], list(st)]; stats = {}
        try:
            inc(x2, twin, stats)
        except (S.Inr, S.TouchedTail):
            continue
        for k in stats:
            if k.startswith('EXIT') or '<-' in k: hits[k] = hits.get(k, 0) + 1
        if run_to(tab, tape_of(x), tape_of(x2)) == 'ok': ok += 1
        else: bad += 1
    return ok, bad, hits

def sec_R():
    n = 600 if QUICK else 2500
    for name, s, twin in (('TM1 map / TM1', TM1, False), ('RIncF / 64f', T64F, True)):
        ok, bad, hits = model_check(s, twin, n, 7)
        need = {'EXIT:D01', 'EXIT:D0011101'} | ({'Inc<-Tp3', 'D00111<-Tp3'} if twin else set())
        report('R', bad == 0 and ok > 0 and need <= set(hits),
               '%s: %d/%d random Inc steps match direct simulation; exit-case hits %s' % (name, ok, ok + bad, hits))

# ------------------------------------------------------------------ S
def sec_S():
    """Run line 64 itself (unflipped, mirror frame) from the blank tape; follow IncF's orbit by
    matching each predicted toC(x_k) (mirrored) when the machine is in C with nothing to its right."""
    tab = S.parse_tm(L64)
    trans = {k: (t[0], 1 if t[1] == 'R' else -1, t[2]) for k, t in tab.items() if t}
    x = S.x0_c(); targets = []
    for k in range(1800):
        X = tape_of(x); targets.append((bytes(X[::-1]), sum(X)))
        S.inc_c(x, True)
    N = 6500000; size = 60000; off = 50000
    tp = bytearray(size); h = off; q = 'A'; hi = off; ones = 0
    idx = 0; fent = []; at = {}
    for step in range(1, N + 1):
        r = tp[h]; w, d, nq = trans[(q, r)]
        ones += w - r; tp[h] = w
        if w and h > hi: hi = h
        h += d; q = nq
        if q == 'F': fent.append((step, idx))
        if q == 'C' and tp.find(1, h + 1, max(hi + 1, h + 1)) < 0:
            tgt, n1 = targets[idx]
            if n1 == ones and bytes(tp[h - len(tgt) + 1:h + 1]) == tgt:
                at[idx] = step; idx += 1
    want = [(39734, 109), (841213, 607), (6436652, 1746)]   # x_0..x_{k-1} matched: inside Inc step k
    report('S', fent == want and at.get(0) == 1699,
           'line 64 (unflipped) from blank: x0 at step %s; F entries (step, toC(x_k) states matched so far) %s, '
           'so they fall in Inc steps %s of IncF (exits 1-3 of D); %d orbit states matched to 6.5e6 steps'
           % (at.get(0), fent, [k for _, k in fent], idx))

# ------------------------------------------------------------------ D
def tape_str(x):
    n, st = x
    return '0001' * n + ''.join('001' if d == 'T' else ''.join(map(str, S.RD[d[0]])) + '0001' * d[1] for d in st[::-1])

def ndiff(ta, tb):
    if len(ta) != len(tb): return -1
    if ta == tb: return 0
    c = 0; i = 0; L = len(ta); stp = 4096
    while i < L:
        if ta[i:i + stp] != tb[i:i + stp]:
            c += sum(1 for j in range(i, min(L, i + stp)) if ta[j] != tb[j])
        i += stp
    return c

def orbit_compare(x0, steps, label):
    a = [x0[0], list(x0[1])]; b = [x0[0], list(x0[1])]
    exa, exb, events = [], [], []
    active = False; prevd = 0; diverged = None; before = None
    for k in range(1, steps + 1):
        pa = [a[0], list(a[1])] if active else None
        sa, sb = {}, {}
        S.inc_c(a, False, sa); S.inc_c(b, True, sb)
        ea = any(x.startswith('EXIT') for x in sa); eb = any(x.startswith('EXIT') for x in sb)
        if ea: exa.append(k)
        if eb: exb.append(k)
        if diverged is None and (ea or eb or active):
            d = ndiff(tape_str(a), tape_str(b))
            if d != prevd: events.append((k, d))
            if d > 16 or d < 0:
                diverged = (k, d, pa, [a[0], list(a[1])], [b[0], list(b[1])])
            active = d != 0
            prevd = d
    return a, b, exa, exb, events, diverged

S_PAT = [('D0011', 33), ('D00001', 416889), ('D00001', 0), ('D0000101', 31217)]

def is_Sprime(x):
    return x[0] == 1 and [d for d in x[1][::-1][:4]] == S_PAT

def sec_D():
    t0 = time.time()
    a, b, exa, exb, events, dv = orbit_compare(S.x0_c(), 1333817, '64')
    re_ok = [e for e in events if e[0] < 528713]
    pairs = [(re_ok[i][0], re_ok[i + 1][0]) for i in range(0, len(re_ok) - 1, 2)]
    ok = (exa[:6] == exb[:6] == [109, 607, 1746, 207707, 370719, 528713]
          and len(pairs) == 5 and all(e[1] in (3, 0) for e in re_ok)
          and dv is not None and dv[0] == 529337 and dv[1] == 374704
          and 529462 in exa and 529462 not in exb)
    report('D', ok, 'exits 1-6 at Inc %s in both; 3-cell defect windows %s each close again (diff 0); '
           'first macroscopic divergence at Inc %s (%s differing cells); TM1 exit 7 at Inc 529462 has no twin '
           'counterpart (twin exits: %s)' % (exa[:6], pairs, dv[0] if dv else None, dv[1] if dv else None, exb))
    if dv:
        print('    before Inc %d   TM1: %s' % (dv[0], S.fmt_c(dv[2], 8)))
        print('    after           TM1: %s' % S.fmt_c(dv[3], 8))
        print('    after           64f: %s' % S.fmt_c(dv[4], 8))
    report('D', is_Sprime(a) and not is_Sprime(b) and len(exa) == 38 and len(exb) == 9,
           "after Inc_Sn 1333816 (1,333,817 Inc steps): TM1 is S' = %s (the upstream proof's cycle state); "
           '64f is %s; exits so far: TM1 %d, 64f %d  (%.0fs)'
           % (S.fmt_c(a, 4), S.fmt_c(b, 4), len(exa), len(exb), time.time() - t0))
    # direct TM-level re-run of the critical Inc steps on the actual list strings
    sys.path.insert(0, HERE)
    TM1M = S.flip_str(TM1)
    allok = True; lines = []
    for twin, tmstr, name in ((True, L64, 'line 64'), (False, TM1M, 'mirror(TM1)')):
        x = S.x0_c(); k = 0
        for target in (109, 528713, 529337, 529462):
            while k < target - 1:
                S.inc_c(x, twin); k += 1
            xb = [x[0], list(x[1])]; st = {}
            S.inc_c(x, twin, st); k += 1
            res, nsteps, fe = tm_inc(tmstr, xb, x)
            ex = any(s.startswith('EXIT') for s in st)
            allok &= res == 'ok' and (fe > 0) == ex
            lines.append('%s Inc %d: %s in %d steps, F entries %d, model exit %s' % (name, k, res, nsteps, fe, ex))
    report('D', allok, 'critical Inc steps re-run on the list strings (mirror frame): ' + '; '.join(lines))

def tm_inc(tmstr, x, xn, cap=10 ** 8):
    tab = S.parse_tm(tmstr)
    trans = {k: ((t[0], 1 if t[1] == 'R' else -1, t[2]) if t else None) for k, t in tab.items()}
    X = tape_of(x); Xn = tape_of(xn); M = 64
    size = len(X) + 2 * M + 16; tp = bytearray(size); h0 = len(X) - 1 + M
    for i, v in enumerate(X): tp[h0 - i] = v
    h = h0; q = 'C'; steps = 0; fe = 0; tgt = bytes(Xn[::-1]); ones = sum(Xn)
    while steps < cap:
        t = trans[(q, tp[h])]
        if t is None: return 'HALT', steps, fe
        tp[h] = t[0]; h += t[1]; q = t[2]; steps += 1
        if q == 'F': fe += 1
        if q == 'C' and h >= h0 - 12:
            lo = h - len(Xn) + 1
            if lo >= 0 and bytes(tp[lo:h + 1]) == tgt and sum(tp) == ones:
                return 'ok', steps, fe
        if h <= 0 or h >= size - 1: return 'offtape', steps, fe
    return 'cap', steps, fe

# ------------------------------------------------------------------ T
def sec_T():
    a, b, exa, exb, events, dv = orbit_compare([1, ['T', ('D0011', 15)]], 600000, '124')
    report('T', dv is not None and dv[0] == 529352 and exa[:6] == exb[:6] and exa[6] == 529477 and 529477 not in exb,
           'INFORMATIONAL (line 124 vs TM3, x0 = (1, D0011 15 D001T)): exits 1-6 at Inc %s in both; '
           'divergence at Inc %s (%s cells); TM3 exit 7 at Inc %s missing in 124'
           % (exa[:6], dv[0] if dv else None, dv[1] if dv else None, exa[6]))

# ------------------------------------------------------------------ N
def sec_N():
    # (1) a wrong twin map: keep the TM1 exit digit D0000101 in the D0011101 exit
    orig = S.rinc_c
    def wrong(st, twin, stats=None, depth=0):
        top = st[-1]
        if twin and isinstance(top, tuple) and top[0] == 'D0011101' and top[1] > 0:
            st[-1] = ('D0000101', top[1] - 1); return 0, 2
        return orig(st, twin, stats, depth)
    S.rinc_c = wrong
    try:
        ok, bad, _ = model_check(T64F, True, 300, 11, inc=S.inc_c)
    finally:
        S.rinc_c = orig
    report('N', bad > 0, 'wrong twin map (D0011101 exit -> D0000101) is caught by R: %d mismatches' % bad)
    # (2) TM1's derivation applied to the twin's table must fail the exit cases (already C), and
    #     the twin map applied to TM1's table must fail them too
    tw_on_tm1 = derive(TM1, True)
    bad2 = sorted(k for k, v in tw_on_tm1.items() if v[0] not in ('ok', 'skip'))
    report('N', bad2 == sorted(EXITS), 'twin map on TM1 fails exactly the exit cases: %s' % bad2)
    # (3) a sabotaged executor table (F0 = 1RA on 64f, i.e. TM1's F0 with 64's D1) must fail C
    sab = T64F[:-6] + '1RA---'
    sb = derive(sab, True)
    bad3 = sorted(k for k, v in sb.items() if v[0] not in ('ok', 'skip'))
    report('N', len(bad3) > 0, 'sabotaged table %s fails %d twin-map obligations' % (sab, len(bad3)))

if __name__ == '__main__':
    t0 = time.time()
    sec_M(); sec_C(); sec_I(); sec_R()
    if not QUICK: sec_S()
    sec_D(); sec_T(); sec_N()
    allok = all(ok for _, ok in results)
    print('SUMMARY: %s  (%d checks; verdict: twin port of Sk1like_TC_v1 TM1 REFUTED for line 64; %.0fs)'
          % ('PASS' if allok else 'FAIL', len(results), time.time() - t0))