#!/usr/bin/env python3
"""check_proof.py -- evidence for the DELTA proof (proof.md) of
1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---   (line 388 of the 778 list)

Parent: kill #33  1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---  (KILLED_NONHALT, check_kill PASS).
The parent's check_proof.py is imported READ-ONLY (python -B; nothing is written there) for its abstract
macro model (mstep, inv, derived, render, parse_digits, k_of_tape's regex), its random-INV generator, its
chain builders and its pure-abstract checks. Everything that depends on the machine or the start is
re-run here on THIS machine's own table, with its own simulator, with the head state of K renamed to D.

  python3 -B check_proof.py [--seed S] [--tm-steps T] [--orbit N] [--induct N] [--lockstep N] [--quick]

Sections (each prints PASS/FAIL with counts):
  S  identity    line 388 byte for byte; 26 snapshots; sheet rows; not on data/discord lists; eqv group;
                 sigma = BCDAEF (no mirror) is the ONLY map (720 perms x mirror) taking #33's table to this one,
                 and it takes #33's state D to A; #11 -> this: CDABEF + mirror, start C (also unique)
  R  lockstep    Lemma R on the real machines: this machine from blank vs #33 from 0^inf D> 0^inf, every
                 step: state = sigma(parent state), same symbol written, same move (--lockstep steps)
  L  lemmas      #33's 20 window lemmas (proof.md 2.1 there) with states renamed by sigma: exact on THIS table,
                 never reading outside the window; F entered only by E1, only in T4/T9/T13, reading 0
  A  rules       M (700) and O (350) random K-configs on THIS table, head state D: exact tape and step count,
                 rightmost cell read as stated; random INV states, one macro step on THIS table (3000)
  H  chains      #33's M and O chains (its proof.md 2.2/2.3), every link renamed by sigma and run on THIS table:
                 whole tape, head and state after every link (same boxes as #33's checks 12/13)
  C  init        blank -> the K-configs at steps 101, 234, 326, 426 (none in INV) -> K((1,1,9); 8, 1) at step
                 687, class A, with the derived quantities; the next macro step (O, 245 steps) -> class B
  D  closure     the real machine from blank vs the abstract model at every macro boundary from step 687 up to
                 --tm-steps (whole tape, head, state), INV at each boundary
  B  base        INV at K((1,1,9); 8, 1) in the parent's set form (inv) and in the Rocq additive form of the
                 parent's .v (INV/PA/Rof, evaluated clause by clause)
  G  orbit       abstract orbit from the base: INV at every macro state (--orbit macro steps); plus the
                 parent's start-independent abstract checks (induction on random INV states, drop algebra)
  X  coupling    (explanation only) the macro orbit vs kill #11's: from macro step 54 on, equal except one
                 exponent +3 on the top digit, same rule at every step (--orbit macro steps)
  V  rocq delta  rocq/delta_check.v is exactly the parent's .v (sha256 pinned) with the delta of proof.md 5
                 (TM string, sigma on every {{X}}, init/base [d1 1 9] 8 1, comments), and rocq/delta_check.out
                 is a clean compile record of that exact file (exit 0, Closed under the global context)
"""
import sys, os, re, random, argparse, itertools, hashlib, importlib.util, glob, csv
from collections import Counter
sys.dont_write_bytecode = True

TW = "1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---"
PARENT = "1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---"
ROOT = "[local working file]"
PDIR = os.path.join(ROOT, "machines", PARENT)
HERE = os.path.dirname(os.path.abspath(__file__))
PARENT_V_SHA = "37cb180280f0896396a28bb32a548a6bfdd22d0b47b2f526230ed2208dbb2053"

_spec = importlib.util.spec_from_file_location("parent_check_proof", os.path.join(PDIR, "check_proof.py"))
P = importlib.util.module_from_spec(_spec)
_spec.loader.exec_module(P)            # read-only import: P.TT is the PARENT's table, never used for the twin
assert P.TM == PARENT

SIG = {'A': 'B', 'B': 'C', 'C': 'D', 'D': 'A', 'E': 'E', 'F': 'F'}     # parent state -> twin state
KQ = SIG['C']                                                          # head state of K on the twin: D
TT = P.parse_tm(TW)

# ---------------------------------------------------------------- the twin's own simulator
def run(cells, head, state, n):
    """as the parent's run(), but on THIS table."""
    pad = n + 8
    t = bytearray(pad) + bytearray(int(c) for c in cells) + bytearray(pad)
    h = head + pad; st = ord(state) - 65; mn = mx = h; tab = TT
    for _ in range(n):
        tr = tab[st][t[h]]
        if tr is None:
            raise P.Halt()
        t[h] = tr[0]; h += tr[1]; st = tr[2]
        if h < mn: mn = h
        if h > mx: mx = h
    return ''.join('01'[x] for x in t), h, chr(st + 65), mn - pad, mx - pad

def render(D, a, b):
    s, h, q = P.render(D, a, b)
    assert q == 'C'
    return s, h, KQ

def k_of_tape(tape, h, st):
    """K-configuration of the twin: state D, head on a blank with only blanks to its left, tape parses."""
    if st != ord(KQ) - 65:
        return None
    return P.k_of_tape(tape, h, 2)       # the parent's parser, called with the parent's head-state index

