#!/usr/bin/env python3
"""check_proof.py -- simulation evidence for proof.md of 1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB (machine #8).

Self-contained direct simulator on THIS table (pure Python; check 10 also builds the plain C simulator
scripts/check_direct_sim.c with cc).  Only check 9a/9d import the event-level macro model
scripts/deepen3_macro.py (round 3); the path algebra of proof.md section 5 is re-implemented here from the
closed forms, and check 10 tests it against direct simulation without any model in between.

  python3 -B check_proof.py [--seed S] [--quick] [--only 1,2,...] [--jobs 2]

Checks (each prints PASS/FAIL with counts):
  1 table      the only halting transition is B1; B is entered only by A0 (1RB) and F1 (1LB)
  2 windows    every window lemma of proof.md 2.1, PEN and PFN included, by an exact finite run that never reads
               outside its window (so it holds in every context); exact output word, exit state and step count.
               PEN/PFN are run on the bare 73-cell window P1 (and, as a sanity check, with each 2-cell right context)
  3 Inc_L      rule Inc_L: exhaustive small (N<=4 digits, all v<2^N-1, gaps 1..3, a 0..3, 6 left contexts)
               + random large; exact tape, the head never enters L before the end, steps 6a+6S+24j+7
  4 pause      Inc, P100, WX, P010, ZX, ZXN, ZXP1, ZXP2: inner record -> next inner record, exact whole tape and
               exact step formula (the step formula is the sum of the chain Inc_L [B1 Inc_L] END_X of proof.md 3)
  5 T(f)       all 16,384 L* fixed parts: the window run 'C> F(f)' (73 cells) exits LEFT (state E or F) without
               reading the end unit, except f = 1^15, which exits RIGHT in state C after 73 steps; and the finite
               facts (T1)-(T4) of proof.md 4.3 that lemma RB turns into TAILFRONT and L* closure: an F-exit leaves 00
               first, y = 0 forces sigma = F, the exit word (first token set to 01 after an F-exit) is F(f') for an
               f' with x' = 1, y' = 1 - y (N) or y' = y (S), and (y,z) -> (y',z') is a TAILFRONT arrow
  6 overflow   one overflow by direct simulation for every L* fixed part (m=3, random end bits), in normal context
               at (r,a,G) = (0,2,()) and (3,3,(9,)) and in pause context at (r,p,wall,G) = (0,1,1,()) and (2,4,2,(8,)):
               NO/PO or SILENT/SILENTP with the exact wall / lead form; the class equals the parity prediction of
               proof.md 4.3; the new RC parses as U^(2r'+H') W(f',e) with the r', H' of lemma RB; L* closed; end
               unit untouched (f != 1^15); TAILFRONT; plus 200 random pairs: PO/SILENTP give the same new RC as
               NO/SILENT
  7 endcarry   ENDCARRY exhaustive for every end unit with m <= 10 (normal and pause context) and random m <= 40
               (all j, incl. growth j = m) by direct simulation
  8 init       blank tape -> first configuration in family X that satisfies INV (step 92,299): exact parse,
               a = 121, G = (28,), r + H = 6, L*, m = 3, f = 11, M = 256, s = 55, kappa = 2; lists the earlier
               all-ones normal-mode records (outside X, or in X but outside INV)
  9 macro      (a) path closed forms S/P1/P1S/P3 vs the event-level macro model on random invariant states;
               (b) interval closure, exact integers, N = 8..400; (c) side conditions along every path, with the
               three-way slot rule (PO iff c <= w-1, WX iff c >= w+1, c = w never); (d) replay of deepen3_macro
               random runs and a DFS over all front-unit sequences (depth 48)
  10 direct    whole paths by plain direct simulation (C core scripts/check_direct_sim.c, no acceleration): build a
               configuration in X with INV from (N, k, kappa, G, f, s, tail), run the real machine to the next
               normal-mode all-ones inner record, parse it, and require INV there with exactly one predicted
               (path, M', s', kappa', f'). N = 8 exhaustive (all G, both kappa, every s of all three intervals);
               random N = 9..12 incl. interval end points, f = 1^15 and the tail 110111111111111 that forces
               ENDCARRY at PO#2; targeted ENDCARRY-at-PO#2; continuous chains; and the real orbit from the blank
               tape (records 92,299 / 1,006,516 / 14,514,329 / 114,113,163: paths P1, P1, S)

Checks 6, 7 and 10 use a pool of 2 worker processes (--jobs).
"""
import sys, os, random, re, itertools, argparse, json
HERE = os.path.dirname(os.path.abspath(__file__))
TM = "1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB"
ST = "ABCDEF"
TT = {}
for i, part in enumerate(TM.split("_")):
    for s in range(2):
        t = part[3 * s:3 * s + 3]
        TT[(ST[i], s)] = None if t == "---" else (int(t[0]), 1 if t[1] == "R" else -1, t[2])
# int-coded table for the fast simulator
NX = [[None, None] for _ in range(6)]
for (q, s), v in TT.items():
    NX[ST.index(q)][s] = None if v is None else (v[0], v[1], ST.index(v[2]))

RESULTS = []
def report(name, ok, detail):
    RESULTS.append((name, ok))
    print("%-10s %s  %s" % (name, "PASS" if ok else "FAIL", detail), flush=True)

POOL = None            # set in main: a fork pool of --jobs workers (at most 2 heavy processes, see the repo rules)
def pmap(fn, jobs, chunksize=16):
    """map fn over jobs (in order), with the worker pool when there is one"""
    if POOL is None: return [fn(j) for j in jobs]
    return POOL.map(fn, jobs, chunksize)

# ----------------------------------------------------------------------------------------------- simulator
class Sim:
    """Bytearray tape. pos = head index, st = state index, last = last move (+1/-1/0)."""
    def __init__(self, left, right, state="A", head_on="right", pad=1 << 16):
        self.off = pad + len(left)
        self.T = bytearray(2 * pad + len(left) + len(right) + 16)
        for i, c in enumerate(left + right): self.T[pad + i] = 1 if c == "1" else 0
        self.pos = self.off if head_on == "right" else self.off - 1
        self.st = ST.index(state); self.steps = 0; self.last = 0
    def step(self):
        tr = NX[self.st][self.T[self.pos]]
        if tr is None: return False
        w, mv, ns = tr
        self.T[self.pos] = w; self.pos += mv; self.st = ns; self.steps += 1; self.last = mv
        return True
    def cells(self, a, b):  # relative to off
        return "".join("1" if self.T[self.off + i] else "0" for i in range(a, b))
    def span(self):
        nz = [i for i in range(len(self.T)) if self.T[i]]
        if not nz: return self.pos - self.off, self.pos - self.off
        return min(nz[0], self.pos) - self.off, max(nz[-1], self.pos) - self.off
    def tape_str(self):
        lo, hi = self.span()
        return self.cells(lo, self.pos - self.off) + "|" + self.cells(self.pos - self.off, hi + 1)

def lead_at(T, k):
    q = 0
    while T[k] == 0 and T[k + 1] == 0 and T[k + 2] == 1: k += 3; q += 1
    return q if (T[k] == 0 and T[k + 1] == 0 and T[k + 2] == 0 and T[k + 4] == 1 and T[k + 5] == 0
                 and T[k + 6] == 0 and T[k + 7] == 0 and T[k + 8] == 1) else None

def is_ir(sim):
    """inner record: A reads a 0 it reached moving left, right side (001)^p 00 0b10001"""
    return sim.st == 0 and sim.last == -1 and sim.T[sim.pos] == 0 and lead_at(sim.T, sim.pos) is not None

def run_to_ir(left, right, cap=10 ** 7):
    s = Sim(left, right)
    while s.steps < cap:
        if s.steps > 0 and is_ir(s): return s
        if not s.step(): return None
    return None

def norm(l, r):
    return l.lstrip("0"), r.rstrip("0")

def ir_split(s):
    lo, hi = s.span()
    return s.cells(lo, s.pos - s.off).lstrip("0"), s.cells(s.pos - s.off, hi + 1).rstrip("0")

