#!/usr/bin/env python3
"""check_proof.py: checks the delta proof.md of W4-3c (1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD), the parent
W4-3 (1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---) mirrored, renamed and started in its state F. Each check prints
PASS or FAIL; the exit code is the number of failures.

Sections (proof.md section in brackets):
  S1  identity: holdout list, sheet row, busycoq                                              [header]
  S2  the relation: mirror + renaming (12/12, the only map among 720 x 2), the start, the halting cell,
      mirrored lockstep with the parent's table from F; the run-length simulator scripts/rlsim.py on this
      machine's mirrored table against tools/sim.py on this machine's own table (direct simulation)  [1]
  S3  the opening run: the moves of lam, the record numbering (one extra start-up 3-cell move), the
      operational record exits 12..28 (step counts and head cells), equal to the parent's defect-model
      snapshots for this start; record exit 16 against direct simulation                          [2]
  S4  the invariant there: (L), (C), (H) at record exits 16..28 by an independent reading of the parent's
      section 3.3, and (W) = V_r5(1) at record exit 28, i.e. C_r5(2); the comparison with the parent's
      own record exits (five gaps differ, in a fixed pattern that moves one place per record)      [2.3, 3, 5]
  S5  the formal base data: cfg28, L28 and nus28 of this machine's .v (and of the parent's .v) are the
      tapes of these runs at record exit 28; the .v is the parent's file with the documented edits [6]
  S6  (--full) the parent's own checks for this start (parent check_proof.py --only S10)
  S7  proof.md's tables (record exits, chain at record exit 28, gap variables) and the numbers of the short
      public write-up (submission/proof.md) are the checked data                                [2.2, 2.3, 6]
Usage: nice -n 10 python3 -B check_proof.py [--full] [--only S1,S3,...] [--tables]
  Default run: about 1 minute. --full runs the records to 33 (windows V_r(1) for all six classes at 28..33,
  about 2.5 minutes more) and re-runs the parent's own checks for this start. --tables prints proof.md's
  tables from the computed data.
AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic)."""
import sys, os, re, itertools, subprocess, pickle, time, csv
from fractions import Fraction as Fr

HERE = os.path.dirname(os.path.abspath(__file__))
ROOT = os.path.abspath(os.path.join(HERE, '..', '..'))
sys.path.insert(0, os.path.join(HERE, 'scripts'))
sys.path.insert(0, os.path.join(ROOT, 'tools'))
import rlsim
import sim

TM = '1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD'
PARENT = '1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---'
TM512 = '1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---'
FLIP = TM.translate(str.maketrans('LR', 'RL'))     # this machine's table, every direction flipped
PDIR = os.path.join(ROOT, 'machines', PARENT)
SIGMA = dict(zip('ABCDEF', 'BCDEFA'))              # parent state -> this machine's state
PHI = {v: k for k, v in SIGMA.items()}             # this machine's state -> parent state (the .v's phi)
FULL = '--full' in sys.argv
TABLES = '--tables' in sys.argv
ONLY = set(sys.argv[sys.argv.index('--only') + 1].split(',')) if '--only' in sys.argv else None
N_LAST = 33 if FULL else 28
RESULTS = []
K0 = rlsim.K0
J = {5: 3, 0: 2, 1: 5, 2: 0, 3: 1, 4: 0}
CLS = {5: 'r5', 0: 'r0', 1: 'r1', 2: 'r2', 3: 'r3', 4: 'r4'}


def claim(sec, text, ok, detail=''):
    RESULTS.append((sec, text, bool(ok)))
    print(f"  [{'PASS' if ok else 'FAIL'}] {text}" + (f"  ({detail})" if detail else ''), flush=True)


def section(name, title):
    if ONLY and name not in ONLY:
        return False
    print(f"\n{name}  {title}", flush=True)
    return True


def cls(n): return (n - 11) % 6
def epoch(n): return (n - 16) // 6


# ------------------------------------------------------------------------------------------------- S1
def s1():
    raw = open(os.path.join(ROOT, 'data', 'holdouts', 'BB6_holdouts_740.txt'), 'rb').read().split(b'\n')
    lines = [l for l in raw if l]
    claim('S1', f'the 740 list has 740 entries; {TM} is line 588, byte for byte, exactly once; the parent is line 341',
          len(lines) == 740 and lines[587] == TM.encode() and lines.count(TM.encode()) == 1 and
          lines[340] == PARENT.encode() and lines.count(PARENT.encode()) == 1)
    r = subprocess.run([sys.executable, '-B', os.path.join(ROOT, 'tools', 'holdouts.py'), 'contains',
                        os.path.join(ROOT, 'data', 'holdouts', 'BB6_holdouts_740.txt'), TM], capture_output=True, text=True)
    claim('S1', 'tools/holdouts.py contains: exit 0, line 588', r.returncode == 0 and 'line 588' in r.stdout)
    rows = {row[0]: row for row in csv.reader(open(os.path.join(ROOT, 'data', 'sheet', '2026-10-09_results.csv')))}
    row = rows.get(TM)
    claim('S1', 'sheet (Results tab, 2026-10-09 export): class "Skelet 1-like Class 2"; status, notes, sources and '
          '"Done By" empty; the parent and line 512 have the same class', row is not None and
          row[2] == 'Skelet 1-like Class 2' and not row[1] and not row[3] and not row[4] and not row[5] and
          rows[PARENT][2] == rows[TM512][2] == 'Skelet 1-like Class 2', str(row))
    r = subprocess.run([sys.executable, '-B', os.path.join(ROOT, 'tools', 'holdouts.py'), 'solved', TM],
                       capture_output=True, text=True)
    pr = re.findall(r'proves=(\S+)', r.stdout)
    claim('S1', 'busycoq verify/ has no completed proof of this string (byte-exact, renamed or mirrored): it occurs '
          'only as an equivalence endpoint, in Eqv_v2.v (as written) and Eqv_v3.v (mirrored), neither proving it '
          '(tools/holdouts.py solved, exit 1)',
          r.returncode == 1 and 'verdict: no completed proof' in r.stdout and pr == ['-', '-'] and
          'Eqv_v2.v' in r.stdout and 'Eqv_v3.v' in r.stdout, f'proves= {pr}')


