#!/usr/bin/env python3
"""check_proof.py for W4-1 = 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB (proof.md in this directory).

Every numbered claim of proof.md is checked here against W4-1's OWN transition table (parsed from the
string; nothing is copied from kill #30's table), by direct simulation: exhaustive small cases plus
random large ones.  Kill #30's .v is read (read-only) for the text of its statements.

Sections (proof.md section in brackets):
  S   [1]   table = sigma(#30's table), cell by cell; busycoq's Perm tm tm30 phi (phi = sigma^-1) on all
            12 cells; the blank run of W4-1 = sigma(#30's table run from 0^inf B> 0^inf), step for step;
            the halting pattern: two steps after 0 0 F> 1 the machine is in C reading 0, and (exhaustive
            over 5-cell windows) that is the only way to be there after two steps
  X   [8]   rename route, text facts: #30's .v sha256; {{A}} 23, {{C}} 28, {{E}} 8, nothing else; every
            occurrence is in a Lemma/Definition statement whose binders are not state names; LP has 18
            constructors and Phi 8; the one 'progress_nonhalt_cond tm' that route A must edit
  K   [8.3] the two compiled drafts: scripts/mk_routeA.py / mk_routeB.py applied to the sha-pinned #30 .v
            give (minus their one 'Print Assumptions' line) exactly the files whose check_kill PASS logs
            are data/check_kill_route{A,B}.log; text facts of each draft
  V   [3.2] the 27 Section-1 statements of #30's .v, parsed from the .v text, renamed by sigma, are exact
            W4-1 runs (every exponent assignment in 0..6, 4 contexts each, step formulas fitted and
            re-checked); control: the unrenamed text on #30's table
  W   [3.1] window rules W1-W11 and shift rules S1-S3 (W4-1 names), same machinery
  LP  [3.3] the computable local pass lpf (= the .v's LP constructors) against the TM: every word of an
            exhaustive small enumeration + random large words, random left contexts
  PH  [3.4] phif (Phi constructors: bounce, eats, D6 inside) against the TM: exhaustive small + random large;
            every small G word at b = 1 has an eat
  R   [3.5] restart Rst, k <= 60
  N   [7]   negative controls: eats at non-G words reach the halting cell C0 (= the pattern 0 B> 0)
  I   [6]   blank -->* K(1,3,t1) in 55 steps, milestones at steps 4, 11, 41, 42; tm30 from (B, blank)
            reaches #30's K(1,3,t1) in 55 steps; the full trace printed in proof.md 6.1 (parsed from
            proof.md) = the W4-1 run, line by line, transition labels included
  F   [6]   the finite part: orbit 100000 691 3 t1 = Some (17712, Y691); Inv 11 17712 Y691 component by
            component; no earlier epoch satisfies Inv for any k; k = 11 is the only k; fuel
  M   [6]   control: the same model code reproduces #30's fin694 literal (proved by vm_compute in #30's .v)
  O   [6]   model orbit = TM left records: stored C log to 1e11 (518 records) + a fresh Python run
  T   [5]   threshold facts N1, N2 for k < 200 and the bound table
  J   [5]   Inv carried along the orbit after epoch 691 with kappa' = max(kappa, k(W')), to 1,200 epochs
  C   [9]   W4-1's orbit and #30's orbit merge at epoch index 795 of both (N = 20922); not a premise
  D   [9]   #30's write-up Lemma D chain on W4-1's orbit (scripts/lemmaD_w41.py, run as a subprocess)
Usage: python3 -B check_proof.py [--seed S] [--quick]      (--quick: smaller random samples, no D)
"""
import sys, os, re, random, json, time, hashlib, itertools, subprocess
HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, os.path.join(HERE, 'scripts'))
import vmodel as V

TM = '1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB'
TM30 = '1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC'
P30 = '[local working file]' + TM30
V30 = os.path.join(P30, TM30 + '.v')
SHA30 = '93a493f5531185781ddecc40b40ad3e5cf0c325326b42aa1d2631802611d90c0'
LOG = os.path.join(HERE, 'data', 'lrec_1e11.txt')
SIGMA = {'A': 'E', 'B': 'A', 'C': 'B', 'D': 'C', 'E': 'D', 'F': 'F'}      # #30 name -> W4-1 name
PHI = {v: k for k, v in SIGMA.items()}                                     # W4-1 name -> #30 name
ST = 'ABCDEF'
SEED = int(sys.argv[sys.argv.index('--seed') + 1]) if '--seed' in sys.argv else 1
QUICK = '--quick' in sys.argv
random.seed(SEED)
RES = {}
INFO = {}


def rec(cid, ok, info=None):
    r = RES.setdefault(cid, {'n': 0, 'pass': 0, 'fail': []})
    r['n'] += 1; r['pass'] += bool(ok)
    if not ok and len(r['fail']) < 3: r['fail'].append(str(info)[:400])


def table(s):
    t = []
    for blk in s.split('_'):
        row = []
        for r in (0, 1):
            x = blk[3 * r:3 * r + 3]
            row.append(None if x == '---' else (int(x[0]), 1 if x[1] == 'R' else -1, ST.index(x[2])))
        t.append(row)
    return t


TT = table(TM)
TT30 = table(TM30)


