#!/usr/bin/env python3
"""Check every rule and claim in proof.md for 1RB0LE_1LC1RD_1LA0RB_1RC1RB_1LF0LC_---0RC.

Run from anywhere:  python3 -B check_proof.py [--cycles N] [--sft]
Checks: shift/wall/junction rules (unknown context), bounces B1-B6, probe P0 on the orbit, NORM (tails normalized:
nonempty, ending in 1; P strips trailing 0s), IFACE (fixed 16-round-trip protocol one cell left of the X0|D cut),
E' (right-part protocol system reproduces P), CYC, INIT1 (C_1(58, 011 D_0) at 758,939), INIT (C_0(59, D_0) at 784,041), HALT.
Independent partial simulator (stdlib only). Cells outside a rule's window are UNKNOWN unless the
rule says 0^inf; reading an unknown cell fails the check. So a passing shift rule holds for every
context, and induction gives it for every repeat count n.
"""
import random, re, sys, os, json

TM = "1RB0LE_1LC1RD_1LA0RB_1RC1RB_1LF0LC_---0RC"
TR = {}
for q, part in enumerate(TM.split("_")):
    for s in (0, 1):
        t = part[3 * s:3 * s + 3]
        TR[(q, s)] = None if t[2] == "-" else (int(t[0]), 1 if t[1] == "R" else -1, ord(t[2]) - 65)
S = "ABCDEF"
HERE = os.path.dirname(os.path.abspath(__file__))

BLK = "1101101101"          # bulk block (resting form)
R1 = "1011110110"           # bulk block after the right sweep
G = "11110101"              # left-sweep gadget: G <E 0
X = ["110111100110011101100100100111101100100110110111010011",
     "1001001001100100100100110110110011101100100110110111010",
     "11011001001100100100100110110110011101100100110110111010",
     "101110100110110010011101100100100111101100100110110111010",
     "1101001101100100110011101100100100111101100100110110111010",
     "11011011001001100110011101100100100111101100100110110111010",
     "10011100110011101100100100111101100100110110111010"]
# junction rules J_k:  R1^c B> X_k [011 if k=6]  -->  R1^(c-m) G <E 0 Y_k      (j steps)
#   (c = context blocks the run needs, m = blocks consumed; Y_k = BLK^(m-1) X_{k+1}, Y_5 = X_6)
J = {1: dict(c=1, m=1, Y=X[2]), 2: dict(c=2, m=2, Y=BLK + X[3]), 3: dict(c=1, m=1, Y=X[4]),
     4: dict(c=1, m=1, Y=X[5]), 5: dict(c=0, m=0, Y=X[6]), 6: dict(c=1, m=1, Y=X[0])}

fails = []
def check(name, ok, info=""):
    print(("PASS " if ok else "FAIL ") + name + (("  " + info) if info else ""))
    if not ok: fails.append(name)

# ---------------- partial simulator ----------------
def cfg(left, tok, right, lzero=False, rzero=False):
    """Directed-head config. tok '<X' reads last cell of `left`; 'X>' reads first cell of `right`.
    lzero/rzero: that side continues as 0^inf (else unknown). Returns (cells dict, head pos, state, lz, rz, lo, hi)."""
    cells = {}
    for i, c in enumerate(left): cells[i] = int(c)
    for i, c in enumerate(right): cells[len(left) + i] = int(c)
    if tok[0] == "<":
        st, h = S.index(tok[1]), len(left) - 1
    else:
        st, h = S.index(tok[0]), len(left)
    return dict(cells=cells, h=h, st=st, lo=0, hi=len(left) + len(right) - 1, lz=lzero, rz=rzero)

def read(c, p):
    if p in c["cells"]: return c["cells"][p]
    if p < c["lo"] and c["lz"]: return 0
    if p > c["hi"] and c["rz"]: return 0
    return None

def step(c):
    v = read(c, c["h"])
    if v is None: return "UNKNOWN"
    t = TR[(c["st"], v)]
    if t is None: return "HALT"
    w, d, n = t
    c["cells"][c["h"]] = w; c["h"] += d; c["st"] = n
    return None