# ------------------------------------------------------------------------------------------------- S2
def table(tm):
    return rlsim.parse(tm)


def maps_between(src, dst):
    """All (renaming pi, mirror) with dst[pi q][s] = (w, +-d, pi q') whenever src[q][s] = (w, d, q')."""
    A, B = table(src), table(dst); out = []
    for perm in itertools.permutations('ABCDEF'):
        pi = dict(zip('ABCDEF', perm))
        for mirror in (False, True):
            ok = True
            for (q, s), t in A.items():
                u = B[(pi[q], s)]
                if t is None or u is None:
                    ok &= t is None and u is None
                else:
                    ok &= u == (t[0], -t[1] if mirror else t[1], pi[t[2]])
                if not ok: break
            if ok: out.append((''.join(perm), mirror))
    return out


def lockstep(n):
    """This machine from the blank tape against the parent's table from 0^inf F> 0^inf, transition by transition:
    same symbol read and written, opposite move, state = sigma(parent state); cell x here is cell -x there."""
    A, P = table(TM), table(PARENT)
    ta, tp = {}, {}; qa, qp = 'A', 'F'; pa = pp = 0
    for k in range(n):
        sa, sp = ta.get(pa, 0), tp.get(pp, 0)
        x, y = A[(qa, sa)], P[(qp, sp)]
        if x is None or y is None or sa != sp or qa != SIGMA[qp] or x != (y[0], -y[1], SIGMA[y[2]]):
            return False, k
        ta[pa] = x[0]; tp[pp] = y[0]; pa += x[1]; pp += y[1]; qa, qp = x[2], y[2]
    return {-x: v for x, v in ta.items()} == tp and pa == -pp and qa == SIGMA[qp], n


def lam_direct(tm, start, n, mirror):
    """Direct simulation: (step, cell) at every change of the leftmost cell that has held 1, in the frame where cell x
    is cell -x of the machine's tape if mirror (so it tracks the rightmost such cell of the machine's tape)."""
    T = table(tm); tape = {}; q = start; p = 0; lam = None; log = []
    sgn = -1 if mirror else 1
    for k in range(1, n + 1):
        w, mv, nq = T[(q, tape.get(p, 0))]
        tape[p] = w
        if w == 1 and (lam is None or sgn * p < lam): lam = sgn * p; log.append((k, lam))
        p += mv; q = nq
    return log


def s2():
    m = maps_between(PARENT, TM)
    claim('S2', 'sigma = (A,B,C,D,E,F) -> (B,C,D,E,F,A) with the mirror (L <-> R) maps the parent\'s table onto this '
          'one, 12/12 cells; it is the only map among the 720 renamings, with and without the mirror',
          m == [('BCDEFA', True)], f'maps found: {m}')
    T, P = table(TM), table(PARENT)
    claim('S2', 'this machine starts in A = sigma(F): it runs the mirror image of the parent\'s table from '
          '0^inf F> 0^inf; the inverse map phi = sigma^-1 is A->F, B->A, C->B, D->C, E->D, F->E (the .v\'s phi)',
          SIGMA['F'] == 'A' and PHI == dict(zip('ABCDEF', 'FABCDE')))
    undef = [k for k, v in T.items() if v is None]; intoA = [k for k, v in T.items() if v and v[2] == 'A']
    claim('S2', 'the only undefined cell is A1 (= sigma of the parent\'s F1); A is entered only by B1 = 0LA (sigma of '
          'the parent\'s A1 = 0RF, mirrored)', undef == [('A', 1)] and intoA == [('B', 1)] and T[('B', 1)] == (0, -1, 'A')
          and [k for k, v in P.items() if v and v[2] == 'F'] == [('A', 1)] and P[('A', 1)] == (0, 1, 'F'))
    ok, k = lockstep(2_000_000)
    claim('S2', 'lockstep: from the blank tape this machine and the parent\'s table from 0^inf F> 0^inf read the same '
          'symbol, write the same symbol and move in opposite directions at every step, with state = sigma(parent '
          'state); after 2,000,000 steps each tape is the other\'s mirror image (cell x here = cell -x there)', ok,
          f'{k:,} steps')
    t0 = time.time()
    ra = sim.run(sim.parse(TM), sim.Config.blank('A'), max_steps=10 ** 9)
    rp = sim.run(sim.parse(PARENT), sim.Config.blank('F'), max_steps=10 ** 9)
    fa, fp = ra.final, rp.final
    claim('S2', 'tools/sim.py (direct simulation): after 10^9 steps this machine from blank and the parent\'s table '
          'from F are mirror images: tape reversed, lo = -hi, head cell negated, opposite direction, state = '
          'sigma(parent state); neither halts',
          not ra.halted and not rp.halted and fa.tape == fp.tape[::-1] and fa.lo == -fp.hi and fa.hi == -fp.lo and
          fa.pos == -fp.pos and fa.state == SIGMA[fp.state] and fa.dir != fp.dir, f'{time.time() - t0:.0f} s')
    good = 0; cases = 0
    for tm_rl, st, tm_sim, mirror in ((FLIP, 'A', TM, True), (PARENT, 'F', PARENT, False)):
        for N in (1, 7, 1000, 123457, 3000001, 30000017, 100000003):
            cases += 1
            rl = rlsim.RL(tm_rl, st); rl.run_to(N)
            lo, cells, h = rl.cells()
            r = sim.run(sim.parse(tm_sim), sim.Config.blank(st), max_steps=N); c = r.final
            sg = -1 if mirror else 1
            rd = lambda x: cells[x - lo] if 0 <= x - lo < len(cells) else 0
            a = min(lo, sg * c.lo, sg * c.hi); b = max(lo + len(cells) - 1, sg * c.lo, sg * c.hi)
            same = all(rd(x) == c.read(sg * x) for x in range(a, b + 1))
            good += same and sg * c.pos == rl.pos and c.state == rl.state and r.step == rl.steps == N and not rl.halted
    claim('S2', 'scripts/rlsim.py (run-length simulator) on this machine\'s mirrored table (every L and R swapped) agrees '
          'with tools/sim.py on this machine\'s own table at 7 step counts from 1 to 100,000,003, cell x of the one '
          'being cell -x of the other (whole tape, head cell, state); rlsim on the parent\'s table from F agrees with '
          'tools/sim.py directly', good == cases, f'{good}/{cases}')
    good = 0
    rl = rlsim.RL(FLIP, 'A'); rl.run_to(2_000_000); good += rl.lam_log == lam_direct(TM, 'A', 2_000_000, True)
    rl = rlsim.RL(PARENT, 'F'); rl.run_to(2_000_000); good += rl.lam_log == lam_direct(PARENT, 'F', 2_000_000, False)
    claim('S2', 'rlsim\'s lam on the mirrored table changes at exactly the steps where, in direct simulation of this '
          'machine, the rightmost cell that has held 1 moves, and to minus that cell (first 2,000,000 steps); likewise '
          'the parent\'s table from F, unmirrored', good == 2)


