#!/usr/bin/env python3
"""Simulation checks for proof.md of 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- (pilot #2).

Every check prints `name: passed/total` (or a count) and the run ends with ALL PASS or a list of failures.
Simulation is evidence, not proof: these checks test the statements of proof.md on random and
exhaustive instances against the real machine (pass-level and configuration-level simulation).

Notation (as in proof.md). Digits L=110, 0=000, 1=100 (cells, left to right); <r> = r's cells.
S(r) := 0^inf 11 D> <r> 0^inf.
Passes over a right part that starts at cell o (nothing left of the exit cell is ever read):
  h  : start `B>` at cell o,                       exit `<C` with the head on cell o-1;  part still starts at o.
  h' : start `1 D>` with the 1 at o-1, D at o,     exit `<C` with the head on cell o-2; part now starts at o-1.
R(tp,k,r) (busycoq RIncs): hx = passes [h'] + h^k over <r>;  h1 = passes h^k over `1 <r>`.

Run:   python3 -B check_proof.py            (default, ~10 s; from-blank part to 1e8 steps)
       python3 -B check_proof.py --full     (from blank to 2e9 steps, bigger samples, plus the Rocq check)
       python3 -B check_proof.py --rocq     (only the Rocq check, ~5 s)

The Rocq check (`--rocq`, also run by `--full`) is not simulation. It compiles ROCQ_SPEC below with Coq 8.20.1
(opam switch bb6) against the unmodified vendor/busycoq/verify. That file states proof.md's Inc and R (all 12
clauses) for the real machine string and proves Inc_spec, the two new segment facts, RIncs_spec (proof.md 3.1),
BigStep (3.2) and the initial segment c0 ->* S(1) (4). Each `Print Assumptions` must be closed. It does not
contain RIncs_nxt' (3.3) or nonhalt; those are still informal.
"""
import itertools
import os
import random
import re
import subprocess
import sys
import tempfile
from collections import Counter

sys.path.insert(0, "[local working file]")
sys.path.insert(0, "[local working file]")
import sim  # noqa: E402
import check_rules  # noqa: E402  (read-only reuse: l_entry, low_level)

TM = "1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---"
TM7 = "1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---"   # SOMDCv6.v Module TM7: same except A1 = 0RC
INV = {"L": "110", "0": "000", "1": "100"}
DIG = {v: k for k, v in INV.items()}
FULL = "--full" in sys.argv
ROCQ_ONLY = "--rocq" in sys.argv
ROOT = "[local working file]"
FAILS = []


def report(name, ok, tot, extra=""):
    print(f"{name}: {ok}/{tot}{('  ' + extra) if extra else ''}")
    if ok != tot:
        FAILS.append(name)


# ---------------------------------------------------------------- abstract relation (proof.md section 2)
def add(r, i, p):
    """Add p to the little-endian binary number formed by the 0/1 digits of r[i:] (L skipped), in place."""
    carry, j = p, i
    while carry and j < len(r):
        if r[j] != "L":
            t = (r[j] == "1") + carry
            r[j] = "1" if t % 2 else "0"
            carry = t // 2
        j += 1
    while carry:
        r.append("1" if carry % 2 else "0")
        carry //= 2


def inc(x):
    r = list(x)
    add(r, 0, 1)
    return "".join(r)


def R(tp, k, r0, ours=True, zero_clauses=True):
    """The relation R(tp,k,r,r') as a partial function: returns (r', clause counts) or None.
    ours=False gives SOMDCv6 TM7's RIncs (no +1 in X1/C1); zero_clauses=False drops Z0/Z1."""
    r, out, i, p, cnt = list(r0), [], 0, 0, Counter()
    while True:
        if p and (i == len(r) or r[i] != "L"):     # pending +1s; L digits are never changed by +1
            add(r, i, p)
            p = 0
        if i == len(r):
            if tp == "x":
                return None                        # hx at the right end: no clause
            while True:                            # R0/R1/R2: write k at the right end
                if k == 0:
                    out.append("1"); cnt["R0"] += 1
                    return "".join(out), cnt
                if k % 2:
                    out.append("0"); cnt["R1"] += 1; k = (k - 1) // 2
                else:
                    out.append("1"); cnt["R2"] += 1; k = (k - 2) // 2
        d = r[i]
        i += 1
        if tp == "x":
            out.append("L")
            if d == "L":
                cnt["X1"] += 1; k += 1; p += ours
            elif d == "0":
                cnt["X2"] += 1; k += 1
            else:
                cnt["X3"] += 1; tp = "1"
        else:
            if k == 0:
                if zero_clauses and i == len(r) and d != "L":   # Z1: [1] -> [L], Z0: [0] -> [1]
                    cnt["Z1" if d == "1" else "Z0"] += 1
                    out.append("L" if d == "1" else "1")
                    return "".join(out), cnt
                return None
            if d == "L":
                cnt["C1"] += 1; out.append("L"); tp = "x"; p += ours
            elif d == "1":
                cnt["C2"] += 1; out.append("L"); k -= 1
            elif k % 2:
                cnt["C3"] += 1; out.append("0"); k = (k - 1) // 2
            else:
                cnt["C4"] += 1; out.append("1"); k = (k - 2) // 2


