#!/usr/bin/env python3
"""check_proof.py -- evidence for proof.md of 1RB0LC_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- (twin of kill #11).

Self-contained: its own Python simulator, plus two small C helpers (embedded below, compiled with gcc
into a temp dir) for the long runs.  Every numbered claim in proof.md is checked here.

  python3 -B check_proof.py [--seed S] [--n N] [--cover-all T1] [--cover-other T2] [--quick]

  1  table facts: halting = F reads 1; F is entered only by E1; E only by D1 (A1 = 0LC, not 0LE)
  2  token machine (proof.md 1.3): all 28 (state, token) entries against the cell machine
  3  24 atomic window lemmas: exact finite runs inside the window; F entered only in T4/T9/T13, reads 0
  4  bounce lemma Lt for v = 1..40 (8v+1 steps), and its chain T4 S3^(v-1) T5b S6^(v-1) T10
  5  M, O, P on random K-configs: exact tape + exact step count on the real machine
  6  P chain (proof.md 3.3), link by link: the stated intermediate configurations, head and state
  7  initial segment: blank tape -> K-configs at steps 142, 283, 428, 609; 142->283 is O, 283->428 is P,
     428->609 is none of M/O/P (it is O* with turn T2, proof.md 3.5)
  8  transition census to T2 (default 1e9) via the C K-dumper: M / P / O / other counts, 0 mismatches;
     and the census by the general rule G (proof.md 3.5): every transition predicted exactly, by turn
  9  coverage: every step of every K->K transition to T1 (default 1e7), and of every non-M transition to
     T2, lies inside one of 23 atomic windows (greedy decomposition, no uncovered step; T3j left out).
     Weak evidence only (proof.md 6): it says the run uses no other local patterns
 10  arithmetic is needed: K((1,0,2); 2, 1) halts at step 2535; in the exhaustive box of proof.md 5,
     807 of 5472 canonical configs halt within 2e6 steps; G predicts every macro step of the halting run
     and its last K-config (step 2384) is in class H1
 11  general rule G (proof.md 3.5) on random K-configs, per turn (Lf, T3S2, Jc, T2, Lt), with random
     unread text left of the turn and an optional Lb1 digit: exact tape, head, state and step count
 12  sweep case analysis (proof.md 3.6): the left-moving automaton read off the table; every left text X
     of length <= 14 (blank-padded, not ending in 10) is in exactly one class; for the covered classes G
     is exact, for H1/H2 the machine halts inside the macro step
"""
import sys, os, re, random, argparse, subprocess, tempfile, collections

TM = "1RB0LC_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---"
PARENT = "1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---"

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
TAB = parse_tm(TM)
ST = 'ABCDEF'
RESULTS = []
def report(name, ok, detail):
    RESULTS.append((name, ok))
    print('%-4s %-4s %s' % (name, 'PASS' if ok else 'FAIL', detail))
    sys.stdout.flush()

# ---------------------------------------------------------------- configurations
# A configuration is (cells: dict pos->bit, head pos, state).  For comparison we render it as
# (string from the leftmost 1 or head to the rightmost 1 or head, head offset in it, state).
def render(t, h, s):
    ones = [i for i, x in enumerate(t) if x]
    lo = min(ones + [h]); hi = max(ones + [h])
    return ''.join(str(t[i]) for i in range(lo, hi + 1)), h - lo, s

def parse_conf(w):
    """'X <E Y' (head on the last cell of X) or 'X E> Y' (head on the first cell of Y); spaces ignored;
    '0^inf' allowed at either end (ignored).  Returns (cells, head offset, state), blank-padded by 4."""
    w = w.replace('0^inf', '').replace(' ', '')
    m = re.search(r'<([A-F])', w)
    if m:
        L, R = w[:m.start()], w[m.end():]; h = len(L) - 1
    else:
        m = re.search(r'([A-F])>', w)
        L, R = w[:m.start()], w[m.end():]; h = len(L)
    return '0000' + L + R + '0000', h + 4, ST.index(m.group(1))

def run_from(w, n):
    """run n steps from the configuration word w; return render() triple or None on halt."""
    s0 = parse_conf(w)
    txt, h, s = s0
    pad = n + 8
    t = [0] * pad + [int(c) for c in txt] + [0] * pad
    h += pad
    for _ in range(n):
        tr = TAB[s][t[h]]
        if tr is None:
            return None
        t[h] = tr[0]; h += tr[1]; s = tr[2]
    return render(t, h, s)

def same(a, b):
    """compare two render() triples up to blank padding (heads aligned)"""
    if a is None or b is None:
        return False
    (ta, ha, sa), (tb, hb, sb) = a, b
    return (sa == sb and ta[:ha].lstrip('0') == tb[:hb].lstrip('0')
            and ta[ha:].rstrip('0') == tb[hb:].rstrip('0'))

def dig(D):
    return ''.join('10' * u + ('' if be else '00') + '01' * v for (u, be, v) in D)

def Kword(L, D, a, b):
    return L + dig(D) + '10' * a + '000' + '10' * b + ' B> 0^inf'

# ---------------------------------------------------------------- 1. table facts
def check_table():
    halts = [(ST[q], r) for q in range(6) for r in (0, 1) if TAB[q][r] is None]
    intoF = [(ST[q], r) for q in range(6) for r in (0, 1) if TAB[q][r] and TAB[q][r][2] == 5]
    intoE = [(ST[q], r) for q in range(6) for r in (0, 1) if TAB[q][r] and TAB[q][r][2] == 4]
    ok = halts == [('F', 1)] and intoF == [('E', 1)] and intoE == [('D', 1)]
    report('1', ok, 'halting only F1: %s; F entered only by %s; E entered only by %s; A1 = 0LC (parent 0LE)'
           % (halts, intoF, intoE))