def scan_K(T):
    tape = bytearray(2 * T + 16); h = T + 8; s = 0; out = []
    for t in range(0, T + 1):
        if t > 0:
            tr = TT[s][tape[h]]
            if tr is None:
                return out, t
            tape[h] = tr[0]; h += tr[1]; s = tr[2]
        if s == ord(KQ) - 65 and tape[h] == 0 and tape[h - 1] == 0:
            k = k_of_tape(tape, h, s)
            if k:
                out.append((t, k))
    return out, None

def report(name, ok, tot, extra=''):
    print('%-13s %s  %d/%d %s' % (name, 'PASS' if ok == tot else 'FAIL', ok, tot, extra))
    sys.stdout.flush()
    return ok == tot

# ---------------------------------------------------------------- S identity
def check_identity():
    ok = tot = 0
    def chk(c, msg):
        nonlocal ok, tot
        tot += 1; ok += bool(c)
        if not c: print('  identity FAIL:', msg)
    hol = os.path.join(ROOT, 'data/holdouts/2026-10-07_778.txt')
    lines = open(hol).read().split('\n')
    chk(len(lines) > 388 and lines[387] == TW and sum(x == TW for x in lines) == 1, 'line 388 of the 778 list')
    snaps = sorted(f for f in glob.glob(os.path.join(os.path.dirname(hol), '*.txt')) if 'eqv' not in f)
    chk(len(snaps) == 26 and all(TW in set(x.strip() for x in open(f)) for f in snaps), 'all 26 snapshots')
    sheet = os.path.join(ROOT, 'data/sheet/')
    rows = {}
    for f in glob.glob(sheet + '*.csv'):
        for i, row in enumerate(csv.reader(open(f, encoding='utf-8', errors='replace'))):
            for j, cell in enumerate(row):
                if TW in cell:
                    rows.setdefault(os.path.basename(f), []).append((i + 1, j, row[j], len(row)))
    res = [r for r in csv.reader(open(sheet + '2026-10-09_results.csv')) if r and r[0] == TW]
    chk(res == [[TW, '', 'Skelet 1-like Class 2', '', '', '']], 'Results row: class only, %s' % res)
    chk(set(rows) == {'2026-10-09_results.csv', '2026-10-09_classifications.csv'},
        'sheet tabs naming it: %s' % sorted(rows))
    dis = glob.glob(os.path.join(ROOT, 'data/discord/*.txt'))
    chk(len(dis) == 2 and not any(TW in open(f).read() for f in dis), 'not on the data/discord lists')
    groups = [g.split() for g in open(os.path.join(os.path.dirname(hol), '2026-10-07_eqv_1590.txt')).read()
              .replace('\r', '').split('\n\n') if g.strip()]
    g = [x for x in groups if TW in x]
    eqvE, eqvF = '1RB1RF_1RC0RA_1LD0RA_1LE0LE_1RB0LD_1RB---', '1RB---_1RC0RF_1LD0RF_1LE0LE_1RB0LD_1RB1RA'
    chk(g == [[TW, eqvE, eqvF]], 'eqv group %s' % g)
    # the eqv members are the same table started in #33's E and F (no mirror)
    for s, x in (('E', eqvE), ('F', eqvF)):
        hit = [(perm, mir) for perm in itertools.permutations(range(6)) for mir in (False, True)
               if P.relabel(P.TT, list(perm), mir) == x]
        chk(len(hit) == 1 and not hit[0][1] and chr(65 + hit[0][0].index(0)) == s,
            'eqv member %s = #33 from %s: %s' % (x, s, hit))
    # sigma: the only relabeling of #33's table giving this string; it sends #33's D to A
    hits = [(''.join(chr(65 + p) for p in perm), mir, chr(65 + perm.index(0)))
            for perm in itertools.permutations(range(6)) for mir in (False, True)
            if P.relabel(P.TT, list(perm), mir) == TW]
    chk(hits == [('BCDAEF', False, 'D')], 'maps #33 -> this: %s' % hits)
    chk([ord(SIG[c]) - 65 for c in 'ABCDEF'] == [1, 2, 3, 0, 4, 5], 'SIG = BCDAEF')
    # cell by cell: twin row sigma(s) = parent row s with targets renamed (12/12)
    cells = 0
    for s in range(6):
        for sym in (0, 1):
            pt = P.TT[s][sym]; tt = TT[ord(SIG[chr(65 + s)]) - 65][sym]
            if pt is None: cells += tt is None
            else: cells += tt == (pt[0], pt[1], ord(SIG[chr(65 + pt[2])]) - 65)
    chk(cells == 12, 'cell by cell %d/12' % cells)
    hits11 = [(''.join(chr(65 + p) for p in perm), mir, chr(65 + perm.index(0)))
              for perm in itertools.permutations(range(6)) for mir in (False, True)
              if P.relabel(P.parse_tm(P.TM11), list(perm), mir) == TW]
    chk(hits11 == [('CDABEF', True, 'C')], 'maps #11 -> this: %s' % hits11)
    # halting cell: only E1 enters F, F1 is the only undefined transition (both fixed by sigma)
    into_F = [(chr(65 + s), sym) for s in range(6) for sym in (0, 1) if TT[s][sym] and TT[s][sym][2] == 5]
    undef = [(chr(65 + s), sym) for s in range(6) for sym in (0, 1) if TT[s][sym] is None]
    chk(into_F == [('E', 1)] and undef == [('F', 1)], 'into F %s, undefined %s' % (into_F, undef))
    return report('S identity', ok, tot, '(line 388; 26 snapshots; sheet: Results class only + Classifications; '
                  'not on discord lists; eqv group {this, #33 from E, #33 from F}; sigma = BCDAEF, no mirror, the '
                  'only map, start = #33\'s D; = #11 mirrored CDABEF from C; halting cell E1 -> F1)')

