#!/usr/bin/env python3
"""check_proof.py -- evidence for the DELTA proof (proof.md) of
1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---   (#11b; line 511 of the 740 list)

Parent: kill #11  1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---  (KILLED_NONHALT, check_kill PASS).
The parent's check_proof.py is imported READ-ONLY (no bytecode written) for its abstract macro model
(mstep, inv, stats, render), its random-INV generator, its window-lemma table LEM, its chain builders
M_chain / O_chain and its pure-abstract checks. Everything that depends on the machine or on the start
is re-run here on THIS machine's own table, with its own simulator, with the head state of K renamed
B -> A.

  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 511 of the 740 list byte for byte (and line 541 of the 778 list; all 27 snapshots);
                 absent from solved_index.tsv; the sheet rows (Results 1276 and Level 1 row 44: Done By
                 hipparcos, thread 1432566675533992019; Results 1277, right below, is #33 with no claim);
                 tau = EABCDF (no mirror) is the ONLY map (720 perms x mirror) taking #11's table to this
                 one, and it takes #11's state B to A; maps from #33 / #33b (unique, informational);
                 only D1 enters F, F1 is the only undefined cell
  R  lockstep    Lemma R on the real machines: this machine from blank vs #11 from 0^inf B> 0^inf, every
                 step: state = tau(parent state), same symbol written, same move (--lockstep steps)
  L  lemmas      #11's 20 window lemmas (its proof.md 2.1) with states renamed by tau: exact on THIS table,
                 never reading outside the window, transitions = tau of #11's; F entered only in T4/T9/T13
                 (by D1 here), reading 0
  A  rules       M (700) and O (350) random K-configs on THIS table, head state A: exact tape and step
                 count, leftmost cell read as stated; random INV states, one macro step on THIS table (3000)
  H  chains      #11's M and O chains (its proof.md 2.2/2.3), every link renamed by tau and run on THIS
                 table: whole tape, head and state after every link (same boxes as #11's checks 12/13,
                 O also at m = 0), plus the init leg K(; 10, 5) -> K((1,1,10); 8, 1)
  C  init        blank -> the K-configs at steps 122, 263, 363, 463 (none in INV) -> K((1,1,10); 8, 1) at
                 step 732, class A, with the derived quantities; #11 from B gives the same list; the next
                 macro step (O, 253 steps) -> class B
  D  closure     the real machine from blank vs the abstract model at every macro boundary from step 732 up
                 to --tm-steps (whole tape, head, state), INV at each boundary
  B  base        INV at K((1,1,10); 8, 1) in the parent's set form (inv) and in the additive form of the
                 parent's .v (INV / PA / Rof / LSBok), 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 #11's and vs #33b's
  V  rocq delta  rocq/delta_check.v is exactly the parent's .v (sha256 pinned) with the delta of proof.md 5,
                 and rocq/delta_check.out is a clean compile record of that exact file (exit 0, closed).
                 Not a check_kill run.
"""
import sys, os, re, random, argparse, itertools, hashlib, importlib.util, glob, csv, math
from collections import Counter
sys.dont_write_bytecode = True

TW = "1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---"
PARENT = "1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---"          # kill #11
TM33 = "1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---"            # kill #33  (#11 mirrored, start D)
TM33B = "1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---"           # kill #33b (#11 mirrored, start C)
ROOT = "[local working file]"
PDIR = os.path.join(ROOT, "machines", PARENT)
HERE = os.path.dirname(os.path.abspath(__file__))
PARENT_V_SHA = "8bca47b193b15a0cbd664fcbafa9bf6a39dfc4c9ca261e1d8f95cb0f425553c0"
THREAD = "1432566675533992019"

