chain.py

"""
chain.py -- does extending a gate's graph chain gates, or free them?

QUESTION. compose.py read 169 hard triples off the point E's reach and
22 on it, each a unit and two of its own ancestors. Extended by one
and by two units, does a hard triple come apart, and does a gate's
output become another gate's input?

BY HAND (frozen before code). RF at T is Up and Down on the drop
vector: Up, each head-to-sink path's delays at most T, up-closed in
drops, its scope a chain; Down, each unit alive, down-closed in drops
(a unit's leftover reads only its cone, rises with L and each inset,
and a unit at floor is alive whatever its insets), its scope a unit
and its cone. Three pairwise incomparable units share no path clause:
an apart hard triple needs a common descendant over all three forced
to drop by a path that misses them, a corner two new units build. But
a kill on apartness (no apart hard triple, no composition) leans on
apartness being needed, and it is not: a circuit's gate o = NAND(a, b)
has o over a and b, and circuit satisfiability is a CSP of such nested
triples. Composing needs a gate whose output is of its inputs' kind.
A GATE is a hard triple one of whose units is a function of the other
two, those two reading all four patterns; with 000 and 111 out,
f(0, 0) = 1 and f(1, 1) = 0, and f = NOT of one input is binary, so a
hard gate is NAND or NOR, each complete. Its output need not be the
top: a path triple u1 < u2 < u3 reading {001, 010, 100, 101} is
u2 = NOR(u1, u3). A CHAIN at one (graph, T): gates (a, b) -> o and
(c, d) -> o2, o in {c, d}, o2 not in {a, b, o}; inputs I = {a, b} and
{c, d} less o (fan-out allowed). STRICT where the relation on I reads
all 2^|I| patterns (each gate's own relation already makes its output
a function at every point), LOOSE otherwise.

DESIGN. The base graphs are re-listed by compose.py's census (X6 at
the 441 cells, X7 at the four), every (cell, units) with a hard triple
at some T. Each is extended by one unit (an unordered pair from fresh
and its units, fresh twice skipped) and by two (the second's pair from
fresh, the units and the first; the first a fresh head only when the
second reads it), deduplicated by dags.canonical per cell, a list the
cell's ranges reject skipped. RF (compose.rf_rows) is read at every T
from the graph's naive - 1 down while non-empty.

PREDICTIONS. Loose chains exist (moderately); strict chains exist
(weakly: fan-out lets the second gate reuse the first's inputs); no
apart hard triple (moderately).

KILL (frozen). "KILL strict chains: N (extended graphs M, gates G)",
over the extensions; fires if N == 0 (gates do not chain at this
scale); UNREADABLE if G == 0 or M < 100. Beside: loose chains,
hard triples by kind (nested: one unit's cone holds the other two;
partly: not nested, some pair comparable; antichain), gates by output
position and kind, the same over the base graphs.

CONTROLS. K0 synthetic: x0, x1, x2 free, x3 = NAND(x0, x1), x4 =
NOR(x3, x2) reads one strict chain; the plant, the points with
x0 = x1 = x2 = 0 removed, reads no strict chain. K1 the path triple
reads one gate, NOR, output the middle. K2 the re-listing's hard
triples sum to 169 off and 22 on. K3 the gate graph's 6-unit prefix,
extended by one unit, holds the gate graph's class, which reads a NAND
gate at T = 7. K4 ukind reads a head as a head (added on review, its
planted break the old label). K5 a print: compose.py's c1 and c2.

FINDINGS (copied from the runs below). K0 gates [(0, 1, 3, NAND),
(2, 3, 4, NOR)], chains (loose 1, strict 1), the plant (1, 0); K1
[(0, 2, 1, NOR)]; K2 169 off, 22 on, over 182 base graphs ((4, 2, 2)
30, (11, 3, 8) 61, (6, 2, 4) 61, (8, 2, 6) 30); K3 21 one-unit
extensions, the gate graph among them, its gate (1, 2, 6) NAND.
Extensions 63,410 (9 units 60,116, 8 units 3,291, 7 units 3), RF sets
122,781. Hard triples nested 58,695, partly 3 (all at (4, 2, 2): a
unit over one of the other two, the third comparable to neither; none
a gate), antichain 0. Gates
45,687: NOR, output not top, 36,056; NOR, top, 8,629; NAND, top,
1,002 (no NAND whose output is not the top). Loose chains 0, strict 0.
Base graphs: 363 sets, 191 hard triples, all nested; 157 gates, 0
chains.
KILL strict chains: 0 (extended graphs 63410, gates 45687). FIRES,
against the weak prediction; loose chains none either, against the
moderate one; no antichain hard triple, as moderately predicted. Read
as a hard triple no unit's cone holds the other two of, apartness
reads the 3 partly nested; read as an antichain (BY HAND's "no apart
hard triple"), it reads 0. Scope: the family is the 182 graphs (6
or 7 units, four cells) that carry a hard triple in compose.py's
census (X6 at the 441 cells, X7 at the four), plus at most two units;
7-unit graphs at the other cells, bases of 8 or more units, a second
gate needing three or more new units, a base with no hard triple, and
functional triples tractable alone yet hard together are unread.
Added after the kill was read (prints by read_graph and ukind): of the
sets with a hard triple, 12,018 hold no gate, 41,584 one, 1,865 two,
122 three or more (so 1,987 sets could hold a chain); pairs of gates
in one set share an input 2,244 times (fan-out exists) and an output
1,580 times, an output of one as an input of the other 0 times. Gate
inputs sit at (z, h) units (10,637), inner
units of floor 1 or 2 (8,791; 57,205) and sinks (14,741); outputs at
inner units of floor 1 or 2 (4,808; 35,914) and sinks of floor 1
(4,965): the two roles share unit kinds, yet no unit holds both in one
set. K5: compose.py's c1 at T = 8 has hard (1, 6, 8) and (2, 6, 8),
no gate; c2 at T = 7 two NAND gates side by side, (1, 2, 6) and
(7, 8, 12), no chain. So in this family gates fan out but never feed
each other.

RUN RECORD. Controls 4/4, 0.0 s. The base census, four shards, 41.8 to
43.0 s, peak commit 31.4 MB; the plan 38.5 s, peak 124.7 MB.
Rehearsed at 50 graphs a shard, 0.1 s. Four shards, 11.3 to 11.4 s,
peak commit 99.3 to 99.9 MB in the last run (run four times as prints
were added and after the head label's fix; every count reproduced).
Rerun from code/: controls 4/4, 0.1 s, 18.4 MB.
"""
import itertools
import json
import os
import sys
import time
from collections import Counter

