#!/usr/bin/env python3
"""check_proof.py -- simulation evidence for proof.md of
1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---   (machine #33).

Self-contained: its own direct simulator on THIS table, its own K-configurations in THIS machine's
orientation (head at the left end), its own copy of the abstract macro model and of the invariant
INV = Common and (A or B or C) (proof.md section 3; the abstract part is the same as kill #11's).
Nothing is imported from kill #11's directory: #11's table and window lemmas appear below only as
data, for the cross-checks of check 10 and check 11, and check 14 reads #11's .v as text.

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

Checks (each prints PASS/FAIL with counts):
  1 sweeps        S1-S4 for many n, S5/S6 for many n (exact finite runs, exact step counts)
  2 rule M_k      random full K-configs (any bits, u>=0, drops included): exact tape, exact step count,
                  and the rightmost cell the head reads is the right 0 of the flipped digit's 00
  3 rule O        random all-ones K-configs: exact tape and step count
  4 init          blank -82-> K(;3,1) -133-> K((1,1,3);4,1) at step 215; the only K-configs in steps
                  0..215 are at 82 and 215; 133 = O's formula at m = 0; K((1,1,3);4,1) is class A with
                  the stated derived quantities; K(;3,1) is not in INV (m = 0)
  5 closure       the real machine from the blank tape agrees with the abstract model at every macro
                  boundary from step 215 up to --tm-steps (whole tape, state, head); INV at each boundary
  6 orbit         abstract orbit from step 215: INV holds at every macro state (--orbit macro steps)
  7 induction     random INV states of each class (not only reachable ones): one macro step is defined
                  (no carry reaches a v = 0 digit, no LSB drop) and lands in INV again
  8 induction-TM  a sample of those random INV states, run on the real machine for the predicted
                  number of steps, gives exactly the abstract successor (merges included)
  9 drop algebra  the closed forms F2 of proof.md 3.1 (R, R1, V, S, T after a drop), m = 2..12
 10 table         (a) the string is line 34 of data/holdouts/2026-10-07_778.txt and in all 26 snapshot
                  files of data/holdouts/ (2024-06-14 .. 2026-10-07); the sheet rows (Results: class +
                  note; Level 0: fun fact); (b) this table is
                  kill #11's table mirrored with states A,B,C,D,E,F -> B,C,D,A,E,F; (c) exactly four
                  strings of the 778 list are relabelings (720 perms x mirror) of this table, with the
                  start states listed in proof.md 0, in four different groups of the eqv_1590 file (this
                  machine a singleton); not on the data/discord lists; (d) the first INV K-config from the blank tape for
                  each of those four start states
 11 lemmas        the 20 window lemmas of proof.md 2.1, by exact finite runs that never read outside the
                  window; their transition lists; "F is entered only in T4, T9, T13 and reads 0";
                  each lemma is the mirror of kill #11's lemma of the same name
 12 M chain       the derivation of M (proof.md 2.2), link by link on the real machine: every
                  intermediate configuration, the step formula, the rightmost cell read (box + random)
 13 O chain       the same for O (proof.md 2.3), including m = 0 (the init's second leg)
 14 interface     (text checks; Review log gap 1) kill #11's .v, read as data: its abstract part uses the
                  machine part only through tm, dg/d0/d1, K, map0, map1, Oz, Oout, M_spec, Mdrop_spec,
                  O_spec, init, and never unfolds K; proof.md 6 quotes the three spec statements
                  verbatim; rocq/abstract_check.v (generated by scripts/make_abstract_check.py) is #11's
                  abstract part verbatim over this machine's plan_check.v, with #11's spec statements
                  as its only hypotheses, and rocq/abstract_check.out is a clean compile of that file
"""
import sys, random, argparse, itertools, re, os
from collections import Counter

TM = "1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---"
TM11 = "1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---"      # kill #11 (data only, for check 10)
HOLDOUTS = "[local working file]"

# ---------------------------------------------------------------- simulator
def parse_tm(s):
    tab = []
    for grp in s.split('_'):
        row = []
        for i in (0, 3):
            t = grp[i:i + 3]
            row.append(None if t == '---' else (int(t[0]), 1 if t[1] == 'R' else -1, ord(t[2]) - 65))
        tab.append(row)
    return tab
TT = parse_tm(TM)

class Halt(Exception):
    pass

def run(cells, head, state, n):
    """Run n steps from the tape `cells` (str of 0/1, blanks outside), head = index into cells (may be
    -1 or len(cells), i.e. a blank cell next to the text), state 'A'..'F'.
    Returns (tape_str, head, state, min_head, max_head), all indices relative to cells[0] via the
    returned tape_str's own coordinates: tape_str[0] is cell (-pad)."""
    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 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):
    """res from run(); compare with configuration (cells, head, state) up to translation."""
    rs, rh, rst = res[0], res[1], res[2]
    if rst != state:
        return False
    f = rs.find('1'); g = cells.find('1')
    if f < 0 or g < 0:
        return False
    if rh - f != head - g:
        return False
    return rs.strip('0') == cells.strip('0')

# ---------------------------------------------------------------- abstract model
# A K-state is (D, a, b); D = list of digits (u, beta, v), d_1 (most significant, next to the fixed
# 1001) first, d_m (least significant, next to the block) last.  THIS machine's tape:
#   K(D; a, b) = 0^inf <C (01)^b 000 (01)^a  dig(d_m) .. dig(d_1)  1001 0^inf
#   dig(u, 0, v) = (10)^v 00 (01)^u      dig(u, 1, v) = (10)^v (01)^u
def dig(d):
    u, beta, v = d
    return '10' * v + ('' if beta else '00') + '01' * u

def render(D, a, b):
    s = '01' * b + '000' + '01' * a + ''.join(dig(d) for d in reversed(D)) + '1001'
    return s, -1, 'C'          # head on the blank cell left of the text, state C

