widex.py

"""
widex.py -- the closed form's KILL past period 3: on X (period 3 to
quotients 8, 4 to 6, 5 to 4, m = 2 .. 12), does c_inf stay c_ov or
c_ov - 1, read by widestep's crude bar and by classform's c_form, and
does a hull key strand at c_ov - 2 wherever pinned moves exist there?

QUESTION. widestep.py reads c_crude = c_form = induct.least at its 1001
cells (period <= 3, quotients <= 6, m <= 12); strand.py reads a hull key
in a zero-reply piece at c_ov - 2 at all 115 of the 1017 with pinned
moves there (H1). phase.py widened to X (7557 cells) and found the full
window's upper end unstranded at [1, 1, 1, 2, 3] x7, where c_inf = c_ov -
1 still (four cells read). X is the first widening past period 3; the
closed form's KILL is owed there, and H1, the open front the upper end's route
left, is read at every X cell with pinned moves at c_ov - 2.

DERIVED BY HAND (before the engine).
  THE BARS' RANGE. widestep.cell's c_crude is c_ov - 1 when slackbar's
  crude bar passes every piece at c_ov - 1 (pinned moves there), else
  c_ov: it never reads outside {c_ov - 1, c_ov}. So the KILL
  (c_crude != c_inf and c_form != c_inf at one cell) can fire two ways:
  c_inf leaves {c_ov - 1, c_ov} (X1's line) while c_form misses it too,
  or the crude bar errs inside the pair and the closed form errs with
  it. c_form reads the forms' hull at every c from the first pinned c
  up, so a hull end off its form (below) can move it.
  X1, a TRANSPLANT. c_inf <= c_ov is keyweld's gap step, derived with
  the endpoint step and the reduced flag read at the 48; c_inf >= c_ov -
  1 is read at the 1017 and at phase.py's four X cells only.
  (M) Pinned moves at c give them at c + 1 (theorem, by hand). By T1
  (strand.py) they are, at every t, m P_(c+1) <= P_1 and m P_c <= P_0
  at c even, m P_c <= P_1 and m P_(c+1) <= P_0 at c odd. At c even,
  c + 1 odd needs m P_(c+1) <= P_1 (given) and m P_(c+2) < m P_c <=
  P_0; at c odd, c + 1 even needs m P_(c+2) < m P_c <= P_1 and m
  P_(c+1) <= P_0 (given); P_k falls strictly in k. So where c_ov - 2
  has no pinned moves no c below has them, induct.least (which needs
  them) reads c_inf >= c_ov - 1, and X1's low side can fire only at
  the cells read for H1. Printed beside: pinned moves at c and none at
  c + 1, over c <= c_ov at every cell (0 by M).
  H1's READING leans on hullform's forms (a rule at the 136, a
  TRANSPLANT at every X cell): a form above the true top makes a key
  "in the hull" that is not, so H1 could pass falsely. The arm HULL
  reads, at c_ov - 2 at the read cells, hull.py's exact fixed points
  against the forms at every node, and the pinned closure's keys (the
  closure grown at that c, induct's) against the forms' [Z_lo, Z_hi].
  A cell where either fires is printed apart, its H1 verdict unread.

DESIGN (frozen before the engine). Cells: X = phase.family() (7557),
and strand.cells() (the 1017: widestep's W and the 136) as control.
Per cell widestep.cell (c_inf = induct.least "pin", c_ov, c_ov at 2m,
c_form, the FORM, LOW, CRUDE bars at c_ov - 1); then at c = c_ov - 2 >=
0 with pinned moves (strand.zero_in), strand.read_c (hull keys in
pieces) and read_c with plant (Z_hi := Z_lo). The HULL arm at the read
cells of X (all, or the period-5 ones if the rehearsal prices all past
ten minutes, named): hull.py's hull(low) for both ends against
hullform.forms at every node, exact; the pinned closure's keys at c
with Z outside the forms' range on their node.
PREDICTIONS. (X1) c_inf in {c_ov - 1, c_ov} at every X cell. (X2)
CRUDE's c = c_inf and (X3) c_form = c_inf at every X cell. (X4) H1:
some piece at c_ov - 2 holds a hull key at every read X cell.
KILLS (printed as, each n > 0 kills):
  "THE KILL: c_crude != c_inf and c_form != c_inf at n of N";
  "X1: c_inf outside {c_ov - 1, c_ov} at n of N";
  "X2: CRUDE's c != c_inf at n of N"; "X3: c_form != c_inf at n of N";
  "X4 (H1): no hull key in any piece at c_ov - 2 at n of N read cells",
  N = 7557 for the first four, each also over the arm (c_inf = c_ov -
  1) and where the bars fire, and by period.
Beside, no kill: LOW's c; c_inf unread (None or past the closure's
limit), counted apart; the HULL arm's two lines; per read cell the kinds
of the stranded keys (closed end, interior, +-K_c); the K1 cells of
phase.py (period 5, [1, 1, 1, ...], hot t = 2): which keys strand there.
CONTROLS (read before the verdicts).
  (a) THE 1017 through this engine: on W (1001) X1 to X3 at 0 with arm
      106, bars firing 672 (widestep's prints); on the 136 at 0 with arm
      17, firing 120; H1 read at 115, no hull key at 0 (strand's).
  (b) THE PLANT on c_ov, m doubled (widestep's (d)): X1's line read
      against c_ov(2m) must fire on X.
  (c) THE PLANT on H1, Z_hi := Z_lo (strand's (d)): X4's line must fire
      at some read X cell.
  (d) THE INSTRUMENT: induct.least against flush.PinGame's solved
      c_inf (widestep.game_cinf) at K4's cell [1, 1, 1, 2, 3] x7 and at
      [1, 1, 1, 1, 2] x2, x3 (period 5): equal at each, else no verdict
      on X is read.
  (e) THE PLANT on the HULL arm: hull.py's plant (d_max full - 1) must
      put its node line above 0.

FINDINGS (copied from the run's prints).
  CONTROLS. (a) W: 1001 cells, arm 106, bars can fire (pinned moves at
      c_ov - 1) at 672; the 136: arm 17, bars can fire at 120; the
      1017: X1 to X3, LOW and the KILL at 0, H1 at 0 of 115 read:
      held. (b) c_ov's m doubled: X1's line at 106
      of 7557. (c) Z_hi := Z_lo: X4's line at 22 of 788. (d) induct.least
      = PinGame at [1, 1, 1, 2, 3] x7 (5), [1, 1, 1, 1, 2] x2 (3), x3
      (5). (e) hull.py's plant moves 8 of 12 nodes at the first read
      cell where it moves any. X1's, X4's and the HULL arm's node line
      can fire; the KILL, X2, X3 and the closure-key line carry no
      plant here or in widestep (whose (b) planted LOW, (d) c_ov).
      Under (c) a key survives at 766 of 788: at the two cells read
      by hand, [1, 1, 1, 2, 3] x7 and [1, 1, 1, 3, 3] x10, the full
      flag's lower hull end -(a_(t+1) + 1, 1) = (-2, -1) at phase 2,
      a_(t+1) = 1, inside a gap, and at x10 a reduced-flag key beside it
      (observation).
  THE HULL ARM. At c_ov - 2 on X's 788 read cells: nodes whose exact
      hull end != its form 0 of 13304; pinned-closure keys outside the
      forms' range 0 of 201139. hullform's four ends hold there. (M):
      0 cells with pinned moves at c and none at c + 1.
  KILLS MISSED on X (7557 cells, c_inf read at all, arm 826, bars can
      fire at 4737): THE KILL 0; X1 0; X2 0; X3 0; LOW's c 0; X4 (H1)
      0 of 788 read (period 3, 4, 5: 122, 370, 296).
  KINDS on X: a closed end in the hull at 787 of 788 (all but K4's
      cell), an interior key at all 788, -K_c among them at 128.
      phase.py's four K1 cells strand interior keys at phases 1 to 3 at
      each, and on the reduced flag at phase 4 at two (phase.py's AFTER
      THE RUN print; the first 12 printed here are a sample).

RUN RECORD. 432.6 s (the 1017 31.9 s, X 398.6 s), peak commit 199.9
MB, estimated at seven to eight minutes from a 60-cell rehearsal (5.8
s). The engine was written whole after the freeze, rehearsed, then run
once. On shipping, the verdicts were made the exit code: 0 iff the
controls (a) to (e), the HULL arm, (M), the verdicts on X and the kinds'
three counts hold as printed; X4's split by period and the K1 cells'
keys are printed, unchecked.

Usage: python widex.py [cells]
"""


