#!/usr/bin/env python3
"""check_proof.py for W5-1 = 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- (740 line 349); proof.md in this directory.

proof.md proves that 349 never halts by way of the table
    TP  = 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC        (W4-2's table with F1 = 1RC instead of 1LF)
349 is TP mirrored (L<->R) and renamed by f = (A->F, B->A, C->B, D->C, E->D, F->E); 349 from blank is TP from
0^inf F> 0^inf seen in a mirror.  TP's left step is W4-2's left step with every F1 stretched into F1 C1 A1 (the
detour); everything above the left step, the right step and the overflow is W4-2's mathematics, unchanged.

Every claim of proof.md is checked here.  The TM-level claims are checked by direct simulation of TP, of 349 (in
mirrored configurations) and, where proof.md compares, of W4-2.  The arithmetic layer (phi, the orbit lemmas, the
overflow words, the macro rules' closed forms, the invariant I, Lemma S, Lemma C) is the same statement as in W4-2's
proof.md; its checks are W4-2's check_proof.py functions, imported as a library and re-run here under this seed.

Sections (proof.md section in brackets):
  T   [1, 3.1]  table facts: TP vs W4-2 (only F1), undefined cells, who enters F/E/C; 349 = mirror+rename of TP;
                busycoq Perm (flip tm349) TP f, both clauses; 349 on the 740 list; Eqv_v3 TM518 vs 349
  E   [3.2]     Lemma E (detour): TP  1 <F 1  -->(3)  <F 1 1  for every context; 349's mirrored form
  TL  [3.2, 9]  the eight one-digit lemmas of the .v on TP (TA0..TB, with TF2'/TF3' restated), exact result and
                step count, all contexts up to 6 cells + random; teeth: W4-2's unrestated TF2/TF3 fail on TP
  PS  [3.2]     phi_spec on TP: the relations PA/PF (as functions) = phi / phi(2w+1)>>1; TP from WS e o <A r and
                from WS e o <F [1] r reaches WS e' o' B> r / B> [1] r in the stated steps; every F1 read has a 1 on
                its right
  LS  [3.2]     left step L0/L1 on TP: result phi(w), steps 1 / 2e+3+2*p11, never right of the boundary, only
                A0 A1 F0 F1 C1 B1 used, every F1 followed by C1 A1
  RS  [3.3]     right step: W4-2's RS chain, every intermediate configuration, on TP (no F1, no E1)
  OV  [3.3]     overflow OV0, CD, OVe, OVo reset, halt, nested: W4-2's checks run on TP
  V   [9]       the .v statements RS, OVe, OVo on TP; the W4-2 .v: which lemmas execute the machine, the cited
                statements are in the file
  K   [3.4]     level-1 rules R1..R4 on TP (exhaustive small words), step counts with L_TP
  D   [3.1,3.4] R1..R4 directly on 349 in mirrored configurations, exhaustive small + random
  M   [3.5, 4]  W4-2's arithmetic checks re-run: PHI (SW, increments, phij), ORB (O3-O6), X (overflow words),
                INV (Lemma S, Lemma C, progress; exhaustive m <= 700 + random to 2^60)
  B   [3.6]     macro rules: closed form = abstract execution (small exhaustive, large random); = direct TP; =
                direct 349; where each rule ends; (std,0,M) only inside S2/P0
  Z   [6]       initial segment: 349 from blank (14 transitions, K'('',0,1) at 14, K'(std 2,0,2) at 73), TP from F
                (the .v's init statements, fallback via BS_S0), the overflow configurations and their step numbers
                of a direct 349 run = the rules' orbit with the step formulas; lockstep 349 = mirror of TP from F;
                lockstep TP from F = W4-2 from F with F1 expanded
  J   [7]       I along the orbit from (std,2,2)
  NEG [5]       controls: off I, a halting overflow halts on 349 (F1) and TP (E1); the detour without a 1 on the
                right is not W4-2's F1
  P   [8, 2]    the whole lemma plan as one file, rocq/plan_check_full.v: the compiled file is the current one
                (sha256 in work/plan_check_full.log), the log says exit 0 and 'Closed under the global context';
                the file is plan_check_phi.v's head + W4-2's .v from PA_spec on, verbatim except initF and the
                tail; tm = line 349 of the 740 list (one top-level Definition tm), tmP = TP, both notations use
                tmP; the 8 cited statements; f349 = f; no forbidden keyword; proof.md cites no internal W4-2 file
                outside its review log; the 1 rule block uses c0 only for busycoq's start
Usage: python3 -B check_proof.py [--seed S] [--quick|--full] [--only T,E,...]
"""
import hashlib
import importlib.util
import json
import os
import random
import re
import sys
import time

HERE = os.path.dirname(os.path.abspath(__file__))
ROOT = os.path.abspath(os.path.join(HERE, '..', '..'))
W42DIR = os.path.join(ROOT, 'machines', '1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF')
W42CP = os.path.join(W42DIR, 'check_proof.py')
W42V = os.path.join(W42DIR, '1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v')

_argv = sys.argv
sys.argv = [sys.argv[0]]
_spec = importlib.util.spec_from_file_location('w42cp', W42CP)
cp = importlib.util.module_from_spec(_spec)
_spec.loader.exec_module(cp)
sys.argv = _argv

SEED = int(sys.argv[sys.argv.index('--seed') + 1]) if '--seed' in sys.argv else 1
QUICK = '--quick' in sys.argv
FULL = '--full' in sys.argv
RNG = random.Random(SEED)
cp.RNG = random.Random(SEED * 7919 + 17)
cp.QUICK, cp.FULL = QUICK, FULL
RES, ORDER, INFO = {}, [], {}
T0 = time.time()

TM349 = '1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---'
W42 = '1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF'
TP = '1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC'
TM518 = '1RB1RA_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---'      # Eqv_v3.v Module TM518, `tm`
ST = 'ABCDEF'
A, B_, C, D, E, F = range(6)
FMAP = [F, A, B_, C, D, E]          # f: 349 state q <-> TP state FMAP[q]  (A->F, B->A, C->B, D->C, E->D, F->E)
FINV = {FMAP[q]: q for q in range(6)}

T349, TTP, TW = cp.table(TM349), cp.table(TP), cp.table(W42)
Run = cp.Run
phi, tz, W, EO, std, pk, word, decode = cp.phi, cp.tz, cp.W, cp.EO, cp.std, cp.pk, cp.word, cp.decode


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


def harvest(prefix, fn, *args):
    """run one of W4-2's check functions and copy its results here under `prefix`"""
    cp.RES, cp.ORDER = {}, []
    fn(*args)
    for cid in cp.ORDER:
        key = prefix + cid
        if key in RES:
            r, s = RES[key], cp.RES[cid]
            r['n'] += s['n']; r['pass'] += s['pass']; r['fail'] = (r['fail'] + s['fail'])[:3]
        else:
            RES[key] = dict(cp.RES[cid])
            ORDER.append(key)


# ---------------------------------------------------------------------------------------------------------
# configurations as cell lists.  lft / rgt: the cells left / right of the head, ADJACENT CELL FIRST (busycoq order).
PAD = 12


def cfg(lft, hs, rgt, pad=PAD):
    cells = [0] * pad + list(reversed(lft)) + [hs] + list(rgt) + [0] * pad
    return cells, pad + len(lft)


