#!/usr/bin/env python3
"""check_proof.py for W5-8c = 1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA (740 line 636); 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 with states renamed by
    sigma = A->E, B->C, C->D, D->F, E->A, F->B (no mirror); it starts in sigma(E), so its run is sigma of the
    parent's table run from 0^inf E> 0^inf (Lemma R), on the same tape;
  * the opening: 6,950,830 direct steps from blank to K(2583,70,76,43,18) (head state sigma(F) = B), then 18 macro
    steps by the parent's rules (S^8 T6 S^7 TE S^6 T6 S^13 T8 S^10 TO S^18 T8 S^14 T6 S^23 TE S^17 T6) to
    Even(13299,220) at step 163,638,058;
  * from there the parent's double cycle Even(n,x) --> Even(n+12x+808, x+32) runs forever (via Lemma R).

Sections (proof.md section in brackets):
  T    [header]  the string; line 636 of the 740 list byte for byte and exactly once (parent: line 214); only F0
                 undefined, F entered only by E1; 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 maps the parent's table onto this one (12/12 cells, no mirror), the only map of 720 x 2; same
             canonical form; start = sigma(E); lockstep with the parent's table from E (Python, every step);
             tapes equal after 163,638,058 steps (C runner)
  OPEN [2]   blank --(6,950,830)--> K(2583,70,76,43,18) for this machine (state B) and the parent's table from E
             (state F); the 18 rows: every application in its rule's domain, the step sums; the K-shaped left records
             of both runs up to 163,638,058 (C scanner, any state) = exactly the predicted points (start, every single
             application, end), the C scanner agreeing with a regex scan; no K-shaped record before 6,950,830
             (tools/sim.py events); every row by direct simulation; one unbroken run to Even(13299,220)
  INV  [3]   Even(13299,220) is in the domain of the double cycle; the orbit's first members
  DC   [4]   whole double cycles of this machine from sigma Even(n,x) (x = 52..252), exact configuration and steps;
             the orbit from step 163,638,058: every predicted even and odd run start by direct simulation (chained,
             and one unbroken run from blank), to 2e9 steps (5e8 --quick, 1e10 --full); every K-shaped left record
             of this machine in that range = the next point predicted by S, TE, TO
  PLAN [6]   the half-length start / end and the 18 follow arguments against the parent's lemma statements (read
             from the parent's kill file)
  REM  [5]   the three list entries of the table (lines, starts, mirror flags) and the Even steps of lines 214, 418;
             starts B and F reach the blank start-C configuration after 1 and 2 steps
  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 163,638,058 steps; sigma(D) = F, D0 / F0 the only undefined cells
  DOC  [*]   proof.md quotes the relation table, sigma, the opening rows, the domain rows and bounds, the chain and the
             follow arguments 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 = '1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA'
PARENT = '1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF'
SIB418 = '1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF'
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': 'E', 'B': 'C', 'C': 'D', 'D': 'F', 'E': 'A', 'F': 'B'}     # parent state -> this machine's state
KSTATE = SIGMA['F']                                                       # = 'B'

OPEN_STEP = 6950830
OPEN_START = (OPEN_STEP, {'n': 2583, 'a': 70, 'b': 76, 'c': 43, 'd': 18})
OPEN_CHAIN = [('S', 8), ('T6', 1), ('S', 7), ('TE', 1), ('S', 6), ('T6', 1), ('S', 13), ('T8', 1), ('S', 10), ('TO', 1),
              ('S', 18), ('T8', 1), ('S', 14), ('T6', 1), ('S', 23), ('TE', 1), ('S', 17), ('T6', 1)]
CHAIN_STR = 'S^8 T6 S^7 TE S^6 T6 S^13 T8 S^10 TO S^18 T8 S^14 T6 S^23 TE S^17 T6'
END = (163638058, (13299, 220))


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 tools: batch runner and K scanner
KRUN = os.path.join(HERE, 'work', 'krun')
KSCAN = os.path.join(HERE, 'work', 'kscan')


def build():
    for exe, src in ((KRUN, 'krun.c'), (KSCAN, 'kscan.c')):
        src = os.path.join(HERE, 'scripts', src)
        if not os.path.exists(exe) or os.path.getmtime(exe) < os.path.getmtime(src):
            os.makedirs(os.path.dirname(exe), exist_ok=True)
            subprocess.run(['gcc', '-O2', '-o', exe, 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(['nice', '-n', '10', 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


def kscan(tm, start, fstate, frm, maxs):
    """K-shaped left records: list of (step, state, val); and the END line"""
    out = subprocess.run(['nice', '-n', '10', KSCAN, tm, start, fstate, str(frm), str(maxs)], capture_output=True,
                         text=True, check=True).stdout.split('\n')
    pts, end = [], None
    for line in out:
        p = line.split()
        if len(p) == 7:
            pts.append((int(p[0]), p[1], dict(zip(VARS, map(int, p[2:])))))
        elif p:
            end = p
    return pts, end


# ------------------------------------------------------------------ the family K
def Kw(val):
    """the parent's K word (head = cell 0)"""
    return P.Kval(val)


