Prove in Rocq that the host family computes SUBLEQ at every word width, check the stored host's startup and step records on decision diagrams, state the stored-host theorems for every stored host with their overhead, bound self-reproduction under noise, remove the neuromorphic mappings, and cut the paper to 30 pages

.gitignore

@@ -17,6 +17,9 @@ rocq/.*.aux
 rocq/.lia.cache
 rocq/extract/physnet.ml
 rocq/extract/physnet.mli
+rocq/extract/hostnet.ml
+rocq/extract/hostnet.mli
+rocq/extract/dumphost
 rocq/.nia.cache
 rocq/extract/dump
 rocq/extract/*.cm*

README.md

@@ -596,7 +596,9 @@ that netlist. It also shows where the restriction to {-1, 0, 1} is paid for,
 and that a fixed ternary network, the two-head machine of
 `src/twohead.py`, holds a stored network in its state and evaluates one
 record per step, which `rocq/` proves for every window of 2^α cells, bank and
-tape. The host itself, compiled by `src/twohead.py` into 36,074 records of
+tape; `rocq/` also proves that the host family computes SUBLEQ at every word
+width, and the H_8 it defines is the netlist of the published serialization. The
+host itself, compiled by `src/twohead.py` into 36,074 records of
 two inputs with records that load its memory, its tape device and a hand-over,
 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
@@ -997,8 +999,8 @@ src/                                the library; `python src/<file>.py <command>
   │                                 and `constructor8`, the neural_subleq8io suite
   ├── twohead.py                    the two-head machine: the organism (`organism`), the netlist
   │                                 N_{G,L} (`net`), and the host stored in it (`stored`)
-  ├── noise.py                      read noise and weight error on the host (`host`), the amplified
-  │                                 host (`amplified`), and the neuromorphic datapath
+  ├── noise.py                      read noise and weight error on the host (`host`), and the
+  │                                 amplified host (`amplified`)
   ├── paper.py                      the paper's checks and runs, one command each
   ├── independent.py                code written from the paper's text alone
   ├── netlist_eval.c                an evaluator of the host family and the amplified host in C
@@ -1007,10 +1009,10 @@ src/                                the library; `python src/<file>.py <command>
   ├── restore_bound.c               the restoration bound of the amplified host along the orbit
   └── nsim.c                        the noise simulator of independent.py
 paper/                              the manuscript, and the record of every run it reports
-rocq/                               Rocq proofs: the netlist of the two-head machine computes its
-                                    step for every window of 2^α cells, the organism builds every
-                                    image from any description of it and reproduces in every
-                                    generation
+rocq/                               Rocq proofs: the host family H_A computes SUBLEQ for every word
+                                    width, the netlist of the two-head machine computes its step
+                                    for every window of 2^α cells, the organism builds every image
+                                    from any description of it and reproduces in every generation
 tools/play.py                       the playground, and a demonstration on each machine
 llm_integration/
   ├── llm.py                        SmolLM2 with the frozen circuits: the circuit wrapper, the

paper/README.md

@@ -12,8 +12,7 @@ runs/                                 the record written by each command
 ## What each command establishes
 
 Each command is `python src/<file>.py <command>` and writes its record to `runs/`;
-`paper.py rocq` needs Rocq 9.1 and ocamlfind on the PATH, and `noise.py neuromorphic run`
-needs Lava, which requires Python 3.10.
+`paper.py rocq` needs Rocq 9.1 and ocamlfind on the PATH.
 
 | Command | Record | Establishes |
 |---|---|---|
@@ -37,14 +36,13 @@ needs Lava, which requires Python 3.10.
 | `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 netlist extracted from it |
+| `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 |
 | `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, 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 N_host (`stored symbolic`), and three generations in C |
 | `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` |
-| `noise.py neuromorphic` | `paper_neuromorphic.json` | the datapath on the Loihi and Akida neuron models |
-| `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, Tables 3 to 6 with the noise simulator `src/nsim.c`, and the datapath on Loihi and Akida |
+| `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` |
 
 Rebuild the typeset paper with any TeX installation:
 

paper/runs/independent_neuromorphic.json

@@ -1,34 +0,0 @@
-{
- "datapath": {
-  "units": 106,
-  "depth": 5,
-  "widths": [
-   48,
-   58,
-   23,
-   23,
-   9
-  ]
- },
- "akida": {
-  "backend": "akida 2.19.3",
-  "patterns": 65536,
-  "failures": 0
- },
- "lava_vth_16": {
-  "backend": "lava fixed_pt",
-  "vth": 16,
-  "patterns": 4096,
-  "failures": 0,
-  "margin_firing_side": 128,
-  "margin_quiet_side": 0
- },
- "lava_vth_17": {
-  "backend": "lava fixed_pt",
-  "vth": 17,
-  "patterns": 4096,
-  "failures": 0,
-  "margin_firing_side": 64,
-  "margin_quiet_side": 64
- }
-}

paper/runs/paper_neuromorphic.json

@@ -1,29 +0,0 @@
-{
- "backend": "Lava 0.10.0, fixed_pt tag (Loihi neuron model)",
- "units": 106,
- "layers": 5,
- "widths": [
-  48,
-  58,
-  23,
-  23,
-  9
- ],
- "worst_accumulation": 16,
- "patterns": 4096,
- "failures": 0,
- "margin_membrane_units": 64,
- "weight_scale": 2,
- "synapse_granularity": 2,
- "bias_offset": 9,
- "ok": true,
- "akida": {
-  "backend": "akida 2.19.3, software backend",
-  "layers": 5,
-  "patterns": 65536,
-  "failures": 0,
-  "weights_bits": 2,
-  "act_bits": 1,
-  "ok": true
- }
-}

paper/runs/paper_rocq.json

@@ -1,7 +1,7 @@
 {
  "rocq": "The Rocq Prover, version 9.1.1",
- "files": 25,
- "build_seconds": 233.8,
+ "files": 30,
+ "build_seconds": 303.5,
  "theorems": {
   "PhysMain.netlist_step": "closed",
   "PhysMain.netlist_step64": "closed",
@@ -18,7 +18,16 @@
   "Main.every_generation": "closed",
   "SelfRep.self_reproduction": "closed",
   "SelfRep.second_generation": "closed",
-  "SelfRep.periodic": "closed"
+  "SelfRep.periodic": "closed",
+  "HostSem.host_step": "closed"
  },
- "extraction_identical": true
+ "extraction_identical": true,
+ "lines": 5093,
+ "host_extraction": {
+  "A": 8,
+  "units": 17598,
+  "identical": true,
+  "sha256_sigma": "2263144948d68cafbf1616a6c0bd74e98cb597c1a6d5b1512d65d3aff574f17a",
+  "sha256_rocq": "2263144948d68cafbf1616a6c0bd74e98cb597c1a6d5b1512d65d3aff574f17a"
+ }
 }

paper/runs/paper_stored_host.json

@@ -66,5 +66,14 @@
   "records": 36074,
   "window_cells": 2896,
   "seconds": 131.8
+ },
+ "symbolic": {
+  "startup_records": 2099,
+  "step_records": 33568,
+  "startup_exact": true,
+  "step_exact": true,
+  "sha256_image": "7a769aa264a89860149962d7e98f8b2a5cb34ceb7778e88bcbffdccdc0996154",
+  "nodes": 1435999,
+  "seconds": 3.6
  }
 }

paper/universal_construction_ternary.pdf

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

rocq/Adder.v

@@ -0,0 +1,128 @@
+(* The subtractor of Lemma 3.2: the carry-lookahead terms are the ripple carries of y + not x + 1,
+   and the sum bits spell (y - x) mod 2^A. *)
+From Stdlib Require Import List Bool Arith Lia.
+Import ListNotations.
+From TH Require Import TwoHead Net PhysSem.
+
+(* the value of the bits f 0 .. f (n - 1), least significant first *)
+Definition bv (f : nat -> bool) (n : nat) : nat := bits2nat (rev (map f (seq 0 n))).
+
+Lemma bv_S : forall f n, bv f (S n) = (if f n then 2 ^ n else 0) + bv f n.
+Proof.
+  intros f n. unfold bv. rewrite seq_S, map_app, rev_app_distr. cbn [map rev app].
+  rewrite bits2nat_cons, length_rev, length_map, length_seq. reflexivity.
+Qed.
+
+Lemma bv_lt : forall f n, bv f n < 2 ^ n.
+Proof.
+  intros f n. unfold bv. pose proof (bits2nat_lt (rev (map f (seq 0 n)))) as H.
+  rewrite length_rev, length_map, length_seq in H. exact H.
+Qed.
+
+Lemma testbit_bv : forall f n k, k < n -> Nat.testbit (bv f n) k = f k.
+Proof.
+  intros f n k Hk. unfold bv.
+  pose proof (testbit_bits2nat (rev (map f (seq 0 n))) (n - 1 - k)) as T.
+  rewrite length_rev, length_map, length_seq in T. replace (n - 1 - (n - 1 - k)) with k in T by lia.
+  rewrite T by lia. rewrite rev_nth by (rewrite length_map, length_seq; lia).
+  rewrite length_map, length_seq. replace (n - S (n - 1 - k)) with k by lia.
+  rewrite nth_map_d with (d' := 0) by (rewrite length_seq; lia). rewrite seq_nth by lia. reflexivity.
+Qed.
+
+Lemma bv_testbit : forall z n, z < 2 ^ n -> bv (Nat.testbit z) n = z.
+Proof.
+  intros z n Hz. apply (bits_eq_nat _ _ n); [apply bv_lt | exact Hz |].
+  intros i Hi. apply testbit_bv. exact Hi.
+Qed.
+
+Lemma bv_compl : forall f n, bv f n + bv (fun i => negb (f i)) n + 1 = 2 ^ n.
+Proof.
+  intros f n. induction n as [|n IH]; [reflexivity|].
+  rewrite !bv_S. cbn [Nat.pow]. destruct (f n); cbn [negb]; lia.
+Qed.
+
+Section Sub.
+Variables x y : nat.
+
+Definition xb (i : nat) : bool := Nat.testbit x i.
+Definition yb (i : nat) : bool := Nat.testbit y i.
+Definition gb (i : nat) : bool := yb i && negb (xb i).
+Definition pg (i : nat) : bool := negb (xb i) || yb i.
+
+Fixpoint carry (k : nat) : bool := match k with O => true | S m => gb m || (pg m && carry m) end.
+
+Definition sumbit (k : nat) : bool := xorb (xorb (yb k) (negb (xb k))) (carry k).
+
+Lemma adder : forall n,
+  bv yb n + bv (fun i => negb (xb i)) n + 1 = bv sumbit n + (if carry n then 2 ^ n else 0).
+Proof.
+  induction n as [|n IH]; [reflexivity|].
+  rewrite !bv_S. cbn [carry Nat.pow]. unfold sumbit, gb, pg in *.
+  destruct (yb n), (xb n), (carry n); cbn [negb xorb andb orb] in *; lia.
+Qed.
+
+Lemma sub_value : forall A, x < 2 ^ A -> y < 2 ^ A -> bv sumbit A = (y + 2 ^ A - x) mod 2 ^ A.
+Proof.
+  intros A Hx Hy. pose proof (adder A) as H. pose proof (bv_compl xb A) as C.
+  change (bv yb A) with (bv (Nat.testbit y) A) in H. rewrite (bv_testbit y A Hy) in H.
+  change (bv xb A) with (bv (Nat.testbit x) A) in C. rewrite (bv_testbit x A Hx) in C.
+  pose proof (bv_lt sumbit A) as L.
+  assert (E : y + 2 ^ A - x = bv sumbit A + (if carry A then 1 else 0) * 2 ^ A)
+    by (destruct (carry A); lia).
+  rewrite E, Nat.Div0.mod_add, Nat.mod_small by exact L. reflexivity.
+Qed.
+
+Lemma sub_bits : forall A k, x < 2 ^ A -> y < 2 ^ A -> k < A ->
+  Nat.testbit ((y + 2 ^ A - x) mod 2 ^ A) k = sumbit k.
+Proof. intros A k Hx Hy Hk. rewrite <- sub_value by assumption. apply testbit_bv. exact Hk. Qed.
+
+Lemma existsb_and_r : forall (T : Type) (g : T -> bool) c l, existsb (fun a => g a && c) l = existsb g l && c.
+Proof.
+  intros T g c l. induction l as [|a l IH]; [reflexivity|]. cbn [existsb]. rewrite IH.
+  destruct (g a), c, (existsb g l); reflexivity.
+Qed.
+
+Lemma forallb_seq_S : forall (f : nat -> bool) m n, forallb f (seq m (S n)) = forallb f (seq m n) && f (m + n).
+Proof. intros f m n. rewrite seq_S, forallb_app. cbn [forallb]. rewrite andb_true_r. reflexivity. Qed.
+
+(* the carry into bit k: all of 0 .. k-1 propagate, or some j generates and j+1 .. k-1 propagate *)
+Lemma carry_closed : forall k,
+  carry k = forallb pg (seq 0 k) || existsb (fun j => gb j && forallb pg (seq (S j) (k - S j))) (seq 0 k).
+Proof.
+  induction k as [|k IH]; [reflexivity|].
+  cbn [carry]. rewrite IH, forallb_seq_S, seq_S, existsb_app. cbn [existsb]. rewrite Nat.add_0_l.
+  replace (S k - S k) with 0 by lia. cbn [seq forallb]. rewrite andb_true_r, orb_false_r.
+  assert (E : existsb (fun j => gb j && forallb pg (seq (S j) (S k - S j))) (seq 0 k)
+              = existsb (fun j => gb j && forallb pg (seq (S j) (k - S j))) (seq 0 k) && pg k).
+  { rewrite (existsb_ext_in _ _ (fun j => (gb j && forallb pg (seq (S j) (k - S j))) && pg k)).
+    - apply (existsb_and_r _ (fun j => gb j && forallb pg (seq (S j) (k - S j)))).
+    - intros j Hj. apply in_seq in Hj. replace (S k - S j) with (S (k - S j)) by lia. rewrite forallb_seq_S.
+      replace (S j + (k - S j)) with k by lia. rewrite andb_assoc. reflexivity. }
+  rewrite E. destruct (pg k), (gb k); cbn [andb orb]; rewrite ?andb_true_r, ?andb_false_r, ?orb_false_r,
+    ?orb_true_r; reflexivity.
+Qed.
+
+End Sub.
+
+Lemma testbit_top : forall r n, 1 <= n -> r < 2 ^ n -> Nat.testbit r (n - 1) = (2 ^ (n - 1) <=? r).
+Proof.
+  intros r n Hn Hr. replace n with (S (n - 1)) in Hr by lia. rewrite Nat.pow_succ_r' in Hr.
+  apply Nat.b2n_inj. rewrite Nat.testbit_spec'.
+  destruct (Nat.leb_spec (2 ^ (n - 1)) r) as [H|H].
+  - assert (D : r / 2 ^ (n - 1) = 1).
+    { symmetry. apply Nat.div_unique with (r - 2 ^ (n - 1)); lia. }
+    rewrite D. reflexivity.
+  - rewrite Nat.div_small by exact H. reflexivity.
+Qed.
+
+Lemma sub_zero : forall A x y, x < 2 ^ A -> y < 2 ^ A -> Nat.eqb ((y + 2 ^ A - x) mod 2 ^ A) 0 = Nat.eqb x y.
+Proof.
+  intros A x y Hx Hy. pose proof (Nat.pow_nonzero 2 A ltac:(lia)) as Hn.
+  destruct (Nat.eqb_spec x y) as [->|E].
+  - replace (y + 2 ^ A - y) with (1 * 2 ^ A) by lia. rewrite Nat.Div0.mod_mul. reflexivity.
+  - apply Nat.eqb_neq. intro Z.
+    destruct (Nat.le_gt_cases x y) as [L|L].
+    + replace (y + 2 ^ A - x) with ((y - x) + 1 * 2 ^ A) in Z by lia.
+      rewrite Nat.Div0.mod_add, Nat.mod_small in Z by lia. lia.
+    + rewrite Nat.mod_small in Z by lia. lia.
+Qed.

rocq/Assumptions.v

@@ -1,5 +1,5 @@
-(* The assumptions of the main theorems, printed by src/check_rocq.py after the build. *)
-From TH Require Import PhysMain PhysFacts NetMain Complete Run PassLemma Main SelfRep.
+(* The assumptions of the main theorems, printed by src/paper.py rocq after the build. *)
+From TH Require Import PhysMain PhysFacts NetMain Complete Run PassLemma Main SelfRep HostSem.
 
 Print Assumptions PhysMain.netlist_step.
 Print Assumptions PhysMain.netlist_step64.
@@ -17,3 +17,4 @@ Print Assumptions Main.every_generation.
 Print Assumptions SelfRep.self_reproduction.
 Print Assumptions SelfRep.second_generation.
 Print Assumptions SelfRep.periodic.
+Print Assumptions HostSem.host_step.

rocq/ExtractHost.v

@@ -0,0 +1,5 @@
+From Stdlib Require Import Extraction ExtrOcamlBasic ExtrOcamlNatInt ExtrOcamlZInt.
+From TH Require Import Net Host.
+Extraction Language OCaml.
+Set Extraction Output Directory "extract".
+Extraction "hostnet.ml" host_units host_next nH.

rocq/Host.v

@@ -0,0 +1,137 @@
+(* The SUBLEQ host H_A as a netlist of ternary threshold units, block by block in the order of
+   the generator, for words of A bits (Construction 3.8), and the machine it computes. *)
+From Stdlib Require Import List Bool Arith ZArith Lia.
+Import ListNotations.
+From TH Require Import TwoHead Net Gates.
+
+Section Host.
+Variable A : nat.
+
+(* the words of memory, and the state bits: the counter, the halt bit, the memory *)
+Definition SW : nat := 2 ^ A.
+Definition nH : nat := A + 1 + SW * A.
+
+(* bit t of an A-bit value, most significant first *)
+Definition bitof (v t : nat) : bool := Nat.testbit v (A - 1 - t).
+
+Definition pcb (i : nat) : sref := SIn i.
+Definition haltb : sref := SIn A.
+Definition mu (j t : nat) : sref := SIn (A + 1 + j * A + t).
+
+(* the literals asserting that the bits f 0 .. f (A - 1), most significant first, spell v *)
+Definition lits (f : nat -> sref) (v : nat) : list lit := map (fun t => (f t, bitof v t)) (seq 0 A).
+
+Definition opb (o t : nat) : sref := SRef 6 (o * A + t) 0.
+Definition xv (i : nat) : sref := SRef 14 (A - 1 - i) 0.
+Definition yv (i : nat) : sref := SRef 15 (A - 1 - i) 0.
+Definition prr (i : nat) : sref := SRef 16 i 0.
+Definition tb : nat := 16 + A.
+
+(* 0 to 16: decode, fetch, operands, reads, propagate signals *)
+Definition blk_P : block := Blk SW 1 (fun j => [sAND (lits pcb j)]).
+Definition blk_HP : block := Blk A 1 (fun i => [sAND [(pcb i, true); (haltb, true)]]).
+Definition blk_FA (o : nat) : block :=
+  Blk (A * SW) 1 (fun m => [sAND [(mu ((m mod SW + o) mod SW) (m / SW), true); (SRef 0 (m mod SW) 0, true)]]).
+Definition blk_Q : block :=
+  Blk A 1 (fun i => [sOR (map (fun j => (SRef 0 j 0, true))
+                              (filter (fun j => bitof ((j + 3) mod SW) i) (seq 0 SW)))]).
+Definition blk_F : block :=
+  Blk (3 * A) 1 (fun m => [sOR (map (fun j => (SRef (2 + m / A) ((m mod A) * SW + j) 0, true)) (seq 0 SW))]).
+Definition blk_PA : block := Blk SW 1 (fun j => [sAND (lits (opb 0) j)]).
+Definition blk_PB : block := Blk SW 1 (fun j => [sAND (lits (opb 1) j)]).
+Definition blk_AC : block := Blk 1 1 (fun _ => [sAND (map (fun t => (opb 2 t, true)) (seq 0 A))]).
+Definition blk_W : block := Blk SW 1 (fun j => [sAND [(haltb, false); (SRef 8 j 0, true)]]).
+Definition blk_RX : block :=
+  Blk (A * SW) 1 (fun m => [sAND [(mu (m mod SW) (m / SW), true); (SRef 7 (m mod SW) 0, true)]]).
+Definition blk_RY : block :=
+  Blk (A * SW) 1 (fun m => [sAND [(mu (m mod SW) (m / SW), true); (SRef 8 (m mod SW) 0, true)]]).
+Definition blk_KP : block :=
+  Blk (SW * A) 1 (fun m => [sAND [(mu (m / A) (m mod A), true); (SRef 10 (m / A) 0, false)]]).
+Definition blk_X : block := Blk A 1 (fun t => [sOR (map (fun j => (SRef 11 (t * SW + j) 0, true)) (seq 0 SW))]).
+Definition blk_Y : block := Blk A 1 (fun t => [sOR (map (fun j => (SRef 12 (t * SW + j) 0, true)) (seq 0 SW))]).
+Definition blk_PR : block := Blk (A - 1) 1 (fun i => [sOR [(xv i, false); (yv i, true)]]).
+
+(* 17 to 15 + A: the carry terms into bit k, for k = 1 .. A - 1 *)
+Definition blk_T (k : nat) : block :=
+  Blk 1 (S k) (fun _ => sAND (map (fun i => (prr i, true)) (seq 0 k))
+                        :: map (fun j => sAND ([(yv j, true); (xv j, false)]
+                                               ++ map (fun i => (prr i, true)) (seq (S j) (k - S j))))
+                               (seq 0 k)).
+
+(* tb to tb + 14: carries, equality, sum bits, branch, next counter, halt latch, next memory *)
+Definition blk_C : block :=
+  Blk (A - 1) 1 (fun m => [sOR ((SRef (16 + S m) 0 0, true)
+                                :: map (fun j => (SRef (16 + S m) 0 (S j), true)) (seq 0 (S m)))]).
+Definition blk_AX : block := Blk A 1 (fun i => [sAND [(xv i, true); (yv i, true)]]).
+Definition blk_NX : block := Blk A 1 (fun i => [sAND [(xv i, false); (yv i, false)]]).
+Definition blk_XN : block := Blk A 1 (fun i => [sOR [(SRef (tb + 1) i 0, true); (SRef (tb + 2) i 0, true)]]).
+Definition blk_EQ : block := Blk 1 1 (fun _ => [sAND (map (fun i => (SRef (tb + 3) i 0, true)) (seq 0 A))]).
+Definition blk_R0 : block :=
+  Blk 1 3 (fun _ => [sOR [(yv 0, true); (xv 0, true)]; sOR [(yv 0, false); (xv 0, false)];
+                     sAND [(SRef (tb + 5) 0 0, true); (SRef (tb + 5) 0 1, true)]]).
+Definition blk_H : block :=
+  Blk (A - 1) 3 (fun m => map (fun b => SU b [(yv (S m), 1%Z); (xv (S m), (-1)%Z); (SRef tb m 0, 1%Z)])
+                              [0%Z; (-1)%Z; (-2)%Z]).
+Definition blk_R : block :=
+  Blk (A - 1) 1 (fun m => [SU (-1) [(SRef (tb + 6) m 0, 1%Z); (SRef (tb + 6) m 1, (-1)%Z);
+                                     (SRef (tb + 6) m 2, 1%Z)]]).
+Definition blk_LEQ : block :=
+  Blk 1 1 (fun _ => [SU (-1) [(SRef (tb + 6) (A - 2) 0, 1%Z); (SRef (tb + 6) (A - 2) 1, (-1)%Z);
+                              (SRef (tb + 6) (A - 2) 2, 1%Z); (SRef (tb + 4) 0 0, 1%Z)]]).
+Definition rbit (k : nat) : sref := if Nat.eqb k 0 then SRef (tb + 5) 0 2 else SRef (tb + 7) (k - 1) 0.
+Definition blk_TA : block :=
+  Blk A 1 (fun i => [sAND [(haltb, false); (SRef (tb + 8) 0 0, true); (opb 2 i, true)]]).
+Definition blk_TB : block :=
+  Blk A 1 (fun i => [sAND [(haltb, false); (SRef (tb + 8) 0 0, false); (SRef 5 i 0, true)]]).
+Definition blk_NP : block :=
+  Blk A 1 (fun i => [sOR [(SRef 1 i 0, true); (SRef (tb + 9) i 0, true); (SRef (tb + 10) i 0, true)]]).
+Definition blk_HAB : block :=
+  Blk 1 3 (fun _ => [sAND [(haltb, false); (SRef (tb + 8) 0 0, true); (SRef 9 0 0, true)];
+                     sAND [(haltb, false); (SRef (tb + 8) 0 0, false); (SRef 0 (SW - 4) 0, true)];
+                     sOR [(haltb, true); (SRef (tb + 12) 0 0, true); (SRef (tb + 12) 0 1, true)]]).
+Definition blk_WR : block :=
+  Blk (SW * A) 1 (fun m => [sAND [(rbit (A - 1 - m mod A), true); (SRef 10 (m / A) 0, true)]]).
+Definition blk_NM : block := Blk (SW * A) 1 (fun m => [sOR [(SRef 13 m 0, true); (SRef (tb + 13) m 0, true)]]).
+
+Definition hpre : list block :=
+  [blk_P; blk_HP; blk_FA 0; blk_FA 1; blk_FA 2; blk_Q; blk_F; blk_PA; blk_PB; blk_AC; blk_W; blk_RX; blk_RY;
+   blk_KP; blk_X; blk_Y; blk_PR].
+Definition hpost : list block :=
+  [blk_C; blk_AX; blk_NX; blk_XN; blk_EQ; blk_R0; blk_H; blk_R; blk_LEQ; blk_TA; blk_TB; blk_NP; blk_HAB;
+   blk_WR; blk_NM].
+Definition hblocks : list block := hpre ++ map blk_T (seq 1 (A - 1)) ++ hpost.
+
+(* the unit computing the next value of each state bit *)
+Definition hout (i : nat) : sref :=
+  if i <? A then SRef (tb + 11) i 0
+  else if Nat.eqb i A then SRef (tb + 12) 0 2
+  else SRef (tb + 14) (i - A - 1) 0.
+
+Definition host_units : list tu := compile nH hblocks.
+Definition host_next : list nat := map (fun i => idx nH hblocks (hout i)) (seq 0 nH).
+
+(* ---- the machine: SUBLEQ on 2^A words of A bits, Definition 3.1 ------------------------ *)
+Record hst := mkH { hpc : nat; hhalt : bool; hmem : list nat }.
+
+Definition memv (s : hst) (j : nat) : nat := nth j (hmem s) 0.
+
+Definition subleq (s : hst) : hst :=
+  if hhalt s then s
+  else
+    let p := hpc s in
+    let a := memv s p in
+    let b := memv s ((p + 1) mod SW) in
+    let c := memv s ((p + 2) mod SW) in
+    let r := (memv s b + SW - memv s a) mod SW in
+    let leq := Nat.eqb r 0 || Nat.leb (2 ^ (A - 1)) r in
+    let p' := if leq then c else (p + 3) mod SW in
+    mkH p' (Nat.eqb p' (SW - 1)) (map (fun j => if Nat.eqb j b then r else memv s j) (seq 0 SW)).
+
+(* the state bits: the counter and each word most significant bit first *)
+Definition wbits (v : nat) : list bool := map (bitof v) (seq 0 A).
+Definition encodeH (s : hst) : list bool := wbits (hpc s) ++ [hhalt s] ++ concat (map wbits (hmem s)).
+
+Definition hvalid (s : hst) : Prop :=
+  hpc s < SW /\ length (hmem s) = SW /\ Forall (fun v => v < SW) (hmem s).
+
+End Host.

rocq/HostSem.v

@@ -0,0 +1,555 @@
+(* The host netlist computes one step of SUBLEQ on 2^A words of A bits, from every state, for
+   every A >= 3 (Proposition 3.9). *)
+From Stdlib Require Import List Bool Arith ZArith Lia.
+Import ListNotations.
+From TH Require Import TwoHead Net Gates PhysSem Host HostWF Adder.
+
+(* ---- the state bits ----------------------------------------------------------------- *)
+Lemma length_wbits : forall A v, length (wbits A v) = A.
+Proof. intros A v. unfold wbits. rewrite length_map, length_seq. reflexivity. Qed.
+
+Lemma nth_wbits : forall A v t, t < A -> nth t (wbits A v) false = bitof A v t.
+Proof.
+  intros A v t Ht. unfold wbits. rewrite nth_map_d with (d' := 0) by (rewrite length_seq; lia).
+  rewrite seq_nth by lia. reflexivity.
+Qed.
+
+Lemma length_encodeH : forall A s, length (hmem s) = SW A -> length (encodeH A s) = nH A.
+Proof.
+  intros A s H. unfold encodeH, nH. rewrite !length_app, length_wbits. cbn [length].
+  rewrite (length_concat_const _ _ A).
+  - rewrite length_map, H. lia.
+  - apply Forall_forall. intros l Hl. apply in_map_iff in Hl as (v & <- & _). apply length_wbits.
+Qed.
+
+Lemma nth_encodeH_pc : forall A s i, i < A -> nth i (encodeH A s) false = bitof A (hpc s) i.
+Proof. intros A s i Hi. unfold encodeH. rewrite app_nth1 by (rewrite length_wbits; lia). apply nth_wbits. exact Hi. Qed.
+
+Lemma nth_encodeH_halt : forall A s, nth A (encodeH A s) false = hhalt s.
+Proof.
+  intros A s. unfold encodeH. rewrite app_nth2 by (rewrite length_wbits; lia).
+  rewrite length_wbits, Nat.sub_diag. reflexivity.
+Qed.
+
+Lemma nth_encodeH_mem : forall A s j t, length (hmem s) = SW A -> j < SW A -> t < A ->
+  nth (A + 1 + j * A + t) (encodeH A s) false = bitof A (memv s j) t.
+Proof.
+  intros A s j t Hl Hj Ht. unfold encodeH. rewrite app_nth2 by (rewrite length_wbits; lia). rewrite length_wbits.
+  replace (A + 1 + j * A + t - A) with (S (A * j + t)) by lia. cbn [app nth].
+  rewrite (nth_concat_const _ false (map (wbits A) (hmem s)) A j t).
+  - rewrite nth_map_d with (d' := 0) by lia. apply nth_wbits. exact Ht.
+  - apply Forall_forall. intros l Hl'. apply in_map_iff in Hl' as (v & <- & _). apply length_wbits.
+  - rewrite length_map. lia.
+  - exact Ht.
+Qed.
+
+(* ---- addresses ---------------------------------------------------------------------- *)
+Lemma bits_eqb : forall A p j, p < 2 ^ A -> j < 2 ^ A ->
+  forallb (fun t => Bool.eqb (bitof A p t) (bitof A j t)) (seq 0 A) = Nat.eqb p j.
+Proof.
+  intros A p j Hp Hj. destruct (Nat.eqb_spec p j) as [->|E].
+  - apply forallb_forall. intros t _. apply eqb_reflx.
+  - apply Bool.not_true_is_false. intro F. apply E. apply (bits_eq_nat _ _ A Hp Hj).
+    intros i Hi. rewrite forallb_forall in F. specialize (F (A - 1 - i) ltac:(apply in_seq; lia)).
+    apply Bool.eqb_prop in F. unfold bitof in F. replace (A - 1 - (A - 1 - i)) with i in F by lia. exact F.
+Qed.
+
+Lemma testbits_eqb : forall A x y, x < 2 ^ A -> y < 2 ^ A ->
+  forallb (fun i => Bool.eqb (Nat.testbit x i) (Nat.testbit y i)) (seq 0 A) = Nat.eqb x y.
+Proof.
+  intros A x y Hx Hy. destruct (Nat.eqb_spec x y) as [->|E].
+  - apply forallb_forall. intros t _. apply eqb_reflx.
+  - apply Bool.not_true_is_false. intro F. apply E. apply (bits_eq_nat _ _ A Hx Hy).
+    intros i Hi. rewrite forallb_forall in F. specialize (F i ltac:(apply in_seq; lia)).
+    apply Bool.eqb_prop in F. exact F.
+Qed.
+
+Lemma lits_fire : forall A (V : sref -> bool) f v w, v < 2 ^ A -> w < 2 ^ A ->
+  (forall t, t < A -> V (f t) = bitof A w t) -> forallb (litv V) (lits A f v) = Nat.eqb w v.
+Proof.
+  intros A V f v w Hv Hw H. unfold lits. rewrite forallb_map', <- (bits_eqb A w v Hw Hv).
+  apply forallb_ext_in. intros t Ht. apply in_seq in Ht. unfold litv. cbn [fst snd]. rewrite H by lia. reflexivity.
+Qed.
+
+Lemma all_ones : forall A w, w < 2 ^ A -> forallb (bitof A w) (seq 0 A) = Nat.eqb w (2 ^ A - 1).
+Proof.
+  intros A w Hw. rewrite <- (bits_eqb A w (2 ^ A - 1) Hw) by lia.
+  apply forallb_ext_in. intros t Ht. apply in_seq in Ht.
+  assert (B : bitof A (2 ^ A - 1) t = true).
+  { unfold bitof. replace (2 ^ A - 1) with (Nat.ones A) by (rewrite Nat.ones_equiv; lia).
+    apply Nat.ones_spec_low. lia. }
+  rewrite B. destruct (bitof A w t); reflexivity.
+Qed.
+
+Lemma existsb_filter_eq : forall (f : nat -> bool) p n, p < n ->
+  existsb (fun j => Nat.eqb p j) (filter f (seq 0 n)) = f p.
+Proof.
+  intros f p n Hp. assert (E : forall l, existsb (fun j => Nat.eqb p j) (filter f l) = existsb (fun j => Nat.eqb p j && f j) l).
+  { induction l as [|a l IH]; [reflexivity|]. cbn [filter existsb]. destruct (f a) eqn:Fa; cbn [existsb];
+      rewrite IH; destruct (Nat.eqb p a); reflexivity. }
+  rewrite E, existsb_pick. replace ((0 <=? p) && (p <? 0 + n)) with true by (symmetry; apply andb_true_iff; split;
+    [apply Nat.leb_le | apply Nat.ltb_lt]; lia). reflexivity.
+Qed.
+
+Lemma existsb_pick_r : forall (g : nat -> bool) c n, c < n ->
+  existsb (fun a => g a && Nat.eqb c a) (seq 0 n) = g c.
+Proof.
+  intros g c n Hc. rewrite (existsb_ext_in _ _ (fun a => Nat.eqb c a && g a)) by (intros a _; apply andb_comm).
+  rewrite existsb_pick. replace ((0 <=? c) && (c <? 0 + n)) with true by (symmetry; apply andb_true_iff; split;
+    [apply Nat.leb_le | apply Nat.ltb_lt]; lia). reflexivity.
+Qed.
+
+(* ---- the step, block by block --------------------------------------------------------- *)
+Section HSem.
+Variables (A : nat) (s : hst).
+Hypotheses (HA : 3 <= A) (Hv : hvalid A s).
+
+Let HS : 8 <= SW A := SW_ge A HA.
+
+Definition hp : nat := hpc s.
+Definition hh : bool := hhalt s.
+Definition mv (j : nat) : nat := memv s j.
+
+Lemma hp_lt : hp < SW A.
+Proof. destruct Hv as (H & _ & _). exact H. Qed.
+
+Lemma mv_lt : forall j, j < SW A -> mv j < SW A.
+Proof.
+  destruct Hv as (_ & Hl & Hf). intros j Hj. unfold mv, memv. rewrite Forall_forall in Hf.
+  apply Hf. apply nth_In. lia.
+Qed.
+
+Definition HX (i : nat) : bool := nth i (encodeH A s) false.
+Definition HF (x : sref) : bool := run (host_units A) (nH A) HX (idx (nH A) (hblocks A) x).
+
+Lemma HX_pc : forall i, i < A -> HX i = bitof A hp i.
+Proof. intros i Hi. apply nth_encodeH_pc. exact Hi. Qed.
+
+Lemma HX_mu : forall j t, j < SW A -> t < A -> HX (A + 1 + j * A + t) = bitof A (mv j) t.
+Proof. destruct Hv as (_ & Hl & _). intros j t Hj Ht. apply nth_encodeH_mem; assumption. Qed.
+
+Lemma HF_in : forall i, i < nH A -> HF (SIn i) = HX i.
+Proof. intros i H. unfold HF, host_units. apply net_in. exact H. Qed.
+
+Lemma HF_pc : forall i, i < A -> HF (pcb i) = bitof A hp i.
+Proof. intros i Hi. unfold pcb. rewrite HF_in by (unfold nH; lia). apply HX_pc. exact Hi. Qed.
+
+Lemma HF_halt : HF (haltb A) = hh.
+Proof. unfold haltb. rewrite HF_in by (unfold nH; lia). apply nth_encodeH_halt. Qed.
+
+Lemma HF_mu : forall j t, j < SW A -> t < A -> HF (mu A j t) = bitof A (mv j) t.
+Proof. intros j t Hj Ht. unfold mu. rewrite HF_in by (unfold nH; nia). apply HX_mu; assumption. Qed.
+
+Lemma HF_unit : forall b j r, b < length (hblocks A) ->
+  j < bcount (nth b (hblocks A) blk0) -> r < bsize (nth b (hblocks A) blk0) ->
+  HF (SRef b j r) = sfire' (sunit (hblocks A) b j r) HF.
+Proof.
+  intros b j r Hb Hj Hr. unfold HF, host_units.
+  apply net_unit; [apply host_wf; exact HA | exact Hb | exact Hj | exact Hr].
+Qed.
+
+(* the units of the blocks before the carry terms, after them, and the carry terms *)
+Lemma HF_pre : forall b j r, b < 17 -> j < bcount (nth b (hpre A) blk0) -> r < bsize (nth b (hpre A) blk0) ->
+  HF (SRef b j r) = sfire' (nth r (bshape (nth b (hpre A) blk0) j) su0) HF.
+Proof.
+  intros b j r Hb Hj Hr. rewrite HF_unit; unfold sunit; rewrite ?nth_hb_pre by exact Hb; try reflexivity; try assumption.
+  rewrite length_hblocks by lia. unfold tb. lia.
+Qed.
+
+Lemma HF_post : forall i j r, i < 15 -> j < bcount (nth i (hpost A) blk0) -> r < bsize (nth i (hpost A) blk0) ->
+  HF (SRef (tb A + i) j r) = sfire' (nth r (bshape (nth i (hpost A) blk0) j) su0) HF.
+Proof.
+  intros i j r Hi Hj Hr. rewrite HF_unit; unfold sunit; rewrite ?nth_hb_post by lia; try reflexivity; try assumption.
+  rewrite length_hblocks by lia. lia.
+Qed.
+
+Lemma HF_Tu : forall k r, 1 <= k -> k < A -> r < S k ->
+  HF (SRef (16 + k) 0 r) = sfire' (nth r (bshape (blk_T A k) 0) su0) HF.
+Proof.
+  intros k r H1 H2 H3. rewrite HF_unit; unfold sunit; rewrite ?nth_hb_T by assumption; try reflexivity.
+  - rewrite length_hblocks by lia. unfold tb. lia.
+  - cbn [bcount blk_T]. lia.
+  - cbn [bsize blk_T]. exact H3.
+Qed.
+
+Ltac pre_fire b := rewrite (HF_pre b) by (cbn [nth hpre bcount bsize blk_P blk_HP blk_FA blk_Q blk_F blk_PA blk_PB
+  blk_AC blk_W blk_RX blk_RY blk_KP blk_X blk_Y blk_PR]; nia);
+  cbn [nth hpre bshape blk_P blk_HP blk_FA blk_Q blk_F blk_PA blk_PB blk_AC blk_W blk_RX blk_RY blk_KP blk_X blk_Y
+       blk_PR].
+
+Ltac post_fire i := rewrite (HF_post i) by (cbn [nth hpost bcount bsize blk_C blk_AX blk_NX blk_XN blk_EQ blk_R0
+  blk_H blk_R blk_LEQ blk_TA blk_TB blk_NP blk_HAB blk_WR blk_NM]; nia);
+  cbn [nth hpost bshape blk_C blk_AX blk_NX blk_XN blk_EQ blk_R0 blk_H blk_R blk_LEQ blk_TA blk_TB blk_NP blk_HAB
+       blk_WR blk_NM].
+
+(* 0: decode lines of the counter *)
+Lemma HF_P : forall j, j < SW A -> HF (SRef 0 j 0) = Nat.eqb hp j.
+Proof.
+  intros j Hj. pre_fire 0. rewrite sAND_fire. apply (lits_fire A HF (pcb) j hp Hj hp_lt).
+  intros t Ht. apply HF_pc. exact Ht.
+Qed.
+
+(* 1 *)
+Lemma HF_HP : forall i, i < A -> HF (SRef 1 i 0) = bitof A hp i && hh.
+Proof.
+  intros i Hi. pre_fire 1. rewrite sAND_fire. cbn [forallb]. rewrite !litv_pos, HF_pc, HF_halt by exact Hi.
+  rewrite andb_true_r. reflexivity.
+Qed.
+
+(* 2, 3, 4: the fetch conjunctions *)
+Lemma HF_FA : forall o m, o < 3 -> m < A * SW A ->
+  HF (SRef (2 + o) m 0) = bitof A (mv ((m mod SW A + o) mod SW A)) (m / SW A) && Nat.eqb hp (m mod SW A).
+Proof.
+  intros o m Ho Hm. pose proof (Nat.mod_upper_bound m (SW A) ltac:(lia)).
+  pose proof (Nat.Div0.div_lt_upper_bound m (SW A) A ltac:(lia)).
+  assert (E : HF (SRef (2 + o) m 0)
+              = forallb (litv HF) [(mu A ((m mod SW A + o) mod SW A) (m / SW A), true); (SRef 0 (m mod SW A) 0, true)]).
+  { destruct o as [|[|[|o]]]; [pre_fire 2 | pre_fire 3 | pre_fire 4 | lia]; apply sAND_fire. }
+  rewrite E. cbn [forallb]. rewrite !litv_pos, andb_true_r.
+  rewrite HF_mu by (try apply Nat.mod_upper_bound; lia). rewrite HF_P by lia. reflexivity.
+Qed.
+
+(* 5: the bits of p + 3 *)
+Lemma HF_Q : forall i, i < A -> HF (SRef 5 i 0) = bitof A ((hp + 3) mod SW A) i.
+Proof.
+  intros i Hi. pre_fire 5. rewrite sOR_fire, existsb_map'.
+  rewrite (existsb_ext_in _ _ (fun j => Nat.eqb hp j)).
+  - apply (existsb_filter_eq (fun j => bitof A ((j + 3) mod SW A) i) hp (SW A) hp_lt).
+  - intros j Hj. apply filter_In in Hj as [Hj _]. apply in_seq in Hj. rewrite litv_pos. apply HF_P. lia.
+Qed.
+
+(* 6: the operands *)
+Lemma HF_F : forall m, m < 3 * A -> HF (SRef 6 m 0) = bitof A (mv ((hp + m / A) mod SW A)) (m mod A).
+Proof.
+  intros m Hm. pose proof (Nat.Div0.div_lt_upper_bound m A 3 ltac:(lia)). pose proof (Nat.mod_upper_bound m A ltac:(lia)).
+  pre_fire 6. rewrite sOR_fire, existsb_map'.
+  rewrite (existsb_ext_in _ _ (fun j => bitof A (mv ((j + m / A) mod SW A)) (m mod A) && Nat.eqb hp j)).
+  - apply (existsb_pick_r (fun j => bitof A (mv ((j + m / A) mod SW A)) (m mod A))). exact hp_lt.
+  - intros j Hj. apply in_seq in Hj. rewrite litv_pos. rewrite HF_FA by (try lia; nia).
+    replace ((m mod A * SW A + j) mod SW A) with j
+      by (rewrite (Nat.add_comm (m mod A * SW A) j), Nat.Div0.mod_add, Nat.mod_small by lia; reflexivity).
+    replace ((m mod A * SW A + j) / SW A) with (m mod A)
+      by (rewrite (Nat.add_comm (m mod A * SW A) j), Nat.div_add, Nat.div_small by lia; lia).
+    reflexivity.
+Qed.
+
+Definition ha : nat := mv hp.
+Definition hb : nat := mv ((hp + 1) mod SW A).
+Definition hc : nat := mv ((hp + 2) mod SW A).
+
+Lemma ha_lt : ha < SW A.
+Proof. apply mv_lt. exact hp_lt. Qed.
+Lemma hb_lt : hb < SW A.
+Proof. apply mv_lt. apply Nat.mod_upper_bound. lia. Qed.
+Lemma hc_lt : hc < SW A.
+Proof. apply mv_lt. apply Nat.mod_upper_bound. lia. Qed.
+
+Lemma HF_opb : forall o t, o < 3 -> t < A -> HF (opb A o t) = bitof A (mv ((hp + o) mod SW A)) t.
+Proof.
+  intros o t Ho Ht. unfold opb. rewrite HF_F by nia.
+  replace ((o * A + t) / A) with o by (rewrite Nat.add_comm, Nat.div_add, Nat.div_small by lia; lia).
+  replace ((o * A + t) mod A) with t by (rewrite Nat.add_comm, Nat.Div0.mod_add, Nat.mod_small by lia; reflexivity).
+  reflexivity.
+Qed.
+
+Lemma HF_opa : forall t, t < A -> HF (opb A 0 t) = bitof A ha t.
+Proof. intros t Ht. rewrite HF_opb by lia. rewrite Nat.add_0_r, Nat.mod_small by exact hp_lt. reflexivity. Qed.
+
+(* 7, 8: decode lines of A and B *)
+Lemma HF_PA : forall j, j < SW A -> HF (SRef 7 j 0) = Nat.eqb ha j.
+Proof.
+  intros j Hj. pre_fire 7. rewrite sAND_fire. apply (lits_fire A HF (opb A 0) j ha Hj ha_lt).
+  intros t Ht. apply HF_opa. exact Ht.
+Qed.
+
+Lemma HF_PB : forall j, j < SW A -> HF (SRef 8 j 0) = Nat.eqb hb j.
+Proof.
+  intros j Hj. pre_fire 8. rewrite sAND_fire. apply (lits_fire A HF (opb A 1) j hb Hj hb_lt).
+  intros t Ht. rewrite HF_opb by lia. reflexivity.
+Qed.
+
+(* 9: C is the halt address *)
+Lemma HF_AC : HF (SRef 9 0 0) = Nat.eqb hc (SW A - 1).
+Proof.
+  pre_fire 9. rewrite sAND_fire, forallb_map'. unfold SW. rewrite <- all_ones by exact hc_lt.
+  apply forallb_ext_in. intros t Ht. apply in_seq in Ht. rewrite litv_pos, HF_opb by lia. reflexivity.
+Qed.
+
+(* 10: write enables *)
+Lemma HF_W : forall j, j < SW A -> HF (SRef 10 j 0) = negb hh && Nat.eqb hb j.
+Proof.
+  intros j Hj. pre_fire 10. rewrite sAND_fire. cbn [forallb]. rewrite litv_neg, litv_pos, HF_halt, HF_PB by exact Hj.
+  rewrite andb_true_r. reflexivity.
+Qed.
+
+(* 11, 12: read conjunctions *)
+Lemma HF_RX : forall m, m < A * SW A ->
+  HF (SRef 11 m 0) = bitof A (mv (m mod SW A)) (m / SW A) && Nat.eqb ha (m mod SW A).
+Proof.
+  intros m Hm. pose proof (Nat.mod_upper_bound m (SW A) ltac:(lia)).
+  pose proof (Nat.Div0.div_lt_upper_bound m (SW A) A ltac:(lia)).
+  pre_fire 11. rewrite sAND_fire. cbn [forallb]. rewrite !litv_pos, HF_mu, HF_PA by lia. rewrite andb_true_r. reflexivity.
+Qed.
+
+Lemma HF_RY : forall m, m < A * SW A ->
+  HF (SRef 12 m 0) = bitof A (mv (m mod SW A)) (m / SW A) && Nat.eqb hb (m mod SW A).
+Proof.
+  intros m Hm. pose proof (Nat.mod_upper_bound m (SW A) ltac:(lia)).
+  pose proof (Nat.Div0.div_lt_upper_bound m (SW A) A ltac:(lia)).
+  pre_fire 12. rewrite sAND_fire. cbn [forallb]. rewrite !litv_pos, HF_mu, HF_PB by lia. rewrite andb_true_r. reflexivity.
+Qed.
+
+(* 13: the cells kept *)
+Lemma HF_KP : forall m, m < SW A * A ->
+  HF (SRef 13 m 0) = bitof A (mv (m / A)) (m mod A) && negb (negb hh && Nat.eqb hb (m / A)).
+Proof.
+  intros m Hm. pose proof (Nat.mod_upper_bound m A ltac:(lia)).
+  pose proof (Nat.Div0.div_lt_upper_bound m A (SW A) ltac:(lia)).
+  pre_fire 13. rewrite sAND_fire. cbn [forallb]. rewrite litv_pos, litv_neg, HF_mu, HF_W by lia.
+  rewrite andb_true_r. reflexivity.
+Qed.
+
+(* 14, 15: x = M[A], y = M[B] *)
+Definition hx : nat := mv ha.
+Definition hy : nat := mv hb.
+
+Lemma HF_X : forall t, t < A -> HF (SRef 14 t 0) = bitof A hx t.
+Proof.
+  intros t Ht. pre_fire 14. rewrite sOR_fire, existsb_map'.
+  rewrite (existsb_ext_in _ _ (fun j => bitof A (mv j) t && Nat.eqb ha j)).
+  - apply (existsb_pick_r (fun j => bitof A (mv j) t)). exact ha_lt.
+  - intros j Hj. apply in_seq in Hj. rewrite litv_pos, HF_RX by nia.
+    rewrite (Nat.add_comm (t * SW A) j), Nat.Div0.mod_add, Nat.mod_small by lia.
+    replace ((j + t * SW A) / SW A) with t by (rewrite Nat.div_add, Nat.div_small by lia; lia).
+    reflexivity.
+Qed.
+
+Lemma HF_Y : forall t, t < A -> HF (SRef 15 t 0) = bitof A hy t.
+Proof.
+  intros t Ht. pre_fire 15. rewrite sOR_fire, existsb_map'.
+  rewrite (existsb_ext_in _ _ (fun j => bitof A (mv j) t && Nat.eqb hb j)).
+  - apply (existsb_pick_r (fun j => bitof A (mv j) t)). exact hb_lt.
+  - intros j Hj. apply in_seq in Hj. rewrite litv_pos, HF_RY by nia.
+    rewrite (Nat.add_comm (t * SW A) j), Nat.Div0.mod_add, Nat.mod_small by lia.
+    replace ((j + t * SW A) / SW A) with t by (rewrite Nat.div_add, Nat.div_small by lia; lia).
+    reflexivity.
+Qed.
+
+Lemma HF_xv : forall i, i < A -> HF (xv A i) = Nat.testbit hx i.
+Proof. intros i Hi. unfold xv. rewrite HF_X by lia. unfold bitof. f_equal. lia. Qed.
+
+Lemma HF_yv : forall i, i < A -> HF (yv A i) = Nat.testbit hy i.
+Proof. intros i Hi. unfold yv. rewrite HF_Y by lia. unfold bitof. f_equal. lia. Qed.
+
+(* 16: propagate signals *)
+Lemma HF_PR : forall i, i < A - 1 -> HF (prr i) = pg hx hy i.
+Proof.
+  intros i Hi. unfold prr. pre_fire 16. rewrite sOR_fire. cbn [existsb]. rewrite litv_neg, litv_pos, HF_xv, HF_yv by lia.
+  rewrite orb_false_r. reflexivity.
+Qed.
+
+(* 17 to 15 + A: the carry terms *)
+Lemma HF_Tn : forall k, 1 <= k -> k < A -> HF (SRef (16 + k) 0 0) = forallb (pg hx hy) (seq 0 k).
+Proof.
+  intros k H1 H2. rewrite HF_Tu by lia. cbn [bshape blk_T nth]. rewrite sAND_fire, forallb_map'.
+  apply forallb_ext_in. intros i Hi. apply in_seq in Hi. rewrite litv_pos. apply HF_PR. lia.
+Qed.
+
+Lemma HF_Tj : forall k j, 1 <= k -> k < A -> j < k ->
+  HF (SRef (16 + k) 0 (S j)) = gb hx hy j && forallb (pg hx hy) (seq (S j) (k - S j)).
+Proof.
+  intros k j H1 H2 H3. rewrite HF_Tu by lia. cbn [bshape blk_T nth].
+  rewrite nth_map_d with (d' := 0) by (rewrite length_seq; lia). rewrite seq_nth by lia.
+  rewrite sAND_fire. cbn [Nat.add forallb]. rewrite forallb_app. cbn [forallb].
+  rewrite litv_pos, litv_neg, HF_xv, HF_yv by lia. rewrite andb_true_r, forallb_map'.
+  rewrite (forallb_ext_in _ _ (pg hx hy)).
+  - unfold gb, xb, yb. reflexivity.
+  - intros i Hi. apply in_seq in Hi. rewrite litv_pos. apply HF_PR. lia.
+Qed.
+
+(* tb: carries *)
+Lemma HF_C : forall m, m < A - 1 -> HF (SRef (tb A) m 0) = carry hx hy (S m).
+Proof.
+  intros m Hm. rewrite <- (Nat.add_0_r (tb A)). post_fire 0. rewrite sOR_fire. cbn [existsb]. rewrite litv_pos.
+  rewrite HF_Tn by lia. rewrite existsb_map'.
+  rewrite (existsb_ext_in _ _ (fun j => gb hx hy j && forallb (pg hx hy) (seq (S j) (S m - S j)))).
+  - rewrite carry_closed. reflexivity.
+  - intros j Hj. apply in_seq in Hj. rewrite litv_pos. apply HF_Tj; lia.
+Qed.
+
+(* tb + 1 to tb + 4: equality *)
+Lemma HF_XN : forall i, i < A -> HF (SRef (tb A + 3) i 0) = Bool.eqb (Nat.testbit hx i) (Nat.testbit hy i).
+Proof.
+  intros i Hi. post_fire 3. rewrite sOR_fire. cbn [existsb]. rewrite !litv_pos, orb_false_r.
+  post_fire 1. post_fire 2. rewrite !sAND_fire. cbn [forallb]. rewrite !litv_pos, !litv_neg, HF_xv, HF_yv by lia.
+  destruct (Nat.testbit hx i), (Nat.testbit hy i); reflexivity.
+Qed.
+
+Lemma HF_EQ : HF (SRef (tb A + 4) 0 0) = Nat.eqb hx hy.
+Proof.
+  post_fire 4. rewrite sAND_fire, forallb_map'. unfold SW in *.
+  rewrite <- (testbits_eqb A hx hy) by (apply mv_lt; first [exact ha_lt | exact hb_lt]).
+  apply forallb_ext_in. intros i Hi. apply in_seq in Hi. rewrite litv_pos. apply HF_XN. lia.
+Qed.
+
+(* tb + 5 to tb + 7: the sum bits *)
+Lemma HF_R0 : HF (SRef (tb A + 5) 0 2) = sumbit hx hy 0.
+Proof.
+  post_fire 5. rewrite sAND_fire. cbn [forallb]. rewrite !litv_pos, andb_true_r.
+  post_fire 5. post_fire 5. rewrite !sOR_fire. cbn [existsb]. rewrite !litv_pos, !litv_neg, HF_xv, HF_yv by lia.
+  unfold sumbit, xb, yb. cbn [carry]. destruct (Nat.testbit hx 0), (Nat.testbit hy 0); reflexivity.
+Qed.
+
+Definition cnt (k : nat) : nat :=
+  (if yb hy k then 1 else 0) + (if xb hx k then 0 else 1) + (if carry hx hy k then 1 else 0).
+
+Lemma HF_H : forall m u, m < A - 1 -> u < 3 -> HF (SRef (tb A + 6) m u) = Nat.leb (S u) (cnt (S m)).
+Proof.
+  intros m u Hm Hu. post_fire 6. rewrite nth_map_d with (d' := 0%Z) by (cbn [length]; lia).
+  unfold sfire'. cbn [sb sin swsum]. rewrite HF_xv, HF_yv by lia. rewrite HF_C by lia.
+  unfold cnt, xb, yb. destruct u as [|[|[|u]]]; [| | | lia]; cbn [nth];
+    destruct (Nat.testbit hy (S m)), (Nat.testbit hx (S m)), (carry hx hy (S m)); reflexivity.
+Qed.
+
+Lemma HF_R : forall m, m < A - 1 -> HF (SRef (tb A + 7) m 0) = sumbit hx hy (S m).
+Proof.
+  intros m Hm. post_fire 7. unfold sfire'. cbn [sb sin swsum]. rewrite !HF_H by lia.
+  unfold sumbit, cnt, xb, yb. destruct (Nat.testbit hy (S m)), (Nat.testbit hx (S m)), (carry hx hy (S m)); reflexivity.
+Qed.
+
+Lemma HF_rbit : forall k, k < A -> HF (rbit A k) = sumbit hx hy k.
+Proof.
+  intros k Hk. unfold rbit. destruct (Nat.eqb_spec k 0) as [->|E]; [apply HF_R0|].
+  rewrite HF_R by lia. f_equal. lia.
+Qed.
+
+(* the difference and the branch *)
+Definition hr : nat := (hy + SW A - hx) mod SW A.
+Definition hleq : bool := Nat.eqb hr 0 || Nat.leb (2 ^ (A - 1)) hr.
+
+Lemma hx_lt : hx < 2 ^ A.
+Proof. apply mv_lt. exact ha_lt. Qed.
+Lemma hy_lt : hy < 2 ^ A.
+Proof. apply mv_lt. exact hb_lt. Qed.
+
+Lemma hr_bits : forall k, k < A -> Nat.testbit hr k = sumbit hx hy k.
+Proof. intros k Hk. unfold hr, SW. apply sub_bits; [exact hx_lt | exact hy_lt | exact Hk]. Qed.
+
+(* tb + 8: the branch *)
+Lemma HF_LEQ : HF (SRef (tb A + 8) 0 0) = hleq.
+Proof.
+  post_fire 8. unfold sfire'. cbn [sb sin swsum]. rewrite !HF_H by lia. rewrite HF_EQ.
+  replace (S (A - 2)) with (A - 1) by lia.
+  assert (T : sumbit hx hy (A - 1) = Nat.leb (2 ^ (A - 1)) hr).
+  { rewrite <- hr_bits by lia. apply testbit_top; [lia|]. unfold hr, SW. apply Nat.mod_upper_bound, Nat.pow_nonzero.
+    lia. }
+  assert (Z : Nat.eqb hx hy = Nat.eqb hr 0).
+  { unfold hr, SW. rewrite sub_zero; [reflexivity | exact hx_lt | exact hy_lt]. }
+  unfold hleq. rewrite <- T, <- Z. unfold sumbit, cnt, xb, yb.
+  destruct (Nat.testbit hy (A - 1)), (Nat.testbit hx (A - 1)), (carry hx hy (A - 1)), (Nat.eqb hx hy); reflexivity.
+Qed.
+
+(* tb + 9 to tb + 11: the next counter *)
+Lemma HF_NP : forall i, i < A ->
+  HF (SRef (tb A + 11) i 0) = (bitof A hp i && hh) || (negb hh && hleq && bitof A hc i)
+                               || (negb hh && negb hleq && bitof A ((hp + 3) mod SW A) i).
+Proof.
+  intros i Hi. post_fire 11. rewrite sOR_fire. cbn [existsb]. rewrite !litv_pos, orb_false_r.
+  rewrite HF_HP by exact Hi. post_fire 9. post_fire 10. rewrite !sAND_fire. cbn [forallb].
+  rewrite !litv_pos, !litv_neg, HF_halt, HF_LEQ, HF_Q by exact Hi. rewrite HF_opb by lia.
+  rewrite !andb_true_r, !andb_assoc, orb_assoc. reflexivity.
+Qed.
+
+(* tb + 12: the halt latch *)
+Lemma HF_NH : HF (SRef (tb A + 12) 0 2) =
+  hh || (negb hh && hleq && Nat.eqb hc (SW A - 1)) || (negb hh && negb hleq && Nat.eqb hp (SW A - 4)).
+Proof.
+  post_fire 12. rewrite sOR_fire. cbn [existsb]. rewrite !litv_pos, orb_false_r, HF_halt.
+  post_fire 12. post_fire 12. rewrite !sAND_fire. cbn [forallb].
+  rewrite !litv_pos, !litv_neg, HF_halt, HF_LEQ, HF_AC, HF_P by lia.
+  rewrite !andb_true_r, !andb_assoc, orb_assoc. reflexivity.
+Qed.
+
+(* tb + 13, tb + 14: the next memory *)
+Lemma HF_NM : forall m, m < SW A * A ->
+  HF (SRef (tb A + 14) m 0) =
+    (bitof A (mv (m / A)) (m mod A) && negb (negb hh && Nat.eqb hb (m / A)))
+    || (bitof A hr (m mod A) && (negb hh && Nat.eqb hb (m / A))).
+Proof.
+  intros m Hm. pose proof (Nat.mod_upper_bound m A ltac:(lia)).
+  pose proof (Nat.Div0.div_lt_upper_bound m A (SW A) ltac:(lia)).
+  post_fire 14. rewrite sOR_fire. cbn [existsb]. rewrite !litv_pos, orb_false_r. rewrite HF_KP by exact Hm.
+  post_fire 13. rewrite sAND_fire. cbn [forallb]. rewrite !litv_pos, andb_true_r, HF_rbit, HF_W by lia.
+  rewrite <- hr_bits by lia. unfold bitof. reflexivity.
+Qed.
+
+End HSem.
+
+(* ---- the step ------------------------------------------------------------------------ *)
+Lemma p3_halt : forall A p, 3 <= A -> p < SW A -> Nat.eqb ((p + 3) mod SW A) (SW A - 1) = Nat.eqb p (SW A - 4).
+Proof.
+  intros A p HA Hp. pose proof (SW_ge A HA).
+  destruct (Nat.lt_ge_cases (p + 3) (SW A)) as [L|L].
+  - rewrite Nat.mod_small by exact L. destruct (Nat.eqb_spec (p + 3) (SW A - 1)), (Nat.eqb_spec p (SW A - 4)); lia.
+  - replace (p + 3) with ((p + 3 - SW A) + 1 * SW A) by lia. rewrite Nat.Div0.mod_add, Nat.mod_small by lia.
+    destruct (Nat.eqb_spec (p + 3 - SW A) (SW A - 1)), (Nat.eqb_spec p (SW A - 4)); lia.
+Qed.
+
+(* the step of the machine in the names of the section *)
+Lemma subleq_halted : forall A s, hhalt s = true -> subleq A s = s.
+Proof. intros A s H. unfold subleq. rewrite H. reflexivity. Qed.
+
+Lemma subleq_run : forall A s, hhalt s = false ->
+  subleq A s = mkH (if hleq A s then hc A s else (hp s + 3) mod SW A)
+                   (Nat.eqb (if hleq A s then hc A s else (hp s + 3) mod SW A) (SW A - 1))
+                   (map (fun j => if Nat.eqb j (hb A s) then hr A s else memv s j) (seq 0 (SW A))).
+Proof. intros A s H. unfold subleq. rewrite H. reflexivity. Qed.
+
+Lemma memv_run : forall A s j, hhalt s = false -> j < SW A ->
+  memv (subleq A s) j = if Nat.eqb j (hb A s) then hr A s else memv s j.
+Proof.
+  intros A s j H Hj. rewrite subleq_run by exact H. unfold memv at 1. cbn [hmem].
+  rewrite nth_map_seq by exact Hj. reflexivity.
+Qed.
+
+Theorem host_step : forall A s, 3 <= A -> hvalid A s ->
+  netstep (nH A) (host_units A) (host_next A) (encodeH A s) = encodeH A (subleq A s).
+Proof.
+  intros A s HA Hv. pose proof (SW_ge A HA) as HS. pose proof Hv as (Hp & Hl & Hf).
+  assert (Hl' : length (hmem (subleq A s)) = SW A).
+  { unfold subleq. destruct (hhalt s); [exact Hl|]. cbn [hmem]. rewrite length_map, length_seq. reflexivity. }
+  unfold netstep, host_next. rewrite map_map.
+  apply nth_ext with (d := false) (d' := false).
+  { rewrite length_map, length_seq, length_encodeH by exact Hl'. reflexivity. }
+  intros i Hi. rewrite length_map, length_seq in Hi.
+  rewrite (nth_map_seq _ (fun i => run (host_units A) (nH A) (fun i0 => nth i0 (encodeH A s) false)
+                                      (idx (nH A) (hblocks A) (hout A i))) (nH A) i false Hi).
+  change (run (host_units A) (nH A) (fun i0 => nth i0 (encodeH A s) false) (idx (nH A) (hblocks A) (hout A i)))
+    with (HF A s (hout A i)).
+  unfold hout. destruct (Nat.ltb_spec i A) as [Hi1|Hi1].
+  - (* the counter *)
+    rewrite HF_NP by assumption. rewrite nth_encodeH_pc by exact Hi1. unfold hh.
+    destruct (hhalt s) eqn:Eh.
+    + rewrite subleq_halted by exact Eh. cbn [negb andb orb]. rewrite andb_true_r, !orb_false_r. reflexivity.
+    + rewrite subleq_run by exact Eh. cbn [hpc negb andb orb]. rewrite andb_false_r, orb_false_l.
+      destruct (hleq A s); cbn [negb andb orb]; rewrite ?orb_false_r; reflexivity.
+  - destruct (Nat.eqb_spec i A) as [->|Hi2].
+    + (* the halt bit *)
+      rewrite HF_NH by assumption. rewrite nth_encodeH_halt. unfold hh.
+      destruct (hhalt s) eqn:Eh.
+      * rewrite subleq_halted by exact Eh. rewrite Eh. reflexivity.
+      * rewrite subleq_run by exact Eh. cbn [hhalt negb andb orb].
+        destruct (hleq A s); cbn [negb andb orb]; [rewrite orb_false_r; reflexivity|].
+        rewrite p3_halt by (unfold hp; assumption). reflexivity.
+    + (* the memory *)
+      remember (i - A - 1) as m eqn:Em. assert (Hm : m < SW A * A) by (unfold nH in Hi; lia).
+      pose proof (Nat.mod_upper_bound m A ltac:(lia)). pose proof (Nat.Div0.div_lt_upper_bound m A (SW A) ltac:(lia)).
+      replace i with (A + 1 + (m / A) * A + m mod A) by (pose proof (Nat.div_mod_eq m A); lia).
+      rewrite HF_NM by assumption. rewrite nth_encodeH_mem by assumption. unfold hh.
+      destruct (hhalt s) eqn:Eh.
+      * rewrite subleq_halted by exact Eh. cbn [negb andb orb]. rewrite andb_true_r, andb_false_r, orb_false_r.
+        reflexivity.
+      * rewrite memv_run by assumption. rewrite (Nat.eqb_sym (m / A) (hb A s)).
+        destruct (Nat.eqb (hb A s) (m / A)); cbn [negb andb orb];
+          rewrite ?andb_true_r, ?andb_false_r, ?orb_false_r, ?orb_false_l; reflexivity.
+Qed.

rocq/HostWF.v

@@ -0,0 +1,251 @@
+(* The host netlist reads, at every unit, only state bits and earlier units, for every A >= 3. *)
+From Stdlib Require Import List Bool Arith ZArith Lia.
+Import ListNotations.
+From TH Require Import TwoHead Net Gates Host.
+
+Lemma SW_ge : forall A, 3 <= A -> 8 <= SW A.
+Proof.
+  intros A H. unfold SW. replace A with (3 + (A - 3)) by lia. rewrite Nat.pow_add_r.
+  pose proof (Nat.pow_nonzero 2 (A - 3) ltac:(lia)). cbn [Nat.pow]. lia.
+Qed.
+
+Lemma length_hpre : forall A, length (hpre A) = 17.
+Proof. reflexivity. Qed.
+
+Lemma length_hpost : forall A, length (hpost A) = 15.
+Proof. reflexivity. Qed.
+
+Lemma length_hblocks : forall A, 1 <= A -> length (hblocks A) = tb A + 15.
+Proof.
+  intros A H. unfold hblocks, tb. rewrite !length_app, length_map, length_seq, length_hpre, length_hpost. lia.
+Qed.
+
+Lemma nth_hb_pre : forall A b, b < 17 -> nth b (hblocks A) blk0 = nth b (hpre A) blk0.
+Proof. intros A b H. unfold hblocks. rewrite app_nth1 by (rewrite length_hpre; exact H). reflexivity. Qed.
+
+Lemma nth_hb_T : forall A k, 1 <= k -> k < A -> nth (16 + k) (hblocks A) blk0 = blk_T A k.
+Proof.
+  intros A k H1 H2. unfold hblocks. rewrite app_nth2 by (rewrite length_hpre; lia). rewrite length_hpre.
+  rewrite app_nth1 by (rewrite length_map, length_seq; lia).
+  rewrite nth_map_d with (d' := 0) by (rewrite length_seq; lia). rewrite seq_nth by lia. f_equal. lia.
+Qed.
+
+Lemma nth_hb_post : forall A i, 1 <= A -> nth (tb A + i) (hblocks A) blk0 = nth i (hpost A) blk0.
+Proof.
+  intros A i H. unfold hblocks, tb. rewrite app_nth2 by (rewrite length_hpre; lia). rewrite length_hpre.
+  rewrite app_nth2 by (rewrite length_map, length_seq; lia). rewrite length_map, length_seq. f_equal. lia.
+Qed.
+
+(* what a conjunction or a disjunction of literals reads *)
+Lemma in_sin_lits : forall ls x w,
+  In (x, w) (sin (sAND ls)) \/ In (x, w) (sin (sOR ls)) -> In x (map fst ls).
+Proof.
+  intros ls x w H. cbn [sin sAND sOR] in H.
+  assert (K : In (x, w) (map lw ls) -> In x (map fst ls)).
+  { intro H'. apply in_map_iff in H' as ([y p] & E & Hl). unfold lw in E. cbn [fst snd] in E.
+    injection E as Ey _. subst y. apply in_map_iff. exists (x, p). split; [reflexivity | exact Hl]. }
+  destruct H as [H|H]; apply K; exact H.
+Qed.
+
+Section Reads.
+Variable A : nat.
+
+Let rb := reads_back (hblocks A) (nH A).
+
+Lemma rb_in : forall b j r i, i < nH A -> rb b j r (SIn i).
+Proof. intros b j r i H. exact H. Qed.
+
+Lemma rb_mu : forall b j r j' t, j' < SW A -> t < A -> rb b j r (mu A j' t).
+Proof. intros b j r j' t H1 H2. unfold mu. apply rb_in. unfold nH. nia. Qed.
+
+Lemma rb_pre : forall b j r b' j' r', b' < 17 -> b' < b ->
+  j' < bcount (nth b' (hpre A) blk0) -> r' < bsize (nth b' (hpre A) blk0) -> rb b j r (SRef b' j' r').
+Proof. intros b j r b' j' r' H1 H2 H3 H4. left. rewrite nth_hb_pre by exact H1. auto. Qed.
+
+Lemma rb_T : forall b j r k r', 1 <= k -> k < A -> 16 + k < b -> r' < S k -> rb b j r (SRef (16 + k) 0 r').
+Proof. intros b j r k r' H1 H2 H3 H4. left. rewrite nth_hb_T by assumption. cbn [bcount bsize blk_T]. lia. Qed.
+
+Lemma rb_post : forall b j r i j' r', 1 <= A -> tb A + i < b ->
+  j' < bcount (nth i (hpost A) blk0) -> r' < bsize (nth i (hpost A) blk0) -> rb b j r (SRef (tb A + i) j' r').
+Proof. intros b j r i j' r' H0 H1 H2 H3. left. rewrite nth_hb_post by lia. auto. Qed.
+
+Lemma rb_post0 : forall b j r j' r', 1 <= A -> tb A < b ->
+  j' < bcount (nth 0 (hpost A) blk0) -> r' < bsize (nth 0 (hpost A) blk0) -> rb b j r (SRef (tb A) j' r').
+Proof.
+  intros b j r j' r' H0 H1 H2 H3. left. pose proof (nth_hb_post A 0 H0) as E. rewrite Nat.add_0_r in E.
+  rewrite E. auto.
+Qed.
+
+Lemma rb_self : forall b j r r', r' < r -> rb b j r (SRef b j r').
+Proof. intros b j r r' H. right. auto. Qed.
+
+Lemma rb_xv : forall b j r i, 1 <= A -> 15 < b -> rb b j r (xv A i).
+Proof. intros b j r i H0 H. unfold xv. apply rb_pre; cbn [nth hpre bcount bsize blk_X]; lia. Qed.
+
+Lemma rb_yv : forall b j r i, 1 <= A -> 15 < b -> rb b j r (yv A i).
+Proof. intros b j r i H0 H. unfold yv. apply rb_pre; cbn [nth hpre bcount bsize blk_Y]; lia. Qed.
+
+Lemma rb_opb : forall b j r o t, 6 < b -> o < 3 -> t < A -> rb b j r (opb A o t).
+Proof. intros b j r o t H1 H2 H3. unfold opb. apply rb_pre; cbn [nth hpre bcount bsize blk_F]; nia. Qed.
+
+Lemma rb_prr : forall b j r i, 16 < b -> i < A - 1 -> rb b j r (prr i).
+Proof. intros b j r i H1 H2. unfold prr. apply rb_pre; cbn [nth hpre bcount bsize blk_PR]; lia. Qed.
+
+Lemma rb_rbit : forall b j r k, tb A + 7 < b -> k < A -> rb b j r (rbit A k).
+Proof.
+  intros b j r k H1 H2. unfold rbit. destruct (Nat.eqb_spec k 0).
+  - apply rb_post; cbn [nth hpost bcount bsize blk_R0]; lia.
+  - apply rb_post; cbn [nth hpost bcount bsize blk_R]; lia.
+Qed.
+
+End Reads.
+
+Lemma mod_lt : forall a n, 0 < n -> a mod n < n.
+Proof. intros a n H. apply Nat.mod_upper_bound. lia. Qed.
+
+Lemma div_lt : forall a b n, a < b * n -> 0 < n -> a / n < b.
+Proof. intros a b n H1 H2. apply Nat.Div0.div_lt_upper_bound. lia. Qed.
+
+Ltac lits_in Hin :=
+  let H := fresh in
+  pose proof (in_sin_lits _ _ _ (or_introl Hin)) as H || pose proof (in_sin_lits _ _ _ (or_intror Hin)) as H;
+  clear Hin; unfold lits in H; rewrite ?map_map in H; cbn [map fst] in H.
+
+Theorem host_wf : forall A, 3 <= A -> wf (hblocks A) (nH A).
+Proof.
+  intros A HA. pose proof (SW_ge A HA) as HS.
+  split.
+  { unfold hblocks. apply Forall_app; split; [|apply Forall_app; split].
+    - unfold hpre. repeat apply Forall_cons; try apply Forall_nil; intros j Hj; reflexivity.
+    - apply Forall_forall. intros blk Hin. apply in_map_iff in Hin as (k & <- & _).
+      intros j Hj. cbn [bshape bsize blk_T length]. rewrite length_map, length_seq. reflexivity.
+    - unfold hpost. repeat apply Forall_cons; try apply Forall_nil; intros j Hj; reflexivity. }
+  intros b j r x w Hb Hj Hr Hin. rewrite length_hblocks in Hb by lia. unfold sunit in Hin.
+  destruct (Nat.lt_ge_cases b 17) as [Hp|Hp].
+  { rewrite nth_hb_pre in Hj, Hr, Hin by exact Hp.
+    assert (Hc : b = 0 \/ b = 1 \/ b = 2 \/ b = 3 \/ b = 4 \/ b = 5 \/ b = 6 \/ b = 7 \/ b = 8 \/ b = 9
+                 \/ b = 10 \/ b = 11 \/ b = 12 \/ b = 13 \/ b = 14 \/ b = 15 \/ b = 16) by lia.
+    destruct Hc as [->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->| ->]]]]]]]]]]]]]]]];
+      cbn [nth hpre bcount bsize bshape blk_P blk_HP blk_FA blk_Q blk_F blk_PA blk_PB blk_AC blk_W
+           blk_RX blk_RY blk_KP blk_X blk_Y blk_PR] in Hj, Hr, Hin;
+      (destruct r as [|r]; [|lia]); cbn [nth] in Hin.
+    - (* P *) lits_in Hin. apply in_map_iff in H as (t & <- & Ht). apply in_seq in Ht. apply rb_in. unfold nH. nia.
+    - (* HP *) lits_in Hin. destruct H as [<-|[<-|[]]]; apply rb_in; unfold nH; nia.
+    - (* FA 0 *) lits_in Hin. pose proof (mod_lt j (SW A) ltac:(lia)). pose proof (div_lt j A (SW A) ltac:(lia) ltac:(lia)).
+      destruct H as [<-|[<-|[]]]; [apply rb_mu; [apply mod_lt|]; lia|].
+      apply rb_pre; cbn [nth hpre bcount bsize blk_P]; lia.
+    - (* FA 1 *) lits_in Hin. pose proof (mod_lt j (SW A) ltac:(lia)). pose proof (div_lt j A (SW A) ltac:(lia) ltac:(lia)).
+      destruct H as [<-|[<-|[]]]; [apply rb_mu; [apply mod_lt|]; lia|].
+      apply rb_pre; cbn [nth hpre bcount bsize blk_P]; lia.
+    - (* FA 2 *) lits_in Hin. pose proof (mod_lt j (SW A) ltac:(lia)). pose proof (div_lt j A (SW A) ltac:(lia) ltac:(lia)).
+      destruct H as [<-|[<-|[]]]; [apply rb_mu; [apply mod_lt|]; lia|].
+      apply rb_pre; cbn [nth hpre bcount bsize blk_P]; lia.
+    - (* Q *) lits_in Hin. rewrite ?map_map in H. apply in_map_iff in H as (j' & <- & Hj').
+      apply filter_In in Hj' as [Hj' _]. apply in_seq in Hj'.
+      apply rb_pre; cbn [nth hpre bcount bsize blk_P]; lia.
+    - (* F *) lits_in Hin. rewrite ?map_map in H. apply in_map_iff in H as (j' & <- & Hj'). apply in_seq in Hj'.
+      cbn [fst]. pose proof (div_lt j 3 A ltac:(lia) ltac:(lia)). pose proof (mod_lt j A ltac:(lia)).
+      apply rb_pre; [lia | lia | |].
+      + assert (Ho : j / A = 0 \/ j / A = 1 \/ j / A = 2) by lia.
+        destruct Ho as [-> | [-> | ->]]; cbn [Nat.add nth hpre bcount blk_FA]; nia.
+      + assert (Ho : j / A = 0 \/ j / A = 1 \/ j / A = 2) by lia.
+        destruct Ho as [-> | [-> | ->]]; cbn [Nat.add nth hpre bsize blk_FA]; lia.
+    - (* PA *) lits_in Hin. apply in_map_iff in H as (t & <- & Ht). apply in_seq in Ht. apply rb_opb; lia.
+    - (* PB *) lits_in Hin. apply in_map_iff in H as (t & <- & Ht). apply in_seq in Ht. apply rb_opb; lia.
+    - (* AC *) lits_in Hin. rewrite ?map_map in H. apply in_map_iff in H as (t & <- & Ht). apply in_seq in Ht.
+      apply rb_opb; lia.
+    - (* W *) lits_in Hin. destruct H as [<-|[<-|[]]]; [apply rb_in; unfold nH; nia|].
+      apply rb_pre; cbn [nth hpre bcount bsize blk_PB]; lia.
+    - (* RX *) lits_in Hin. pose proof (mod_lt j (SW A) ltac:(lia)). pose proof (div_lt j A (SW A) ltac:(lia) ltac:(lia)).
+      destruct H as [<-|[<-|[]]]; [apply rb_mu; lia|]. apply rb_pre; cbn [nth hpre bcount bsize blk_PA]; lia.
+    - (* RY *) lits_in Hin. pose proof (mod_lt j (SW A) ltac:(lia)). pose proof (div_lt j A (SW A) ltac:(lia) ltac:(lia)).
+      destruct H as [<-|[<-|[]]]; [apply rb_mu; lia|]. apply rb_pre; cbn [nth hpre bcount bsize blk_PB]; lia.
+    - (* KP *) lits_in Hin. pose proof (mod_lt j A ltac:(lia)). pose proof (div_lt j (SW A) A ltac:(lia) ltac:(lia)).
+      destruct H as [<-|[<-|[]]]; [apply rb_mu; lia|]. apply rb_pre; cbn [nth hpre bcount bsize blk_W]; lia.
+    - (* X *) lits_in Hin. rewrite ?map_map in H. apply in_map_iff in H as (j' & <- & Hj'). apply in_seq in Hj'.
+      apply rb_pre; cbn [nth hpre bcount bsize blk_RX]; nia.
+    - (* Y *) lits_in Hin. rewrite ?map_map in H. apply in_map_iff in H as (j' & <- & Hj'). apply in_seq in Hj'.
+      apply rb_pre; cbn [nth hpre bcount bsize blk_RY]; nia.
+    - (* PR *) lits_in Hin. destruct H as [<-|[<-|[]]]; [apply rb_xv | apply rb_yv]; lia. }
+  destruct (Nat.lt_ge_cases b (tb A)) as [HT|HT].
+  { (* the carry terms into bit k = b - 16 *)
+    unfold tb in HT. replace b with (16 + (b - 16)) in Hj, Hr, Hin |- * by lia.
+    rewrite nth_hb_T in Hj, Hr, Hin by lia. cbn [bcount bsize bshape blk_T] in Hj, Hr, Hin.
+    destruct r as [|r].
+    - cbn [nth] in Hin. lits_in Hin. rewrite ?map_map in H. apply in_map_iff in H as (i & <- & Hi). apply in_seq in Hi.
+      apply rb_prr; lia.
+    - cbn [nth] in Hin. rewrite nth_map_d with (d' := 0) in Hin by (rewrite length_seq; lia).
+      rewrite seq_nth in Hin by lia. lits_in Hin. rewrite ?map_app, ?map_map in H. cbn [map fst] in H.
+      destruct H as [<-|[<-|H]]; [apply rb_yv; lia | apply rb_xv; lia|].
+      apply in_map_iff in H as (i & <- & Hi). apply in_seq in Hi. apply rb_prr; lia. }
+  replace b with (tb A + (b - tb A)) in Hj, Hr, Hin |- * by lia.
+  rewrite nth_hb_post in Hj, Hr, Hin by lia.
+  assert (Hi : b - tb A < 15) by (unfold tb in *; lia).
+  remember (b - tb A) as i eqn:Ei. clear Ei Hb Hp HT.
+  assert (Hc : i = 0 \/ i = 1 \/ i = 2 \/ i = 3 \/ i = 4 \/ i = 5 \/ i = 6 \/ i = 7 \/ i = 8 \/ i = 9
+               \/ i = 10 \/ i = 11 \/ i = 12 \/ i = 13 \/ i = 14) by lia.
+  destruct Hc as [->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->| ->]]]]]]]]]]]]]];
+    cbn [nth hpost bcount bsize bshape blk_C blk_AX blk_NX blk_XN blk_EQ blk_R0 blk_H blk_R blk_LEQ
+         blk_TA blk_TB blk_NP blk_HAB blk_WR blk_NM] in Hj, Hr, Hin.
+  - (* C *) destruct r as [|r]; [|lia]. cbn [nth] in Hin. lits_in Hin. destruct H as [<-|H].
+    + apply rb_T; unfold tb; lia.
+    + rewrite ?map_map in H. apply in_map_iff in H as (j' & <- & Hj'). apply in_seq in Hj'. apply rb_T; unfold tb; lia.
+  - (* AX *) destruct r as [|r]; [|lia]. cbn [nth] in Hin. lits_in Hin.
+    destruct H as [<-|[<-|[]]]; [apply rb_xv | apply rb_yv]; unfold tb; lia.
+  - (* NX *) destruct r as [|r]; [|lia]. cbn [nth] in Hin. lits_in Hin.
+    destruct H as [<-|[<-|[]]]; [apply rb_xv | apply rb_yv]; unfold tb; lia.
+  - (* XN *) destruct r as [|r]; [|lia]. cbn [nth] in Hin. lits_in Hin.
+    destruct H as [<-|[<-|[]]]; apply rb_post; cbn [nth hpost bcount bsize blk_AX blk_NX]; lia.
+  - (* EQ *) destruct r as [|r]; [|lia]. cbn [nth] in Hin. lits_in Hin. rewrite ?map_map in H.
+    apply in_map_iff in H as (i' & <- & Hi'). apply in_seq in Hi'.
+    apply rb_post; cbn [nth hpost bcount bsize blk_XN]; lia.
+  - (* R0 *) assert (Hj0 : j = 0) by lia. subst j. assert (Hr3 : r = 0 \/ r = 1 \/ r = 2) by lia.
+    destruct Hr3 as [->|[->| ->]]; cbn [nth] in Hin; lits_in Hin.
+    + destruct H as [<-|[<-|[]]]; [apply rb_yv | apply rb_xv]; unfold tb; lia.
+    + destruct H as [<-|[<-|[]]]; [apply rb_yv | apply rb_xv]; unfold tb; lia.
+    + destruct H as [<-|[<-|[]]]; apply rb_self; lia.
+  - (* H *) assert (Hr3 : r = 0 \/ r = 1 \/ r = 2) by lia.
+    destruct Hr3 as [->|[->| ->]];
+      cbn [nth map sin] in Hin; repeat (destruct Hin as [Hin|Hin]; [injection Hin as <- <-|]); try destruct Hin;
+      first [apply rb_yv; unfold tb; lia | apply rb_xv; unfold tb; lia
+            | apply rb_post0; cbn [nth hpost bcount bsize blk_C]; lia].
+  - (* R *) destruct r as [|r]; [|lia]. cbn [nth sin] in Hin.
+    repeat (destruct Hin as [Hin|Hin]; [injection Hin as <- <-|]); try destruct Hin;
+      apply rb_post; cbn [nth hpost bcount bsize blk_H]; lia.
+  - (* LEQ *) destruct r as [|r]; [|lia]. cbn [nth sin] in Hin.
+    repeat (destruct Hin as [Hin|Hin]; [injection Hin as <- <-|]); try destruct Hin;
+      apply rb_post; cbn [nth hpost bcount bsize blk_H blk_EQ]; lia.
+  - (* TA *) destruct r as [|r]; [|lia]. cbn [nth] in Hin. lits_in Hin.
+    destruct H as [<-|[<-|[<-|[]]]]; [apply rb_in; unfold nH; lia
+                                    | apply rb_post; cbn [nth hpost bcount bsize blk_LEQ]; lia
+                                    | apply rb_opb; unfold tb; lia].
+  - (* TB *) destruct r as [|r]; [|lia]. cbn [nth] in Hin. lits_in Hin.
+    destruct H as [<-|[<-|[<-|[]]]]; [apply rb_in; unfold nH; lia
+                                    | apply rb_post; cbn [nth hpost bcount bsize blk_LEQ]; lia
+                                    | apply rb_pre; [lia | unfold tb; lia | cbn [nth hpre bcount blk_Q]; lia
+                                                    | cbn [nth hpre bsize blk_Q]; lia]].
+  - (* NP *) destruct r as [|r]; [|lia]. cbn [nth] in Hin. lits_in Hin.
+    destruct H as [<-|[<-|[<-|[]]]];
+      [ apply rb_pre; [lia | unfold tb; lia | cbn [nth hpre bcount blk_HP]; lia | cbn [nth hpre bsize blk_HP]; lia]
+      | apply rb_post; cbn [nth hpost bcount bsize blk_TA]; lia
+      | apply rb_post; cbn [nth hpost bcount bsize blk_TB]; lia ].
+  - (* HA, HB, NH *) assert (Hj0 : j = 0) by lia. subst j. assert (Hr3 : r = 0 \/ r = 1 \/ r = 2) by lia.
+    destruct Hr3 as [->|[->| ->]]; cbn [nth] in Hin; lits_in Hin.
+    + destruct H as [<-|[<-|[<-|[]]]];
+        [ apply rb_in; unfold nH; lia
+        | apply rb_post; cbn [nth hpost bcount bsize blk_LEQ]; lia
+        | apply rb_pre; [lia | unfold tb; lia | cbn [nth hpre bcount blk_AC]; lia | cbn [nth hpre bsize blk_AC]; lia] ].
+    + destruct H as [<-|[<-|[<-|[]]]];
+        [ apply rb_in; unfold nH; lia
+        | apply rb_post; cbn [nth hpost bcount bsize blk_LEQ]; lia
+        | apply rb_pre; [lia | unfold tb; lia | cbn [nth hpre bcount blk_P]; lia | cbn [nth hpre bsize blk_P]; lia] ].
+    + destruct H as [<-|[<-|[<-|[]]]]; [apply rb_in; unfold nH; lia | apply rb_self; lia | apply rb_self; lia].
+  - (* WR *) destruct r as [|r]; [|lia]. cbn [nth] in Hin. lits_in Hin.
+    pose proof (div_lt j (SW A) A ltac:(lia) ltac:(lia)).
+    destruct H as [<-|[<-|[]]]; [apply rb_rbit; lia|].
+    apply rb_pre; [lia | unfold tb; lia | cbn [nth hpre bcount blk_W]; lia | cbn [nth hpre bsize blk_W]; lia].
+  - (* NM *) destruct r as [|r]; [|lia]. cbn [nth] in Hin. lits_in Hin.
+    destruct H as [<-|[<-|[]]];
+      [ apply rb_pre; [lia | unfold tb; lia | cbn [nth hpre bcount blk_KP]; lia | cbn [nth hpre bsize blk_KP]; lia]
+      | apply rb_post; cbn [nth hpost bcount bsize blk_WR]; lia ].
+Qed.

rocq/PhysSem.v

@@ -98,6 +98,21 @@ Proof.
   unfold stepA, stepres, cellof, wnext, clearq. cbv zeta. rewrite Hk, Hp, Hd. subst v. reflexivity.
 Qed.
 
+Lemma existsb_pick : forall (g : nat -> bool) c n m,
+  existsb (fun a => Nat.eqb c a && g a) (seq m n) = if (m <=? c) && (c <? m + n) then g c else false.
+Proof.
+  intros g c n. induction n as [|n IH]; intro m; cbn [seq existsb].
+  - destruct (Nat.leb_spec m c), (Nat.ltb_spec c (m + 0)); cbn [andb]; try reflexivity; lia.
+  - rewrite IH. destruct (Nat.eqb_spec c m) as [E|E].
+    + subst c. rewrite Nat.leb_refl.
+      replace (m <? m + S n) with true by (symmetry; apply Nat.ltb_lt; lia).
+      replace (S m <=? m) with false by (symmetry; apply Nat.leb_gt; lia).
+      cbn [andb orb]. destruct (g m); reflexivity.
+    + cbn [andb orb].
+      destruct (Nat.leb_spec m c), (Nat.leb_spec (S m) c), (Nat.ltb_spec c (S m + n)), (Nat.ltb_spec c (m + S n));
+        cbn [andb]; try reflexivity; lia.
+Qed.
+
 Section Sem.
 Variables (al N L : nat) (s : st).
 Hypotheses (Hal : 3 <= al) (HN : recw al <= N) (HL : 1 <= L)
@@ -258,21 +273,6 @@ Proof.
     destruct (Nat.eqb_spec (a - 3) 0); [lia|]. f_equal. lia.
 Qed.
 
-Lemma existsb_pick : forall (g : nat -> bool) c n m,
-  existsb (fun a => Nat.eqb c a && g a) (seq m n) = if (m <=? c) && (c <? m + n) then g c else false.
-Proof.
-  intros g c n. induction n as [|n IH]; intro m; cbn [seq existsb].
-  - destruct (Nat.leb_spec m c), (Nat.ltb_spec c (m + 0)); cbn [andb]; try reflexivity; lia.
-  - rewrite IH. destruct (Nat.eqb_spec c m) as [E|E].
-    + subst c. rewrite Nat.leb_refl.
-      replace (m <? m + S n) with true by (symmetry; apply Nat.ltb_lt; lia).
-      replace (S m <=? m) with false by (symmetry; apply Nat.leb_gt; lia).
-      cbn [andb orb]. destruct (g m); reflexivity.
-    + cbn [andb orb].
-      destruct (Nat.leb_spec m c), (Nat.leb_spec (S m) c), (Nat.ltb_spec c (S m + n)), (Nat.ltb_spec c (m + S n));
-        cbn [andb]; try reflexivity; lia.
-Qed.
-
 Definition fa (o : nat) : nat := bits2nat (field o).
 
 Lemma fa_lt : forall o, o + al <= recw al -> fa o < W al.

rocq/_CoqProject

@@ -24,3 +24,8 @@ PhysMain.v
 PhysFacts.v
 NetMain.v
 Extract.v
+Host.v
+HostWF.v
+Adder.v
+HostSem.v
+ExtractHost.v

rocq/extract/dumphost.ml

@@ -0,0 +1,13 @@
+(* writes the host netlist defined in Host.v, extracted by ExtractHost.v: dumphost A PATH *)
+let () =
+  let a = int_of_string Sys.argv.(1) in
+  let us = Hostnet.host_units a and nx = Hostnet.host_next a in
+  let oc = open_out_bin Sys.argv.(2) in
+  let put x = let b = Bytes.create 4 in Bytes.set_int32_le b 0 (Int32.of_int x); output_bytes oc b in
+  let edges = List.fold_left (fun acc (u : Hostnet.tu) -> acc + List.length u.tin) 0 us in
+  put (Hostnet.nH a); put (List.length us); put edges;
+  List.iter (fun (u : Hostnet.tu) -> put u.tb) us;
+  List.iter (fun (u : Hostnet.tu) -> put (List.length u.tin)) us;
+  List.iter (fun (u : Hostnet.tu) -> List.iter (fun (s, wt) -> put (wt * (s + 1))) u.tin) us;
+  List.iter put nx;
+  close_out oc

src/independent.py

@@ -1,4 +1,4 @@
-"""Code written from the paper's text alone: H_A, the levelization, noise, weight error, the datapath."""
+"""Code written from the paper's text alone: H_A, the levelization, noise and weight error."""
 import hashlib
 import json
 import math
@@ -393,177 +393,6 @@ def main_levelize():
             w(len(blob))
             f.write(blob)
 
-NPZ = os.path.join(WORK, 'datapath.npz')
-
-RECORD = os.path.join(REPO, 'paper', 'runs', 'independent_neuromorphic.json')
-
-K = 9
-
-
-def record(key, value):
-    rec = json.load(open(RECORD)) if os.path.exists(RECORD) else {}
-    rec[key] = value
-    json.dump(rec, open(RECORD, 'w'), indent=1)
-
-
-def export():
-    N, nxt = build(8)
-    blocks = N.block
-    nst = N.n
-    keep = [k for k, b in enumerate(blocks) if b in ('sub', 'eq', 'LEQ')]
-    keepset = set(N.n + k for k in keep)
-    # inputs: the units X_t, Y_t of block XY; outputs: r_0..r_7 and LEQ
-    xy = [N.n + k for k, b in enumerate(blocks) if b == 'XY']
-    X, Y = xy[:8], xy[8:]
-    units = {N.n + k: (N.bias[k], N.ins[k]) for k in keep}
-    # the outputs: the sum bits are the last 8 units feeding WR, recovered as the inputs of NM's AND units
-    sub = [N.n + k for k, b in enumerate(blocks) if b == 'sub']
-    r = [sub[-8]] + sub[-7:]           # r_0 is the AND of the XOR cell, then r_1..r_7
-    leq = [N.n + k for k, b in enumerate(blocks) if b == 'LEQ'][0]
-    inputs = X + Y
-    outputs = r + [leq]
-    # check the choice of outputs by evaluating the cut-out circuit on all pairs
-    def ev(xa, xb):
-        v = {}
-        for t in range(8):
-            v[X[t]] = (xa >> t) & 1
-            v[Y[t]] = (xb >> t) & 1
-        for u in sorted(units):
-            b, ins = units[u]
-            v[u] = 1 if b + sum(w * v[s] for s, w in ins) >= 0 else 0
-        return sum(v[r[k]] << k for k in range(8)), v[leq]
-    for xa in range(256):
-        for xb in (0, 1, 127, 128, 255, xa, (xa + 1) % 256):
-            res = (xb - xa) % 256
-            assert ev(xa, xb) == (res, int(res == 0 or res >= 128)), (xa, xb)
-    # levelize (Lemma 2.6) with the inputs at layer 0
-    depth = {s: 0 for s in inputs}
-    for u in sorted(units):
-        depth[u] = 1 + max(depth[s] for s, _ in units[u][1])
-    d = max(depth[o] for o in outputs)
-    lam = {}
-    for u in units:
-        for s, _ in units[u][1]:
-            lam[s] = max(lam.get(s, 0), depth[u])
-    for o in outputs:
-        lam[o] = d + 1
-    layers, prev = [], {s: i for i, s in enumerate(inputs)}
-    for l in range(1, d + 1):
-        rows = []
-        if l < d:
-            for s in list(inputs) + sorted(units):
-                if s in units and depth[s] == l:
-                    rows.append((s, units[s][0], units[s][1]))
-                elif depth[s] < l < lam.get(s, -1):
-                    rows.append((s, -1, [(s, 1)]))
-        else:
-            for o in outputs:
-                rows.append((o, units[o][0], units[o][1]) if depth[o] == d else (o, -1, [(o, 1)]))
-        W = np.zeros((len(rows), len(prev)), dtype=np.int32)
-        b = np.zeros(len(rows), dtype=np.int32)
-        for i, (_, bb, ins) in enumerate(rows):
-            b[i] = bb
-            for s, w in ins:
-                W[i, prev[s]] = w
-        layers.append((W, b))
-        prev = {s: i for i, (s, _, _) in enumerate(rows)}
-    out = dict(n_layers=np.array([d]), n_units=np.array([len(units)]))
-    for i, (W, b) in enumerate(layers):
-        out[f'W{i}'], out[f'b{i}'] = W, b
-    os.makedirs(WORK, exist_ok=True)
-    np.savez(NPZ, **out)
-    res = dict(units=len(units), depth=d, widths=[int(W.shape[0]) for W, _ in layers])
-    record('datapath', res)
-    print(json.dumps(res))
-
-
-def reference(xa, xb):
-    res = (xb - xa) % 256
-    return res, int(res == 0 or res >= 128)
-
-
-def operands(n, seed):
-    rng = np.random.default_rng(seed)
-    xa = rng.integers(0, 256, n)
-    xb = rng.integers(0, 256, n)
-    xa[:256], xb[:256] = np.arange(256), 0
-    xa[256:512], xb[256:512] = 0, np.arange(256)
-    xa[512:768], xb[512:768] = np.arange(256), np.arange(256)
-    return xa, xb
-
-
-def lava(off):
-    from lava.magma.core.run_conditions import RunSteps
-    from lava.magma.core.run_configs import Loihi2SimCfg
-    from lava.proc.dense.process import Dense
-    from lava.proc.io.sink import RingBuffer as Sink
-    from lava.proc.io.source import RingBuffer as Source
-    from lava.proc.lif.process import LIF
-    z = np.load(NPZ)
-    L = int(z['n_layers'][0])
-    layers = [(z[f'W{i}'], z[f'b{i}']) for i in range(L)]
-    N = 4096
-    xa, xb = operands(N, 77)
-    spikes = np.zeros((16, N))
-    for k in range(8):
-        spikes[k] = (xa >> k) & 1
-        spikes[8 + k] = (xb >> k) & 1
-    T = N + L + 2
-    src = Source(data=np.pad(spikes, ((0, 0), (0, T - N))))
-    prev, first = src.s_out, None
-    vth = 2 * K - 2 + off
-    for W, b in layers:
-        dn = Dense(weights=(2 * W).astype(np.int32))
-        lif = LIF(shape=(W.shape[0],), du=4095, dv=4095, bias_mant=(b + K).astype(np.int32), bias_exp=7, vth=vth)
-        prev.connect(dn.s_in)
-        dn.a_out.connect(lif.a_in)
-        prev, first = lif.s_out, first or lif
-    snk = Sink(shape=(9,), buffer=T)
-    prev.connect(snk.a_in)
-    first.run(condition=RunSteps(num_steps=T), run_cfg=Loihi2SimCfg(select_tag='fixed_pt'))
-    out = snk.data.get()
-    first.stop()
-    bad = 0
-    for t in range(N):
-        col = out[:, t + L]
-        bad += (sum(int(col[k]) << k for k in range(8)), int(col[8])) != reference(int(xa[t]), int(xb[t]))
-    # the membrane potential of a unit at pre-activation z is 128 (z + K); the threshold is 64 vth
-    margin_fire = 128 * K - 64 * vth
-    margin_quiet = 64 * vth - 128 * (K - 1)
-    res = dict(backend='lava fixed_pt', vth=vth, patterns=N, failures=bad,
-               margin_firing_side=margin_fire, margin_quiet_side=margin_quiet)
-    record(f'lava_vth_{vth}', res)
-    print(json.dumps(res))
-
-
-def akida():
-    import akida as ak
-    from akida import FullyConnected, InputData, Model
-    z = np.load(NPZ)
-    L = int(z['n_layers'][0])
-    layers = [(z[f'W{i}'], z[f'b{i}']) for i in range(L)]
-    m = Model()
-    m.add(InputData(input_shape=(1, 1, 16), input_bits=1))
-    for i, (W, b) in enumerate(layers):
-        m.add(FullyConnected(units=int(W.shape[0]), weights_bits=2, activation=True, act_bits=1, name=f'l{i}'))
-        lay = m.get_layer(i + 1)
-        wv = np.zeros(lay.variables['weights'].shape, dtype=np.int8)
-        wv[0, 0, :, :] = W.T.astype(np.int8)
-        lay.variables['weights'] = wv
-        lay.variables['threshold'] = (-b - 1).astype(np.int32)
-    N = 65536
-    xa, xb = np.arange(N) % 256, np.arange(N) // 256
-    Xin = np.zeros((N, 1, 1, 16), dtype=np.uint8)
-    for k in range(8):
-        Xin[:, 0, 0, k] = (xa >> k) & 1
-        Xin[:, 0, 0, 8 + k] = (xb >> k) & 1
-    out = np.concatenate([m.forward(Xin[i:i + 8192]).reshape(-1, 9) for i in range(0, N, 8192)])
-    bad = sum((sum(int(out[t, k]) << k for k in range(8)), int(out[t, 8])) != reference(int(xa[t]), int(xb[t]))
-              for t in range(N))
-    res = dict(backend=f'akida {ak.__version__}', patterns=N, failures=int(bad))
-    record('akida', res)
-    print(json.dumps(res))
-
 NSIM, BIN, HIST = os.path.join(WORK, 'nsim'), os.path.join(WORK, 'host_lev.bin'), os.path.join(WORK, 'hist_sd.bin')
 
 M = 41967
@@ -624,7 +453,6 @@ def main_noise():
     print(json.dumps({k: v for k, v in out.items() if k in ('exact_self_reproducing', 'profile', 'seconds')}))
 
 
-
 def load():
     b = open(BIN, 'rb').read()
     pos = 0
@@ -748,17 +576,7 @@ def cmd_host_family():
     json.dump(out, open(os.path.join(RUNS, 'independent_host_family.json'), 'w'), indent=1)
 
 
-def cmd_neuromorphic():
-    cmd = sys.argv[1]
-    if cmd == 'export':
-        export()
-    elif cmd == 'lava':
-        lava(int(sys.argv[2]))
-    else:
-        akida()
-
-
-COMMANDS = {'host-family': cmd_host_family, 'levelize': main_levelize, 'neuromorphic': cmd_neuromorphic, 'noise': main_noise, 'weight-error': main_weight_error}
+COMMANDS = {'host-family': cmd_host_family, 'levelize': main_levelize, 'noise': main_noise, 'weight-error': main_weight_error}
 
 
 if __name__ == "__main__":

src/noise.py

@@ -1,4 +1,4 @@
-"""Perturbation experiments on the levelized host, the amplified host, and the neuromorphic datapath."""
+"""Perturbation experiments on the levelized host and on the amplified host."""
 from __future__ import annotations
 
 import argparse
@@ -12,8 +12,6 @@ import tempfile
 import time
 from typing import Dict, List, Tuple
 
-import numpy as np
-
 from host import (
     encode,
     M_P,
@@ -21,17 +19,14 @@ from host import (
     HALT_PC,
     Tape,
     describe,
-    field,
     inst,
     read_host,
     ser,
     tau_star,
-    run_reference,
     STATE_LAYOUT,
     IO_CELLS,
-    STATE_BITS,
 )
-from paper import levelize, parse_sigma, write_flat, framed_parts
+from paper import levelize, parse_sigma, write_flat
 
 
 REPO = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
@@ -1301,227 +1296,7 @@ def main_amplified() -> int:
             "curve": cmd_curve, "restore": cmd_restore, "layers": cmd_layers,
             "bound": cmd_bound}[args.mode](args)
 
-K = 9                                    # bias offset making the threshold >= 0
-
-NPZ = os.path.join(REPO, "paper", "runs", "datapath_layers.npz")
-
-
-def datapath_net():
-    """The subtractor, equality test and branch of H_8, cut out of the host netlist."""
-    sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
-    from host import build
-    from machines import Net
-    full, _, _ = build(8)
-    A = 8
-    xv = [f"X{A - 1 - i}" for i in range(A)]
-    yv = [f"Y{A - 1 - i}" for i in range(A)]
-    keep = set()
-    stack = [f"R{k}" for k in range(A)] + ["LEQ"]
-    while stack:
-        g = stack.pop()
-        if g in keep or g in xv or g in yv:
-            continue
-        keep.add(g)
-        stack.extend(s for s, _ in full.gates[g][0])
-    net = Net()
-    for gname, (ins, bias) in full.gates.items():
-        if gname in keep:
-            net.g(gname, list(ins), bias)
-    return net, xv, yv, [f"R{k}" for k in range(A)], "LEQ"
-
-
-def export() -> int:
-    """Levelize the datapath and write its integer weights and biases."""
-    sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
-    from machines import compile_net
-    net, xv, yv, r, leq = datapath_net()
-    inputs = xv + yv
-    outputs = r + [leq]
-    layers, info = compile_net(net, inputs, outputs, final_ordered=True)
-    d = {"n_layers": np.array([len(layers)]),
-         "n_units": np.array([len(net.gates)]),
-         "n_inputs": np.array([len(inputs)]),
-         "n_outputs": np.array([len(outputs)])}
-    for i, (W, bb) in enumerate(layers):
-        d[f"W{i}"] = W.numpy().astype(np.int32)
-        d[f"b{i}"] = bb.numpy().astype(np.int32)
-    os.makedirs(os.path.dirname(NPZ), exist_ok=True)
-    np.savez(NPZ, **d)
-    print(f"  datapath: {len(net.gates)} units on {len(inputs)} inputs, "
-          f"{len(layers)} layers of widths "
-          f"{[int(W.shape[0]) for W, _ in layers]}")
-    print(f"  wrote {NPZ}")
-    return 0
-
-
-def reference(xa, xb):
-    """The subtraction and the branch predicate of Definition 3.1, as integers."""
-    res = (xb - xa) & 0xFF
-    leq = 1 if (res == 0 or res >= 128) else 0
-    return res, leq
-
-
-def run() -> int:
-    from lava.magma.core.run_conditions import RunSteps
-    from lava.magma.core.run_configs import Loihi2SimCfg
-    from lava.proc.dense.process import Dense
-    from lava.proc.io.sink import RingBuffer as Sink
-    from lava.proc.io.source import RingBuffer as Source
-    from lava.proc.lif.process import LIF
-
-    z = np.load(NPZ)
-    L = int(z["n_layers"][0])
-    n_in = int(z["n_inputs"][0])
-    n_out = int(z["n_outputs"][0])
-    layers = [(z[f"W{i}"], z[f"b{i}"]) for i in range(L)]
-    print(f"  datapath: {int(z['n_units'][0])} units on {n_in} inputs, "
-          f"{L} layers of widths {[int(W.shape[0]) for W, _ in layers]}",
-          flush=True)
-
-    worst = 0
-    for W, b in layers:
-        hi = np.maximum(W, 0).sum(axis=1) + b + K
-        lo = np.minimum(W, 0).sum(axis=1) + b + K
-        worst = max(worst, int(np.abs(np.concatenate([hi, lo])).max()))
-    print(f"  worst |<w,x> + b + K| over all units and all inputs: {worst}, "
-          f"so the membrane potential stays below {128 * worst} < 4096: "
-          f"{'yes' if 128 * worst < 4096 else 'NO'}", flush=True)
-    assert 128 * worst < 4096
-
-    rng = np.random.default_rng(20260910)
-    N = 4096
-    xa = rng.integers(0, 256, N)
-    xb = rng.integers(0, 256, N)
-    xa[:256] = np.arange(256); xb[:256] = 0           # every difference through zero
-    xa[256:512] = 0; xb[256:512] = np.arange(256)
-    xa[512:768] = np.arange(256); xb[512:768] = np.arange(256)   # x = y
-
-    spikes = np.zeros((n_in, N))
-    for t in range(N):
-        for k in range(8):
-            spikes[k, t] = (xa[t] >> k) & 1           # x, value bits
-            spikes[8 + k, t] = (xb[t] >> k) & 1       # y
-
-    T = N + L + 2
-    src = Source(data=np.pad(spikes, ((0, 0), (0, T - N))))
-    prev = src.s_out
-    first_lif = None
-    for W, b in layers:
-        dn = Dense(weights=(2 * W).astype(np.int32))
-        lif = LIF(shape=(W.shape[0],), du=4095, dv=4095,
-                  bias_mant=(b + K).astype(np.int32), bias_exp=7, vth=2 * K - 1)
-        prev.connect(dn.s_in)
-        dn.a_out.connect(lif.a_in)
-        prev = lif.s_out
-        first_lif = first_lif or lif
-    snk = Sink(shape=(n_out,), buffer=T)
-    prev.connect(snk.a_in)
-
-    print(f"  running {T} time steps of the {L}-layer chain on the "
-          f"bit-accurate fixed-point model", flush=True)
-    first_lif.run(condition=RunSteps(num_steps=T),
-                  run_cfg=Loihi2SimCfg(select_tag="fixed_pt"))
-    out = snk.data.get()
-    first_lif.stop()
-
-    bad = []
-    for t in range(N):
-        col = out[:, t + L]
-        res = sum(int(col[k]) << k for k in range(8))
-        leq = int(col[8])
-        want = reference(int(xa[t]), int(xb[t]))
-        if (res, leq) != want:
-            bad.append((t, (res, leq), want))
-    print(f"  {N} operand pairs, pipelined one per time step: "
-          f"{'all exact' if not bad else f'{len(bad)} FAILED {bad[:3]}'}",
-          flush=True)
-
-    print(f"  one unit weight moves the membrane potential by 128 units and "
-          f"the comparator sits midway between the firing and non-firing "
-          f"values, so the margin of Theorem 6.2 is 64 units of membrane "
-          f"potential on this model")
-
-    ok = not bad
-    json.dump({"backend": "Lava 0.10.0, fixed_pt tag (Loihi neuron model)",
-               "units": int(z["n_units"][0]), "layers": L,
-               "widths": [int(W.shape[0]) for W, _ in layers],
-               "worst_accumulation": worst, "patterns": N,
-               "failures": len(bad), "margin_membrane_units": 64,
-               "weight_scale": 2, "synapse_granularity": 2,
-               "bias_offset": K, "ok": ok},
-              open(runs_path("paper_neuromorphic.json"), "w"), indent=1)
-    print("NEUROMORPHIC:", "PASS" if ok else "FAIL")
-    return 0 if ok else 1
-
-
-def akida() -> int:
-    """The same datapath on the Akida layer model."""
-    import numpy as np
-    import akida as ak
-    from akida import FullyConnected, InputData, Model
-
-    z = np.load(NPZ)
-    L = int(z["n_layers"][0])
-    n_in = int(z["n_inputs"][0])
-    layers = [(z[f"W{i}"], z[f"b{i}"]) for i in range(L)]
-    print(f"  Akida {ak.__version__}; devices attached: {len(ak.devices())}; "
-          f"{L} layers of widths {[int(W.shape[0]) for W, _ in layers]}",
-          flush=True)
-
-    m = Model()
-    m.add(InputData(input_shape=(1, 1, n_in), input_bits=1))
-    for i, (W, b) in enumerate(layers):
-        m.add(FullyConnected(units=int(W.shape[0]), weights_bits=2,
-                             activation=True, act_bits=1, name=f"layer{i}"))
-        lay = m.get_layer(i + 1)
-        wv = np.zeros(lay.variables["weights"].shape, dtype=np.int8)
-        wv[0, 0, :, :] = W.T.astype(np.int8)
-        lay.variables["weights"] = wv
-        lay.variables["threshold"] = (-b - 1).astype(np.int32)
-
-    N = 65536                                        # every operand pair
-    xa = np.arange(N) % 256
-    xb = np.arange(N) // 256
-    X = np.zeros((N, 1, 1, n_in), dtype=np.uint8)
-    for k in range(8):
-        X[:, 0, 0, k] = (xa >> k) & 1
-        X[:, 0, 0, 8 + k] = (xb >> k) & 1
-    out = np.concatenate([m.forward(X[i:i + 8192]).reshape(-1, out_w)
-                          for i in range(0, N, 8192)
-                          for out_w in [int(layers[-1][0].shape[0])]])
-
-    bad = []
-    for t in range(N):
-        res = sum(int(out[t, k]) << k for k in range(8))
-        leq = int(out[t, 8])
-        want = reference(int(xa[t]), int(xb[t]))
-        if (res, leq) != want:
-            bad.append((t, (res, leq), want))
-    print(f"  all {N} operand pairs forwarded through the layer stack: "
-          f"{'all exact' if not bad else f'{len(bad)} FAILED {bad[:3]}'}",
-          flush=True)
-    print(f"  weights are stored at two bits and thresholds as integers, so "
-          f"the circuit is represented without rounding")
-
-    ok = not bad
-    old = {}
-    p = runs_path("paper_neuromorphic.json")
-    if os.path.exists(p):
-        old = json.load(open(p))
-    old["akida"] = {"backend": f"akida {ak.__version__}, software backend",
-                    "layers": L, "patterns": N, "failures": len(bad),
-                    "weights_bits": 2, "act_bits": 1, "ok": ok}
-    json.dump(old, open(p, "w"), indent=1)
-    print("AKIDA:", "PASS" if ok else "FAIL")
-    return 0 if ok else 1
-
-
-def cmd_neuromorphic():
-    mode = sys.argv[1] if len(sys.argv) > 1 else "run"
-    sys.exit({"export": export, "run": run, "akida": akida}[mode]())
-
-
-COMMANDS = {'host': main_host, 'amplified': main_amplified, 'neuromorphic': cmd_neuromorphic}
+COMMANDS = {'host': main_host, 'amplified': main_amplified}
 
 
 if __name__ == "__main__":

src/paper.py

@@ -1048,6 +1048,30 @@ 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."""
+    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()
+    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())
+
+
 def main_rocq():
     for tool in ('rocq', 'make', 'ocamlfind'):
         if shutil.which(tool) is None:
@@ -1075,13 +1099,15 @@ def main_rocq():
     if len(lines) != len(names) or any(l != 'Closed under the global context' for l in lines):
         print(out.stdout)
         return 1
+    host = host_extraction()
     ext = subprocess.run([sys.executable, os.path.join(REPO, 'src', 'twohead.py'), 'net', 'extract'],
                          capture_output=True, text=True)
-    identical = ext.returncode == 0 and '"identical": true' in ext.stdout
+    identical = ext.returncode == 0 and '"identical": true' in ext.stdout and host['identical']
     files = [l for l in open(os.path.join(ROCQ, '_CoqProject')).read().split() if l.endswith('.v')]
-    res = dict(rocq=version.splitlines()[0], files=len(files),
+    lines = sum(len(open(os.path.join(ROCQ, f)).read().splitlines()) for f in files)
+    res = dict(rocq=version.splitlines()[0], files=len(files), lines=lines,
                build_seconds=round(build, 1), theorems={n: 'closed' for n in names},
-               extraction_identical=identical)
+               host_extraction=host, extraction_identical=identical)
     rec = json.load(open(RECORD)) if os.path.exists(RECORD) else {}
     rec.update(res)
     json.dump(rec, open(RECORD, 'w'), indent=1)

src/twohead.py

@@ -653,7 +653,7 @@ def main_net():
                                 sha256_generator=hashlib.sha256(ours).hexdigest(),
                                 sha256_rocq=hashlib.sha256(theirs).hexdigest()))
         for f in os.listdir(ex):
-            if f not in ('dump.ml', 'physnet.ml', 'physnet.mli'):
+            if not f.endswith(('.ml', '.mli')):
                 os.remove(os.path.join(ex, f))
         res = dict(members=members, identical=all(m['identical'] for m in members))
         net_update_record('extraction', res)
@@ -714,6 +714,7 @@ HALT = 8
 class Prog:
     def __init__(self):
         self.recs = []                           # (a0, w0, a1, w1, beta, ao), cells by name
+        self.ends = {}                           # record -> the unit of the host whose value it writes
         self.uid = 0
 
     def tmp(self):
@@ -853,6 +854,7 @@ def compile_host(P):
             P.threshold(t, lits, dst)
         else:
             _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)]
@@ -1082,7 +1084,7 @@ def build_stored():
     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))
+                n_host_records=n_host, host=(n, units, nxt), ends=P.ends)
 
 
 # ---------------------------------------------------------------------------
@@ -1233,6 +1235,118 @@ def check_stored(trials=40, seed=3, verbose=False):
     return dict(trials=trials, disagreements=bad, records=G, window_cells=S['top'])
 
 
+class BDD:
+    """Reduced ordered decision diagrams; a node is an integer, 0 and 1 the leaves."""
+    def __init__(self):
+        self.node = [None, None]
+        self.uniq, self.memo = {}, {}
+
+    def mk(self, v, lo, hi):
+        if lo == hi:
+            return lo
+        r = self.uniq.get((v, lo, hi))
+        if r is None:
+            r = self.uniq[(v, lo, hi)] = len(self.node)
+            self.node.append((v, lo, hi))
+        return r
+
+    def var(self, v):
+        return self.mk(v, 0, 1)
+
+    def ite(self, f, g, h):
+        if f < 2:
+            return g if f else h
+        if g == h:
+            return g
+        if g == 1 and h == 0:
+            return f
+        key = (f, g, h)
+        r = self.memo.get(key)
+        if r is None:
+            v = min(self.node[x][0] for x in key if x > 1)
+            lo = [x if x < 2 or self.node[x][0] != v else self.node[x][1] for x in key]
+            hi = [x if x < 2 or self.node[x][0] != v else self.node[x][2] for x in key]
+            r = self.memo[key] = self.mk(v, self.ite(*lo), self.ite(*hi))
+        return r
+
+    def record(self, w0, x, w1, y, beta):
+        """H(w0 x + w1 y + beta) of the bits x and y."""
+        val = lambda a, b: 1 if w0 * a + w1 * b + beta >= 0 else 0
+        return self.ite(x, self.ite(y, val(1, 1), val(1, 0)), self.ite(y, val(0, 1), val(0, 0)))
+
+    def atleast(self, t, lits):
+        """At least t of the literals (x, positive) are true."""
+        if t <= 0:
+            return 1
+        row = [1] + [0] * t
+        for x, pos in reversed(lits):
+            row = [1] + [self.ite(x, row[j - 1], row[j]) if pos else self.ite(x, row[j], row[j - 1])
+                         for j in range(1, t + 1)]
+        return row[t]
+
+
+def symbolic_check():
+    """The startup and step records of the image of S on decision diagrams over the signals of N_host."""
+    sys.setrecursionlimit(100000)
+    t0 = time.time()
+    S = build_stored()
+    n, units, nxt = host_units()
+    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']
+    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])
+        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)
+    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):
+        # 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):
+            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)
+            if k in ends:
+                u = ends[k]
+                agree[0] &= g == fn[u]
+                g = val[n + u]
+            window[ao] = g
+
+    # 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)] + \
+        [addr[('d', 'dest')]]
+    before = list(window)
+    run(window, 0, lo)
+    B0 = before[boot]
+    x0 = [0] * n
+    for j in range(256):
+        for t in range(8):
+            x0[mem_bit(j, t)] = (SR.M_STAR[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)]
+    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,
+                sha256_image=hashlib.sha256(S['image']).hexdigest(), nodes=len(D.node),
+                seconds=round(time.time() - t0, 1))
+
+
 def stored_update_record(key, value):
     rec = json.load(open(STORED_RECORD)) if os.path.exists(STORED_RECORD) else {}
     rec[key] = value
@@ -1281,6 +1395,11 @@ def cmd_stored():
         stored_update_record('pass_check', 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)
+        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)