def Rw(tp, k, r, **kw):
    x = R(tp, k, r, **kw)
    return None if x is None else x[0]


def sweep(r, **kw):
    return Rw("x", 0, r, **kw)


# ---------------------------------------------------------------- machine-level simulation
def table(tm):
    T = {}
    for qi, part in enumerate(tm.split("_")):
        for s in range(2):
            t = part[3 * s:3 * s + 3]
            T[("ABCDEF"[qi], s)] = None if t[2] == "-" else (int(t[0]), 1 if t[1] == "R" else -1, t[2])
    return T


TAB = {TM: table(TM), TM7: table(TM7)}


def cells(r):
    return "".join(INV[d] for d in r)


def put(tape, o, s):
    for j, ch in enumerate(s):
        tape[o + j] = int(ch)


def read_side(tape, o):
    hi = max([c for c, v in tape.items() if v] + [o - 1])
    s = "".join(str(tape.get(c, 0)) for c in range(o, hi + 1))
    s += "0" * ((-len(s)) % 3)
    w = "".join(DIG.get(s[i:i + 3], "?") for i in range(0, len(s), 3))
    return w


class Run:
    def __init__(self, tm):
        self.T, self.steps, self.a1, self.fread = TAB[tm], 0, 0, Counter()

    def go(self, tape, pos, q, stop, cap=10 ** 7):
        """Run until the head first stands on cell `stop`. Returns (state, pos) or raises."""
        for _ in range(cap):
            if pos == stop:
                return q
            s = tape.get(pos, 0)
            if q == "A" and s == 1:
                self.a1 += 1
            if q == "F":
                self.fread[s] += 1
            tr = self.T[(q, s)]
            if tr is None:
                raise RuntimeError("HALT")
            w, mv, q = tr
            tape[pos] = w
            pos += mv
            self.steps += 1
        raise RuntimeError("TIMEOUT")


def passes(tm, tp, k, r):
    """Simulate the pass list of R(tp,k,r) on the real machine; return (word read back, Run)."""
    tape, run, o = {}, Run(tm), 0
    if tp == "x":
        put(tape, 0, cells(r))
        tape[-1] = 1                               # h': `1 D>`, the 1 belongs to the pass
        if run.go(tape, 0, "D", -2) != "C":
            raise RuntimeError("h' exit state")
        o = -1
    else:
        tape[0] = 1                                # h1: the extra cell `1 <r>`
        put(tape, 1, cells(r))
    for _ in range(k):
        if run.go(tape, o, "B", o - 1) != "C":
            raise RuntimeError("h exit state")
    return read_side(tape, o), run


def sweep_tm(tm, r):
    """Real machine from S(r) (11 at cells -2,-1; D at 0) until the head first reaches cell -3, then 2 steps.
    Returns (word, Run) if the result is S(word) one cell further left, else (None, Run)."""
    tape, run = {-2: 1, -1: 1}, Run(tm)
    put(tape, 0, cells(r))
    q = run.go(tape, 0, "D", -3)
    pos = -3
    for _ in range(2):
        s = tape.get(pos, 0)
        w, mv, q = run.T[(q, s)]
        tape[pos] = w
        pos += mv
        run.steps += 1
    ok = q == "D" and pos == -1 and tape.get(-3) == 1 and tape.get(-2) == 1
    return (read_side(tape, -1) if ok else None), run


# ---------------------------------------------------------------- random words
def rword(rng, n=None):
    n = rng.randint(0, 30) if n is None else n
    kind = rng.random()
    if kind < 0.4:
        w = "".join(rng.choice("L01") for _ in range(n))
    elif kind < 0.7:
        w = "L" * rng.randint(0, 40) + "".join(rng.choice("L01") for _ in range(rng.randint(0, 12)))
    else:
        w = "".join(rng.choice(rng.choice(["LLL01", "L01", "01", "0001", "LLLLLL1", "11L"])) for _ in range(n))
    return w + "1"


