#!/usr/bin/env python3
"""check_proof.py, pool #7 = 1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA: the delta proof against kill #30
(1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC). Checks every claim of proof.md's delta section by direct simulation
and with #30's own check functions, which are imported from #30's check_proof.py (not copied).
   python3 -B check_proof.py [--quick] [--seed S]      (writes data/check_proof_seed<S>.json unless --quick)
Claim ids (proof.md, section "Delta proof"):
  X0  the string is the holdout-list entry (740 list)
  X1  the renaming + mirror: the unique (permutation, orientation) mapping #7's table onto #30's; #7's A is #30's E
  X2  lockstep: #7 from the blank tape = the mirror image of #30's table run from the blank tape in state E, renamed
  X3  initial segment, #7's own table: every L-form configuration up to step 1059 (e1..e5), the exact tapes at
      steps 1059 (mirror of L(16, 0001)) and 1114 (mirror of K(1, 17, t1)), no halt
  X4  #30's orbit invariant (I1)-(I4) at e5, clause by clause; e1..e4 cannot serve as the base
  X5  rules-only orbit from e5 = the TM's left records (fresh Python run in #30's frame; stored C log if present)
  X6  no merge: #7's orbit shares no epoch with #30's or W4-1's below N = 20,000 (so #7 needs its own finite part)
  D  #30's section D (Lemma D links, FIN, H3), its source run unchanged except for the start (e5 instead of #30's
      epoch 3)
  V   the .v route: rules-only orbit from K(1,17,t1) to the first epoch with N >= 17,705 (687 epochs e5..e691,
      landing at e692), #30's Inv there, and Inv carried along the orbit to the end of section D
  RQ  the Rocq draft of the plan (rocq/M7_draft.v) and its stored check_kill log (if present)
  #30's table-level sections (A, RP, LP, B, E, R, D6, H, D.3, threshold, ADV) run unchanged: they depend only on the
  transition table, which #7 shares with #30 up to X1."""
import sys, os, json, time, itertools, inspect, importlib.util
HERE = os.path.dirname(os.path.abspath(__file__))
P30 = os.path.join(os.path.dirname(HERE), '1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC')
_spec = importlib.util.spec_from_file_location('cp30', os.path.join(P30, 'check_proof.py'))
cp30 = importlib.util.module_from_spec(_spec); _spec.loader.exec_module(cp30)   # seeds random with --seed, reads --quick
common, M, rec, RES = cp30.common, cp30.M, cp30.rec, cp30.RES
from fs_val_rules import inG          # #30's scripts dir is on sys.path now (cp30 put it there)

QUICK, SEED = cp30.QUICK, cp30.SEED
T0 = time.time()
TM7 = '1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA'
TM30 = common.TMS
TMW41 = '1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB'      # Wave 4 pick W4-1: the table's third start
ST = 'ABCDEF'
norm = cp30.norm

def derive(fn, subs, name):
    """fn's source with each (old, new) substitution applied exactly once, compiled in fn's own module globals.
    Used to run #30's code unchanged except for its hard-coded start."""
    src = inspect.getsource(fn)
    for old, new in subs:
        assert src.count(old) == 1, (fn.__name__, old)
        src = src.replace(old, new)
    g = fn.__globals__
    exec(compile(src, f'<{name} derived from {fn.__module__}.{fn.__name__}>', 'exec'), g)
    return g[name]

# common.events with the start state as a parameter (it is hard-coded to A there)
events_from = derive(common.events, [('def events(end, size=1 << 16):', 'def events_from(q0, end, size=1 << 16):'),
                                     ('pos = off; q = 0;', 'pos = off; q = q0;')], 'events_from')
# #30's section D with the start (epoch 3 = L(7, 000010001)) as a parameter
section_D_from = derive(cp30.section_D, [('def section_D(maxN, Nstar):', 'def section_D_from(maxN, Nstar, k0, T0, ep0):'),
                                         ("k, T = 7, '000010001'", 'k, T = k0, T0'),
                                         ('ep = 2;', 'ep = ep0 - 1;'),
                                         ("'epochs_3..below_N*': ep - 3", "'epochs_base..below_N*': ep - ep0")],
                        'section_D_from')

