#!/usr/bin/env python3
"""check_proof.py: simulation evidence for the DELTA proof of 1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA--- (holdout line 604).

The parent is kill #3, 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB--- (KILLED_NONHALT). This script imports the
parent's check_proof.py read-only, for its abstract map (the rules of the parent's proof.md section 2), its
INV+(e) checker and its cycle-pair checker, and the parent's rocq/jcheck.py for the Rocq invariant J. Everything
that depends on the machine or on the start is re-run here on the twin: the twin's own transition table is
simulated directly, and the twin's own orbit is checked.

Nothing here is a proof. Every claim it checks is a hypothesis until Rocq accepts it.

Sections (each prints PASS/FAIL lines; the SUMMARY is the conjunction of S, A, C, D, B, G, N):
  S  the relation: rho = A->D, B->A, C->B, D->C (E, F fixed) is the only state renaming, with or without
     mirroring, that takes the parent's table to the twin's; the twin starts in A = rho(B), so its blank-tape run
     is the parent's run from 0^inf B> 0^inf, relabelled (checked step by step), not the parent's own run (which
     is at 0^inf 1 B> 0^inf after step 1). Also the relation to siblings #25 and #24 (informational).
  A  every macro rule of the parent's proof.md section 2, from random instances, simulated on the TWIN's table
     (canonical head state D = rho(A)), against the parent's abstract map; the halting cell
  C  the twin's initial segment: blank tape -> K0' = K(2; (7,4,0); -) at step 402
  D  the twin's direct simulation from blank vs the abstract map, transition by transition; the steps of the
     re-pairings and the base E-start K(2; (47,32,0),(40,33,1),(13,34,1); -) after re-pairing 6, at step 38,732
  B  the base: INV+(e) clause by clause (parent's inv_violations), with L* = 3; the Rocq J_base clauses (PC E1 of
     the parent's .v, transcribed) at the twin's base; the earlier E-starts (re-pairings 2, 4) have L* = 2
  G  the twin's orbit from its base: parent's section G2 (every lemma of proof.md 3.8 at every cycle pair) and
     section F (every clause of INV at every cycle), to L* > lmax; the parent's rocq/jcheck.py invariant J,
     macro step by macro step, for a number of re-pairings
  N  L* = 3 neighbourhood of the base: random regular L* = 3 INV+(e) starts in a box from the thresholds up to
     about twice the base's values, one checked cycle pair each (parent's cycle_pair_checked)
  O  (informational, not in the SUMMARY) the twin's orbit vs the parent's: not coupled, not a shifted copy;
     tape statistics at 1e9 steps (tools/sim.py C core)
Usage: python3 -B check_proof.py [--quick] [--seed N] [--steps N] [--lmax N] [--jcyc N] [--nbox N] [--no-o]
"""
import os, sys, random, argparse, itertools, importlib.util
from collections import Counter
sys.dont_write_bytecode = True

TM = '1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---'
PARENT = '1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---'
SIB25 = '1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---'
SIB24 = '1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---'
HERE = os.path.dirname(os.path.abspath(__file__))
PDIR = os.path.join(os.path.dirname(HERE), PARENT)
ROOT = os.path.dirname(os.path.dirname(HERE))

def load(name, path):
    spec = importlib.util.spec_from_file_location(name, path)
    mod = importlib.util.module_from_spec(spec); spec.loader.exec_module(mod)
    return mod

cp = load('parent_check_proof', os.path.join(PDIR, 'check_proof.py'))   # parent's checks (read-only)
assert cp.TM == PARENT

ST = 'ABCDEF'
RHO = {'A': 'D', 'B': 'A', 'C': 'B', 'D': 'C', 'E': 'E', 'F': 'F'}       # parent state -> twin state
TAB = cp.parse_tm(TM)                                                    # (state index, read) -> (write, move, next) | None
CANON = ST.index(RHO['A'])                                               # the twin's K head state: D
PSTART = [c for c in ST if RHO[c] == 'A'][0]                             # parent state the twin starts in: B

INIT_STEP = 402
INIT_K = (2, [(7, 4, 0)], None)
BASE_STEP = 38732          # checked in section D (parent: 78,710)
BASE_K = (2, [(47, 32, 0), (40, 33, 1), (13, 34, 1)], None)
PARENT_BASE_K = (2, [(95, 68, 0), (34, 33, 1), (10, 15, 1), (1, 24, 1)], None)