import os
import sys
import time

os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")
from induct import Field, Window, le  # noqa: E402
from hull import Coords, hull, eq  # noqa: E402
from hullform import forms  # noqa: E402
from strand import cells as strand_cells, read_c as strand_read  # noqa: E402
from strand import zero_in  # noqa: E402
from widestep import cell as wcell, game_cinf, necklaces  # noqa: E402
from induct import least  # noqa: E402
from flush import PERIODIC  # noqa: E402
from decide import FRESH  # noqa: E402
from phase import family  # noqa: E402


def hull_arm(F, m, c, plant=False):
    """At c: (nodes, nodes whose exact hull end != its form, closure keys,
    closure keys outside the forms' range on their node)."""
    win = Window(F, m, c)
    st, _miss = win.pin_starts()
    co = Coords(F, m, c)
    fm = {t: forms(F, co, m, c, t) for t in range(F.p)}
    nodes = off = 0
    for low in (False, True):
        val, _ = hull(win, co, st, low=low, plant=plant)
        for (t, f), v in val.items():
            nodes += 1
            off += not eq(v, fm[t][(f, low)])
    _ok, S, _bad = win.closure(st)
    out = 0
    for G, H, f, t in S:
        z = co.Z(G, H, t)
        out += not (le(fm[t][(f, True)], z) and le(z, fm[t][(f, False)]))
    return nodes, off, len(S), out


