#!/usr/bin/env python3
"""check_proof.py: simulation evidence for the DELTA proof.md of twin #24 (1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---)
against the parent kill #3 (1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---).

The twin is the parent mirrored (L <-> R) and renamed (twin A,B,C,D,E,F = parent D,A,B,C,E,F), but started in
parent state D. So every rule, outside case and invariant of the parent's proof.md carries over unchanged; only the
initial segment and the base E-start differ. This script checks exactly that delta. It has its own direct
simulator of the TWIN string (section A, C, D never run the parent's table) and reuses the parent's abstract map,
INV+(e) checker, cycle-pair checker (machines/<parent>/check_proof.py) and Rocq invariant J (rocq/jcheck.py).

Sections (each prints PASS/FAIL lines; SUMMARY is PASS only if M, S, A, C, D, B, G and J all pass):
  M  the map: transition-table identity under mirror + renaming (12/12 entries), uniqueness over all 2 x 720
     candidates, image of the start state (D, not A), and the halting transition of the twin
  S  step-by-step conjugacy: twin from the blank tape vs parent started in D on the blank tape, in lockstep
  A  every macro rule of the parent's proof.md section 2, transported to the twin (mirrored words, state B),
     from random concrete instances, by direct simulation of the TWIN machine
  C  the initial segment of the twin: blank tape -> K0' = K(2; (11,12,0); -) at step 1021
  D  direct simulation of the twin from the blank tape: every canonical transition is predicted by the parent's
     abstract map; the base E-start after overflow 6 is reached at step 78,911
  B  the base E-start K(2; (95,68,0),(34,33,1),(10,15,1),(1,25,1); -): INV+(e) clause by clause, and the parent's
     Rocq invariant J (ghost phase E1)
  G  the parent's cycle_pair_checked (all identities of proof.md 3.8) on the twin's orbit from the base to L* > lmax
  J  the parent's Rocq invariant J at every macro step of the twin's orbit from the base, for N re-pairings
  L  INFORMATIONAL: lockstep with the parent's abstract orbit (same rule sequence; the states differ by exactly +1
     on the far/tail block). Not used by the proof.
  N  (--selftest) negative controls: every check above is fed a deliberately wrong input and must FAIL
Usage: python3 -B check_proof.py [--quick] [--selftest] [--seed N] [--steps N] [--lmax N] [--sstep N] [--jcyc N] [--llmax N]
"""
import sys, os, re, random, argparse, hashlib, itertools, importlib.util

HERE = os.path.dirname(os.path.abspath(__file__))
TW = '1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---'
PA = '1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---'
PDIR = os.path.join(os.path.dirname(HERE), PA)

# parent files this delta rests on (sha256 at the time of writing; a change prints WARN, not FAIL)
PINS = {
    'check_proof.py': '7d1c92b9cf8fdd9f59a03d33dbc06309675461deca038d72cb4ef7e83aeff7fc',
    'rocq/jcheck.py': '0e3909cc37b53c188d48f9cf9033c3b62dac34f5fa37a1e812738ce220fa483a',
    'proof.md': 'e884353649ff3354f0abde5fbbf6965d31396cd35101e12cdb1f02013937d931',
    PA + '.v': '91861259c71ce3338425a86a465c4af5b854f63f071737b8cd7feaa36713fcbf',
}

def load_parent():
    argv = sys.argv; sys.argv = ['check_proof.py']
    try:
        spec = importlib.util.spec_from_file_location('parent_cp', os.path.join(PDIR, 'check_proof.py'))
        cp = importlib.util.module_from_spec(spec); spec.loader.exec_module(cp)
        sys.path.insert(0, os.path.join(PDIR, 'rocq'))
        import jcheck
    finally:
        sys.argv = argv
    return cp, jcheck

cp, jc = load_parent()

# ---------------------------------------------------------------- tables and the map
def parse_tm(s):
    """(state index, read) -> None | (write, +1/-1, next state index)."""
    tab = {}
    for i, blk in enumerate(s.split('_')):
        for r in (0, 1):
            t = blk[3*r:3*r+3]
            tab[(i, r)] = None if t == '---' else (int(t[0]), 1 if t[1] == 'R' else -1, ord(t[2]) - 65)
    return tab