# =====================================================================================
# S. the renaming
# =====================================================================================
def section_S():
    cells30 = {(ST[i], r): b[3 * r:3 * r + 3] for i, b in enumerate(TM30.split('_')) for r in (0, 1)}
    cells41 = {(ST[i], r): b[3 * r:3 * r + 3] for i, b in enumerate(TM.split('_')) for r in (0, 1)}
    for (q, r), c in cells30.items():
        want = c if c == '---' else c[:2] + SIGMA[c[2]]
        rec('S1   W4-1 cell (sigma q, r) = sigma(#30 cell (q, r)), 12 cells', cells41[(SIGMA[q], r)] == want, (q, r))
    # busycoq Permute.v: Perm tm tm' f := (tm (q,s) = None -> tm' (f q, s) = None) /\
    #   (tm (q,s) = Some (s',d,q') -> tm' (f q, s) = Some (s',d,f q')), here tm = W4-1, tm' = tm30, f = phi
    for q in ST:
        for s in (0, 1):
            a = TT[ST.index(q)][s]; b = TT30[ST.index(PHI[q])][s]
            ok = (b is None) if a is None else (b is not None and b[:2] == a[:2] and ST[b[2]] == PHI[ST[a[2]]])
            rec('S2   Perm tm tm30 phi (phi = sigma^-1: A->B, B->C, C->D, D->E, E->A, F->F), 12 cells', ok, (q, s))
    undef = [(ST[i], r) for i in range(6) for r in (0, 1) if TT[i][r] is None]
    rec('S3   the only undefined W4-1 cell is C0 (= #30 D0)', undef == [('C', 0)], undef)
    into_C = [(ST[i], r) for i in range(6) for r in (0, 1) if TT[i][r] and TT[i][r][2] == 2]
    rec('S4   C is entered only by B0 = 1LC (so halting <=> the pattern 0 B> 0 occurs)',
        into_C == [('B', 0)] and TT[1][0] == (1, -1, 2), into_C)
    into_B = [(ST[i], r) for i in range(6) for r in (0, 1) if TT[i][r] and TT[i][r][2] == 1]
    rec('S6   B is entered only by A0 = 1RB (a 1 left behind) and F1 = 0LB',
        into_B == [('A', 0), ('F', 1)] and TT[0][0] == (1, 1, 1) and TT[5][1] == (0, -1, 1), into_B)
    # S7 forward: from l 0 0 F> 1 r, F1 then B0 leave the machine in C reading 0, where no transition is
    # defined (busycoq: halted).  Two steps, not three: the undefined C0 is not a step.
    ctxs = [([0] * 6, [0] * 6), ([1] * 6, [1] * 6)] + [([random.randint(0, 1) for _ in range(6)],
                                                         [random.randint(0, 1) for _ in range(6)]) for _ in range(200)]
    for lb, rbs in ctxs:
        tape = lb + [0, 0, 1] + rbs; pos = len(lb) + 2; q = ST.index('F'); seen = []
        for _ in range(2):
            tr = TT[q][tape[pos]]
            if tr is None: break
            tape[pos] = tr[0]; pos += tr[1]; q = tr[2]; seen.append((ST[q], tape[pos]))
        rec('S7   from l 0 0 F> 1 r: after 1 step B reads 0, after 2 steps C reads 0 (undefined: halted), 202 contexts',
            seen == [('B', 0), ('C', 0)] and TT[q][tape[pos]] is None, (lb, rbs, seen))
    # S8 converse, exhaustive: every (state, 5-cell window, head in the middle) that is in C reading 0 after
    # exactly two steps (and not halted after one) is F reading 1 with 0 0 to its left; every one-step
    # predecessor of C reading 0 is B reading 0 with a 0 to its left
    two = []; one = []
    for q0 in range(6):
        for win in itertools.product((0, 1), repeat=5):
            tape = list(win); pos = 2; q = q0; path = []
            for _ in range(2):
                tr = TT[q][tape[pos]]
                if tr is None: break
                tape[pos] = tr[0]; pos += tr[1]; q = tr[2]; path.append((q, pos, tape[pos]))
            if len(path) >= 1 and path[0][0] == 2 and path[0][2] == 0: one.append((ST[q0], win))
            if len(path) == 2 and path[1][0] == 2 and path[1][2] == 0: two.append((ST[q0], win))
    rec('S8   exhaustive (6 states x 32 windows): in C reading 0 after exactly 2 steps <=> start F reading 1 with 0 0 to its left',
        len(two) == 4 and all(q == 'F' and w[0:3] == (0, 0, 1) for q, w in two), two)
    rec('S8   exhaustive: in C reading 0 after 1 step <=> start B reading 0 with a 0 to its left',
        len(one) == 8 and all(q == 'B' and w[1:3] == (0, 0) for q, w in one), one)
    # step-for-step: W4-1 from (A, blank) vs tm30 from (B, blank)
    n = 300000 if QUICK else 2000000
    t1 = bytearray(1 << 16); t2 = bytearray(1 << 16); p1 = p2 = 1 << 15; q1 = 0; q2 = 1; ok = True
    for st in range(n):
        a = TT[q1][t1[p1]]; b = TT30[q2][t2[p2]]
        if a is None or b is None or ST[q1] != SIGMA[ST[q2]]: ok = False; break
        t1[p1] = a[0]; p1 += a[1]; q1 = a[2]; t2[p2] = b[0]; p2 += b[1]; q2 = b[2]
        if p1 != p2 or not (100 < p1 < len(t1) - 100): ok = False; break
    ok = ok and t1 == t2 and ST[q1] == SIGMA[ST[q2]]
    rec('S5   W4-1 run from 0^inf A> 0^inf = sigma(tm30 run from 0^inf B> 0^inf): same tape, head, sigma-state, %d steps' % n, ok, st)


# =====================================================================================
# a tiny reader for busycoq tape statements  l <* <[..]^^x {{Q}}> [..] *> r  -->+  ...
# =====================================================================================
TOK = re.compile(r'\s*(-->\+|<\*|\*>|const 0|0inf|<\{\{([A-F])\}\}|\{\{([A-F])\}\}>|<\[([0-9;]+)\]|\[([0-9;]+)\]|\^\^(\([^()]*(?:\([^()]*(?:\([^()]*\))?[^()]*\))?[^()]*\)|[a-zA-Z]\w*)|\b([lr])\b)')


def ev_exp(s, env):
    s = s.strip()
    while s.startswith('(') and s.endswith(')'): s = s[1:-1].strip()
    if s.startswith('S '): return 1 + ev_exp(s[2:], env)
    if s.isdigit(): return int(s)
    return env[s]


def tokens(s):
    out = []; i = 0; s = s.strip()
    while i < len(s):
        m = TOK.match(s, i)
        if not m: raise ValueError('cannot parse at: ' + s[i:i + 40])
        g = m.group(1)
        if g.startswith('<{{'): out.append(('hl', m.group(2)))
        elif g.startswith('{{'): out.append(('hr', m.group(3)))
        elif g.startswith('<['): out.append(('rlist', [int(x) for x in m.group(4).split(';')]))
        elif g.startswith('['): out.append(('list', [int(x) for x in m.group(5).split(';')]))
        elif g.startswith('^^'): out.append(('pow', m.group(6)))
        else: out.append(('w', g))
        i = m.end()
    return out


def build(side_toks, env, lbits, rbits):
    """-> (cells dict index->sym (nonzero only), head index, state, l_lo, r_lo, base) with the l block ending at 0."""
    toks = list(side_toks)
    base = toks.pop(0)[1]
    assert base in ('l', 'const 0'), base
    left = []                                         # reading order, starting at index 0
    head = None; right = []; term = None
    i = 0
    while i < len(toks):
        t = toks[i]
        if t == ('w', '<*'):
            u = toks[i + 1]; rep = 1; j = i + 2
            if j < len(toks) and toks[j][0] == 'pow': rep = ev_exp(toks[j][1], env); j += 1
            unit = u[1] if u[0] == 'rlist' else list(reversed(u[1]))
            left += unit * rep; i = j; continue
        if t[0] in ('hl', 'hr'): head = t; i += 1; continue
        if t[0] == 'list':
            rep = 1; j = i + 1
            if j < len(toks) and toks[j][0] == 'pow': rep = ev_exp(toks[j][1], env); j += 1
            assert toks[j] == ('w', '*>'), toks[j:j + 2]
            right += t[1] * rep; i = j + 1; continue
        if t[0] == 'w' and t[1] in ('r', '0inf', 'const 0'): term = t[1]; i += 1; continue
        raise ValueError(t)
    cells = {}
    L = lbits if base == 'l' else []
    for k, b in enumerate(L): cells[k - len(L)] = b
    for k, b in enumerate(left): cells[k] = b
    if head[0] == 'hr':
        hpos = len(left)
        for k, b in enumerate(right): cells[hpos + k] = b
        r_lo = hpos + len(right)
    else:
        hpos = len(left) - 1
        for k, b in enumerate(right): cells[hpos + 1 + k] = b
        r_lo = hpos + 1 + len(right)
    if term == 'r':
        for k, b in enumerate(rbits): cells[r_lo + k] = b
    return {k: v for k, v in cells.items() if v}, hpos, head[1], base, r_lo, term


def run_stmt(tt, lhs, rhs, env, lbits, rbits, maxsteps=200000):
    c, h, q, base, r_lo, term = build(lhs, env, lbits, rbits)
    c2, h2, q2, _, r_lo2, _ = build(rhs, env, lbits, rbits)
    q = ST.index(q); q2 = ST.index(q2)
    # busycoq configurations are head-relative (left stream, head symbol, right stream): compare relative to the head
    rel2 = frozenset(i - h2 for i in c2)
    for st in range(1, maxsteps + 1):
        if base == 'l' and h < 0: return None, 'read l'
        if term == 'r' and h >= r_lo: return None, 'read r'
        tr = tt[q][c.get(h, 0)]
        if tr is None: return None, 'halt'
        if tr[0]: c[h] = 1
        else: c.pop(h, None)
        h += tr[1]; q = tr[2]
        if q == q2 and len(c) == len(rel2) and frozenset(i - h for i in c) == rel2: return st, 'ok'
    return None, 'max'