def letters(s):
    t = {}
    for i, blk in enumerate(s.split('_')):
        for r in (0, 1):
            x = blk[3*r:3*r+3]
            t[(ST[i], r)] = None if x == '---' else (int(x[0]), x[1], x[2])
    return t

# ---------------------------------------------------------------- S: the relation
def image(tp, sig, mirror):
    out = {}
    for (q, r), v in tp.items():
        out[(sig[q], r)] = None if v is None else (v[0], {'L': 'R', 'R': 'L'}[v[1]] if mirror else v[1], sig[v[2]])
    return out

def maps(src, dst):
    tp, tt = letters(src), letters(dst)
    return [(dict(zip(ST, perm)), mir) for perm in itertools.permutations(ST) for mir in (False, True)
            if image(tp, dict(zip(ST, perm)), mir) == tt]

def lockstep(n):
    """Twin from 0^inf A> 0^inf vs parent from 0^inf B> 0^inf: same tape, same position, twin state = rho(parent state)."""
    tp, tt = cp.TAB, TAB
    sg = [ST.index(RHO[c]) for c in ST]
    size = 2*n + 16
    a = bytearray(size); b = bytearray(size); pa = pb = n + 8
    sa, sb = 0, ST.index(PSTART)                       # twin starts in A, parent in B
    for step in range(n):
        if sa != sg[sb] or pa != pb or a[pa] != b[pb]: return step
        ta, tb = tt[(sa, a[pa])], tp[(sb, b[pb])]
        if (ta is None) != (tb is None): return step
        if ta is None: return None
        a[pa] = ta[0]; pa += ta[1]; sa = ta[2]
        b[pb] = tb[0]; pb += tb[1]; sb = tb[2]
    return None if a == b else -1

def fmt_map(s): return ''.join(s[c] for c in ST)

def section_S(n):
    print('== S. relation to the parent: renaming / mirror search, start state, lockstep')
    sols = maps(PARENT, TM)
    uniq = len(sols) == 1 and sols[0] == (RHO, False)
    print('  maps phi with twin = phi(parent) among 720 renamings x {plain, mirror}: %s' %
          [(fmt_map(s), 'mirror' if m else 'plain') for s, m in sols])
    print('  unique, no mirror, rho = %s (A->D B->A C->B D->C, E, F fixed; the 4-cycle (A D C B)) ->' % fmt_map(RHO),
          'PASS' if uniq else 'FAIL')
    print('  twin start state A = rho(%s): the twin from blank is rho(parent from 0^inf %s> 0^inf)' % (PSTART, PSTART))
    r = lockstep(n)
    okl = r is None
    print('  lockstep %d steps, twin from blank vs relabelled parent from 0^inf B> 0^inf: %s -> %s' % (
        n, 'identical at every step' if okl else 'differ at step %s' % r, 'PASS' if okl else 'FAIL'))
    # the parent's own run: A0 = 1RB, so after step 1 it is at 0^inf 1 B> 0^inf (not 0^inf B> 0^inf)
    own = cp.TAB[(0, 0)] == (1, 1, 1)
    print('  parent from its own blank start: A0 = 1RB, so step 1 is 0^inf 1 B> 0^inf; the twin lacks that 1 ->',
          'PASS' if own else 'FAIL')
    # siblings (informational): #25 = sigma(parent), #24 = phi(mirror(parent))
    s25 = maps(SIB25, TM); s24 = maps(SIB24, TM)
    print('  (info) twin = psi(#25): %s, start = #25\'s %s; twin = psi(#24): %s, start = #24\'s %s' % (
        [(fmt_map(s), 'mirror' if m else 'plain') for s, m in s25], [c for c in ST if s25 and s25[0][0][c] == 'A'],
        [(fmt_map(s), 'mirror' if m else 'plain') for s, m in s24], [c for c in ST if s24 and s24[0][0][c] == 'A']))
    return uniq and okl and own and PSTART == 'B' and CANON == 3