# ---------------------------------------------------------------------------------------------------------------
def section_X0():
    hd = os.path.join(HERE, '..', '..', 'data', 'holdouts')
    lines = [l.rstrip('\n') for l in open(os.path.join(hd, 'BB6_holdouts_740.txt'))]
    rec('X0   TM string is byte-exact in the 740-machine holdout list (line 381)', lines.count(TM7) == 1 and lines[380] == TM7,
        [i + 1 for i, l in enumerate(lines) if l == TM7])
    lists = sorted(f for f in os.listdir(hd) if f.endswith('.txt'))
    counts = {f: [l.rstrip('\n') for l in open(os.path.join(hd, f))].count(TM7) for f in lists}
    rec('X0   TM string is byte-exact (once) in every stored holdout list', all(c == 1 for c in counts.values()) and len(counts) > 20, counts)

def conjugacies(src, dst):
    """every (perm, mirror) with  dst[perm q][s] = (w, +-d, perm q')  whenever  src[q][s] = (w, d, q'),
    and the same undefined transitions"""
    ts, td = common.table(src), common.table(dst)
    out = []
    for perm in itertools.permutations(range(6)):
        for mirror in (False, True):
            ok = True
            for q in range(6):
                for s in (0, 1):
                    a, b = ts[q][s], td[perm[q]][s]
                    if a is None or b is None: ok &= a is None and b is None
                    else: ok &= b == (a[0], -a[1] if mirror else a[1], perm[a[2]])
            if ok: out.append((perm, mirror))
    return out

PERM = (4, 0, 1, 5, 2, 3)          # #7 state -> #30 state: A->E, B->A, C->B, D->F, E->C, F->D (mirror)
INV = tuple(PERM.index(i) for i in range(6))

def section_X1():
    c = conjugacies(TM7, TM30)
    rec('X1   #7 = #30 mirrored, states A,B,C,D,E,F -> E,A,B,F,C,D; unique among 720 x 2', c == [(PERM, True)], c)
    rec("X1   #7's start A is #30's state E (the halting transition #7 F0 is #30's D0)",
        PERM[0] == 4 and common.table(TM7)[5][0] is None and common.table(TM30)[3][0] is None, None)
    c4 = conjugacies(TMW41, TM30)
    rec("X1   W4-1 = #30 renamed (no mirror), its start A is #30's state B: the third start of the same table",
        len(c4) == 1 and c4[0][1] is False and c4[0][0][0] == 1, c4)
    RES['_X1'] = {'perm #7->#30': ''.join(ST[PERM[q]] for q in range(6)), 'mirror': True,
                  'perm #30->#7': ''.join(ST[INV[q]] for q in range(6)), 'W4-1 perm W4-1->#30': ''.join(ST[i] for i in c4[0][0])}

def section_X2(nsteps):
    """step-by-step: #7 at cell x in state q  <->  #30's table at cell -x in state PERM[q], same tape mirrored"""
    t7, t30 = common.table(TM7), common.table(TM30)
    size = 1 << 16; off = size // 2
    a7 = bytearray(size); a30 = bytearray(size); p7 = p30 = off; q7, q30 = 0, 4
    ok = True; checks = 0; marks = {15, 81, 183, 573, 1059, 1114, 2915}
    for st in range(1, nsteps + 1):
        r7, r30 = t7[q7][a7[p7]], t30[q30][a30[p30]]
        if r7 is None or r30 is None: ok = False; break
        a7[p7] = r7[0]; p7 += r7[1]; q7 = r7[2]
        a30[p30] = r30[0]; p30 += r30[1]; q30 = r30[2]
        if q30 != PERM[q7] or p7 - off != off - p30: ok = False; break
        if st in marks or st % 100000 == 0:
            checks += 1
            if a7[1:] != a30[:0:-1] or a7[0] or a30[0]:      # a7[off + x] == a30[off - x] for every cell x
                ok = False; break
    rec('X2   lockstep: #7 from blank in A = mirror of #30 table from blank in E, renamed (every step; full tapes at checkpoints)',
        ok and checks > 0, (st, q7, q30, p7 - off, off - p30))
    RES['_X2'] = {'steps': nsteps, 'full_tape_checks': checks}

