Prove self-reproduction by the dynamics for the stored host of every word width, with a sign-extending device read and the record count in closed form, check the stored hosts of widths 9 and 10 symbolically and on random states, check the extracted host family for widths 8 to 10, and remove the to-do note

README.md

@@ -604,7 +604,8 @@ and stored in the member with 4096 cells, runs the 27-instruction program on a
 recipe for its own records: it writes them into the idle bank, copies the recipe
 and hands control to the copy, so that it reproduces itself, weights included,
 by the dynamics alone; `src/stored_host_run.c` runs three generations of
-79,464,240,088 steps each. An organism of 133 records on the member with 64
+79,464,240,088 steps each. The paper proves that every member of the host family
+with wider words does the same in a larger window. An organism of 133 records on the member with 64
 cells does the same with a description code of its own, every generation of it
 proved in Rocq. Its robustness section gives the margin every orbit has
 against perturbation, a certificate of the leakage an orbit tolerates from the

paper/README.md

@@ -36,10 +36,10 @@ Each command is `python src/<file>.py <command>` and writes its record to `runs/
 | `paper.py family-gate` | `paper_runs_family_gate.json` | four of them on the netlist of sigma |
 | `paper.py c` | `paper_c_evaluator.json` | the host on the evaluator in C, `src/netlist_eval.c` |
 | `paper.py throughput` | `paper_throughput.json` | the rate of each evaluator |
-| `paper.py rocq` | `paper_rocq.json` | the Rocq development of `rocq/`, its assumptions, and the host H_8 extracted from it against the netlist sigma(N_host) denotes |
+| `paper.py rocq` | `paper_rocq.json` | the Rocq development of `rocq/`, its assumptions, and the host family extracted from it for A = 8, 9, 10 against sigma(N_host) and the generator |
 | `twohead.py organism` | `paper_twohead.json` | the translating organism on the two-head machine, three generations |
 | `twohead.py net` | `paper_twohead_net.json` | the netlist N_{G,L} against the machine for windows of 64 and 4096 cells, its file, the organism on it in C, and the netlist extracted from Rocq |
-| `twohead.py stored` | `paper_stored_host.json` | the host compiled into records of the two-head machine: one pass against the host's step and its device, the startup and step records on decision diagrams over the signals of N_host (`stored symbolic`), and three generations in C |
+| `twohead.py stored` | `paper_stored_host.json` | the host compiled into records of the two-head machine: one pass against the host's step and its device, the startup and step records on decision diagrams over the signals of the host (`stored symbolic`), and three generations in C; `--width A` checks H_A in place of H_8, and `stored widths` tabulates A = 8 to 12 |
 | `noise.py host` | `paper_noise_*.json` | the margin, the profile bound, read noise, the deviation curve, weight error with leakage, the active-input counts of the orbit certificate |
 | `noise.py amplified` | `paper_redundant_*.json` | the amplified host N_3: one step on replicated states, the margin 3/2, exact self-reproduction in C, the run under noise, the deviation curve and its bound by layer, the failure rate of the state read by majority and the restoration bound, computed by `src/restore_bound.c` |
 | `independent.py` | `independent_*.json` | code written from the paper's definitions alone: H_A rebuilt from Construction 3.8 for A = 3 to 12, Lev(N_host) from sigma and the measurements of Section 6.1 and Appendix A with the noise simulator `src/nsim.c` |

paper/runs/paper_rocq.json

@@ -1,7 +1,7 @@
 {
  "rocq": "The Rocq Prover, version 9.1.1",
  "files": 30,
- "build_seconds": 303.5,
+ "build_seconds": 251.8,
  "theorems": {
   "PhysMain.netlist_step": "closed",
   "PhysMain.netlist_step64": "closed",
@@ -24,10 +24,29 @@
  "extraction_identical": true,
  "lines": 5093,
  "host_extraction": {
-  "A": 8,
-  "units": 17598,
-  "identical": true,
-  "sha256_sigma": "2263144948d68cafbf1616a6c0bd74e98cb597c1a6d5b1512d65d3aff574f17a",
-  "sha256_rocq": "2263144948d68cafbf1616a6c0bd74e98cb597c1a6d5b1512d65d3aff574f17a"
+  "members": [
+   {
+    "A": 8,
+    "units": 17598,
+    "identical": true,
+    "sha256_generator": "2263144948d68cafbf1616a6c0bd74e98cb597c1a6d5b1512d65d3aff574f17a",
+    "sha256_rocq": "2263144948d68cafbf1616a6c0bd74e98cb597c1a6d5b1512d65d3aff574f17a"
+   },
+   {
+    "A": 9,
+    "units": 39130,
+    "identical": true,
+    "sha256_generator": "0ff74a207964d69eaf8857eb39ca93a085ee1f59d680edd7a81dd9906a82e916",
+    "sha256_rocq": "0ff74a207964d69eaf8857eb39ca93a085ee1f59d680edd7a81dd9906a82e916"
+   },
+   {
+    "A": 10,
+    "units": 86263,
+    "identical": true,
+    "sha256_generator": "9465daed0832b5942d120e685597e4db16a155dbd12adccb1b0ea18852a4a8a4",
+    "sha256_rocq": "9465daed0832b5942d120e685597e4db16a155dbd12adccb1b0ea18852a4a8a4"
+   }
+  ],
+  "identical": true
  }
 }

paper/runs/paper_stored_host.json

@@ -65,15 +65,147 @@
   "disagreements": 0,
   "records": 36074,
   "window_cells": 2896,
-  "seconds": 131.8
+  "seconds": 75.0
  },
  "symbolic": {
+  "A": 8,
   "startup_records": 2099,
   "step_records": 33568,
   "startup_exact": true,
   "step_exact": true,
   "sha256_image": "7a769aa264a89860149962d7e98f8b2a5cb34ceb7778e88bcbffdccdc0996154",
-  "nodes": 1435999,
-  "seconds": 3.6
- }
+  "nodes": 79870,
+  "seconds": 0.9
+ },
+ "symbolic_A9": {
+  "A": 9,
+  "startup_records": 4660,
+  "step_records": 75366,
+  "startup_exact": true,
+  "step_exact": true,
+  "sha256_image": "40affa80c17e09eddf8267b377ca48fb19ce1616366bf0f2020f0f574fb19aee",
+  "nodes": 177802,
+  "seconds": 1.7
+ },
+ "symbolic_A10": {
+  "A": 10,
+  "startup_records": 10297,
+  "step_records": 167351,
+  "startup_exact": true,
+  "step_exact": true,
+  "sha256_image": "a2e7bd1326e149fef968b232b35f4d9496022bbc706f59330994fbb8410498e0",
+  "nodes": 392233,
+  "seconds": 5.8
+ },
+ "pass_check_A9": {
+  "trials": 300,
+  "disagreements": 0,
+  "records": 80448,
+  "window_cells": 6228,
+  "seconds": 204.6
+ },
+ "pass_check_A10": {
+  "trials": 100,
+  "disagreements": 0,
+  "records": 178100,
+  "window_cells": 13404,
+  "seconds": 156.2
+ },
+ "widths": [
+  {
+   "A": 8,
+   "records": 36074,
+   "startup": 2099,
+   "step": 33568,
+   "device": 402,
+   "handover": 5,
+   "window_cells": 2896,
+   "alpha": 12,
+   "record_bits": 44,
+   "counter_bits": 20,
+   "image_bytes": 198407,
+   "tau_bytes": 199971,
+   "literal_tokens": 1563,
+   "repeat_tokens": 0,
+   "passes": 2202812,
+   "applications": 79464240088,
+   "seconds": 0.4
+  },
+  {
+   "A": 9,
+   "records": 80448,
+   "startup": 4660,
+   "step": 75366,
+   "device": 413,
+   "handover": 9,
+   "window_cells": 6228,
+   "alpha": 13,
+   "record_bits": 47,
+   "counter_bits": 20,
+   "image_bytes": 472632,
+   "tau_bytes": 476355,
+   "literal_tokens": 3722,
+   "repeat_tokens": 0,
+   "passes": 5247354,
+   "applications": 422139134592,
+   "seconds": 1.0
+  },
+  {
+   "A": 10,
+   "records": 178100,
+   "startup": 10297,
+   "step": 167351,
+   "device": 448,
+   "handover": 4,
+   "window_cells": 13404,
+   "alpha": 14,
+   "record_bits": 50,
+   "counter_bits": 22,
+   "image_bytes": 1113125,
+   "tau_bytes": 1121891,
+   "literal_tokens": 8765,
+   "repeat_tokens": 0,
+   "passes": 12358336,
+   "applications": 2201019641600,
+   "seconds": 3.7
+  },
+  {
+   "A": 11,
+   "records": 391216,
+   "startup": 22588,
+   "step": 368148,
+   "device": 471,
+   "handover": 9,
+   "window_cells": 28770,
+   "alpha": 15,
+   "record_bits": 53,
+   "counter_bits": 23,
+   "image_bytes": 2591806,
+   "tau_bytes": 2612215,
+   "literal_tokens": 20408,
+   "repeat_tokens": 0,
+   "passes": 28775186,
+   "applications": 11257313166176,
+   "seconds": 9.9
+  },
+  {
+   "A": 12,
+   "records": 853167,
+   "startup": 49215,
+   "step": 803454,
+   "device": 494,
+   "handover": 4,
+   "window_cells": 61544,
+   "alpha": 16,
+   "record_bits": 56,
+   "counter_bits": 24,
+   "image_bytes": 5972169,
+   "tau_bytes": 6019191,
+   "literal_tokens": 47025,
+   "repeat_tokens": 2,
+   "passes": 66305186,
+   "applications": 56569396624062,
+   "seconds": 26.0
+  }
+ ]
 }

paper/universal_construction_ternary.pdf

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:c973871985a763cf000c4cfa9e8126aa37eb0efb94c99261d4289b10a39e1b10
-size 327298
+oid sha256:07d0ca48862fbcbbff532d926d57af98543fb0c3acf837dc3ecd5b8e38f6f0be
+size 327765

paper/universal_construction_ternary.tex

@@ -79,8 +79,9 @@ step. Stored in it as $36{,}074$ records of two inputs, the SUBLEQ computer runs
 the second program on a description of its own records: it writes them into the
 idle bank, copies the description and hands control to the copy, which does the
 same, so the fixed network rebuilds, exactly and in every generation, the weights
-of the stored network that computes, with no map outside it; a constructor of
-$133$ records does the same with every step proved in Rocq. Because every
+of the stored network that computes, with no map outside it, and so does every
+member of the family with wider words; a constructor of $133$ records does the same
+with every step proved in Rocq. Because every
 pre-activation is an integer, every orbit survives perturbations below $1/2$, and
 a bound computed from the pre-activation profile is within $20\%$ of the measured
 failure rate under Gaussian read noise. Replacing each unit by $r$ copies that read
@@ -106,9 +107,7 @@ copies the description, produces a copy of itself together with a copy of the
 description~\cite{vonNeumann1966}. The self-reproducing automata that followed
 \cite{Arbib1966,Codd1968,Langton1984,Pesavento1995,PerrierSipperZahnd1996},
 surveyed in~\cite{Sipper1998}, reproduce configurations of a cellular space
-under a fixed transition rule. Neural networks have been trained to output
-approximations of their own parameters
-\cite{ChangLipson2018,Gabor2022,RandazzoVersariMordvintsev2021,ShvartzmanRam2024}.
+under a fixed transition rule.
 
 This paper makes the parameters of a threshold network the object of exact
 reproduction. The networks have weights in $\Tern$ and integer thresholds and
@@ -159,13 +158,12 @@ networks $N^\alpha_{G,L}$ whose state holds a stored network as records in two
 banks, with two tapes and three heads, each step evaluating one record, proved in
 Rocq to compute the step of this two-head machine from every state for every
 window of $2^\alpha$ cells and every $G$ and $L$ (Theorem~\ref{thm:physnet}).
-Stored in it as records of two inputs, the host running $P^\ast$ builds every
-image of its size into the idle bank and hands control to it, and started on a
-recipe for its own records it reproduces in every generation, weights included,
-a generation of $G$ records taking at most $\tfrac{25}{16}(8+3\alpha)G^2+29G$
-steps (Theorems~\ref{thm:storedconstruct} and~\ref{thm:storedrep}); three
-generations of the host, $36{,}074$ records and $7.9\times10^{10}$ steps each,
-were run. A constructor of $133$ records with a description code of its own does
+Stored in it as records of two inputs, the host $H_A$ of every word width $A\ge8$
+running $P^\ast$ builds every image of its size into the idle bank and hands
+control to it, and started on a recipe for its own records reproduces in every
+generation, weights included, in $\Theta(A^34^A)$ steps
+(Theorems~\ref{thm:storedconstruct} to~\ref{thm:widths}); three generations of
+$H_8$, $36{,}074$ records and $7.9\times10^{10}$ steps each, were run. A constructor of $133$ records with a description code of its own does
 the same in the member with $64$ cells, every step of it proved in Rocq
 (Section~\ref{sec:organism}).
 \item \emph{Robustness.} Every orbit survives perturbations below $1/2$ per
@@ -177,12 +175,10 @@ copies of its inputs, Pierce's interwoven redundancy~\cite{Pierce1965} with
 threshold units, multiplies every margin by $r$: the probability of leaving an
 orbit within $T$ steps under read noise of deviation $s$ is at most
 $T\,rM\erfc(r/2\sqrt2 s)$, so any noise level is survived with redundancy
-$O(s\sqrt{\log(TM/\delta)})$, and $O(s_{\mathrm w}^2\log(TM/\delta))$ when the
-noise sits on every synapse (Theorem~\ref{thm:amplify},
-Corollary~\ref{cor:synapse}). The state read by majority fails only when two wrong
-copies meet, a second-order event whose bound certifies the complete run of the
-threefold host where the first-order bound exceeds one
-(Proposition~\ref{prop:restore}).
+$O(s\sqrt{\log(TM/\delta)})$, and $O(s_{\mathrm w}^2\log(TM/\delta))$ with noise on
+every synapse (Theorem~\ref{thm:amplify}, Corollary~\ref{cor:synapse}); a
+second-order bound certifies the complete run of the threefold host where the
+first-order bound exceeds one (Proposition~\ref{prop:restore}).
 \end{enumerate}
 
 % =============================================================================
@@ -308,13 +304,10 @@ $\omega$, we write $\Out(x_0,\tau)=\omega$.
 \end{definition}
 
 \begin{remark}[Device realization]\label{rem:devices}
-In the host the registers and the request and status bits are memory-mapped
-cells of the SUBLEQ memory at the addresses of Table~\ref{tab:device}, and
-$c_{\mathrm{halt}}$ is a state bit that latches the predicate $p=255$ on the
-program counter of the state produced by the step, so that a halted state is a
-fixed point. A request fires on the value held by its cell, so the device is a
-function of the machine state, and the transition map $F$ treats the device
-cells as ordinary memory.
+In the host the registers and the request and status bits are memory cells at
+the addresses of Table~\ref{tab:device}, and $c_{\mathrm{halt}}$ is a state bit
+latching $p=255$ for the state the step produces, so that a halted state is a fixed
+point; $F$ treats the device cells as ordinary memory.
 \end{remark}
 
 \begin{table}[ht]
@@ -426,7 +419,8 @@ bits, is at most $0$, and $p\leftarrow p+3$ otherwise~\cite{MavaddatParhami1988}
 Indices are taken modulo $S$, and the machine halts when $p=S-1$. The device
 cells of Definition~\ref{def:transducer} are the seven top words, in the order of
 Table~\ref{tab:device}; a request fires on the value $1$, a read loads a tape byte
-into $R_{\mathrm{in}}$, and an emission appends the low byte of $R_{\mathrm{out}}$.
+into $R_{\mathrm{in}}$, its sign bit copied into the bits above the eighth, and an
+emission appends the low byte of $R_{\mathrm{out}}$.
 We write $\mathrm{SUBLEQ}_A$ for this machine. The host is $A=8$: $256$ words of
 one byte.
 \end{definition}
@@ -628,14 +622,13 @@ $\mathrm{SUBLEQ}_A$ with the halt latch, from every state and for every $A\ge3$,
 is proved in Rocq from a definition of $H_A$ block by block in the order of
 Table~\ref{tab:blocks}: every unit is given its value in terms of the state,
 the carries through the recurrence of Lemma~\ref{lem:sub}, and induction over the
-units shows that the netlist computes these values. Extracted for $A=8$, the
-definition gives the netlist that $\sigma(\Nhost)$ denotes, unit for unit.
+units shows that the netlist computes these values. Extracted for $A=8$ to $10$,
+the definition gives the netlist that $\sigma(\Nhost)$ denotes and those of the
+generator, unit for unit.
 \end{proof}
 
 \begin{remark}[Depth]\label{rem:fold}
-A ripple-carry datapath makes the depth grow linearly with $A$; for $A=8$ it has
-depth $33$ and a levelization of $87{,}080$ rows, $79\%$ of them identity units,
-against $58\%$ here. Writing every fetch conjunction $FA_{o,t,j}$, every read
+Writing every fetch conjunction $FA_{o,t,j}$, every read
 conjunction $RX_{t,j}$, $RY_{t,j}$ and every write enable $W_j$ as a single unit
 that reads the bits of its address directly, of fan-in $A+1$, removes the decode
 lines of $a$ and $b$ and one level each from the fetch and from the operand reads,
@@ -643,8 +636,7 @@ so the step has depth $11$ for every $A$. For $A=8$ the folded netlist has
 $17{,}086$ units and $120{,}508$ edges, against $17{,}598$ and $51{,}132$, and for
 every $A$ from $3$ to $12$ one step of it agreed with $\mathrm{SUBLEQ}_A$ on
 $2^{16}$ uniformly random full states for $A\le10$ and on $2^{15}$ and $2^{14}$
-for $A=11$ and $12$. We do not know the least depth of a ternary SUBLEQ step; the
-constructions below use $H_8$.
+for $A=11$ and $12$. The least depth of a ternary SUBLEQ step is open.
 \end{remark}
 
 % =============================================================================
@@ -756,11 +748,7 @@ the output of an instance with host $\Nhost$ and memory image $m_P$. Writing $L$
 and $R$ for the numbers of literal and repeat tokens of $r$ and
 $f_{\mathrm{lit}}$, $f_{\mathrm{rep}}$ for the numbers of bytes each kind
 contributes to $\delta(r)$, the run takes exactly
-\[
-  5f_{\mathrm{lit}}+4f_{\mathrm{rep}}+7L+9R+8
-\]
-steps, hence at most $5|\delta(r)|+9\bigl\lfloor(|r|-1)/2\bigr\rfloor+8$ and at
-least $4|\delta(r)|+8$.
+$5f_{\mathrm{lit}}+4f_{\mathrm{rep}}+7L+9R+8$ steps.
 \end{theorem}
 
 \begin{proof}
@@ -792,9 +780,7 @@ length $T$ then executes $6$, $T$ passes of $9$ to $12$ of which the first $T-1$
 also execute $13$, and $14$: $5T+7$ steps. A repeat token of run length
 $\ell=256-T$ executes $7$, $8$ and $15$, $\ell$ passes of $16$ to $18$ of which the
 first $\ell-1$ also execute $19$, and $14$: $4\ell+9$ steps. The end token executes
-$0$ to $5$, $7$ and $20$: eight steps. For the bounds,
-$f_{\mathrm{lit}}+f_{\mathrm{rep}}=|\delta(r)|$, and every token occupies at least
-two bytes of $r$, so $7L+9R\le9(L+R)\le9\lfloor(|r|-1)/2\rfloor$.
+$0$ to $5$, $7$ and $20$: eight steps.
 \end{proof}
 
 \begin{corollary}[Self-description]\label{cor:selfdesc}
@@ -841,6 +827,48 @@ elsewhere, and let
 \]
 \end{construction}
 
+\begin{table}[t]\centering\small
+\begin{tabular}{@{}rlllll@{}}
+\toprule
+$k$ & addr & $A$ & $B$ & $C$ & effect\\
+\midrule
+0 & \cell{0x00} & \cell{T2} & \cell{T2} & \cell{0x03} & $M[\cell{T2}]\leftarrow 0$\\
+1 & \cell{0x03} & \cell{T1} & \cell{T1} & \cell{0x06} & $M[\cell{T1}]\leftarrow 0$\\
+2 & \cell{0x06} & \cell{NEG1} & $c_{\mathrm{rd}}$ & \cell{0x09} & read request\\
+3 & \cell{0x09} & $R_{\mathrm{in}}$ & \cell{T1} & \cell{0x0C} & $M[\cell{T1}]\leftarrow\nu(T)$\\
+4 & \cell{0x0C} & \cell{T1} & \cell{T2} & \cell{0x0F} & $M[\cell{T2}]\leftarrow T$\\
+5 & \cell{0x0F} & \cell{Z} & \cell{T2} & \cell{0x15} & branch if $T=0$ or $T\ge128$\\
+6 & \cell{0x12} & \cell{Z} & \cell{Z} & \cell{0x1B} & goto \textsc{lit}\\
+7 & \cell{0x15} & \cell{Z} & \cell{T1} & \cell{0x3C} & branch to \textsc{end} if $\nu(T)\le0$\\
+8 & \cell{0x18} & \cell{Z} & \cell{Z} & \cell{0x2D} & goto \textsc{rep}\\
+9 & \cell{0x1B} & \cell{NEG1} & $c_{\mathrm{rd}}$ & \cell{0x1E} & \textsc{lit}: read request\\
+10 & \cell{0x1E} & $R_{\mathrm{in}}$ & $R_{\mathrm{out}}$ & \cell{0x21} & $M[R_{\mathrm{out}}]\leftarrow\nu(b)$\\
+11 & \cell{0x21} & \cell{NEG1} & $c_{\mathrm{wr}}$ & \cell{0x24} & write request\\
+12 & \cell{0x24} & \cell{ONE} & \cell{T2} & \cell{0x2A} & $M[\cell{T2}]\mathrel{-}=1$; done $\to$ 14\\
+13 & \cell{0x27} & \cell{Z} & \cell{Z} & \cell{0x1B} & next literal byte\\
+14 & \cell{0x2A} & \cell{Z} & \cell{Z} & \cell{0x00} & goto 0\\
+15 & \cell{0x2D} & \cell{NEG1} & $c_{\mathrm{rd}}$ & \cell{0x30} & \textsc{rep}: read request\\
+16 & \cell{0x30} & $R_{\mathrm{in}}$ & $R_{\mathrm{out}}$ & \cell{0x33} & $M[R_{\mathrm{out}}]\leftarrow\nu(b)$\\
+17 & \cell{0x33} & \cell{NEG1} & $c_{\mathrm{wr}}$ & \cell{0x36} & write request\\
+18 & \cell{0x36} & \cell{ONE} & \cell{T1} & \cell{0x2A} & $M[\cell{T1}]\mathrel{-}=1$; done $\to$ 14\\
+19 & \cell{0x39} & \cell{Z} & \cell{Z} & \cell{0x30} & emit again\\
+20 ($P$) & \cell{0x3C} & \cell{Z} & \cell{Z} & \cell{0xFF} & \textsc{end}: halt\\
+20 ($P^\ast$) & \cell{0x3C} & \cell{NEG1} & $c_{\mathrm{rw}}$ & \cell{0x3F} & \textsc{r}: rewind request\\
+21 & \cell{0x3F} & \cell{NEG1} & $c_{\mathrm{rd}}$ & \cell{0x42} & \textsc{b}: read request\\
+22 & \cell{0x42} & $c_{\mathrm{eot}}$ & \cell{EOK} & \cell{0xFF} & $M[\cell{EOK}]\leftarrow1-c_{\mathrm{eot}}$; halt if $\le0$\\
+23 & \cell{0x45} & $R_{\mathrm{in}}$ & \cell{Z} & \cell{0x48} & $M[\cell{Z}]\leftarrow\nu(b)$\\
+24 & \cell{0x48} & \cell{Z} & $R_{\mathrm{out}}$ & \cell{0x4B} & $M[R_{\mathrm{out}}]\leftarrow b$\\
+25 & \cell{0x4B} & \cell{NEG1} & $c_{\mathrm{wr}}$ & \cell{0x4E} & write request\\
+26 & \cell{0x4E} & \cell{Z} & \cell{Z} & \cell{0x3F} & $M[\cell{Z}]\leftarrow0$; goto \textsc{b}\\
+\bottomrule
+\end{tabular}
+\caption{The constructor $P$ of Construction~\ref{con:P}, instructions $0$ to $20$ at
+\cell{0x00}--\cell{0x3E}, and the self-reproducing program $P^\ast$ of
+Construction~\ref{con:selfrep}, instructions $0$ to $19$ of $P$ followed by $20$ to $26$ at
+\cell{0x3C}--\cell{0x50}. An instruction $A\;B\;C$ assigns $M[B]\leftarrow M[B]-M[A]$ and
+branches to $C$ when the result is at most $0$; $b$ is the tape byte just read.}
+\label{tab:P}\label{tab:Pstar}\end{table}
+
 \begin{theorem}[Exact self-reproduction]\label{thm:selfrep}
 For every recipe $\tau$ the instance $(\Nhost,m^\ast,\tau)$ halts and
 $\Out(\Nhost,m^\ast,\tau)=\delta(\tau)\cat\tau$; its run reads no byte at
@@ -901,6 +929,16 @@ $794{,}960$ steps in phase~(A), one in phase~(R) and $869{,}978$ in phase~(B),
 $1{,}664{,}939$ in all.
 \end{remark}
 
+\begin{remark}[Wider words]\label{rem:wider}
+For $A\ge8$ let $m^\ast_A$ hold $P^\ast$ in $2^A$ words, the cells $\cell{0xF0}$ to
+$\cell{0xFF}$ and the addresses naming them moved to the top sixteen words, with
+$M[\cell{ONE}]=M[\cell{EOK}]=1$ and $M[\cell{NEG1}]=2^A-1$, so that $m^\ast_8=m^\ast$.
+Theorem~\ref{thm:selfrep} and Proposition~\ref{prop:steps} hold for $H_A$ and
+$m^\ast_A$ with the same proofs: a byte read with its sign bit copied has the same
+value in two's complement on $A$ bits as on eight, and the low byte of
+$R_{\mathrm{out}}$ is again $\nu(b)$ or $b$, since $256$ divides $2^A$.
+\end{remark}
+
 
 % =============================================================================
 \section{Robustness under perturbation}\label{sec:robust}
@@ -989,11 +1027,6 @@ evaluation whose input is unperturbed and whose perturbation satisfies
 $|e|\ge\tfrac12$. There are $TM$ evaluations up to time $T$.
 \end{proof}
 
-A row can change its output only when its noise crosses the comparator on the
-side away from its pre-activation, with a probability that falls rapidly with the
-distance from the comparator. The following bound counts each row by that
-probability.
-
 \begin{proposition}[Profile bound]\label{prop:profile}
 Let the perturbations be independent centred Gaussians of standard deviation
 $s$, let $(x_t)$ be the orbit of $F$ from $x_0$, and for $t\ge0$ and each row $i$
@@ -1034,11 +1067,9 @@ without leakage and for $\gamma<6.09\times10^{-5}$ with exact weights. Along the
 first $10{,}000$ steps of the self-describing instance $K^\ast=8$ and
 $A^\ast=349$, and (ii) certifies $\gamma<1.43\times10^{-3}$ and
 $\varepsilon<1/16$, each alone; along the self-reproducing run $A^\ast=441$,
-certifying $\gamma<1.13\times10^{-3}$. With every programmed weight perturbed
-uniformly in $[-\varepsilon,\varepsilon]$ or every zero entry in
-$[-\gamma,\gamma]$, the first $10{,}000$ steps stayed exact up to
-$\gamma=3.9\times10^{-3}$ and up to $\varepsilon=1/16$, and deviated at
-$\gamma=1.56\times10^{-2}$ and at $\varepsilon=1/4$.
+certifying $\gamma<1.13\times10^{-3}$. Under uniform random errors the first
+$10{,}000$ steps stayed exact up to $\gamma=3.9\times10^{-3}$ and up to
+$\varepsilon=1/16$.
 
 For Gaussian read noise of deviation $s=0.05$, $p=1.52\times10^{-23}$, and over the
 $T=1{,}664{,}939$ steps of the self-reproducing run, $TM=6.99\times10^{10}$,
@@ -1272,9 +1303,7 @@ copies, which is their common value, and writes every copy, so the run of $N_r$
 from $\rho_r(x_0(m))$ visits the replications of the states $\Nhost$ visits from
 $x_0(m)$ on the same tape and emits the same bytes. The proofs of
 Theorems~\ref{thm:univ} and~\ref{thm:selfrep} use the transducer alone, so they
-hold with $N_r$ in place of $\Nhost$. The census of $\tau^\ast_3$ is $L=23{,}892$,
-$R=1{,}581$, $f_{\mathrm{lit}}=2{,}995{,}056$ and $f_{\mathrm{rep}}=126{,}755$, so
-phase~(A) takes $15{,}663{,}780$ steps and phase~(B) $18{,}132{,}668$.
+hold with $N_r$ in place of $\Nhost$.
 \end{proof}
 
 One step of $N_3$ agreed with Definition~\ref{def:subleq} on $65{,}536$
@@ -1494,12 +1523,8 @@ $i+1\bmod N$ or bit $i$ of the bank after the arm's write, as cell $5$ after the
 write requests; the cell under the arm after the write is a multiplexer of $v$
 and the old cell on the decode line of $2$. The tapes are alike, with cells $4$
 and $6$ and the decode line of $3$. Counting the units and edges of the blocks
-gives the sizes. The depth of a unit depends only on its block: the record and
-the cells under the heads are selected at depth $2$, the decode lines lie at
-depth $3$, the operands at $5$, the products at $6$, the tests $p\ge c$ at $7$
-and $v$ at $9$, the written window cells, the requests among them, at $11$, the
-next bank bits at $14$, the signals that turn the tapes at $13$ and the next tape
-bits at $15$. That the next state is the encoding of the next state of $x$, for
+gives the sizes. The depth of a unit depends only on its block, from $2$ for the
+selected record to $15$ for the next tape bits. That the next state is the encoding of the next state of $x$, for
 all $\alpha$, $G$, $L$ and $x$, is proved in Rocq with the number of units and the
 weights: every unit is given a value in terms of $x$ and fires to it on the values
 of the units it reads, and induction over the units shows that the netlist
@@ -1507,11 +1532,8 @@ computes these values.
 \end{proof}
 
 \begin{remark}[Corroboration]\label{rem:physcheck}
-For $\alpha=6$, $G=133$ and $L=2930$, the member that Section~\ref{sec:organism}
-uses, $N^6_{G,L}$ has $45{,}891$ units, $99{,}602$ edges and $12{,}837$ state bits;
-for $\alpha=12$, $G=36{,}074$ and $L=1{,}599{,}768$, the member that
-Section~\ref{sec:storedhost} uses, it has $22{,}329{,}613$ units,
-$47{,}964{,}818$ edges and $6{,}378{,}141$ state bits. For $N^6_{133,2930}$ and
+The member $N^6_{133,2930}$ of Section~\ref{sec:organism} has $45{,}891$ units and
+the member of Section~\ref{sec:storedhost} $22{,}329{,}613$. For $N^6_{133,2930}$ and
 $N^{12}_{5,40}$ the generator's file is byte for byte the netlist extracted from
 the Rocq definition, and three generations of the organism, $2{,}762{,}676$ steps,
 were run on $N^6_{133,2930}$ in C beside a transcription of
@@ -1524,10 +1546,10 @@ Definition~\ref{def:twohead}, the full state compared after every step.
 
 Inside the two-head machine the instantiation step of Section~\ref{sec:selfrep}
 is a write into the idle bank followed by a change of $\kappa$. This section
-stores the host as a network of two-input records in a bank of $T^{12}_{G,L}$,
-whose window of $4096$ cells holds the host's $2057$ state bits, with a device
-that writes the bytes the host emits under the arm until the tape is rewound and
-under the copy head after it. Run on a recipe for its own records, $P^\ast$ then
+stores the host, and every member of its family with wider words, as a network of
+two-input records in a bank of a two-head machine whose window holds its state
+bits, $4096$ cells for $\Nhost$, with a device that writes the bytes the host emits
+under the arm until the tape is rewound and under the copy head after it. Run on a recipe for its own records, $P^\ast$ then
 writes the host into the idle bank, copies the recipe and hands control to the
 copy (Figure~\ref{fig:generation}).
 
@@ -1549,10 +1571,9 @@ its predecessors on the current state, a state bit being unchanged until the
 record of its next value, which follows its last reader.
 \end{proof}
 
-Gate-level logic simulation engines evaluate one stored gate per step from
-operand memory and rank-order the gates so that one pass
-suffices~\cite{Denneau1982}, and Lemma~\ref{lem:feedback} is the fixed-order
-sequential schedule of automata networks~\cite{RiosWilsonTheyssier2024c}.
+Lemma~\ref{lem:feedback} is the rank-ordered schedule of gate-level simulation
+engines~\cite{Denneau1982} and the fixed-order sequential schedule of automata
+networks~\cite{RiosWilsonTheyssier2024c}.
 
 \begin{lemma}[Compilation]\label{cor:compile}
 A ternary threshold unit $\Hv(\sum_{i\in P}x_i-\sum_{i\in N}x_i+b)$ is $1$
@@ -1576,55 +1597,54 @@ others are, and its base cases are the chains and the constants.
 \end{proof}
 
 \begin{construction}[The stored host]\label{con:stored}
-Let $\alpha=12$. The window holds, after the eight cells of
+Let $A\ge8$ and $w\ge20$. The window holds, after the eight cells of
 Definition~\ref{def:twohead}, a cell $\mathrm{booted}$ at $8$, a counter
-$\mathrm{cnt}$ of $20$ bits at $9$ to $28$, least significant first, a cell
-$\mathrm{dest}$ at $29$, a limit $\mathrm{lim}$ of $20$ bits at $30$ to $49$, the
-$2057$ state bits of $\Nhost$ at $50$ to $2106$ in the order of
-Construction~\ref{con:host}, and temporaries from $2107$ on. The stored host $S$
-lists the following $36{,}074$ records.
+$\mathrm{cnt}$ of $w$ bits from $9$ on, least significant first, a cell
+$\mathrm{dest}$, a limit $\mathrm{lim}$ of $w$ bits, the $n=A+1+A2^A$ state bits of
+$H_A$ in the order of Construction~\ref{con:host}, and temporaries. The stored host
+$S_{A,w}$ lists the following records.
 \begin{enumerate}[label=(\alph*),leftmargin=2em]
-\item \emph{Startup}, $2099$ records: for each memory bit $c$,
-$c\leftarrow c\vee\neg\mathrm{booted}$ if its value in $m^\ast$ is $1$ and
+\item \emph{Startup}, $A2^A+A+2w+3$ records: for each memory bit $c$,
+$c\leftarrow c\vee\neg\mathrm{booted}$ if its value in $m^\ast_A$ is $1$ and
 $c\leftarrow c\wedge\mathrm{booted}$ if it is $0$; then
 $c\leftarrow c\wedge\mathrm{booted}$ for the bits of the counter, the halt bit and
 the bits of $\mathrm{cnt}$, $\mathrm{lim}$ and $\mathrm{dest}$; then
 $\mathrm{booted}\leftarrow1$.
-\item \emph{Step}, $33{,}568$ records: the units of $\Nhost$ compiled by
-Lemma~\ref{cor:compile}, in two stages. The first evaluates every unit that a
-next value depends on, other than the units of the next values and the units read
-by a single unit, each after its predecessors. The second takes the counter bits,
-the halt bit and the memory bits in this order, and evaluates for each the unit of
-its next value, with the units read by it alone just before it, its last record
-writing the bit.
-\item \emph{Device}, $402$ records: the device of Definition~\ref{def:ring} on the
-state that~(b) leaves.
-\item \emph{Hand-over}, five records: $\mathrm{booted}\leftarrow
-\mathrm{booted}\wedge\neg h$, where $h$ is the halt bit; a record with both
-weights $0$ that writes $0$ into the sink, which makes $S$ a whole number of bytes;
-and $\kappa\leftarrow\kappa\oplus h$ in three records.
+\item \emph{Step}: the units of $H_A$ compiled by Lemma~\ref{cor:compile}, in two
+stages. The first evaluates every unit that a next value depends on, other than the
+units of the next values and the units read by a single unit, each after its
+predecessors. The second takes the counter bits, the halt bit and the memory bits
+in this order, and evaluates for each the unit of its next value, with the units
+read by it alone just before it, its last record writing the bit.
+\item \emph{Device}, $11A+12w+74$ records: the device of Definition~\ref{def:ring}
+on the state that~(b) leaves.
+\item \emph{Hand-over}: $\mathrm{booted}\leftarrow\mathrm{booted}\wedge\neg h$, where
+$h$ is the halt bit; the fewest records with both weights $0$ writing $0$ into the
+sink, at most seven, that make the image a whole number of bytes; and
+$\kappa\leftarrow\kappa\oplus h$ in three records.
 \end{enumerate}
 Temporaries whose live intervals, from the first write to the last read, are
-disjoint share a cell, $789$ cells in all, so $S$ uses the window cells $0$ to
-$2895$. The image of $S$, its records in order, has $1{,}587{,}256$ bits, read as
-$198{,}407$ bytes most significant bit first, and $\tau_S=\describe(S)$ has
-$199{,}971$ bytes.
+disjoint share a cell, and the window is the least $2^\alpha$ that holds the cells
+used. The host $S=S_{8,20}$ has its state bits at $50$ to $2106$ and $789$ cells of
+temporaries after them, so $\alpha=12$; its image, its records in order, has
+$1{,}587{,}256$ bits, read as $198{,}407$ bytes most significant bit first, and
+$\tau_S=\describe(S)$ has $199{,}971$ bytes.
 \end{construction}
 
 \begin{definition}[The device of the stored host]\label{def:ring}
-The device acts on the state $y$ of the host after a step, the registers
+The device acts on the state $y$ of $H_A$ after a step, the registers
 $\mathrm{cnt}$, $\mathrm{lim}$ and $\mathrm{dest}$, the read tape, the idle bank
 and the copy tape, each request firing on the value $1$:
 \begin{enumerate}[label=(\roman*)]
-\item if $y_{c_{\mathrm{wr}}}=1$, the eight bits of $y_{R_{\mathrm{out}}}$, most
+\item if $y_{c_{\mathrm{wr}}}=1$, the low eight bits of $y_{R_{\mathrm{out}}}$, most
 significant first, are written under the arm if $\mathrm{dest}=0$ and under the
 copy head if $\mathrm{dest}=1$, that head turning after each, and
 $R_{\mathrm{out}}$ is cleared;
 \item if $y_{c_{\mathrm{rd}}}=1$, then $c_{\mathrm{eot}}$ is set if
 $\mathrm{dest}=1$ and $\mathrm{cnt}=\mathrm{lim}$, and otherwise the eight bits
-under the read head, the head turning after each, are loaded into
-$R_{\mathrm{in}}$ most significant first, $c_{\mathrm{eot}}$ is cleared and
-$\mathrm{cnt}$ is incremented;
+under the read head, the head turning after each, are loaded into the low byte of
+$R_{\mathrm{in}}$ most significant first, their sign bit is copied into the bits
+above them, $c_{\mathrm{eot}}$ is cleared and $\mathrm{cnt}$ is incremented;
 \item if $y_{c_{\mathrm{rw}}}=1$, then $\mathrm{lim}\leftarrow\mathrm{cnt}$,
 $\mathrm{cnt}\leftarrow0$ and $\mathrm{dest}\leftarrow1$;
 \item the request cells are cleared.
@@ -1670,13 +1690,13 @@ loads $m^\ast$ and runs the copy.}
 \end{figure}
 
 \begin{proposition}[One pass]\label{prop:storedpass}
-Let a state of $T^{12}_{G,L}$ with $G=36{,}074$ hold $S$ in the active bank from
-its first record, and in the window clear requests and a host state $x$. One pass
-replaces $x$ by $x_0(m^\ast)$ and clears $\mathrm{cnt}$, $\mathrm{lim}$ and
-$\mathrm{dest}$ if $\mathrm{booted}=0$; then carries out one step of $\Nhost$
-followed by the device of Definition~\ref{def:ring}; then sets $\mathrm{booted}$
-to the negation of the halt bit and, if the halt bit is $1$, changes $\kappa$ at
-its last step. It leaves $S$ in the active bank from its first record and the
+Let a state of $T^\alpha_{G,L}$ hold $S_{A,w}$, of $G$ records, in the active bank
+from its first record, and in the window clear requests and a state $x$ of $H_A$.
+One pass replaces $x$ by $x_0(m^\ast_A)$ and clears $\mathrm{cnt}$, $\mathrm{lim}$
+and $\mathrm{dest}$ if $\mathrm{booted}=0$; then carries out one step of $H_A$
+followed by the device of Definition~\ref{def:ring}; then sets $\mathrm{booted}$ to
+the negation of the halt bit and, if the halt bit is $1$, changes $\kappa$ at its
+last step. It leaves $S_{A,w}$ in the active bank from its first record and the
 requests clear, whatever the temporaries held.
 \end{proposition}
 
@@ -1684,40 +1704,44 @@ requests clear, whatever the temporaries held.
 By Lemma~\ref{lem:feedback} the pass evaluates the blocks of
 Construction~\ref{con:stored} in order. The startup records leave every cell
 unchanged when $\mathrm{booted}=1$; otherwise they set each memory bit to its value
-in $m^\ast$ and clear the other cells they name. The step block is $\Nhost$
+in $m^\ast_A$ and clear the other cells they name. The step block is $H_A$
 compiled by Lemma~\ref{cor:compile}, in an order that Lemma~\ref{lem:feedback}
-admits: the first stage writes temporaries only, and no record reads a state bit
-after the record that writes its next value, a condition checked over the records.
-So after the block the state bits hold the next state of $\Nhost$, which
-Remark~\ref{rem:storedcheck} also checks on every window. The device
-records form the requests $[y_c=1]$ as conjunctions of eight literals, the bit
-$[\mathrm{cnt}=\mathrm{lim}]$ as a conjunction of twenty equivalences, and its
-conjunction with $\mathrm{dest}$. They then write each bit of $R_{\mathrm{out}}$
-under the arm or the copy head by a multiplexer, followed by the request that turns
-that head, and clear $R_{\mathrm{out}}$ on a write; load each bit under the read
-head into $R_{\mathrm{in}}$ by a multiplexer on the condition of a read, followed
-by the request that turns the read tape; set $c_{\mathrm{eot}}$; increment
-$\mathrm{cnt}$ by carries formed before any of its bits changes; carry out the
-rewind; and clear the requests: these are clauses (i) to (iv) of
-Definition~\ref{def:ring}. The hand-over records set $\mathrm{booted}$ and,
-last, $\kappa$. Every temporary is written in the pass before it is read and is not
-written after its last read, so a cell shared by temporaries holds, at each read,
-the value of the temporary read. No record writes the active bank, which turns by
-$G$ records.
+admits: the first stage writes temporaries only, and in the second the group of a
+state bit evaluates with its unit only units read by that unit alone, $HP_i$,
+$Q_i$, $TA_i$ and $TB_i$ for a counter bit, $AC$, $HA$ and $HB$ for the halt bit,
+$KP_{j,t}$ and $WR_{j,t}$ for a memory bit (Table~\ref{tab:blocks}), which read,
+besides temporaries, only that bit and, for a counter bit, the halt bit, whose
+group comes later. So after the block the state bits hold the next state of
+$H_A$, which Remark~\ref{rem:storedcheck} also checks on every window for
+$A\le10$. The device records form the requests $[y_c=1]$ as conjunctions of $A$
+literals, the bit $[\mathrm{cnt}=\mathrm{lim}]$ as a conjunction of $w$
+equivalences, and its conjunction with $\mathrm{dest}$. They then write each bit of
+the low byte of $R_{\mathrm{out}}$ under the arm or the copy head by a multiplexer,
+followed by the request that turns that head, and clear $R_{\mathrm{out}}$ on a
+write; load each bit under the read head into $R_{\mathrm{in}}$ by a multiplexer on
+the condition of a read, followed by the request that turns the read tape, and copy
+the sign bit above them; set $c_{\mathrm{eot}}$; increment $\mathrm{cnt}$ by carries
+formed before any of its bits changes; carry out the rewind; and clear the
+requests: these are clauses (i) to (iv) of Definition~\ref{def:ring}. The hand-over
+records set $\mathrm{booted}$ and, last, $\kappa$. Every temporary is written in the
+pass before it is read and is not written after its last read, so a cell shared by
+temporaries holds, at each read, the value of the temporary read. No record writes
+the active bank, which turns by $G$ records.
 \end{proof}
 
 The theorems below hold for every image $S'$ of $G$ records of which a pass of
-$T^\alpha_{G,L}$, $\alpha\ge12$, does what Proposition~\ref{prop:storedpass}
-states for $S$, on the window cells of Construction~\ref{con:stored}, every cell
-that a record after the startup records reads, other than $\kappa$, the cells
-under the heads and the sink, being written earlier in the pass; we call such an
-image a \emph{stored host}, of $B=bG/8$ bytes with $b=8+3\alpha$. Its step block may
-compile any netlist whose step is that of $\Nhost$, and $S$ is a stored host with
-$\alpha=12$, $G=36{,}074$ and $B=198{,}407$.
+$T^\alpha_{G,L}$ does what Proposition~\ref{prop:storedpass} states for some
+$S_{A,w}$, on the window cells of Construction~\ref{con:stored}, every cell that a
+record after the startup records reads, other than $\kappa$, the cells under the
+heads and the sink, being written earlier in the pass; we call such an image a
+\emph{stored host}, of $B=bG/8$ bytes with $b=8+3\alpha$, and $w$ the width of its
+counters. Its step block may compile any netlist whose step is that of $H_A$; every
+$S_{A,w}$ is a stored host, and $S$ one with $\alpha=12$, $G=36{,}074$ and
+$B=198{,}407$.
 
 \begin{theorem}[Universal construction by the dynamics]\label{thm:storedconstruct}
-Let $S'$ be a stored host of $G$ records and $B<2^{19}$ bytes, let $X$ be an image
-of $G$ records, let $r$ be a recipe with $\delta(r)=X$, and let $L=8|r|$. Let $x$
+Let $S'$ be a stored host of $G$ records and $B$ bytes with $2B+1<2^w$, let $X$ be
+an image of $G$ records, let $r$ be a recipe with $\delta(r)=X$, and let $L=8|r|$. Let $x$
 be a state of $T^\alpha_{G,L}$ with $S'$ in the active bank from its first record,
 $r$ on the read tape from its head, and in the window $\mathrm{booted}=0$ and clear
 requests, whatever the idle bank, the copy tape and the other cells hold. After as
@@ -1730,15 +1754,15 @@ $T^\alpha_{G,L}$ evaluates the records of $X$.
 
 \begin{proof}
 By the conclusion of Proposition~\ref{prop:storedpass} the first pass loads
-$x_0(m^\ast)$ and carries out the first step of the host, and each later pass one
+$x_0(m^\ast_A)$ and carries out the first step of the host, and each later pass one
 more step, with the device of Definition~\ref{def:ring}, up to the pass in which
 the halt bit is set, which clears $\mathrm{booted}$ and changes $\kappa$ at its
-last step. By Theorem~\ref{thm:selfrep}, $P^\ast$ on $r$ with the device of
-Definition~\ref{def:transducer} halts after the steps of
+last step. By Theorem~\ref{thm:selfrep} and Remark~\ref{rem:wider}, $P^\ast$ on
+$r$ with the device of Definition~\ref{def:transducer} halts after the steps of
 Proposition~\ref{prop:steps} with output $\delta(r)\cat r$, reads no byte at
 $h=|r|$ before it requests the rewind, and requests it at $h=|r|$. On this run the
 two devices agree. A token covers at least one byte in at most two, so
-$|r|\le2B+1<2^{20}$ and $\mathrm{cnt}$ does not wrap. Before the rewind
+$|r|\le2B+1<2^w$ and $\mathrm{cnt}$ does not wrap. Before the rewind
 $\mathrm{dest}=0$ and each read loads the next
 byte of $r$ and increments $\mathrm{cnt}$, so $\mathrm{cnt}=h$; at the rewind the
 read head has turned $8|r|=L$ cells and is back at its start, and $\mathrm{lim}$
@@ -1756,8 +1780,8 @@ By Lemma~\ref{lem:complete} every image of $G$ records has a recipe, so a stored
 host builds every image of its own size, itself among them.
 
 \begin{theorem}[Self-reproduction of the host by the dynamics]\label{thm:storedrep}
-Let $S'$ be a stored host of $G$ records and $B<2^{19}$ bytes, $\tau'=\describe(S')$
-and $L=8|\tau'|$, and let $x_0$ be the state of $T^\alpha_{G,L}$ with $S'$ in $Q_0$,
+Let $S'$ be a stored host of $G$ records and $B$ bytes with $2B+1<2^w$,
+$\tau'=\describe(S')$ and $L=8|\tau'|$, and let $x_0$ be the state of $T^\alpha_{G,L}$ with $S'$ in $Q_0$,
 $\tau'$ on $D_0$, and $Q_1$, $D_1$ and the window clear. For every $g\ge1$, the
 state after $g$ generations of $P$ passes, $GP$ applications of $T^\alpha_{G,L}$
 each, holds $S'$ in both banks and $\tau'$ on both tapes, each from its head, with
@@ -1795,6 +1819,42 @@ address are never written. So the two generations perform the same steps and end
 in the same state. Theorem~\ref{thm:physnet} carries the statement to the network.
 \end{proof}
 
+\begin{theorem}[Every word width]\label{thm:widths}
+For every $A\ge8$ there is a least $w_A\ge20$ for which $S_A=S_{A,w_A}$ has
+$2B+1<2^{w_A}$. The stored host $S_A$ builds every image of its size and
+reproduces itself by the dynamics of $N^{\alpha_A}_{G_A,L_A}$ as
+Theorems~\ref{thm:storedconstruct} and~\ref{thm:storedrep} state, with
+\[
+G_A=35A2^{A-1}-2^{A+1}+\tfrac16(A^3-A)+A^2+29A+14w_A+85+\pi_A
+\]
+records, $\pi_A\le7$ the sink records of its hand-over, a window of $2^{\alpha_A}$
+cells with $\alpha_A=A+\Theta(\log A)$, and generations of $\Theta(A^34^A)$
+applications of $T^{\alpha_A}_{G_A,L_A}$.
+\end{theorem}
+
+\begin{proof}
+A pass of $S_A$ does what Proposition~\ref{prop:storedpass} states, and every cell
+a record after the startup reads, other than $\kappa$, the cells under the heads and
+the sink, is written earlier in the pass, so $S_A$ is a stored host; $w_A$ exists
+since $B$ grows with $w$ far slower than $2^w$. The startup and device records are counted in Construction~\ref{con:stored} and the
+hand-over has $4+\pi_A$. Lemma~\ref{cor:compile} compiles a conjunction or a
+disjunction of $k\ge2$ literals into $k-1$ records and a unit of threshold $2$ on
+three or four literals into four or eight, and summing over the blocks of
+Table~\ref{tab:blocks} gives
+$\tfrac{33}{2}A2^A-2^{A+1}+\tfrac16(A^3-A)+A^2+17A+4$ step records, the cubic term
+from the carry terms. The window holds the $A2^A+A+1$ state bits and at most $G_A$
+temporaries, so $\alpha_A=A+\Theta(\log A)$; then $b=8+3\alpha_A=\Theta(A)$,
+$B=bG_A/8=\Theta(A^22^A)$, and Theorem~\ref{thm:storedrep} gives a generation of
+$\Theta(B)$ passes of $G_A$ steps.
+\end{proof}
+
+For $A=8$ to $12$, $S_A$ has $36{,}074$, $80{,}448$, $178{,}100$, $391{,}216$ and
+$853{,}167$ records, windows of $2^{12}$ to $2^{16}$ cells, counters of $20$, $20$,
+$22$, $23$ and $24$ bits and images of $198{,}407$ to $5{,}972{,}169$ bytes, and a
+generation takes $2{,}202{,}812$, $5{,}247{,}354$, $12{,}358{,}336$,
+$28{,}775{,}186$ and $66{,}305{,}186$ passes, $7.95\times10^{10}$ to
+$5.66\times10^{13}$ applications of $T$.
+
 \begin{corollary}[Self-reproduction under noise]\label{cor:storednoise}
 $\Lev(N^{12}_{G,L})$ has depth $15$ and $110{,}775+58N+32L$ rows, $M=143{,}364{,}199$
 for the member that holds $S$. Under independent centred Gaussian perturbations of
@@ -1814,25 +1874,23 @@ coefficients.
 \end{proof}
 
 \begin{remark}[Corroboration]\label{rem:storedcheck}
-Three generations from $x_0$ were run on a transcription of
-Definition~\ref{def:twohead} in C, $79{,}464{,}240{,}088$ steps each: after each
-the new active bank held $S$ and the new read tape $\tau_S$, each from its head,
-the other bank and tape still held them, $\kappa$ alternated, and the full state
-after the third generation equalled the state after the first. A transcription in
-Python agreed with the C program on the full state after three passes and
-$12{,}345$ further steps. One pass was compared with the startup, one step of
+Three generations of $S$ from $x_0$ were run on a transcription of
+Definition~\ref{def:twohead} in C: after each the new active bank held $S$ and the
+new read tape $\tau_S$, each from its head, the other bank and tape still held them,
+$\kappa$ alternated, and the full state after the third generation equalled the
+state after the first. One pass of $S$ agreed with the startup, one step of
 $\Nhost$ and the device of Definition~\ref{def:ring} from $300$ random states, a
-fifth of them not booted and a third with requests holding random bytes, with
-random tapes, idle bank, registers and temporaries, and agreed in every case; that no
-record of the step block reads a state bit after the record of its next value, and
-that no temporary is written after its last read, was checked over the records.
-The startup and step records of the image were also evaluated on reduced ordered
-decision diagrams over variables for the state bits and the units of $\Nhost$, the
-variable of a unit replacing, at the record the compiler names as writing its
-value, a diagram checked to equal the unit's function of the variables of its
-predecessors: from every window the startup records leave $x_0(m^\ast)$ or the
-state as $\mathrm{booted}$ is $0$ or $1$, and the step records leave every state bit
-holding the variable of the unit of its next value.
+fifth of them not booted and a third with requests holding random words, with
+random tapes, idle bank, registers and temporaries, and so did one pass of $S_9$
+from $300$ and of $S_{10}$ from $100$. The startup and step records of $S_8$ to
+$S_{10}$ were also evaluated on reduced ordered decision diagrams over variables for
+the state bits and the units of $H_A$, the variable of a unit replacing, at the
+record the compiler names as writing its value, a diagram checked to equal the
+unit's function of the variables of its predecessors: from every window the startup
+records leave $x_0(m^\ast_A)$ or the state as $\mathrm{booted}$ is $0$ or $1$, and the
+step records leave every state bit holding the variable of the unit of its next
+value. The counts of Theorem~\ref{thm:widths} agree with the construction for $A=8$
+to $12$.
 \end{remark}
 
 % =============================================================================
@@ -1840,11 +1898,10 @@ holding the variable of the unit of its next value.
 % =============================================================================
 
 Theorem~\ref{thm:storedrep} is proved on paper over the Rocq proofs of
-Proposition~\ref{prop:host} and Theorem~\ref{thm:physnet}, and was run for three
-generations. This section gives a smaller stored network, the
-organism, that performs von Neumann's cycle in $T_{G,L}$, the machine of $64$
-cells, with a description code of its own; every step of its reproduction is
-proved in Rocq.
+Proposition~\ref{prop:host} and Theorem~\ref{thm:physnet}. This section gives a
+smaller stored network, the organism, that performs von Neumann's cycle in
+$T_{G,L}$, the machine of $64$ cells, with a description code of its own; every step
+of its reproduction is proved in Rocq.
 
 \begin{definition}[The description code]\label{def:code}
 A \emph{gate} is a record that computes the conjunction or the disjunction of
@@ -1944,10 +2001,8 @@ last pass; from then on $T_{133,L}$ evaluates the records of $X$.
 
 \begin{proof}
 By Proposition~\ref{prop:pass} it suffices to follow the decoder over whole
-tapes. In construct mode a gate codon costs $4$ passes in phase C, $8$ in G and
-$18$ in A, and writes the gate's eight bits and the $18$ address bits under the
-arm; an escape costs as many and writes the $26$ bits that follow it; the end
-codon costs $4$ passes and switches to copy mode. Every consumed bit turns the
+tapes. In construct mode a gate codon or an escape costs $30$ passes and writes a
+record under the arm, and the end codon $4$ passes, switching to copy mode. Every consumed bit turns the
 read tape, so after the end codon it has turned $L$ cells and holds $d$ from its
 start again, and the arm has written the $26\cdot133$ bits of $X$ in order and
 turned once per bit, so the idle bank holds $X$. In copy mode every pass consumes
@@ -1986,11 +2041,9 @@ $T$ evaluated in the Rocq kernel, are equal, so the orbit is periodic.
 \begin{remark}\label{rem:organismcheck}
 The description of $\rho$ has $2930$ bits against $3458$ for the bank: a gate is
 named by four bits and its eight bits are written by the organism. Three
-generations from $x_0$ were also run on the transcription of
-Definition~\ref{def:twohead} and on the netlist in C beside it
-(Remark~\ref{rem:physcheck}), with the outcome the theorem states, and the full
-states of the Rocq definition and of the transcription agree after $1000$ and
-$20{,}000$ steps.
+generations were also run on the transcription of Definition~\ref{def:twohead} and
+on the netlist beside it (Remark~\ref{rem:physcheck}), with the outcome the theorem
+states.
 \end{remark}
 
 % =============================================================================
@@ -2027,14 +2080,11 @@ simulated one, while here the simulating network is fixed.
 
 \emph{Finiteness and noise.} Every network here is a finite
 automaton~\cite{Kleene1956,Minsky1967,SimaWiedermann1998}; power beyond finite
-automata comes from weights of unbounded precision~\cite{SiegelmannSontag1995},
-numbers of units that grow with the computation~\cite{ChungSiegelmann2021}
-or weights that change over time~\cite{CabessaSiegelmann2014}, and von Neumann's
-cellular automaton is universal because its tape can be
-extended~\cite{vonNeumann1966,Burks1970}. Analog noise reduces discrete-time analog
-models to finite automata~\cite{MaassOrponen1998}; here bounded perturbations
-preserve every orbit for all time, and the failure probability under unbounded ones
-grows linearly with the run and falls with the margin at every noise level.
+automata comes from unbounded precision~\cite{SiegelmannSontag1995}, growing
+numbers of units~\cite{ChungSiegelmann2021} or changing
+weights~\cite{CabessaSiegelmann2014}, and von Neumann's cellular automaton is
+universal because its tape can be extended~\cite{vonNeumann1966,Burks1970}. Analog
+noise reduces discrete-time analog models to finite automata~\cite{MaassOrponen1998}.
 
 \emph{Self-reproduction.} Von Neumann's universal constructor uses a description
 once as instructions for construction and once as data to be
@@ -2059,14 +2109,12 @@ constructor is a configuration of a fixed threshold network that holds the weigh
 of the network that computes.
 
 \emph{Networks that produce their own parameters.} Neural networks have been
-trained to output their own weights~\cite{ChangLipson2018}, to reach approximate
-fixed points of self-application~\cite{Gabor2022}, to reproduce over
-generations~\cite{RandazzoVersariMordvintsev2021}, to emit the program text that
-trains them~\cite{Schmidgall2021} and to copy a genotype with
-errors~\cite{ShvartzmanRam2024}; hypernetworks generate the weights of other
-networks~\cite{HaDaiLe2017}, and self-referential weight matrices modify
-themselves~\cite{Schmidhuber1993,IrieEtAl2022}. In each case the relation between a
-network and its parameters is learned and approximate.
+trained to output their own weights~\cite{ChangLipson2018,Gabor2022}, to reproduce
+over generations~\cite{RandazzoVersariMordvintsev2021,ShvartzmanRam2024} and to
+emit the program text that trains them~\cite{Schmidgall2021}; hypernetworks and
+self-referential weight matrices generate or modify
+weights~\cite{HaDaiLe2017,Schmidhuber1993,IrieEtAl2022}. In each case the relation
+between a network and its parameters is learned and approximate.
 
 \appendix
 % =============================================================================
@@ -2079,9 +2127,8 @@ and~\ref{sec:amplify} summarize; every run is recorded in the artifact.
 \subsection{The host}
 
 Along the first $4000$ steps of the self-describing instance on $\Lev(\Nhost)$,
-an average of $26{,}825$ rows per step sit at pre-activation $-1$, $4{,}066$ at
-$0$, $10{,}396$ at $-2$, $176$ at $-3$, $499$ at $-4$ and below, and $5$ at $1$ and
-above. Table~\ref{tab:curve} compares the per-step rate at which $256$ noisy
+an average of $26{,}825$ rows per step sit at pre-activation $-1$ and $4{,}066$ at
+$0$. Table~\ref{tab:curve} compares the per-step rate at which $256$ noisy
 copies first leave the exact orbit with the bound of
 Proposition~\ref{prop:profile}, evaluated on the same orbit and weighted by the
 steps each copy ran, and with the bound $Mp$ of Proposition~\ref{prop:random};
@@ -2170,13 +2217,11 @@ $0.36$ & 64/64 & 2{,}188 & $2.93\times10^{-2}$ & $4.30\times10^{-2}$ & $3.89$\\
 \section{Verification}\label{sec:verification}
 % =============================================================================
 
-Four evaluators of the host transition were used, each built from a different
-representation: (a) an integer reference implementing
+Four evaluators of the host transition were used: (a) an integer reference of
 Definitions~\ref{def:subleq} and~\ref{def:transducer}; (b) the netlist that
-$\sigma(\Nhost)$ denotes, evaluated unit by unit; (c) $\Lev(\Nhost)$, as $13$ dense
-ternary matrices or from its $75{,}501$ nonzero entries; and (d) an evaluator in C,
-\texttt{src/netlist\_eval.c}, with its own SUBLEQ reference, device, parser and
-levelization. Evaluators (b)--(d) are built from $\sigma(\Nhost)$. The
+$\sigma(\Nhost)$ denotes, unit by unit; (c) $\Lev(\Nhost)$, dense or sparse; and
+(d) \texttt{src/netlist\_eval.c}, with its own reference, device, parser and
+levelization; (b)--(d) are built from $\sigma(\Nhost)$. The
 self-describing instance ran to completion on (a), (b) and (d) in lockstep,
 $793{,}709$ steps emitting $\sigma(\Nhost)$; $\Omega^\ast$ for three generations on
 (a), (b) and (d) and for one on (c), each of $1{,}664{,}939$ steps emitting
@@ -2210,10 +2255,10 @@ computation; it proves Lemma~\ref{lem:code}, Proposition~\ref{prop:pass},
 Theorem~\ref{thm:construct} for images of any number of records with an idle bank
 of their length, and Theorem~\ref{thm:organism}. The file that defines the
 organism and its description is written by \texttt{src/twohead.py}, and the
-netlist definitions, extracted to OCaml, write for $H_8$ the netlist file of the
-netlist that $\sigma(\Nhost)$ denotes and for $N^6_{133,2930}$ and
-$N^{12}_{5,40}$ files byte for byte equal to those that
-\texttt{src/twohead.py} writes.
+netlist definitions, extracted to OCaml, write for $H_8$ the netlist that
+$\sigma(\Nhost)$ denotes, for $H_9$ and $H_{10}$ those that \texttt{src/host.py}
+generates, and for $N^6_{133,2930}$ and $N^{12}_{5,40}$ files byte for byte equal to
+those that \texttt{src/twohead.py} writes.
 
 The encoder satisfies $\delta(\describe(f))=f$ within the bound of
 Lemma~\ref{lem:describe} on the $29$ serialized machines of the artifact,
@@ -2225,15 +2270,12 @@ $137{,}781$ ternary units on eight inputs with biases in $[-10,10]$ computes the
 branch predicate; $\inst(\ser(\Omega))=\Omega$ on $310$ instances; the constructor,
 run on the $29$ recipes on the reference and on four of them on the netlist of
 $\sigma(\Nhost)$, emitted every target in the number of steps the reference took;
-and rebuilding the host from source reproduces its serialization byte for byte.
-
-Every run of $\Omega^\ast$ produced the same output, of SHA-256 digest
-\texttt{c5950d3f\ldots6e7fb523}, and the artifact~\cite{Norton2026} is identified by
-the digests of $\ser(\Omega^\ast)$, of the host serialization, of the serialization
-of $N_3$, of $\ser(\Omega^\ast_3)$, of the netlist file of $N^6_{133,2930}$, of
-the organism's record image and its description written as $3458$ and $2930$
-bytes of value $0$ or $1$, and of the image of the stored host and $\tau_S$ as
-bytes:
+rebuilding the host from source reproduces its serialization byte for byte.
+
+Every run of $\Omega^\ast$ produced the same output, and the
+artifact~\cite{Norton2026} is identified by the following SHA-256 digests, the
+organism's image and description taken as $3458$ and $2930$ bytes of value $0$ or
+$1$:
 \begin{center}\ttfamily\small
 \begin{tabular}{@{}l@{\quad}l@{}}
 \normalfont $\ser(\Omega^\ast)$ & c5950d3fec6bcf70e8111586a030d21b2dfa55bd69a1c7fe5f016cb06e7fb523\\
@@ -2281,65 +2323,6 @@ safetensors 0.8.0 and GCC 13.3.0 on Ubuntu 24.04, on an Intel Core i9-12900H
 with $20$ hardware threads and $31$ GiB of memory and an NVIDIA GeForce RTX 3070
 Ti Laptop GPU with $8$ GiB of memory.
 
-% =============================================================================
-\section{Program listings}\label{app:listings}
-% =============================================================================
-
-An instruction $A\;B\;C$ assigns $M[B]\leftarrow M[B]-M[A]$ and branches to $C$
-when the result is at most $0$ (Definition~\ref{def:subleq}); the device cells are
-those of Table~\ref{tab:device} and the variables those of
-Construction~\ref{con:P}, with $\cell{EOK}=\cell{0xF5}$ holding $1$. Writing $b$ for
-the tape byte just read, $\nu(b)$ is the value the program emits for it.
-
-\begin{table}[ht]\centering\small
-\begin{tabular}{@{}rlllll@{}}
-\toprule
-$k$ & addr & $A$ & $B$ & $C$ & effect\\
-\midrule
-0 & \cell{0x00} & \cell{T2} & \cell{T2} & \cell{0x03} & $M[\cell{T2}]\leftarrow 0$\\
-1 & \cell{0x03} & \cell{T1} & \cell{T1} & \cell{0x06} & $M[\cell{T1}]\leftarrow 0$\\
-2 & \cell{0x06} & \cell{NEG1} & $c_{\mathrm{rd}}$ & \cell{0x09} & read request\\
-3 & \cell{0x09} & $R_{\mathrm{in}}$ & \cell{T1} & \cell{0x0C} & $M[\cell{T1}]\leftarrow\nu(T)$\\
-4 & \cell{0x0C} & \cell{T1} & \cell{T2} & \cell{0x0F} & $M[\cell{T2}]\leftarrow T$\\
-5 & \cell{0x0F} & \cell{Z} & \cell{T2} & \cell{0x15} & branch if $T=0$ or $T\ge128$\\
-6 & \cell{0x12} & \cell{Z} & \cell{Z} & \cell{0x1B} & goto \textsc{lit}\\
-7 & \cell{0x15} & \cell{Z} & \cell{T1} & \cell{0x3C} & branch to \textsc{end} if $\nu(T)\le0$\\
-8 & \cell{0x18} & \cell{Z} & \cell{Z} & \cell{0x2D} & goto \textsc{rep}\\
-9 & \cell{0x1B} & \cell{NEG1} & $c_{\mathrm{rd}}$ & \cell{0x1E} & \textsc{lit}: read request\\
-10 & \cell{0x1E} & $R_{\mathrm{in}}$ & $R_{\mathrm{out}}$ & \cell{0x21} & $M[R_{\mathrm{out}}]\leftarrow\nu(b)$\\
-11 & \cell{0x21} & \cell{NEG1} & $c_{\mathrm{wr}}$ & \cell{0x24} & write request\\
-12 & \cell{0x24} & \cell{ONE} & \cell{T2} & \cell{0x2A} & $M[\cell{T2}]\mathrel{-}=1$; done $\to$ 14\\
-13 & \cell{0x27} & \cell{Z} & \cell{Z} & \cell{0x1B} & next literal byte\\
-14 & \cell{0x2A} & \cell{Z} & \cell{Z} & \cell{0x00} & goto 0\\
-15 & \cell{0x2D} & \cell{NEG1} & $c_{\mathrm{rd}}$ & \cell{0x30} & \textsc{rep}: read request\\
-16 & \cell{0x30} & $R_{\mathrm{in}}$ & $R_{\mathrm{out}}$ & \cell{0x33} & $M[R_{\mathrm{out}}]\leftarrow\nu(b)$\\
-17 & \cell{0x33} & \cell{NEG1} & $c_{\mathrm{wr}}$ & \cell{0x36} & write request\\
-18 & \cell{0x36} & \cell{ONE} & \cell{T1} & \cell{0x2A} & $M[\cell{T1}]\mathrel{-}=1$; done $\to$ 14\\
-19 & \cell{0x39} & \cell{Z} & \cell{Z} & \cell{0x30} & emit again\\
-20 ($P$) & \cell{0x3C} & \cell{Z} & \cell{Z} & \cell{0xFF} & \textsc{end}: halt\\
-20 ($P^\ast$) & \cell{0x3C} & \cell{NEG1} & $c_{\mathrm{rw}}$ & \cell{0x3F} & \textsc{r}: rewind request\\
-21 & \cell{0x3F} & \cell{NEG1} & $c_{\mathrm{rd}}$ & \cell{0x42} & \textsc{b}: read request\\
-22 & \cell{0x42} & $c_{\mathrm{eot}}$ & \cell{EOK} & \cell{0xFF} & $M[\cell{EOK}]\leftarrow1-c_{\mathrm{eot}}$; halt if $\le0$\\
-23 & \cell{0x45} & $R_{\mathrm{in}}$ & \cell{Z} & \cell{0x48} & $M[\cell{Z}]\leftarrow\nu(b)$\\
-24 & \cell{0x48} & \cell{Z} & $R_{\mathrm{out}}$ & \cell{0x4B} & $M[R_{\mathrm{out}}]\leftarrow b$\\
-25 & \cell{0x4B} & \cell{NEG1} & $c_{\mathrm{wr}}$ & \cell{0x4E} & write request\\
-26 & \cell{0x4E} & \cell{Z} & \cell{Z} & \cell{0x3F} & $M[\cell{Z}]\leftarrow0$; goto \textsc{b}\\
-\bottomrule
-\end{tabular}
-\caption{The constructor $P$ of Construction~\ref{con:P}, instructions $0$ to $20$ at
-\cell{0x00}--\cell{0x3E}, and the self-reproducing program $P^\ast$ of
-Construction~\ref{con:selfrep}, instructions $0$ to $19$ of $P$ followed by $20$ to $26$ at
-\cell{0x3C}--\cell{0x50}.}
-\label{tab:P}\label{tab:Pstar}\end{table}
-
-
-\noindent The memory image $m^\ast$ is zero except for the $81$ program bytes at
-\cell{0x00}--\cell{0x50} and the constants $M[\cell{ONE}]=1$,
-$M[\cell{NEG1}]=255$, $M[\cell{EOK}]=1$; $m_P$ carries the same constants with the
-$63$ bytes of $P$.
-
-
-
 % =============================================================================
 \begin{thebibliography}{99}
 \setlength{\itemsep}{0pt}

src/host.py

@@ -887,6 +887,24 @@ M_P = memory_image(P)
 M_STAR = memory_image(P_STAR)
 
 
+def program_a(prog: List[Tuple[int, int, int]], A: int) -> List[Tuple[int, int, int]]:
+    """A program moved to 2^A words: the cells from 0xF0 up name the top sixteen words."""
+    top = (1 << A) - 256
+    return [tuple(x + top if x >= 0xF0 else x for x in ins) for ins in prog]
+
+
+def memory_image_a(prog: List[Tuple[int, int, int]], A: int) -> List[int]:
+    """The initial memory of 2^A words holding a program moved there and its constants."""
+    S = 1 << A
+    top = S - 256
+    mem = [0] * S
+    for addr, val in _emit(program_a(prog, A)).items():
+        mem[addr] = val
+    for cell, val in ((Z, 0), (ONE, 1), (T1, 0), (T2, 0), (NEG1, S - 1), (EOK, 1)):
+        mem[cell + top] = val
+    return mem
+
+
 # =============================================================================
 # Device
 # =============================================================================
@@ -944,6 +962,37 @@ def run_reference(mem0: List[int], tau: bytes, max_steps: int = 1 << 34,
         steps += 1
     return bytes(dev.out), steps
 
+
+def run_reference_a(mem0: List[int], tau: bytes, A: int, max_steps: int = 1 << 40) -> Tuple[bytes, int]:
+    """SUBLEQ_A with the device on its top words, a read extending the byte by its sign."""
+    S, half = 1 << A, 1 << (A - 1)
+    io = io_cells(A)
+    wr, eot, rw, rd, rin, rout, halt = (io[k] for k in ('c_wr', 'c_eot', 'c_rw', 'c_rd', 'r_in', 'r_out',
+                                                         'halt_pc'))
+    mem, out = list(mem0), bytearray()
+    pc = h = steps = 0
+    while pc != halt and steps < max_steps:
+        a, b, c = mem[pc], mem[(pc + 1) % S], mem[(pc + 2) % S]
+        r = (mem[b] - mem[a]) % S
+        mem[b] = r
+        pc = c if r == 0 or r >= half else (pc + 3) % S
+        if mem[wr] == 1:
+            out.append(mem[rout] & 0xFF)
+            mem[rout] = 0
+        if mem[rd] == 1:
+            if h < len(tau):
+                v = tau[h]
+                mem[rin] = v if v < 128 else v + S - 256
+                mem[eot] = 0
+                h += 1
+            else:
+                mem[eot] = 1
+        if mem[rw] == 1:
+            h = 0
+        mem[wr] = mem[rd] = mem[rw] = 0
+        steps += 1
+    return bytes(out), steps
+
 # =============================================================================
 # The host netlist and its canonical serialization
 # =============================================================================

src/paper.py

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

src/twohead.py

@@ -1,6 +1,7 @@
 """The two-head machine: the organism, the netlist N_{G,L}, and the host stored in it."""
 import argparse
 import hashlib
+import heapq
 import json
 import os
 import random
@@ -661,21 +662,15 @@ def main_net():
 
 STORED_RECORD = os.path.join(REPO, 'paper', 'runs', 'paper_stored_host.json')
 
-SH_ALPHA = 12
-
-SH_W = 1 << SH_ALPHA
-
-SH_B = 8 + 3 * SH_ALPHA
-
-CW = 20                                         # width of the device's byte counters
+CW = 20                                         # the least width of the device's byte counters
 
 
 # ---------------------------------------------------------------------------
 # the host netlist from its serialization
 # ---------------------------------------------------------------------------
 
-def host_units():
-    data = SR.read_host()
+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 = {}
@@ -695,16 +690,16 @@ def host_units():
     return len(nxt), units, nxt
 
 
-# state layout of sigma: pc bits 0..7 most significant first, halt 8, memory byte j bit k at 9 + 8 j + k,
-# k = 0 the most significant
-def mem_bit(j, t):
-    """State index of bit t (value 2^t) of memory byte j."""
-    return 9 + 8 * j + (7 - t)
+# 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)
 
 
-PC_BIT = lambda t: 7 - t                         # bit t of the counter
-
-HALT = 8
+def pc_bit(t, A=8):
+    """State index of bit t of the counter."""
+    return A - 1 - t
 
 
 # ---------------------------------------------------------------------------
@@ -795,9 +790,9 @@ class Prog:
         self.OR((a, True), (c, True), dst)
 
 
-def compile_host(P):
-    """The records of one step of H_8; state bits are cells ('s', i)."""
-    n, units, nxt = host_units()
+def compile_host(P, A=8):
+    """The records of one step of H_A; state bits are cells ('s', i)."""
+    n, units, nxt = host_units(A)
     cons = {}
     for u, (_, ins) in enumerate(units):
         for s, _w in ins:
@@ -856,8 +851,8 @@ def compile_host(P):
             _chain_lazy(P, 'and' if t == k else 'or', lits, dst, before)
         P.ends[len(P.recs) - 1] = u
 
-    order_next = [nxt[PC_BIT(t)] - n for t in range(8)] + [nxt[HALT] - n] + \
-                 [nxt[mem_bit(j, t)] - n for j in range(256) for t in range(8)]
+    order_next = [nxt[pc_bit(t, A)] - n for t in range(A)] + [nxt[A] - n] + \
+                 [nxt[mem_bit(j, t, A)] - n for j in range(1 << A) for t in range(A)]
     for u in order_next:                         # stage A: everything the next values read
         ensure_ancestors(u)
     for u in order_next:                         # stage B: the next values, in place
@@ -888,27 +883,30 @@ def _chain_lazy(P, kind, lits, dst, before):
 # the device, the startup block and the hand-over
 # ---------------------------------------------------------------------------
 
-def mem_cell(j, t):
-    return ('s', mem_bit(j, t))
+def mem_cell(j, t, A=8):
+    return ('s', mem_bit(j, t, A))
 
 
-def byte_is_one(P, j):
-    """[memory byte j == 1]"""
+def word_is_one(P, j, A=8):
+    """[memory word j == 1]"""
     dst = P.tmp()
-    lits = [(mem_cell(j, 0), True)] + [(mem_cell(j, t), False) for t in range(1, 8)]
+    lits = [(mem_cell(j, 0, A), True)] + [(mem_cell(j, t, A), False) for t in range(1, A)]
     P.chain('and', lits, dst)
     return dst
 
 
-def compile_device(P):
-    cnt = [('d', 'cnt', i) for i in range(CW)]
-    lim = [('d', 'lim', i) for i in range(CW)]
+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')
-    wr, rd, rw = byte_is_one(P, SR.C_WR), byte_is_one(P, SR.C_RD), byte_is_one(P, SR.C_RW)
+    wr = word_is_one(P, io['c_wr'], A)
+    rd = word_is_one(P, io['c_rd'], A)
+    rw = word_is_one(P, io['c_rw'], A)
     # [cnt == lim]
     eq = P.tmp()
     xs = []
-    for i in range(CW):
+    for i in range(w):
         e = P.tmp()
         a1, a0 = P.tmp(), P.tmp()
         P.AND((cnt[i], True), (lim[i], True), a1)
@@ -918,69 +916,73 @@ def compile_device(P):
     P.chain('and', xs, eq)
     eot = P.tmp()                                # the end of the tape is known after the rewind
     P.AND((eq, True), (dest, True), eot)
-    # (i) R_out, most significant bit first, under the arm or under the copy head
+    # (i) the low byte of R_out, most significant bit first, under the arm or under the copy head
     ca, cc = P.tmp(), P.tmp()
     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(SR.R_OUT, t), True), (('c', ARM), True), ('c', ARM))
+        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(SR.R_OUT, t), True), (('c', CPY), True), ('c', CPY))
+        P.MUX(cc, (mem_cell(out, t, A), True), (('c', CPY), True), ('c', CPY))
         P.COPY((cc, True), ('c', AC))
-    for t in range(8):
-        P.AND((mem_cell(SR.R_OUT, t), True), (wr, False), mem_cell(SR.R_OUT, t))
+    for t in range(A):
+        P.AND((mem_cell(out, t, A), True), (wr, False), mem_cell(out, t, A))
     g = P.tmp()
     P.AND((rd, True), (eot, False), g)
-    # (ii) the byte under the read head into R_in, most significant bit first, each bit turning the tape
+    # (ii) the byte under the read head into R_in, most significant bit first, each bit turning the tape,
+    # and its sign bit into the bits above it
     for t in range(7, -1, -1):
-        P.MUX(g, (('c', RD), True), (mem_cell(SR.R_IN, t), True), mem_cell(SR.R_IN, t))
+        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(SR.C_EOT, 0), True), mem_cell(SR.C_EOT, 0))
-    for t in range(1, 8):
-        P.AND((mem_cell(SR.C_EOT, t), True), (rd, False), mem_cell(SR.C_EOT, t))
+    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(CW - 1):
+    for i in range(w - 1):
         c = P.tmp()
         P.AND((car[-1], True), (cnt[i], True), c)
         car.append(c)
-    for i in range(CW):
+    for i in range(w):
         P.XOR((cnt[i], True), (car[i], True), cnt[i])
     # (iii) a rewind: the limit takes the count, the count returns to 0, the writes go to the copy tape
-    for i in range(CW):
+    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 j in (SR.C_WR, SR.C_RD, SR.C_RW):
-        for t in range(8):
-            P.CONST(0, mem_cell(j, t))
+    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):
-    """The startup records: while booted is 0, load m* and clear the counter, halt bit and registers."""
+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."""
     b = ('d', 'booted')
-    for j in range(256):
-        for t in range(8):
-            c = mem_cell(j, t)
+    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(8):
-        P.AND((('s', PC_BIT(t)), True), (b, True), ('s', PC_BIT(t)))
-    P.AND((('s', HALT), True), (b, True), ('s', HALT))
-    for i in range(CW):
+    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'))
     P.CONST(1, b)
 
 
-def compile_handover(P):
+def compile_handover(P, A=8):
     """The hand-over records: at the halt, clear booted and flip the bank bit at the end of the pass."""
-    h = ('s', HALT)
+    h = ('s', A)
     P.AND((('d', 'booted'), True), (h, False), ('d', 'booted'))
     P.XOR((('c', KAPPA), True), (h, True), ('c', KAPPA))
 
@@ -1011,16 +1013,18 @@ def allocate(recs):
         if ao[0] == 't':
             first_w.setdefault(ao, i)
     base = nxt_addr
-    free_at = {}                                 # cell -> index after which it is free
+    busy, free, top = [], [], base               # (index after which it is free, cell); free cells
     addr = dict(fixed)
     for name in sorted(first_w, key=lambda x: first_w[x]):
         start, end = first_w[name], last_r.get(name, first_w[name])
-        cand = [c for c, f in free_at.items() if f < start]
-        c = min(cand) if cand else base + len(free_at)
+        while busy and busy[0][0] < start:
+            heapq.heappush(free, heapq.heappop(busy)[1])
+        if free:
+            c = heapq.heappop(free)
+        else:
+            c, top = top, top + 1
         addr[name] = c
-        free_at[c] = end
-    top = base + len(free_at)
-    assert top <= SH_W, ('window too small', top)
+        heapq.heappush(busy, (end, c))
 
     def res(a):
         if a is None:
@@ -1067,24 +1071,34 @@ def check_schedule(recs, lo, hi, n):
     return dict(state_bits_written=len(written))
 
 
-def build_stored():
-    P = Prog()
-    compile_startup(P, SR.M_STAR)
-    lo = len(P.recs)
-    n, units, nxt = compile_host(P)
-    n_host = len(P.recs) - lo
-    check_schedule(P.recs, lo, len(P.recs), n)
-    compile_device(P)
-    compile_handover(P)
-    recs, addr, top = allocate(P.recs)
-    if len(recs) % 2:                            # an image of whole bytes
-        recs.insert(len(recs) - 3, (SINK, 0, SINK, 0, -1, SINK))
-    image_bits = [b for r in recs for b in encode_record(r, SH_ALPHA)]
+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)
+        recs, addr, top = allocate(P.recs)
+        alpha = (top - 1).bit_length()
+        b = 8 + 3 * alpha
+        while b * len(recs) % 8:                 # an image of whole bytes
+            recs.insert(len(recs) - 3, (SINK, 0, SINK, 0, -1, SINK))
+        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(recs=recs, addr=addr, top=top, image=image, image_bits=image_bits, tau=tau,
-                n_host_records=n_host, host=(n, units, nxt), ends=P.ends)
+    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,
+                host=(n, units, nxt), ends=P.ends)
 
 
 # ---------------------------------------------------------------------------
@@ -1093,12 +1107,13 @@ def build_stored():
 
 class HeadMachine:
     """T_{G,L} with a window of W cells; banks and tapes listed from their heads."""
-    def __init__(self, Q0, Q1, D0, D1, window):
+    def __init__(self, Q0, Q1, D0, D1, window, alpha=12):
         self.Q = [list(Q0), list(Q1)]
         self.D = [list(D0), list(D1)]
         self.h = [[0, 0], [0, 0]]                # heads of the banks and of the tapes
         self.w = list(window)
         self.N, self.L = len(Q0), len(D0)
+        self.alpha, self.b = alpha, 8 + 3 * alpha
 
     def cell(self, a):
         k = self.w[KAPPA]
@@ -1114,7 +1129,7 @@ class HeadMachine:
         k = self.w[KAPPA]
         if rec is None:
             hq = self.h[0][k]
-            rec = decode_record([self.Q[k][(hq + i) % self.N] for i in range(SH_B)], SH_ALPHA)
+            rec = decode_record([self.Q[k][(hq + i) % self.N] for i in range(self.b)], self.alpha)
         a0, w0, a1, w1, beta, ao = rec
         v = 1 if w0 * self.cell(a0) + w1 * self.cell(a1) + beta >= 0 else 0
         if ao == ARM:
@@ -1123,7 +1138,7 @@ class HeadMachine:
             self.D[1 - k][self.h[1][1 - k]] = v
         elif ao != RD:
             self.w[ao] = v
-        self.h[0][k] = (self.h[0][k] + SH_B) % self.N
+        self.h[0][k] = (self.h[0][k] + self.b) % self.N
         if self.w[AA]:
             self.h[0][1 - k] = (self.h[0][1 - k] + 1) % self.N
         if self.w[AR]:
@@ -1144,36 +1159,38 @@ def host_step(n, units, nxt, x):
     return [sig[v] for v in nxt]
 
 
-def check_stored(trials=40, seed=3, verbose=False):
-    S = build_stored()
-    recs, addr = S['recs'], S['addr']
+def check_stored(trials=40, seed=3, verbose=False, A=8):
+    S = build_stored(A)
+    recs, addr, w, alpha = S['recs'], S['addr'], S['w'], S['alpha']
     n, units, nxt = S['host']
+    io = SR.io_cells(A)
     G = len(recs)
     rng = random.Random(seed)
     bad = 0
-    image_bits = [b for r in recs for b in encode_record(r, SH_ALPHA)]
+    image_bits = S['image_bits']
+    m0 = SR.memory_image_a(SR.P_STAR, A)
     x0 = [0] * n                                 # the state x_0(m*)
-    for j in range(256):
-        for t in range(8):
-            x0[mem_bit(j, t)] = (SR.M_STAR[j] >> t) & 1
+    for j in range(1 << A):
+        for t in range(A):
+            x0[mem_bit(j, t, A)] = (m0[j] >> t) & 1
     for trial in range(trials):
         # a random host state with random device registers, temporaries and tapes; every fifth
-        # state not yet booted, and in every third the requests hold random bytes
+        # state not yet booted, and in every third the requests hold random words
         x = [rng.randrange(2) for _ in range(n)]
-        x[HALT] = 0 if trial % 4 else 1
+        x[A] = 0 if trial % 4 else 1
         booted = 0 if trial % 5 == 0 else 1
-        for j in (SR.C_WR, SR.C_RD, SR.C_RW):
-            v = rng.randrange(256) if trial % 3 == 0 else rng.choice((0, 1))
-            for t in range(8):
-                x[mem_bit(j, t)] = (v >> t) & 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
         L = 64
         cnt, lim = rng.randrange(8), rng.randrange(8)
         dest = rng.randrange(2)
-        win = [rng.randrange(2) for _ in range(SH_W)]
+        win = [rng.randrange(2) for _ in range(1 << alpha)]
         win[KAPPA] = 0
         for i in range(n):
             win[addr[('s', i)]] = x[i]
-        for i in range(CW):
+        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
@@ -1182,55 +1199,57 @@ def check_stored(trials=40, seed=3, verbose=False):
         D0 = [rng.randrange(2) for _ in range(L)]
         Q1 = [rng.randrange(2) for _ in range(len(image_bits))]
         D1 = [rng.randrange(2) for _ in range(L)]
-        M = HeadMachine(image_bits, Q1, D0, D1, win)
+        M = HeadMachine(image_bits, Q1, D0, D1, win, alpha)
         for g in range(G):
             M.step(recs[g])
-        # expected: the startup if not booted, one step of H_8, then the device on the ring tapes
+        # expected: the startup if not booted, one step of H_A, then the device on the ring tapes
         if not booted:
             x, cnt, lim, dest = list(x0), 0, 0, 0
         y = host_step(n, units, nxt, x)
-        get = lambda j: sum(y[mem_bit(j, t)] << t for t in range(8))
+        get = lambda j: sum(y[mem_bit(j, t, A)] << t for t in range(A))
 
         def put(j, v):
-            for t in range(8):
-                y[mem_bit(j, t)] = (v >> t) & 1
+            for t in range(A):
+                y[mem_bit(j, t, A)] = (v >> t) & 1
         e_q1, e_d1, hq1, hd0, hd1 = list(Q1), list(D1), 0, 0, 0
         e_cnt, e_lim, e_dest = cnt, lim, dest
-        if get(SR.C_WR) == 1:
-            byte = get(SR.R_OUT)
+        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:
                     e_d1[hd1] = bit; hd1 += 1
                 else:
                     e_q1[hq1] = bit; hq1 += 1
-            put(SR.R_OUT, 0)
-        if get(SR.C_RD) == 1:
+            put(io['r_out'], 0)
+        if get(io['c_rd']) == 1:
             if not (e_dest and e_cnt == e_lim):
-                put(SR.R_IN, sum(D0[hd0 + kk] << (7 - kk) for kk in range(8)))
+                byte = sum(D0[hd0 + kk] << (7 - kk) for kk in range(8))
+                put(io['r_in'], byte if byte < 128 else byte + (1 << A) - 256)
                 hd0 += 8
-                put(SR.C_EOT, 0)
-                e_cnt = (e_cnt + 1) % (1 << CW)
+                put(io['c_eot'], 0)
+                e_cnt = (e_cnt + 1) % (1 << w)
             else:
-                put(SR.C_EOT, 1)
-        if get(SR.C_RW) == 1:
+                put(io['c_eot'], 1)
+        if get(io['c_rw']) == 1:
             e_lim, e_cnt, e_dest = e_cnt, 0, 1
-        put(SR.C_WR, 0); put(SR.C_RD, 0); put(SR.C_RW, 0)
-        e_kappa = 1 if y[HALT] else 0
+        for c in ('c_wr', 'c_rd', 'c_rw'):
+            put(io[c], 0)
+        e_kappa = 1 if y[A] else 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(CW))
-        g_lim = sum(M.w[addr[('d', 'lim', i)]] << i for i in range(CW))
+        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[1] == e_q1, copy=M.D[1] == e_d1,
                      arm=M.h[0][1] == hq1, read=M.h[1][0] == hd0, copyhead=M.h[1][1] == hd1,
                      kappa=M.w[KAPPA] == e_kappa, tape=M.D[0] == D0,
-                     booted=M.w[addr[('d', 'booted')]] == 1 - y[HALT],
+                     booted=M.w[addr[('d', 'booted')]] == 1 - y[A],
                      requests=M.w[AR] == M.w[AA] == M.w[AC] == 0, active=M.Q[0] == image_bits)
         ok = all(parts.values())
         if not ok and verbose:
             print(trial, [k for k, v in parts.items() if not v], 'reqs',
-                  [get(j) for j in (SR.C_WR, SR.C_RD, SR.C_RW)], 'dest', dest, 'cnt', cnt, 'lim', lim,
-                  'halt', x[HALT], [i for i in range(n) if got[i] != y[i]][:10])
+                  [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'])
 
@@ -1285,34 +1304,39 @@ class BDD:
         return row[t]
 
 
-def symbolic_check():
-    """The startup and step records of the image of S on decision diagrams over the signals of N_host."""
+def symbolic_check(A=8):
+    """The startup and step records of the image of S_A on decision diagrams over the signals of H_A."""
     sys.setrecursionlimit(100000)
     t0 = time.time()
-    S = build_stored()
-    n, units, nxt = host_units()
+    S = build_stored(A)
+    n, units, nxt = host_units(A)
+    b, alpha = S['b'], S['alpha']
     bits = bytes_to_bits(S['image'])
-    recs = [decode_record(bits[k * SH_B:(k + 1) * SH_B], SH_ALPHA) for k in range(len(bits) // SH_B)]
-    lo, hi = 2099, 2099 + S['n_host_records']
+    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']
     addr = S['addr']
     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
-    val, first, fn = [D.var(s) for s in range(n)], {}, []
-    for u, (b, ins) in enumerate(units):
-        f = D.atleast(sum(1 for _, w in ins if w < 0) - b, [(val[s], w > 0) for s, w in ins])
+    # 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(D.var(first.setdefault(f, n + u)) if f > 1 and D.node[f][1:] not in ((0, 1), (1, 0)) else 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, b):
+    def run(window, a, z):
         # 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
-        for k in range(a, b):
+        for k in range(a, z):
             a0, w0, a1, w1, beta, ao = recs[k]
             assert ao >= 7, ('a record writes a head or a request', k)
             g = D.record(w0, window[a0], w1, window[a1], beta)
@@ -1324,25 +1348,26 @@ def symbolic_check():
 
     # the startup: x_0(m*) when booted is 0, the window unchanged when it is 1
     boot = addr[('d', 'booted')]
-    window = [unknown(c) for c in range(SH_W)]
-    regs = [addr[('d', 'cnt', i)] for i in range(CW)] + [addr[('d', 'lim', i)] for i in range(CW)] + \
+    window = [unknown(c) for c in range(1 << alpha)]
+    regs = [addr[('d', 'cnt', i)] for i in range(S['w'])] + [addr[('d', 'lim', i)] for i in range(S['w'])] + \
         [addr[('d', 'dest')]]
     before = list(window)
     run(window, 0, lo)
     B0 = before[boot]
+    m0 = SR.memory_image_a(SR.P_STAR, A)
     x0 = [0] * n
-    for j in range(256):
-        for t in range(8):
-            x0[mem_bit(j, t)] = (SR.M_STAR[j] >> t) & 1
+    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))
-    # the step: from every window, the state bits end holding the next state of N_host
-    window = [unknown(c) for c in range(SH_W)]
+    # 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 i in range(n):
         window[state[i]] = val[i]
     run(window, lo, hi)
     step = agree[0] and len(ends) == len(units) and all(window[state[i]] == val[nxt[i]] for i in range(n))
-    return dict(startup_records=lo, step_records=hi - lo, startup_exact=startup, step_exact=step,
+    return dict(A=A, startup_records=lo, step_records=hi - lo, startup_exact=startup, step_exact=step,
                 sha256_image=hashlib.sha256(S['image']).hexdigest(), nodes=len(D.node),
                 seconds=round(time.time() - t0, 1))
 
@@ -1353,27 +1378,49 @@ def stored_update_record(key, value):
     json.dump(rec, open(STORED_RECORD, 'w'), indent=1)
 
 
-def run_stored(generations):
+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 5.4."""
+    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):
     """Generations of the stored host on the machine in C, against the reference run of P*."""
-    S = build_stored()
-    recs, image_bits, tau = S['recs'], S['image_bits'], S['tau']
+    S = build_stored(A)
+    recs, image_bits, tau, alpha = S['recs'], S['image_bits'], S['tau'], S['alpha']
     G = len(recs)
-    out, steps = SR.run_reference(SR.M_STAR, tau)
-    assert out == S['image'] + tau
+    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)
     tau_bits = bytes_to_bits(tau)
     work = os.path.join(REPO, 'variants')
-    inp, exe = os.path.join(work, '.stored_host.bin'), os.path.join(work, '.stored_host_run')
+    inp, exe = os.path.join(work, f'.stored_host_{A}.bin'), os.path.join(work, f'.stored_host_run_{A}')
     with open(inp, 'wb') as f:
-        f.write(struct.pack('<4i', SH_W, SH_ALPHA, G, len(tau_bits)))
-        f.write(bytes(image_bits) + bytes(tau_bits) + bytes(SH_W))
+        f.write(struct.pack('<4i', 1 << alpha, alpha, G, len(tau_bits)))
+        f.write(bytes(image_bits) + bytes(tau_bits) + bytes(1 << alpha))
     subprocess.run(['gcc', '-O3', '-march=native', '-o', exe, os.path.join(REPO, 'src', 'stored_host_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)
     lines = [json.loads(l) for l in p.stdout.split('\n') if l.strip()]
     gens = [l for l in lines if 'generation' in l]
-    res = dict(records=G, window_cells=S['top'], record_bits=SH_B, bank_bits=len(image_bits),
-               image_bytes=len(S['image']), tau_bytes=len(tau), passes_expected=steps,
+    res = dict(A=A, records=G, window_cells=S['top'], record_bits=S['b'], counter_bits=S['w'],
+               bank_bits=len(image_bits), image_bytes=len(S['image']), tau_bytes=len(tau), passes_expected=steps,
                generations=gens, seconds=round(time.time() - t0, 1),
                sha256_image=hashlib.sha256(S['image']).hexdigest(),
                sha256_tau=hashlib.sha256(tau).hexdigest())
@@ -1382,36 +1429,65 @@ def run_stored(generations):
             res['state_after_3_equals_after_1'] = l['state_after_3_equals_after_1']
     res['every_generation_exact'] = all(g['passes'] == steps and g['steps'] == steps * G and g['bank_holds_image']
                                         and g['tape_holds_tau'] for g in gens) and len(gens) == generations
-    stored_update_record('run', res)
+    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'],
+                         handover=G - S['startup_records'] - S['n_host_records'] - S['device_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 * G, seconds=round(time.time() - t0, 1)))
+        print(json.dumps(rows[-1]), flush=True)
+    stored_update_record('widths', rows)
+    return rows
+
+
 def cmd_stored():
-    cmd = sys.argv[1] if len(sys.argv) > 1 else 'build'
+    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(sys.argv[2]) if len(sys.argv) > 2 else 40)
+        res = check_stored(int(args[1]) if len(args) > 1 else 40, A=A)
         res['seconds'] = round(time.time() - t0, 1)
-        stored_update_record('pass_check', res)
+        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()
-        stored_update_record('symbolic', res)
+        res = symbolic_check(A)
+        stored_update_record(stored_key('symbolic', A), res)
         print(json.dumps(res))
         sys.exit(0 if res['startup_exact'] and res['step_exact'] else 1)
     elif cmd == 'run':
-        gens = int(sys.argv[2]) if len(sys.argv) > 2 else 3
-        res = run_stored(gens)
+        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'] and (gens < 3 or res.get('state_after_3_equals_after_1') == 1)
                  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()
-        print(json.dumps(dict(records=len(S['recs']), host_records=S['n_host_records'],
-                              window_cells=S['top'], record_bits=SH_B, bank_bits=len(S['image_bits']),
-                              image_bytes=len(S['image']), tau_bytes=len(S['tau']),
+        S = build_stored(A)
+        print(json.dumps(dict(A=A, records=len(S['recs']), host_records=S['n_host_records'],
+                              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))))
 
 

todo.md

@@ -1,5 +0,0 @@
-# todo
-
-Unfinished work.
-
-1. A machine-checked correctness proof relates the shipped weights to the ISA.