# ----------------------------------------------------------------------------------------------- notation
def digits(bits, gaps):
    out = "0%d10001" % bits[0]
    for b, g in zip(bits[1:], gaps): out += "100" * g + "0%d10001" % b
    return out
def bits_of(v, N): return [(v >> i) & 1 for i in range(N)]
FIXED = "0?0?0?10001" "0?0?10001" "0?1000?10001" "0?0?1000?10001" "0?1000?1000?1000?1000?10001"
def fill(t, bits):
    it = iter(bits); return "".join(next(it) if c == "?" else c for c in t)
def Wword(fb, eb): return fill(FIXED + "0?" * len(eb) + "01", fb + eb)
def RC(r, fb, eb):
    return "0110001100" * r + ("01100" if fb[1] == "1" else "") + Wword(fb, eb)
GAP2 = "0110001100100"          # the gap-2 digit with bit 1, followed by its gap (100)^2
def parse_rc(rc):
    """rc with its digit bits set (set_bits, as at the next overflow) -> (fixed bits, end bits, H, r) or None"""
    for m in range(0, 400):
        t = FIXED + "0?" * m + "01"; L = len(t)
        if len(rc) < L: return None
        w = rc[-L:]
        if not all(c == "?" or c == d for c, d in zip(t, w)): continue
        b = "".join(d for c, d in zip(t, w) if c == "?")
        mm = re.fullmatch(r"((?:0110001100)*)(01100)?", rc[:-L])
        if mm: return b[:15], b[15:], 1 if mm.group(2) else 0, len(mm.group(1)) // 10
    return None
def set_bits(s):
    """set every digit bit of the leading run of digits 0b10001 (100)^g (counter at its next overflow)"""
    s = list(s); pos = 0; n = len(s)
    while pos + 7 <= n and "".join(s[pos:pos + 7]) in ("0010001", "0110001"):
        s[pos + 1] = "1"; pos += 7
        while pos + 3 <= n and "".join(s[pos:pos + 3]) == "100": pos += 3
    return "".join(s)

# ----------------------------------------------------------------------------------------------- 1 table
def check_table():
    halts = [k for k, v in TT.items() if v is None]
    into_B = sorted(k[0] + str(k[1]) for k, v in TT.items() if v is not None and v[2] == "B")
    ok = halts == [("B", 1)] and into_B == ["A0", "F1"]
    report("1 table", ok, "halting transitions %s; B entered by %s" % (halts, into_B))

# ----------------------------------------------------------------------------------------------- 2 windows
def win(u, X, v, cap=100000):
    """Run u <X v (head on last cell of u) or u X> v (head on first cell of v) until the head leaves the window."""
    w = [int(c) for c in u + v]
    if X.startswith("<"): pos = len(u) - 1; st = X[1]
    else: pos = len(u); st = X[0]
    steps = 0
    while 0 <= pos < len(w) and steps < cap:
        tr = TT[(st, w[pos])]
        if tr is None: return ("HALT", steps)
        a, mv, st = tr; w[pos] = a; pos += mv; steps += 1
    s = "".join(map(str, w))
    if pos < 0: return ("<%s %s" % (st, s), steps)
    if pos >= len(w): return ("%s %s>" % (s, st), steps)
    return ("CAP", steps)

F1 = fill(FIXED, "1" * 15)
F1P = "1010100101010100101010010100101010100101001010100101001010010100101001010"   # C-image of F(1^15)
WINDOWS = [
    # name, u, X, v, expected result, steps                                   (proof.md 2.1)
    ("R2", "", "A>", "00", "10 C>", 2),
    ("R4", "", "C>", "100", "010 C>", 3),
    ("R6", "", "C>", "01", "10 C>", 2),
    ("R7", "", "C>", "00", "<E 01", 3),
    ("R3", "", "C>", "0110001", "1001010 C>", 7),
    ("R5", "", "C>", "0010001", "<E 0110001", 3),
    ("L1", "010", "<E", "", "<E 100", 3),
    ("L2", "1001010", "<E", "", "<E 0010001", 17),
    ("L3", "10", "<E", "", "<F 00", 2),
    ("L3F", "10", "<F", "", "<E 01", 2),
    ("L4", "100", "<F", "", "<F 001", 3),
    ("UE", "10010", "<E", "", "<F 00100", 5),
    ("UF", "10010", "<F", "00", "<E 0010001", 15),
    ("PE", "1001010010", "<E", "", "<E 0010001100", 20),
    ("PF", "1001010010", "<F", "00", "<F 001000010001", 20),
    # left ends (proof.md 3.2)
    ("END", "00", "<F", "", "<A 01", 2),
    ("B1", "01", "<F", "", "00 A>", 3),
    ("ENDZX", "010010100100", "<F", "", "<A 000100011001", 22),
    # overflow boundaries (proof.md 4.2)
    ("BN", "010010", "<F", "00", "<A 00010001", 16),
    ("BS", "1001010010010", "<E", "", "<E 0010001100100", 23),
    # ENDCARRY pieces (proof.md 4.4): CF1, and the two returns over the processed F(1^15) = P1 (73-cell windows:
    # the run never reads the cell right of P1, so the end unit to the right is untouched)
    ("CF1", "", "C>", F1, F1P + " C>", 73),
    ("PEN", F1P, "<E", "", "<E " + fill(FIXED, "100100010001010"), 133),
    ("PFN", F1P, "<F", "", "<F " + fill(FIXED, "010000100100101"), 123),
]
def check_windows():
    bad = []; n = 0
    for name, u, X, v, exp, k in WINDOWS:
        r, kk = win(u, X, v); n += 1
        if r != exp or kk != k: bad.append((name, r, kk, exp, k))
    # sanity: PEN / PFN with each 2-cell right context -- same run, context unchanged
    nctx = 0
    for ctx in ("00", "01", "10", "11"):
        for name, X, f in (("PEN", "<E", "100100010001010"), ("PFN", "<F", "010000100100101")):
            r, kk = win(F1P, X, ctx); nctx += 1
            if r != X + " " + fill(FIXED, f) + ctx: bad.append((name + "+" + ctx, r, kk))
    report("2 windows", not bad, "%d window lemmas exact (full output word, exit side and state, steps), incl. "
           "PEN P1 <E -> <E F(100100010001010) in 133 and PFN P1 <F -> <F F(010000100100101) in 123 on the bare "
           "73-cell window; %d PEN/PFN runs with a 2-cell right context leave it unchanged%s"
           % (n, nctx, "" if not bad else "  BAD %s" % bad[:3]))

# ----------------------------------------------------------------------------------------------- 3 Inc_L
LEFTS = ["", "1", "01", "1001", "100100101001", "0101001001001"]
def inc_l_case(L, a, bits, gaps, tail):
    N = len(bits); v = sum(b << i for i, b in enumerate(bits))
    if v + 1 >= 1 << N: return None
    j = 0
    while bits[j]: j += 1
    S = sum(gaps[:j])
    right = "001" * a + "00" + digits(bits, gaps) + tail
    s = Sim("1" + L, right)                 # a guard cell '1' left of L makes 'never enters L' observable
    target = s.off - 1
    while s.steps < 10 ** 6:
        if s.pos < s.off: break
        if not s.step(): return False
    want = "001" * a + "00" + digits(bits_of(v + 1, N), gaps) + tail
    got = s.cells(0, len(want))
    return (s.pos == target and ST[s.st] == "F" and got == want and s.cells(-len(L) - 1, 0) == "1" + L
            and s.steps == 6 * a + 6 * S + 24 * j + 7)