# ---------------------------------------------------------------- 2. token machine
# left-moving: head at a 2-cell boundary in state X, about to enter the token on its left.
# right-moving: head at a boundary in state B or C' (C reading the first cell of the token on its right).
TOKL = {  # (state, token) -> (new token, state, direction)   'H' = halt
    ('E', '10'): ('01', 'E', 'L'), ('E', '00'): ('11', 'A', 'L'), ('E', '01'): ('11', 'D', 'L'), ('E', '11'): 'H',
    ('D', '01'): ('10', 'D', 'L'), ('D', '11'): ('10', 'F', 'L'), ('D', '10'): ('01', 'C', 'L'), ('D', '00'): ('10', 'C', 'R'),
    ('F', '10'): ('01', 'E', 'L'), ('F', '00'): ('11', 'A', 'L'), ('F', '01'): 'H', ('F', '11'): 'H',
    ('A', '01'): ('10', 'D', 'L'), ('A', '11'): ('01', 'C', 'R'), ('A', '00'): ('01', 'B', 'R'), ('A', '10'): ('11', 'B', 'R'),
    ('C', '10'): ('01', 'E', 'L'), ('C', '00'): ('11', 'A', 'L'), ('C', '01'): ('00', 'B', 'R'), ('C', '11'): ('10', 'B', 'R'),
}
TOKR = {
    ('B', '01'): ('10', 'B', 'R'), ('B', '11'): ('00', 'B', 'R'), ('B', '00'): ('01', 'E', 'L'), ('B', '10'): ('11', 'A', 'L'),
    ('C', '10'): ('01', 'C', 'R'), ('C', '11'): ('00', 'C', 'R'), ('C', '00'): ('10', 'D', 'L'), ('C', '01'): ('11', 'D', 'L'),
}
def tok_run(tok, s, side):
    """window = 1 guard cell, the token, 1 guard cell.  Run until the head leaves the token; return
    (new token, state, direction) or 'H'."""
    t = [0, int(tok[0]), int(tok[1]), 0]
    h = 2 if side == 'L' else 1
    q = ST.index(s)
    for _ in range(10):
        tr = TAB[q][t[h]]
        if tr is None:
            return 'H'
        t[h] = tr[0]; h += tr[1]; q = tr[2]
        if h == 0:
            return ('%d%d' % (t[1], t[2]), ST[q], 'L')
        if h == 3:
            return ('%d%d' % (t[1], t[2]), ST[q], 'R')
    return 'loop'

def check_tokens():
    bad = []
    for (s, tok), want in TOKL.items():
        if tok_run(tok, s, 'L') != want:
            bad.append((s, tok, 'L'))
    for (s, tok), want in TOKR.items():
        if tok_run(tok, s, 'R') != want:
            bad.append((s, tok, 'R'))
    report('2', not bad and len(TOKL) + len(TOKR) == 28,
           'token machine: %d/28 entries agree with the cell machine%s'
           % (28 - len(bad), '' if not bad else ' BAD %s' % bad))

# ---------------------------------------------------------------- 3. window lemmas
LEM = {  # name: (lhs, rhs, steps)   twin exits; '<X' = head on the cell left of the mark
    'S1': ('B>01', '10B>', 2), 'S2': ('C>10', '01C>', 2), 'S3': ('01<D', '<D10', 2), 'S4': ('10<E', '<E01', 2),
    'S4c': ('10<C', '<E01', 2), 'S5': ('C>1101', '10C>11', 6), 'S6': ('0B>10', '100B>', 6),
    'T1': ('B>00', '<E01', 3), 'T2': ('000<E', '100B>', 5), 'T2c': ('000<C', '100B>', 5),
    'T3': ('100<E', '<C011', 3), 'T3j': ('0100<E', '<D1011', 4), 'T4': ('01<E', '<D11', 2), 'T5': ('10<D', '<C01', 2), 'T5b': ('110<D', '010B>', 5),
    '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', '<C01101', 13), 'T13': ('101<E', '<E011', 3), 'T14': ('B>1101', '0010B>', 4),
}
PARENT_EXIT = {'T3': '<E011', 'T5': '<E01', 'T12': '<E01101'}
def parse_window(w):
    i = w.find('>')
    if i > 0 and w[i - 1] in ST:
        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 run_window(lhs, n, trace=False):
    c, h, st = parse_window(lhs); t = [int(x) for x in c]; s = ST.index(st); tr_ = []
    for _ in range(n):
        if not (0 <= h < len(t)):
            return None
        tr = TAB[s][t[h]]
        if tr is None:
            return None
        tr_.append((ST[s], t[h]))
        t[h] = tr[0]; h += tr[1]; s = tr[2]
    out = (''.join(map(str, t)), h, ST[s])
    return (out, tr_) if trace else out

def check_windows():
    bad = []; fent = {}
    for name, (lhs, rhs, n) in LEM.items():
        c2, h2, s2 = parse_window(rhs)
        r = run_window(lhs, n, trace=True)
        if r is None or r[0] != (c2, h2, s2):
            bad.append(name); continue
        for (s, x) in r[1]:
            if s == 'F':
                fent.setdefault(name, set()).add(x)
    fok = set(fent) == {'T4', 'T9', 'T13'} and all(v == {0} for v in fent.values())
    report('3', not bad and fok and len(LEM) == 24,
           '24 atomic windows exact: %d/24 (T3/T5/T12 exit C where the parent exits E; S4c/T2c are the C-entry '
           'copies of S4/T2; T5b, T3j new); F entered in %s, always reading 0%s'
           % (24 - len(bad), sorted(fent), '' if not bad else ' BAD %s' % bad))

def check_Lt():
    ok = tot = 0
    for v in range(1, 41):
        lhs = '1' + '10' + '01' * v + '<E'
        want = ('01' + '10' * (v - 1) + '000', 3 + 2 * v, 'B')
        r = run_window(lhs, 8 * v + 1)
        tot += 1; ok += r == want
        # chain: T4 (2), S3^(v-1) (2 each), T5b (5), S6^(v-1) (6 each), T10 (2)  ->  8v+1
        ok += (2 + 2 * (v - 1) + 5 + 6 * (v - 1) + 2) == 8 * v + 1; tot += 1
    report('4', ok == tot, 'Lt: 1 10 (01)^v <E -> 01 (10)^(v-1) 000 B> in 8v+1 steps, v = 1..40, and the '
           'chain sum T4+S3^(v-1)+T5b+S6^(v-1)+T10 = 8v+1: %d/%d' % (ok, tot))