# ---------------------------------------------------------------- A: the parent's rules on the twin's table
def run_macro(h, P, T, cap=None):
    """Parent's run_macro, on the twin's table, with the twin's canonical head state D (= rho(A))."""
    w = cp.build(h, P, T); n = len(w)
    if cap is None: cap = 400*n*n + 100000
    pad = 4*n + 64
    tape = bytearray(pad) + bytearray(int(c) for c in w) + bytearray(pad)
    pos = pad - 1; st = CANON; lo = pos; steps = 0
    while steps < cap:
        tr = TAB[(st, tape[pos])]
        if tr is None: return ('HALT', steps, st)
        tape[pos] = tr[0]; pos += tr[1]; st = tr[2]; steps += 1
        if pos < 0 or pos >= len(tape):
            ext = bytearray(len(tape))
            if pos < 0: tape = ext + tape; pos += len(ext); lo += len(ext)
            else: tape = tape + ext
        if pos < lo: lo = pos
        if st == CANON and pos <= lo + 1 and tape[pos] == 0 and not any(tape[lo:pos]):
            r = cp.parse(''.join('1' if b else '0' for b in tape[pos+1:]))
            if r is not None and r[0] != '?': return (r, steps)
    return ('CAP', steps)

def section_A(n, rng):
    print('== A. the parent\'s macro rules (proof.md section 2 of the parent) on the TWIN\'s table, head state D')
    allok = True; tot = 0
    for rule in cp.RULES:
        ok = 0; fails = []
        for i in range(n):
            h, P, T = cp.gen(rule, rng, i)
            exp = cp.astep(h, P, T)
            assert exp[3] == rule, (rule, exp[3], h, P, T)
            got = run_macro(h, P, T)
            good = got[0] not in ('HALT', 'CAP') and got[0] == (exp[0], exp[1], exp[2]) and got[1] >= 1
            ok += good
            if not good: fails.append((h, P, T, str(got)[:120]))
        tot += n; allok &= (ok == n)
        print('  %-14s %3d/%d %s' % (rule, ok, n, 'PASS' if ok == n else 'FAIL ' + str(fails[:2])))
    # the halting cell, relabelled: parent halts on F1, F entered only from C1 (=1RF), C only from B0;
    # twin: F1 is ---, F is entered only from B1 (=1RF), B is entered only from A0 (=1RB)
    entF = sorted(ST[q] + str(r) for (q, r), v in TAB.items() if v and v[2] == 5)
    entB = sorted(ST[q] + str(r) for (q, r), v in TAB.items() if v and v[2] == 1)
    okh = TAB[(5, 1)] is None and entF == ['B1'] and entB == ['A0'] and TAB[(1, 1)] == (1, 1, 5) and TAB[(0, 0)] == (1, 1, 1)
    print('  halting transition: F1 undefined; F entered only from %s, B only from %s; so the twin halts exactly at A> 0 1 1 ->'
          % (entF, entB), 'PASS' if okh else 'FAIL')
    print('  A total: %s (%d instances)' % ('PASS' if allok and okh else 'FAIL', tot))
    return allok and okh

# ---------------------------------------------------------------- C, D: the twin's initial segment, direct cross-check
def stream_canonical(max_steps):
    """Direct simulation of the twin from the blank tape; yields (step, K) at every canonical record config
    (state D on a new leftmost cell, tape to its right parses as some K)."""
    size = 1 << 16
    tape = bytearray(size); pos = size//2; st = 0; lo = pos; hi = pos; steps = 0
    while steps < max_steps:
        tr = TAB[(st, tape[pos])]
        if tr is None: yield (steps, 'HALT'); return
        tape[pos] = tr[0]; pos += tr[1]; st = tr[2]; steps += 1
        if pos < 0 or pos >= len(tape):
            ext = bytearray(len(tape))
            if pos < 0: tape = ext + tape; pos += len(ext); lo += len(ext); hi += len(ext)
            else: tape = tape + ext
        if pos > hi: hi = pos
        if pos < lo:
            lo = pos
            if st == CANON:
                r = cp.parse(tape[pos+1:hi+1].translate(cp.BITS).decode())
                if r is not None and r[0] != '?': yield (steps, r)

REPAIRS = {}               # filled by section_CD: re-pairing number -> (step, K)