# ------------------------------------------------------------------------------------------------- S3, S4 data
RUNS = {}


def defect_state(lo_c, cells, h):
    """Defect description of a tape with the head on cell h moving right (proof.md 2.1 of the parent): lo, hi, the
    pre-sweep defects strictly between them (edge h - 1 toggled), head cell, phase phi (B1 place: h = phi + 3)."""
    first1 = next(i for i, c in enumerate(cells) if c) + lo_c
    last1 = max(i for i, c in enumerate(cells) if c) + lo_c
    rd = lambda x: cells[x - lo_c] if 0 <= x - lo_c < len(cells) else 0
    D = set(e for e in range(first1, last1) if rd(e) == rd(e + 1))
    D ^= {h - 1}
    return dict(lo=first1 - 1, hi=last1 + 1, D=tuple(sorted(D)), p=h, dir=1, phi=(h - 3) % 4)


def snap_cb(store, rename):
    def cb(n, rl):
        lo_c, cells, h = rl.cells()
        st = defect_state(lo_c, cells, rl.pos)
        st.update(steps=rl.steps, state=rename[rl.state], read=rl.head_symbol(), facing=rl.facing, lam=rl.lam,
                  own_state=rl.state)
        if n in (16, 28): st['runs'] = rl.runs(); st['cells'] = (lo_c, cells)
        store[n] = st
    return cb


def get_runs():
    if RUNS: return RUNS
    for tag, tm, exit_state, rename, shift in (('588', FLIP, 'C', PHI, 1),
                                               ('341', PARENT, 'B', {q: q for q in 'ABCDEF'}, 0)):
        t0 = time.time(); store = {}
        rl, bursts, exits = rlsim.records(tm, 'A', exit_state, N_LAST, n_first=12, shift=shift,
                                          on_exit=snap_cb(store, rename))
        RUNS[tag] = dict(bursts=bursts, exits=exits, snaps=store, secs=time.time() - t0, iters=rl.iters,
                         lam_log=rl.lam_log)
    return RUNS


def load_parent_snaps():
    out = {}
    R = os.path.join(PDIR, 'scripts', 'closeout3', 'results')
    for tag, files in (('341', ['snap_341.pkl', 'snap_341_e3.pkl']), ('588', ['snap_588.pkl'])):
        out[tag] = {}
        for f in files:
            out[tag].update(pickle.load(open(os.path.join(R, f), 'rb')))
    return out


THREE17 = [9, 56, 329, 7891, 10906, 20681, 76882, 422401, 621182, 1179635, 4613856, 6881197, 12196818, 43554645,
           65364494, 114281959, 397794936]