_spec = importlib.util.spec_from_file_location("parent_check_proof_11", 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 this machine
assert P.TM == PARENT

TAU = {'A': 'E', 'B': 'A', 'C': 'B', 'D': 'C', 'E': 'D', 'F': 'F'}     # parent state -> this machine's state
KQ = TAU['B']                                                          # head state of K here: A
TT = P.parse_tm(TW)
BASE = ([(1, 1, 10)], 8, 1)
T0 = 732
PBASE = ([(1, 1, 2)], 8, 5)                                            # #11's own base, step 483
PT0 = 483


# ---------------------------------------------------------------- generic helpers
def relabel(tab, perm, mirror):
    """machine string of table tab with parent state s renamed perm[s] (and L/R swapped if mirror)."""
    rows = [None] * 6
    for s in range(6):
        cells = []
        for sym in (0, 1):
            tr = tab[s][sym]
            if tr is None:
                cells.append('---')
            else:
                w, d, t = tr
                cells.append('%d%s%s' % (w, 'R' if (d == 1) != mirror else 'L', chr(65 + perm[t])))
        rows[perm[s]] = ''.join(cells)
    return '_'.join(rows)

def maps_to(tab, target):
    return [(''.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 relabel(tab, list(perm), mir) == target]

def run(cells, head, state, n, tab=None):
    """n steps on THIS table (or tab). Returns (tape_str, head_idx, state, min_head, max_head), the last two
    relative to cells[0]."""
    tab = TT if tab is None else tab
    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
    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 same_cfg(res, cells, head, state):
    return P.same_cfg(res[:4], cells, head, state)

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

def parse_K(txt):
    """txt = the cells from the leading 1 up to the cell left of the head. Returns (D, a, b) if
    txt = 1001 d_1..d_m (10)^a 000 (10)^b with canonical-shape digits (v >= 1), else None. The parse is unique:
    b and a are forced by stripping 10s from the right (a digit ends in 01), the digits by greedy reading."""
    if not txt.startswith('1001'):
        return None
    s = txt; b = 0
    while s.endswith('10'):
        s = s[:-2]; b += 1
    if not s.endswith('000'):
        return None
    s = s[:-3]; a = 0
    while s.endswith('10') and len(s) > 4:
        s = s[:-2]; a += 1
    mid = s[4:]; D = []; i = 0
    while i < len(mid):
        u = 0
        while mid.startswith('10', i): u += 1; i += 2
        beta = 1
        if mid.startswith('00', i): beta = 0; i += 2
        v = 0
        while mid.startswith('01', i): v += 1; i += 2
        if v == 0:
            return None
        D.append((u, beta, v))
    if P.render(D, a, b)[0] != txt:
        return None
    return D, a, b

def scan_K(tab, start, kq, T):
    """every K-configuration in steps 0..T from the blank tape: head state kq on a cell with only blanks
    from there to the right, only blanks left of the leading 1, the text in between parsing as a K."""
    n = T + 16
    tape = bytearray(2 * n); h = n; s = ord(start) - 65; q = ord(kq) - 65; out = []
    for t in range(T + 1):
        if t > 0:
            tr = tab[s][tape[h]]
            if tr is None:
                return out, t
            tape[h] = tr[0]; h += tr[1]; s = tr[2]
        if s == q and not any(tape[h:]):
            f = tape.find(1)
            if 0 <= f < h:
                k = parse_K(''.join('01'[x] for x in tape[f:h]))
                if k:
                    out.append((t, k))
    return out, None

def derived(D, a, b):
    st, V = P.stats(D)
    m = len(D); Rtot = 2 ** m - 1 - V
    return {'per': st, 'V': V, 'Rtot': Rtot, 'S': a + Rtot - (2 ** (m + 1) - 2), 'T': b - (2 * V - 1)}

def O0(a, b):
    """O with no digits (m = 0), as derived in #11's proof.md 2.3 with m = 0; used only in the init."""
    return 'O(m=0)', [(1, 1, a)], b + 3, 1, 89 + 8 * a + 20 * b, {}

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)
    hd = os.path.join(ROOT, 'data/holdouts')
    raw = open(os.path.join(hd, 'BB6_holdouts_740.txt'), 'rb').read().split(b'\n')
    chk(len(raw) > 511 and raw[510] == TW.encode('ascii') and sum(x == TW.encode() for x in raw) == 1,
        'line 511 of BB6_holdouts_740.txt, byte for byte, once')
    chk(sum(1 for x in raw if x.strip()) == 740, 'the 740 list has 740 entries')
    l778 = open(os.path.join(hd, '2026-10-07_778.txt')).read().split('\n')
    chk(l778[540] == TW, 'line 541 of the 778 list')
    snaps = sorted(f for f in glob.glob(os.path.join(hd, '*.txt')) if 'eqv' not in f)
    chk(len(snaps) == 27 and all(TW in set(x.strip() for x in open(f)) for f in snaps), 'all 27 snapshots')
    groups = [g.split() for g in open(os.path.join(hd, '2026-10-07_eqv_1590.txt')).read()
              .replace('\r', '').split('\n\n') if g.strip()]
    chk([g for g in groups if TW in g] == [[TW]], 'eqv group = {this} alone')
    solved = open(os.path.join(ROOT, 'data/solved_index.tsv')).read()
    chk(TW not in solved, 'absent from solved_index.tsv (no busycoq proof)')
    sh = os.path.join(ROOT, 'data/sheet/')
    def rows_of(tab):
        return list(csv.reader(open(sh + '2026-10-09_%s.csv' % tab, encoding='utf-8')))
    res = rows_of('results'); lv1 = rows_of('level-1')
    chk(res[1275] == [TW, '', 'Skelet 1-like Class 2', '', '1', 'hipparcos'], 'Results row 1276: %s' % res[1275])
    chk(res[1276][0] == TM33 and res[1276][5] == '' and res[1276][4] == '', 'Results row 1277 = #33, no claim')
    chk(lv1[43] == [TW, '', '', '1', 'hipparcos', ''], 'Level 1 row 44: %s' % lv1[43])
    links = [r for r in csv.reader(open(sh + '2026-10-09_links.csv')) if THREAD in r[-1]]
    chk(sorted((r[0], r[2], r[4]) for r in links) == [('Level 1', '44', TW), ('Results', '1276', TW)],
        'thread %s linked from exactly those two rows' % THREAD)
    tabs = set()
    for f in glob.glob(sh + '2026-10-09_*.csv'):
        if TW in open(f, encoding='utf-8', errors='replace').read():
            tabs.add(os.path.basename(f)[11:-4])
    chk(tabs == {'results', 'level-1', 'classifications', 'links'}, 'sheet tabs naming it: %s' % sorted(tabs))
    chk(not any(TM33 in r[0] for r in lv1), '#33 is not on the Level 1 tab')
    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')
    # tau: the only relabeling of #11's table giving this string; it sends #11's B to A
    chk(maps_to(P.TT, TW) == [('EABCDF', False, 'B')], 'maps #11 -> this: %s' % maps_to(P.TT, TW))
    chk([TAU[c] for c in 'ABCDEF'] == list('EABCDF'), 'TAU = EABCDF')
    cells = 0
    for s in range(6):
        for sym in (0, 1):
            pt = P.TT[s][sym]; tt = TT[ord(TAU[chr(65 + s)]) - 65][sym]
            if pt is None: cells += tt is None
            else: cells += tt == (pt[0], pt[1], ord(TAU[chr(65 + pt[2])]) - 65)
    chk(cells == 12, 'cell by cell %d/12' % cells)
    m33 = maps_to(P.parse_tm(TM33), TW); m33b = maps_to(P.parse_tm(TM33B), TW)
    chk(m33 == [('CEABDF', True, 'C')] and m33b == [('BCEADF', True, 'D')], 'from #33 %s, from #33b %s' % (m33, m33b))
    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 == [('D', 1)] and undef == [('F', 1)], 'into F %s, undefined %s' % (into_F, undef))
    return report('S identity', ok, tot, '(line 511 of the 740 list, byte for byte; line 541 of the 778 list; 27/27 '
                  'snapshots; eqv group of one; not in solved_index; sheet: Results 1276 + Level 1 row 44, Done By '
                  'hipparcos, thread %s; Results 1277 = #33, no claim; tau = EABCDF, no mirror, the only map, '
                  'start = #11\'s B; from #33 CEABDF+mirror (start C), from #33b BCEADF+mirror (start D); '
                  'halting cell D1 -> F1)' % THREAD)