def section_CD(max_steps):
    print('== C. the twin\'s initial segment')
    seq = list(stream_canonical(max_steps))
    halted = any(k == 'HALT' for _, k in seq)
    pre = [(s, k) for s, k in seq if s < INIT_STEP]
    first = [x for x in seq if x[0] == INIT_STEP]
    okC = bool(first) and first[0][1] == INIT_K and not halted
    print('  canonical configs before step %d: %s' % (INIT_STEP, pre))
    okpre = len(pre) == 1 and pre[0][1][1] == []
    if pre:
        try:
            cp.astep(*pre[0][1]); print('  step %d: in D (unexpected)' % pre[0][0]); okpre = False
        except cp.Outside as e:
            print('  step %d has L = 0: outside D (%s), so the argument starts at the next canonical config' % (pre[0][0], e))
    okC = okC and okpre
    print('  step %d: K0\' = %s -> %s' % (INIT_STEP, first[0][1] if first else None, 'PASS' if okC else 'FAIL'))
    print('== D. the twin\'s direct simulation from blank (%d steps) vs the parent\'s abstract map' % max_steps)
    cnt = Counter(); bad = 0; rep = 0; base = None; reps = []
    post = [x for x in seq if x[0] >= INIT_STEP and x[1] != 'HALT']
    for (s0, k0), (s1, k1) in zip(post, post[1:]):
        try:
            h, P, T, name = cp.astep(*k0)
            if (h, P, T) == (k1[0], k1[1], k1[2]):
                cnt[name] += 1
                if name in ('Ov', 'X1'):
                    rep += 1; reps.append(s1); REPAIRS[rep] = (s1, k1)
                    if rep == 6: base = (s1, k1)
            else: bad += 1; print('  MISMATCH at step', s0, k0, '->', k1, 'predicted', (h, P, T))
        except cp.Outside as e:
            bad += 1; print('  OUTSIDE at step', s0, e)
    okD = bad == 0 and len(post) > 1 and not halted
    print('  %d consecutive canonical transitions, %s; last canonical step %d -> %s' % (
        sum(cnt.values()), dict(cnt), post[-1][0], 'PASS' if okD else 'FAIL'))
    print('  re-pairings (Ov/X1) at steps:', reps[:12], '...' if len(reps) > 12 else '')
    okB = base is not None and base[0] == BASE_STEP and base[1] == BASE_K
    print('  base E-start (after re-pairing 6): step %s, %s -> %s' % (base[0] if base else None, base[1] if base else None,
                                                                   'PASS' if okB else 'FAIL'))
    return okC, okD and okB

# ---------------------------------------------------------------- B: INV+(e) and the Rocq J clauses at the base
def dv(P):
    v = 0
    for (_, _, d) in reversed(P): v = d + 2*v
    return v

def PC_E1(h, i, p, q, n, tv):
    """PC E1 false h i p q n tv of the parent's .v (Definitions PN, PI, PC), transcribed literally."""
    w = 2**n
    pn = (q >= tv + w + 1 and p + tv + w >= 3) if n == 0 else \
         (q >= tv + 3*w + 1 and (p + tv) % 2 == 1 and p + tv + w >= 3*w)
    if i == 1: pi = h % 2 == 0 and 2 <= n and p + tv + w + 3 >= 11*w and h + 4*(tv + w) + 6 >= 12*w
    elif i == 2: pi = p + tv + w + 1 >= 7*w
    else: pi = True
    return 1 <= p and 1 <= q and pn and pi

def J_base(K):
    """J (mkst h P TN E1 false): P <> [], TC E1 false TN (T = TN, c4 = false), AllI (PCx E1 false h) 1 P."""
    h, P, T = K
    if not P or T is not None: return False, []
    res = [PC_E1(h, i+1, p, q, len(P)-1-i, dv(P[i:])) for i, (p, q, d) in enumerate(P)]
    return all(res), res