def lform_7(tape, pos, q, hi):
    """#7's frame: is this the mirror image of an L-form configuration 0^inf <A 101 (001)^k T 0^inf of #30's frame?
    (#30's A is #7's B; the head reads a blank, every cell right of it is blank, the cells left of it read 1,0,1 going
    left.) Returns (k, T) or None."""
    if q != INV[0] or tape[pos] != 0 or (tape[pos - 1], tape[pos - 2], tape[pos - 3]) != (1, 0, 1): return None
    if any(tape[pos + 1:hi + 2]): return None
    lo = 0
    while tape[lo] == 0: lo += 1
    s = ''.join(map(str, tape[pos - 1:lo - 1 if lo else None:-1]))          # read leftwards = #30's left-to-right
    j = 3; k = 0
    while s[j:j + 3] == '001': j += 3; k += 1
    return k, s[j:]

E_RECORDS = [(15, 0, '0001'), (81, 1, '000010010001'), (183, 3, '0001000010001'),
             (573, 5, '000010010010001000110010001'), (1059, 16, '0001')]

def section_X3():
    t7 = common.table(TM7)
    size = 1 << 14; off = size // 2
    tape = bytearray(size); pos = off; q = 0; hi = pos; got = []; halted = False; snap = {}
    for st in range(1, 1115):
        r = t7[q][tape[pos]]
        if r is None: halted = True; break
        tape[pos] = r[0]; pos += r[1]; q = r[2]; hi = max(hi, pos)
        L = lform_7(tape, pos, q, hi)
        if L: got.append((st, L[0], L[1]))
        if st in (1059, 1114): snap[st] = (bytes(tape), pos, q)
    rec('X3   #7 own table: the L-form configurations up to step 1059 are exactly e1..e5 (steps 15, 81, 183, 573, 1059)',
        not halted and got == E_RECORDS, got)
    # step 1059: 0^inf 1000 (100)^16 101 B> 0^inf  =  mirror of  L(16, 0001) = 0^inf <A 101 (001)^16 0001 0^inf
    tp, p, q = snap[1059]
    w = '1000' + '100' * 16 + '101'
    ok = q == INV[0] and tp[p] == 0 and ''.join(map(str, tp[p - len(w):p])) == w and not any(tp[:p - len(w)]) and not any(tp[p:])
    rec("X3   step 1059: #7's tape is exactly 0^inf 1000 (100)^16 101 B> 0^inf, the mirror of L(16, 0001)", ok, (p - off, ST[q]))
    # step 1114: 0^inf 1 <E (110)^17 0 011 0^inf  =  mirror of  K(1, 17, t1) = 0^inf 110 0 (011)^17 C> 1 0^inf
    tp, p, q = snap[1114]
    w = '1' + '110' * 17 + '0' + '011'
    ok = q == INV[2] and ''.join(map(str, tp[p:p + len(w)])) == w and not any(tp[:p]) and not any(tp[p + len(w):])
    rec("X3   step 1114: #7's tape is exactly 0^inf 1 <E (110)^17 0 011 0^inf, the mirror of K(1, 17, t1)", ok, (p - off, ST[q]))
    # the same records in #30's frame (start E), and the restart R: L(16, 000 1) -> K(1, 17, 1) in 3*16 + 7 = 55 steps
    ev = []
    for e in events_from(4, 1115):
        if e[0] in ('L', 'HALT'): ev.append(e)
        if e[0] == 'K' and e[1] == 1114: ev.append(e)
    rec("X3   #30's frame from state E: the same left records, then K(1, 17, '1') at step 1114 = 1059 + 3*16 + 7",
        ev == [('L',) + r for r in E_RECORDS] + [('K', 1114, 1, 17, '1')], ev)