def parse_v_statements(text):
    """every 'Lemma NAME vars : LHS -->+ RHS.' of Section 1 (up to the first word definition)"""
    sec1 = text.split('Section 2.')[0]
    out = []
    for m in re.finditer(r'Lemma (\w+)((?: \w+)*) :(.*?)\.\s*\nProof\.', sec1, re.S):
        body = ' '.join(m.group(3).split())
        if '-->+' not in body: continue
        lhs, rhs = body.split('-->+')
        out.append((m.group(1), m.group(2).split(), lhs.strip(), rhs.strip()))
    return out


def rename(s, mp): return re.sub(r'\{\{([A-F])\}\}', lambda m: '{{' + mp[m.group(1)] + '}}', s)


def fit_steps(name, varnames, samples):
    """steps linear in the exponent variables?  fit from the zero and unit samples, check every sample"""
    vs = [v for v in varnames if v not in ('l', 'r')]
    z = samples.get(tuple(0 for _ in vs))
    coef = []
    for i in range(len(vs)):
        u = tuple(1 if j == i else 0 for j in range(len(vs)))
        coef.append(samples[u] - z)
    ok = all(st == z + sum(c * x for c, x in zip(coef, key)) for key, st in samples.items())
    form = ' + '.join(['%d%s' % (c, v) if c != 1 else v for c, v in zip(coef, vs) if c] + ([str(z)] if z else [])) or '0'
    return ok, form


def check_statements(tag, tt, stmts, maxv=6, nctx=2):
    forms = {}
    for name, binders, lhs, rhs in stmts:
        vs = [v for v in binders if v not in ('l', 'r')]
        lt, rt = tokens(lhs), tokens(rhs)
        samples = {}
        allok = True
        for vals in itertools.product(range(maxv + 1), repeat=len(vs)):
            env = dict(zip(vs, vals))
            ctxs = [([0] * 6, [0] * 6), ([1] * 6, [1] * 6)] + [([random.randint(0, 1) for _ in range(7)],
                                                                 [random.randint(0, 1) for _ in range(7)]) for _ in range(nctx)]
            sts = set()
            for lb, rb in ctxs:
                st, why = run_stmt(tt, lt, rt, env, lb, rb)
                rec('%s %s' % (tag, name), st is not None, (env, why, lb, rb))
                sts.add(st); allok &= st is not None
            if len(sts) == 1 and None not in sts: samples[vals] = sts.pop()
            else: allok = False
        if allok:
            ok, form = fit_steps(name, binders, samples)
            rec('%s step formula linear in the exponents (fit on 0/unit values, checked on all)' % tag, ok, name)
            forms[name] = form
    return forms


def section_XV():
    text = open(V30).read()
    rec('X1   #30 .v sha256 = 93a493f5...0c0 (the check_kill PASS file)', hashlib.sha256(text.encode()).hexdigest() == SHA30)
    cnt = {s: len(re.findall(r'\{\{%s\}\}' % s, text)) for s in ST}
    rec('X2   #30 .v state notations: {{A}} 23, {{C}} 28, {{E}} 8, no {{B}} {{D}} {{F}}', cnt == {'A': 23, 'B': 0, 'C': 28, 'D': 0, 'E': 8, 'F': 0}, cnt)
    # every occurrence is inside a Lemma/Definition statement: walking back from the line, the nearest
    # line that opens a statement or a proof must open a Lemma/Definition (never 'Proof.')
    lines = text.split('\n'); bad = []; owner = {}
    for i, ln in enumerate(lines):
        if '{{' not in ln: continue
        j = i
        while j >= 0 and not re.match(r'\s*(Lemma|Definition|Theorem|Proof\.)', lines[j]) and 'Qed.' not in lines[j]: j -= 1
        m = re.match(r'\s*(Lemma|Definition) (\w+)', lines[j]) if j >= 0 else None
        if not m: bad.append(i + 1)
        else: owner[i + 1] = m.group(2)
    rec('X3   every {{q}} occurrence of #30 .v sits in a Lemma/Definition statement, none in a proof script', bad == [], bad)
    users = sorted(set(owner.values()))
    INFO['X_statements_using_states'] = users
    hit = []
    for name in users:
        m = re.search(r'(?:Lemma|Definition) %s\b(.*?)(?<![<{])\s:(?!=)' % name, text, re.S)
        hdr = m.group(1) if m else ''
        # binder names: identifiers in the header, minus type names and the ':' annotations
        names = re.findall(r"[A-Za-z_][\w']*", re.sub(r':\s*[A-Za-z_]\w*', ' ', hdr))
        if any(x in ST for x in names): hit.append((name, names))
    rec('X4   no statement that uses {{q}} binds a variable named A-F (no capture after renaming)', hit == [], hit)
    rn = rename(text, SIGMA)
    cnt2 = {s: len(re.findall(r'\{\{%s\}\}' % s, rn)) for s in ST}
    rec('X5   after the simultaneous rename A->E, C->B, E->D: {{E}} 23, {{B}} 28, {{D}} 8', cnt2 == {'A': 0, 'B': 28, 'C': 0, 'D': 8, 'E': 23, 'F': 0}, cnt2)
    mlp = re.search(r'Inductive LP : [^\n]*:=\n(.*?)\nwith Phi', text, re.S)
    mph = re.search(r'\nwith Phi : [^\n]*:=\n(.*?)\.\n', text, re.S)
    lpc = re.findall(r'^\| (LP_\w+)', mlp.group(1), re.M) if mlp else []
    phc = re.findall(r'^\| (Phi_\w+)', mph.group(1), re.M) if mph else []
    rec('X6   #30 .v: Inductive LP has 18 constructors, Phi has 8 (proof.md 3.3, 3.4)', len(lpc) == 18 and len(phc) == 8, (lpc, phc))
    INFO['X_constructors'] = {'LP': lpc, 'Phi': phc}
    rec("X7   #30 .v: nonhalt_from calls 'progress_nonhalt_cond tm (nat * word)' once (route A edits it to tm30)",
        text.count('progress_nonhalt_cond tm (nat * word)') == 1 and text.count('progress_nonhalt_cond') == 1)
    stmts = parse_v_statements(text)
    INFO['V_statements'] = [s[0] for s in stmts]
    rec('V0   Section 1 of #30 .v has 27 tape statements (-->+)', len(stmts) == 27, [s[0] for s in stmts])
    mv = 4 if QUICK else 6
    f30 = check_statements('V30  control: #30 .v statement on #30 table:', TT30, stmts, mv, 1)
    stmts41 = [(n, b, rename(l, SIGMA), rename(r, SIGMA)) for n, b, l, r in stmts]
    f41 = check_statements('V41  renamed #30 .v statement on W4-1 table:', TT, stmts41, mv, 2)
    rec('V2   step formulas identical on both tables', f30 == f41, (f30, f41))
    INFO['V_step_formulas'] = f41
    INFO['V_renamed_statements'] = {n: l + '  -->+  ' + r for n, b, l, r in stmts41}


# =====================================================================================
# K. the two compiled drafts (proof.md 8.3); check_kill itself is not re-run here
# =====================================================================================
SHA_A = 'fe7819692bfff1a95ee35273aa8bea11e13d877648cb16ac29a0a317b7e18e15'
SHA_B = 'c81ad0aebf0d452e7fa740c8fbf5086ed98be6905c3685e452a5215a96a5372f'
PA = 'Print Assumptions nonhalt.\n'


def ck_json(path):
    for ln in open(path):
        if ln.startswith('JSON: '): return json.loads(ln[6:])
    return None