TT = parse_tm(TW)          # twin
TP = parse_tm(PA)          # parent
S = 'ABCDEF'
MAP = {'A': 'D', 'B': 'A', 'C': 'B', 'D': 'C', 'E': 'E', 'F': 'F'}      # twin state -> parent state
MI = {S.index(a): S.index(b) for a, b in MAP.items()}
INV_MI = {v: k for k, v in MI.items()}
TB_ = S.index('B')         # twin state playing the parent's A (the canonical state)

def conj_ok(perm, mirror):
    for (q, b), v in TT.items():
        w = TP[(perm[q], b)]
        if v is None or w is None:
            if (v is None) != (w is None): return False
            continue
        if (v[0], -v[1] if mirror else v[1], perm[v[2]]) != w: return False
    return True

def section_M():
    print('== M. the map: twin = mirror + renaming of the parent')
    ok = conj_ok(MI, True)
    print('  table identity under mirror and %s: %s' % (', '.join('%s->%s' % kv for kv in MAP.items()), 'PASS (12/12 entries, halting entry F1 -> F1)' if ok else 'FAIL'))
    hits = []
    for mirror in (False, True):
        for perm in itertools.permutations(range(6)):
            if conj_ok(dict(enumerate(perm)), mirror): hits.append((mirror, perm))
    uniq = len(hits) == 1 and hits[0][0] and dict(enumerate(hits[0][1])) == MI
    print('  candidates searched: 2 orientations x 720 renamings; matches: %d (%s) -> %s' % (
        len(hits), ['mirror ' + ''.join(S[p] for p in h[1]) if h[0] else 'plain ' + ''.join(S[p] for p in h[1]) for h in hits],
        'PASS (unique)' if uniq else 'FAIL'))
    st = MI[0]
    okst = st == S.index('D')
    print('  start state: twin A -> parent %s, so the twin runs the parent from %s;; tape0, not from c0 -> %s' % (
        S[st], S[st], 'PASS' if okst else 'FAIL'))
    # halting transition of the twin: which (state, read) is undefined, who enters it, who enters that
    und = [k for k, v in TT.items() if v is None]
    intoF = [(S[q], b) for (q, b), v in TT.items() if v is not None and v[2] == 5]
    intoD = [(S[q], b) for (q, b), v in TT.items() if v is not None and v[2] == 3]
    okh = und == [(5, 1)] and intoF == [('D', 1)] and intoD == [('C', 0)] and TT[(3, 1)][1] == -1 and TT[(2, 0)][1] == -1
    print('  twin halts only on F1; only D1 (1LF) enters F; only C0 (1LD) enters D: halts exactly from `1 1 0 <C` '
          '(mirror of the parent\'s `B> 0 1 1`) -> %s' % ('PASS' if okh else 'FAIL'))
    return ok and uniq and okst and okh

# ---------------------------------------------------------------- S: lockstep conjugacy
def section_S(nsteps):
    print('== S. lockstep: twin from the blank tape vs parent from D on the blank tape, %d steps' % nsteps)
    size = 1 << 16
    t1 = bytearray(size); t2 = bytearray(size); p1 = size // 2; p2 = size // 2; q1 = 0; q2 = MI[0]
    bad = None
    for n in range(nsteps):
        if q2 != MI[q1]: bad = (n, 'state'); break
        s1 = t1[p1]; s2 = t2[p2]
        if s1 != s2: bad = (n, 'read'); break
        a = TT[(q1, s1)]; b = TP[(q2, s2)]
        if a is None or b is None:
            bad = (n, 'halt' if (a is None) == (b is None) else 'halt mismatch'); break
        if b != (a[0], -a[1], MI[a[2]]): bad = (n, 'transition'); break
        t1[p1] = a[0]; p1 += a[1]; q1 = a[2]
        t2[p2] = b[0]; p2 += b[1]; q2 = b[2]
        if not (0 < p1 < len(t1) - 1 and 0 < p2 < len(t2) - 1):
            # re-centre both tapes (keep the mirror relation: p2 - c2 = -(p1 - c1))
            e = bytearray(len(t1)); t1 = e + t1 + bytearray(len(t1)); p1 += len(e)
            e = bytearray(len(t2)); t2 = e + t2 + bytearray(len(t2)); p2 += len(e)
    # final tapes, mirrored around the heads
    c1 = [i - p1 for i, v in enumerate(t1) if v]; c2 = sorted(p2 - i for i, v in enumerate(t2) if v)
    same = bad is None and c1 == c2
    print('  %s; at step %d: twin state %s, parent state %s, %d nonzeros each, tapes mirror images around the head: %s' % (
        'every step: mapped state, same symbol read, mirrored transition' if bad is None else 'BROKEN at step %d (%s)' % bad,
        nsteps, S[q1], S[q2], len(c1), 'PASS' if same else 'FAIL'))
    return same