def section_B():
    print('== B. the base E-start: INV+(e) (parent proof.md 3.8.1) and the Rocq J_base clauses')
    h, P, T = BASE_K
    v = cp.inv_violations(*BASE_K)
    Ls = cp.Lstar(P, T)
    print('  %s: L* = %d; (a) p_1=%d >= 7, digits %s, far pair (p,q) = (%d,%d), q >= 6; (b) q_1+1=%d >= %d, q_2=%d >= %d;'
          ' (c) p+d = %d, %d odd; (d) L* = %d >= 3; (e1) p_1+1=%d >= %d, (e2) p_2=%d >= %d' % (
          BASE_K, Ls, P[0][0], [d for _, _, d in P], P[2][0], P[2][1], P[0][1]+1, 5*2**(Ls-1), P[1][1], 5*2**(Ls-2),
          P[0][0]+P[0][2], P[1][0]+P[1][2], Ls, P[0][0]+1, 2**(Ls+2), P[1][0], 2**Ls))
    okI = not v and Ls == 3
    print('  INV+(e) violations:', v or 'none', '->', 'PASS' if okI else 'FAIL')
    okJ, res = J_base(BASE_K)
    okJp, resp = J_base(PARENT_BASE_K)
    print('  Rocq J (mkst 2 base TN E1 false), PC E1 per pair:', res, '-> twin', 'PASS' if okJ else 'FAIL',
          '| parent base (sanity):', 'PASS' if okJp else 'FAIL')
    # the clauses in numbers (n = pairs to the right, tv = digit value from the pair up, w = 2^n)
    for i, (p, q, d) in enumerate(P):
        n = len(P)-1-i; tv = dv(P[i:]); w = 2**n
        if n == 0: s = 'q=%d >= tv+w+1=%d; p+tv+w=%d >= 3' % (q, tv+w+1, p+tv+w)
        else: s = 'q=%d >= tv+3w+1=%d; p+tv=%d odd; p+tv+w=%d >= 3w=%d' % (q, tv+3*w+1, p+tv, p+tv+w, 3*w)
        if i == 0: s += '; PI: n=%d >= 2, p+tv+w+3=%d >= 11w=%d, h+4(tv+w)+6=%d >= 12w=%d (tight)' % (n, p+tv+w+3, 11*w, h+4*(tv+w)+6, 12*w)
        if i == 1: s += '; PI: p+tv+w+1=%d >= 7w=%d' % (p+tv+w+1, 7*w)
        print('    pair %d (n=%d, tv=%d, w=%d): %s' % (i+1, n, tv, w, s))
    # the earlier E-starts (even re-pairings before 6) cannot be the base: L* = 2 violates (d) (and J's 2 <= n for pair 1)
    early = []
    for r in (2, 4):
        if r in REPAIRS:
            s, K = REPAIRS[r]; early.append((r, s, K, cp.inv_violations(*K), J_base(K)[0]))
    for r, s, K, vv, jj in early: print('  (info) E-start after re-pairing %d (step %d): %s, INV+(e) violations %s, J %s' % (r, s, K, vv, jj))
    okE = len(early) == 2 and all('d:L*>=3' in vv and not jj for _, _, _, vv, jj in early)
    print('  re-pairing 6 is the first E-start where INV+(e) and J hold ->', 'PASS' if okE else 'FAIL')
    return okI and okJ and okJp and okE

# ---------------------------------------------------------------- G: the twin's orbit through the parent's checks
def section_G(lmax, jcyc):
    print('== G. the twin\'s orbit from its base through the parent\'s checks (G2, F) and the parent\'s jcheck J')
    saved = (cp.INIT_K, cp.BASE_K)
    cp.INIT_K, cp.BASE_K = INIT_K, BASE_K          # the parent's orbit_e/class_invariants read these globals
    try:
        r2 = cp.orbit_e(lmax)
        rF = cp.class_invariants(lmax, base_ov=6)
    finally:
        cp.INIT_K, cp.BASE_K = saved
    jc = load('parent_jcheck', os.path.join(PDIR, 'rocq', 'jcheck.py'))
    Pb = [list(x) for x in BASE_K[1]]
    res = jc.run(BASE_K[0], Pb, ('N',), ('E1', False), jcyc)
    okj = res[0] == 'OK'
    print('  jcheck J (parent rocq/jcheck.py) at every macro step from the twin\'s base, %d re-pairings: %s %s rules %s -> %s'
          % (jcyc, res[0], res[1] or '', res[3], 'PASS' if okj else 'FAIL'))
    ok = r2 and rF and okj
    print('  G total:', 'PASS' if ok else 'FAIL')
    return ok