def is_K(res, val, state, kind='MAX'):
    """res of a run ends at K(val) with the head in `state`: nothing but 0 left of the head, the word from the head on
    = the K word (trailing 0s ignored)"""
    k, s, q, h, w = res
    return k == kind and q == state and '1' not in w[:h] and w[h:].rstrip('0') == Kw(val).rstrip('0')


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


def Kfmt(v):
    return 'K(%s)' % ','.join(str(v[x]) for x in VARS)


def open_points():
    """(row, rule, k, start step, start val, end step, end val, ok, singles) for the 18 rows; singles = the
    (step, val) after every single application"""
    step, val = OPEN_START
    rows = []
    for i, (r, k) in enumerate(OPEN_CHAIN, 1):
        s0, v0, ok, singles = step, dict(val), True, []
        for _ in range(k):
            ok &= P.in_dom(RULES[r]['dom'], val)
            step += P.rule_steps(r, val)
            val = P.apply_rule(r, val)
            singles.append((step, dict(val)))
        rows.append((i, r, k, s0, v0, step, dict(val), ok, singles))
    return rows


# ================================================================== T
def check_T():
    rec('T.machine_string', TM == '1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA')
    raw = open(os.path.join(ROOT, 'data', 'holdouts', 'BB6_holdouts_740.txt'), 'rb').read()
    lines = raw.split(b'\n')
    rec('T.holdout_740_line636_byte_exact', lines[635] == TM.encode(), lines[635])
    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_F0_undefined', und == [('F', 0)], und)
    into_F = [k for k, v in TABLE.items() if v and v[2] == 'F']
    rec('T.F_entered_only_by_E1', into_F == [('E', 1)], into_F)
    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)
    cl = list(csv.reader(open(os.path.join(sheet, '2026-10-09_classifications.csv'))))
    cols = sorted({cl[0][i] for r in cl[1:] for i, x in enumerate(r) if x == TM})
    rec('T.sheet_classifications_only_class_column', cols == ['Bouncer + Chaotic Edge'], cols)
    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 and TM in variants,
            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_maps_parent_onto_this_no_mirror', image(PTABLE, SIGMA, False) == TM, image(PTABLE, SIGMA, False))
    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'), False), maps)
    rec('REL.start_is_sigma(E)', SIGMA['E'] == 'A')
    rec('REL.canon(this,A)=canon(parent,E)', canon(TABLE, 'A') == canon(PTABLE, 'E'))
    # lockstep: this machine from blank vs the parent's table from 0^inf E> 0^inf, every step (Python)
    N = scale(200000, 2000000, 10000000)
    ta, pa, sa = {}, 0, 'A'
    tp, pp, sp = {}, 0, 'E'
    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 ta == tp
    rec('REL.lockstep_with_parent_table_from_E_python', ok, i)
    INFO['lockstep_steps'] = N
    ra = krun(TM, 'L', [('A', 0, 0, END[0], '0')])[0]
    rp = krun(PARENT, 'L', [('E', 0, 0, END[0], '0')])[0]
    rec('REL.equal_tapes_after_163638058_steps_C_runner',
        ra[0] == rp[0] == 'MAX' and ra[2] == SIGMA[rp[2]] and ra[4] == rp[4] and ra[3] == rp[3], (ra[:4], rp[:4]))