def s3():
    R = get_runs(); SN = load_parent_snaps()
    b = R['588']['bursts']; lg = R['588']['lam_log']
    small = [(x[0], x[1]) for x in b if x[2] != 3]; three = [x for x in b if x[2] == 3]
    first_ok = lg[:2] == [(1, 0), (2, -1)]
    claim('S3', 'this machine from blank (rlsim on its mirrored table; lam = minus the rightmost cell of its own tape '
          'that has held 1): lam is set to 0 at step 1 and moves 1 cell at step 2; after that it moves by 2 cells at '
          'steps 48-49 (to -6) and 219-220 (to -11) and by 1 cell at step 6360 (to -15), and every other move is 3 '
          'cells in 3 consecutive steps; no halt',
          first_ok and small == [(1, 2), (48, 49), (219, 220), (6360, 6360)] and
          [c for k, c in lg if k in (48, 49, 219, 220, 6360)] == [-5, -6, -10, -11, -15] and
          all(x[1] - x[0] == 2 for x in three) and len(three) >= N_LAST + 1,
          f'{len(small)} small moves, {len(three)} 3-cell moves; lam at the small moves: '
          f'{[(k, c) for k, c in lg if k in (1, 2, 48, 49, 219, 220, 6360)]}')
    claim('S3', 'its 3-cell moves 1..17 begin at steps 9, 56, 329, 7891, 10906, 20681, 76882, 422401, 621182, 1179635, '
          '4613856, 6881197, 12196818, 43554645, 65364494, 114281959, 397794936',
          [x[0] for x in three[:17]] == THREE17)
    p = R['341']['bursts']
    psmall = [(x[0], x[1]) for x in p if x[2] != 3]
    claim('S3', 'the parent from blank (same code): small moves at 1, 6-7, 838-839, 7820, 17531-17532 and its 16th '
          '3-cell move at 398,088,768-770, as in the parent\'s section 3.1; so record n is the parent\'s n-th 3-cell '
          'move and this run\'s (n + 1)-th (the parent\'s write-up, section 9: one extra start-up 3-cell move here)',
          psmall == [(1, 1), (6, 7), (838, 839), (7820, 7820), (17531, 17532)] and
          [x for x in p if x[2] == 3][15][:2] == (398088768, 398088770) and three[16][:2] == (397794936, 397794938))
    ex = R['588']['exits']; exp = R['341']['exits']
    ok = all(ex[n][0] == SN['588'][n]['steps'] and ex[n][1] == SN['588'][n]['B'] - 1 for n in range(12, N_LAST + 1))
    okp = all(exp[n][0] == SN['341'][n]['steps'] and exp[n][1] == SN['341'][n]['B'] - 1 for n in range(12, N_LAST + 1))
    claim('S3', f'operational record exits n = 12..{N_LAST} (first configuration after record n with the head in '
          'this machine\'s C = sigma(B) reading 1, moving right in the mirror frame, and exactly 10 + 4K - 2 pre-sweep '
          'defects in [lam, h-1], K = K0(r) + 2e, e = -1 for n = 12..15): their steps and head cells (= B - 1) are '
          'those of the parent\'s defect-model snapshots for this start; the same holds for the parent\'s own run',
          ok and okp, f"rlsim {R['588']['secs']:.0f} s + {R['341']['secs']:.0f} s")
    claim('S3', 'record exit 16 at step 397,796,108 (head cell 1,092 in the mirror frame); record exit 28 at step '
          '2,629,080,059,236 (head cell 111,832); the parent\'s record exit 28 is at step 2,629,088,227,408 (head cell '
          '111,894), 8,168,172 steps later',
          ex[16] == (397796108, 1092) and ex[28] == (2629080059236, 111832) and exp[28] == (2629088227408, 111894) and
          exp[28][0] - ex[28][0] == 8168172)
    good = 0
    for n in range(12, N_LAST + 1):
        s = R['588']['snaps'][n]; t = SN['588'][n]
        good += (s['lo'], s['hi'], s['D'], s['p'], s['phi']) == (t['lo'], t['hi'], tuple(t['D']), t['p'], t['phi'] % 4) \
            and t['dir'] == 1 and s['own_state'] == 'C' and s['read'] == 1
    claim('S3', f'at each record exit 12..{N_LAST} the defect state read off the rlsim tape (lo, hi, every pre-sweep '
          'defect, head cell, direction, phase) equals the parent\'s defect-model snapshot for this start; the head '
          'is in this machine\'s C reading 1', good == N_LAST - 11, f'{good}/{N_LAST - 11}')
    # record exit 16 against direct simulation of this machine's own (unmirrored) table
    s16 = R['588']['snaps'][16]; lo_c, cells = s16['cells']
    r = sim.run(sim.parse(TM), sim.Config.blank('A'), max_steps=s16['steps']); c = r.final
    rd = lambda x: cells[x - lo_c] if 0 <= x - lo_c < len(cells) else 0
    a = min(lo_c, -c.hi); bb = max(lo_c + len(cells) - 1, -c.lo)
    same = all(rd(x) == c.read(-x) for x in range(a, bb + 1))
    claim('S3', 'direct simulation of this machine\'s own table (tools/sim.py) to step 397,796,108 is the mirror image '
          'of the rlsim tape at record exit 16: every cell, head on cell -1,092 in state C reading 1; C1 = 0LC moves '
          'left on this tape (right in the mirror)',
          not r.halted and r.step == 397796108 and same and c.pos == -1092 and c.state == 'C' and c.symbol == 1 and
          table(TM)[('C', 1)] == (0, -1, 'C'))


# ------------------------------------------------------------------------------------------------- S4
def v_table():
    """V_r(u) as written in the parent's write-up (submission/proof.md, section 3.4)."""
    txt = open(os.path.join(PDIR, 'submission', 'proof.md')).read()
    sec = txt[txt.index('### 3.4 The window vectors'):txt.index('## 4. Three regions')]
    V = {}
    for line in sec.split('\n'):
        m = re.match(r'\| r([0-5]) \| (.*) \| (.*) \|$', line)
        if not m: continue
        def parse(cell):
            if cell.strip() == '(none)': return []
            return [re.sub(r'(\d+)u', r'\1*u', item.strip()) for item in cell.split(', ')]
        V[int(m.group(1))] = (parse(m.group(2)), parse(m.group(3)))
    return V


def ev_v(expr, u):
    val = eval(expr.replace('/', '*Fr(1)/'), {'u': u, 'Fr': Fr})
    assert Fr(val).denominator == 1
    return int(val)


LEFT_WORD = (-32, -27, -26, -21, -20, -15, -14, -9, -8, -4)
NLEFT = len(LEFT_WORD) + 1          # gaps lo -> first left-word defect -> ... -> A-4 -> A+2


def parse_C(s, n):
    """An independent reading of the parent's section 3.3 at record exit n: returns (ok, info). info has A, B, K, the
    chain gaps (in order), the right gaps (B -> x_1 -> ... -> hi), all gaps from lo to hi, and what failed."""
    r = cls(n); e = epoch(n); K = K0[r] + 2 * e
    D = list(s['D']); lo, hi = s['lo'], s['hi']; A = lo + 34; bad = []
    if s['lam'] != lo + 1: bad.append('lam != lo + 1')
    left = [x - A for x in D if x < A]
    if tuple(left) != LEFT_WORD: bad.append('(L)')
    rest = [x for x in D if x >= A]
    chain = rest[:4 * K - 2]; right = rest[4 * K - 2:]
    if len(chain) < 4 * K - 2 or chain[:2] != [A + 2, A + 3]: bad.append('block 1')
    gaps = [b - a for a, b in zip(chain, chain[1:])]
    roles = ['d'] + ['i', 'd', 's', 's'] * (K - 1)
    need = {'d': (1, 1), 's': (0, 4), 'i': (1, 5)}
    for g, ro in zip(gaps, roles):
        res, mn = need[ro]
        if g % 4 != res or g < mn: bad.append(f'gap {g} role {ro}')
    B = chain[-1] + 2
    if not (s['p'] == B - 1 and s['state'] == 'B' and s['read'] == 1 and s['facing'] > 0): bad.append('(H)')
    if right and right[0] <= B: bad.append('x_1 <= B')
    rgaps = [b - a for a, b in zip([B] + right, right + [hi])]
    allg = [b - a for a, b in zip([lo] + D, D + [hi])]
    return not bad, dict(A=A, B=B, K=K, lo=lo, hi=hi, gaps=gaps, roles=roles, right=rgaps, all=allg, bad=bad,
                         win=gaps[len(gaps) - J[r]:] if J[r] else [])