# ---------------------------------------------------------------- R lockstep (Lemma R on the real machines)
def check_lockstep(N):
    n = N + 8
    t1 = bytearray(2 * n); t2 = bytearray(2 * n); h1 = h2 = n
    s1 = 0; s2 = 3                                         # twin from A; parent from D
    sig = [ord(SIG[chr(65 + i)]) - 65 for i in range(6)]
    tw, pa = TT, P.TT
    ok = 0
    for i in range(N):
        if s1 != sig[s2]:
            break
        a = tw[s1][t1[h1]]; b = pa[s2][t2[h2]]
        if a is None or b is None or a[0] != b[0] or a[1] != b[1]:
            break
        t1[h1] = a[0]; h1 += a[1]; s1 = a[2]
        t2[h2] = b[0]; h2 += b[1]; s2 = b[2]
        ok += 1
    same = ok == N and t1 == t2 and h1 == h2 and s1 == sig[s2]
    return report('R lockstep', ok + same, N + 1, '(this machine from blank = sigma(#33 from 0^inf D> 0^inf) at every '
                  'step to %d: state, symbol, move; final tapes identical)' % N)

# ---------------------------------------------------------------- L lemmas
def ren_window(w):
    i = w.find('>')
    if i > 0 and w[i - 1] in 'ABCDEF':
        return w[:i - 1] + SIG[w[i - 1]] + w[i:]
    i = w.find('<')
    return w[:i + 1] + SIG[w[i + 1]] + w[i + 2:]

def lemma_run(lhs, rhs, n):
    c, h, st = P.parse_window(lhs); c2, h2, st2 = P.parse_window(rhs)
    t = [int(x) for x in c]; s = ord(st) - 65; good = len(c) == len(c2); trs = []; fr = []
    for _ in range(n):
        if not (0 <= h < len(t)) or TT[s][t[h]] is None:
            return False, trs, fr
        trs.append(chr(s + 65) + str(t[h]))
        if s == 5: fr.append(t[h])
        w, d, s = TT[s][t[h]]; t[h] = w; h += d
    good = good and ''.join(map(str, t)) == c2 and h == h2 and s == ord(st2) - 65
    return good, trs, fr

def check_lemmas():
    ok = 0; fs = []; lines = []
    for name, (lhs, rhs, n) in P.LEM.items():
        L2, R2 = ren_window(lhs), ren_window(rhs)
        good, trs, fr = lemma_run(L2, R2, n)
        # the parent's lemma holds on the parent's table with the sigma-preimage transitions
        pg, ptrs, _ = P.lemma_run(lhs, rhs, n)
        good = good and pg and [SIG[x[0]] + x[1] for x in ptrs] == trs
        ok += good
        fs += [(name, x) for x in fr]
        lines.append('    %-4s %-10s -> %-10s %2d  %s' % (name, L2, R2, n, ' '.join(trs)))
        if not good: print('  lemma FAIL', name, L2, R2)
    fok = all(x == 0 for _, x in fs) and sorted({nm for nm, _ in fs}) == ['T13', 'T4', 'T9']
    for x in lines: print(x)
    return report('L lemmas', ok + fok, len(P.LEM) + 1, '(20 windows of #33 renamed by sigma, exact on this table, '
                  'transitions = sigma of #33\'s; F entered only in T4/T9/T13, reading 0)')

# ---------------------------------------------------------------- A rules on the twin's table
def check_rules(r, NM, NO, NI, big=300):
    okM = okO = okI = 0; drops = 0; zero_u = 0
    for it in range(NM):
        k = it % 7
        pre = [P.rand_digit(r, r.randint(0, 1), big) for _ in range(r.randint(0, 3))]
        flip = P.rand_digit(r, 0, big)
        if r.random() < 0.25: flip = (0, 0, flip[2])
        if r.random() < 0.25: flip = (flip[0], 0, 1)
        ones = [P.rand_digit(r, 1, big) for _ in range(k)]
        D = pre + [flip] + ones
        a = P.rnd(r, 0, big); b = P.rnd(r, 0, big)
        name, D2, a2, b2, steps, info = P.mstep(D, a, b)
        s, h, q = render(D, a, b)
        res = run(s, h, q, steps)
        i00r = len(s) - 4 - sum(len(P.dig(d)) for d in pre) - 2 * flip[0] - 1
        g = P.same_cfg(res, *render(D2, a2, b2)) and res[4] == i00r
        okM += g; drops += info['drop'] is not None; zero_u += flip[0] == 0
        if not g: print('  M FAIL', D, a, b)
    for it in range(NO):
        n = 1 + it % 7
        D = [P.rand_digit(r, 1, big) for _ in range(n)]
        a = P.rnd(r, 1, big); b = P.rnd(r, 0, big)
        name, D2, a2, b2, steps, _ = P.mstep(D, a, b)
        s, h, q = render(D, a, b)
        res = run(s, h, q, steps)
        g = P.same_cfg(res, *render(D2, a2, b2)) and res[4] == len(s) - 1 + 3
        okO += g
        if not g: print('  O FAIL', D, a, b)
    totI = 0
    for it in range(NI):
        cls = 'ABC'[it % 3]
        m = 1 + r.randint(0, 5)
        if cls == 'B' and m < 2: m = 2
        st = P.rand_inv_state(r, cls, m, 12)
        if st is None: continue
        D, a, b = st
        if sum(u + v for (u, _, v) in D) + a + b > 400: continue
        name, D2, a2, b2, steps, info = P.mstep(D, a, b)
        totI += 1; okI += P.same_cfg(run(*render(D, a, b), steps), *render(D2, a2, b2))
    return report('A rules', okM + okO + okI, NM + NO + totI,
                  '(on this table, head state D: M %d/%d (k=0..6, %d drops, %d with u*=0; rightmost read = right 0 of '
                  'the flipped 00), O %d/%d (m=1..7; rightmost read = 3 right of the old 1001), random INV states one '
                  'macro step %d/%d)' % (okM, NM, drops, zero_u, okO, NO, okI, totI))

