src/paper.py

"""The checks and runs behind the paper's statements, one command each, each writing its record."""
from __future__ import annotations

import argparse
import concurrent.futures as cf
import hashlib
import itertools
import json
import os
import random
import re
import shutil
import struct
import subprocess
import sys
import tempfile
import time
from array import array
from collections import Counter, defaultdict
from typing import Dict, List, Tuple

import torch

from host import (
    describe,
    describe_literal,
    decode,
    Tape,
    C_WR,
    C_EOT,
    C_RW,
    C_RD,
    R_IN,
    R_OUT,
    run_reference,
    M_P,
    NetEvaluator,
    read_host,
    ser,
    inst,
    lam,
    HOST_PATH,
    M_STAR,
    tau_star,
    HALT_PC,
    net_of_sigma,
    sigma_of_net,
    STATE_LAYOUT,
    IO_CELLS,
    host_netlist,
    sigma_host,
    P,
    P_STAR,
    LevEvaluator,
)


REPO = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))

SRC = os.path.join(REPO, "src")


def runs_path(name: str) -> str:
    d = os.path.join(REPO, "paper", "runs")
    os.makedirs(d, exist_ok=True)
    return os.path.join(d, name)


def parse_sigma(data: bytes):
    """Biases, predecessor lists and next-state indices from a serialization."""
    hlen = struct.unpack("<Q", data[:8])[0]
    head = json.loads(data[8:8 + hlen])
    T = {}
    for k, spec in head.items():
        if k == "__metadata__":
            continue
        lo, hi = spec["data_offsets"]
        a = array({"I8": "b", "I16": "h", "I32": "i"}[spec["dtype"]])
        a.frombytes(data[8 + hlen + lo:8 + hlen + hi])
        if sys.byteorder != "little":
            a.byteswap()
        T[k] = list(a)
    bias, fanin, pred, nxt = T["net.bias"], T["net.fanin"], T["net.pred"], T["net.next"]
    units, p = [], 0
    for j in range(len(bias)):
        units.append((bias[j], [(abs(e) - 1, 1 if e > 0 else -1) for e in pred[p:p + fanin[j]]]))
        p += fanin[j]
    return len(nxt), units, nxt