def blocks_of(info):
    """The chain by blocks: block 1 = [digit gap]; block j >= 2 = [inter, digit, sep, sep]."""
    g = info['gaps']
    return [[g[0]]] + [g[1 + 4 * j:5 + 4 * j] for j in range(info['K'] - 1)]


PATTERN = [0, 1, 2, 3, 7]
PDIFF = [-4, -12, -16, 8, -36]


def s4():
    R = get_runs(); V = v_table()
    claim('S4', 'the V_r(u) table parsed from the parent\'s write-up (section 3.4) has six rows; at u = 1 every entry '
          'is an integer; r5 reads chain (8277, 24912, 74808), right (224493, 673559, 7, 9841, 1942040, 3)',
          sorted(V) == [0, 1, 2, 3, 4, 5] and [ev_v(x, 1) for x in V[5][0]] == [8277, 24912, 74808] and
          [ev_v(x, 1) for x in V[5][1]] == [224493, 673559, 7, 9841, 1942040, 3])
    for tag in ('588', '341'):
        good = 0; bads = []
        for n in range(16, N_LAST + 1):
            ok, info = parse_C(R[tag]['snaps'][n], n)
            good += ok
            if not ok: bads.append((n, info['bad'][:3]))
        who = 'this machine (mirror frame, parent\'s state names)' if tag == '588' else 'the parent (control)'
        claim('S4', f'{who}: at record exits 16..{N_LAST}, (L) lo = A - 34 = lam - 1 and the left word at A - 32, -27, '
              '-26, -21, -20, -15, -14, -9, -8, -4; (C) K = K0(r) + 2e blocks in U0, block 1 = (A+2; A+3), every chain '
              'gap with the residue and minimum of its role; (H) the head on B - 1 in state B (parent\'s naming) reading '
              '1, moving right', good == N_LAST - 15, f'{good}/{N_LAST - 15} {bads[:2]}')
    good = 0; rng = range(28, N_LAST + 1)
    for n in rng:
        ok, info = parse_C(R['588']['snaps'][n], n); r = cls(n); u = 9 ** (epoch(n) - 2)
        good += ok and info['win'] == [ev_v(x, u) for x in V[r][0]] and info['right'] == [ev_v(x, u) for x in V[r][1]]
    ok28, i28 = parse_C(R['588']['snaps'][28], 28)
    claim('S4', 'record exit 28 of this machine is in C_r5(2): K = 7, the last 3 chain gaps are V_r5(1)\'s '
          '(8277, 24912, 74808) and the right region B -> x_1 -> ... -> hi is (224493, 673559, 7, 9841, 1942040, 3); '
          'lo = -94, A = -60, B = 111,833, hi = 2,961,776 in the mirror frame',
          ok28 and i28['K'] == 7 and i28['win'] == [8277, 24912, 74808] and
          i28['right'] == [224493, 673559, 7, 9841, 1942040, 3] and
          (i28['lo'], i28['A'], i28['B'], i28['hi']) == (-94, -60, 111833, 2961776))
    if N_LAST > 28:
        claim('S4', f'record exits 28..{N_LAST} of this machine (all six classes, e = 2) are in C_r(2) with window '
              'V_r(1)', good == len(rng), f'{good}/{len(rng)}')
    # comparison with the parent, record exit by record exit
    gl = lambda s: [y - x for x, y in zip([s['lo']] + list(s['D']), list(s['D']) + [s['hi']])]
    good = 0; idx = {}
    for n in range(12, N_LAST + 1):
        a, b = gl(R['588']['snaps'][n]), gl(R['341']['snaps'][n])
        d = [i for i in range(len(a)) if len(a) == len(b) and a[i] != b[i]]
        if len(a) == len(b) and len(d) == 5 and [x - d[0] for x in d] == PATTERN and \
                [a[i] - b[i] for i in d] == PDIFF and sum(a) - sum(b) == -60:
            good += 1; idx[n] = d[0]
    claim('S4', f'at every record exit 12..{N_LAST} the gap lists of the two runs (lo -> each defect -> hi) have the same '
          'length and differ in exactly five entries, at places i, i+1, i+2, i+3 and i+7, by -4, -12, -16, +8 and '
          '-36 (this run minus the parent\'s; 60 cells in all); i grows by one per record',
          good == N_LAST - 11 and all(idx[n] == idx[12] + n - 12 for n in idx), f'{good}/{N_LAST - 11}, i at 12: '
          f'{idx.get(12)}')
    good_late = 0; good_early = 0; late = range(26, N_LAST + 1); early = range(16, 26); where = {}
    for n in range(16, N_LAST + 1):
        oka, a = parse_C(R['588']['snaps'][n], n); okb, b = parse_C(R['341']['snaps'][n], n)
        d = [i for i, (x, y) in enumerate(zip(a['all'], b['all'])) if x != y]
        ci = [i - NLEFT for i in d]; nch = len(a['gaps']); deep = [0 <= c < nch - J[cls(n)] for c in ci]
        base = oka and okb and len(d) == 5 and a['K'] == b['K'] and a['A'] - b['A'] == -2 \
            and a['all'][:NLEFT] == b['all'][:NLEFT]
        dB = a['B'] - b['B']
        if n >= 26:
            good_late += base and all(deep) and a['win'] == b['win'] and a['right'] == b['right'] and dB == -62
        else:
            where[n] = 'window' if ci[4] < nch else 'right region'
            good_early += base and all(deep[:4]) and not deep[4] and dB == (-62 if ci[4] < nch else -26)
    claim('S4', f'against the parent\'s own record exits 16..{N_LAST}: the same K and left word, A 2 cells further left '
          '(mirror frame); from record exit 26 on all five differing gaps are deep chain gaps, so the window and the '
          'right region are the parent\'s and B is 62 cells further left; at 16..25 the first four are deep and the '
          'fifth (936 against 972 at 16, the first fossil of the start-up windows) still lies in the window (B 62 '
          'cells further left) or the right region (B 26 cells further left)',
          good_late == len(late) and good_early == len(early), f'{good_late}/{len(late)}, {good_early}/{len(early)}; '
          f'fifth gap at 16..25: {where}')
    ok28p, p28 = parse_C(R['341']['snaps'][28], 28)
    ba, bp = blocks_of(i28), blocks_of(p28)
    diffb = [j + 1 for j in range(7) if ba[j] != bp[j]]
    roles_ok = all(g % 4 == res and g >= mn for g, (res, mn) in zip(ba[4] + ba[5], [(1, 5), (1, 1), (0, 4), (0, 4)] * 2))
    claim('S4', 'at record exit 28 the five are block 5\'s inter, digit and two separator gaps, (5, 1, 8, 52) here against '
          '(9, 13, 24, 44), and block 6\'s last separator gap, 936 against 972; blocks 1-4 and 7 are the parent\'s; '
          'all of them have the residue and minimum of their role',
          ok28p and diffb == [5, 6] and ba[4] == [5, 1, 8, 52] and bp[4] == [9, 13, 24, 44] and
          ba[5] == [37, 37, 36, 936] and bp[5] == [37, 37, 36, 972] and roles_ok, f'blocks here: {ba}')