def mstep(D, a, b):
    """One macro step. Returns (name, D2, a2, b2, steps, info) or raises ValueError (no rule)."""
    m = len(D)
    if m >= 1 and all(d[1] == 1 for d in D):                          # rule O
        if any(d[0] < 1 or d[2] < 1 for d in D):
            raise ValueError('O: non-canonical digit')
        if a < 1:
            raise ValueError('O: a = 0')
        u = [d[0] for d in D]; v = [d[2] for d in D]
        D2 = [(0, 0, u[0])] + [(v[i - 1] - 1, 0, u[i]) for i in range(1, m)] + [(v[m - 1], 1, a)]
        steps = 89 - 4 * m + 8 * a + 20 * b + 4 * sum(u) + 8 * sum(v)
        return 'O', D2, b + 3, 1, steps, {}
    if m == 0:
        raise ValueError('empty digit list')
    k = 0
    while D[m - 1 - k][1] == 1:
        k += 1
    js = m - 1 - k                                                     # 0-based index of j*
    steps = 32 + 8 * a + 8 * b
    D2 = list(D)
    for i in range(js + 1, m):                                         # 1 -> 0
        u, _, v = D[i]
        if v < 1 or u < 1:
            raise ValueError('M: bit-1 digit with u or v = 0')
        D2[i] = (u, 0, v - 1); steps += 8 * u + 4 * v
    u, _, v = D[js]
    if v < 1:
        raise ValueError('M%d: carry reaches a bit-0 digit with v = 0' % k)   # the failure mode
    steps += 4 * v
    info = {'k': k, 'jstar': js + 1, 'drop': None}
    if v - 1 >= 1:
        D2[js] = (u + 1, 1, v - 1)
        a2 = a + 1
    elif js == m - 1:                                                  # LSB drop: (01)^(u+1) joins a
        del D2[js]; a2 = a + 1 + u + 1; info['drop'] = 'LSB'
    else:                                                              # drop: fuses with the next digit
        uu, bb, vv = D2[js + 1]
        D2[js + 1] = (uu + u + 1, bb, vv); del D2[js]; a2 = a + 1
        info['drop'] = 'top' if js == 0 else 'mid'
    return 'M%d' % k, D2, a2, b + 2, steps, info

# ---------------------------------------------------------------- invariant (proof.md section 3)
def stats(D):
    """per digit j=1..m: (u, beta, v, R, R1, ubar, vbar); plus V."""
    out = []; U = 0
    for j, (u, beta, v) in enumerate(D, start=1):
        U = 2 * U + beta
        R = 2 ** j - 1 - U
        R1 = (R + 1 - beta) // 2
        out.append((u, beta, v, R, R1, u + R1, v - R))
    return out, U

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

def inv(D, a, b):
    """Returns 'A', 'B' or 'C' if INV holds, else None."""
    m = len(D)
    if m < 1 or a < 1 or b % 2 == 0:
        return None
    st, V = stats(D)
    Rtot = 2 ** m - 1 - V
    S = a + Rtot - 2 ** (m + 1) + 2
    T = b - 2 * V + 1
    if (a + Rtot) % 2 or S < 0 or T < 0:
        return None
    for (u, beta, v, R, R1, ub, vb) in st:
        if v < 1 or (beta == 1 and u < 1) or u < 0:
            return None
    if st[-1][6] < 1:                                   # LSB keeps spare fuel
        return None
    top = D[0]
    par = all((v + beta) % 2 == 1 for (u, beta, v, R, R1, ub, vb) in st)
    if (top[1] == 0 and top[0] == 0 and top[2] >= 2) or (top[1] == 1 and top[0] == 1):
        if S >= 1 and all(vb >= 1 and ub % 2 == 1 for (u, beta, v, R, R1, ub, vb) in st):
            return 'A'
        return None
    if top == (0, 0, 1):
        if par and all(st[j - 1][5] >= 2 ** (j - 1) for j in range(2, m + 1)):
            return 'B'
        return None
    if par and S >= 1 and T >= 2 and all(st[j - 1][5] >= 2 ** j for j in range(1, m + 1)):
        return 'C'
    return None

# ---------------------------------------------------------------- K-config recognition (this orientation)
KRE = re.compile(r'^((?:01)*)000((?:01)*)(.*)1001$')

def parse_digits(s):
    """greedy, canonical parse of the digit string (left to right = d_m .. d_1)."""
    D = []; i = 0
    while i < len(s):
        v = 0
        while s.startswith('10', i): v += 1; i += 2
        beta = 1
        if s.startswith('00', i): beta = 0; i += 2
        u = 0
        while s.startswith('01', i): u += 1; i += 2
        if v < 1 or (beta == 1 and u < 1):
            return None                                 # not canonical (or not a digit at all)
        D.append((u, beta, v))
    return D[::-1]                                       # d_1 first

def k_of_tape(tape, h, st):
    """tape: bytearray or str of 0/1, head index h, state index st. Returns (D, a, b) if the
    configuration is a K-configuration (state C, head on a blank with only blanks to its left)."""
    if st != 2:
        return None
    if isinstance(tape, (bytes, bytearray)):
        if any(tape[:h + 1]):
            return None
        r = tape[h + 1:].rstrip(b'\x00')
        s = r.translate(bytes.maketrans(b'\x00\x01', b'01')).decode()
    else:
        if '1' in tape[:h + 1]:
            return None
        s = tape[h + 1:].rstrip('0')
    m = KRE.match(s)
    if not m:
        return None
    D = parse_digits(m.group(3))
    if D is None:
        return None
    b = len(m.group(1)) // 2; a = len(m.group(2)) // 2
    if render(D, a, b)[0] != s:
        return None
    return D, a, b

def scan_K(start, T):
    """all K-configurations of the run from the blank tape in state `start`, steps 0..T."""
    tape = bytearray(2 * T + 16); h = T + 8; s = ord(start) - 65; 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 == 2 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

# ---------------------------------------------------------------- random INV states
def rnd(r, lo, big):
    x = r.random()
    if x < 0.45: return lo + r.randint(0, 2)
    if x < 0.85: return lo + r.randint(0, 40)
    return lo + r.randint(0, big)