# ---------------------------------------------------------------- the twin's own canonical configurations
# Twin canonical moment: state B (= parent A) on a blank cell with only blanks to its right, and the cells to its
# left, read from the head outward, parse as the parent's K word.  K'(h;P;T) := mirror of K(h;P;T).
BITS = bytes.maketrans(bytes([0, 1]), b'01')

def run_macro_twin(h, P, T, cap=None):
    """Direct simulation of the TWIN from the mirrored K(h;P;T) (state B on the blank cell right of the word) to the
    next canonical twin configuration. Returns ((h',P',T'), steps) | ('HALT', steps) | ('CAP', steps)."""
    w = cp.build(h, P, T)[::-1]; 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 + n; st = TB_; hi = pos; steps = 0
    while steps < cap:
        tr = TT[(st, tape[pos])]
        if tr is None: return ('HALT', steps)
        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); hi += len(ext)
            else: tape = tape + ext
        if pos > hi: hi = pos
        if st == TB_ and pos >= hi - 1 and tape[pos] == 0 and not any(tape[pos:hi+1]):
            r = cp.parse(bytes(reversed(tape[:pos])).translate(BITS).decode())
            if r is not None and r[0] != '?': return (r, steps)
    return ('CAP', steps)

def stream_twin(max_steps):
    """Direct simulation of the twin from the blank tape; yields (step, K) at every canonical record config."""
    size = 1 << 16
    tape = bytearray(size); pos = size // 2; st = 0; lo = pos; hi = pos; steps = 0
    while steps < max_steps:
        tr = TT[(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 < lo: lo = pos
        if pos > hi:
            hi = pos
            if st == TB_:
                r = cp.parse(bytes(reversed(tape[lo:pos])).translate(BITS).decode())
                if r is not None and r[0] != '?': yield (steps, r)

# ---------------------------------------------------------------- A: rules on the twin directly
def section_A(n, rng):
    print('== A. the parent\'s macro rules, transported (mirrored words), on the TWIN machine: random instances')
    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_twin(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])))
    print('  A total: %s (%d instances)' % ('PASS' if allok else 'FAIL', tot))
    return allok

# ---------------------------------------------------------------- C, D: initial segment, cross-check, base
INIT_STEP = 1021
INIT_K = (2, [(11, 12, 0)], None)
BASE_STEP = 78911
BASE_K = (2, [(95, 68, 0), (34, 33, 1), (10, 15, 1), (1, 25, 1)], None)
ALT_BASE = (19589, (2, [(47, 32, 0), (16, 15, 1), (4, 21, 1)], None))      # E-start after overflow 4 (option)