# ---------------------------------------------------------------- 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 = 1                                         # this machine from A; #11 from B
    tau = [ord(TAU[chr(65 + i)]) - 65 for i in range(6)]
    tw, pa = TT, P.TT
    ok = 0
    for _ in range(N):
        if s1 != tau[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 == tau[s2]
    return report('R lockstep', ok + same, N + 1, '(this machine from blank = tau(#11 from 0^inf B> 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] + TAU[w[i - 1]] + w[i:]
    i = w.find('<')
    return w[:i + 1] + TAU[w[i + 1]] + w[i + 2:]

def lemma_run(lhs, rhs, n, tab):
    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; trs = []; fr = []
    for _ in range(n):
        if not (0 <= h < len(t)) or tab[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 = tab[s][t[h]]; t[h] = w; h += d
    good = len(c) == len(c2) and ''.join(map(str, t)) == c2 and h == h2 and s == ord(st2) - 65
    return good, trs, fr

def check_lemmas(verbose=True):
    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, TT)
        pg, ptrs, _ = lemma_run(lhs, rhs, n, P.TT)
        good = good and pg and [TAU[x[0]] + x[1] for x in ptrs] == trs
        ok += good
        fs += [(name, x) for x in fr]
        lines.append('    %-4s %-11s -> %-11s %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']
    if verbose:
        for x in lines: print(x)
    return report('L lemmas', ok + fok, len(P.LEM) + 1, '(20 windows of #11 renamed by tau, exact on this table, '
                  'transitions = tau of #11\'s; F entered only in T4/T9/T13 (by D1), reading 0)')


# ---------------------------------------------------------------- A rules on this 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)
        i00 = 4 + sum(len(P._dig([d])) for d in pre) + 2 * flip[0]      # first 0 of the flipped 00
        g = same_cfg(res, *render(D2, a2, b2)) and res[3] == i00
        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 = same_cfg(res, *render(D2, a2, b2)) and res[3] == -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 += 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 A: M %d/%d (k=0..6, %d drops, %d with u*=0; leftmost read = first 0 of '
                  'the flipped 00), O %d/%d (m=1..7; leftmost read = 3 left of the leading 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, pad=64):
    """#11's run_chain, on THIS table, with every link's state renamed by tau."""
    l, mo, st, r = c0
    n = sum(P.LEM[nm][2] * k for (nm, k, _) in ln)
    t = bytearray(pad) + bytearray(int(x) for x in l + r) + bytearray(pad + n)
    h = pad + (len(l) if mo == '>' else len(l) - 1); s = ord(TAU[st]) - 65; mn = 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, None
            t[h] = tr[0]; h += tr[1]; s = tr[2]; mn = min(mn, h); tot += 1
            if h < 0:
                return False, tot, None, None
        want = bytearray(pad) + bytearray(int(x) for x in l2 + r2)
        want += bytearray(len(t) - len(want))
        if t != want or h != pad + (len(l2) if mo2 == '>' else len(l2) - 1) or s != ord(TAU[st2]) - 65:
            return False, tot, None, None
    return True, tot, mn - pad, ''.join(map(str, t)).strip('0')

def _M_case(pre, us, vs, ones, a, b):
    c0, ln, i00 = P.M_chain(pre, us, vs, ones, a, b)
    good, steps, mn, end = 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 mn == i00 and end == render(D2, a2, b2)[0].strip('0') \
        and mof == '>' and TAU[stf] == KQ and rf == ''

def _O_case(ones, a, b):
    c0, ln = P.O_chain(ones, a, b)
    good, steps, mn, end = 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, _ = O0(a, b)
    lf, mof, stf, rf = ln[-1][2]
    return good and steps == st and mn == 0 and end == render(D2, a2, b2)[0].strip('0') \
        and mof == '>' and TAU[stf] == KQ and rf == ''

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([], 10, 5)                   # the init's last leg: K(; 10, 5) -> K((1,1,10); 8, 1)
    return report('H chains', ok + i0, tot + 1, '(#11\'s chains renamed by tau, link by link on this table: M %d/%d '
                  '(box + %d random), O %d/%d (box m=0..%d + %d random), plus the init leg K(;10,5) -> K((1,1,10);8,1))'
                  % (mo, mt, 100 if quick else 500, ok - mo, tot - mt, mmax, 60 if quick else 300))


# ---------------------------------------------------------------- C init
INIT_K = [(122, ([(1, 1, 2)], 2, 1)), (263, ([(0, 0, 1), (2, 1, 2)], 4, 1)), (363, ([(3, 0, 1)], 5, 3)),
          (463, ([], 10, 5)), (732, BASE)]

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(TT, 'A', KQ, T0)
    chk(halted is None and ks == INIT_K, 'K-configs in 0..732: %s' % ks)
    chk([P.inv(*k) for _, k in ks] == [None, None, None, None, 'A'], 'only the last is in INV')
    d122 = derived(*INIT_K[0][1]); d263 = derived(*INIT_K[1][1]); d363 = derived(*INIT_K[2][1])
    chk(d122['S'] == 0 and d122['per'][0][5] == 1, 'step 122: S = %d (class A needs S >= 1), ubar = 1 (C needs >= 2)'
        % d122['S'])
    chk(d263['per'][-1][6] == 0, 'step 263: LSB vbar = %d (Common needs >= 1)' % d263['per'][-1][6])
    chk(INIT_K[2][1][0] == [(3, 0, 1)] and d363['per'][-1][6] == 0, 'step 363: only digit bit 0 with v = 1 = R')
    chk(INIT_K[3][1][0] == [], 'step 463: no digits (m = 0)')
    chain = []
    for (t1, k1), (t2, k2) in zip(INIT_K, INIT_K[1:]):
        D, a, b = k1
        nm, D2, a2, b2, st, info = P.mstep(D, a, b) if D else O0(a, 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)
    res = run('', 0, 'A', T0)
    chk(same_cfg(res, *render(*BASE)), 'blank -732-> K((1,1,10);8,1), whole tape')
    pks, ph = scan_K(P.TT, 'B', 'B', T0)
    chk(ph is None and pks == INIT_K, '#11 from B: same K list')
    pks0, _ = scan_K(P.TT, 'A', 'B', PT0)
    chk([t for t, _ in pks0] == [142, 283, 383, 483] and pks0[-1][1] == PBASE, '#11 from A: its own init (sanity)')
    D, a, b = BASE
    dv = 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, 10), '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), (10, 1, 8)], 4, 1, 253) and P.inv(D2, a2, b2) == 'B',
        'next: %s' % ((nm, D2, a2, b2, st),))
    chk(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 122 O-> 263 M1(top drop)-> 363 M0(LSB drop)-> 463 (m=0) O(m=0)-> '
                  '732 = K((1,1,10);8,1), class A: V=1, R=0, S=6, T=0, ubar=1, vbar=10; the first four not in INV; '
                  '#11 from B identical; next O (253 steps) -> K((0,0,1),(10,1,8);4,1), class B)')


# ---------------------------------------------------------------- D closure
def check_closure(Tmax):
    Rpad = int(4 * math.sqrt(max(Tmax, 1))) + 20000; Lpad = 20000
    tape = bytearray(Lpad + Rpad); tab = TT
    state = {'h': Lpad, 's': 0}
    tr01 = bytes.maketrans(b'01', b'\x00\x01')
    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):
        s_, _, _ = render(D, a, b)
        if state['s'] != ord(KQ) - 65:
            return False
        seg = s_.encode().translate(tr01); hh = state['h']
        return tape[hh - len(seg):hh] == seg and tape.count(1) == s_.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 732 + 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')
    # additive form of the parent's .v (Definition INV / PA / Rof / LSBok / Rd / ub) at ([d1 1 10], 8, 1)
    u, v, m = 1, 10, 1
    Rof = 0                                          # Rof (d1 _ _ :: []) = 2 * Rof [] = 0
    r_above = 0; Rd = 2 * r_above; ub = u + r_above  # Rd (d1) r = 2r; ub (d1 u) r = u + r
    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,10);8,1): set form class A; additive form of #11\'s .v, 12 '
                  'clauses, all true: a+R+2 = 10, b+3+2R = 4 (tight), a+R+1 = 9, v = 10 >= 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
    def rep(name, ok, tot, extra=''):
        return report('G ' + name.split(' ', 1)[1] + '*', ok, tot, extra + '  [* #11\'s check, abstract map only]')
    P.report = rep
    try:
        res = [P.check_induct(r, NI), P.check_drop_algebra(r, 20000)]
    finally:
        P.report = saved
    return all(res)