os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")

import dags  # noqa: E402
import graphs  # noqa: E402
from compose import (C1, C2, at, cone, cond, hard_triples,  # noqa: E402
                     heads_feed_zh, rf_rows)
from minclose import cell_named  # noqa: E402
from pairwise import jobs, seven  # noqa: E402
from schaefer import NAND1, classes_of  # noqa: E402

CHECKS = []


def check(name, ok, detail=""):
    CHECKS.append(bool(ok))
    tail = f"  ({detail})" if detail else ""
    print(f"  {'PASS' if ok else 'FAIL'}  {name}{tail}")


def drops(P, floors):
    return {tuple(int(x < f) for x, f in zip(p, floors)) for p in P}


def hard_of(D):
    """The hard triples of a drop set, compose.hard_triples' test."""
    out = []
    for U in itertools.combinations(range(len(next(iter(D)))), 3):
        R = {tuple(x[u] for u in U) for x in D}
        if (0, 0, 0) not in R and (1, 1, 1) not in R and not classes_of(R):
            out.append(U)
    return out


def gates(D, H):
    """[(a, b, o, kind)] over hard triples H: o a function of (a, b),
    (a, b) reading all four patterns; kind NAND or NOR."""
    out = []
    for U in H:
        for i in range(3):
            o = U[i]
            a, b = [u for u in U if u != o]
            f = {}
            ok = True
            for x in D:
                k = (x[a], x[b])
                if f.setdefault(k, x[o]) != x[o]:
                    ok = False
                    break
            if ok and len(f) == 4:
                kind = "NAND" if f[(0, 1)] == 1 else "NOR"
                out.append((a, b, o, kind))
    return out


