choice.py
Checks: LATENCY: Trees of units property; rule; theorem; observation.
Cited on: LATENCY.
To run it: save choice.py, with chains.py, dags.py, graphs.py, manystream.py, median.py, minclose.py, poles.py, redundant.py, sublattice.py beside it; needs numpy.
"""
choice.py -- is a gain below naive ever a choice of raises?
QUESTION. A delay set F (every unit's delays alive at latency at most
T, brute's window 0..L*+3) at T below naive with no RAISE-FREE point
(every unit at or below its floor) is a GAIN NEEDING A RAISE. glue.py
found 101 at Y4, Y5 and X6 (X6 at three cells), each with one least
raised set over the whole set. Is any gain a CHOICE: two minimal
raised sets buying the same drop?
KEYING. Per point p, D(p) the units below their floors, R(p) those
above. F's points grouped by D(p) exactly; a CHOICE at D when the
minimal elements of {R(p) : D(p) = D} number two or more. A set counts
once if it holds a choice at any D. Beside it the SET-LEVEL count
(minimal R over all of F, glue.py's), which also reads two gains each
forced as a choice: printed, not the kill.
ARMS. HAND: h = (z, z), c = (z, h), a chain x1 = (z, z), x2 = (z, x1)
[, x3 = (z, x2)], r = (c, x_last), 5 and 6 units, a tree, at the 441
cells. X6: minclose.six() at the 441 cells, sharded by cell index mod
4, rehearsed at 10 cells first.
BY HAND (frozen before code). v_r rises in each inset; c's inset rises
in L_c and, through h's inset, in L_h. Where x's path is longer than
c's, c has slack, so either raise alone fits; if either alone lifts r's
leftover over 0 at L*_r - 1, the drop {r} has minimal raised sets {h}
and {c}. A unit's two inputs cannot both be in slack while it is
critical, so a raise OR must be two units on one input's side.
TRANSPLANT: a raise lifts the inset where the room does not bind.
PREDICTIONS. HAND gains with a choice at some cell (weakly); X6 at 441
cells holds a choice (weakly); every choice found is two ancestors on
one input's side (moderately).
KILL (frozen). "KILL gains below naive with a choice of raises: N
(gains needing a raise M)" over HAND and X6 together, N per drop;
fires if N == 0, UNREADABLE if M < 10.
CONTROLS. K1 synthetic, floors (2, 2, 2): {(3, 2, 1), (2, 3, 1)} a
choice at D = {2}; {(3, 2, 1), (3, 3, 1)} forced; {(3, 2, 1),
(2, 3, 2)} no choice per drop (D differ) and a choice set-level. K2 X6
at the three cells reproduces glue.py's 94 gains needing a raise, all
forced set-level. K3 a plant: each K2 set with a point added, its
forced raise moved to another unit at its floor, same D, read back as
a choice.
FINDINGS (copied from the runs below). K1 passes; K2 94 gains needing
a raise at the three cells, 94 forced set-level (glue.py's X6 count);
K3 94 of 94 moved raises read back as a choice (by construction, it
tests the grouping on real sets). K4 (added at the audit: a found
choice's key was a tuple, which json cannot dump, so --shard would have
crashed on the first choice) passes.
HAND: below-naive sets 26 (hand2) and 33 (hand3), gains needing a
raise 0 at both (hand2's chain matches h, c, so c has no slack there;
hand3 is the shape the argument wants): the shape gains, always with a point that raises
nothing, so its drop is bought by drops alone.
X6 at the 441 cells: below-naive sets 33,500, gains needing a raise
102, choice per drop 0, set-level choice 0.
KILL gains below naive with a choice of raises: 0 (gains needing a
raise 102). FIRES; both predictions of a choice were wrong, and the
third (a choice is two ancestors on one side) is unread.
Added after the kill was read: the 102 by cell, (6, 2, 4) 72,
(35, 8, 27) 20, (4, 2, 2) 2, and 8 off the three cells, (9, 2, 7) 2,
(18, 3, 15) 2, (36, 5, 31) 2, (10, 5, 5) 1, (6, 3, 3) 1; by naive - T,
99 at 1 and 3 at 2 (each first printed raises one unit).
The first at (10, 5, 5): h, a = (z, h), b = (z, a), c = (z, b),
(h, a), (c, (h, a)) at T = 5 against 6, floors (2, 1, 1, 1, 1, 1), the
unit (h, a), read only by the sink, raised. So over X6 at the 441
cells a gain below naive is decided by drops alone or by a forced
raise, at 8 cells. Keyed per exact drop set, a choice layered over a
forced set, or two raised sets buying one unit's drop beside
different further drops, is unread.
RUN RECORD. Controls 3/3 (before K4), 5.8 s, peak commit 19.2 MB. HAND 1.8 s.
X6 rehearsed at 10 cells, 19.0 s (2 gains needing a raise); then four
shards by cell mod 4, 191.5 to 203.6 s each, peak commit 20.3 MB;
rerun with the by-cell print, 192.2 to 200.5 s, the same counts. In
code/: four shards, 192.5 to 202.8 s, every X6 count above reproduced.
"""
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
import median # noqa: E402
import sublattice as sl # noqa: E402
from minclose import CELLS, cell_named, six # noqa: E402
CHECKS = []
HAND = (
("hand2", ((None, None), (None, 0), (None, None), (None, 2), (1, 3))),
("hand3", ((None, None), (None, 0), (None, None), (None, 2), (None, 3),
(1, 4))),
)
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 minimal(sets_):
sets_ = set(sets_)
return sorted((r for r in sets_ if not any(q < r for q in sets_)),
key=lambda r: sorted(r))
def read(P, floors):
"""(raise_free, per-drop choices {D: minimal Rs} with two or more,
set-level minimal Rs)."""
by = {}
allr = set()
free = False
for p in P:
D = frozenset(u for u, (x, f) in enumerate(zip(p, floors)) if x < f)
R = frozenset(u for u, (x, f) in enumerate(zip(p, floors)) if x > f)
free |= not R
by.setdefault(D, set()).add(R)
allr.add(R)
ch = {D: minimal(Rs) for D, Rs in by.items() if len(minimal(Rs)) > 1}
return free, ch, minimal(allr)
def sweep_one(tag, cell, units, out, first):
try:
d = dags.Dag(cell, units)
except AssertionError:
out[(tag, "skipped")] += 1
return
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"]
out[(tag, "below")] += 1
free, ch, mins = read(P, d.Ls)
if free:
continue
out[(tag, "M")] += 1
# added after the kill was read: where they sit, and the first
out[(tag, "M", graphs.name(cell))] += 1
out[(tag, "M gap", nv - T)] += 1
if len(first.setdefault("M " + tag, [])) < 12:
first["M " + tag].append((graphs.name(cell), units, T, nv, d.Ls,
[sorted(r) for r in mins]))
if len(mins) > 1:
out[(tag, "set-level choice")] += 1
if ch:
out[(tag, "N")] += 1
out[(tag, "N", graphs.name(cell))] += 1
if len(first.setdefault(tag, [])) < 6:
first[tag].append((graphs.name(cell), units, T, nv, d.Ls,
{str(sorted(D)): [sorted(r) for r in Rs]
for D, Rs in ch.items()}))
def controls():
print("K1..K4 the instrument")
f = (2, 2, 2)
a = read({(3, 2, 1), (2, 3, 1)}, f)
b = read({(3, 2, 1), (3, 3, 1)}, f)
c = read({(3, 2, 1), (2, 3, 2)}, f)
check("K1 synthetic: a choice, forced, set-level only",
(not a[0]) and set(a[1]) == {frozenset({2})}
and not b[1] and len(b[2]) == 1
and not c[1] and len(c[2]) == 2,
f"{a[1]}, {b[1]}/{b[2]}, {c[1]}/{c[2]}")
M = forced = 0
planted = caught = 0
for cell in [cell_named(nm) for nm in CELLS]:
for units in six():
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"]
free, ch, mins = read(P, d.Ls)
if free:
continue
M += 1
forced += len(mins) == 1
# K3: move the forced raise of one point to a unit at
# its floor outside D, same D
p = next(iter(sorted(P)))
Dp = {u for u in range(d.n) if p[u] < d.Ls[u]}
Rp = [u for u in range(d.n) if p[u] > d.Ls[u]]
vs = [v for v in range(d.n) if p[v] == d.Ls[v]]
if not vs:
continue
q = list(p)
for u in Rp:
q[u] = d.Ls[u]
q[vs[0]] += 1
q = tuple(q)
if q in P:
continue
planted += 1
_, ch2, _ = read(P | {q}, d.Ls)
caught += frozenset(Dp) in ch2
check("K2 X6 at the three cells: 94 gains needing a raise, all "
"forced set-level", M == 94 and forced == 94, f"{M}, {forced}")
check("K3 a moved raise read back as a choice", planted >= 10
and caught == planted, f"{caught} of {planted}")
# K4 (added at the audit): a shard's record with a choice in it
# survives dump and merge
import tempfile
out, first = Counter(), {}
d = dags.Dag(cell_named("(6, 2, 4)"), six()[0])
out[("X6", "N")] += 1
first["X6"] = [("(6, 2, 4)", six()[0], 5, 6, d.Ls,
{str(sorted(D)): [sorted(r) for r in Rs]
for D, Rs in a[1].items()})]
path = os.path.join(tempfile.mkdtemp(), "k4.json")
try:
dump(path, out, first, 0.0, 1)
back, bf = merge([path])
ok = back[("X6", "N")] == 1 and len(bf["X6"]) == 1
except TypeError as e:
ok = False
print(f" K4: {e}")
check("K4 a record holding a choice dumps and merges", ok)
def run(arm, shard, ncells):
cells_ = list(graphs.cells())
if ncells:
step = max(1, len(cells_) // ncells)
cells_ = cells_[::step][:ncells]
out, first = Counter(), {}
t0 = time.time()
nrun = 0
for i, cell in enumerate(cells_):
if shard is not None and i % 4 != shard:
continue
nrun += 1
if arm == "hand":
for tag, units in HAND:
sweep_one(tag, cell, units, out, first)
else:
for units in six():
sweep_one("X6", cell, units, out, first)
return out, first, time.time() - t0, nrun
def dump(path, out, first, secs, n):
rec = {"out": [[list(k), v] for k, v in out.items()],
"first": first, "secs": secs, "cells": n}
with open(path, "w", encoding="utf-8", newline="\n") as fh:
json.dump(rec, fh, default=str)
def merge(paths):
out, first = Counter(), {}
for p in paths:
with open(p, encoding="utf-8") as fh:
rec = json.load(fh)
for k, v in rec["out"]:
out[tuple(k)] += v
for tag, xs in rec["first"].items():
first.setdefault(tag, []).extend(xs)
print(f" {os.path.basename(p)}: {rec['cells']} cells, "
f"{rec['secs']:.1f} s")
return out, first
def report(out, first):
tags = sorted({k[0] for k in out})
for tag in tags:
print(f" {tag}: below-naive sets {out[(tag, 'below')]}, gains "
f"needing a raise {out[(tag, 'M')]}, choice per drop "
f"{out[(tag, 'N')]}, set-level choice "
f"{out[(tag, 'set-level choice')]}, skipped "
f"{out[(tag, 'skipped')]}")
cells_ = {k[2]: v for k, v in out.items()
if k[0] == tag and k[1] == "N" and len(k) == 3}
if cells_:
print(f" choices by cell {cells_}")
ms = {k[2]: v for k, v in out.items()
if k[0] == tag and k[1] == "M" and len(k) == 3}
gp = {k[2]: v for k, v in out.items()
if k[0] == tag and k[1] == "M gap"}
if ms:
print(f" gains needing a raise by cell {dict(sorted(ms.items()))}"
f"; by naive - T {dict(sorted(gp.items()))}")
seen = set()
for x in first.get("M " + tag, []):
if x[0] not in seen:
seen.add(x[0])
print(f" first needing a raise at {x[0]}: {x[1:]}")
for x in first.get(tag, [])[:6]:
print(f" choice {x}")
N = sum(out[(t, "N")] for t in tags)
M = sum(out[(t, "M")] for t in tags)
print(f"KILL gains below naive with a choice of raises: {N} (gains "
f"needing a raise {M}){' UNREADABLE' if M < 10 else ''}")
def main(argv):
t0 = time.time()
if argv and argv[0] == "--merge":
out, first = merge(argv[1:])
report(out, first)
return 0
if argv and argv[0] == "--shard":
arm, shard, ncells, path = argv[1], int(argv[2]), int(argv[3]), \
argv[4]
out, first, secs, n = run(arm, None if shard < 0 else shard, ncells)
dump(path, out, first, secs, n)
print(f"{arm} shard {shard}: {secs:.1f} s")
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:]))