def section_CD(max_steps):
    print('== C. twin initial segment')
    seq = list(stream_twin(max_steps))
    if any(k == 'HALT' for _, k in seq):
        print('  HALT in direct simulation -> FAIL'); return False, None
    pre = [(s, k) for s, k in seq if s < INIT_STEP]
    first = [k for s, k in seq if s == INIT_STEP]
    okC = first == [INIT_K]
    print('  canonical configs before step %d: %s' % (INIT_STEP, pre))
    print('  step %d: %s -> %s' % (INIT_STEP, first[0] if first else None, 'PASS' if okC else 'FAIL'))
    print('== D. direct simulation of the twin from blank (%d steps) vs the parent\'s abstract map' % max_steps)
    from collections import Counter
    cnt = Counter(); bad = 0; rep = 0; base = None; reps = []
    post = [x for x in seq if x[0] >= INIT_STEP]
    for (s0, k0), (s1, k1) in zip(post, post[1:]):
        try:
            h, P, T, name = cp.astep(*k0)
            if (h, P, T) == tuple(k1): cnt[name] += 1
            else: bad += 1; print('  MISMATCH at step', s0, k0, '->', k1, 'predicted', (h, P, T))
        except cp.Outside as e:
            bad += 1; name = None; print('  OUTSIDE at step', s0, e)
        if name in ('Ov', 'X1'):
            rep += 1; reps.append(s1)
            if rep == 6: base = (s1, k1)
    okD = bad == 0 and len(post) > 1
    print('  %d consecutive canonical transitions, %s; re-pairings at steps %s; last canonical step %d -> %s' % (
        sum(cnt.values()), dict(cnt), reps[:8] + (['...'] if len(reps) > 8 else []), post[-1][0], 'PASS' if okD else 'FAIL'))
    return okC and okD, (base, seq)

def section_B(base, seq):
    print('== B. the base E-start (after overflow 6)')
    okpos = base is not None and base[0] == BASE_STEP and tuple(base[1]) == BASE_K
    print('  direct simulation: step %s, %s; expected step %d, %s -> %s' % (
        base[0] if base else None, base[1] if base else None, BASE_STEP, BASE_K, 'PASS' if okpos else 'FAIL'))
    h, P, T = BASE_K
    v = cp.inv_violations(h, P, T)
    Ls = cp.Lstar(P, T)
    print('  L* = %d; (a) h = %d, p_1 = %d >= 7, digits %s, far pair %s (p_L >= 1, q_L >= 6)' % (Ls, h, P[0][0], [d for _, _, d in P], P[-1]))
    print('  (b) q_1+1 = %d >= 5*2^3 = 40, q_2 = %d >= 20, q_3 = %d >= 10; (c) p_j + d_j = %s odd; (d) L* = %d >= 3; '
          '(e) p_1+1 = %d >= 2^6 = 64, p_2 = %d >= 2^4 = 16' % (
          P[0][1] + 1, P[1][1], P[2][1], [P[j][0] + P[j][2] for j in range(3)], Ls, P[0][0] + 1, P[1][0]))
    print('  INV+(e) (parent\'s inv_violations): %s' % (v or 'all clauses hold'))
    jb = jc.J(h, [list(x) for x in P], ('N',), ('E1', False))
    print('  Rocq invariant J (parent rocq/jcheck.py, ghost (E1, false)): %s' % (jb or 'holds'))
    diff = [(j + 1, a, b) for j, (a, b) in enumerate(zip(P, cp.BASE_K[1])) if a != b]
    print('  difference to the parent\'s base %s: %s (only the far pair\'s q)' % (cp.BASE_K, diff))
    a_s, a_k = ALT_BASE
    okalt = any(s == a_s and k == a_k for s, k in seq) and not cp.inv_violations(*a_k) and \
        jc.J(a_k[0], [list(x) for x in a_k[1]], ('N',), ('E1', False)) is None
    print('  option: the E-start after overflow 4, step %d, %s: on the orbit, INV+(e) and J hold -> %s' % (
        a_s, a_k, 'yes' if okalt else 'NO'))
    ok = okpos and not v and jb is None and diff == [(4, (1, 25, 1), (1, 24, 1))]
    print('  B:', 'PASS' if ok else 'FAIL')
    return ok

# ---------------------------------------------------------------- G: the parent's cycle-pair checker on the twin orbit
def section_G(lmax):
    print('== G. parent\'s cycle_pair_checked (proof.md 3.8 identities) on the twin orbit, base -> L* > %d' % lmax)
    st = cp.new_stats(); fails = []; K = BASE_K
    try:
        while cp.Lstar(K[1], K[2]) <= lmax and len(fails) < 20:
            K = cp.cycle_pair_checked(K, fails, st)
    except cp.Outside as e:
        fails.append('OUTSIDE %s' % e)
    for f in fails[:10]: print('  FAIL', f)
    print('  ' + cp.fmt_stats(st))
    ok = not fails
    print('  G:', 'PASS' if ok else 'FAIL')
    return ok

