#!/usr/bin/env python3
"""check_proof.py: validate every claim of proof.md for 1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB.

usage:  python3 -B check_proof.py [quick|full] [--only S1,S2,...]

Sections (numbers match proof.md):
  S1  base macros (sweeps)                       exhaustive n <= 40 + random large n, random contexts
  S2  unit rules by ORACLE simulation            finite computation = the proof of each unit lemma (Lemma U1-U3)
  S3  Theorem U (arrival = inc)                  exhaustive unit words (<= 4 units, 14 unit kinds) + random words,
                                                 exact step-count recursion
  S4  initial segment                            blank tape -> first cycle record at step 203,465 (exact); the transition
                                                 table printed in proof.md equals the holdout string, A1 the only halt
  S5  Lemma N (nursery cycle)                    PROOF: 8 window computations (scripts/proof2/lemma_nt.py) close the cycle,
                                                 R touched only by the W rule (Lemma C1 checked); CROSS-CHECK at every
                                                 left record to MAXSTEP: next record = G' F (pop o inc^3)^k (U), cells,
                                                 state and exact step count; L_gap, conveyor prefix >= 42 units
  S6  Lemma T (top relation)                     unit-level run driven by the S5 cycle from U_0: N_j = 3A_j + D_j + p,
                                                 the flux identity for p, equality with the machine at every S5 record,
                                                 Z_1 and the closed system's N_j, stored machine replay on the overlap;
                                                 at every absorption c_j = r_j (mod 3) (fixed points are triple boundaries)
  S7  closed system canonical states (Lemma C0)  C(b) at j = 32b+17 for every b < B
  S8  block map, random huge b (Theorem B)       every class k <= KMAX, random b < 2^BITS
  S9  symbolic engines                           entry (o = 1, q >= 1), descent (13 + 8 steps), plant
  S10 value form (vtot.py); Lemma L representative runs (scripts/proof3/locality.py): small classes, endgame
      residues mod 2^R (quick R = 8, full R = 16; both modes also R = 12, the smaller split of proof.md section 10),
      nested range v <= 60 / 600
  S10s quick mode only: the stored full-size Lemma L results, checked by content (full mode reruns them)
  S11 lemma VF and the plant as checked lemmas (scripts/proof4/vf.py): every representative of the one-step
      descent lemma under Lemma L' (cut R = 8: 24 entry + 256 region-A + 1,024 region-B steps, hypotheses, next
      form, transfer algebra); the hand entry lemma (C(b) -> off 20) and the hand plant lemma (off' 12 -> 17) on
      random instances; whole chains from C(b) (level 1) and from the plant start (level 2); random members
  S12 Lemmas Z0 and Z1 (scripts/proof5/z1.py): every shift of the closed-system orbit from Z_1 classified by kind
      (wall / absorption) and target (only D1, P or the blank allowed), Z0's hypothesis at every absorption, the normal
      form (no trailing D0) of every zone; Lemma Z1
      (the absorption shift never lands on S1) on every zone of <= 5 (quick) / 6 (full) units and feeds 1..32 / 1..40, and on
      random zones with any number of walls, plus a c = 0 negative control
Exit status 0 iff every section passes.  quick: about 45 s; full: about 10 min.
"""
import json, os, random, re, subprocess, sys, time, tempfile, shutil, atexit

HERE = os.path.dirname(os.path.abspath(__file__))
SCR = os.path.join(HERE, 'scripts')
TOOLS = '[local working file]'
TM = '1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB'
MODE = 'full' if 'full' in sys.argv[1:] else 'quick'
ONLY = None
if '--only' in sys.argv:
    ONLY = set(sys.argv[sys.argv.index('--only') + 1].split(','))
RES = {}
ST = 'ABCDEF'
TMPD = tempfile.mkdtemp(prefix='cp14_')          # per-run scratch files (no clash with other check runs)
atexit.register(shutil.rmtree, TMPD, True)

# ---------------------------------------------------------------- machine
TAB = {}
for qi, row in enumerate(TM.split('_')):
    for s in (0, 1):
        t = row[3 * s:3 * s + 3]
        TAB[(qi, s)] = None if t == '---' else (int(t[0]), 1 if t[1] == 'R' else -1, ST.index(t[2]))
B, C = ST.index('B'), ST.index('C')


def run_word(word, head, state, steps=None, stop_left=None, maxs=10 ** 8):
    """Run on a finite word (0^inf on both sides, grown as needed). Returns (status, steps, tape(str), head, state).
    stop_left: stop when the head moves to index < stop_left (returns 'LEFT')."""
    off = 64
    tape = bytearray(64) + bytearray(int(c) for c in word) + bytearray(64)
    h = head + off; q = state; n = 0
    lim = steps if steps is not None else maxs
    while n < lim:
        if h < 4:
            tape = bytearray(len(tape)) + tape; h += len(tape) // 2; off += len(tape) // 2
        if h >= len(tape) - 4:
            tape.extend(bytearray(len(tape)))
        tr = TAB[(q, tape[h])]
        if tr is None:
            return ('HALT', n, None, h - off, q)
        w, d, q = tr; tape[h] = w; h += d; n += 1
        if stop_left is not None and h - off < stop_left:
            return ('LEFT', n, tape[off:].decode('latin1') if False else ''.join(map(str, tape[off:])), h - off, q)
    return ('STEPS', n, ''.join(map(str, tape[off:])), h - off, q)


def arrive(R, maxs=10 ** 8):
    """Arrival on a right word R (cells; 0^inf after): B on R[0]; run until the head leaves to the left.
    Returns ('OK', steps, R') with R' the cell word (trailing zeros stripped) and the exit state checked = C."""
    st, n, tape, h, q = run_word(R, 0, B, stop_left=0, maxs=maxs)
    if st != 'LEFT':
        return (st, n, None)
    if q != C:
        return ('BADEXIT' + ST[q], n, None)
    return ('OK', n, tape.rstrip('0'))


def ok(name, cond, info=None):
    RES.setdefault(name, {'pass': 0, 'fail': 0, 'first_fail': None})
    if cond:
        RES[name]['pass'] += 1
    else:
        RES[name]['fail'] += 1
        if RES[name]['first_fail'] is None:
            RES[name]['first_fail'] = info
    return cond