# ---------------------------------------------------------------- H chains, renamed link by link
def run_chain(c0, ln, margin=64):
    """the parent's run_chain, on THIS table, with every link's state renamed by sigma."""
    l, mo, st, r = c0
    n = sum(P.LEM[nm][2] * k for (nm, k, _) in ln)
    E = margin + n + len(l + r) + 8; size = E + margin
    def place(l, r):
        f = l + r; w = bytearray(size); w[E - len(f):E] = bytes(int(x) for x in f); return w
    def hpos(l, mo, r):
        return E - len(r) if mo == '>' else E - len(r) - 1
    t = place(l, r); h = hpos(l, mo, r); s = ord(SIG[st]) - 65; mx = h; tot = 0
    for (nm, k, (l2, mo2, st2, r2)) in ln:
        for _ in range(P.LEM[nm][2] * k):
            tr = TT[s][t[h]]
            if tr is None:
                return False, tot, None
            t[h] = tr[0]; h += tr[1]; s = tr[2]; tot += 1
            if h > mx: mx = h
            if h < 0 or h >= size:
                return False, tot, None
        if t != place(l2, r2) or h != hpos(l2, mo2, r2) or s != ord(SIG[st2]) - 65:
            return False, tot, None
    return True, tot, E - 1 - mx

def _M_case(pre, us, vs, ones, a, b):
    c0, ln, right00 = P.M_chain(pre, us, vs, ones, a, b)
    good, steps, mxoff = run_chain(c0, ln)
    D = pre + [(us, 0, vs)] + [(u, 1, v) for (u, v) in ones]
    _, D2, a2, b2, st, _ = P.mstep(D, a, b)
    lf, mof, stf, rf = ln[-1][2]
    return good and steps == st and mxoff == right00 and lf == '' and mof == '<' and SIG[stf] == KQ \
        and rf == render(D2, a2, b2)[0]

def _O_case(ones, a, b):
    c0, ln = P.O_chain(ones, a, b)
    good, steps, mxoff = run_chain(c0, ln)
    if ones:
        _, D2, a2, b2, st, _ = P.mstep([(u, 1, v) for (u, v) in ones], a, b)
    else:
        D2, a2, b2, st = [(1, 1, a)], b + 3, 1, 89 + 8 * a + 20 * b
    lf, mof, stf, rf = ln[-1][2]
    return good and steps == st and mxoff == 0 and lf == '' and mof == '<' and SIG[stf] == KQ \
        and rf == render(D2, a2, b2)[0]

def check_chains(r, quick):
    ok = tot = 0
    kmax = 2 if quick else 3
    for pre in [[], [(1, 1, 1)], [(0, 0, 2)], [(2, 1, 3), (1, 0, 1)]]:
        for us in range(3):
            for vs in range(1, 4):
                for k in range(kmax + 1):
                    for ones in itertools.product([(u, v) for u in (1, 2) for v in (1, 2)], repeat=k):
                        for a in range(4):
                            for b in range(3):
                                tot += 1; g = _M_case(pre, us, vs, list(ones), a, b); ok += g
                                if not g: print('  M chain FAIL', pre, us, vs, ones, a, b)
    for _ in range(100 if quick else 500):
        pre = [P.rand_digit(r, r.randint(0, 1), 30) for _ in range(r.randint(0, 3))]
        ones = [(P.rnd(r, 1, 60), P.rnd(r, 1, 60)) for _ in range(r.randint(0, 7))]
        args = (pre, P.rnd(r, 0, 60), P.rnd(r, 1, 60), ones, P.rnd(r, 0, 300), P.rnd(r, 0, 300))
        tot += 1; g = _M_case(*args); ok += g
        if not g: print('  M chain FAIL', args)
    mt, mo = tot, ok
    mmax = 3 if quick else 4
    for m in range(0, mmax + 1):
        rng = (1, 2, 3) if m <= 3 else (1, 2)
        for ones in itertools.product([(u, v) for u in rng for v in rng], repeat=m):
            for a in range(1, 5 if m == 0 else 4):
                for b in range(5 if m == 0 else 3):
                    tot += 1; g = _O_case(list(ones), a, b); ok += g
                    if not g: print('  O chain FAIL', ones, a, b)
    for _ in range(60 if quick else 300):
        ones = [(P.rnd(r, 1, 60), P.rnd(r, 1, 60)) for _ in range(r.randint(0, 8))]
        args = (ones, P.rnd(r, 1, 300), P.rnd(r, 0, 300))
        tot += 1; g = _O_case(*args); ok += g
        if not g: print('  O chain FAIL', args)
    i0 = _O_case([], 9, 5)                    # the init's last leg: K(; 9, 5) -> K((1,1,9); 8, 1)
    return report('H chains', ok + i0, tot + 1, '(#33\'s chains renamed by sigma, link by link on this table: M %d/%d '
                  '(box + 500 random), O %d/%d (box m=0..%d + 300 random), plus the init leg K(;9,5) -> K((1,1,9);8,1))'
                  % (mo, mt, ok - mo, tot - mt, mmax))