def L_(l, r):
    """busycoq  l <{{q}} r : the head reads hd l"""
    return (l[1:], l[0] if l else 0, r)


def R_(l, r):
    """busycoq  l {{q}}> r : the head reads hd r"""
    return (l, r[0] if r else 0, r[1:])


def is_cfg(R, q, lft, hs, rgt):
    """R is exactly in state q with these cells (and 0 elsewhere)"""
    if R.halted is not None or R.s != q or R.tape[R.h] != hs:
        return False
    t = R.tape
    h = R.h
    for i, c in enumerate(lft):
        if t[h - 1 - i] != c:
            return False
    for i, c in enumerate(rgt):
        if t[h + 1 + i] != c:
            return False
    lo, hi = h - 1 - len(lft), h + 1 + len(rgt)
    return not any(t[:lo + 1]) and not any(t[hi:])


def run_from(tt, q, lft, hs, rgt, steps, track=True):
    cells, head = cfg(lft, hs, rgt, pad=PAD + 2 * steps + 8)
    R = Run(tt, cells, head, q, size=8)
    R.step(steps, track=track)
    return R


def rbits(n):
    return [RNG.randint(0, 1) for _ in range(n)]


def contexts(maxlen):
    """all 0/1 lists of length <= maxlen"""
    out = [[]]
    for L in range(1, maxlen + 1):
        for x in range(1 << L):
            out.append([(x >> i) & 1 for i in range(L)])
    return out


def wcells(w, length=None):
    """word int -> cells from offset 0 upwards (the order of a left side, adjacent first)"""
    L = max(w.bit_length(), 1) if length is None else length
    return [(w >> d) & 1 for d in range(L)]


def p11(w, e):
    """F1 reads in TP's left scan of w with lowest 00 pair (e, e+1): adjacent 11 pairs (c-1, c), 1 <= c <= e-1"""
    if e <= 1:
        return 0
    return bin((w & (w >> 1)) & ((1 << (e - 1)) - 1)).count('1')


def lowest00(w):
    z = ~w
    return tz(z & (z >> 1))


def L_TP(w):
    """proof.md 3.2: steps of TP's left step on w"""
    if w & 1 == 0:
        return 1
    e = lowest00(w)
    return 2 * e + 3 + 2 * p11(w, e)


def L_W42(w):
    if w & 1 == 0:
        return 1
    return 2 * lowest00(w) + 3


def PAf(e, o):
    """the relation PA of the .v, read as a function (constructor chosen by the parities)"""
    stack = []
    mode = 'A'
    while True:
        if mode == 'A':
            if e % 2 == 0:
                e2, o2 = e + 1, o                     # PA0
                break
            stack.append(1)
            mode = 'A' if o % 2 == 0 else 'F'         # PA1 / PA2
        else:
            if e % 2 == 0 and o % 2 == 0:
                e2, o2 = e, o + 1                     # PF0
                break
            stack.append(1)
            mode = 'A' if (e % 2 == 1 and o % 2 == 0) else 'F'   # PF2 / PF1, PF3
        e, o = e // 2, o // 2
    for _ in stack:
        e2, o2 = 2 * e2, 2 * o2
    return e2, o2


