#!/usr/bin/env python3
"""check_proof.py for W5-8b = 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF (740 line 418); proof.md in this directory.

proof.md is a delta proof from the parent W5-8 = 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF (740 line 214, killed):
  * the relation: this table is the parent's table mirrored, with states renamed by
    sigma = A->B, B->C, C->A, D->D, E->E, F->F; it starts in sigma(C), so its run is the mirror image of the
    parent's table run from 0^inf C> 0^inf (Lemma M);
  * the opening: 4,098,826 direct steps from blank to Phi K(1953,34,68,45,18) (the mirror of the parent's family K),
    then the parent's rules in the same order as the parent's own opening (S^4 TO S^4 T6 ... S^16 T6), with the same
    a, b, c, d and with n smaller by 6, to Phi Even(12857,212) at step 153,013,640;
  * from there the parent's double cycle Even(n,x) --> Even(n+12x+808, x+32) runs forever (via Lemma M).

Sections (proof.md section in brackets):
  T    [header]  the string; line 418 of the 740 list byte for byte and exactly once (parent: line 214); only D0
                 undefined, D entered only by B1; sheet rows (class only, no claim); the only Discord file that
                 lists it is mxdys's UBRRBA to-do list; busycoq index: absent; upstream tree (if present): none of the
                 1,440 variants of the table
  REL  [1]   sigma + mirror maps the parent's table onto this one (12/12 cells), the only map of 720 x 2; same
             canonical form; start = sigma(C); lockstep with the parent's table from C (Python, every step);
             this machine's tape after 153,013,640 steps = the mirror of the parent's table from C (C runner)
  K    [1]   the mirrored word Phi K of proof.md = the reverse of the parent's K word; G^R
  OPEN [2]   blank --(4,098,826)--> Phi K(1953,34,68,45,18), for this machine and (unmirrored) for the parent's
             table from C; no K-shaped record before it (tools/sim.py, both); the 20 rows: every application in its
             rule's domain, the step sums, a,b,c,d = the parent's rows and n = the parent's n - 6; every row by
             direct simulation of this machine; one unbroken run from blank to Phi Even(12857,212) at 153,013,640
  INV  [3]   Even(12857,212) is in the domain of the double cycle
  DC   [4]   whole double cycles of this machine from Phi Even(n,x) (x = 52..252), exact configuration and steps;
             the orbit from step 153,013,640: every predicted even and odd run start by direct simulation of this
             machine (chained, and one unbroken run from blank), to 2e9 steps (5e8 --quick, 1e10 --full)
  REM  [5]   line 636 = the parent's table from E (no mirror); it is at Even(13299,220) at step 163,638,058
  PAR  [4]   the parent's own check_proof.py (same mode) exits 0 with every check PASS (its rules S, TE, TO, T6, T8
             by symbolic execution, the double cycle, the halting cell); skipped with --no-parent
  HALT [4]   no halt of this machine in its first 153,013,640 steps; sigma(D) = D and D0 is the only undefined cell
             of both tables
  DOC  [*]   proof.md quotes the relation table, the opening and its 20 rows as checked; proof.md before
             section 7 passes tools/writeup_lint.py with 0 errors
Usage: python3 -B check_proof.py [--seed S] [--quick|--full] [--only T,REL,...] [--no-parent]
"""
import importlib.util
import itertools
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, '..', '..'))
TM = '1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF'
PARENT = '1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF'
PDIR = os.path.join(ROOT, 'machines', PARENT)
UPSTREAM = '/tmp/claude-1000/-home-dennis/dbf3e2a9-21e7-4eb2-b481-38a0113aca31/scratchpad/pr3/busycoq/verify'

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
NO_PARENT = '--no-parent' in sys.argv
RNG = random.Random(SEED)
RES, ORDER, INFO = {}, [], {}
T0 = time.time()

# the parent's check module: its rules (domains, updates, step formulas), its K word and its executor's table parser
_spec = importlib.util.spec_from_file_location('w58_check', os.path.join(PDIR, 'check_proof.py'))
P = importlib.util.module_from_spec(_spec)
_spec.loader.exec_module(P)
sx = P.sx
VARS = P.VARS
RULES = P.RULES
G = P.G
PTABLE = sx.parse_table(PARENT)
TABLE = sx.parse_table(TM)