def section_K():
    import tempfile
    with tempfile.TemporaryDirectory() as td:
        fa, fb = os.path.join(td, 'A.v'), os.path.join(td, 'B.v')
        pa = subprocess.run([sys.executable, '-B', os.path.join(HERE, 'scripts', 'mk_routeA.py'), V30, fa], capture_output=True, text=True)
        pb = subprocess.run([sys.executable, '-B', os.path.join(HERE, 'scripts', 'mk_routeB.py'), V30, fa, fb], capture_output=True, text=True)
        ok = pa.returncode == 0 and pb.returncode == 0
        rec('K0   scripts/mk_routeA.py and mk_routeB.py run on the sha-pinned #30 .v; route B renames 59 tokens',
            ok and pb.stdout.strip() == 'renamed tokens 59', (pa.stderr[-300:], pb.stderr[-300:], pb.stdout))
        if not ok: return
        raw = {'A': open(fa).read(), 'B': open(fb).read()}
    txt = {}
    for r, sha in (('A', SHA_A), ('B', SHA_B)):
        rec('K1   route %s: generator output has exactly one %r line' % (r, PA.strip()), raw[r].count(PA) == 1, raw[r].count(PA))
        txt[r] = raw[r].replace(PA, '', 1)
        h = hashlib.sha256(txt[r].encode()).hexdigest()
        rec('K1   route %s: generator output minus that line has sha256 %s... (the file check_kill passed)' % (r, sha[:8]), h == sha, h)
        j = ck_json(os.path.join(HERE, 'data', 'check_kill_route%s.log' % r))
        ok = (j is not None and j.get('result') == 'PASS' and j.get('exit') == 0 and j.get('sha256') == sha and j.get('tm') == TM
              and j.get('theorem') == 'nonhalt' and j.get('assumptions') == [] and j.get('coqchk') == 'pass'
              and j.get('framework_head', '').startswith('0940bb9') and all(c['status'] == 'PASS' for c in j.get('checks', [])))
        rec('K2   route %s: data/check_kill_route%s.log is a PASS for that sha256 (all checks PASS, 0 assumptions, coqchk pass, framework 0940bb9)' % (r, r), ok, j and j.get('result'))
        warn = [w for c in (j or {}).get('checks', []) if c['id'] == 'tm_text' for w in c['warnings']]
        want = 1 if r == 'A' else 0
        rec('K3   route %s: check_kill tm_text warnings = %d (route A: the second TM_from_str literal)' % (r, want),
            len(warn) == want and all('another TM_from_str literal' in w for w in warn), warn)
        INFO['K_route%s' % r] = {'sha256': sha, 'compile_s': j and j.get('compile_seconds'), 'coqchk_s': j and j.get('coqchk_seconds'),
                                 'tm_text_warnings': warn, 'lines': txt[r].count('\n')}
    a, b = txt['A'], txt['B']
    rec('K4   route A: two TM_from_str literals, tm30 bound in the three notations, init from B;; tape0, the tm30 edit in nonhalt_from, the Perm bridge',
        a.count('TM_from_str "') == 2 and a.count('-[ tm30 ]->') == 3 and 'Lemma init : B;; tape0 -->* K 3 t1.' in a
        and a.count('progress_nonhalt_cond tm30 (nat * word)') == 1 and 'progress_nonhalt_cond tm (' not in a
        and 'Lemma perm_w41 : Perm tm tm30 phi.' in a and 'perm_halts _ _ _ _ _ perm_w41 H' in a)
    cnt = {s: len(re.findall(r'\{\{%s\}\}' % s, b)) for s in ST}
    rec('K5   route B: one TM_from_str literal (W4-1), {{E}} 23, {{B}} 28, {{D}} 8, init c0 -->* K 3 t1, nonhalt as in #30',
        b.count('TM_from_str "') == 1 and 'TM_from_str "%s"' % TM in b and cnt == {'A': 0, 'B': 28, 'C': 0, 'D': 8, 'E': 23, 'F': 0}
        and 'Lemma init : c0 -->* K 3 t1.' in b and 'Perm' not in b and 'apply (nonhalt_from 17712 Y691' in b, cnt)
    for r, t in (('A', a), ('B', b)):
        rec('K6   route %s: fin691, inv691 and the exists 11 step are the finite part of proof.md 6.2-6.3' % r,
            'Lemma fin691 : orbit 100000 691 3 t1 = Some (17712, Y691).' in t and 'Lemma inv691 : Inv 11 17712 Y691.' in t
            and 'exists 11. exact inv691.' in t and 'Definition Y691 : word := p11 10 (gw B691 0).' in t)
        # not a defect of the proof, a to-do for the formalization stage (proof.md 8.3)
        rec('K7   route %s: (to-do) still opens with #30\'s header comment and closes with #30\'s table comment' % r,
            t.startswith('(* %s never halts.' % TM30) and t.rstrip().endswith(' start      c0 -->* K(1,8,010001)\n*)'))


# =====================================================================================
# W. window and shift rules (proof.md 3.1), W4-1 names, written in the same notation
# =====================================================================================
WRULES = [
    ('W1', 'l r', 'l <* [1] {{F}}> [1] *> r', 'l <* <[1;1] {{F}}> r'),
    ('W2', 'l r', 'l {{F}}> [0;0;1] *> r', 'l <* <[0;1;1] {{F}}> r'),
    ('W3', 'l r', 'l {{F}}> [0;0;0] *> r', 'l <* <[0;1;1] {{B}}> r'),
    ('W4', 'l r', 'l {{B}}> [1;0;1] *> r', 'l <* <[1;1;1] {{F}}> r'),
    ('W5', 'l r', 'l <* <[0;1;1] {{D}}> [0] *> r', 'l {{D}}> [0;0;1;0] *> r'),
    ('W6', 'l r', 'l <* [0] {{D}}> [0] *> r', 'l <* <[1;1] {{F}}> r'),
    ('W7', 'l r', 'l {{F}}> [0;1] *> r', 'l <* <[0;0] {{F}}> r'),
    ('W8', 'l r', 'l <* <[0;1;1] <{{E}} [1;0;0] *> r', 'l {{D}}> [0;0;1;0;0;0] *> r'),
    ('W9', 'l r', 'l <* <[0;1;1] <{{E}} [1;0;1] *> r', 'l {{D}}> [0;0;1;0;0;1] *> r'),
    ('W10', 'l r', 'l <* <[0;1;1;1] <{{D}} r', 'l <{{E}} [1;0;0;0] *> r'),
    ('W11', 'l r', 'l {{B}}> [1;0] *> r', 'l <* <[1;1] {{F}}> r'),
    ('S1(n+1)', 'l n r', 'l <* <[0;1;1]^^(S n) {{D}}> [0] *> r', 'l {{D}}> [0] *> [0;1;0]^^(S n) *> r'),
    ('S2(n+1)', 'l n r', 'l {{F}}> [0;0;1]^^(S n) *> r', 'l <* <[0;1;1]^^(S n) {{F}}> r'),
    ('S3(n+1)', 'l n r', 'l <* [1] {{F}}> [1]^^(S n) *> r', 'l <* [1] <* <[1]^^(S n) {{F}}> r'),
]
WSTEPS = {'W1': '5', 'W2': '3', 'W3': '3', 'W4': '9', 'W5': '5', 'W6': '3', 'W7': '2', 'W8': '4', 'W9': '4', 'W10': '4',
          'W11': '4', 'S1(n+1)': '5n + 5', 'S2(n+1)': '3n + 3', 'S3(n+1)': '5n + 5'}


def section_W():
    st = [(n, b.split(), l, r) for n, b, l, r in WRULES]
    forms = check_statements('W    W4-1 window/shift rule:', TT, st, 13, 2)
    for n in WSTEPS:
        rec('W    step count as stated in proof.md 3.1', forms.get(n) == WSTEPS[n], (n, forms.get(n)))
    INFO['W_step_formulas'] = forms