# ---------------------------------------------------------------- X coupling (explanation, not a premise)
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)

def coupling(x, tx, y, ty, N, delta):
    """from the first macro step k at which the states differ in exactly one top-digit exponent by delta,
    check that this persists and that the same rule fires, to N macro steps."""
    first = None; seen = Counter(); ok = tot = 0
    for k in range(N):
        r_ = _rel(x, y)
        good = r_ is not None and len(r_) == 1 and r_[0][2] == delta 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
        x, y, tx, ty = (D, a, b), (D2, a2, b2), tx + s1, ty + s2
    return first, ok, tot, seen, tx - ty, tx

def check_coupling(N):
    f11, ok1, tot1, seen1, lag1, tx = coupling(BASE, T0, PBASE, PT0, N, 4)
    f33b, ok2, tot2, seen2, lag2, _ = coupling(BASE, T0, ([(1, 1, 9)], 8, 1), 687, N, 1)
    good = f11 is not None and f33b == (0, T0, 687)
    return report('X coupling', ok1 + ok2 + good, tot1 + tot2 + 1, '(informational: vs #11 from macro step %s (step %s '
                  'vs %s): one top-digit exponent +4, same rule, to %d; where: %s; lag %d steps at t=%.3g. vs #33b from '
                  'macro step 0: one top-digit exponent +1, same rule; where: %s; lag %d)'
                  % (f11[0] if f11 else '-', f11[1] if f11 else '-', f11[2] if f11 else '-', N, dict(seen1), lag1, tx,
                     dict(seen2), lag2))