SIGMA = {'A': 'B', 'B': 'C', 'C': 'A', 'D': 'D', 'E': 'E', 'F': 'F'}     # parent state -> this machine's state


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 (this machine or the parent's table)
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(tm, side, jobs):
    """jobs: (state, headidx, nrec, maxsteps, tape) -> (kind, steps, state, headoff, word); records on side L/R"""
    if not jobs:
        return []
    inp = ''.join('%s %d %d %d %s\n' % j for j in jobs)
    out = subprocess.run([KRUN, tm, side], 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


# ------------------------------------------------------------------ the mirrored family
def Kp(val):
    """the parent's K word (head = cell 0, state F)"""
    return P.Kval(val)


def Km(val):
    """Phi K: the mirror image; the head is on the LAST cell, state F (= sigma(F))"""
    return P.Kval(val)[::-1]


def is_Km(res, val, kind='MAX'):
    """res of a run of this machine ends at Phi K(val): head on the rightmost written-or-visited cell that matters,
    state F, nothing but 0 right of the head, the word up to the head = Km(val) (leading 0s ignored)"""
    k, s, q, h, w = res
    return (k == kind and q == 'F' and '1' not in w[h + 1:] and w[:h + 1].lstrip('0') == Km(val).lstrip('0'))


def is_Kp(res, val, kind='MAX'):
    k, s, q, h, w = res
    return k == kind and q == 'F' and '1' not in w[:h] and w[h:].rstrip('0') == Kp(val).rstrip('0')


def even(n, x):
    return P.even(n, x)


# ================================================================== T
def check_T():
    rec('T.machine_string', TM == '1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF')
    raw = open(os.path.join(ROOT, 'data', 'holdouts', 'BB6_holdouts_740.txt'), 'rb').read()
    lines = raw.split(b'\n')
    rec('T.holdout_740_line418_byte_exact', lines[417] == TM.encode(), lines[417])
    rec('T.holdout_740_exactly_once', lines.count(TM.encode()) == 1, lines.count(TM.encode()))
    rec('T.holdout_740_no_CR', b'\r' not in raw)
    rec('T.parent_is_740_line214', lines[213] == PARENT.encode(), 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_B1', into_D == [('B', 1)], into_D)
    # sheet: results tab row = class only; level-0 tab status '-'; no other sheet file names it except the class column
    import csv
    sheet = os.path.join(ROOT, 'data', 'sheet')
    rows = [r for r in csv.reader(open(os.path.join(sheet, '2026-10-09_results.csv'))) if r and r[0] == TM]
    rec('T.sheet_results_row_class_only', len(rows) == 1 and rows[0][2] == 'Bouncer + Chaotic Edge' and
        not any(x.strip() for i, x in enumerate(rows[0]) if i not in (0, 2)), rows)
    rows = [r for r in csv.reader(open(os.path.join(sheet, '2026-10-09_level-0.csv'))) if r and r[0] == TM]
    rec('T.sheet_level0_row_no_status', len(rows) == 1 and rows[0][1] == '' and rows[0][2] in ('', '-') and
        not any(x.strip() for x in rows[0][3:]), rows)
    files = sorted(f for f in os.listdir(sheet) if f.endswith('.csv') and TM in open(os.path.join(sheet, f)).read())
    rec('T.sheet_files_naming_it', files == ['2026-10-09_classifications.csv', '2026-10-09_level-0.csv',
                                             '2026-10-09_results.csv'], files)
    disc = os.path.join(ROOT, 'data', 'discord')
    files = sorted(f for f in os.listdir(disc) if TM in open(os.path.join(disc, f)).read())
    rec('T.discord_only_in_UBRRBA_todo', files == ['2026-08-24_mxdys_ubrrba_86.txt'], files)
    r = subprocess.run([sys.executable, '-B', os.path.join(ROOT, 'tools', 'holdouts.py'), 'solved', TM],
                       capture_output=True, text=True)
    rec('T.busycoq_index_absent', r.returncode != 0 and 'absent from verify/' in r.stdout and
        'equivalent (L/R mirror and/or renamed states): none' in r.stdout, r.stdout[-300:])
    if os.path.isdir(UPSTREAM):
        variants = all_variants(PTABLE)
        hits = []
        for dp, _, fs in os.walk(UPSTREAM):
            for f in fs:
                if f.endswith('.v'):
                    t = open(os.path.join(dp, f), errors='ignore').read()
                    hits += [(f, v) for v in variants if v in t]
        rec('T.upstream_tree_has_no_variant_of_the_table', not hits and len(variants) == 1440, hits[:3])
    else:
        INFO['upstream'] = 'upstream tree not present; T.upstream check skipped'


# ================================================================== REL
def emit(T):
    out = []
    for s in 'ABCDEF':
        row = ''
        for b in (0, 1):
            t = T[(s, b)]
            row += '---' if t is None else '%d%s%s' % (t[0], 'R' if t[1] == 1 else 'L', t[2])
        out.append(row)
    return '_'.join(out)


def image(T, perm, mirror):
    """the table T with states renamed by perm (dict) and, if mirror, L and R swapped"""
    U = {}
    for (s, b), t in T.items():
        U[(perm[s], b)] = None if t is None else (t[0], -t[1] if mirror else t[1], perm[t[2]])
    return emit(U)


def canon(T, start):
    """the least string over all renamings that send `start` to A, with and without the mirror"""
    rest = [q for q in 'ABCDEF' if q != start]
    return min(image(T, dict(zip([start] + rest, ('A',) + p)), m)
               for p in itertools.permutations('BCDEF') for m in (False, True))


def all_variants(T):
    out = set()
    for p in itertools.permutations('ABCDEF'):
        perm = dict(zip('ABCDEF', p))
        for m in (False, True):
            out.add(image(T, perm, m))
    return out


def check_REL():
    rec('REL.sigma_mirror_maps_parent_onto_this', image(PTABLE, SIGMA, True) == TM, image(PTABLE, SIGMA, True))
    cells = 0
    for (s, b), t in PTABLE.items():
        u = TABLE[(SIGMA[s], b)]
        cells += (t is None and u is None) or (t is not None and u == (t[0], -t[1], SIGMA[t[2]]))
    rec('REL.cells_12_of_12', cells == 12, cells)
    maps = [(p, m) for p in itertools.permutations('ABCDEF') for m in (False, True)
            if image(PTABLE, dict(zip('ABCDEF', p)), m) == TM]
    rec('REL.unique_map_of_720x2', len(maps) == 1 and maps[0] == (tuple(SIGMA[s] for s in 'ABCDEF'), True), maps)
    rec('REL.start_is_sigma(C)', SIGMA['C'] == 'A')
    rec('REL.canon(this,A)=canon(parent,C)', canon(TABLE, 'A') == canon(PTABLE, 'C'))
    # lockstep: this machine from blank vs the parent's table from 0^inf C> 0^inf, every step (Python)
    N = scale(200000, 2000000, 10000000)
    ta, pa, sa = {}, 0, 'A'
    tp, pp, sp = {}, 0, 'C'
    ok = True
    for i in range(N):
        u = TABLE[(sa, ta.get(pa, 0))]
        t = PTABLE[(sp, tp.get(pp, 0))]
        if u is None or t is None:
            ok = False
            break
        ta[pa] = u[0]
        pa += u[1]
        sa = u[2]
        tp[pp] = t[0]
        pp += t[1]
        sp = t[2]
        if sa != SIGMA[sp] or pa != -pp:
            ok = False
            break
    ok = ok and all(ta.get(-p, 0) == v for p, v in tp.items()) and all(tp.get(-p, 0) == v for p, v in ta.items())
    rec('REL.lockstep_with_parent_table_from_C_python', ok, i)
    INFO['lockstep_steps'] = N
    # C runner: both runs to 153,013,640 steps; this machine's word = the mirror of the parent's
    ra = krun(TM, 'R', [('A', 0, 0, 153013640, '0')])[0]
    rp = krun(PARENT, 'L', [('C', 0, 0, 153013640, '0')])[0]
    rec('REL.mirror_after_153013640_steps_C_runner',
        ra[0] == rp[0] == 'MAX' and ra[2] == SIGMA[rp[2]] and ra[4] == rp[4][::-1] and
        ra[3] == len(ra[4]) - 1 - rp[3], (ra[:4], rp[:4]))


# ================================================================== K
GR_RUNS = '0^2 1^2 0 1^5 0 1^2 0^2 1^5 0 1^2 0 1^6 0 1^2 0 1^4 0 1^2 0^2'
KM_WORD = ('0^inf 1^3 0 1^2 0^2 1^2 0 1^d 0^6 1^4 0 1^2 0 1^c 0^6 1^b 0 1^2 0 1^a 0 1^n ' + GR_RUNS + ' F> 0^inf')


def check_K():
    gr = P.word_value(P.parse_word(GR_RUNS), {})
    rec('K.G_reversed_word', gr == G[::-1] and len(gr) == 43, gr)
    inner = KM_WORD.replace('0^inf ', '').replace(' F> 0^inf', '')
    w = P.parse_word(inner)
    for _ in range(50):
        val = P.dom_sample_rand(RULES['S']['dom'], 50, RNG)
        # Phi K = (word left of the head) + the head cell (a 0, read by F)
        rec('K.mirrored_K_word_is_reverse_of_parent_K', P.word_value(w, val) + '0' == Km(val), val)


# ================================================================== OPEN
OPEN_STEP = 4098826
OPEN_START = (OPEN_STEP, {'n': 1953, 'a': 34, 'b': 68, 'c': 45, 'd': 18})
END = (153013640, (12857, 212))


def open_checkpoints():
    saved = P.OPEN_START
    P.OPEN_START = OPEN_START
    try:
        return P.open_checkpoints()      # same chain P.OPEN_CHAIN as the parent's opening
    finally:
        P.OPEN_START = saved


def check_OPEN():
    r = krun(TM, 'R', [('A', 0, 0, OPEN_STEP, '0')])[0]
    rec('OPEN.blank_to_PhiK(1953,34,68,45,18)_at_4098826', is_Km(r, OPEN_START[1]), r[:4])
    r = krun(PARENT, 'L', [('C', 0, 0, OPEN_STEP, '0')])[0]
    rec('OPEN.parent_table_from_C_to_K(1953,34,68,45,18)_at_4098826', is_Kp(r, OPEN_START[1]), r[:4])
    # no K-shaped record before it (tools/sim.py event iterator): right records of this machine, left records of
    # the parent's table from C
    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*)$')
        found = []
        for ev in sim.events(sim.parse(TM), max_steps=OPEN_STEP + 1, on_record=True, snapshot=True):
            c = ev.config
            t = c.tape_str()
            if ev.side == 'R' and c.head == len(t) - 1 and c.state == 'F' and pat.match(t[::-1]):
                found.append(ev.step)
        rec('OPEN.first_PhiK_shaped_right_record_is_4098826', found == [OPEN_STEP], found)
        found = []
        for ev in sim.events(sim.parse(PARENT), config=sim.Config.blank('C'), max_steps=OPEN_STEP + 1,
                             on_record=True, snapshot=True):
            c = ev.config
            if ev.side == 'L' and c.head == 0 and c.state == 'F' and pat.match(c.tape_str()):
                found.append(ev.step)
        rec('OPEN.parent_table_from_C_first_K_shaped_left_record_is_4098826', found == [OPEN_STEP], found)
    except ImportError as e:
        rec('OPEN.first_PhiK_shaped_right_record_is_4098826', False, e)
    pts = open_checkpoints()
    ppts = P.open_checkpoints()
    rec('OPEN.chain_is_the_parents', len(pts) == len(ppts) == 21 and [p[0] for p in pts] == [p[0] for p in ppts])
    rec('OPEN.every_application_in_domain', all(p[3] for p in pts), [p[0] for p in pts if not p[3]])
    for p, q in zip(pts, ppts):
        rec('OPEN.row_abcd_equal_parent_n_minus_6',
            all(p[2][v] == q[2][v] for v in 'abcd') and p[2]['n'] == q[2]['n'] - 6, (p, q))
    rec('OPEN.end_is_Even(12857,212)_at_153013640', pts[-1][1] == END[0] and pts[-1][2] == even(*END[1]), pts[-1])
    # every row by direct simulation of this machine (mirrored), checkpoint to checkpoint
    cfg = Km(OPEN_START[1])
    for i, (name, step, val, _) in enumerate(pts[1:]):
        r = krun(TM, 'R', [('F', len(cfg) - 1, 0, step - pts[i][1], cfg)])[0]
        rec('OPEN.direct_row_this_machine', is_Km(r, val), (name, step, val, r[:4]))
        cfg = Km(val)
    # one unbroken run from blank
    r = krun(TM, 'R', [('A', 0, 0, END[0], '0')])[0]
    rec('OPEN.blank_to_PhiEven(12857,212)_at_153013640_unbroken', is_Km(r, even(*END[1])), r[:4])
    INFO['OPEN'] = [(p[0], p[1], [p[2][v] for v in VARS]) for p in pts]


# ================================================================== INV
def check_INV():
    n, x = END[1]
    rec('INV.n_odd', n % 2 == 1)
    rec('INV.x=4mod8_>=52', x % 8 == 4 and x >= 52)
    rec('INV.b=(x+76)/2_c=35_d=18', even(n, x) == {'n': 12857, 'a': 212, 'b': 144, 'c': 35, 'd': 18})


# ================================================================== DC
def check_DC():
    # whole double cycles of THIS machine from Phi Even(n, x)
    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, _ = P.double_cycle(n, x)
        rec('DC.every_application_in_domain', ok, x)
        trips = 3 * x + 201
        w = Km(even(n, x))
        jobs.append(('F', len(w) - 1, 2 * trips, 10 ** 11, w))
        exp.append((val, tot))
    for x, r, (val, tot) in zip(xs, krun(TM, 'R', jobs), exp):
        rec('DC.direct_double_cycle_this_machine', is_Km(r, val, 'REC') and r[1] == tot, (x, r[:4]))
    # the orbit from step 153,013,640: predicted even and odd run starts
    limit = scale(5 * 10 ** 8, 2 * 10 ** 9, 10 ** 10)
    step, val = END[0], even(*END[1])
    pts = []
    while True:
        x = val['a']
        v2, s2 = dict(val), step
        for r in ['S'] * ((x - 4) // 8) + ['TE']:
            s2 += P.rule_steps(r, v2)
            v2 = P.apply_rule(r, v2)
        nv, tot, ok, _ = P.double_cycle(val['n'], x)
        rec('DC.orbit_every_application_in_domain', ok, (step, val))
        if s2 > limit:
            break
        pts.append(('odd', s2, v2))
        if step + tot > limit:
            break
        pts.append(('even', step + tot, nv))
        step, val = step + tot, nv
    cfg, prev = Km(even(*END[1])), END[0]
    for kind, s, v in pts:
        r = krun(TM, 'R', [('F', len(cfg) - 1, 0, s - prev, cfg)])[0]
        rec('DC.orbit_%s_start_direct' % kind, is_Km(r, v), (s, v, r[:4]))
        cfg, prev = Km(v), s
    r = krun(TM, 'R', [('A', 0, 0, pts[-1][1], '0')])[0]
    rec('DC.orbit_last_point_unbroken_run_from_blank', is_Km(r, pts[-1][2]), (pts[-1][:2], r[:4]))
    INFO['ORBIT'] = [(k, s, [v[x] for x in VARS]) for k, s, v in pts]
    # observation (proof.md 3): the parent's observed run starts (its run to 1e10) have the same a, b, c, d and n + 6
    tsv = os.path.join(PDIR, 'work', 'run_starts_K.tsv')
    rows = [l.split('\t') for l in open(tsv).read().split('\n')[1:] if l]
    par = {tuple(int(x) for x in r[4].strip('()').split(','))[1:]: int(r[4].strip('()').split(',')[0]) for r in rows}
    mine = [('even', END[0], even(*END[1]))] + pts
    hits = [(tuple(v[x] for x in 'abcd'), v['n']) for _, _, v in mine if tuple(v[x] for x in 'abcd') in par]
    rec('DC.orbit_same_abcd_as_parent_run_and_n_minus_6', len(hits) == len(mine) and
        all(par[k] == n + 6 for k, n in hits), (len(hits), len(mine), [h for h in hits if par[h[0]] != h[1] + 6][:3]))


# ================================================================== REM
SIB636 = '1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA'


def check_REM():
    """section 5 remark: line 636 = the parent's table from E (no mirror), Even(13299,220) at 163,638,058"""
    lines = open(os.path.join(ROOT, 'data', 'holdouts', 'BB6_holdouts_740.txt')).read().split('\n')
    rec('REM.line636_is_parent_table_from_E', lines[635] == SIB636 and canon(sx.parse_table(SIB636), 'A') ==
        canon(PTABLE, 'E') and any(image(PTABLE, dict(zip('ABCDEF', p)), False) == SIB636 and p[4] == 'A'
                                   for p in itertools.permutations('ABCDEF')), lines[635])
    r = krun(PARENT, 'L', [('E', 0, 0, 163638058, '0')])[0]
    rec('REM.parent_table_from_E_at_Even(13299,220)_step_163638058', is_Kp(r, even(13299, 220)), r[:4])


# ================================================================== PAR
def check_PAR():
    if NO_PARENT:
        INFO['PAR'] = 'skipped (--no-parent)'
        return
    mode = ['--quick'] if QUICK else (['--full'] if FULL else [])
    t = time.time()
    r = subprocess.run(['nice', '-n', '10', sys.executable, '-B', os.path.join(PDIR, 'check_proof.py'),
                        '--seed', str(SEED)] + mode, capture_output=True, text=True, cwd=PDIR)
    last = [l for l in r.stdout.split('\n') if l.startswith('seed ')]
    m = re.search(r'(\d+)/(\d+) checks PASS', last[-1]) if last else None
    rec('PAR.parent_check_proof_exit_0_all_PASS', r.returncode == 0 and m and m.group(1) == m.group(2),
        (r.returncode, last[-1:] or r.stderr[-300:]))
    for sec in ('MR.', 'DC.', 'HALT.'):
        lines = [l for l in r.stdout.split('\n') if re.match(r'(PASS|FAIL) +' + re.escape(sec), l)]
        rec('PAR.parent_%s_checks_present_and_PASS' % sec.strip('.'), lines and all(l.startswith('PASS')
                                                                                   for l in lines), lines[:3])
    INFO['PAR'] = '%s (%.0f s)' % (last[-1] if last else '?', time.time() - t)
    os.makedirs(os.path.join(HERE, 'work'), exist_ok=True)
    with open(os.path.join(HERE, 'work', 'parent_check_proof_%s_seed%d.log' % (
            'quick' if QUICK else ('full' if FULL else 'default'), SEED)), 'w') as f:
        f.write(r.stdout)


# ================================================================== HALT
def check_HALT():
    rec('HALT.sigma(D)=D', SIGMA['D'] == 'D')
    pund = [k for k, v in PTABLE.items() if v is None]
    rec('HALT.parent_only_D0_undefined', pund == [('D', 0)], pund)
    rec('HALT.halting_cells_correspond', [(SIGMA[s], b) for s, b in pund] ==
        [k for k, v in TABLE.items() if v is None])
    r = krun(TM, 'R', [('A', 0, 0, END[0], '0')])[0]
    rec('HALT.no_halt_in_first_153013640_steps', r[0] == 'MAX', r[:4])


# ================================================================== 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()
    # relation table rows: | this state | 0 | 1 | = sigma(parent state) | parent 0 | parent 1 |
    inv = {v: k for k, v in SIGMA.items()}
    fmt = lambda tr: '---' if tr is None else '%d%s%s' % (tr[0], 'R' if tr[1] == 1 else 'L', tr[2])
    for s in 'ABCDEF':
        q = inv[s]
        row = '| %s | %s | %s | σ(%s) | %s | %s |' % (s, fmt(TABLE[(s, 0)]), fmt(TABLE[(s, 1)]), q,
                                                     fmt(PTABLE[(q, 0)]), fmt(PTABLE[(q, 1)]))
        rec('DOC.relation_row_quoted', row in t, row)
    rec('DOC.sigma_quoted', 'A -> B,  B -> C,  C -> A,  D -> D,  E -> E,  F -> F' in t)
    rec('DOC.mirrored_K_word_quoted', KM_WORD in t, KM_WORD)
    pts = open_checkpoints()
    ppts = P.open_checkpoints()
    for (name, step, val, _), q in zip(pts, ppts):
        s = 'K(%s)' % ','.join(str(val[v]) for v in VARS)
        row = '| %s | %s | %s |' % ('{:,}'.format(step), s, '{:,}'.format(q[1]))
        rec('DOC.opening_row_quoted', row in t, row)
    rec('DOC.end_quoted', 'Even(12857, 212)' in t and '153,013,640' in t)
    try:
        sys.path.insert(0, os.path.join(ROOT, 'tools'))
        import writeup_lint
        hits = writeup_lint.lint_text(t[:t.index('\n## 7.')])
        errs = [(h['line'], h['rule']) for h in hits if h['level'] == 'ERROR']
        rec('DOC.sections_before_7_lint_0_errors', not errs, errs[:5])
        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_before_7_lint_0_errors', False, e)


SECTIONS = [('T', check_T), ('REL', check_REL), ('K', check_K), ('OPEN', check_OPEN), ('INV', check_INV),
            ('DC', check_DC), ('REM', check_REM), ('PAR', check_PAR), ('HALT', check_HALT), ('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)
    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 %-64s %d/%d %s' % (st, c, r['pass'], r['n'], ('' if st == 'PASS' else r['fail'])))
    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()