# =====================================================================================
# TM runs for words (LP, Phi, Rst)
# =====================================================================================
def bits(s): return [int(c) for c in s]
def rb(n): return ''.join(random.choice('01') for _ in range(n))
def norm(s): return s.rstrip('0')
def tstr(t, i): return norm(''.join(map(str, t[i:])))


def run_until_left(tt, cells, head, q, left_stop, maxsteps=5 * 10**7):
    tape = bytearray(cells) + bytearray(4096)
    pos = head; st = 0
    while st < maxsteps:
        if pos == left_stop: return (ST[q], tape, st)
        if pos >= len(tape) - 8: tape += bytearray(len(tape))
        tr = tt[q][tape[pos]]
        if tr is None: return ('HALT', tape, st)
        w, d, q = tr; tape[pos] = w; pos += d; st += 1
        if pos < left_stop: return ('PASSED', tape, st)
    return ('MAX', tape, st)


def lp_tm(w, w2, d, junk):
    s = junk + '011' + V.enc(w)
    st, tape, steps = run_until_left(TT, bits(s), len(junk) + 3, ST.index('B'), len(junk) - 1)
    want = ('101000' if d else '100') + V.enc(w2)
    return st == 'E' and tstr(tape, len(junk)) == norm(want) and ''.join(map(str, tape[:len(junk)])) == junk, (st, steps)


def phi_tm(a, b, w, k, y, junk):
    s = junk + '110' * a + '0' + '011' * b + V.enc(w)
    st, tape, steps = run_until_left(TT, bits(s), len(junk) + 3 * a + 1 + 3 * b, ST.index('B'), len(junk) - 1)
    want = '01' + '001' * k + '000' + V.enc(y)
    return st == 'D' and tstr(tape, len(junk)) == norm(want) and ''.join(map(str, tape[:len(junk)])) == junk, (st, steps)


def lp_case(w):
    k = w[0]
    if k == 't': return 'LP_t%d' % w[1]
    if k == 'blk': return 'LP_b (carry)' if w[1] else 'LP_a (toggle)'
    if k == 'p11': return 'LP_11S' if w[1] > 0 else 'LP_110'
    if k == 'p01': return 'LP_01'
    if k == 'p00': return 'LP_00'
    v = w[1]
    if v[0] == 'blk': return 'LP_6 (D6, nested sub-epoch)' if v[1] else 'LP_5'
    return 'LP_T* / normalized end word'


def phi_case(b, w):
    if b >= 2: return 'Phi_B (bounce)'
    k = w[0]
    if k == 'blk': return 'Phi_E2 (b-block eat)' if w[1] else 'Phi_E1 (a-block eat)'
    if k == 't': return ['Phi_E0', 'Phi_Et1', 'Phi_Et2', 'Phi_Et3'][w[1]]
    return 'Phi eat at a normalized word (Phi_eq)'


def small_words(depth, emax=2):
    """all words with at most `depth` non-tail constructors, exponents <= emax"""
    if depth == 0: return [('t', s) for s in range(4)]
    sub = small_words(depth - 1, emax)
    out = list(sub)
    for w in sub:
        for e in range(emax + 1):
            out += [('blk', False, e, w), ('blk', True, e, w), ('p11', e, w), ('p01', e, w)]
        out += [('p00', w), ('p10', w)]
    seen = set(); res = []
    for w in out:
        if w not in seen: seen.add(w); res.append(w)
    return res


def G_words(maxk, emax):
    out = []
    for k in range(maxk + 1):
        for ds in itertools.product([False, True], repeat=k):
            for es in itertools.product(range(emax + 1), repeat=k):
                for s in range(4):
                    w = ('t', s)
                    for d, e in reversed(list(zip(ds, es))): w = ('blk', d, e, w)
                    out.append(w)
    return out


def rG(maxk=6, maxe=4):
    w = ('t', random.randrange(4))
    for _ in range(random.randrange(maxk + 1)):
        w = ('blk', random.random() < 0.5, random.randrange(maxe + 1), w)
    return w


def rO2():
    W = rG(4, 3); x = random.randrange(6)
    return random.choice([('p11', x, W), ('p01', x, W), ('p00', W), ('p10', W)])


def rH():
    w = rO2()
    for _ in range(random.randrange(4)): w = ('blk', random.random() < 0.5, random.randrange(4), w)
    return w


CONSTS = [('p10', V.T0), ('p10', V.T1), ('p10', V.T2), ('p10', V.T3), ('p10', ('p00', V.T0)), ('p10', ('p00', V.T1)),
          ('p10', ('p00', V.T2)), ('p10', ('p01', 0, V.T2)), ('p10', ('p01', 1, V.T1)), ('p10', ('p10', ('p00', V.T2))),
          V.T0, V.T1, V.T2, V.T3]


def rword(big=False):
    E = 40 if big else 8
    rr = lambda: rG(9 if big else 6, E if big else 5) if random.random() < 0.5 else rH()
    c = random.randrange(11)
    if c == 0: return ('t', random.randrange(4))
    if c == 1: return ('blk', False, random.randrange(E), rr())
    if c == 2: return ('blk', True, random.randrange(E), rr())
    if c == 3: return ('p11', random.randint(1, E), rG(6, 4))
    if c == 4: return ('p11', 0, rG(6, 4))
    if c == 5: return ('p01', random.randrange(E), rG(6, 4))
    if c == 6: return ('p00', rG(6, 4) if random.random() < 0.6 else rO2())
    if c == 7: return ('p10', ('blk', False, random.randrange(E), rr()))
    if c == 8: return ('p10', ('blk', True, random.randrange(E), rG(6, 3)))
    if c == 9: return random.choice(CONSTS)
    return rH()


def section_LP():
    ws = small_words(2, 2) if QUICK else sorted(set(small_words(2, 2)) | set(small_words(3, 1)), key=repr)
    n_some = 0
    for w in ws:
        r = V.lpf(100000, w)
        if r is None: continue
        n_some += 1
        for junk in ('0000000', '1111111', rb(7)):
            ok, info = lp_tm(w, r[0], r[1], junk)
            rec('LP   exhaustive small (depth <= 2, exponents <= 2): ' + lp_case(w), ok, (V.enc(w), info))
    INFO['LP_small_words'] = {'enumerated': len(ws), 'with_lpf_Some': n_some}
    n = 300 if QUICK else 1500
    done = 0
    while done < n:
        w = rword(big=random.random() < 0.4)
        r = V.lpf(100000, w)
        if r is None: continue
        ok, info = lp_tm(w, r[0], r[1], rb(7))
        rec('LP   random large: ' + lp_case(w), ok, (V.enc(w)[:80], info)); done += 1


def section_PH():
    ws = small_words(1, 2) if QUICK else sorted(set(small_words(1, 3)) | set(small_words(2, 1)), key=repr)
    INFO['PH_small_words'] = len(ws)
    for a in (0, 1, 2):
        for b in range(1, 6):
            for w in ws:
                r = V.phif(100000, a, b, w)
                if r is None: continue
                ok, info = phi_tm(a, b, w, r[0], r[1], rb(7))
                rec('PH   exhaustive small (a <= 2, b <= 5, depth <= 1): ' + phi_case(b, w), ok, (a, b, V.enc(w), info))
    # every G word at b = 1 has an eat (phif Some), small exhaustive
    for w in G_words(3, 2):
        for a in (0, 1, 3):
            r = V.phif(100000, a, 1, w)
            rec('PH   every G word (k <= 3, e <= 2, all tails) at b = 1 has an eat rule (phif Some)', r is not None, V.enc(w))
            if r is not None:
                ok, info = phi_tm(a, 1, w, r[0], r[1], rb(7))
                rec('PH   ... and it is the TM run: ' + phi_case(1, w), ok, (a, V.enc(w), info))
    n = 200 if QUICK else 700
    for eats in (False, True):
        done = 0
        while done < n:
            w = rword(big=random.random() < 0.3) if random.random() < 0.6 else rG(8, 6)
            a = random.randint(0, 40); b = 1 if eats else random.randint(1, 45)
            r = V.phif(100000, a, b, w)
            if r is None: continue
            ok, info = phi_tm(a, b, w, r[0], r[1], rb(7))
            rec('PH   random large (a <= 40, b <= 45): ' + phi_case(b, w), ok, (a, b, V.enc(w)[:60], info)); done += 1