# ---------------------------------------------------------------- 5. macro rules
def M_rule(L, D, a, b):
    m = len(D); k = 0
    while D[m - 1 - k][1] == 1:
        k += 1
    js = m - 1 - k
    u, _, v = D[js]
    D2 = list(D[:js]) + [(u + 1, 1, v - 1)] + [(uu, 0, vv - 1) for (uu, _, vv) in D[js + 1:]]
    steps = 32 + 8 * a + 8 * b + 4 * v + sum(8 * uu + 4 * vv for (uu, _, vv) in D[js + 1:])
    return Kword(L, D2, a + 1, b + 2), steps

def O_rule(D, a, b):
    m = len(D); 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 Kword('1001', D2, b + 3, 1), steps

def P_tail(S, a):
    k = len(S); u = [d[0] for d in S]; v = [d[2] for d in S]
    if k == 1:
        return '10' * v[0] + '01' * a
    tail = '10' * (v[0] - 1) + '00' + '01' * u[1]
    for i in range(1, k - 1):
        tail += '10' * (v[i] - 1) + '00' + '01' * u[i + 1]
    return tail + '10' * v[k - 1] + '01' * a

def P_rule(L, S, a, b):
    k = len(S); u = [d[0] for d in S]; v = [d[2] for d in S]
    steps = 77 - 4 * k + 8 * a + 20 * b + 4 * sum(u) + 8 * sum(v)
    return L[:-1] + '01' + P_tail(S, a) + '10' * (b + 3) + '000' + '10' + ' B> 0^inf', steps

def rnd(r, lo, hi):
    return lo + r.randint(0, 2) if r.random() < 0.5 else r.randint(lo, hi)

def rand_left(r):
    kind = r.randint(0, 2)
    if kind == 0:
        return '1001' + dig([(rnd(r, 0, 9), r.randint(0, 1), rnd(r, 1, 9)) for _ in range(r.randint(0, 3))])
    if kind == 1:
        return '1001' + ''.join(r.choice(['10', '00', '01', '1', '0', '11']) for _ in range(r.randint(0, 12)))
    return '1'

def check_rules(r, N):
    okM = okO = okP = 0
    for _ in range(N):
        L = rand_left(r)
        D = [(rnd(r, 0, 20), 0, rnd(r, 1, 20))] + [(rnd(r, 2, 20), 1, rnd(r, 1, 20)) for _ in range(r.randint(0, 5))]
        a, b = rnd(r, 1, 40), rnd(r, 0, 40)
        want, n = M_rule(L, D, a, b)
        okM += same(run_from(Kword(L, D, a, b), n), parse_conf(want))
    for _ in range(N):
        D = [(rnd(r, 2, 20), 1, rnd(r, 1, 20)) for _ in range(r.randint(1, 6))]
        a, b = rnd(r, 1, 40), rnd(r, 0, 40)
        want, n = O_rule(D, a, b)
        okO += same(run_from(Kword('1001', D, a, b), n), parse_conf(want))
    for _ in range(N):
        if r.random() < 0.5:
            L = rand_left(r) + dig([(rnd(r, 0, 9), 0, rnd(r, 1, 9))] +
                                   [(rnd(r, 1, 9), r.randint(0, 1), rnd(r, 1, 9)) for _ in range(r.randint(0, 2))])
        else:
            L = '1001' + dig([(rnd(r, 1, 9), 1, rnd(r, 1, 9)) for _ in range(r.randint(0, 3))])
        if not L.endswith('1'):
            L += '01'
        S = [(1, 1, rnd(r, 1, 20))] + [(rnd(r, 2, 20), 1, rnd(r, 1, 20)) for _ in range(r.randint(0, 4))]
        a, b = rnd(r, 1, 40), rnd(r, 0, 40)
        want, n = P_rule(L, S, a, b)
        okP += same(run_from(Kword(L, S, a, b), n), parse_conf(want))
    report('5', okM == okO == okP == N, 'M %d/%d, O %d/%d, P %d/%d on random K-configs (exact tape, head, state '
           'after exactly the stated step count)' % (okM, N, okO, N, okP, N))

# ---------------------------------------------------------------- 6. P chain
def P_chain(L, S, a, b):
    """the intermediate configurations of proof.md 3.3, with cumulative step counts"""
    u = [d[0] for d in S]; v = [d[2] for d in S]; k = len(S)
    Yp = ''.join('01' * u[i] + '10' * (v[i] - 1) + '11' for i in range(1, k))   # swept d_{p+1..m}
    Y3 = ''.join('10' * (u[i] - 1) + '1' + '10' * (v[i] - 1) + '000' for i in range(1, k))
    tail = '01' * a + '011' + '01' * (b + 2)
    links = []
    n = 4 * b + 10
    links.append(('phase 1', L + dig(S) + '10' * (a + 1) + '0' + '10' * (b + 1) + ' B> 0^inf', n))
    n += 2 * a + 2 * b + 8 + sum(2 * u[i] + 2 * v[i] for i in range(1, k))
    links.append(('phase 2 (Lb on d_{p+1..m})', L + '10' + '01' * v[0] + ' <E ' + Yp + tail, n))
    n += 8 * v[0] + 1
    links.append(('Lt on d_p', L[:-1] + '01' + '10' * (v[0] - 1) + '000 B> ' + Yp + tail, n))
    n += sum(2 * u[i] + 6 * v[i] - 4 for i in range(1, k))
    links.append(('Ro on d_{p+1..m}', L[:-1] + '01' + '10' * (v[0] - 1) + '000' + Y3 + ' B> ' + tail, n))
    want, steps = P_rule(L, S, a, b)
    n += 2 * a + 8 * b + 30 + 2 * a + 1 + 2 * a + 6 * b + 27
    links.append(('phases 5-7 (as in O)', want, n))
    return links, steps

