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

proof.md proves that W5-8 never halts:
  * two shift rules R1 (C> 11 --> 10 C>) and R2b (0 10 B> 000 --> 0 B> 000 11; it needs the 0 on the left),
    exact finite runs + induction;
  * five macro rules on the family K(n,a,b,c,d) (S, TE, TO, T6, T8), each proved for its whole domain by
    symbolic execution (scripts/symexec.py: concrete transitions, R1/R2b on symbolic blocks, case splits);
    S is also given as twelve one-trip phase rules P1..P12, and TE and TO as one-trip rules in Appendices A, B;
  * the double cycle Even(n,x) --> Even(n+12x+808, x+32) (x = 4 mod 8, x >= 52, n odd), by arithmetic on the
    rule domains;
  * the opening: blank --(4,097,897)--> K(1959,34,68,45,18), then 20 macro steps to Even(12863,212) at step
    153,126,993.

Sections (proof.md section in brackets):
  T    [1,2]  table facts: only D0 undefined, D entered only by A1; the string is line 214 of the 740 list;
              G (43 cells) and the K word
  SR   [3.1]  R1, R2b (and R2a, unused) as exact window runs that never leave the window; k-fold forms for
              k <= 40 in random contexts; R2b and R2a fail with a 1 on the left
  ENG  [3.2]  the symbolic executor against direct simulation: random symbolic tapes, random branches,
              random values; exact tape, head, state, step count; an unsound variant is caught
  MR   [3.2-3.4] S, TE, TO, T6, T8 by the executor: every leaf reaches the claimed configuration; step formula;
              no D0; R2a never used; the case splits
  PH   [3.3]  the twelve phase rules P1..P12 of S, each by the executor, and their step sum = S's formula
  COL  [3.4, App. A, B] the per-trip tables of TE and TO, parsed from proof.md: row 0 and the last row are the
              rule's start and end; every row by the executor from the row above (one branch, exact steps, R1 and
              R2b only); the step column sums to the rule's formula; the described structure; direct simulation
  DIR  [3.3, 3.4] every macro rule and phase rule by direct simulation: exhaustive boxes at the bottom of each
              domain + random large values; exact configuration and step count
  TEETH[3.3]  each lower bound of S is sharp: one below it the claimed result fails (direct)
  DC   [4]    the double cycle: every rule application inside its domain (x = 52 .. 3,996), the n and x
              updates; direct simulation of whole double cycles
  OPEN [5]    the opening: 4,097,897 steps to K(1959,34,68,45,18) (and no K-shaped left record before it);
              the 20 macro steps, their domains and step formulas; direct simulation of every checkpoint;
              Even(12863,212) at 153,126,993
  ORB  [4, 5] the law's orbit vs the observe-stage table work/run_starts_K.tsv (run to 1e10)
  HALT [7.1]  the executor raises on D0 (control); no leaf of any rule reads D0; no halt in the opening
  PLAN [8]    the Rocq-outline statements in half-length form (Kr, Ev) equal the rules; the DC chain's arguments
  DOC  [*]    proof.md quotes the rule statements, the phase table, the R2b trace and the opening table as checked
              here; proof.md before section 9 (sections 0-8 and the appendices) passes tools/writeup_lint.py
              with 0 errors
