#!/usr/bin/env python3
"""check_proof.py: checks the delta proof.md of W4-3b (1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---), the parent
W4-3 (1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---) started in its state B. 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: the renaming (12/12, the only map among 720 x 2), the start, the halting cell,
      lockstep with the parent's table from B; the run-length simulator scripts/rlsim.py against
      tools/sim.py (direct simulation)                                                         [1]
  S3  the opening run, on this machine's own table with rlsim: the moves of lam, the record numbering,
      the operational record exits 16..28 (step counts and head cells), equal to the parent's
      defect-model snapshots for this start                                                   [2, 3]
  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 (one deep chain gap differs, by 4)                                       [3, 4]
  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 [5]
Usage: nice -n 10 python3 -B check_proof.py [--full] [--only S1,S3,...]
  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 (parent check_proof.py --only S10).
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 = '1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---'
PARENT = '1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---'
TM588 = '1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD'
PDIR = os.path.join(ROOT, 'machines', PARENT)
SIGMA = dict(zip('ABCDEF', 'EABCDF'))          # parent state -> this machine's state
FULL = '--full' 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}


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 512, byte for byte, exactly once; the parent is line 341',
          len(lines) == 740 and lines[511] == 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 512', r.returncode == 0 and 'line 512' 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 588 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[TM588][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)
    claim('S1', 'busycoq verify/ has no completed proof of this string (byte-exact, renamed or mirrored): it occurs '
          'only as an equivalence endpoint (tools/holdouts.py solved, exit 1)',
          r.returncode == 1 and 'no completed proof' in r.stdout and 'byte-exact: none' in r.stdout)


# ------------------------------------------------------------------------------------------------- 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 B> 0^inf, transition by transition."""
    A, P = table(TM), table(PARENT)
    ta, tp = {}, {}; qa, qp = 'A', 'B'; 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 ta == tp and pa == pp and qa == SIGMA[qp], n


def lam_direct(tm, n):
    """Direct simulation: (step, cell) at every change of the leftmost cell that has held 1."""
    T = table(tm); tape = {}; q = 'A'; p = 0; lam = None; log = []
    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 p < lam): lam = p; log.append((k, p))
        p += mv; q = nq
    return log