def PFf(e, o):
    """PF as a function: same recursion, started in mode F"""
    if e % 2 == 0 and o % 2 == 0:
        return e, o + 1
    if e % 2 == 1 and o % 2 == 0:
        e2, o2 = PAf(e // 2, o // 2)
    else:
        e2, o2 = PFf(e // 2, o // 2)
    return 2 * e2, 2 * o2


# ---------------------------------------------------------------------------------------------------------
def sec_T():
    diff = [ST[i // 2] + str(i % 2) for i in range(12) if TTP[i] != TW[i]]
    rec('T.TP_vs_W42_only_F1', diff == ['F1'] and TTP[2 * F + 1] == (1, 1, C) and TW[2 * F + 1] == (1, -1, F), diff)
    rec('T.TP_only_E1_undefined', [ST[i // 2] + str(i % 2) for i in range(12) if TTP[i] is None] == ['E1'])
    rec('T.349_only_F1_undefined', [ST[i // 2] + str(i % 2) for i in range(12) if T349[i] is None] == ['F1'])
    rec('T.mirror_rename(TP,f)==349', cp.mirror_rename(TP, FMAP) == TM349, cp.mirror_rename(TP, FMAP))
    rec('T.mirror_rename(W42,f)==TM518', cp.mirror_rename(W42, FMAP) == TM518)
    d518 = [ST[i // 2] + str(i % 2) for i in range(12) if cp.table(TM518)[i] != T349[i]]
    rec('T.349_vs_TM518_only_A1', d518 == ['A1'], d518)
    # 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'))
    # with tm = flip tm349 (directions swapped) and tm' = TP
    ok1 = ok2 = True
    for q in range(6):
        for s in (0, 1):
            a = T349[2 * q + s]
            fa = None if a is None else (a[0], -a[1], a[2])          # flip
            b = TTP[2 * FMAP[q] + s]
            if fa is None:
                ok1 = ok1 and b is None
            else:
                ok2 = ok2 and b == (fa[0], fa[1], FMAP[fa[2]])
    rec('T.Perm_flip349_TP_f_clause_None', ok1)
    rec('T.Perm_flip349_TP_f_clause_Some', ok2)
    rec('T.f(A)=F', FMAP[A] == F)
    into = lambda tt, q: [ST[i // 2] + str(i % 2) for i in range(12) if tt[i] and tt[i][2] == q]
    rec('T.TP_into_F_only_A1_writes1_movesL', into(TTP, F) == ['A1'] and TTP[2 * A + 1][:2] == (1, -1), into(TTP, F))
    rec('T.TP_into_E_only_D1', into(TTP, E) == ['D1'], into(TTP, E))
    rec('T.TP_into_C', into(TTP, C) == ['B0', 'D0', 'F1'], into(TTP, C))
    rec('T.TP_C1_is_1LA', TTP[2 * C + 1] == (1, -1, A))
    hl = open(os.path.join(ROOT, 'data', 'holdouts', 'BB6_holdouts_740.txt')).read().split('\n')
    rec('T.349_on_740_line_349', hl[348] == TM349, hl[348])
    rec('T.TP_W42_TM518_not_on_740', all(x not in hl for x in (TP, TM518)) and W42 in hl)


def sec_E():
    """Lemma E: [1] *> l <{{F}} [1] *> r -->(3) l <{{F}} [1;1] *> r on TP (F1 C1 A1)"""
    ctx = contexts(5 if QUICK else 6)
    for l in ctx:
        for r in ctx[::max(1, len(ctx) // 40)]:
            R = run_from(TTP, F, *L_([1] + l, [1] + r), 3)
            rec('E.detour_TP_3_steps', is_cfg(R, F, *L_(l, [1, 1] + r)) and R.used == {'F1', 'C1', 'A1'}, (l, r))
    for _ in range(300 if QUICK else 3000):
        l, r = rbits(RNG.randint(0, 40)), rbits(RNG.randint(0, 40))
        R = run_from(TTP, F, *L_([1] + l, [1] + r), 3)
        rec('E.detour_TP_3_steps', is_cfg(R, F, *L_(l, [1, 1] + r)), (l, r))
        # the same tape change is W4-2's F1 (1 step)
        R2 = run_from(TW, F, *L_([1] + l, [1] + r), 1)
        rec('E.W42_F1_same_result_1_step', is_cfg(R2, F, *L_(l, [1, 1] + r)), (l, r))
        # 349's form: x 1 A> 1 y --(A1 D1 B1)--> x 1 1 A> y   (mirror; left list = TP's right list)
        R3 = run_from(T349, A, *R_([1] + r, [1] + l), 3)
        rec('E.detour_349_A1_D1_B1', is_cfg(R3, A, *R_([1, 1] + r, l)) and R3.used == {'A1', 'D1', 'B1'}, (l, r))


TL_LEMMAS = [
    # name, start state, start (side builder, l, r) as functions of (l, r), end state, end, TP steps, W4-2 steps
    ('TA0_a0', A, lambda l, r: L_([0, 0] + l, r), B_, lambda l, r: R_([1, 0] + l, r), 1, 1),
    ('TA0_a1', A, lambda l, r: L_([0, 1] + l, r), B_, lambda l, r: R_([1, 1] + l, r), 1, 1),
    ('TA1', A, lambda l, r: L_([1, 0] + l, r), A, lambda l, r: L_(l, [1, 1] + r), 2, 2),
    ('TA2', A, lambda l, r: L_([1, 1] + l, r), F, lambda l, r: L_(l, [1, 1] + r), 4, 2),
    ('TF0', F, lambda l, r: L_([0, 0] + l, r), B_, lambda l, r: R_([0, 1] + l, r), 3, 3),
    ('TF1', F, lambda l, r: L_([0, 1] + l, r), F, lambda l, r: L_(l, [1, 1] + r), 2, 2),
    ("TF2'", F, lambda l, r: L_([1, 0] + l, [1] + r), A, lambda l, r: L_(l, [1, 1] + [1] + r), 4, 2),
    ("TF3'", F, lambda l, r: L_([1, 1] + l, [1] + r), F, lambda l, r: L_(l, [1, 1] + [1] + r), 6, 2),
    ('TB', B_, lambda l, r: R_(l, [1, 1] + r), B_, lambda l, r: R_([0, 0] + l, r), 2, 2),
]


def sec_TL():
    ctx = contexts(4 if QUICK else 6)
    sub = ctx[::max(1, len(ctx) // 30)]
    pairs = [(l, r) for l in ctx for r in sub] + [(rbits(RNG.randint(0, 30)), rbits(RNG.randint(0, 30)))
                                                  for _ in range(200 if QUICK else 2000)]
    for name, q0, st, q1, en, ntp, nw in TL_LEMMAS:
        for l, r in pairs:
            R = run_from(TTP, q0, *st(l, r), ntp)
            rec('TL.%s_TP_exact_%d_steps' % (name, ntp), is_cfg(R, q1, *en(l, r)), (l, r))
            R2 = run_from(TW, q0, *st(l, r), nw)
            rec('TL.%s_W42_exact_%d_steps' % (name, nw), is_cfg(R2, q1, *en(l, r)), (l, r))
    # teeth: W4-2's TF2 / TF3 (for every l, r) are false on TP.  A counterexample (l, r) with r starting with 0: the
    # configuration of the statement is not reached within 40 steps.  (A configuration is a tape up to translation,
    # so for some l, e.g. the blank one for TF2, the machine meets an equal configuration later by coincidence; one
    # counterexample refutes the universal statement.)
    for name, start, target in (('TF2', [1, 0], A), ('TF3', [1, 1], F)):
        bad = 0
        first = None
        for l, r in [([], []), ([1], []), ([0, 1], [])] + pairs[:400]:
            r0 = [0] + r
            st = L_(start + l, r0)
            en = L_(l, [1, 1] + r0)
            cells, head = cfg(*st, pad=PAD + 90)
            R = Run(TTP, cells, head, F, size=8)
            hit = False
            for _ in range(40):
                if not R.step(1):
                    break
                if is_cfg(R, target, *en):
                    hit = True
                    break
            bad += not hit
            if not hit and first is None:
                first = (l, r0)
        rec('TL.%s_unrestated_false_on_TP_(counterexample_exists)' % name, first is not None, bad)
        INFO['TL_%s_unrestated_counterexamples' % name] = '%d/%d, first (l, r) = %s' % (bad, 3 + min(400, len(pairs)), first)


def sec_PS():
    """phi_spec on TP.  PA: WS e o <A r -->+ WS e' o' B> r.  PF (restated): WS e o <F [1] r -->+ WS e' o' B> [1] r."""
    maxlen = 10 if QUICK else 13
    words = list(range(1 << maxlen)) + [RNG.getrandbits(RNG.randint(14, 90)) for _ in range(300 if QUICK else 3000)]
    f1_ok = True
    for w in words:
        e, o = EO(w)
        ea, oa = PAf(e, o)
        ef, of_ = PFf(e, o)
        rec('PS.PA_relation_eq_phi', W(ea, oa) == phi(w), w)
        rec('PS.PF_relation_eq_phi(2w+1)>>1', W(ef, of_) == phi(2 * w + 1) >> 1 and phi(2 * w + 1) & 1 == 0, w)
        if w >= (1 << maxlen) or w < (1 << (maxlen - 2)) or RNG.random() < 0.5:
            r = rbits(RNG.randint(0, 6))
            wl = max(w.bit_length(), 1)
            # PA run
            nst = L_TP(w)
            R = run_from(TTP, A, *L_(wcells(w, wl), r), nst)
            rec('PS.PA_spec_TP', is_cfg(R, B_, *R_(wcells(W(ea, oa)) if W(ea, oa) else [], r)), (w, r))
            # PF run (restated: a 1 right of F)
            nsf = L_TP(2 * w + 1) - 2
            cells, head = cfg(*L_(wcells(w, wl), [1] + r), pad=PAD + 2 * nsf + 8)
            R = Run(TTP, cells, head, F, size=8)
            for _ in range(nsf):
                if R.s == F and R.tape[R.h] == 1 and R.tape[R.h + 1] != 1:
                    f1_ok = False
                R.step(1)
            rec('PS.PF_spec_TP_restated', is_cfg(R, B_, *R_(wcells(W(ef, of_)) if W(ef, of_) else [], [1] + r)), (w, r))
    rec('PS.every_F1_read_has_1_on_its_right', f1_ok)


def sec_LS():
    """L0: l 0 <A r --> l 1 B> r (1 step); L1: l 0 0 z <A r --> l 1 0^(|z|+1) B> r (2e+3+2*p11 steps) on TP"""
    maxlen = 11 if QUICK else 14
    words = list(range(1 << maxlen)) + [cp.rand_word(15, 90) for _ in range(300 if QUICK else 3000)]
    used = set()
    detour_ok = True
    for w in words:
        wl = max(w.bit_length(), 1)
        ctx = rbits(RNG.randint(0, 8))
        pad = 4
        cells = [0] * pad + cp.bits_to_cells(w, wl) + ctx
        p0 = pad + wl - 1
        R = Run(TTP, cells, p0, A)
        prev = None
        while True:
            s, r = R.s, R.tape[R.h]
            if prev == 'F1' and not (s == C and r == 1):
                detour_ok = False
            if not R.step():
                break
            prev = ST[s] + str(r)
            if prev == 'C1' and R.s != A:
                detour_ok = False
            if R.h - R.off > p0:
                break
        if R.halted:
            rec('LS.no_halt', False, w)
            continue
        got = R.cells(-60, p0 + 1)
        okw = got == cp.bits_to_cells(phi(w), 60 + p0 + 1)
        okc = R.cells(p0 + 1, p0 + 1 + len(ctx)) == ctx and R.s == B_ and R.h - R.off == p0 + 1
        if w & 1 == 0:
            rec('LS.L0_TP', okw and okc and R.steps == 1, (w, R.steps))
        else:
            rec('LS.L1_TP_steps_2e+3+2p11', okw and okc and R.steps == L_TP(w), (bin(w), R.steps, L_TP(w)))
            rec('LS.F1_reads_eq_p11', R.steps - L_W42(w) == 2 * p11(w, lowest00(w)), bin(w))
        used |= R.used
        rec('LS.no_halt', True)
    rec('LS.transitions_used', used <= {'A0', 'A1', 'F0', 'F1', 'C1', 'B1'}, sorted(used))
    rec('LS.every_F1_followed_by_C1_reading_1_then_A1', detour_ok)


def sec_RS_OV():
    cp.TT = TTP
    try:
        harvest('TP.', cp.sec_RS)
        harvest('TP.', cp.sec_OV)
    finally:
        cp.TT = TW


def sec_V():
    """the .v statements on TP: RS, OVe, OVo; and facts about W4-2's .v file that the lemma plan relies on"""
    for n in range(0, 25 if QUICK else 40):
        for m in range(0, 6):
            l = rbits(RNG.randint(0, 10))
            # RS l n m: l {{B}}> R (S n) m -->+ l <{{A}} R n (S m)
            st = R_(l, cp.Rcells(n + 1, m))
            R = run_from(TTP, B_, *st, 10 * (n + 1) + 7)
            rec('V.RS_TP', is_cfg(R, A, *L_(l, cp.Rcells(n, m + 1))), (n, m))
    for u in range(0, 10 if QUICK else 16):
        for m in range(0, 6):
            l = rbits(RNG.randint(0, 10))
            # OVe l u m: ([0;0]^^u *> [1] *> l) {{B}}> R 0 m -->+ l <{{A}} R (1+u+m) 0     (2u+8 steps)
            R = run_from(TTP, B_, *R_([0, 0] * u + [1] + l, cp.Rcells(0, m)), 2 * u + 8)
            rec('V.OVe_TP', is_cfg(R, A, *L_(l, cp.Rcells(1 + u + m, 0))), (u, m, l))
            # OVo l u m: ([0;0]^^u *> [0;1;0;0] *> l) {{B}}> R 0 m -->+ l <{{A}} R 0 (u+2+m)   (2u+15 steps)
            R = run_from(TTP, B_, *R_([0, 0] * u + [0, 1, 0, 0] + l, cp.Rcells(0, m)), 2 * u + 15)
            rec('V.OVo_TP', is_cfg(R, A, *L_(l, cp.Rcells(0, u + 2 + m))), (u, m, l))
    # W4-2's .v: the lemmas whose proofs execute the machine, and the statements proof.md 9 cites
    src = open(W42V).read()
    INFO['W42_v_sha256'] = hashlib.sha256(src.encode()).hexdigest()
    code = re.sub(r'\(\*.*?\*\)', '', src, flags=re.S)
    blocks = re.findall(r'\n(Lemma|Theorem|Corollary|Definition|Fixpoint|Inductive)\s+([A-Za-z0-9_\']+)(.*?)(?=\n(?:Lemma|Theorem|Corollary|Definition|Fixpoint|Inductive|Scheme|Combined|Notation|Ltac|Local|Require|From|Open)\b|\Z)', code, flags=re.S)
    execs = sorted(name for kind, name, body in blocks if re.search(r'\b(es|esx|execute|solve_init|step)\b\s*[.;]', body))
    want = sorted(['TA0', 'TA1', 'TA2', 'TF0', 'TF1', 'TF2', 'TF3', 'TB', 'RS', 'OVe', 'OVo', 'init0'])
    rec('V.W42_v_lemmas_that_execute_tm', execs == want, execs)
    tms = [name for kind, name, body in blocks if body.count('-[ tm ]->')]
    rec('V.W42_v_tm_only_in_two_notations', re.findall(r'-\[ *tm *\]->', code) == ['-[ tm ]->', '-[ tm ]->'] and tms == [], tms)
    stmts = ['Lemma TA2 l r: [1;1] *> l <{{A}} r -->+ l <{{F}} [1;1] *> r.',
             'Lemma TF2 l r: [1;0] *> l <{{F}} r -->+ l <{{A}} [1;1] *> r.',
             'Lemma TF3 l r: [1;1] *> l <{{F}} r -->+ l <{{F}} [1;1] *> r.',
             '(forall e o e\' o\', PF e o e\' o\' -> forall r, WS e o <{{F}} r -->+ WS e\' o\' {{B}}> r).',
             'Definition PA_spec := proj1 phi_spec.',
             'Lemma BS_S0 i m: K (2^i-1) 0 0 m -->+ K (1+i+m) 0 0 (1+i+m).',
             'Lemma init0: c0 -->* K 1 0 0 1.',
             'Lemma step_I s: I s -> exists s\', St s -->+ St s\' /\\ I s\'.',
             'Lemma nonhalt: ~halts tm c0.']
    missing = [s for s in stmts if s not in src]
    rec('V.W42_v_cited_statements_present', missing == [], missing)
    rec('V.W42_v_PF_clause_used_only_in_phi_spec', src.count('proj2 phi_spec') == 0 and code.count('phi_spec') == 2)
    st = json.load(open(os.path.join(W42DIR, 'status.json')))
    rec('V.W42_status_KILLED_NONHALT', st.get('status') == 'KILLED_NONHALT', st.get('status'))
    rec('V.W42_v_sha_eq_status', st.get('kill', {}).get('sha256') == INFO['W42_v_sha256'], st.get('kill', {}).get('sha256'))


def sec_K():
    """R1 and the overflow rules on TP's K configurations, with TP's step counts"""
    for w in range(0, 1 << (9 if QUICK else 11)):
        wl = max(w.bit_length(), 1)
        pad = 6
        for n, m in ((1, 0), (2, 1), (3, 2), (1, 5)):
            cells = [0] * pad + cp.bits_to_cells(w, wl) + cp.Rcells(n, m)
            b0 = pad + wl
            R = Run(TTP, cells, b0 - 1, A)
            R.step(L_TP(w) + 10 * n + 7)
            ok = (R.s == A and R.h - R.off == b0 - 1 and R.cells(b0, b0 + 2 * (n + m) + 8) == cp.Rcells(n - 1, m + 1) + [0] * 4
                  and R.cells(0, b0) == cp.bits_to_cells(phi(w), b0))
            rec('K.R1_TP', ok, (bin(w), n, m))
        for m in (0, 1, 3):
            kind, x, mm = cp.overflow(w, m)
            cells = [0] * pad + cp.bits_to_cells(w, wl) + cp.Rcells(0, m)
            b0 = pad + wl
            R = Run(TTP, cells, b0 - 1, A)
            q = tz(phi(w))
            sl = L_TP(w)
            if kind == 'R2':
                R.step(sl + q + 8)
                bp = b0 - q - 1
                ok = (R.s == A and R.h - R.off == bp - 1 and R.cells(bp, bp + 2 * mm + 8) == cp.Rcells(mm, 0) + [0] * 4
                      and R.cells(0, bp) == cp.bits_to_cells(x, bp))
                rec('K.R2_TP', ok, (bin(w), m))
            elif kind == 'R3':
                R.step(sl + q + 14)
                bp = b0 - q - 3
                ok = (R.s == A and R.h - R.off == bp - 1 and R.cells(bp, bp + 2 * mm + 8) == cp.Rcells(0, mm) + [0] * 4
                      and R.cells(0, bp) == cp.bits_to_cells(x, bp))
                rec('K.R3_TP', ok, (bin(w), m))
            elif kind == 'R4':
                R.step(sl + q + 9 + 5)
                rec('K.R4_TP_halts_E1_at_step', R.halted == (E, 1) and R.steps == sl + q + 8, (bin(w), m, R.steps))
            else:
                R.step(sl + q + 10)
                rec('K.R5_TP_enters_F_scan', R.halted is None and R.s == F, (bin(w), m))


# ---------------------------------------------------------------------------------------------------------
# 349-oriented configurations: TP's K(w,n,m) = 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf, mirrored:
#   K'(w,n,m) = 0^inf (01)^m 0 (01)^(1+n) 1 B> w~ 0^inf   (w~ = w read from offset 0, left to right)
def cfg349(w, n, m):
    wc = cp.bits_to_cells(w) or [0]
    rc = cp.Rcells(n, m)
    return list(reversed(wc + rc)), len(rc)


def same349(R, w, n, m, q=B_):
    cells, head = cfg349(w, n, m)
    if R.halted or R.s != q:
        return False
    base = R.h - head
    t = R.tape
    if any(t[:base]) or any(t[base + len(cells):]):
        return False
    return bytes(t[base:base + len(cells)]) == bytes(cells)


def run349(w, n, m, steps):
    cells, head = cfg349(w, n, m)
    R = Run(T349, cells, head, B_, size=len(cells) + 2 * steps + 64)
    R.step(steps, track=False)
    return R


def sec_D():
    cases = [(w, n, m) for w in range(0, 1 << (8 if QUICK else 10)) for (n, m) in ((0, 0), (0, 2), (1, 0), (2, 3))]
    for _ in range(300 if QUICK else 2000):
        cases.append((RNG.getrandbits(RNG.randint(1, 60)), RNG.choice([0, 0, RNG.randint(1, 30)]), RNG.randint(0, 30)))
    cnt = {}
    for w, n, m in cases:
        if n >= 1:
            R = run349(w, n, m, L_TP(w) + 10 * n + 7)
            rec('D.R1_349', same349(R, phi(w), n - 1, m + 1), (w, n, m))
            k = 'R1'
        else:
            f = phi(w)
            q = tz(f)
            x = f >> (q + 1)
            k, _, mm = cp.overflow(w, m)
            if k == 'R2':
                R = run349(w, 0, m, L_TP(w) + q + 8)
                rec('D.R2_349', same349(R, x, mm, 0), (w, m))
            elif k == 'R3':
                R = run349(w, 0, m, L_TP(w) + q + 14)
                rec('D.R3_349', same349(R, x >> 2, 0, mm), (w, m))
            elif k == 'R4':
                R = run349(w, 0, m, L_TP(w) + q + 14)
                rec('D.R4_349_halts_F1_at_step', R.halted == (F, 1) and R.steps == L_TP(w) + q + 8, (w, m, R.halted, R.steps))
        cnt[k] = cnt.get(k, 0) + 1
    INFO['D_counts'] = cnt


def sec_M():
    """W4-2's arithmetic checks (the same statements; proof.md 3.5 and 4), re-run under this seed"""
    for name in ('sec_PHI', 'sec_ORB', 'sec_X', 'sec_INV'):
        t = time.time()
        harvest('M.', getattr(cp, name))
        INFO['M_' + name + '_s'] = round(time.time() - t, 1)
    INFO['M_INV_exhaustive'] = cp.INFO.get('INV_exhaustive')


# ---------------------------------------------------------------------------------------------------------
def run349_to_clean(w, m, max_steps, visits=None):
    """direct 349 run from K'(w,0,m) to the first K'(w',0,m') with w' != 0 clean; ((typ,N,m'), steps)"""
    cells, head = cfg349(w, 0, m)
    size = 8 * (len(cells) + m) + 400
    R = Run(T349, cells, head, B_, size=size)
    tape, h, s = R.tape, R.h, R.s
    steps = 0
    while steps < max_steps:
        r = tape[h]
        a = T349[2 * s + r]
        if a is None:
            return ('HALT', (s, r)), steps
        tape[h] = a[0]
        h += a[1]
        s = a[2]
        steps += 1
        if s == B_ and a[1] > 0 and tape[h - 1] == 1 and tape[h - 2] == 1 and tape[h - 3] == 0 and tape[h - 4] == 0:
            p = h - 5
            mm = 0
            while tape[p] == 1 and tape[p - 1] == 0:
                mm += 1
                p -= 2
            if tape[p] == 0 and tape.find(1, 0, p + 1) == -1:
                last = tape.rfind(1)
                ww = 0 if last < h else int(''.join(map(str, reversed(tape[h:last + 1]))), 2)
                if visits is not None:
                    visits.append((ww, mm, steps))
                if ww != 0:
                    d = decode(ww)
                    if d is not None:
                        return (d[0], d[1], mm), steps
    return ('TIMEOUT', None), steps


def sec_B():
    seen = {r: 0 for r in cp.RULES}
    M1 = 40 if QUICK else 90
    for m in range(0, M1 + 1):
        for N in range(0, 3 * m + 9):
            for typ in ('std', 'pk'):
                if typ == 'pk' and N < 2:
                    continue
                name, nxt = cp.rule(typ, N, m)
                if name is None:
                    continue
                got, path = cp.abstract_B(word(typ, N), m)
                rec('B.closed_eq_abstract_small', got == nxt, (typ, N, m, name, nxt, got, path))
                seen[name] += 1
                harvest('', cp.end_checks, typ, N, m, name, nxt, cp.overflow_states(word(typ, N), m), 'abstract')
    for r in cp.RULES:
        rec('B.rule_exercised_small:' + r, seen[r] > 0, seen[r])
    cnt = {r: 0 for r in cp.RULES}
    target = 200 if QUICK else 2000
    tries = 0
    while min(cnt.values()) < target and tries < 400000:
        tries += 1
        s = cp.constructed_state(RNG.choice(cp.RULES), RNG.randint(6, 60))
        if s is None:
            continue
        name, nxt = cp.rule(*s)
        if name is None or cnt[name] >= target:
            continue
        got, path = cp.abstract_B(word(s[0], s[1]), s[2], fast=True)
        rec('B.closed_eq_abstract_large', got == nxt, (s, name, nxt, got, path))
        cnt[name] += 1
    # direct TP and direct 349, on the same constructed states
    per = 6 if QUICK else 30
    cntd = {r: 0 for r in cp.RULES}
    tries = 0
    while min(cntd.values()) < per and tries < 200000:
        tries += 1
        s = cp.constructed_state(RNG.choice(cp.RULES), RNG.randint(3, 7))
        if s is None:
            continue
        typ, N, m = s
        if m > 160 or N > 2000:
            continue
        name, nxt = cp.rule(typ, N, m)
        if name is None or cntd[name] >= per:
            continue
        vis = []
        got, steps = cp.run_K_to_clean(word(typ, N), m, 4 * 10 ** 6, tt=TTP, visits=vis)
        rec('B.closed_eq_direct_TP', got == nxt, (s, name, nxt, got, steps))
        rec('B.progress_steps_ge_9_TP', steps >= 9 and nxt[2] >= m + 1, (s, steps))
        tm_states = [(ww, mm) for (ww, mm, _) in vis]
        rec('B.overflow_states_TP_eq_abstract', tm_states == cp.overflow_states(word(typ, N), m), (s, name, tm_states))
        harvest('', cp.end_checks, typ, N, m, name, nxt, tm_states, 'TP')
        vis2 = []
        got2, steps2 = run349_to_clean(word(typ, N), m, 4 * 10 ** 6, visits=vis2)
        rec('B.closed_eq_direct_349', got2 == nxt, (s, name, nxt, got2))
        rec('B.TP_and_349_same_steps_and_overflow_states', steps2 == steps and vis2 == vis, (s, steps, steps2))
        cntd[name] += 1
    for r in cp.RULES:
        rec('B.rule_exercised_large:' + r, cnt[r] >= min(target, 50), cnt[r])
        rec('B.rule_exercised_direct:' + r, cntd[r] >= per, cntd[r])


# ---------------------------------------------------------------------------------------------------------
TRANS14_TP = 'F0 A0 B1 B0 C0 D0 C0 D1 E0 A0 B0 C0 D0 C1'.split()


def sec_Z():
    # 349 from blank, first 73 steps
    R = Run(T349, [0] * 8, 4, A, size=600)
    trans = []
    first_detour = None
    for t in range(73):
        trans.append(ST[R.s] + str(R.tape[R.h]))
        R.step(1)
        if R.steps == 14:
            rec("Z.349_K'('',0,1)_at_14", same349(R, 0, 0, 1), R.cells(-10, 10))
    rec('Z.349_trans14_eq_TP_renamed', trans[:14] == [ST[FINV[ST.index(x[0])]] + x[1] for x in TRANS14_TP], ' '.join(trans[:14]))
    INFO['Z_349_trans14'] = ' '.join(trans[:14])
    rec("Z.349_K'(std2,0,2)_at_73", same349(R, std(2), 0, 2), R.cells(-15, 10))
    # TP from 0^inf F> 0^inf: the .v's init statements
    R = Run(TTP, [0] * 8, 4, F, size=600)
    tr = []
    for t in range(14):
        tr.append(ST[R.s] + str(R.tape[R.h]))
        R.step(1)
    rec('Z.TP_from_F_trans14', tr == TRANS14_TP, ' '.join(tr))
    rec('Z.TP_from_F_K(0,0,1)=K_0_0_0_1_at_14', is_cfg(R, A, *L_([], cp.Rcells(0, 1))), R.cells(-10, 10))
    # proof.md 6: the rows 15-23, 24-51, 52-73
    rows = [(9, 'A0 B1 B1 B0 C0 D0 C0 D0 C1', ([], cp.Rcells(2, 0))),
            (28, None, ([1], cp.Rcells(1, 1))),
            (22, 'A1 F0 A0 B1 B1', (wcells(std(2)), cp.Rcells(0, 2)))]
    for k, (n, tlist, (lw, rr)) in enumerate(rows):
        tr = []
        for t in range(n):
            tr.append(ST[R.s] + str(R.tape[R.h]))
            R.step(1)
        okt = tlist is None or ' '.join(tr).startswith(tlist)
        rec('Z.TP_from_F_row_%d_at_%d' % (k + 2, R.steps), okt and is_cfg(R, A, *L_(lw, rr)), (' '.join(tr), R.cells(-10, 10)))
    rec('Z.TP_from_F_K_2_0_0_2_at_73', R.steps == 73 and is_cfg(R, A, *L_(wcells(std(2)), cp.Rcells(0, 2))), R.cells(-10, 10))
    rec('Z.no_F1_in_first_73_TP', 'F1' not in R.used, sorted(R.used))
    R.step(200)
    first = None
    R2 = Run(TTP, [0] * 8, 4, F, size=900)
    for t in range(400):
        if R2.s == F and R2.tape[R2.h] == 1:
            first = t + 1
            break
        R2.step(1)
    INFO['Z_first_F1_step_TP'] = first
    # fallback: 14 steps to K 0 0 0 1, then BS_S0 with i = 0, m = 1  (K (2^0-1) 0 0 1 -->+ K 2 0 0 2)
    name, nxt = cp.rule('std', 0, 1)
    rec('Z.BS_S0(i=0,m=1)_is_S0_to_(std,2,2)', name == 'S0' and nxt == ('std', 2, 2) and (1 + 0 + 1) == 2)
    got, steps = cp.run_K_to_clean(0, 1, 10 ** 5, tt=TTP)
    rec('Z.TP_(std,0,1)_to_(std,2,2)_in_59', got == ('std', 2, 2) and steps == 59, (got, steps))
    rec('Z.I(std,2,2)_and_not_I(std,0,1)', cp.I('std', 2, 2) and not cp.I('std', 0, 1))
    # the overflow configurations of a direct 349 run from blank (all of them: clean, dirty, empty), with their
    # step numbers, vs the orbit of R1-R3 from K(0,0,1) at step 14 with TP's step formulas
    NZ = 3 * 10 ** 6 if QUICK else (3 * 10 ** 8 if FULL else 6 * 10 ** 7)
    size = 40000
    tape = bytearray(2 * size)
    h, s = size, A
    steps = 0
    seen = []
    tt = T349
    while steps < NZ:
        r = tape[h]
        a = tt[2 * s + r]
        if a is None:
            seen.append(('HALT', steps))
            break
        tape[h] = a[0]
        h += a[1]
        s = a[2]
        steps += 1
        if s == 1 and a[1] > 0 and tape[h - 1] == 1 and tape[h - 2] == 1 and tape[h - 3] == 0 and tape[h - 4] == 0:
            p = h - 5
            mm = 0
            while tape[p] == 1 and tape[p - 1] == 0:
                mm += 1
                p -= 2
            if tape[p] == 0 and tape.find(1, 0, p + 1) == -1:
                last = tape.rfind(1)
                ww = 0 if last < h else int(''.join(map(str, reversed(tape[h:last + 1]))), 2)
                seen.append((steps, ww, mm))
    # the rules' orbit
    orb = [(14, 0, 1)]
    w, m, t = 0, 1, 14
    while len(orb) < len(seen) + 1:
        kind, x, mm = cp.overflow(w, m)
        q = tz(phi(w))
        if kind == 'R2':
            t += L_TP(w) + q + 8
            w, n = x, mm
            while n > 0:
                t += L_TP(w) + 10 * n + 7
                w = phi(w)
                n -= 1
            m = mm
        elif kind == 'R3':
            t += L_TP(w) + q + 14
            w, m = x, mm
        else:
            orb.append(('HALT?', kind))
            break
        orb.append((t, w, m))
    ok = len(seen) >= 20 and seen == orb[:len(seen)] and orb[len(seen)][0] > NZ
    bad = next(((i, seen[i], orb[i]) for i in range(min(len(seen), len(orb))) if seen[i] != orb[i]), None)
    rec('Z.direct_349_overflow_configs_and_steps_eq_rules_orbit', ok, (len(seen), bad))
    ncl = sum(1 for (_, ww, _) in seen if ww and decode(ww) is not None)
    INFO['Z_orbit'] = {'steps': NZ, 'overflow_configs': len(seen), 'clean': ncl,
                       'dirty': sum(1 for (_, ww, _) in seen if ww and decode(ww) is None),
                       'empty': sum(1 for (_, ww, _) in seen if ww == 0), 'last': seen[-1][0] if seen else None}
    # the clean subsequence = the macro-rule orbit from (std,2,2) (after the empty start (std,0,1))
    clean = [(decode(ww)[0], decode(ww)[1], mm) for (_, ww, mm) in seen if ww and decode(ww) is not None]
    st = ('std', 2, 2)
    seq = [st]
    while len(seq) < len(clean):
        _, st = cp.rule(*st)
        seq.append(st)
    rec('Z.clean_subsequence_eq_macro_orbit_from_(std,2,2)', seq == clean, next(((i, seq[i], clean[i]) for i in range(len(seq)) if seq[i] != clean[i]), None))
    INFO['Z_macro_steps'] = len(clean)
    # lockstep: 349 from blank = mirror of TP from F (state renamed by f, head at minus the position, cells mirrored)
    nst = 2 * 10 ** 5 if QUICK else (5 * 10 ** 6 if FULL else 10 ** 6)
    R1 = Run(TTP, [0] * 8, 4, F, size=12000)
    R2 = Run(T349, [0] * 8, 4, A, size=12000)
    ok = True
    right1 = True          # proof.md 3.2: after step 0, whenever TP's F reads a cell, the cell on its right is 1
    t = 0
    for t in range(nst):
        R1.step(1, track=False)
        R2.step(1, track=False)
        if R1.s == F and R1.tape[R1.h + 1] != 1:
            right1 = False
        if R1.halted or R2.halted or FMAP[R2.s] != R1.s or (R1.h - R1.off - 4) != -(R2.h - R2.off - 4):
            ok = False
            break
        if t % 50000 == 49999 or t == nst - 1:
            P = 2 + max(abs(x - R.off - 4) for R in (R1, R2) for x in (R.lo, R.hi))
            if any(R1.tape[R1.off + 4 + p] != R2.tape[R2.off + 4 - p] for p in range(-P, P + 1)):
                ok = False
                break
    rec('Z.lockstep_349_eq_mirror_of_TP_from_F', ok, (t, R1.s, R2.s))
    rec('Z.TP_from_F_every_F_read_after_step_0_has_1_on_its_right', right1 and ok)
    INFO['Z_lockstep_steps'] = nst
    # lockstep: TP from F = W4-2 from F with every F1 expanded to F1 C1 A1 (evidence for proof.md 0; not used)
    nw = 3 * 10 ** 5 if QUICK else (3 * 10 ** 7 if FULL else 3 * 10 ** 6)
    size = 20000
    tw, tp = bytearray(2 * size), bytearray(2 * size)
    hw = hp = size
    sw = sp = F
    nf1 = stp = 0
    ok, bad = True, None
    for t in range(nw):
        r = tw[hw]
        a = TW[2 * sw + r]
        if sw == F and r == 1:
            if not (sp == F and hp == hw and tp[hp] == 1 and tp[hp + 1] == 1):
                ok, bad = False, ('F1 precondition', t)
                break
            for _ in range(3):
                b = TTP[2 * sp + tp[hp]]
                tp[hp] = b[0]; hp += b[1]; sp = b[2]; stp += 1
            nf1 += 1
        else:
            b = TTP[2 * sp + tp[hp]]
            tp[hp] = b[0]; hp += b[1]; sp = b[2]; stp += 1
        tw[hw] = a[0]; hw += a[1]; sw = a[2]
        if sw != sp or hw != hp:
            ok, bad = False, ('state/pos', t)
            break
    ok = ok and tw == tp
    rec('Z.lockstep_TP_from_F_eq_W42_from_F_with_F1_expanded', ok and stp == nw + 2 * nf1, (bad, stp, nw, nf1))
    INFO['Z_expand'] = {'W42_steps': nw, 'TP_steps': stp, 'F1_reads': nf1}


def sec_J():
    s = ('std', 2, 2)
    ncyc = 50000 if QUICK else (2000000 if FULL else 500000)
    cnt = {}
    ok = True
    t = 0
    for t in range(ncyc):
        if not cp.I(*s):
            ok = False
            break
        name, s = cp.rule(*s)
        if name is None:
            ok = False
            break
        cnt[name] = cnt.get(name, 0) + 1
    rec('J.orbit_from_(std,2,2)_in_I', ok, (t, s))
    INFO['J'] = {'cycles': ncyc, 'final_m': s[2], 'per_rule': cnt}


def sec_NEG():
    """off I: a halting overflow (R4) halts on 349 at F1 and on TP at E1; the F1 detour needs the 1 on its right"""
    found = 0
    tries = 0
    while found < (3 if QUICK else 10) and tries < 20000:
        tries += 1
        L = RNG.randint(3, 7)
        k = RNG.randint((1 << (L - 1)) + 1, (1 << L) - 1)
        o = k - (1 << (L - 1))
        lands = [g for g in range(tz(o) + 1, L - 1) if not (o >> g) & 1] if o else []
        if L - 2 not in lands:
            continue
        g = L - 2
        Tg = 2 * (((o >> g) << g) + (1 << g))
        m = Tg - 2 * o - 2
        if m < 1:
            continue
        N = 2 * k
        got, path = cp.abstract_B(pk(N), m)
        if got[0] != 'R4':
            continue
        rec('NEG.not_I', not cp.I('pk', N, m), (N, m))
        r1, _ = cp.run_K_to_clean(pk(N), m, 2 * 10 ** 6, tt=TTP)
        r2, _ = run349_to_clean(pk(N), m, 2 * 10 ** 6)
        rec('NEG.R4_halts_TP_E1_and_349_F1', r1 == ('HALT', (E, 1)) and r2 == ('HALT', (F, 1)), (N, m, r1, r2))
        found += 1
    rec('NEG.found_halting_examples', found >= (3 if QUICK else 10), found)
    for _ in range(200):
        l, r = rbits(RNG.randint(0, 12)), rbits(RNG.randint(0, 12))
        R = run_from(TTP, F, *L_([1] + l, [0] + r), 3)
        rec('NEG.detour_without_1_on_right_differs', not is_cfg(R, F, *L_(l, [1, 1, 0] + r)), (l, r))


# ---------------------------------------------------------------------------------------------------------
PLAN_FULL = os.path.join(HERE, 'rocq', 'plan_check_full.v')
PLAN_PHI = os.path.join(HERE, 'rocq', 'plan_check_phi.v')
PLAN_LOG = os.path.join(HERE, 'work', 'plan_check_full.log')


def sec_P():
    """proof.md 8: the whole lemma plan compiles as one file; static facts about that file; proof.md self-contained"""
    v = open(PLAN_FULL).read()
    sha = hashlib.sha256(v.encode()).hexdigest()
    INFO['plan_check_full_sha256'] = sha
    log = open(PLAN_LOG).read() if os.path.exists(PLAN_LOG) else ''
    m = re.search(r'sha256 ([0-9a-f]{64})', log)
    rec('P.plan_full_log_is_for_current_file', bool(m) and m.group(1) == sha, m and m.group(1))
    rec('P.plan_full_log_exit0_closed', 'Closed under the global context' in log and 'EXIT 0' in log
        and 'Exit status: 0' in log and 'Error' not in log)
    t = re.search(r'Elapsed \(wall clock\) time \(h:mm:ss or m:ss\): (\S+)', log)
    INFO['plan_check_full_wall'] = t and t.group(1)
    # structure: plan_check_phi.v head + W4-2's .v from PA_spec on, verbatim except init0 -> initF and the tail
    w42 = open(W42V).read()
    phi = open(PLAN_PHI).read()
    cut = 'Definition PA_spec := proj1 phi_spec.'
    rec('P.plan_full_head_is_plan_check_phi', v.index(cut) == phi.index(cut) and v[:v.index(cut)] == phi[:phi.index(cut)])
    i0, i1 = w42.index(cut), w42.index('Lemma init0: c0 -->* K 1 0 0 1.')
    i2 = w42.index('Qed.', i1) + len('Qed.')
    i3 = w42.index('Lemma nonhalt: ~halts tm c0.')
    j0, j1 = v.index(cut), v.index('Ltac solve_initF :=')
    j2 = v.index('Qed.', v.index('Lemma initF: F;; tape0 -->* K 2 0 0 2.')) + len('Qed.')
    j3 = v.index('Lemma nonhalt_F: ~halts tmP (F;; tape0).')
    rec('P.plan_full_W42_part1_verbatim', v[j0:j1] == w42[i0:i1], (j1 - j0, i1 - i0))
    rec('P.plan_full_W42_part2_verbatim', v[j2:j3] == w42[i2:i3], (j3 - j2, i3 - i2))
    rec('P.plan_full_W42_part2_has_step_I', 'Lemma step_I s: I s -> exists s\', St s -->+ St s\' /\\ I s\'.' in v[j2:j3])
    # top-level definitions and notations
    code = re.sub(r'\(\*.*?\*\)', '', v, flags=re.S)
    tms = re.findall(r'^Definition tm\s*:=\s*Eval compute in \(TM_from_str "([^"]*)"\)\.', code, flags=re.M)
    hl = open(os.path.join(ROOT, 'data', 'holdouts', 'BB6_holdouts_740.txt')).read().split('\n')
    rec('P.plan_full_one_tm_eq_740_line_349', tms == [TM349] and hl[348] == TM349
        and len(re.findall(r'^\s*Definition\s+tm\b', code, flags=re.M)) == 1, tms)
    tps = re.findall(r'^Definition tmP\s*:=\s*Eval compute in \(TM_from_str "([^"]*)"\)\.', code, flags=re.M)
    rec('P.plan_full_tmP_eq_TP', tps == [TP], tps)
    rec('P.plan_full_notations_use_tmP', re.findall(r'-\[ *tmP? *\]->', code) == ['-[ tmP ]->', '-[ tmP ]->'],
        re.findall(r'-\[ *tmP? *\]->', code))
    stmts = ['Lemma TF2 l r: [1;0] *> l <{{F}} [1] *> r -->+ l <{{A}} [1;1] *> [1] *> r.',
             'Lemma TF3 l r: [1;1] *> l <{{F}} [1] *> r -->+ l <{{F}} [1;1] *> [1] *> r.',
             "(forall e o e' o', PF e o e' o' -> forall r, WS e o <{{F}} [1] *> r -->+ WS e' o' {{B}}> [1] *> r).",
             'Lemma initF: F;; tape0 -->* K 2 0 0 2.',
             'unfold R. cbn [lpow Str_app app]. solve_initF.',
             'Lemma nonhalt_F: ~halts tmP (F;; tape0).',
             'Lemma perm_349 : Perm (flip tm) tmP f349.',
             'Lemma nonhalt: ~halts tm c0.']
    rec('P.plan_full_statements_present_once', all(code.count(x) == 1 for x in stmts),
        [x for x in stmts if code.count(x) != 1])
    fm = re.search(r'Definition f349 \(q : Q\) : Q :=\s*match q with (.*?) end\.', code, flags=re.S)
    pairs = re.findall(r'([A-F]) => ([A-F])', fm.group(1)) if fm else []
    rec('P.plan_full_f349_eq_f', sorted((ST.index(a), ST.index(b)) for a, b in pairs) == [(q, FMAP[q]) for q in range(6)],
        pairs)
    bad = re.findall(r'\b(Admitted|admit|Axiom|Parameter|Hypothesis|Conjecture|Abort|bypass_check)\b|Unset Guard Checking', code)
    rec('P.plan_full_no_forbidden_keyword', bad == [], bad)
    rec('P.plan_full_ends_with_print_assumptions', code.rstrip().endswith('Print Assumptions nonhalt.'))
    # proof.md: no citation of an internal W4-2 file outside the review log; c0 only for busycoq's start in 1
    pm = open(os.path.join(HERE, 'proof.md')).read()
    body = pm[:pm.index('## Review log')]
    cites = re.findall(r'W4-2 proof\.md|its proof\.md|W4-2 \(its|its §\d', body)
    rec('P.proof_md_no_internal_W42_citation', cites == [], cites)
    blk = body[body.index('## 1. Rule table'):body.index('## 2. Notation')]
    rec('P.proof_md_rule_block_c0_only_start', re.findall(r'\bc\d\b', blk) == ['c0'] and 'from c0 = 0^inf A> 0^inf' in blk,
        re.findall(r'\bc\d\b', blk))


def main():
    secs = [('T', sec_T), ('E', sec_E), ('TL', sec_TL), ('PS', sec_PS), ('LS', sec_LS), ('RS', sec_RS_OV),
            ('V', sec_V), ('K', sec_K), ('D', sec_D), ('M', sec_M), ('B', sec_B), ('Z', sec_Z), ('J', sec_J),
            ('NEG', sec_NEG), ('P', sec_P)]
    only = sys.argv[sys.argv.index('--only') + 1].split(',') if '--only' in sys.argv else None
    for name, fn in secs:
        if only and name not in only:
            continue
        t = time.time()
        fn()
        print('# section %s done in %.1fs' % (name, time.time() - t), flush=True)
    nfail = 0
    for cid in ORDER:
        r = RES[cid]
        st = 'PASS' if r['pass'] == r['n'] else 'FAIL'
        nfail += st == 'FAIL'
        print('%-62s %s %d/%d %s' % (cid, st, r['pass'], r['n'], r['fail'] if st == 'FAIL' else ''))
    print('INFO', json.dumps(INFO, default=str))
    print('SUMMARY %s %d/%d checks (seed %d, %s, %.0fs)' % ('PASS' if nfail == 0 else 'FAIL', len(ORDER) - nfail, len(ORDER),
                                                           SEED, 'quick' if QUICK else ('full' if FULL else 'default'),
                                                           time.time() - T0))
    return nfail


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