def expand(s, **v):
    """'(11000)^n 1 0^3' style -> cell string."""
    out = []
    for tok in s.split():
        m = re.fullmatch(r'\(([01]+)\)\^(\w+)|([01]+)\^(\w+)|([01]+)', tok)
        if m.group(5):
            out.append(m.group(5)); continue
        w = m.group(1) or m.group(3); e = m.group(2) or m.group(4)
        out.append(w * (int(e) if e.isdigit() else v[e]))
    return ''.join(out)


def rctx(rng, n):
    return ''.join(rng.choice('01') for _ in range(n))


# ---------------------------------------------------------------- S1 sweeps
def S1():
    rng = random.Random(1)
    # (lhs with head marker, rhs with head marker, steps(n))  head marker: 'B>' before the read cell, '<C' after it
    sweeps = {
        'SR  B> (11000)^n -> (10111)^n B>': ('B>', '(11000)^n', '(10111)^n', 'B>', lambda n: 5 * n),
        'SR6 B> (111000)^n -> (100111)^n B>': ('B>', '(111000)^n', '(100111)^n', 'B>', lambda n: 6 * n),
        'KB  B> (1000)^n -> (1111)^n B>': ('B>', '(1000)^n', '(1111)^n', 'B>', lambda n: 4 * n),
        "SL' (10111)^n <C -> <C (11000)^n": ('<C', '(10111)^n', '(11000)^n', '<C', lambda n: 5 * n),
        'SL  (11110)^n <C -> <C (00011)^n': ('<C', '(11110)^n', '(00011)^n', '<C', lambda n: 5 * n),
        'KC  1^n <C -> <C 0^n': ('<C', '1^n', '0^n', '<C', lambda n: n),
    }
    ns = list(range(0, 41)) + [rng.randint(100, 5000) for _ in range(10 if MODE == 'quick' else 40)]
    for name, (hd, lhs, rhs, hd2, f) in sweeps.items():
        for n in ns:
            for _ in range(3):
                L = '1' + rctx(rng, rng.randint(0, 8)); R = rctx(rng, rng.randint(0, 8)) + '1'
                a = expand(lhs, n=n); b = expand(rhs, n=n)
                if hd == 'B>':
                    st, k, tape, h, q = run_word(L + a + R, len(L), B, steps=f(n))
                    good = st == 'STEPS' and q == B and h == len(L) + len(b) and tape.startswith(L + b + R)
                else:
                    st, k, tape, h, q = run_word(L + a + R, len(L) + len(a) - 1, C, steps=f(n))
                    good = st == 'STEPS' and q == C and h == len(L) - 1 and tape.startswith(L + b + R)
                ok('S1 ' + name, good, (n, L, R))
    # EdgeL / EdgeR and the rotor rules of the observation stage (already in validate_rules.py; re-run small)
    for n in range(0, 25):
        R = rctx(rng, 6) + '1'
        st, k, tape, h, q = run_word('0' * 8 + R, 7, C, steps=4)
        ok('S1 EdgeL 0^inf <C -> 0^inf 1 0 B> 1  (4 steps)', st == 'STEPS' and q == B and h == 7 and tape.startswith('000001' + '01' + R[0:0]) and tape[5:8] == '101' and tape[8:].startswith(R), n)


# ---------------------------------------------------------------- S2 unit lemmas by oracle simulation
# A unit is h+'1000' (h a head word without '000') or the 0 digit '0000'.  The arrival lemma for a unit is proved by
# running the machine on the unit's own cells, with the rest r of the word replaced by an ORACLE: whenever the head
# steps onto r's first cell in state B, the induction hypothesis Arr(r) puts it back on the unit's last cell in state C
# (and r becomes inc(r)).  Any other contact with r, a halt, or a left exit in a state other than C fails the lemma.
HEADS_DEFINED = ['', '1', '11', '111', '101', '1111', '1101']   # depth <= 3 heads with a nonzero first cell
HEADS_ZERO = ['0', '01', '011', '001', '0111', '0101']            # first cell 0
HEADS_DEPTH4 = ['11111', '11101', '01111', '01101']


def oracle_unit(h):
    word = h + '1000' if h is not None else '0000'
    n = len(word)
    tape = [int(c) for c in word]
    pos = 0; q = B; steps = 0; segs = [0]; f = 0
    while True:
        if pos == n:
            if q != B:
                return {'status': 'TOUCHES_REST_IN_' + ST[q], 'steps': steps}
            f += 1; segs.append(0); pos = n - 1; q = C
            continue
        if pos < 0:
            if q != C:
                return {'status': 'EXIT_LEFT_IN_' + ST[q], 'steps': steps, 'f': f}
            res = ''.join(map(str, tape))
            return {'status': 'OK', 'f': f, 'segments': segs, 'kappa': sum(segs), 'result_cells': res}
        tr = TAB[(q, tape[pos])]
        if tr is None:
            return {'status': 'HALT', 'steps': steps}
        w, d, q = tr; tape[pos] = w; pos += d; steps += 1; segs[-1] += 1
        if steps > 10000:
            return {'status': 'LOOP'}


def unit_rule_from_cells(h, res):
    """Read the oracle result h' 1000 0^e (same length as h 1000).  Returns (h', e) or None."""
    k = res.rfind('1000')
    if k < 0:
        return None
    hp, e = res[:k], len(res) - k - 4
    if res[k + 4:] != '0' * e or '000' in hp:
        return None
    return hp, e


UNIT_TABLE = {}   # h -> (h', f, e, kappa)   (for '' : the digit-1 rule; h None: digit 0)


def S2():
    expect = {'': ('', 1, 0), '1': ('1', 1, 0), '11': ('1', 3, 1), '111': ('01', 2, 1), '101': ('01', 1, 1),
              '1111': ('111', 2, 1), '1101': ('111', 1, 1)}
    # digit 1 ('' head): the oracle result is 0000 (= the 0 digit), carry on: record as ('0digit', 1, 0)
    for h in HEADS_DEFINED:
        r = oracle_unit(h)
        if r['status'] != 'OK':
            ok('S2 unit lemma ' + repr(h), False, r); continue
        if h == '':
            good = r['result_cells'] == '0000' and r['f'] == 1
            UNIT_TABLE[''] = (None, 1, 0, r['kappa'])
        else:
            hp_e = unit_rule_from_cells(h, r['result_cells'])
            good = hp_e is not None and (hp_e[0], r['f'], hp_e[1]) == expect[h]
            if good:
                UNIT_TABLE[h] = (hp_e[0], r['f'], hp_e[1], r['kappa'])
        RES.setdefault('S2 oracle table', {})[repr(h)] = {'f': r['f'], 'segments': r['segments'], 'kappa': r['kappa'],
                                                          'result': r['result_cells']}
        ok('S2 unit lemma (oracle proof) h=' + repr(h), good, r)
    # first cell 0 (0 digit and every 0-led head): B0 = 1LC, one step, stop
    for h in [None] + HEADS_ZERO:
        r = oracle_unit(h)
        cells = '0000' if h is None else h + '1000'
        good = r['status'] == 'OK' and r['f'] == 0 and r['kappa'] == 1 and r['result_cells'] == '1' + cells[1:]
        ok('S2 first-cell-0 lemma h=' + repr(h), good, r)
    UNIT_TABLE['ZERO'] = (None, 0, 0, 1)
    # depth-4 heads: no oracle proof (documented failure mode)
    for h in HEADS_DEPTH4:
        r = oracle_unit(h)
        RES.setdefault('S2 depth-4 heads (no local rule, informational)', {})[h] = r['status'] if r['status'] != 'OK' else 'OK->' + r['result_cells']
    # top of the word: B> 0^inf -> <C 1 (1 step) is B0, same as the first-cell-0 lemma