def chains(D, G):
    """(loose, strict) counts of ordered gate pairs g1 -> g2."""
    loose = strict = 0
    for a, b, o, _ in G:
        for c, d, o2, _ in G:
            if o not in (c, d) or o2 in (a, b, o):
                continue
            loose += 1
            I = sorted({a, b} | ({c, d} - {o}))
            if len({tuple(x[u] for u in I) for x in D}) == 2 ** len(I):
                strict += 1
    return loose, strict


def kind(d, U):
    cones = {u: cone(d, u) for u in U}
    if any(set(U) - {u} <= cones[u] for u in U):
        return "nested"
    if any(v in cones[u] for u in U for v in U if u != v):
        return "partly"
    return "antichain"


def ukind(d, u):
    """A unit's place: head, (z, h) (fresh and a head), sink, or
    inner, with its floor."""
    a, b = d.units[u]
    heads = {j for j, x in enumerate(d.units) if tuple(x) == (None, None)}
    ins = {a, b} - {None}
    zh = None in (a, b) and len(ins) == 1 and ins <= heads
    place = ("head" if u in heads else "(z, h)" if zh
             else "sink" if not d.readers[u] else "inner")
    return f"{place}, floor {d.Ls[u]}"


def read_graph(d, out, first, tag):
    nv = d.naive()
    rows = rf_rows(d, nv - 1)
    for T in range(nv - 1, -1, -1):
        P = at(rows, T)
        if not P:
            break
        out[f"{tag} sets"] += 1
        H = hard_triples(P, d.Ls)
        if not H:
            continue
        D = drops(P, d.Ls)
        for U in H:
            out[f"{tag} hard {kind(d, U)}"] += 1
        G = gates(D, H)
        for a, b, o, k in G:
            for role, u in (("in", a), ("in", b), ("out", o)):
                out[f"{tag} gate {role} units: {ukind(d, u)}"] += 1
            top = {a, b} <= cone(d, o)
            out[f"{tag} gates {k}, output {'top' if top else 'not top'}"] += 1
        lo, st = chains(D, G)
        out[f"{tag} sets with gates {min(len(G), 3)}"] += 1
        for g, h in itertools.combinations(G, 2):
            for role in ("in in", "in out", "out out"):
                gi = set(g[:2]) if role != "out out" else {g[2]}
                hi = set(h[:2]) if role == "in in" else {h[2]}
                if role == "in out":
                    x = bool(gi & hi) or g[2] in h[:2]
                else:
                    x = bool(gi & hi)
                out[f"{tag} gate pairs sharing {role}"] += x
        out[f"{tag} gates"] += len(G)
        out[f"{tag} loose"] += lo
        out[f"{tag} strict"] += st
        if (st or any(kind(d, U) != "nested" for U in H)) and \
                sum(f[0] == tag for f in first) < 6:
            first.append([tag, graphs.name(d.cell), d.units, T, nv, d.Ls,
                          [list(g) for g in G][:6], lo, st,
                          [[list(U), kind(d, U)] for U in H][:6]])