# ---------------------------------------------------------------------------------------------------------------
def section_X4():
    """#30's invariant (proof.md D.6) at e5, clause by clause, and why no earlier record can be the base"""
    k, T = 16, '0001'
    a, N, Y = M.restart(k, T)
    rec('X4   e5 = L(16, 000 Y) with Y = 1, restart R gives K(1, N, Y) with N = k + 1 = 17', (a, N, Y) == (1, 17, '1'), (a, N, Y))
    rec('X4   Y = 1 is in H (section 4), so Lemma H / the corollary of section 4 apply', cp30.inH(Y), Y)
    kind = cp30.classify(Y)
    rec('X4   (I1) Y is special: Y = t1 is in G', kind == 'G', kind)
    rec('X4   (I2) vacuous (Y is not ordinary, no W)', not Y.startswith('11'), Y)
    r = cp30.run_epoch(N, Y)
    G0, Dl0 = cp30.Gfix(0)
    # D.6's k_t is k(W_t), the number of blocks of W_t (0 for a special residue), not the record index k of L(k, T):
    # kappa_5 = k(W_5) = 0. Read with the record index 16, (I4) would fail at the base (N_lo(16) = 2^19 - 2^14 > 17).
    kW = 0 if kind else len(cp30.parse_residue(Y)[3])
    rec('X4   kappa_5 = k(W_5) = 0 (special residue, no W), not the record index k = 16 of L(16, 0001)',
        kind != '' and kW == 0 and k == 16 and cp30.N_lo(16) == 2 ** 19 - 2 ** 14 > N, (kind, kW, cp30.N_lo(16)))
    rec('X4   (I3) k(W) = 0, c = 0 (special), kappa = 0: c <= Gamma(0, 0) = 0 and k(W) + c = 0 <= G(0) = 0',
        r['c'] == 0 and cp30.gamma_k(kW, 0, Dl0) == 0 and kW + r['c'] <= G0 == 0, (kW, r['c'], cp30.gamma_k(kW, 0, Dl0), G0))
    rec('X4   (I4) N = 17 >= N_lo(kappa_5) = N_lo(0) = 2^3 - 2^(floor((G(0)+1)/2)+4) = -8', N >= cp30.N_lo(kW) == -8, cp30.N_lo(kW))
    rec('X4   epoch e5 finishes: beta = 0 <= N - 2 (Y in G), next record = model', r['beta'] == 0 and (r['k2'], r['T2']) == (23, '0001000010001'),
        (r['beta'], r['k2'], r['T2']))
    RES['_X4'] = {'N': N, 'Y': Y, 'record index k': k, 'k(W_5)': kW, 'kappa_5': kW, 'c': r['c'], 'G(0)': G0,
                  'Gamma(0,0)': cp30.gamma_k(0, 0, Dl0), 'N_lo(0)': cp30.N_lo(0), 'N_lo(16), not used': cp30.N_lo(16),
                  'next': (r['k2'], r['T2'])}
    # e1..e4: e1 has N = 1 (beta <= N - 2 is false although its eat is at a G word); e2 and e3 have special residues
    # whose digestion does not fit (beta = 2 > 0, beta = 11 > 2: the model meets an eat outside G); e4's residue is
    # not in H. So the induction cannot start before e5.
    def unsafe(N, Y):
        try: cp30.run_epoch(N, Y); return False
        except (M.Unsafe, M.Unknown): return True
    nb = [(1, '1', cp30.classify('1') == 'G' and 0 > 1 - 2),
          (2, '010010001', cp30.classify('010010001') == 'E*' and unsafe(2, '010010001')),
          (4, '1000010001', cp30.classify('1000010001') == 'E*' and unsafe(4, '1000010001')),
          (6, '010010010001000110010001', not cp30.inH('010010010001000110010001') and cp30.classify('010010010001000110010001') == '?')]
    for N_, Y_, ok in nb:
        rec('X4n  e1..e4 are not a valid base (e1: N = 1; e2, e3: digestion does not fit, eat outside G; e4: Y not in H)', ok, (N_, Y_))
    rec('X4n  the restarts of e1..e4 match the records (N = k + 1)', [M.restart(k_, T_)[1:] for _, k_, T_ in E_RECORDS[:4]] ==
        [(N_, Y_) for N_, Y_, _ in nb], None)
    # e4's epoch itself is computed by the rules (LP0/LP11/LPC on its prefix, then eats at G words) and ends at e5;
    # it is still outside the family because (I1) fails there (Y4 is neither ordinary nor special)
    try: e4 = M.epoch(1, 6, '010010010001000110010001')
    except (M.Unsafe, M.Unknown) as ex: e4 = str(ex)
    rec("X4n  e4's epoch is rule-covered (eats at G words) and ends at e5 = L(16, 0001), but (I1) fails at e4", e4 == (16, '0001'), e4)