def s2():
    m = maps_between(PARENT, TM)
    claim('S2', 'sigma = (A,B,C,D,E,F) -> (E,A,B,C,D,F), no mirror, 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 == [('EABCDF', False)], f'maps found: {m}')
    T, P = table(TM), table(PARENT)
    claim('S2', 'this machine starts in A = sigma(B): it runs the parent\'s table from 0^inf B> 0^inf; the inverse '
          'map phi = sigma^-1 is A->B, B->C, C->D, D->E, E->A, F->F (the .v\'s phi)',
          SIGMA['B'] == 'A' and {v: k for k, v in SIGMA.items()} == dict(zip('ABCDEF', 'BCDEAF')))
    undef = [k for k, v in T.items() if v is None]; intoF = [k for k, v in T.items() if v and v[2] == 'F']
    claim('S2', 'the only undefined cell is F1 (the parent\'s F1, sigma fixes F); F is entered only by E1 = 0RF '
          '(sigma of the parent\'s A1 = 0RF)', undef == [('F', 1)] and intoF == [('E', 1)] and
          [k for k, v in P.items() if v and v[2] == 'F'] == [('A', 1)])
    ok, k = lockstep(2_000_000)
    claim('S2', 'lockstep: from the blank tape this machine and the parent\'s table from 0^inf B> 0^inf read the same '
          'symbol, write the same symbol and move the same way at every step, with state = sigma(parent state); '
          'the tapes are identical after 2,000,000 steps', 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('B'), 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 B have the same tape, head cell and direction, with state = sigma(parent state); neither halts',
          not ra.halted and not rp.halted and fa.tape == fp.tape and fa.lo == 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, st in ((TM, 'A'), (PARENT, 'A')):
        for N in (1, 7, 1000, 123457, 3000001, 30000017, 100000003):
            cases += 1
            rl = rlsim.RL(tm, st); rl.run_to(N)
            lo, cells, h = rl.cells()
            r = sim.run(sim.parse(tm), sim.Config.blank(st), max_steps=N); c = r.final
            a = min(lo, c.lo); b = max(lo + len(cells) - 1, c.hi)
            same = all((cells[x - lo] if 0 <= x - lo < len(cells) else 0) == c.read(x) for x in range(a, b + 1))
            good += same and 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, one move per alternating segment in a sweep cycle) agrees '
          'with tools/sim.py at 7 step counts from 1 to 100,000,003, for this machine and for the parent: whole '
          'tape, head cell, state', good == cases, f'{good}/{cases}')
    good = 0
    for tm in (TM, PARENT):
        rl = rlsim.RL(tm, 'A'); rl.run_to(2_000_000)
        good += rl.lam_log == lam_direct(tm, 2_000_000)
    claim('S2', 'rlsim\'s lam (the leftmost cell that has held 1) changes at exactly the steps and cells of direct '
          'simulation, first 2,000,000 steps, both machines', 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, exit_state, 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 == 28: st['runs'] = rl.runs()
        store[n] = st
    return cb


def get_runs():
    if RUNS: return RUNS
    inv = {v: k for k, v in SIGMA.items()}
    for tag, tm, start, exit_state, rename in (('512', TM, 'A', 'A', inv), ('341', PARENT, 'A', 'B', {q: q for q in 'ABCDEF'})):
        t0 = time.time(); store = {}
        rl, bursts, exits = rlsim.records(tm, start, exit_state, N_LAST, n_first=12,
                                          on_exit=snap_cb(store, exit_state, rename))
        RUNS[tag] = dict(bursts=bursts, exits=exits, snaps=store, secs=time.time() - t0, iters=rl.iters)
    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']), ('512', ['snap_512.pkl'])):
        out[tag] = {}
        for f in files:
            out[tag].update(pickle.load(open(os.path.join(R, f), 'rb')))
    return out


def s3():
    R = get_runs(); SN = load_parent_snaps()
    b = R['512']['bursts']
    small = [(x[0], x[1]) for x in b if x[2] != 3]; three = [x for x in b if x[2] == 3]
    claim('S3', 'this machine from blank (rlsim on its own table): lam moves left by 1 or 2 cells only at steps 1, 4-5, '
          '18-19, 930-931, 7984, 17719-17720; every other move is 3 cells in 3 consecutive steps; no halt',
          small == [(1, 1), (4, 5), (18, 19), (930, 931), (7984, 7984), (17719, 17720)] and
          all(x[1] - x[0] == 2 for x in three) and len(three) >= N_LAST,
          f'{len(small)} small moves, {len(three)} 3-cell moves')
    claim('S3', 'its 3-cell moves 1..16 are at steps 34, 75, 1042, 1265, 29525, 91614, 443229, 648082, 1213303, '
          '4665524, 6953169, 12290878, 43671313, 65535690, 114514475, 398094148 (each the first of three)',
          [x[0] for x in three[:16]] == [34, 75, 1042, 1265, 29525, 91614, 443229, 648082, 1213303, 4665524, 6953169,
                                        12290878, 43671313, 65535690, 114514475, 398094148])
    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 both runs number record n as their n-th '
          '3-cell move', 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))
    ex = R['512']['exits']; exp = R['341']['exits']
    ok = all(ex[n][0] == SN['512'][n]['steps'] and ex[n][1] == SN['512'][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 the n-th 3-cell move with the head '
          'in this machine\'s A = sigma(B) reading 1, moving right, 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['512']['secs']:.0f} s + {R['341']['secs']:.0f} s")
    claim('S3', 'record exit 16 at step 398,095,384 (head cell 1,156); record exit 28 at step 2,629,088,387,088 '
          '(head cell 111,896); the parent\'s record exit 28 is at step 2,629,088,227,408 (head cell 111,894)',
          ex[16] == (398095384, 1156) and ex[28] == (2629088387088, 111896) and exp[28] == (2629088227408, 111894))
    good = 0
    for n in range(12, N_LAST + 1):
        s = R['512']['snaps'][n]; t = SN['512'][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
    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',
          good == N_LAST - 11, f'{good}/{N_LAST - 11}')


# ------------------------------------------------------------------------------------------------- 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 []
            out = []
            for item in cell.split(', '):
                expr = re.sub(r'(\d+)u', r'\1*u', item.strip())
                out.append(expr)
            return out
        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)


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: block 1 is (digit, separator); then per block (inter gap to its digit, digit gap, sep gap, sep gap)
    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, gaps=gaps, roles=roles, right=rgaps, all=allg, bad=bad,
                         win=gaps[len(gaps) - J[r]:] if J[r] else [])


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 ('512', '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' if tag == '512' 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['512']['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['512']['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)',
          ok28 and i28['K'] == 7 and i28['win'] == [8277, 24912, 74808] and
          i28['right'] == [224493, 673559, 7, 9841, 1942040, 3])
    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['512']['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) == 1 and a[d[0]] - b[d[0]] == 4:
            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 one entry, 4 larger here; its index 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}, index at 12: '
          f'{idx.get(12)}')
    good = 0; where = {}
    for n in range(16, N_LAST + 1):
        oka, a = parse_C(R['512']['snaps'][n], n); okb, b = parse_C(R['341']['snaps'][n], n)
        diff = [i for i, (x, y) in enumerate(zip(a['all'], b['all'])) if x != y]
        same_len = len(a['all']) == len(b['all'])
        one = same_len and len(diff) == 1 and a['all'][diff[0]] - b['all'][diff[0]] == 4
        nleft = len(LEFT_WORD) + 1          # gaps lo -> first defect -> ... -> last left-word defect, then -> A+2
        ci = diff[0] - nleft if one else None   # index into the chain gap list
        deep = one and 0 <= ci < len(a['gaps']) - J[cls(n)]
        same_rest = a['win'] == b['win'] and a['right'] == b['right'] and a['K'] == b['K'] and a['A'] - b['A'] == -2 \
            and a['B'] - b['B'] == 2
        good += oka and okb and one and deep and same_rest
        if one: where[n] = (ci, a['roles'][ci], b['all'][diff[0]], a['all'][diff[0]])
    claim('S4', f'against the parent\'s own record exits 16..{N_LAST}: the same K, the same window and right region, '
          'every gap from lo to hi the same except exactly one deep chain gap (outside the window), 4 cells longer '
          'here; A is 2 cells further left and B 2 cells further right than in the parent', good == N_LAST - 15,
          f'{good}/{N_LAST - 15}')
    w28 = where.get(28)
    trav = all(where.get(n, (None,))[0] == where[16][0] + (n - 16) for n in range(16, N_LAST + 1)) if 16 in where else False
    claim('S4', 'that gap is one physical gap: its index in the chain grows by one per record (the new left digit); at '
          'record exit 16 it is the digit gap of block 2, at record exit 28 the digit gap of block 5: 17 here, 13 in '
          'the parent (both 1 mod 4 and >= 1, as (C) requires)',
          trav and where[16][:2] == (2, 'd') and w28 == (14, 'd', 13, 17), f'16: {where.get(16)}, 28: {w28}')