# ---------------------------------------------------------------- C init
BASE = ([(1, 1, 9)], 8, 1)
T0 = 687

def check_init():
    ok = tot = 0
    def chk(c, msg):
        nonlocal ok, tot
        tot += 1; ok += bool(c)
        if not c: print('  init FAIL:', msg)
    ks, halted = scan_K(T0)
    want = [(101, ([(1, 1, 1)], 2, 1)), (234, ([(0, 0, 1), (1, 1, 2)], 4, 1)), (326, ([(2, 0, 1)], 5, 3)),
            (426, ([], 9, 5)), (687, BASE)]
    chk(halted is None and ks == want, 'K-configs in 0..687: %s' % ks)
    chk([P.inv(*k) for _, k in ks] == [None, None, None, None, 'A'], 'only the last is in INV')
    # why the first four are not in INV (the parent's derived quantities)
    d101 = P.derived(*want[0][1]); d234 = P.derived(*want[1][1])
    chk(d101['S'] == 0, 'step 101: S = %d (class A needs S >= 1)' % d101['S'])
    chk(d234['per'][-1][6] == 0, 'step 234: LSB vbar = %d (Common needs >= 1)' % d234['per'][-1][6])
    chk(len(want[2][1][0]) == 1 and want[2][1][0][0][2] == 1, 'step 326: the only digit is bit 0 with v = 1 (LSB drop next)')
    chk(want[3][1][0] == [], 'step 426: no digits (m = 0)')
    # the macro steps between them are the parent's rules (incl. the LSB-drop and m = 0 cases, init only)
    s, h, q = render(*want[0][1])
    chain = []
    for (t1, k1), (t2, k2) in zip(want, want[1:]):
        D, a, b = k1
        if D:
            nm, D2, a2, b2, st, info = P.mstep(D, a, b)
        else:
            nm, D2, a2, b2, st, info = 'O(m=0)', [(1, 1, a)], b + 3, 1, 89 + 8 * a + 20 * b, {}
        chain.append(nm + ('/' + info['drop'] if info.get('drop') else ''))
        chk((D2, a2, b2) == k2 and t1 + st == t2, '%s at %d -> %s' % (nm, t1, k2))
    chk(chain == ['O', 'M1/top', 'M0/LSB', 'O(m=0)'], 'init legs %s' % chain)
    # direct runs: blank -687-> base, exact whole tape
    chk(P.same_cfg(run('', 0, 'A', T0), *render(*BASE)), 'blank -687-> K((1,1,9);8,1)')
    # parent from D gives the same K list (Lemma R), via the parent's own scan_K
    pks, ph = P.scan_K('D', T0)
    chk(ph is None and pks == want, 'parent from D: same K list')
    D, a, b = BASE
    dv = P.derived(D, a, b); (u, beta, v, R, R1, ub, vb), = dv['per']
    chk((dv['V'], dv['Rtot'], dv['S'], dv['T'], R, R1, ub, vb) == (1, 0, 6, 0, 0, 0, 1, 9), 'derived %s' % dv)
    chk(P.inv(D, a, b) == 'A', 'class A')
    nm, D2, a2, b2, st, _ = P.mstep(D, a, b)
    chk((nm, D2, a2, b2, st) == ('O', [(0, 0, 1), (9, 1, 8)], 4, 1, 245) and P.inv(D2, a2, b2) == 'B',
        'next: O -> K((0,0,1),(9,1,8);4,1), class B: %s' % ((nm, D2, a2, b2, st),))
    chk(P.same_cfg(run(*render(D, a, b), st), *render(D2, a2, b2)), 'next step on the machine')
    return report('C init', ok, tot, '(blank: K at 101 O-> 234 M1(top drop)-> 326 M0(LSB drop)-> 426 (m=0) O(m=0)-> '
                  '687 = K((1,1,9);8,1), class A: V=1, R=0, S=6, T=0, ubar=1, vbar=9; the first four not in INV; '
                  'parent from D identical; next O (245 steps) -> K((0,0,1),(9,1,8);4,1), class B)')

