#!/usr/bin/env python3
"""check_proof.py for W4-2 = 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF (proof.md in this directory).

Every claim of proof.md is checked against the machine's own transition table (parsed from the string) by
direct simulation, or (for the arithmetic lemmas) by exact integer computation: exhaustive small cases plus
random large ones.  Self-contained: nothing is imported from scripts/ or tools/.

Sections (proof.md section in brackets):
  T   [1]    table facts: E1 is the only undefined transition; which transitions each low-level rule uses
  LS  [3.1]  left step L0/L1 (= phi) on the TM: all words up to length 14 (+ random long ones), random right
             contexts; exact result, step count 1 / 2|z|+3, head never right of the boundary before the exit
  RS  [3.1]  right step RS: l B> R n m -->(10n+7) l <A R (n-1) (m+1), every intermediate configuration of the
             proof.md chain; n <= 40, m <= 6 exhaustive + random large; left context untouched; TM1/TM2 agree
  OV  [3.1]  overflow OV0, CD, OVe, OVo, halt, nested: every word f up to length 13, m <= 3 (+ random long);
             exact result and step count (q+8 / q+14), halting after q+9 steps when x ends in 1
  K   [3.2]  level-1 rules R1, R2, R3, R4 on K(w,n,m) (composition), exhaustive small
  PHI [3.3]  phi (definition) = the TM's left step; phi in W(e,o) coordinates: lemma SW (i)/(ii)/(iii) with the
             landing cells, exhaustive (h <= 5, every high word up to length 6) + random (h <= 40);
             increments INC-std / INC-pk; the accelerated phij (used by the large checks) = plain iteration
  ORB [3.3]  orbit lemmas O3-O6 (closed forms of phi^j), exhaustive small parameters + random large
  X   [3.4]  overflow words: phi(std(N)) and phi(pk(N)) give x = W(0,k) / W(2^(L-1), r) / std(k) / reset
  B   [3.4]  macro rules S0-S3, P0-P4: closed form = abstract execution (R1-R4 + plain phi) exhaustively on small
             states; = abstract execution with phij on random large states; = direct TM simulation on samples;
             where a rule ends: the first clean overflow state with N >= 1 (abstract trace = direct TM's overflow
             states); the empty state (std,0,M) only inside S2/P0, once, outside I, and left by S0
  INV [4]    Lemma S (coverage: every state with I satisfies the precondition of exactly one rule, and only the
             listed rules occur) and Lemma C (closure), exhaustive for m <= MEXH and random boundary states to
             2^60; every inequality step of the hand proof as its own check
  Z   [6]    initial segment from blank: the 32-step transition list, K('',0,0) at 5, K('',1,0) at 14,
             K('1',0,1) at 32; first 1,002 overflow configurations of the stored direct C run (to 1e10 steps)
             = the rules' orbit; a fresh direct run of the first cycles
  F   [7.3]  start F (machine 349 via TM518): K('',0,1) at step 14, (std,2,2) at step 73, then inside I;
             TM518 tm = this table mirrored + renamed (F->A, A->B, ..., E->F) started in A; the Eqv_v3.v strings;
             Perm (flip TM518) table; lockstep run of TM518 from blank vs the mirror of this table from F
  J   [7]    I along the blank-tape orbit for many cycles (closed-form rules)
  NEG [5]    controls: off the invariant, the H / N landings really halt / nest on the TM
  TPL [8]    template carry-over: on std words the left step never reads F1 (TM2 LIncs), and L+OV on std words
             (TM1 ROv) gives the same run on this machine, TM1 and TM2
Usage: python3 -B check_proof.py [--seed S] [--quick] [--full]
"""
import sys, os, random, time, json

HERE = os.path.dirname(os.path.abspath(__file__))
TM = '1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF'
TM1 = '1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA0RB'     # BECv5 TM1
TM2 = '1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LB'     # BECv5 TM2
ST = 'ABCDEF'
A, B_, C, D, E, F = range(6)
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)
RES = {}
ORDER = []
T0 = time.time()


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 table(s):
    t = []
    for blk in s.split('_'):
        for r in (0, 1):
            x = blk[3 * r:3 * r + 3]
            t.append(None if x == '---' else (int(x[0]), 1 if x[1] == 'R' else -1, ST.index(x[2])))
    return t      # index 2*state + symbol


TT = table(TM)


# ----------------------------------------------------------------------------------------------------------
# direct simulator on a bytearray tape
class Run:
    def __init__(self, tt, cells, head, state, size=None):
        self.tt = tt
        n = len(cells)
        self.off = 64 + n if size is None else size
        self.tape = bytearray(2 * self.off + n + 64)
        self.tape[self.off:self.off + n] = bytes(cells)
        self.h = self.off + head
        self.s = state
        self.steps = 0
        self.used = set()
        self.lo = self.hi = self.h
        self.last = 0          # last move direction
        self.halted = None

    def step(self, k=1, track=True):
        tt, tape = self.tt, self.tape
        h, s = self.h, self.s
        for _ in range(k):
            r = tape[h]
            a = tt[2 * s + r]
            if a is None:
                self.halted = (s, r)
                break
            if track:
                self.used.add(ST[s] + str(r))
            tape[h] = a[0]
            h += a[1]
            s = a[2]
            self.last = a[1]
            self.steps += 1
            if h < self.lo: self.lo = h
            if h > self.hi: self.hi = h
        self.h, self.s = h, s
        return self.halted is None

    def cells(self, a, b):           # absolute positions relative to the original cell 0
        return list(self.tape[self.off + a:self.off + b])


def bits_to_cells(w, length=None):
    """word int (bit d = cell at offset d) -> list of cells, highest first"""
    L = w.bit_length() if length is None else length
    return [(w >> d) & 1 for d in range(L - 1, -1, -1)]


def Rcells(n, m):
    return [1] + [1, 0] * (1 + n) + [0] + [1, 0] * m


# ----------------------------------------------------------------------------------------------------------
# words: int, bit d = cell at offset d (offset 0 = the cell A reads)
def tz(x):
    return (x & -x).bit_length() - 1


def phi(w):
    """proof.md 3.3: last cell 0 -> 1; else the lowest pair of adjacent 0 cells (e, e+1) (0^inf counts):
    cell e+1 := 1, cells 0..e := 0"""
    if w & 1 == 0:
        return w | 1
    z = ~w
    p = z & (z >> 1)
    e = tz(p)
    return ((w >> (e + 2)) << (e + 2)) | (1 << (e + 1))


def spread(x):
    r = 0
    d = 0
    while x:
        if x & 1:
            r |= 1 << (2 * d)
        x >>= 1
        d += 1
    return r


def unspread(w):
    r = 0
    d = 0
    while w:
        if w & 1:
            r |= 1 << d
        w >>= 2
        d += 1
    return r


def W(e, o):
    return spread(e) | (spread(o) << 1)


def EO(w):
    return unspread(w), unspread(w >> 1)


def std(N):
    return W(N, 0)


def pk(N):
    assert N >= 2
    P = N.bit_length() - 2
    return W(N - (1 << (P + 1)), 1 << P)


def decode(w):
    e, o = EO(w)
    if o == 0:
        return ('std', e)
    if o & (o - 1) == 0:
        P = o.bit_length() - 1
        if e < (1 << (P + 1)):
            return ('pk', (1 << (P + 1)) + e)
    return None


def word(typ, N):
    return std(N) if typ == 'std' else pk(N)


def phij_plain(w, j):
    for _ in range(j):
        w = phi(w)
    return w


def phij(w, j):
    """phi^j accelerated with lemma SW(i): below a non-full counter, phi^t adds t to the E-bits"""
    while j > 0:
        e, o = EO(w)
        if o == 0:
            return W(e + j, 0)
        P = tz(o)
        c = e & ((1 << (P + 1)) - 1)
        room = (1 << (P + 1)) - 1 - c
        if j <= room:
            return W(e + j, o)
        w = phi(W(e + room, o))
        j -= room + 1
    return w