# ---------------------------------------------------------------- N: L* = 3 starts around the base
def section_N(nbox, rng):
    print('== N. %d random regular L* = 3 INV+(e) starts, thresholds .. about 2x the base, one checked cycle pair each' % nbox)
    st = cp.new_stats(); fails = []; bad = None; n = 0; nxt = Counter()
    for _ in range(nbox):
        p1 = rng.randrange(31, 96, 2); q1 = rng.randint(19, 64)
        p2 = rng.randrange(8, 81, 2); q2 = rng.randint(10, 66)
        pf = rng.randint(1, 26); qf = rng.randint(6, 68)
        K = (2, [(p1, q1, 0), (p2, q2, 1), (pf, qf, 1)], None)
        assert not cp.inv_violations(*K), K
        n += 1; f0 = len(fails)
        try:
            K2 = cp.cycle_pair_checked(K, fails, st)
            nxt[cp.Lstar(K2[1], K2[2])] += 1
        except cp.Outside as e: fails.append('OUTSIDE %s' % e)
        if len(fails) > f0 and bad is None: bad = (K, fails[f0:f0+3])
        if len(fails) > 50: break
    ok = not fails
    print('  %d starts (box contains the base %s): %s | next L*: %s | %s' % (
        n, BASE_K[1], 'PASS' if ok else 'FAIL first %s' % (bad,), dict(sorted(nxt.items())), cp.fmt_stats(st)))
    return ok

# ---------------------------------------------------------------- O: orbit comparison (informational)
def estarts(K, count):
    """The E-starts of the abstract orbit from E-start K (every second re-pairing)."""
    out = [K]; h, P, T = K
    while len(out) < count:
        for _ in range(2): _, (h, P, T) = cp.run_to_repair((h, P, T))
        out.append((h, list(P), T))
    return out

def section_O(n):
    print('== O. (informational) the twin\'s orbit vs the parent\'s')
    tw = estarts(BASE_K, n); pa = estarts(PARENT_BASE_K, n)
    key = lambda K: (K[0], tuple(map(tuple, K[1])), K[2])
    common = set(map(key, tw)) & set(map(key, pa))
    print('  first %d E-starts of each orbit (from each base): %d in common (a shifted copy would share all but finitely many)' % (n, len(common)))
    for i in (0, 1, 2, 5, 10, 20, n-1):
        a, b = tw[i], pa[i]
        print('    E-start %3d: twin L* = %3d, p_1 = %d | parent L* = %3d, p_1 = %d' % (i, cp.Lstar(a[1], a[2]), a[1][0][0], cp.Lstar(b[1], b[2]), b[1][0][0]))
    try:
        sys.path.insert(0, os.path.join(ROOT, 'tools')); import sim
        r = sim.run(sim.parse(TM), max_steps=10**9, final=False)
        print('  twin at 1e9 steps (tools/sim.py): span %d..%d = %d cells, %d nonzeros, halted %s (parent: 67,343 cells, 33,665 nonzeros)'
              % (r.lo, r.hi, r.hi - r.lo + 1, r.nonzeros, r.halted))
    except Exception as e:
        print('  sim at 1e9 skipped:', e)

if __name__ == '__main__':
    ap = argparse.ArgumentParser()
    ap.add_argument('--quick', action='store_true')
    ap.add_argument('--seed', type=int, default=20261010)
    ap.add_argument('--steps', type=int, default=None)
    ap.add_argument('--lmax', type=int, default=None)
    ap.add_argument('--jcyc', type=int, default=None)
    ap.add_argument('--nbox', type=int, default=None)
    ap.add_argument('--no-o', action='store_true')
    a = ap.parse_args()
    rng = random.Random(a.seed)
    n = 12 if a.quick else 45
    steps = a.steps or (2*10**6 if a.quick else 3*10**7)
    lmax = a.lmax or (60 if a.quick else 300)
    jcyc = a.jcyc or (26 if a.quick else 34)
    nbox = a.nbox or (500 if a.quick else 5000)
    r = {'S relation': section_S(2*10**5 if a.quick else 2*10**6), 'A rules on twin': section_A(n, rng)}
    okC, okD = section_CD(steps)
    r['C init'] = okC; r['D cross-check+base'] = okD
    r['B base INV+(e), J'] = section_B()
    r['G twin orbit'] = section_G(lmax, jcyc)
    r['N L*=3 box'] = section_N(nbox, rng)
    if not a.no_o: section_O(40 if a.quick else 120)
    print('== SUMMARY:', ', '.join('%s %s' % (k, 'PASS' if v else 'FAIL') for k, v in r.items()), '->',
          'PASS' if all(r.values()) else 'FAIL',
          '| Simulation checks the claims of proof.md; the proof is the argument in proof.md (and the parent\'s).')
    sys.exit(0 if all(r.values()) else 1)