def section_X5():
    end = 3 * 10**6 if QUICK else 2 * 10**7
    tmL = [(e[2], e[3]) for e in events_from(4, end) if e[0] == 'L']
    M.FAST = True
    k, T = tmL[4]; ok = (k, T) == (16, '0001')
    for i in range(5, len(tmL)):
        a, b, w = M.restart(k, T); k, T = M.epoch(a, b, w)
        ok &= (k, T) == tmL[i]
    rec('X5   rules-only orbit from e5 = TM left records (fresh Python run, #30 frame from E)', ok and len(tmL) > 10, len(tmL))
    RES['_X5_python'] = {'steps': end, 'records': len(tmL), 'from_e5': len(tmL) - 4}
    path = os.path.join(HERE, 'data', 'orbit_E_1e11_LE.txt')
    if os.path.exists(path):
        lines = open(path).read().split('\n')
        tm = [l.split() for l in lines if l.startswith('L ')]
        tmL = [(int(f[2]), f[3] if len(f) > 3 else '') for f in tm]
        halted = any(l.startswith(('HALT', 'EDGE')) for l in lines)
        end_line = [l for l in lines if l.startswith('END')]
        k, T = tmL[4]; good = 0
        for i in range(5, len(tmL)):
            a, b, w = M.restart(k, T); k, T = M.epoch(a, b, w)
            good += (k, T) == tmL[i]
        rec('X5   rules-only orbit from e5 = stored C log (scripts/delta30/orbit_E.c, 1e11 steps), no halt',
            good == len(tmL) - 5 and not halted and bool(end_line), (good, len(tmL) - 5, end_line[:1]))
        RES['_X5_C'] = {'records': len(tmL), 'from_e5_checked': len(tmL) - 5, 'last_N': tmL[-1][0] + 1, 'end': end_line[:1]}

def section_X6(Nmax=20000):
    """#7's orbit from e5 shares no epoch (N, Y) with #30's orbit from its epoch 3 or with W4-1's orbit from its first
    special-residue record (#30's table from state B: L(2, 0001) at step 42), up to N >= Nmax: #30's finite part
    cannot be reused, #7 needs its own"""
    ev = [e for e in events_from(1, 400) if e[0] in ('L', 'HALT')]
    rec("X6   W4-1 (#30's table from state B): left records L(0,'')@4, L(2,0001)@42, L(7,0001)@194", ev[:3] ==
        [('L', 4, 0, ''), ('L', 42, 2, '0001'), ('L', 194, 7, '0001')], ev)
    M.FAST = True
    def orb(k, T):
        out = []
        while True:
            a, b, w = M.restart(k, T); out.append((b, w))
            if b >= Nmax: return out
            k, T = M.epoch(a, b, w)
    o7, o30, o41 = orb(16, '0001'), orb(7, '000010001'), orb(2, '0001')
    rec('X6   no merge: #7 (from e5), #30 (from epoch 3) and W4-1 (from L(2,0001)) share no epoch (N, Y) up to N >= %d' % Nmax,
        not (set(o7) & set(o30)) and not (set(o7) & set(o41)) and not (set(o30) & set(o41)), (len(o7), len(o30), len(o41)))
    RES['_X6'] = {'epochs to N >= %d' % Nmax: {'#7': len(o7), '#30': len(o30), 'W4-1': len(o41)},
                  'first N': {'#7': [x[0] for x in o7[:8]], '#30': [x[0] for x in o30[:8]], 'W4-1': [x[0] for x in o41[:8]]}}

