src/twohead.py

"""The ring machine M^alpha_{K,S,L}: the organism, the netlist N^alpha_{K,S,L}, and the host stored in it."""
import argparse
import hashlib
import json
import math
import os
import random
import struct
import subprocess
import sys
import time

import numpy as np

import host as SR


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

ALPHA = 6

# the window cells the machine gives a meaning: the sink, the cells under the read head, the arm and
# the copy head, and nine requests, each acting at the end of the step in which a record sets it
SINK, RD, ARM, CPY, AR, AA, AC, RR, RA, RC, CB, CT, HO = range(13)

FREE = 13

REQUESTS = tuple(range(AR, HO + 1))

GATE = 8

ADDR = 18


def width(alpha):
    return 8 + 3 * alpha


# ---------------------------------------------------------------------------
# records and the description code
# ---------------------------------------------------------------------------

def encode_record(r, alpha=ALPHA):
    """r = (a0, w0, a1, w1, beta, ao), laid out gate first, with addresses of alpha bits."""
    a0, w0, a1, w1, beta, ao = r
    bits = []
    put = lambda val, w: bits.extend((val >> (w - 1 - j)) & 1 for j in range(w))
    wc = {1: 1, -1: 2, 0: 0}
    put(wc[w0], 2); put(wc[w1], 2); put(beta & 15, 4); put(a0, alpha); put(a1, alpha); put(ao, alpha)
    return bits


def decode_record(bits, alpha=ALPHA):
    it = iter(bits)
    get = lambda w: sum(next(it) << (w - 1 - j) for j in range(w))
    c0 = get(2); c1 = get(2); beta = get(4); a0 = get(alpha); a1 = get(alpha); ao = get(alpha)
    wd = {1: 1, 2: -1, 0: 0, 3: 0}
    return a0, wd[c0], a1, wd[c1], beta - 16 if beta >= 8 else beta, ao


def gate_bits(kind, s0, s1):
    """The eight gate bits of a codon: w0 (2), w1 (2), beta (4); kind 0 AND, 1 OR, 2 COPY."""
    sgn = {0: s0 | s1, 1: s0 & s1, 2: s0}[kind]
    odd = {0: s0 ^ s1, 1: 1 - (s0 ^ s1), 2: s0}[kind]
    w1 = (0, 0) if kind == 2 else (1 - s1, s1)
    return [1 - s0, s0, w1[0], w1[1], sgn, sgn, sgn, odd]


def codon_of(gbits):
    """The gate codon whose gate bits are gbits, if any."""
    for kind in (0, 1, 2):
        for s0 in (0, 1):
            for s1 in ((0, 1) if kind != 2 else (0,)):
                if gate_bits(kind, s0, s1) == gbits:
                    return [kind >> 1, kind & 1, s0, s1]
    return None


ESC = [1, 1, 0, 0]

END = [1, 1, 1, 1]