# ================================================================== OPEN
def check_OPEN():
    r = krun(TM, 'L', [('A', 0, 0, OPEN_STEP, '0')])[0]
    rec('OPEN.blank_to_K(2583,70,76,43,18)_state_B_at_6950830', is_K(r, OPEN_START[1], KSTATE), r[:4])
    r = krun(PARENT, 'L', [('E', 0, 0, OPEN_STEP, '0')])[0]
    rec('OPEN.parent_table_from_E_to_K(2583,70,76,43,18)_at_6950830', is_K(r, OPEN_START[1], 'F'), r[:4])
    rows = open_points()
    rec('OPEN.18_rows', len(rows) == 18)
    rec('OPEN.every_application_in_domain', all(x[7] for x in rows), [x[0] for x in rows if not x[7]])
    rec('OPEN.rows_chain', all(rows[i][3] == rows[i - 1][5] and rows[i][4] == rows[i - 1][6]
                               for i in range(1, len(rows))) and rows[0][3:5] == OPEN_START)
    rec('OPEN.chain_string', ' '.join(r + ('^%d' % k if k > 1 else '') for r, k in OPEN_CHAIN) == CHAIN_STR)
    rec('OPEN.end_is_Even(13299,220)_at_163638058', rows[-1][5] == END[0] and rows[-1][6] == even(*END[1]), rows[-1])
    # every K-shaped left record of both runs up to END = the predicted points (start, every single application, end)
    pred = [OPEN_START] + [s for x in rows for s in x[8]]
    for tm, st, ks in ((TM, 'A', KSTATE), (PARENT, 'E', 'F')):
        pts, end = kscan(tm, st, '*', 0, END[0])
        rec('OPEN.K_shaped_left_records_to_163638058_are_the_predicted_points_%s' % ('this' if tm == TM else 'parentE'),
            [(s, v) for s, _, v in pts] == pred and all(q == ks for _, q, _ in pts) and end[0] == 'END',
            (len(pts), len(pred), pts[:2], end))
        rec('OPEN.first_K_shaped_left_record_any_state_is_6950830', pts and pts[0][0] == OPEN_STEP, pts[:1])
    INFO['K_records_opening'] = len(pred)
    # independent: the regex of the parent's check (tools/sim.py event iterator) up to the opening start
    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
            if ev.side == 'L' and c.head == 0 and pat.match(c.tape_str()):
                found.append((ev.step, c.state))
        rec('OPEN.sim_py_first_K_shaped_left_record_is_6950830', found == [(OPEN_STEP, KSTATE)], found)
    except ImportError as e:
        rec('OPEN.sim_py_first_K_shaped_left_record_is_6950830', False, e)
    # every row by direct simulation of this machine, checkpoint to checkpoint
    for i, r, k, s0, v0, s1, v1, _, _ in rows:
        res = krun(TM, 'L', [(KSTATE, 0, 0, s1 - s0, Kw(v0))])[0]
        rec('OPEN.direct_row_this_machine', is_K(res, v1, KSTATE), (i, r, s1, v1, res[:4]))
    r = krun(TM, 'L', [('A', 0, 0, END[0], '0')])[0]
    rec('OPEN.blank_to_Even(13299,220)_at_163638058_unbroken', is_K(r, even(*END[1]), KSTATE), r[:4])
    INFO['OPEN'] = [(x[0], x[1], x[2], x[5], Kfmt(x[6])) for x in rows]