# ------------------------------------------------------------------------------------------------- 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, '512', 'A'), (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,088,387,088 (state A = 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 one run only, (S0, 17) here against (S0, 13), so the '
          'two nus28 differ only in block 3 (from the head): [10; 5; 4; 1] against [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 == [10] and Ls[10] == (0, 17) and Lp[10] == (0, 13) and ns[2] == [10, 5, 4, 1] and
          np_[2] == [10, 5, 3, 1] and ns[:2] == np_[:2] and ns[3:] == np_[3:] and ns[0] == [18701, 6227, 2069, 683],
          f'nus28 here: {ns}')
    # 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, inv_step and the invariant '
          '(everything before the base case), byte for byte with tm renamed tmP',
          same_body, f'{len(body)} lines')
    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]]
    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 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_tail, f'{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 tm tmP phi.' in ts and
           'Lemma init28 : B;; tape0 -->* ev_cfg [] (fun _ => const S0) cfg28.' in ts and
           'match q with A => B | B => C | C => D | D => E | E => A | F => F end.' in ts)
    claim('S5', 'the .v defines tm (this string) and tmP (the parent), init28 from B;; tape0, phi = sigma^-1, '
          'perm_phi : Perm tm tmP phi, and ends with Lemma nonhalt : ~ halts tm c0', 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]) == 18571902 and ts.count('native_compute') >= 38
    claim('S5', 'the base case is 38 pieces ck_0 .. ck_37 (runp 500000 each, the last runp 71902 to cfg28): '
          '18,571,902 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 'line 512' in l or '512' 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 512)', ok,
          f'exit {r.returncode}, {len(lines)} lines on 512')


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()
    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()