def describe(image, alpha=ALPHA):
    b = width(alpha)
    assert len(image) % b == 0
    out = []
    for r in range(len(image) // b):
        rec = image[r * b:(r + 1) * b]
        c = codon_of(rec[:GATE])
        out += (c + rec[GATE:]) if c else (ESC + rec)
    return out + END


def translate(desc, alpha=ALPHA):
    """The decoding the organism carries out, written plainly."""
    addr = 3 * alpha
    out, i = [], 0
    while True:
        c = desc[i:i + 4]; i += 4
        kind, s0, s1 = c[0] * 2 + c[1], c[2], c[3]
        if kind == 3 and s0 and s1:
            return out, i
        if kind == 3:
            out += desc[i:i + GATE]; i += GATE
        else:
            out += gate_bits(kind, s0, s1)
        out += desc[i:i + addr]; i += addr


# ---------------------------------------------------------------------------
# the machine, transcribed
# ---------------------------------------------------------------------------

class Machine:
    """M^alpha_{K,S,L}: K banks of S slots of b bits and K tapes of L cells, at absolute positions.

    Bank k carries the slot s[k] and the bit j[k] of its head and tape k the cell t[k] of its head.
    Bank kappa is active and bank kappa + 1 idle; tape kappa is read and tape kappa + 1 copied onto.
    A step evaluates the record at the active head on the cells it names, writes the value into the
    window, under the arm or under the copy head, carries out the requests the window then holds,
    turns the active head by one slot and clears the requests."""

    def __init__(self, K, S, L, banks=None, tapes=None, window=None, kappa=0, alpha=ALPHA):
        assert K >= 2 and S >= 1 and L >= 1
        self.K, self.S, self.L, self.alpha = K, S, L, alpha
        self.b = width(alpha)
        self.N = S * self.b
        banks = list(banks or [])
        tapes = list(tapes or [])
        self.Q = [list(banks[k]) if k < len(banks) else [0] * self.N for k in range(K)]
        self.D = [list(tapes[k]) if k < len(tapes) else [0] * L for k in range(K)]
        assert all(len(q) == self.N for q in self.Q) and all(len(d) == L for d in self.D)
        self.s, self.j, self.t = [0] * K, [0] * K, [0] * K
        self.w = list(window) if window is not None else [0] * (1 << alpha)
        assert len(self.w) == 1 << alpha
        self.kap = kappa
        self.steps = 0
        self.ver = [0] * K
        self._dec = None

    def records(self):
        """The records of the active bank, decoded once per version of the bank."""
        k = self.kap
        if self._dec is None or self._dec[0] != (k, self.ver[k]):
            q, b = self.Q[k], self.b
            self._dec = ((k, self.ver[k]), [decode_record(q[s * b:(s + 1) * b], self.alpha) for s in range(self.S)])
        return self._dec[1]

    def cell(self, a, k, i):
        if a == SINK:
            return 0
        if a == RD:
            return self.D[k][self.t[k]]
        if a == ARM:
            return self.Q[i][self.s[i] * self.b + self.j[i]]
        if a == CPY:
            return self.D[i][self.t[i]]
        return self.w[a]

    def step(self, rec=None):
        k = self.kap
        i = (k + 1) % self.K
        if rec is None:
            rec = self.records()[self.s[k]]
        a0, w0, a1, w1, beta, ao = rec
        v = 1 if w0 * self.cell(a0, k, i) + w1 * self.cell(a1, k, i) + beta >= 0 else 0
        if ao == ARM:
            self.Q[i][self.s[i] * self.b + self.j[i]] = v
            self.ver[i] += 1
        elif ao == CPY:
            self.D[i][self.t[i]] = v
        elif ao > CPY:
            self.w[ao] = v
        w = self.w
        if w[RR]:
            self.t[k] = 0
        elif w[AR]:
            self.t[k] = (self.t[k] + 1) % self.L
        if w[CB]:
            self.Q[i] = [0] * self.N
            self.ver[i] += 1
        if w[RA]:
            self.s[i] = self.j[i] = 0
        elif w[AA]:
            if self.j[i] + 1 < self.b:
                self.j[i] += 1
            else:
                self.j[i] = 0
                self.s[i] = (self.s[i] + 1) % self.S
        if w[CT]:
            self.D[i] = [0] * self.L
        if w[RC]:
            self.t[i] = 0
        elif w[AC]:
            self.t[i] = (self.t[i] + 1) % self.L
        self.s[k] = (self.s[k] + 1) % self.S
        if w[HO]:
            self.kap = i
        for c in REQUESTS:
            w[c] = 0
        self.steps += 1

    def generation(self, limit=1 << 40):
        """Steps until the bank bit changes; a run of empty records is passed in one move."""
        k0, first = self.kap, self.steps
        recs = self.records()
        zero = (0, 0, 0, 0, 0, 0)
        nxt = [None] * self.S                     # the next slot that holds a record other than the empty one
        upto = self.S
        for s in range(self.S - 1, -1, -1):
            nxt[s] = upto
            if recs[s] != zero:
                upto = s
        nonempty = [r != zero for r in recs]
        while self.kap == k0:
            s = self.s[k0]
            if not nonempty[s]:
                e = nxt[s]
                if e == self.S:                      # empty to the end of the bank: around to its first slot
                    self.steps += self.S - s
                    self.s[k0] = 0
                else:
                    self.steps += e - s
                    self.s[k0] = e
                continue
            self.step(recs[s])
            if self.steps - first > limit:
                raise RuntimeError('no hand-over')
        return self.steps - first

    def state(self):
        return (tuple(self.w[4:]), self.kap, tuple(tuple(q) for q in self.Q), tuple(self.s), tuple(self.j),
                tuple(tuple(d) for d in self.D), tuple(self.t))


def bank_image(recs, S, alpha=ALPHA):
    """A bank of S slots holding the records recs from its first slot, the rest empty."""
    bits = [x for r in recs for x in encode_record(r, alpha)]
    assert len(recs) <= S
    return bits + [0] * ((S - len(recs)) * width(alpha))


def padded(bits, L):
    assert len(bits) <= L
    return list(bits) + [0] * (L - len(bits))


# ---------------------------------------------------------------------------
# the organism
# ---------------------------------------------------------------------------

class Asm:
    """Records over named cells."""
    def __init__(self):
        self.recs, self.persist, self.names, self.uid = [], {}, {}, 0

    def keep(self, name):
        self.persist[name] = FREE + len(self.persist)
        return name

    def reg(self, name):
        return name

    def fresh(self, base):
        self.uid += 1
        return f'{base}#{self.uid}'

    def emit(self, a0, w0, a1, w1, beta, ao):
        assert -8 <= beta <= 7 and w0 in (-1, 0, 1) and w1 in (-1, 0, 1)
        self.recs.append((a0, w0, a1, w1, beta, ao))

    def AND(self, x, y, dst):
        (a, pa), (c, pc) = x, y
        self.emit(a, 1 if pa else -1, c, 1 if pc else -1, -(pa + pc), dst)

    def OR(self, x, y, dst):
        (a, pa), (c, pc) = x, y
        self.emit(a, 1 if pa else -1, c, 1 if pc else -1, (2 - pa - pc) - 1, dst)

    def COPY(self, x, dst):
        a, pa = x
        self.emit(a, 1 if pa else -1, SINK, 0, -1 if pa else 0, dst)

    def MUX(self, s, a, b, dst):
        t1, t2 = self.fresh('m'), self.fresh('m')
        self.AND((s, True), a, t1)
        self.AND((s, False), b, t2)
        self.OR((t1, True), (t2, True), dst)

    def XOR(self, a, b, dst):
        t1, t2 = self.fresh('x'), self.fresh('x')
        self.OR(a, b, t1)
        self.OR((a[0], not a[1]), (b[0], not b[1]), t2)
        self.AND((t1, True), (t2, True), dst)

    def allocate(self, cells):
        """Map every name to a window address; check each temporary is written before it is read."""
        first_w, last_r = {}, {}
        for i, (a0, w0, a1, w1, be, ao) in enumerate(self.recs):
            for a, w in ((a0, w0), (a1, w1)):
                if isinstance(a, str) and a not in self.persist and w != 0:
                    assert a in first_w, f'{a} read before written'
                    last_r[a] = i
            if isinstance(ao, str) and ao not in self.persist:
                first_w.setdefault(ao, i)
        free_from = {}
        base = FREE + len(self.persist)
        addr = dict(self.persist)
        for name in sorted(first_w, key=lambda n: first_w[n]):
            end = last_r.get(name, first_w[name])
            cand = [a for a, f in free_from.items() if f <= first_w[name]]
            a = min(cand) if cand else base + len(free_from)
            assert a < cells, 'window full'
            addr[name] = a
            free_from[a] = end
        self.names = addr
        res = lambda a: addr[a] if isinstance(a, str) else a
        self.recs = [(res(a0) if w0 else SINK, w0, res(a1) if w1 else SINK, w1, be, res(ao))
                     for (a0, w0, a1, w1, be, ao) in self.recs]
        self.next_reg = base + len(free_from)
        return self


def organism():
    """The organism: one pass carries out one step of the decoder of its description code."""
    A = Asm()
    y, n = True, False
    m, I, C, Gp, Ad = (A.keep(s) for s in ('m', 'I', 'C', 'G', 'Ad'))
    c = [A.keep(f'c{i}') for i in range(4)]     # c[3] is the first codon bit
    z = [A.keep(f'z{i}') for i in range(5)]     # down counter, z[0] least significant
    T = lambda s: A.reg('T_' + s)
    A.COPY((I, y), T('init'))
    # flags from the old state
    A.AND((z[0], n), (z[1], n), T('q'))
    A.AND((T('q'), y), (z[2], n), T('q'))
    A.AND((T('q'), y), (z[3], n), T('q'))
    A.AND((T('q'), y), (z[4], n), T('zero'))
    # the codon after this pass's shift is (c2, c1, c0, R); END and ESC at its completion
    A.AND((c[2], y), (c[1], y), T('k11'))
    A.AND((c[0], y), (RD, y), T('ss'))
    A.AND((T('k11'), y), (T('ss'), y), T('endc'))
    A.AND((T('k11'), y), (T('ss'), n), T('escn'))
    A.AND((C, y), (T('zero'), y), T('cdone'))
    A.AND((T('cdone'), y), (T('endc'), y), T('end'))
    A.AND((T('cdone'), y), (T('endc'), n), T('cgo'))
    A.AND((T('end'), y), (m, n), T('rew'))     # the end codon in construct mode: read the description again
    A.AND((T('end'), y), (m, y), T('hand'))    # the end codon in copy mode: hand over to the copy
    # the escape flag of the codon held during G (the codon is complete then)
    A.AND((c[3], y), (c[2], y), T('k'))
    A.AND((c[1], y), (c[0], y), T('s'))
    A.AND((T('k'), y), (T('s'), n), T('esc'))
    # consume, emit, copy
    A.AND((Gp, y), (T('esc'), y), T('gesc'))
    A.OR((C, y), (Ad, y), T('ca'))
    A.OR((T('ca'), y), (T('gesc'), y), T('cons'))
    A.OR((Gp, y), (Ad, y), T('ga'))
    A.AND((T('ga'), y), (m, n), T('emit'))
    A.AND((Gp, y), (T('esc'), n), T('tsel'))
    A.AND((m, y), (T('cons'), y), T('cw'))
    # the table bit at position 7 - z of the gate field, from the held codon
    A.AND((c[3], y), (c[2], n), T('cpy'))                   # COPY kind
    A.XOR((c[1], y), (c[0], y), T('x'))
    A.AND((c[1], y), (c[0], y), T('a11'))
    A.OR((c[1], y), (c[0], y), T('o11'))
    A.MUX(c[2], (T('a11'), y), (T('o11'), y), T('sg0'))     # OR: s0 and s1; AND: s0 or s1
    A.MUX(c[3], (c[1], y), (T('sg0'), y), T('sign'))        # COPY: s0
    A.XOR((c[2], y), (T('x'), y), T('od0'))                 # OR: not x; AND: x
    A.MUX(c[3], (c[1], y), (T('od0'), y), T('odd'))
    A.AND((T('cpy'), n), (c[0], n), T('w1h'))
    A.AND((T('cpy'), n), (c[0], y), T('w1l'))
    A.MUX(z[0], (c[1], n), (c[1], y), T('t11'))             # z2=1, z1=1: z0 ? not s0 : s0
    A.MUX(z[0], (T('w1h'), y), (T('w1l'), y), T('t10'))     # z2=1, z1=0: z0 ? w1h : w1l
    A.MUX(z[1], (T('t11'), y), (T('t10'), y), T('t1'))
    A.OR((z[1], y), (z[0], y), T('lo'))
    A.MUX(T('lo'), (T('sign'), y), (T('odd'), y), T('t0'))
    A.MUX(z[2], (T('t1'), y), (T('t0'), y), T('tbl'))
    A.MUX(T('tsel'), (T('tbl'), y), (RD, y), T('av'))
    # next phases: I after the hand-over, C after I
    A.AND((C, y), (T('zero'), n), T('n1'))
    A.OR((T('n1'), y), (T('rew'), y), T('n2'))
    A.AND((Ad, y), (T('zero'), y), T('n3'))
    A.OR((T('n2'), y), (T('n3'), y), T('n4'))
    A.OR((T('n4'), y), (I, y), T('nC'))
    A.OR((m, n), (T('escn'), y), T('g1'))                  # construct mode, or an escape
    A.AND((T('cgo'), y), (T('g1'), y), T('g2'))
    A.AND((Gp, y), (T('zero'), n), T('g3'))
    A.OR((T('g2'), y), (T('g3'), y), T('nG'))
    A.AND((T('cgo'), y), (T('g1'), n), T('a1'))
    A.AND((Gp, y), (T('zero'), y), T('a2'))
    A.OR((T('a1'), y), (T('a2'), y), T('a3'))
    A.AND((Ad, y), (T('zero'), n), T('a4'))
    A.OR((T('a3'), y), (T('a4'), y), T('nA'))
    # the counter: at zero and in I it loads 3, 7 or 17 for the next phase, otherwise it counts down
    A.OR((T('zero'), y), (I, y), T('ld'))
    A.COPY((z[0], n), T('d0'))
    A.COPY((z[0], n), T('b1'))
    A.XOR((z[1], y), (T('b1'), y), T('d1'))
    A.AND((T('b1'), y), (z[1], n), T('b2'))
    A.XOR((z[2], y), (T('b2'), y), T('d2'))
    A.AND((T('b2'), y), (z[2], n), T('b3'))
    A.XOR((z[3], y), (T('b3'), y), T('d3'))
    A.AND((T('b3'), y), (z[3], n), T('b4'))
    A.XOR((z[4], y), (T('b4'), y), T('d4'))
    A.OR((T('nC'), y), (T('nG'), y), T('l1'))
    A.OR((T('ld'), y), (T('d0'), y), z[0])                           # every load is odd
    A.MUX(T('ld'), (T('l1'), y), (T('d1'), y), z[1])                 # 3 and 7
    A.MUX(T('ld'), (T('nG'), y), (T('d2'), y), z[2])                 # 7
    A.AND((T('ld'), n), (T('d3'), y), z[3])
    A.MUX(T('ld'), (T('nA'), y), (T('d4'), y), z[4])                 # 17
    # the codon shifts during C
    A.MUX(C, (c[2], y), (c[3], y), c[3])
    A.MUX(C, (c[1], y), (c[2], y), c[2])
    A.MUX(C, (c[0], y), (c[1], y), c[1])
    A.MUX(C, (RD, y), (c[0], y), c[0])
    # under the arm and the copy head, from the old mode
    A.MUX(T('emit'), (T('av'), y), (ARM, y), ARM)
    A.MUX(T('cw'), (RD, y), (CPY, y), CPY)
    # the mode flips at the end codon and is construct in I
    A.XOR((m, y), (T('end'), y), T('mx'))
    A.AND((T('mx'), y), (I, n), m)
    A.COPY((T('nC'), y), C); A.COPY((T('nG'), y), Gp); A.COPY((T('nA'), y), Ad); A.COPY((T('hand'), y), I)
    # requests last: the moves, the rewinds and clears, and the hand-over at the end of the pass
    A.COPY((T('emit'), y), AA)
    A.COPY((T('cw'), y), AC)
    A.COPY((T('cons'), y), AR)
    A.OR((T('init'), y), (T('rew'), y), RR)
    A.OR((T('init'), y), (T('hand'), y), T('home'))
    A.COPY((T('home'), y), RA)
    A.COPY((T('home'), y), RC)
    A.COPY((T('init'), y), CB)
    A.COPY((T('init'), y), CT)
    A.COPY((T('hand'), y), HO)
    return A.allocate(1 << ALPHA)


def organism_bits():
    A = organism()
    rho = [b for r in A.recs for b in encode_record(r)]
    desc = describe(rho)
    out, used = translate(desc)
    assert out == rho and used == len(desc)
    return A, rho, desc


def start(A, rho, desc, K, S, L):
    """The organism in bank 0 from its first slot, its description on tape 0, the window in phase I."""
    window = [0] * (1 << ALPHA)
    window[A.names['I']] = 1
    banks = [bank_image(A.recs, S)]
    return Machine(K, S, L, banks, [padded(desc, L)], window)


def sha(bits):
    return hashlib.sha256(bytes(bits)).hexdigest()


def org_passes(rho, desc):
    """The passes of a generation: one in I, 30 per record and 4 on the end codon, one per bit of desc."""
    return 1 + 30 * (len(rho) // width(ALPHA)) + 4 + len(desc)


def run_organism(K, S, L, generations):
    A, rho, desc = organism_bits()
    G = len(A.recs)
    M = start(A, rho, desc, K, S, L)
    P = org_passes(rho, desc)
    image, tape = bank_image(A.recs, S), padded(desc, L)
    gens, states = [], []
    t0 = time.time()
    for g in range(1, generations + 1):
        steps = M.generation()
        copies = sum(1 for q in M.Q if q == image)
        gens.append(dict(generation=g, steps=steps, expected_steps=(P - 1) * S + G, kappa=M.kap, copies=copies,
                         descriptions=sum(1 for d in M.D if d == tape),
                         heads_at_origin=M.s[M.kap] == 0 and M.t[M.kap] == 0))
        states.append(M.state())
    period = [g + 1 for g in range(len(states)) if g >= K and states[g] == states[g - K]]
    esc = sum(1 for r in range(G) if codon_of(rho[r * width(ALPHA):r * width(ALPHA) + GATE]) is None)
    return dict(K=K, S=S, L=L, records=G, bank_bits=G * width(ALPHA), description_bits=len(desc), passes=P,
                escaped_records=esc, window_cells_used=A.next_reg, generations=gens,
                periodic_from=period, sha256_organism=sha(rho), sha256_description=sha(desc),
                seconds=round(time.time() - t0, 1))


def rocq_files(out_dir):
    """Write Organism.v for the Rocq development."""
    A, rho, desc = organism_bits()
    z = lambda v: f'({v})%Z' if v < 0 else f'{v}%Z'
    recs = ';\n'.join(f'  Rec {a0} {z(w0)} {a1} {z(w1)} {z(be)} {ao}' for a0, w0, a1, w1, be, ao in A.recs)
    names = ', '.join(f'{k} = {v}' for k, v in sorted(A.names.items(), key=lambda kv: kv[1])
                      if k in ('m', 'I', 'C', 'G', 'Ad') or k[0] in 'cz' and k[1:].isdigit())
    with open(os.path.join(out_dir, 'Organism.v'), 'w') as f:
        f.write(f'(* The organism: {len(A.recs)} records, generated by src/twohead.py. *)\n')
        f.write('From Stdlib Require Import List Bool Arith ZArith.\nImport ListNotations.\n'
                'From TH Require Import TwoHead.\n\n')
        f.write('Definition organism : list rec := [\n' + recs + '\n].\n\n')
        f.write(f'(* {names} *)\n')
        f.write('Definition rho : list bool := concat (map enc_rec organism).\n'
                'Definition desc : list bool := describe rho.\n')


def main_organism():
    ap = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter)
    sub = ap.add_subparsers(dest='cmd', required=True)
    r = sub.add_parser('run')
    r.add_argument('--generations', type=int, default=4)
    r.add_argument('--K', type=int, default=3)
    r.add_argument('--S', type=int, default=0)
    r.add_argument('--L', type=int, default=0)
    q = sub.add_parser('rocq')
    q.add_argument('--out', default=os.path.join(REPO, 'rocq'))
    a = ap.parse_args()
    if a.cmd == 'run':
        A, rho, desc = organism_bits()
        S = a.S or len(A.recs) + 7
        L = a.L or len(desc) + 70
        res = run_organism(a.K, S, L, a.generations)
        path = os.path.join(REPO, 'paper', 'runs', 'paper_twohead.json')
        json.dump(res, open(path, 'w'), indent=1)
        print(json.dumps(res, indent=1))
    else:
        rocq_files(a.out)


# ---------------------------------------------------------------------------
# the netlist N^alpha_{K,S,L}, in blocks, unit for unit as rocq/Phys.v defines it
# ---------------------------------------------------------------------------

NET_RECORD = os.path.join(REPO, 'paper', 'runs', 'paper_twohead_net.json')


def sand(lits):
    """The conjunction of literals (ref, positive)."""
    return (-sum(1 for _, p in lits if p), [(r, 1 if p else -1) for r, p in lits])


def sor(lits):
    return (sum(1 for _, p in lits if not p) - 1, [(r, 1 if p else -1) for r, p in lits])


def mux3(b, j, r0, sel, a, c):
    """sel ? a : c at units r0, r0 + 1, r0 + 2 of member j of block b."""
    return [sand([(sel, True), (a, True)]), sand([(sel, False), (c, True)]),
            sor([(('ref', b, j, r0), True), (('ref', b, j, r0 + 1), True)])]


class Layout:
    """The state bits: the window cells from 4 on, kappa one-hot, the banks with their head tracks,
    the tapes with theirs."""
    def __init__(self, K, S, L, alpha):
        self.K, self.S, self.L, self.alpha = K, S, L, alpha
        self.W, self.b = 1 << alpha, width(alpha)
        self.N = S * self.b
        self.nw = self.W - 4
        self.okap = self.nw
        self.obank = self.nw + K
        self.otape = self.obank + K * (self.N + S + self.b)
        self.n = self.otape + 2 * K * L

    def win(self, c):
        return ('in', c - 4)

    def kap(self, k):
        return ('in', self.okap + k % self.K)

    def q(self, k, p):
        return ('in', self.obank + k * (self.N + self.S + self.b) + p)

    def h(self, k, s):
        return ('in', self.obank + k * (self.N + self.S + self.b) + self.N + s)

    def jb(self, k, j):
        return ('in', self.obank + k * (self.N + self.S + self.b) + self.N + self.S + j)

    def d(self, k, i):
        return ('in', self.otape + k * 2 * self.L + i)

    def th(self, k, i):
        return ('in', self.otape + k * 2 * self.L + self.L + i)


# block indices, in the order of rocq/Phys.v
(B_ZERO, B_REC, B_FLD, B_TC, B_AC, B_HEAD, B_DEC0, B_DEC1, B_DECO, B_TERM0, B_XS0, B_TERM1, B_XS1, B_POS, B_NEG,
 B_MT, B_NT, B_PGE, B_B4, B_BGE, B_VAND, B_V, B_XHAT, B_KAP, B_BW, B_Q, B_HQ, B_HS, B_HJ, B_TW, B_D, B_T) = range(32)


def net_blocks(lay):
    """The blocks of N^alpha_{K,S,L}: (count, size, shape) with shape(j) the units of member j."""
    K, S, L, alpha, W, b, N, nw = lay.K, lay.S, lay.L, lay.alpha, lay.W, lay.b, lay.N, lay.nw
    R = lambda bk, j, r: ('ref', bk, j, r)
    zero = R(B_ZERO, 0, 0)
    fld = lambda x: R(B_FLD, x, K)
    act = lambda k: lay.kap(k)
    idl = lambda k: lay.kap(k + K - 1)
    v = R(B_V, 0, 0)
    req = lambda c: R(B_XHAT, c - 4, 2)
    bitsof = lambda a, t: (a >> (alpha - 1 - t)) & 1

    def cellref(a):
        if a == SINK:
            return zero
        if a in (RD, ARM, CPY):
            return R(B_HEAD, a - 1, K)
        return lay.win(a)

    blocks = [None] * 32
    blocks[B_ZERO] = (1, 1, lambda j: [sor([])])
    blocks[B_REC] = (K * b, S + 1, lambda m: [sand([(lay.h(m // b, s), True), (lay.q(m // b, s * b + m % b), True)])
                                              for s in range(S)] + [sor([(R(B_REC, m, s), True) for s in range(S)])])
    blocks[B_FLD] = (b, K + 1, lambda j: [sand([(act(k), True), (R(B_REC, k * b + j, S), True)]) for k in range(K)]
                     + [sor([(R(B_FLD, j, k), True) for k in range(K)])])
    blocks[B_TC] = (K, L + 1, lambda k: [sand([(lay.th(k, i), True), (lay.d(k, i), True)]) for i in range(L)]
                    + [sor([(R(B_TC, k, i), True) for i in range(L)])])
    blocks[B_AC] = (K, b + 1, lambda k: [sand([(lay.jb(k, j), True), (R(B_REC, k * b + j, S), True)])
                                         for j in range(b)] + [sor([(R(B_AC, k, j), True) for j in range(b)])])

    def head(m):
        if m == 0:
            us = [sand([(act(k), True), (R(B_TC, k, L), True)]) for k in range(K)]
        elif m == 1:
            us = [sand([(idl(k), True), (R(B_AC, k, b), True)]) for k in range(K)]
        else:
            us = [sand([(idl(k), True), (R(B_TC, k, L), True)]) for k in range(K)]
        return us + [sor([(R(B_HEAD, m, k), True) for k in range(K)])]
    blocks[B_HEAD] = (3, K + 1, head)
    for bk, o in ((B_DEC0, 8), (B_DEC1, 8 + alpha), (B_DECO, 8 + 2 * alpha)):
        blocks[bk] = (W, 1, lambda a, o=o: [sand([(fld(o + t), bool(bitsof(a, t))) for t in range(alpha)])])
    blocks[B_TERM0] = (W, 1, lambda a: [sand([(R(B_DEC0, a, 0), True), (cellref(a), True)])])
    blocks[B_XS0] = (1, 1, lambda j: [sor([(R(B_TERM0, a, 0), True) for a in range(W)])])
    blocks[B_TERM1] = (W, 1, lambda a: [sand([(R(B_DEC1, a, 0), True), (cellref(a), True)])])
    blocks[B_XS1] = (1, 1, lambda j: [sor([(R(B_TERM1, a, 0), True) for a in range(W)])])
    xs = lambda i: R(B_XS0, 0, 0) if i == 0 else R(B_XS1, 0, 0)
    blocks[B_POS] = (2, 1, lambda i: [sand([(fld(2 * i), False), (fld(2 * i + 1), True)])])
    blocks[B_NEG] = (2, 1, lambda i: [sand([(fld(2 * i), True), (fld(2 * i + 1), False)])])
    blocks[B_MT] = (2, 1, lambda i: [sand([(R(B_POS, i, 0), True), (xs(i), True)])])
    blocks[B_NT] = (2, 1, lambda i: [sand([(R(B_NEG, i, 0), True), (xs(i), True)])])
    blocks[B_PGE] = (5, 1, lambda i: [(2 - i, [(R(B_MT, 0, 0), 1), (R(B_MT, 1, 0), 1), (R(B_NT, 0, 0), -1),
                                              (R(B_NT, 1, 0), -1)])])
    f = fld
    blocks[B_B4] = (1, 4, lambda j: [sor([(f(5), True), (f(6), True), (f(7), True)]), sor([(f(5), True), (f(6), True)]),
                                     sand([(f(5), True), (f(6), True), (f(7), True)]), sand([(f(5), True), (f(6), True)])])
    blocks[B_BGE] = (1, 5, lambda j: [sand([(f(4), False)]), sand([(f(4), False), (R(B_B4, 0, 0), True)]),
                                      sand([(f(4), False), (R(B_B4, 0, 1), True)]),
                                      sor([(f(4), False), (R(B_B4, 0, 2), True)]),
                                      sor([(f(4), False), (R(B_B4, 0, 3), True)])])
    vand_bge = {0: 2, 1: 1, 2: 0, 3: 3, 4: 4}
    blocks[B_VAND] = (5, 1, lambda i: [sand([(R(B_PGE, i, 0), True), (R(B_BGE, 0, vand_bge[i]), True)])])
    blocks[B_V] = (1, 1, lambda j: [sor([(R(B_VAND, i, 0), True) for i in range(5)])])
    blocks[B_XHAT] = (nw, 3, lambda c: mux3(B_XHAT, c, 0, R(B_DECO, c + 4, 0), v, ('in', c)))
    blocks[B_KAP] = (K, 3, lambda k: mux3(B_KAP, k, 0, req(HO), idl(k), act(k)))
    blocks[B_BW] = (K, 2, lambda k: [sand([(idl(k), True), (R(B_DECO, ARM, 0), True)]),
                                     sand([(idl(k), True), (req(CB), True)])])

    def qbit(m):
        k, p = m // N, m % N
        return [sand([(R(B_BW, k, 0), True), (lay.h(k, p // b), True), (lay.jb(k, p % b), True)]),
                sand([(R(B_Q, m, 0), True), (v, True), (R(B_BW, k, 1), False)]),
                sand([(R(B_Q, m, 0), False), (lay.q(k, p), True), (R(B_BW, k, 1), False)]),
                sor([(R(B_Q, m, 1), True), (R(B_Q, m, 2), True)])]
    blocks[B_Q] = (K * N, 4, qbit)
    blocks[B_HQ] = (K, 4, lambda k: [sand([(idl(k), True), (req(RA), True)]),
                                     sand([(idl(k), True), (req(RA), False), (req(AA), True)]),
                                     sand([(R(B_HQ, k, 1), True), (lay.jb(k, b - 1), True)]),
                                     sor([(act(k), True), (R(B_HQ, k, 2), True)])])

    def track(bk, m, n, adv, rew, cur, prev):
        """the next bit m of a one-hot track of n cells: one back if adv, the first if rew, else itself"""
        x = m % n
        return [sand([(adv, True), (prev, True)]),
                sand([(rew, False), (adv, False), (cur, True)]),
                sand([(rew, True)]) if x == 0 else sand([(rew, True), (zero, True)]),
                sor([(R(bk, m, 0), True), (R(bk, m, 1), True), (R(bk, m, 2), True)])]
    blocks[B_HS] = (K * S, 4, lambda m: track(B_HS, m, S, R(B_HQ, m // S, 3), R(B_HQ, m // S, 0),
                                              lay.h(m // S, m % S), lay.h(m // S, (m % S + S - 1) % S)))
    blocks[B_HJ] = (K * b, 4, lambda m: track(B_HJ, m, b, R(B_HQ, m // b, 1), R(B_HQ, m // b, 0),
                                              lay.jb(m // b, m % b), lay.jb(m // b, (m % b + b - 1) % b)))
    blocks[B_TW] = (K, 8, lambda k: [sand([(idl(k), True), (R(B_DECO, CPY, 0), True)]),
                                     sand([(idl(k), True), (req(CT), True)]),
                                     sand([(act(k), True), (req(RR), True)]),
                                     sand([(idl(k), True), (req(RC), True)]),
                                     sor([(R(B_TW, k, 2), True), (R(B_TW, k, 3), True)]),
                                     sand([(act(k), True), (req(RR), False), (req(AR), True)]),
                                     sand([(idl(k), True), (req(RC), False), (req(AC), True)]),
                                     sor([(R(B_TW, k, 5), True), (R(B_TW, k, 6), True)])])

    def dbit(m):
        k, i = m // L, m % L
        return [sand([(R(B_TW, k, 0), True), (lay.th(k, i), True)]),
                sand([(R(B_D, m, 0), True), (v, True), (R(B_TW, k, 1), False)]),
                sand([(R(B_D, m, 0), False), (lay.d(k, i), True), (R(B_TW, k, 1), False)]),
                sor([(R(B_D, m, 1), True), (R(B_D, m, 2), True)])]
    blocks[B_D] = (K * L, 4, dbit)
    blocks[B_T] = (K * L, 4, lambda m: track(B_T, m, L, R(B_TW, m // L, 7), R(B_TW, m // L, 4),
                                             lay.th(m // L, m % L), lay.th(m // L, (m % L + L - 1) % L)))
    return blocks


def net_next(lay):
    """The signal computing the next value of each state bit."""
    K, S, L, b, N = lay.K, lay.S, lay.L, lay.b, lay.N
    R = lambda bk, j, r: ('ref', bk, j, r)
    out = []
    for c in range(4, lay.W):
        out.append(R(B_ZERO, 0, 0) if c <= HO else R(B_XHAT, c - 4, 2))
    out += [R(B_KAP, k, 2) for k in range(K)]
    for k in range(K):
        out += [R(B_Q, k * N + p, 3) for p in range(N)]
        out += [R(B_HS, k * S + s, 3) for s in range(S)]
        out += [R(B_HJ, k * b + j, 3) for j in range(b)]
    for k in range(K):
        out += [R(B_D, k * L + i, 3) for i in range(L)]
        out += [R(B_T, k * L + i, 3) for i in range(L)]
    assert len(out) == lay.n
    return out


def build_net(K, S, L, alpha=ALPHA):
    """The netlist: units (bias, [(signal, weight)]) in block order, and the next-state signals."""
    lay = Layout(K, S, L, alpha)
    blocks = net_blocks(lay)
    off, total = [], 0
    for count, size, _ in blocks:
        off.append(total)
        total += count * size

    def idx(r):
        return r[1] if r[0] == 'in' else lay.n + off[r[1]] + blocks[r[1]][1] * r[2] + r[3]
    units = []
    for count, size, shape in blocks:
        for j in range(count):
            us = shape(j)
            assert len(us) == size
            for bias, ins in us:
                units.append((bias, [(idx(r), w) for r, w in ins]))
    nxt = [idx(r) for r in net_next(lay)]
    return units, nxt, lay


def sizes(alpha, K, S, L):
    """The units, edges and state bits of N^alpha_{K,S,L}."""
    W, b = 1 << alpha, width(alpha)
    N = S * b
    units = 5 * K * N + 4 * K * S + 7 * K * b + 9 * K * L + 22 * K + 8 * W + b + 22
    edges = 14 * K * N + 10 * K * S + 16 * K * b + 23 * K * L + 43 * K + 3 * alpha * W + 12 * W + 46
    return dict(units=units, edges=edges, state_bits=W - 4 + K + K * (N + S + b) + 2 * K * L)


def stats(units, nxt, n):
    depth = np.zeros(n + len(units), dtype=np.int64)
    edges = 0
    for i, (bb, ins) in enumerate(units):
        depth[n + i] = 1 + max((depth[s] for s, _ in ins), default=0)
        edges += len(ins)
    return dict(units=len(units), edges=edges, depth=int(max(depth[s] for s in nxt)), state_bits=n)


def lev_rows(units, nxt, n):
    """The depth and the number of rows of the levelized map Lev(N) of Lemma 2.5, counted without
    building it: every live unit of depth below d once, a copy of every live signal in each layer
    strictly between its depth and the last layer that reads it, and the n rows of the last layer."""
    v = len(units)
    live = np.zeros(n + v, dtype=bool)
    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 = np.zeros(n + v, dtype=np.int64)
    for j, (_, ins) in enumerate(units):
        depth[n + j] = 1 + max((depth[k] for k, _ in ins), default=0)
    d = int(max(depth[n + j] for j in range(v) if live[n + j]))
    lam = np.zeros(n + v, dtype=np.int64)
    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
    rows = n
    for s in range(n + v):
        if s < n or live[s]:
            if s >= n and depth[s] < d:
                rows += 1
            rows += max(0, min(int(lam[s]) - 1, d - 1) - int(depth[s]))
    return d, rows


def evaluate(units, nxt, n, x):
    sig = list(x) + [0] * len(units)
    for i, (bb, ins) in enumerate(units):
        sig[n + i] = 1 if bb + sum(w * sig[s] for s, w in ins) >= 0 else 0
    return [sig[s] for s in nxt]


def encode(M):
    """The state bits of a state of the machine, in the order of Layout."""
    x = list(M.w[4:])
    x += [1 if k == M.kap else 0 for k in range(M.K)]
    for k in range(M.K):
        x += M.Q[k] + [1 if s == M.s[k] else 0 for s in range(M.S)] + [1 if j == M.j[k] else 0 for j in range(M.b)]
    for k in range(M.K):
        x += M.D[k] + [1 if i == M.t[k] else 0 for i in range(M.L)]
    return x


def random_machine(rnd, K, S, L, alpha):
    """A random state: random cells, kappa, banks, tapes and heads, the requests random as well."""
    b = width(alpha)
    bits = lambda k: [rnd.randint(0, 1) for _ in range(k)]
    M = Machine(K, S, L, [bits(S * b) for _ in range(K)], [bits(L) for _ in range(K)], bits(1 << alpha),
                rnd.randrange(K), alpha)
    M.s = [rnd.randrange(S) for _ in range(K)]
    M.j = [rnd.randrange(b) for _ in range(K)]
    M.t = [rnd.randrange(L) for _ in range(K)]
    M.w[:4] = [0, 0, 0, 0]
    return M


def check_net(K, S, L, trials, seed=7, alpha=ALPHA):
    """One step of the netlist against the transcription from random full states."""
    units, nxt, lay = build_net(K, S, L, alpha)
    rnd = random.Random(seed)
    bad = 0
    for _ in range(trials):
        M = random_machine(rnd, K, S, L, alpha)
        y = evaluate(units, nxt, lay.n, encode(M))
        M.step()
        bad += y != encode(M)
    st = stats(units, nxt, lay.n)
    assert {k: st[k] for k in ('units', 'edges', 'state_bits')} == sizes(alpha, K, S, L), (st, sizes(alpha, K, S, L))
    return bad, st


def netfile_bytes(units, nxt, n):
    parts = [np.array([n, len(units), sum(len(i) for _, i in units)], dtype='<i4'),
             np.array([b for b, _ in units], dtype='<i4'),
             np.array([len(i) for _, i in units], dtype='<i4'),
             np.array([w * (s + 1) for _, i in units for s, w in i], dtype='<i4'),
             np.array(nxt, dtype='<i4')]
    return b''.join(p.tobytes() for p in parts)


ORG_UNIVERSE = dict(K=3, S=160, L=3200)


def net_update_record(key, value):
    rec = json.load(open(NET_RECORD)) if os.path.exists(NET_RECORD) else {}
    rec[key] = value
    json.dump(rec, open(NET_RECORD, 'w'), indent=1)


def main_net():
    cmd = sys.argv[1] if len(sys.argv) > 1 else 'check'
    if cmd == 'check':
        t0 = time.time()
        res = {}
        for name, (K, S, L, alpha, trials) in dict(small=(2, 3, 9, 6, 300), ring=(4, 2, 5, 6, 300),
                                                   wide=(3, 2, 7, 8, 100)).items():
            bad, st = check_net(K, S, L, trials, alpha=alpha)
            res[name] = dict(K=K, S=S, L=L, alpha=alpha, states=trials, disagreements=bad, netlist=st)
            print(name, res[name], flush=True)
        u = ORG_UNIVERSE
        units, nxt, lay = build_net(u['K'], u['S'], u['L'])
        res['organism_universe'] = dict(**u, netlist=stats(units, nxt, lay.n))
        res['seconds'] = round(time.time() - t0, 1)
        net_update_record('random_states', res)
        print(json.dumps(res, indent=1))
        sys.exit(0 if all(res[k]['disagreements'] == 0 for k in ('small', 'ring', 'wide')) else 1)
    elif cmd == 'lockstep':
        gens = int(sys.argv[2]) if len(sys.argv) > 2 else 1
        u = ORG_UNIVERSE
        A, rho, desc = organism_bits()
        units, nxt, lay = build_net(u['K'], u['S'], u['L'])
        tmp = os.path.join(REPO, 'variants')
        netpath, initpath = os.path.join(tmp, '.ring_net.bin'), os.path.join(tmp, '.ring_init.bin')
        open(netpath, 'wb').write(netfile_bytes(units, nxt, lay.n))
        M = start(A, rho, desc, u['K'], u['S'], u['L'])
        write_machine(initpath, M, bank_image(A.recs, u['S']), padded(desc, u['L']))
        exe = os.path.join(tmp, '.ring_run')
        subprocess.run(['gcc', '-O2', '-o', exe, os.path.join(REPO, 'src', 'ring_run.c')], check=True)
        t0 = time.time()
        out = subprocess.run([exe, initpath, str(gens), netpath], capture_output=True, text=True).stdout
        for p in (initpath, exe, netpath):
            os.remove(p)
        lines = [json.loads(l) for l in out.splitlines() if l.strip()]
        res = dict(**u, generations=lines, seconds=round(time.time() - t0, 1))
        net_update_record('lockstep', res)
        print(json.dumps(res, indent=1))
    elif cmd == 'lev':
        # the rows of Lev(N^alpha_{3,S,L}) for the window of the stored host, affine in S and L, and the noise
        # a generation of the stored host survives with probability 0.999 by Proposition 8.4 and Theorem 8.8(ii)
        t0 = time.time()
        run = json.load(open(STORED_RECORD))['run']
        alpha = (run['record_bits'] - 8) // 3
        pts = []
        for S, L in ((2, 3), (3, 3), (2, 5), (3, 5), (4, 9), (6, 4)):
            units, nxt, lay = build_net(3, S, L, alpha)
            d, rows = lev_rows(units, nxt, lay.n)
            pts.append(dict(S=S, L=L, depth=d, rows=rows))
            print(pts[-1], flush=True)
        r0 = {(p['S'], p['L']): p['rows'] for p in pts}
        cS, cL = r0[(3, 3)] - r0[(2, 3)], (r0[(2, 5)] - r0[(2, 3)]) // 2
        c0 = r0[(2, 3)] - 2 * cS - 3 * cL
        affine = all(c0 + cS * p['S'] + cL * p['L'] == p['rows'] for p in pts)
        M = c0 + cS * run['S'] + cL * run['L']
        T = run['steps_expected']

        def s_max(r):
            lo, hi = 1e-4, 2.0
            for _ in range(200):
                mid = (lo + hi) / 2
                if T * r * M * math.erfc(r / (2 * math.sqrt(2) * mid)) <= 1e-3:
                    lo = mid
                else:
                    hi = mid
            return lo
        res = dict(K=3, alpha=alpha, members=pts, rows=dict(constant=c0, per_slot=cS, per_cell=cL),
                   affine=affine, depth=pts[0]['depth'], stored_member=dict(S=run['S'], L=run['L'], rows=M,
                   steps=T), s_max_0999={str(r): round(s_max(r), 4) for r in (1, 3, 5)},
                   seconds=round(time.time() - t0, 1))
        net_update_record('levelized', res)
        print(json.dumps(res, indent=1))
    elif cmd == 'extract':
        # rocq/Extract.v writes rocq/extract/physnet.ml during the build of rocq/
        ex = os.path.join(REPO, 'rocq', 'extract')
        subprocess.run(['ocamlfind', 'ocamlopt', '-package', 'stdlib', 'physnet.mli', 'physnet.ml', 'dump.ml',
                        '-o', 'dump'], cwd=ex, check=True)
        out = os.path.join(ex, 'phys_rocq.bin')
        members = []
        u = ORG_UNIVERSE
        for alpha, K, S, L in ((ALPHA, u['K'], u['S'], u['L']), (12, 2, 3, 40), (6, 5, 2, 7)):
            units, nxt, lay = build_net(K, S, L, alpha)
            ours = netfile_bytes(units, nxt, lay.n)
            subprocess.run([os.path.join(ex, 'dump'), str(alpha), str(K), str(S), str(L), out], check=True)
            theirs = open(out, 'rb').read()
            members.append(dict(alpha=alpha, K=K, S=S, L=L, 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))
        res = dict(members=members, identical=all(m['identical'] for m in members))
        net_update_record('extraction', res)
        print(json.dumps(res, indent=1))


# ---------------------------------------------------------------------------
# the machine in C: the state written for src/ring_run.c
# ---------------------------------------------------------------------------

def write_machine(path, M, image, tape):
    """int32 alpha, K, S, L, kappa; the window; each bank, each tape; the heads; the image and the tape that a
    bank and a tape are compared with at each hand-over, one byte per bit."""
    with open(path, 'wb') as f:
        f.write(struct.pack('<5i', M.alpha, M.K, M.S, M.L, M.kap))
        f.write(bytes(M.w))
        for q in M.Q:
            f.write(bytes(q))
        for d in M.D:
            f.write(bytes(d))
        f.write(struct.pack(f'<{3 * M.K}i', *(M.s + M.j + M.t)))
        f.write(bytes(image) + bytes(tape))


# ---------------------------------------------------------------------------
# the host netlist from its serialization
# ---------------------------------------------------------------------------

STORED_RECORD = os.path.join(REPO, 'paper', 'runs', 'paper_stored_host.json')

CW = 20                                         # the least width of the device's byte counters


def host_units(A=8):
    data = SR.read_host() if A == 8 else SR.sigma(A)
    hlen = struct.unpack('<Q', data[:8])[0]
    head = json.loads(data[8:8 + hlen])
    T = {}
    import array
    for k, spec in head.items():
        if k == '__metadata__':
            continue
        lo, hi = spec['data_offsets']
        a = array.array({'I8': 'b', 'I16': 'h', 'I32': 'i'}[spec['dtype']])
        a.frombytes(data[8 + hlen + lo:8 + hlen + hi])
        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


# state layout of sigma: the A counter bits most significant first, the halt bit at A, and bit k of
# word j at A + 1 + A j + k, k = 0 the most significant
def mem_bit(j, t, A=8):
    """State index of bit t (value 2^t) of memory word j."""
    return A + 1 + A * j + (A - 1 - t)


def pc_bit(t, A=8):
    """State index of bit t of the counter."""
    return A - 1 - t


# ---------------------------------------------------------------------------
# records over named cells
# ---------------------------------------------------------------------------

MX = (('v', 'm0'), ('v', 'm1'))                 # the two cells inside a multiplexer or an exclusive or


class Prog:
    def __init__(self):
        self.recs = []                           # (a0, w0, a1, w1, beta, ao), cells by name
        self.ends = {}                           # record -> the unit of the host whose value it writes

    def emit(self, a0, w0, a1, w1, beta, ao):
        assert -8 <= beta <= 7
        self.recs.append((a0 if w0 else ('c', SINK), w0, a1 if w1 else ('c', SINK), w1, beta, ao))

    def AND(self, x, y, dst):
        (a, pa), (b, pb) = x, y
        self.emit(a, 1 if pa else -1, b, 1 if pb else -1, -(pa + pb), dst)

    def OR(self, x, y, dst):
        (a, pa), (b, pb) = x, y
        self.emit(a, 1 if pa else -1, b, 1 if pb else -1, 1 - pa - pb, dst)

    def COPY(self, x, dst):
        a, pa = x
        self.emit(a, 1 if pa else -1, None, 0, -1 if pa else 0, dst)

    def CONST(self, v, dst):
        # a gate of one literal and its negation: OR is 1, AND is 0
        x = ('c', SINK)
        (self.OR if v else self.AND)((x, True), (x, False), dst)

    def XOR(self, x, y, dst):
        t1, t2 = MX
        self.OR(x, y, t1)
        self.OR((x[0], not x[1]), (y[0], not y[1]), t2)
        self.AND((t1, True), (t2, True), dst)

    def MUX(self, s, a, b, dst):
        """dst <- s ? a : b, s a cell, a and b literals."""
        t1, t2 = MX
        self.AND((s, True), a, t1)
        self.AND((s, False), b, t2)
        self.OR((t1, True), (t2, True), dst)

    def chain(self, kind, lits, dst, acc):
        """The literals joined by 'and' or 'or', accumulated in acc, the last record writing dst."""
        g = self.AND if kind == 'and' else self.OR
        k = len(lits)
        if k == 1:
            self.COPY(lits[0], dst)
            return
        if k == 2:
            g(lits[0], lits[1], dst)
            return
        g(lits[0], lits[1], acc)
        for i in range(2, k - 1):
            g((acc, True), lits[i], acc)
        g((acc, True), lits[k - 1], dst)

    def unit(self, t, lits, dst, acc, lev):
        """At least t of the literals, into dst, by T_t(x1..xk) = T_t(x2..xk) or (x1 and T_{t-1}(x2..xk)),
        the three cells of level lev holding T_t(x2..xk), T_{t-1}(x2..xk) and the conjunction."""
        k = len(lits)
        if t <= 0:
            self.CONST(1, dst)
        elif t > k:
            self.CONST(0, dst)
        elif t == 1:
            self.chain('or', lits, dst, acc)
        elif t == k:
            self.chain('and', lits, dst, acc)
        else:
            a, b, c = (('x', lev, i) for i in range(3))
            self.unit(t, lits[1:], a, a, lev + 1)
            self.unit(t - 1, lits[1:], b, b, lev + 1)
            self.AND(lits[0], (b, True), c)
            self.OR((a, True), (c, True), dst)


def unit_threshold(bias, ins):
    """The least number of true literals at which the unit fires."""
    return sum(1 for _, w in ins if w < 0) - bias


def compile_host(P, A=8):
    """The records of one step of H_A: the units in the order of the netlist, unit u in cell ('u', u), and the
    unit of the next value of state bit i writing ('s', i) with its last record."""
    n, units, nxt = host_units(A)
    is_next = {nxt[i] - n: i for i in range(n)}
    assert len(is_next) == n and all(v >= n for v in nxt)
    for u, (bias, ins) in enumerate(units):
        assert all(w in (1, -1) for _, w in ins)
        lits = [(('s', s) if s < n else ('u', s - n), w > 0) for s, w in ins]
        dst = ('s', is_next[u]) if u in is_next else ('u', u)
        P.unit(unit_threshold(bias, ins), lits, dst, ('u', u), 0)
        P.ends[len(P.recs) - 1] = u
    return n, units, nxt


def threshold_levels(units):
    """The levels of cells the units of threshold strictly between 1 and their fan-in use."""
    return max([len(ins) - 2 for b, ins in units if 1 < unit_threshold(b, ins) < len(ins)] or [0])


# ---------------------------------------------------------------------------
# the device, the startup block and the hand-over
# ---------------------------------------------------------------------------

def mem_cell(j, t, A=8):
    return ('s', mem_bit(j, t, A))


def word_is_one(P, j, dst, A=8):
    """[memory word j == 1] into dst"""
    lits = [(mem_cell(j, 0, A), True)] + [(mem_cell(j, t, A), False) for t in range(1, A)]
    P.chain('and', lits, dst, dst)
    return dst


def device_cells(w):
    """The cells of the device, in the order of their addresses."""
    return ['wr', 'rd', 'rw'] + [('e', i) for i in range(w)] + ['eq', 'eot', 'ca', 'cc', 'g'] + \
        [('car', i) for i in range(1, w)] + ['m0', 'm1']


def compile_device(P, A=8, w=CW):
    io = SR.io_cells(A)
    cnt = [('d', 'cnt', i) for i in range(w)]
    lim = [('d', 'lim', i) for i in range(w)]
    dest = ('d', 'dest')
    v = lambda name: ('v', name)
    wr = word_is_one(P, io['c_wr'], v('wr'), A)
    rd = word_is_one(P, io['c_rd'], v('rd'), A)
    rw = word_is_one(P, io['c_rw'], v('rw'), A)
    # [cnt == lim]
    eq = v('eq')
    xs = []
    for i in range(w):
        e = v(('e', i))
        a1, a0 = MX
        P.AND((cnt[i], True), (lim[i], True), a1)
        P.AND((cnt[i], False), (lim[i], False), a0)
        P.OR((a1, True), (a0, True), e)
        xs.append((e, True))
    P.chain('and', xs, eq, eq)
    eot = v('eot')                               # the end of the recipe is known after the rewind
    P.AND((eq, True), (dest, True), eot)
    # (i) the low byte of R_out, most significant bit first, under the arm or under the copy head
    ca, cc = v('ca'), v('cc')
    P.AND((wr, True), (dest, False), ca)
    P.AND((wr, True), (dest, True), cc)
    out, inp, ceot = io['r_out'], io['r_in'], io['c_eot']
    for t in range(7, -1, -1):
        P.MUX(ca, (mem_cell(out, t, A), True), (('c', ARM), True), ('c', ARM))
        P.COPY((ca, True), ('c', AA))
        P.MUX(cc, (mem_cell(out, t, A), True), (('c', CPY), True), ('c', CPY))
        P.COPY((cc, True), ('c', AC))
    for t in range(A):
        P.AND((mem_cell(out, t, A), True), (wr, False), mem_cell(out, t, A))
    g = v('g')
    P.AND((rd, True), (eot, False), g)
    # (ii) the byte under the read head into R_in, most significant bit first, each bit moving the head,
    # and its sign bit into the bits above it
    for t in range(7, -1, -1):
        P.MUX(g, (('c', RD), True), (mem_cell(inp, t, A), True), mem_cell(inp, t, A))
        P.COPY((g, True), ('c', AR))
    for t in range(8, A):
        P.MUX(g, (mem_cell(inp, 7, A), True), (mem_cell(inp, t, A), True), mem_cell(inp, t, A))
    # c_eot: bit 0 <- [cnt == lim] on a read, the other bits cleared on a read
    P.MUX(rd, (eot, True), (mem_cell(ceot, 0, A), True), mem_cell(ceot, 0, A))
    for t in range(1, A):
        P.AND((mem_cell(ceot, t, A), True), (rd, False), mem_cell(ceot, t, A))
    # the counter of bytes read: carries first, then the sum bits
    car = [g]
    for i in range(w - 1):
        c = v(('car', i + 1))
        P.AND((car[-1], True), (cnt[i], True), c)
        car.append(c)
    for i in range(w):
        P.XOR((cnt[i], True), (car[i], True), cnt[i])
    # (iii) a rewind: the read head returns to the first cell, the limit takes the count, the count
    # returns to 0, and the writes go to the copy tape
    P.COPY((rw, True), ('c', RR))
    for i in range(w):
        P.MUX(rw, (cnt[i], True), (lim[i], True), lim[i])
        P.AND((cnt[i], True), (rw, False), cnt[i])
    P.OR((dest, True), (rw, True), dest)
    # (iv) the request cells cleared
    for c in ('c_wr', 'c_rd', 'c_rw'):
        for t in range(A):
            P.CONST(0, mem_cell(io[c], t, A))


def compile_startup(P, mem_image, A=8, w=CW):
    """The startup records: while booted is 0, load the memory image and clear the counter, halt bit and
    registers, rewind the read head, and clear the idle bank and the copy tape with their heads at the origin."""
    b = ('d', 'booted')
    for j in range(1 << A):
        for t in range(A):
            c = mem_cell(j, t, A)
            if (mem_image[j] >> t) & 1:
                P.OR((c, True), (b, False), c)           # b ? c : 1
            else:
                P.AND((c, True), (b, True), c)           # b ? c : 0
    for t in range(A):
        P.AND((('s', pc_bit(t, A)), True), (b, True), ('s', pc_bit(t, A)))
    P.AND((('s', A), True), (b, True), ('s', A))
    for i in range(w):
        P.AND((('d', 'cnt', i), True), (b, True), ('d', 'cnt', i))
        P.AND((('d', 'lim', i), True), (b, True), ('d', 'lim', i))
    P.AND((('d', 'dest'), True), (b, True), ('d', 'dest'))
    for c in (RR, CB, RA, CT, RC):
        P.COPY((b, False), ('c', c))
    P.CONST(1, b)


def compile_handover(P, A=8):
    """The hand-over records: at the halt, clear booted, bring the arm and the copy head to their origins,
    and hand over, the last record."""
    h = ('s', A)
    P.AND((('d', 'booted'), True), (h, False), ('d', 'booted'))
    for c in (RA, RC, HO):
        P.COPY((h, True), ('c', c))


HANDOVER_RECORDS = 4


# ---------------------------------------------------------------------------
# allocation and encoding
# ---------------------------------------------------------------------------

def layout(A, w, n, n_units, levels):
    """Window addresses: booted, the counter, dest and the limit, the state bits, one cell for each unit of
    H_A, three cells for each level of a threshold unit, and the cells of the device."""
    addr = {('d', 'booted'): FREE}
    for i in range(w):
        addr[('d', 'cnt', i)] = FREE + 1 + i
        addr[('d', 'lim', i)] = FREE + 2 + w + i
    addr[('d', 'dest')] = FREE + 1 + w
    base = FREE + 2 + 2 * w
    for i in range(n):
        addr[('s', i)] = base + i
    for u in range(n_units):
        addr[('u', u)] = base + n + u
    xbase = base + n + n_units
    for lev in range(levels):
        for k in range(3):
            addr[('x', lev, k)] = xbase + 3 * lev + k
    dbase = xbase + 3 * levels
    names = device_cells(w)
    for k, name in enumerate(names):
        addr[('v', name)] = dbase + k
    return addr, dbase + len(names)


def bits_to_bytes(bits):
    assert len(bits) % 8 == 0
    return bytes(sum(bits[i + k] << (7 - k) for k in range(8)) for i in range(0, len(bits), 8))


def bytes_to_bits(data):
    return [(b >> (7 - k)) & 1 for b in data for k in range(8)]


def check_schedule(recs, lo, hi, n):
    """Check the in-place order of the host block: every state bit written once, after its last reader,
    and every other cell the block reads written earlier in it."""
    written = {}
    for i in range(lo, hi):
        ao = recs[i][5]
        if ao[0] == 's':
            assert ao not in written, ('state bit written twice', ao)
            written[ao] = i
    assert len(written) == n, 'a state bit without its next value'
    seen = set()
    for i in range(lo, hi):
        a0, w0, a1, w1, _, ao = recs[i]
        for a, w in ((a0, w0), (a1, w1)):
            if w and a[0] == 's':
                assert i <= written[a], ('state bit read after it is written', a)
            elif w and a[0] != 'c':
                assert a in seen, ('read before written', a)
        seen.add(ao)
    return dict(state_bits_written=len(written))


EMPTY = (SINK, 0, SINK, 0, 0, SINK)


def build_stored(A=8):
    """The stored host of H_A, with the least counters from CW bits on and the least window that hold it."""
    w = CW
    while True:
        P = Prog()
        compile_startup(P, SR.memory_image_a(SR.P_STAR, A), A, w)
        lo = len(P.recs)
        n, units, nxt = compile_host(P, A)
        n_host = len(P.recs) - lo
        check_schedule(P.recs, lo, len(P.recs), n)
        compile_device(P, A, w)
        n_device = len(P.recs) - lo - n_host
        compile_handover(P, A)
        addr, top = layout(A, w, n, len(units), threshold_levels(units))
        res = lambda a: a[1] if a[0] == 'c' else addr[a]
        recs = [(res(a0), w0, res(a1), w1, be, res(ao)) for (a0, w0, a1, w1, be, ao) in P.recs]
        alpha = (top - 1).bit_length()
        b = 8 + 3 * alpha
        pad = 0
        while b * len(recs) % 8:                 # an image of whole bytes: empty records before the hand-over
            recs.insert(len(recs) - HANDOVER_RECORDS, EMPTY)
            pad += 1
        if 2 * (b * len(recs) // 8) + 1 < 1 << w:
            break
        w += 1
    image_bits = [x for r in recs for x in encode_record(r, alpha)]
    image = bits_to_bytes(image_bits)
    tau = SR.describe(image)
    assert SR.decode(tau) == image
    return dict(A=A, w=w, alpha=alpha, b=b, recs=recs, addr=addr, top=top, image=image, image_bits=image_bits,
                tau=tau, startup_records=lo, n_host_records=n_host, device_records=n_device, padding=pad,
                host=(n, units, nxt), ends=P.ends)


# ---------------------------------------------------------------------------
# one pass against H_A and the device
# ---------------------------------------------------------------------------

def host_step(n, units, nxt, x):
    sig = list(x) + [0] * len(units)
    for u, (b, ins) in enumerate(units):
        sig[n + u] = 1 if b + sum(w * sig[s] for s, w in ins) >= 0 else 0
    return [sig[v] for v in nxt]


def check_stored(trials=40, seed=3, verbose=False, A=8):
    """One pass of S_A from random states, against the startup, a step of H_A and the device."""
    S = build_stored(A)
    recs, addr, w, alpha, b = S['recs'], S['addr'], S['w'], S['alpha'], S['b']
    n, units, nxt = S['host']
    io = SR.io_cells(A)
    G = len(recs)
    rng = random.Random(seed)
    bad = 0
    m0 = SR.memory_image_a(SR.P_STAR, A)
    x0 = [0] * n                                 # the state x_0(m*)
    for j in range(1 << A):
        for t in range(A):
            x0[mem_bit(j, t, A)] = (m0[j] >> t) & 1
    K, slots, L = 3, G + 2, 80
    for trial in range(trials):
        # a random host state with random device registers, temporaries, tapes, idle bank and heads; every
        # fifth state not yet booted, and in every third the requests hold random words
        x = [rng.randrange(2) for _ in range(n)]
        x[A] = 0 if trial % 4 else 1
        booted = 0 if trial % 5 == 0 else 1
        for c in ('c_wr', 'c_rd', 'c_rw'):
            v = rng.randrange(1 << A) if trial % 3 == 0 else rng.choice((0, 1))
            for t in range(A):
                x[mem_bit(io[c], t, A)] = (v >> t) & 1
        cnt, lim = rng.randrange(8), rng.randrange(8)
        dest = rng.randrange(2)
        win = [rng.randrange(2) for _ in range(1 << alpha)]
        for i in range(n):
            win[addr[('s', i)]] = x[i]
        for i in range(w):
            win[addr[('d', 'cnt', i)]] = (cnt >> i) & 1
            win[addr[('d', 'lim', i)]] = (lim >> i) & 1
        win[addr[('d', 'dest')]] = dest
        win[addr[('d', 'booted')]] = booted
        for c in REQUESTS:
            win[c] = 0
        win[:4] = [0, 0, 0, 0]
        kap = rng.randrange(K)
        bits = lambda k: [rng.randrange(2) for _ in range(k)]
        banks = [bits(slots * b) for _ in range(K)]
        banks[kap] = bank_image(recs, slots, alpha)
        tapes = [bits(L) for _ in range(K)]
        M = Machine(K, slots, L, banks, tapes, win, kap, alpha)
        M.s = [rng.randrange(slots) for _ in range(K)]
        M.j = [rng.randrange(b) for _ in range(K)]
        M.t = [rng.randrange(L - 16) for _ in range(K)]
        M.s[kap] = 0
        idle = (kap + 1) % K
        Q1, D0, D1 = list(M.Q[idle]), list(M.D[kap]), list(M.D[idle])
        sq, jq, hd0, hd1 = M.s[idle], M.j[idle], M.t[kap], M.t[idle]
        for g in range(G):
            M.step()
        # expected: the startup if not booted, one step of H_A, then the device
        if not booted:
            x, cnt, lim, dest = list(x0), 0, 0, 0
            Q1, D1 = [0] * len(Q1), [0] * L
            sq, jq, hd0, hd1 = 0, 0, 0, 0
        y = host_step(n, units, nxt, x)
        get = lambda j: sum(y[mem_bit(j, t, A)] << t for t in range(A))

        def put(j, v):
            for t in range(A):
                y[mem_bit(j, t, A)] = (v >> t) & 1
        e_cnt, e_lim, e_dest = cnt, lim, dest
        if get(io['c_wr']) == 1:
            byte = get(io['r_out']) & 0xFF
            for kk in range(8):
                bit = (byte >> (7 - kk)) & 1
                if e_dest:
                    D1[hd1] = bit
                    hd1 = (hd1 + 1) % L
                else:
                    Q1[sq * b + jq] = bit
                    jq += 1
                    if jq == b:
                        jq, sq = 0, (sq + 1) % slots
            put(io['r_out'], 0)
        if get(io['c_rd']) == 1:
            if not (e_dest and e_cnt == e_lim):
                byte = sum(D0[(hd0 + kk) % L] << (7 - kk) for kk in range(8))
                put(io['r_in'], byte if byte < 128 else byte + (1 << A) - 256)
                hd0 = (hd0 + 8) % L
                put(io['c_eot'], 0)
                e_cnt = (e_cnt + 1) % (1 << w)
            else:
                put(io['c_eot'], 1)
        if get(io['c_rw']) == 1:
            e_lim, e_cnt, e_dest, hd0 = e_cnt, 0, 1, 0
        for c in ('c_wr', 'c_rd', 'c_rw'):
            put(io[c], 0)
        h = y[A]
        e_kap = idle if h else kap
        if h:
            sq, jq, hd1 = 0, 0, 0
        got = [M.w[addr[('s', i)]] for i in range(n)]
        g_cnt = sum(M.w[addr[('d', 'cnt', i)]] << i for i in range(w))
        g_lim = sum(M.w[addr[('d', 'lim', i)]] << i for i in range(w))
        parts = dict(state=got == y, cnt=g_cnt == e_cnt, lim=g_lim == e_lim,
                     dest=M.w[addr[('d', 'dest')]] == e_dest, bank=M.Q[idle] == Q1, copy=M.D[idle] == D1,
                     arm=(M.s[idle], M.j[idle]) == (sq, jq), read=M.t[kap] == hd0, copyhead=M.t[idle] == hd1,
                     kappa=M.kap == e_kap, tape=M.D[kap] == D0,
                     booted=M.w[addr[('d', 'booted')]] == 1 - h,
                     requests=all(M.w[c] == 0 for c in REQUESTS), active=M.Q[kap] == bank_image(recs, slots, alpha),
                     active_head=M.s[kap] == G % slots)
        ok = all(parts.values())
        if not ok and verbose:
            print(trial, [k for k, v in parts.items() if not v], 'reqs',
                  [get(io[c]) for c in ('c_wr', 'c_rd', 'c_rw')], 'dest', dest, 'cnt', cnt, 'lim', lim,
                  'halt', x[A], [i for i in range(n) if got[i] != y[i]][:10])
        bad += not ok
    return dict(trials=trials, disagreements=bad, records=G, window_cells=S['top'])


# ---------------------------------------------------------------------------
# the records on decision diagrams
# ---------------------------------------------------------------------------

class BDD:
    """Reduced ordered decision diagrams; a node is an integer, 0 and 1 the leaves."""
    def __init__(self):
        self.node = [None, None]
        self.uniq, self.memo = {}, {}

    def mk(self, v, lo, hi):
        if lo == hi:
            return lo
        r = self.uniq.get((v, lo, hi))
        if r is None:
            r = self.uniq[(v, lo, hi)] = len(self.node)
            self.node.append((v, lo, hi))
        return r

    def var(self, v):
        return self.mk(v, 0, 1)

    def ite(self, f, g, h):
        if f < 2:
            return g if f else h
        if g == h:
            return g
        if g == 1 and h == 0:
            return f
        key = (f, g, h)
        r = self.memo.get(key)
        if r is None:
            v = min(self.node[x][0] for x in key if x > 1)
            lo = [x if x < 2 or self.node[x][0] != v else self.node[x][1] for x in key]
            hi = [x if x < 2 or self.node[x][0] != v else self.node[x][2] for x in key]
            r = self.memo[key] = self.mk(v, self.ite(*lo), self.ite(*hi))
        return r

    def NOT(self, f):
        return self.ite(f, 0, 1)

    def AND(self, f, g):
        return self.ite(f, g, 0)

    def OR(self, f, g):
        return self.ite(f, 1, g)

    def XOR(self, f, g):
        return self.ite(f, self.NOT(g), g)

    def record(self, w0, x, w1, y, beta):
        """H(w0 x + w1 y + beta) of the bits x and y."""
        val = lambda a, b: 1 if w0 * a + w1 * b + beta >= 0 else 0
        return self.ite(x, self.ite(y, val(1, 1), val(1, 0)), self.ite(y, val(0, 1), val(0, 0)))

    def atleast(self, t, lits):
        """At least t of the literals (x, positive) are true."""
        if t <= 0:
            return 1
        row = [1] + [0] * t
        for x, pos in reversed(lits):
            row = [1] + [self.ite(x, row[j - 1], row[j]) if pos else self.ite(x, row[j], row[j - 1])
                         for j in range(1, t + 1)]
        return row[t]


class SymHead:
    """A head on a symbolic tape: P[i] is the diagram of 'the head is i cells from where it started', cells[i]
    the content of that cell, a fresh variable until it is written. A rewind is recorded as a diagram."""
    def __init__(self, D, fresh, span):
        self.D, self.span = D, span
        self.P = [1] + [0] * span
        self.cells = [fresh(i) for i in range(span + 1)]
        self.rewound = 0

    def read(self):
        D, acc = self.D, 0
        for i in range(self.span + 1):
            acc = D.OR(acc, D.AND(self.P[i], self.cells[i]))
        return acc

    def write(self, cond, v):
        D = self.D
        for i in range(self.span + 1):
            here = D.AND(cond, self.P[i])
            self.cells[i] = D.ite(here, v, self.cells[i])

    def advance(self, cond):
        D = self.D
        assert self.P[self.span] == 0, 'the head left the window of the check'
        self.P = [D.ite(cond, self.P[i - 1] if i else 0, self.P[i]) for i in range(self.span + 1)]

    def rewind(self, cond):
        self.rewound = self.D.OR(self.rewound, cond)


def symbolic_check(A=8):
    """The records of S_A on decision diagrams: the startup, the step of H_A, the device and the hand-over."""
    sys.setrecursionlimit(100000)
    t0 = time.time()
    S = build_stored(A)
    n, units, nxt = host_units(A)
    b, alpha, w = S['b'], S['alpha'], S['w']
    bits = bytes_to_bits(S['image'])
    recs = [decode_record(bits[k * b:(k + 1) * b], alpha) for k in range(len(bits) // b)]
    lo = S['startup_records']
    hi = lo + S['n_host_records']
    hd = hi + S['device_records']
    addr = S['addr']
    io = SR.io_cells(A)
    D = BDD()
    # the value of every signal on the current state: a unit that is a constant or a literal is that,
    # and the units of one function share the variable of the first; fn[u] is the function of unit u
    # of the values of its predecessors; later signals lie nearer the root
    var = lambda s: D.var((1 << 29) - s)
    top = lambda x: D.node[x][0] if x > 1 else 1 << 31
    val, first, fn = [var(s) for s in range(n)], {}, []
    for u, (bias, ins) in enumerate(units):
        lits = sorted(((val[s], wt > 0) for s, wt in ins), key=lambda l: top(l[0]))
        f = D.atleast(sum(1 for _, wt in ins if wt < 0) - bias, lits)
        fn.append(f)
        val.append(var(first.setdefault(f, n + u)) if f > 1 and D.node[f][1:] not in ((0, 1), (1, 0)) else f)
    unknown = lambda c: D.var(1 << 30 | c)
    state = [addr[('s', i)] for i in range(n)]
    ends = S['ends']
    agree = [True]

    def run(window, a, z, heads=None):
        # at the record that the compiler names as writing the value of unit u, the cell must hold
        # the function of u, and from then on it holds the value of u; the request cells act on the
        # symbolic heads after each record
        reqlog = []
        for k in range(a, z):
            a0, w0, a1, w1, beta, ao = recs[k]
            if heads is not None:
                window[RD], window[ARM], window[CPY] = heads['R'].read(), heads['A'].read(), heads['C'].read()
            g = D.record(w0, window[a0], w1, window[a1], beta)
            if k in ends:
                u = ends[k]
                agree[0] &= g == fn[u]
                g = val[n + u]
            if ao == ARM:
                heads['A'].write(1, g)
            elif ao == CPY:
                heads['C'].write(1, g)
            elif ao > CPY:
                window[ao] = g
            if ao in REQUESTS:
                reqlog.append((ao, g))
                if heads is not None:
                    if ao == AR:
                        heads['R'].advance(g)
                    elif ao == AA:
                        heads['A'].advance(g)
                    elif ao == AC:
                        heads['C'].advance(g)
                    elif ao == RR:
                        heads['R'].rewind(g)
                window[ao] = 0
        return reqlog

    # the startup: x_0(m*) when booted is 0, the window unchanged when it is 1, and the requests ~booted
    boot = addr[('d', 'booted')]
    window = [unknown(c) for c in range(1 << alpha)]
    for c in REQUESTS:
        window[c] = 0
    regs = [addr[('d', 'cnt', i)] for i in range(w)] + [addr[('d', 'lim', i)] for i in range(w)] + \
        [addr[('d', 'dest')]]
    before = list(window)
    log = run(window, 0, lo)
    B0 = before[boot]
    m0 = SR.memory_image_a(SR.P_STAR, A)
    x0 = [0] * n
    for j in range(1 << A):
        for t in range(A):
            x0[mem_bit(j, t, A)] = (m0[j] >> t) & 1
    startup = window[boot] == 1 and all(window[c] == D.ite(B0, before[c], 0) for c in regs) and \
        all(window[state[i]] == D.ite(B0, before[state[i]], x0[i]) for i in range(n)) and \
        sorted(log) == sorted((c, D.NOT(B0)) for c in (RR, CB, RA, CT, RC))
    # the step: from every window, the state bits end holding the next state of H_A
    window = [unknown(c) for c in range(1 << alpha)]
    for c in REQUESTS:
        window[c] = 0
    for i in range(n):
        window[state[i]] = val[i]
    log = run(window, lo, hi)
    step = agree[0] and len(ends) == len(units) and not log and \
        all(window[state[i]] == val[nxt[i]] for i in range(n))
    # the device: on a window holding a state y of H_A (fresh variables), the registers and tapes with fresh
    # cells, the records against Definition 7.2; the bits of cnt and lim alternate in the order of the variables
    order = {}
    for i in range(w):
        order[addr[('d', 'cnt', i)]], order[addr[('d', 'lim', i)]] = 2 * i, 2 * i + 1
    window = [D.var((1 << 30) | order.get(c, 2 * w + c)) for c in range(1 << alpha)]
    for c in REQUESTS:
        window[c] = 0
    heads = dict(R=SymHead(D, lambda i: D.var(1 << 28 | i), 8), A=SymHead(D, lambda i: D.var(1 << 27 | i), 8),
                 C=SymHead(D, lambda i: D.var(1 << 26 | i), 8))
    y = [window[state[i]] for i in range(n)]
    cnt = [window[addr[('d', 'cnt', i)]] for i in range(w)]
    lim = [window[addr[('d', 'lim', i)]] for i in range(w)]
    dest = window[addr[('d', 'dest')]]
    word1 = lambda j: D.AND(y[mem_bit(j, 0, A)], _all_zero(D, [y[mem_bit(j, t, A)] for t in range(1, A)]))
    wr, rd, rwq = word1(io['c_wr']), word1(io['c_rd']), word1(io['c_rw'])
    eq = 1
    for i in range(w):
        eq = D.AND(eq, D.ite(cnt[i], lim[i], D.NOT(lim[i])))
    eot = D.AND(eq, dest)
    rin_cells = list(heads['R'].cells)
    a_cells, c_cells = list(heads['A'].cells), list(heads['C'].cells)
    log = run(window, hi, hd, heads)
    gread = D.AND(rd, D.NOT(eot))
    ca, cc = D.AND(wr, D.NOT(dest)), D.AND(wr, dest)
    ybit = lambda j, t: y[mem_bit(j, t, A)]
    exp = {}
    # (i) the low byte of R_out under the arm or the copy head, the head moving after each bit
    exp_a = [D.ite(ca, ybit(io['r_out'], 7 - kk), a_cells[kk]) for kk in range(8)] + [a_cells[8]]
    exp_c = [D.ite(cc, ybit(io['r_out'], 7 - kk), c_cells[kk]) for kk in range(8)] + [c_cells[8]]
    dev_ok = all(heads['A'].cells[i] == exp_a[i] for i in range(9)) and \
        all(heads['C'].cells[i] == exp_c[i] for i in range(9))
    dev_ok &= heads['A'].P == [D.NOT(ca)] + [0] * 7 + [ca] and heads['C'].P == [D.NOT(cc)] + [0] * 7 + [cc]
    for t in range(A):
        exp[mem_bit(io['r_out'], t, A)] = D.AND(ybit(io['r_out'], t), D.NOT(wr))
    # (ii) a read: eot after the rewind at cnt = lim, else the byte under the read head, sign extended
    for t in range(A):
        src = rin_cells[7 - min(t, 7)]
        exp[mem_bit(io['r_in'], t, A)] = D.ite(gread, src, ybit(io['r_in'], t))
    exp[mem_bit(io['c_eot'], 0, A)] = D.ite(rd, eot, ybit(io['c_eot'], 0))
    for t in range(1, A):
        exp[mem_bit(io['c_eot'], t, A)] = D.AND(ybit(io['c_eot'], t), D.NOT(rd))
    dev_ok &= heads['R'].P == [D.NOT(gread)] + [0] * 7 + [gread]
    dev_ok &= heads['R'].rewound == rwq
    # the counter, the limit and dest: the count incremented on a read, then the rewind
    carry, cnt1 = gread, []
    for i in range(w):
        cnt1.append(D.XOR(cnt[i], carry))
        carry = D.AND(carry, cnt[i])
    for i in range(w):
        dev_ok &= window[addr[('d', 'lim', i)]] == D.ite(rwq, cnt1[i], lim[i])
        dev_ok &= window[addr[('d', 'cnt', i)]] == D.AND(cnt1[i], D.NOT(rwq))
    dev_ok &= window[addr[('d', 'dest')]] == D.OR(dest, rwq)
    # (iv) the request words cleared; every other bit of the state unchanged
    for c in ('c_wr', 'c_rd', 'c_rw'):
        for t in range(A):
            exp[mem_bit(io[c], t, A)] = 0
    dev_ok &= all(window[state[i]] == exp.get(i, y[i]) for i in range(n))
    dev_ok &= {c for c, _ in log} <= {AR, AA, AC, RR}
    # the hand-over: booted <- booted and not h, then the arm and the copy head home and the hand-over, each h
    window = [unknown(c) for c in range(1 << alpha)]
    for c in REQUESTS:
        window[c] = 0
    hb, bb = window[state[A]], window[boot]
    pad_ok = all(recs[k] == (0, 0, 0, 0, 0, 0) for k in range(hd, len(recs) - HANDOVER_RECORDS))
    log = run(window, len(recs) - HANDOVER_RECORDS, len(recs))
    hand_ok = pad_ok and window[boot] == D.AND(bb, D.NOT(hb)) and log == [(RA, hb), (RC, hb), (HO, hb)]
    return dict(A=A, startup_records=lo, step_records=hi - lo, device_records=hd - hi,
                padding_records=len(recs) - HANDOVER_RECORDS - hd, handover_records=HANDOVER_RECORDS,
                startup_exact=startup, step_exact=step, device_exact=bool(dev_ok), handover_exact=bool(hand_ok),
                sha256_image=hashlib.sha256(S['image']).hexdigest(), nodes=len(D.node),
                seconds=round(time.time() - t0, 1))


def _all_zero(D, fs):
    acc = 1
    for f in fs:
        acc = D.AND(acc, D.NOT(f))
    return acc


# ---------------------------------------------------------------------------
# generations of the stored host
# ---------------------------------------------------------------------------

def stored_update_record(key, value):
    rec = json.load(open(STORED_RECORD)) if os.path.exists(STORED_RECORD) else {}
    rec[key] = value
    json.dump(rec, open(STORED_RECORD, 'w'), indent=1)


def census(tau):
    """The literal and repeat tokens of a recipe and the bytes each kind gives."""
    i = lit = rep = flit = frep = 0
    while tau[i]:
        t = tau[i]
        if t < 128:
            lit, flit, i = lit + 1, flit + t, i + 1 + t
        else:
            rep, frep, i = rep + 1, frep + 256 - t, i + 2
    return lit, rep, flit, frep


def passes(tau):
    """The steps of P* on a recipe, Proposition 6.13."""
    lit, rep, flit, frep = census(tau)
    return 5 * flit + 4 * frep + 7 * lit + 9 * rep + 7 + 1 + 6 * len(tau) + 2


def stored_key(name, A):
    return name if A == 8 else f'{name}_A{A}'


def run_stored(generations, A=8, K=3, extra_slots=5, extra_cells=64):
    """Generations of the stored host on the machine in C, against the reference run of P*."""
    S_ = build_stored(A)
    recs, tau, alpha = S_['recs'], S_['tau'], S_['alpha']
    G = len(recs)
    out, steps = SR.run_reference_a(SR.memory_image_a(SR.P_STAR, A), tau, A)
    assert out == S_['image'] + tau and steps == passes(tau)
    slots, L = G + extra_slots, 8 * len(tau) + extra_cells
    image, tape = bank_image(recs, slots, alpha), padded(bytes_to_bits(tau), L)
    M = Machine(K, slots, L, [image], [tape], [0] * (1 << alpha), 0, alpha)
    work = os.path.join(REPO, 'variants')
    inp, exe = os.path.join(work, f'.stored_host_{A}.bin'), os.path.join(work, f'.ring_run_{A}')
    write_machine(inp, M, image, tape)
    subprocess.run(['gcc', '-O3', '-march=native', '-o', exe, os.path.join(REPO, 'src', 'ring_run.c')], check=True)
    t0 = time.time()
    p = subprocess.run([exe, inp, str(generations)], capture_output=True, text=True)
    os.remove(inp); os.remove(exe)
    gens = [json.loads(l) for l in p.stdout.split('\n') if l.strip()]
    res = dict(A=A, K=K, S=slots, L=L, records=G, window_cells=S_['top'], record_bits=S_['b'],
               counter_bits=S_['w'], image_bytes=len(S_['image']), tau_bytes=len(tau), passes_expected=steps,
               steps_expected=(steps - 1) * slots + G, generations=gens, seconds=round(time.time() - t0, 1),
               sha256_image=hashlib.sha256(S_['image']).hexdigest(), sha256_tau=hashlib.sha256(tau).hexdigest())
    res['every_generation_exact'] = len(gens) == generations and all(
        g['steps'] == res['steps_expected'] and g['copies'] == min(g['generation'] + 1, K) for g in gens)
    stored_update_record(stored_key('run', A), res)
    return res


def stored_widths(widths):
    """The stored host of every word width: its records, window, counters, image and generation."""
    rows = []
    for A in widths:
        t0 = time.time()
        S_ = build_stored(A)
        G, tau = len(S_['recs']), S_['tau']
        lit, rep, flit, frep = census(tau)
        P = passes(tau)
        rows.append(dict(A=A, records=G, startup=S_['startup_records'], step=S_['n_host_records'],
                         device=S_['device_records'], padding=S_['padding'], handover=HANDOVER_RECORDS,
                         window_cells=S_['top'], alpha=S_['alpha'], record_bits=S_['b'], counter_bits=S_['w'],
                         image_bytes=len(S_['image']), tau_bytes=len(tau), literal_tokens=lit, repeat_tokens=rep,
                         passes=P, applications=(P - 1) * G + G, seconds=round(time.time() - t0, 1)))
        print(json.dumps(rows[-1]), flush=True)
    stored_update_record('widths', rows)
    return rows


def cmd_stored():
    args = sys.argv[1:]
    A = 8
    if '--width' in args:
        i = args.index('--width')
        A = int(args[i + 1])
        del args[i:i + 2]
    cmd = args[0] if args else 'build'
    if cmd == 'check':
        t0 = time.time()
        res = check_stored(int(args[1]) if len(args) > 1 else 40, A=A)
        res['seconds'] = round(time.time() - t0, 1)
        stored_update_record(stored_key('pass_check', A), res)
        print(json.dumps(res))
        sys.exit(0 if res['disagreements'] == 0 else 1)
    elif cmd == 'symbolic':
        res = symbolic_check(A)
        stored_update_record(stored_key('symbolic', A), res)
        print(json.dumps(res))
        sys.exit(0 if all(res[k] for k in ('startup_exact', 'step_exact', 'device_exact', 'handover_exact')) else 1)
    elif cmd == 'run':
        gens = int(args[1]) if len(args) > 1 else 3
        res = run_stored(gens, A)
        print(json.dumps(res, indent=1))
        sys.exit(0 if res['every_generation_exact'] else 1)
    elif cmd == 'widths':
        stored_widths([int(a) for a in args[1:]] or list(range(8, 13)))
    elif cmd == 'build':
        t0 = time.time()
        S_ = build_stored(A)
        print(json.dumps(dict(A=A, records=len(S_['recs']), host_records=S_['n_host_records'],
                              device_records=S_['device_records'], padding=S_['padding'],
                              window_cells=S_['top'], record_bits=S_['b'], counter_bits=S_['w'],
                              bank_bits=len(S_['image_bits']), image_bytes=len(S_['image']),
                              tau_bytes=len(S_['tau']), sha256_image=hashlib.sha256(S_['image']).hexdigest(),
                              seconds=round(time.time() - t0, 1))))


COMMANDS = {'organism': main_organism, 'net': main_net, 'stored': cmd_stored}


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]())