#!/usr/bin/env python3
"""check_proof.py -- simulation evidence for proof.md of W5-7 = 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---

Run from anywhere:  python3 -B check_proof.py  [--quick] [--heavy]
Sections (proof.md section 10 lists every check):
  T  the table is SOBCv6.v TM3's table under the state map A,B,C,D,E,F -> B,C,A,E,D,F
  W  word rules on the tape (partial simulator: cells marked unknown must never be read)
     W1 LInc, W2 LOv, W3 Incs, W4 Ov, W5 walk-in of W0, W6 walk-in of a W1 W1 pair, W7 the far tail halts
  L  list lemmas on explicit lists (block lemmas, peels, LInc through a 10-block)
  A  abstract functions (lower-bound blocks) against the explicit functions on random instantiations
     (A1-A4) and on every small abstract list, misaligned pairs included (A5)
  I  initial segment: blank -> P(x0) at 847 -> P(x1) at 2,136 -> P(x2) at 38,573 (direct simulation)
  C  the abstract chain x2 -> x194 (192 steps, maxv = 256), its statistics, the fuel of every LInc_rec
     call under TM3's fuel convention (C9), and a cross-check with the observe-stage stack model work/model/fast.py
  H  the halt: LIncs at cycle 194, split into walkable prefix + far tail, doom_rec (H6, H7), and a direct
     run of the whole instantiated overflow to the halt
  D  direct simulation of instantiated abstract cycles (Ov phase) against the abstract step
Nothing here is a proof. Every check prints PASS/FAIL; the last line is SUMMARY.
"""
import sys, os, random, itertools, time
HERE = os.path.dirname(os.path.abspath(__file__))
QUICK = '--quick' in sys.argv
HEAVY = '--heavy' in sys.argv
RNG = random.Random(20261013)

TM = '1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---'
TM3 = '1LB0LE_1RC0RE_1LA1RD_1LA1RB_0RD0RF_0LD---'
SN = 'ABCDEF'
def table(s):
    tr = {}
    for qi, part in enumerate(s.split('_')):
        for b in (0, 1):
            t = part[3*b:3*b+3]
            tr[(SN[qi], b)] = None if t == '---' else (int(t[0]), 1 if t[1] == 'R' else -1, t[2])
    return tr
TR = table(TM)

RESULTS = []
def report(name, ok, detail=''):
    RESULTS.append((name, ok))
    print(('PASS ' if ok else 'FAIL ') + name + ('  ' + detail if detail else ''), flush=True)

# ---------------------------------------------------------------- words and configurations
# A counter list is head-first: x[0] is the word next to the head. Words: 0 = W0 = 001, 1 = W1 = 111 (paper order).
WORD = {0: (0, 0, 1), 1: (1, 1, 1)}
def lmp_cells(x):
    """paper-order cells of Lmp x (far end first)."""
    out = []
    for d in reversed(x): out.extend(WORD[d])
    return out
def RC(n): return [1] + [0, 1, 1] * n + [0, 1]
U = 2   # unknown cell

class ReadUnknown(Exception): pass

class PSim:
    """Partial simulator. Cells hold 0, 1 or U (unknown). Reading U raises ReadUnknown.
    left: cells left of the head boundary; for headdir 'L' the head reads left[-1] (busycoq `l <S r`),
    for 'R' it reads right[0] (`l S> r`). leftfill/rightfill: 0 (= 0inf) or U for the cells beyond."""
    def __init__(self, left, state, right, headdir='L', leftfill=0, rightfill=0, margin=4000):
        n = margin + len(left) + len(right) + margin
        self.t = bytearray([leftfill]) * (margin) + bytearray(left) + bytearray(right) + bytearray([rightfill]) * margin
        self.base = margin                     # index of left[0]
        self.b = margin + len(left)            # index of right[0] (boundary)
        self.pos = self.b - 1 if headdir == 'L' else self.b
        self.st = state; self.steps = 0; self.halted = False
        self.lo = self.hi = self.pos
    def run(self, maxsteps, stop=None):
        t = self.t; pos = self.pos; st = self.st
        for _ in range(maxsteps):
            if stop is not None:
                self.pos = pos; self.st = st
                if stop(self): return True
            s = t[pos]
            if s == U: self.pos = pos; self.st = st; raise ReadUnknown()
            tr = TR[(st, s)]
            if tr is None:
                self.pos = pos; self.st = st; self.halted = True; return False
            w, d, st = tr
            t[pos] = w; pos += d; self.steps += 1
            if pos < self.lo: self.lo = pos
            if pos > self.hi: self.hi = pos
            if pos < 0 or pos >= len(t): raise RuntimeError('margin too small')
        self.pos = pos; self.st = st
        return False

def strip0(cells):
    i = 0
    while i < len(cells) and cells[i] == 0: i += 1
    return list(cells[i:])

def left_equals(sim, upto, cells):
    """tape[ .. upto) (exclusive) equals 0inf followed by `cells` (right-aligned at upto)."""
    seg = list(sim.t[:upto])
    return strip0(seg) == strip0(cells)

# ---------------------------------------------------------------- explicit list functions (TM3's relations)
def ex_LInc(x):
    """TM3's LInc as a function: W0 skipped, W1 W1 -> W1 W0 (carry on), W1 W0 -> W1 W1 (stop). None if undefined."""
    out = []; i = 0
    while True:
        if i >= len(x): return None
        if x[i] == 0: out.append(0); i += 1; continue
        if i + 1 >= len(x): return None
        if x[i+1] == 1: out += [1, 0]; i += 2; continue
        return out + [1, 1] + list(x[i+2:])

def ex_LIncs(x, cap=None):
    """TM3's LIncs: (x with every pair set to W1 W1, count). count = sum over pairs p (from the head) of (1-b_p) 2^p.
    With cap: count is min(count, cap) but the parity is exact (returned separately)."""
    toks = []; i = 0
    while i < len(x):
        if x[i] == 0: toks.append(None); i += 1
        else:
            if i + 1 >= len(x): return None
            toks.append(x[i+1]); i += 2
    ones = []; c = 0; par = None; p = 0
    bits = [b for b in toks if b is not None]
    for tk in toks:
        ones += [0] if tk is None else [1, 1]
    if bits: par = 1 - bits[0]
    else: par = 0
    if cap is None:
        for k, b in enumerate(bits): c += (1 - b) << k
        return ones, c, par
    # capped: compute from the far end with saturation
    for b in reversed(bits):
        c = min(cap, 2 * c + (1 - b))
    return ones, c, par