def overflow(w, m):
    """proof.md 3.2: K(w,0,m) -> ... ; f = phi(w) = x 1 0^q"""
    f = phi(w)
    q = tz(f)
    x = f >> (q + 1)
    if q % 2 == 0:
        return ('R2', x, m + 1 + q // 2)            # K(x, m+1+q/2, 0)
    if x & 3 == 0:
        return ('R3', x >> 2, m + (q + 3) // 2)     # K(x', 0, m+(q+3)/2)
    if x & 1:
        return ('R4', None, None)                   # halts
    return ('R5', None, None)                       # nested


def abstract_B(w, m, fast=False, maxc=6):
    """run R1-R4 from K(w,0,m) to the first K(w',0,m') with w' != 0 clean; returns ((typ,N,m'), path)"""
    path = []
    for _ in range(maxc):
        kind, x, mm = overflow(w, m)
        path.append(kind)
        if kind in ('R4', 'R5'):
            return (kind, None), path
        if kind == 'R2':
            w = phij(x, mm) if fast else phij_plain(x, mm)
            m = mm
        else:
            w, m = x, mm
        if w != 0:
            d = decode(w)
            if d is not None:
                return (d[0], d[1], m), path
            path.append('dirty')
        else:
            path.append('empty')
    return ('LONG', None), path


def overflow_states(w, m, maxc=6):
    """proof.md 3.4 (end of a macro step): the overflow configurations K(w',0,m') met from K(w,0,m) up to and
    including the first one whose word is clean with N >= 1 (w' != 0); list of (w', m'), or None on R4/R5/too long"""
    out = []
    for _ in range(maxc):
        kind, x, mm = overflow(w, m)
        if kind in ('R4', 'R5'):
            return None
        if kind == 'R2':
            w, m = phij_plain(x, mm), mm
        else:
            w, m = x, mm
        out.append((w, m))
        if w != 0 and decode(w) is not None:
            return out
    return None


# ----------------------------------------------------------------------------------------------------------
# proof.md 3.4: the macro rules (closed forms)
def params(N):
    i = tz(~N)                  # trailing 1 bits (N = 0 -> 0)
    k = N >> (i + 1)
    return i, k


def ispow2(x):
    return x > 0 and x & (x - 1) == 0


def rule(typ, N, m):
    """(name, next state) for the clean state (typ, N, m), or (None, reason) when no rule's precondition holds"""
    i, k = params(N)
    b = 1 + i + m
    if typ == 'std':
        if k == 0:
            return 'S0', ('std', b, b)
        L = k.bit_length()
        if ispow2(k) or 2 * k + b >= 1 << (L + 1):
            return 'S1', ('pk', 2 * k + b, b)
        T = 2 * k + b + 1
        if T == 1 << (L + 1):
            return 'S2', ('std', b + L + 3, b + L + 3)
        if not (k >> (L - 2)) & 1 and 3 << (L - 1) < T < 1 << (L + 1):
            v = T - (3 << (L - 1))
            u = tz(v); h = L - 2 - u; g = v >> (u + 1); n = b + 1 + u
            if g == 0:
                return 'S3a', ('std', (3 << h) + n, n)
            if n >= (1 << (h + 1)) - 2 * g:
                return 'S3b', ('std', (1 << (h + 1)) + 2 * g + n, n)
            return None, 'S3 merge after the overflow'
        return None, 'std dirty outside the final gap'
    if N < 2:
        return None, 'pk N<2'
    if k == 0:
        return 'P0', ('std', b + 1, b + 1)
    if ispow2(k):
        return 'P1', ('std', k + b, b)
    L = k.bit_length()
    r = k - (1 << (L - 1))
    T = 2 * r + b + 1
    if T - 1 >= 1 << L:
        return 'P2', ('std', 2 * r + b, b)
    if T == 1 << L:
        return 'P3', ('std', b + 1 + L, b + 1 + L)
    if r < 1 << (L - 2) and 1 << (L - 1) < T < 1 << L:
        v = T - (1 << (L - 1))
        u = tz(v); h = L - 2 - u; g = v >> (u + 1); n = b + 1 + u
        if g == 0:
            return 'P4a', ('pk', (3 << h) + n, n)
        if n >= (1 << (h + 1)) - 2 * g:
            return 'P4b', ('pk', (1 << (h + 1)) + 2 * g + n, n)
        return None, 'P4 merge after the overflow'
    return None, 'pk dirty outside the final gap'


RULES = ['S0', 'S1', 'S2', 'S3a', 'S3b', 'P0', 'P1', 'P2', 'P3', 'P4a', 'P4b']


# proof.md 4: the invariant
def I(typ, N, m):
    if m < 1 or N < m:
        return False
    if typ == 'pk' and N < 2:
        return False
    if (N - m) % 2 == 0:
        if typ == 'std':
            return 2 * N <= 3 * m + 6 if N % 2 == 0 else N <= 2 * m + 3
        return N <= 2 * m + 3 if N % 2 == 0 else 2 * N <= 5 * m + 6
    return N <= m + 3


def Nmax(typ, m):
    """largest N with I(typ, N, m) (for enumeration)"""
    return max(N for N in range(m, 3 * m + 8) if I(typ, N, m)) if m < 64 else int(2.5 * m) + 8


# ----------------------------------------------------------------------------------------------------------
# direct TM runs of the low-level rules
def K_cells(w, n, m, wl=None):
    wc = bits_to_cells(w, wl)
    return wc, Rcells(n, m)


def run_K_to_clean(w, m, max_steps, tt=TT, visits=None):
    """direct TM run from K(w,0,m) to the first K(w',0,m') with w' != 0 a clean counter; returns ((typ,N,m'), steps).
    If `visits` is a list, every overflow configuration K(w',0,m') met on the way (dirty, empty and the final clean
    one) is appended to it as (w', m', steps)."""
    wc = bits_to_cells(w)
    rc = Rcells(0, m)
    size = 8 * (len(wc) + m) + 400
    R = Run(tt, wc + rc, len(wc) - 1, A, size=size)
    tape = R.tape
    tt_ = R.tt
    h, s = R.h, R.s
    steps = 0
    while steps < max_steps:
        r = tape[h]
        a = tt_[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 == 0 and a[1] < 0 and tape[h + 1] == 1 and tape[h + 2] == 1 and tape[h + 3] == 0 and tape[h + 4] == 0:
            # parse 1 1 0 0 (10)^m' 0^inf
            p = h + 5
            mm = 0
            while tape[p] == 1 and tape[p + 1] == 0:
                mm += 1
                p += 2
            if tape[p] == 0 and not any(tape[p:p + 2 * (len(wc) + m) + 300]):
                lw = 0
                q = h
                # left word: cells up to the leftmost nonzero
                first = tape.find(1)
                if first == -1 or first > h:
                    ww = 0
                else:
                    ww = int(''.join(map(str, tape[first:h + 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_T():
    halts = [ST[i // 2] + str(i % 2) for i, a in enumerate(TT) if a is None]
    rec('T.only_E1_undefined', halts == ['E1'], halts)
    t1, t2 = table(TM1), table(TM2)
    diff1 = [ST[i // 2] + str(i % 2) for i in range(12) if t1[i] != TT[i]]
    diff2 = [ST[i // 2] + str(i % 2) for i in range(12) if t2[i] != TT[i]]
    rec('T.TM1_TM2_differ_only_in_F1', diff1 == ['F1'] and diff2 == ['F1'], (diff1, diff2))


def rand_word(lo, hi):
    L = RNG.randint(lo, hi)
    return RNG.getrandbits(L) if L else 0


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 (2|z|+3 steps)"""
    maxlen = 11 if QUICK else 14
    words = list(range(1 << maxlen)) + [rand_word(15, 90) for _ in range(300 if QUICK else 3000)]
    used = set()
    for w in words:
        wl = max(w.bit_length(), 1)
        wc = bits_to_cells(w, wl)
        ctx = [RNG.randint(0, 1) for _ in range(RNG.randint(0, 8))]
        pad = 4
        cells = [0] * pad + wc + ctx
        R = Run(TT, cells, pad + wl - 1, A)
        p0 = pad + wl - 1
        ok = True
        while R.step():
            if R.h - R.off > p0:          # crossed the boundary to the right
                break
        if R.halted:
            rec('LS.no_halt', False, w)
            continue
        got = R.cells(-60, p0 + 1)
        exp_w = phi(w)
        expc = bits_to_cells(exp_w, 60 + p0 + 1)
        okw = got == expc
        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:
            st_ok = R.steps == 1
            rec('LS.L0', okw and okc and st_ok, (w, R.steps))
        else:
            z_len = tz(~w ^ 0) if False else None
            # |z| = e where (e, e+1) is the lowest 00 pair
            zz = ~w
            e = tz(zz & (zz >> 1))
            st_ok = R.steps == 2 * e + 3
            rec('LS.L1', okw and okc and st_ok, (bin(w), R.steps, e))
        used |= R.used
        rec('LS.no_halt', True)
    rec('LS.transitions_used', used <= {'A0', 'A1', 'F0', 'F1', 'B1'}, sorted(used))


def rs_chain(n, m, lw):
    """the proof.md 3.1 chain for RS, as (steps, cells from the boundary cell's right neighbour, state, head offset)
    head offset: position relative to the first cell right of the boundary (0) ; X = (10)^m"""
    X = [1, 0] * m
    ch = []
    # l B> 1 1 0 (10)^n 0 X
    ch.append((0, [1, 1, 0] + [1, 0] * n + [0] + X, B_, 0))
    # l 0 0 0 C> (10)^n 0 X
    ch.append((3, [0, 0, 0] + [1, 0] * n + [0] + X, C, 3))
    # l 0 0 (10)^n 0 C> 0 X
    ch.append((3 + 4 * n, [0, 0] + [1, 0] * n + [0, 0] + X, C, 2 * n + 3))
    # l 0 (01)^(n-1) <A 0 0 0 1 0 X       (A reads the last cell of "0 (01)^(n-1)")
    ch.append((8 + 4 * n, [0] + [0, 1] * (n - 1) + [0, 0, 0, 1, 0] + X, A, 2 * n - 2))
    # l 0 <A (11)^(n-1) 0 0 0 1 0 X
    ch.append((8 + 4 * n + 2 * (n - 1), [0] + [1, 1] * (n - 1) + [0, 0, 0, 1, 0] + X, A, 0))
    # l 1 0^(2n-1) C> 0 0 1 0 X
    ch.append((8 + 4 * n + 2 * (n - 1) + 2 * n, [1] + [0] * (2 * n - 1) + [0, 0, 1, 0] + X, C, 2 * n))
    # l 1 0 <D (01)^(n-1) 0 0 1 0 X
    ch.append((8 + 4 * n + 2 * (n - 1) + 2 * n + 2 * n - 1, [1, 0] + [0, 1] * (n - 1) + [0, 0, 1, 0] + X, D, 1))
    # l <A 1 1 (01)^(n-1) 0 0 1 0 X  = l <A R (n-1) (m+1)
    ch.append((10 * n + 7, Rcells(n - 1, m + 1), A, -1))
    return ch


def sec_RS():
    nmax = 25 if QUICK else 40
    cases = [(n, m) for n in range(1, nmax + 1) for m in range(0, 7)]
    cases += [(RNG.randint(1, 400), RNG.randint(0, 400)) for _ in range(30 if QUICK else 200)]
    used = set()
    for n, m in cases:
        lw = [RNG.randint(0, 1) for _ in range(RNG.randint(0, 10))]
        rc = Rcells(n, m)
        cells = lw + rc
        b0 = len(lw)                     # absolute index of the first right cell
        chain = rs_chain(n, m, lw)
        R = Run(TT, cells, b0, B_)
        okall = True
        for (st, exp, state, hoff) in chain:
            R.step(st - R.steps)
            got = R.cells(b0, b0 + len(exp) + 4)
            ok = got == exp + [0] * 4 and R.s == state and R.h - R.off == b0 + hoff and R.cells(0, b0) == lw
            if not ok:
                okall = False
                rec('RS.chain', False, (n, m, st, got[:30], ST[R.s], R.h - R.off - b0))
                break
        if okall:
            rec('RS.chain', True)
            rec('RS.left_untouched', R.lo - R.off >= b0 - 1 and R.cells(0, b0) == lw, (n, m))
        used |= R.used
        # TM1, TM2: the same run
        for name, tm in (('TM1', TM1), ('TM2', TM2)):
            if n <= 12 or RNG.random() < 0.1:
                R2 = Run(table(tm), cells, b0, B_)
                R2.step(10 * n + 7)
                rec('RS.same_on_' + name, R2.cells(b0, b0 + len(rc) + 4) == Rcells(n - 1, m + 1) + [0] * 4 and R2.s == A
                    and R2.h - R2.off == b0 - 1, (n, m))
    rec('RS.transitions_used', 'F1' not in used and 'E1' not in used, sorted(used))


def sec_OV():
    maxlen = 10 if QUICK else 13
    fs = list(range(1, 1 << maxlen)) + [rand_word(14, 80) | 1 << RNG.randint(0, 3) for _ in range(300 if QUICK else 2000)]
    used = {}
    for f in fs:
        for m in (range(0, 4) if f < (1 << maxlen) else [RNG.randint(0, 50)]):
            q = tz(f)
            x = f >> (q + 1)
            fl = f.bit_length()
            fc = bits_to_cells(f, fl)
            rc = Rcells(0, m)
            pad = 6
            cells = [0] * pad + fc + rc
            b0 = pad + fl
            R = Run(TT, cells, b0, B_)
            # OV0: 7 steps to f <C (10)^(m+2)
            R.step(7)
            ok0 = (R.s == C and R.h - R.off == b0 - 1 and R.cells(b0, b0 + 2 * (m + 2) + 4) == [1, 0] * (m + 2) + [0] * 4
                   and R.cells(0, b0) == [0] * pad + fc)
            rec('OV.OV0', ok0, (bin(f), m))
            if q % 2 == 0:
                u = q // 2
                # CD^u : x 1 <C (10)^u Y   after 2u more steps
                R.step(2 * u)
                okc = R.s == C and R.h - R.off == b0 - 1 - q and R.cells(b0 - q, b0) == [1, 0] * u
                rec('OV.CD', okc, (bin(f), m))
                R.step(1)
                exp_r = Rcells(u + m + 1, 0)
                ok = (R.s == A and R.h - R.off == b0 - q - 2 and R.steps == q + 8
                      and R.cells(b0 - q - 1, b0 - q - 1 + len(exp_r) + 4) == exp_r + [0] * 4
                      and R.cells(0, b0 - q - 1) == bits_to_cells(x, b0 - q - 1))
                rec('OV.OVe', ok, (bin(f), m))
            else:
                u = (q - 1) // 2
                R.step(2 * u)
                okc = R.s == C and R.h - R.off == b0 - 1 - 2 * u and R.cells(b0 - 2 * u, b0) == [1, 0] * u
                rec('OV.CD', okc, (bin(f), m))
                R.step(2)          # C0, D1 -> x <E 0 0 (10)^u Y
                oke = R.s == E and R.h - R.off == b0 - q - 2 and R.cells(b0 - q - 1, b0 - q + 1) == [0, 0]
                rec('OV.OVo_to_E', oke, (bin(f), m))
                if x & 1:
                    R.step(1)
                    rec('OV.halt_when_x_ends_in_1', R.halted == (E, 1) and R.steps == q + 8, (bin(f), m, R.steps))
                elif x & 3 == 0:
                    R.step(6)
                    exp_r = Rcells(0, m + (q + 3) // 2)
                    ok = (R.s == A and R.h - R.off == b0 - q - 4 and R.steps == q + 14
                          and R.cells(b0 - q - 3, b0 - q - 3 + len(exp_r) + 4) == exp_r + [0] * 4
                          and R.cells(0, b0 - q - 3) == bits_to_cells(x >> 2, b0 - q - 3))
                    rec('OV.OVo_reset', ok, (bin(f), m))
                else:
                    R.step(2)      # E0, A1 -> F reading the cell left of x's last two cells
                    rec('OV.nested_enters_F_scan', R.s == F and R.h - R.off == b0 - q - 4 and R.halted is None, (bin(f), m))
            used.setdefault('all', set()).update(R.used)


def sec_K():
    """R1 and the overflow rules at the level of K configurations (composition of L, RS, OV)"""
    for w in range(0, 1 << (9 if QUICK else 11)):
        for n, m in ((1, 0), (2, 1), (3, 2), (1, 5)):
            wl = max(w.bit_length(), 1)
            pad = 6
            cells = [0] * pad + bits_to_cells(w, wl) + Rcells(n, m)
            b0 = pad + wl
            R = Run(TT, cells, b0 - 1, A)
            zz = ~w
            e = tz(zz & (zz >> 1))
            sl = 1 if w & 1 == 0 else 2 * e + 3
            R.step(sl + 10 * n + 7)
            pw = phi(w)
            ok = (R.s == A and R.h - R.off == b0 - 1 and R.cells(b0, b0 + 2 * (n + m) + 8) == Rcells(n - 1, m + 1) + [0] * 4
                  and R.cells(0, b0) == bits_to_cells(pw, b0))
            rec('K.R1', ok, (bin(w), n, m))
        for m in (0, 1, 3):
            kind, x, mm = overflow(w, m)
            wl = max(w.bit_length(), 1)
            pad = 6
            cells = [0] * pad + bits_to_cells(w, wl) + Rcells(0, m)
            b0 = pad + wl
            R = Run(TT, cells, b0 - 1, A)
            f = phi(w)
            q = tz(f)
            zz = ~w
            e = tz(zz & (zz >> 1))
            sl = 1 if w & 1 == 0 else 2 * e + 3
            if kind == 'R2':
                R.step(sl + q + 8)
                bp = b0 - q - 1          # new boundary (first right cell)
                ok = (R.s == A and R.h - R.off == bp - 1 and R.cells(bp, bp + 2 * mm + 8) == Rcells(mm, 0) + [0] * 4
                      and R.cells(0, bp) == bits_to_cells(x, bp))
                rec('K.R2', 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) == Rcells(0, mm) + [0] * 4
                      and R.cells(0, bp) == bits_to_cells(x, bp))
                rec('K.R3', ok, (bin(w), m))
            elif kind == 'R4':
                R.step(sl + q + 9)
                rec('K.R4_halts', R.halted == (E, 1), (bin(w), m))
            else:
                rec('K.R5_seen', True)


def sec_PHI():
    # SW: Hi high word, low part of 2h cells: E-bits c < 2^(tz(o)+1), O-bits 1 <= o < 2^h
    hmax = 4 if QUICK else 5
    his = list(range(0, 1 << (5 if QUICK else 6)))
    for h in range(1, hmax + 1):
        for o in range(1, 1 << h):
            P = tz(o)
            for c in range(0, 1 << (P + 1)):
                for Hi in his:
                    sw_one(Hi, h, o, c)
    for _ in range(3000 if QUICK else 30000):
        h = RNG.randint(1, 40)
        o = RNG.randint(1, (1 << h) - 1)
        if RNG.random() < 0.3:
            o = (1 << h) - (1 << RNG.randint(0, h - 1))       # full run up to h-1: case (iii) reachable
        P = tz(o)
        c = RNG.choice([(1 << (P + 1)) - 1, RNG.randint(0, (1 << (P + 1)) - 1)])
        Hi = rand_word(0, 40)
        sw_one(Hi, h, o, c)
    # increments
    for N in list(range(0, 1 << (10 if QUICK else 13))) + [RNG.getrandbits(RNG.randint(1, 200)) for _ in range(5000)]:
        rec('PHI.INC_std', phi(std(N)) == std(N + 1), N)
        if N >= 2:
            rec('PHI.INC_pk', phi(pk(N)) == pk(N + 1), N)
    # the string definition in proof.md 3.3 (lowest 00 pair) = bit version; also phi never yields 0
    for w in range(0, 1 << 12):
        s = '00' + (bin(w)[2:] if w else '')
        if s[-1] == '0':
            t = s[:-1] + '1'
        else:
            e = s.rfind('00')
            t = s[:e] + '1' + '0' * (len(s) - e - 1)
        rec('PHI.string_definition', int(t, 2) == phi(w), w)
    # constants used in proof.md 3.3 (SW iii for the four high words) and the pk examples of proof.md 2
    rec('PHI.constants', [bin(phi(int(x, 2)))[2:] for x in ('1', '11', '1011', '111')] == ['100', '1000', '100000', '10000'])
    rec('PHI.pk_examples', bin(pk(6))[2:] == '1100' and bin(pk(7))[2:] == '1101' and pk(6) == W(2, 2))
    # phij (accelerated, used only by the large random checks) = plain iteration
    for _ in range(400 if QUICK else 3000):
        w = rand_word(0, 24)
        j = RNG.randint(0, 3000)
        rec('PHI.phij_eq_plain', phij(w, j) == phij_plain(w, j), (w, j))


def sw_one(Hi, h, o, c):
    w = (Hi << (2 * h)) | W(c, o)
    P = tz(o)
    pw = phi(w)
    if c + 1 < 1 << (P + 1):
        rec('PHI.SW_i', pw == (Hi << (2 * h)) | W(c + 1, o), (Hi, h, o, c))
    elif o + (1 << P) < 1 << h:
        o2 = o + (1 << P)
        g = tz(o2)
        ok = pw == (Hi << (2 * h)) | W(0, o2)
        # landing: lowest 1 at offset 2g+1; the two cells above it (offsets 2g+3, 2g+2)
        ok2 = tz(pw) == 2 * g + 1
        above = ((pw >> (2 * g + 3)) & 1, (pw >> (2 * g + 2)) & 1)
        if g + 1 < h:
            exp_above = ((o >> (g + 1)) & 1, 0)
        else:
            exp_above = ((Hi >> 1) & 1, Hi & 1)
        rec('PHI.SW_ii', ok and ok2 and above == exp_above, (Hi, h, o, c, above, exp_above))
    else:
        rec('PHI.SW_iii', pw == (phi((Hi << 1) | 1) << (2 * h - 1)), (Hi, h, o, c))


def sec_ORB():
    """O3-O6"""
    def chk_std_gen1(k, jmax):
        L = k.bit_length()
        x = W(0, k)
        w = x
        top = 1 << (L + 1)
        for j in range(0, jmax + 1):
            T = 2 * k + j
            if T >= top:
                if w != pk(T):
                    return ('pk', k, j)
            if L >= 2 and not ispow2(k) and not (k >> (L - 2)) & 1 and 3 << (L - 1) <= T < top:
                if w != W(T - (3 << (L - 1)), 3 << (L - 2)):
                    return ('gap', k, j)
            if ispow2(k) and w != pk(T):
                return ('pow2', k, j)
            w = phi(w)
        return None

    def chk_pk_gen1(k, jmax):
        L = k.bit_length()
        r = k - (1 << (L - 1))
        w = W(1 << (L - 1), r)
        for j in range(0, jmax + 1):
            T = 2 * r + j
            if T >= 1 << L and w != std(T):
                return ('std', k, j)
            if L >= 3 and 1 <= r < 1 << (L - 2) and 1 << (L - 1) <= T < 1 << L:
                if w != W((1 << (L - 1)) + T - (1 << (L - 1)), 1 << (L - 2)):
                    return ('gap', k, j)
            w = phi(w)
        return None

    def chk_gen2(typ, h, g, jmax):
        x = W(3 << h, g) if typ == 'std' else W(1 << h, (1 << h) + g)
        w = x
        j0 = (1 << (h + 1)) - 2 * g
        for j in range(0, jmax + 1):
            if g == 0:
                exp = std((3 << h) + j) if typ == 'std' else pk((3 << h) + j)
                if w != exp:
                    return (typ, h, g, j)
            elif j >= j0:
                exp = std((1 << (h + 1)) + 2 * g + j) if typ == 'std' else pk((1 << (h + 1)) + 2 * g + j)
                if w != exp:
                    return (typ, h, g, j)
            w = phi(w)
        return None

    kmax = 1 << (7 if QUICK else 9)
    for k in range(1, kmax):
        L = k.bit_length()
        r = chk_std_gen1(k, (1 << (L + 1)) + 20 - 2 * k)
        rec('ORB.O3_std_gen1', r is None, r)
        if k >= 2 and not ispow2(k):
            r = chk_pk_gen1(k, (1 << L) + 20)
            rec('ORB.O4_pk_gen1', r is None, r)
    for h in range(0, 8 if QUICK else 10):
        for g in range(0, 1 << h):
            for typ in ('std', 'pk'):
                r = chk_gen2(typ, h, g, (1 << (h + 2)) + 10)
                rec('ORB.O5O6_gen2', r is None, r)
    # random large: phij (validated against plain phi) at random j
    for _ in range(2000 if QUICK else 20000):
        L = RNG.randint(2, 60)
        k = RNG.randint((1 << (L - 1)) + 1, (1 << L) - 1)
        j = RNG.randint(0, 1 << (L + 2))
        T = 2 * k + j
        wj = phij(W(0, k), j)
        if T >= 1 << (L + 1):
            rec('ORB.O3_large', wj == pk(T), (k, j))
        elif not (k >> (L - 2)) & 1 and T >= 3 << (L - 1):
            rec('ORB.O3_large', wj == W(T - (3 << (L - 1)), 3 << (L - 2)), (k, j))
        if L >= 3:
            r = RNG.randint(1, (1 << (L - 1)) - 1)
            kk = (1 << (L - 1)) + r
            T = 2 * r + j
            wj = phij(W(1 << (L - 1), r), j)
            if T >= 1 << L:
                rec('ORB.O4_large', wj == std(T), (kk, j))
            elif r < 1 << (L - 2) and T >= 1 << (L - 1):
                rec('ORB.O4_large', wj == W(T, 1 << (L - 2)), (kk, j))
        h = RNG.randint(0, 60)
        g = RNG.randint(0, max(0, (1 << h) - 1))
        j = RNG.randint((1 << (h + 1)) - 2 * g, (1 << (h + 3)))
        for typ in ('std', 'pk'):
            x = W(3 << h, g) if typ == 'std' else W(1 << h, (1 << h) + g)
            wj = phij(x, j)
            V = ((3 << h) if g == 0 else (1 << (h + 1)) + 2 * g) + j
            rec('ORB.O5O6_large', wj == (std(V) if typ == 'std' else pk(V)), (typ, h, g, j))


def sec_X():
    """the overflow decomposition of clean words (proof.md 3.4)"""
    Ns = list(range(0, 1 << (10 if QUICK else 13))) + [RNG.getrandbits(RNG.randint(2, 120)) for _ in range(5000)]
    for N in Ns:
        i, k = params(N)
        for typ in ('std', 'pk'):
            if typ == 'pk' and N < 2:
                continue
            f = phi(word(typ, N))
            q = tz(f)
            x = f >> (q + 1)
            if typ == 'std':
                rec('X.std', q == 2 * i and x == W(0, k), N)
            else:
                if k == 0:
                    rec('X.pk_allones', q % 2 == 1 and x == 0 and (q + 3) // 2 == i + 1, N)
                else:
                    L = k.bit_length()
                    r = k - (1 << (L - 1))
                    rec('X.pk', q == 2 * i and x == W(1 << (L - 1), r), N)
                    if r == 0:
                        rec('X.pk_pow2_is_std', x == std(k), N)


def sec_B():
    """macro rules: closed form vs abstract execution; vs direct TM"""
    seen = {r: 0 for r in RULES}
    # exhaustive small: every clean state with m <= M1, N <= 3m+8 for which a rule applies
    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 = rule(typ, N, m)
                if name is None:
                    continue
                got, path = abstract_B(word(typ, N), m)
                rec('B.closed_eq_abstract_small', got == nxt, (typ, N, m, name, nxt, got, path))
                seen[name] += 1
                end_checks(typ, N, m, name, nxt, overflow_states(word(typ, N), m), 'abstract')
    for r in RULES:
        rec('B.rule_exercised_small:' + r, seen[r] > 0, seen[r])
    # random large: abstract with phij
    cnt = {r: 0 for r in RULES}
    tries = 0
    target = 300 if QUICK else 3000
    while min(cnt.values()) < target and tries < 400000:
        tries += 1
        typ = RNG.choice(('std', 'pk'))
        name_t = RNG.choice(RULES)
        s = constructed_state(name_t, RNG.randint(6, 60))
        if s is None:
            continue
        typ, N, m = s
        name, nxt = rule(typ, N, m)
        if name is None or cnt[name] >= target:
            continue
        got, path = abstract_B(word(typ, N), m, fast=True)
        rec('B.closed_eq_abstract_large', got == nxt, (typ, N, m, name, nxt, got, path))
        cnt[name] += 1
    for r in RULES:
        rec('B.rule_exercised_large:' + r, cnt[r] >= min(target, 50), cnt[r])
    # direct TM
    per = 6 if QUICK else 30
    cntd = {r: 0 for r in RULES}
    tries = 0
    while min(cntd.values()) < per and tries < 200000:
        tries += 1
        name_t = RNG.choice(RULES)
        s = constructed_state(name_t, RNG.randint(3, 7))
        if s is None:
            continue
        typ, N, m = s
        if m > 160 or N > 2000:
            continue
        name, nxt = rule(typ, N, m)
        if name is None or cntd[name] >= per:
            continue
        vis = []
        got, steps = run_K_to_clean(word(typ, N), m, 4 * 10 ** 6, visits=vis)
        rec('B.closed_eq_TM', got == nxt, (typ, N, m, name, nxt, got, steps))
        tm_states = [(ww, mm) for (ww, mm, _) in vis]
        rec('B.overflow_states_TM_eq_abstract', tm_states == overflow_states(word(typ, N), m), (typ, N, m, name, tm_states))
        end_checks(typ, N, m, name, nxt, tm_states, 'TM')
        cntd[name] += 1
    for r in RULES:
        rec('B.rule_exercised_TM:' + r, cntd[r] >= per, cntd[r])


def end_checks(typ, N, m, name, nxt, states, how):
    """proof.md 3.4 (where a macro step ends): it ends at the first overflow state whose word is clean with N >= 1;
    the only clean overflow state with N = 0 met inside a macro rule is (std,0,M) = K(0^inf,0,M), exactly once and
    only in S2 (M = b+L+2) and P0 (M = b); it is outside I, and S0 applied to it gives the result of S2 / P0"""
    if states is None:
        rec('B.end_first_clean_N>=1_' + how, False, (typ, N, m, name, 'R4/R5/long'))
        return
    last_ok = states[-1] == (word(nxt[0], nxt[1]), nxt[2])
    inner_ok = all(w == 0 or decode(w) is None for (w, _) in states[:-1])
    rec('B.end_first_clean_N>=1_' + how, last_ok and inner_ok, (typ, N, m, name, states))
    empties = [mm for (w, mm) in states if w == 0]
    if name not in ('S2', 'P0'):
        rec('B.empty_state_only_in_S2_P0_' + how, empties == [], (typ, N, m, name, states))
        return
    i, k = params(N)
    b = m + 1 + i
    M = b + k.bit_length() + 2 if name == 'S2' else b
    rec('B.S2_P0_pass_(std,0,M)_once_' + how, empties == [M], (typ, N, m, name, M, states))
    rec('B.S2_P0_(std,0,M)_not_I_then_S0_' + how, not I('std', 0, M) and rule('std', 0, M) == ('S0', nxt), (name, M, nxt))


def constructed_state(name, Lmax):
    """a random clean state for which rule `name` should apply (used to exercise rare cases)"""
    R = RNG
    if name == 'S0':
        i = R.randint(0, Lmax); return ('std', (1 << i) - 1, R.randint(0, 1 << Lmax))
    if name in ('S1', 'S2', 'S3a', 'S3b'):
        L = R.randint(2, Lmax)
        i = R.randint(0, 2)
        if name == 'S1':
            k = R.randint(1 << (L - 1), (1 << L) - 1)
            b = R.randint(max(1 + i, (1 << (L + 1)) - 2 * k), (1 << (L + 2)))
        elif name == 'S2':
            k = R.randint((1 << (L - 1)) + 1, (1 << L) - 1)
            b = (1 << (L + 1)) - 1 - 2 * k
        else:
            if L < 2: return None
            k = R.randint((1 << (L - 1)) + 1, (3 << (L - 2)) - 1) if L >= 3 else None
            if k is None: return None
            T = R.randint((3 << (L - 1)) + 1, (1 << (L + 1)) - 1)
            b = T - 1 - 2 * k
        m = b - 1 - i
        if m < 0: return None
        return ('std', ((2 * k + 1) << i) - 1, m)
    if name == 'P0':
        i = R.randint(2, Lmax); return ('pk', (1 << i) - 1, R.randint(0, 1 << Lmax))
    L = R.randint(1, Lmax)
    i = R.randint(0, 2)
    if name == 'P1':
        k = 1 << (L - 1)
        b = R.randint(1 + i, 1 << (L + 2))
    else:
        if L < 2: return None
        r = R.randint(1, (1 << (L - 1)) - 1)
        if name == 'P2':
            b = R.randint(max(1 + i, (1 << L) - 2 * r), 1 << (L + 2))
        elif name == 'P3':
            b = (1 << L) - 1 - 2 * r
        else:
            if L < 3: return None
            r = R.randint(1, (1 << (L - 2)) - 1)
            T = R.randint((1 << (L - 1)) + 1, (1 << L) - 1)
            b = T - 1 - 2 * r
        k = (1 << (L - 1)) + r
    m = b - 1 - i
    if m < 0: return None
    N = ((2 * k + 1) << i) - 1
    if N < 2: return None
    return ('pk', N, m)


# ----------------------------------------------------------------------------------------------------------
def lemmaS_claims(typ, N, m):
    """the inequality steps of proof.md 4.2 (Lemma S) for one state with I; returns list of (id, ok)"""
    out = []
    i, k = params(N)
    b = 1 + i + m
    P = (N - m) % 2 == 0
    if typ == 'std' and k >= 1 and not ispow2(k):
        L = k.bit_length()
        T = 2 * k + b + 1
        dirty = T < 1 << (L + 1)
        if dirty:
            out.append(('S.std_dirty_needs_i0_P', i == 0 and P))
            if i == 0 and P:
                out.append(('S.std_3T_ge_10k', 3 * T >= 10 * k))
                out.append(('S.std_bitL-2_zero', not (k >> (L - 2)) & 1))
                out.append(('S.std_T_gt_3*2^(L-1)', T > 3 << (L - 1)))
                out.append(('S.std_m_ge_(2^(L+1)-2)/3', 3 * m >= (1 << (L + 1)) - 2))
                v = T - (3 << (L - 1))
                out.append(('S.std_v_even', v % 2 == 0))
                u = tz(v)
                n = b + 1 + u
                out.append(('S.std_n_gt_2^(L-1)', n > 1 << (L - 1)))
    if typ == 'pk' and k >= 1 and not ispow2(k):
        L = k.bit_length()
        r = k - (1 << (L - 1))
        T = 2 * r + b + 1
        dirty = T < 1 << L
        if dirty:
            out.append(('S.pk_dirty_needs_P_i<=1', P and i <= 1))
            if P and i <= 1:
                out.append(('S.pk_r_lt_2^(L-2)', r < 1 << (L - 2)))
                out.append(('S.pk_T_gt_2^(L-1)', T > 1 << (L - 1)))
                v = T - (1 << (L - 1))
                out.append(('S.pk_v_even', v % 2 == 0))
                u = tz(v)
                n = b + 1 + u
                out.append(('S.pk_n_gt_2^(L-1)', n > 1 << (L - 1)))
                if i == 0:
                    out.append(('S.pk_i0_m_ge_k-1', m >= k - 1))
                    out.append(('S.pk_i0_3r_lt_2^(L-1)', 3 * r + (1 << (L - 1)) + 1 <= T))
                else:
                    out.append(('S.pk_i1_5m_ge_8k-4', 5 * m >= 8 * k - 4))
    return out


def lemmaC_claims(typ, N, m, name, nxt):
    """proof.md 4.3 (Lemma C) bounds per rule: D = N'-m' and the class it lands in"""
    out = []
    t2, N2, m2 = nxt
    D = N2 - m2
    out.append(('C.D_ge_0', D >= 0))
    i, k = params(N)
    if name in ('S0', 'S2', 'P0', 'P3'):
        out.append(('C.D_eq_0:' + name, D == 0))
    if name == 'S1':
        out.append(('C.S1_D_eq_2k', D == 2 * k))
    if name == 'P1':
        out.append(('C.P1_D_eq_k', D == k))
        if k >= 2 and i >= 1 and P_of(N, m) and (N2 % 2 == 0):
            out.append(('C.P1_i_even_ge2_when_Nprime_even', i % 2 == 0 and i >= 2))
    if name == 'P2':
        L = k.bit_length()
        r = k - (1 << (L - 1))
        out.append(('C.P2_D_eq_2r_lt_k', D == 2 * r and 2 * r < k))
    if name in ('S3a', 'S3b', 'P4a', 'P4b'):
        b = 1 + i + m
        if typ == 'std':
            L = k.bit_length(); T = 2 * k + b + 1; v = T - (3 << (L - 1))
        else:
            L = k.bit_length(); r = k - (1 << (L - 1)); T = 2 * r + b + 1; v = T - (1 << (L - 1))
        u = tz(v)
        h = L - 2 - u
        out.append(('C.gen2_u_ge_1', u >= 1))
        out.append(('C.gen2_D_lt_2^(L-u)', D < 1 << (L - u)))
        out.append(('C.gen2_D_odd_only_D3', D % 2 == 0 or (D == 3 and h == 0)))
        out.append(('C.gen2_n_parity_eq_u_parity', (m2 - u) % 2 == 0))
    return out


def P_of(N, m):
    return (N - m) % 2 == 0


def check_state(typ, N, m, abstract=None):
    name, nxt = rule(typ, N, m)
    rec('INV.S_rule_applies', name is not None, (typ, N, m, nxt))
    if name is None:
        return None
    # which rules occur under I: the dirty ones only from the listed kinds
    i, k = params(N)
    if name in ('S3a', 'S3b'):
        rec('INV.S_dirty_kinds', i == 0 and P_of(N, m), (typ, N, m))
    if name in ('P4a', 'P4b'):
        rec('INV.S_dirty_kinds', i <= 1 and P_of(N, m), (typ, N, m))
    for cid, ok in lemmaS_claims(typ, N, m):
        rec('INV.' + cid, ok, (typ, N, m))
    ok = I(*nxt)
    rec('INV.C_closure', ok, (typ, N, m, name, nxt))
    for cid, okc in lemmaC_claims(typ, N, m, name, nxt):
        rec('INV.' + cid, okc, (typ, N, m, name, nxt))
    rec('INV.progress_m_increases', nxt[2] >= m + 1, (typ, N, m, nxt))
    if abstract is not None:
        got, path = abstract_B(word(typ, N), m, fast=(abstract == 'fast'))
        rec('INV.closed_eq_abstract_' + abstract, got == nxt, (typ, N, m, name, nxt, got, path))
    return name


def sec_INV():
    mex = 300 if QUICK else (1300 if FULL else 700)
    cnt = {}
    nstates = 0
    for m in range(1, mex + 1):
        for typ in ('std', 'pk'):
            for N in range(m, Nmax(typ, m) + 1):
                if not I(typ, N, m):
                    continue
                nstates += 1
                ab = 'plain' if m <= (60 if QUICK else 150) else ('fast' if m <= (300 if QUICK else 700) else None)
                name = check_state(typ, N, m, ab)
                cnt[name] = cnt.get(name, 0) + 1
    INFO['INV_exhaustive'] = {'m_max': mex, 'states': nstates, 'per_rule': cnt}
    # Nmax sanity: nothing with I above the enumeration bound
    for m in range(1, 400):
        for typ in ('std', 'pk'):
            top = Nmax(typ, m)
            rec('INV.enumeration_bound', not any(I(typ, N, m) for N in range(top + 1, top + 40)), (typ, m))
    # random boundary states up to 2^60
    nr = 20000 if QUICK else 300000
    for t in range(nr):
        bits = RNG.choice((8, 14, 20, 30, 48, 60))
        m = RNG.randint(1, 1 << bits)
        typ = RNG.choice(('std', 'pk'))
        cls = RNG.randint(0, 2)
        if cls == 2:
            N = m + RNG.choice((1, 3)) - (RNG.randint(0, 2) * 2 if RNG.random() < 0.3 else 0)
        else:
            top = None
            for Nt in (int(2.5 * m) + 6, 2 * m + 3, (3 * m + 6) // 2):
                pass
            # pick the class bound for the chosen parity of N, then step down a little (same parity class)
            par = RNG.randint(0, 1)
            if typ == 'std':
                top = (3 * m + 6) // 2 if par == 0 else 2 * m + 3
            else:
                top = 2 * m + 3 if par == 0 else (5 * m + 6) // 2
            N = top - RNG.randint(0, 40)
            if (N - m) % 2:
                N -= 1
        if N < max(m, 2 if typ == 'pk' else 0) or not I(typ, N, m):
            continue
        check_state(typ, N, m, 'fast' if t % 10 == 0 else None)


def sec_Z():
    # 32-step blank run
    R = Run(TT, [0] * 8, 4, A, size=400)
    trans = []
    for s in range(32):
        trans.append(ST[R.s] + str(R.tape[R.h]))
        R.step()
        if R.steps == 5:
            rec('Z.K(\'\',0,0)_at_5', R.s == A and R.cells(-150, 150) == cells_K(0, 0, 0, R.h - R.off, -150, 150), R.cells(-5, 10))
        if R.steps == 14:
            rec('Z.K(\'\',1,0)_at_14', R.s == A and R.cells(-150, 150) == cells_K(0, 1, 0, R.h - R.off, -150, 150), R.cells(-5, 10))
    exp = 'A0 B0 C0 D0 C1 A0 B1 B1 B0 C0 D0 C0 D0 C1 A0 B1 B1 B0 C1 A0 B1 B0 C0 D0 C0 D1 E0 A0 B0 C0 D0 C1'.split()
    rec('Z.trace_32', trans == exp, ' '.join(trans))
    rec('Z.K(\'1\',0,1)_at_32', R.s == A and R.cells(-150, 150) == cells_K(1, 0, 1, R.h - R.off, -150, 150), R.cells(-5, 10))
    rec('Z.I(std,1,1)', I('std', 1, 1))
    # stored direct C run: all overflow configurations K(w,0,m) to 1e10 steps
    path = os.path.join(HERE, 'work', 'overflow_configs_1e10.txt')
    rows = []
    with open(path) as fh:
        for line in fh:
            p = line.split()
            if p[0] == 'END':
                break
            rows.append((int(p[0]), int(p[1]), int(p[2], 2) if len(p) > 2 else 0))
    # the rules' orbit of overflow configurations from K('',0,0)
    w, m = 0, 0
    orbit = [(0, 0)]
    while len(orbit) < len(rows):
        kind, x, mm = overflow(w, m)
        if kind == 'R2':
            w, m = phij(x, mm), mm
        elif kind == 'R3':
            w, m = x, mm
        else:
            break
        orbit.append((m, w))
    # step counts from the low-level step formulas (L: 1 or 2e+3; RS: 10n+7; OV: q+8 / q+14) = the direct run's steps
    w, m, stp = 0, 0, 5
    steps_ok = rows[0][0] == 5
    for t in range(1, len(rows)):
        f = phi(w)
        q = tz(f)
        stp += lstep(w)
        kind, x, mm = overflow(w, m)
        if kind == 'R2':
            stp += q + 8
            w, n = x, mm
            while n > 0:
                stp += lstep(w) + 10 * n + 7
                w = phi(w)
                n -= 1
            m = mm
        else:
            stp += q + 14
            w, m = x, mm
        if stp != rows[t][0]:
            steps_ok = False
            break
    rec('Z.step_formulas_eq_direct_1e10', steps_ok, (t, stp, rows[t][0] if t < len(rows) else None))
    rec('Z.orbit_eq_direct_1e10', [(r[1], r[2]) for r in rows] == orbit[:len(rows)],
        next(((t, rows[t], orbit[t]) for t in range(min(len(rows), len(orbit))) if (rows[t][1], rows[t][2]) != orbit[t]), None))
    INFO['Z_rows'] = len(rows)
    # clean subsequence = macro-rule orbit from (std,1,1)
    clean = [(decode(wq)[0], decode(wq)[1], mq) for (mq, wq) in orbit[:len(rows)] if wq != 0 and decode(wq) is not None]
    s = ('std', 1, 1)
    seq = [s]
    names = {}
    while len(seq) < len(clean):
        name, s = rule(*s)
        names[name] = names.get(name, 0) + 1
        seq.append(s)
    rec('Z.macro_orbit_eq_direct_clean', seq == clean[:len(seq)], next(((t, seq[t], clean[t]) for t in range(len(seq)) if seq[t] != clean[t]), None))
    INFO['Z_rules_used_first_rows'] = names
    # fresh direct run: first 40 macro steps by direct simulation, chained
    s = ('std', 1, 1)
    tot = 32
    for t in range(12 if QUICK else 40):
        name, nxt = rule(*s)
        got, steps = run_K_to_clean(word(s[0], s[1]), s[2], 5 * 10 ** 6)
        rec('Z.fresh_direct_chain', got == nxt, (t, s, name, nxt, got))
        tot += steps
        s = nxt
    INFO['Z_fresh_steps'] = tot


def lstep(w):
    """steps of the left step L on w: 1 (last cell 0) or 2e+3 ((e, e+1) = lowest 00 pair)"""
    if w & 1 == 0:
        return 1
    z = ~w
    return 2 * tz(z & (z >> 1)) + 3


def cells_K(w, n, m, hpos, a, b):
    """cells a..b-1 of the configuration K(w,n,m) with the head (A) at absolute position hpos"""
    out = []
    wl = w.bit_length()
    rc = Rcells(n, m)
    for p in range(a, b):
        d = hpos - p                # offset in the word (>= 0 on the left)
        if d >= 0:
            out.append((w >> d) & 1)
        else:
            j = -d - 1
            out.append(rc[j] if j < len(rc) else 0)
    return out


def sec_F():
    R = Run(TT, [0] * 8, 4, F, size=400)
    R.step(14)
    rec('F.K(\'\',0,1)_at_14', R.s == A and R.cells(-150, 150) == cells_K(0, 0, 1, R.h - R.off, -150, 150), R.cells(-10, 10))
    name, nxt = rule('std', 0, 1)
    rec('F.S0_to_(std,2,2)', name == 'S0' and nxt == ('std', 2, 2) and I(*nxt), (name, nxt))
    got, steps = run_K_to_clean(0, 1, 10 ** 5)
    rec('F.(std,2,2)_at_73', got == ('std', 2, 2) and 14 + steps == 73, (got, steps))
    s = ('std', 2, 2)
    ok = True
    for t in range(20000 if QUICK else 300000):
        if not I(*s):
            ok = False
            break
        name, s = rule(*s)
        if name is None:
            ok = False
            break
    rec('F.orbit_in_I', ok, (t, s))
    sec_F_349()


TM518 = '1RB1RA_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---'      # Eqv_v3.v Module TM518, `tm`
TM349 = '1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---'      # Eqv_v3.v Module TM518, `tm'` (holdout 349)
F518 = [F, A, B_, C, D, E]     # proof.md 7.3: TM518 state q is this table's state F518[q] (A->F, B->A, ..., F->E)


def mirror_rename(s, f):
    """the table s mirrored (L<->R) with state q of the result = state f[q] of s"""
    blocks = s.split('_')
    inv = {f[q]: q for q in range(6)}
    out = []
    for q in range(6):
        blk = blocks[f[q]]
        tr = ''
        for x in (blk[:3], blk[3:]):
            tr += x if x == '---' else x[0] + ('L' if x[1] == 'R' else 'R') + ST[inv[ST.index(x[2])]]
        out.append(tr)
    return '_'.join(out)


def sec_F_349():
    """proof.md 7.3 / 8: 349 = Eqv_v3 TM518 `tm'`; TM518 `tm` = this table mirrored and renamed, started in its A
    (= this table's F).  So flip(TM518 tm) relates to this table by the renaming F518 (busycoq Perm)."""
    rec('F.TM518_eq_mirror_rename_of_table', mirror_rename(TM, F518) == TM518, mirror_rename(TM, F518))
    # the strings in the vendored Eqv_v3.v (read only)
    path = os.path.join(HERE, '..', '..', 'vendor', 'busycoq', 'verify', 'Eqv_v3.v')
    try:
        src = open(path).read()
        blk = src[src.index('Module TM518.'):src.index('End TM518.')]
        lines = [l for l in blk.splitlines() if l.startswith('Definition tm ') or l.startswith("Definition tm' ")]
        got = [l.split('"')[1] for l in lines]
        ok = got == [TM518, TM349] and 'Lemma eqv: halts tm c0 <-> halts tm\' c0.' in blk
    except (OSError, ValueError) as ex:
        ok, got = False, str(ex)
    rec('F.Eqv_v3_TM518_strings_and_eqv', ok, got)
    try:
        hl = open(os.path.join(HERE, '..', '..', 'data', 'holdouts', 'BB6_holdouts_740.txt')).read().split()
        ok = TM349 in hl and TM in hl
    except OSError as ex:
        ok = False
    rec('F.349_and_table_on_740_list', ok)
    # Perm (flip TM518) tm F518: every transition of flip(TM518) at q is this table's transition at F518[q]
    t518 = table(TM518)
    ok = True
    for q in range(6):
        for sym in (0, 1):
            a, bq = t518[2 * q + sym], TT[2 * F518[q] + sym]
            if a is None:
                ok = ok and bq is None
            else:
                ok = ok and bq == (a[0], -a[1], F518[a[2]])
    rec('F.Perm_flip_TM518_to_table', ok)
    # lockstep: TM518 from blank in A = the mirror image of this table from blank in F, state by state
    nst = 50000 if QUICK else (1000000 if FULL else 200000)
    R1 = Run(TT, [0] * 8, 4, F, size=6000)
    R2 = Run(t518, [0] * 8, 4, A, size=6000)
    ok = True
    for t in range(nst):
        R1.step(1, track=False)
        R2.step(1, track=False)
        if R1.halted or R2.halted or F518[R2.s] != R1.s or (R1.h - R1.off - 4) != -(R2.h - R2.off - 4):
            ok = False
            break
        if t % 10000 == 9999 or t == nst - 1:
            # cell p of R1 (relative to its start cell) <-> cell -p of R2, over every visited cell plus a margin
            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('F.TM518_lockstep_mirror_of_startF', ok, (t, R1.s, R2.s))
    INFO['F_lockstep_steps'] = nst


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


def sec_NEG():
    """off the invariant the landing points matter: a pk gen-1 H landing halts on the TM, a std gen-1 N landing nests"""
    found = {'H': 0, 'N': 0, 'R': 0}
    tries = 0
    while min(found.values()) < (3 if QUICK else 10) and tries < 20000:
        tries += 1
        typ = RNG.choice(('std', 'pk'))
        L = RNG.randint(3, 7)
        i = 0
        k = RNG.randint((1 << (L - 1)) + 1, (1 << L) - 1)
        if typ == 'std':
            o = k
            lands = [(g, 2 * (((o >> g) << g) + (1 << g))) for g in range(tz(o) + 1, L) if not (o >> g) & 1]
            base = 2 * k
        else:
            o = k - (1 << (L - 1))
            if o == 0:
                continue
            lands = [(g, 2 * (((o >> g) << g) + (1 << g))) for g in range(tz(o) + 1, L - 1) if not (o >> g) & 1]
            base = 2 * o
        if not lands:
            continue
        g, Tg = RNG.choice(lands)
        b = Tg - base - 1
        m = b - 1
        if m < 1:
            continue
        N = 2 * k
        kind = 'H' if (typ == 'pk' and g == L - 2) else ('N' if (o >> (g + 1)) & 1 else 'R')
        if found[kind] >= 10:
            continue
        got, path = abstract_B(word(typ, N), m)
        rec('NEG.not_I', not I(typ, N, m), (typ, N, m))
        if kind == 'H':
            res, steps = run_K_to_clean(word(typ, N), m, 2 * 10 ** 6)
            rec('NEG.H_landing_halts_on_TM', res[0] == 'HALT' and got[0] == 'R4', (typ, N, m, res, path))
        elif kind == 'N':
            rec('NEG.N_landing_nested', got[0] == 'R5' or path[:3] == ['R2', 'dirty', 'R5'], (typ, N, m, path))
        else:
            rec('NEG.R_landing_resets', 'R3' in path, (typ, N, m, path))
        found[kind] += 1


def sec_TPL():
    """proof.md 8: on std words the left step never reads F1, and L+OV (TM1's ROv) runs identically on TM1 and TM2"""
    t1, t2 = table(TM1), table(TM2)
    for N in range(0, 1 << (8 if QUICK else 11)):
        for m in (0, 1, 4):
            w = std(N)
            wl = max(w.bit_length(), 1)
            pad = 6
            cells = [0] * pad + bits_to_cells(w, wl) + Rcells(0, m)
            b0 = pad + wl
            i, k = params(N)
            nst = lstep(w) + 2 * i + 8
            outs = []
            for tt in (TT, t1, t2):
                R = Run(tt, cells, b0 - 1, A)
                R.step(nst)
                outs.append((R.s, R.h - R.off, R.cells(0, b0 + 2 * m + 2 * i + 12), R.halted, 'F1' in R.used))
            bp = b0 - 2 * i - 1
            exp = bits_to_cells(W(0, k), bp) + Rcells(1 + i + m, 0)
            ok = outs[0] == outs[1] == outs[2] and not outs[0][4] and outs[0][0] == A and outs[0][1] == bp - 1
            ok = ok and outs[0][2][:len(exp)] == exp and not any(outs[0][2][len(exp):])
            rec('TPL.ROv_std_same_on_TM1_TM2_no_F1', ok, (N, m))
            # LIncs: the left step alone on std words never reads F1
            R = Run(TT, [0] * pad + bits_to_cells(w, wl) + [1, 1, 0], pad + wl - 1, A)
            R.step(lstep(w))
            rec('TPL.LInc_std_no_F1', 'F1' not in R.used and R.cells(0, b0) == bits_to_cells(std(N + 1), b0), N)


INFO = {}


def main():
    secs = [('T', sec_T), ('LS', sec_LS), ('RS', sec_RS), ('OV', sec_OV), ('K', sec_K), ('PHI', sec_PHI),
            ('ORB', sec_ORB), ('X', sec_X), ('B', sec_B), ('INV', sec_INV), ('Z', sec_Z), ('F', sec_F),
            ('J', sec_J), ('NEG', sec_NEG), ('TPL', sec_TPL)]
    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'
        if st == 'FAIL':
            nfail += 1
        print('%-48s %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)