Remove the scripts and records of the results cut from the paper: the organism on the record interpreter, tapes that are not recipes, order-independent settling and the dependence hypothesis

README.md

@@ -997,8 +997,6 @@ src/                                the library (run scripts as `python src/<nam
   ├── paper_stats.py                unit counts, levelization sizes, effective fan-in
   ├── paper_verify.py               codec, framing, serialization, datapath, interpreter
   ├── paper_runs.py                 self-description, three generations, lockstep
-  ├── organism.py                   an organism on neural_reflect: decodes a description into
-  │                                 the idle bank, copies it and hands over
   ├── host_family.py                the host family H_A: a constant-depth SUBLEQ step for
   │                                 every word width, and its serialization in build order
   ├── netlist_eval.c                an evaluator of the host family, the amplified host and the
@@ -1027,10 +1025,9 @@ src/                                the library (run scripts as `python src/<nam
   │                                 against the bounds, weight error with zero-entry leakage, the
   │                                 active-input counts that certify an orbit
   ├── neuromorphic.py               the datapath on the Loihi and Akida neuron models
-  └── check_*.py                    codec boundaries and optimality, step counts, tapes that are
-                                    not recipes, ternary depth, environment cost, device, host,
-                                    host family, levelization, framing, settling, dependence,
-                                    serialization, all 29 machines
+  └── check_*.py                    codec boundaries and optimality, step counts, ternary depth,
+                                    environment cost, device, host, host family, levelization,
+                                    framing, serialization, all 29 machines
 paper/                              the manuscript, and the record of every run it reports
 rocq/                               Rocq proofs: the netlist of the two-head machine computes its
                                     step, the organism builds every image from any description

paper/runs/paper_organism.json

@@ -1,93 +0,0 @@
-{
- "A": 13,
- "S": 8192,
- "G": 33,
- "b": 50,
- "N": 1650,
- "records": 33,
- "passes_per_generation": 1651,
- "steps_per_generation": 54483,
- "D0": 51,
- "D1": 1701,
- "NET0": 4892,
- "NET1": 6542,
- "reference": {
-  "generations": [
-   {
-    "bank": 1,
-    "bank_ok": true,
-    "ptr": 0,
-    "gp": 0,
-    "Q0": true,
-    "Q1": true,
-    "D0": true,
-    "D1": true,
-    "halt": 0
-   },
-   {
-    "bank": 0,
-    "bank_ok": true,
-    "ptr": 0,
-    "gp": 0,
-    "Q0": true,
-    "Q1": true,
-    "D0": true,
-    "D1": true,
-    "halt": 0
-   },
-   {
-    "bank": 1,
-    "bank_ok": true,
-    "ptr": 0,
-    "gp": 0,
-    "Q0": true,
-    "Q1": true,
-    "D0": true,
-    "D1": true,
-    "halt": 0
-   },
-   {
-    "bank": 0,
-    "bank_ok": true,
-    "ptr": 0,
-    "gp": 0,
-    "Q0": true,
-    "Q1": true,
-    "D0": true,
-    "D1": true,
-    "halt": 0
-   }
-  ],
-  "periodic": true,
-  "ok": true
- },
- "universal": {
-  "adder_records": 9,
-  "inputs": 8,
-  "failures": 0,
-  "ok": true
- },
- "net_units": 90862,
- "net_levels": 59,
- "netlist": {
-  "lockstep_steps": 4224,
-  "lockstep_ok": true,
-  "generations": [
-   {
-    "bank": 1,
-    "bank_ok": true,
-    "ptr": 0,
-    "gp": 0,
-    "Q0": true,
-    "Q1": true,
-    "D0": true,
-    "D1": true,
-    "halt": 0,
-    "equals_reference": true
-   }
-  ],
-  "ok": true
- },
- "seconds": 647.9628848040011,
- "ok": true
-}

paper/runs/paper_settle.json

@@ -1,12 +0,0 @@
-{
- "records": 9,
- "depth": 4,
- "G": 11,
- "orders": 362880,
- "inputs": 8,
- "states": 2903040,
- "wrong_after_d": 0,
- "wrong_after_d_minus_1": 134784,
- "ok": true,
- "seconds": 215.41703450400382
-}

paper/runs/paper_total.json

@@ -1,13 +0,0 @@
-{
- "P_cases": 825,
- "P_halting": 383,
- "P_divergent": 442,
- "P_failures": 0,
- "Pe_failures": 0,
- "Pe_bound_slack": 1.007727975270479,
- "recipe_agreement": 600,
- "recipe_disagreements": 0,
- "Pe_selfdescription_steps": 794994,
- "Pe_selfdescription_exact": true,
- "Pe_instructions": 22
-}

src/check_dependence.py

@@ -1,121 +0,0 @@
-"""Witness search for the dependence hypothesis of the size proposition.
-
-For every coordinate q of the record region, exhibit a state x and a data-region
-coordinate s with U(x)_s != U(x xor e_q)_s. Random states almost never witness
-this because a random output address lands in the 106-bit data region with
-probability about one in ten; the search below forces the record under
-evaluation to write into the data region and randomizes everything else.
-"""
-import os, random, sys
-sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
-import torch
-from reflect import (Cfg, build_net, Leveled, encode_gate, pad, state_to_vec,
-                     vec_to_state, slot_off, field_off)
-
-
-def targeted(cfg, U, rng, q, g, r, D0, D1, budget=4000):
-    """Second pass for address bits, index flags and weight codes: make the
-    field under test decide the output, and place both the read and the write
-    where they can be observed. Free coordinates are the data region and the
-    inactive record region, neither of which the evaluated record occupies."""
-    A, SLOT = cfg.A, cfg.SLOT
-    free = list(range(D0, D1)) + list(range(cfg.NET1, cfg.S))
-    freeset = set(free)
-    Q0 = cfg.NET0
-    base = Q0 + g * cfg.R
-    for _ in range(budget):
-        slot = 0 if r < SLOT else (1 if r < 2 * SLOT else None)
-        # the tested slot decides the output: out = x at that slot's address
-        if slot is None:
-            w = (1, 1)
-            bias = rng.randrange(-(1 << (cfg.BB - 1)), 1 << (cfg.BB - 1))
-        else:
-            w = (1, 0) if slot == 0 else (0, 1)
-            bias = -1
-        a = [rng.choice(free), rng.choice(free)]
-        i = [rng.randint(0, 1), rng.randint(0, 1)]
-        ao = rng.randrange(D0, D1)
-        io = 0
-        ptr = rng.randrange(0, 1 << A)
-        rec = encode_gate(cfg, pad(cfg, [(a[0], w[0], i[0]), (a[1], w[1], i[1])]),
-                          bias, (ao, io))
-        sig = [0] * cfg.S
-        for d in free:
-            sig[d] = rng.randint(0, 1)
-        for k in range(A):
-            sig[cfg.PTR_BASE + k] = (ptr >> (A - 1 - k)) & 1
-        sig[base:base + cfg.R] = rec
-        s0, s1 = list(sig), list(sig)
-        s1[q] ^= 1
-        x = U(s0, g)
-        y = U(s1, g)
-        if any(x[d] != y[d] for d in range(D0, D1)):
-            return budget
-    return 0
-
-
-def main() -> int:
-    cfg = Cfg()
-    net, inputs, outputs = build_net(cfg)
-    lev = Leveled(net, inputs, outputs, device="cpu")
-
-    def U(sig, gp):
-        v = state_to_vec(cfg, {"sig": sig, "gp": gp, "halt": 0}).unsqueeze(0)
-        return vec_to_state(cfg, lev.step(v[:, :len(inputs)])[0])["sig"]
-
-    D0, D1 = cfg.WORK_BASE, cfg.NET0          # data region [D0, D1)
-    rng = random.Random(20260910)
-    Q0 = cfg.NET0
-    Qbits = list(range(Q0, Q0 + cfg.G * cfg.R))
-    witnessed, tries_used = [], []
-    for q in Qbits:
-        g, r = divmod(q - Q0, cfg.R)
-        found = 0
-        for attempt in range(160):
-            # a record that writes into the data region, everything else random
-            a0 = rng.randrange(D0, D1 - 1)
-            a1 = rng.randrange(D0, D1 - 1)
-            ao = rng.randrange(D0, D1 - 1)
-            w0 = rng.choice((-1, 0, 1))
-            w1 = rng.choice((-1, 0, 1))
-            bias = rng.randrange(-(1 << (cfg.BB - 1)), 1 << (cfg.BB - 1))
-            i0, i1, io = rng.randint(0, 1), rng.randint(0, 1), rng.randint(0, 1)
-            rec = encode_gate(cfg, pad(cfg, [(a0, w0, i0), (a1, w1, i1)]),
-                              bias, (ao, io))
-            sig = [0] * cfg.S
-            for d in range(D0, D1):
-                sig[d] = rng.randint(0, 1)
-            ptr = rng.choice((0, 1, 2, 3))
-            for k in range(cfg.A):
-                sig[cfg.PTR_BASE + k] = (ptr >> (cfg.A - 1 - k)) & 1
-            base = cfg.bank_base(0) + g * cfg.R
-            sig[base:base + cfg.R] = rec
-            s0 = list(sig)
-            s1 = list(sig)
-            s1[q] ^= 1
-            a = U(s0, g)
-            b = U(s1, g)
-            if any(a[d] != b[d] for d in range(D0, D1)):
-                found = attempt + 1
-                break
-        if not found:
-            found = targeted(cfg, U, rng, q, g, r, D0, D1)
-        if found:
-            witnessed.append(q)
-            tries_used.append(found)
-    ok = len(witnessed) == len(Qbits)
-    print(f"record-region bits: {len(Qbits)}")
-    print(f"bits with an exhibited witness: {len(witnessed)}"
-          f"{'  (hypothesis holds for every bit)' if ok else '  MISSING: '
-             + str([q - Q0 for q in Qbits if q not in witnessed][:20])}")
-    if tries_used:
-        print(f"attempts needed: max {max(tries_used)}, mean "
-              f"{sum(tries_used)/len(tries_used):.1f}")
-    print("every data coordinate of U is a multiplexer output depending on the "
-          "write-select line and the previous value, hence on at least two "
-          "coordinates")
-    return 0 if ok else 1
-
-
-if __name__ == "__main__":
-    sys.exit(main())

src/check_settle.py

@@ -1,108 +0,0 @@
-"""Order-independent settling on the interpreter itself.
-
-The full adder of Lemma 3.2, with carry-in a primary input, is compiled to
-stored records and laid out in every one of the 9! orders of its records. For
-every order and every one of the eight inputs the interpreter's netlist is run
-for d passes, d the depth of the adder, and the outputs are compared with
-a + b + c_in, as Lemma 7.5 asserts. The same states are also read after d - 1
-passes, where some order must still be wrong, since a pass that evaluates the
-records against the order of the netlist advances the correct front by one
-level only.
-
-    python src/check_settle.py [--device cuda] [--batch 16384]
-"""
-import argparse
-import itertools
-import json
-import os
-import sys
-import time
-
-sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
-import torch
-from matrix8 import Net
-from reflect import Cfg, SparseLeveled, build_net, compile_to_reflect, encode_netlist, topo
-
-REPO = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
-
-
-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 main() -> int:
-    ap = argparse.ArgumentParser()
-    ap.add_argument("--device", default="cuda" if torch.cuda.is_available() else "cpu")
-    ap.add_argument("--batch", type=int, default=16384)
-    args = ap.parse_args()
-    t_start = time.perf_counter()
-
-    cfg = Cfg()
-    net = Net()
-    s_out, c_out = net.FA("fa", "a", "b", "cin")
-    depth = {}
-    for g in topo(net):
-        depth[g] = 1 + max((depth.get(s, 0) for s, _ in net.gates[g][0]), default=0)
-    d = max(depth.values())
-    ia = {"a": cfg.WORK_BASE, "b": cfg.WORK_BASE + 1, "cin": cfg.WORK_BASE + 2}
-    rg, addr, _ = compile_to_reflect(cfg, net, ia, [s_out, c_out], cfg.WORK_BASE + 3)
-    n = len(rg)
-    print(f"  full adder of Lemma 3.2: {n} records of depth {d}; U has G = {cfg.G}")
-
-    unet, uin, uout = build_net(cfg)
-    lev = SparseLeveled(unet, uin, uout, device=args.device)
-    width = cfg.STATE_BITS
-
-    # the record bits of each record, and of the no-op that fills the region
-    enc = torch.tensor([encode_netlist(cfg, [r])[:cfg.R] for r in rg], dtype=torch.float32)
-    pad = torch.tensor(encode_netlist(cfg, [])[:cfg.R * (cfg.G - n)], dtype=torch.float32)
-    perms = torch.tensor(list(itertools.permutations(range(n))), dtype=torch.long)
-    P = perms.shape[0]
-    inputs = torch.tensor([[(v >> 0) & 1, (v >> 1) & 1, (v >> 2) & 1] for v in range(8)],
-                          dtype=torch.float32)
-    want = inputs.sum(1)
-    print(f"  {P:,} record orders x 8 inputs = {8 * P:,} states, {d} passes of "
-          f"{cfg.G} records each")
-
-    bad_d = bad_early = 0
-    done = 0
-    t0 = time.perf_counter()
-    orders_per_batch = max(1, args.batch // 8)
-    for lo in range(0, P, orders_per_batch):
-        pb = perms[lo:lo + orders_per_batch]
-        B = pb.shape[0] * 8
-        region = enc[pb].reshape(pb.shape[0], n * cfg.R)
-        region = torch.cat([region, pad.expand(pb.shape[0], -1)], dim=1)
-        X = torch.zeros(B, width)
-        X[:, cfg.NET0:cfg.NET0 + cfg.G * cfg.R] = region.repeat_interleave(8, dim=0)
-        iv = inputs.repeat(pb.shape[0], 1)
-        X[:, ia["a"]], X[:, ia["b"]], X[:, ia["cin"]] = iv[:, 0], iv[:, 1], iv[:, 2]
-        X = X.to(args.device)
-        wv = want.repeat(pb.shape[0]).to(args.device)
-        for p in range(d):
-            for _ in range(cfg.G):
-                X = lev.step(X)
-            if p == d - 2:
-                got = X[:, addr[s_out]] + 2 * X[:, addr[c_out]]
-                bad_early += int((got != wv).sum())
-        got = X[:, addr[s_out]] + 2 * X[:, addr[c_out]]
-        bad_d += int((got != wv).sum())
-        done += B
-        if lo // orders_per_batch % 8 == 0:
-            rate = done / (time.perf_counter() - t0)
-            print(f"      {done:,}/{8 * P:,} states ({rate:,.0f} states/s)", flush=True)
-    ok = bad_d == 0 and bad_early > 0
-    print(f"  after {d} passes: {'every order and every input correct' if bad_d == 0 else f'{bad_d} WRONG'}; "
-          f"after {d - 1} passes: {bad_early:,} states still wrong, so {d} passes are needed")
-    json.dump({"records": n, "depth": d, "G": cfg.G, "orders": P, "inputs": 8,
-               "states": 8 * P, "wrong_after_d": bad_d, "wrong_after_d_minus_1": bad_early,
-               "ok": ok, "seconds": time.perf_counter() - t_start},
-              open(runs_path("paper_settle.json"), "w"), indent=1)
-    print("SETTLE:", "PASS" if ok else "FAIL")
-    return 0 if ok else 1
-
-
-if __name__ == "__main__":
-    sys.exit(main())

src/check_total.py

@@ -1,156 +0,0 @@
-"""The constructor on tapes that are not recipes.
-
-Two statements are checked. First, the decoding loop of P halts on an arbitrary
-tape exactly when a tag byte in {0, 128} is reached, counting the stale input
-register as the tag once the tape is exhausted, and its output on every such
-tape is the extension of delta computed by selfrep.decode_any. Second, the
-program P_e obtained by inserting one end-of-tape guard after the tag read
-halts on every tape, agrees with P on recipes, and runs in at most
-643 |tau| + 9 steps.
-"""
-import json
-import os
-import random
-import sys
-
-sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
-from selfrep import (HOST_PATH, M_STAR, P, P_TOTAL, decode, decode_any, describe,
-                     describe_literal, memory_image, run_reference, tau_star)
-
-REPO = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
-M_E = memory_image(P_TOTAL)
-M_PP = memory_image(P)
-
-
-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 budget(tape: bytes) -> int:
-    """The bound proved for P_e: at most |tau| passes that consume a tape byte,
-    each of at most 5*127 + 8 steps, and one final pass of at most nine."""
-    return 643 * len(tape) + 9
-
-
-def tapes():
-    rng = random.Random(777)
-    out = [(b"", "empty")]
-    for t in (0, 1, 2, 127, 128, 129, 200, 255):
-        out.append((bytes([t]), f"a single byte {t}"))
-        out.append((bytes([t, 0x41]), f"byte {t} then a payload byte"))
-    out.append((b"\x05\x01", "a literal token truncated after one payload byte"))
-    out.append((b"\x7f", "a literal tag with no payload at all"))
-    out.append((b"\xff", "a repeat tag with no payload"))
-    out.append((b"\x80\x41\x41", "the reserved tag 128"))
-    sigma = open(HOST_PATH, "rb").read()
-    r = describe(sigma)
-    out.append((r, "a real recipe"))
-    out.append((r[:-1], "that recipe with its end token removed"))
-    out.append((r[:5000], "a truncated recipe"))
-    out.append((tau_star(sigma, M_STAR), "tau*"))
-    for _ in range(600):
-        n = rng.randrange(0, 60)
-        alpha = rng.choice([2, 3, 130, 256])
-        out.append((bytes(rng.randrange(alpha) for _ in range(n)), "random"))
-    for _ in range(200):
-        f = bytes(rng.randrange(rng.choice([2, 256])) for _ in range(rng.randrange(0, 80)))
-        enc = rng.choice((describe, describe_literal))
-        r = enc(f)
-        k = rng.randrange(0, len(r) + 1)
-        out.append((r[:k], "a prefix of a recipe"))
-    return out
-
-
-def main() -> int:
-    out = {}
-    ok = True
-    cases = tapes()
-
-    # P: the halting characterization, and the output when it halts.
-    diverge = halt = 0
-    bad = []
-    for tape, label in cases:
-        want, halts = decode_any(tape, guard=False)
-        cap = budget(tape) * 4
-        try:
-            got, steps = run_reference(M_PP, tape, max_steps=cap)
-        except Exception as exc:                     # pragma: no cover
-            bad.append((label, repr(exc)))
-            continue
-        ran_out = steps >= cap
-        if halts:
-            halt += 1
-            if ran_out or got != want:
-                bad.append((label, "halting case wrong"))
-        else:
-            diverge += 1
-            if not ran_out or not got.startswith(want):
-                bad.append((label, "divergent case wrong"))
-    print(f"  P on {len(cases)} tapes: {halt} halt, {diverge} do not; the "
-          f"characterization and the emitted bytes agree in every case: "
-          f"{'yes' if not bad else f'NO {bad[:3]}'}")
-    ok &= not bad
-    out["P_cases"] = len(cases)
-    out["P_halting"] = halt
-    out["P_divergent"] = diverge
-    out["P_failures"] = len(bad)
-
-    # P_e: total, and within the proved bound.
-    ebad = []
-    worst = 0.0
-    for tape, label in cases:
-        want, halts = decode_any(tape, guard=True)
-        assert halts
-        cap = budget(tape)
-        got, steps = run_reference(M_E, tape, max_steps=cap + 1)
-        if steps > cap or got != want:
-            ebad.append((label, steps, cap))
-        worst = max(worst, steps / cap)
-    print(f"  P_e on the same {len(cases)} tapes: halts on every one, output "
-          f"equals the extended decoding, and the step bound 643|tau| + 9 "
-          f"holds: {'yes' if not ebad else f'NO {ebad[:3]}'}")
-    print(f"  the worst case observed reaches {worst * 100:.0f} per cent of the "
-          f"bound")
-    ok &= not ebad
-    out["Pe_failures"] = len(ebad)
-    out["Pe_bound_slack"] = 1 / worst if worst else None
-
-    # P_e agrees with P on recipes.
-    rng = random.Random(31337)
-    agree = 0
-    abad = 0
-    for _ in range(300):
-        f = bytes(rng.randrange(rng.choice([2, 5, 256]))
-                  for _ in range(rng.randrange(0, 400)))
-        for enc in (describe, describe_literal):
-            r = enc(f)
-            a, _ = run_reference(M_PP, r)
-            b, _ = run_reference(M_E, r)
-            agree += 1
-            if not (a == b == f):
-                abad += 1
-    print(f"  P and P_e emit the same bytes on {agree} recipes, equal to the "
-          f"described string: {'yes' if abad == 0 else f'NO ({abad})'}")
-    ok &= abad == 0
-    out["recipe_agreement"] = agree
-    out["recipe_disagreements"] = abad
-
-    # the self-description still goes through, on the total program
-    sigma = open(HOST_PATH, "rb").read()
-    o, n = run_reference(M_E, describe(sigma))
-    same = o == sigma
-    print(f"  P_e emits sigma(N_host) from its recipe in {n:,} steps: "
-          f"{'exact' if same else 'FAILED'}")
-    ok &= same
-    out["Pe_selfdescription_steps"] = n
-    out["Pe_selfdescription_exact"] = same
-    out["Pe_instructions"] = len(P_TOTAL)
-
-    json.dump(out, open(runs_path("paper_total.json"), "w"), indent=1)
-    return 0 if ok else 1
-
-
-if __name__ == "__main__":
-    sys.exit(main())

src/organism.py

@@ -1,318 +0,0 @@
-"""A von Neumann organism inside the interpreter.
-
-The organism is a stored netlist R held in the active record region together
-with a description held in a data region of the same size. Each pass of the
-interpreter handles one bit position p, the value of the pointer: the
-description bit of the active copy is copied into the description region of
-the other copy, and its negation is written into the inactive record region.
-When the pointer reaches the size N of a record region the organism clears the
-pointer and flips the bank bit, and the interpreter continues from the netlist
-that was just written.
-
-With R's own description, every generation constructs R from the description
-and copies the description, bit for bit, and hands over to the result, which
-does the same. With the description of any other netlist X of the same size the
-first generation constructs X and hands over to it, so the constructor is
-universal over stored netlists. Construction, copying and instantiation are all
-carried out by the dynamics of the interpreter: the pointer clause is part of
-its netlist and the output device is not used.
-
-    records   role
-    t_k       conjunction of the pointer bits 2k, 2k+1 with the bits of N
-    tree      e = [PTR = N]
-    reset     PTR_j <- PTR_j and not e, for every bit j of N that is 1
-    transfer  D_other[p], D_active[p] <- D_active[p];
-              Q_other[p] <- not D_active[p], Q_active[p] <- Q_active[p]
-    advance   PTR_ADV <- not e
-    flip      BANK <- BANK xor e
-
-    python src/organism.py [--generations N] [--net-generations N] [--device D]
-"""
-from __future__ import annotations
-
-import argparse
-import json
-import os
-import random
-import sys
-import time
-
-sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
-from reflect import Cfg, Leveled, Runner, build_net, encode_netlist, ref_step, to_bits
-
-REPO = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
-A_ORG = 13
-
-
-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 records_needed(A: int, N: int) -> int:
-    """Pairs, tree, reset, transfer, advance and flip."""
-    pairs = -(-A // 2)
-    return pairs + (pairs - 1) + bin(N).count("1") + 10 + 1 + 3
-
-
-def organism_cfg(A: int = A_ORG) -> Cfg:
-    """The two-bank member whose record region holds exactly the organism."""
-    R = 3 * A + 11
-    for G in range(8, 1 << 12):
-        if records_needed(A, G * R) == G:
-            return Cfg(A=A, G=G, banks=2, self_mod=True)
-    raise ValueError("no record count is a fixed point")
-
-
-class Layout:
-    """Scratch coordinates, then the two description regions, below NET0."""
-
-    def __init__(self, cfg: Cfg):
-        self.N = cfg.G * cfg.R
-        self.scratch = cfg.WORK_BASE
-        self.n_scratch = 32
-        self.D0 = self.scratch + self.n_scratch
-        self.D1 = self.D0 + self.N
-        self.free = self.D1 + self.N
-        assert self.free <= cfg.NET0, "the description regions overlap the records"
-
-
-def organism_program(cfg: Cfg, L: Layout):
-    """The G records of the organism, in evaluation order."""
-    w = [L.scratch]
-
-    def fresh():
-        s = w[0]
-        w[0] += 1
-        assert w[0] <= L.scratch + L.n_scratch
-        return s
-
-    bits = to_bits(L.N, cfg.A)             # coordinate PTR_BASE + i carries bits[i]
-    prog = []
-    leaves = []
-    for k in range(0, cfg.A, 2):
-        slots, bias = [], 0
-        for j in (k, k + 1):
-            if j < cfg.A:
-                if bits[j]:
-                    slots.append((cfg.PTR_BASE + j, 1, 0))
-                    bias -= 1
-                else:
-                    slots.append((cfg.PTR_BASE + j, -1, 0))
-        t = fresh()
-        prog.append((slots, bias, (t, 0)))
-        leaves.append(t)
-    e = fresh()
-    level = leaves
-    while len(level) > 1:
-        nxt = []
-        for i in range(0, len(level) - 1, 2):
-            dst = e if len(level) == 2 else fresh()
-            prog.append(([(level[i], 1, 0), (level[i + 1], 1, 0)], -2, (dst, 0)))
-            nxt.append(dst)
-        if len(level) % 2:
-            nxt.append(level[-1])
-        level = nxt
-    assert level == [e]
-    for i in range(cfg.A):                  # PTR = N -> PTR = 0
-        if bits[i]:
-            prog.append(([(cfg.PTR_BASE + i, 1, 0), (e, -1, 0)], -1,
-                         (cfg.PTR_BASE + i, 0)))
-    k = cfg.BANK_SIG
-    c, d, u, v, u2, v2 = (fresh() for _ in range(6))
-    prog += [
-        ([(L.D0, 1, 1), (k, -1, 0)], -1, (c, 0)),           # D0[p] and not k
-        ([(L.D1, 1, 1), (k, 1, 0)], -2, (d, 0)),            # D1[p] and k
-        ([(c, 1, 0), (d, 1, 0)], -1, (L.D1, 1)),            # D1[p] <- D_k[p]
-        ([(c, 1, 0), (d, 1, 0)], -1, (L.D0, 1)),            # D0[p] <- D_k[p]
-        ([(L.D0, -1, 1), (k, -1, 0)], 0, (u, 0)),           # not D_k[p] and not k
-        ([(cfg.NET1, 1, 1), (k, 1, 0)], -2, (v, 0)),        # Q1[p] and k
-        ([(u, 1, 0), (v, 1, 0)], -1, (cfg.NET1, 1)),        # Q1[p] <- k ? Q1[p] : not D_k[p]
-        ([(L.D0, -1, 1), (k, 1, 0)], -1, (u2, 0)),          # not D_k[p] and k
-        ([(cfg.NET0, 1, 1), (k, -1, 0)], -1, (v2, 0)),      # Q0[p] and not k
-        ([(u2, 1, 0), (v2, 1, 0)], -1, (cfg.NET0, 1)),      # Q0[p] <- k ? not D_k[p] : Q0[p]
-    ]
-    prog.append(([(e, -1, 0)], 0, (cfg.PTR_ADV, 0)))       # advance unless PTR = N
-    to, tn = fresh(), fresh()
-    prog += [([(k, 1, 0), (e, 1, 0)], -1, (to, 0)),
-             ([(k, -1, 0), (e, -1, 0)], 1, (tn, 0)),
-             ([(to, 1, 0), (tn, 1, 0)], -2, (k, 0))]       # k <- k xor e
-    assert len(prog) == cfg.G, (len(prog), cfg.G)
-    return prog
-
-
-def negate(bits):
-    return [1 - b for b in bits]
-
-
-def initial_state(cfg: Cfg, L: Layout, organism, description, seed: int):
-    """Bank 0 holds the organism and D0 the description; PTR, PTR_ADV, BANK,
-    HALT, the record counter and the halt bit are 0; every other coordinate is
-    random, the inactive record region and D1 included."""
-    rng = random.Random(seed)
-    sig = [rng.randint(0, 1) for _ in range(cfg.S)]
-    for c in list(range(cfg.PTR_BASE, cfg.PTR_BASE + cfg.A)) + [
-            cfg.PTR_ADV, cfg.BANK_SIG, cfg.HALT_SIG, cfg.OUT_STROBE]:
-        sig[c] = 0
-    sig[cfg.NET0:cfg.NET0 + L.N] = organism
-    sig[L.D0:L.D0 + L.N] = description
-    return {"sig": sig, "gp": 0, "halt": 0}
-
-
-def run_generation(cfg, L, step, st):
-    """N + 1 passes: N bit positions, then the hand-over pass."""
-    for _ in range((L.N + 1) * cfg.G):
-        st = step(st)
-    return st
-
-
-def regions(cfg, L, sig):
-    return {"Q0": sig[cfg.NET0:cfg.NET0 + L.N], "Q1": sig[cfg.NET1:cfg.NET1 + L.N],
-            "D0": sig[L.D0:L.D0 + L.N], "D1": sig[L.D1:L.D1 + L.N]}
-
-
-def check_generation(cfg, L, st, k, organism):
-    """After generation k the bank bit is k mod 2, the pointer and the record
-    counter are 0, and both copies hold the organism and its description."""
-    sig = st["sig"]
-    r = regions(cfg, L, sig)
-    ptr = int("".join(map(str, sig[cfg.PTR_BASE:cfg.PTR_BASE + cfg.A])), 2)
-    desc = negate(organism)
-    return {"bank": sig[cfg.BANK_SIG], "bank_ok": sig[cfg.BANK_SIG] == k % 2,
-            "ptr": ptr, "gp": st["gp"],
-            "Q0": r["Q0"] == organism, "Q1": r["Q1"] == organism,
-            "D0": r["D0"] == desc, "D1": r["D1"] == desc,
-            "halt": st["halt"]}
-
-
-def adder_program(cfg, L):
-    """The full adder of Lemma 3.2 on inputs held in the free region, padded
-    with no-op records to G records: a netlist other than the organism."""
-    from matrix8 import Net
-    from reflect import compile_to_reflect
-    net = Net()
-    s, co = net.FA("fa", "a", "b", "cin")
-    ia = {"a": L.free, "b": L.free + 1, "cin": L.free + 2}
-    rg, addr, _ = compile_to_reflect(cfg, net, ia, [s, co], L.free + 3)
-    noop = ([], -1, (cfg.TRASH, 0))
-    prog = rg + [noop] * (cfg.G - len(rg))
-    return prog, ia, addr[s], addr[co], len(rg)
-
-
-def main() -> int:
-    ap = argparse.ArgumentParser()
-    ap.add_argument("--generations", type=int, default=4)
-    ap.add_argument("--net-generations", type=int, default=2)
-    ap.add_argument("--device", default="cuda")
-    args = ap.parse_args()
-    t_start = time.perf_counter()
-
-    cfg = organism_cfg()
-    L = Layout(cfg)
-    prog = organism_program(cfg, L)
-    organism = encode_netlist(cfg, prog)
-    desc = negate(organism)
-    print(f"  member: A = {cfg.A}, S = {cfg.S}, G = {cfg.G}, b = {cfg.R}, "
-          f"two banks, span {cfg.span}; N = {L.N} bits per record region")
-    print(f"  organism: {len(prog)} records; description regions at {L.D0} and "
-          f"{L.D1}; one generation is N + 1 = {L.N + 1} passes, "
-          f"{(L.N + 1) * cfg.G:,} steps")
-    out = {"A": cfg.A, "S": cfg.S, "G": cfg.G, "b": cfg.R, "N": L.N,
-           "records": len(prog), "passes_per_generation": L.N + 1,
-           "steps_per_generation": (L.N + 1) * cfg.G, "D0": L.D0, "D1": L.D1,
-           "NET0": cfg.NET0, "NET1": cfg.NET1}
-
-    # --- self-reproduction on the reference of Definition 7.1 --------------
-    ref = lambda s: ref_step(cfg, s)
-    st = initial_state(cfg, L, organism, desc, seed=1)
-    gens, states = [], []
-    t0 = time.perf_counter()
-    for k in range(1, args.generations + 1):
-        st = run_generation(cfg, L, ref, st)
-        g = check_generation(cfg, L, st, k, organism)
-        gens.append(g)
-        states.append(list(st["sig"]))
-        print(f"  reference, generation {k}: bank {g['bank']}, PTR {g['ptr']}, "
-              f"Q0 {'=' if g['Q0'] else '!='} R, Q1 {'=' if g['Q1'] else '!='} R, "
-              f"D0 {'=' if g['D0'] else '!='} d(R), D1 {'=' if g['D1'] else '!='} d(R)",
-              flush=True)
-    periodic = all(states[i] == states[i + 2] for i in range(len(states) - 2))
-    ok_ref = all(g["bank_ok"] and g["ptr"] == 0 and g["gp"] == 0 and g["Q0"] and g["Q1"]
-                 and g["D0"] and g["D1"] and g["halt"] == 0 for g in gens) and periodic
-    print(f"  reference: {args.generations} generations exact; the state after "
-          f"generation k equals the state after generation k + 2: "
-          f"{'yes' if periodic else 'NO'} ({time.perf_counter() - t0:.0f} s)", flush=True)
-    out["reference"] = {"generations": gens, "periodic": periodic, "ok": ok_ref}
-
-    # --- universal construction: the full adder, on every input -------------
-    aprog, ia, s_addr, c_addr, n_adder = adder_program(cfg, L)
-    X = encode_netlist(cfg, aprog)
-    ubad = 0
-    for v in range(8):
-        a, b, cin = v & 1, (v >> 1) & 1, (v >> 2) & 1
-        st = initial_state(cfg, L, organism, negate(X), seed=100 + v)
-        st["sig"][ia["a"]], st["sig"][ia["b"]], st["sig"][ia["cin"]] = a, b, cin
-        st = run_generation(cfg, L, ref, st)
-        built = st["sig"][cfg.NET1:cfg.NET1 + L.N] == X and st["sig"][cfg.BANK_SIG] == 1
-        for _ in range(4 * cfg.G):          # the adder's depth is four
-            st = ref(st)
-        total = st["sig"][s_addr] + 2 * st["sig"][c_addr]
-        if not built or total != a + b + cin:
-            ubad += 1
-    print(f"  universal construction: the description of a {n_adder}-record full "
-          f"adder yields the adder in bank 1, which then computes a + b + c_in on "
-          f"all 8 inputs: {'yes' if ubad == 0 else f'NO ({ubad} failures)'}", flush=True)
-    out["universal"] = {"adder_records": n_adder, "inputs": 8, "failures": ubad,
-                        "ok": ubad == 0}
-
-    # --- the netlist of the member, generation by generation ----------------
-    t0 = time.perf_counter()
-    net, inputs, outputs = build_net(cfg)
-    lev = Leveled(net, inputs, outputs, device=args.device)
-    R = Runner(cfg, lev)
-    print(f"  netlist N_U+: {len(net.gates):,} units in {len(lev.plan)} levels "
-          f"({time.perf_counter() - t0:.0f} s to build)", flush=True)
-    out["net_units"] = len(net.gates)
-    out["net_levels"] = len(lev.plan)
-    st_n = initial_state(cfg, L, organism, desc, seed=1)
-    st_r = initial_state(cfg, L, organism, desc, seed=1)
-    lock = 2 * cfg.G * 64
-    diverged = None
-    for n in range(lock):
-        st_n = R.step(st_n)
-        st_r = ref(st_r)
-        if st_n["sig"] != st_r["sig"] or st_n["gp"] != st_r["gp"]:
-            diverged = n
-            break
-    print(f"  netlist and reference agree on the full state over the first {lock:,} "
-          f"steps: {'yes' if diverged is None else f'NO at step {diverged}'}", flush=True)
-    st_n = initial_state(cfg, L, organism, desc, seed=1)
-    net_gens = []
-    t0 = time.perf_counter()
-    for k in range(1, args.net_generations + 1):
-        st_n = run_generation(cfg, L, R.step, st_n)
-        g = check_generation(cfg, L, st_n, k, organism)
-        g["equals_reference"] = st_n["sig"] == states[k - 1]
-        net_gens.append(g)
-        print(f"  netlist, generation {k}: bank {g['bank']}, Q0 {'=' if g['Q0'] else '!='} R, "
-              f"Q1 {'=' if g['Q1'] else '!='} R, descriptions "
-              f"{'exact' if g['D0'] and g['D1'] else 'WRONG'}, full state equals the "
-              f"reference's: {'yes' if g['equals_reference'] else 'NO'} "
-              f"({time.perf_counter() - t0:.0f} s)", flush=True)
-    ok_net = diverged is None and all(
-        g["bank_ok"] and g["Q0"] and g["Q1"] and g["D0"] and g["D1"] and g["equals_reference"]
-        for g in net_gens)
-    out["netlist"] = {"lockstep_steps": lock, "lockstep_ok": diverged is None,
-                      "generations": net_gens, "ok": ok_net}
-
-    ok = ok_ref and ubad == 0 and ok_net
-    out["seconds"] = time.perf_counter() - t_start
-    out["ok"] = ok
-    json.dump(out, open(runs_path("paper_organism.json"), "w"), indent=1)
-    print("ORGANISM:", "PASS" if ok else "FAIL")
-    return 0 if ok else 1
-
-
-if __name__ == "__main__":
-    sys.exit(main())

src/paper_verify.py

@@ -231,12 +231,11 @@ def check_host_datapath():
 
 # ---------------------------------------------------------------------------
 def check_interpreter():
-    """One-record semantics exhaustively over record fields, and the dependence
-    hypothesis of the size proposition."""
+    """One-record semantics exhaustively over record fields, and the record counter."""
     print("[5] Interpreter U")
     import torch
-    from reflect import (Cfg, build_net, Leveled, encode_gate, encode_netlist,
-                         pad, ref_step, state_to_vec, vec_to_state)
+    from reflect import (Cfg, build_net, Leveled, encode_netlist, state_to_vec,
+                         vec_to_state)
     cfg = Cfg()
     net, inputs, outputs = build_net(cfg)
     lev = Leveled(net, inputs, outputs, device="cpu")
@@ -277,64 +276,10 @@ def check_interpreter():
     print(f"    record counter advances mod G on all {cfg.G} values: "
           f"{'exact' if cbad == 0 else 'FAILED'}")
 
-    # dependence hypothesis of the size proposition: for every record-region
-    # coordinate q, exhibit a state x and a data coordinate s with
-    # U(x)_s != U(x xor e_q)_s. A random state rarely witnesses this, because a
-    # random output address lands in the 106-bit data region about one time in
-    # ten; the targeted pass of check_dependence forces the record under test to
-    # write into the data region and makes the tested field decisive.
-    import random
-    from check_dependence import targeted
-
-    def U1(sig, gp):
-        return U(sig, gp)["sig"]
-
-    rng = random.Random(20260910)
-    D0, D1 = cfg.WORK_BASE, cfg.NET0
-    Q0 = cfg.NET0
-    Qbits = list(range(Q0, Q0 + cfg.G * cfg.R))
-    influenced = set()
-    for q in Qbits:
-        g, r = divmod(q - Q0, cfg.R)
-        found = 0
-        for attempt in range(160):
-            slots = [(rng.randrange(D0, D1 - 1), rng.choice((-1, 0, 1)),
-                      rng.randint(0, 1)) for _ in range(2)]
-            bias = rng.randrange(-(1 << (cfg.BB - 1)), 1 << (cfg.BB - 1))
-            out = (rng.randrange(D0, D1 - 1), rng.randint(0, 1))
-            rec = encode_gate(cfg, pad(cfg, slots), bias, out)
-            sig = [0] * cfg.S
-            for d in range(D0, D1):
-                sig[d] = rng.randint(0, 1)
-            ptr = rng.choice((0, 1, 2, 3))
-            for k in range(cfg.A):
-                sig[cfg.PTR_BASE + k] = (ptr >> (cfg.A - 1 - k)) & 1
-            base = cfg.bank_base(0) + g * cfg.R
-            sig[base:base + cfg.R] = rec
-            s0, s1 = list(sig), list(sig)
-            s1[q] ^= 1
-            a0, a1 = U1(s0, g), U1(s1, g)
-            if any(a0[d] != a1[d] for d in range(D0, D1)):
-                found = attempt + 1
-                break
-        if not found:
-            found = targeted(cfg, U1, rng, q, g, r, D0, D1)
-        if found:
-            influenced.add(q)
-    print(f"    every one of the {len(Qbits)} record-region bits influences some "
-          f"data-region bit of U(x): {len(influenced)}/{len(Qbits)}"
-          f"{'  (hypothesis holds)' if len(influenced) == len(Qbits) else '  FAILED'}")
     R["interpreter"] = {
         "onerecord_cases": total, "onerecord_failures": bad,
-        "counter_failures": cbad,
-        "Q_bits": len(Qbits), "influencing": len(influenced),
-        "S": cfg.S, "G": cfg.G, "R": cfg.R, "b": cfg.R,
-        "Q_size": cfg.G * cfg.R, "records_max": (cfg.G * cfg.R) // cfg.R,
-        "units_lower_bound": (cfg.G * cfg.R + 1) // 2,
+        "counter_failures": cbad, "S": cfg.S, "G": cfg.G, "b": cfg.R,
     }
-    print(f"    |Q| = {cfg.G*cfg.R}, b = {cfg.R}: at most {(cfg.G*cfg.R)//cfg.R} "
-          f"records stored; any fan-in-2 netlist realising U has at least "
-          f"{(cfg.G*cfg.R+1)//2} units")
 
 
 # ---------------------------------------------------------------------------