# ================================================================== 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': 13299, 'a': 220, 'b': 148, 'c': 35, 'd': 18})
    v1, _, ok1, _ = P.double_cycle(13299, 220)
    v2, _, ok2, _ = P.double_cycle(v1['n'], v1['a'])
    rec('INV.orbit_first_members', ok1 and ok2 and v1 == even(16747, 252) and v2 == even(20579, 284), (v1, v2))


# ================================================================== DC
def check_DC():
    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
        jobs.append((KSTATE, 0, 2 * trips, 10 ** 11, Kw(even(n, x))))
        exp.append((val, tot))
    for x, r, (val, tot) in zip(xs, krun(TM, 'L', jobs), exp):
        rec('DC.direct_double_cycle_this_machine', is_K(r, val, KSTATE, 'REC') and r[1] == tot, (x, r[:4]))
    # the orbit from step 163,638,058: predicted even and odd run starts, and every single application
    limit = scale(5 * 10 ** 8, 2 * 10 ** 9, 10 ** 10)
    step, val = END[0], even(*END[1])
    pts, singles = [], []
    done = False
    while not done:
        x = val['a']
        nv, tot, ok, _ = P.double_cycle(val['n'], x)
        rec('DC.orbit_every_application_in_domain', ok, (step, val))
        v2, s2 = dict(val), step
        for i, r in enumerate(['S'] * ((x - 4) // 8) + ['TE'] + ['S'] * ((x - 52) // 8) + ['TO']):
            s2 += P.rule_steps(r, v2)
            v2 = P.apply_rule(r, v2)
            if s2 > limit:
                done = True
                break
            singles.append((s2, dict(v2)))
            if r == 'TE':
                pts.append(('odd', s2, dict(v2)))
        if not done:
            rec('DC.orbit_cycle_end_is_Even', s2 == step + tot and v2 == nv, (step, val))
            pts.append(('even', s2, dict(v2)))
            step, val = s2, v2
    cfg, prev = Kw(even(*END[1])), END[0]
    for kind, s, v in pts:
        r = krun(TM, 'L', [(KSTATE, 0, 0, s - prev, cfg)])[0]
        rec('DC.orbit_%s_start_direct' % kind, is_K(r, v, KSTATE), (s, v, r[:4]))
        cfg, prev = Kw(v), s
    r = krun(TM, 'L', [('A', 0, 0, pts[-1][1], '0')])[0]
    rec('DC.orbit_last_point_unbroken_run_from_blank', is_K(r, pts[-1][2], KSTATE), (pts[-1][:2], r[:4]))
    # every K-shaped left record of this machine in (END, limit] is the next predicted single application
    found, end = kscan(TM, 'A', '*', END[0] + 1, limit)
    rec('DC.K_shaped_left_records_to_limit_are_the_predicted_points',
        [(s, v) for s, _, v in found] == singles and all(q == KSTATE for _, q, _ in found) and end[0] == 'END',
        (len(found), len(singles), end))
    INFO['ORBIT'] = '%d even/odd run starts, %d K records to %d steps' % (len(pts), len(singles), limit)


# ================================================================== PLAN
def Kr(N, a, b, c, d):
    """proof.md 6: Kr N a b c d = K(2N+1, 2a, 2b, 2c+1, 2d)"""
    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)


# the parent .v's lemma statements, as (name, arity, lhs, rhs) on the arguments
LEMMAS = {
    'S_iter': (6, lambda k, n, a, b, c, d: Kr(n, 4 * k + 1 + a, 3 + b, 3 + c, 1 + d),
               lambda k, n, a, b, c, d: Kr(24 * k + n, 1 + a, 2 * k + 3 + b, 3 + c, 2 * k + 1 + d)),
    "TE'": (3, 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)),
    "TO'": (4, 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)),
    "T6'": (4, 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)),
    "T8'": (3, 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)),
}
# the same statements as Rocq text in the parent's kill file
LEMMA_TEXT = {
    'S_iter': 'Lemma S_iter k: forall n a b c d,\n  Kr n (4*k+1+a) (3+b) (3+c) (1+d) -->* '
              'Kr (24*k+n) (1+a) (2*k+3+b) (3+c) (2*k+1+d).',
    "TE'": "Lemma TE' n b d:\n  Kr n 2 (44+b) 17 (10+d) -->* Kr (278+n) (1+b) 41 (35+d) 9.",
    "TO'": "Lemma TO' n b c d:\n  Kr n 1 (41+b) (18+c) (9+d) -->* Kr (294+n) (14+b+c) (40+d) 17 9.",
    "T6'": "Lemma T6' n b c d:\n  Kr n 3 (41+b) (17+c) (9+d) -->* Kr (296+n) (13+b+c) (40+d) 17 9.",
    "T8'": "Lemma T8' n b d:\n  Kr n 4 (44+b) 17 (10+d) -->* Kr (270+n) (7+b) 43 (33+d) 9.",
}
FOLLOWS = ['(S_iter 8 1291 2 35 18 8)', "(T6' 1483 13 4 16)", '(S_iter 7 1779 1 53 14 8)', "(TE' 1947 26 13)",
           '(S_iter 6 2225 2 38 45 8)', "(T6' 2369 12 31 12)", '(S_iter 13 2665 3 49 14 8)', "(T8' 2977 34 25)",
           '(S_iter 10 3247 0 40 55 8)', "(TO' 3487 22 40 20)", '(S_iter 18 3781 3 57 14 8)', "(T8' 4213 52 35)",
           '(S_iter 14 4483 2 40 65 8)', "(T6' 4819 30 51 28)", '(S_iter 23 5115 1 65 14 8)', "(TE' 5667 70 45)",
           '(S_iter 17 5945 2 38 77 8)', "(T6' 6353 34 63 34)"]