def run(c, n):
    for i in range(n):
        e = step(c)
        if e: return e, i
    return None, n

def same(c, t, shift=0):
    """c equals target t placed `shift` cells to the right (same unknown/zero structure assumed)."""
    if c["st"] != t["st"] or c["h"] != t["h"] + shift: return False
    keys = set(c["cells"]) | {k + shift for k in t["cells"]}
    for k in keys:
        a = read(c, k)
        b = t["cells"].get(k - shift, 0 if ((k - shift < t["lo"] and t["lz"]) or (k - shift > t["hi"] and t["rz"])) else None)
        if a != b: return False
    return True

def rule(name, src, dst, nsteps, shift=0):
    c = src; err, done = run(c, nsteps)
    ok = err is None and same(c, dst, shift)
    check(name, ok, f"{nsteps} steps" if ok else f"err={err} after {done}")
    return ok

def first_left_record(c, cap):
    lo = c["h"]; n = 0
    while n < cap:
        e = step(c); n += 1
        if e: return e, n
        if c["h"] < lo: return None, n
    return "CAP", n

rng = random.Random(20261010)

# ---------------- 1. shift rules and wall rules ----------------
print("== shift and wall rules (unknown context; induction gives all n)")
rule("RS   B> blk --> R1 B>", cfg("", "B>", BLK), cfg(R1, "B>", ""), 12)
rule("LS   R1 G <E 0 --> G <E 0 blk", cfg(R1 + G, "<E", "0"), cfg(G, "<E", "0" + BLK), 58)
rule("WS   0^inf <A --> 0^inf 1 B>", cfg("0", "<A", "", lzero=True), cfg("1", "B>", "", lzero=True), 1)
rule("WE   0^inf 1 G <E 0 --> 0^inf <A blk", cfg("1" + G, "<E", "0", lzero=True),
     cfg("", "<A", BLK, lzero=True), 29)
# (WE target: head on the 0 just left of the old window; blk occupies the old 10-cell window)

# ---------------- 2. junction rules J_k (k=1..6) ----------------
print("== junction rules J_k: R1^c B> X_k --> R1^(c-m) G <E 0 Y_k")
jsteps = {}
for k in range(1, 7):
    p = J[k]; tail = "011" if k == 6 else ""
    src = cfg(R1 * p["c"], "B>", X[k] + tail)
    # find step count by running to the target shape, then re-check exactly
    probe = cfg(R1 * p["c"], "B>", X[k] + tail); n = 0; got = None
    tgt = cfg(R1 * (p["c"] - p["m"]) + G, "<E", "0" + p["Y"])
    while n < 5000:
        if same(probe, tgt): got = n; break
        if step(probe): break
        n += 1
    if got is None:
        check(f"J{k}", False, "target not reached"); continue
    jsteps[k] = got
    rule(f"J{k}   R1^{p['c']} B> X{k}{' 011' if k == 6 else ''} --> R1^{p['c'] - p['m']} G <E 0 Y{k}", src, tgt, got)
    # minimality of context: one block less must read an unknown cell (documents why the domain is a>=c)
    if p["c"] > 0:
        c2 = cfg(R1 * (p["c"] - 1), "B>", X[k] + tail); e, _ = run(c2, got)
        check(f"J{k}   needs exactly c={p['c']} context block(s)", e == "UNKNOWN")