# ---------------------------------------------------------------------------------------------------------------
# the .v route (#30's .v, Sections 10-11): the bound functions, transcribed from the .v
def w_(q): return 2 ** ((q + 1) // 2)
def v2(q): return 2 ** (q // 2)
def Ws(P): return sum(w_(q) for q in range(P))
def V2s(P): return sum(v2(q) for q in range(P))
def Pf(k): return max(12, k + 3)
def Af(k): return 5 * Ws(Pf(k)) + 6 * w_(Pf(k)) + 2 * Ws(k)
def Bf(k): return Af(k) + 5 * V2s(Pf(k)) + 6 * v2(Pf(k)) + 2 ** (k + 1)
def Xf(k): return Af(k) + 5 * Pf(k) + 7
def Costf(k): return 2 * Xf(k) + 2 + 2 * Af(k) + 11 * Ws(Pf(k)) + 13 * w_(Pf(k))
def Nlo(k): return max(0, 2 ** (k + 3) - 8 * 2 ** ((Pf(k) + 3) // 2))      # nat subtraction
NSTAR_V = 17705
SPECIAL_V = {'1', '010010001', '1000010001'}           # t1, p01 1 t1, p10 (p00 t2)
def Mw(es): return sum(w_(q) * e for q, e in enumerate(es))
def M2(es): return sum(2 ** (q + 1) * e for q, e in enumerate(es))

def inv_v(k, N, Y):
    """#30's Inv k N y, clause by clause: returns (ok, dict of clauses)"""
    Y = norm(Y); cl = {'N >= Nstar = 17705': N >= NSTAR_V, 'N >= Nlo(k) = %d' % Nlo(k): N >= Nlo(k)}
    if Y in SPECIAL_V:
        cl['Y special'] = True
    else:
        x, W, ds, es, t = cp30.parse_residue(Y)
        cl['Y = 11 a^x z W with W in G'] = Y.startswith('11') and t >= 0 and inG(W)
        cl['k(W) = %d <= k' % len(es)] = len(es) <= k
        cl['Mw(W) = %d <= Af(k) = %d' % (Mw(es), Af(k))] = Mw(es) <= Af(k)
        cl['M2(W) = %d <= Bf(k) = %d' % (M2(es), Bf(k))] = M2(es) <= Bf(k)
        cl['x = %d <= Xf(k) = %d' % (x, Xf(k))] = x <= Xf(k)
    return all(cl.values()), cl

def orbit_v(N, Y, n):
    """the .v's  orbit f n N y : n epochs of the rules-only model from K(1, N, Y)"""
    M.FAST = True
    for _ in range(n):
        k, T = M.epoch(1, N, Y); _, N, Y = M.restart(k, T)
    return N, Y

def section_V(maxN):
    # transcription self-test against #30's write-up (section 8.3 table) and #30's fin694 / inv694
    tab = {8: (12, 1419, 8725, 1024), 9: (12, 1451, 8853, 3072), 10: (13, 2219, 13471, 6144), 11: (14, 2923, 17705, 14336),
           12: (15, 4459, 26931, 28672), 13: (16, 5867, 35389, 61440)}
    rec("V0   bound functions reproduce #30's table (P, A, Cost + 2, N_lo') for kappa = 8..13",
        all((Pf(k), Af(k), Costf(k) + 2, Nlo(k)) == v for k, v in tab.items()), {k: (Pf(k), Af(k), Costf(k) + 2, Nlo(k)) for k in tab})
    rec('V0   #30 N2: Cost(k) + 2 <= 17,705 for k <= 11 and <= Nlo(k) for 12 <= k < 200', all(Costf(k) + 2 <= NSTAR_V for k in range(12)) and
        all(Costf(k) + 2 <= Nlo(k) for k in range(12, 200)), None)
    B694 = [(0, 17), (1, 1), (1, 1), (1, 1), (1, 1), (0, 1), (0, 1), (0, 1), (1, 1), (0, 0)]
    Y694 = norm('11' + '001' * 7 + '000' + M.build_G([d for d, _ in B694], [e for _, e in B694], 0))
    N30, Yt = orbit_v(8, '010001', 691)
    ok30, cl30 = inv_v(10, N30, Yt)
    rec("V0   Python model = #30's fin694: orbit 691 8 t2 = (17713, Y694), and Inv 10 17713 Y694 (Mw 77, M2 1054)",
        (N30, Yt) == (17713, Y694) and ok30 and Mw([e for _, e in B694]) == 77 and M2([e for _, e in B694]) == 1054, (N30, cl30))
    # #7: from K(1, 17, t1) to the first epoch with N >= 17,705
    M.FAST = True
    N, Y, n = 17, '1', 0
    while N < NSTAR_V:
        Nprev = N
        k, T = M.epoch(1, N, Y); _, N, Y = M.restart(k, T); n += 1
    # orbit n runs the n epochs e5 .. e(n+4) and lands at e(n+5), the first record with N >= 17,705
    rec('V1   orbit 687 17 t1 runs the 687 epochs e5..e691 and lands at e692 (N = 17,724), the first record with '
        'N >= 17,705; e691 has N = 17,670', (n, n + 4, n + 5, Nprev, N) == (687, 691, 692, 17670, 17724), (n, Nprev, N))
    x, W, ds, es, t = cp30.parse_residue(Y) if not cp30.classify(Y) else (None, None, [], [], None)
    kap = len(es)
    ok, cl = inv_v(kap, N, Y)
    rec('V1   #7 finite part: orbit %d 17 t1 = (%d, Y_%d); Inv %d N Y holds there, clause by clause' % (n, N, n + 5, kap), ok, cl)
    good = [kk for kk in range(0, 40) if inv_v(kk, N, Y)[0]]
    RES['_V'] = {'epochs_from_K(1,17,t1)': n, 'epochs_run': 'e5..e%d' % (n + 4), 'N_e%d' % (n + 4): Nprev,
                 'epoch_index_#7': n + 5, 'N': N, 'x': x, 'blocks (d,e)': list(zip(ds, es)), 'tail': t,
                 'kappa': kap, 'm(W)': (4 + t) * 2 ** kap + sum(d << i for i, d in enumerate(ds)) if t is not None else None,
                 'clauses': cl, 'kappas_with_Inv': good}
    # Inv carried along: kappa' = max(kappa, k(W')), as in the .v's inv_step (proved there; checked here on the orbit)
    bad = 0; steps = 0
    while N < maxN:
        k, T = M.epoch(1, N, Y); _, N, Y = M.restart(k, T); steps += 1
        if not cp30.classify(Y): kap = max(kap, len(cp30.parse_residue(Y)[3]))
        bad += not inv_v(kap, N, Y)[0]
    rec("V2   #30's Inv holds at every later epoch of #7's orbit (kappa = running max), to the end of section D", bad == 0 and steps > 0, (bad, steps))
    RES['_V']['carried_epochs'] = steps; RES['_V']['kappa_end'] = kap
    RES['_V']['_blocks_e692'] = list(zip(ds, es))

def section_RQ():
    """the Rocq draft of section 6's plan (rocq/M7_draft.v) and its stored check_kill log: the log is a PASS for this
    exact file, the draft states init7 / fin7 / inv7 / nonhalt_E / perm7 / nonhalt as the plan says, and its Y692
    blocks are the ones the Python model computes at e692 (section V)"""
    vf, lf = os.path.join(HERE, 'rocq', 'M7_draft.v'), os.path.join(HERE, 'rocq', 'check_kill_draft.out')
    if not (os.path.exists(vf) and os.path.exists(lf)): return
    import hashlib, re
    src = open(vf).read(); sha = hashlib.sha256(src.encode()).hexdigest()
    js = [json.loads(l[6:]) for l in open(lf) if l.startswith('JSON: ')]
    rec('RQ   stored check_kill log: PASS for this exact draft (sha256), tm = #7, theorem nonhalt, 0 assumptions, coqchk pass',
        len(js) == 1 and js[0]['result'] == 'PASS' and js[0]['sha256'] == sha and js[0]['tm'] == TM7 and
        js[0]['theorem'] == 'nonhalt' and js[0]['assumptions'] == [] and js[0]['coqchk'] == 'pass', (sha[:16], js[0]['result'] if js else None))
    stmts = ['Definition tm := Eval compute in (TM_from_str "%s").' % TM7,
             'Definition tm30 := Eval compute in (TM_from_str "%s").' % TM30,
             'Lemma fin7 : orbit 100000 687 17 t1 = Some (17724, Y692).', 'Lemma inv7 : Inv 10 17724 Y692.',
             'Lemma init7 : E;; tape0 -->* K 17 t1.', 'Lemma nonhalt_E : ~ halts tm30 (E;; tape0).',
             'Lemma perm7 : Perm (flip tm) tm30 phi.', 'Lemma nonhalt: ~halts tm c0.',
             'match q with A => E | B => A | C => B | D => F | E => C | F => D end.',
             'change (E, tape0) with (cconfig_to_config (nil,nil,S0,E));', 'cbn - [tape0]',
             'Definition Y692 : word := p11 16 (gw B692 0).']
    rec('RQ   the draft states the plan of section 6 (init7, fin7, inv7, nonhalt_E, phi = sigma, perm7, nonhalt)',
        all(src.count(s) == 1 for s in stmts), [s for s in stmts if src.count(s) != 1])
    m = re.search(r'Definition B692 : blks := \[(.*?)\]\.', src, re.S)
    b692 = [(d == 'true', int(e)) for d, e in re.findall(r'\((true|false),\s*(\d+)\)', m.group(1))] if m else None
    rec("RQ   the draft's B692 = the blocks of W at e692 from the Python model (x = 16, 10 blocks, bare tail)",
        b692 == [(bool(d), e) for d, e in RES['_V']['_blocks_e692']] and RES['_V']['x'] == 16 and RES['_V']['tail'] == 0, b692)
    m = re.search(r'Definition phi \(q : Q\) : Q :=\s*match q with (.*?) end\.', src, re.S)
    perm = dict(re.findall(r'([A-F]) => ([A-F])', m.group(1))) if m else {}
    rec("RQ   the draft's phi is X1's sigma (the unique conjugacy)", len(perm) == 6 and all(perm[ST[q]] == ST[PERM[q]] for q in range(6)), perm)
    RES['_RQ'] = {'draft_sha256': sha, 'compile_seconds': js[0].get('compile_seconds'), 'coqchk_seconds': js[0].get('coqchk_seconds'),
                  'checked_at': js[0].get('checked_at')}

# ---------------------------------------------------------------------------------------------------------------
def main():
    section_X0(); section_X1(); section_X2(2 * 10**5 if QUICK else 2 * 10**6); section_X3()
    print('X0-X3 done', round(time.time() - T0, 1), flush=True)
    # #30's table-level sections, unchanged
    cp30.section_A(); cp30.section_RP(); cp30.section_LP(); cp30.section_B(); cp30.section_E(); cp30.section_R()
    cp30.section_D6(); cp30.section_H(); cp30.section_D3()
    print("#30 table-level sections done", round(time.time() - T0, 1), flush=True)
    cp30.TAU_ = cp30.tau(); cp30.TEND = cp30.end_extra()
    RES['_tau'] = cp30.TAU_; RES['_T_end_extra'] = cp30.TEND
    k0, Nstar, around = cp30.analytic_threshold(cp30.TAU_, 48 if QUICK else 160)
    RES['_analytic'] = {'tau': cp30.TAU_, 'T': cp30.TEND, 'last_failing_kappa': k0, 'N_star': Nstar}
    print('threshold done, N* =', Nstar, round(time.time() - T0, 1), flush=True)
    section_X4(); section_X5(); section_X6(); print('X4-X6 done', round(time.time() - T0, 1), flush=True)
    maxN = max(Nstar + 1, 400000) if not QUICK else max(Nstar + 1, 20000)
    section_D_from(maxN, Nstar, 16, '0001', 5); print('D done', round(time.time() - T0, 1), flush=True)
    section_V(maxN); section_RQ(); print('V, RQ done', round(time.time() - T0, 1), flush=True)
    cp30.section_ADV(1500 if not QUICK else 200, 40 if not QUICK else 8); print('ADV done', round(time.time() - T0, 1), flush=True)
    bad = 0
    for cid in sorted(k for k in RES if not k.startswith('_')):
        r = RES[cid]; ok = r['pass'] == r['n']; bad += not ok
        print(('PASS ' if ok else 'FAIL ') + f"{r['pass']}/{r['n']}  {cid}" + ('' if ok else '  e.g. ' + str(r['fail'][:1])))
    for k in sorted(k for k in RES if k.startswith('_') and k not in ('_ESTAR',)): print(k, RES[k])
    print('ALL PASS' if bad == 0 else f'{bad} CLAIMS FAIL', f'({round(time.time() - T0, 1)} s, seed {SEED})')
    if not QUICK:
        os.makedirs(os.path.join(HERE, 'data'), exist_ok=True)
        with open(os.path.join(HERE, f'data/check_proof_seed{SEED}.json'), 'w') as f:
            json.dump({'seed': SEED, 'seconds': round(time.time() - T0, 1), 'claims': RES}, f, indent=1, default=str)

if __name__ == '__main__':
    main()