RULE_OF = {'S_iter': 'S', "TE'": 'TE', "TO'": 'TO', "T6'": 'T6', "T8'": 'T8'}


def check_PLAN():
    vfile = os.path.join(PDIR, PARENT + '.v')
    vt = open(vfile).read()
    for name, txt in LEMMA_TEXT.items():
        rec('PLAN.lemma_statement_in_parent_v', txt in vt, name)
    rec('PLAN.Kr_Ev_definitions_in_parent_v', 'Definition Ev N X := Kr N (4*X+26) (2*X+32) 17 9.' in vt and
        'Lemma DC N X:\n  Ev N X -->+ Ev (48*X+716+N) (4+X).' in vt)
    rec('PLAN.start_Kr_1291_35_38_21_9', Kr(1291, 35, 38, 21, 9) == OPEN_START[1])
    rec('PLAN.end_Ev_6649_21', Ev(6649, 21) == even(*END[1]))
    rows = open_points()
    rec('PLAN.18_follows', len(FOLLOWS) == len(rows) == 18)
    for f, (i, r, k, s0, v0, s1, v1, _, _) in zip(FOLLOWS, rows):
        p = f.strip('()').split()
        name, xs = p[0], [int(t) for t in p[1:]]
        ar, lhs, rhs = LEMMAS[name]
        ok = len(xs) == ar and all(t >= 0 for t in xs) and RULE_OF[name] == r and lhs(*xs) == v0 and rhs(*xs) == v1
        if name == 'S_iter':
            ok = ok and xs[0] == k
        rec('PLAN.follow_args_match_row', ok, (i, f, v0, v1))
    # the Rocq DC step agrees with the double cycle
    for N, X in ((6649, 21), (RNG.randrange(10 ** 6), RNG.randrange(10 ** 3))):
        v, _, ok, _ = P.double_cycle(2 * N + 1, 8 * X + 52)
        rec('PLAN.DC_Ev_step', ok and v == Ev(48 * X + 716 + N, 4 + X), (N, X))