def check_P_chain(r, nrand):
    cases = []
    for Lc in ['1', '1001', '100101', '10011001', '1001' + dig([(2, 0, 1)]) + '01']:
        for v0 in (1, 2, 3):
            for k in (1, 2, 3):
                for a in (1, 2, 3):
                    for b in (0, 1, 2):
                        S = [(1, 1, v0)] + [(2 + (i % 2), 1, 1 + (i % 3)) for i in range(k - 1)]
                        cases.append((Lc, S, a, b))
    for _ in range(nrand):
        L = rand_left(r)
        if not L.endswith('1'):
            L += '01'
        S = [(1, 1, rnd(r, 1, 30))] + [(rnd(r, 2, 30), 1, rnd(r, 1, 30)) for _ in range(r.randint(0, 6))]
        cases.append((L, S, rnd(r, 1, 50), rnd(r, 0, 50)))
    ok = 0
    for (L, S, a, b) in cases:
        links, steps = P_chain(L, S, a, b)
        start = Kword(L, S, a, b)
        good = links[-1][2] == steps
        for (_, w, n) in links:
            good = good and same(run_from(start, n), parse_conf(w))
        ok += good
    report('6', ok == len(cases), 'P chain link by link (phase 1, phase 2, Lt, Ro, phases 5-7), exact config at '
           'every link and total = P step formula: %d/%d (box + %d random)' % (ok, len(cases), nrand))

# ---------------------------------------------------------------- 11/12. the general rule G (proof.md 3.5, 3.6)
# K(L; a, b): phase 1 and phase 2 as in M; the sweep then crosses the maximal swept suffix of L (Lb on bit-1
# digits with u >= 2, Lb1 on a u = 1 digit whose left cell is 0), and turns on the text X left of it.  C-exit
# turns are followed by Rb on the swept digits and M's right end; B-exit turns by Ro and O's phases 5-7.
def _seg(S, i, j):
    """S[i:j]; cells left of S are blank"""
    if i >= 0:
        return S[i:j]
    return '0' * (min(j, 0) - i) + (S[:j] if j > 0 else '')

def _runback(S, j, w):
    k = 0
    while _seg(S, j - 2, j) == w:
        k += 1; j -= 2
    return k, j

def g_turn(S, j):
    """turn on X = S[:j].  (name, keep, W, cost, exit): X is replaced by S[:keep] + W"""
    v, i = _runback(S, j, '01')
    if v >= 1 and _seg(S, i - 2, i) == '00':
        return 'Lf', i - 2, '10' + '01' * (v - 1), 4 * v + 1, 'C'      # 00 (01)^v      -> 10 (01)^(v-1) C> 11
    if _seg(S, j - 4, j) == '1100':
        return 'T3S2', j - 4, '01', 5, 'C'                             # 1100           -> 01 C> 11
    if _seg(S, j - 2, j) == '00':
        v, i = _runback(S, j - 2, '01')
        if v >= 1 and _seg(S, i - 2, i) == '00':
            return 'Jc', i - 2, '10' + '01' * v, 4 * v + 5, 'C'        # 00 (01)^v 00   -> 10 (01)^v C> 11
    if _seg(S, j - 3, j) == '000':
        return 'T2', j - 3, '100', 5, 'B'                              # 000            -> 100 B>
    return None, xclass(S[:j]), None, None, None

def xclass(X):
    """proof.md 3.6: the class of a left text X (blank-padded) that does not end in 10"""
    X = '0' * 6 + X
    v, i = _runback(X, len(X), '01')
    if v == 0 and X.endswith('11'):
        return 'H1'
    if v >= 1:
        e = X[:i]
        return 'Lf' if e.endswith('00') else 'H2' if e.endswith('111') else 'U1' if e.endswith('011') else '?'
    if X.endswith('000'):
        return 'T2'
    if X.endswith('1100'):
        return 'T3S2'
    if X.endswith('0100'):
        w, i = _runback(X, len(X) - 4, '01')
        e = X[:i]
        return 'Jc' if e.endswith('00') else 'U2' if e.endswith('10') else 'U3' if e.endswith('11') else '?'
    return '?'

def g_split(L):
    """maximal swept suffix of L: (j, swept digits left to right, Lt-turn or None)"""
    j = len(L); swept = []; t = None
    while True:
        v, i = _runback(L, j, '01')
        u, i2 = _runback(L, i, '10')
        if u == 0 or v == 0:
            break
        if u >= 2 or _seg(L, i2 - 1, i2) == '0':
            swept.append((u, v)); j = i2
            if u == 1:
                break                         # Lb1: exits C before a 0, the next cell is not a digit end
            continue
        t = ('Lt', i2 - 1, '01' + '10' * (v - 1) + '000', 8 * v + 1, 'B')  # 1 10 (01)^v -> 01 (10)^(v-1) 000 B>
        break
    return j, swept[::-1], t

def g_predict(L, a, b):
    """the general rule G.  returns ((type, turn, k), predicted K-word, steps) or (None, class, None)"""
    if a < 1:
        return None, 'a = 0', None
    j, swept, t = g_split(L)
    if t is None:
        t = g_turn(L, j)
        if t[0] is None:
            return None, t[1], None
    name, keep, W, cost, ex = t
    head = L[:keep] if keep > 0 else ''
    n = (4 * b + 10) + (2 * a + 2 * b + 8) + sum(2 * u + 2 * v for u, v in swept) + cost
    if ex == 'C':
        n += sum(6 * u + 2 * v for u, v in swept) + 6 * a + 2 * b + 13
        out = head + W + ''.join('10' * u + '00' + '01' * (v - 1) for u, v in swept) + '10' * (a + 1) + '000' + '10' * (b + 2)
        typ = 'M*'
    else:
        Z = head + W + ''.join('10' * (u - 1) + '1' + '10' * (v - 1) + '000' for u, v in swept)
        if not Z.endswith('000'):
            return None, 'O*-turn with no swept digit', None
        n += sum(2 * u + 6 * v - 4 for u, v in swept) + 6 * a + 14 * b + 58
        out = Z[:-3] + '100' + '10' * (a - 1) + '1' + '10' * (b + 3) + '000' + '10'
        typ = 'O*'
    return (typ, name, len(swept)), out.lstrip('0') + ' B> 0^inf', n