def check_inc(R, quick):
    n = 0; bad = []
    for N in range(1, 5):
        for gaps in itertools.product(range(1, 4), repeat=N - 1):
            for v in range(0, (1 << N) - 1):
                for a in range(0, 4):
                    for L in LEFTS:
                        r = inc_l_case(L, a, bits_of(v, N), list(gaps), "0110001100")
                        n += 1
                        if not r: bad.append((L, a, v, gaps))
    nr = 0
    for _ in range(100 if quick else 400):
        N = R.randint(1, 8); v = R.randrange(0, (1 << N) - 1); gaps = [R.randint(1, R.choice([5, 60, 300])) for _ in range(N - 1)]
        a = R.randint(0, R.choice([5, 60, 300])); L = "".join(R.choice("01") for _ in range(R.randint(0, 12)))
        r = inc_l_case(L, a, bits_of(v, N), gaps, "".join(R.choice("01") for _ in range(9)))
        nr += 1
        if not r: bad.append(("rnd", L, a, v, gaps))
    report("3 Inc_L", not bad, "exhaustive %d + random %d instances: exact tape, F on the last cell of L, L untouched, "
           "steps 6a+6S+24j+7%s" % (n, nr, "" if not bad else "  BAD %s" % bad[:3]))

# ----------------------------------------------------------------------------------------------- 4 pause rules
def rnd_Y(R):
    return R.choice(["", "100" * R.randint(1, 30) + "101001" + "010" * R.randint(3, 30) + "1001",
                     "100" * R.randint(1, 30) + "010" * R.randint(3, 30) + "1001", "100" * R.randint(1, 30)])