# ------------------------------------------------------------------------------------------------- S5
def parse_cfg28(vtext):
    m = re.search(r'Definition cfg28 : cfg :=\s*Rc (\w)\s*\(\[(.*?)\], T0\)\s*\(\[(.*?)\], T0\)\.', vtext, re.S)
    if not m: return None
    def runs(t): return [(1 if a == 'S1' else 0, int(b)) for a, b in re.findall(r'\((S[01]), cn (\d+)\)', t)]
    return m.group(1), runs(m.group(2)), runs(m.group(3))


def parse_nus(vtext):
    m = re.search(r'Definition nus28 : list \(list N\) :=\s*\[(.*?)\]%N\.', vtext, re.S)
    return [[int(x) for x in re.findall(r'\d+', blk)] for blk in re.findall(r'\[([\d; ]+)\]', m.group(1))]


def parse_L28(vtext):
    m = re.search(r'Definition L28 : list run :=\s*\[(.*?)\]%N\.', vtext, re.S)
    return [(1 if a == 'S1' else 0, int(b)) for a, b in re.findall(r'\((S[01]), cn (\d+)\)', m.group(1))]


def decode_nus(L):
    """nus from the left run list (nearest first): 6 blocks of 4 runs (t, s, a, lp) = (4+4x0, 4+4x1, 1+4x2, 5+4x3)."""
    out = []
    for j in range(6):
        r = [n for _, n in L[4 * j:4 * j + 4]]
        x = [r[0] - 4, r[1] - 4, r[2] - 1, r[3] - 5]
        if any(v % 4 or v < 0 for v in x): return None
        out.append([v // 4 for v in x])
    return out


def s5():
    vs = os.path.join(HERE, TM + '.v'); vp = os.path.join(PDIR, PARENT + '.v')
    if not os.path.exists(vs):
        claim('S5', 'this machine\'s .v exists', False); return
    ts, tp = open(vs).read(), open(vp).read()
    R = get_runs()
    good = 0
    for vt, tag, st_ok in ((ts, '588', 'C'), (tp, '341', 'B')):
        q, L, Rr = parse_cfg28(vt)
        sn = R[tag]['snaps'][28]
        l2, r2 = sn['runs']
        good += q == 'B' and sn['own_state'] == st_ok and sn['facing'] > 0 and \
            rlsim.expand_runs(L) == rlsim.expand_runs(l2) and rlsim.expand_runs(Rr) == rlsim.expand_runs(r2)
    claim('S5', 'cfg28 of each .v (Rc B, both sides blank beyond the listed runs) is exactly the tape of the rlsim run at '
          'its record exit 28: this machine at step 2,629,080,059,236 read in the mirror (its state C = sigma(B)), the '
          'parent at 2,629,088,227,408 (state B); cell by cell on both sides of the head', good == 2, f'{good}/2')
    Ls, Lp = parse_L28(ts), parse_L28(tp); ns, np_ = parse_nus(ts), parse_nus(tp)
    cs, cp = parse_cfg28(ts), parse_cfg28(tp)
    diffL = [i for i, (a, b) in enumerate(zip(Ls, Lp)) if a != b]
    claim('S5', 'L28 = the left side of cfg28 in both files; nus28 decodes from L28 (t, s, a, lp = 4+4x0, 4+4x1, 1+4x2, '
          '5+4x3, nearest block first); the two L28 differ in runs 5 and 9-12 only, (S0, 936) against (S0, 972) and '
          '52, 8, 1, 5 against 44, 24, 13, 9, so the two nus28 differ only in blocks 2 and 3 (from the head): '
          '[233; 8; 9; 8] and [12; 1; 0; 0] against [242; 8; 9; 8] and [10; 5; 3; 1]',
          Ls == cs[1] and Lp == cp[1] and decode_nus(Ls) == ns and decode_nus(Lp) == np_ and len(Ls) == len(Lp) and
          diffL == [4, 8, 9, 10, 11] and Ls[4] == (0, 936) and Lp[4] == (0, 972) and
          [x[1] for x in Ls[8:12]] == [52, 8, 1, 5] and [x[1] for x in Lp[8:12]] == [44, 24, 13, 9] and
          ns[1] == [233, 8, 9, 8] and np_[1] == [242, 8, 9, 8] and ns[2] == [12, 1, 0, 0] and np_[2] == [10, 5, 3, 1]
          and ns[0] == np_[0] == [18701, 6227, 2069, 683] and ns[3:] == np_[3:] == [[0, 0, 0, 0]] * 3,
          f'nus28 here: {ns}')
    ok28, i28 = parse_C(R['588']['snaps'][28], 28)
    claim('S5', 'L28 read from the head is the chain of record exit 28 (S4) backwards: its first 25 runs are the 25 chain '
          'gaps from B - 2 down to A + 2, the next 11 the gaps of the left word down to lo; cfg28\'s right side starts '
          'with x_1 - (B - 2) = 224493 + 2', [n for _, n in Ls] == i28['all'][:NLEFT + 25][::-1] and
          cs[2][0] == (1, i28['right'][0] + 2))
    # the .v is the parent's with the documented edits
    pl, sl = tp.split('\n'), ts.split('\n')
    i0 = pl.index(next(x for x in pl if x.startswith('Notation "c --> c\'"')))
    i1 = pl.index(next(x for x in pl if x.startswith('(* Base case'))) - 1
    body = [re.sub(r'\btm\b', 'tmP', x) for x in pl[i0:i1]]
    j0 = sl.index(body[0]) if body[0] in sl else -1
    same_body = j0 >= 0 and sl[j0:j0 + len(body)] == body
    claim('S5', 'the .v contains the parent\'s file from its notations through Lemma S (everything before the base '
          'case), byte for byte with tm renamed tmP', same_body, f'{len(body)} lines')
    k0 = pl.index(next(x for x in pl if x.startswith('(* The invariant at the start of every record interval')))
    k1 = pl.index(next(x for x in pl if x.startswith('(* From record exit 28 to the invariant')))
    inv = [re.sub(r'\btm\b', 'tmP', x) for x in pl[k0:k1]]
    m0 = sl.index(inv[0]) if inv[0] in sl else -1
    same_inv = m0 >= 0 and sl[m0:m0 + len(inv)] == inv
    i2 = pl.index('Lemma inv28 : Inv (C5, 2, 0%N, nus28).'); i3 = pl.index(next(x for x in pl if x.startswith('Lemma nonhalt')))
    tail = [re.sub(r'\btm\b', 'tmP', x) for x in pl[i2:i3]]
    while tail and not tail[-1].strip(): tail.pop()
    j2 = sl.index(tail[0]) if tail[0] in sl else -1
    same_tail = j2 >= 0 and sl[j2:j2 + len(tail)] == tail
    claim('S5', 'and the parent\'s invariant section (Inv, inv_step) and its inv28, split1, b28a, b28b, b28_chain, '
          'b28_right and base28, byte for byte with tm renamed tmP (so the record-exit episode and the step into Inv '
          'are unchanged)', same_inv and same_tail, f'{len(inv)} + {len(tail)} lines')
    has = ('Definition tm := Eval compute in (TM_from_str "%s").' % TM in ts and
           'Definition tmP := Eval compute in (TM_from_str "%s").' % PARENT in ts and
           'Lemma nonhalt : ~ halts tm c0.' in ts and 'Lemma perm_phi : Perm (flip tm) tmP phi.' in ts and
           'Lemma init28 : F;; tape0 -->* ev_cfg [] (fun _ => const S0) cfg28.' in ts and
           'Lemma nonhalt_P : ~ halts tmP (F;; tape0).' in ts and
           'match q with A => F | B => A | C => B | D => C | E => D | F => E end.' in ts and
           re.search(r'Lemma nonhalt : ~ halts tm c0\.\s*Proof\.\s*intros H\. apply flip_halts in H\.\s*'
                     r'change \(halts \(flip tm\) \(A;; tape0\)\) in H\.\s*'
                     r'exact \(nonhalt_P \(perm_halts _ _ _ _ _ perm_phi H\)\)\.\s*Qed\.', ts) is not None)
    claim('S5', 'the .v defines tm (this string) and tmP (the parent), init28 from F;; tape0, nonhalt_P, phi = '
          'sigma^-1, perm_phi : Perm (flip tm) tmP phi, and ends with Lemma nonhalt : ~ halts tm c0 by flip_halts '
          'and perm_halts', has)
    cks = re.findall(r'Lemma ck_(\d+) : runp (\d+) b28_(\d+) = Some \((b28_(\d+)|cfg28), true\)\.', ts)
    okc = len(cks) == 38 and all(int(c[0]) == i == int(c[2]) for i, c in enumerate(cks)) and \
        all(c[1] == '500000' and c[4] == str(i + 1) for i, c in enumerate(cks[:37])) and cks[37][3] == 'cfg28' and \
        37 * 500000 + int(cks[37][1]) == 18571554 and ts.count('native_compute') >= 38 and \
        'Definition b28_0 : cfg := mkc true F [] [].' in ts
    claim('S5', 'the base case is 38 pieces ck_0 .. ck_37 from b28_0 = F on the blank tape (runp 500000 each, the last '
          'runp 71554 to cfg28): 18,571,554 simulator steps in all', okc, f'{len(cks)} pieces')
    log = os.path.join(HERE, 'rocq', 'check_kill.log')
    st = open(log).read() if os.path.exists(log) else ''
    print(f"  [INFO] check_kill on this .v: {'PASS' if 'PASS' in st and 'FAIL' not in st else 'not passed (yet)'} "
          f"(rocq/check_kill.log; only a check_kill PASS is a kill)")


def s_parent():
    r = subprocess.run(['nice', '-n', '10', sys.executable, '-B', os.path.join(PDIR, 'check_proof.py'), '--only', 'S10'],
                       capture_output=True, text=True, cwd=PDIR)
    lines = [l for l in r.stdout.split('\n') if '588' in l and '[' in l]
    ok = r.returncode == 0 and lines and all('[PASS]' in l for l in lines)
    for l in lines: print('     ' + l.strip()[:200])
    claim('S6', 'the parent\'s check_proof.py --only S10 passes, including its claims for this start (line 588)', ok,
          f'exit {r.returncode}, {len(lines)} lines on 588')


# ------------------------------------------------------------------------------------------------- S7
def fmt(x): return f'{x:,}'


def table_rows():
    R = get_runs()
    rows = []
    for n in range(16, 29):
        r = cls(n); K = K0[r] + 2 * epoch(n)
        rows.append((n, CLS[r], K, R['588']['exits'][n][0], R['341']['exits'][n][0], R['588']['exits'][n][1]))
    return rows


def md_table(txt, start_marker):
    """The markdown table rows (as lists of cells) of the first table after start_marker."""
    if start_marker not in txt: return []
    i = txt.index(start_marker); out = []; seen = False
    for line in txt[i:].split('\n'):
        if line.startswith('|'):
            seen = True
            cells = [c.strip().replace('**', '') for c in line.strip().strip('|').split('|')]
            if not all(set(c) <= set('-:') for c in cells): out.append(cells)
        elif seen:
            break
    return out[1:]


def s7():
    R = get_runs()
    txt = open(os.path.join(HERE, 'proof.md')).read()
    rows = table_rows()
    if TABLES:
        print('| n | class | K | step here | step in the parent | head cell (mirror frame) |')
        print('|---:|---|---:|---:|---:|---:|')
        for n, c, K, a, b, h in rows: print(f'| {n} | {c} | {K} | {fmt(a)} | {fmt(b)} | {fmt(h)} |')
    got = md_table(txt, '### 2.2 Record exits')
    exp = [[str(n), c, str(K), fmt(a), fmt(b), fmt(h)] for n, c, K, a, b, h in rows]
    claim('S7', 'proof.md 2.2: the record-exit table (n = 16..28: class, K, step here, step in the parent, head cell) is '
          'the computed data, row for row', got == exp, f'{sum(1 for x, y in zip(got, exp) if x == y)}/{len(exp)} rows')
    exp22 = exp
    ok28, i28 = parse_C(R['588']['snaps'][28], 28); ok28p, p28 = parse_C(R['341']['snaps'][28], 28)
    ba, bp = blocks_of(i28), blocks_of(p28)
    exp = []
    for j, (x, y) in enumerate(zip(ba, bp)):
        def cell(k):
            if j == 0: return ['–', str(x[0]), '–'][k]
            v = [str(x[0]), str(x[1]), f'{x[2]}, {x[3]}'][k]
            w = [str(y[0]), str(y[1]), f'{y[2]}, {y[3]}'][k]
            return v if v == w else f'{v} (parent {w})'
        exp.append([str(j + 1), cell(0), cell(1), cell(2)])
    if TABLES:
        print('| block | inter gap before its digit | digit gap | separator gaps |')
        print('|---|---:|---:|---|')
        for r in exp: print('| ' + ' | '.join(r) + ' |')
    got = md_table(txt, '### 2.3 Record exit 28')
    claim('S7', 'proof.md 2.3: the chain table at record exit 28 (inter, digit and separator gaps of blocks 1..7, with '
          'the parent\'s value where it differs) is the computed chain', got == exp,
          f'{sum(1 for x, y in zip(got, exp) if x == y)}/{len(exp)} rows')
    exp23 = exp
    vs = open(os.path.join(HERE, TM + '.v')).read(); ns = parse_nus(vs)
    m = re.search(r'this start:\s+(.*)\n\s*parent:\s+(.*)\n', txt)
    def fmt_nus(nu):
        s = ' '.join('[' + '; '.join(map(str, b)) + ']' for b in nu[:3])
        return s + ' [0; 0; 0; 0]^3' if nu[3:] == [[0, 0, 0, 0]] * 3 else None
    np_ = parse_nus(open(os.path.join(PDIR, PARENT + '.v')).read())
    claim('S7', 'proof.md 6: the gap variables quoted for this start and the parent are the two .v files\' nus28',
          m is not None and m.group(1).strip() == fmt_nus(ns) and m.group(2).strip() == fmt_nus(np_),
          f'{m.groups() if m else None}')
    # the short public write-up (submission/proof.md): its block lines, gap variables and step counts
    sub = open(os.path.join(HERE, 'submission', 'proof.md')).read()
    Ls = parse_L28(vs); Lp = parse_L28(open(os.path.join(PDIR, PARENT + '.v')).read())
    exp = {2: ([n for _, n in Ls[4:8]], [n for _, n in Lp[4:8]]), 3: ([n for _, n in Ls[8:12]], [n for _, n in Lp[8:12]])}
    m2 = re.search(r'this start:\s+(.*)\n\s*parent:\s+(.*)\n', sub)
    mt = re.search(r't\s+=\s+4 \+ 4 x \d+\s+=\s+(\d+)\s+against\s+4 \+ 4 x \d+\s+=\s+(\d+)', sub)
    mq = re.search(r'\(t, s, a, lp\)\s+=\s+\(([\d, ]+)\)\s+against\s+\(([\d, ]+)\)', sub)
    blk_ok = (mt is not None and [int(mt.group(1)), int(mt.group(2))] == [exp[2][0][0], exp[2][1][0]] and
              mq is not None and [int(x) for x in mq.group(1).split(',')] == exp[3][0] and
              [int(x) for x in mq.group(2).split(',')] == exp[3][1])
    sub22, sub23 = md_table(sub, '### 2.2 Record exits'), md_table(sub, '### 2.3 Record exit 28')
    claim('S7', 'submission/proof.md (the public write-up): its 2.2 record-exit table and 2.3 chain table are the '
          'computed data; its block 2 gap t (936 against 972) and block 3 (t, s, a, lp) (52, 8, 1, 5 against 44, 24, '
          '13, 9) are runs of the two .v files\' L28; its gap variables are the two nus28; and its step counts are '
          '2,629,080,059,236 machine steps and 18,571,554 simulator steps',
          sub22 == exp22 and sub23 == exp23 and blk_ok and m2 is not None and m2.group(1).strip() == fmt_nus(ns) and
          m2.group(2).strip() == fmt_nus(np_) and '2,629,080,059,236' in sub and '18,571,554' in sub,
          f'2.2 {sub22 == exp22}, 2.3 {sub23 == exp23}, blocks {blk_ok}')


def main():
    t0 = time.time()
    if section('S1', 'identity'): s1()
    if section('S2', 'the relation; rlsim against direct simulation'): s2()
    if section('S3', 'the opening run from the blank tape'): s3()
    if section('S4', 'the invariant at the record exits'): s4()
    if section('S5', 'the formal base data'): s5()
    if FULL and section('S6', 'the parent\'s own checks for this start'): s_parent()
    if section('S7', 'proof.md\'s tables'): s7()
    nf = sum(1 for r in RESULTS if not r[2])
    print(f"\nSUMMARY {'PASS' if nf == 0 else 'FAIL'}: {len(RESULTS) - nf}/{len(RESULTS)} claims, {time.time() - t0:.0f} s")
    sys.exit(nf)


if __name__ == '__main__':
    main()