def controls():
    print("K0, K1, K3  the instrument")
    D = set()
    for x0, x1, x2 in itertools.product((0, 1), repeat=3):
        x3 = 1 - (x0 & x1)
        D.add((x0, x1, x2, x3, 1 - (x3 | x2)))
    plant = {x for x in D if x[:3] != (0, 0, 0)}
    G, Gp = gates(D, hard_of(D)), gates(plant, hard_of(plant))
    check("K0 NAND then NOR reads a strict chain; less the 000 inputs, none",
          chains(D, G)[1] >= 1 and chains(plant, Gp)[1] == 0,
          f"gates {G}; chains {chains(D, G)}; plant {chains(plant, Gp)}")
    P = {(0, 0, 1), (0, 1, 0), (1, 0, 0), (1, 0, 1)}
    G1 = gates(P, [(0, 1, 2)])
    check("K1 the path triple is u2 = NOR(u1, u3)",
          G1 == [(0, 2, 1, "NOR")], f"{G1}")
    cell = cell_named("(4, 2, 2)")
    want = dags.canonical(NAND1)
    ext = extensions(list(NAND1[:6]), cell, two=False)
    d = dags.Dag(cell, want)
    Hd = hard_triples(at(rf_rows(d, 7), 7), d.Ls)
    Gd = gates(drops(at(rf_rows(d, 7), 7), d.Ls), Hd)
    check("K3 the prefix's one-unit extensions hold the gate graph, which "
          "reads a NAND gate at T = 7", want in ext and
          any(g[3] == "NAND" for g in Gd), f"{len(ext)} extensions; {Gd}")
    kinds = [ukind(d, u).rsplit(", floor", 1)[0] for u in range(3)]
    check("K4 ukind: unit 0 a head, units 1 and 2 (z, h)",
          kinds == ["head", "(z, h)", "(z, h)"], f"{kinds}")
    for nm, units in (("c1", C1), ("c2", C2)):
        dc = dags.Dag(cell, units)
        rows = rf_rows(dc, dc.naive() - 1)
        for T in range(dc.naive() - 1, -1, -1):
            P = at(rows, T)
            if not P:
                break
            H = hard_triples(P, dc.Ls)
            G = gates(drops(P, dc.Ls), H)
            print(f"  K5 {nm} T = {T}: RF {len(P)}, hard {H}, gates {G}, "
                  f"chains {chains(drops(P, dc.Ls), G)}")


def extensions(units, cell, two=True):
    """The classes of units extended by one unit, and by two."""
    n = len(units)
    out = set()

    def ok(us):
        try:
            dags.Dag(cell, us)
            return True
        except AssertionError:
            return False

    def pairs(m):
        xs = [None] + list(range(m))
        return [(x, y) for x, y in itertools.combinations_with_replacement(
            xs, 2) if x is None or y is None or x != y]

    for p in pairs(n):
        if p != (None, None) and ok(units + [p]):
            out.add(dags.canonical(units + [p]))
        if not two:
            continue
        for q in pairs(n + 1):
            if p == (None, None) and n not in q:
                continue
            if ok(units + [p, q]):
                out.add(dags.canonical(units + [p, q]))
    return out


def base_shard(shard, ncells):
    out, rec, conds = Counter(), {}, {}
    t0 = time.time()
    for tag, cell, cls in jobs(shard, ncells, seven()):
        if tag not in ("X6", "X7"):
            continue
        nm = graphs.name(cell)
        if nm not in conds:
            conds[nm] = cond(cell)
        for units in cls:
            try:
                d = dags.Dag(cell, units)
            except AssertionError:
                continue
            nv = d.naive()
            rows = rf_rows(d, nv - 1)
            prot = conds[nm] and heads_feed_zh(d)
            for T in range(nv - 1, -1, -1):
                P = at(rows, T)
                if not P:
                    break
                H = hard_triples(P, d.Ls)
                if not H:
                    continue
                arm = "on" if prot and T == nv - 1 else "off"
                out[arm] += len(H)
                key = json.dumps([nm, [list(u) for u in units]])
                rec.setdefault(key, Counter())[arm] += len(H)
    return out, {k: dict(v) for k, v in rec.items()}, time.time() - t0