# ---------------- 3. bounce rules B_k = WS, RS^a, J_k, LS^(a-m), WE ----------------
print("== bounce rules C_k(a,D) --> C_k+1(a',D), checked by full simulation with D UNKNOWN")
beta = {k: 1 + jsteps[k] + 29 - 58 * J[k]["m"] for k in jsteps}
print("   beta_k = 1 + j_k + 29 - 58 m_k:", beta, " j_k:", jsteps)
for k in range(1, 7):
    if k not in beta: continue
    p = J[k]; ok_all = True; bad = None
    avals = list(range(p["c"], p["c"] + 12)) + [rng.randint(20, 200) for _ in range(6)] + [rng.randint(500, 3000) for _ in range(3)]
    for a in avals:
        tail = "011" if k == 6 else ""
        src = cfg("0", "<A", BLK * a + X[k] + tail, lzero=True)
        a2 = a + (1 if k == 5 else 0); nx = 0 if k == 6 else k + 1
        dst = cfg("0", "<A", BLK * a2 + X[nx], lzero=True)
        # bulk length changes by +-10 at k=5 and the junction length changes: align on the D cut
        cut_src = 1 + len(BLK * a + X[k] + tail); cut_dst = 1 + len(BLK * a2 + X[nx])
        e, n = run(src, 70 * a + beta[k])
        if e or not same(src, dst, cut_src - cut_dst): ok_all = False; bad = (a, e); break
        # and it is the first left record (the bounce ends exactly here)
    check(f"B{k}   C{k}(a,D) --> C{(k + 1) % 7}(a{'+1' if k == 5 else ''},D) in 70a+{beta[k]} steps, a>={p['c']}"
          + (", D=011D'" if k == 6 else ""), ok_all, f"{len(avals)} values of a up to {max(avals)}" if ok_all else str(bad))

# ---------------- 4. probe rule on orbit tails ----------------
print("== probe P0: R1 B> X0 D --> G <E 0 X1 011 P(D)   (only on tails from the orbit; NOT proved for a language)")
IFACE = len(R1) + len(X[0]) - 1     # index of the last cell of X0 = cell 0 of the right side
def edge(D, cap=10**6, census=None):
    """Run the junction-level probe on D with 1 context block (R1). Returns (P(D), j0) or (None, reason).
    D is normalized: empty or ending in 1 (trailing 0s belong to 0^inf); P(D) is returned normalized too.
    census: optional dict; receives the crossing sequences at the boundary IFACE-1|IFACE (one cell left of
    the X0|D cut) and at the cut IFACE|IFACE+1, as tuples of ('>' or '<', state after the move)."""
    c = cfg(R1, "B>", X[0] + D, rzero=True); bi, bc = [], []
    for n in range(cap):
        # target shape: R1^0 G <E 0 X1 011 ...   head at index len(G)-1
        if c["st"] == 4 and c["h"] == len(G) - 1:
            w = "".join(str(read(c, i)) for i in range(0, len(G) + 1 + len(X[1]) + 3))
            if w == G + "0" + X[1] + "011":
                hi = max(c["cells"]); r = "".join(str(c["cells"].get(i, 0)) for i in range(len(G) + 1 + len(X[1]) + 3, hi + 1))
                if census is not None: census["iface"] = tuple(bi); census["cut"] = tuple(bc)
                return r.rstrip("0"), n
        h0 = c["h"]; e = step(c)
        if e: return None, ("BADJ (left the R1 context block)" if e == "UNKNOWN" else e)
        if census is not None:
            h1 = c["h"]
            for b, lst in ((IFACE, bi), (IFACE + 1, bc)):
                if h0 == b - 1 and h1 == b: lst.append((">", S[c["st"]]))
                elif h0 == b and h1 == b - 1: lst.append(("<", S[c["st"]]))
    return None, "CAP"

# The right-side protocol system (proof.md section 6): right side = cells >= IFACE, i.e. "1" D 0^inf.
PROTO_IN, PROTO_OUT = "BDCDBDCBDBBBDCCB", "CEACCFAEECECAAAC"
def edge_right(D, cap=10**6):
    """Right side only. Excursion p: head enters cell 0 in state PROTO_IN[p]; it must step left off cell 0
    in state PROTO_OUT[p]. After excursion 16, cells 0..3 must read 0011; P(D) = cells 4.. (normalized)."""
    t = {i: int(ch) for i, ch in enumerate("1" + D)}; n = 0
    for p in range(16):
        h, q = 0, S.index(PROTO_IN[p])
        while h >= 0:
            if n >= cap: return None, "CAP"
            v = t.get(h, 0); tr = TR[(q, v)]
            if tr is None: return None, "HALT"
            t[h] = tr[0]; h += tr[1]; q = tr[2]; n += 1
        if S[q] != PROTO_OUT[p]: return None, f"BREAK at excursion {p + 1}"
    hi = max(t)
    if "".join(str(t.get(i, 0)) for i in range(4)) != "0011": return None, "BADTAIL"
    return "".join(str(t.get(i, 0)) for i in range(4, hi + 1)).rstrip("0"), n