# ---------------------------------------------------------------- S3 Theorem U
class Undefined(Exception):
    pass


def inc(w, depth=0):
    """Model arrival on a cell word w (unit word, 0^inf after).  Returns (w', steps)."""
    if w.strip('0') == '':
        return '1', 1
    if w[0] == '0':
        return '1' + w[1:], 1
    if w.startswith('1000'):
        r, s = inc(w[4:], depth + 1)
        return '0000' + r, UNIT_TABLE[''][3] + s
    k = w.find('1000')
    if k < 0:
        return inc(w + '000', depth)
    h = w[:k]
    if h not in UNIT_TABLE or '000' in h:
        raise Undefined(h)
    hp, f, e, kappa = UNIT_TABLE[h]
    r = w[k + 4:]; tot = kappa
    for _ in range(f):
        r, s = inc(r, depth + 1); tot += s
    return hp + '1000' + '0' * e + r, tot


UNITS = {'D0': '0000', 'D1': '1000', 'P': '11000', 'S1': '01000', 'SP': '011000', 'W': '111000',
         'sSP': '0011000', 'sW': '0111000', 'Q': '1111000', '101': '1011000', '0111': '01111000',
         '0101': '01011000', '1111': '11111000', '1101': '11011000'}


def S3():
    import itertools
    names = list(UNITS)
    L = 3 if MODE == 'quick' else 4
    words = []
    for n in range(1, L + 1):
        for t in itertools.product(names, repeat=n):
            if t[-1] == 'D0':
                continue
            words.append(''.join(UNITS[x] for x in t))
    rng = random.Random(3)
    lg = ['D0', 'D1', 'P', 'S1', 'SP', 'W']
    for _ in range(2000 if MODE == 'quick' else 20000):
        t = []
        for _ in range(rng.randint(1, 12)):
            x = rng.choice(lg + ['P'] * 3)
            t += [x] * (rng.randint(1, 40) if x == 'P' and rng.random() < 0.3 else 1)
        if rng.random() < 0.3:
            t.insert(rng.randrange(len(t)), rng.choice(names))
        words.append(''.join(UNITS[x] for x in t))
    undefined = 0
    for w in words:
        try:
            m, s = inc(w)
        except Undefined:
            undefined += 1
            continue
        except RecursionError:
            ok('S3 Theorem U: machine arrival == inc (cells and exact steps)', False, ('RecursionError', w[:60]))
            continue
        st, n, out = arrive(w)
        ok('S3 Theorem U: machine arrival == inc (cells and exact steps)', st == 'OK' and out == m.rstrip('0') and n == s,
           (w, st, n, s, out, m))
        # Lemma U-term: on L_gap words, inc never increases the number of walls (SP, W) unless a hit occurs
        tin, tout = htok(w), htok(m)
        if tin is not None and all(x == '0' or x in NAMES for x in tin):
            if tout is not None and all(x == '0' or x in NAMES for x in tout):
                ok('S3 Lemma U-term: on L_gap words without a hit, walls(inc(w)) <= walls(w)',
                   sum(x in ('h01', 'h11') for x in tout) <= sum(x in ('h01', 'h11') for x in tin), (comp(tin), comp(tout)))
    RES['S3 words where the model is undefined (skipped; depth-4 or no-unit heads)'] = undefined