def pause_instances(R, n):
    """yield (name, wall, p, bits, gaps, expected (wall', p', bits', gaps'), expected steps or None)"""
    for _ in range(n):
        Nd = R.randint(1, 6); gaps = [R.randint(1, R.choice([3, 20, 60])) for _ in range(Nd - 1)]
        v = 2 * R.randrange(0, max(1, (1 << Nd) // 2 - 1)); bits = bits_of(v, Nd)
        if v + 2 >= 1 << Nd: continue
        p = R.randint(0, R.choice([4, 40, 200])); b2 = bits_of(v + 2, Nd)
        j2 = 0
        while bits_of(v + 1, Nd)[j2]: j2 += 1
        S2 = sum(gaps[:j2])
        nn = R.randint(0, R.choice([3, 30, 200]))
        st2 = 12 * p + 6 * S2 + 24 * j2 + 19; st3 = 12 * p + 6 * S2 + 24 * j2 + 39
        yield ("Inc", "", p, bits, gaps, ("", p + 1, bits_of(v + 1, Nd), gaps), 6 * p + 9)
        yield ("P100", "100" * (nn + 1) + "1", p, bits, gaps, ("100" * nn + "1", p + 1, b2, gaps), st2)
        yield ("WX", "1", p, bits, gaps, ("", p + 1, b2, gaps), st2)
        Y = rnd_Y(R); m = R.randint(0, 40)
        yield ("P010", Y + "010" * (m + 1) + "01", p, bits, gaps, (Y + "010" * m + "01", p + 1, b2, gaps), st2)
        h = R.randint(3, 40); Y = R.choice(["", "100" * R.randint(1, 30) + "101001", "100" * R.randint(1, 30)])
        yield ("ZX", Y + "010" * h + "100101", p, bits, gaps, (Y + "010" * (h - 3) + "01", 0, [0] + b2, [p + 2] + gaps), st3)
        nz = R.randint(2, 40)
        yield ("ZXN", "100" * nz + "10100101", p, bits, gaps, ("100" * (nz - 2) + "1", 0, [0] + b2, [p + 2] + gaps), st3)
        n3 = R.randint(3, 40)
        if v + 3 < 1 << Nd:
            yield ("ZXP1", "100" * n3 + "01", p, bits, gaps, ("100" * (n3 - 1) + "10", p + 1, b2, gaps), st2)
            yield ("ZXP2", "100" * (n3 - 1) + "10", p + 1, b2, gaps,
                   ("100" * (n3 - 3) + "1", 0, [0] + bits_of(v + 3, Nd), [p + 1] + gaps), 6 * (p + 1) + 23)
def check_pause(R, quick):
    tally = {}; bad = []
    tail = "0110001100" + "01100" + Wword("110000100100101", "000")    # a real-shaped RC (never reached here)
    insts = list(pause_instances(R, 40 if quick else 150))
    # exhaustive small: all walls of the listed shapes with tiny parameters and all v up to 2^3
    for Nd in (1, 2, 3):
        for gaps in itertools.product((1, 2), repeat=Nd - 1):
            for v in range(0, 1 << Nd, 2):
                for p in range(0, 3):
                    R2 = random.Random(v * 100 + p * 10 + Nd)
                    for x in pause_instances(R2, 1):
                        if x[3] == bits_of(v, Nd) or True: insts.append(x)
    for name, wall, p, bits, gaps, exp, st in insts:
        Nv = len(bits)
        if sum(b << i for i, b in enumerate(bits)) + (1 if name in ("Inc", "ZXP2") else 2) >= 1 << Nv: continue
        s = run_to_ir(wall, "001" * p + "00" + digits(bits, gaps) + tail)
        ok = s is not None
        if ok:
            got = ir_split(s); w2, p2, b2, g2 = exp
            want = norm(w2, "001" * p2 + "00" + digits(b2, g2) + tail)
            ok = got == want and (st is None or s.steps == st)
        t = tally.setdefault(name, [0, 0]); t[0] += 1; t[1] += ok
        if not ok and len(bad) < 4: bad.append((name, wall[-20:], p, bits, gaps, s and s.steps, st))
    allok = all(a == b for a, b in tally.values()) and len(tally) == 8
    report("4 pause", allok, " ".join("%s %d/%d" % (k, v[1], v[0]) for k, v in tally.items()) +
           "  (exact whole tape at the next inner record + exact steps)" + ("" if not bad else "  BAD %s" % bad))

# ----------------------------------------------------------------------------------------------- 5 T(f)
LSTAR = [b for b in range(1 << 15) if b & 1]          # x = 1
def fb_str(b): return "".join(str((b >> i) & 1) for i in range(15))
FU_NEXT = {("10", "e0"): "01", ("01", "e1"): "11", ("11", "e0"): "00", ("00", "e1"): "10", ("11", "S"): "10"}
def tf_facts(fb, sig, Fp):
    """The finite facts (T1)-(T4) of proof.md 4.3 for one fixed part f != 1^15 with x = 1, from its T(f) exit
    (state sig, exit word Fp).  Returns (class, f') or (None, reason)."""
    y = fb[1]
    if sig == "F" and not Fp.startswith("00"): return None, "T1: F-exit does not leave 00"
    if y == "0" and sig != "F": return None, "T2: y = 0 but sigma = E"
    Fq = "01" + Fp[2:] if sig == "F" else Fp            # lemma RB: after an F-exit the next UF / BN sets x to 1
    if len(Fq) != len(FIXED) or not all(c == "?" or c == d for c, d in zip(FIXED, Fq)): return None, "T3: not F(f')"
    f2 = "".join(d for c, d in zip(FIXED, Fq) if c == "?")
    cls = "S" if (y == "1" and sig == "F") else "N"     # lemma RB: N iff mu = F, mu = sigma flipped q = 2r + y times
    act = "S" if cls == "S" else "e%d" % (1 - int(y))   # lemma RB: emission 1 - H = 1 - y at N, 0 at S
    yy = y if cls == "S" else str(1 - int(y))           # lemma RB: H' = H at S, 1 - H at N; L* needs y' = H'
    if f2[0] != "1" or f2[1] != yy: return None, "T4: L* not closed"
    if FU_NEXT.get((fb[1:3], act)) != f2[1:3]: return None, "T4: not a TAILFRONT arrow"
    return cls, f2
def check_tf():
    TF = {}; cnt = {}; facts = {}; badf = []
    for b in LSTAR:
        fb = fb_str(b); r, k = win("", "C>", fill(FIXED, fb))
        if r.startswith("<"):
            key = (r[1], fb[1]); TF[fb] = (r[1], r.split()[1], k)
            cls, f2 = tf_facts(fb, r[1], r.split()[1])
            if cls is None: badf.append((fb, f2))
            else:
                kk = "%s-%s->%s" % (fb[1:3], cls if cls == "S" else "N,e%d" % (1 - int(fb[1])), f2[1:3])
                facts[kk] = facts.get(kk, 0) + 1
        else: key = ("RIGHT-" + r.split()[-1], fb[1]); TF[fb] = ("RIGHT", r.split()[0], k)
        cnt[key] = cnt.get(key, 0) + 1
    ok = (not badf and cnt.get(("RIGHT-C>", "1")) == 1 and TF["1" * 15] == ("RIGHT", F1P, 73)
          and sum(v for k, v in cnt.items() if not k[0].startswith("RIGHT")) == len(LSTAR) - 1)
    report("5 T(f)", ok, "16,384 L* fixed parts: window exits %s (window = the 73-cell fixed part only: the end "
           "unit is never read unless f = 1^15); facts (T1)-(T4) hold for all %d f != 1^15, giving %s%s"
           % (json.dumps({"%s,y=%s" % k: v for k, v in sorted(cnt.items())}), sum(facts.values()),
              json.dumps(dict(sorted(facts.items()))), "" if not badf else "  BAD %s" % badf[:3]))
    return TF

# ----------------------------------------------------------------------------------------------- 6 overflow
def overflow(left_wall, lead, G, r, fb, eb, pause):
    """One overflow from a normal-mode (pause=False: 0^inf A>(001)^lead 00 D(all 1) RC) or a pause-mode slot
    (pause=True: 0^inf (100)^w 1 A>(001)^lead 00 D(2^N-2) RC, wall given as left_wall = (100)^w 1).
    Returns (kind, new RC as found, H, steps) or (error,...)."""
    big = "".join("0110001" + "100" * g for g in G)
    D1 = big + GAP2 + "0110001100" * r + ("01100" if fb[1] == "1" else "")
    if pause: D1 = "0010001" + D1[7:] if D1 else D1      # b0 = 0 (v = 2^N - 2)
    rc = Wword(fb, eb)
    s = run_to_ir(left_wall, "001" * lead + "00" + D1 + rc)
    if s is None: return ("NOIR",)
    l, rr = ir_split(s)
    m = re.match(r"((?:001)*)00", rr); p = len(m.group(1)) // 3; rest = rr[m.end():]
    Gz = "".join("0010001" + "100" * g for g in G)
    if not pause:
        wallN = "100" * lead + "101001" + "".join("010" * (g + 1) + "1001" for g in G) + "01"
        if l == "" and p == lead + 1 and rest.startswith(Gz + "0010001100100"):
            return ("S", rest[len(Gz) + 13:], s.steps)
        if l == wallN and p == 0: return ("N", rest, s.steps)
        return ("X", l[-40:], p)
    w = left_wall
    n = (len(w) - 1) // 3
    wallN = "100" * n + "010" * (lead + 1) + "1001" + "".join("010" * (g + 1) + "1001" for g in G) + "01"
    if l == ("100" * (n - 1) + "1").lstrip("0") and p == lead + 1 and rest.startswith(Gz + "0010001100100"):
        return ("S", rest[len(Gz) + 13:], s.steps)
    if l == wallN and p == 0: return ("N", rest, s.steps)
    return ("X", l[-40:], p)
def _ovf_job(job):
    """worker: one overflow; returns (kind, parsed new RC or None)"""
    pause, r, lead, G, n, fb, eb = job
    res = overflow("100" * n + "1" if pause else "", lead, G, r, fb, eb, pause)
    if res[0] not in ("N", "S"): return (res[0], str(res[1:])[:120])
    return (res[0], parse_rc(set_bits(res[1])), res[1])
def check_overflow(R, TF, quick):
    stats = {"inputs": 0, "N": 0, "S": 0, "pred_ok": 0, "rb_ok": 0, "closed": 0, "endunit": 0, "tailfront": 0, "bad": []}
    # (pause, r, lead, G, wall n)
    sets = [(False, 0, 2, (), 0), (True, 0, 1, (), 1), (False, 3, 3, (9,), 0), (True, 2, 4, (8,), 2)]
    if quick: sets = sets[:2]
    jobs = []
    for pause, r, lead, G, n in sets:
        for b in LSTAR:
            fb = fb_str(b); eb = "".join(R.choice("01") for _ in range(3))
            if b == (1 << 15) - 1: eb = "010"
            jobs.append((pause, r, lead, G, n, fb, eb))
    ctx = {}
    for job, res in zip(jobs, pmap(_ovf_job, jobs, 64)):
        pause, r, lead, G, n, fb, eb = job; stats["inputs"] += 1
        c = ctx.setdefault("%s r=%d" % ("pause" if pause else "normal", r), [0, 0])
        if res[0] not in ("N", "S"):
            if len(stats["bad"]) < 3: stats["bad"].append(("kind", job, res))
            continue
        stats[res[0]] += 1; c[0 if res[0] == "N" else 1] += 1
        # parity prediction (proof.md 4.3): mu = sigma(f) flipped q = 2r + y times; N iff mu = F
        sig, _, _ = TF[fb]; q = 2 * r + int(fb[1])
        if sig != "RIGHT":
            mode = sig if q % 2 == 0 else ("E" if sig == "F" else "F")
            stats["pred_ok"] += ("N" if mode == "F" else "S") == res[0]
        else: stats["pred_ok"] += 1          # f = 1^15: ENDCARRY (check 7)
        pr = res[1]
        if pr is None:
            if len(stats["bad"]) < 3: stats["bad"].append(("shape", job, res[2][:60]))
            continue
        f2, e2, H2, r2 = pr
        # lemma RB: the restored block has q + 1 units after N (BN adds one), q units after S
        stats["rb_ok"] += 2 * r2 + H2 == (q + 1 if res[0] == "N" else q)
        stats["closed"] += f2[0] == "1" and H2 == int(f2[1])
        stats["endunit"] += e2 == eb or fb == "1" * 15
        e = (r2 + H2) - (r + int(fb[1]))
        fu, fu2 = fb[1:3], f2[1:3]; act = "S" if res[0] == "S" else "e%d" % e
        stats["tailfront"] += FU_NEXT.get((fu, act)) == fu2 and (res[0] == "N" or e == 0)
    # pause context: PO / SILENTP give the same new RC as NO / SILENT (random sample, random r, gaps, lead, wall)
    pjobs = []
    for _ in range(40 if quick else 200):
        fb = "1" + "".join(R.choice("01") for _ in range(14)); eb = "".join(R.choice("01") for _ in range(R.randint(0, 6)))
        r = R.randint(0, 5); G = tuple(R.randint(7, 40) for _ in range(R.choice([0, 1, 2]))); lead = R.randint(3, 40)
        n = R.randint(1, 30)
        pjobs.append((False, r, R.randint(2, 30), G, 0, fb, eb)); pjobs.append((True, r, lead, G, n, fb, eb))
    pres = pmap(_ovf_job, pjobs, 8); pc = [0, 0]
    for i in range(0, len(pjobs), 2):
        A, B = pres[i], pres[i + 1]
        pc[0] += 1; pc[1] += A[0] == B[0] and A[0] in ("N", "S") and A[2] == B[2]
    n = stats["inputs"]
    ok = (stats["pred_ok"] == n and stats["rb_ok"] == n and stats["closed"] == n and stats["endunit"] == n
          and stats["tailfront"] == n and not stats["bad"] and pc[0] == pc[1])
    report("6 overflow", ok, "%d overflows (%d N, %d S; N/S by context %s): class = parity prediction %d, "
           "2r'+H' as lemma RB %d, L* closed %d, end unit untouched %d, TAILFRONT %d; pause context (PO/SILENTP) "
           "same new RC as NO/SILENT %d/%d%s" % (n, stats["N"], stats["S"], json.dumps(ctx), stats["pred_ok"],
           stats["rb_ok"], stats["closed"], stats["endunit"], stats["tailfront"], pc[1], pc[0],
           "" if not stats["bad"] else "  BAD %s" % stats["bad"]))

# ----------------------------------------------------------------------------------------------- 7 ENDCARRY
def endcarry_want(e):
    """proof.md 4.4: (class, new end bits, new fixed bits, H') for the end bits e when f = 1^15"""
    m = len(e); j = 0
    while j < m and e[j] == "1": j += 1
    jj = j if j < m else m + 1; rest = e[j + 1:] if j < m else ""
    if jj % 2 == 0: want = ("N", "10" * (jj // 2) + "1" + rest, "100100010001010", 0)
    else: want = ("S", "01" * ((jj + 1) // 2) + rest, "110000100100101", 1)
    return want
def check_endcarry(R, quick):
    jobs = []
    # exhaustive: every end unit with m <= 10 (quick: m <= 7), normal context and pause context
    for pause in (False, True):
        for m in range(0, 8 if quick else 11):
            for b in range(1 << m):
                e = format(b, "0%db" % m) if m else ""
                jobs.append((pause, 1, 3, (9,), 2 if pause else 0, "1" * 15, e))
    nex = len(jobs)
    for _ in range(60 if quick else 300):
        m = R.randint(0, 40); r = R.randint(0, 8); a = R.randint(2, 30); pause = R.random() < 0.3
        G = tuple(R.randint(7, 30) for _ in range(R.choice([0, 1, 2])))
        j = R.choice([R.randint(0, m), m, max(0, m - 1), min(m, R.randint(0, 5))])
        e = "1" * j + ("0" + "".join(R.choice("01") for _ in range(m - j - 1)) if j < m else "")
        jobs.append((pause, r, a, G, R.randint(1, 30) if pause else 0, "1" * 15, e))
    t = [0, 0]; bad = []; tal = {}
    for job, res in zip(jobs, pmap(_ovf_job, jobs, 16)):
        pause, r, a, G, n, fb, e = job
        cls, we, wf, wH = endcarry_want(e)
        if len(we) == len(e) + 2: we = we[:-1]        # growth: the old end marker became a bit, a new 01 marker
        ok = res[0] == cls
        if ok:
            pr = res[1]
            ok = (pr is not None and pr[0] == wf and pr[1] == we and pr[2] == wH and (pr[3] + pr[2]) - (r + 1) == 0)
        t[0] += 1; t[1] += ok; k = "%s:%s" % ("pause" if pause else "normal", res[0]); tal[k] = tal.get(k, 0) + 1
        if not ok and len(bad) < 3: bad.append((job, res[:1]))
    report("7 endcarry", t[0] == t[1], "ENDCARRY %d/%d (%d exhaustive: every end unit with m <= %d, normal and pause "
           "context; %d random m <= 40, j incl. growth j = m) %s: j even -> N, end (10)^(j/2) 1 rest; j odd -> S, end "
           "(01)^((j+1)/2) rest; fixed bits 100100010001010/H'=0 or 110000100100101/H'=1; e0%s"
           % (t[1], t[0], nex, 7 if quick else 10, t[0] - nex, json.dumps(tal), "" if not bad else "  BAD %s" % bad))

# ----------------------------------------------------------------------------------------------- 8 init + real run
def macro_inv(a, G, R_):
    k = len(G); N = k + 1 + R_; M = 2 ** N
    Gam = sum((g - 1) << i for i, g in enumerate(G)); c = 2 ** (k + R_) - 2 ** (k + 1) - 2 * Gam - 4
    return M, a - c, c - M // 4
def body_digits(body):
    """leading digits 0b10001 (100)^g of a normal-mode body -> list of (bit, gap), end position"""
    out = []; pos = 0
    while True:
        mm = re.match(r"0([01])10001((?:100)*)", body[pos:])
        if not mm: break
        out.append((int(mm.group(1)), len(mm.group(2)) // 3)); pos += mm.end()
    return out, pos
def parse_family(a, body):
    """body right of the lead of an all-ones normal-mode configuration -> (a, G, r, H, (m, bits)) or None"""
    mm = re.fullmatch(r"((?:0110001(?:100){3,})*)0110001100100((?:0110001100)*)(01100)?(.*)", body)
    if not mm: return None
    G = tuple(len(x) // 3 for x in re.findall(r"0110001((?:100)+)", mm.group(1)))
    r = len(mm.group(2)) // 10; H = 1 if mm.group(3) else 0; W = mm.group(4)
    for m_ in range(0, 400):
        tt = FIXED + "0?" * m_ + "01"
        if len(tt) > len(W): return None
        if len(tt) == len(W) and all(c == "?" or c == d for c, d in zip(tt, W)):
            return a, G, r, H, (m_, "".join(d for c, d in zip(tt, W) if c == "?"))
    return None
def check_init(quick):
    """Run from the blank tape to the first normal-mode inner record that is a configuration of the family X
    (proof.md 1.3): all counter bits 1, large gaps >= 3, gap-2 digit, R block, W(f, e) in the template."""
    s = Sim("", ""); first = None; n_ir = 0; early = []
    while s.steps < 3_000_000:
        if s.steps > 0 and is_ir(s):
            lo, hi = s.span()
            if lo == s.pos - s.off:                         # normal mode: nothing left of the head
                n_ir += 1
                rr = s.cells(lo, hi + 1); m = re.match(r"((?:001)*)00", rr)
                body = rr[m.end():].rstrip("0") if m else ""
                dg, _ = body_digits(body)
                if m and len(dg) >= 2 and all(b for b, g in dg):
                    fam = parse_family(len(m.group(1)) // 3, body)
                    if fam is not None:
                        M_, s_, k_ = macro_inv(fam[0], fam[1], fam[2] + fam[3])
                        if fam[1] and k_ in (2, 8) and fam[4][1][1:3] == "11" and 24 <= s_ <= M_ // 4 + 2:
                            first = (s.steps, fam); break
                    early.append((s.steps, "X" if fam else "-"))
        if not s.step(): report("8 init", False, "HALT at %d" % s.steps); return
    if first is None: report("8 init", False, "no family configuration"); return
    steps, (a, G, r, H, t) = first
    M, sv, kap = macro_inv(a, G, r + H)
    ok = (t is not None and a == 121 and G == (28,) and r + H == 6 and t[0] == 3 and t[1][0] == "1"
          and H == int(t[1][1]) and t[1][1:3] == "11" and M == 256 and sv == 55 and kap == 2)
    report("8 init", ok, "blank -> first configuration in X and INV at step %d (normal-mode inner record no. %d; earlier "
           "all-ones normal-mode records (X = in family X but outside the invariant, - = not in X): %s): "
           "a=%d G=%s r=%d H=%d m=%s fixed=%s end=%s; M=%d s=%d kappa=%d (expected a=121, G=(28,), r+H=6, m=3, x=1, "
           "H=y, f=11, M=256, s=55, kappa=2)" % (steps, n_ir, early, a, G, r, H, t and t[0], t and t[1][:15], t and t[1][15:],
           M, sv, kap))

# ----------------------------------------------------------------------------------------------- 9 macro
def check_macro(R, quick):
    sys.path.insert(0, os.path.join(HERE, "scripts"))
    import deepen3_macro as DM
    PRED = {("S",): lambda M, s: (M, s + M, 2), ("e0", "e1"): lambda M, s: (4 * M, M + 10 - s, 2),
            ("e0", "e1", "S"): lambda M, s: (4 * M, 5 * M + 10 - s, 2),
            ("e0", "e1", "e0", "e1"): lambda M, s: (32 * M, 9 * M + 32 - s, 8)}
    def inv(f, M, s, kap):
        if kap not in (2, 8) or M < 256: return False
        if f == "11": return 24 <= s <= M // 4 + 2
        if f == "10": return 8 <= s <= M - 14 or M + 24 <= s <= 2 * M
        return False
    # (a) path closed forms vs event-level model, random runs (incl. S-heavy)
    tally = {"nslots": 0, "inv_ok": 0, "pred_ok": 0, "pred_bad": 0, "other": 0, "flags": 0, "trans": {}}
    for seed in range(20 if quick else 80):
        RR = random.Random(seed); q = RR.choice([0.1, 0.5, 0.9]); st = DM.START; fu = DM.START_FU; cur = None; path = []
        for i in range(300 if quick else 700):
            if st[0] == "N":
                _, a, G, NR = st; M, s, kap = macro_inv(a, G, NR)
                tally["nslots"] += 1; tally["inv_ok"] += inv(fu, M, s, kap)
                if cur is not None:
                    key = tuple(path); p = PRED.get(key); nm = "%s:%s" % (cur[0], "-".join(key))
                    tally["trans"][nm] = tally["trans"].get(nm, 0) + 1
                    if p is None: tally["other"] += 1
                    elif p(cur[1], cur[2]) == (M, s, kap): tally["pred_ok"] += 1
                    else: tally["pred_bad"] += 1
                cur = (fu, M, s); path = []
            opts = DM.FU_ACTS[fu]; act = opts[0] if len(opts) == 1 else ("S" if RR.random() < q else "e0")
            st2, f = DM.apply(st, act); fu = DM.FU_NEXT[(fu, act)]; path.append(act)
            if st2 is None or f: tally["flags"] += 1; break
            st = st2
    oka = tally["inv_ok"] == tally["nslots"] and tally["pred_bad"] == 0 and tally["other"] == 0 and tally["flags"] == 0
    # (b) interval closure, exact: images of the interval end points (all maps have slope +-1)
    badb = []
    for N in range(8, 401):
        M = 2 ** N
        cases = [("11", 24, M // 4 + 2, "S", lambda s: (M, s + M), "10"),
                 ("11", 24, M // 4 + 2, "P1", lambda s: (4 * M, M + 10 - s), "10"),
                 ("10", 8, M - 14, "P1", lambda s: (4 * M, M + 10 - s), "11"),
                 ("10", M + 24, 2 * M, "P1S", lambda s: (4 * M, 5 * M + 10 - s), "10"),
                 ("10", M + 24, 2 * M, "P3", lambda s: (32 * M, 9 * M + 32 - s), "10")]
        for f, lo, hi, nm, fn, f2 in cases:
            for s in (lo, hi):
                M2, s2 = fn(s)
                if f2 == "11": okk = 24 <= s2 <= M2 // 4 + 2
                else: okk = 8 <= s2 <= M2 - 14 or M2 + 24 <= s2 <= 2 * M2
                if not okk: badb.append((N, nm, s))
            # interval stays inside ONE target interval (images of both ends in the same piece)
            M2, a2 = fn(lo); _, b2 = fn(hi); l2, h2 = min(a2, b2), max(a2, b2)
            if f2 == "11": okk = 24 <= l2 and h2 <= M2 // 4 + 2
            else: okk = (8 <= l2 and h2 <= M2 - 14) or (M2 + 24 <= l2 and h2 <= 2 * M2)
            if not okk: badb.append((N, nm, "interval"))
    # (c) side conditions along each path, from the closed forms of proof.md 5.2, at both interval ends, N = 8..400
    #     (every quantity is linear in s, so the interval end points suffice).  slot(cyc, w): the pause has outer wall
    #     (100)^w 1 and the next overflow slot is cyc P100 cycles away: PO iff cyc <= w - 1, WX iff cyc >= w + 1,
    #     and cyc = w (bare wall '1' at the slot) is covered by no rule, so it must never occur.
    def slot(cyc, w): return "PO" if cyc <= w - 1 else ("WX" if cyc >= w + 1 else "NONE")
    badc = []
    def need(cond, tag):
        if not cond: badc.append(tag)
    for N in range(8, 401):
        M = 2 ** N
        for kap in (2, 8):
            c = M // 4 + kap
            for f, lo, hi in (("11", 24, M // 4 + 2), ("10", 8, M - 14), ("10", M + 24, 2 * M)):
                for s in (lo, hi):
                    t = (N, kap, f, s); a = s + c
                    need(a >= 2, ("NO a>=2",) + t)                                  # ZXN at the end of the NO rebuild
                    need(slot(c + 3, a - 2) == "PO", ("PO#1 slot",) + t)           # wall a-2 after ZXN, c' = c+3
                    w1 = a - 2 - (c + 3); need(w1 == s - 5 and w1 >= 3, ("PO#1 wall",) + t)
                    need(c + 3 >= 8, ("PO#1 p>=8 (new gap >= 7)",) + t)
                    w2 = w1 - 3                                                     # ZXP1 + ZXP2
                    if f == "11" or s <= M - 14:                                    # P1 (and S from 11)
                        need(slot(M + 2, w2) == "WX", ("P1 WX",) + t)
                        if f == "11": need(s + M >= M + 24, ("S",) + t)
                        continue
                    need(slot(M + 2, w2) == "PO", ("PO#2 slot",) + t)              # P1S / P3
                    w3 = w2 - (M + 2); need(w3 == s - M - 10 and w3 >= 14, ("PO#2 wall",) + t)
                    need(slot(2 * M - 1, w3 - 1) == "WX", ("P1S WX after SILENTP",) + t)   # SILENTP: wall -1, value 0
                    w4 = w3 - 3; need(slot(8, w4) == "PO", ("PO#3 slot",) + t)     # e0 at PO#2: new gap M+1
                    w5 = w4 - 8; need(w5 == s - M - 21 and w5 >= 3, ("PO#3 wall",) + t)
                    need(slot(8 * M + 8, w5 - 3) == "WX", ("P3 WX",) + t)          # PO#3: new gap 7
    # (d) deepen3_macro random runs (front-unit language) + DFS
    agg = {"seeds": 0, "clean": 0}
    for seed in range(40 if quick else 200):
        RR = random.Random(10_000 + seed); st = DM.START; fu = DM.START_FU; clean = True
        for i in range(400 if quick else 1500):
            opts = DM.FU_ACTS[fu]; act = opts[0] if len(opts) == 1 else ("S" if RR.random() < 0.3 else "e0")
            st2, f = DM.apply(st, act); fu = DM.FU_NEXT[(fu, act)]
            if f: clean = False; break
            st = st2
        agg["seeds"] += 1; agg["clean"] += clean
    depth = 24 if quick else 48
    stack = [(DM.START, DM.START_FU, 0)]; nodes = 0; flags = 0; leaves = 0
    while stack:
        st, fu, d = stack.pop(); nodes += 1
        if d == depth: leaves += 1; continue
        for act in DM.FU_ACTS[fu]:
            st2, f = DM.apply(st, act)
            if f: flags += 1
            if st2 is None: continue
            stack.append((st2, DM.FU_NEXT[(fu, act)], d + 1))
    ok = oka and not badb and not badc and agg["seeds"] == agg["clean"] and flags == 0
    report("9 macro", ok, "(a) %d normal-mode overflows, invariant %d, path closed forms %d ok / %d bad / %d other, "
           "transitions %s; (b) interval closure N=8..400 %s; (c) side conditions %s; (d) %d/%d random runs clean, "
           "DFS depth %d: %d leaves, %d nodes, %d flags" % (tally["nslots"], tally["inv_ok"], tally["pred_ok"],
           tally["pred_bad"], tally["other"], json.dumps(tally["trans"]), "ok" if not badb else badb[:3],
           "ok" if not badc else badc[:3], agg["clean"], agg["seeds"], depth, leaves, nodes, flags))

# ----------------------------------------------------------------------------------------------- 10 direct paths
_DLIB = None
def dlib():
    """build (if needed) and load the plain C simulator scripts/check_direct_sim.c"""
    global _DLIB
    if _DLIB is None:
        import ctypes, subprocess
        src = os.path.join(HERE, "scripts", "check_direct_sim.c"); so = os.path.join(HERE, "work", "check_direct_sim.so")
        if not os.path.exists(so) or os.path.getmtime(so) < os.path.getmtime(src):
            tmp = so + ".%d" % os.getpid()
            subprocess.check_call(["cc", "-O2", "-shared", "-fPIC", "-o", tmp, src]); os.replace(tmp, so)
        L = ctypes.CDLL(so); L.run.restype = ctypes.c_int
        P = ctypes.POINTER
        L.run.argtypes = [ctypes.c_void_p, ctypes.c_long, P(ctypes.c_long), P(ctypes.c_int), P(ctypes.c_int),
                          ctypes.c_longlong, ctypes.c_int, P(ctypes.c_longlong)]
        _DLIB = L
    return _DLIB
class CTape:
    """tape for the C core; grows (re-centres) when the head reaches a border"""
    def __init__(self, right):
        n = len(right); pad = max(1 << 14, 4 * n)
        self.T = bytearray(2 * pad + n); self.T[pad:pad + n] = right.encode().translate(bytes.maketrans(b"01", b"\x00\x01"))
        self.pos = pad; self.st = 0; self.lastmv = 0; self.steps = 0
    def regrow(self):
        lo = self.T.find(1); hi = self.T.rfind(1)
        lo = self.pos if lo < 0 else min(lo, self.pos); hi = self.pos if hi < 0 else max(hi, self.pos)
        core = self.T[lo:hi + 1]; pad = max(1 << 14, 2 * len(core))
        self.T = bytearray(pad) + core + bytearray(pad); self.pos = pad + (self.pos - lo)
    def run(self, cap, mode):
        import ctypes
        L = dlib()
        while True:
            buf = (ctypes.c_uint8 * len(self.T)).from_buffer(self.T)
            p = ctypes.c_long(self.pos); st = ctypes.c_int(self.st); lm = ctypes.c_int(self.lastmv); n = ctypes.c_longlong(0)
            rc = L.run(ctypes.addressof(buf), len(self.T), ctypes.byref(p), ctypes.byref(st), ctypes.byref(lm),
                       cap - self.steps, mode, ctypes.byref(n))
            del buf
            self.pos = p.value; self.st = st.value; self.lastmv = lm.value; self.steps += n.value
            if rc == 3: self.regrow(); continue
            return rc
    def split(self):
        lo = self.T.find(1); hi = self.T.rfind(1)
        lo = min(lo, self.pos); hi = max(hi, self.pos); tr = bytes.maketrans(b"\x00\x01", b"01")
        return (bytes(self.T[lo:self.pos]).translate(tr).decode().lstrip("0"),
                bytes(self.T[self.pos:hi + 1]).translate(tr).decode().rstrip("0"))

def X_word(a, G, r, H, f, e):
    """proof.md 1.3: (001)^a 00 [0110001 Z^g]_i 0110001 Z^2 U^(2r+H) W(f, e)"""
    return "001" * a + "00" + "".join("0110001" + "100" * g for g in G) + GAP2 + "01100" * (2 * r + H) + Wword(f, e)
def quantities(a, G, R_, f):
    M, s_, kap = macro_inv(a, G, R_)
    return M, s_, kap, f[1:3]
def INV_ok(a, G, r, H, f):
    """INV of proof.md 5.3 (with M >= 256) at a configuration X(a; G; r, H; f, e)"""
    M, s_, kap, fu = quantities(a, G, r + H, f)
    if kap not in (2, 8) or M < 256 or any(g < 7 for g in G) or f[0] != "1" or int(f[1]) != H: return False
    if fu == "11": return 24 <= s_ <= M // 4 + 2
    if fu == "10": return 8 <= s_ <= M - 14 or M + 24 <= s_ <= 2 * M
    return False
def predict_paths(fu, M, s_, kap):
    """proof.md 5.2 / 5.3: the possible (path, M', s', kappa', f') from a configuration in INV"""
    out = []
    if fu == "11": out += [("S", M, s_ + M, kap, "10"), ("P1", 4 * M, M + 10 - s_, 2, "10")]
    if fu == "10":
        if 8 <= s_ <= M - 14: out.append(("P1", 4 * M, M + 10 - s_, 2, "11"))
        if M + 24 <= s_ <= 2 * M: out += [("P1S", 4 * M, 5 * M + 10 - s_, 2, "10"), ("P3", 32 * M, 9 * M + 32 - s_, 8, "10")]
    return out
def G_options(N, k, kap):
    """all large-gap tuples G (g_i >= 7, k of them) with c = M/4 + kappa, i.e. Gamma = 2^(N-3) - 2^k - 2 - kappa/2"""
    R_ = N - k - 1
    if R_ < 1: return []
    Gam = 2 ** (N - 3) - 2 ** k - 2 - kap // 2; E = Gam - 6 * (2 ** k - 1)
    if E < 0: return []
    if k == 0: return [()] if E == 0 else []
    out = []
    def rec(i, E, acc):          # choose g_i - 7 for i = k..2 (weight 2^(i-1)); g_1 takes the rest
        if i == 1: out.append(tuple([7 + E] + acc)); return
        w = 2 ** (i - 1)
        for x in range(E // w + 1): rec(i - 1, E - x * w, [7 + x] + acc)
    rec(k, E, []); return out
def parse_record(R_side):
    """right side at a normal-mode all-ones record -> (a, G, r, H, f, e) or None (family X, proof.md 1.3)"""
    m = re.match(r"((?:001)*)00", R_side)
    if not m: return None
    fam = parse_family(len(m.group(1)) // 3, R_side[m.end():])
    if fam is None: return None
    a, G, r, H, (mm, bits) = fam
    return a, G, r, H, bits[:15], bits[15:]
def _path_job(job):
    """worker: one path by direct simulation from X(a; G; r, H; f, e) in INV -> (ok, path or reason, steps)"""
    a, G, r, H, f, e = job
    M, s_, kap, fu = quantities(a, G, r + H, f)
    t = CTape(X_word(a, G, r, H, f, e)); rc = t.run(1 << 62, 1)
    if rc != 2: return (False, "rc%d" % rc, t.steps)
    L, Rs = t.split()
    if L != "": return (False, "not normal mode", t.steps)
    y = parse_record(Rs)
    if y is None: return (False, "not in X", t.steps)
    if not INV_ok(*y[:5]): return (False, "not in INV", t.steps)
    M2, s2, k2, fu2 = quantities(y[0], y[1], y[2] + y[3], y[4])
    hit = [p[0] for p in predict_paths(fu, M, s_, kap) if p[1:] == (M2, s2, k2, fu2)]
    return (len(hit) == 1, hit[0] if len(hit) == 1 else "no predicted path %s" % ((M2, s2, k2, fu2),), t.steps)
def make_start(N, k, kap, G, fu, s_, R, tail=None, e=None):
    """X configuration in INV with the given parameters (H = y = 1 since both front units 10 and 11 have y = 1)"""
    M = 2 ** N; c = M // 4 + kap; a = s_ + c; r = N - k - 2
    f = "1" + fu + (tail if tail is not None else "".join(R.choice("01") for _ in range(12)))
    if e is None: e = "".join(R.choice("01") for _ in range(R.randint(0, 10)))
    x = (a, tuple(G), r, 1, f, e)
    assert quantities(a, G, r + 1, f)[:3] == (M, s_, kap) and INV_ok(*x[:5]), x
    return x
def _chain_job(job):
    """worker: continuous direct simulation through successive normal-mode overflows while N <= Nmax"""
    x, Nmax = job
    a, G, r, H, f, e = x
    t = CTape(X_word(*x)); seq = []
    while len(G) + 1 + r + H <= Nmax:
        M, s_, kap, fu = quantities(a, G, r + H, f)
        t.lastmv = 0; rc = t.run(1 << 62, 1)                 # lastmv = 0: the current record does not count
        if rc != 2: return (False, seq + ["rc%d" % rc], t.steps)
        L, Rs = t.split(); y = parse_record(Rs)
        if L != "" or y is None or not INV_ok(*y[:5]): return (False, seq + ["left INV"], t.steps)
        M2, s2, k2, fu2 = quantities(y[0], y[1], y[2] + y[3], y[4])
        hit = [p[0] for p in predict_paths(fu, M, s_, kap) if p[1:] == (M2, s2, k2, fu2)]
        if len(hit) != 1: return (False, seq + ["unpredicted"], t.steps)
        seq.append(hit[0]); a, G, r, H, f, e = y
    return (True, seq, t.steps)
def check_direct(R, quick):
    out = {}; bad = []
    def run(tag, jobs, fn=_path_job, chunk=4):
        res = pmap(fn, jobs, chunk); tal = {}; ok = 0; steps = 0
        for job, rr in zip(jobs, res):
            ok += rr[0]; steps += rr[2]
            if fn is _path_job: key = "%s:%s" % (job[4][1:3], rr[1] if rr[0] else "BAD")
            else: key = " ".join(rr[1]) if rr[0] else "BAD"
            tal[key] = tal.get(key, 0) + 1
            if not rr[0] and len(bad) < 4: bad.append((tag, job if fn is _path_job else job[0], rr[1]))
        out[tag] = (ok, len(jobs), tal, steps)
        return res
    # (a) N = 8 exhaustive: all (k, kappa, G) and every s of the three intervals (quick: every 8th s)
    jobs = []
    N = 8; M = 2 ** N
    for k in range(N):
        for kap in (2, 8):
            for G in G_options(N, k, kap):
                for fu, lo, hi in (("11", 24, M // 4 + 2), ("10", 8, M - 14), ("10", M + 24, 2 * M)):
                    for s_ in range(lo, hi + 1, 8 if quick else 1):
                        tail = "1" * 12 if (fu == "11" and R.random() < 0.05) else None
                        jobs.append(make_start(N, k, kap, G, fu, s_, R, tail))
    run("N=8 exhaustive" if not quick else "N=8 every 8th s", jobs)
    # (b) random N = 9..12: end points, random G (random / max / min spread), special tails
    SPECIAL = {"11": "1" * 12, "10": "1" * 12}      # f = 1^15 (ENDCARRY at the NO), 110111111111111 (ENDCARRY at PO#2)
    plan = [(9, 30), (10, 16), (11, 8), (12, 4)] if quick else [(9, 100), (10, 50), (11, 16), (12, 6)]
    jobs = []
    for N, cnt in plan:
        M = 2 ** N; feas = [(k, kap) for k in range(N) for kap in (2, 8) if G_options(N, k, kap)]
        for _ in range(cnt):
            k, kap = R.choice(feas); Gs = G_options(N, k, kap)
            G = R.choice([Gs[0], Gs[-1], R.choice(Gs)])
            fu, lo, hi = R.choice([("11", 24, M // 4 + 2), ("10", 8, M - 14), ("10", M + 24, 2 * M)])
            s_ = R.choice([lo, hi, lo + 1, hi - 1, R.randint(lo, hi), R.randint(lo, hi)])
            tail = e = None
            if R.random() < 0.35:
                tail = SPECIAL[fu]; m = R.randint(0, 12); e = "".join(R.choice("01") for _ in range(m))
                if R.random() < 0.4:
                    j = R.randint(0, m); e = "1" * j + ("0" + e[j + 1:] if j < m else "")
            jobs.append(make_start(N, k, kap, G, fu, s_, R, tail, e))
    run("random N=9..12", jobs)
    # (c) ENDCARRY at PO#2: front unit 10 with the preimage tail 110111111111111 (after e0, e1 it is 1^15), s in the
    #     upper interval, every j parity incl. growth
    f = "110111111111111"                                    # T(f) table: two N overflows take it to 1^15
    for _ in range(2):
        r_, _k = win("", "C>", fill(FIXED, f)); f = tf_facts(f, r_[1], r_.split()[1])[1]
    if f != "1" * 15: bad.append(("ENDCARRY preimage", f))
    jobs = []
    for N in ((8,) if quick else (8, 9)):
        M = 2 ** N; feas = [(k, kap) for k in range(N) for kap in (2, 8) if G_options(N, k, kap)]
        for e in ["", "0", "1", "11", "111", "10", "110", "1110", "0101", "11111", "111110", "1111111"]:
            for s_ in (M + 24, 2 * M, R.randint(M + 24, 2 * M)):
                k, kap = R.choice(feas); G = R.choice(G_options(N, k, kap))
                jobs.append(make_start(N, k, kap, G, "10", s_, R, "111111111111", e))
    run("ENDCARRY at PO#2", jobs)
    # (d) continuous chains from N = 8 (one simulation through several paths, N <= Nmax)
    cj = []
    for _ in range(2 if quick else 6):
        N = 8; M = 2 ** N; feas = [(k, kap) for k in range(N) for kap in (2, 8) if G_options(N, k, kap)]
        k, kap = R.choice(feas); G = R.choice(G_options(N, k, kap))
        fu, lo, hi = R.choice([("11", 24, M // 4 + 2), ("10", 8, M - 14), ("10", M + 24, 2 * M)])
        cj.append((make_start(N, k, kap, G, fu, R.randint(lo, hi), R), 11 if quick else 12))
    run("chains", cj, _chain_job, 1)
    # (e) the real orbit: blank tape, the first normal-mode all-ones records in X with INV and the paths between them
    t = CTape(""); recs = []; okr = True
    while len(recs) < 4 and t.steps < 3 * 10 ** 8:
        rc = t.run(3 * 10 ** 8, 1)
        if rc != 2: okr = False; break
        L, Rs = t.split(); y = parse_record(Rs)
        if L == "" and y is not None and INV_ok(*y[:5]): recs.append((t.steps, y))
        elif recs: okr = False; break                      # after the first INV record every record must be in INV
        t.lastmv = 0                                         # move on past this record
    paths = []
    for (s1, x), (s2, y) in zip(recs, recs[1:]):
        M, s_, kap, fu = quantities(x[0], x[1], x[2] + x[3], x[4]); M2, s2_, k2, fu2 = quantities(y[0], y[1], y[2] + y[3], y[4])
        hit = [p[0] for p in predict_paths(fu, M, s_, kap) if p[1:] == (M2, s2_, k2, fu2)]
        paths.append(hit[0] if len(hit) == 1 else "BAD")
    okr = okr and [s for s, _ in recs] == [92299, 1006516, 14514329, 114113163] and paths == ["P1", "P1", "S"]
    out["real orbit"] = (int(okr), 1, {"records": [s for s, _ in recs], "paths": paths}, recs[-1][0] if recs else 0)
    ok = all(v[0] == v[1] for v in out.values()) and not bad
    report("10 direct", ok, "; ".join("%s %d/%d %s (%.3g steps)" % (k, v[0], v[1], json.dumps(v[2]), v[3])
                                      for k, v in out.items()) + ("" if not bad else "  BAD %s" % bad))

# ----------------------------------------------------------------------------------------------- main
if __name__ == "__main__":
    ap = argparse.ArgumentParser(); ap.add_argument("--seed", type=int, default=8); ap.add_argument("--quick", action="store_true")
    ap.add_argument("--only", default="")
    ap.add_argument("--jobs", type=int, default=2)
    A = ap.parse_args(); R = random.Random(A.seed)
    if A.jobs > 1:
        import multiprocessing
        POOL = multiprocessing.get_context("fork").Pool(min(A.jobs, 2))
    only = set(A.only.split(",")) if A.only else None
    def want(k): return only is None or k in only
    if want("1"): check_table()
    if want("2"): check_windows()
    if want("3"): check_inc(R, A.quick)
    if want("4"): check_pause(R, A.quick)
    TF = check_tf() if (want("5") or want("6")) else None
    if want("6"): check_overflow(R, TF, A.quick)
    if want("7"): check_endcarry(R, A.quick)
    if want("8"): check_init(A.quick)
    if want("9"): check_macro(R, A.quick)
    if want("10"): check_direct(R, A.quick)
    nf = sum(1 for _, ok in RESULTS if not ok)
    print("ALL PASS" if nf == 0 else "%d FAIL" % nf)
    sys.exit(0 if nf == 0 else 1)