def rand_inv_state(r, cls, m, big=300):
    """A random state satisfying INV in class cls (rejection on the few global constraints)."""
    for _ in range(200):
        bits = [r.randint(0, 1) for _ in range(m)]
        if cls == 'B':
            bits[0] = 0
        st0 = []; U = 0
        for j in range(1, m + 1):
            U = 2 * U + bits[j - 1]; R = 2 ** j - 1 - U; R1 = (R + 1 - bits[j - 1]) // 2
            st0.append((R, R1))
        D = []; ok = True
        for j in range(1, m + 1):
            beta = bits[j - 1]; R, R1 = st0[j - 1]
            umin = 1 if beta else 0
            if cls == 'A':
                if j == 1:
                    u = 1 if beta else 0
                    v = rnd(r, 1 if beta else 2, big)
                else:
                    ub = R1 + umin + rnd(r, 0, big); ub += (ub % 2 == 0)
                    u = ub - R1
                    v = R + 1 + rnd(r, 0, big)
            else:
                if cls == 'B' and j == 1:
                    u, v = 0, 1
                else:
                    need = 2 ** (j - 1) if cls == 'B' else 2 ** j
                    ub = max(need, R1 + umin) + rnd(r, 0, big)
                    u = ub - R1
                    v = rnd(r, 1, big)
                    if (v + beta) % 2 == 0: v += 1
                    if j == m and v - R < 1:
                        v = R + 1 + (R + 1 + beta + 1) % 2
            if u < umin: ok = False
            D.append((u, beta, v))
        if not ok:
            continue
        st, V = stats(D)
        Rtot = 2 ** m - 1 - V
        Tmin = 2 if cls == 'C' else 0
        b = 2 * V - 1 + Tmin + 2 * rnd(r, 0, big // 4)
        if b < 1: b = 1
        if b % 2 == 0: b += 1
        Smin = 0 if cls == 'B' else 1
        a = max(1, 2 ** (m + 1) - 2 + Smin - Rtot) + rnd(r, 0, big)
        if (a + Rtot) % 2: a += 1
        if inv(D, a, b) == cls:
            return D, a, b
    return None

# ---------------------------------------------------------------- window lemmas (proof.md 2.1)
# 'X>' = head in state X on the next cell; '<X' = head in state X on the previous cell.
LEM = {
    'S1': ('10<C', '<C01', 2), 'S2': ('01<D', '<D10', 2), 'S3': ('A>10', '01A>', 2), 'S4': ('E>01', '10E>', 2),
    'S5': ('1011<D', '11<D01', 6), 'S6': ('01<C0', '<C001', 6),
    'T1': ('00<C', '10E>', 3), 'T2': ('E>000', '<C001', 5), 'T3': ('E>001', '110E>', 3),
    'T4': ('E>10', '11A>', 2), 'T5': ('A>01', '10E>', 2), 'T6': ('A>00', '<D01', 3), 'T7': ('11<D', '<D00', 2),
    'T8': ('11011<D', '<C00001', 9), 'T9': ('E>1001000', '<C0001001', 13), 'T10': ('11<C', '<C00', 2),
    'T11': ('0<C', '<D1', 1), 'T12': ('00011<D', '10110E>', 13), 'T13': ('E>101', '110E>', 3),
    'T14': ('1011<C', '<C0100', 4),
}
# kill #11's lemmas (its proof.md 2.1), as data, for the mirror cross-check
LEM11 = {
    'S1': ('B>01', '10B>', 2), 'S2': ('C>10', '01C>', 2), 'S3': ('01<D', '<D10', 2), 'S4': ('10<E', '<E01', 2),
    'S5': ('C>1101', '10C>11', 6), 'S6': ('0B>10', '100B>', 6),
    'T1': ('B>00', '<E01', 3), 'T2': ('000<E', '100B>', 5), 'T3': ('100<E', '<E011', 3),
    'T4': ('01<E', '<D11', 2), 'T5': ('10<D', '<E01', 2), 'T6': ('00<D', '10C>', 3), 'T7': ('C>11', '00C>', 2),
    'T8': ('C>11011', '10000B>', 9), 'T9': ('0001001<E', '1001000B>', 13), 'T10': ('B>11', '00B>', 2),
    'T11': ('B>0', '1C>', 1), 'T12': ('C>11000', '<E01101', 13), 'T13': ('101<E', '<E011', 3),
    'T14': ('B>1101', '0010B>', 4),
}
PI = {'A': 'B', 'B': 'C', 'C': 'D', 'D': 'A', 'E': 'E', 'F': 'F'}   # #11 state -> this machine's state

def parse_window(w):
    """-> (cells, head index (may be -1 or len), state)."""
    i = w.find('>')
    if i > 0 and w[i - 1] in 'ABCDEF':
        return w[:i - 1] + w[i + 1:], i - 1, w[i - 1]
    i = w.find('<')
    return w[:i] + w[i + 2:], i - 1, w[i + 1]

def mirror_window(w):
    c, h, st = parse_window(w)
    return c[::-1], len(c) - 1 - h, PI[st]

def lemma_run(lhs, rhs, n):
    """exact window run. Returns (ok, transitions used, F-reads)."""
    c, h, st = parse_window(lhs); c2, h2, st2 = 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

# ---------------------------------------------------------------- chains (proof.md 2.2, 2.3)
# A configuration is (left, mode, state, right): the tape reads left+right; mode '>' = head on right[0],
# '<' = head on left[-1] (left may be '', then the head is on the blank cell left of right).
# Chains are aligned at their RIGHT end, which never moves (the right end carries a '000' margin in O).
def M_chain(pre, us, vs, ones, a, b):
    """M on K(pre ++ [(us,0,vs)] ++ [(u,1,v) for (u,v) in ones]; a, b). pre = digits d_1..d_{j*-1}
    (MSB first); ones = (u,v) of d_{j*+1}..d_m. Returns c0, links, offset-from-right of the cell the
    head must reach at most (the right 0 of d_{j*}'s 00)."""
    Xm = ''.join(dig(d) for d in reversed(pre)) + '1001'
    F = '10' * vs + '00' + '01' * us
    Ym = ''.join('10' * v + '01' * u for (u, v) in reversed(ones))
    ln = []
    def L(name, n, l, mo, st, r): ln.append((name, n, (l, mo, st, r)))
    c0 = ('', '<', 'C', '01' * b + '000' + '01' * a + Ym + F + Xm)
    R0 = '01' * a + Ym + F + Xm
    # phase 1: left-edge preamble with a dip into the 000 gap
    L('T1', 1, '10', '>', 'E', '01' * b + '000' + R0)
    L('S4', b, '10' * (b + 1), '>', 'E', '000' + R0)
    L('T2', 1, '10' * (b + 1), '<', 'C', '001' + R0)
    L('S1', b + 1, '', '<', 'C', '01' * (b + 1) + '001' + R0)
    # phase 2: one long right sweep to the 00 of d_{j*}
    L('T1', 1, '10', '>', 'E', '01' * (b + 1) + '0' + '01' * (a + 1) + Ym + F + Xm)
    L('S4', b + 1, '10' * (b + 2), '>', 'E', '0' + '01' * (a + 1) + Ym + F + Xm)
    L('T3', 1, '10' * (b + 2) + '110', '>', 'E', '01' * a + Ym + F + Xm)
    Lc = '10' * (b + 2) + '110' + '10' * a
    L('S4', a, Lc, '>', 'E', Ym + F + Xm)
    rev = list(reversed(ones))                               # d_m first: the sweep goes left to right
    for i, (u, v) in enumerate(rev):                          # Lb on each bit-1 digit
        rest = ''.join('10' * vv + '01' * uu for (uu, vv) in rev[i + 1:]) + F + Xm
        L('T4', 1, Lc + '11', '>', 'A', '10' * (v - 1) + '01' * u + rest)
        L('S3', v - 1, Lc + '11' + '01' * (v - 1), '>', 'A', '01' * u + rest)
        L('T5', 1, Lc + '11' + '01' * (v - 1) + '10', '>', 'E', '01' * (u - 1) + rest)
        Lc = Lc + '11' + '01' * (v - 1) + '10' * u
        L('S4', u - 1, Lc, '>', 'E', rest)
    # Lf: flip d_{j*}
    L('T4', 1, Lc + '11', '>', 'A', '10' * (vs - 1) + '00' + '01' * us + Xm)
    L('S3', vs - 1, Lc + '11' + '01' * (vs - 1), '>', 'A', '00' + '01' * us + Xm)
    L('T6', 1, Lc + '11' + '01' * (vs - 1), '<', 'D', '01' + '01' * us + Xm)
    Rc = '10' * (vs - 1) + '01' * (us + 1) + Xm
    L('S2', vs - 1, Lc + '11', '<', 'D', Rc)
    # phase 3: leftward pass with 2-cell back-bounces (Rb on each swept digit), then the a block and the edge
    base = '10' * (b + 2) + '110' + '10' * a
    for i, (u, v) in enumerate(ones):                         # d_{j*+1} first: right to left
        Lpre = base + ''.join('11' + '01' * (vv - 1) + '10' * uu for (uu, vv) in reversed(ones[i + 1:]))
        L('S5', u, Lpre + '11' + '01' * (v - 1) + '11', '<', 'D', '01' * u + Rc)
        L('T7', 1, Lpre + '11' + '01' * (v - 1), '<', 'D', '00' + '01' * u + Rc)
        Rc = '10' * (v - 1) + '00' + '01' * u + Rc
        L('S2', v - 1, Lpre + '11', '<', 'D', Rc)
    L('S5', a, '10' * (b + 2) + '110' + '11', '<', 'D', '01' * a + Rc)
    L('T8', 1, '10' * (b + 2), '<', 'C', '00001' + '01' * a + Rc)
    L('S1', b + 2, '', '<', 'C', '01' * (b + 2) + '00001' + '01' * a + Rc)
    right00 = len(F) - 2 * vs - 2 + len(Xm)                  # cells right of the right 0 of the 00
    return c0, ln, right00

def O_chain(ones, a, b):
    """O on the all-ones K([(u,1,v) for (u,v) in ones]; a, b), MSB first; ones may be [] (m = 0).
    The right end carries a 3-cell '000' margin after the 1001, for T9."""
    Ym = ''.join('10' * v + '01' * u for (u, v) in reversed(ones))
    ln = []
    def L(name, n, l, mo, st, r): ln.append((name, n, (l, mo, st, r)))
    c0 = ('', '<', 'C', '01' * b + '000' + '01' * a + Ym + '1001000')
    R0 = '01' * a + Ym + '1001000'
    L('T1', 1, '10', '>', 'E', '01' * b + '000' + R0)                                # phase 1
    L('S4', b, '10' * (b + 1), '>', 'E', '000' + R0)
    L('T2', 1, '10' * (b + 1), '<', 'C', '001' + R0)
    L('S1', b + 1, '', '<', 'C', '01' * (b + 1) + '001' + R0)
    L('T1', 1, '10', '>', 'E', '01' * (b + 1) + '0' + '01' * (a + 1) + Ym + '1001000')  # phase 2
    L('S4', b + 1, '10' * (b + 2), '>', 'E', '0' + '01' * (a + 1) + Ym + '1001000')
    L('T3', 1, '10' * (b + 2) + '110', '>', 'E', '01' * a + Ym + '1001000')
    Lc = '10' * (b + 2) + '110' + '10' * a
    L('S4', a, Lc, '>', 'E', Ym + '1001000')
    rev = list(reversed(ones))
    for i, (u, v) in enumerate(rev):
        rest = ''.join('10' * vv + '01' * uu for (uu, vv) in rev[i + 1:]) + '1001000'
        L('T4', 1, Lc + '11', '>', 'A', '10' * (v - 1) + '01' * u + rest)
        L('S3', v - 1, Lc + '11' + '01' * (v - 1), '>', 'A', '01' * u + rest)
        L('T5', 1, Lc + '11' + '01' * (v - 1) + '10', '>', 'E', '01' * (u - 1) + rest)
        Lc = Lc + '11' + '01' * (v - 1) + '10' * u
        L('S4', u - 1, Lc, '>', 'E', rest)
    L('T9', 1, Lc, '<', 'C', '0001001')                                               # phase 3: far-right turn
    Rc = '0001001'
    base = '10' * (b + 2) + '110' + '10' * a
    for i, (u, v) in enumerate(ones):                                                 # phase 4: Ro, d_1 first
        Lpre = base + ''.join('11' + '01' * (vv - 1) + '10' * uu for (uu, vv) in reversed(ones[i + 1:]))
        L('S1', u, Lpre + '11' + '01' * (v - 1), '<', 'C', '01' * u + Rc)
        L('S6', v - 1, Lpre + '11', '<', 'C', '0' + '01' * (v - 1) + '1' + '01' * (u - 1) + Rc)
        Rc = '000' + '01' * (v - 1) + '1' + '01' * (u - 1) + Rc
        L('T10', 1, Lpre, '<', 'C', Rc)
    L('S1', a, '10' * (b + 2) + '110', '<', 'C', '01' * a + Rc)                       # phase 5: left end
    L('T11', 1, '10' * (b + 2) + '11', '<', 'D', '1' + '01' * a + Rc)
    L('S5', b + 2, '11', '<', 'D', '01' * (b + 2) + '1' + '01' * a + Rc)
    L('T12', 1, '10110', '>', 'E', '01' * (b + 2) + '1' + '01' * a + Rc)
    L('S4', b + 2, '10110' + '10' * (b + 2), '>', 'E', '1' + '01' * a + Rc)
    L('T13', 1, '10110' + '10' * (b + 2) + '110', '>', 'E', '01' * (a - 1) + Rc)       # phase 6: back over a
    Lz = '10110' + '10' * (b + 2) + '110' + '10' * (a - 1)
    L('S4', a - 1, Lz, '>', 'E', Rc)
    assert Rc.startswith('000')
    L('T2', 1, Lz, '<', 'C', '001' + Rc[3:])                                          # phase 7: turn, final run
    L('S1', a, '10110' + '10' * (b + 2) + '1', '<', 'C', '01' * a + '001' + Rc[3:])
    L('S6', b + 3, '1011', '<', 'C', '0' + '01' * (b + 3) + '1' + '01' * (a - 1) + '001' + Rc[3:])
    L('T14', 1, '', '<', 'C', '0100' + '0' + '01' * (b + 3) + '1' + '01' * (a - 1) + '001' + Rc[3:])
    return c0, ln

def run_chain(c0, ln, margin=64):
    """Run the real machine link by link from c0; after each link the whole tape, head and state must equal
    the link's configuration (right-aligned). Returns (ok, steps, max head as offset from the right end,
    final configuration as (left+right string stripped, head offset from the right end))."""
    l, mo, st, r = c0
    n = sum(LEM[nm][2] * k for (nm, k, _) in ln)
    full = l + r
    E = margin + n + len(full) + 8                     # right end (exclusive), fixed for the whole chain
    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(st) - 65; mx = h; tot = 0
    for (nm, k, (l2, mo2, st2, r2)) in ln:
        for _ in range(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]; tot += 1
            if h > mx: mx = h
            if h < 0 or h >= size:
                return False, tot, None, None
        if t != place(l2, r2) or h != hpos(l2, mo2, r2) or s != ord(st2) - 65:
            return False, tot, None, None
    lf, mof, stf, rf = ln[-1][2]
    return True, tot, E - 1 - mx, (stf, len(rf) - (0 if mof == '>' else -1))

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

def _O_case(ones, a, b):
    c0, ln = O_chain(ones, a, b)
    good, steps, mxoff, fin = run_chain(c0, ln)
    if ones:
        _, D2, a2, b2, st, _ = mstep([(u, 1, v) for (u, v) in ones], a, b)
    else:                                                       # O at m = 0 (proof.md 4)
        D2, a2, b2, st = [(1, 1, a)], b + 3, 1, 89 + 8 * a + 20 * b
    lf, mof, stf, rf = ln[-1][2]
    want = render(D2, a2, b2)[0]
    # the right end is the margin cell after the moved 1001: the result reads ... 1001 with no margin left
    endok = (lf == '' and mof == '<' and stf == 'C' and rf == want)
    return good and steps == st and mxoff == 0 and endok

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

def check_sweeps():
    ok = tot = 0
    for n in list(range(0, 12)) + [50, 333, 1000]:
        cases = [  # (cells, head, state, steps, cells', head', state')
            ('1' + '10' * n + '1', 2 * n, 'C', 2 * n, '1' + '01' * n + '1', 0, 'C'),          # S1 (10)^n <C
            ('1' + '01' * n + '1', 2 * n, 'D', 2 * n, '1' + '10' * n + '1', 0, 'D'),          # S2 (01)^n <D
            ('1' + '10' * n + '1', 1, 'A', 2 * n, '1' + '01' * n + '1', 1 + 2 * n, 'A'),      # S3 A> (10)^n
            ('1' + '01' * n + '1', 1, 'E', 2 * n, '1' + '10' * n + '1', 1 + 2 * n, 'E'),      # S4 E> (01)^n
            ('1' + '10' * n + '11', 2 * n + 2, 'D', 6 * n, '1' + '11' + '01' * n, 2, 'D'),    # S5 (10)^n 11 <D
            ('1' + '01' * n + '01', 2 * n, 'C', 6 * n, '1' + '0' + '01' * n + '1', 0, 'C'),   # S6 (01)^n <C 0
        ]
        for (c, h, s, k, c2, h2, s2) in cases:
            res = run(c, h, s, k)
            tot += 1; ok += same_cfg(res, c2, h2, s2)
    return report('1 sweeps', ok, tot, '(S1-S6, n in 0..11, 50, 333, 1000)')

def rand_digit(r, beta, big):
    return (rnd(r, 1 if beta else 0, big), beta, rnd(r, 1, big))

def check_M(r, N, big):
    ok = tot = 0; maxk = 0; drops = 0; rightok = 0; zero_u = 0
    for it in range(N):
        k = it % 7
        pre = [rand_digit(r, r.randint(0, 1), big) for _ in range(r.randint(0, 3))]
        flip = 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 = [rand_digit(r, 1, big) for _ in range(k)]
        D = pre + [flip] + ones
        a = rnd(r, 0, big); b = rnd(r, 0, big)
        name, D2, a2, b2, steps, info = mstep(D, a, b)
        s, h, q = render(D, a, b)
        res = run(s, h, q, steps)
        good = same_cfg(res, *render(D2, a2, b2))
        # the right 0 of d_{j*}'s 00, as an index into s
        i00r = len(s) - 4 - sum(len(dig(d)) for d in pre) - 2 * flip[0] - 1
        rgood = res[4] == i00r
        tot += 1; ok += good and rgood; rightok += rgood
        drops += info['drop'] is not None; maxk = max(maxk, k); zero_u += flip[0] == 0
        if not (good and rgood):
            print('  M FAIL', D, a, b, good, rgood)
    return report('2 rule M_k', ok, tot, '(k=0..%d, %d with a drop, %d with u*=0, a,b>=0; rightmost cell read = the right 0 '
                  'of the flipped 00: %d/%d)' % (maxk, drops, zero_u, rightok, tot))

def check_O(r, N, big):
    ok = tot = 0
    for it in range(N):
        n = 1 + it % 7
        D = [rand_digit(r, 1, big) for _ in range(n)]
        a = rnd(r, 1, big); b = rnd(r, 0, big)
        name, D2, a2, b2, steps, _ = mstep(D, a, b)
        s, h, q = render(D, a, b)
        res = run(s, h, q, steps)
        good = same_cfg(res, *render(D2, a2, b2))
        # rightmost read: 3 cells right of the old 1001's last cell
        good = good and res[4] == len(s) - 1 + 3
        tot += 1; ok += good
        if not good: print('  O FAIL', D, a, b)
    return report('3 rule O', ok, tot, '(m=1..7; rightmost cell read = 3 right of the old 1001)')

def check_init():
    ok = 0; tot = 0
    def chk(c, msg):
        nonlocal ok, tot
        tot += 1; ok += bool(c)
        if not c: print('  init FAIL:', msg)
    res = run('', 0, 'A', 82)
    chk(same_cfg(res, *render([], 3, 1)), 'step 82 = K(;3,1)')
    res = run('', 0, 'A', 215)
    chk(same_cfg(res, *render([(1, 1, 3)], 4, 1)), 'step 215 = K((1,1,3);4,1)')
    s, h, q = render([], 3, 1)
    chk(89 + 8 * 3 + 20 * 1 == 133 and same_cfg(run(s, h, q, 133), *render([(1, 1, 3)], 4, 1)),
        'K(;3,1) -133-> K((1,1,3);4,1), 133 = 89 + 8a + 20b at m=0')
    ks, halted = scan_K('A', 215)
    chk(halted is None and [(t, k) for t, k in ks] == [(82, ([], 3, 1)), (215, ([(1, 1, 3)], 4, 1))],
        'K-configs in steps 0..215: %s' % ks)
    chk(inv([], 3, 1) is None, 'K(;3,1) not in INV')
    D, a, b = [(1, 1, 3)], 4, 1
    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, 2, 0, 0, 0, 1, 3), 'derived %s' % dv)
    chk(inv(D, a, b) == 'A', 'class A')
    # Rocq-form (additive) INV of proof.md 6 at the base: Rof=0, a+R+2>=4, b+3+2R>=4, a+R+1>=4, LSB 3>=1
    chk(a + 0 + 2 >= 4 and b + 3 + 0 >= 4 and a + 0 + 1 >= 4 and 3 >= 0 + 1 and (a + 0) % 2 == 0, 'additive form')
    # the next macro step from the base: O (all bits 1) to K((0,0,1),(3,1,4);4,1), class B
    name, D2, a2, b2, st, _ = mstep(D, a, b)
    chk((name, D2, a2, b2, st) == ('O', [(0, 0, 1), (3, 1, 4)], 4, 1, 165) and inv(D2, a2, b2) == 'B',
        'next: O -> K((0,0,1),(3,1,4);4,1) class B')
    chk(same_cfg(run(*render(D, a, b), st), *render(D2, a2, b2)), 'next step on the machine')
    return report('4 init', ok, tot, '(blank -82-> K(;3,1) -133 (O at m=0)-> K((1,1,3);4,1) at step 215, class A: '
                  'V=1, R=0, S=2, T=0, ubar=1, vbar=3; no other K in 0..215; next O -> class B in %d steps)' % st)