def check_general(r, N):
    res = collections.Counter(); bad = []
    def junk():
        return ''.join(r.choice('01') for _ in range(r.randint(0, 20)))
    for kind in ('Lf', 'T3S2', 'Jc', 'T2', 'Lt'):
        done = 0
        while done < N:
            Xp = junk()
            sw = [(rnd(r, 2, 15), rnd(r, 1, 15)) for _ in range(r.randint(1 if kind == 'T2' else 0, 4))]
            lb1 = kind in ('T2', 'T3S2', 'Jc') and r.random() < 0.3
            X = {'Lf': lambda: Xp + '00' + '01' * rnd(r, 1, 15), 'T3S2': lambda: Xp + '1100',
                 'Jc': lambda: Xp + '00' + '01' * rnd(r, 1, 15) + '00', 'T2': lambda: Xp + '000',
                 'Lt': lambda: Xp + '1' + '10' + '01' * rnd(r, 1, 15)}[kind]()
            L = X + ('10' + '01' * rnd(r, 1, 15) if lb1 else '') + ''.join('10' * u + '01' * v for u, v in sw)
            a, b = rnd(r, 1, 30), rnd(r, 0, 30)
            k, want, n = g_predict(L, a, b)
            done += 1
            if k is None or k[1] != kind:
                bad.append((kind, 'classified', k)); continue
            ok = same(run_from(Kword(L, [], a, b), n), parse_conf(want))
            res[kind] += ok
            if not ok:
                bad.append((kind, L[-40:], a, b))
    report('11', not bad, 'general rule G on random K-configs (random unread text left of the turn, optional Lb1 '
           'digit): %s of %d each; failures %d%s' % (', '.join('%s %d' % kv for kv in res.items()), N, len(bad),
                                                     '' if not bad else ' %s' % bad[:3]))

LEFT = {  # the left-moving part of the table (proof.md 3.6): (state, read) -> (write, next) ; 'R' = turns right
    ('E', 0): (1, 'D'), ('E', 1): (1, 'F'), ('D', 0): (1, 'A'), ('D', 1): (0, 'E'),
    ('A', 0): (1, 'R'), ('A', 1): (0, 'C'), ('C', 0): (1, 'D'), ('C', 1): (0, 'R'),
    ('F', 0): (1, 'D'), ('F', 1): 'H',
}
def check_sweep_classes(r):
    # (a) the left-moving automaton is the table
    okA = True
    for (q, x), want in LEFT.items():
        tr = TAB[ST.index(q)][x]
        if want == 'H':
            okA &= tr is None
        else:
            w, nx = want
            okA &= tr is not None and tr[0] == w and ((nx == 'R' and tr[1] == 1 and tr[2] == ST.index('B')) or
                                                      (nx != 'R' and tr[1] == -1 and ST[tr[2]] == nx))
    # (b) partition and behaviour: every X of length <= 14 that does not end in a digit 10 (01)^v (v >= 0)
    cls = collections.Counter(); badp = []; badb = []; beh = collections.Counter()
    D = '10' * 3 + '01' * 2                      # one swept digit (3,1,2); a = 2, b = 1
    def digit_end(X):
        v, i = _runback(X, len(X), '01')
        return _seg(X, i - 2, i) == '10'
    for n in range(0, 15):
        for x in range(2 ** n):
            X = format(x, 'b').zfill(n) if n else ''
            if digit_end(X):
                continue
            c = xclass(X)
            cls[c] += 1
            if c == '?':
                badp.append(X); continue
            if n <= 7 or x % 11 == 0:                    # behaviour: all X up to length 7, a sample above
                pre = ''.join(r.choice('01') for _ in range(6)) + '1'
                for L in (pre + X + D, pre + X):
                    if digit_end(L) and not L.endswith(D):
                        continue
                    j, sw, t = g_split(L)
                    xc = 'Lt' if t else xclass(L[:j])
                    k, want, steps = g_predict(L, 2, 1)
                    if xc in ('Lf', 'T2', 'T3S2', 'Jc', 'Lt'):
                        if k is None:
                            ok = xc in ('T2', 'Lt') and not sw          # O*-turn with no swept digit: excluded
                        else:
                            ok = k[1] == xc and same(run_from(Kword(L, [], 2, 1), steps), parse_conf(want))
                    elif xc in ('H1', 'H2'):
                        ok = k is None and run_from(Kword(L, [], 2, 1), 400 + 40 * len(L)) is None
                    else:
                        ok = k is None and xc in ('U1', 'U2', 'U3')
                    beh[xc] += 1
                    if not ok:
                        badb.append((L, xc, k))
    detail = ', '.join('%s %d' % kv for kv in sorted(cls.items()))
    report('12', okA and not badp and not badb,
           'sweep automaton = table [%s]; all %d left texts X of length <= 14 that do not end in a digit fall in '
           'exactly one class: %s; behaviour on %d K-configs (X up to length 7, a sample above): G exact on '
           'Lf/T2/T3S2/Jc/Lt, H1/H2 halt inside the macro step; failures %d%s'
           % (okA, sum(cls.values()), detail, sum(beh.values()), len(badp) + len(badb),
              '' if not (badp or badb) else ' %s' % (badp + badb)[:3]))