def rst_tm(k, y, junk_right=''):
    pad = 12
    s = '0' * pad + '01' + '001' * k + '000' + V.enc(y)
    tape = bytearray(bits(s)) + bytearray(4096); pos = pad - 1; q = ST.index('D'); st = 0
    want = '0' * (pad - 2) + '110' + '0' + '011' * (k + 1)
    while st < 10 * k + 100:
        tr = TT[q][tape[pos]]
        if tr is None: return False, st
        w, d, q = tr; tape[pos] = w; pos += d; st += 1
        if ST[q] == 'B' and d == 1 and pos == len(want):
            return ''.join(map(str, tape[:pos])) == want and tstr(tape, pos) == norm(V.enc(y)), st
    return False, st


def section_R():
    stepsok = True
    for k in range(0, 61):
        ys = [V.T0, V.T1, V.T2, V.T3, rword(), rword(True)]
        for y in ys:
            ok, st = rst_tm(k, y)
            rec('R    Rst: 0^inf <D 01 (001)^k 000 y -->+ K(1,k+1,y), k <= 60', ok, (k, V.enc(y)[:40]))
            stepsok &= (st == 3 * k + 8)
    rec('R    Rst takes 3k + 8 steps (1 to the left record L, then 3k + 7)', stepsok)


# =====================================================================================
# N. negative controls: non-G eats halt
# =====================================================================================
def section_N():
    for word, name in (('11000110001', "'11' z t3"), ('00110001', "'00' t3")):
        for a in (1, 2, 5):
            s = '0' * 8 + '110' * a + '0' + '011' + word
            st, tape, steps = run_until_left(TT, bits(s), 8 + 3 * a + 1 + 3, ST.index('B'), 0, 10**6)
            rec('N    K(a, 1, %s) halts (C reads 0) before reaching a pre-record, a in {1,2,5}' % name, st == 'HALT', (a, st, steps))


# =====================================================================================
# I. initial segment
# =====================================================================================
def run_blank(tt, q0, nsteps, watch):
    tape = bytearray(400); pos = 200; q = q0; hits = {}
    for st in range(nsteps + 1):
        for name, fn in watch.items():
            if name not in hits and fn(tape, pos, q): hits[name] = st
        if st == nsteps: break
        tr = tt[q][tape[pos]]
        if tr is None: return hits, 'HALT'
        w, d, q = tr; tape[pos] = w; pos += d
    return hits, (tape, pos, q)


def is_conf(left, q, right):
    """config 0^inf left q> right 0^inf exactly (the head reads right[0]; right may be '' = a blank)"""
    def f(tape, pos, qq):
        if ST[qq] != q: return False
        s = ''.join(map(str, tape)); L = s[:pos]; R = s[pos:]
        return L.endswith(left) and set(L[:len(L) - len(left)]) <= {'0'} and R.startswith(right) and set(R[len(right):]) <= {'0'}
    return f


def section_I():
    W = {
        'L(0, empty) = 0^inf <E 101 0^inf': is_conf('', 'E', '0101'),
        'K(1,1,t0) = 0^inf 110 0 011 B> 0^inf': is_conf('1100011', 'B', ''),
        'pre-record 0^inf <D 01 (001)^2 000 1': is_conf('', 'D', '0' + '01' + '001' * 2 + '000' + '1'),
        'L(2, 0001) = 0^inf <E 101 (001)^2 0001': is_conf('', 'E', '0' + '101' + '001' * 2 + '0001'),
        'K(1,3,t1) = 0^inf 110 0 (011)^3 B> 1 0^inf': is_conf('110' + '0' + '011' * 3, 'B', '1'),
    }
    hits, _ = run_blank(TT, 0, 60, W)
    want = {'L(0, empty) = 0^inf <E 101 0^inf': 4, 'K(1,1,t0) = 0^inf 110 0 011 B> 0^inf': 11,
            'pre-record 0^inf <D 01 (001)^2 000 1': 41, 'L(2, 0001) = 0^inf <E 101 (001)^2 0001': 42,
            'K(1,3,t1) = 0^inf 110 0 (011)^3 B> 1 0^inf': 55}
    for k, v in want.items():
        rec('I    W4-1 from blank: first time at step %d: %s' % (v, k), hits.get(k) == v, hits.get(k))
    INFO['I_milestones'] = hits
    # the same from the .v text: Definition K, renamed, with N = 3, y = t1 (enc t1 = [1] *> const 0)
    text = open(V30).read()
    m = re.search(r'Definition K \(N : nat\) \(y : word\) : Q \* tape :=\s*(.*?)\.\n', text, re.S)
    kbody = ' '.join(m.group(1).split()).replace('enc y', '[1] *> 0inf')
    for tag, tt, body, q0, want in (('W4-1: c0 -->* K 3 t1 (renamed K)', TT, rename(kbody, SIGMA), 'A', 55),
                                     ('tm30: B;; tape0 -->* K 3 t1 (#30 K)', TT30, kbody, 'B', 55)):
        st, why = run_stmt(tt, tokens('const 0 {{%s}}> 0inf' % q0), tokens(body), {'N': 3}, [], [])
        rec('I    from the .v text, ' + tag + ', first at step 55', st == want, (st, why, body))
    INFO['I_K_text'] = kbody
    # tm30 from (B, blank): #30's K(1,3,t1) has C> instead of B>
    W30 = {'K30': is_conf('110' + '0' + '011' * 3, 'C', '1')}
    h30, _ = run_blank(TT30, 1, 60, W30)
    rec('I    tm30 from 0^inf B> 0^inf: #30 K 3 t1 (= 0^inf 110 0 (011)^3 C> 1) first at step 55', h30.get('K30') == 55, h30)
    # the model reproduces the start: phif 1 1 t0 = (2, t1)
    rec('I    model: phif _ 1 1 t0 = Some (2, t1) (the epoch from K(1,1,t0) is Phi_E0)', V.phif(100000, 1, 1, V.T0) == (2, V.T1))
    # the full trace printed in proof.md 6.1, parsed from proof.md, against the run
    rows = trace_from_proof()
    rec('I    proof.md 6.1 trace: 56 parsable lines, steps 0..55 in order', [r and r[0] for r in rows] == list(range(56)), len(rows))
    cells = {(ST[i], r): b[3 * r:3 * r + 3] for i, b in enumerate(TM.split('_')) for r in (0, 1)}
    tape = bytearray(400); pos = 200; q = 0
    for st in range(56):
        s = ''.join(map(str, tape)); nz = [i for i, c in enumerate(s) if c == '1']
        lo = min(nz) if nz else pos; hi = max(nz) + 1 if nz else pos + 1
        left = s[lo:pos] if lo < pos else ''; right = s[pos:max(hi, pos + 1)]
        row = rows[st] if st < len(rows) else None
        lab_ok = True
        if row and st < 55:
            lab_ok = row[4] is not None and row[4][:2] == (ST[q], tape[pos]) and row[4][2] == cells[(ST[q], tape[pos])]
        if row and st == 55: lab_ok = row[4] is None
        rec('I    proof.md 6.1 trace line = the W4-1 run from blank (left, state, head and right, transition label), 56 lines',
            row is not None and row[1:4] == (left, ST[q], right) and lab_ok, (st, row, (left, ST[q], right)))
        if st < 55:
            tr = TT[q][tape[pos]]; tape[pos] = tr[0]; pos += tr[1]; q = tr[2]