Usage: python3 -B check_proof.py [--seed S] [--quick|--full] [--only T,SR,...]
"""
import os
import random
import re
import subprocess
import sys
import time

HERE = os.path.dirname(os.path.abspath(__file__))
ROOT = os.path.abspath(os.path.join(HERE, '..', '..'))
sys.path.insert(0, os.path.join(HERE, 'scripts'))
import symexec as sx  # noqa: E402
from symexec import L, add, show, subst_expr, V2  # noqa: E402

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
ONLY = set(sys.argv[sys.argv.index('--only') + 1].split(',')) if '--only' in sys.argv else None
RNG = random.Random(SEED)
RES, ORDER = {}, []
T0 = time.time()
TM = sx.TM
TABLE = sx.TABLE
G = sx.G
Kstr = sx.Kstr


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 scale(q, d, f):
    return q if QUICK else (f if FULL else d)


# ------------------------------------------------------------------ C batch runner
KRUN = os.path.join(HERE, 'work', 'krun')


def build_krun():
    src = os.path.join(HERE, 'scripts', 'krun.c')
    if not os.path.exists(KRUN) or os.path.getmtime(KRUN) < os.path.getmtime(src):
        os.makedirs(os.path.dirname(KRUN), exist_ok=True)
        subprocess.run(['gcc', '-O2', '-o', KRUN, src], check=True)


def krun(jobs):
    """jobs: list of (state, headidx, nrec, maxsteps, tape) -> list of (kind, steps, state, headoff, word)"""
    if not jobs:
        return []
    inp = ''.join('%s %d %d %d %s\n' % j for j in jobs)
    out = subprocess.run([KRUN], input=inp, capture_output=True, text=True, check=True).stdout.split('\n')
    res = []
    for line in out:
        if not line:
            continue
        k, s, q, h, w = line.split()
        res.append((k, int(s), q, int(h), w))
    assert len(res) == len(jobs)
    return res


def rstrip0(w):
    return w.rstrip('0')


# ------------------------------------------------------------------ python reference simulator (small runs)
def run_window(cells, pos, st, nsteps):
    """run on a finite window; return (cells, pos, st, max_lo, max_hi) or None if the head reads outside"""
    cells = list(cells)
    for _ in range(nsteps):
        if not 0 <= pos < len(cells):
            return None
        tr = TABLE[(st, cells[pos])]
        if tr is None:
            return None
        cells[pos] = tr[0]
        pos += tr[1]
        st = tr[2]
    return cells, pos, st


def run_dict(tape, pos, st, nsteps):
    """unbounded reference run: tape = dict pos->bit"""
    for i in range(nsteps):
        tr = TABLE[(st, tape.get(pos, 0))]
        if tr is None:
            return ('HALT', i, tape, pos, st)
        tape[pos] = tr[0]
        pos += tr[1]
        st = tr[2]
    return ('OK', nsteps, tape, pos, st)


# ------------------------------------------------------------------ expressions in the original variables
VARS = 'nabcd'


def parse_lin(s):
    """'n+3', 'a-2', '2b+5', 'c', '7n+14a+1135' -> {var: coef, '': const}"""
    s = s.replace(' ', '').replace('-', '+-')
    d = {'': 0}
    for term in s.split('+'):
        if not term:
            continue
        m = re.fullmatch(r'(-?\d*)([a-z]?)', term)
        assert m, term
        co, v = m.groups()
        if v:
            c = int(co) if co not in ('', '-') else (-1 if co == '-' else 1)
            d[v] = d.get(v, 0) + c
        else:
            d[''] += int(co)
    return d


def parse_word(s):
    """'1^(n+3) 0^3 1^2 0 1^c' -> tokens with exponents as linear forms in the ORIGINAL variables"""
    toks = []
    for t in s.split():
        m = re.fullmatch(r'([01])(?:\^(\d+|\([^)]*\)|[a-z]))?', t)
        assert m, t
        sym, ex = m.groups()
        e = {'': 1} if ex is None else (parse_lin(ex.strip('()')) if not ex.isdigit() else {'': int(ex)})
        toks.append((sym, e))
    return toks


def word_value(toks, val):
    return ''.join(sym * sx.ev(e, val) for sym, e in toks)


def word_tokens(toks, forms):
    """tokens with original-variable exponents -> executor tokens, via forms: var -> linear form"""
    out = []
    for sym, e in toks:
        f = subst_expr(e, forms)
        if sym == '1':
            out.append(('1', f))
        else:
            assert sx.isconst(f), (sym, e)
            out += [('0',)] * sx.const(f)
    return out


# ------------------------------------------------------------------ the rules (proof.md sections 1, 3.3, 3.4)
# domain: var -> (parity residue, lower bound) or an exact constant
RULES = {
    'S':  dict(dom={'n': (1, 1), 'a': (0, 10), 'b': (0, 6), 'c': (1, 7), 'd': (0, 2)}, trips=12,
               to='n+48,a-8,b+4,c,d+4', steps='84n+84a+77b+70c+63d+13628'),
    'TE': dict(dom={'n': (1, 1), 'a': 4, 'b': (0, 88), 'c': 35, 'd': (0, 20)}, trips=138,
               to='n+556,b-86,82,d+51,18', steps='966n+952b+812d+455332'),
    'TO': dict(dom={'n': (1, 1), 'a': 2, 'b': (0, 82), 'c': (1, 37), 'd': (0, 18)}, trips=147,
               to='n+588,b+c-91,d+62,35,18', steps='1029n+1001b+987c+882d+458476'),
    'T6': dict(dom={'n': (1, 1), 'a': 6, 'b': (0, 82), 'c': (1, 35), 'd': (0, 18)}, trips=147,
               to='n+592,b+c-91,d+62,35,18', steps='1029n+1008b+987c+882d+462814'),
    'T8': dict(dom={'n': (1, 1), 'a': 8, 'b': (0, 88), 'c': 35, 'd': (0, 20)}, trips=135,
               to='n+540,b-74,86,d+47,18', steps='945n+938b+784d+446893'),
}

# the twelve phases of S: K_j = 0^inf <F G w_j 0^inf  (G includes its last two 0s)
PHASES = [
    '1^n 0 1^a 0 1^2 0 1^b 0^6 1^c 0 1^2 0 1^4 0^6 1^d 0 1^2 0^2 1^2 0 1^3',
    '1^(n+3) 0^3 1^(a-2) 0^6 1^(b-2) 0^2 1^2 0^2 1^(c+3) 0^3 1^2 0^2 1^2 0^2 1^(d+2) 0 1^2 0 1^6 0 1^2',
    '1^(n+7) 0 1^2 0^2 1^(a-4) 0^2 1^4 0^6 1^(b-1) 0 1^2 0 1^(c-1) 0^6 1^6 0^6 1^(d+5)',
    '1^(n+12) 0^2 1^(a-4) 0^2 1^4 0^6 1^(b-1) 0 1^2 0 1^(c-1) 0^6 1^6 0^6 1^(d+5)',
    '1^(n+15) 0^2 1^(a-2) 0^12 1^(b-1) 0 1^(c-1) 0^6 1^6 0^6 1^(d+5)',
    '1^(n+19) 0 1^2 0 1^(a-4) 0 1^2 0^7 1^(b-1) 0 1^(c-1) 0^6 1^6 0^6 1^(d+5)',
    '1^(n+24) 0 1^(a-4) 0 1^2 0^7 1^(b-1) 0 1^(c-1) 0^6 1^6 0^6 1^(d+5)',
    '1^(n+27) 0^3 1^(a-6) 0^2 1^4 0 1^(b+1) 0 1^(c-1) 0^6 1^6 0^6 1^(d+5)',
    '1^(n+31) 0 1^2 0^2 1^(a-8) 0^2 1^(b+8) 0^2 1^(c-1) 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3',
    '1^(n+36) 0^2 1^(a-8) 0^2 1^(b+8) 0^2 1^(c-1) 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3',
    '1^(n+39) 0^2 1^(a-6) 0^6 1^(b+4) 0^6 1^c 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3',
    '1^(n+43) 0 1^2 0 1^(a-8) 0 1^2 0 1^(b+4) 0^6 1^c 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3',
    '1^(n+48) 0 1^(a-8) 0 1^2 0 1^(b+4) 0^6 1^c 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3',
]
PHASE_STEPS = ['7n+7a+7b+14c+14d+1135', '7n+14a+28b+14c+21d+1459', '7n+841', '7n+14a+7b+933', '7n+7a+897',
               '7n+925', '7n+7a+971', '7n+14a+21b+28c+28d+2247', '7n+1009', '7n+14a+14b+14c+1081', '7n+7a+1037',
               '7n+1093']
GWORD = '0' + G          # the head cell (F reads it) and G


def dom_forms(dom):
    """original variable -> linear form in fresh variables (v = 2v' + low, or a constant)"""
    f = {}
    for v in VARS:
        x = dom[v]
        f[v] = L(x) if isinstance(x, int) else V2(x[1], v)
    return f


def K_forms(dom):
    return dom_forms(dom)


def end_forms(rule, forms):
    exprs = [parse_lin(e) for e in RULES[rule]['to'].split(',')]
    return [subst_expr(e, forms) for e in exprs]


def dom_sample_box(dom, k):
    """all values in the box: each variable over its first k admissible values"""
    import itertools
    axes = []
    for v in VARS:
        x = dom[v]
        axes.append([x] if isinstance(x, int) else [x[1] + 2 * i for i in range(k)])
    return [dict(zip(VARS, p)) for p in itertools.product(*axes)]


def dom_sample_rand(dom, hi, rng):
    val = {}
    for v in VARS:
        x = dom[v]
        val[v] = x if isinstance(x, int) else x[1] + 2 * rng.randrange(0, hi)
    return val


def in_dom(dom, val):
    for v in VARS:
        x = dom[v]
        if isinstance(x, int):
            if val[v] != x:
                return False
        elif val[v] % 2 != x[0] or val[v] < x[1]:
            return False
    return True


_PC = {}


def _parsed(rule):
    if rule not in _PC:
        _PC[rule] = ([parse_lin(e) for e in RULES[rule]['to'].split(',')], parse_lin(RULES[rule]['steps']))
    return _PC[rule]


def apply_rule(rule, val):
    return {v: sx.ev(e, val) for v, e in zip(VARS, _parsed(rule)[0])}


def rule_steps(rule, val):
    return sx.ev(_parsed(rule)[1], val)


def Kval(val):
    return Kstr(*[val[v] for v in VARS])


# ================================================================== T
def check_T():
    rec('T.machine_string', TM == '1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF')
    lines = open(os.path.join(ROOT, 'data', 'holdouts', 'BB6_holdouts_740.txt')).read().split('\n')
    rec('T.holdout_740_line214_byte_exact', lines[213] == TM, lines[213])
    und = [k for k, v in TABLE.items() if v is None]
    rec('T.only_D0_undefined', und == [('D', 0)], und)
    into_D = [k for k, v in TABLE.items() if v and v[2] == 'D']
    rec('T.D_entered_only_by_A1', into_D == [('A', 1)], into_D)
    rec('T.A1_writes1_moves_left', TABLE[('A', 1)] == (1, -1, 'D'))
    rec('T.D1_is_1LE', TABLE[('D', 1)] == (1, -1, 'E'))
    rec('T.G_is_43_cells', len(G) == 43 and word_value(parse_word(GWORD_RUNS), {}) == '0' + G)
    # the K word of proof.md 2 equals Kstr
    w = parse_word('0 0^2 1^2 0 1^4 0 1^2 0 1^6 0 1^2 0 1^5 0^2 1^2 0 1^5 0 1^2 0^2 ' + PHASES[0])
    for _ in range(50):
        val = dom_sample_rand(RULES['S']['dom'], 50, RNG)
        rec('T.K_word_matches_Kstr', word_value(w, val) == Kval(val), val)


# ================================================================== SR
SHIFT = {
    # name: (window before, head index, state, steps, window after, head index after, state after)
    'R1': ('11', 0, 'C', 2, '10', 2, 'C'),
    'R2b': ('010000', 3, 'B', 12, '000011', 1, 'B'),
    'R2a': ('010110', 5, 'C', 12, '011011', 3, 'C'),
}


def check_SR():
    for name, (w0, h0, s0, n, w1, h1, s1) in SHIFT.items():
        cells = [int(c) for c in w0]
        # exact run that never reads outside the window (the last move may leave it: R1 ends just right of it)
        st, pos, ok = s0, h0, True
        for i in range(n):
            if not 0 <= pos < len(cells):
                ok = False
                break
            tr = TABLE[(st, cells[pos])]
            if tr is None:
                ok = False
                break
            cells[pos] = tr[0]
            pos += tr[1]
            st = tr[2]
        rec('SR.%s_window_run' % name, ok and ''.join(map(str, cells)) == w1 and pos == h1 and st == s1,
            (cells, pos, st))
        # k-fold form in random contexts, by unbounded simulation
        for k in range(0, 41):
            for _ in range(scale(2, 5, 20)):
                lc = [RNG.randrange(2) for _ in range(RNG.randrange(0, 8))]
                rc = [RNG.randrange(2) for _ in range(RNG.randrange(0, 8))]
                if name == 'R1':
                    word = lc + [1, 1] * k + rc
                    pos = len(lc)
                    exp = lc + [1, 0] * k + rc
                    epos = len(lc) + 2 * k
                    steps = 2 * k
                elif name == 'R2b':
                    word = lc + [0] + [1, 0] * k + [0, 0, 0] + rc
                    pos = len(lc) + 1 + 2 * k
                    exp = lc + [0] + [0, 0, 0] + [1, 1] * k + rc
                    epos = len(lc) + 1
                    steps = 12 * k
                else:
                    word = lc + [0] + [1, 0] * k + [1, 1, 0] + rc
                    pos = len(lc) + 1 + 2 * k + 2
                    exp = lc + [0] + [1, 1, 0] + [1, 1] * k + rc
                    epos = len(lc) + 3
                    steps = 12 * k
                tape = {i: b for i, b in enumerate(word)}
                kind, ns, tape, p, st = run_dict(tape, pos, s0, steps)
                got = [tape.get(i, 0) for i in range(min(tape) if tape else 0, max(len(word), max(tape) + 1))]
                ok = kind == 'OK' and st == s0 and p == epos and all(
                    tape.get(i, 0) == (exp[i] if 0 <= i < len(exp) else 0) for i in range(-3, len(word) + 3))
                rec('SR.%s_kfold_k<=40' % name, ok, (k, lc, rc, got))
        if name != 'R1':
            # teeth: with a 1 left of the crossed copies the 12-step result is different
            cells = [1] + [int(c) for c in w0[1:]]
            tape = {i: b for i, b in enumerate(cells)}
            kind, ns, tape, p, st = run_dict(tape, h0, s0, n)
            got = ''.join(str(tape.get(i, 0)) for i in range(len(cells)))
            rec('SR.%s_needs_the_0_on_the_left' % name, not (got == w1 and p == h1 and st == s1), (got, p, st))


# ================================================================== ENG
def rand_tokens(rng, vars_):
    toks = []
    for _ in range(rng.randrange(3, 14)):
        r = rng.random()
        if r < 0.35:
            toks.append(('0',))
        elif r < 0.55:
            toks.append(('1', L(1)))
        elif r < 0.8:
            v = rng.choice(vars_)
            toks.append(('1', L(rng.randrange(0, 4), **{v: 2})))
        else:
            v = rng.choice(vars_)
            toks.append(('10', L(rng.randrange(0, 3), **{v: 1})))
    return toks


def tok_cells(toks, val):
    out = []
    for t in toks:
        if t[0] == '0':
            out.append(0)
        elif t[0] == '1':
            out += [1] * sx.ev(t[1], val)
        else:
            out += [1, 0] * sx.ev(t[1], val)
    return out


def rand_case(rng, vars_):
    """a random symbolic configuration; half of them are set up so that a shift rule fires at once"""
    left = rand_tokens(rng, vars_)
    right = rand_tokens(rng, vars_)
    st = rng.choice('ABCDEF')
    r = rng.random()
    v = rng.choice(vars_)
    X = L(rng.randrange(0, 2), **{v: 1})
    if r < 0.15:          # R1
        st = 'C'
        right = [('1', L(rng.randrange(0, 3), **{v: 2}))] + right
    elif r < 0.35:        # R2b, with a random cell (or block) left of the crossed copies
        st = 'B'
        left = left + [('10', X)]
        right = [('0',)] * 3 + right
    elif r < 0.5:         # R2a
        st = 'C'
        left = left + [('10', X), ('1', L(2))]
        right = [('0',)] + right
    return left, st, right


def eng_case(strict):
    vars_ = ['u', 'v', 'w']
    left, st, right = rand_case(RNG, vars_)
    ex = sx.Exec(left, st, right)
    ex.strict = strict
    start_left, start_right = list(left), list(right)
    sub = {}
    nst = RNG.randrange(1, 300)
    halted = False
    try:
        for _ in range(nst):
            while True:
                try:
                    ex.step()
                    break
                except sx.NeedSplit as ns:
                    s1 = {ns.var: L(0)} if RNG.random() < 0.4 else {ns.var: L(1, **{ns.var: 1})}
                    ex = ex.subst(s1)
                    sub = sx.compose(sub, s1)
    except sx.Halt:
        halted = True
    fired = sum(ex.uses.values())
    # instantiate: fresh values for the leaf variables
    fv = {v: RNG.randrange(0, 6) for v in vars_}
    orig = {v: sx.ev(sub[v], fv) if v in sub else fv[v] for v in vars_}
    lc, rc = tok_cells(start_left, orig), tok_cells(start_right, orig)
    tape = {i - len(lc): b for i, b in enumerate(lc + rc)}
    steps = sx.ev(ex.steps, fv)
    kind, ns_, tape, pos, st2 = run_dict(tape, 0, st, steps)
    el = tok_cells(ex.left, fv)
    er = tok_cells(list(reversed(ex.right)), fv)
    ok = (kind == 'OK') and st2 == ex.st
    if ok:
        # compare all cells relative to the head
        span = range(-len(el) - 5, len(er) + 5)
        for off in span:
            want = el[len(el) + off] if -len(el) <= off < 0 else (er[off] if 0 <= off < len(er) else 0)
            if tape.get(pos + off, 0) != want:
                ok = False
                break
        # and nothing nonzero outside the engine's words
        if ok:
            for p_, b in tape.items():
                if b and not (pos - len(el) <= p_ < pos + len(er)):
                    ok = False
                    break
    if halted:
        # the engine stopped before a '---'; the direct run must also stop there after `steps` steps
        ok = kind == 'OK' and TABLE[(st2, tape.get(pos, 0))] is None
    return ok, fired, (start_left, st, start_right, sub, fv)


def check_ENG():
    n_cases = scale(400, 2000, 10000)
    fired = 0
    for _ in range(n_cases):
        ok, f, info = eng_case(True)
        fired += f > 0
        rec('ENG.differential_random_symbolic_tapes', ok, info)
    rec('ENG.a_shift_rule_fired_in_>=30%_of_cases', fired >= 0.3 * n_cases, (fired, n_cases))
    # teeth: the same test catches an executor that drops R2a/R2b's 0-on-the-left condition
    bad = sum(not eng_case(False)[0] for _ in range(n_cases))
    rec('ENG.teeth_unsound_variant_is_caught', bad > 0, bad)


# ================================================================== MR, PH
LEAVES = {}


def leaf_orig(sub, forms):
    """the original variables as linear forms in the leaf's variables"""
    return {v: subst_expr(forms[v], sub) for v in VARS}


def check_MR():
    for rule, R in RULES.items():
        forms = K_forms(R['dom'])
        t = time.time()
        lv = sx.prove_K_rule(forms, lambda f, rule=rule: end_forms(rule, f), 2 * R['trips'])
        LEAVES[rule] = lv
        rec('MR.%s_all_leaves_reach_claimed_K' % rule, all(l.ok for l in lv), [(l.sub, l.ok) for l in lv])
        claimed = parse_lin(R['steps'])
        for l in lv:
            o = leaf_orig(l.sub, forms)
            rec('MR.%s_step_formula_exact' % rule, sx.eqexpr(subst_expr(claimed, o), l.ex.steps),
                (show(subst_expr(claimed, o)), show(l.ex.steps)))
            rec('MR.%s_no_D0' % rule, 'D0' not in l.ex.trans, l.ex.trans)
            rec('MR.%s_R2a_unused' % rule, l.ex.uses['R2a'] == 0, l.ex.uses)
        splits = sorted({k for l in lv for k in l.sub})
        exp_splits = ['d'] if rule == 'S' else []
        rec('MR.%s_case_splits' % rule, splits == exp_splits and len(lv) == (2 if rule == 'S' else 1), splits)
        # the same leaves without R2a in the rule set
        lv2 = sx.prove_K_rule(forms, lambda f, rule=rule: end_forms(rule, f), 2 * R['trips'], rules=('R1', 'R2b'))
        rec('MR.%s_proved_with_R1_R2b_only' % rule, all(l.ok for l in lv2) and len(lv2) == len(lv))
        RES.setdefault('_info', {}).setdefault('MR', {})[rule] = {
            'leaves': [{k: show(v) for k, v in l.sub.items()} for l in lv],
            'concrete_steps': [l.ex.nconc for l in lv], 'R1': [l.ex.uses['R1'] for l in lv],
            'R2b': [l.ex.uses['R2b'] for l in lv], 'sec': round(time.time() - t, 1)}


def check_PH():
    dom = RULES['S']['dom']
    forms = K_forms(dom)
    words = [parse_word(GWORD_RUNS + ' ' + w) for w in PHASES]
    tot = {'': 0}
    for j in range(12):
        ex = sx.Exec([], 'F', word_tokens(words[j], forms))
        lv = sx.explore(ex, 2, lambda sub, j=j: word_tokens(words[j + 1], {v: subst_expr(forms[v], sub) for v in VARS}))
        claimed = parse_lin(PHASE_STEPS[j])
        tot = add(tot, claimed)
        ok = all(l.ok for l in lv)
        rec('PH.P%d_by_executor' % (j + 1), ok, [(l.sub, fmt_got(l)) for l in lv if not l.ok])
        for l in lv:
            o = leaf_orig(l.sub, forms)
            rec('PH.P%d_step_formula' % (j + 1), sx.eqexpr(subst_expr(claimed, o), l.ex.steps),
                (show(subst_expr(claimed, o)), show(l.ex.steps)))
            rec('PH.no_D0', 'D0' not in l.ex.trans)
    rec('PH.sum_of_phase_steps_is_S_formula', sx.eqexpr(tot, parse_lin(RULES['S']['steps'])), show(tot))
    rec('PH.P13_word_is_K(n+48,a-8,b+4,c,d+4)', all(
        word_value(words[12], val) == Kval(apply_rule('S', val))
        for val in [dom_sample_rand(dom, 40, RNG) for _ in range(30)]))


def fmt_got(l):
    return sx.fmt(l.got)[:200]


GWORD_RUNS = '0 0^2 1^2 0 1^4 0 1^2 0 1^6 0 1^2 0 1^5 0^2 1^2 0 1^5 0 1^2 0^2'


# ================================================================== COL
# proof.md Appendices A and B: one row per trip, 'trip  steps  word-after-G'; row 0 is the start word
APPENDIX = {'TE': 'Appendix A', 'TO': 'Appendix B'}
# the described structure (proof.md 3.4): rows 12j (j >= 1): first block n + base + 48(j-1), and the second
# variable block = shrink - 8(j-1); in TO the b and c blocks merge first at trip 10
S_PATTERN = {'TE': (52, 'b-2'), 'TO': (48, 'b+c-3')}


def appendix_rows(rule):
    t = open(os.path.join(HERE, 'proof.md')).read()
    i = t.index('\n## %s.' % APPENDIX[rule])
    blocks = t[i:].split('```')
    blk = blocks[3]                       # [1] is the rule statement, [3] the table
    lines = [ln for ln in blk.split('\n') if ln.strip()]
    assert lines[0].split()[0] == 'trip', lines[0]
    rows = []
    for ln in lines[1:]:
        m = re.fullmatch(r'\s*(\d+)\s+(\S+)\s+(\S.*\S)\s*', ln)
        assert m, ln
        rows.append((int(m.group(1)), m.group(2), m.group(3)))
    return rows


def var_tokens(toks):
    """the 1-blocks of a parsed word whose exponent has a variable, as (index, form)"""
    return [(i, e) for i, (sym, e) in enumerate(toks) if any(k != '' and c for k, c in e.items())]


def check_COL():
    words_all = {}
    for rule in ('TE', 'TO'):
        R = RULES[rule]
        dom = R['dom']
        forms = K_forms(dom)
        try:
            rows = appendix_rows(rule)
        except (ValueError, IndexError, AssertionError) as e:
            rec('COL.%s_table_parsed_from_proof_md' % rule, False, e)
            continue
        rec('COL.%s_table_parsed_from_proof_md' % rule, True)
        rec('COL.%s_rows_0_to_%d' % (rule, R['trips']), [r[0] for r in rows] == list(range(R['trips'] + 1)),
            [r[0] for r in rows][:5])
        words = [parse_word(GWORD_RUNS + ' ' + r[2]) for r in rows]
        words_all[rule] = (rows, words)
        rec('COL.%s_row0_is_K_start' % rule,
            sx.eqruns(sx.norm(word_tokens(words[0], forms)), sx.norm(sx.Ktoks(*[forms[v] for v in VARS]))))
        rec('COL.%s_last_row_is_K_end' % rule,
            sx.eqruns(sx.norm(word_tokens(words[-1], forms)), sx.norm(sx.Ktoks(*end_forms(rule, forms)))))
        tot = {'': 0}
        for j in range(1, len(rows)):
            claimed = parse_lin(rows[j][1])
            tot = add(tot, claimed)
            ex = sx.Exec([], 'F', word_tokens(words[j - 1], forms), rules=('R1', 'R2b'))
            lv = sx.explore(ex, 2, lambda sub, j=j: word_tokens(
                words[j], {v: subst_expr(forms[v], sub) for v in VARS}))
            rec('COL.%s_every_trip_by_executor_one_branch' % rule, len(lv) == 1 and lv[0].ok and not lv[0].sub,
                (j, [(l.sub, l.ok, fmt_got(l)) for l in lv]))
            for l in lv:
                o = leaf_orig(l.sub, forms)
                rec('COL.%s_every_trip_step_formula' % rule, sx.eqexpr(subst_expr(claimed, o), l.ex.steps),
                    (j, show(subst_expr(claimed, o)), show(l.ex.steps)))
                rec('COL.%s_no_D0' % rule, 'D0' not in l.ex.trans, j)
            # structure claims of proof.md 3.4
            rec('COL.%s_every_trip_has_7n' % rule, claimed.get('n') == 7, (j, rows[j][1]))
            rec('COL.%s_variable_coefficients_multiple_of_7' % rule,
                all(c % 7 == 0 for k, c in claimed.items() if k), (j, rows[j][1]))
        rec('COL.%s_step_column_sums_to_rule_formula' % rule, sx.eqexpr(tot, parse_lin(R['steps'])), show(tot))
        for j, w in enumerate(words):
            vt = var_tokens(w)
            # every exponent >= 1 on the whole domain (constant term of the form in the fresh variables)
            fs = [subst_expr(e, forms) for _, e in w]
            rec('COL.%s_every_exponent_>=1_on_domain' % rule,
                all(sx.const(f) >= 1 and all(c >= 0 for c in f.values()) for f in fs), j)
            # right of the d block the word is constant: the last variable block is the d block, and d only
            last = vt[-1][1]
            rec('COL.%s_last_variable_block_is_d' % rule, set(k for k, c in last.items() if k and c) == {'d'},
                (j, rows[j][2]))
            # the first block is n + const
            rec('COL.%s_first_block_is_n_block' % rule,
                vt[0][0] == len(parse_word(GWORD_RUNS)) and set(k for k, c in vt[0][1].items() if k and c) == {'n'},
                j)
            if j >= 12 and j % 12 == 0:
                base, shrink = S_PATTERN[rule]
                k = j // 12 - 1
                want1 = add(parse_lin('n'), {'': base + 48 * k})
                want2 = add(parse_lin(shrink), {'': -8 * k})
                rec('COL.%s_rows_12j_repeat_S_pattern' % rule,
                    sx.eqexpr(vt[0][1], want1) and sx.eqexpr(vt[1][1], want2), (j, rows[j][2]))
        if rule == 'TO':
            first = [j for j, w in enumerate(words) if any({'b', 'c'} <= set(k for k, c in e.items() if c)
                                                          for _, e in var_tokens(w))]
            rec('COL.TO_b_and_c_blocks_merge_at_trip_10', first[:1] == [10] and first == list(range(10, len(words))),
                first[:3])
    # direct simulation of every row at sampled values (exhaustive box + random)
    for rule, (rows, words) in words_all.items():
        dom = RULES[rule]['dom']
        vals = dom_sample_box(dom, scale(2, 3, 4)) + [dom_sample_rand(dom, 500, RNG) for _ in range(scale(4, 12, 60))]
        jobs, exp = [], []
        for j in range(1, len(rows)):
            sf = parse_lin(rows[j][1])
            for v in vals:
                jobs.append(('F', 0, 2, 10 ** 9, word_value(words[j - 1], v)))
                exp.append((j, v, word_value(words[j], v), sx.ev(sf, v)))
        for (j, v, w, s), r in zip(exp, krun(jobs)):
            rec('COL.%s_every_trip_direct' % rule, check_result(r, w, s), (j, v, r[:4]))


# ================================================================== DIR, TEETH
def direct_rule(rule, val):
    return ('F', 0, 2 * RULES[rule]['trips'], 10 ** 10, Kval(val))


def check_result(res, exp_word, exp_steps):
    k, s, q, h, w = res
    return k == 'REC' and q == 'F' and h == 0 and rstrip0(w) == rstrip0(exp_word) and s == exp_steps


def check_DIR():
    box = {'S': scale(3, 5, 7), 'TE': scale(6, 12, 20), 'TO': scale(4, 6, 10), 'T6': scale(4, 6, 10),
           'T8': scale(6, 12, 20)}
    for rule, R in RULES.items():
        vals = dom_sample_box(R['dom'], box[rule])
        nr = scale(20, 60, 300)
        vals += [dom_sample_rand(R['dom'], 1000, RNG) for _ in range(nr)]
        jobs = [direct_rule(rule, v) for v in vals]
        res = krun(jobs)
        for v, r in zip(vals, res):
            rec('DIR.%s_exact' % rule, check_result(r, Kval(apply_rule(rule, v)), rule_steps(rule, v)), (v, r[:4]))
    # phase rules, from K_j words
    words = [parse_word(GWORD_RUNS + ' ' + w) for w in PHASES]
    dom = RULES['S']['dom']
    vals = dom_sample_box(dom, scale(2, 3, 4)) + [dom_sample_rand(dom, 800, RNG) for _ in range(scale(20, 60, 200))]
    for j in range(12):
        jobs = [('F', 0, 2, 10 ** 9, word_value(words[j], v)) for v in vals]
        res = krun(jobs)
        for v, r in zip(vals, res):
            rec('DIR.P%d_exact' % (j + 1), check_result(r, word_value(words[j + 1], v),
                                                       sx.ev(parse_lin(PHASE_STEPS[j]), v)), (v, r[:4]))


def check_TEETH():
    # one value below each lower bound of S (same parity): the claimed result fails.  (The bounds of TE, TO, T6,
    # T8 are sufficient, not minimal: proof.md 3.4 claims nothing about them.)
    for rule in ('S',):
        R = RULES[rule]
        for v in VARS:
            x = R['dom'][v]
            if isinstance(x, int) or v == 'n':
                continue
            fails = 0
            vals = []
            for _ in range(scale(3, 6, 12)):
                val = dom_sample_rand(R['dom'], 60, RNG)
                val[v] = x[1] - 2
                vals.append(val)
            res = krun([direct_rule(rule, val) for val in vals])
            for val, r in zip(vals, res):
                fails += not check_result(r, Kval(apply_rule(rule, val)), rule_steps(rule, val))
            rec('TEETH.%s_%s>=%d_sharp' % (rule, v, x[1]), fails == len(vals), (fails, len(vals)))


# ================================================================== DC
def even(n, x):
    return {'n': n, 'a': x, 'b': (x + 76) // 2, 'c': 35, 'd': 18}


def double_cycle(n, x, steps_out=None):
    """apply the rules S^((x-4)/8), TE, S^((x-52)/8), TO with domain checks; return (Even params, steps, ok)"""
    val = even(n, x)
    total = 0
    ok = True
    seq = ['S'] * ((x - 4) // 8) + ['TE'] + ['S'] * ((x - 52) // 8) + ['TO']
    for r in seq:
        ok &= in_dom(RULES[r]['dom'], val)
        total += rule_steps(r, val)
        val = apply_rule(r, val)
    return val, total, ok, len(seq)


def check_DC():
    for x in range(52, scale(1004, 4004, 20004), 8):
        n = 2 * RNG.randrange(0, 10 ** 6) + 1
        val, tot, ok, _ = double_cycle(n, x)
        rec('DC.every_application_in_domain', ok, x)
        rec('DC.result_is_Even(n+12x+808,x+32)', val == even(n + 12 * x + 808, x + 32), (x, val))
        rec('DC.progress', tot >= 1)
    # direct simulation of whole double cycles
    xs = list(range(52, scale(100, 252, 404) + 1, 8))
    jobs, exp = [], []
    for x in xs:
        n = 2 * RNG.randrange(0, 60) + 1
        val, tot, ok, nr = double_cycle(n, x)
        trips = 12 * ((x - 4) // 8) + 138 + 12 * ((x - 52) // 8) + 147
        rec('DC.trips_3x+201', trips == 3 * x + 201, x)
        jobs.append(('F', 0, 2 * trips, 10 ** 11, Kval(even(n, x))))
        exp.append((Kval(val), tot))
    for x, r, (w, s) in zip(xs, krun(jobs), exp):
        rec('DC.direct_double_cycle', check_result(r, w, s), (x, r[:4]))


# ================================================================== OPEN
OPEN_START = (4097897, {'n': 1959, 'a': 34, 'b': 68, 'c': 45, 'd': 18})
# (rule, count) applied in order from OPEN_START
OPEN_CHAIN = [('S', 4), ('TO', 1), ('S', 4), ('T6', 1), ('S', 6), ('T8', 1), ('S', 5), ('T6', 1), ('S', 12), ('T8', 1),
              ('S', 9), ('TO', 1), ('S', 17), ('T8', 1), ('S', 13), ('T6', 1), ('S', 22), ('TE', 1), ('S', 16), ('T6', 1)]


def open_checkpoints():
    step, val = OPEN_START
    pts = [('start', step, dict(val), True)]
    for r, k in OPEN_CHAIN:
        ok = True
        for _ in range(k):
            ok &= in_dom(RULES[r]['dom'], val)
            step += rule_steps(r, val)
            val = apply_rule(r, val)
        pts.append(('%s^%d' % (r, k) if k > 1 else r, step, dict(val), ok))
    return pts


def check_OPEN():
    blank = ('A', 0, 0, OPEN_START[0], '0')
    r = krun([blank])[0]
    rec('OPEN.blank_to_K(1959,34,68,45,18)_at_4097897',
        r[0] == 'MAX' and r[2] == 'F' and rstrip0(r[4][r[3]:]) == rstrip0(Kval(OPEN_START[1])) and
        '1' not in r[4][:r[3]], r[:4])
    # no K-shaped left record before 4,097,897 (tools/sim event iterator)
    try:
        sys.path.insert(0, os.path.join(ROOT, 'tools'))
        import sim
        pat = re.compile('^0' + G + r'(1+)0(1+)0110(1+)000000(1+)01101111000000(1+)01100110111(0*)$')
        m = sim.parse(TM)
        found = []
        for ev in sim.events(m, max_steps=OPEN_START[0] + 1, on_record=True, snapshot=True):
            if ev.side == 'L' and ev.config.head == 0 and pat.match(ev.config.tape_str()):
                found.append(ev.step)
        rec('OPEN.first_K_shaped_left_record_is_4097897', found == [OPEN_START[0]], found)
    except ImportError as e:
        rec('OPEN.first_K_shaped_left_record_is_4097897', False, e)
    pts = open_checkpoints()
    rec('OPEN.every_application_in_domain', all(p[3] for p in pts), [p[0] for p in pts if not p[3]])
    rec('OPEN.end_is_Even(12863,212)_at_153126993', pts[-1][1] == 153126993 and pts[-1][2] == even(12863, 212),
        pts[-1])
    rec('OPEN.212=4mod8_>=52', 212 % 8 == 4 and 212 >= 52)
    # direct: chain the runs checkpoint to checkpoint
    cfg = ('F', 0, Kval(OPEN_START[1]))
    for i, (name, step, val, _) in enumerate(pts[1:]):
        prev_step = pts[i][1]
        r = krun([(cfg[0], cfg[1], 0, step - prev_step, cfg[2])])[0]
        ok = r[0] == 'MAX' and r[2] == 'F' and '1' not in r[4][:r[3]] and rstrip0(r[4][r[3]:]) == rstrip0(Kval(val))
        rec('OPEN.direct_checkpoint', ok, (name, step, val, r[:4]))
        cfg = ('F', 0, Kval(val))
    RES.setdefault('_info', {})['OPEN'] = [(p[0], p[1], [p[2][v] for v in VARS]) for p in pts]


# ================================================================== ORB
def check_ORB():
    rows = [l.split('\t') for l in open(os.path.join(HERE, 'work', 'run_starts_K.tsv')).read().split('\n')[1:] if l]
    data = {int(r[1]): tuple(int(x) for x in r[4].strip('()').split(',')) for r in rows}
    step, val = 153126993, even(12863, 212)
    n_ok = 0
    while step <= max(data):
        x = val['a']
        rec('ORB.even_start_in_table', data.get(step) == tuple(val[v] for v in VARS), (step, val))
        # odd start: after S^((x-4)/8), TE
        v2, s2 = dict(val), step
        for r in ['S'] * ((x - 4) // 8) + ['TE']:
            s2 += rule_steps(r, v2)
            v2 = apply_rule(r, v2)
        if s2 <= max(data):
            rec('ORB.odd_start_in_table', data.get(s2) == tuple(v2[v] for v in VARS), (s2, v2))
        nv, tot, ok, _ = double_cycle(val['n'], x)
        step += tot
        val = nv
        n_ok += 1
    rec('ORB.count_even_starts_16', n_ok == 16, n_ok)


# ================================================================== HALT
def check_HALT():
    ex = sx.Exec([('0',)], 'A', [('1', L(1))])     # 0 A> 1 : A1, then D reads the 0
    try:
        ex.step()
        ex.step()
        rec('HALT.engine_raises_on_D0_control', False)
    except sx.Halt as h:
        rec('HALT.engine_raises_on_D0_control', str(h) == 'D0', h)
    for rule, lv in LEAVES.items():
        for l in lv:
            rec('HALT.no_leaf_reads_D0', 'D0' not in l.ex.trans, rule)
    # direct: no rule run ends in HALT on sampled values (DIR covers this); reference check on the opening
    r = krun([('A', 0, 0, 153126993, '0')])[0]
    rec('HALT.no_halt_in_first_153126993_steps', r[0] == 'MAX', r[:4])


# ================================================================== PLAN
def Kr(n, a, b, c, d):
    """proof.md 8: Kr n a b c d = K(2n+1, 2a, 2b, 2c+1, 2d), as a parameter dict"""
    return {'n': 2 * n + 1, 'a': 2 * a, 'b': 2 * b, 'c': 2 * c + 1, 'd': 2 * d}


def Ev(N, X):
    return Kr(N, 4 * X + 26, 2 * X + 32, 17, 9)


PLAN_LEMMAS = {
    # name: (rule, start args, end args) as functions of the lemma's arguments
    'S_step': ('S', lambda n, a, b, c, d: Kr(n, 5 + a, 3 + b, 3 + c, 1 + d),
               lambda n, a, b, c, d: Kr(24 + n, 1 + a, 5 + b, 3 + c, 3 + d), 5),
    'TE': ('TE', lambda n, b, d: Kr(n, 2, 44 + b, 17, 10 + d), lambda n, b, d: Kr(278 + n, 1 + b, 41, 35 + d, 9), 3),
    'TO': ('TO', lambda n, b, c, d: Kr(n, 1, 41 + b, 18 + c, 9 + d),
           lambda n, b, c, d: Kr(294 + n, 14 + b + c, 40 + d, 17, 9), 4),
    'T6': ('T6', lambda n, b, c, d: Kr(n, 3, 41 + b, 17 + c, 9 + d),
           lambda n, b, c, d: Kr(296 + n, 13 + b + c, 40 + d, 17, 9), 4),
    'T8': ('T8', lambda n, b, d: Kr(n, 4, 44 + b, 17, 10 + d), lambda n, b, d: Kr(270 + n, 7 + b, 43, 33 + d, 9), 3),
}


def S_iter_start(k, n, a, b, c, d):
    return Kr(n, 4 * k + 1 + a, 3 + b, 3 + c, 1 + d)


def S_iter_end(k, n, a, b, c, d):
    return Kr(24 * k + n, 1 + a, 2 * k + 3 + b, 3 + c, 2 * k + 1 + d)


def check_PLAN():
    for name, (rule, st, en, ar) in PLAN_LEMMAS.items():
        for _ in range(scale(50, 200, 1000)):
            args = [RNG.randrange(0, 300) for _ in range(ar)]
            v0, v1 = st(*args), en(*args)
            rec('PLAN.%s_start_in_domain' % name, in_dom(RULES[rule]['dom'], v0), (args, v0))
            rec('PLAN.%s_end_is_rule_result' % name, apply_rule(rule, v0) == v1, (args, v0, v1))
    for _ in range(scale(50, 200, 1000)):
        k, n, a, b, c, d = [RNG.randrange(0, 60) for _ in range(6)]
        v = S_iter_start(k, n, a, b, c, d)
        ok = True
        for _ in range(k):
            ok &= in_dom(RULES['S']['dom'], v)
            v = apply_rule('S', v)
        rec('PLAN.S_iter', ok and v == S_iter_end(k, n, a, b, c, d), (k, n, a, b, c, d))
    for _ in range(scale(30, 100, 500)):
        N, X = RNG.randrange(0, 10 ** 6), RNG.randrange(0, 2000)
        seq = [S_iter_start(X + 6, N, 1, 2 * X + 29, 14, 8) == Ev(N, X)]
        e1 = S_iter_end(X + 6, N, 1, 2 * X + 29, 14, 8)
        n1 = (e1['n'] - 1) // 2
        seq.append(e1 == PLAN_LEMMAS['TE'][1](n1, 4 * X, 2 * X + 11))
        e2 = PLAN_LEMMAS['TE'][2](n1, 4 * X, 2 * X + 11)
        n2 = (e2['n'] - 1) // 2
        seq.append(e2 == S_iter_start(X, n2, 0, 38, 2 * X + 43, 8))
        e3 = S_iter_end(X, n2, 0, 38, 2 * X + 43, 8)
        n3 = (e3['n'] - 1) // 2
        seq.append(e3 == PLAN_LEMMAS['TO'][1](n3, 2 * X, 2 * X + 28, 2 * X))
        e4 = PLAN_LEMMAS['TO'][2](n3, 2 * X, 2 * X + 28, 2 * X)
        seq.append(e4 == Ev(48 * X + 716 + N, 4 + X))
        seq.append(Ev(N, X) == even(2 * N + 1, 8 * X + 52) and e4 == even(2 * N + 1 + 12 * (8 * X + 52) + 808,
                                                                         8 * X + 84))
        rec('PLAN.DC_chain_arguments', all(seq), (N, X, seq))
    rec('PLAN.opening_ends', Kr(979, 17, 34, 22, 9) == OPEN_START[1] and Ev(6431, 20) == even(12863, 212))


# ================================================================== DOC
def check_DOC():
    p = os.path.join(HERE, 'proof.md')
    if not os.path.exists(p):
        rec('DOC.proof_md_exists', False)
        return
    t = open(p).read()
    for rule, R in RULES.items():
        rec('DOC.rule_%s_to_quoted' % rule, ('K(%s)' % R['to']) in t, R['to'])
        rec('DOC.rule_%s_steps_quoted' % rule, R['steps'] in t, R['steps'])
    for j, w in enumerate(PHASES):
        rec('DOC.phase_K%d_word_quoted' % j, ('`' + w + '`') in t, j)
    for j, s in enumerate(PHASE_STEPS):
        rec('DOC.phase_P%d_steps_quoted' % (j + 1), s in t, s)
    c, p_, st = [0, 1, 0, 0, 0, 0], 3, 'B'
    for i in range(12):
        bit = c[p_]
        w, m, nx = TABLE[(st, bit)]
        row = '| %d | %s%d = %d%s%s | %d |' % (i + 1, st, bit, w, 'R' if m == 1 else 'L', nx, p_ + m)
        c[p_] = w
        p_ += m
        st = nx
        rec('DOC.R2b_trace_row_quoted', (row + ' ' + ''.join(map(str, c)) + ' |') in t, row)
    pts = open_checkpoints()
    for name, step, val, _ in pts:
        s = 'K(%s)' % ','.join(str(val[v]) for v in VARS)
        rec('DOC.opening_row_quoted', ('{:,}'.format(step) in t) and (s in t), (name, step, s))
    # the part before section 9 (sections 0-8 and the appendices) is what a public copy keeps: 0 linter errors
    try:
        sys.path.insert(0, os.path.join(ROOT, 'tools'))
        import writeup_lint
        hits = writeup_lint.lint_text(t[:t.index('\n## 9.')])
        errs = [(h['line'], h['rule']) for h in hits if h['level'] == 'ERROR']
        rec('DOC.sections_0_to_8_and_appendices_lint_0_errors', not errs, errs[:5])
        RES.setdefault('_info', {})['LINT'] = {'errors': errs, 'warnings': [(h['line'], h['rule']) for h in hits
                                                                           if h['level'] == 'WARN']}
    except (ImportError, ValueError) as e:
        rec('DOC.sections_0_to_8_and_appendices_lint_0_errors', False, e)


SECTIONS = [('T', check_T), ('SR', check_SR), ('ENG', check_ENG), ('MR', check_MR), ('PH', check_PH),
            ('COL', check_COL),
            ('DIR', check_DIR), ('TEETH', check_TEETH), ('DC', check_DC), ('OPEN', check_OPEN), ('ORB', check_ORB),
            ('HALT', check_HALT), ('PLAN', check_PLAN), ('DOC', check_DOC)]


def main():
    build_krun()
    for name, fn in SECTIONS:
        if ONLY and name not in ONLY:
            continue
        t = time.time()
        fn()
        print('[%s] %.1fs' % (name, time.time() - t), flush=True)
    info = RES.pop('_info', None)
    npass = sum(1 for c in ORDER if RES[c]['pass'] == RES[c]['n'])
    for c in ORDER:
        r = RES[c]
        st = 'PASS' if r['pass'] == r['n'] else 'FAIL'
        print('%-4s %-58s %d/%d %s' % (st, c, r['pass'], r['n'], ('' if st == 'PASS' else r['fail'])))
    if info:
        for k, v in info.items():
            print('info', k, v)
    print('seed %d, %s mode: %d/%d checks PASS, %.1fs' % (SEED, 'quick' if QUICK else ('full' if FULL else 'default'),
                                                         npass, len(ORDER), time.time() - T0))
    sys.exit(0 if npass == len(ORDER) else 1)


if __name__ == '__main__':
    main()