# ---------------------------------------------------------------- C helpers
KDUMP_C = r'''
#include <stdio.h>
#include <stdlib.h>
#define N (1<<26)
static unsigned char t[N];
int main(int argc,char**argv){
  const char*s=argv[1]; long long maxs=atoll(argv[2]);
  int w[6][2],mv[6][2],nx[6][2];
  for(int q=0;q<6;q++)for(int r=0;r<2;r++){const char*g=s+q*7+r*3;
    if(g[0]=='-'){w[q][r]=-1;continue;} w[q][r]=g[0]-'0'; mv[q][r]=g[1]=='R'?1:-1; nx[q][r]=g[2]-'A';}
  long long h=N/2, lo=h, hi=h; int q=0;
  static char buf[1<<22];
  for(long long st=0; st<maxs; st++){
    int r=t[h]; if(w[q][r]<0){printf("HALT %lld\n",st);return 0;}
    t[h]=w[q][r]; h+=mv[q][r]; q=nx[q][r];
    if(h<=0||h>=N-1){printf("OOB %lld\n",st);return 1;}
    if(h<lo)lo=h;
    if(h>hi){hi=h;
      if(q==1){
        long long p=h-1; long b=0,a=0;
        while(p-1>lo-2 && t[p]==0 && t[p-1]==1){b++;p-=2;}
        if(!(t[p]==0&&t[p-1]==0&&t[p-2]==0)) continue;
        p-=3;
        while(t[p]==0 && t[p-1]==1){a++;p-=2;}
        int n=0; char last=0; long cnt=0;
        long long left=lo; while(t[left]==0 && left<p) left++;
        while(p>=left){
          char c;
          if(p-1<left){ c='1'; p-=1; }
          else { int x=t[p-1],y=t[p]; c= x? (y?'X':'a') : (y?'o':'z'); p-=2; }
          if(c==last) cnt++; else { if(last) n+=sprintf(buf+n,"%c%ld ",last,cnt); last=c; cnt=1; }
          if(n>(1<<22)-100) break;
        }
        if(last) n+=sprintf(buf+n,"%c%ld",last,cnt);
        buf[n]=0;
        printf("%lld %ld %ld %s\n",st+1,a,b,buf);
      }
    }
  }
  printf("END %lld lo=%lld hi=%lld\n",maxs,lo-N/2,hi-N/2);
  return 0;
}
'''
HALTBOX_C = r'''
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#define T (1<<20)
static unsigned char t[T];
int main(int argc,char**argv){
  const char*s=argv[1]; long long NS=atoll(argv[2]);
  int w[6][2],mv[6][2],nx[6][2];
  for(int q=0;q<6;q++)for(int r=0;r<2;r++){const char*g=s+q*7+r*3;
    if(g[0]=='-'){w[q][r]=-1;continue;} w[q][r]=g[0]-'0'; mv[q][r]=g[1]=='R'?1:-1; nx[q][r]=g[2]-'A';}
  char txt[4096]; int a,b;
  while(scanf("%4000s %d %d",txt,&a,&b)==3){
    memset(t,0,T); long long h=T/2;
    for(char*c=txt;*c;c++) t[h++]=*c-'0';
    for(int i=0;i<a;i++){t[h++]=1;t[h++]=0;}
    h+=3; for(int i=0;i<b;i++){t[h++]=1;t[h++]=0;}
    int q=1; long long st; int res=0;
    for(st=0;st<NS;st++){ int r=t[h]; if(w[q][r]<0){res=1;break;} t[h]=w[q][r]; h+=mv[q][r]; q=nx[q][r];
      if(h<=0||h>=T-1){res=2;break;} }
    printf("%s %lld\n", res==1?"HALT":res==2?"OOB":"OK", st);
  }
  return 0;
}
'''
def build(tmp, name, src):
    p = os.path.join(tmp, name)
    with open(p + '.c', 'w') as f:
        f.write(src)
    subprocess.run(['gcc', '-O2', '-o', p, p + '.c'], check=True)
    return p

# ---------------------------------------------------------------- K-config parsing (kdump output)
TOK = {'a': '10', 'z': '00', 'o': '01', 'X': '11', '1': '1'}
def load_k(lines):
    out = []
    for line in lines:
        p = line.split()
        if not p or not p[0].isdigit():
            continue
        out.append((int(p[0]), int(p[1]), int(p[2]), [(x[0], int(x[1:])) for x in p[3:]]))
    return out

def text_of(runs):
    return ''.join(TOK[c] * n for (c, n) in reversed(runs))

def digits_of(runs):
    toks = [[c, n] for c, n in runs]
    D = []; i = 0
    while i < len(toks):
        v = 0; beta = 1; u = 0; j = i
        if toks[j][0] == 'o':
            v = toks[j][1]; j += 1
        if j < len(toks) and toks[j][0] == 'z' and toks[j][1] == 1:
            beta = 0; j += 1
        if j < len(toks) and toks[j][0] == 'a':
            u = toks[j][1]; j += 1
        if j == i or (v == 0 and beta == 1):
            break
        D.append((u, beta, v)); i = j
    return toks[i:], D[::-1]

def predict(cfg):
    """which of M / O / P applies (proof.md 3), and its predicted K-word and step count"""
    st, a, b, runs = cfg
    pre, D = digits_of(runs)
    pre_txt = ''.join(TOK[c] * n for (c, n) in reversed(pre))
    if not D:
        return None, 'no digits'
    m = len(D); k = 0
    while k < m and D[m - 1 - k][1] == 1:
        k += 1
    for i in range(m - 1, m - 1 - k, -1):
        u, _, v = D[i]
        if v < 1:
            return None, 'swept digit with v = 0'
        if u == 1:
            L = pre_txt + dig(D[:i])
            if i == 0 and pre_txt == '':
                if v == 1:
                    break
                return None, 'far-left wall 10 (01)^v, v >= 2'
            if not L.endswith('1'):
                return None, 'u = 1 digit with left neighbour 0'
            return P_rule(L, D[i:], a, b), 'P'
        if u == 0:
            return None, 'swept bit-1 digit with u = 0'
    if k < m:
        js = m - 1 - k
        if D[js][2] < 1:
            return None, 'carry reaches bit-0 digit with v = 0'
        if a < 1:
            return None, 'a = 0'
        return M_rule(pre_txt + dig(D[:js]), D[js:], a, b), 'M'
    if pre_txt == '' and D[0] == (1, 1, 1):
        if m == 1:
            return None, 'O with no digits'
        return O_rule(D[1:], a, b), 'O'
    return None, 'sweep enters the prefix'

def kword_of(cfg):
    st, a, b, runs = cfg
    return text_of(runs) + '10' * a + '000' + '10' * b + ' B> 0^inf'

def fast_run(text_with_head, n):
    """run n steps from 'text B> 0^inf' on a bytearray; return render() triple"""
    txt = text_with_head.replace(' B> 0^inf', '').lstrip('0')
    pad = len(txt) + 64 + n // 4
    t = bytearray(pad) + bytearray(int(c) for c in txt) + bytearray(pad)
    h = pad + len(txt); s = 1
    for _ in range(n):
        tr = TAB[s][t[h]]
        if tr is None:
            return None
        t[h] = tr[0]; h += tr[1]; s = tr[2]
    lo = t.find(1); hi = t.rfind(1)
    lo = min(lo, h); hi = max(hi, h)
    return ''.join('01'[x] for x in t[lo:hi + 1]), h - lo, s