def trace_from_proof():
    text = open(os.path.join(HERE, 'proof.md')).read()
    blk = text.split('The full trace:', 1)[1].split('```', 2)[1]
    rows = []
    for ln in blk.strip('\n').split('\n'):
        m = re.match(r'^\s*(\d+)\s+(?:([01]+)\s+)?([A-F])>\s+([01]+)(?:\s+([A-F])([01]) = ([01][LR][A-F]))?\s*$', ln)
        rows.append(m and (int(m.group(1)), m.group(2) or '', m.group(3), m.group(4),
                           (m.group(5), int(m.group(6)), m.group(7)) if m.group(5) else None))
    return rows


# =====================================================================================
# F / M. the finite part
# =====================================================================================
Y691 = ('p11', 10, None)
B691 = [(False, 10), (False, 6), (True, 1), (False, 1), (True, 1), (False, 1), (True, 1), (False, 1), (False, 1), (True, 1), (False, 0)]
B694 = [(False, 17), (True, 1), (True, 1), (True, 1), (True, 1), (False, 1), (False, 1), (False, 1), (True, 1), (False, 0)]


def gw(bs, s):
    w = ('t', s)
    for d, e in reversed(bs): w = ('blk', d, e, w)
    return w


def inv_parts(k, N, y):
    g = V.as_gw(y[2]) if y[0] == 'p11' else None
    bs, s = g
    ex = [e for _, e in bs]
    Mw = sum(V.wq(i) * e for i, e in enumerate(ex)); M2 = sum(V.p2(i) * e for i, e in enumerate(ex))
    return {'N': N, 'Nstar': V.NSTAR, 'Nlo(k)': V.Nlo(k), 'k(W)': len(bs), 's': s, 'Mw': Mw, 'Af(k)': V.Af(k),
            'M2': M2, 'Bf(k)': V.Bf(k), 'x': y[1], 'Xf(k)': V.Xf(k), 'value m(W)': gval(bs, s)}


def gval(bs, s):
    v = 4 + s
    for d, _ in reversed(bs): v = (1 if d else 0) + 2 * v
    return v


def section_F():
    y691 = ('p11', 10, gw(B691, 0))
    V.STATS['min_fuel_left'] = None
    Ns = []; first = []
    def cb(t, N, y):
        Ns.append(N)
        if not first and V.inv_ks(N, y): first.append((t, N, y, V.inv_ks(N, y)))
    res, t = V.orbit(3, V.T1, 691, 100000, cb)
    rec('F1   orbit 100000 691 3 t1 = Some (17712, Y691), Y691 = p11 10 (gw B691 0)', res == (17712, y691), (res and res[0], t))
    minfuel = V.STATS['min_fuel_left']
    rec('F2   fuel 100000 is never exhausted (min fuel left over the 691 epochs >= 1)', minfuel is not None and minfuel >= 1, minfuel)
    INFO['F_min_fuel_left_691'] = minfuel
    INFO['F_N_first_20'] = Ns[:20]
    INFO['F_N_every_100'] = {i: Ns[i] for i in range(0, 691, 100)}
    # the model's epochs: Inv first holds at index 691 (after 691 epochs)
    rec('F3   no epoch before index 691 satisfies Inv k for any k <= 40; index 691 does', len(first) == 0, first[:1] and first[0][:2])
    ks = V.inv_ks(17712, y691)
    rec('F4   Inv k 17712 Y691 holds exactly for k = 11 (k <= 40 tried)', ks == [11], ks)
    p = inv_parts(11, 17712, y691)
    INFO['F_inv691'] = p
    rec('F5   Inv 11: Nstar <= N (17705 <= 17712)', p['Nstar'] <= p['N'], p)
    rec('F5   Inv 11: Nlo 11 = 14336 <= N', p['Nlo(k)'] == 14336 and p['Nlo(k)'] <= p['N'], p)
    rec('F5   Inv 11: length bs = 11 <= 11, s = 0 <= 3', p['k(W)'] == 11 and p['s'] == 0)
    rec('F5   Inv 11: Mw bs <= Af 11', p['Mw'] <= p['Af(k)'], p)
    rec('F5   Inv 11: M2 bs <= Bf 11', p['M2'] <= p['Bf(k)'], p)
    rec('F5   Inv 11: x = 10 <= Xf 11', p['x'] == 10 and p['x'] <= p['Xf(k)'], p)
    rec('F6   Nlo 12 = 28672 > 17712 (k >= 12 fails), length 11 > k for k <= 10', V.Nlo(12) == 28672 > 17712)
    # alternative start: orbit 100000 692 1 t0 gives the same (the step-11 hub K(1,1,t0))
    res2, _ = V.orbit(1, V.T0, 692, 100000)
    rec('F7   orbit 100000 692 1 t0 = Some (17712, Y691) as well', res2 == (17712, y691))
    # the first values: N = 3, 8, 10, 14, ... must equal k+1 of the TM left records 42, 194, 708, ...
    rec('F8   first N values 3, 8, 10, 14, 22, 24, 35, 38, 46, 64', Ns[:10] == [3, 8, 10, 14, 22, 24, 35, 38, 46, 64], Ns[:10])
    allN = Ns + [res[0]]
    rec('F9   index 691 is the first epoch with N >= Nstar = 17705 (N = 17684 at index 690)', next(i for i, x in enumerate(allN) if x >= 17705) == 691 and allN[690] == 17684, allN[688:692])
    rec('F9   index 591 is the first epoch with N >= 14796 (the write-up threshold N*), N = 14797', next(i for i, x in enumerate(allN) if x >= 14796) == 591 and allN[591] == 14797)
    INFO['F_B691_coq'] = '[' + '; '.join('(%s, %d)' % ('true' if d else 'false', e) for d, e in B691) + ']'


def section_M():
    y694 = ('p11', 7, gw(B694, 0))
    res, _ = V.orbit(8, V.T2, 691, 100000)
    rec('M    control: the same model code gives #30 fin694: orbit 100000 691 8 t2 = Some (17713, Y694)', res == (17713, y694), res and res[0])
    ks = V.inv_ks(17713, y694)
    rec('M    control: #30 inv694 (Inv 10 17713 Y694) holds in the Python mirror of Inv', 10 in ks, ks)
    INFO['M_inv694_ks'] = ks