# ---------------------------------------------------------------- J: the Rocq invariant on the twin orbit
def section_J(ncyc):
    print('== J. parent\'s Rocq invariant J at every macro step of the twin orbit from the base, %d re-pairings' % ncyc)
    h, P, T = BASE_K
    res = jc.run(h, [list(x) for x in P], ('N',), ('E1', False), ncyc)
    ok = res[0] == 'OK'
    print('  %s %s; rules %s -> %s' % (res[0], res[1] or '', res[3], 'PASS' if ok else 'FAIL'))
    if not ok: print('  at', res[2])
    return ok

# ---------------------------------------------------------------- L: lockstep with the parent's abstract orbit (informational)
def section_L(lmax):
    print('== L. INFORMATIONAL: twin abstract orbit vs parent abstract orbit, in lockstep, to L > %d' % lmax)
    from collections import Counter
    A = cp.INIT_K; B = INIT_K; nmac = 0; where = Counter(); bad = None
    def app(K, m):
        h, P, T = K; V = cp.value(P); W = V - m
        return (h + 4*m, [(p + cp.touches(V, m, j), q - cp.touches(V, m, j), (W >> j) & 1) for j, (p, q, d) in enumerate(P)], T)
    def plus_one(a, b):
        """None if b = a except +1 on exactly one of p_L, q_L, the tail value; else the location name."""
        if a[0] != b[0] or len(a[1]) != len(b[1]) or (a[2] is None) != (b[2] is None): return 'shape'
        if a[2] is not None and a[2][0] != b[2][0]: return 'shape'
        d = [(j, c, y - x) for j, (u, v) in enumerate(zip(a[1], b[1])) for c, (x, y) in enumerate(zip(u, v)) if x != y]
        if a[2] is not None and a[2][1] != b[2][1]: d.append(('T', a[2][0], b[2][1] - a[2][1]))
        if len(d) != 1 or d[0][2] != 1: return 'diff %s' % d
        j, c, _ = d[0]
        if j == 'T': return c
        if j != len(a[1]) - 1 or c == 2: return 'diff %s' % d
        return 'pL' if c == 0 else 'qL'
    while len(A[1]) <= lmax:
        ba = cp.bulk(*A); bb = cp.bulk(*B)
        if ba and bb:
            m = min(ba[3], bb[3]); A = app(A, m); B = app(B, m); nmac += m
        else:
            ha, Pa, Ta, na = cp.astep(*A); hb, Pb, Tb, nb = cp.astep(*B); nmac += 1
            if na != nb: bad = 'rule sequences diverge: %s vs %s at %s / %s' % (na, nb, A, B); break
            A = (ha, Pa, Ta); B = (hb, Pb, Tb)
        loc = plus_one(A, B)
        if loc not in ('pL', 'qL', 'T1', 'T2'): bad = 'not a +1 on the far/tail block: %s at %s / %s' % (loc, A, B); break
        where[loc] += 1
    ok = bad is None
    print('  %s; macro steps ~2^%d; +1 location counts (per lockstep move): %s -> %s' % (
        'same rule at every macro step, states differ by exactly +1 on the far pair or the tail' if ok else bad,
        nmac.bit_length(), dict(where), 'PASS (informational)' if ok else 'FAIL (informational)'))
    # different orbits: no canonical twin configuration occurs among the parent's (direct simulation, both machines)
    N = 3*10**5
    par = {repr(k) for s, k in cp.stream_canonical(N)}
    tw = [(s, k) for s, k in stream_twin(N)]
    common = [(s, k) for s, k in tw if repr(k) in par]
    ok2 = not common
    print('  first %d steps: %d twin and %d parent canonical configurations, %d in common -> %s' % (
        N, len(tw), len(par), len(common), 'PASS (informational: different orbits)' if ok2 else 'FAIL %s' % common[:3]))
    return ok and ok2