# ---------------------------------------------------------------- 7. initial segment
INIT = [  # step, a, b, digits after the leading 10 01 (None = not in that shape), text
    (142, 2, 1, '1001' + dig([(3, 1, 1)])),
    (283, 4, 1, '1001' + dig([(0, 0, 3), (1, 1, 2)])),
    (428, 4, 1, '1001000' + dig([(2, 1, 1), (2, 1, 4)])),
    (609, 4, 1, '1001' + dig([(1, 1, 2), (0, 0, 2), (4, 1, 4)])),
]
def check_init(kd):
    cf = {c[0]: c for c in kd}
    ok = 0
    for (st, a, b, txt) in INIT:
        c = cf.get(st)
        ok += c is not None and c[1] == a and c[2] == b and text_of(c[3]).lstrip('0') == txt
    seq = [c[0] for c in kd[:4]]
    # transitions
    w1, why1 = predict(cf[142]); w2, why2 = predict(cf[283]); w3, why3 = predict(cf[428])
    t1 = why1 == 'O' and w1[1] == 283 - 142 and same(fast_run(kword_of(cf[142]), w1[1]), parse_conf(kword_of(cf[283])))
    t2 = why2 == 'P' and w2[1] == 428 - 283 and same(parse_conf(w2[0]), parse_conf(kword_of(cf[428])))
    g3 = g_predict(text_of(cf[428][3]).lstrip('0'), cf[428][1], cf[428][2])
    t3 = why3 not in ('M', 'O', 'P') and g3[0] is not None and g3[0][:2] == ('O*', 'T2') and g3[2] == 609 - 428 \
        and same(parse_conf(g3[1]), parse_conf(kword_of(cf[609])))
    # and the blank-tape run itself reaches the step-142 config (Python, independent of kdump)
    t = [0] * 400; h = 200; s = 0
    for _ in range(142):
        tr = TAB[s][t[h]]; t[h] = tr[0]; h += tr[1]; s = tr[2]
    t0 = same(render(t, h, s), parse_conf(kword_of(cf[142])))
    report('7', ok == 4 and seq == [142, 283, 428, 609] and t0 and t1 and t2 and t3,
           'init: blank -142-> K((3,1,1);2,1) [python sim: %s]; -O-> K((0,0,3),(1,1,2);4,1) @283 [%s]; -P-> '
           '1001000 (2,1,1)(2,1,4) a=4 b=1 @428 [%s]; 428->609 is %s for M/O/P, and O* with turn T2 (181 steps) '
           'under G'
           % (t0, t1, t2, why3))

# ---------------------------------------------------------------- 8/9. census and coverage
# the greedy cover uses the 23 windows of the earlier stage: T3j (= T3 then one C0 step) is left out, because
# longest-first greedy would also take it where T3 is followed by S4c, and no window starts with the D1 step
# that then follows
ATOM = sorted(((len(parse_window(l)[0]), n_, parse_window(l), s_) for n_, (l, _, s_) in LEM.items() if n_ != 'T3j'),
              key=lambda x: -x[0])
def cover(text_with_head, nsteps):
    """greedy decomposition into atomic windows; returns (#lemma applications, #uncovered steps, end render)"""
    txt = text_with_head.replace(' B> 0^inf', '').lstrip('0')
    pad = len(txt) + 4096
    t = bytearray(pad) + bytearray(int(c) for c in txt) + bytearray(pad)
    h = pad + len(txt); s = 1; done = 0; apps = 0; unk = 0
    pats = [(L, name, [int(x) for x in c], off, ST.index(st), n) for (L, name, (c, off, st), n) in ATOM]
    while done < nsteps:
        hit = None
        for (L, name, cells, off, st, n) in pats:
            if st != s or done + n > nsteps:
                continue
            b0 = h - off
            if b0 < 0 or b0 + L > len(t):
                continue
            okp = True
            for i in range(L):
                if t[b0 + i] != cells[i]:
                    okp = False; break
            if okp:
                hit = n; break
        n = hit if hit else 1
        if not hit:
            unk += 1
        for _ in range(n):
            tr = TAB[s][t[h]]
            if tr is None:
                return apps, unk + 1, None
            t[h] = tr[0]; h += tr[1]; s = tr[2]
        done += n; apps += 1
    lo = min(t.find(1), h); hi = max(t.rfind(1), h)
    return apps, unk, (''.join('01'[x] for x in t[lo:hi + 1]), h - lo, s)

def check_census_cover(kd, T1, T2, expect):
    cnt = collections.Counter(); bad = 0
    for c1, c2 in zip(kd, kd[1:]):
        pr, why = predict(c1)
        if pr is None:
            cnt['other: ' + why] += 1; continue
        if pr[1] == c2[0] - c1[0] and same(parse_conf(pr[0]), parse_conf(kword_of(c2))):
            cnt[why] += 1
        else:
            bad += 1
    other = sum(v for k, v in cnt.items() if k.startswith('other'))
    got = (cnt['M'], cnt['P'], cnt['O'], other, bad)
    detail = ', '.join('%s %d' % (k, v) for k, v in sorted(cnt.items(), key=lambda x: -x[1]))
    # the general rule G: every transition, by turn
    gcnt = collections.Counter(); gbad = 0; gnone = collections.Counter()
    for c1, c2 in zip(kd, kd[1:]):
        L = text_of(c1[3]).lstrip('0')
        k, want, n = g_predict(L, c1[1], c1[2])
        if k is None:
            gnone[want] += 1; continue
        if n == c2[0] - c1[0] and want.replace(' B> 0^inf', '') == text_of(c2[3]).lstrip('0') + '10' * c2[1] + '000' + '10' * c2[2]:
            gcnt[k[1]] += 1
        else:
            gbad += 1
    gdet = ', '.join('%s %d' % (t, gcnt[t]) for t in ('Lf', 'T3S2', 'Jc', 'T2', 'Lt'))
    gok = gbad == 0 and not gnone and sum(gcnt.values()) == len(kd) - 1
    if expect:
        gok = gok and tuple(gcnt[t] for t in ('Lf', 'T3S2', 'Jc', 'T2', 'Lt')) == (22353, 8, 2, 37, 35)
    gtxt = ('; general rule G: %d of %d transitions predicted exactly (%s), unpredicted %d, mismatches %d'
            % (sum(gcnt.values()), len(kd) - 1, gdet, sum(gnone.values()), gbad))
    if expect:
        report('8', got == expect and gok, 'census of K->K transitions to %.0e: %s; mismatches %d (expected M/P/O/other '
               '= %s)%s' % (T2, detail, bad, '/'.join(map(str, expect[:4])), gtxt))
    else:
        report('8', bad == 0 and gok, 'census to %.0e: %s; mismatches %d%s' % (T2, detail, bad, gtxt))
    # coverage
    nall = nother = unk_tot = endbad = 0
    for c1, c2 in zip(kd, kd[1:]):
        pr, why = predict(c1)
        if c1[0] < T1 or why != 'M':
            apps, unk, end = cover(kword_of(c1), c2[0] - c1[0])
            unk_tot += unk
            endbad += not same(end, parse_conf(kword_of(c2)))
            if c1[0] < T1:
                nall += 1
            else:
                nother += 1
    report('9', unk_tot == 0 and endbad == 0,
           'coverage by 23 of the atomic windows (T3j left out): all %d transitions before step %.0e and the %d '
           'non-M transitions after it (to %.0e); uncovered steps %d; end-config mismatches %d.  This shows only '
           'that the run uses no other local patterns; it is not evidence for non-halting' % (nall, T1, nother, T2, unk_tot, endbad))