# ================================================================== REM
def check_REM():
    lines = open(os.path.join(ROOT, 'data', 'holdouts', 'BB6_holdouts_740.txt')).read().split('\n')
    for ln, tm, start, mirror in ((214, PARENT, 'A', False), (418, SIB418, 'C', True), (636, TM, 'E', False)):
        t = sx.parse_table(tm)
        maps = [(p, m) for p in itertools.permutations('ABCDEF') for m in (False, True)
                if image(PTABLE, dict(zip('ABCDEF', p)), m) == tm]
        rec('REM.line_start_mirror', lines[ln - 1] == tm and canon(t, 'A') == canon(PTABLE, start) and
            len(maps) == 1 and maps[0][1] == mirror and maps[0][0]['ABCDEF'.index(start)] == 'A', (ln, maps))
    r = krun(PARENT, 'L', [('A', 0, 0, 153126993, '0')])[0]
    rec('REM.line214_Even(12863,212)_at_153126993', is_K(r, even(12863, 212), 'F'), r[:4])
    r = krun(PARENT, 'L', [('C', 0, 0, 153013640, '0')])[0]
    rec('REM.parent_table_from_C_Even(12857,212)_at_153013640', is_K(r, even(12857, 212), 'F'), r[:4])
    # starts B and F: the tape stays blank and the run enters C after 1 / 2 steps
    for q, k in (('B', 1), ('F', 2)):
        tape, pos, st = {}, 0, q
        for _ in range(k):
            w, d, st2 = PTABLE[(st, tape.get(pos, 0))]
            tape[pos] = w
            pos += d
            st = st2
        rec('REM.start_%s_blank_C_after_%d' % (q, k), st == 'C' and not any(tape.values()), (st, tape))
    # the first two lines of the table have killed proofs (status.json)
    import json
    for tm in (PARENT, SIB418):
        s = json.load(open(os.path.join(ROOT, 'machines', tm, 'status.json')))
        rec('REM.sibling_status_killed', s.get('status') == 'KILLED_NONHALT', (tm, s.get('status')))


# ================================================================== 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)=F', SIGMA['D'] == 'F')
    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])
    rec('HALT.E1_is_sigma_of_parent_A1', TABLE[('E', 1)] == (1, -1, 'F') and PTABLE[('A', 1)] == (1, -1, 'D'))
    r = krun(TM, 'L', [('A', 0, 0, END[0], '0')])[0]
    rec('HALT.no_halt_in_first_163638058_steps', r[0] == 'MAX', r[:4])


# ================================================================== DOC
def dom_rows():
    out = []
    for i, r, k, s0, v0, s1, v1, _, _ in open_points():
        a = '%d, …, %d' % (v0['a'], v0['a'] - 8 * (k - 1)) if r == 'S' else str(v0['a'])
        out.append('| %d | %s | %s | %s | %d | %d | %d |' % (i, r + ('^%d' % k if k > 1 else ''), Kfmt(v0), a,
                                                            v0['b'], v0['c'], v0['d']))
    return out