def mono(F, m, cov):
    """c <= c_ov with pinned moves at c and none at c + 1 (M)."""
    bad = []
    pin = [zero_in(F, m, c) for c in range(cov + 2)]
    for c in range(cov + 1):
        if pin[c] and not pin[c + 1]:
            bad.append(c)
    return bad


def read(per, m, do_hull):
    x = wcell(per, m)
    F = Field(per)
    x["p"] = F.p
    x["mono"] = mono(F, m, x["cov"])
    c = x["cov"] - 2
    x["read"] = False
    if c >= 0 and zero_in(F, m, c):
        r = strand_read(F, m, c)
        if r is not None:
            x["read"] = True
            x["c2"] = c
            x["keys"] = r["keys"]
            x["plant"] = bool(strand_read(F, m, c, plant=True)["keys"])
            if do_hull:
                x["hull"] = hull_arm(F, m, c)
    return x


def verdicts(label, rows):
    n = len(rows)
    ok = [x for x in rows if isinstance(x["cinf"], int)]
    arm = [x for x in ok if x["cinf"] == x["cov"] - 1]
    fire = [x for x in ok if x["fire"]]
    tests = (
        ("THE KILL", "c_crude != c_inf and c_form != c_inf",
         lambda x: x["bars"]["crude"] != x["cinf"] and x["cf"] != x["cinf"]),
        ("X1", "c_inf outside {c_ov - 1, c_ov}",
         lambda x: x["cinf"] not in (x["cov"] - 1, x["cov"])),
        ("X2", "CRUDE's c != c_inf",
         lambda x: x["bars"]["crude"] != x["cinf"]),
        ("X3", "c_form != c_inf", lambda x: x["cf"] != x["cinf"]),
        ("beside", "LOW's c != c_inf",
         lambda x: x["bars"]["low"] != x["cinf"]),
    )
    print(f"== {label}: {n} cells, c_inf read at {len(ok)}, arm "
          f"{len(arm)}, bars can fire at {len(fire)}")
    out = {}
    for tag, what, bad in tests:
        b = [x for x in ok if bad(x)]
        out[tag] = len(b)
        byp = {}
        for x in b:
            byp[x["p"]] = byp.get(x["p"], 0) + 1
        print(f"  {tag}: {what} at {len(b)} of {n}; arm "
              f"{sum(bad(x) for x in arm)} of {len(arm)}; where bars can fire "
              f"{sum(bad(x) for x in fire)} of {len(fire)}; by period "
              f"{dict(sorted(byp.items()))}")
        if b:
            print("     first (alpha, m, c_inf, c_ov, crude, c_form):",
                  [(x["per"], x["m"], x["cinf"], x["cov"],
                    x["bars"]["crude"], x["cf"]) for x in b[:8]])
    rd = [x for x in rows if x["read"]]
    h1 = [x for x in rd if not x["keys"]]
    out["X4"] = len(h1)
    byp = {}
    for x in rd:
        byp[x["p"]] = byp.get(x["p"], 0) + 1
    print(f"  X4 (H1): no hull key in any piece at c_ov - 2 at {len(h1)} of "
          f"{len(rd)} read cells (by period {dict(sorted(byp.items()))}): "
          f"{[(x['per'], x['m']) for x in h1[:8]]}")
    out.update(n=n, ok=len(ok), arm=len(arm), fire=len(fire), read=len(rd))
    return out