def main():
    rng = random.Random(20261010)
    nrand = 12000 if FULL else 4000

    # 1. Inc: one h-pass turns <r> into <inc r> in 6j+1 steps (j = digits before the first 0-digit).
    ok = tot = 0
    words = ["".join(w) for n in range(7) for w in itertools.product("L01", repeat=n)]
    words += [rword(rng) for _ in range(nrand)]
    for r in words:
        tape = {}
        put(tape, 0, cells(r))
        run = Run(TM)
        q = run.go(tape, 0, "B", -1)
        j = r.index("0") if "0" in r else len(r)
        tot += 1
        same = read_side(tape, 0).rstrip("0") == inc(r).rstrip("0")   # trailing 000 digits = 0^inf
        ok += q == "C" and same and run.steps == 6 * j + 1 and run.a1 == 0
    report("Inc: h-pass <r> -> <inc r> in 6j+1 steps, no A1 (all r up to 6 digits + random)", ok, tot)

    # 2. R(tp,k,r) is exact at pass level (RIncs_spec), every clause incl. X1/C1 (+1) and Z0/Z1;
    #    #A1 firings = #X1 + #C1 (A1 fires once per L entered); F always reads 0.
    cover, first, ok, tot, fbad = Counter(), Counter(), 0, 0, 0
    inst = []
    for tp in "x1":
        for k in range(0, 9):
            for n in range(0, 5):
                for w in itertools.product("L01", repeat=n):
                    inst.append((tp, k, "".join(w)))
    for k in range(0, 80):                       # right-end clauses R0/R1/R2 and Z0/Z1 with many k
        for r in ("", "0", "1", "L", "00", "01", "10", "11"):
            inst.append(("1", k, r))
    for _ in range(nrand):
        tp = rng.choice("x1")
        k = rng.choice([0, 0, 1, 2, 3, rng.randint(0, 20), rng.randint(0, 200)])
        inst.append((tp, k, rword(rng)))
    for tp, k, r in inst:
        x = R(tp, k, r)
        if x is None:
            continue
        want, cnt = x
        try:
            got, run = passes(TM, tp, k, r)
        except RuntimeError:
            got, run = None, None
        tot += 1
        good = got == want and run.a1 == cnt["X1"] + cnt["C1"]
        ok += good
        if run is not None:
            fbad += run.fread[1]
        cover.update(cnt)
        # clause used on the first digit (or at the right end)
        if r:
            d = r[0]
            c = {("x", "L"): "X1", ("x", "0"): "X2", ("x", "1"): "X3"}.get((tp, d)) if tp == "x" else \
                ("Z1" if d == "1" else "Z0") if k == 0 else {"L": "C1", "1": "C2"}.get(d, "C3" if k % 2 else "C4")
        else:
            c = "R0" if k == 0 else ("R1" if k % 2 else "R2")
        first[c] += 1
    report("R(tp,k,r) = pass-level result on the real machine, #A1 = #X1+#C1 (instances where R is defined)",
           ok, tot)
    print("   clause uses:", dict(sorted(cover.items())), "\n   instances by first clause:", dict(sorted(first.items())))
    report("F never reads 1 inside any pass (count of F-reads-1)", 0 if fbad else 1, 1)

    # 2b. The TM7 template: SOMDCv6 TM7 (same relation without +1) is exact for TM7 too, same A1 count.
    ok = tot = 0
    for tp, k, r in inst[: 3000]:
        x = R(tp, k, r, ours=False, zero_clauses=False)
        if x is None:
            continue
        want, cnt = x
        got, run = passes(TM7, tp, k, r)
        tot += 1
        ok += got == want and run.a1 == cnt["X1"] + cnt["C1"]
    report("TM7 template: TM7's RIncs is exact on TM7, #A1 = #X1+#C1", ok, tot)

    # 3. Machine-level L entry (reuse check_rules.l_entry): ours `1 D> 110 X -> 1 111 D> inc X` (6j+13) and
    #    `B> 1 110 X -> 1 111 D> inc X` (6j+12); TM7 the same without inc in 11 / 10 steps.
    le = check_rules.l_entry(n_random=150)
    for name, (t, o) in le.items():
        report(f"L entry {name}", o, t)

    # 4. Lemma A: inc(R(tp,k,r)) = R(tp,k+1,r) whenever R(tp,k,r) is defined.
    ok = tot = 0
    for tp in "x1":
        for k in range(0, 13):
            for n in range(0, 7):
                for w in itertools.product("L01", repeat=n):
                    a = Rw(tp, k, w)
                    if a is None:
                        continue
                    tot += 1
                    ok += Rw(tp, k + 1, w) == inc(a)
    report("Lemma A (Inc then R(tp,k) = R(tp,k+1)), all r up to 6 digits, k <= 12", ok, tot)
    # The instance used by the Z1/Z0 rows of 3.3: R(h1,m,[],w) /\ Inc(w,w+) -> R(h1,m+1,[],w+).
    ok = sum(Rw("1", m + 1, "") == inc(Rw("1", m, "")) for m in range(2000))
    report("Lemma A at the right end (R0-R2 derivations), m < 2000", ok, 2000)

    # 5. End lemmas, stated relationally in proof.md: R(h1,m,[],w) /\ m <= q => R(h1,q,w,_) (End_1);
    #    R(h1,m,[],w) /\ m <= 2q+2 => R(hx,q,w,_) (End_x). Here w = Rw("1", m, "") (R0-R2 are deterministic).
    ok = tot = 0
    for m in range(0, 300):
        wm = Rw("1", m, "")
        for q in range(0, 160):
            if m <= q:
                tot += 1; ok += Rw("1", q, wm) is not None
            if m <= 2 * q + 2:
                tot += 1; ok += Rw("x", q, wm) is not None
    report("End_1 / End_x (m < 300, q < 160)", ok, tot)
    # sharpness: End_1 fails at m = q+1 for some q; End_x fails at m = 2q+3 for some q
    s1 = [q for q in range(60) if Rw("1", q, Rw("1", q + 1, "")) is None]
    print(f"   (End_1's bound is tight: m = q+1 fails for q in {s1[:6]}...; End_x's bound has slack)")

    # 6. Domain lemma (RIncs_nxt'): R(tp,k,r) defined and Inv(tp,k,j,tq,kq) => R(tq,kq, R(tp,k+j,r)) defined.
    def inv(tp, k, j, tq, kq):
        if (tp, tq) == ("x", "x"):
            return k <= kq and j <= kq
        if (tp, tq) == ("1", "x"):
            return k + 1 <= kq and j <= kq
        if (tp, tq) == ("1", "1"):
            return (j == 0 and 2 * k + 1 <= kq) or (j >= 1 and k + j <= kq and kq >= 1)
        return False

    ok = tot = 0
    small = ["".join(w) for n in range(0, 6) for w in itertools.product("L01", repeat=n)]
    for tp, tq in (("x", "x"), ("1", "x"), ("1", "1")):
        for k in range(0, 9):
            for j in range(0, 9):
                kqs = [kq for kq in range(0, 40) if inv(tp, k, j, tq, kq)]
                if not kqs:
                    continue
                kq = kqs[0]                       # the smallest kq allowed (monotone in kq by Lemma A)
                for r in small:
                    if Rw(tp, k, r) is None:
                        continue
                    tot += 1
                    ok += Rw(tq, kq, Rw(tp, k + j, r)) is not None
    for _ in range(nrand * 3):
        tp, tq = rng.choice([("x", "x"), ("1", "x"), ("1", "1")])
        k, j = rng.choice([rng.randint(0, 6), rng.randint(0, 60)]), rng.choice([0, 1, 2, rng.randint(0, 60)])
        kqs = [kq for kq in range(0, 300) if inv(tp, k, j, tq, kq)]
        r = rword(rng)
        if not kqs or Rw(tp, k, r) is None:
            continue
        tot += 1
        ok += Rw(tq, kqs[0], Rw(tp, k + j, r)) is not None
    report("Domain lemma RIncs_nxt' at the smallest allowed kq (exhaustive r <= 5 digits, k,j <= 8; + random)",
           ok, tot)

    # 6b. Closure of Inv under the per-digit case analysis of proof.md section 3.3 (abstract pair states).
    ok, tot = pair_closure(28)
    report("Inv closed under every case of the induction step (pair states, k < 28, K,kq < 56)", ok, tot)

    # 7. The sweep map's domain is closed: sweep(r) defined => sweep(sweep(r)) defined (all words <= 10 digits);
    #    without Z0/Z1 it is not (first counterexample printed).
    ok = tot = nz = 0
    top = 11 if FULL else 10
    for n in range(0, top + 1):
        for w in itertools.product("L01", repeat=n):
            w = "".join(w)
            a = sweep(w)
            if a is not None:
                tot += 1
                ok += sweep(a) is not None
            b = sweep(w, zero_clauses=False)
            if b is not None and sweep(b, zero_clauses=False) is None:
                nz += 1
    report(f"Domain closed: sweep(r) defined => sweep(sweep r) defined (all words up to {top} digits)", ok, tot)
    cex = "LLLL10LL1L1"
    b = sweep(cex, zero_clauses=False)
    print(f"   without Z0/Z1 it is NOT closed: {nz} words up to {top} digits fail, e.g. r={cex} -> {b} -> undefined"
          f" (with Z0/Z1: {b} -> {sweep(b)}; real machine: {sweep_tm(TM, b)[0]})")
    if not (b is not None and sweep(b, zero_clauses=False) is None and sweep_tm(TM, b)[0] == sweep(b)):
        FAILS.append("Z0/Z1 counterexample")

    # 8. BigStep on the real machine: S(r) ->+ S(sweep r), one cell to the left; incl. instances that use Z0/Z1.
    ok = tot = zuse = 0
    pool = [rword(rng) for _ in range(nrand)] + ["LLLLL1LLLLLLL111", "0LLLL0LLLLLLL0001", "LLLLLLL1LLLLLL111"]
    for _ in range(3000):                         # search for words whose sweep uses Z0/Z1
        w = rword(rng)
        x = R("x", 0, w)
        if x and (x[1]["Z0"] or x[1]["Z1"]):
            pool.append(w)
    for r in pool:
        x = R("x", 0, r)
        if x is None:
            continue
        want, cnt = x
        got, run = sweep_tm(TM, r)
        tot += 1
        ok += got == want and run.fread[1] == 0
        zuse += bool(cnt["Z0"] or cnt["Z1"])
    report(f"BigStep: real machine S(r) ->+ S(sweep r) one cell left ({zuse} instances use Z0/Z1)", ok, tot)

    # 8b. proof.md's worked example (the picture pair's start S(L^4 1L1)), abstract and on both real machines.
    ex = [inc(inc(inc(inc("1L1")))) == "1L11", inc("11") == "001",
          sweep("LLLL1L1") == "LLLLLLLLL111" == sweep_tm(TM, "LLLL1L1")[0],
          Rw("x", 0, "LLLL1L1", ours=False, zero_clauses=False) == "LLLLLLL101" == sweep_tm(TM7, "LLLL1L1")[0]]
    report("Worked example S(L^4 1L1): ours -> S(L^9 111), TM7 -> S(L^7 101), intermediate words", sum(ex), len(ex))

    # 9. Initial segment and the run from blank: c0 ->(5) S(1); every left record (+2 steps) is S(r) and
    #    consecutive ones are related by the sweep map (with Z0/Z1; none of them is used).
    m = sim.parse(TM)
    r5 = sim.run(m, sim.Config.blank(), 5, engine="py")
    c5 = r5.final.trimmed()
    init_ok = (not r5.halted) and c5.state == "D" and "".join(map(str, c5.tape)).rstrip("0") == "111" \
        and c5.head == 2 and c5.dir == "R"
    report("Initial segment: 0^inf A> 0^inf ->(5) 0^inf 11 D> 100 0^inf = S(1)", int(init_ok), 1)
    N = 2 * 10 ** 9 if FULL else 10 ** 8
    seq = []
    for ev in sim.events(m, max_steps=N, on_record=True, snapshot=True):
        if ev.side != "L":
            continue
        c = ev.config
        tape, h = "".join(map(str, c.tape)), c.head
        rr = tape[h + 2:].rstrip("0")
        rr += "0" * ((-len(rr)) % 3)
        seq.append((ev.step + 2, ev.pos + 2, "".join(DIG.get(rr[i:i + 3], "?") for i in range(0, len(rr), 3))))
    good = sum(sweep(a) == b and p1 == p0 - 1 for (_, p0, a), (_, p1, b) in zip(seq, seq[1:]))
    zfree = sum(not (R("x", 0, a)[1]["Z0"] or R("x", 0, a)[1]["Z1"]) for _, _, a in seq[:-1])
    report(f"From blank to {N:.0e} steps: {len(seq)} sweeps' boundaries S(r), consecutive pairs follow sweep",
           good, len(seq) - 1, f"(first S(1) at step {seq[0][0]}; Z0/Z1 unused in {zfree}/{len(seq) - 1})")
    last = seq[-1][2]
    nl = len(last) - len(last.lstrip("L"))
    print(f"   last boundary: step {seq[-1][0]:,} = S(L^{nl} {last[nl:]})")

    # 10. Abstract orbit from S(1): stays in the domain; Z0/Z1 never needed.
    r, nz, M = "1", 0, (3000 if FULL else 800)
    for i in range(M):
        x = R("x", 0, r)
        if x is None:
            break
        nz += bool(x[1]["Z0"] or x[1]["Z1"])
        r = x[0]
    n = len(r) - len(r.lstrip("L"))
    report(f"Abstract orbit from S(1): {M} sweeps in the domain (Z0/Z1 used in {nz}); ends at S(L^{n} {r[n:]})",
           int(x is not None), 1)

    if FULL:
        rocq_check()
    print("ALL PASS" if not FAILS else "FAILURES: " + "; ".join(FAILS))