def ex_LOv(x):
    """TM3's LOv as a function (defined on lists of W0 and W1 W1 only)."""
    toks = []; i = 0
    while i < len(x):
        if x[i] == 0: toks.append('S'); i += 1
        elif i + 1 < len(x) and x[i+1] == 1: toks.append('P'); i += 2
        else: return None
    v = [1, 0]                    # reversed (far -> near); head-first [W0, W1]
    for tk in reversed(toks):
        if tk == 'S': v.append(1); continue
        h = v.pop()
        if h == 0: v += [1, 0, 0]
        else:
            if rev_LInc(v) is None: return None
            v += [0, 0, 0]
    return v[::-1]

def rev_LInc(v):
    """LInc in place on a reversed explicit list (head = end of v). None if undefined."""
    tmp = []
    while True:
        if not v: return None
        if v[-1] == 0: tmp.append(v.pop()); continue
        if len(v) < 2: return None
        if v[-2] == 1: v.pop(); v.pop(); tmp += [1, 0]; continue
        v.pop(); v.pop(); tmp += [1, 1]; break
    for it in reversed(tmp): v.append(it)
    return True

def ex_step(x):
    """one exact cycle P x -> P y (TM3's Incs then Ov). Returns (y, count) or (None, reason)."""
    r = ex_LIncs(x)
    if r is None: return None, 'LIncs undefined'
    ones, c, par = r
    if c % 2 == 0: return None, 'count even'
    v = ex_LOv(ones)
    if v is None: return None, 'LOv undefined'
    if v[0] != 0: return None, 'LOv starts with W1'
    return [1, 0] * ((c - 1) // 2) + [1, 1] + v[1:], c

# ---------------------------------------------------------------- abstract lists (lower-bound blocks)
# tokens: 'W0', 'W1', ('A', l) = [W1;W0]^(1+l+n), ('B', l) = [W1;W1]^(1+l+n), n >= 0 free per block.
MAXV = 256
STATS = {'linc_A': 0, 'ov_keep': 0, 'ov_peel1': 0, 'ov_w11': 0}
# Fuel as in SOBCv6.v TM3: LOv_rec x0 gets S(length x0) and loses 1 per token level, so the level of token j
# (0 = head) has fuel 1 + length x0 - j; the LInc_rec call made at that level gets that level's fuel and
# needs one unit per token it visits, the stopping token included.
FUEL = {'calls': 0, 'min_slack': None, 'max_depth': 0}
def note_fuel(T, d):
    FUEL['calls'] += 1
    if FUEL['min_slack'] is None or T - d < FUEL['min_slack']: FUEL['min_slack'] = T - d
    if d > FUEL['max_depth']: FUEL['max_depth'] = d
    return d <= T

def ab_LInc(x):
    out = []; i = 0
    while True:
        if i >= len(x): return None
        h = x[i]
        if h == 'W0': out.append('W0'); i += 1; continue
        if h == 'W1' and i + 1 < len(x) and x[i+1] == 'W1': out += ['W1', 'W0']; i += 2; continue
        if h == 'W1' and i + 1 < len(x) and x[i+1] == 'W0': return out + ['W1', 'W1'] + list(x[i+2:])
        if isinstance(h, tuple) and h[0] == 'A' and h[1] >= 1:
            STATS['linc_A'] += 1
            return out + ['W1', 'W1', ('A', h[1] - 1)] + list(x[i+1:])
        return None

def ab_rev_LInc(v):
    """LInc_rec in place on a reversed abstract list (head = end of v). Returns the number of LInc_rec levels
    used (tokens visited, the stopping token included), or None if it fails."""
    tmp = []; d = 0
    while True:
        if not v: return None
        h = v[-1]; d += 1
        if h == 'W0': tmp.append(v.pop()); continue
        if h == 'W1' and len(v) >= 2 and v[-2] == 'W1': v.pop(); v.pop(); tmp += ['W1', 'W0']; continue
        if h == 'W1' and len(v) >= 2 and v[-2] == 'W0': v.pop(); v.pop(); tmp += ['W1', 'W1']; break
        if isinstance(h, tuple) and h[0] == 'A' and h[1] >= 1:
            v.pop(); STATS['linc_A'] += 1; tmp += ['W1', 'W1', ('A', h[1] - 1)]; break
        return None
    for it in reversed(tmp): v.append(it)
    return d

def ab_tokens(x):
    toks = []; i = 0
    while i < len(x):
        h = x[i]
        if h == 'W0': toks.append(('S',)); i += 1
        elif h == 'W1':
            if i + 1 < len(x) and x[i+1] in ('W0', 'W1'): toks.append(('P', 1 if x[i+1] == 'W0' else 0)); i += 2
            else: return None
        else: toks.append(('K', 1 if h[0] == 'A' else 0, h[1])); i += 1
    return toks

def ab_LIncs(x, maxv=MAXV):
    """(x0, n, m): x0 = x with pairs -> W1 W1 and 10-blocks -> 11-blocks; count = n'*2+m with n' >= n."""
    toks = ab_tokens(x)
    if toks is None: return None
    n = 0; m = 0; out = []
    for tk in reversed(toks):
        if tk[0] == 'S': out.append('W0')
        elif tk[0] == 'P': n = min(maxv, 2*n + m); m = tk[1]; out += ['W1', 'W1']
        else: n = min(maxv, 2*n + m); m = tk[1]; out.append(('B', tk[2]))
    out.reverse()
    return out, n, m

def ab_LOv(x):
    toks = []; i = 0
    while i < len(x):
        h = x[i]
        if h == 'W0': toks.append('S'); i += 1
        elif h == 'W1':
            if i + 1 < len(x) and x[i+1] == 'W1': toks.append('P'); i += 2
            else: return None
        elif h[0] == 'B': toks.append(h); i += 1
        else: return None
    v = ['W1', 'W0']
    L = len(x)
    for j in range(len(toks) - 1, -1, -1):
        tk = toks[j]; T = 1 + L - j                      # fuel of this LOv_rec level (TM3's convention)
        if tk == 'S': v.append('W1'); continue
        if tk == 'P':
            h = v.pop()
            if h == 'W0': v += ['W1', 'W0', 'W0']
            elif h == 'W1':
                d = ab_rev_LInc(v)
                if d is None or not note_fuel(T, d): return None
                v += ['W0', 'W0', 'W0']
            else: return None
            continue
        l = tk[1]; STATS['ov_w11'] += 1
        h1 = v[-1]; h2 = v[-2] if len(v) >= 2 else None
        if h1 == 'W0' and h2 == 'W0':                    # TM3's case: keep the block
            v.pop(); v.pop(); v += [('A', l), 'W0', 'W0']; STATS['ov_keep'] += 1
        elif h1 == 'W1':                                 # peel the far pair; deeper result W1 v0, LInc v0
            if l == 0: return None
            v.pop()
            d = ab_rev_LInc(v)
            if d is None or not note_fuel(T, d): return None
            v += ['W0', ('A', l - 1), 'W0', 'W0']; STATS['ov_peel1'] += 1
        else: return None                                # deeper result W0 V', V' not starting with W0: no case
    return v[::-1]

def ab_step(x, maxv=MAXV):
    r = ab_LIncs(x, maxv)
    if r is None: return None, 'LIncs_rec None'
    x0, n, m = r
    if m != 1: return None, 'count even'
    if n < 1: return None, 'n = 0'
    x1 = ab_LOv(x0)
    if x1 is None: return None, 'LOv_rec None'
    if x1[0] != 'W0': return None, 'LOv_rec result starts with W1'
    return [('A', n - 1), 'W1', 'W1'] + x1[1:], n

def inst(xa, rng, nmax=2, fixed=None):
    out = []
    for t in xa:
        if t == 'W0': out.append(0)
        elif t == 'W1': out.append(1)
        else:
            k = 1 + t[1] + (fixed if fixed is not None else rng.randint(0, nmax))
            out += ([1, 0] if t[0] == 'A' else [1, 1]) * k
    return out

def matches(xa, x):
    """Lmp' xa x (some choice of the free n of each block)."""
    from functools import lru_cache
    xa = tuple(xa); x = tuple(x)
    sys.setrecursionlimit(100000)
    @lru_cache(maxsize=None)
    def go(i, j):
        if i == len(xa): return j == len(x)
        t = xa[i]
        if t == 'W0': return j < len(x) and x[j] == 0 and go(i + 1, j + 1)
        if t == 'W1': return j < len(x) and x[j] == 1 and go(i + 1, j + 1)
        pair = (1, 0) if t[0] == 'A' else (1, 1)
        k = 0; jj = j
        while jj + 1 < len(x) and x[jj:jj+2] == pair:
            k += 1; jj += 2
            if k >= 1 + t[1] and go(i + 1, jj): return True
        return False
    return go(0, 0)

def show_ab(x, n=None):
    s = []
    for t in (x if n is None else x[:n]):
        s.append(t[1] if isinstance(t, str) else ('(10)^(%d+)' % (1 + t[1]) if t[0] == 'A' else '(11)^(%d+)' % (1 + t[1])))
    return ' '.join(s)

# ================================================================= T: the table
def check_T():
    # sigma: ours -> TM3
    sig = dict(zip('ABCDEF', 'BCAEDF'))
    t3 = table(TM3)
    ok = True
    for (q, b), tr in TR.items():
        u = t3[(sig[q], b)]
        if tr is None or u is None: ok &= (tr is None and u is None); continue
        ok &= (u == (tr[0], tr[1], sig[tr[2]]))
    report('T1 table = TM3 table renamed (ours A,B,C,D,E,F = TM3 B,C,A,E,D,F)', ok)
    # holdout list membership (byte exact)
    p = os.path.join(HERE, '..', '..', 'data', 'holdouts', 'BB6_holdouts_740.txt')
    try:
        lines = open(p).read().split('\n')
        report('T2 string is line %d of BB6_holdouts_740.txt (byte exact)' % (lines.index(TM) + 1), TM in lines)
    except FileNotFoundError:
        report('T2 holdout list present', False)
    halts = [k for k, v in TR.items() if v is None]
    report('T3 the only undefined transition is F1', halts == [('F', 1)])

# ================================================================= W: word rules on the tape
def lists_upto(L):
    for n in range(L + 1):
        for x in itertools.product((0, 1), repeat=n): yield list(x)
def ones_lists(T):
    """lists of tokens W0 / W1 W1 with up to T tokens"""
    for n in range(T + 1):
        for toks in itertools.product((0, 1), repeat=n):
            x = []
            for k in toks: x += [0] if k == 0 else [1, 1]
            yield x
def rand_list(rng, n):
    return [rng.choice((0, 1)) for _ in range(n)]
def rand_ones(rng, ntok):
    x = []
    for _ in range(ntok): x += [0] if rng.random() < 0.4 else [1, 1]
    return x

def run_LInc(x):
    """Lmp x <D 010 r  ->*  Lmp x' 001 A> r, r unknown (never read). Returns True/False."""
    y = ex_LInc(x)
    left = lmp_cells(x); right = [0, 1, 0]
    s = PSim(left, 'D', right, 'L', 0, U)
    rb = s.b + 3
    try:
        s.run(10**7, stop=lambda m: m.pos >= rb)
    except ReadUnknown:
        return False
    return s.pos == rb and s.st == 'A' and left_equals(s, rb, lmp_cells(y) + [0, 0, 1])

def run_LOv(x):
    """Lmp x <D 010 1 r ->* Lmp x' A> r (x' = LOv x), r unknown."""
    y = ex_LOv(x)
    left = lmp_cells(x); right = [0, 1, 0, 1]
    s = PSim(left, 'D', right, 'L', 0, U)
    rb = s.b + 4
    try:
        s.run(10**7, stop=lambda m: m.pos >= rb)
    except ReadUnknown:
        return False
    return s.pos == rb and s.st == 'A' and left_equals(s, rb, lmp_cells(y))

def run_target_D(x, rc, y, rc2, maxsteps):
    """Lmp x <D 010 RC(rc) ->* Lmp y <D 010 RC(rc2) (whole tape explicit). Returns steps or None."""
    left = lmp_cells(x); right = [0, 1, 0] + RC(rc)
    s = PSim(left, 'D', right, 'L', 0, 0, margin=4000 + 6 * rc2)
    R = bytes([0, 1, 0] + RC(rc2)); L = strip0(lmp_cells(y))
    def stop(m):
        if m.st != 'D': return False
        p = m.pos
        if bytes(m.t[p+1:p+1+len(R)]) != R: return False
        if any(m.t[p+1+len(R):m.hi+2]): return False
        return strip0(list(m.t[:p+1])) == L
    ok = s.run(maxsteps, stop=stop)
    return s.steps if ok else None

def check_W():
    # W1 LInc
    L = 8 if QUICK else 10
    tot = ok = 0
    for x in lists_upto(L):
        if ex_LInc(x) is None: continue
        tot += 1; ok += run_LInc(x)
    for _ in range(100 if QUICK else 400):
        x = rand_list(RNG, RNG.randint(11, 60))
        if ex_LInc(x) is None: continue
        tot += 1; ok += run_LInc(x)
    report('W1 LInc_spec: Lmp x <D 010 r ->* Lmp LInc(x) 001 A> r, r never read', ok == tot, '%d/%d (all lists <= %d words + random 11..60)' % (ok, tot, L))
    # W2 LOv
    T = 6 if QUICK else 8
    tot = ok = 0
    for x in ones_lists(T):
        if ex_LOv(x) is None: continue
        tot += 1; ok += run_LOv(x)
    for _ in range(60 if QUICK else 300):
        x = rand_ones(RNG, RNG.randint(9, 40))
        if ex_LOv(x) is None: continue
        tot += 1; ok += run_LOv(x)
    report('W2 LOv_spec: Lmp x <D 010 1 r ->* Lmp LOv(x) A> r, r never read', ok == tot, '%d/%d (all ones-lists <= %d tokens + random 9..40)' % (ok, tot, T))
    # W3 Incs (count odd)
    T = 5 if QUICK else 6
    tot = ok = 0
    cases = []
    for n in range(1, T + 1):
        for toks in itertools.product((0, 1, 2), repeat=n):
            x = []
            for k in toks: x += [0] if k == 0 else ([1, 0] if k == 1 else [1, 1])
            cases.append(x)
    for _ in range(40 if QUICK else 150):
        x = []
        for _ in range(RNG.randint(7, 12)):
            r = RNG.random(); x += [0] if r < 0.3 else ([1, 0] if r < 0.6 else [1, 1])
        cases.append(x)
    for x in cases:
        r = ex_LIncs(x)
        if r is None: continue
        ones, c, par = r
        if c % 2 == 0 or c > 400: continue
        tot += 1
        ok += run_target_D(x, 1, ones, c + 1, 10**7) is not None
    report('W3 Incs: Lmp x <D 010 RC 1 ->* Lmp ones(x) <D 010 RC(c+1), c = count odd', ok == tot, '%d/%d' % (ok, tot))
    # W4 Ov
    T = 5 if QUICK else 6
    tot = ok = 0
    cases = list(ones_lists(T)) + [rand_ones(RNG, RNG.randint(7, 20)) for _ in range(40 if QUICK else 150)]
    for x in cases:
        v = ex_LOv(x)
        if v is None or v[0] != 0: continue
        for m in ((0, 1, 3) if len(x) < 14 else (RNG.randint(0, 6),)):
            tot += 1
            y = [1, 0] * m + [1, 1] + v[1:]
            ok += run_target_D(x, 2 * m + 2, y, 1, 10**7) is not None
    report('W4 Ov: LOv x = W0 x\' => Lmp x <D 010 RC(2m+2) ->* Lmp ((W1 W0)^m W1 W1 x\') <D 010 RC 1', ok == tot, '%d/%d' % (ok, tot))
    # W5 / W6 walk-in, with Lmp x and r both unknown
    for name, word, steps, rp in (('W5', [0, 0, 1], 19, [0, 1, 1]), ('W6', [1, 1, 1, 1, 1, 1], 12, [0, 1, 0, 1, 0, 1])):
        s = PSim(word, 'D', [0, 1, 0, 1], 'L', U, U)
        tb = s.base - 1                       # last cell of Lmp x
        rb = s.b + 4
        good = True
        try:
            s.run(10**5, stop=lambda m: m.pos == tb and m.st == 'D')
        except ReadUnknown:
            good = False
        good = good and s.pos == tb and s.st == 'D' and s.steps == steps and s.hi < rb
        good = good and list(s.t[tb + 1:tb + 1 + 4 + len(rp)]) == [0, 1, 0, 1] + rp
        report('%s walk-in: Lmp x %s <D 010 1 r ->(%d) Lmp x <D 010 1 %s r, Lmp x and r never read' % (
            name, ''.join(map(str, word)), steps, ''.join(map(str, rp))), good, 'steps %d' % s.steps)
    # W7 far tail halts
    xf = XFAR
    s = PSim(lmp_cells(xf), 'D', [0, 1, 0, 1], 'L', 0, U)
    far = s.base; rb = s.b + 4
    good = True
    try:
        s.run(10**6, stop=lambda m: m.pos >= rb)
    except ReadUnknown:
        good = False
    good = good and s.halted and s.st == 'F' and s.t[s.pos] == 1 and s.hi < rb
    report('W7 far tail: Lmp x_far <D 010 1 r halts (F reads 1) after %d steps, r never read' % s.steps, good and s.steps == 1368,
           'head in cells far%+d .. far%+d, halt at far%+d' % (s.lo - far, s.hi - far, s.pos - far))
    # W7c: the milestone configurations of proof.md 8.2 (cells between the far end region and r)
    def cells(t): return [int(c) for c in t.replace(' ', '')]
    ms = {191: ('D', [], cells('010 1' + ' 010101' * 3 + ' 011 010101' * 5)),
          1047: ('D', [], cells('010 101010101010101010101101101101101101101101101101101101101011010101')),
          1368: ('F', cells('1' * 6 + ('00' + '1' * 4) * 2 + '00' + '1' * 7 + ('00' + '1' * 4) * 5 + '00' + '1' + '0000' + '1'),
                 cells('010101'))}
    s = PSim(lmp_cells(xf), 'D', [0, 1, 0, 1], 'L', 0, U)
    rb = s.b + 4
    seen = {}
    def stop(m):
        if m.steps in ms:
            q, L, R = ms[m.steps]
            # left: 0inf then L ending at the head cell (or the head on 0 with all zeros left when L is empty)
            okL = strip0(list(m.t[:m.pos + 1])) == L if L else (not any(m.t[:m.pos + 1]))
            okR = list(m.t[m.pos + 1:rb]) == R
            seen[m.steps] = (m.st == q and okL and okR)
        return False
    try:
        s.run(10**6, stop=stop)
    except ReadUnknown:
        pass
    report('W7c far-run milestones at steps 191, 1047, 1368 are the configurations of proof.md 8.2', len(seen) == 3 and all(seen.values()), str(seen))
    # W7b: the far tail is minimal (shorter token suffixes read r)
    toks = [[1, 1] if t == 'P' else [0] for t in ['P', 'S'] * 5 + ['P'] * 3]
    short_ok = True
    for k in range(1, 13):
        xs = sum(toks[len(toks) - k:], [])
        s = PSim(lmp_cells(xs), 'D', [0, 1, 0, 1], 'L', 0, U)
        try:
            s.run(10**6)
            if s.halted: short_ok = False
        except ReadUnknown:
            pass
    report('W7b no shorter token suffix of x_far halts without reading r (k = 1..12 tokens)', short_ok)

XFAR = [1, 1, 0] * 5 + [1, 1, 1, 1, 1, 1]      # (P S)^5 P P P, head-first

# ================================================================= L: list lemmas (explicit lists)
def check_L():
    rng = RNG
    ok = {k: True for k in ('lpow', 'lpow1', 'ovlpow', 'peel1', 'incblk')}
    cnt = {k: 0 for k in ok}
    xs = [list(x) for x in lists_upto(6)] + [rand_list(rng, rng.randint(7, 30)) for _ in range(200)]
    for x in xs:
        r = ex_LIncs(x)
        for n in range(0, 9):
            if r is not None:
                ones, c, _ = r
                r1 = ex_LIncs([1, 0] * n + x); r2 = ex_LIncs([1, 1] * n + x)
                cnt['lpow'] += 1; ok['lpow'] &= (r1[0] == [1, 1] * n + ones and r1[1] == (c + 1) * 2**n - 1)
                cnt['lpow1'] += 1; ok['lpow1'] &= (r2[0] == [1, 1] * n + ones and r2[1] == c * 2**n)
            v = ex_LOv(x)
            if v is not None:
                big = ex_LOv([1, 1] * (1 + n) + x)
                if v[:2] == [0, 0]:
                    cnt['ovlpow'] += 1
                    ok['ovlpow'] &= (ex_LOv([1, 1] * n + x) == [0, 0] + [1, 0] * n + v[2:])
                if v[0] == 1:
                    v1 = ex_LInc(v[1:])
                    cnt['peel1'] += 1
                    ok['peel1'] &= (big == ([0, 0] + [1, 0] * n + [0] + v1) if v1 is not None else big is None)
            cnt['incblk'] += 1
            ok['incblk'] &= (ex_LInc([1, 0] * (1 + n) + x) == [1, 1] + [1, 0] * n + x)
    report('L1 LIncs_lpow: LIncs((W1 W0)^n x) = ((W1 W1)^n ones(x), (c+1) 2^n - 1)', ok['lpow'], '%d cases' % cnt['lpow'])
    report("L2 LIncs_lpow': LIncs((W1 W1)^n x) = ((W1 W1)^n ones(x), c 2^n)", ok['lpow1'], '%d cases' % cnt['lpow1'])
    report('L3 LOv_lpow: LOv x = W0 W0 v => LOv((W1 W1)^n x) = W0 W0 (W1 W0)^n v', ok['ovlpow'], '%d cases' % cnt['ovlpow'])
    report('L4 LOv_peel1: LOv x = W1 v => LOv((W1 W1)^(1+n) x) = W0 W0 (W1 W0)^n W0 LInc(v)', ok['peel1'], '%d cases' % cnt['peel1'])
    report('L5 LInc_blk: LInc((W1 W0)^(1+n) x) = W1 W1 (W1 W0)^n x', ok['incblk'], '%d cases' % cnt['incblk'])

# ================================================================= A: abstract functions vs explicit ones
def rand_abs(rng, ntok, ones_only=False, lmax=3):
    x = []
    for _ in range(ntok):
        r = rng.random()
        if r < 0.3: x.append('W0')
        elif r < 0.55: x += ['W1', 'W1']
        elif r < 0.7 and not ones_only: x += ['W1', 'W0']
        elif r < 0.85: x.append(('B', rng.randint(0, lmax)))
        elif not ones_only: x.append(('A', rng.randint(0, lmax)))
        else: x.append('W0')
    return x

def check_A():
    rng = RNG
    N = 1500 if QUICK else 6000
    c_inc = c_incs = c_ov = c_step = 0; bad = []
    for _ in range(N):
        xa = rand_abs(rng, rng.randint(0, 9))
        # LInc_rec
        ya = ab_LInc(xa)
        if ya is not None:
            for _ in range(3):
                x = inst(xa, rng); y = ex_LInc(x)
                c_inc += 1
                if y is None or not matches(ya, y): bad.append(('LInc', xa))
        # LIncs_rec
        r = ab_LIncs(xa, 64)
        if r is not None:
            x0a, n, m = r
            for _ in range(3):
                x = inst(xa, rng); e = ex_LIncs(x)
                c_incs += 1
                if e is None: bad.append(('LIncs undefined', xa)); continue
                ones, c, _ = e
                if not (matches(x0a, ones) and c % 2 == m and (c - m) // 2 >= n): bad.append(('LIncs', xa, n, m, c))
        # LOv_rec on ones-lists
        xo = rand_abs(rng, rng.randint(0, 9), ones_only=True)
        za = ab_LOv(xo)
        if za is not None:
            for _ in range(3):
                x = inst(xo, rng); z = ex_LOv(x)
                c_ov += 1
                if z is None or not matches(za, z): bad.append(('LOv', xo))
        # step_rec: abstract result vs exact cycle (head block compared through its length only)
        xs = ['W1', 'W0'] + rand_abs(rng, rng.randint(0, 8))
        sa, n = ab_step(xs, 64)
        if sa is not None:
            for _ in range(2):
                x = inst(xs, rng)
                e = ex_LIncs(x)
                ones, c, _ = e
                v = ex_LOv(ones)
                c_step += 1
                ok = (c % 2 == 1 and v is not None and v[0] == 0 and (c - 1) // 2 >= n and
                      sa[0] == ('A', n - 1) and matches(sa[1:], [1, 1] + v[1:]))
                if not ok: bad.append(('step', xs))
    report('A1 LInc_rec sound (abstract result matches LInc of every sampled instantiation)', not [b for b in bad if b[0] == 'LInc'], '%d instances' % c_inc)
    report('A2 LIncs_rec sound (x0 matches, parity m exact, n\' >= n; maxv = 64 here)', not [b for b in bad if b[0].startswith('LIncs')], '%d instances' % c_incs)
    report('A3 LOv_rec sound (keep / peel cases)', not [b for b in bad if b[0] == 'LOv'], '%d instances' % c_ov)
    report('A4 step_rec sound: P x -> P x\' for every sampled instantiation', not [b for b in bad if b[0] == 'step'], '%d instances' % c_step)
    if bad: print('   first failures:', bad[:3])

def first_bad_W1(X):
    """head-first token parse of an abstract list: index of the first W1 that is not followed by an explicit
    W0 or W1 token (a lone W1, or a W1 followed by a block), else None."""
    i = 0
    while i < len(X):
        if X[i] == 'W1':
            if i + 1 < len(X) and X[i+1] in ('W0', 'W1'): i += 2
            else: return i
        else: i += 1
    return None

def linc_reaches_bad(X):
    """LInc_rec's walk from the head reaches such a W1 before it stops."""
    i = 0
    while i < len(X):
        h = X[i]
        if h == 'W0': i += 1; continue
        if h == 'W1':
            if i + 1 < len(X) and X[i+1] == 'W1': i += 2; continue
            return not (i + 1 < len(X) and X[i+1] == 'W0')
        return False                      # a block token: LInc_rec stops or fails here
    return False

def all_inst(xa, nmax=1):
    """every instantiation of xa with the free n of each block in 0..nmax."""
    nb = sum(1 for t in xa if isinstance(t, tuple))
    for ns in itertools.product(range(nmax + 1), repeat=nb):
        it = iter(ns); out = []
        for t in xa:
            if t == 'W0': out.append(0)
            elif t == 'W1': out.append(1)
            else: out += ([1, 0] if t[0] == 'A' else [1, 1]) * (1 + t[1] + next(it))
        yield out

def check_A5():
    """exhaustive over small abstract lists (misaligned ones included): every result of LInc_rec,
    LIncs_rec, LOv_rec denotes the explicit result of every instantiation, and a W1 without an explicit
    partner (lone, or followed by a block) makes the functions fail (proof.md 5.2-5.4 failure rows)."""
    alpha = ['W0', 'W1', ('A', 0), ('A', 1), ('B', 0), ('B', 1)]
    L = 4 if QUICK else 5
    nl = ni = nmis = nmis_inc = 0; nres = [0, 0, 0]; bad = []
    for k in range(L + 1):
        for xa in itertools.product(alpha, repeat=k):
            xa = list(xa); nl += 1
            ya = ab_LInc(xa); r = ab_LIncs(xa, 8); za = ab_LOv(xa)
            if first_bad_W1(xa) is not None:
                nmis += 1
                if r is not None or za is not None: bad.append(('misaligned accepted', xa))
            if linc_reaches_bad(xa):
                nmis_inc += 1
                if ya is not None: bad.append(('LInc_rec misaligned accepted', xa))
            nres[0] += ya is not None; nres[1] += r is not None; nres[2] += za is not None
            for x in all_inst(xa):
                ni += 1
                if ya is not None:
                    y = ex_LInc(x)
                    if y is None or not matches(ya, y): bad.append(('LInc', xa))
                if r is not None:
                    e = ex_LIncs(x)
                    if e is None or not (matches(r[0], e[0]) and e[1] % 2 == r[2] and (e[1] - r[2]) // 2 >= r[1]):
                        bad.append(('LIncs', xa))
                if za is not None:
                    z = ex_LOv(x)
                    if z is None or not matches(za, z): bad.append(('LOv', xa))
    report('A5 all abstract lists <= %d tokens over W0, W1, W10(0..1), W11(0..1): LInc_rec / LIncs_rec / LOv_rec sound '
           'on every instantiation (n = 0..1); misaligned W1 always rejected' % L, not bad,
           '%d lists, %d instantiations, results %d / %d / %d; %d lists with a misaligned W1 (%d reached by LInc_rec)' % (
               nl, ni, nres[0], nres[1], nres[2], nmis, nmis_inc))
    if bad: print('   first failures:', bad[:3])

# ================================================================= I: initial segment
X0 = [int(c) for c in '1000111011']
def P_cells(x): return lmp_cells(x), [0, 1, 0] + RC(1)

def check_I():
    # direct simulation from blank, compare at the claimed steps
    targets = {}
    x1, c0 = ex_step(X0); x2, c1 = ex_step(x1)
    report('I1 exact cycles: count(x0) = 5, count(x1) = 51', (c0, c1) == (5, 51),
           'x1 = %s, x2 = %s' % (''.join(map(str, x1)), ''.join(map(str, x2))))
    for st, x in ((847, X0), (2136, x1), (38573, x2)): targets[st] = x
    t = bytearray(200000); off = 100000; pos = off; q = 'A'
    res = {}
    for step in range(1, 38574):
        w, d, q = TR[(q, t[pos])]
        t[pos] = w; pos += d
        if step in targets:
            L, R = P_cells(targets[step])
            okL = strip0(list(t[:pos + 1])) == strip0(L)
            okR = list(t[pos + 1:pos + 1 + len(R)]) == R and not any(t[pos + 1 + len(R):])
            res[step] = (q == 'D' and okL and okR)
    for st in sorted(targets):
        report('I2 blank ->(%d) P(x) = 0^inf Lmp(x) <D 010 1 011 01 0^inf with x = %s' % (st, ''.join(map(str, targets[st]))), res[st])
    return x2

# ================================================================= C: the abstract chain
def chain(x2, maxv=MAXV, ncyc=192, keep=()):
    xa = ['W0' if d == 0 else 'W1' for d in x2]
    kept = {2: list(xa)}
    info = []
    for k in range(2, 2 + ncyc):
        keep0 = STATS['ov_keep']
        y, n = ab_step(xa, maxv)
        if y is None: return None, k, n, kept, info
        lbs = [t[1] for t in y if isinstance(t, tuple)]
        info.append((k, n, len(y), len(lbs), min(lbs or [None]), STATS['ov_keep'] - keep0, lbs[1] if len(lbs) > 1 else None))
        xa = y
        if (k + 1) in keep: kept[k + 1] = list(xa)
    return xa, 2 + ncyc, None, kept, info

def check_C(x2):
    for kk in STATS: STATS[kk] = 0
    FUEL.update(calls=0, min_slack=None, max_depth=0)
    t0 = time.time()
    keep = set(range(2, 12)) | {50, 100, 150, 190, 193, 194}
    x194, kend, why, kept, info = chain(x2, keep=keep)
    report('C1 abstract chain x2 -> x194: all 192 step_rec calls succeed (maxv = 256)', x194 is not None,
           'failed at cycle %s: %s' % (kend, why) if x194 is None else '%.1fs' % (time.time() - t0))
    if x194 is None: return None, kept
    ns = set(i[1] for i in info)
    report('C2 the count lower bound saturates at maxv in every abstract cycle (n = 256)', ns == {256})
    minl = min(i[4] for i in info)
    report('C3 smallest block bound at any time >= 1 (min l = %d); list length at x194 = %d, blocks = %d' % (minl, info[-1][2], info[-1][3]), minl >= 1)
    report('C4 case counts: LInc through a 10-block %d; of %d W11-block cases in LOv_rec, keep %d, peel %d' % (
        STATS['linc_A'], STATS['ov_w11'], STATS['ov_keep'], STATS['ov_peel1']),
        STATS['ov_keep'] == 191 and STATS['ov_keep'] + STATS['ov_peel1'] == STATS['ov_w11'])
    report('C9 fuel (TM3 convention): every LInc_rec call inside LOv_rec over the chain has enough fuel: %d calls, '
           'min slack %d, max depth %d' % (FUEL['calls'], FUEL['min_slack'], FUEL['max_depth']), FUEL['min_slack'] >= 0)
    keep1 = all(i[5] == 1 and i[6] == 255 for i in info[1:]) and info[0][5] == 0
    report('C4b in every cycle from 3 on, keep is used exactly once, on the block made in the previous cycle (its bound stays 255)', keep1)
    lbs = [t[1] for t in x194 if isinstance(t, tuple)]
    report('C5 block bounds at x194 (head first): newest %d, oldest %d' % (lbs[0], lbs[-1]), lbs[0] == 255 and lbs[-1] >= 1)
    # block i (0 = newest) was made in cycle 193 - i and processed in i cycles: 1 keep + (i-1) peels + hits LInc stops
    hits = [256 - i - lbs[i] for i in range(1, len(lbs))]
    report('C5b LInc stops per block over its life: between 0 and 3 (max %d, total %d)' % (max(hits), sum(hits)),
           min(hits) >= 0 and max(hits) <= 3)
    # smaller maxv: 195 still works, 194 fails (margin)
    lo_ok = chain(x2, maxv=194)[0] is not None
    lo_bad = chain(x2, maxv=193)[0] is None
    report('C6 margin: maxv = 194 also succeeds, maxv = 193 fails (so 256 leaves 62 to spare)', lo_ok and lo_bad)
    # starting the abstract chain earlier fails: the blocks of cycles 0 and 1 are short
    fails = []
    for k0, x in ((0, X0), (1, ex_step(X0)[0])):
        xa = ['W0' if d == 0 else 'W1' for d in x]; k = k0
        while k < 194:
            xa, why = ab_step(xa)
            if xa is None: break
            k += 1
        fails.append(k)
    report('C8 abstract chain started at x0 fails in cycle %d, started at x1 fails in cycle %d (so start at x2)' % tuple(fails),
           fails[0] < 194 and fails[1] < 194)
    # cross-check with the observe-stage stack model
    try:
        sys.path.insert(0, os.path.join(HERE, 'work', 'model'))
        import fast
        sys.setrecursionlimit(1000000)
        y = fast.from_bits_near_first(X0)
        same = True; first_diff = None
        for k in range(194):
            y, c = fast.step(y)
            if (k + 1) in kept:
                a = canon_ab(kept[k + 1]); b = canon_fast(y)
                if a != b:
                    same = False; first_diff = k + 1; break
        report('C7 abstract chain = fast.py stack model (BIG blocks) at cycles %s' % sorted(kept), same,
               '' if same else 'first difference at cycle %d' % first_diff)
    except ImportError:
        report('C7 fast.py present', False)
    return x194, kept

def canon_tokens(items):
    """items head-first: 'W0', 'W1', 'X' (a 10-block), 'Y' (an 11-block). Parse into tokens from the head and
    absorb explicit pairs next to a block of the same kind (both models allow that: a block's length is free)."""
    toks = []; i = 0
    while i < len(items):
        h = items[i]
        if h in ('X', 'Y'): toks.append(h); i += 1
        elif h == 'W0': toks.append('S'); i += 1
        else:
            toks.append('P0' if items[i+1] == 'W0' else 'P1'); i += 2
    out = []
    for t in toks:
        if out and ((t == 'P0' and out[-1] == 'X') or (t == 'P1' and out[-1] == 'Y')): continue
        if t in ('X', 'Y'):
            while out and out[-1] == ('P0' if t == 'X' else 'P1'): out.pop()
            if out and out[-1] == t: continue
        out.append(t)
    return ' '.join(out)
def canon_ab(xa):
    return canon_tokens([('X' if t[0] == 'A' else 'Y') if isinstance(t, tuple) else t for t in xa])
def canon_fast(y):
    items = []
    for it in reversed(y):
        if isinstance(it, tuple):
            t, k = it
            if k >= 10**12: items.append('X' if t == 'A' else 'Y')
            else: items += (['W1', 'W0'] if t == 'A' else ['W1', 'W1']) * k
        else: items.append('W0' if it == 0 else 'W1')
    return canon_tokens(items)

# ================================================================= H: the halt
XFAR_AB = ['W0' if d == 0 else 'W1' for d in XFAR]
def doom_rec(X):
    """proof.md 9.4 written as a loop. At each position: first, is the rest equal to x_far' (list equality)?
    Only then strip one prefix token W0', W1' W1' or W11 l. Returns (result, position reached)."""
    i = 0
    while True:
        if len(X) - i == len(XFAR_AB) and X[i:] == XFAR_AB: return True, i
        if i < len(X) and X[i] == 'W0': i += 1
        elif i + 1 < len(X) and X[i] == 'W1' and X[i+1] == 'W1': i += 2
        elif i < len(X) and isinstance(X[i], tuple) and X[i][0] == 'B': i += 1
        else: return False, i

def run_doomed(x):
    """Lmp x <D 010 1 r with r unknown: number of steps to the halt (F reads 1), None otherwise."""
    s = PSim(lmp_cells(x), 'D', [0, 1, 0, 1], 'L', 0, U, margin=100)
    rb = s.b + 4
    try:
        s.run(10**7, stop=lambda mm: mm.pos >= rb)
    except ReadUnknown:
        return None
    return s.steps if (s.halted and s.st == 'F' and s.t[s.pos] == 1) else None

def check_H(x194):
    r = ab_LIncs(x194)
    x0a, n, m = r
    report('H1 cycle 194: LIncs_rec gives m = 1 (count odd) and n = 256', (n, m) == (256, 1))
    report('H2 LOv_rec(x0) fails (the overflow does not complete)', ab_LOv(x0a) is None)
    xfa = ['W0' if d == 0 else 'W1' for d in XFAR]
    k = len(x0a) - len(xfa)
    tail_ok = x0a[k:] == xfa
    pre = x0a[:k]; i = 0; pre_ok = True; ntok = {'S': 0, 'P': 0, 'B': 0}
    while i < len(pre):
        if pre[i] == 'W0': ntok['S'] += 1; i += 1
        elif pre[i] == 'W1' and i + 1 < len(pre) and pre[i+1] == 'W1': ntok['P'] += 1; i += 2
        elif isinstance(pre[i], tuple) and pre[i][0] == 'B': ntok['B'] += 1; i += 1
        else: pre_ok = False; break
    report('H3 x0 = prefix ++ x_far, x_far = (W1 W1 W0)^5 (W1 W1)^3 (21 words), prefix = %d W0 + %d pairs + %d 11-blocks' % (
        ntok['S'], ntok['P'], ntok['B']), tail_ok and pre_ok)
    # far tail in LOv terms: the far 3 + 2j tokens (W1 W1 W0)^j (W1 W1)^3
    res = [ex_LOv([1, 1, 0] * j + [1, 1] * 3) for j in range(5)]
    vals = [None if r is None else ''.join(map(str, r)) for r in res]
    report('H4 LOv on the far 3 + 2j tokens: defined for j = 0..3, undefined for j = 4 (LInc carries off)',
           all(r is not None for r in res[:4]) and res[4] is None,
           'j=0..3: ' + ', '.join(vals[:4]))
    # doom_rec of proof.md 9.4: equality with x_far' first, then strip one token
    res6 = doom_rec(x0a)
    report("H6 doom_rec(x0) = true; it meets x_far' at list position %d = the split of H3" % res6[1], res6 == (True, k))
    # doom_rec soundness on random abstract lists: true => every instantiation halts (F reads 1), r never read,
    # after 19 steps per W0 + 12 per W1 W1 pair of the prefix + 1,368
    rng = random.Random(7)
    ntrue = nfalse = nrun = 0; okd = True
    for _ in range(80 if QUICK else 300):
        pre = []
        for _ in range(rng.randint(0, 12)):
            u = rng.random()
            if u < 0.35: pre.append('W0')
            elif u < 0.65: pre += ['W1', 'W1']
            elif u < 0.9: pre.append(('B', rng.randint(0, 3)))
            elif u < 0.95: pre += ['W1', 'W0']
            else: pre.append(('A', rng.randint(0, 3)))
        xa = pre + (xfa if rng.random() < 0.9 else xfa[2:])
        dr, pos = doom_rec(xa)
        if not dr: nfalse += 1; continue
        ntrue += 1
        for _ in range(2):
            x = inst(xa, rng)
            p = len(x) - len(XFAR); nw0 = x[:p].count(0); npairs = (p - nw0) // 2
            nrun += 1
            okd &= run_doomed(x) == 19 * nw0 + 12 * npairs + 1368
    report('H7 doom_rec sound on random lists: every instantiation of a true case halts (F reads 1, r never read) '
           'in 19 #W0 + 12 #pairs + 1368 steps', okd and ntrue > 0, '%d true (%d runs), %d false' % (ntrue, nrun, nfalse))
    # whole instantiated overflow, direct (partial) simulation: walk-in through the prefix, halt in the far tail
    for fixed in (0, 1):
        x = inst(x0a, None, fixed=fixed)
        s = PSim(lmp_cells(x), 'D', [0, 1, 0, 1], 'L', 0, U, margin=100)
        far = s.base; rb = s.b + 4
        good = True
        try:
            s.run(10**8, stop=lambda mm: mm.pos >= rb)
        except ReadUnknown:
            good = False
        good = good and s.halted and s.st == 'F'
        # predicted steps: walk-in 19 per W0 and 12 per W1 W1 pair, then 1,368
        npairs = (len(x) - len(XFAR) - x[:len(x) - len(XFAR)].count(0)) // 2
        nw0 = x[:len(x) - len(XFAR)].count(0)
        pred = 19 * nw0 + 12 * npairs + 1368
        report('H5 instantiated cycle-194 overflow (blocks = bound + %d): halts, F reads 1, at far%+d after %d steps (= 19*%d + 12*%d + 1368)' % (
            fixed, s.pos - far, s.steps, nw0, npairs), good and s.steps == pred and s.pos - far == 60, 'words %d' % len(x))

# ================================================================= D: direct simulation of abstract cycles
def check_D(kept):
    ks = [k for k in sorted(kept) if k <= (6 if QUICK else 9)]
    if HEAVY: ks += [50]
    tot = ok = 0
    for k in ks:
        xa = kept[k]
        if k == 194: continue
        y, n = ab_step(xa)
        x0a, nn, mm = ab_LIncs(xa)
        for fixed in ((0,) if QUICK else (0, 1)):
            # Ov phase only (the Incs phase has 2^256+ bounces): run Lmp(inst x0) <D 010 RC(2m+2) for small m
            x0 = inst(x0a, None, fixed=fixed)
            v = ex_LOv(x0)
            mq = 1 + fixed
            tgt = [1, 0] * mq + [1, 1] + v[1:]
            steps = run_target_D(x0, 2 * mq + 2, tgt, 1, 10**8)
            good = steps is not None and matches(y[1:], [1, 1] + v[1:])
            tot += 1; ok += good
    report('D1 instantiated abstract cycles %s: Ov phase on the tape reaches the exact next P-config, and the abstract step matches it' % ks, ok == tot, '%d/%d' % (ok, tot))

# ================================================================= main
if __name__ == '__main__':
    t0 = time.time()
    check_T()
    check_W()
    check_L()
    check_A()
    check_A5()
    x2 = check_I()
    x194, kept = check_C(x2)
    if x194 is not None:
        check_H(x194)
        check_D(kept)
    nf = sum(1 for _, o in RESULTS if not o)
    print('SUMMARY %d checks, %d FAIL (%.0fs)' % (len(RESULTS), nf, time.time() - t0))
    sys.exit(1 if nf else 0)