# ---------------------------------------------------------------- D closure
def check_closure(Tmax):
    import math
    L = int(4 * math.sqrt(max(Tmax, 1))) + 20000; Rpad = 20000
    tape = bytearray(L + Rpad); h = L; s = 0; tab = TT
    tr01 = bytes.maketrans(b'01', b'\x00\x01')
    state = {'h': h, 's': s}
    def go(n):
        t_ = tape; hh = state['h']; ss = state['s']
        for _ in range(n):
            tr = tab[ss][t_[hh]]
            if tr is None:
                raise P.Halt()
            t_[hh] = tr[0]; hh += tr[1]; ss = tr[2]
        state['h'] = hh; state['s'] = ss
    def matches(D, a, b):
        st_, _, q = render(D, a, b)
        if state['s'] != ord(KQ) - 65:
            return False
        seg = st_.encode().translate(tr01); hh = state['h']
        return tape[hh + 1:hh + 1 + len(seg)] == seg and not any(tape[:hh + 1]) and tape.count(1) == st_.count('1')
    go(T0)
    (D, a, b), t = BASE, T0
    n = ok = int(matches(D, a, b)); names = Counter(); cls = Counter(); drops = Counter()
    while True:
        c = P.inv(D, a, b); cls[c] += 1
        if c is None:
            print('  closure: INV fails at', t); ok -= 1; break
        name, D2, a2, b2, st, info = P.mstep(D, a, b)
        if t + st > Tmax:
            break
        go(st)
        D, a, b, t = D2, a2, b2, t + st
        g = matches(D, a, b)
        n += 1; ok += g
        names[name if name == 'O' or int(name[1:]) < 6 else 'M6+'] += 1
        if info.get('drop'): drops[info['drop']] += 1
        if not g:
            print('  closure FAIL at step', t, name); break
    return report('D closure', ok, n, '(K at 687 + every macro step of the real run to step %d: %s; drops %s; '
                  'INV classes %s; last K: m=%d, a=%d, b=%d)' % (t, dict(names), dict(drops),
                  {str(k): v for k, v in cls.items()}, len(D), a, b))

# ---------------------------------------------------------------- B base, both forms
def check_base():
    ok = tot = 0
    def chk(c, msg):
        nonlocal ok, tot
        tot += 1; ok += bool(c)
        if not c: print('  base FAIL:', msg)
    D, a, b = BASE
    chk(P.inv(D, a, b) == 'A', 'set form: class A')
    # Rocq additive form (the parent's .v, Definition INV / PA / Rof / LSBok), ds = [d1 1 9] (LSB first)
    u, v = 1, 9; m = 1
    Rof = 0                                          # Rof (d1 _ _ :: []) = 2 * Rof [] = 0
    Rd = 2 * 0; ub = u + 0                           # Rd (d1) r = 2r; ub (d1 u) r = u + r, r = Rof [] = 0
    clauses = {
        'ds <> []': m >= 1, 'a >= 1': a >= 1, 'b mod 2 = 1': b % 2 == 1, '(a + Rof) mod 2 = 0': (a + Rof) % 2 == 0,
        'a + Rof + 2 >= 2^(S m)': a + Rof + 2 >= 2 ** (m + 1), 'b + 3 + 2 Rof >= 2^(S m)': b + 3 + 2 * Rof >= 2 ** (m + 1),
        'LSBok: v >= Rof + 1': v >= Rof + 1,
        'A: canon (u >= 1, v >= 1)': u >= 1 and v >= 1, 'A: v >= Rd + 1': v >= Rd + 1, 'A: ub mod 2 = 1': ub % 2 == 1,
        'A: p = 0 -> ub = 1': ub == 1, 'A: a + Rof + 1 >= 2^(S m)': a + Rof + 1 >= 2 ** (m + 1),
    }
    for k, c in clauses.items():
        chk(c, k)
    return report('B base', ok, tot, '(INV at K((1,1,9);8,1): set form class A; Rocq additive form, 12 clauses, all '
                  'true: a+R+2 = 10, b+3+2R = 4 (tight, as the parent\'s), a+R+1 = 9, v = 9 >= 1, ub = 1)')

# ---------------------------------------------------------------- G orbit + parent's abstract checks
def check_orbit(N):
    (D, a, b), t = BASE, T0
    cls = Counter(); drops = Counter(); ok = 0; ovf = 0
    for i in range(N):
        c = P.inv(D, a, b)
        cls[c] += 1; ok += c is not None
        if c is None:
            print('  orbit FAIL at macro step', i, D, a, b); break
        name, D, a, b, st, info = P.mstep(D, a, b); t += st
        ovf += name == 'O'
        if info.get('drop'): drops[info['drop']] += 1
    return report('G orbit', ok, N, '(abstract orbit from the base: classes %s; drops %s; %d overflows; t=%.3g, '
                  '%d digits)' % (dict(cls), dict(drops), ovf, t, len(D)))

def parent_abstract(r, NI):
    saved = P.report
    res = []
    def rep(name, ok, tot, extra=''):
        return report('G ' + name.split(' ', 1)[1] + '*', ok, tot, extra + '  [* parent\'s check, abstract map only]')
    P.report = rep
    try:
        res.append(P.check_induct(r, NI))
        res.append(P.check_drop_algebra(r, 20000))
    finally:
        P.report = saved
    return all(res)