# =====================================================================================
# O. model = TM
# =====================================================================================
def section_O():
    L = []
    for line in open(LOG):
        f = line.split()
        if f and f[0] == 'L': L.append((int(f[1]), int(f[2]), f[3] if len(f) > 3 else ''))
    end = [l for l in open(LOG) if l.startswith('END') or l.startswith('HALT')]
    rec('O1   stored log: no halt in 1e11 steps (last line END 100000000000)', end == ['END 100000000000\n'], end)
    rec('O1   stored log: records at steps 4 (k=0, T empty) and 42 (k=2, T=0001) come first', L[:2] == [(4, 0, ''), (42, 2, '0001')], L[:2])
    N, y = 3, V.T1; good = 0
    for i in range(2, len(L)):
        r = V.phif(100000, 1, N, y)
        ok = r is not None and (L[i][1], L[i][2]) == (r[0], norm('000' + V.enc(r[1])))
        rec('O1   model epoch from K(1,N,y) = next TM left record (k, T), all 518 records of the 1e11 log', ok, (i, L[i][:2]))
        if r is None: break
        N, y = r[0] + 1, r[1]
    r0 = V.phif(100000, 1, 1, V.T0)
    rec('O1   the step-42 record is the model epoch from K(1,1,t0) (step 11): phif 1 1 t0 = (2, t1), T = 000 1', r0 == (2, V.T1) and L[1][1:] == (2, norm('000' + V.enc(V.T1))))
    INFO['O_log'] = {'records': len(L), 'compared': len(L) - 2, 'last_step': L[-1][0], 'last_k': L[-1][1], 'model_N_after': N}
    # fresh Python run from blank (independent of the C logger)
    nmax = 3 * 10**6 if QUICK else 2 * 10**7
    tape = bytearray(1 << 17); pos = 1 << 16; q = 0; lo = pos; recs = []
    T = TT
    st = 0
    while st < nmax:
        s = tape[pos]; tr = T[q][s]
        if tr is None: break
        tape[pos] = tr[0]; pos += tr[1]; q = tr[2]; st += 1
        if pos < lo:
            lo = pos
            if q == 4 and tape[pos] == 0 and tape[pos + 1:pos + 4] == b'\x01\x00\x01':
                j = pos + 4; k = 0
                while tape[j:j + 3] == b'\x00\x00\x01': k += 1; j += 3
                recs.append((st, k, norm(''.join(map(str, tape[j:j + 4000])))))
    rec('O2   fresh run: no halt in %d steps' % nmax, st == nmax)
    rec('O2   fresh run: left records = the stored log, record for record', recs == [(a, b, c) for a, b, c in L[:len(recs)]], len(recs))
    INFO['O_fresh'] = {'steps': nmax, 'records': len(recs)}


# =====================================================================================
# T. thresholds (start-independent; the .v proves them, recomputed here)
# =====================================================================================
def Costf(k): return 2 * V.Xf(k) + 2 + 2 * V.Af(k) + 11 * V.Ws(V.Pf(k)) + 13 * V.wq(V.Pf(k))


def section_T():
    ok1 = all(7 * 2 ** k + V.Bf(k) < 2 ** (V.Pf(k) + 1) for k in range(200))
    rec('T1   N1: 7*2^k + Bf k < 2^(Pf k + 1) for k < 200', ok1)
    ok2 = all(Costf(k) + 2 <= V.NSTAR or Costf(k) + 2 <= V.Nlo(k) for k in range(200))
    rec('T2   N2: Costf k + 2 <= 17705 or <= Nlo k, for k < 200', ok2)
    rec('T3   Costf 11 + 2 = 17705 = Nstar (the threshold is attained at k = 11)', Costf(11) + 2 == 17705)
    rec('T4   Costf k + 2 > Nlo k exactly for k <= 11', [k for k in range(200) if Costf(k) + 2 > V.Nlo(k)] == list(range(12)))
    tab = {k: {'Pf': V.Pf(k), 'Af': V.Af(k), 'Bf': V.Bf(k), 'Xf': V.Xf(k), 'Costf+2': Costf(k) + 2, 'Nlo': V.Nlo(k)} for k in range(8, 14)}
    INFO['T_table'] = tab
    rec('T5   table matches #30 submission 8.3 (A 1419/1451/2219/2923/4459/5867, Cost+2 8725/8853/13471/17705/26931/35389)',
        [tab[k]['Af'] for k in range(8, 14)] == [1419, 1451, 2219, 2923, 4459, 5867] and
        [tab[k]['Costf+2'] for k in range(8, 14)] == [8725, 8853, 13471, 17705, 26931, 35389], tab)


# =====================================================================================
# J. Inv along the orbit after the finite part
# =====================================================================================
def section_J():
    nep = 300 if QUICK else 1200
    N, y = 17712, ('p11', 10, gw(B691, 0)); kap = 11; ok = True; t = 691
    for i in range(nep - 691):
        r = V.phif(100000, 1, N, y)
        if r is None: ok = False; break
        N, y = r[0] + 1, r[1]; t += 1
        if y[0] == 'p11':
            g = V.as_gw(y[2]); kap = max(kap, len(g[0]))
        ks = V.inv_ks(N, y)
        rec('J    Inv kappa_t N_t Y_t on every epoch after 691, kappa_t = running max of k(W) (next_inv choice)', kap in ks, (t, N, kap, ks))
    INFO['J_end'] = {'epoch_index': t, 'N': N, 'kappa': kap}


# =====================================================================================
# C. not coupled to #30's orbit
# =====================================================================================
def section_C():
    """informational (not a premise): the two model orbits merge"""
    def orb(N, y, n):
        out = []
        for _ in range(n):
            out.append((N, repr(y)))
            r = V.phif(100000, 1, N, y); N, y = r[0] + 1, r[1]
        return out
    n = 900 if QUICK else 1200
    a = orb(3, V.T1, n); b = orb(8, V.T2, n)
    ib = {x: i for i, x in enumerate(b)}
    first = next(((i, ib[x]) for i, x in enumerate(a) if x in ib), None)
    rec('C1   the W4-1 orbit (from K(1,3,t1)) and the #30 orbit (from K(1,8,t2)) first share an epoch at index 795 of both, N = 20922',
        first == (795, 795) and a[795][0] == 20922, first)
    rec('C2   the two orbits are distinct before index 795 and identical from index 795 on (to index %d)' % (n - 1),
        not (set(a[:795]) & set(b[:795])) and a[795:] == b[795:], first)
    INFO['C_merge'] = {'index': first, 'N': a[795][0] if first else None, 'W4-1 N before': [x[0] for x in a[790:795]],
                       '#30 N before': [x[0] for x in b[790:795]]}


# =====================================================================================
# D. #30's write-up Lemma D on W4-1's orbit
# =====================================================================================
def section_D():
    p = subprocess.run([sys.executable, '-B', os.path.join(HERE, 'scripts', 'lemmaD_w41.py'), '400000'],
                       capture_output=True, text=True, timeout=3600)
    out = p.stdout
    open(os.path.join(HERE, 'data', 'lemmaD_w41.log'), 'w').write(out + '\nrc=%d\n' % p.returncode)
    rec('D    #30 write-up Lemma D chain (D.0-D.8 links) on W4-1 rules-only orbit to N >= 400,000: ALL PASS',
        p.returncode == 0 and 'ALL PASS' in out, out[-500:])
    m = re.search(r"_D (\{.*\})", out)
    INFO['D'] = m.group(1)[:600] if m else None


def main():
    t0 = time.time()
    for f in (section_S, section_XV, section_K, section_W, section_LP, section_PH, section_R, section_N, section_I, section_F,
              section_M, section_O, section_T, section_J, section_C) + (() if QUICK else (section_D,)):
        t1 = time.time(); f(); print('%-12s %6.1f s' % (f.__name__, time.time() - t1), flush=True)
    bad = 0
    for cid in sorted(RES):
        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(INFO): print('INFO', k, json.dumps(INFO[k], default=str)[:1500])
    print('SUMMARY', 'ALL PASS' if bad == 0 else f'{bad} CLAIMS FAIL', f'({round(time.time() - t0, 1)} s, seed {SEED}{", quick" if QUICK else ""})')
    with open(os.path.join(HERE, 'data', f'check_proof_seed{SEED}{"_quick" if QUICK else ""}.json'), 'w') as f:
        json.dump({'seed': SEED, 'quick': QUICK, 'claims': RES, 'info': INFO}, f, indent=1, default=str)
    return bad


if __name__ == '__main__':
    sys.exit(1 if main() else 0)