# ---------------------------------------------------------------- S4 initial segment
def htok(s):
    """Tokenize a right-part cell string into units: '0' (0 digit) or 'h'+head; None if not a unit word."""
    s = s.rstrip('0')
    if not s:
        return []
    s = s + '000'; out = []; i = 0; n = len(s)
    while i < n:
        j = i
        while j < n and s[j] == '0':
            j += 1
        if j >= n:
            break
        z = j - i
        out.extend(['0'] * (z // 4)); sh = z % 4
        k = s.find('1000', j)
        if k < 0:
            return None
        h = '0' * sh + s[j:k]
        if '000' in h:
            return None
        out.append('h' + h); i = k + 4
    return out


NAMES = {'h': 'D1', 'h0': 'S1', 'h1': 'P', 'h01': 'SP', 'h11': 'W'}


def comp(u):
    out = []
    for x in u:
        n = NAMES.get(x, x)
        if out and out[-1][0] == n:
            out[-1][1] += 1
        else:
            out.append([n, 1])
    return ' '.join(n if c == 1 else '%s^%d' % (n, c) for n, c in out)


def split_record(t):
    """Left-record tape (t[0] = the cell under the head at lo) -> (gadget cells, unit tokens).
    The gadget is the first three 1-runs after t[0]; the unit word starts 3 cells after the third run
    (that gap is the unit lattice's 3-cell gap)."""
    s = t[1:].rstrip('0')
    it = list(re.finditer(r'1+', s))
    cut = it[3].start(); gap = cut - it[2].end()
    return s[:cut - (gap - 3)], htok(s[cut - (gap - 3):])


S4_RECORD = {}


def S4():
    sys.path.insert(0, TOOLS)
    import sim
    M = sim.parse(TM)
    r = sim.run(M, max_steps=203465)
    cfg = r.final
    t = ''.join(map(str, cfg.tape))
    g, u = split_record(t)
    want = 'P SP P W P^3 SP P^4 W P^7 W P^11 W P^10 0^2 D1^4'
    G_X = '111111' + '0000' + '11' + '0000' + '11' + '000'
    good = (not r.halted) and cfg.state == 'C' and cfg.pos == cfg.lo and u is not None and comp(u) == want and g == G_X \
        and t[0] == '0' and t[1 + len(g):].rstrip('0') == ''.join('0000' if x == '0' else x[1:] + '1000' for x in u).rstrip('0')
    S4_RECORD['t'] = t
    RES['S4 record at 203,465'] = {'state': cfg.state, 'pos': cfg.pos, 'lo': cfg.lo, 'gadget': g, 'units': comp(u) if u else None}
    ok('S4 initial segment: blank -> 0^inf <C G_X U_0 at step 203,465 (gadget cells and unit word both compared)', good,
       (g, comp(u) if u else t[:80]))
    # the transition table printed in proof.md ("## Machine") is the holdout string, and A1 is the only undefined entry
    md = open(os.path.join(HERE, 'proof.md')).read()
    blk = md.split('## Machine', 1)[1].split('```')[1].strip().splitlines()
    rows = [ln.split() for ln in blk[1:7]]
    good = [r[0] for r in rows] == list('ABCDEF') and '_'.join(r[1] + r[2] for r in rows) == TM \
        and [k for k, v in TAB.items() if v is None] == [(0, 1)]
    ok('S4 proof.md transition table == holdout string; the only halting transition is A1', good, rows)


# ---------------------------------------------------------------- S5 left records
def lgap_ok(u):
    """L_gap at the unit level: heads only '', 0, 1, 01, 11 (D1, S1, P, SP, W); returns (ok, reason)."""
    for x in u:
        if x != '0' and x not in NAMES:
            return False, 'head ' + x
    return True, ''


def walls_and_wires(u):
    """Conveyor/zone walls: indices of SP/W units; wire of a wall = 1 + P units directly after it."""
    out = []
    for i, x in enumerate(u):
        if x in ('h01', 'h11'):
            k = i + 1
            while k < len(u) and u[k] == 'h1':
                k += 1
            nxt = u[k] if k < len(u) else None
            out.append((i, k - i, nxt))
    return out


def _record_tape_203465():
    if 'X' not in S4_RECORD:
        sys.path.insert(0, TOOLS)
        import sim
        r = sim.run(sim.parse(TM), max_steps=203465)
        S4_RECORD['X'] = ''.join(map(str, r.final.tape))
    return S4_RECORD['X']


CYCLE = {}     # (state, gadget) -> window-run data (filled by S5, used by S6)
RECS = []      # machine left records (filled by S5)


def S5():
    """Lemma N.  (a) the proof: the window computation (scripts/proof2/lemma_nt.py) from the step-203,465 record
    closes after 8 records, using only the arrival rule, the W rule and Lemma C1.  (b) a cross-check against the
    machine at every left record to MAXSTEP: next record = G' F (pop o inc^3)^k (U), cells, state and exact step count."""
    sys.path.insert(0, os.path.join(SCR, 'proof2'))
    sys.path.insert(0, TOOLS)
    import sim
    import lemma_nt as L
    c1 = L.lemma_c1()
    ok('S5 Lemma C1: inc^3 of a word led by P, S1, SP or W starts with P', all(v == 'P' for v in c1.values()), c1)
    t0 = _record_tape_203465()
    out, st = L.chain(t0, 'C', split_record, htok, 8)
    good = st['status'] == 'OK' and st['final'] == ('C', L.gadget_of(t0)) and len(out) == 8 \
        and all(set(o['ops']) <= {'W'} for o in out)
    ok('S5 Lemma N (proof): the 8 window computations close the cycle XC..ZE -> XC, R touched only by the W rule', good, (st, [o['ops'] for o in out]))
    RES['S5 Lemma N cycle'] = [{'from': o['from'][0] + ':' + o['from'][1], 'to': o['to'][0] + ':' + o['to'][1], 'W_rules': len(o['ops']),
                                'F': ' '.join(o['F']), 'window_steps': o['steps']} for o in out]
    for o in out:
        CYCLE[o['from']] = o
    # (b) machine cross-check
    M = sim.parse(TM)
    mx = 3e8 if MODE == 'quick' else 2e9
    recs = []
    for ev in sim.events(M, max_steps=int(mx), on_record=True, snapshot=True):
        if ev.side != 'L' or ev.step < 203465:
            continue
        recs.append((ev.step, ev.state, ev.config.lo, ''.join(map(str, ev.config.tape))))
    RECS[:] = recs
    order = ['C', 'D', 'E', 'C', 'D', 'E', 'D', 'E']
    xs = []
    for i, (step, q, lo, t) in enumerate(recs):
        ok('S5 left records follow the 8-cycle XC XD XE YC YD YE ZD ZE', q == order[i % 8], (step, q, i))
        g = L.gadget_of(t)
        u = htok(t[1 + len(g):])
        good, why = lgap_ok(u) if u is not None else (False, 'untok')
        ok('S5 every left record: unit word in L_gap', good, (step, why))
        if u is None:
            continue
        conv = 0
        while conv < len(u) and u[conv] in ('h1', 'h01', 'h11'):
            conv += 1
        ok('S5 conveyor prefix ({P,SP,W} units before the first other unit) has >= 42 units', conv >= 42, (step, conv))
        o = CYCLE.get((q, g))
        ok('S5 every left record has one of the 8 gadget words of the cycle', o is not None, (step, q, g))
        if i % 8 == 0:
            xs.append((step, lo, t))
        if o is None or i + 1 >= len(recs):
            continue
        wd = L.Word(L.tokens_from_htok(u))
        try:
            wd.apply_ops(o['ops'])
        except L.Hit as ex:
            ok('S5 Lemma N cross-check: next record = G\' F (pop o inc^3)^k (U), state and exact steps', False, (step, repr(ex)))
            continue
        pred = o['to'][1] + L.cells_of(o['F']) + L.cells_of(wd.u)
        s2, q2, lo2, t2 = recs[i + 1]
        ok('S5 Lemma N cross-check: next record = G\' F (pop o inc^3)^k (U), state and exact steps',
           q2 == o['to'][0] and t2[1:].rstrip('0') == pred.rstrip('0') and s2 - step == o['steps'] + wd.steps,
           (step, q2, s2 - step, o['steps'] + wd.steps))
    for (s0, lo0, t0_), (s1, lo1, t1) in zip(xs, xs[1:]):
        ok('S5 X records: left edge moves exactly -8 per cycle', lo1 == lo0 - 8, (s0, s1, lo0, lo1))
    RES['S5 range'] = {'max_step': mx, 'left_records': len(recs), 'X_records': len(xs)}


# ---------------------------------------------------------------- S6-S10: closed system and symbolic engines
def sub(cmd, cwd, env=None, timeout=3600):
    e = dict(os.environ); e.update(env or {})
    t0 = time.time()
    p = subprocess.run(['nice', '-n', '10'] + cmd, cwd=cwd, env=e, capture_output=True, text=True, timeout=timeout)
    return p.returncode, p.stdout, p.stderr, round(time.time() - t0, 1)


def last_json(out):
    for line in reversed(out.strip().splitlines()):
        line = line.strip()
        if line.startswith('{'):
            try:
                return json.loads(line)
            except ValueError:
                pass
    return None


def S6():
    """Lemma T.  Unit-level run of the right part driven by the Lemma-N cycle (proved in S5), from U_0 (S4):
    (a) N_j obeys N_j = 3A_j + D_j + p(j mod 8) for every j >= 1;
    (b) the flux identity p(j) = z0 - 3 b_j + 2 b_{j-1} + s_{j-1} + H_{j-1} holds for every j whose two walls were born
        in the run (b = birth index, s = born as W, H = carries wall j-1 received before wall j was born);
    (c) the unit-level run equals the machine at every left record of S5 (cells);
    (d) the closed system (deepen6/topsys.py semantics) started from the run's own zone after absorption 0 gives the
        same N_j; (e) the stored machine replay N_j (deepen5/results/N_final.json) agrees on the overlap."""
    sys.path.insert(0, os.path.join(SCR, 'proof2'))
    import lemma_nt as L
    if not CYCLE:
        S5()
    t0 = _record_tape_203465()
    g0 = L.gadget_of(t0)

    class Word3(L.Word):
        # records, at each absorption, the carries received so far by the absorbed wall and by the next wall
        # (for the triple-boundary check (f) below); the run itself is unchanged
        def _leave(self, a, w, zone_wall):
            n0 = len(self.absorptions)
            super()._leave(a, w, zone_wall)
            if len(self.absorptions) > n0:
                rec = self.absorptions[-1]; nxt = self.alive[0] if self.alive else None
                rec['recv_abs'] = self.walls[w]['recv']; rec['next'] = nxt
                rec['recv_next'] = None if nxt is None else self.walls[nxt]['recv']

    wd = Word3(L.tokens_from_htok(htok(t0[1 + len(g0):])))
    wd.register_existing_walls()
    ncyc = 60 if MODE == 'quick' else 150
    key = ('C', g0); seq = []
    for _ in range(8):
        o = CYCLE[key]; seq.append(o); key = o['to']
    recmap = {i: r for i, r in enumerate(RECS)}
    # the invariant Inv(n, J) of proof.md section 7 (scripts/proof3/invariant.py): U_n is reconstructed from n and J
    # alone (birth tables, clause-c carry chain, clause-d zone feed, closed-system state CS_J from the stated Z_1)
    sys.path.insert(0, os.path.join(SCR, 'proof3')); sys.path.insert(0, os.path.join(SCR, 'deepen4'))
    sys.path.insert(0, os.path.join(SCR, 'deepen6'))
    import invariant as INV
    import topsys
    sy0 = topsys.Sys(['0', None, '', '', '', None, ''], 0, 1); CS = {}; NSTOP = {0: 33}
    for _ in range(9 * ncyc + 60):
        CS[sy0.j] = (list(sy0.Z), sy0.D); jj = sy0.j; NSTOP[jj] = sy0.onestep()[0]
    inv = {'records': 0, 'bad': 0, 'perturbed': 0, 'perturbed_rejected': 0, 'births_checked': 0}

    def strip(u):
        u = list(u)
        while u and u[-1] == 'D0':
            u.pop()
        return u

    def inv_check(n):
        J = len(wd.absorptions)
        U, info = INV.reconstruct(n, J, CS, NSTOP)
        good = U is not None and strip(wd.u) == U and wd.base == info['base'] and wd.alive and wd.alive[0] == J \
            and wd.Ncur == info['m'] and set(wd.alive) == set(info['walls']) \
            and all(wd.walls[w]['recv'] == info['walls'][w]['R'] for w in info['walls'])
        inv['records'] += 1
        ok('S6 Inv(n, J): U_n equals the reconstruction from (n, J) (clauses a-d; walls, R chain, m, zone = inc^m(CS_J))',
           good, (n, J, info if U is None else info['m']))
        if U is None or n % 3:
            return
        top = info['walls'][J]['pos'] - info['base']
        perts = []
        if top + 1 < len(wd.u) and wd.u[top + 1] == 'P':
            p = list(wd.u); del p[top + 1]; perts.append(p)                       # one P less in the top wire
            p = list(wd.u); p[top], p[top + 1] = p[top + 1], p[top]; perts.append(p)   # top wall moved up one unit
        p = list(wd.u); p.insert(top + 1, 'P'); perts.append(p)                  # one P more in the top wire
        for p in perts:
            p = strip(p); inv['perturbed'] += 1
            if all(INV.reconstruct(n, Jp, CS, NSTOP)[0] != p for Jp in range(max(0, J - 4), J + 5)):
                inv['perturbed_rejected'] += 1

    def birth_check(n):
        # newborn walls sit below every older live wall (FIFO placement, proof.md section 4)
        ws = sorted(wd.alive)
        posn = {w: next(i for i, x in enumerate(wd.wid) if x == w) + wd.base for w in ws}
        inv['births_checked'] += 1
        ok('S6 births: every live wall sits strictly below every older live wall', all(posn[a] > posn[b] for a, b in zip(ws, ws[1:])),
           (n, posn))

    k = 0; mism = 0; compared = 0
    inv_check(0)
    try:
        for c in range(ncyc):
            for o in seq:
                wd.apply_ops(o['ops']); wd.exc += 1; wd.prepend(o['F'])
                k += 1
                inv_check(k)
                if o['F']:
                    birth_check(k)
                if k in recmap:
                    compared += 1
                    t = recmap[k][3]; pred = o['to'][1] + L.cells_of(wd.u)
                    if t[1:].rstrip('0') != pred.rstrip('0'):
                        mism += 1
    except L.Hit as ex:
        ok('S6 unit-level run has no hit', False, repr(ex)); return
    ok('S6 perturbations of the top wire (one P less, one P more, wall moved up) violate Inv(n, J\') for every J\' in J-4..J+4',
       inv['perturbed'] > 0 and inv['perturbed_rejected'] == inv['perturbed'], inv)
    RES['S6 invariant'] = inv
    ok('S6 unit-level run == machine at every left record of S5 (cells)', mism == 0 and compared > 0, (mism, compared))
    ab = wd.absorptions
    p8 = (47, 48, 48, 47, 48, 47, 48, 47)
    z = [a['z'] for a in ab]; N = [a['N'] for a in ab]
    for j in range(1, len(ab)):
        A = z[j] - z[j - 1]; D = z[j - 1] - z[0]
        ok('S6 Lemma T: N_j = 3A_j + D_j + p(j mod 8)', N[j] == 3 * A + D + p8[j % 8], (j, N[j], A, D))
    ok('S6 FIFO: the wall absorbed at absorption j is the j-th wall in birth order (U_0 walls first), through every level-up',
       all(a['wall'] == j for j, a in enumerate(ab)), [a['wall'] for a in ab[:12]])
    nid = 0
    for j in range(1, len(ab)):
        wj = wd.walls[ab[j]['wall']]; wi = wd.walls[ab[j - 1]['wall']]
        if wj['b'] is None or wi['b'] is None:
            continue
        H = wi.get('H', 0) if wi['exc'] != wj['exc'] else 0
        nid += 1
        ok('S6 flux identity p(j) = z0 - 3b_j + 2b_{j-1} + s_{j-1} + H_{j-1}', z[0] - 3 * wj['b'] + 2 * wi['b'] + wi['s'] + H == p8[j % 8],
           (j, wj, wi, H))
    # (f) proof.md sections 5 and 7 (absorption): every fixed point m = c + 3A(m) of interval j is a triple boundary of
    # wall j, because c_j = r_j (mod 3), where r_j in {0, 1, 2} is the number of carries of wall j's triple still to
    # come at absorption j-1 (the triple boundaries of interval j are m = r_j + 3i).  r_j is read off the run:
    # r_j = N_j - 3 * (firings of wall j after absorption j-1); firings = floor((received + s)/2).
    n3 = 0; bad3 = []; rcount = {0: 0, 1: 0, 2: 0}
    for j in range(1, len(ab)):
        w = ab[j]['wall']
        if ab[j - 1].get('next') != w or ab[j - 1].get('recv_next') is None:
            bad3.append((j, 'next wall', ab[j - 1].get('next'), w)); continue
        sw = wd.walls[w]['s']
        f_then = (ab[j - 1]['recv_next'] + sw) // 2; f_end = (ab[j]['recv_abs'] + sw) // 2
        r = N[j] - 3 * (f_end - f_then); c = (z[j - 1] - z[0]) + p8[j % 8]
        n3 += 1
        if r in rcount:
            rcount[r] += 1
        if not (0 <= r <= 2 and (c - r) % 3 == 0 and f_end == z[j] - wd.walls[w]['b'] and N[j] >= c):
            bad3.append((j, r, c, f_then, f_end, z[j], wd.walls[w]['b']))
    ok('S6 absorption at the least fixed point: r_j in {0,1,2}, c_j = r_j (mod 3), wall j fires z_j - b_j times in all '
       '(so every fixed point of interval j is a triple boundary)', n3 == len(ab) - 1 and not bad3, (n3, bad3[:3]))
    # (d) closed system from the run's own zone after absorption 0
    sys.path.insert(0, os.path.join(SCR, 'deepen4')); sys.path.insert(0, os.path.join(SCR, 'deepen6'))
    import topsys
    conv = {'D0': None, 'D1': '', 'S1': '0', 'SP': '01', 'W': '11'}
    Z = []
    for x in ab[0]['zone']:
        if x == 'P':
            if Z and type(Z[-1]) is int: Z[-1] += 1
            else: Z.append(1)
        else:
            Z.append(conv[x])
    Z1 = ['0', None, '', '', '', None, '']
    ok('S6 zone after absorption 0 is Z_1 = S1 D0 D1 D1 D1 D0 D1 (and N_0 = 33)', Z == Z1 and N[0] == 33, (Z, N[0]))
    sy = topsys.Sys(Z, 0, 1); badc = 0
    for j in range(1, len(ab)):
        n, A, land = sy.onestep()
        if n != N[j]:
            badc += 1
    ok('S6 closed system from Z_1 reproduces the unit-level N_j', badc == 0, badc)
    ok('S6 closed system: no zone wall alive at an absorption, no hit (same range)', sy.alive_at_abs == 0 and len(sy.hitlog) == 0,
       (sy.alive_at_abs, len(sy.hitlog)))
    Nst = json.load(open(os.path.join(SCR, 'deepen5', 'results', 'N_final.json')))['N']
    ov = min(len(Nst), len(N))
    ok('S6 stored machine-replay N_j agree on the overlap', Nst[:ov] == N[:ov], ov)
    RES['S6 run'] = {'cycles': ncyc, 'absorptions': len(ab), 'flux_identity_checked': nid, 'triple_boundary_checked': n3, 'r_j_counts': rcount, 'records_compared_with_machine': compared,
                     'conveyor_walls_alive_at_end': len(wd.alive), 'zone_walls_created': wd.zone_walls}


def S7():
    B_ = 20000 if MODE == 'quick' else 131250
    rc, out, err, dt = sub([sys.executable, '-B', 'canon.py', str(32 * B_)], os.path.join(SCR, 'deepen6'))
    j = last_json(out)
    RES['S7 canon'] = j
    ok('S7 canonical state C(b) at j = 32b+17 for every b < B (closed system from the blank-run zone)',
       rc == 0 and j and j['not_canonical'] == 0 and j['blocks_canonical_at_r17'] >= B_ - 1, (rc, err[-300:]))
    # alive/hits over the same range
    rc, out, err, dt = sub([sys.executable, '-B', 'topsys.py', 'run', str(32 * B_), TMPD + '/cp_run.json'],
                           os.path.join(SCR, 'deepen6'))
    j = last_json(out)
    RES['S7 run'] = j
    ok('S7 no zone wall alive at any absorption, no hit (j < 32B)', rc == 0 and j and j['zone_walls_alive_at_an_absorption'] == 0
       and j['hits'] == 0, (rc, err[-300:]))
    ok('S7 every absorption shift lands on a D1 or a P (never on S1, SP, W or the blank; Lemma Z1)',
       rc == 0 and j and set(j['shift_landings']) <= {'', 'P'} and sum(j['shift_landings'].values()) == 32 * B_ - 1,
       j and j.get('shift_landings'))


def S8():
    kmax, bits = (60, 200) if MODE == 'quick' else (130, 400)
    samples = 1 if MODE == 'quick' else 3
    outp = TMPD + '/cp_symb.json'
    rc, out, err, dt = sub([sys.executable, '-B', 'symb.py', str(kmax), str(samples), str(bits), '11', outp],
                           os.path.join(SCR, 'deepen6'))
    try:
        j = json.load(open(outp))
    except Exception:
        j = None
    allgood = rc == 0 and j is not None
    if j:
        for k in range(kmax + 1):
            r = j.get(str(k)) or j.get(k)
            if r is None:
                allgood = False; continue
            want = 1 + (k + 9) // 32
            good = r['alive_at_absorption'] == 0 and r['hits'] == 0 and set(map(int, r['first_canonical_after_blocks'])) == {want}
            ok('S8 block map C(b) -> C(b + 1 + floor((k+9)/32)), random b < 2^BITS, 0 alive, 0 hits', good, (k, r))
    ok('S8 symb.py ran', allgood, (rc, err[-300:]))


def S9():
    d7, d8 = os.path.join(SCR, 'deepen7'), os.path.join(SCR, 'deepen8')
    rc, out, err, dt = sub([sys.executable, '-B', 'rundesc.py', TMPD + '/cp_rundesc.json'], d7)
    ok('S9 descent lemma: 13 entry + 8 phase steps symbolic (rundesc.py ALL OK)', rc == 0 and 'ALL OK' in out, err[-300:])
    for v0 in ([9] if MODE == 'quick' else [9, 10, 12, 16]):
        rc, out, err, dt = sub([sys.executable, '-B', 'symplant.py', TMPD + '/cp_symplant.json'], d8, env={'V0': str(v0)})
        j = last_json(out)
        ok('S9 plant lemma symbolic (symplant.py, V0 = %d)' % v0, rc == 0 and j and j['ok'] and j['walls_alive'] == 0 and j['hits'] == 0, (rc, err[-300:]))
    for scr in ('symentry1.py', 'symentryq.py'):
        rc, out, err, dt = sub([sys.executable, '-B', scr, TMPD + '/cp_' + scr + '.json'], d8, env={'V0': '8'})
        j = last_json(out)
        ok('S9 entry steps symbolic (%s, k >= 3)' % scr, rc == 0 and j and j['ok'] and j['walls_alive'] == 0 and j['hits'] == 0, (rc, err[-300:]))


def S10():
    d7, d8 = os.path.join(SCR, 'deepen7'), os.path.join(SCR, 'deepen8')
    q = MODE == 'quick'
    # value form below the growth range
    rc, out, err, dt = sub([sys.executable, '-B', 'vtot.py', 'validate', '20' if q else '300', '5', TMPD + '/cp_vtot.json', '3'], d7)
    j = last_json(out)
    ok('S10 value form exact for L >= 3 (vtot.py)', rc == 0 and j is not None and j.get('mismatch', j.get('mismatches', 1)) == 0, (rc, out[-300:], err[-300:]))
    RES['S10 vtot'] = j
    # Lemma L (locality, proof.md 6.4): representative runs with the lemma's hypotheses checked at every step
    d3 = os.path.join(SCR, 'proof3')
    rc, out, err, dt = sub([sys.executable, '-B', 'locality.py', 'smallk', '12' if q else '40', '4', TMPD + '/cp_lsmallk.json'], d3)
    j = last_json(out)
    RES['S10 small classes (Lemma L)'] = j
    ok('S10 small classes k <= KMAX: o = o0 direct, o0 + t*2^4 by Lemma L (locality.py smallk)', rc == 0 and j is not None
       and j['lemma_L_ok'] == j['representative_runs'] and j['direct_ok'] == j['direct_runs'] and j['representative_runs'] > 0,
       (rc, out[-300:], err[-300:]))
    R = 8 if q else 16
    rc, out, err, dt = sub([sys.executable, '-B', 'locality.py', 'endgame', str(R), str(R + 40), str(R + 3), TMPD + '/cp_lendgame.json'], d3)
    j = last_json(out)
    RES['S10 endgame (Lemma L)'] = j
    ok('S10 endgame: every residue k mod 2^R with nu2(k+9) <= R-2 by Lemma L (locality.py endgame)', rc == 0 and j is not None
       and j['lemma_L_ok'] == j['runs'] and j['runs'] + j['to_nested(nu2(k+9) >= R-1)'] == 2 ** R, (rc, out[-300:], err[-300:]))
    if R != 12:
        # the smaller split proposed for Rocq (proof.md section 10): residues mod 2^12 cover nu2(k+9) <= 10, the nested
        # range covers 11 <= v <= 50, and v > 50 goes through Lemma P, VF level 2 and E(v - 10) with v - 10 >= 41
        rc, out, err, dt = sub([sys.executable, '-B', 'locality.py', 'endgame', '12', '52', '15', TMPD + '/cp_lendgame12.json'], d3)
        j = last_json(out)
        RES['S10 endgame R = 12 (Rocq split)'] = j
        ok('S10 endgame R = 12: every residue k mod 2^12 with nu2(k+9) <= 10 by Lemma L (the Rocq split of section 10)',
           rc == 0 and j is not None and j['lemma_L_ok'] == j['runs'] == 4094 and j['to_nested(nu2(k+9) >= R-1)'] == 2,
           (rc, out[-300:], err[-300:]))
    V1 = 60 if q else 600
    rc, out, err, dt = sub([sys.executable, '-B', 'locality.py', 'nested', str(V1), TMPD + '/cp_lnested.json'], d3)
    j = last_json(out)
    RES['S10 nested range (Lemma L)'] = j
    ok('S10 nested range v = 10..V1, S mod 4 by Lemma L (locality.py nested)', rc == 0 and j is not None
       and j['lemma_L_ok'] == j['runs'] == 2 * (V1 - 9) and j['max_landing_minus_v'] <= 1, (rc, out[-300:], err[-300:]))


def S10_stored():
    """Quick mode only: the full-size Lemma L runs (R = 16, v <= 600; about 1 + 4 min) are rerun by S10 in full mode.
    In quick mode their stored results (scripts/proof3/results) are checked by content."""
    if MODE == 'full':
        return
    d3 = os.path.join(SCR, 'proof3', 'results')
    j = json.load(open(os.path.join(d3, 'locality_endgame_R16.json')))
    ok('S10s stored: Lemma L endgame R = 16 (65,534 residues + 2 with nu2(k+9) >= 15 to the nested recursion), all hypotheses hold',
       j['R'] == 16 and j['runs'] == 65534 and j['lemma_L_ok'] == 65534 and j['to_nested(nu2(k+9) >= R-1)'] == 2, j.get('first_bad'))
    j = json.load(open(os.path.join(d3, 'locality_nested_600.json')))
    ok('S10s stored: Lemma L nested range v = 10..600, S mod 4, all hypotheses hold',
       j['runs'] == 1182 and j['lemma_L_ok'] == 1182 and j['max_landing_minus_v'] <= 1 and j['v_range'][1] == 600, j.get('first_bad'))


def S11():
    """Lemma VF and the plant (proof.md 6.1-6.3, 6.5) as checked lemmas."""
    d4 = os.path.join(SCR, 'proof4')
    q = MODE == 'quick'
    rc, out, err, dt = sub([sys.executable, '-B', 'vf.py', 'reps', '8', '12', TMPD + '/cp_vfreps.json'], d4)
    j = last_json(out)
    RES['S11 VF representatives (Lemma L\', R = 8)'] = j and {k: j[k] for k in ('E', 'A', 'B', 'max_land', 'min_r_end', 'ab')}
    ok('S11 VF step lemma: 24 entry + 256 region-A + 1,024 region-B representatives satisfy Lemma L\' and give the next form',
       rc == 0 and j is not None and j['all_ok'] and j['E'] == [24, 24] and j['A'] == [256, 256] and j['B'] == [1024, 1024]
       and j['max_land'] <= 7 and j['min_r_end'] >= 1, (rc, out[-300:], err[-300:]))
    for mode, n, extra, key, need in (('entry', 300 if q else 2000, [], 'ok', 'runs'),
                                      ('plant', 300 if q else 3000, ['3000'], 'ok', 'runs'),
                                      ('chain1', 30 if q else 300, ['400'], 'runs_ok', 'runs'),
                                      ('chain2', 30 if q else 300, ['400'], 'runs_ok', 'runs')):
        rc, out, err, dt = sub([sys.executable, '-B', 'vf.py', mode, str(n), '21', TMPD + '/cp_vf_%s.json' % mode] + extra, d4)
        j = last_json(out)
        RES['S11 ' + mode] = j
        ok('S11 %s: %s/%s' % (mode, j and j.get(key), n), rc == 0 and j is not None and j[key] == j[need] == n
           and not j['first_bad'], (rc, out[-300:], err[-300:]))
    rc, out, err, dt = sub([sys.executable, '-B', 'vf.py', 'members', '300' if q else '3000', '22', TMPD + '/cp_vf_members.json'], d4)
    j = last_json(out)
    RES['S11 members'] = j
    ok('S11 random members: one real step from VF(off) gives VF(off+1)', rc == 0 and j is not None and not j['first_bad']
       and all(v[0] == v[1] and v[0] > 0 for v in j['members_by_region(run, ok)'].values()), (rc, out[-300:], err[-300:]))


def S12():
    """Lemmas Z0 and Z1 (proof.md section 6): where the shifts of the closed system land."""
    d5 = os.path.join(SCR, 'proof5')
    q = MODE == 'quick'
    JM = 32 * (20000 if q else 131250)
    rc, out, err, dt = sub([sys.executable, '-B', 'z1.py', 'orbit', str(JM), TMPD + '/cp_z1_orbit.json'], d5)
    j = last_json(out)
    RES['S12 orbit'] = j
    ok('S12 orbit from Z_1 to j = 32B: every wall shift and absorption shift lands on D1, P or the blank; no unit outside '
       'D0/D1/S1/P before any absorption (Lemma Z0); every zone in normal form (last unit not D0)', rc == 0 and j is not None
       and j['ok'] and j['jmax'] == JM and j.get('trailing_D0') == 0
       and j['landings'].get('abs->D1', 0) + j['landings'].get('abs->P', 0) + j['landings'].get('abs->blank', 0) == JM - 1,
       (rc, out[-300:], err[-300:]))
    nm, cm = (5, 32) if q else (6, 40)
    rc, out, err, dt = sub([sys.executable, '-B', 'z1.py', 'exhaustive', str(nm), str(cm), TMPD + '/cp_z1_exh.json'], d5)
    j = last_json(out)
    RES['S12 exhaustive'] = j
    ok('S12 Lemma Z1 exhaustive: every zone of <= NMAX units over D0/D1/S1/P/SP/W, every feed 1..CMAX: the first non-D0 '
       'unit after the carry phase is never S1', rc == 0 and j is not None and j['ok'] and j['zones'] == sum(5 * 6 ** i for i in range(nm))
       and j['phases'] == j['zones'] * cm, (rc, out[-300:], err[-300:]))
    rc, out, err, dt = sub([sys.executable, '-B', 'z1.py', 'random', '20000' if q else '200000', '5', TMPD + '/cp_z1_random.json'], d5)
    j = last_json(out)
    RES['S12 random'] = j
    ok('S12 Lemma Z1 on random zones (feed c >= 1, any walls): the first non-D0 unit after the carry phase is never S1; '
       'c = 0 control finds S1', rc == 0 and j is not None and j['ok'] and j['S1_targets'] == 0, (rc, out[-300:], err[-300:]))


SECTIONS = [('S1', S1), ('S2', S2), ('S3', S3), ('S4', S4), ('S5', S5), ('S6', S6), ('S7', S7), ('S8', S8), ('S9', S9),
            ('S10', S10), ('S10s', S10_stored), ('S11', S11), ('S12', S12)]

if __name__ == '__main__':
    sys.setrecursionlimit(100000)
    t0 = time.time()
    for name, fn in SECTIONS:
        if ONLY and name not in ONLY and not (name == 'S2' and ONLY & {'S3'}):
            continue
        ts = time.time()
        try:
            fn()
        except Exception as ex:   # a crash is a failure of that section
            ok(name + ' crashed', False, repr(ex))
        RES.setdefault('_time', {})[name] = round(time.time() - ts, 1)
    fails = {k: v for k, v in RES.items() if isinstance(v, dict) and v.get('fail')}
    RES['_mode'] = MODE
    RES['_all_pass'] = not fails
    print(json.dumps(RES, indent=1, default=str))
    print('ALL PASS' if not fails else 'FAILURES: ' + ', '.join(fails))
    sys.exit(0 if not fails else 1)