# ---------------------------------------------------------------- X coupling to #11 (explanation, not a premise)
def check_coupling(N):
    """this machine's macro orbit vs kill #11's (its own base K((1,1,2); 8, 5) at step 483, in the shared triple
    notation): from macro step 54 on, the two states agree except for ONE exponent, larger by 3 here, on the top
    digit (v_1 in class A, u_2 in class B, u_1 in class C), and the same rule fires."""
    def rel(x, y):
        (D1, a1, b1), (D2, a2, b2) = x, y
        if a1 != a2 or b1 != b2 or len(D1) != len(D2):
            return None
        out = []
        for j, (d1, d2) in enumerate(zip(D1, D2)):
            if d1[1] != d2[1]: return None
            if d1[0] != d2[0]: out.append((j + 1, 'u', d1[0] - d2[0]))
            if d1[2] != d2[2]: out.append((j + 1, 'v', d1[2] - d2[2]))
        return tuple(out)
    x, tx = BASE, T0; y, ty = ([(1, 1, 2)], 8, 5), 483
    first = None; seen = Counter(); ok = 0; tot = 0; ovf = 0
    for k in range(N):
        r_ = rel(x, y)
        good = r_ is not None and len(r_) == 1 and r_[0][2] == 3 and r_[0][0] <= 2
        if good and first is None:
            first = (k, tx, ty)
        n1, D, a, b, s1, _ = P.mstep(*x); n2, D2, a2, b2, s2, _ = P.mstep(*y)
        if first is not None:
            tot += 1; good = good and n1 == n2; ok += good
            seen[(r_[0][0], r_[0][1], P.inv(*x)) if r_ else None] += 1
            if not good:
                print('  coupling FAIL at macro step', k, x, y, r_); break
        ovf += n1 == 'O'
        x, y, tx, ty = (D, a, b), (D2, a2, b2), tx + s1, ty + s2
    good0 = first is not None and first[0] == 54
    return report('X coupling', ok + good0, tot + 1, '(informational: vs the orbit of #11, from macro step %s (step %s vs '
                  '%s) to %d: one exponent +3 on the top digit, same rule; where it sits: %s; %d overflows; lag %d steps '
                  'at t=%.3g)' % (first[0] if first else '-', first[1] if first else '-', first[2] if first else '-',
                  N, dict(seen), ovf, tx - ty, tx))

# ---------------------------------------------------------------- V rocq delta
def delta_text(src):
    """the delta of proof.md 5, applied to the parent's .v text. Every edit is asserted."""
    def one(s, old, new, count=1):
        assert s.count(old) == count, (old, s.count(old))
        return s.replace(old, new)
    # 1. header comment (lines 1-14 of the parent's file) -> this machine's header
    i = src.index('From BusyCoq Require Import Individual62.')
    hdr = src[:i]
    assert hdr.startswith('(* 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA--- never halts.') and hdr.rstrip().endswith('*)')
    new_hdr = ("(* " + TW + " never halts.\n"
               "   This is kill #33's table (" + PARENT + ") with its states renamed\n"
               "   sigma = (A,B,C,D,E,F) -> (B,C,D,A,E,F), no mirror, started in #33's state D (equivalently kill #11's\n"
               "   table 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- mirrored, started in #11's state C).\n"
               "   Delta from #33's .v (sha256 37cb1802...): the TM string, sigma applied to every state name {{X}}\n"
               "   (window lemmas, digit lemmas, sweeps, chunks, K), and the base: init is 687 steps to\n"
               "   K [d1 1 9] 8 1 (class A) instead of 215 steps to K [d1 1 3] 4 1. Every proof script, the three rule\n"
               "   specs (M_spec, Mdrop_spec, O_spec) and the abstract part (INV, closure, macro_step) are #33's text.\n"
               "   Informal proof: the accompanying write-up (proof.md, a delta proof from #33's proof.md).\n"
               "   Formalized with Claude Code (AI-assisted).\n"
               "   Checked: compiles against unmodified busycoq (commit 0940bb9) with Coq 8.20.1;\n"
               "   Print Assumptions nonhalt: Closed under the global context. *)\n\n")
    body = src[i:]
    # 2. the TM string
    body = one(body, 'TM_from_str "' + PARENT + '"', 'TM_from_str "' + TW + '"')
    # 3. sigma on every state name, simultaneously (through placeholders)
    counts = {q: body.count('{{%s}}' % q) for q in 'ABCDEF'}
    assert counts == {'A': 5, 'B': 0, 'C': 22, 'D': 18, 'E': 18, 'F': 0}, counts
    for q in 'ABCDEF':
        body = body.replace('{{%s}}' % q, '{{#%s#}}' % SIG[q])
    body = re.sub(r'\{\{#([A-F])#\}\}', r'{{\1}}', body)
    # 4. the base
    body = one(body, 'Lemma init: c0 -->* K [d1 1 3] 4 1.', 'Lemma init: c0 -->* K [d1 1 9] 8 1.')
    body = one(body, 'change (K [d1 1 3] 4 1) with (Kc ([d1 1 3], 4, 1)).',
               'change (K [d1 1 9] 8 1) with (Kc ([d1 1 9], 8, 1)).')
    # 5. comments that name the head state or the start
    body = one(body, '(* end of M: (10)^(b+2) 110 (10)^a 11 <D -> <C (01)^(b+2) 000 (01)^(a+1) *)',
               '(* end of M: (10)^(b+2) 110 (10)^a 11 <A -> <D (01)^(b+2) 000 (01)^(a+1) *)')
    body = one(body, '(* left-edge chunk shared by M and O: <C (01)^b 000 (01)^a -> (10)^(b+2) 110 (10)^a E> *)',
               '(* left-edge chunk shared by M and O: <D (01)^b 000 (01)^a -> (10)^(b+2) 110 (10)^a E> *)')
    body = one(body, '(* end of O: (10)^(b+2) 110 (10)^(a+1) <C 000 -> <C 01 000 (01)^(b+3) (10)^(a+1) 01 *)',
               '(* end of O: (10)^(b+2) 110 (10)^(a+1) <D 000 -> <D 01 000 (01)^(b+3) (10)^(a+1) 01 *)')
    j = body.index('\n(*\n```\n' + PARENT)
    tail = body[j:]
    tail = one(tail, '```\n' + PARENT + '\n', '```\n' + TW + '\n')
    tail = one(tail, 'K(d_1 .. d_m; a, b) := 0^inf <C (01)^b', 'K(d_1 .. d_m; a, b) := 0^inf <D (01)^b')
    tail = one(tail, 'start: 0^inf A> 0^inf  -->*  K((1,1,3); 4, 1)                       (step 215)',
               'start: 0^inf A> 0^inf  -->*  K((1,1,9); 8, 1)                       (step 687)')
    return new_hdr + body[:j] + tail