def bound_lines():
    rows = open_points()
    S = [x for x in rows if x[1] == 'S']
    amin = min(x[4]['a'] - 8 * (x[2] - 1) for x in S)
    arow = [x[0] for x in S if x[4]['a'] - 8 * (x[2] - 1) == amin]
    # the bounds also hold for every single application (b, d grow, c fixed, a falls)
    ok = all(P.in_dom(RULES[x[1]]['dom'], x[4]) for x in rows)
    by = lambda r: [x[4] for x in rows if x[1] == r]
    TE, TO, T6, T8 = by('TE'), by('TO'), by('T6'), by('T8')
    lines = [
        '- In the S rows the smallest a is %d (row %s), the smallest b is %d, every c is at least %d and every d is '
        '%s.' % (amin, ','.join(map(str, arow)), min(x[4]['b'] for x in S), min(x[4]['c'] for x in S),
                 '/'.join(str(d) for d in sorted({x[4]['d'] for x in S}))),
        '- The TE rows have c = %s, b ≥ %d and d ≥ %d.' % ('/'.join(sorted({str(v['c']) for v in TE})),
                                                          min(v['b'] for v in TE), min(v['d'] for v in TE)),
        '- The TO row has b = %d, c = %d and d = %d.' % (TO[0]['b'], TO[0]['c'], TO[0]['d']) if len(TO) == 1 else '?',
        '- The T6 rows have b ≥ %d, c ≥ %d and d ≥ %d.' % (min(v['b'] for v in T6), min(v['c'] for v in T6),
                                                          min(v['d'] for v in T6)),
        '- The T8 rows have c = %s, b ≥ %d and d ≥ %d.' % ('/'.join(sorted({str(v['c']) for v in T8})),
                                                          min(v['b'] for v in T8), min(v['d'] for v in T8)),
    ]
    return lines, ok


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()
    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 -> E,  B -> C,  C -> D,  D -> F,  E -> A,  F -> B' in t)
    rec('DOC.opening_start_quoted', '| opening | (direct run) | 6,950,830 | K(2583,70,76,43,18) |' in t and
        'K(2583, 70, 76, 43, 18)' in t)
    for i, r, k, s0, v0, s1, v1, _, _ in open_points():
        row = '| %d | %s | %s | %s |' % (i, r + ('^%d' % k if k > 1 else ''), '{:,}'.format(s1), Kfmt(v1))
        rec('DOC.opening_row_quoted', row in t, row)
    for row in dom_rows():
        rec('DOC.domain_row_quoted', row in t, row)
    lines, ok = bound_lines()
    rec('DOC.domain_rows_in_domain', ok)
    for l in lines:
        rec('DOC.bound_line_quoted', l in t, l)
    for name, dom in RULES.items():
        d = dom['dom']
        cell = lambda v: str(d[v]) if isinstance(d[v], int) else '%s, ≥ %d' % ('odd' if d[v][0] else 'even', d[v][1])
        row = '| %s | %s | %s | %s | %s |' % (name, cell('a'), cell('b'), cell('c'), cell('d'))
        rec('DOC.domain_definition_row_quoted', row in t and d['n'] == (1, 1), row)
    rec('DOC.chain_quoted', CHAIN_STR in t)
    v = {'n': 1, 'a': 0, 'b': 0, 'c': 0, 'd': 0}
    rec('DOC.n_increments_quoted', sorted(P.apply_rule(r, v)['n'] - 1 for r in RULES) == [48, 540, 556, 588, 592]
        and '(48, 556, 588, 592 or 540)' in t)
    rec('DOC.records_count_quoted', 'these 126 configurations' in t and
        1 + sum(k for _, k in OPEN_CHAIN) == 126)
    for f in FOLLOWS:
        rec('DOC.follow_quoted', 'follow %s.' % f in t, f)
    rec('DOC.start_end_half_quoted', 'Kr 1291 35 38 21 9' in t and 'Ev 6649 21' in t and '(6649, 21)' in t)
    rec('DOC.end_quoted', 'Even(13299, 220)' in t and '163,638,058' in t and
        'Even(13299, 220) --> Even(16747, 252) --> Even(20579, 284)' 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), ('OPEN', check_OPEN), ('INV', check_INV), ('DC', check_DC),
            ('PLAN', check_PLAN), ('REM', check_REM), ('PAR', check_PAR), ('HALT', check_HALT), ('DOC', check_DOC)]


def main():
    build()
    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 %-72s %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()