def plan(base_paths, path):
    out, rec = Counter(), {}
    for p in base_paths:
        with open(p, encoding="utf-8") as fh:
            r = json.load(fh)
        out.update(r["out"])
        rec.update(r["rec"])
        print(f"  {os.path.basename(p)}: {r['secs']:.1f} s")
    print(f"  base graphs {len(rec)}: by cell "
          f"{dict(Counter(json.loads(k)[0] for k in rec))}")
    for k, v in sorted(rec.items()):
        print(f"    {k} {v}")
    check("K2 the re-listing's hard triples: 169 off, 22 on",
          out["off"] == 169 and out["on"] == 22, f"{dict(out)}")
    t0 = time.time()
    base = {}
    ext = {}
    for k in rec:
        nm, units = json.loads(k)
        units = [tuple(u) for u in units]
        base.setdefault(nm, set()).add(dags.canonical(units))
        ext.setdefault(nm, set()).update(
            extensions(units, cell_named(nm)))
    jobs_ = []
    for nm in sorted(ext):
        for c in sorted(ext[nm] - base[nm], key=str):
            jobs_.append([nm, [list(u) for u in c]])
    bjobs = [[nm, [list(u) for u in c]] for nm in sorted(base)
             for c in sorted(base[nm], key=str)]
    print(f"  extensions {len(jobs_)} (by size "
          f"{dict(Counter(len(j[1]) for j in jobs_))}), "
          f"{time.time() - t0:.1f} s")
    with open(path, "w", encoding="utf-8", newline="\n") as fh:
        json.dump({"ext": jobs_, "base": bjobs}, fh)


def ext_shard(plan_path, shard, limit):
    with open(plan_path, encoding="utf-8") as fh:
        pl = json.load(fh)
    out, first = Counter(), []
    t0 = time.time()
    for tag in ("base", "ext"):
        js = pl[tag][shard::4]
        if limit:
            js = js[:limit]
        for nm, units in js:
            d = dags.Dag(cell_named(nm), [tuple(u) for u in units])
            out[f"{tag} graphs"] += 1
            read_graph(d, out, first, tag)
    return out, first, time.time() - t0


def report(paths):
    out, first = Counter(), []
    for p in paths:
        with open(p, encoding="utf-8") as fh:
            r = json.load(fh)
        out.update(r["out"])
        first += r["first"]
        print(f"  {os.path.basename(p)}: {r['secs']:.1f} s")
    for k in sorted(out):
        print(f"  {k}: {out[k]}")
    for f in first:
        print(f"    {f}")
    N, M, G = out["ext strict"], out["ext graphs"], out["ext gates"]
    tail = "  UNREADABLE" if G == 0 or M < 100 else ""
    print(f"KILL strict chains: {N} (extended graphs {M}, gates {G}){tail}")


def dump(path, rec):
    with open(path, "w", encoding="utf-8", newline="\n") as fh:
        json.dump(rec, fh)


def main(argv):
    t0 = time.time()
    if argv and argv[0] == "--bases":
        out, rec, secs = base_shard(int(argv[1]), int(argv[2]))
        dump(argv[3], {"out": dict(out), "rec": rec, "secs": secs})
        print(f"bases shard {argv[1]}: {secs:.1f} s, {len(rec)} graphs")
        return 0
    if argv and argv[0] == "--plan":
        plan(argv[2:], argv[1])
        return 0 if all(CHECKS) else 1
    if argv and argv[0] == "--ext":
        out, first, secs = ext_shard(argv[1], int(argv[2]), int(argv[3]))
        dump(argv[4], {"out": dict(out), "first": first, "secs": secs})
        print(f"ext shard {argv[2]}: {secs:.1f} s")
        return 0
    if argv and argv[0] == "--merge":
        report(argv[1:])
        return 0
    controls()
    if not all(CHECKS):
        print("\nCONTROL FAILED: nothing below is read.")
        return 1
    print(f"\n{sum(CHECKS)}/{len(CHECKS)} checks, {time.time() - t0:.1f} s")
    return 0


if __name__ == "__main__":
    sys.exit(main(sys.argv[1:]))