def pair_closure(B):
    """Abstract pair states (tp,k,K,tq,kq): the first process is at count k on r with K = k+j as seen by the
    second process (count kq). Checks, for every state satisfying Inv in the box: the end case, the Z0/Z1 end
    case, and for each next digit d the first can read: the second can read its digit and the successor
    satisfies Inv (the case analysis of proof.md section 3.3)."""
    def inv(tp, k, K, tq, kq):
        j = K - k
        if j < 0:
            return False
        if (tp, tq) == ("x", "x"):
            return k <= kq and j <= kq
        if (tp, tq) == ("1", "x"):
            return k + 1 <= kq and j <= kq
        if (tp, tq) == ("1", "1"):
            return (j == 0 and 2 * K + 1 <= kq) or (j >= 1 and K <= kq and kq >= 1)
        return False

    def step(st, d):
        tp, k, K, tq, kq = st
        if tp == "x":
            if d == "1":
                nt, nk, NK = "1", k, K
            else:
                nt, nk, NK = "x", k + 1, K + 1
            o = "L"
        else:
            if k == 0:
                return None                       # only Z0/Z1 at the last digit (checked separately)
            if d == "L":
                nt, nk, NK, o = "x", k, K, "L"
            elif d == "1":
                nt, nk, NK, o = "1", k - 1, K - 1, "L"
            else:
                nt, nk, o, NK = "1", (k - 1) // 2, ("0" if K % 2 else "1"), (K - 1) // 2
        if tq == "x":
            if o == "L":
                return (nt, nk, NK + 1, "x", kq + 1)
            if o == "0":
                return (nt, nk, NK, "x", kq + 1)
            return (nt, nk, NK, "1", kq)
        if kq == 0:
            return "FAIL"
        if o == "L":
            return (nt, nk, NK + 1, "x", kq)
        if o == "1":
            return (nt, nk, NK, "1", kq - 1)
        return (nt, nk, NK, "1", (kq - 1) // 2)

    ok = tot = 0
    for tp, tq in (("x", "x"), ("1", "x"), ("1", "1")):
        for k in range(B):
            for K in range(k, 2 * B):
                for kq in range(2 * B):
                    st = (tp, k, K, tq, kq)
                    if not inv(*st):
                        continue
                    good = True
                    if tp == "1":
                        if Rw(tq, kq, Rw("1", K, "")) is None:
                            good = False
                        if k == 0:
                            for d in "01":
                                if Rw(tq, kq, Rw("1", K, d)) is None:
                                    good = False
                    for d in "L01":
                        ns = step(st, d)
                        if ns is None:
                            continue
                        if ns == "FAIL" or not inv(*ns):
                            good = False
                    tot += 1
                    ok += good
    return ok, tot


# ---------------------------------------------------------------- Rocq check of proof.md 3.1, 3.2 and 4
# Written by the 2026-10-10 reviewer (scratch name RSpec2.v); header and the 8 unchanged clause proofs are
# copied from vendor/busycoq/verify/SOMDCv6.v Module TM7. The two new segment facts are the ones probed in
# rocq-scratch/probe_segments_2.v (probe_hx_ld, probe_h1_ld).
ROCQ_SPEC = r"""
From BusyCoq Require Import Individual62 Longitudinal DivModCases.
Require Import ZifyNat Lia.
Require Import ZArith.
Require Import String.
Require Import List.

Ltac esc :=
  (apply BoundedConfig.segRLs_c_spec with (T:=10^3); reflexivity) ||
  (apply BoundedConfig.sideRLs_c_spec with (T:=10^3); reflexivity) ||
  (eapply sideRLs_c_spec with (T:=10^6); [vm_compute; reflexivity | st; reflexivity]).

Ltac ec := econstructor.

Ltac am a a' k b b' :=
  applys_eq (segRLs_addmul_v2 a a' k b b'); unfold DH0; flia; esc.

Definition tm := Eval compute in (TM_from_str "1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---").

Notation ld := [1;1;0].
Notation d0 := [0;0;0].
Notation d1 := [1;0;0].
Notation w1ld := [1;1;1;0].
Notation hR := (B,@nil Sym).
Notation hR' := (D,[1]).
Notation hL := (C,@nil Sym).
Notation h := [(hR,hL)].
Notation h' := [(hR',hL)].

Inductive RD := LD|D0|D1.
Inductive H := hx|h1.

Fixpoint toRC ls :=
match ls with
| [] => 0inf
| LD::ls => ld*>toRC ls
| D0::ls => d0*>toRC ls
| D1::ls => d1*>toRC ls
end.

Definition toH' x := match x with | hx => [] | h1 => [1] end.
Definition toH x := match x with | hx => h' | h1 => [] end.

Inductive Inc: list RD -> list RD -> Prop :=
| Inc_d1 r r': Inc r r' -> Inc (D1::r) (D0::r')
| Inc_d0 r: Inc (D0::r) (D1::r)
| Inc_ld r r': Inc r r' -> Inc (LD::r) (LD::r')
| Inc_nil: Inc [] [D1].

Inductive RIncs: H->nat->(list RD)->(list RD)->Prop :=
| RIncs_hx_ld k r r1 r':
  Inc r r1 ->
  RIncs hx (1+k) r1 r' ->
  RIncs hx k (LD::r) (LD::r')
| RIncs_hx_d1 k r r':
  RIncs h1 k r r' ->
  RIncs hx k (D1::r) (LD::r')
| RIncs_hx_d0 k r r':
  RIncs hx (1+k) r r' ->
  RIncs hx k (D0::r) (LD::r')
| RIncs_h1_ld k r r1 r':
  Inc r r1 ->
  RIncs hx (1+k) r1 r' ->
  RIncs h1 (1+k) (LD::r) (LD::r')
| RIncs_h1_d1 k r r':
  RIncs h1 k r r' ->
  RIncs h1 (1+k) (D1::r) (LD::r')
| RIncs_h1_d0_0 k r r':
  RIncs h1 k r r' ->
  RIncs h1 (1+k*2) (D0::r) (D0::r')
| RIncs_h1_d0_1 k r r':
  RIncs h1 k r r' ->
  RIncs h1 (2+k*2) (D0::r) (D1::r')
| RIncs_h1_rh_0:
  RIncs h1 0 [] [D1]
| RIncs_h1_rh_1 k r':
  RIncs h1 k [] r' ->
  RIncs h1 (1+k*2) [] (D0::r')
| RIncs_h1_rh_2 k r':
  RIncs h1 k [] r' ->
  RIncs h1 (2+k*2) [] (D1::r')
| RIncs_z1: RIncs h1 0 [D1] [LD]
| RIncs_z0: RIncs h1 0 [D0] [D1]
.

Ltac cat3 :=
  eapply @segRLs_sideRLs_concat with (w1:=[_;_;_]) (w2:=[_;_;_]); [|eauto 1].
Ltac tr1 :=
  rewrite lpow_add,app_assoc;
  eapply segRLs_trans; [esx | ].
Ltac wal :=
  eapply segRLs_wall''; esx.
Ltac tr2 :=
  eapply sideRLs_trans; [esx | ].

Open Scope nat.

Lemma Inc_spec r r': Inc r r' -> sideRLs tm h (toRC r) (toRC r').
Proof.
  induction 1; cbn[toRC].
  - cat3. esx.
  - eapply @segRLs_sideRLs_concat with (w1:=[_;_;_]) (w2:=[_;_;_]) (ls2:=[]); [esx | constructor].
  - cat3. esx.
  - esc.
Qed.

Lemma seg_hx_ld k: segRLs tm (h' ++ h^^k) (h ++ h' ++ h^^(1+k)) ld ld.
Proof.
  rewrite lpow_add.
  change (h ++ h' ++ h^^1 ++ h^^k) with ((h ++ h' ++ h^^1) ++ h^^k).
  eapply segRLs_trans; [esx | wal].
Qed.

Lemma seg_h1_ld k: segRLs tm (h^^1 ++ h^^k) (h ++ h' ++ h^^(1+k)) w1ld ld.
Proof.
  rewrite lpow_add.
  change (h ++ h' ++ h^^1 ++ h^^k) with ((h ++ h' ++ h^^1) ++ h^^k).
  eapply segRLs_trans; [esx | wal].
Qed.

Lemma RIncs_spec tp k r r':
  RIncs tp k r r' ->
  sideRLs tm (toH tp++h^^k) (toH' tp*>toRC r) (toRC r').
Proof.
  intro H.
  induction H; intros; cbn[toH toH' toRC] in *.
  - (* X1: NEW *)
    eapply @segRLs_sideRLs_concat with (w1:=[_;_;_]) (w2:=[_;_;_]);
      [apply seg_hx_ld | eapply sideRLs_trans; [apply Inc_spec; eauto | apply IHRIncs]].
  - tr2.
    cat3; wal.
  - cat3; tr1; wal.
  - (* C1: NEW *)
    rewrite lpow_add.
    eapply @segRLs_sideRLs_concat with (w1:=[_;_;_;_]) (w2:=[_;_;_]);
      [apply seg_h1_ld | eapply sideRLs_trans; [apply Inc_spec; eauto | apply IHRIncs]].
  - rewrite lpow_add,app_assoc.
    tr2.
    cat3; wal.
  - cat3.
    rewrite app_nil_l.
    am 2 1 k 1 1.
    rewrite Nat.add_comm,lpow_add,Nat.mul_1_r.
    tr2; eauto 1.
  - cat3.
    rewrite Nat.add_comm.
    am 2 1 k 2 1.
    rewrite Nat.add_comm,lpow_add,Nat.mul_1_r.
    tr2; eauto 1.
  - esc.
  - rewrite lpow_add,app_assoc.
    tr2.
    cat3.
    rewrite app_nil_l.
    am 2 1 k 0 0.
  - change (2+k*2) with (1+(1+k*2)).
    rewrite lpow_add,app_assoc.
    tr2.
    cat3.
    rewrite app_nil_l.
    am 2 1 k 1 0.
  - (* Z1: NEW, zero passes *)
    cbn. applys_eq sideRLseq_O. cbn. rewrite (const_unfold _ s0) at 1. reflexivity.
  - (* Z0: NEW, zero passes *)
    cbn. applys_eq sideRLseq_O. cbn. rewrite (const_unfold _ s0) at 1. reflexivity.
Qed.

Open Scope sym.
Notation lh := (0inf<*<[1]).
Definition S' r := lh {{{ (hR',R) }}} toH' hx *> toRC r.
Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).

Lemma BigStep r r':
  RIncs hx 0 r r' ->
  S' r -->+ S' r'.
Proof.
  intros H.
  apply RIncs_spec in H.
  unfold S'.
  eapply sideRLs_1 in H.
  follow10 H.
  es.
Qed.

Lemma init: c0 -[ tm ]->* S' [D1].
Proof. esx. Qed.

Print Assumptions RIncs_spec.
Print Assumptions BigStep.
Print Assumptions init.
"""


def rocq_check():
    """Compile ROCQ_SPEC in a fresh temp dir; pass iff coqc exits 0, the file has no escape hatch, and all three
    `Print Assumptions` say 'Closed under the global context'."""
    banned = re.findall(r"\b(Admitted|admit|Axiom|Parameter|Hypothesis|Conjecture|Abort|bypass_check)\b|"
                        r"Unset Guard Checking", ROCQ_SPEC)
    with tempfile.TemporaryDirectory(prefix="m2_rspec_") as d:
        with open(os.path.join(d, "RSpec.v"), "w") as f:
            f.write(ROCQ_SPEC)
        v = f"{ROOT}/vendor/busycoq/verify"
        cmd = (f"eval $(opam env --switch=bb6) && ulimit -s unlimited && cd {d} && "
               f"coqc -Q {v} BusyCoq -Q {v}/BigInt BigInt -native-compiler yes RSpec.v")
        p = subprocess.run(["bash", "-c", cmd], capture_output=True, text=True, timeout=1200)
    out = p.stdout + p.stderr
    closed = out.count("Closed under the global context")
    ok = p.returncode == 0 and not banned and closed == 3
    report("Rocq: Inc_spec, RIncs_spec (all 12 clauses), BigStep, init c0 ->* S(1) compile; "
           "3 x Print Assumptions closed", int(ok), 1,
           f"(coqc exit {p.returncode}, closed {closed}/3, banned words {len(banned)})")
    if not ok:
        print(out[-3000:])


if __name__ == "__main__":
    if ROCQ_ONLY and not FULL:
        rocq_check()
        print("ALL PASS" if not FAILS else "FAILURES: " + "; ".join(FAILS))
    else:
        main()