def check_closure(Tmax):
    """the real machine from blank vs the abstract model at every macro boundary from step 215."""
    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')
    def go(n):
        nonlocal h, s
        t_ = tape; hh = h; ss = s
        for _ in range(n):
            tr = tab[ss][t_[hh]]
            if tr is None:
                raise Halt()
            t_[hh] = tr[0]; hh += tr[1]; ss = tr[2]
        h = hh; s = ss
    def matches(D, a, b):
        st_, hh, q = render(D, a, b)
        if s != 2:
            return False
        seg = st_.encode().translate(tr01)
        if tape[h + 1:h + 1 + len(seg)] != seg:
            return False
        return tape.count(1) == st_.count('1')
    go(215)
    D, a, b, t = [(1, 1, 3)], 4, 1, 215
    n = ok = int(matches(D, a, b)); names = Counter(); cls = Counter(); drops = Counter()
    while True:
        c = inv(D, a, b); cls[c] += 1
        if c is None:
            print('  closure: INV fails at', t); break
        name, D2, a2, b2, st, info = 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('5 closure', ok, n, '(K at 215 + 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))

def check_orbit(N):
    D, a, b, t = [(1, 1, 3)], 4, 1, 215
    cls = Counter(); drops = Counter(); ok = 0; ovf = 0
    for i in range(N):
        c = 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 = mstep(D, a, b); t += st
        ovf += name == 'O'
        if info.get('drop'): drops[info['drop']] += 1
    return report('6 orbit', ok, N, '(classes %s; drops %s; %d overflows; t=%.3g, %d digits)'
                  % (dict(cls), dict(drops), ovf, t, len(D)))

def check_induct(r, N):
    ok = tot = 0; trans = Counter(); drops = Counter(); fails = []
    for it in range(N):
        cls = 'ABC'[it % 3]
        m = 1 + r.randint(0, 9) if r.random() < 0.8 else 1 + r.randint(0, 2)
        if cls == 'B' and m < 2: m = 2
        big = r.choice([5, 40, 300, 5000])
        st = rand_inv_state(r, cls, m, big)
        if st is None:
            continue
        D, a, b = st
        tot += 1
        try:
            name, D2, a2, b2, steps, info = mstep(D, a, b)
        except ValueError as e:
            fails.append((cls, D, a, b, str(e))); continue
        c2 = inv(D2, a2, b2)
        good = c2 is not None and info.get('drop') != 'LSB' and steps >= 32
        ok += good
        trans[(cls, c2)] += 1
        if info.get('drop'): drops[info['drop']] += 1
        if not good: fails.append((cls, D, a, b, name, D2, a2, b2))
    for f in fails[:5]: print('  induct FAIL', f)
    return report('7 induction', ok, tot, '(transitions %s; drops %s; every step >= 32 machine steps)'
                  % (dict(sorted(trans.items(), key=str)), dict(drops)))

def check_induct_tm(r, N):
    ok = tot = 0
    for it in range(N):
        cls = 'ABC'[it % 3]
        m = 1 + r.randint(0, 5)
        if cls == 'B' and m < 2: m = 2
        st = 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 = mstep(D, a, b)
        res = run(*render(D, a, b), steps)
        tot += 1; ok += same_cfg(res, *render(D2, a2, b2))
    return report('8 induction-TM', ok, tot, '(random INV states, one macro step on the real machine)')

def check_drop_algebra(r, N):
    ok = tot = 0
    for _ in range(N):
        m = r.randint(2, 12); js = r.randint(1, m - 1)
        bits = [r.randint(0, 1) for _ in range(js - 1)] + [0] + [1] * (m - js)
        H = int(''.join(map(str, bits[:js - 1])) or '0', 2)
        V = int(''.join(map(str, bits)), 2)
        nd = bits[:js - 1] + [1] + [0] * (m - js)
        dr = bits[:js - 1] + [0] * (m - js)
        def RR1(bb, j):
            U = int(''.join(map(str, bb[:j])), 2); R = 2 ** j - 1 - U
            return R, (R + 1 - bb[j - 1]) // 2
        good = True
        for j in range(js + 1, m + 1):
            Rn, R1n = RR1(nd, j); Rp, R1p = RR1(dr, j - 1)
            good &= (Rn - Rp == 2 ** (j - js) * (2 ** (js - 1) - 1 - H))
            if j >= js + 2: good &= (2 * R1p == R1n + 2 ** (j - js - 1))
            else:           good &= (R1p == RR1(bits, js)[1])
            if js == 1: good &= (Rn == Rp and R1n == R1p)      # a falling top changes nothing below
        Vp = int(''.join(map(str, dr)) or '0', 2)
        good &= (V + 1 - Vp == (H + 1) * 2 ** (m - js))
        Rtot0 = 2 ** m - 1 - V; Rtotp = 2 ** (m - 1) - 1 - Vp
        dS = (1 + Rtotp - 2 ** m + 2) - (Rtot0 - 2 ** (m + 1) + 2)
        good &= (dS == 2 ** (m - 1) + (H + 1) * 2 ** (m - js))
        good &= ((Rtotp - (Rtot0 - 1)) % 2 == 0)
        tot += 1; ok += good
    return report('9 drop algebra', ok, tot, '(m=2..12, every j*)')

def relabel(tab, perm, mirror):
    """perm: list, perm[s] = new name of state s. Returns the table string."""
    inv_ = [0] * 6
    for s, p in enumerate(perm): inv_[p] = s
    out = []
    for p in range(6):
        s = inv_[p]; row = ''
        for sym in (0, 1):
            tr = tab[s][sym]
            if tr is None: row += '---'
            else:
                w, d, t = tr
                if mirror: d = -d
                row += '%d%s%s' % (w, 'R' if d == 1 else 'L', chr(65 + perm[t]))
        out.append(row)
    return '_'.join(out)

def check_table():
    ok = tot = 0
    def chk(c, msg):
        nonlocal ok, tot
        tot += 1; ok += bool(c)
        if not c: print('  table FAIL:', msg)
    lines = open(HOLDOUTS).read().split('\n')
    chk(len(lines) > 34 and lines[33] == TM, 'line 34 of the 778 list')
    import glob, csv
    snaps = sorted(f for f in glob.glob(os.path.join(os.path.dirname(HOLDOUTS), '*.txt')) if 'eqv' not in f)
    chk(len(snaps) == 26 and all(TM in set(x.strip() for x in open(f)) for f in snaps),
        'on all %d snapshots 2024-06-14 .. 2026-10-07' % len(snaps))
    sheet = '[local working file]'
    res_rows = [row for row in csv.reader(open(sheet + '2026-10-09_results.csv')) if row and row[0] == TM]
    lv0_rows = [row for row in csv.reader(open(sheet + '2026-10-09_level-0.csv')) if row and row[0] == TM]
    chk(res_rows == [[TM, '', 'Skelet 1-like Class 2', 'Machine with the most common transitions', '', '']]
        and len(lv0_rows) == 1 and 'Fun fact: machine with the most common transitions' in lv0_rows[0],
        'sheet rows %s %s' % (res_rows, lv0_rows))
    perm11 = [ord(PI[c]) - 65 for c in 'ABCDEF']
    chk(relabel(parse_tm(TM11), perm11, True) == TM, 'mirror + rename of #11')
    hs = set(x.strip() for x in lines if x.strip())
    found = {}
    for perm in itertools.permutations(range(6)):
        for mir in (False, True):
            sname = relabel(TT, list(perm), mir)
            if sname in hs:
                start = chr(65 + perm.index(0))           # the state of THIS table that becomes A
                found.setdefault(sname, set()).add((start, mir))
    want = {TM: {('A', False)}, TM11: {('B', True)},
            '1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---': {('C', True)},
            '1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---': {('D', False)}}
    chk(found == want, 'relabelings found: %s' % found)
    # the equivalence file keeps the four in separate groups; this machine is a singleton group
    groups = [g.split() for g in open(os.path.join(os.path.dirname(HOLDOUTS), '2026-10-07_eqv_1590.txt')).read()
              .replace('\r', '').split('\n\n') if g.strip()]
    gid = {x: i for i, g in enumerate(groups) for x in g}
    chk(len(groups) == 778 and len({gid.get(x) for x in want}) == 4 and None not in {gid.get(x) for x in want}
        and groups[gid[TM]] == [TM], 'eqv_1590 groups')
    dis = glob.glob('[local working file]')
    chk(len(dis) == 2 and not any(TM in open(f).read() for f in dis), 'not on the data/discord lists')
    inits = {}
    for st, (tt, D, a, b) in {'A': (215, [(1, 1, 3)], 4, 1), 'B': (483, [(1, 1, 2)], 8, 5),
                              'C': (732, [(1, 1, 10)], 8, 1), 'D': (687, [(1, 1, 9)], 8, 1)}.items():
        ks, halted = scan_K(st, tt)
        first = next(((t, k) for t, k in ks if inv(*k)), None)
        chk(halted is None and first == (tt, (D, a, b)) and inv(D, a, b) == 'A', 'start %s: %s' % (st, ks))
        inits[st] = (tt, [t for t, k in ks if t < tt])
    return report('10 table', ok, tot, '(line 34; on all 26 snapshot files; sheet: Results class + note, Level 0 fun fact; not on data/discord lists; = #11 mirrored, A..F -> B,C,D,A,E,F; 4 holdouts share the table '
                  '(starts A, B mirror, C mirror, D); first INV K from blank per start [step, earlier K steps]: %s)' % inits)

def check_lemmas():
    ok = 0; fs = []; trs_all = {}
    for name, (lhs, rhs, n) in LEM.items():
        good, trs, fr = lemma_run(lhs, rhs, n)
        # mirror of #11's lemma of the same name
        l11, r11, n11 = LEM11[name]
        mm = (mirror_window(l11) == parse_window(lhs) and mirror_window(r11) == parse_window(rhs) and n11 == n)
        ok += good and mm
        trs_all[name] = ' '.join(trs)
        fs += [(name, x) for x in fr]
        if not (good and mm): print('  lemma FAIL', name, lhs, rhs, good, mm)
    fok = all(x == 0 for _, x in fs) and sorted({nm for nm, _ in fs}) == ['T13', 'T4', 'T9']
    only_e1 = [(chr(65 + s), sym) for s in range(6) for sym in (0, 1) if TT[s][sym] and TT[s][sym][2] == 5] == [('E', 1)]
    for name in LEM:
        print('    %-4s %-10s -> %-10s %2d  %s' % (name, LEM[name][0], LEM[name][1], LEM[name][2], trs_all[name]))
    return report('11 lemmas', ok + fok + only_e1, len(LEM) + 2,
                  '(20 windows exact on this table and equal to #11\'s mirrored; F entered only in %s, by E1 (the only '
                  'transition into F), reading 0 every time)' % ','.join(sorted({nm for nm, _ in fs})))

def check_M_chain(r, quick):
    ok = tot = 0
    pres = [[], [(1, 1, 1)], [(0, 0, 2)], [(2, 1, 3), (1, 0, 1)]]
    kmax = 2 if quick else 3
    for pre in pres:
        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)
    box = tot
    for _ in range(100 if quick else 500):
        pre = [rand_digit(r, r.randint(0, 1), 30) for _ in range(r.randint(0, 3))]
        ones = [(rnd(r, 1, 60), rnd(r, 1, 60)) for _ in range(r.randint(0, 7))]
        args = (pre, rnd(r, 0, 60), rnd(r, 1, 60), ones, rnd(r, 0, 300), rnd(r, 0, 300))
        tot += 1; g = _M_case(*args); ok += g
        if not g: print('  M chain FAIL', args)
    return report('12 M chain', ok, tot, '(box: %d configs, u*<=2, v*<=3, k<=%d, u,v<=2, a<=3 (a=0 incl.), b<=2, '
                  '4 right contexts; plus %d random, k<=7, values up to 360)' % (box, kmax, tot - box))