def write_flat(path, n, units, nxt):
    B, F, P = array("i"), array("i"), array("i")
    for b, ins in units:
        B.append(b)
        F.append(len(ins))
        for k, w in ins:
            P.append(k)
            P.append(w)
    with open(path, "wb") as f:
        f.write(struct.pack("<iii", n, len(units), len(P) // 2))
        f.write(B.tobytes() + F.tobytes() + P.tobytes() + array("i", nxt).tobytes())


def levelize(n, units, nxt):
    """Lemma 2.5: every row of every layer reads only rows of the layer before."""
    v = len(units)
    live = [False] * (n + v)
    stack = [k for k in nxt if k >= 0]
    while stack:
        s = stack.pop()
        if not live[s]:
            live[s] = True
            if s >= n:
                stack.extend(k for k, _ in units[s - n][1])
    depth = [0] * (n + v)
    for j, (_, ins) in enumerate(units):
        depth[n + j] = 1 + max((depth[k] for k, _ in ins), default=0)
    d = max(depth[n + j] for j in range(v) if live[n + j])
    lam = [0] * (n + v)
    for j, (_, ins) in enumerate(units):
        if live[n + j]:
            for k, _ in ins:
                lam[k] = max(lam[k], depth[n + j])
    for s in nxt:
        lam[s] = d + 1
    layers = [[("copy", i) for i in range(n)]]
    where = [{i: i for i in range(n)}]
    for ell in range(1, d):
        rows, pos = [], {}
        for s in range(n + v):
            if s >= n and live[s] and depth[s] == ell:
                pos[s] = len(rows); rows.append(("unit", s))
        for s in range(n + v):
            if (s < n or live[s]) and depth[s] < ell < lam[s]:
                pos[s] = len(rows); rows.append(("copy", s))
        layers.append(rows); where.append(pos)
    layers.append([("unit" if depth[s] == d else "copy", s) for s in nxt])
    base, out_units = [0], []
    for ell in range(1, d + 1):
        base.append(base[-1] + len(layers[ell - 1]))
        for kind, s in layers[ell]:
            if kind == "copy":
                out_units.append((-1, [(base[ell - 1] + where[ell - 1][s], 1)]))
            else:
                b, ins = units[s - n]
                out_units.append((b, [(base[ell - 1] + where[ell - 1][k], w) for k, w in ins]))
    return (n, out_units, [base[d] + i for i in range(n)],
            {"depth": d, "rows": sum(len(L) for L in layers[1:]),
             "identity_rows": sum(1 for L in layers[1:] for kind, _ in L if kind == "copy"),
             "max_width": max(len(L) for L in layers[1:]),
             "layer_sizes": [len(L) for L in layers[1:]]})


def framed_parts(s: bytes):
    a = struct.unpack("<Q", s[:8])[0]
    b = struct.unpack("<Q", s[8 + a:16 + a])[0]
    return s[8:8 + a], s[16 + a:16 + a + b], s[16 + a + b:]


def main_c() -> int:
    ap = argparse.ArgumentParser()
    ap.add_argument("--cc", default="gcc")
    args = ap.parse_args()
    t_start = time.perf_counter()
    from host import M_P, M_STAR, describe, field, ser, read_host
    work = tempfile.mkdtemp(prefix="netlist_eval_")
    exe = os.path.join(work, "netlist_eval")
    subprocess.run([args.cc, "-O3", "-march=native", "-fopenmp", "-o", exe,
                    os.path.join(SRC, "netlist_eval.c")], check=True)
    J = lambda *p: os.path.join(work, *p)

    def ev(*a):
        r = subprocess.run([exe] + [str(x) for x in a], capture_output=True, text=True)
        return r.returncode, r.stdout.strip()

    sigma = read_host()
    n, units, nxt = parse_sigma(sigma)
    write_flat(J("host.bin"), n, units, nxt)
    ln, lunits, lnxt, lev_info = levelize(n, units, nxt)
    write_flat(J("lev.bin"), ln, lunits, lnxt)
    r_H = describe(sigma)
    tau = describe(field(sigma) + field(bytes(M_STAR)))
    expect_star = ser(sigma, bytes(M_STAR), tau)
    for name, b in (("mP", bytes(M_P)), ("mstar", bytes(M_STAR)), ("rH", r_H), ("tau", tau)):
        open(J(name), "wb").write(b)
    out = {"lev": lev_info}

    with cf.ThreadPoolExecutor(max_workers=4) as ex:
        f_rand = ex.submit(ev, "rand", J("host.bin"), 1 << 20, 1)
        f_lrand = ex.submit(ev, "rand", J("lev.bin"), 1 << 20, 2)
        f_desc = ex.submit(ev, "run", J("host.bin"), J("mP"), J("rH"), J("desc.out"), "lock")
        out["netlist_random"] = f_rand.result()[1]
        out["lev_random"] = f_lrand.result()[1]
        out["self_describing"] = f_desc.result()[1]
        # three generations, each rebuilt from the bytes the previous one emitted
        gens = []
        net_path, mem_path, tau_path = J("host.bin"), J("mstar"), J("tau")
        for g in range(1, 4):
            mode = "lock" if g == 1 else "net"
            rc, msg = ev("run", net_path, mem_path, tau_path, J(f"gen{g}.out"), mode)
            emitted = open(J(f"gen{g}.out"), "rb").read()
            gens.append({"generation": g, "mode": mode, "result": msg,
                         "sha256": hashlib.sha256(emitted).hexdigest(),
                         "equals_ser": emitted == expect_star})
            s_g, m_g, t_g = framed_parts(emitted)
            n2, u2, x2 = parse_sigma(s_g)
            net_path = J(f"host_g{g + 1}.bin")
            write_flat(net_path, n2, u2, x2)
            mem_path, tau_path = J(f"m_g{g + 1}"), J(f"tau_g{g + 1}")
            open(mem_path, "wb").write(m_g)
            open(tau_path, "wb").write(t_g)
        out["generations"] = gens
    desc_ok = open(J("desc.out"), "rb").read() == sigma
    ok = (out["netlist_random"].endswith("0 halted batches not fixed")
          and " 0 disagree" in out["netlist_random"] and " 0 disagree" in out["lev_random"]
          and desc_ok and all(g["equals_ser"] for g in gens))
    out["self_describing_equals_sigma"] = desc_ok
    out["ok"] = ok
    out["seconds"] = time.perf_counter() - t_start
    for k in ("netlist_random", "lev_random", "self_describing"):
        print(f"  {k}: {out[k]}")
    for g in gens:
        print(f"  generation {g['generation']} ({g['mode']}): {g['result']}; equals ser: "
              f"{'yes' if g['equals_ser'] else 'NO'}; {g['sha256'][:16]}")
    json.dump(out, open(runs_path("paper_c_evaluator.json"), "w"), indent=1)
    print("C EVALUATOR:", "PASS" if ok else "FAIL")
    return 0 if ok else 1


def bound(n: int) -> int:
    return n + -(-n // 127) + 1


def tags(tape: bytes):
    i, out = 0, []
    while True:
        t = tape[i]
        out.append(t)
        i += 1
        if t == 0:
            return out
        i += t if t <= 127 else 1


class Audit:
    def __init__(self):
        self.n = 0
        self.roundtrip = []
        self.overlong = []
        self.not_tight = []
        self.tag128 = []

    def check(self, b: bytes) -> None:
        self.n += 1
        for enc in (describe, describe_literal):
            r = enc(b)
            if decode(r) != b:
                self.roundtrip.append((enc.__name__, len(b)))
            if len(r) > bound(len(b)):
                self.overlong.append((enc.__name__, len(b), len(r)))
        if len(describe_literal(b)) != bound(len(b)):
            self.not_tight.append(len(b))
        if 128 in tags(describe(b)):
            self.tag128.append(len(b))

    @property
    def ok(self) -> bool:
        return not (self.roundtrip or self.overlong or self.not_tight or self.tag128)


def main_codec() -> int:
    a = Audit()
    for n in range(0, 15):
        for t in itertools.product((0, 1), repeat=n):
            a.check(bytes(t))
    binary = a.n
    for n in range(0, 10):
        for t in itertools.product((0, 1, 2), repeat=n):
            a.check(bytes(t))
    ternary = a.n - binary
    print(f"  exhaustive: {binary:,} binary strings to length 14, "
          f"{ternary:,} ternary to length 9")

    edges = (list(range(0, 12))
             + [126, 127, 128, 129, 130, 251, 252, 253, 254, 255, 256, 257,
                380, 381, 382, 508, 509, 510])
    before = a.n
    for L in edges:
        a.check(bytes([0x41]) * L)
        a.check(bytes([0x00]) * L)
        a.check(bytes([0xFF]) * L)
        a.check(bytes(range(256))[:L] if L <= 256 else bytes(range(256)) * (L // 256))
        a.check(bytes([0x41] * L + [0x42]))
        a.check(bytes([0x42] + [0x41] * L))
        a.check(bytes([0x41] * L + [0x42] * L))
        a.check(bytes(([0x41] * 4 + [0x42]) * max(1, L)))
        a.check(bytes(([0x41] * 3 + [0x42]) * max(1, L)))
    print(f"  boundaries: {a.n - before:,} strings straddling the literal cap, "
          f"the extreme repeat tags, and the run/literal transitions")

    rng = random.Random(11)
    before = a.n
    for _ in range(4000):
        n = rng.randrange(0, 900)
        alpha = rng.choice([2, 3, 7, 256])
        a.check(bytes(rng.randrange(alpha) for _ in range(n)))
    for _ in range(1500):
        n = rng.randrange(0, 900)
        out = bytearray()
        while len(out) < n:
            out += bytes([rng.randrange(256)]) * rng.choice([1, 2, 3, 4, 5, 126, 127, 128, 253])
        a.check(bytes(out[:n]))
    print(f"  random and run-structured: {a.n - before:,} strings")

    print(f"  total {a.n:,}: round-trip exact, neither encoder exceeds "
          f"|f| + ceil(|f|/127) + 1, the literal encoder attains it, "
          f"tag 128 never emitted: {'yes' if a.ok else 'NO'}")
    if not a.ok:
        print("   roundtrip:", a.roundtrip[:5])
        print("   overlong:", a.overlong[:5])
        print("   not tight:", a.not_tight[:5])
        print("   tag128:", a.tag128[:5])
    json.dump({"strings": a.n, "roundtrip_failures": len(a.roundtrip),
               "bound_failures": len(a.overlong),
               "literal_not_tight": len(a.not_tight),
               "tag128_emitted": len(a.tag128)},
              open(runs_path("paper_codec.json"), "w"), indent=1)
    return 0 if a.ok else 1


def spec(mem, tau, h, omega):
    """Definition 5.1, clause by clause, on (mem, h, omega)."""
    m = list(mem)
    w = list(omega)
    if m[C_WR] == 1:                                   # (i)
        w.append(m[R_OUT])
        m[R_OUT] = 0
    hp = h
    if m[C_RD] == 1:                                   # (ii)
        if h < len(tau):
            m[R_IN] = tau[h]
            m[C_EOT] = 0
            hp = h + 1
        else:
            m[C_EOT] = 1
    if m[C_RW] == 1:                                   # (iii)
        hp = 0
    m[C_WR] = m[C_RD] = m[C_RW] = 0                    # (iv)
    return m, hp, w


def main_device() -> int:
    tapes = [b"", b"\x07", b"\x01\x02", bytes(range(5)), bytes(range(64))]
    vals = (0, 1, 2, 3, 127, 128, 255)
    bad, n = [], 0
    for tau in tapes:
        heads = sorted({0, 1, max(0, len(tau) - 1), len(tau)})
        for h in heads:
            for wr, rd, rw in itertools.product(vals, repeat=3):
                for eot, rin, rout in ((0, 0, 0), (1, 9, 200), (0, 255, 1), (1, 1, 255)):
                    mem = [0] * 256
                    mem[C_WR], mem[C_RD], mem[C_RW] = wr, rd, rw
                    mem[C_EOT], mem[R_IN], mem[R_OUT] = eot, rin, rout
                    mem[0x10] = 0xAB                    # an ordinary cell, must not move
                    want_mem, want_h, want_out = spec(mem, tau, h, b"")

                    dev = Tape(tau)
                    dev.h = h
                    got_mem = list(mem)
                    dev.apply(got_mem)
                    n += 1
                    if (got_mem != want_mem or dev.h != want_h
                            or bytes(dev.out) != bytes(want_out)):
                        bad.append({"tau": len(tau), "h": h, "wr": wr, "rd": rd,
                                    "rw": rw, "eot": eot,
                                    "spec": (want_mem[C_EOT], want_mem[R_IN],
                                             want_mem[R_OUT], want_h, list(want_out)),
                                    "impl": (got_mem[C_EOT], got_mem[R_IN],
                                             got_mem[R_OUT], dev.h, list(dev.out))})
    print(f"  device applications compared: {n:,}")
    print(f"  implementation agrees with Definition 5.1 on every one: "
          f"{'yes' if not bad else f'NO ({len(bad)} disagreements)'}")
    for b in bad[:5]:
        print("   ", b)

    # A request fires on the value 1 and on no other value. The head starts off
    # zero so that a rewind is observable; without that a rewind of a head
    # already at 0 changes nothing and the test would not see it fire.
    fires = []
    for cell in (C_WR, C_RD, C_RW):
        for v in range(256):
            mem = [0] * 256
            mem[cell] = v
            mem[R_OUT] = 0x5A
            dev = Tape(b"\x11\x22")
            dev.h = 1
            before = (dev.h, len(dev.out))
            dev.apply(mem)
            acted = (dev.h, len(dev.out)) != before or mem[R_IN] != 0 or mem[C_EOT] != 0
            if acted != (v == 1):
                fires.append((cell, v, acted))
    print(f"  each request fires exactly on the value 1, over all 256 cell values: "
          f"{'yes' if not fires else f'NO {fires[:5]}'}")

    ok = not bad and not fires
    json.dump({"applications": n, "disagreements": len(bad),
               "value_trigger_failures": len(fires)},
              open(runs_path("paper_device.json"), "w"), indent=1)
    return 0 if ok else 1


def main_environment() -> int:
    from host import M_STAR, inst, ser, tau_star, run_reference, read_host, host_netlist, sigma_host
    from host import net_of_sigma
    from machines import compile_net

    sigma_bytes = read_host()
    tau = tau_star(sigma_bytes, M_STAR)
    s = ser(sigma_bytes, bytes(M_STAR), tau)

    # sigma: parameters and predecessor entries stored, and the time to write
    t0 = time.perf_counter()
    net, inputs, outputs = host_netlist()
    t_build = time.perf_counter() - t0
    t0 = time.perf_counter()
    encoded = sigma_host()
    t_sigma = time.perf_counter() - t0
    assert encoded == sigma_bytes
    stored, _, _, _ = net_of_sigma(sigma_bytes)
    entries = (2 * len(stored.gates)                       # bias and fan-in
               + sum(len(i) for i, _ in stored.gates.values())
               + len(outputs))
    print(f"  sigma: {entries:,} stored entries -> {len(encoded):,} bytes "
          f"in {t_sigma * 1e3:.0f} ms ({t_build * 1e3:.0f} ms to assemble "
          f"the netlist from source)")

    # inst: one pass over the serialized instance, then sigma^-1 on its first field
    t0 = time.perf_counter()
    reps = 50
    for _ in range(reps):
        a, b, c = inst(s)
    t_inst = (time.perf_counter() - t0) / reps
    assert (a, b, c) == (sigma_bytes, bytes(M_STAR), tau)
    t0 = time.perf_counter()
    for _ in range(5):
        N, I, O, _ = net_of_sigma(a)
    t_sigma_inv = (time.perf_counter() - t0) / 5
    assert len(N.gates) == len(stored.gates)
    print(f"  inst: {len(s):,} bytes parsed in {t_inst * 1e3:.2f} ms, and "
          f"{len(N.gates):,} units rebuilt from the first field in "
          f"{t_sigma_inv * 1e3:.0f} ms")

    # Lev: the units placed, and the time to place them
    t0 = time.perf_counter()
    layers, info = compile_net(N, I, O)
    t_lev = time.perf_counter() - t0
    M = sum(int(W.shape[0]) for W, _ in layers)
    nnz = sum(int((W != 0).sum()) for W, _ in layers)
    print(f"  Lev: {len(N.gates):,} units in, {M:,} rows and {nnz:,} nonzero "
          f"entries placed over {info['layers']} layers in {t_lev:.1f} s")

    # the device: one application per step, at most one byte moved
    t0 = time.perf_counter()
    emitted, T = run_reference(M_STAR, tau)
    t_run = time.perf_counter() - t0
    assert emitted == s
    print(f"  device: {T:,} applications, {len(emitted):,} bytes emitted "
          f"({t_run:.2f} s for the whole reference run)")

    env_ops = len(s) + len(sigma_bytes) + M + nnz + T
    closed = 2 * len(sigma_bytes) + len(bytes(M_STAR)) + len(tau) + 16 + M + nnz + T
    assert env_ops == closed, (env_ops, closed)
    net_ops = T * M
    print(f"  instantiation: {env_ops:,} elementary operations per generation, "
          f"which is the closed form 2|sigma|+|m|+|tau|+16+M+nnz+T")
    print(f"  network:     {net_ops:,} unit evaluations (T = {T:,}, M = {M:,})")
    print(f"  ratio: {env_ops / net_ops:.3e}")

    out = {"sigma_entries": entries, "sigma_bytes": len(encoded),
           "sigma_seconds": t_sigma, "build_seconds": t_build,
           "inst_bytes": len(s), "inst_seconds": t_inst,
           "sigma_inverse_seconds": t_sigma_inv,
           "lev_units_in": len(N.gates), "lev_units_out": M, "lev_nonzero": nnz,
           "lev_layers": info["layers"], "lev_seconds": t_lev,
           "lev_entries": info["total_weights"],
           "steps": T, "emitted_bytes": len(emitted),
           "reference_seconds": t_run,
           "environment_ops": env_ops, "network_ops": net_ops,
           "ratio": env_ops / net_ops}
    json.dump(out, open(runs_path("paper_environment.json"), "w"), indent=1)
    return 0


def files():
    out = [os.path.join(REPO, "neural_computer.safetensors")]
    v = os.path.join(REPO, "variants")
    out += sorted(os.path.join(v, f) for f in os.listdir(v) if f.endswith(".safetensors"))
    return out


def one(p):
    data = open(p, "rb").read()
    r = describe(data)
    out, steps = run_reference(M_P, r, expect=data)
    return {"file": os.path.basename(p), "bytes": len(out), "recipe": len(r),
            "steps": steps, "exact": out == data,
            "sha256": hashlib.sha256(out).hexdigest()}


def main_family() -> int:
    ap = argparse.ArgumentParser()
    ap.add_argument("--jobs", type=int, default=os.cpu_count() or 1)
    args = ap.parse_args()
    t0 = time.perf_counter()
    paths = files()
    # the largest machines first, so the pool is not left waiting on one of them
    order = sorted(paths, key=os.path.getsize, reverse=True)
    with cf.ProcessPoolExecutor(max_workers=args.jobs) as ex:
        got = dict(zip(order, ex.map(one, order)))
    rec = [got[p] for p in paths]
    for r in rec:
        print(f"  {'OK ' if r['exact'] else 'FAIL'} {r['file']:<44} "
              f"{r['bytes']:>10,} B  {r['steps']:>12,} steps", flush=True)
    bad = sum(not r["exact"] for r in rec)
    tot_b = sum(r["bytes"] for r in rec)
    tot_s = sum(r["steps"] for r in rec)
    tot_r = sum(r["recipe"] for r in rec)
    dt = time.perf_counter() - t0
    print(f"{len(rec)} machines, {tot_b:,} bytes emitted in {tot_s:,} steps "
          f"from {tot_r:,} bytes of recipe ({dt/60:.1f} min); failures: {bad}")
    json.dump({"machines": rec, "bytes": tot_b, "steps": tot_s,
               "recipe_bytes": tot_r, "failures": bad, "seconds": dt},
              open(runs_path("paper_runs_family.json"), "w"), indent=1)
    return 0 if bad == 0 else 1

TARGETS = ["neural_tile.safetensors", "neural_ca.safetensors",
           "neural_reversible.safetensors", "neural_attractor.safetensors"]


def main_family_gate() -> int:
    import torch
    device = "cuda" if torch.cuda.is_available() else "cpu"
    F = NetEvaluator(read_host(), device=device,
                     graph=device.startswith("cuda"))
    rows = []
    bad = 0
    total_b = total_s = 0
    t_all = time.perf_counter()
    for name in TARGETS:
        path = os.path.join(REPO, "variants", name)
        data = open(path, "rb").read()
        r = describe(data)
        ref_out, ref_steps = run_reference(M_P, r, expect=data)
        assert ref_out == data
        t0 = time.perf_counter()
        out, steps = F.run(M_P, r, max_steps=ref_steps + 8, expect=data,
                           progress=200000)
        dt = time.perf_counter() - t0
        ok = out == data and steps == ref_steps
        bad += not ok
        total_b += len(out)
        total_s += steps
        rows.append({"file": name, "bytes": len(out), "recipe": len(r),
                     "steps": steps, "reference_steps": ref_steps,
                     "exact": ok, "seconds": dt,
                     "steps_per_second": steps / dt if dt else None,
                     "sha256": hashlib.sha256(out).hexdigest()})
        print(f"  {'OK ' if ok else 'FAIL'} {name:<34} {len(out):>9,} B  "
              f"{steps:>10,} steps  ({dt / 60:.1f} min, "
              f"{steps / dt:,.0f} steps/s)", flush=True)
    dt = time.perf_counter() - t_all
    print(f"  {len(rows)} machines on the netlist of sigma: {total_b:,} bytes in "
          f"{total_s:,} steps ({dt / 60:.1f} min); failures: {bad}")
    json.dump({"machines": rows, "bytes": total_b, "steps": total_s,
               "failures": bad, "seconds": dt},
              open(runs_path("paper_runs_family_gate.json"), "w"), indent=1)
    return 0 if bad == 0 else 1


def shapes():
    rng = random.Random(5)
    host = open(HOST_PATH, "rb").read()
    m0 = bytes(256)
    m1 = bytes([255]) * 256
    mr = bytes(rng.randrange(256) for _ in range(256))
    # A payload whose first eight bytes are a plausible length field, and a tape
    # that begins the way a framed field begins: if inst read a length from the
    # wrong offset these would decode to the wrong split.
    trap = lam(1 << 40) + b"trap"
    out = [
        (b"", m0, b""),
        (b"", m0, b"\x00"),
        (b"\x00", m0, b""),
        (b"\x00" * 3, m1, b""),
        (trap, mr, b""),
        (b"", mr, trap),
        (trap, m0, trap),
        (bytes(range(256)), mr, bytes(range(256))),
        (host, bytes(M_STAR), tau_star(host, M_STAR)),
        (host, m0, b""),
    ]
    for _ in range(300):
        a = bytes(rng.randrange(256) for _ in range(rng.randrange(0, 300)))
        t = bytes(rng.randrange(256) for _ in range(rng.randrange(0, 300)))
        out.append((a, bytes(rng.randrange(256) for _ in range(256)), t))
    return out


def main_framing() -> int:
    cases = shapes()
    rt_bad, digests = [], {}
    for sg, m, t in cases:
        b = ser(sg, m, t)
        if inst(b) != (sg, m, t):
            rt_bad.append((len(sg), len(t)))
        digests.setdefault(hashlib.sha256(b).hexdigest(), []).append((len(sg), len(m), len(t)))
    collisions = {k: v for k, v in digests.items() if len(v) > 1}
    print(f"  inst(ser(Omega)) = Omega on {len(cases)} instances: "
          f"{'exact' if not rt_bad else f'{len(rt_bad)} FAILED'}")
    print(f"  ser injective over them (distinct instances, distinct bytes): "
          f"{'yes' if not collisions else f'NO {list(collisions.values())[:2]}'}")

    # Truncations. A string shorter than the framed serialization and memory
    # image is not an instance and must be rejected; one that reaches at least
    # that far is the instance with a correspondingly shorter tape, and must
    # parse to exactly that.
    host = open(HOST_PATH, "rb").read()
    tau = tau_star(host, M_STAR)
    full = ser(host, bytes(M_STAR), tau)
    minimal = 16 + len(host) + 256
    probes = sorted({p for p in
                     [0, 1, 7, 8, 9, 15, 16, 17,
                      8 + len(host) - 1, 8 + len(host), 8 + len(host) + 7,
                      8 + len(host) + 8, minimal - 256, minimal - 1, minimal,
                      minimal + 1, len(full) - 1, len(full)]
                     if 0 <= p <= len(full)})
    wrongly_accepted, wrongly_rejected = [], []
    for k in probes:
        try:
            got = inst(full[:k])
        except (ValueError, IndexError, struct.error):
            if k >= minimal:
                wrongly_rejected.append(k)
            continue
        if k < minimal:
            wrongly_accepted.append((k, len(got[1])))
        elif got != (host, bytes(M_STAR), full[minimal:k]):
            wrongly_accepted.append((k, "wrong triple"))
    short = sum(1 for k in probes if k < minimal)
    print(f"  {short} truncations below a complete memory image rejected: "
          f"{'yes' if not wrongly_accepted else f'NO {wrongly_accepted}'}")
    print(f"  {len(probes) - short} longer prefixes parse to the instance with "
          f"that tape: {'yes' if not wrongly_rejected else f'NO {wrongly_rejected}'}")
    accepted = wrongly_accepted + wrongly_rejected

    # a memory field of the wrong length must be rejected
    wrong = []
    for size in (0, 1, 255, 257, 512):
        b = lam(len(host)) + host + lam(size) + bytes(size) + tau
        try:
            inst(b)
            wrong.append(size)
        except (ValueError, IndexError, struct.error):
            pass
    print(f"  memory field of length != 256 rejected: "
          f"{'yes' if not wrong else f'NO for {wrong}'}")

    # the full instance is accepted and recovers exactly
    exact = inst(full) == (host, bytes(M_STAR), tau)
    print(f"  the distributed instance parses back exactly: {exact}")

    ok = not rt_bad and not collisions and not accepted and not wrong and exact
    json.dump({"instances": len(cases), "roundtrip_failures": len(rt_bad),
               "digest_collisions": len(collisions),
               "truncations_accepted": len(accepted),
               "bad_memory_lengths_accepted": len(wrong),
               "distributed_instance_exact": exact},
              open(runs_path("paper_framing.json"), "w"), indent=1)
    return 0 if ok else 1


def spec_step(mem, p):
    """Definition 5.2, transcribed."""
    A = mem[p % 256]
    B = mem[(p + 1) % 256]
    C = mem[(p + 2) % 256]
    m = list(mem)
    r = (m[B % 256] - m[A % 256]) % 256
    m[B % 256] = r
    two_c = r - 256 if r >= 128 else r
    return m, (C if two_c <= 0 else (p + 3) % 256)


def impl_step(mem, p):
    """The reference of selfrep.run_reference, one step, device detached."""
    m = list(mem)
    A = m[p]
    B = m[(p + 1) & 0xFF]
    C = m[(p + 2) & 0xFF]
    r = (m[B] - m[A]) & 0xFF
    m[B] = r
    return m, (C if (r == 0 or r >= 0x80) else (p + 3) & 0xFF)


def main_host() -> int:
    rng = random.Random(31)
    bad, n = [], 0
    mems = [[0] * 256, [255] * 256, list(range(256)), list(reversed(range(256)))]
    mems += [[rng.randrange(256) for _ in range(256)] for _ in range(60)]
    for mem in mems:
        for p in range(256):                       # every counter, wraps included
            if p == HALT_PC:
                continue
            sm, sp = spec_step(mem, p)
            im, ip = impl_step(mem, p)
            n += 1
            if sm != im or sp != ip:
                bad.append((p, sp, ip))
    print(f"  reference steps compared with Definition 5.2: {n:,}")
    print(f"  agree on every one: {'yes' if not bad else f'NO {bad[:4]}'}")

    wrapped = sum(1 for p in (254, 255, 253) if p != HALT_PC) * len(mems)
    print(f"  of which {len(mems) * 3:,} fetch an operand across the top of memory")

    # A halted state is a fixed point of the levelized map. The state is halted
    # when the halt bit is set, coordinate 8 of the vector; the bit latches one
    # step after the next counter decodes to 255, so setting the counter alone
    # does not halt the machine.
    from host import LevEvaluator, read_host
    import torch
    L = LevEvaluator(read_host(), device="cpu", dense=False)
    gen = torch.Generator().manual_seed(97)
    V = (torch.rand(48, L.N, generator=gen) < 0.5).float()
    V[:, 8] = 1.0
    fixed = bool((L.step(V) == V).all())
    print(f"  halted states are fixed points of Lev(N_host), 48 random states: "
          f"{'yes' if fixed else 'NO'}")

    # And the bit latches exactly when the next counter is 255: run one step
    # from unhalted states and compare the latched bit against the reference.
    U = (torch.rand(64, L.N, generator=gen) < 0.5).float()
    U[:, 8] = 0.0
    W = L.step(U)
    latch_bad = 0
    for i in range(U.shape[0]):
        mem = [int(sum(int(U[i, 9 + j * 8 + k]) << (7 - k) for k in range(8)))
               for j in range(256)]
        pc = int(sum(int(U[i, k]) << (7 - k) for k in range(8)))
        _, npc = impl_step(mem, pc)
        if int(W[i, 8]) != (1 if npc == HALT_PC else 0):
            latch_bad += 1
    print(f"  the halt bit latches exactly when the next counter is 255, "
          f"64 random states: {'yes' if latch_bad == 0 else f'NO ({latch_bad})'}")
    fixed = fixed and latch_bad == 0

    ok = not bad and fixed
    json.dump({"steps_compared": n, "disagreements": len(bad),
               "halt_fixed_point": fixed},
              open(runs_path("paper_host.json"), "w"), indent=1)
    return 0 if ok else 1


def main_host_family() -> int:
    ap = argparse.ArgumentParser()
    ap.add_argument("--widths", default="3-12")
    ap.add_argument("--states", type=int, default=1 << 16)
    ap.add_argument("--cc", default="gcc")
    args = ap.parse_args()
    lo, hi = (int(x) for x in args.widths.split("-"))
    from host import sigma
    work = tempfile.mkdtemp(prefix="host_family_")
    exe = os.path.join(work, "netlist_eval")
    subprocess.run([args.cc, "-O3", "-march=native", "-fopenmp", "-o", exe,
                    os.path.join(REPO, "src", "netlist_eval.c")], check=True)
    rows, ok = [], True
    for A in range(lo, hi + 1):
        t0 = time.perf_counter()
        s = sigma(A)
        n, units, nxt = parse_sigma(s)
        path = os.path.join(work, f"h{A}.bin")
        write_flat(path, n, units, nxt)
        N = max(64, args.states >> max(0, A - 10))
        r = subprocess.run([exe, "rand", path, str(N), str(A)], capture_output=True, text=True)
        line = r.stdout.strip()
        good = r.returncode == 0
        ok &= good
        rows.append({"A": A, "sigma_bytes": len(s), "units": len(units),
                     "edges": sum(len(i) for _, i in units), "states": N,
                     "result": line, "ok": good, "seconds": time.perf_counter() - t0})
        print(f"  A={A}: {len(units):,} units, {len(s):,} bytes; {line}", flush=True)
        os.remove(path)
    json.dump({"widths": rows, "ok": ok}, open(runs_path("paper_host_family.json"), "w"), indent=1)
    print("HOST FAMILY:", "PASS" if ok else "FAIL")
    return 0 if ok else 1


def depth_of(n, units, nxt):
    d = [0] * (n + len(units))
    for j, (_, ins) in enumerate(units):
        d[n + j] = 1 + max((d[k] for k, _ in ins), default=0)
    return max(d[s] for s in nxt)


def main_host_fold() -> int:
    ap = argparse.ArgumentParser()
    ap.add_argument("--widths", default="3-12")
    ap.add_argument("--states", type=int, default=1 << 16)
    ap.add_argument("--cc", default="gcc")
    args = ap.parse_args()
    lo, hi = (int(x) for x in args.widths.split("-"))
    from host import build, family_sigma_of_net as sigma_of_net, sigma
    work = tempfile.mkdtemp(prefix="host_fold_")
    exe = os.path.join(work, "netlist_eval")
    subprocess.run([args.cc, "-O3", "-march=native", "-fopenmp", "-o", exe,
                    os.path.join(REPO, "src", "netlist_eval.c")], check=True)
    rows, ok = [], True
    for A in range(lo, hi + 1):
        t0 = time.perf_counter()
        net, inputs, outputs = build(A, fold=True)
        s = sigma_of_net(net, inputs, outputs, A)
        n, units, nxt = parse_sigma(s)
        n0, units0, nxt0 = parse_sigma(sigma(A))
        path = os.path.join(work, f"f{A}.bin")
        write_flat(path, n, units, nxt)
        N = max(64, args.states >> max(0, A - 10))
        r = subprocess.run([exe, "rand", path, str(N), str(A)], capture_output=True, text=True)
        line = r.stdout.strip().splitlines()[-1] if r.stdout.strip() else r.stderr.strip()
        good = r.returncode == 0
        ok &= good
        row = {"A": A, "units": len(units), "edges": sum(len(i) for _, i in units),
               "depth": depth_of(n, units, nxt), "depth_unfolded": depth_of(n0, units0, nxt0),
               "units_unfolded": len(units0), "edges_unfolded": sum(len(i) for _, i in units0),
               "states": N, "result": line, "agrees": good, "seconds": round(time.perf_counter() - t0, 1)}
        rows.append(row)
        print(f"  A={A}: {row['units']:,} units, {row['edges']:,} edges, depth {row['depth']} "
              f"(H_A: {row['units_unfolded']:,}, {row['edges_unfolded']:,}, depth {row['depth_unfolded']}); "
              f"{line}", flush=True)
    json.dump({"rows": rows, "all_agree": ok},
              open(os.path.join(REPO, "paper", "runs", "paper_host_fold.json"), "w"), indent=1)
    return 0 if ok else 1


def gate_by_gate(net, inputs, outputs, V):
    """Evaluate the netlist directly: topological order, one gate at a time."""
    gates = net.gates
    indeg, cons = {}, {}
    for g, (ins, _) in gates.items():
        indeg[g] = len([s for s, _ in ins if s in gates])
        for s, _ in ins:
            cons.setdefault(s, []).append(g)
    order = [g for g, d in indeg.items() if d == 0]
    i = 0
    while i < len(order):
        for c in cons.get(order[i], []):
            indeg[c] -= 1
            if indeg[c] == 0:
                order.append(c)
        i += 1
    assert len(order) == len(gates)

    B = V.shape[0]
    val = {"#0": torch.zeros(B), "#1": torch.ones(B)}
    for k, name in enumerate(inputs):
        val[name] = V[:, k]
    for g in order:
        ins, bias = gates[g]
        acc = torch.full((B,), float(bias))
        for s, w in ins:
            acc = acc + w * val[s]
        val[g] = (acc >= 0).float()
    return torch.stack([val[o] for o in outputs], dim=1)


def main_lev() -> int:
    from host import net_of_sigma
    from host import LevEvaluator, NetEvaluator, read_host

    sigma = read_host()
    net, inputs, outputs, _ = net_of_sigma(sigma)
    L = LevEvaluator(sigma, device="cpu", dense=False)

    gen = torch.Generator().manual_seed(20260910)
    B = 96
    V = (torch.rand(B, len(inputs), generator=gen) < 0.5).float()

    direct = gate_by_gate(net, inputs, outputs, V)
    levelled = L.step(V)
    agree = bool((direct == levelled).all())
    print(f"  netlist has {len(net.gates):,} gates on {len(inputs):,} state bits")
    print(f"  gate-by-gate evaluation equals Lev(N_host) on {B} uniformly random "
          f"states: {'yes' if agree else 'NO'}")
    if not agree:
        d = (direct != levelled).nonzero()
        print("   first disagreements:", d[:5].tolist())

    grouped = NetEvaluator(sigma, device="cpu").step(V)
    agree_net = bool((direct == grouped).all())
    print(f"  the evaluator that carries only the netlist's own predecessor "
          f"entries agrees on the same states: {'yes' if agree_net else 'NO'}")

    # The dense form: ternary weights, integer pre-activations, margin one half.
    D = LevEvaluator(sigma, device="cpu", dense=True)
    nonternary = [i for i, W in enumerate(D.W)
                  if not set(torch.unique(W).tolist()) <= {-1.0, 0.0, 1.0}]
    nonint = [i for i, b in enumerate(D.B) if not bool((b == b.round()).all())]
    print(f"  every weight of all {len(D.W)} layers lies in {{-1,0,1}}: "
          f"{'yes' if not nonternary else f'NO at {nonternary[:3]}'}")
    print(f"  every bias is an integer: {'yes' if not nonint else f'NO at {nonint[:3]}'}")

    y, worst, frac = V, float("inf"), 0.0
    for W, b in zip(D.W, D.B):
        pre = y @ W.T + b
        worst = min(worst, float((pre + 0.5).abs().min()))
        frac = max(frac, float((pre - pre.round()).abs().max()))
        y = (pre >= 0).float()
    same_dense = bool((y == levelled).all())
    print(f"  dense stack agrees with the sparse evaluation on the same states: "
          f"{'yes' if same_dense else 'NO'}")
    print(f"  minimum distance of a pre-activation from -1/2 over all "
          f"{len(D.W)} layers: {worst:.6f}")
    print(f"  maximum distance of a pre-activation from an integer: {frac:.3e}")

    ok = (agree and agree_net and same_dense and not nonternary
          and not nonint and abs(worst - 0.5) < 1e-9)
    json.dump({"states": B, "gates": len(net.gates), "agree": agree,
               "agree_grouped": agree_net,
               "dense_agree": same_dense, "nonternary_layers": len(nonternary),
               "noninteger_bias_layers": len(nonint),
               "min_margin": worst, "max_noninteger": frac},
              open(runs_path("paper_lev.json"), "w"), indent=1)
    return 0 if ok else 1


def shortest(f: bytes) -> int:
    """Length of a shortest r in R with delta(r) = f, by dynamic programming."""
    n = len(f)
    INF = float("inf")
    cost = [INF] * (n + 1)
    cost[n] = 0
    for i in range(n - 1, -1, -1):
        best = INF
        for c in range(1, min(127, n - i) + 1):
            v = cost[i + c] + c + 1                       # literal token
            if v < best:
                best = v
        run = 0
        while run < min(127, n - i) and f[i + run] == f[i]:
            run += 1
            v = cost[i + run] + 2                         # repeat token
            if v < best:
                best = v
        cost[i] = best
    return cost[0] + 1


def run_free(f: bytes) -> bool:
    return all(f[i] != f[i + 1] for i in range(len(f) - 1))


def main_optimal() -> int:
    out = {}
    ok = True

    # Exhaustive over ternary strings with no two equal adjacent bytes.
    tested = 0
    bad = []
    for n in range(0, 11):
        for t in itertools.product((0, 1, 2), repeat=n):
            f = bytes(t)
            if not run_free(f):
                continue
            tested += 1
            s = shortest(f)
            if s != bound(n) or len(describe_literal(f)) != bound(n):
                bad.append(n)
    print(f"  every ternary string of length at most 10 with no two equal "
          f"adjacent bytes ({tested:,} of them): the shortest recipe has "
          f"exactly |f| + ceil(|f|/127) + 1 bytes: "
          f"{'yes' if not bad else f'NO at lengths {sorted(set(bad))[:5]}'}")
    ok &= not bad
    out["run_free_exhaustive"] = tested
    out["run_free_failures"] = len(bad)

    # Longer run-free strings over the full alphabet, including the lengths at
    # which a further literal token becomes necessary.
    rng = random.Random(4)
    lens = [0, 1, 126, 127, 128, 253, 254, 255, 380, 381, 508, 509, 700]
    lens += [rng.randrange(0, 900) for _ in range(120)]
    lbad = []
    for n in lens:
        f = bytearray()
        prev = -1
        for _ in range(n):
            c = rng.randrange(256)
            while c == prev:
                c = rng.randrange(256)
            f.append(c)
            prev = c
        f = bytes(f)
        if shortest(f) != bound(n) or len(describe_literal(f)) != bound(n):
            lbad.append(n)
    print(f"  {len(lens)} further run-free strings, lengths to 900 and at every "
          f"multiple of 127: shortest recipe equals the bound: "
          f"{'yes' if not lbad else f'NO at {lbad[:5]}'}")
    ok &= not lbad
    out["run_free_sampled"] = len(lens)
    out["run_free_sampled_failures"] = len(lbad)

    # On arbitrary strings the bound is an upper bound only; record how far the
    # encoder of the artifact is from the optimum.
    gaps = []
    abad = 0
    for _ in range(300):
        n = rng.randrange(0, 600)
        alpha = rng.choice([1, 2, 3, 9, 256])
        f = bytes(rng.randrange(alpha) for _ in range(n))
        s = shortest(f)
        d = len(describe(f))
        if decode(describe(f)) != f or d < s or d > bound(n):
            abad += 1
        gaps.append(d - s)
    print(f"  300 arbitrary strings: describe is never shorter than the optimum "
          f"and never longer than the bound: {'yes' if abad == 0 else 'NO'}; "
          f"excess over the optimum: max {max(gaps)}, mean {sum(gaps)/len(gaps):.2f}")
    ok &= abad == 0
    out["arbitrary_strings"] = len(gaps)
    out["arbitrary_failures"] = abad
    out["describe_excess_max"] = max(gaps)
    out["describe_excess_mean"] = sum(gaps) / len(gaps)

    # The serialization of the host is not run-free, so its optimum is shorter.
    from host import HOST_PATH
    sigma = open(HOST_PATH, "rb").read()
    s = shortest(sigma)
    print(f"  sigma(N_host): {len(sigma):,} bytes; bound {bound(len(sigma)):,}, "
          f"describe {len(describe(sigma)):,}, shortest recipe {s:,}")
    out["sigma_bytes"] = len(sigma)
    out["sigma_bound"] = bound(len(sigma))
    out["sigma_describe"] = len(describe(sigma))
    out["sigma_shortest"] = s
    ok &= s <= len(describe(sigma)) <= bound(len(sigma))

    json.dump(out, open(runs_path("paper_optimal.json"), "w"), indent=1)
    return 0 if ok else 1

ROCQ = os.path.join(REPO, 'rocq')

RECORD = os.path.join(REPO, 'paper', 'runs', 'paper_rocq.json')


def host_extraction(widths=(8, 9, 10)):
    """The host family of rocq/Host.v, extracted to OCaml, against sigma(N_host) and the generator's H_A."""
    from host import sigma as sigma_family
    ex = os.path.join(ROCQ, 'extract')
    subprocess.run(['ocamlfind', 'ocamlopt', '-package', 'stdlib', 'hostnet.mli', 'hostnet.ml', 'dumphost.ml',
                    '-o', 'dumphost'], cwd=ex, check=True)
    out = os.path.join(ex, 'host_rocq.bin')
    members = []
    for A in widths:
        subprocess.run([os.path.join(ex, 'dumphost'), str(A), out], check=True)
        theirs = open(out, 'rb').read()
        n, units, nxt = parse_sigma(read_host() if A == 8 else sigma_family(A))
        words = array('i', [n, len(units), sum(len(ins) for _, ins in units)])
        words.extend(b for b, _ in units)
        words.extend(len(ins) for _, ins in units)
        words.extend(w * (k + 1) for _, ins in units for k, w in ins)
        words.extend(nxt)
        if sys.byteorder != 'little':
            words.byteswap()
        ours = words.tobytes()
        members.append(dict(A=A, units=len(units), identical=ours == theirs,
                            sha256_generator=hashlib.sha256(ours).hexdigest(),
                            sha256_rocq=hashlib.sha256(theirs).hexdigest()))
    for f in os.listdir(ex):
        if not f.endswith(('.ml', '.mli')):
            os.remove(os.path.join(ex, f))
    return dict(members=members, identical=all(m['identical'] for m in members))


def stored_extraction(widths=(8, 9, 10)):
    """The stored host of rocq/Stored.v, extracted to OCaml, against the image src/twohead.py builds."""
    import twohead
    ex = os.path.join(ROCQ, 'extract')
    subprocess.run(['ocamlfind', 'ocamlopt', '-package', 'stdlib', 'storednet.mli', 'storednet.ml',
                    'dumpstored.ml', '-o', 'dumpstored'], cwd=ex, check=True)
    out = os.path.join(ex, 'stored_rocq.bin')
    members = []
    for A in widths:
        S = twohead.build_stored(A)
        subprocess.run([os.path.join(ex, 'dumpstored'), str(A), str(S['w']), out], check=True)
        theirs = open(out, 'rb').read()
        members.append(dict(A=A, w=S['w'], records=len(S['recs']), bytes=len(S['image']),
                            identical=theirs == S['image'], sha256=hashlib.sha256(theirs).hexdigest()))
    for f in os.listdir(ex):
        if not f.endswith(('.ml', '.mli')):
            os.remove(os.path.join(ex, f))
    return dict(members=members, identical=all(m['identical'] for m in members))


def pstar_images():
    """The memory images m* and m_P written in rocq/Pstar.v, against those of src/host.py."""
    from host import M_P, M_STAR
    src = open(os.path.join(ROCQ, 'Pstar.v')).read()
    defs = {}

    def value(name):
        body = re.search(r'Definition %s : list nat :=(.*?)\.\n' % name, src, re.S).group(1)
        toks = re.findall(r'\+\+|\[|\]|;|\w+', body)
        out, i = [], 0
        while i < len(toks):
            t = toks[i]
            if t == '[':
                j = toks.index(']', i)
                out += [int(x) for x in toks[i + 1:j] if x != ';']
                i = j + 1
            elif t == 'repeat':
                out += [int(toks[i + 1])] * int(toks[i + 2])
                i += 3
            elif t == 'firstn':
                out += defs[toks[i + 2]][:int(toks[i + 1])]
                i += 3
            elif t == '++':
                i += 1
            else:
                raise ValueError(t)
        defs[name] = out
        return out

    star, p = value('m_star'), value('m_P')
    return dict(m_star=star == list(M_STAR), m_P=p == list(M_P))


def main_rocq():
    for tool in ('rocq', 'make', 'ocamlfind'):
        if shutil.which(tool) is None:
            print(f'{tool} not found on PATH')
            return 1
    version = subprocess.run(['rocq', '--version'], capture_output=True, text=True).stdout.strip()
    t0 = time.time()
    subprocess.run(['rocq', 'makefile', '-f', '_CoqProject', '-o', 'Makefile'], cwd=ROCQ, check=True)
    subprocess.run(['make', 'clean'], cwd=ROCQ, check=True, capture_output=True)
    jobs = str(os.cpu_count() or 1)
    if subprocess.run(['make', '-j', jobs], cwd=ROCQ).returncode != 0:
        print('the build failed')
        return 1
    build = time.time() - t0
    out = subprocess.run(['rocq', 'compile', '-R', '.', 'TH', 'Assumptions.v'], cwd=ROCQ,
                         capture_output=True, text=True)
    for f in os.listdir(ROCQ):
        if f.startswith('Assumptions.') and f != 'Assumptions.v' or f == '.Assumptions.aux':
            os.remove(os.path.join(ROCQ, f))
    if out.returncode != 0:
        print(out.stdout, out.stderr)
        return 1
    names = re.findall(r'^Print Assumptions (\S+)\.$', open(os.path.join(ROCQ, 'Assumptions.v')).read(), re.M)
    # one block per theorem: closed, or the axioms it depends on, each named at the start of a line
    blocks = []
    for line in out.stdout.splitlines():
        if line.startswith('Closed under the global context'):
            blocks.append(None)
        elif line.startswith('Axioms:'):
            blocks.append([])
        elif blocks and blocks[-1] is not None and re.match(r"^[A-Za-z_][\w.']* :", line):
            blocks[-1].append(line.split(' :')[0])
    # the theorems on real numbers use the axioms of the standard library's reals; the values evaluated by the interval
    # tactic also the specifications of the primitive integers and floating-point numbers; all others none
    reals = {'ClassicalDedekindReals.sig_forall_dec', 'ClassicalDedekindReals.sig_not_dec',
             'FunctionalExtensionality.functional_extensionality_dep', 'Classical_Prop.classic'}
    prim = ('Uint63Axioms.', 'Sint63Axioms.', 'FloatAxioms.', 'PrimInt63.', 'PrimFloat.', 'PrimArray.')
    real_modules = ('Lower.', 'Margin.', 'Erfc.', 'Choose.', 'Noise.', 'Restore.', 'FlipLower.')
    theorems = {}
    if len(blocks) != len(names):
        print(out.stdout)
        return 1
    for n, ax in zip(names, blocks):
        if ax is None:
            theorems[n] = 'closed'
        elif n.startswith(real_modules) and set(ax) <= reals:
            theorems[n] = 'reals'
        elif n.startswith('NoiseNum.') and all(a in reals or a.startswith(prim) for a in ax):
            theorems[n] = 'reals, primitive numbers'
        else:
            print(n, ax)
            return 1
    host = host_extraction()
    stored = stored_extraction()
    images = pstar_images()
    ext = subprocess.run([sys.executable, os.path.join(REPO, 'src', 'twohead.py'), 'net', 'extract'],
                         capture_output=True, text=True)
    identical = (ext.returncode == 0 and '"identical": true' in ext.stdout and host['identical']
                 and stored['identical'] and all(images.values()))
    files = [l for l in open(os.path.join(ROCQ, '_CoqProject')).read().split() if l.endswith('.v')]
    lines = sum(len(open(os.path.join(ROCQ, f)).read().splitlines()) for f in files)
    res = dict(rocq=version.splitlines()[0], files=len(files), lines=lines,
               build_seconds=round(build, 1), theorems=theorems,
               host_extraction=host, stored_extraction=stored, pstar_images=images,
               extraction_identical=identical)
    rec = json.load(open(RECORD)) if os.path.exists(RECORD) else {}
    rec.update(res)
    json.dump(rec, open(RECORD, 'w'), indent=1)
    print(json.dumps(res, indent=1))
    return 0 if identical else 1

_DTORD = {"F64": 0, "F32": 1, "F16": 2, "I64": 3, "I32": 4, "I16": 5, "I8": 6,
          "U8": 7, "BOOL": 8}


def resigma(data: bytes) -> bytes:
    """Serialize the netlist that `data` denotes."""
    net, inputs, outputs, meta = net_of_sigma(data)
    return sigma_of_net(net, inputs, outputs, meta["machine"],
                        json.loads(meta["signal_registry"]),
                        json.loads(meta["io"]))


def main_sigma() -> int:
    rebuilt = sigma_host()
    dist = open(HOST_PATH, "rb").read()
    same = rebuilt == dist
    n = struct.unpack("<Q", dist[:8])[0]
    h = json.loads(dist[8:8 + n])
    meta = h.pop("__metadata__")
    order = list(h)
    by_dtype_name = order == sorted(order, key=lambda k: (_DTORD[h[k]["dtype"]], k))
    signed_int = all(h[k]["dtype"] in ("I8", "I16", "I32", "I64") for k in order)
    print(f"rebuild from source equals the distributed encoding byte for byte: {same}")
    print(f"  bytes {len(dist):,}   header {n:,}   tensor entries {len(order)}")
    print(f"  metadata keys in order: {list(meta)}")
    print(f"  tensor entries ordered by (element type, name): {by_dtype_name}")
    print(f"  every element type is a signed integer type: {signed_int}")
    print(f"  data begins at offset {8+n}, which is 8-aligned: {(8+n) % 8 == 0}")
    print(f"  header padded with {len(dist[8:8+n]) - len(dist[8:8+n].rstrip(b' '))} spaces")

    again = sigma_host()
    print(f"  two independent builds agree: {again == rebuilt}")
    from host import sigma as family_sigma
    vec = family_sigma(8) == dist
    print(f"  the vectorized writer produces the same bytes: {vec}")

    # sigma(sigma^-1(s)) = s on the image: the encoding determines the netlist
    # and the netlist determines the encoding.
    round_trip = resigma(dist) == dist
    print(f"  the netlist the encoding denotes serializes back to it: {round_trip}")

    net, inputs, outputs = host_netlist()
    built, _, _, _ = net_of_sigma(dist)
    entries = sum(len(i) for i, _ in built.gates.values())
    print(f"  {len(built.gates):,} units and {entries:,} predecessor entries "
          f"recovered from the file alone, on {len(inputs):,} state bits")

    # the netlist recovered from the file computes the transition the source
    # netlist computes, on states no trajectory visits
    gen = torch.Generator().manual_seed(41)
    V = (torch.rand(64, len(inputs), generator=gen) < 0.5).float()
    src = gate_by_gate(net, inputs, outputs, V)
    rec_net, rec_in, rec_out, _ = net_of_sigma(dist)
    rec = gate_by_gate(rec_net, rec_in, rec_out, V)
    agree = bool((src == rec).all())
    print(f"  it computes the transition of the source netlist on 64 uniformly "
          f"random states: {agree}")

    ok = (same and again == rebuilt and vec and round_trip and agree and by_dtype_name
          and signed_int)
    return 0 if ok else 1


def census(r: bytes):
    """(literal tokens, repeat tokens, bytes from each) of a recipe."""
    i = 0
    lit = rep = f_lit = f_rep = 0
    while True:
        t = r[i]
        i += 1
        if t == 0:
            return lit, rep, f_lit, f_rep
        if t <= 127:
            lit += 1
            f_lit += t
            i += t
        else:
            rep += 1
            f_rep += 256 - t
            i += 1


def steps_P(r: bytes) -> int:
    """Closed form for the run of the constructor P on a recipe."""
    lit, rep, f_lit, f_rep = census(r)
    return 5 * f_lit + 4 * f_rep + 7 * lit + 9 * rep + 8


def steps_P_star(tau: bytes):
    """Closed form for the three phases of P* on its own description tape."""
    lit, rep, f_lit, f_rep = census(tau)
    a = 5 * f_lit + 4 * f_rep + 7 * lit + 9 * rep + 7
    return {"A": a, "R": 1, "B": 6 * len(tau) + 2}


def upper_bound(r: bytes) -> int:
    """5|delta(r)| + 9k + 8 with k the number of tokens, k <= (|r|-1)/2."""
    lit, rep, f_lit, f_rep = census(r)
    return 5 * (f_lit + f_rep) + 9 * (lit + rep) + 8


def coarse_bound(r: bytes) -> int:
    return 5 * len(decode(r)) + (9 * (len(r) - 1)) // 2 + 8


def phase_split(mem0, tau: bytes):
    mem = list(mem0)
    dev = Tape(tau)
    pc = 0
    counts = {"A": 0, "R": 0, "B": 0}
    while pc != HALT_PC:
        counts["A" if pc < 3 * 20 else ("R" if pc == 3 * 20 else "B")] += 1
        A = mem[pc]
        B = mem[(pc + 1) & 0xFF]
        C = mem[(pc + 2) & 0xFF]
        r = (mem[B] - mem[A]) & 0xFF
        mem[B] = r
        pc = C if (r == 0 or r >= 0x80) else (pc + 3) & 0xFF
        dev.apply(mem)
    return counts


def main_steps() -> int:
    out = {}
    ok = True
    sigma = open(HOST_PATH, "rb").read()

    named = [("r_H = describe(sigma(N_host))", describe(sigma)),
             ("the all-literal encoding of sigma(N_host)", describe_literal(sigma)),
             ("tau* (the self-reproducing tape)", tau_star(sigma, M_STAR))]
    rows = []
    for label, r in named:
        _, n = run_reference(M_P, r)
        pred = steps_P(r)
        rows.append({"tape": label, "recipe_bytes": len(r), "output_bytes":
                     len(decode(r)), "steps": n, "closed_form": pred,
                     "agrees": n == pred, "upper": upper_bound(r),
                     "coarse": coarse_bound(r)})
        print(f"  {label}: {n:,} steps, closed form {pred:,}, "
              f"{'agree' if n == pred else 'DISAGREE'}; "
              f"bound 5|f|+9k+8 = {upper_bound(r):,}", flush=True)
        ok &= n == pred and n <= upper_bound(r) <= coarse_bound(r)
    out["named"] = rows

    # random recipes: both encoders, and strings built to force each token kind
    rng = random.Random(1009)
    bad = 0
    tested = 0
    for _ in range(400):
        n = rng.randrange(0, 700)
        alpha = rng.choice([1, 2, 3, 17, 256])
        f = bytes(rng.randrange(alpha) for _ in range(n))
        for enc in (describe, describe_literal):
            r = enc(f)
            _, s = run_reference(M_P, r)
            tested += 1
            if s != steps_P(r) or s > upper_bound(r) or upper_bound(r) > coarse_bound(r):
                bad += 1
    print(f"  {tested:,} random runs of P: closed form exact and within the "
          f"bound on every one: {'yes' if bad == 0 else f'NO ({bad})'}", flush=True)
    ok &= bad == 0
    out["random_runs"] = tested
    out["random_failures"] = bad

    # the three phases of P*
    tau = tau_star(sigma, M_STAR)
    measured = phase_split(M_STAR, tau)
    pred = steps_P_star(tau)
    agree = measured == pred
    print(f"  P* phases measured {measured}, closed form {pred}: "
          f"{'agree' if agree else 'DISAGREE'}", flush=True)
    print(f"  total {sum(measured.values()):,} = {sum(pred.values()):,}", flush=True)
    ok &= agree
    out["phases_measured"] = measured
    out["phases_closed_form"] = pred
    out["total"] = sum(pred.values())

    # phase B is six steps per tape byte and two more, over recipes of every
    # shape; P* is run only on recipes, on which it halts
    bbad = 0
    probes = 0
    for _ in range(40):
        for enc in (describe, describe_literal):
            probe = enc(bytes(rng.randrange(rng.choice([2, 4, 256]))
                              for _ in range(rng.randrange(0, 200))))
            got = phase_split(M_STAR, probe)
            probes += 1
            if got != steps_P_star(probe):
                bbad += 1
    print(f"  phase B = 6|tau| + 2 and phase R = 1 on {probes} further recipes: "
          f"{'yes' if bbad == 0 else f'NO ({bbad})'}", flush=True)
    ok &= bbad == 0
    out["phase_b_failures"] = bbad

    json.dump(out, open(runs_path("paper_steps.json"), "w"), indent=1)
    return 0 if ok else 1


def predicate(n: int):
    """[r <= 0] for r read in two's complement on `n` bits, as a 2^n vector."""
    rows = []
    for v in range(1 << n):
        two_c = v - (1 << n) if v >> (n - 1) else v
        rows.append(1 if two_c <= 0 else 0)
    return torch.tensor(rows, dtype=torch.long)


def bitmatrix(n: int):
    """Row v holds the bits r_0 .. r_{n-1} of v, least significant first."""
    return torch.tensor([[(v >> i) & 1 for i in range(n)] for v in range(1 << n)],
                        dtype=torch.long)


def ternary_units_computing(n: int, target, bias_range):
    """Every (w, b) in {-1,0,1}^n x bias_range whose unit computes `target`."""
    X = bitmatrix(n)
    found = []
    total = 0
    for w in itertools.product((-1, 0, 1), repeat=n):
        pre = X @ torch.tensor(w, dtype=torch.long)
        for b in bias_range:
            total += 1
            if bool(((pre + b >= 0).long() == target).all()):
                found.append((w, b))
    return found, total


def main_ternarity() -> int:
    out = {}
    ok = True

    # The predicate is a threshold function of the eight result bits, realized
    # by one unit whose weights are the positional values of the bits.
    n = 8
    target = predicate(n)
    X = bitmatrix(n)
    big = torch.tensor([-(1 << i) for i in range(n - 1)] + [1 << (n - 1)],
                       dtype=torch.long)
    exact = bool(((X @ big >= 0).long() == target).all())
    print(f"  one integer-weight unit with weights "
          f"(-1,-2,-4,-8,-16,-32,-64,+128) and bias 0 computes [r <= 0] on all "
          f"{1 << n} results: {'yes' if exact else 'NO'}")
    ok &= exact
    out["integer_unit_exact"] = exact
    out["integer_unit_max_weight"] = int(big.abs().max())

    # No ternary unit does, for any integer bias. A bias outside [-n, n] makes
    # the unit constant, so the sweep below is exhaustive over all biases.
    bias_range = range(-(n + 2), n + 3)
    found, total = ternary_units_computing(n, target, bias_range)
    print(f"  ternary units on the eight result bits enumerated: {total:,} "
          f"(all {3 ** n:,} weight vectors, biases {bias_range.start} to "
          f"{bias_range.stop - 1})")
    print(f"  ternary units computing [r <= 0]: {len(found)}"
          f"{'  (none, as the proposition asserts)' if not found else f'  {found[:3]}'}")
    ok &= not found
    out["ternary_units_enumerated"] = total
    out["ternary_units_computing_predicate"] = len(found)
    # A unit with p weights +1 and q weights -1 is constant unless
    # -p <= b <= q - 1; those biases lie inside the swept range.
    nonconst = sum(sum(1 for x in w if x) for w in itertools.product((-1, 0, 1), repeat=n))
    print(f"  of these, {nonconst:,} are not constant, and none of them computes "
          f"[r <= 0]")
    out["nonconstant_ternary_units"] = nonconst

    # The separation begins at three bits: on two bits the predicate is ternary.
    firstfail = None
    widths = {}
    for m in range(2, 9):
        f, _ = ternary_units_computing(m, predicate(m), range(-(m + 2), m + 3))
        widths[m] = len(f)
        if not f and firstfail is None:
            firstfail = m
    print(f"  ternary realizations by width: {widths}; the predicate stops "
          f"being a ternary threshold function at {firstfail} bits")
    out["ternary_realizations_by_width"] = widths
    out["first_width_without_ternary_unit"] = firstfail
    ok &= firstfail == 3

    # Depth two suffices, by the cell the host uses.
    z = (X.sum(dim=1) == 0).long()
    leq = ((X[:, n - 1] + z) >= 1).long()
    two = bool((leq == target).all())
    print(f"  the depth-two cell OR(r_7, z(r)) of the host computes it on all "
          f"{1 << n} results: {'yes' if two else 'NO'}")
    ok &= two
    out["depth_two_cell_exact"] = two

    # The 256-way address decoder is not an instance of the same exchange: it
    # is one ternary unit already.
    from machines import Net
    net = Net()
    bits = [f"a{i}" for i in range(8)]
    net.DECODE("sel", bits, 0xA7)
    ins, bias = net.gates["sel"]
    dec_ternary = all(w in (-1, 0, 1) for _, w in ins)
    A = bitmatrix(8)
    # DECODE reads its bits most significant first
    w = torch.tensor([wt for _, wt in ins], dtype=torch.long)
    pre = A.flip(1) @ w + bias
    hit = (pre >= 0).long()
    dec_exact = bool((hit == (torch.arange(256) == 0xA7).long()).all())
    print(f"  the address decoder of the memory is one ternary unit of fan-in "
          f"eight and fires on exactly one address: "
          f"{'yes' if dec_ternary and dec_exact else 'NO'}")
    ok &= dec_ternary and dec_exact
    out["decoder_is_one_ternary_unit"] = dec_ternary and dec_exact

    json.dump(out, open(runs_path("paper_ternarity.json"), "w"), indent=1)
    return 0 if ok else 1

BUDGET = 1 << 22


def sha(b: bytes) -> str:
    return hashlib.sha256(b).hexdigest()


def out_path(name: str) -> str:
    d = os.path.join(REPO, "paper", "runs")
    os.makedirs(d, exist_ok=True)
    return os.path.join(d, f"paper_runs_{name}.json")


def runs_phase_split(mem0: List[int], tau: bytes) -> Dict[str, int]:
    """Steps spent in each phase of P*, counted on the reference."""
    mem = list(mem0)
    dev = Tape(tau)
    pc = 0
    counts = {"A": 0, "R": 0, "B": 0}
    while pc != HALT_PC:
        phase = "A" if pc < 3 * 20 else ("R" if pc == 3 * 20 else "B")
        counts[phase] += 1
        A = mem[pc]
        B = mem[(pc + 1) & 0xFF]
        C = mem[(pc + 2) & 0xFF]
        r = (mem[B] - mem[A]) & 0xFF
        mem[B] = r
        pc = C if (r == 0 or r >= 0x80) else (pc + 3) & 0xFF
        dev.apply(mem)
    return counts


class Reference:
    """The integer reference, in the interface the generations loop expects."""

    info = {"evaluator": "integer reference"}
    build_seconds = 0.0

    def __init__(self, sigma: bytes):
        self.sigma = sigma

    def run(self, mem0, tau, max_steps, expect=None, progress=0):
        return run_reference(mem0, tau, max_steps=max_steps, expect=expect)


def generations(build, label: str, n_gen: int = 3, progress: int = 0) -> Dict:
    """Run n_gen generations, each instantiated only from the previous output."""
    sigma0 = read_host()
    tau0 = tau_star(sigma0, M_STAR)
    target = ser(sigma0, bytes(M_STAR), tau0)
    rec = []
    sigma, m, tau = sigma0, list(M_STAR), tau0
    for k in range(n_gen):
        t0 = time.perf_counter()
        ev = build(sigma)
        t_build = time.perf_counter() - t0
        t0 = time.perf_counter()
        out, steps = ev.run(m, tau, max_steps=BUDGET, expect=target,
                            progress=progress)
        dt = time.perf_counter() - t0
        d = sha(out)
        rec.append({"generation": k + 1, "bytes": len(out), "steps": steps,
                    "sha256": d, "seconds": dt, "instantiate_seconds": t_build,
                    "equals_ser": out == ser(sigma, bytes(m), tau)})
        print(f"    [{label}] generation {k+1}: instantiated in "
              f"{t_build:.1f} s, {len(out):,} bytes in {steps:,} steps, "
              f"{dt/60:.1f} min, sha {d[:16]}, "
              f"Out = ser(Omega): {rec[-1]['equals_ser']}", flush=True)
        sigma, mb, tau = inst(out)
        m = list(mb)
        if sigma != sigma0 or m != list(M_STAR) or tau != tau0:
            raise AssertionError(f"generation {k+1} did not reproduce the instance")
    digests = {r["sha256"] for r in rec}
    print(f"    [{label}] all {n_gen} generations identical: {len(digests) == 1}",
          flush=True)
    return {"generations": rec, "digests_coincide": len(digests) == 1,
            "target_sha256": sha(target), "target_bytes": len(target)}


def main_runs() -> int:
    ap = argparse.ArgumentParser()
    ap.add_argument("mode", choices=["reference", "net", "lev", "lockstep"])
    ap.add_argument("--generations", type=int, default=3)
    ap.add_argument("--device", default="cuda")
    ap.add_argument("--lockstep-steps", type=int, default=20000)
    ap.add_argument("--dense", action="store_true",
                    help="evaluate Lev(N_host) as dense matrices")
    args = ap.parse_args()

    sigma = read_host()
    r_H = describe(sigma)
    tau = tau_star(sigma, M_STAR)
    target = ser(sigma, bytes(M_STAR), tau)
    res: Dict = {"sigma_bytes": len(sigma), "sigma_sha256": sha(sigma),
                 "r_H_bytes": len(r_H), "tau_star_bytes": len(tau),
                 "ser_bytes": len(target), "ser_sha256": sha(target),
                 "P_instructions": len(P), "P_star_instructions": len(P_STAR)}

    if args.mode == "reference":
        print("[reference] self-description")
        t0 = time.perf_counter()
        out, n = run_reference(M_P, r_H, expect=sigma)
        res["selfdesc"] = {"bytes": len(out), "steps": n,
                           "seconds": time.perf_counter() - t0,
                           "exact": out == sigma, "sha256": sha(out)}
        print(f"    {len(out):,} bytes in {n:,} steps, exact={out == sigma}")
        print("[reference] self-reproduction, three generations")
        res["selfrep"] = generations(Reference, "reference", args.generations)
        res["phase_steps"] = runs_phase_split(M_STAR, tau)
        print(f"    phase split: {res['phase_steps']}")

    elif args.mode == "net":
        build = lambda s: NetEvaluator(s, device=args.device,
                                       graph=args.device.startswith("cuda"))
        E = build(sigma)
        res["evaluator"] = "the netlist of sigma, unit by unit"
        res["net_info"] = {k: int(v) for k, v in E.info.items()}
        print(f"[net] {E.info['units']:,} units over {E.info['levels']} levels, "
              f"{E.info['entries']:,} predecessor entries, built in "
              f"{E.build_seconds:.1f} s", flush=True)
        print("[net] self-description", flush=True)
        t0 = time.perf_counter()
        out, n = E.run(M_P, r_H, max_steps=BUDGET, expect=sigma, progress=200000)
        res["selfdesc"] = {"bytes": len(out), "steps": n,
                           "seconds": time.perf_counter() - t0,
                           "exact": out == sigma, "sha256": sha(out)}
        print(f"    {len(out):,} bytes in {n:,} steps "
              f"({res['selfdesc']['seconds']/60:.1f} min), exact={out == sigma}")
        print("[net] self-reproduction, three generations", flush=True)
        res["selfrep"] = generations(build, "net", args.generations, 200000)

    elif args.mode == "lev":
        build = lambda s: LevEvaluator(
            s, device=args.device, dense=args.dense,
            graph=(not args.dense) and args.device.startswith("cuda"))
        E = build(sigma)
        res["lev_info"] = {k: int(v) for k, v in E.info.items()
                           if isinstance(v, (int, float))}
        res["lev_form"] = ("dense matrices" if args.dense
                           else "nonzero entries, CUDA graph")
        print(f"[lev] {E.info['size']:,} units over {E.info['layers']} layers, "
              f"maximal width {E.info['max_width']:,}, "
              f"{E.info['total_weights']:,} entries of which "
              f"{E.info['nonzero']:,} are nonzero; built in "
              f"{E.build_seconds:.1f} s as "
              f"{'dense matrices' if args.dense else 'its nonzero entries'}",
              flush=True)
        print("[lev] self-reproduction", flush=True)
        res["selfrep"] = generations(build, "lev", args.generations, 200000)

    elif args.mode == "lockstep":
        print(f"[lockstep] reference vs the netlist of sigma vs Lev(N_host) "
              f"dense and sparse, {args.lockstep_steps:,} steps of generation 1",
              flush=True)
        import torch
        N = NetEvaluator(sigma, device=args.device,
                         graph=args.device.startswith("cuda"))
        D = LevEvaluator(sigma, device=args.device, dense=True)
        S = LevEvaluator(sigma, device=args.device, dense=False)
        rmem = list(M_STAR); rpc = 0; rdev = Tape(tau)
        states, devs = [], []
        for E in (N, D, S):
            states.append(E._vec(0, M_STAR).unsqueeze(0).to(args.device))
            devs.append(Tape(tau))
        pow2 = [1 << (7 - k) for k in range(8)]
        bad = 0
        t0 = time.perf_counter()
        for n in range(args.lockstep_steps):
            A = rmem[rpc]; B = rmem[(rpc + 1) & 0xFF]; C = rmem[(rpc + 2) & 0xFF]
            r = (rmem[B] - rmem[A]) & 0xFF
            rmem[B] = r
            rpc = C if (r == 0 or r >= 0x80) else (rpc + 3) & 0xFF
            rdev.apply(rmem)
            mems, pcs = [], []
            for i, E in enumerate((N, D, S)):
                v = E.step(states[i])
                vc = v[0].cpu()
                cells = {j: E._byte(vc, j) for j in E._DEVCELLS}
                sh = [0] * 256
                for j, val in cells.items():
                    sh[j] = val
                devs[i].apply(sh)
                for j, val in cells.items():
                    if sh[j] != val:
                        E._set_byte(v, j, sh[j])
                states[i] = v
                vc = v[0].cpu()
                pcs.append(sum(p for p, k in zip(pow2, range(8))
                               if int(vc[k])))
                mems.append([E._byte(vc, j) for j in range(256)])
            if not (all(m == rmem for m in mems) and all(p == rpc for p in pcs)
                    and all(d.out == rdev.out for d in devs)
                    and all(d.h == rdev.h for d in devs)):
                print(f"    DIVERGENCE at step {n}")
                bad += 1
                break
            if n and n % 2000 == 0:
                print(f"      {n:,} steps agreed "
                      f"({n/(time.perf_counter()-t0):.0f} steps/s, "
                      f"{len(rdev.out):,} bytes)", flush=True)
        res["lockstep"] = {"steps": args.lockstep_steps, "divergences": bad,
                           "bytes": len(rdev.out),
                           "seconds": time.perf_counter() - t0}
        print(f"    {args.lockstep_steps:,} steps: full state, tape head and "
              f"output word equal on all four evaluators: {bad == 0}")

    name = args.mode
    if args.mode == "lev":
        name = "lev_dense" if args.dense else "lev_sparse"
    p = out_path(name)
    json.dump(res, open(p, "w"), indent=1)
    print(f"wrote {p}")
    return 0


def levelize_net(net, inputs: List[str], outputs: List[str]) -> Dict:
    """The level assignment of matrix8.compile_net, counted and not built."""
    allgates = net.gates
    level: Dict[str, int] = {s: 0 for s in inputs}
    consumers: Dict[str, List[str]] = defaultdict(list)
    indeg: Dict[str, int] = {}
    for gname, (ins, _) in allgates.items():
        indeg[gname] = len([s for s, _ in ins if s in allgates])
        for s, _ in ins:
            consumers[s].append(gname)
    order = [g for g, d in indeg.items() if d == 0]
    i = 0
    while i < len(order):
        for c in consumers.get(order[i], []):
            indeg[c] -= 1
            if indeg[c] == 0:
                order.append(c)
        i += 1
    if len(order) != len(allgates):
        raise ValueError("cycle")
    for gname in order:
        ins, _ = allgates[gname]
        level[gname] = 1 + max((level[s] for s, _ in ins), default=0)

    live: set = set()
    stack = [s for s in outputs if s in allgates]
    while stack:
        g = stack.pop()
        if g in live:
            continue
        live.add(g)
        for s, _ in allgates[g][0]:
            if s in allgates and s not in live:
                stack.append(s)
    gates = {g: allgates[g] for g in live}

    kmax = max(level[g] for g in gates)
    K = kmax

    last_use: Dict[str, int] = {}
    for gname, (ins, _) in gates.items():
        for s, _ in ins:
            last_use[s] = max(last_use.get(s, 0), level[gname])
    for s in outputs:
        if s not in ("#0", "#1"):
            last_use[s] = K

    by_level: Dict[int, List[str]] = defaultdict(list)
    for gname in gates:
        by_level[level[gname]].append(gname)

    vec = list(inputs)
    widths = [len(vec)]
    n_new, n_pass = [], []
    for lv in range(1, K + 1):
        if lv < K:
            new_gates = sorted(by_level.get(lv, []))
            passes = [s for s in vec if last_use.get(s, 0) > lv]
            rows = new_gates + passes
            n_new.append(len(new_gates))
            n_pass.append(len(passes))
        else:
            rows = list(outputs)
            new_here = sum(1 for s in rows if s in gates and level[s] == lv)
            n_new.append(new_here)
            n_pass.append(len(rows) - new_here)
        widths.append(len(rows))
        vec = rows

    fanins = [len(ins) for ins, _ in gates.values()]
    biases = [b for _, b in gates.values()]
    nonzero = sum(fanins)
    return {
        "depth": K,
        "gates": len(gates),
        "netlist_gates": len(allgates),
        "state_bits": len(inputs),
        "widths": widths,
        "M": sum(widths[1:]),
        "dense_entries": sum(widths[i] * widths[i + 1] for i in range(len(widths) - 1)),
        "identity_units": sum(n_pass),
        "new_units": sum(n_new),
        "max_fanin_netlist": max(fanins),
        "nonzero_weights_netlist": nonzero,
        "bias_min": min(biases),
        "bias_max": max(biases),
        "fanin_hist": dict(sorted(Counter(fanins).items())),
    }


DATAPATH = ["p + 3", "subtractor", "zero test", "branch", "counter and halt override",
            "halt latch"]

MEMORY = ["decode p", "operand fetch", "decode A and B", "read mux", "write cells"]

_COMPONENT = {
    "P": "decode p", "FA": "operand fetch", "F": "operand fetch",
    "PA": "decode A and B", "PB": "decode A and B",
    "RX": "read mux", "RY": "read mux", "X": "read mux", "Y": "read mux",
    "W": "write cells", "KP": "write cells", "WR": "write cells", "NM": "write cells",
    "Q": "p + 3",
    "PR": "subtractor", "T": "subtractor", "C": "subtractor", "O": "subtractor",
    "N": "subtractor", "R": "subtractor", "H": "subtractor",
    "AX": "zero test", "NX": "zero test", "XN": "zero test", "EQ": "zero test",
    "LEQ": "branch",
    "HP": "counter and halt override", "TA": "counter and halt override",
    "TB": "counter and halt override", "NP": "counter and halt override",
    "AC": "halt latch", "HA": "halt latch", "HB": "halt latch", "NH": "halt latch",
}


def component(name: str) -> str:
    """The block of the host that a unit of host_family.build belongs to."""
    import re
    return _COMPONENT[re.match(r"[A-Z]+", name).group(0)]


def host_component_table() -> Dict:
    """Per-component counts of the step netlist of the host."""
    from host import host_netlist
    net, inputs, outputs = host_netlist()
    d: Dict[str, int] = {}
    rows: Dict[str, Dict] = {}
    for name, (ins, _) in net.gates.items():
        d[name] = 1 + max((d.get(x, 0) for x, _ in ins), default=0)
        c = component(name)
        r = rows.setdefault(c, {"units": 0, "weights": 0, "max_fanin": 0,
                                "level_lo": 10 ** 9, "level_hi": 0})
        r["units"] += 1
        r["weights"] += len(ins)
        r["max_fanin"] = max(r["max_fanin"], len(ins))
        r["level_lo"] = min(r["level_lo"], d[name])
        r["level_hi"] = max(r["level_hi"], d[name])
    return {
        "rows": rows,
        "built_units": len(net.gates),
        "units": len(net.gates),
        "weights": sum(r["weights"] for r in rows.values()),
        "datapath_units": sum(rows[k]["units"] for k in DATAPATH if k in rows),
        "datapath_weights": sum(rows[k]["weights"] for k in DATAPATH if k in rows),
        "memory_units": sum(rows[k]["units"] for k in MEMORY if k in rows),
        "memory_weights": sum(rows[k]["weights"] for k in MEMORY if k in rows),
    }


def main_stats() -> int:
    out = {}
    print("=" * 74)
    print(" The step netlist of the host, by component")
    print("=" * 74)
    h = host_component_table()
    for name in DATAPATH + MEMORY:
        if name not in h["rows"]:
            continue
        d = h["rows"][name]
        lv = (f"{d['level_lo']}" if d["level_lo"] == d["level_hi"]
              else f"{d['level_lo']}-{d['level_hi']}")
        print(f"  {name:<18} units={d['units']:>6}  weights={d['weights']:>6}  "
              f"levels={lv:<7} max eff fan-in={d['max_fanin']}")
    print(f"  {'datapath':<18} units={h['datapath_units']:>6}  "
          f"weights={h['datapath_weights']:>6}")
    print(f"  {'memory':<18} units={h['memory_units']:>6}  "
          f"weights={h['memory_weights']:>6}")
    print(f"  {'step netlist':<18} units={h['units']:>6}  "
          f"weights={h['weights']:>6}")
    out["host_components"] = h

    print()
    print("=" * 74)
    print(" Lev(N_host): levelization of the SUBLEQ step circuit")
    print("=" * 74)
    from host import net_of_sigma
    from host import read_host
    net, inputs, outputs, _ = net_of_sigma(read_host())
    lev = levelize_net(net, inputs, outputs)
    for k in ("depth", "gates", "netlist_gates", "state_bits", "M",
              "dense_entries", "identity_units",
              "new_units", "max_fanin_netlist", "nonzero_weights_netlist",
              "bias_min", "bias_max"):
        print(f"  {k:<26} {lev[k]:,}" if isinstance(lev[k], int) else f"  {k:<26} {lev[k]}")
    print(f"  fan-in histogram          {lev['fanin_hist']}")
    print(f"  widths                    {lev['widths']}")
    out["lev_host"] = lev

    path = runs_path("paper_stats.json")
    json.dump(out, open(path, "w"), indent=1)
    print(f"\nwrote {path}")
    return 0

R: Dict = {}


def family_files() -> List[str]:
    files = [os.path.join(REPO, "neural_computer.safetensors")]
    vdir = os.path.join(REPO, "variants")
    files += sorted(os.path.join(vdir, f) for f in os.listdir(vdir)
                    if f.endswith(".safetensors"))
    return files


# ---------------------------------------------------------------------------
def check_codec():
    from host import describe, describe_literal, decode
    print("[1] Recipe language")
    files = family_files()
    total = 0
    bad = 0
    tape_total = 0
    for p in files:
        data = open(p, "rb").read()
        r = describe(data)
        if decode(r) != data:
            bad += 1
        total += len(data)
        tape_total += len(r)
    print(f"    delta(describe(f)) = f on all {len(files)} artifact files "
          f"({total:,} bytes -> {tape_total:,} bytes of recipe): "
          f"{'all exact' if bad == 0 else f'{bad} FAILED'}")

    # the length bound of the completeness lemma, with c1 = 1, c2 = 127, c3 = 1
    worst = 0.0
    lb = 0
    for p in files:
        data = open(p, "rb").read()
        rl = describe_literal(data)
        assert decode(rl) == data
        bound = len(data) + -(-len(data) // 127) + 1
        assert len(rl) == bound, (len(rl), bound)
        lb += 1
    # exhaustive on short strings
    import random
    rng = random.Random(0)
    ebad = 0
    for n in range(0, 600):
        s = bytes(rng.randrange(256) for _ in range(n))
        for enc in (describe, describe_literal):
            r = enc(s)
            if decode(r) != s:
                ebad += 1
        if len(describe_literal(s)) != len(s) + -(-len(s) // 127) + 1:
            ebad += 1
    print(f"    literal encoding meets |r| = |f| + ceil(|f|/127) + 1 on all "
          f"{len(files)} files and on 600 random strings: "
          f"{'exact' if ebad == 0 else 'FAILED'}")
    R["codec"] = {"files": len(files), "bytes": total, "recipe_bytes": tape_total,
                  "roundtrip_failures": bad, "bound_failures": ebad}


# ---------------------------------------------------------------------------
def check_framing():
    from host import ser, inst, M_STAR, M_P, read_host, tau_star, describe
    print("[2] Framing")
    sigma = read_host()
    bad = 0
    cases = [(sigma, M_STAR, tau_star(sigma, M_STAR)),
             (sigma, M_P, describe(b"")),
             (b"", M_P, b"\x00"),
             (b"\x00" * 3, M_STAR, b"")]
    for sg, m, tau in cases:
        s = ser(sg, bytes(m), tau)
        got = inst(s)
        if got != (sg, bytes(m), tau):
            bad += 1
    print(f"    inst(ser(Omega)) = Omega on {len(cases)} instances: "
          f"{'exact' if bad == 0 else 'FAILED'}")
    R["framing"] = {"cases": len(cases), "failures": bad}


# ---------------------------------------------------------------------------
def check_serialization():
    """Rebuilding the host from source reproduces its encoding byte for byte."""
    print("[3] Canonical serialization")
    import struct
    from host import read_host, sigma_host
    original = read_host()
    rebuilt = sigma_host()
    deterministic = sigma_host() == rebuilt
    same = rebuilt == original
    round_trip = resigma(original) == original
    print(f"    rebuild from source is byte-identical: {same} "
          f"({len(original):,} bytes, sha {sha(original)[:16]})")
    print(f"    two independent builds agree: {deterministic}")
    print(f"    the netlist the encoding denotes serializes back to it: "
          f"{round_trip}")
    n = struct.unpack("<Q", original[:8])[0]
    hdr = json.loads(original[8:8 + n])
    meta = hdr.pop("__metadata__", {})
    keys = list(hdr)
    dtypes = sorted({v["dtype"] for v in hdr.values()})
    order = {"F64": 0, "F32": 1, "F16": 2, "I64": 3, "I32": 4, "I16": 5,
             "I8": 6, "U8": 7, "BOOL": 8}
    by_dtype_name = keys == sorted(keys, key=lambda k: (order[hdr[k]["dtype"]], k))
    pad = len(original[8:8 + n]) - len(original[8:8 + n].rstrip(b" "))
    print(f"    header {n:,} bytes, {len(keys)} tensors, dtypes {dtypes}, "
          f"metadata keys {sorted(meta)}")
    print(f"    tensor entries ordered by (element type, name): {by_dtype_name}; "
          f"data begins at {8+n:,}, 8-aligned: {(8 + n) % 8 == 0}, "
          f"{pad} bytes of padding")
    R["serialization"] = {"byte_identical": same, "deterministic": deterministic,
                          "round_trip": round_trip,
                          "bytes": len(original), "sha256": sha(original),
                          "header_bytes": n, "tensors": len(keys),
                          "dtypes": dtypes, "metadata_keys": sorted(meta),
                          "ordered_by_dtype_then_name": by_dtype_name,
                          "data_offset": 8 + n, "header_padding": pad}


# ---------------------------------------------------------------------------
def _batch_vectors(m, p, device):
    """State vectors for a batch of (memory image, counter) pairs."""
    import torch
    v = torch.zeros(len(p), 2057, device=device)
    for k in range(8):
        v[:, k] = ((p >> (7 - k)) & 1).float()
        v[:, 9 + k::8] = ((m >> (7 - k)) & 1).float()
    return v


def _bytes_of(v):
    """The counter and the 256 memory bytes of every state of a batch."""
    import torch
    pw = torch.tensor([1 << (7 - k) for k in range(8)], dtype=torch.long,
                      device=v.device)
    q = v.detach().long()
    pc = (q[:, :8] * pw).sum(1)
    mem = (q[:, 9:].reshape(q.shape[0], 256, 8) * pw).sum(2)
    return pc, mem


def _reference_batch(mem, pc):
    """One step of Definition 5.2 on a batch of memory images and counters."""
    import torch
    take = lambda idx: mem.gather(1, idx.unsqueeze(1)).squeeze(1)
    A = take(pc)
    B = take((pc + 1) & 0xFF)
    C = take((pc + 2) & 0xFF)
    r = (take(B) - take(A)) & 0xFF
    out = mem.clone()
    out.scatter_(1, B.unsqueeze(1), r.unsqueeze(1))
    leq = (r == 0) | (r >= 0x80)
    return out, torch.where(leq, C, (pc + 3) & 0xFF)


def check_host_datapath():
    """One step of the netlist of sigma(N_host) against Definition 5.2 on all operand and counter pairs."""
    print("[4] Host datapath")
    import torch
    from host import NetEvaluator, read_host
    device = "cuda" if torch.cuda.is_available() else "cpu"
    E = NetEvaluator(read_host(), device=device)

    def sweep(mems, pcs, chunk=256):
        bad = 0
        for i in range(0, len(pcs), chunk):
            m = mems[i:i + chunk].to(device)
            p = pcs[i:i + chunk].to(device)
            got_pc, got_mem = _bytes_of(E.step(_batch_vectors(m, p, device)))
            want_mem, want_pc = _reference_batch(m, p)
            bad += int(((got_mem != want_mem).any(1)
                        | (got_pc != want_pc)).sum())
        return bad

    a = torch.arange(65536) % 256
    b = torch.arange(65536) // 256
    mems = torch.zeros(65536, 256, dtype=torch.long)
    mems[:, 0], mems[:, 1], mems[:, 2] = 0x90, 0x91, 0x30
    mems[:, 0x90] = a
    mems[:, 0x91] = b
    bad_ops = sweep(mems, torch.zeros(65536, dtype=torch.long))
    print(f"    one step against Definition 5.2 over all 65,536 operand pairs: "
          f"{'exact' if bad_ops == 0 else f'{bad_ops} FAILED'}")

    pc = torch.arange(65536) // 256
    c = torch.arange(65536) % 256
    mems = torch.zeros(65536, 256, dtype=torch.long)
    mems[:, 0xA0], mems[:, 0xA1] = 4, 5
    rows = torch.arange(65536)
    mems[rows, pc] = 0xA0
    mems[rows, (pc + 1) % 256] = 0xA1
    mems[rows, (pc + 2) % 256] = c
    bad_ctr = sweep(mems, pc)
    print(f"    one step against Definition 5.2 over all 65,536 (pc, C) pairs, "
          f"the counter wrapping across the top of memory: "
          f"{'exact' if bad_ctr == 0 else f'{bad_ctr} FAILED'}")
    R["datapath"] = {"operand_pairs": 65536, "operand_failures": bad_ops,
                     "counter_pairs": 65536, "counter_failures": bad_ctr}


# ---------------------------------------------------------------------------
def check_lev_sparse_dense():
    """The sparse and dense evaluations of Lev(N_host) agree."""
    print("[5] Lev(N_host): sparse vs dense")
    import torch
    from host import LevEvaluator, NetEvaluator, read_host
    sigma = read_host()
    dense = LevEvaluator(sigma, device="cpu", dense=True)
    sparse = LevEvaluator(sigma, device="cpu", dense=False)
    netl = NetEvaluator(sigma, device="cpu")
    gen = torch.Generator().manual_seed(4242)
    V = (torch.rand(64, LevEvaluator.N, generator=gen) < 0.5).float()
    a = dense.step(V)
    b = sparse.step(V)
    c = netl.step(V)
    same = bool((a == b).all()) and bool((a == c).all())
    print(f"    identical next state on 64 uniformly random states: {same}")
    print(f"    dense: {dense.info['layers']} layers, max width "
          f"{dense.info['max_width']}, {dense.info['total_weights']:,} entries")
    R["lev"] = {"sparse_dense_agree": same,
                "layers": dense.info["layers"],
                "max_width": dense.info["max_width"],
                "total_weights": dense.info["total_weights"]}


def main_verify() -> int:
    t0 = time.perf_counter()
    check_codec()
    check_framing()
    check_serialization()
    check_host_datapath()
    check_lev_sparse_dense()
    R["seconds"] = time.perf_counter() - t0
    path = runs_path("paper_verify.json")
    json.dump(R, open(path, "w"), indent=1)
    print(f"\nwrote {path}  ({R['seconds']:.0f}s)")
    return 0


def main_throughput() -> int:
    import torch
    from host import M_P, LevEvaluator, NetEvaluator, describe, read_host, run_reference
    torch.set_num_threads(1)                 # the processor rates are for one core
    sigma = read_host()
    r_H = describe(sigma)
    out = {}

    t0 = time.perf_counter()
    o, n = run_reference(M_P, r_H, expect=sigma)
    dt = time.perf_counter() - t0
    assert o == sigma
    out["reference"] = {"steps": n, "seconds": dt, "steps_per_second": n / dt}
    print(f"  integer reference: {n:,} steps in {dt:.2f} s "
          f"({n / dt:,.0f} steps/s)", flush=True)

    N = 20000
    for key, what, ev in (
            ("net_cpu", "the netlist of sigma unit by unit, one core",
             lambda: NetEvaluator(sigma, device="cpu")),
            ("net_gpu", "the netlist of sigma unit by unit, GPU",
             lambda: NetEvaluator(sigma, device="cuda", graph=True))):
        G = ev()
        G.run(M_P, r_H, max_steps=200)                   # warm up
        t0 = time.perf_counter()
        G.run(M_P, r_H, max_steps=N, expect=sigma)
        dt = time.perf_counter() - t0
        out[key] = {"steps": N, "seconds": dt, "steps_per_second": N / dt,
                    "units": G.info["units"], "entries": G.info["entries"]}
        print(f"  {what}: {N:,} steps in {dt:.1f} s ({N / dt:,.0f} steps/s)",
              flush=True)

    D = LevEvaluator(sigma, device="cuda", dense=True)
    entries = sum(int(W.numel()) for W in D.W)
    nonzero = sum(int((W != 0).sum()) for W in D.W)
    D.run(M_P, r_H, max_steps=200)
    t0 = time.perf_counter()
    D.run(M_P, r_H, max_steps=N, expect=sigma)
    dt = time.perf_counter() - t0
    rate = N / dt
    out["dense_gpu"] = {"steps": N, "seconds": dt, "steps_per_second": rate,
                        "entries": entries, "nonzero": nonzero,
                        "bytes_per_step": entries * 4,
                        "bandwidth_gbs": rate * entries * 4 / 1e9}
    print(f"  Lev(N_host) dense on the GPU: {N:,} steps in {dt:.1f} s "
          f"({rate:,.0f} steps/s); {entries:,} entries of which {nonzero:,} "
          f"are nonzero, {entries * 4 / 1e6:.0f} MB read per step, "
          f"{rate * entries * 4 / 1e9:.0f} GB/s", flush=True)

    G2 = LevEvaluator(sigma, device="cuda", dense=False, graph=True)
    G2.run(M_P, r_H, max_steps=200)
    t0 = time.perf_counter()
    G2.run(M_P, r_H, max_steps=N, expect=sigma)
    dt = time.perf_counter() - t0
    out["graph_gpu"] = {"steps": N, "seconds": dt, "steps_per_second": N / dt}
    print(f"  the same map from its nonzero entries, captured as a CUDA graph: "
          f"{N:,} steps in {dt:.1f} s ({N / dt:,.0f} steps/s)", flush=True)

    S = LevEvaluator(sigma, device="cpu", dense=False)
    S.run(M_P, r_H, max_steps=200)
    t0 = time.perf_counter()
    S.run(M_P, r_H, max_steps=N, expect=sigma)
    dt = time.perf_counter() - t0
    out["sparse_cpu"] = {"steps": N, "seconds": dt, "steps_per_second": N / dt}
    print(f"  the same map from its nonzero entries on one core: {N:,} steps in "
          f"{dt:.1f} s ({N / dt:,.0f} steps/s)", flush=True)

    # evaluator (d): the netlist in C, one core, on the self-describing instance
    import subprocess
    import tempfile
    work = tempfile.mkdtemp(prefix="throughput_")
    exe = os.path.join(work, "netlist_eval")
    subprocess.run(["gcc", "-O3", "-march=native", "-fopenmp", "-o", exe,
                    os.path.join(REPO, "src", "netlist_eval.c")], check=True)
    nb, units, nxt = parse_sigma(sigma)
    write_flat(os.path.join(work, "host.bin"), nb, units, nxt)
    open(os.path.join(work, "mP"), "wb").write(bytes(M_P))
    open(os.path.join(work, "rH"), "wb").write(r_H)
    env = dict(os.environ, OMP_NUM_THREADS="1")
    t0 = time.perf_counter()
    subprocess.run([exe, "run", os.path.join(work, "host.bin"), os.path.join(work, "mP"),
                    os.path.join(work, "rH"), os.path.join(work, "out"), "net"],
                   check=True, capture_output=True, env=env)
    dt = time.perf_counter() - t0
    assert open(os.path.join(work, "out"), "rb").read() == sigma
    out["c_evaluator"] = {"steps": n, "seconds": dt, "steps_per_second": n / dt}
    print(f"  the netlist of sigma in C, one core: {n:,} steps in {dt:.1f} s "
          f"({n / dt:,.0f} steps/s)", flush=True)

    json.dump(out, open(runs_path("paper_throughput.json"), "w"), indent=1)
    return 0


COMMANDS = {'c': main_c, 'codec': main_codec, 'device': main_device, 'environment': main_environment, 'family': main_family, 'family-gate': main_family_gate, 'framing': main_framing, 'host': main_host, 'host-family': main_host_family, 'host-fold': main_host_fold, 'lev': main_lev, 'optimal': main_optimal, 'rocq': main_rocq, 'sigma': main_sigma, 'steps': main_steps, 'ternarity': main_ternarity, 'runs': main_runs, 'stats': main_stats, 'verify': main_verify, 'throughput': main_throughput}


if __name__ == "__main__":
    if len(sys.argv) < 2 or sys.argv[1] not in COMMANDS:
        sys.exit('commands: ' + ', '.join(COMMANDS))
    cmd = sys.argv.pop(1)
    sys.argv[0] += ' ' + cmd
    sys.exit(COMMANDS[cmd]())