def selftest():
    """Negative controls: each check is run on a deliberately wrong input and must FAIL."""
    import io, contextlib
    print('== N. negative controls (--selftest): every check must FAIL on a wrong input')
    g = globals()
    def run(patch, f, *a):
        old = {k: g[k] for k in patch}
        g.update(patch)
        try:
            with contextlib.redirect_stdout(io.StringIO()):
                r = f(*a)
        finally:
            g.update(old)
        return r[0] if isinstance(r, tuple) else r
    bad_map = dict(MI); bad_map[4], bad_map[5] = MI[5], MI[4]
    from_A = dict(MI); from_A[0] = 0
    skeptic = (2, [(7, 19, 0), (2, 10, 1), (1, 6, 1)], None)
    _, (b, seq) = section_CD_quiet(100000)
    cases = [
        ('M: map with E and F swapped', {'MI': bad_map}, section_M, ()),
        ('S: parent started in A instead of D', {'MI': from_A}, section_S, (5000,)),
        ('A: rules run on the parent\'s (unmirrored) table', {'TT': TP}, section_A, (1, random.Random(1))),
        ('C: expecting the parent\'s K0 = K(2;(11,11,0);-)', {'INIT_K': cp.INIT_K}, section_CD, (5000,)),
        ('B: expecting the parent\'s base at step 78,710', {'BASE_K': cp.BASE_K, 'BASE_STEP': 78710}, section_B, (b, seq)),
        ('G: from the skeptic start (violates (e))', {'BASE_K': skeptic}, section_G, (10,)),
        ('J: from the skeptic start', {'BASE_K': skeptic}, section_J, (4,)),
    ]
    ok = True
    for name, patch, f, a in cases:
        r = run(patch, f, *a)
        ok &= not r
        print('  %-55s -> %s' % (name, 'FAILS as it should' if not r else 'PASSES: the check is too weak'))
    print('  N:', 'PASS' if ok else 'FAIL')
    return ok

def section_CD_quiet(n):
    import io, contextlib
    with contextlib.redirect_stdout(io.StringIO()):
        return section_CD(n)

def pins():
    print('== pins: parent files used by this delta')
    okall = True
    for rel, want in PINS.items():
        try:
            got = hashlib.sha256(open(os.path.join(PDIR, rel), 'rb').read()).hexdigest()
        except OSError:
            got = None
        ok = got == want; okall &= ok
        print('  %-50s %s' % (rel, 'unchanged' if ok else 'WARN changed since the delta was written (%s)' % (got and got[:16])))
    return okall

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, help='section D direct-simulation steps (default 3e7; quick 2e5)')
    ap.add_argument('--sstep', type=int, default=None, help='section S lockstep steps (default 5e6; quick 2e5)')
    ap.add_argument('--lmax', type=int, default=None, help='section G: L* bound (default 300; quick 60)')
    ap.add_argument('--jcyc', type=int, default=None, help='section J: re-pairings (default 30; quick 16)')
    ap.add_argument('--llmax', type=int, default=None, help='section L: L bound (default 120; quick 40)')
    ap.add_argument('--selftest', action='store_true', help='also run the negative controls (section N)')
    a = ap.parse_args()
    rng = random.Random(a.seed)
    q = a.quick
    n = 12 if q else 45
    steps = a.steps or (2*10**5 if q else 3*10**7)
    sstep = a.sstep or (2*10**5 if q else 5*10**6)
    lmax = a.lmax or (60 if q else 300)
    jcyc = a.jcyc or (16 if q else 30)
    llmax = a.llmax or (40 if q else 120)
    pins()
    res = {}
    res['M'] = section_M()
    res['S'] = section_S(sstep)
    res['A'] = section_A(n, rng)
    okCD, (base, seq) = section_CD(steps)
    res['C+D'] = okCD
    res['B'] = section_B(base, seq)
    res['G'] = section_G(lmax)
    res['J'] = section_J(jcyc)
    infoL = section_L(llmax)
    if a.selftest: res['N'] = selftest()
    allok = all(res.values())
    print('SUMMARY: %s  (%s; L informational: %s)' % ('PASS' if allok else 'FAIL',
          ', '.join('%s %s' % (k, 'PASS' if v else 'FAIL') for k, v in res.items()), 'PASS' if infoL else 'FAIL'))
    sys.exit(0 if allok else 1)