glue.py
Checks: LATENCY: Trees of units property; rule; observation.
Cited on: LATENCY.
To run it: save glue.py, with chains.py, dags.py, graphs.py, manystream.py, median.py, minclose.py, poles.py, raises.py, redundant.py, sublattice.py beside it; needs numpy.
"""
glue.py -- do the least witness's clauses survive gluing?
QUESTION. The least witness W at (6, 2, 4) (h, c = (z, h),
r = (h, c)) forces one prime 3-unit clause in delays at latency 6,
[L_h >= 3] or [L_c >= 3] or [L_r >= 2]. Glued twice, in parallel (one
h, two (c, r) pairs) and in series (r1 as copy 2's head), does each
copy keep its clause, and does the composite force anything the copies
do not, read through the shared unit?
DESIGN (frozen before code). F the composite's FD set at T
(median.sets), F1, F2 its projections on each copy's units, S the
shared unit, J = F1 joined to F2 on S. F lies in J; the join excess
|J \\ F| counts what the copies do not imply. A copy is kept when its
box (C2's, carried) is a prime clause of F (raises.clauses). Series
copy 2's box: r1 at its hull low in F, c2 at its floor 2, r2 below its
floor 1. Beside the kill, BUDGET-ONLY: is F the join of the uncapped
alive set's projections, cut by the latency, so that r1's leftover
carries copy 1 into copy 2 only through L_r1?
PREDICTIONS. Parallel kept 2, excess 0 (by construction). Series:
excess > 0 at its least latency, new clauses caps across the copies
(the path budget); copy 1 lost there (weakly), copy 2 kept (weakly);
BUDGET-ONLY holds (weakly).
KILL (frozen). "KILL parallel: copy clauses kept K of 2, new N" and
the same for series, N the join excess, at each gluing's least
latency; fires if K < 2 or N > 0 in either.
CONTROLS. G1 the bare witness at 6 reads exactly C2's clause, its join
with itself excess 0. G2 parallel reads K = 2, N = 0 at every latency
(a known yes: both copies are ancestor-closed). G3 a set of two
points whose copies agree on the shared unit but vary apart reads its
join excess, the two cross points, by hand.
FINDINGS (copied from the run below). G1 the witness's one clause
((2, 2), (2, 2), (1, 1)), excess 0; G2 parallel off nowhere (latency
6 only); G3 the two cross points read. (First run: G3 deleted a
point whose projections kept other witnesses, which reads excess 1 by
construction; replaced at the audit.)
Parallel, floors 2 each, least = naive = 6: |F| 5, |J| 5, excess 0,
6 prime 3-unit clauses, both copies kept (four more: resolvents
through h, kinds R.D.C or C.R.D).
Series, floors (2, 2, 2, 2, 1), least = naive = 9: |F| 4, |J| 4,
excess 0, one prime 3-unit clause (copy 1's), copy 2's box lost:
r2's hull is [1, 1], it never drops. BUDGET-ONLY 0 and 0.
KILL parallel: copy clauses kept 2 of 2, new 0
KILL series: copy clauses kept 1 of 2, new 0
FIRES, on series copy 2's box only. Added after the kill was read,
delays less floors at the least latency: parallel (0,0,0,0,0),
(0,0,0,1,-1), (0,1,-1,0,0), (0,1,-1,1,-1), (1,0,-1,0,-1); series
(0,0,0,0,0), (0,0,1,-1,0), (0,1,-1,0,0), (1,0,-1,0,0).
So the predictions split: parallel as derived; series' excess 0
(predicted > 0, wrong: at its least latency r1 alone fixes copy 2's
delays), copy 1 kept (predicted lost, wrong), BUDGET-ONLY held. Copy
2's drop moves to c2, guarded by r1 raised: a two-unit clause, the
witness's mechanism one unit up. In both gluings each point's raises
and drops cancel along every longest path (h, c, r of each copy;
series' one path through all five), and the least latency is the
naive one: the floors are alive there, so these clauses describe the
set without making its emptiness a question.
BELOW NAIVE (frozen after the gluing kill was read). Is
that so of the census? raises.py's prime 3-unit clauses over the 990
non-median-closed FD sets of Y5 and X6, split by T < naive (dags.Dag
asserts the floors alive at naive). KILL "D.R.R. clauses below naive:
N (sets below naive M, their clauses K)", fires if N == 0, UNREADABLE
if M == 0. Control B1: the split's totals are raises.py's.
Predicted: below-naive sets a minority (moderately); D.R.R. among them
(weakly). From the run: B1 990 sets, 3,063 clauses. At naive 933 sets,
2,997 clauses (C.C.C. 1,562, D.R.R. 915, C.D.R. 339, C.C.D. 157,
C.C.R. 12, D.D.R. 9, C.D.D. 2, C.R.R. 1). Below naive 57 sets (X6
54, Y5 3), 66 clauses: D.R.R. 56 (X6 53, Y5 3), C.C.C. 6, C.D.R. 3,
C.R.R. 1.
KILL D.R.R. clauses below naive: 56 (non-median-closed sets below
naive 57, their prime 3-unit clauses 66). MISSES; both predictions
held. Where the latency is below naive the forced clauses are
nearly all a drop guarded by two raises, and the caps nearly all sit
at naive (1,562 of 1,568). The first D.R.R. below naive: X6, (6, 2, 4), heads
h0, h1, u2 = (z, h0), u3 = (h0, u2), u4 = (h1, u3), u5 = (z, u4),
T = 8 against naive 9, its clause on (h0, u2, u3) with sides (2, 2),
(2, 2), (1, 1): the least witness's own clause, the witness read on by
two units in a graph that gains.
GUARDED GAINS (frozen after the census was read). A D.R.R.
clause holds wherever r does not drop, so a set with a RAISE-FREE point
(every unit at or below its floor) is decided by drops alone. Over
every FD set below naive (Y4, Y5, X6), does some set hold none? KILL
"below-naive FD sets with no raise-free point: N (M)", fires if
N == 0. Control R1: the witness at 6 less its floors point reads none,
with it one. Predicted N == 0 (moderately). From the run: R1 passes.
KILL below-naive FD sets with no raise-free point: 101 (below-naive FD
sets 3837). MISSES; the prediction was wrong. Added after the kill
was read: X6 94, Y5 7, Y4 none; every one has a single minimal set of
raised units (one unit in 100, two in 1), so the raise is forced and
no gain offers a choice. By naive - T: X6 91 at 1, 3 at 2; Y5 7 at 1. The first: X6, (6, 2, 4), heads h0, h1, h2,
u3 = (z, h0), u4 = (h0, h1), u5 = (h2, u3), T = 5 against naive 6,
every point raising h2 to 3 or 4 and dropping u5 to 1: h2 arrives
early, so its raise spends slack and buys the drop. A gain that needs
a raise exists from 5 units; a gain guarded by an OR of raises, the
choice a reduction would build a variable from, does not appear to 6
units at the three cells (to 5 at the 34).
RUN RECORD. main: 3/3 checks, 0.0 s; under a memory cap, peak commit
19.2 MB. With BELOW NAIVE: 4/4 checks, 22.8 s, peak commit 20.1 MB.
With GUARDED GAINS: 5/5 checks, 37.4 s, peak commit 20.6 MB. After
the audit (G3 replaced, clauses and the gap split printed): 5/5
checks, 37.3 s, peak commit 20.6 MB. In code/: 5/5 checks, 37.5 s,
20.9 MB, every count above reproduced.
"""
import os
import sys
import time
os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")
import dags # noqa: E402
import graphs # noqa: E402
import median # noqa: E402
import raises # noqa: E402
import sublattice as sl # noqa: E402
from minclose import cell_named # noqa: E402
CHECKS = []
CELL = "(6, 2, 4)"
WITNESS = ((None, None), (None, 0), (0, 1))
# name, units, copies (unit indices, in witness order h, c, r), shared
GLUES = (
("parallel", ((None, None), (None, 0), (0, 1), (None, 0), (0, 3)),
((0, 1, 2), (0, 3, 4)), (0,)),
("series", ((None, None), (None, 0), (0, 1), (None, 2), (2, 3)),
((0, 1, 2), (2, 3, 4)), (2,)),
)
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 proj(P, U):
return {tuple(p[u] for u in U) for p in P}
def join(P, copies, shared):
"""The points of the full space whose projection on each copy lies
in P's projection there (copies cover every unit)."""
A, B = copies
PA, PB = proj(P, A), proj(P, B)
n = len(next(iter(P)))
out = set()
for a in PA:
for b in PB:
p = [None] * n
ok = True
for U, v in ((A, a), (B, b)):
for u, x in zip(U, v):
if p[u] is not None and p[u] != x:
ok = False
p[u] = x
if ok:
out.add(tuple(p))
return out
def box(P, U, tops):
"""The clause box on units U, sides (hull low, top)."""
return (tuple(U), tuple((min(p[u] for p in P), t)
for u, t in zip(U, tops)))
def wanted(name, P, copies):
"""The copies' boxes as frozen."""
out = [box(P, copies[0], (2, 2, 1))]
if name == "parallel":
out.append(box(P, copies[1], (2, 2, 1)))
else:
r1 = copies[1][0]
lo = min(p[r1] for p in P)
out.append(box(P, copies[1], (lo, 2, 0)))
return out
def new_clauses(P, J):
"""Prime 3-unit clauses of P whose box meets J's projection."""
out = []
for U, sides in raises.clauses(P):
hit = any(all(s <= q[u] <= t for u, (s, t) in zip(U, sides))
for q in J)
if hit:
out.append((U, sides))
return out
def controls():
print("G1..G3 the instrument")
d = dags.Dag(cell_named(CELL), WITNESS)
rows = sl.alive_all(d, d.naive())
P = median.sets(d, d.naive(), rows, 6)["FD"]
cl = raises.clauses(P)
want = [box(P, (0, 1, 2), (2, 2, 1))]
ex = len(join(P, ((0, 1, 2), (0, 1, 2)), None) - P)
check("G1 the bare witness at 6: exactly C2's clause, self-join "
"excess 0", cl == want and ex == 0, f"{cl}, excess {ex}")
name, units, copies, shared = GLUES[0]
d = dags.Dag(cell_named(CELL), units)
nv = d.naive()
rows = sl.alive_all(d, nv)
least = min(r[0] for r in rows)
bad = []
for T in range(least, nv + 1):
P = median.sets(d, nv, rows, T)["FD"]
cl = set(raises.clauses(P))
K = sum(w in cl for w in wanted(name, P, copies))
N = len(join(P, copies, shared) - P)
if (K, N) != (2, 0):
bad.append((T, K, N))
check("G2 parallel: kept 2, excess 0 at every latency", not bad,
f"latencies {least}..{nv}, off {bad}")
# by hand: copy 1 {(0,0,0), (1,0,0)} and copy 2 {(0,0,0), (0,1,1)}
# agree on unit 2 everywhere, so the join is their 2 x 2 product
P = {(0, 0, 0, 0, 0), (1, 0, 0, 1, 1)}
ex = sorted(join(P, ((0, 1, 2), (2, 3, 4)), None) - P)
check("G3 a set whose copies vary apart: excess (0, 0, 0, 1, 1), "
"(1, 0, 0, 0, 0) by hand",
ex == [(0, 0, 0, 1, 1), (1, 0, 0, 0, 0)], f"{ex}")
def budget_only(d, copies, T):
"""Points of (A1 joined A2, cut at latency T) not in F, and the
reverse, A the uncapped alive set (delays, arrivals)."""
rows = sl.alive_all(d, 10 ** 6)
A = {r[1]: r[0] for r in rows}
full = set(A)
J = join(full, copies, None)
F = {p for p, lat in A.items() if lat <= T}
# latency of a joined point: a series graph's path sum
Jc = {p for p in J if sum(p) <= T}
return len(Jc - F), len(F - Jc)
def below_naive():
"""raises.py's census split by T < naive (frozen after
the gluing kill was read)."""
from collections import Counter
n = Counter()
first = {}
for tag, cls, cells_ in median.populations():
if tag == "Y4":
continue
for cell in cells_:
for units in cls:
d = dags.Dag(cell, units)
nv = d.naive()
rows = sl.alive_all(d, nv)
least = min(r[0] for r in rows)
for T in range(least, nv + 1):
P = median.sets(d, nv, rows, T)["FD"]
if len(P) < 3 or median.fast(P)[0]:
continue
arm = "below" if T < nv else "naive"
n[(arm, "sets")] += 1
# added after the kill was read: by population
n[("pop", arm, tag)] += 1
for cl in raises.clauses(P):
tg = raises.kinds(P, d.Ls, cl)
pat = "".join(sorted(t.ljust(2, ".") for t in tg))
n[(arm, "clauses")] += 1
n[(arm, pat)] += 1
n[("pop", arm, tag, pat)] += 1
if arm == "below":
first.setdefault(pat, (tag, graphs.name(cell),
units, T, nv, cl))
for arm in ("naive", "below"):
pats = {k[1]: v for k, v in sorted(n.items())
if k[0] == arm and k[1] not in ("sets", "clauses")}
pop = {k[2:]: v for k, v in sorted(n.items())
if k[0] == "pop" and k[1] == arm}
print(f" {arm}: sets {n[(arm, 'sets')]}, prime 3-unit clauses "
f"{n[(arm, 'clauses')]}, patterns {pats}")
print(f" by population {pop}")
for k in sorted(first):
print(f" first below naive {k}: {first[k]}")
tot_s = n[("naive", "sets")] + n[("below", "sets")]
tot_c = n[("naive", "clauses")] + n[("below", "clauses")]
check("B1 the split's totals are raises.py's 990 sets, 3,063 clauses",
(tot_s, tot_c) == (990, 3063), f"{tot_s}, {tot_c}")
M, K = n[("below", "sets")], n[("below", "clauses")]
print(f"KILL D.R.R. clauses below naive: {n[('below', 'D.R.R.')]} "
f"(non-median-closed sets below naive {M}, their prime 3-unit "
f"clauses {K}){' UNREADABLE' if M == 0 else ''}")
def raise_free(P, floors):
"""Does P hold a point with every unit at or below its floor?"""
return any(all(x <= f for x, f in zip(p, floors)) for p in P)
def guarded_gains():
"""Every FD set below naive: does it hold a raise-free point
(frozen after the census was read)?"""
w = sorted(((2, 3, 1), (3, 2, 1)))
check("R1 the witness less its floors point reads no raise-free "
"point; with it, one", not raise_free(w, (2, 2, 2))
and raise_free(w + [(2, 2, 2)], (2, 2, 2)))
from collections import Counter
M = N = 0
first = None
by, sizes, choice, gap = Counter(), Counter(), [], Counter()
for tag, cls, cells_ in median.populations():
for cell in cells_:
for units in cls:
d = dags.Dag(cell, units)
nv = d.naive()
rows = sl.alive_all(d, nv)
least = min(r[0] for r in rows)
for T in range(least, nv):
P = median.sets(d, nv, rows, T)["FD"]
M += 1
if not raise_free(P, d.Ls):
N += 1
# added after the kill was read: by population,
# and the minimal sets of raised units (more
# than one: a choice among raises)
rs = {frozenset(u for u, (x, f) in
enumerate(zip(p, d.Ls)) if x > f)
for p in P}
mins = [r for r in rs if not any(q < r for q in rs)]
arm = "choice" if len(mins) > 1 else "forced"
by[(tag, arm)] += 1
gap[(tag, nv - T)] += 1
sizes[max(len(r) for r in mins)] += 1
if len(mins) > 1 and not choice:
choice.append((tag, graphs.name(cell), units, T,
nv, sorted(sorted(r)
for r in mins)))
first = first or (tag, graphs.name(cell), units,
T, nv, d.Ls, len(P), sorted(P))
if first:
print(f" first with no raise-free point: {first}")
print(f" by population: {dict(sorted(by.items()))}; largest minimal "
f"raise set: {dict(sorted(sizes.items()))}; by naive - T: "
f"{dict(sorted(gap.items()))}")
if choice:
print(f" first with a choice: {choice[0]}")
print(f"KILL below-naive FD sets with no raise-free point: {N} "
f"(below-naive FD sets {M}){' UNREADABLE' if M < 10 else ''}")
def main():
t0 = time.time()
controls()
if not all(CHECKS):
print("\nCONTROL FAILED: nothing below is read.")
return 1
kill = {}
for name, units, copies, shared in GLUES:
d = dags.Dag(cell_named(CELL), units)
nv = d.naive()
rows = sl.alive_all(d, nv)
least = min(r[0] for r in rows)
print(f"\n{name} floors {d.Ls}, latencies {least}..{nv}, "
f"copies {copies}, shared {shared}")
for T in range(least, nv + 1):
P = median.sets(d, nv, rows, T)["FD"]
if len(P) < 2:
print(f" T {T}: |F| {len(P)}")
continue
cl = raises.clauses(P)
have = set(cl)
ws = wanted(name, P, copies)
kept = [w in have for w in ws]
J = join(P, copies, shared)
N = len(J - P)
nc = new_clauses(P, J)
print(f" T {T}: |F| {len(P)}, |J| {len(J)}, excess {N}, "
f"prime 3-unit clauses {len(cl)}, kept {kept}")
for w, k in zip(ws, kept):
if not k:
near = [c for c in cl if c[0] == w[0]]
print(f" lost {w}; on its units: "
f"{[(c, raises.kinds(P, d.Ls, c)) for c in near]}")
for c in nc:
print(f" new {c} {raises.kinds(P, d.Ls, c)}")
# added at the audit: every prime 3-unit clause, by kind
for c in cl:
print(f" clause {c} {raises.kinds(P, d.Ls, c)}")
if name == "series":
over, under = budget_only(d, copies, T)
print(f" BUDGET-ONLY: joined and cut, not in F {over}; "
f"in F, not joined {under}")
if T == least:
kill[name] = (sum(kept), N)
if T == least and N:
print(f" the excess at the least latency: "
f"{sorted(J - P)[:12]}")
if T == least:
# added after the kill was read: the set itself, and
# each point's delays less the floors
for p in sorted(P):
print(f" F {p} less floors "
f"{tuple(x - f for x, f in zip(p, d.Ls))}")
print()
for name in ("parallel", "series"):
K, N = kill[name]
print(f"KILL {name}: copy clauses kept {K} of 2, new {N}")
fired = any(K < 2 or N > 0 for K, N in kill.values())
print("FIRES" if fired else "MISSES")
print("\nBELOW NAIVE raises.py's census split by latency")
below_naive()
print("\nGUARDED GAINS every FD set below naive")
guarded_gains()
print(f"\n{sum(CHECKS)}/{len(CHECKS)} checks, {time.time() - t0:.1f} s")
return 0
if __name__ == "__main__":
sys.exit(main())