def check_O_chain(r, quick):
    ok = tot = 0
    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)
    box = tot
    for _ in range(60 if quick else 300):
        ones = [(rnd(r, 1, 60), rnd(r, 1, 60)) for _ in range(r.randint(0, 8))]
        args = (ones, rnd(r, 1, 300), rnd(r, 0, 300))
        tot += 1; g = _O_case(*args); ok += g
        if not g: print('  O chain FAIL', args)
    i0 = _O_case([], 3, 1)
    return report('13 O chain', ok + i0, tot + 1, '(box: %d configs, m=0..%d, u,v<=3 (<=2 at m=4), a<=3 (<=4 at m=0), b<=2 '
                  '(<=4 at m=0); plus %d random, m<=8 (m=0 incl.); plus the init leg K(;3,1) -> K((1,1,3);4,1))'
                  % (box, mmax, tot - box))


# ---------------------------------------------------------------- Rocq interface (proof.md 6; Review log, gap 1)
# Text checks on kill #11's .v (read as data, never imported or compiled here) and on this machine's
# rocq/ scratch files.  They back the claim of proof.md 6 that #11's abstract part carries over
# unchanged once M_spec / Mdrop_spec / O_spec are proved on this table.
HERE = os.path.dirname(os.path.abspath(__file__))
V11 = os.path.join(os.path.dirname(HERE), TM11, TM11 + '.v')
IFACE = {'tm', 'dg', 'd0', 'd1', 'K', 'map0', 'map1', 'Oz', 'Oout', 'M_spec', 'Mdrop_spec', 'O_spec', 'init'}
SPECS = ('M_spec', 'Mdrop_spec', 'O_spec')