D0 = open(os.path.join(HERE, "work", "D_cycle0.txt")).read().strip()
ncyc = int(sys.argv[sys.argv.index("--cycles") + 1]) if "--cycles" in sys.argv else 3000
D = D0; orbit = [D0]; js = []; okc = True; ifaces = set(); cuts = set()
for i in range(ncyc):
    cen = {}
    Dn, j = edge(D, census=cen)
    if Dn is None: okc = False; print("   cycle", i, "->", j); break
    js.append(j); D = Dn; orbit.append(D); ifaces.add(cen["iface"]); cuts.add(cen["cut"])
check(f"P0   orbit of the edge map from D_0: {len(orbit) - 1} cycles, junction intact, no halt", okc,
      f"|D| in [{min(map(len, orbit))},{max(map(len, orbit))}], j0 in [{min(js)},{max(js)}]")
check("NORM every orbit tail D_n is normalized (nonempty, ends in 1); |D_n| + 3n = 21 (mod 30)",
      all(d and d[-1] == "1" and (len(d) + 3 * n) % 30 == 21 for n, d in enumerate(orbit)))
proto = tuple(x for a, b in zip(PROTO_IN, PROTO_OUT) for x in ((">", a), ("<", b)))
check(f"IFACE crossing sequence one cell left of the X0|D cut: identical in all {len(orbit) - 1} cycles, "
      f"32 crossings = 16 round trips = (in,out) {list(zip(PROTO_IN, PROTO_OUT))}", ifaces == {proto})
print(f"   (info) at the X0|D cut itself: {len(cuts)} distinct crossing sequences, lengths {sorted({len(c) for c in cuts})}")
nr = min(len(orbit) - 1, 500); ok_r = all(edge_right(orbit[i])[0] == orbit[i + 1] for i in range(nr))
check(f"E'   right-side protocol system reproduces P on the first {nr} orbit tails", ok_r)
cmpf = os.path.join(HERE, "work", "D_edgemap_1951.txt")
if os.path.exists(cmpf) and len(orbit) > 1951:
    check("P0   edge-map orbit at cycle 1951 == work/D_edgemap_1951.txt (scripts/edgemap.c)", orbit[1951] == open(cmpf).read().strip())
c2 = cfg("", "B>", X[0] + D0, rzero=True); e, _ = run(c2, js[0])
check("P0   needs the R1 context block (reads left of X0)", e == "UNKNOWN")
# whole-bounce probe: C0(a,D) --> C1(a, 011 P(D)) in 70a + 1 + j0 + 29 - 58 steps, random a, sampled orbit tails
ok_all = True; bad = None
for t in range(25):
    i = rng.randrange(len(orbit) - 1); D, Dn = orbit[i], orbit[i + 1]; a = rng.choice([1, 2, 3, rng.randint(4, 60), rng.randint(100, 800)])
    src = cfg("0", "<A", BLK * a + X[0] + D, lzero=True, rzero=True)
    dst = cfg("0", "<A", BLK * a + X[1] + "011" + Dn, lzero=True, rzero=True)
    n = 70 * a + 1 + js[i] + 29 - 58
    e, _ = run(src, n)
    if e or not same(src, dst, src["h"] - dst["h"]):   # both ends 0^inf: compare up to translation
        ok_all = False; bad = (i, a, e); break