def check_rocq_delta():
    ok = tot = 0
    def chk(c, msg):
        nonlocal ok, tot
        tot += 1; ok += bool(c)
        if not c: print('  rocq delta FAIL:', msg)
    pv = os.path.join(PDIR, PARENT + '.v')
    src = open(pv).read()
    chk(hashlib.sha256(src.encode()).hexdigest() == PARENT_V_SHA, 'parent .v sha256 pinned')
    dv = os.path.join(HERE, 'rocq', 'delta_check.v')
    if not os.path.exists(dv):
        chk(False, 'rocq/delta_check.v missing')
        return report('V rocq delta', ok, tot)
    d = open(dv).read()
    chk(delta_text(src) == d, 'delta_check.v == delta(parent .v), byte for byte')
    # outside comments, the only differences from the parent are the TM string, {{X}} names and the base
    a = P._nocomment(src); b = P._nocomment(d)
    a2 = a.replace(PARENT, TW).replace('[d1 1 3] 4 1', '[d1 1 9] 8 1').replace('([d1 1 3], 4, 1)', '([d1 1 9], 8, 1)')
    a2 = re.sub(r'\{\{([A-F])\}\}', lambda m_: '{{%s}}' % SIG[m_.group(1)], a2)
    chk(a2.strip() == b.strip(), 'code (comments stripped) = parent code with the delta substitutions only')
    nl = sum(1 for x, y in zip(a.split('\n'), b.split('\n')) if x != y)
    chk(len(re.findall(r'TM_from_str', b)) == 1 and 'Lemma nonhalt: ~halts tm c0.' in b, 'one TM_from_str, nonhalt')
    bad = re.findall(r'\b(Admitted|admit|Axiom|Parameter|Hypothesis|Conjecture|Abort|Variable|Context)\b', b)
    chk(not bad, 'no assumptions: %s' % bad)
    lg = os.path.join(HERE, 'rocq', 'delta_check.out')
    log = open(lg).read() if os.path.exists(lg) else ''
    sha = hashlib.sha256(d.encode()).hexdigest()
    chk(log.startswith(sha) and 'exit 0' in log and 'Closed under the global context' in log
        and re.search(r'nonhalt\s*:\s*~\s*halts tm c0', log), 'rocq/delta_check.out = clean compile of this exact file')
    return report('V rocq delta', ok, tot, '(delta_check.v = parent .v + proof.md 5 delta, byte for byte; code lines '
                  'changed: %d; compile record: sha256 match, exit 0, closed; NOT a check_kill run)' % nl)


if __name__ == '__main__':
    ap = argparse.ArgumentParser()
    ap.add_argument('--seed', type=int, default=388)
    ap.add_argument('--orbit', type=float, default=3e5)
    ap.add_argument('--induct', type=float, default=1.5e5)
    ap.add_argument('--tm-steps', type=float, default=3e7)
    ap.add_argument('--lockstep', type=float, default=2e6)
    ap.add_argument('--quick', action='store_true')
    A = ap.parse_args()
    r = random.Random(A.seed)
    if A.quick:
        A.orbit, A.induct, A.tm_steps, A.lockstep = 2e4, 2e4, 2e6, 2e5
    print('check_proof.py (delta from #33) for %s (seed %d)' % (TW, A.seed))
    res = [check_identity(),
           check_lockstep(int(A.lockstep)),
           check_lemmas(),
           check_rules(r, 700 if not A.quick else 140, 350 if not A.quick else 70, 3000 if not A.quick else 300),
           check_chains(r, A.quick),
           check_init(),
           check_closure(int(A.tm_steps)),
           check_base(),
           check_orbit(int(A.orbit)),
           parent_abstract(r, int(A.induct)),
           check_coupling(int(A.orbit)),
           check_rocq_delta()]
    print('SUMMARY ' + ('PASS' if all(res) else 'FAIL'))
    sys.exit(0 if all(res) else 1)