def _nocomment(x):
    out, d, i = [], 0, 0
    while i < len(x):
        if x.startswith('(*', i):
            d += 1; i += 2; continue
        if d and x.startswith('*)', i):
            d -= 1; i += 2; continue
        if not d:
            out.append(x[i])
        i += 1
    return ''.join(out)

def _ws(x):
    return ' '.join(x.split())

def _spec11(src, name):
    m = re.search(r'^Lemma %s ([^:]*):(.*?)\.\nProof\.' % re.escape(name), src, re.S | re.M)
    return m.group(1).strip(), _ws(m.group(2))

def check_interface():
    ok = tot = 0
    def chk(c, msg):
        nonlocal ok, tot
        tot += 1; ok += bool(c)
        if not c: print('  interface FAIL:', msg)
    import hashlib
    s11 = open(V11).read()
    c11 = _nocomment(s11)
    i = c11.index('Open Scope nat_scope.')
    mach, abst = c11[:i], c11[i:]
    # (a) the abstract part uses the machine part only through IFACE, and never unfolds K
    names = set(re.findall(r'^\s*(?:Lemma|Definition|Fixpoint|Inductive|Ltac|Theorem|Corollary|Notation)\s+"?([A-Za-z_][\w\']*)',
                           mach, re.M)) | {'d0', 'd1'}
    used = names & set(re.findall(r"[A-Za-z_][\w']*", abst))
    chk(used == IFACE, 'machine-part names used by #11\'s abstract part: %s' % sorted(used))
    nk_abs = len(re.findall(r'\bunfold\b[^.]*\bK\b', abst))
    nk_mach = len(re.findall(r'\bunfold\b[^.]*\bK\b', mach))
    chk(nk_abs == 0 and nk_mach >= 1, 'unfold K: %d in the abstract part, %d in the machine part' % (nk_abs, nk_mach))
    kref = [ln.strip() for ln in abst.split('\n') if re.search(r'\bK\b', ln)]
    chk(len(kref) == 2 and kref[0].startswith('Definition Kc') and kref[1].startswith('change (K [d1 1 2] 8 5)'),
        'K occurs in the abstract part only in Kc and in nonhalt\'s change: %s' % kref)
    # (b) proof.md 6 quotes #11's three spec statements word for word
    pm = open(os.path.join(HERE, 'proof.md')).read()
    for name in SPECS:
        _, st = _spec11(s11, name)
        q = [_ws(ln.split(':', 1)[1]) for ln in pm.split('\n') if re.match(r'\s*%s\s+:' % name, ln)]
        chk(q == [st], 'proof.md 6 quotes %s as in #11: %s vs %s' % (name, q, st))
    # (c) dg and K's signature are #11's, in this machine's compiled plan_check.v
    plan = open(os.path.join(HERE, 'rocq', 'plan_check.v')).read()
    dgl = 'Inductive dg := d0 (u v : nat) | d1 (u v : nat).'
    ksig = 'Definition K (ds : list dg) (a b : nat) : Q * tape :='
    chk(dgl in s11 and dgl in plan and ksig in s11 and ksig in plan, 'dg and K signature as in #11')
    # (d) rocq/abstract_check.v is #11's abstract part verbatim over this machine's plan_check.v,
    #     with #11's spec statements as its only hypotheses and only the base of nonhalt changed
    ab = open(os.path.join(HERE, 'rocq', 'abstract_check.v')).read()
    a0 = s11.index('Open Scope nat_scope.'); a1 = s11.index('Lemma nonhalt: ~halts tm c0.')
    chk(plan.rstrip() in ab and s11[a0:a1] in ab, 'abstract_check.v contains plan_check.v and #11\'s abstract part verbatim')
    for d in ('Definition map1 ', 'Definition map0 ', 'Fixpoint Oz ', 'Definition Oout '):
        j = s11.index(d); chk(s11[j:s11.index('.\n', j) + 2] in ab, '%sverbatim' % d)
    hyps = re.findall(r'^Hypothesis (\w+) : forall ([^,]*),(.*?)\.\n', ab, re.S | re.M)
    chk([h[0] for h in hyps] == list(SPECS) and
        all((b.strip(), _ws(p)) == _spec11(s11, n) for n, b, p in hyps), 'hypotheses = #11\'s spec statements')
    n1 = s11.index('Qed.', a1) + 4
    nh = s11[a1:n1].replace('K [d1 1 2] 8 5', 'K [d1 1 3] 4 1').replace('([d1 1 2], 8, 5)', '([d1 1 3], 4, 1)')
    chk(nh in ab and 'Lemma init: c0 -->* K [d1 1 3] 4 1.' in ab, 'nonhalt = #11\'s with base K [d1 1 3] 4 1; init proved')
    bad = re.findall(r'\b(Admitted|admit|Axiom|Parameter|Conjecture|Abort|Variable|Context)\b', _nocomment(ab))
    chk(not bad and len(re.findall(r'\bHypothesis\b', _nocomment(ab))) == 3, 'no other assumption in abstract_check.v: %s' % bad)
    # (e) its compile record is for this exact file: exit 0, closed, nonhalt with exactly the three premises
    log = open(os.path.join(HERE, 'rocq', 'abstract_check.out')).read()
    sha = hashlib.sha256(ab.encode()).hexdigest()
    chk(log.startswith(sha) and 'exit 0' in log and 'Closed under the global context' in log
        and log.count('-->+') == 3 and '~ halts tm c0' in log, 'rocq/abstract_check.out is a clean compile of this file')
    return report('14 interface', ok, tot, '(#11\'s abstract part uses only %s, never unfolds K; proof.md 6 quotes the 3 specs verbatim; '
                  'rocq/abstract_check.v = #11\'s abstract part verbatim over this machine\'s K/init, specs as hypotheses, '
                  'compile record clean)' % '/'.join(sorted(IFACE)))


if __name__ == '__main__':
    ap = argparse.ArgumentParser()
    ap.add_argument('--seed', type=int, default=33)
    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('--quick', action='store_true')
    A = ap.parse_args()
    r = random.Random(A.seed)
    if A.quick:
        A.orbit, A.induct, A.tm_steps = 2e4, 2e4, 2e6
    print('check_proof.py for %s (seed %d)' % (TM, A.seed))
    res = [check_sweeps(),
           check_M(r, 700 if not A.quick else 140, 300),
           check_O(r, 350 if not A.quick else 70, 300),
           check_init(),
           check_closure(int(A.tm_steps)),
           check_orbit(int(A.orbit)),
           check_induct(r, int(A.induct)),
           check_induct_tm(r, 3000 if not A.quick else 300),
           check_drop_algebra(r, 20000),
           check_table(),
           check_lemmas(),
           check_M_chain(r, A.quick),
           check_O_chain(r, A.quick),
           check_interface()]
    print('ALL PASS' if all(res) else 'SOME CHECKS FAILED')
    sys.exit(0 if all(res) else 1)