check("P0   C0(a,D) --> C1(a,011 P(D)) in 70a+j0(D)-28 steps (25 random (a, orbit D), a>=1)", ok_all, "" if ok_all else str(bad))

# ---------------- 5. cycle law and initial segment ----------------
print("== cycle law and initial segment")
SB = sum(beta.values())
ok_all = True
for t in range(6):
    i = rng.randrange(len(orbit) - 1); a = rng.randint(1, 40)
    src = cfg("0", "<A", BLK * a + X[0] + orbit[i], lzero=True, rzero=True)
    dst = cfg("0", "<A", BLK * (a + 1) + X[0] + orbit[i + 1], lzero=True, rzero=True)
    n = 490 * a + 70 + SB + js[i] - 28
    e, _ = run(src, n)
    if e or not same(src, dst, src["h"] - dst["h"]):
        ok_all = False; break
check(f"CYC  C0(a,D) --> C0(a+1,P(D)) in 490a+{70 + SB - 28}+j0(D) steps (6 random)", ok_all)

c = cfg("", "A>", "", lzero=True, rzero=True)
N0, N1 = 784041, 758939
e, _ = run(c, N1)
lo = min(k for k, v in c["cells"].items() if v) ; hi = max(k for k, v in c["cells"].items() if v)
tape = "".join(str(c["cells"].get(i, 0)) for i in range(lo, hi + 1))
check(f"INIT1 0^inf A> 0^inf --({N1})--> C1(58, 011 D_0) (earliest entry into the family with full X_k words)",
      e is None and c["st"] == 0 and c["h"] == lo - 1 and tape == BLK * 58 + X[1] + "011" + D0)
e, _ = run(c, N0 - N1)
lo = min(k for k, v in c["cells"].items() if v) ; hi = max(k for k, v in c["cells"].items() if v)
tape = "".join(str(c["cells"].get(i, 0)) for i in range(lo, hi + 1))
init_ok = (e is None and c["st"] == 0 and c["h"] == lo - 1 and tape == BLK * 59 + X[0] + D0)
check(f"INIT 0^inf A> 0^inf --({N0})--> C0(59, D_0) = 0^inf <A blk^59 X0 D_0 0^inf, |D_0|={len(D0)}", init_ok)

# ---------------- 6. halting transition ----------------
into_F = [(S[q] + str(s)) for (q, s), t in TR.items() if t and t[2] == 5]
check("HALT only F0 is undefined; F is entered only by E0 (1LF)", into_F == ["E0"] and [k for k, t in TR.items() if t is None] == [(5, 0)])

# ---------------- 7. optional: SFT_k closure falsification ----------------
if "--sft" in sys.argv:
    print("== SFT_k test: random D whose k-factors all occur on the orbit; one probe")
    for k in (8, 12, 16):
        Sk = set(); P = set()
        for D in orbit:
            w = D + "0" * k
            Sk.update(w[j:j + k] for j in range(len(w) - k + 1)); P.add(D[:k - 1])
        ext = {}
        for f in Sk: ext.setdefault(f[:-1], []).append(f[-1])
        st = {"ok": 0, "break": 0, "escape": 0}; Pl = sorted(P); tries = 0
        while sum(st.values()) < 200 and tries < 10000:
            tries += 1; w = rng.choice(Pl)
            while not w.endswith("000") and len(w) < 600:
                ch = ext.get(w[-(k - 1):])
                if not ch: w = None; break
                w += rng.choice(ch)
            if w is None or len(w) >= 600 or len(w) < 120: continue
            Dn, j = edge(w.rstrip("0"))
            if Dn is None: st["break"] += 1; continue
            ww = Dn + "0" * k
            if any(ww[i:i + k] not in Sk for i in range(len(ww) - k + 1)): st["escape"] += 1
            else: st["ok"] += 1
        print(f"   k={k}: {len(Sk)} factors; {st}")

print("\nSUMMARY:", "ALL PASS" if not fails else f"{len(fails)} FAIL: {fails}")
sys.exit(1 if fails else 0)