# ---------------------------------------------------------------- 10. arithmetic is needed
def check_halting_examples(hb):
    w = Kword('1001', [(1, 0, 2)], 2, 1)
    txt, h, s = parse_conf(w)
    t = [0] * 6000 + [int(c) for c in txt] + [0] * 6000; h += 6000; n = 0
    while n < 10 ** 5:
        tr = TAB[s][t[h]]
        if tr is None:
            break
        t[h] = tr[0]; h += tr[1]; s = tr[2]; n += 1
    ex = TAB[s][t[h]] is None and n == 2535
    # G along the same run: K-configs = B on a new right record, reading 0, with (10)^a 000 (10)^b behind it
    t = [0] * 6000 + [int(c) for c in txt] + [0] * 6000; h = parse_conf(w)[1] + 6000; s = 1; n = 0; hi = h
    ks = []
    while TAB[s][t[h]] is not None:
        if s == 1 and h >= hi and t[h] == 0:
            p = h - 1; bb = 0
            while t[p] == 0 and t[p - 1] == 1:
                bb += 1; p -= 2
            if t[p] == t[p - 1] == t[p - 2] == 0:
                p -= 3; aa = 0
                while t[p] == 0 and t[p - 1] == 1:
                    aa += 1; p -= 2
                lo = t.index(1)
                ks.append((n, ''.join(map(str, t[lo:p + 1])), aa, bb))
        tr = TAB[s][t[h]]; t[h] = tr[0]; h += tr[1]; s = tr[2]; n += 1; hi = max(hi, h)
    gsteps = 0
    for (n1, L1, a1, b1), (n2, L2, a2, b2) in zip(ks, ks[1:]):
        k, want, m = g_predict(L1, a1, b1)
        gsteps += k is not None and m == n2 - n1 and want.replace(' B> 0^inf', '') == L2 + '10' * a2 + '000' + '10' * b2
    last = g_predict(ks[-1][1], ks[-1][2], ks[-1][3])
    gex = gsteps == len(ks) - 1 and last[0] is None and last[1] == 'H1' and ks[-1][0] == 2384
    lines = []
    import itertools
    for m in (1, 2):
        for D in itertools.product([(u, be, v) for u in range(1, 4) for be in (0, 1) for v in range(1, 4)], repeat=m):
            for a in range(4):
                for b in range(4):
                    lines.append('1001' + dig(D) + ' %d %d' % (a, b))
    out = subprocess.run([hb, TM, '2000000'], input='\n'.join(lines) + '\n', capture_output=True, text=True).stdout.split('\n')
    halts = sum(1 for l in out if l.startswith('HALT'))
    report('10', ex and gex and len(lines) == 5472 and halts == 807,
           'K((1,0,2);2,1) halts at step 2535 [%s]; G predicts %d of its %d macro steps exactly and puts its last '
           'K-config (step %d) in class %s [%s]; box m<=2, u,v in 1..3, beta in {0,1}, a,b in 0..3: %d of %d halt '
           'within 2e6 steps' % (ex, gsteps, len(ks) - 1, ks[-1][0], last[1], gex, halts, len(lines)))

# ---------------------------------------------------------------- main
if __name__ == '__main__':
    ap = argparse.ArgumentParser()
    ap.add_argument('--seed', type=int, default=11)
    ap.add_argument('--n', type=int, default=400)
    ap.add_argument('--cover-all', type=float, default=1e7)
    ap.add_argument('--cover-other', type=float, default=1e9)
    ap.add_argument('--quick', action='store_true', help='T2 = 1e8 (census expectations then not asserted)')
    A = ap.parse_args()
    if A.quick:
        A.cover_other = 1e8
    r = random.Random(A.seed)
    check_table()
    check_tokens()
    check_windows()
    check_Lt()
    check_rules(r, A.n)
    check_P_chain(r, 150)
    check_general(r, A.n)
    check_sweep_classes(r)
    with tempfile.TemporaryDirectory() as tmp:
        kd_bin = build(tmp, 'kdump', KDUMP_C)
        hb_bin = build(tmp, 'haltbox', HALTBOX_C)
        out = subprocess.run(['bash', '-c', 'ulimit -v 6000000; exec "$0" "$@"', kd_bin, TM, str(int(A.cover_other))],
                             capture_output=True, text=True).stdout.split('\n')
        kd = load_k(out)
        endline = [l for l in out if l.startswith('END') or l.startswith('HALT')]
        print('     K-dumper to %.0e: %d K-configs; %s' % (A.cover_other, len(kd), endline[-1] if endline else '?'))
        check_init(kd)
        expect = (22349, 35, 6, 45, 0) if int(A.cover_other) == 10 ** 9 else None
        check_census_cover(kd, A.cover_all, A.cover_other, expect)
        check_halting_examples(hb_bin)
    nok = sum(ok for _, ok in RESULTS)
    print('SUMMARY %s  %d/%d checks pass' % ('PASS' if nok == len(RESULTS) else 'FAIL', nok, len(RESULTS)))
    sys.exit(0 if nok == len(RESULTS) else 1)