# ---------------------------------------------------------------- V rocq delta
def _nocomment(s):
    out = []; depth = 0; i = 0
    while i < len(s):
        if s.startswith('(*', i): depth += 1; i += 2; continue
        if depth and s.startswith('*)', i): depth -= 1; i += 2; continue
        if not depth: out.append(s[i])
        i += 1
    return '\n'.join(x.rstrip() for x in ''.join(out).split('\n') if x.strip())

HEADER = ("(* " + TW + " never halts.\n"
          "   This is kill #11's table (" + PARENT + ") with its states renamed\n"
          "   tau = (A,B,C,D,E,F) -> (E,A,B,C,D,F), no mirror, started in #11's state B.\n"
          "   Delta from #11's .v (sha256 8bca47b1...): the TM string, tau applied to every state name {{X}}\n"
          "   (window lemmas, digit lemmas, sweeps, chunks, K), and the base: init is 732 steps to\n"
          "   K [d1 1 10] 8 1 (class A) instead of 483 steps to K [d1 1 2] 8 5. Every proof script, the three rule\n"
          "   specs (M_spec, Mdrop_spec, O_spec) and the abstract part (INV, closure, step) are #11's text.\n"
          "   Informal proof: the accompanying write-up (proof.md, a delta proof from #11'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")

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)
    i = src.index('From BusyCoq Require Import Individual62.')
    hdr = src[:i]
    assert hdr.startswith('(* ' + PARENT + ' never halts.') and hdr.rstrip().endswith('*)')
    body = src[i:]
    body = one(body, 'TM_from_str "' + PARENT + '"', 'TM_from_str "' + TW + '"')
    counts = {q: body.count('{{%s}}' % q) for q in 'ABCDEF'}
    assert counts == {'A': 0, 'B': 22, 'C': 18, 'D': 5, 'E': 18, 'F': 0}, counts
    for q in 'ABCDEF':
        body = body.replace('{{%s}}' % q, '{{#%s#}}' % TAU[q])
    body = re.sub(r'\{\{#([A-F])#\}\}', r'{{\1}}', body)
    body = one(body, 'Lemma init: c0 -->* K [d1 1 2] 8 5.', 'Lemma init: c0 -->* K [d1 1 10] 8 1.')
    body = one(body, 'change (K [d1 1 2] 8 5) with (Kc ([d1 1 2], 8, 5)).',
               'change (K [d1 1 10] 8 1) with (Kc ([d1 1 10], 8, 1)).')
    body = one(body, '(* right-edge chunk shared by M and O: (10)^a 000 (10)^b B> 0^inf -> <E (01)^a 011 (01)^(b+2) 0^inf *)',
               '(* right-edge chunk shared by M and O: (10)^a 000 (10)^b A> 0^inf -> <D (01)^a 011 (01)^(b+2) 0^inf *)')
    body = one(body, '(* end of M: C> 11 (01)^a 011 (01)^(b+2) 0^inf -> (10)^(a+1) 000 (10)^(b+2) B> 0^inf *)',
               '(* end of M: B> 11 (01)^a 011 (01)^(b+2) 0^inf -> (10)^(a+1) 000 (10)^(b+2) A> 0^inf *)')
    body = one(body, '(* end of O: 000 B> (01)^(a+1) 011 (01)^(b+2) 0^inf -> 10 (01)^(a+1) (10)^(b+3) 000 10 B> 0^inf *)',
               '(* end of O: 000 A> (01)^(a+1) 011 (01)^(b+2) 0^inf -> 10 (01)^(a+1) (10)^(b+3) 000 10 A> 0^inf *)')
    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 10 01 d_1 .. d_m (10)^a 000 (10)^b B> 0^inf',
               'K(d_1 .. d_m; a, b) := 0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b A> 0^inf')
    tail = one(tail, 'start: 0^inf A> 0^inf  -->*  K((1,1,2); 8, 5)                       (step 483)',
               'start: 0^inf A> 0^inf  -->*  K((1,1,10); 8, 1)                      (step 732)')
    return HEADER + 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)
    src = open(os.path.join(PDIR, PARENT + '.v')).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')
    a = _nocomment(src); b = _nocomment(d)
    a2 = a.replace(PARENT, TW).replace('[d1 1 2] 8 5', '[d1 1 10] 8 1').replace('([d1 1 2], 8, 5)', '([d1 1 10], 8, 1)')
    a2 = re.sub(r'\{\{([A-F])\}\}', lambda m_: '{{%s}}' % TAU[m_.group(1)], a2)
    chk(a2 == b, '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 = #11\'s .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=511)
    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')
    ap.add_argument('--no-rocq', action='store_true', help='skip section V')
    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 #11) 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))]
    if not A.no_rocq:
        res.append(check_rocq_delta())
    print('SUMMARY ' + ('PASS' if all(res) else 'FAIL'))
    sys.exit(0 if all(res) else 1)