def main():
    t0 = time.time()
    only = int(sys.argv[1]) if len(sys.argv) > 1 else None
    old = [read(per, m, False) for per, m in strand_cells()[:only]]
    t1 = time.time()
    fam = family()
    if only:
        step = max(1, len(fam) // only)
        fam = fam[::step]
    X = [read(per, m, True) for per, m in fam]
    t2 = time.time()
    print("== CONTROLS")
    wset = {(tuple(per), m) for per in necklaces() for m in range(2, 13)}
    s136 = {(tuple(per), m) for _n, per in list(PERIODIC) + list(FRESH)
            for m in range(2, 10)}
    a1 = verdicts("(a) W", [x for x in old if (x["per"], x["m"]) in wset])
    a2 = verdicts("(a) the 136", [x for x in old if (x["per"], x["m"])
                                  in s136])
    a3 = verdicts("(a) the 1017", old)
    d = [x for x in X if isinstance(x["cinf"], int)
         and x["cinf"] not in (x["cov2"] - 1, x["cov2"])]
    print(f"  (b) THE PLANT c_ov's m doubled: X1's line fires at {len(d)} of "
          f"{len(X)}")
    rx = [x for x in X if x["read"]]
    pc = sum(not x["plant"] for x in rx)
    print(f"  (c) THE PLANT Z_hi := Z_lo: X4's line fires at {pc} of "
          f"{len(rx)}")
    games = []
    for per, ms in (((1, 1, 1, 2, 3), (7,)), ((1, 1, 1, 1, 2), (2, 3))):
        for m in ms:
            t3 = time.time()
            li = least(Field(per), m, "pin")
            g = game_cinf(per, m)
            games.append((per, m, li, g, round(time.time() - t3, 1)))
    print(f"  (d) THE INSTRUMENT (alpha, m, induct.least, PinGame, s): "
          f"{games}; apart {sum(g[2] != g[3] for g in games)}")
    hp = None
    for x in rx:
        F = Field(x["per"])
        hp = hull_arm(F, x["m"], x["c2"], plant=True)
        if hp[1]:
            break
    print(f"  (e) THE PLANT d_max full - 1 on the HULL arm, first read cell "
          f"where it moves a node: {hp}")
    print("== THE HULL ARM at c_ov - 2 on X's read cells (TRANSPLANT check)")
    hn = sum(x["hull"][0] for x in rx)
    ho = [x for x in rx if x["hull"][1]]
    cn = sum(x["hull"][2] for x in rx)
    co_ = [x for x in rx if x["hull"][3]]
    print(f"  nodes whose exact hull end != its form: "
          f"{sum(x['hull'][1] for x in rx)} of {hn}, at {len(ho)} cells: "
          f"{[(x['per'], x['m']) for x in ho[:8]]}")
    print(f"  pinned-closure keys outside the forms' range: "
          f"{sum(x['hull'][3] for x in rx)} of {cn}, at {len(co_)} cells: "
          f"{[(x['per'], x['m']) for x in co_[:8]]}")
    mb = [(x["per"], x["m"], x["mono"]) for x in old + X if x["mono"]]
    print(f"  (M) pinned at c, none at c + 1, c <= c_ov: at {len(mb)} cells "
          f"{mb[:4]}")
    print("== VERDICTS on X")
    v = verdicts("X", X)
    unread = [(x["per"], x["m"], x["cinf"]) for x in X
              if not isinstance(x["cinf"], int)]
    print(f"  c_inf unread (None or limit) at {len(unread)}: {unread[:8]}")
    print("== BESIDE: stranded keys' kinds at c_ov - 2 on X")
    kinds = {}
    for x in rx:
        ks = set(k[3] for k in x["keys"])
        for kd in ks:
            kinds[kd] = kinds.get(kd, 0) + 1
    print(f"  cells holding each kind: {dict(sorted(kinds.items()))}")
    for x in rx:
        if x["per"][:3] == (1, 1, 1) and x["p"] == 5 and (
                (x["per"], x["m"]) in (((1, 1, 1, 2, 3), 7),
                                       ((1, 1, 1, 3, 3), 10),
                                       ((1, 1, 1, 3, 4), 10),
                                       ((1, 1, 1, 4, 3), 12))):
            ks = sorted(set(tuple(k) for k in x["keys"]))[:12]
            print(f"  K1 {x['per']} x{x['m']} c {x['c2']} c_inf - c_ov "
                  f"{x['cinf'] - x['cov']}: keys {ks}")
    if only:
        return
    closed = sum(any(k[3].startswith("closed") for k in x["keys"]) for x in rx)
    inner = sum(any(k[3].startswith("in") for k in x["keys"]) for x in rx)
    mkc = sum(any("-Kc" in k[3] for k in x["keys"]) for x in rx)
    zero = ("THE KILL", "X1", "X2", "X3", "beside")
    checks = [
        (a1["n"], a1["arm"], a1["fire"]) == (1001, 106, 672),
        (a2["n"], a2["arm"], a2["fire"]) == (136, 17, 120),
        a3["n"] == 1017 and a3["read"] == 115 and a3["X4"] == 0
        and all(a[k] == 0 for a in (a1, a2, a3) for k in zero),
        (len(d), len(X)) == (106, 7557),
        (pc, len(rx)) == (22, 788),
        [(g[2], g[3]) for g in games] == [(5, 5), (3, 3), (5, 5)],
        hp is not None and (hp[0], hp[1]) == (12, 8),
        (hn, sum(x["hull"][1] for x in rx), cn,
         sum(x["hull"][3] for x in rx)) == (13304, 0, 201139, 0),
        mb == [],
        (v["n"], v["ok"], v["arm"], v["fire"], v["read"])
        == (7557, 7557, 826, 4737, 788)
        and all(v[k] == 0 for k in zero + ("X4",)),
        unread == [],
        (closed, inner, mkc) == (787, 788, 128),
    ]
    print(f"  {sum(checks)}/{len(checks)} checks as recorded; 1017 "
          f"{t1 - t0:.1f} s, X {t2 - t1:.1f} s, all "
          f"{time.time() - t0:.1f} s")
    sys.exit(0 if all(checks) else 1)


if __name__ == "__main__":
    main()