ControllerBits

Comment and keyword shading is a reading aid only. It is not a verification marker; the evidence is the build record on the Build page.

1import Controller2import NimCorrBridge34/- Phase 4, Priority 3 (bit level): per-update circuits for the two-pass controller5   and their refinement.  Written by Claude (10 October 2026).  Lean 4.26.0, core/Std.67   State layout (B value bits, r counter bits; little-endian bit k at offset + k):8     mode 0 | acc 1.. | prev 1+B.. | valid 1+2B | sig 2+2B.. | idx 2+3B.. |9     selF 2+3B+r | selI 3+3B+r.. | selV 3+3B+2r.. | fnzF 3+4B+2r | fnzI 4+4B+2r.. |10     fnzV 4+4B+3r..   — 4 + 5B + 3r state bits;11   token bits: isRow 4+5B+3r, isReset 5+5B+3r, x 6+5B+3r.. .12   Each next-state bit and each output bit is an explicit formula of depth ≤ 8.13   REFINEMENT: decoding the evaluated next-state formulas gives exactly the semantic14   next state, and decoding the output formulas gives exactly the semantic output,15   for every state whose registers fit their fields (and no counter overflow). -/1617namespace NimAudit18namespace ControllerBits1920open Game Rollout Prob Attain Recurrent AC0 AC0.Circ Controller CorrBridge AttainCircuit2122def optI : Option (Nat × Nat) → Nat23  | some m => m.124  | none => 02526def optV : Option (Nat × Nat) → Nat27  | some m => m.228  | none => 02930def tokRow : Tok → Bool31  | .row _ => true32  | _ => false3334def tokRst : Tok → Bool35  | .reset => true36  | _ => false3738def tokX : Tok → Nat39  | .row x => x40  | _ => 04142/-- The register layout, generic in the payload (bits or circuits). -/43def layout {α : Type} (B r : Nat) (dflt m : α) (acc prev : Nat → α) (valid : α) (sig idx : Nat → α)44    (selF : α) (selI selV : Nat → α) (fnzF : α) (fnzI fnzV : Nat → α) (j : Nat) : α :=45  if j = 0 then m46  else if j < 1 + B then acc (j - 1)47  else if j < 1 + 2 * B then prev (j - (1 + B))48  else if j = 1 + 2 * B then valid49  else if j < 2 + 3 * B then sig (j - (2 + 2 * B))50  else if j < 2 + 3 * B + r then idx (j - (2 + 3 * B))51  else if j = 2 + 3 * B + r then selF52  else if j < 3 + 3 * B + 2 * r then selI (j - (3 + 3 * B + r))53  else if j < 3 + 4 * B + 2 * r then selV (j - (3 + 3 * B + 2 * r))54  else if j = 3 + 4 * B + 2 * r then fnzF55  else if j < 4 + 4 * B + 3 * r then fnzI (j - (4 + 4 * B + 2 * r))56  else if j < 4 + 5 * B + 3 * r then fnzV (j - (4 + 4 * B + 3 * r))57  else dflt5859theorem layout_map {α β : Type} (f : α → β) (B r : Nat) (d m : α) (acc prev : Nat → α) (valid : α)60    (sig idx : Nat → α) (selF : α) (selI selV : Nat → α) (fnzF : α) (fnzI fnzV : Nat → α) (j : Nat) :61    f (layout B r d m acc prev valid sig idx selF selI selV fnzF fnzI fnzV j) =62      layout B r (f d) (f m) (fun k => f (acc k)) (fun k => f (prev k)) (f valid) (fun k => f (sig k))63        (fun k => f (idx k)) (f selF) (fun k => f (selI k)) (fun k => f (selV k)) (f fnzF)64        (fun k => f (fnzI k)) (fun k => f (fnzV k)) j := by65  simp only [layout, apply_ite f]6667theorem layout_congr {α : Type} {B r : Nat} {d m d' m' : α} {acc prev acc' prev' : Nat → α}68    {valid valid' : α} {sig idx sig' idx' : Nat → α} {selF selF' : α} {selI selV selI' selV' : Nat → α}69    {fnzF fnzF' : α} {fnzI fnzV fnzI' fnzV' : Nat → α}70    (hd : d = d') (hm : m = m') (hacc : ∀ k < B, acc k = acc' k) (hprev : ∀ k < B, prev k = prev' k)71    (hvalid : valid = valid') (hsig : ∀ k < B, sig k = sig' k) (hidx : ∀ q < r, idx q = idx' q)72    (hselF : selF = selF') (hselI : ∀ q < r, selI q = selI' q) (hselV : ∀ k < B, selV k = selV' k)73    (hfnzF : fnzF = fnzF') (hfnzI : ∀ q < r, fnzI q = fnzI' q) (hfnzV : ∀ k < B, fnzV k = fnzV' k)74    (j : Nat) :75    layout B r d m acc prev valid sig idx selF selI selV fnzF fnzI fnzV j =76      layout B r d' m' acc' prev' valid' sig' idx' selF' selI' selV' fnzF' fnzI' fnzV' j := by77  simp only [layout]78  by_cases h1 : j = 079  · simp only [if_pos h1]; exact hm80  by_cases h2 : j < 1 + B81  · simp only [if_neg h1, if_pos h2]; exact hacc _ (by omega)82  by_cases h3 : j < 1 + 2 * B83  · simp only [if_neg h1, if_neg h2, if_pos h3]; exact hprev _ (by omega)84  by_cases h4 : j = 1 + 2 * B85  · simp only [if_neg h1, if_neg h2, if_neg h3, if_pos h4]; exact hvalid86  by_cases h5 : j < 2 + 3 * B87  · simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_pos h5]; exact hsig _ (by omega)88  by_cases h6 : j < 2 + 3 * B + r89  · simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_pos h6]; exact hidx _ (by omega)90  by_cases h7 : j = 2 + 3 * B + r91  · simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_neg h6, if_pos h7]; exact hselF92  by_cases h8 : j < 3 + 3 * B + 2 * r93  · simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_neg h6, if_neg h7, if_pos h8]; exact hselI _ (by omega)94  by_cases h9 : j < 3 + 4 * B + 2 * r95  · simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_neg h6, if_neg h7, if_neg h8, if_pos h9]; exact hselV _ (by omega)96  by_cases h10 : j = 3 + 4 * B + 2 * r97  · simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_neg h6, if_neg h7, if_neg h8, if_neg h9, if_pos h10]; exact hfnzF98  by_cases h11 : j < 4 + 4 * B + 3 * r99  · simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_neg h6, if_neg h7, if_neg h8, if_neg h9, if_neg h10, if_pos h11]; exact hfnzI _ (by omega)100  by_cases h12 : j < 4 + 5 * B + 3 * r101  · simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_neg h6, if_neg h7, if_neg h8, if_neg h9, if_neg h10, if_neg h11, if_pos h12]; exact hfnzV _ (by omega)102  simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_neg h6, if_neg h7, if_neg h8, if_neg h9, if_neg h10, if_neg h11, if_neg h12]; exact hd103104/-- The canonical state vector (4 + 5B + 3r bits; false beyond). -/105def sbits (B r : Nat) (s : CState) : Nat → Bool :=106  layout B r false s.replayMode s.acc.testBit s.prev.testBit s.valid s.sig.testBit s.idx.testBit107    s.sel.isSome (optI s.sel).testBit (optV s.sel).testBit s.fnz.isSome (optI s.fnz).testBit108    (optV s.fnz).testBit109110/-- Token wires. -/111def tbits (B r : Nat) (t : Tok) (j : Nat) : Bool :=112  if j = 4 + 5 * B + 3 * r then tokRow t113  else if j = 5 + 5 * B + 3 * r then tokRst t114  else (tokX t).testBit (j - (6 + 5 * B + 3 * r))115116/-- The input vector of the per-update circuits: an arbitrary state vector v on the117    state wires, the token on the token wires. -/118def inp (B r : Nat) (v : Nat → Bool) (t : Tok) (j : Nat) : Bool :=119  if j < 4 + 5 * B + 3 * r then v j else tbits B r t j120121/-- Canonical bit encoding of (state, token). -/122def enc (B r : Nat) (s : CState) (t : Tok) : Nat → Bool := inp B r (sbits B r s) t123124section EncLemmas125variable (B r : Nat) (s : CState) (t : Tok)126127theorem e_mode : enc B r s t 0 = s.replayMode := by128  simp (disch := omega) only [enc, inp, sbits, layout, if_pos, ↓reduceIte]129theorem e_acc {k : Nat} (hk : k < B) : enc B r s t (1 + k) = s.acc.testBit k := by130  simp (disch := omega) only [enc, inp, sbits, layout, tbits, if_neg, if_pos, ↓reduceIte]; congr 1; omega131theorem e_prev {k : Nat} (hk : k < B) : enc B r s t (1 + B + k) = s.prev.testBit k := by132  simp (disch := omega) only [enc, inp, sbits, layout, tbits, if_neg, if_pos, ↓reduceIte]; congr 1; omega133theorem e_valid : enc B r s t (1 + 2 * B) = s.valid := by134  simp (disch := omega) only [enc, inp, sbits, layout, tbits, if_neg, if_pos, ↓reduceIte]135theorem e_sig {k : Nat} (hk : k < B) : enc B r s t (2 + 2 * B + k) = s.sig.testBit k := by136  simp (disch := omega) only [enc, inp, sbits, layout, tbits, if_neg, if_pos, ↓reduceIte]; congr 1; omega137theorem e_idx {q : Nat} (hq : q < r) : enc B r s t (2 + 3 * B + q) = s.idx.testBit q := by138  simp (disch := omega) only [enc, inp, sbits, layout, tbits, if_neg, if_pos, ↓reduceIte]; congr 1; omega139theorem e_selF : enc B r s t (2 + 3 * B + r) = s.sel.isSome := by140  simp (disch := omega) only [enc, inp, sbits, layout, tbits, if_neg, if_pos, ↓reduceIte]141theorem e_selI {q : Nat} (hq : q < r) : enc B r s t (3 + 3 * B + r + q) = (optI s.sel).testBit q := by142  simp (disch := omega) only [enc, inp, sbits, layout, tbits, if_neg, if_pos, ↓reduceIte]; congr 1; omega143theorem e_selV {k : Nat} (hk : k < B) : enc B r s t (3 + 3 * B + 2 * r + k) = (optV s.sel).testBit k := by144  simp (disch := omega) only [enc, inp, sbits, layout, tbits, if_neg, if_pos, ↓reduceIte]; congr 1; omega145theorem e_fnzF : enc B r s t (3 + 4 * B + 2 * r) = s.fnz.isSome := by146  simp (disch := omega) only [enc, inp, sbits, layout, tbits, if_neg, if_pos, ↓reduceIte]147theorem e_fnzI {q : Nat} (hq : q < r) : enc B r s t (4 + 4 * B + 2 * r + q) = (optI s.fnz).testBit q := by148  simp (disch := omega) only [enc, inp, sbits, layout, tbits, if_neg, if_pos, ↓reduceIte]; congr 1; omega149theorem e_fnzV {k : Nat} (hk : k < B) : enc B r s t (4 + 4 * B + 3 * r + k) = (optV s.fnz).testBit k := by150  simp (disch := omega) only [enc, inp, sbits, layout, tbits, if_neg, if_pos, ↓reduceIte]; congr 1; omega151theorem e_row : enc B r s t (4 + 5 * B + 3 * r) = tokRow t := by152  simp (disch := omega) only [enc, inp, sbits, layout, tbits, if_neg, if_pos, ↓reduceIte]153theorem e_rst : enc B r s t (5 + 5 * B + 3 * r) = tokRst t := by154  simp (disch := omega) only [enc, inp, sbits, layout, tbits, if_neg, if_pos, ↓reduceIte]155theorem e_x (k : Nat) : enc B r s t (6 + 5 * B + 3 * r + k) = (tokX t).testBit k := by156  simp (disch := omega) only [enc, inp, sbits, layout, tbits, if_neg, if_pos, ↓reduceIte]; congr 1; omega157158end EncLemmas159160/-! ## Arithmetic facts -/161162theorem testBit_succ : ∀ (q n : Nat),163    (n + 1).testBit q = xor (n.testBit q) (decide (∀ t < q, n.testBit t = true))164  | 0, n => by rw [testBit0_succ]; simp165  | q + 1, n => by166    rw [← Nat.testBit_div_two (n + 1) q, ← Nat.testBit_div_two n q]167    rcases Nat.mod_two_eq_zero_or_one n with h | h168    · rw [show (n + 1) / 2 = n / 2 by omega]169      have : ¬ ∀ t < q + 1, n.testBit t = true := by170        intro hall; have := hall 0 (by omega); simp [Nat.testBit_zero, h] at this171      simp [this]172    · rw [show (n + 1) / 2 = n / 2 + 1 by omega, testBit_succ q (n / 2)]173      congr 1174      apply Bool.eq_iff_iff.mpr175      simp only [decide_eq_true_iff]176      constructor177      · intro hall t ht178        cases t with179        | zero => simp [Nat.testBit_zero, h]180        | succ t => rw [← Nat.testBit_div_two]; exact hall t (by omega)181      · intro hall t ht; rw [Nat.testBit_div_two]; exact hall (t + 1) (by omega)182183theorem top_bit {σ k : Nat} (hσ0 : σ ≠ 0) (hk : σ.testBit k = true)184    (habove : ∀ k', k < k' → σ.testBit k' = false) : σ.log2 = k := by185  rw [Nat.log2_eq_iff hσ0]186  refine ⟨Nat.ge_two_pow_of_testBit hk, ?_⟩187  apply Nat.lt_pow_two_of_testBit188  intro i hi; exact habove i (by omega)189190theorem canc_iff {σ x B : Nat} (hσ : σ < 2 ^ B) :191    (σ ≠ 0 ∧ x ^^^ σ < x) ↔ ∃ k < B, σ.testBit k = true ∧ x.testBit k = true ∧192      ∀ t < B - 1 - k, σ.testBit (k + 1 + t) = false := by193  have above : ∀ i, B ≤ i → σ.testBit i = false := fun i hi =>194    Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hσ (Nat.pow_le_pow_right (by decide) hi))195  constructor196  · rintro ⟨h0, hlt⟩197    have hx := (cancel_iff_bit h0).1 hlt198    have htop : σ.testBit σ.log2 = true := by199      cases hb : σ.testBit σ.log2 with200      | true => rfl201      | false =>202        exfalso203        have : σ < 2 ^ σ.log2 := by204          apply Nat.lt_pow_two_of_testBit205          intro i hi206          by_cases hik : i = σ.log2207          · subst hik; exact hb208          · exact Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le Nat.lt_log2_self209              (Nat.pow_le_pow_right (by decide) (by omega)))210        exact absurd (Nat.log2_self_le h0) (Nat.not_le.mpr this)211    have hkB : σ.log2 < B := by212      rcases Nat.lt_or_ge σ.log2 B with h | h213      · exact h214      · rw [above _ h] at htop; cases htop215    refine ⟨σ.log2, hkB, htop, hx, fun t _ => ?_⟩216    exact Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le Nat.lt_log2_self217      (Nat.pow_le_pow_right (by decide) (by omega)))218  · rintro ⟨k, hk, hσk, hxk, habove⟩219    have h0 : σ ≠ 0 := by intro h; subst h; simp at hσk220    have hlog : σ.log2 = k := by221      apply top_bit h0 hσk222      intro k' hk'223      rcases Nat.lt_or_ge k' B with h | h224      · have := habove (k' - k - 1) (by omega)225        rwa [show k + 1 + (k' - k - 1) = k' by omega] at this226      · exact above k' h227    refine ⟨h0, (cancel_iff_bit h0).2 ?_⟩228    rw [hlog]; exact hxk229230theorem pos_iff_bitLE {x B : Nat} (hx : x < 2 ^ B) : 0 < x ↔ ∃ k < B, x.testBit k = true := by231  constructor232  · intro h233    obtain ⟨i, hi⟩ := Nat.exists_testBit_of_ne_zero (Nat.pos_iff_ne_zero.mp h)234    refine ⟨i, ?_, hi⟩235    rcases Nat.lt_or_ge i B with h' | h'236    · exact h'237    · rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le hx (Nat.pow_le_pow_right (by decide) h'))] at hi238      cases hi239  · rintro ⟨k, _, hk⟩240    rcases Nat.eq_zero_or_pos x with h | h241    · subst h; simp at hk242    · exact h243244/-! ## The circuits -/245246section Circuits247variable (B r : Nat)248249def Rc : Circ := input (5 + 5 * B + 3 * r)250def Wc : Circ := and [input (4 + 5 * B + 3 * r), not (input (5 + 5 * B + 3 * r))]251def Ec : Circ := and [not (input (4 + 5 * B + 3 * r)), not (input (5 + 5 * B + 3 * r))]252def Mc : Circ := input 0253def mux (c a b : Circ) : Circ := or [and [c, a], and [not c, b]]254def xI (k : Nat) : Circ := input (6 + 5 * B + 3 * r + k)255256/-- σ ≠ 0 ∧ x XOR σ < x for the stored summary σ and the row x. -/257def cancC : Circ :=258  or ((List.range B).map (fun k => and ([input (2 + 2 * B + k), xI B r k] ++259    (List.range (B - 1 - k)).map (fun t => not (input (2 + 2 * B + (k + 1 + t)))))))260261def nzC : Circ := or ((List.range B).map (fun k => xI B r k))262263/-- Bit k of x − 1. -/264def decC (k : Nat) : Circ := xor2 (xI B r k) (and ((List.range k).map (fun t => not (xI B r t))))265266/-- Bit q of idx + 1. -/267def incC (q : Nat) : Circ :=268  xor2 (input (2 + 3 * B + q)) (and ((List.range q).map (fun t => input (2 + 3 * B + t))))269270def modeN : Circ := and [not (Rc B r), or [and [Wc B r, Mc], and [Ec B r, not Mc]]]271def accN (k : Nat) : Circ :=272  and [not (Rc B r), or [and [Wc B r, not Mc, xor2 (input (1 + k)) (xI B r k)],273    and [Wc B r, Mc, input (1 + k)], and [Ec B r, Mc, input (1 + k)]]]274def prevN (k : Nat) : Circ :=275  and [not (Rc B r), mux (and [Ec B r, not Mc]) (input (1 + k)) (input (1 + B + k))]276def validN : Circ := and [not (Rc B r), or [and [Ec B r, not Mc], input (1 + 2 * B)]]277def sigN (k : Nat) : Circ :=278  and [not (Rc B r), mux (and [Ec B r, not Mc]) (input (1 + k)) (input (2 + 2 * B + k))]279def idxN (q : Nat) : Circ := and [not (Rc B r), Wc B r, mux Mc (incC B q) (input (2 + 3 * B + q))]280def selFN : Circ := and [not (Rc B r), Wc B r, or [input (2 + 3 * B + r), and [Mc, cancC B r]]]281def selIN (q : Nat) : Circ :=282  and [not (Rc B r), Wc B r, or [and [input (2 + 3 * B + r), input (3 + 3 * B + r + q)],283    and [not (input (2 + 3 * B + r)), Mc, cancC B r, input (2 + 3 * B + q)]]]284def selVN (k : Nat) : Circ :=285  and [not (Rc B r), Wc B r, or [and [input (2 + 3 * B + r), input (3 + 3 * B + 2 * r + k)],286    and [not (input (2 + 3 * B + r)), Mc, cancC B r, xor2 (xI B r k) (input (2 + 2 * B + k))]]]287def fnzFN : Circ := and [not (Rc B r), Wc B r, or [input (3 + 4 * B + 2 * r), and [Mc, nzC B r]]]288def fnzIN (q : Nat) : Circ :=289  and [not (Rc B r), Wc B r, or [and [input (3 + 4 * B + 2 * r), input (4 + 4 * B + 2 * r + q)],290    and [not (input (3 + 4 * B + 2 * r)), Mc, nzC B r, input (2 + 3 * B + q)]]]291def fnzVN (k : Nat) : Circ :=292  and [not (Rc B r), Wc B r, or [and [input (3 + 4 * B + 2 * r), input (4 + 4 * B + 3 * r + k)],293    and [not (input (3 + 4 * B + 2 * r)), Mc, nzC B r, decC B r k]]]294295/-- Output formulas. -/296def sumOutC : Circ := and [Ec B r, not Mc]297def sumBitC (k : Nat) : Circ := input (1 + k)298def diffBitC (k : Nat) : Circ := xor2 (input (1 + B + k)) (input (1 + k))299def diffValidC : Circ := input (1 + 2 * B)300def moveOutC : Circ := and [Ec B r, Mc]301def moveValidC : Circ := or [input (2 + 3 * B + r), input (3 + 4 * B + 2 * r)]302def moveIC (q : Nat) : Circ := mux (input (2 + 3 * B + r)) (input (3 + 3 * B + r + q)) (input (4 + 4 * B + 2 * r + q))303def moveVC (k : Nat) : Circ :=304  mux (input (2 + 3 * B + r)) (input (3 + 3 * B + 2 * r + k)) (input (4 + 4 * B + 3 * r + k))305306end Circuits307308/-- Decoded output from the evaluated output formulas. -/309def decodeOut (B r : Nat) (z : Nat → Bool) : Option COut :=310  if eval z (sumOutC B r) then311    some (COut.summary (ofBits B (fun k => eval z (sumBitC k)))312      (if eval z (diffValidC B) then some (ofBits B (fun k => eval z (diffBitC B k))) else none))313  else if eval z (moveOutC B r) then314    some (COut.move (if eval z (moveValidC B r) then315      some (ofBits r (fun q => eval z (moveIC B r q)), ofBits B (fun k => eval z (moveVC B r k))) else none))316  else none317318/-! ## Evaluation of the arithmetic sub-circuits -/319320section Eval321variable {B r : Nat} {s : CState} {t : Tok}322323theorem ev_inc {q : Nat} (hq : q < r) : eval (enc B r s t) (incC B q) = (s.idx + 1).testBit q := by324  rw [incC, eval_xor2, testBit_succ, eval_input, e_idx B r s t hq]325  congr 1326  apply Bool.eq_iff_iff.mpr327  simp only [eval_and, List.all_map, List.all_eq_true, List.mem_range, Function.comp_apply, eval_input,328    decide_eq_true_iff]329  constructor330  · intro h u hu; rw [← e_idx B r s t (show u < r by omega)]; exact h u hu331  · intro h u hu; rw [e_idx B r s t (show u < r by omega)]; exact h u hu332333theorem ev_canc (hσ : s.sig < 2 ^ B) :334    eval (enc B r s t) (cancC B r) = decide (s.sig ≠ 0 ∧ tokX t ^^^ s.sig < tokX t) := by335  apply Bool.eq_iff_iff.mpr336  rw [decide_eq_true_iff, canc_iff hσ]337  simp only [cancC, xI, eval_or, eval_and, eval_not, eval_input, List.any_map, List.all_append,338    List.all_cons, List.all_nil, List.all_map, List.any_eq_true, List.all_eq_true, List.mem_range,339    Function.comp_apply, Bool.and_eq_true, Bool.not_eq_true', e_x, Bool.and_true]340  constructor341  · rintro ⟨k, hk, ⟨h1, h2⟩, h3⟩342    refine ⟨k, hk, ?_, h2, fun u hu => ?_⟩343    · rwa [e_sig B r s t hk] at h1344    · have := h3 u hu; rwa [e_sig B r s t (show k + 1 + u < B by omega)] at this345  · rintro ⟨k, hk, h1, h2, h3⟩346    refine ⟨k, hk, ⟨?_, h2⟩, fun u hu => ?_⟩347    · rwa [e_sig B r s t hk]348    · rw [e_sig B r s t (show k + 1 + u < B by omega)]; exact h3 u hu349350theorem ev_nz (hx : tokX t < 2 ^ B) : eval (enc B r s t) (nzC B r) = decide (0 < tokX t) := by351  apply Bool.eq_iff_iff.mpr352  rw [decide_eq_true_iff, pos_iff_bitLE hx]353  simp only [nzC, xI, eval_or, eval_input, List.any_map, List.any_eq_true, List.mem_range,354    Function.comp_apply, e_x]355356theorem ev_dec (hx : 0 < tokX t) (k : Nat) : eval (enc B r s t) (decC B r k) = (tokX t - 1).testBit k := by357  rw [decC, eval_xor2, testBit_pred _ hx, xI, eval_input, e_x]358  congr 1359  apply Bool.eq_iff_iff.mpr360  simp only [eval_and, List.all_map, List.all_eq_true, List.mem_range, Function.comp_apply, eval_not,361    eval_input, xI, e_x, decide_eq_true_iff, Bool.not_eq_true']362363end Eval364365/-! ## Bit-level correctness of every next-state formula -/366367section Fields368variable {B r : Nat} {s : CState} {t : Tok}369370theorem f_mode : eval (enc B r s t) (modeN B r) = (cstep s t).1.replayMode := by371  cases t <;> cases hm : s.replayMode <;>372    simp [modeN, Rc, Wc, Ec, Mc, e_mode, e_row, e_rst, tokRow, tokRst, cstep, cinit, hm]373374theorem f_acc {k : Nat} (hk : k < B) : eval (enc B r s t) (accN B r k) = (cstep s t).1.acc.testBit k := by375  cases t <;> cases hm : s.replayMode <;>376    simp [accN, Rc, Wc, Ec, Mc, xI, e_mode, e_row, e_rst, e_acc, e_x, hk, tokRow, tokRst, tokX, cstep,377      cinit, hm, eval_xor2, Nat.testBit_xor]378379theorem f_prev {k : Nat} (hk : k < B) : eval (enc B r s t) (prevN B r k) = (cstep s t).1.prev.testBit k := by380  cases t <;> cases hm : s.replayMode <;>381    simp [prevN, mux, Rc, Wc, Ec, Mc, e_mode, e_row, e_rst, e_acc, e_prev, hk, tokRow, tokRst, cstep,382      cinit, hm]383384theorem f_valid : eval (enc B r s t) (validN B r) = (cstep s t).1.valid := by385  cases t <;> cases hm : s.replayMode <;>386    simp [validN, Rc, Wc, Ec, Mc, e_mode, e_row, e_rst, e_valid, tokRow, tokRst, cstep, cinit, hm]387388theorem f_sig {k : Nat} (hk : k < B) : eval (enc B r s t) (sigN B r k) = (cstep s t).1.sig.testBit k := by389  cases t <;> cases hm : s.replayMode <;>390    simp [sigN, mux, Rc, Wc, Ec, Mc, e_mode, e_row, e_rst, e_acc, e_sig, hk, tokRow, tokRst, cstep,391      cinit, hm]392393theorem f_idx {q : Nat} (hq : q < r) : eval (enc B r s t) (idxN B r q) = (cstep s t).1.idx.testBit q := by394  cases t <;> cases hm : s.replayMode <;>395    simp [idxN, mux, Rc, Wc, Ec, Mc, e_mode, e_row, e_rst, e_idx, hq, ev_inc hq, tokRow, tokRst, cstep,396      cinit, hm, replayStep]397398theorem f_selF (hσ : s.sig < 2 ^ B) : eval (enc B r s t) (selFN B r) = (cstep s t).1.sel.isSome := by399  cases t with400  | reset => simp [selFN, Rc, e_rst, tokRst, cstep, cinit]401  | sep => cases hm : s.replayMode <;> simp [selFN, Rc, Wc, e_rst, e_row, tokRst, tokRow, cstep, hm]402  | row x =>403    cases hm : s.replayMode <;> cases hs : s.sel <;>404      simp [selFN, Rc, Wc, Mc, e_rst, e_row, e_mode, e_selF, ev_canc hσ, tokRst, tokRow, tokX, cstep, hm, hs,405        replayStep] <;>406      (by_cases h1 : s.sig = 0 <;> by_cases h2 : x ^^^ s.sig < x <;> simp [h1, h2])407408theorem f_selI {q : Nat} (hq : q < r) (hσ : s.sig < 2 ^ B) :409    eval (enc B r s t) (selIN B r q) = (optI (cstep s t).1.sel).testBit q := by410  cases t with411  | reset => simp [selIN, Rc, e_rst, tokRst, cstep, cinit, optI]412  | sep => cases hm : s.replayMode <;> simp [selIN, Rc, Wc, e_rst, e_row, tokRst, tokRow, cstep, hm, optI]413  | row x =>414    cases hm : s.replayMode <;> cases hs : s.sel <;>415      simp [selIN, Rc, Wc, Mc, e_rst, e_row, e_mode, e_selF, e_selI, e_idx, hq, ev_canc hσ, tokRst, tokRow,416        tokX, cstep, hm, hs, replayStep, optI] <;>417      (by_cases h1 : s.sig = 0 <;> by_cases h2 : x ^^^ s.sig < x <;> simp [h1, h2, optI])418419theorem f_selV {k : Nat} (hk : k < B) (hσ : s.sig < 2 ^ B) :420    eval (enc B r s t) (selVN B r k) = (optV (cstep s t).1.sel).testBit k := by421  cases t with422  | reset => simp [selVN, Rc, e_rst, tokRst, cstep, cinit, optV]423  | sep => cases hm : s.replayMode <;> simp [selVN, Rc, Wc, e_rst, e_row, tokRst, tokRow, cstep, hm, optV]424  | row x =>425    cases hm : s.replayMode <;> cases hs : s.sel <;>426      simp [selVN, Rc, Wc, Mc, xI, e_rst, e_row, e_mode, e_selF, e_selV, e_sig, e_x, hk, ev_canc hσ, tokRst,427        tokRow, tokX, cstep, hm, hs, replayStep, optV, eval_xor2, Nat.testBit_xor] <;>428      (by_cases h1 : s.sig = 0 <;> by_cases h2 : x ^^^ s.sig < x <;> simp [h1, h2, optV, Nat.testBit_xor])429430theorem f_fnzF (hx : tokX t < 2 ^ B) : eval (enc B r s t) (fnzFN B r) = (cstep s t).1.fnz.isSome := by431  cases t with432  | reset => simp [fnzFN, Rc, e_rst, tokRst, cstep, cinit]433  | sep => cases hm : s.replayMode <;> simp [fnzFN, Rc, Wc, e_rst, e_row, tokRst, tokRow, cstep, hm]434  | row x =>435    cases hm : s.replayMode <;> cases hs : s.fnz <;>436      simp [fnzFN, Rc, Wc, Mc, e_rst, e_row, e_mode, e_fnzF, ev_nz hx, tokRst, tokRow, tokX, cstep, hm, hs,437        replayStep] <;>438      (by_cases h1 : 0 < x <;> simp [h1])439440theorem f_fnzI {q : Nat} (hq : q < r) (hx : tokX t < 2 ^ B) :441    eval (enc B r s t) (fnzIN B r q) = (optI (cstep s t).1.fnz).testBit q := by442  cases t with443  | reset => simp [fnzIN, Rc, e_rst, tokRst, cstep, cinit, optI]444  | sep => cases hm : s.replayMode <;> simp [fnzIN, Rc, Wc, e_rst, e_row, tokRst, tokRow, cstep, hm, optI]445  | row x =>446    cases hm : s.replayMode <;> cases hs : s.fnz <;>447      simp [fnzIN, Rc, Wc, Mc, e_rst, e_row, e_mode, e_fnzF, e_fnzI, e_idx, hq, ev_nz hx, tokRst, tokRow,448        tokX, cstep, hm, hs, replayStep, optI] <;>449      (by_cases h1 : 0 < x <;> simp [h1, optI])450451theorem f_fnzV {k : Nat} (hk : k < B) (hx : tokX t < 2 ^ B) :452    eval (enc B r s t) (fnzVN B r k) = (optV (cstep s t).1.fnz).testBit k := by453  cases t with454  | reset => simp [fnzVN, Rc, e_rst, tokRst, cstep, cinit, optV]455  | sep => cases hm : s.replayMode <;> simp [fnzVN, Rc, Wc, e_rst, e_row, tokRst, tokRow, cstep, hm, optV]456  | row x =>457    by_cases hx0 : 0 < x458    · have hd := fun k => ev_dec (B := B) (r := r) (s := s) (t := Tok.row x) (by simpa [tokX] using hx0) k459      simp only [tokX] at hd460      cases hm : s.replayMode <;> cases hs : s.fnz <;>461        simp [fnzVN, Rc, Wc, Mc, e_rst, e_row, e_mode, e_fnzF, e_fnzV, hk, ev_nz hx, hd, hx0, tokRst, tokRow,462          tokX, cstep, hm, hs, replayStep, optV]463    · have hx0' : x = 0 := by omega464      subst hx0'465      cases hm : s.replayMode <;> cases hs : s.fnz <;>466        simp [fnzVN, Rc, Wc, Mc, e_rst, e_row, e_mode, e_fnzF, e_fnzV, hk, ev_nz hx, tokRst, tokRow,467          tokX, cstep, hm, hs, replayStep, optV]468469end Fields470471/-! ## The per-update circuit and its refinement -/472473/-- The next-state circuit for wire j (constant false beyond the 4 + 5B + 3r state wires). -/474def nextC (B r : Nat) : Nat → Circ :=475  layout B r (const false) (modeN B r) (accN B r) (prevN B r) (validN B r) (sigN B r) (idxN B r)476    (selFN B r) (selIN B r) (selVN B r) (fnzFN B r) (fnzIN B r) (fnzVN B r)477478/-- One update of the bit-level machine: evaluate the next-state circuits and the output479    circuits on (state vector, token). -/480def bstep (B r : Nat) (v : Nat → Bool) (t : Tok) : (Nat → Bool) × Option COut :=481  (fun j => eval (inp B r v t) (nextC B r j), decodeOut B r (inp B r v t))482483/-- Field-width hypotheses needed for one exact update. -/484structure Decodable (B r : Nat) (s : CState) (t : Tok) : Prop where485  acc : s.acc < 2 ^ B486  prev : s.prev < 2 ^ B487  sig : s.sig < 2 ^ B488  sel : ∀ i v, s.sel = some (i, v) → i < 2 ^ r ∧ v < 2 ^ B489  fnz : ∀ i v, s.fnz = some (i, v) → i < 2 ^ r ∧ v < 2 ^ B490  tok : tokX t < 2 ^ B491492section Refine493variable {B r : Nat} {s : CState} {t : Tok}494495theorem step_state (hd : Decodable B r s t) :496    (fun j => eval (enc B r s t) (nextC B r j)) = sbits B r (cstep s t).1 := by497  funext j498  unfold nextC sbits499  rw [layout_map (eval (enc B r s t))]500  apply layout_congr501  · simp502  · exact f_mode503  · intro k hk; exact f_acc hk504  · intro k hk; exact f_prev hk505  · exact f_valid506  · intro k hk; exact f_sig hk507  · intro q hq; exact f_idx hq508  · exact f_selF hd.sig509  · intro q hq; exact f_selI hq hd.sig510  · intro k hk; exact f_selV hk hd.sig511  · exact f_fnzF hd.tok512  · intro q hq; exact f_fnzI hq hd.tok513  · intro k hk; exact f_fnzV hk hd.tok514515theorem step_out (hd : Decodable B r s t) : decodeOut B r (enc B r s t) = (cstep s t).2 := by516  cases t with517  | reset => simp [decodeOut, sumOutC, moveOutC, Ec, Mc, e_row, e_rst, tokRow, tokRst, cstep]518  | row x =>519    cases hm : s.replayMode <;>520      simp [decodeOut, sumOutC, moveOutC, Ec, Mc, e_row, e_rst, tokRow, tokRst, cstep, hm]521  | sep =>522    have hA : ofBits B (fun k => eval (enc B r s Tok.sep) (sumBitC k)) = s.acc :=523      ofBits_testBit_eq hd.acc _ (fun k hk => by simp [sumBitC, e_acc, hk])524    have hD : ofBits B (fun k => eval (enc B r s Tok.sep) (diffBitC B k)) = s.prev ^^^ s.acc :=525      ofBits_testBit_eq (Nat.xor_lt_two_pow hd.prev hd.acc) _526        (fun k hk => by simp [diffBitC, eval_xor2, e_acc, e_prev, hk, Nat.testBit_xor])527    cases hm : s.replayMode528    · simp [decodeOut, sumOutC, Ec, Mc, e_mode, e_row, e_rst, tokRow, tokRst, cstep, hm, hA, hD,529        diffValidC, e_valid]530    · cases hs : s.sel with531      | some p =>532        obtain ⟨i, v⟩ := p533        have hb := hd.sel i v hs534        have hI : ofBits r (fun q => eval (enc B r s Tok.sep) (moveIC B r q)) = i :=535          ofBits_testBit_eq hb.1 _ (fun q hq => by simp [moveIC, mux, e_selF, e_selI, hq, hs, optI])536        have hV : ofBits B (fun k => eval (enc B r s Tok.sep) (moveVC B r k)) = v :=537          ofBits_testBit_eq hb.2 _ (fun k hk => by simp [moveVC, mux, e_selF, e_selV, hk, hs, optV])538        simp [decodeOut, sumOutC, moveOutC, moveValidC, Ec, Mc, e_mode, e_row, e_rst, e_selF, tokRow,539          tokRst, cstep, hm, hs, hI, hV, firstSome]540      | none =>541        cases hf : s.fnz with542        | none =>543          simp [decodeOut, sumOutC, moveOutC, moveValidC, Ec, Mc, e_mode, e_row, e_rst, e_selF, e_fnzF,544            tokRow, tokRst, cstep, hm, hs, hf, firstSome]545        | some p =>546          obtain ⟨i, v⟩ := p547          have hb := hd.fnz i v hf548          have hI : ofBits r (fun q => eval (enc B r s Tok.sep) (moveIC B r q)) = i :=549            ofBits_testBit_eq hb.1 _ (fun q hq => by simp [moveIC, mux, e_selF, e_fnzI, hq, hs, hf, optI])550          have hV : ofBits B (fun k => eval (enc B r s Tok.sep) (moveVC B r k)) = v :=551            ofBits_testBit_eq hb.2 _ (fun k hk => by simp [moveVC, mux, e_selF, e_fnzV, hk, hs, hf, optV])552          simp [decodeOut, sumOutC, moveOutC, moveValidC, Ec, Mc, e_mode, e_row, e_rst, e_selF, e_fnzF,553            tokRow, tokRst, cstep, hm, hs, hf, hI, hV, firstSome]554555/-- ONE-STEP REFINEMENT: on the canonical encoding of a state, one evaluation of the556    per-update circuits yields the canonical encoding of the semantic successor state and557    (after decoding the output wires) exactly the semantic output. -/558theorem step_refines (hd : Decodable B r s t) :559    bstep B r (sbits B r s) t = (sbits B r (cstep s t).1, (cstep s t).2) := by560  show ((fun j => eval (enc B r s t) (nextC B r j)), decodeOut B r (enc B r s t)) = _561  rw [step_state hd, step_out hd]562563end Refine564565/-! ## Lossless decoding of the state vector -/566567def decodeS (B r : Nat) (v : Nat → Bool) : CState :=568  ⟨v 0, ofBits B (fun k => v (1 + k)), ofBits B (fun k => v (1 + B + k)), v (1 + 2 * B),569   ofBits B (fun k => v (2 + 2 * B + k)), ofBits r (fun q => v (2 + 3 * B + q)),570   if v (2 + 3 * B + r) then571     some (ofBits r (fun q => v (3 + 3 * B + r + q)), ofBits B (fun k => v (3 + 3 * B + 2 * r + k)))572   else none,573   if v (3 + 4 * B + 2 * r) then574     some (ofBits r (fun q => v (4 + 4 * B + 2 * r + q)), ofBits B (fun k => v (4 + 4 * B + 3 * r + k)))575   else none⟩576577/-- All registers fit their B-bit and r-bit fields. -/578structure FitsR (B r : Nat) (s : CState) : Prop where579  acc : s.acc < 2 ^ B580  prev : s.prev < 2 ^ B581  sig : s.sig < 2 ^ B582  idx : s.idx < 2 ^ r583  sel : ∀ i v, s.sel = some (i, v) → i < 2 ^ r ∧ v < 2 ^ B584  fnz : ∀ i v, s.fnz = some (i, v) → i < 2 ^ r ∧ v < 2 ^ B585586/-- LOSSLESS: the 4 + 5B + 3r state wires determine the semantic state exactly. -/587theorem decodeS_sbits {B r : Nat} {s : CState} (h : FitsR B r s) : decodeS B r (sbits B r s) = s := by588  have es : ∀ j, j < 4 + 5 * B + 3 * r → sbits B r s j = enc B r s Tok.sep j := fun j hj => by589    simp [enc, inp, hj]590  have hm : sbits B r s 0 = s.replayMode := by rw [es 0 (by omega)]; exact e_mode B r s _591  have ha : ofBits B (fun k => sbits B r s (1 + k)) = s.acc :=592    ofBits_testBit_eq h.acc _ (fun k hk => by rw [es (1 + k) (by omega)]; exact e_acc B r s _ hk)593  have hp : ofBits B (fun k => sbits B r s (1 + B + k)) = s.prev :=594    ofBits_testBit_eq h.prev _ (fun k hk => by rw [es (1 + B + k) (by omega)]; exact e_prev B r s _ hk)595  have hv : sbits B r s (1 + 2 * B) = s.valid := by rw [es (1 + 2 * B) (by omega)]; exact e_valid B r s _596  have hg : ofBits B (fun k => sbits B r s (2 + 2 * B + k)) = s.sig :=597    ofBits_testBit_eq h.sig _ (fun k hk => by rw [es (2 + 2 * B + k) (by omega)]; exact e_sig B r s _ hk)598  have hi : ofBits r (fun q => sbits B r s (2 + 3 * B + q)) = s.idx :=599    ofBits_testBit_eq h.idx _ (fun q hq => by rw [es (2 + 3 * B + q) (by omega)]; exact e_idx B r s _ hq)600  have hsel : (if sbits B r s (2 + 3 * B + r) then601      some (ofBits r (fun q => sbits B r s (3 + 3 * B + r + q)),602        ofBits B (fun k => sbits B r s (3 + 3 * B + 2 * r + k))) else none) = s.sel := by603    rw [es (2 + 3 * B + r) (by omega), e_selF]604    cases hs : s.sel with605    | none => rfl606    | some p =>607      obtain ⟨i, v⟩ := p608      obtain ⟨hi', hv'⟩ := h.sel i v hs609      simp only [Option.isSome_some, if_true]610      rw [ofBits_testBit_eq hi' _ (fun q hq => by611            rw [es (3 + 3 * B + r + q) (by omega), e_selI B r s _ hq, hs]; rfl),612          ofBits_testBit_eq hv' _ (fun k hk => by613            rw [es (3 + 3 * B + 2 * r + k) (by omega), e_selV B r s _ hk, hs]; rfl)]614  have hfnz : (if sbits B r s (3 + 4 * B + 2 * r) then615      some (ofBits r (fun q => sbits B r s (4 + 4 * B + 2 * r + q)),616        ofBits B (fun k => sbits B r s (4 + 4 * B + 3 * r + k))) else none) = s.fnz := by617    rw [es (3 + 4 * B + 2 * r) (by omega), e_fnzF]618    cases hs : s.fnz with619    | none => rfl620    | some p =>621      obtain ⟨i, v⟩ := p622      obtain ⟨hi', hv'⟩ := h.fnz i v hs623      simp only [Option.isSome_some, if_true]624      rw [ofBits_testBit_eq hi' _ (fun q hq => by625            rw [es (4 + 4 * B + 2 * r + q) (by omega), e_fnzI B r s _ hq, hs]; rfl),626          ofBits_testBit_eq hv' _ (fun k hk => by627            rw [es (4 + 4 * B + 3 * r + k) (by omega), e_fnzV B r s _ hk, hs]; rfl)]628  simp only [decodeS]629  rw [hm, ha, hp, hv, hg, hi, hsel, hfnz]630631/-! ## Runs of the bit-level machine -/632633def brun (B r : Nat) : (Nat → Bool) → List Tok → (Nat → Bool) × List COut634  | v, [] => (v, [])635  | v, t :: ts => ((brun B r (bstep B r v t).1 ts).1, (bstep B r v t).2.toList ++ (brun B r (bstep B r v t).1 ts).2)636637theorem brun_append (B r : Nat) (v : Nat → Bool) (ts us : List Tok) :638    brun B r v (ts ++ us) =639      ((brun B r (brun B r v ts).1 us).1, (brun B r v ts).2 ++ (brun B r (brun B r v ts).1 us).2) := by640  induction ts generalizing v with641  | nil => simp [brun]642  | cons t ts ih => simp only [List.cons_append, brun, ih, List.append_assoc]643644/-- Every visited (state, token) pair satisfies the one-step width hypotheses. -/645def AllDec (B r : Nat) : CState → List Tok → Prop646  | _, [] => True647  | s, t :: ts => Decodable B r s t ∧ AllDec B r (cstep s t).1 ts648649/-- RUN REFINEMENT: started on the canonical encoding of s, the bit-level machine tracks650    the semantic controller exactly along the whole token stream. -/651theorem brun_refines {B r : Nat} : ∀ (s : CState) (ts : List Tok), AllDec B r s ts →652    brun B r (sbits B r s) ts = (sbits B r (crun s ts).1, (crun s ts).2)653  | s, [], _ => rfl654  | s, t :: ts, ⟨hd, hrest⟩ => by655    simp only [brun, crun]656    rw [step_refines hd, brun_refines _ ts hrest]657658theorem self_mem_crunStates (s : CState) (ts : List Tok) : s ∈ crunStates s ts := by659  cases ts <;> simp [crunStates]660661theorem allDec_of_fits {B r N : Nat} (hN : N < 2 ^ r) : ∀ (s : CState) (ts : List Tok),662    (∀ st ∈ crunStates s ts, Fits B N st) → (∀ t ∈ ts, tokX t < 2 ^ B) → AllDec B r s ts663  | _, [], _, _ => trivial664  | s, t :: ts, hf, ht => by665    have hs : Fits B N s := hf s (by simp [crunStates])666    obtain ⟨h1, h2, h3, _, h5, h6⟩ := hs667    refine ⟨⟨h1, h2, h3, fun i v hiv => ?_, fun i v hiv => ?_, ht t (by simp)⟩,668      allDec_of_fits hN _ ts (fun st hst => hf st (by simp [crunStates, hst]))669        (fun t' ht' => ht t' (by simp [ht']))⟩670    · obtain ⟨a, b⟩ := h5 i v hiv; exact ⟨by omega, b⟩671    · obtain ⟨a, b⟩ := h6 i v hiv; exact ⟨by omega, b⟩672673theorem tok_bound_stream {B : Nat} (Ps : List (List Nat)) (hP : ∀ P ∈ Ps, Width B P) :674    ∀ t ∈ stream Ps, tokX t < 2 ^ B := by675  intro t ht676  simp only [stream, List.mem_flatMap, dtoks, List.mem_append, List.mem_map, List.mem_singleton] at ht677  obtain ⟨P, hP', hm⟩ := ht678  rcases hm with ((⟨x, hx, rfl⟩ | rfl) | ⟨x, hx, rfl⟩) | rfl679  · exact hP P hP' x hx680  · exact Nat.two_pow_pos B681  · exact hP P hP' x hx682  · exact Nat.two_pow_pos B683684/-- STREAM THEOREM (bit level): on any well-formed stream of N-heap, B-bit boards with685    N < 2^r, the bit-level machine started in the all-zero vector (the encoding of the686    initial state) produces exactly the semantic outputs: for each board, the summary687    (with the difference to the previous summary) and the replay move. -/688theorem bits_stream {B r N : Nat} (hN : N < 2 ^ r) (Ps : List (List Nat))689    (hP : ∀ P ∈ Ps, P.length = N ∧ Width B P) :690    (brun B r (sbits B r cinit) (stream Ps)).2 = ctrlOuts false 0 Ps := by691  have hfit : Fits B N cinit := by692    refine ⟨Nat.two_pow_pos B, Nat.two_pow_pos B, Nat.two_pow_pos B, Nat.zero_le _, ?_, ?_⟩ <;>693      simp [cinit]694  have hall := allDec_of_fits (B := B) hN cinit (stream Ps) (stream_fits cinit cinit_idle hfit Ps hP)695    (tok_bound_stream Ps (fun P h => (hP P h).2))696  rw [brun_refines _ _ hall, (crun_stream cinit cinit_idle Ps).1]697  rfl698699/-! ## Reset from an arbitrary vector, and streams of games -/700701theorem inp_row (B r : Nat) (v : Nat → Bool) (t : Tok) : inp B r v t (4 + 5 * B + 3 * r) = tokRow t := by702  simp (disch := omega) only [inp, tbits, if_neg, if_pos, ↓reduceIte]703theorem inp_rst (B r : Nat) (v : Nat → Bool) (t : Tok) : inp B r v t (5 + 5 * B + 3 * r) = tokRst t := by704  simp (disch := omega) only [inp, tbits, if_neg, if_pos, ↓reduceIte]705706/-- RESET: from ANY state vector whatsoever (not necessarily a valid encoding), a reset707    token produces the all-zero encoding of the initial state and no output. -/708theorem bstep_reset (B r : Nat) (v : Nat → Bool) : bstep B r v Tok.reset = (sbits B r cinit, none) := by709  have h1 : (fun j => eval (inp B r v Tok.reset) (nextC B r j)) = sbits B r cinit := by710    funext j711    unfold nextC sbits712    rw [layout_map (eval (inp B r v Tok.reset))]713    apply layout_congr <;> intros <;>714      simp [modeN, accN, prevN, validN, sigN, idxN, selFN, selIN, selVN, fnzFN, fnzIN, fnzVN, Rc,715        inp_rst, tokRst, cinit, optI, optV]716  have h2 : decodeOut B r (inp B r v Tok.reset) = none := by717    simp [decodeOut, sumOutC, moveOutC, Ec, inp_row, inp_rst, tokRow, tokRst]718  show ((fun j => eval (inp B r v Tok.reset) (nextC B r j)), decodeOut B r (inp B r v Tok.reset)) = _719  rw [h1, h2]720721/-- GAMES THEOREM (bit level): from an ARBITRARY initial state vector, a stream of games,722    each preceded by a reset and each consisting of well-formed boards with some number723    N < 2^r of heaps, yields game by game exactly the outputs of a fresh controller. -/724theorem bits_games (B r : Nat) (v : Nat → Bool) (gs : List (List (List Nat)))725    (h : ∀ g ∈ gs, ∃ N, N < 2 ^ r ∧ ∀ P ∈ g, P.length = N ∧ Width B P) :726    (brun B r v (gameStream gs)).2 = gs.flatMap (ctrlOuts false 0) := by727  induction gs generalizing v with728  | nil => rfl729  | cons g gs ih =>730    have e : gameStream (g :: gs) = (Tok.reset :: stream g) ++ gameStream gs := by simp [gameStream]731    have h1 : brun B r v (Tok.reset :: stream g) = brun B r (sbits B r cinit) (stream g) := by732      simp only [brun, bstep_reset, Option.toList, List.nil_append]733    obtain ⟨N, hN, hg⟩ := h g (by simp)734    rw [e, brun_append, h1, List.flatMap_cons, bits_stream hN g hg,735      ih _ (fun g' hg' => h g' (by simp [hg']))]736737/-- LOSSLESS ON REACHABLE STATES: along a well-formed stream every reachable semantic738    state fits the fields (counter included: idx ≤ N < 2^r, so no overflow) and is739    recovered exactly from its 4 + 5B + 3r state bits. -/740theorem reachable_lossless {B r N : Nat} (hN : N < 2 ^ r) (Ps : List (List Nat))741    (hP : ∀ P ∈ Ps, P.length = N ∧ Width B P) :742    ∀ st ∈ crunStates cinit (stream Ps), FitsR B r st ∧ decodeS B r (sbits B r st) = st := by743  have hfit : Fits B N cinit := by744    refine ⟨Nat.two_pow_pos B, Nat.two_pow_pos B, Nat.two_pow_pos B, Nat.zero_le _, ?_, ?_⟩ <;>745      simp [cinit]746  intro st hst747  obtain ⟨h1, h2, h3, h4, h5, h6⟩ := stream_fits cinit cinit_idle hfit Ps hP st hst748  have hr : FitsR B r st := ⟨h1, h2, h3, by omega, fun i v hiv => ⟨by have := (h5 i v hiv).1; omega,749    (h5 i v hiv).2⟩, fun i v hiv => ⟨by have := (h6 i v hiv).1; omega, (h6 i v hiv).2⟩⟩750  exact ⟨hr, decodeS_sbits hr⟩751752/-- Logical update counts: one circuit evaluation per token; a decision on an N-heap board753    takes exactly 2N + 2 updates, a stream of D such boards D(2N + 2). -/754theorem dtoks_length (P : List Nat) : (dtoks P).length = 2 * P.length + 2 := by755  simp [dtoks]; omega756757theorem stream_length {N : Nat} (Ps : List (List Nat)) (hP : ∀ P ∈ Ps, P.length = N) :758    (stream Ps).length = Ps.length * (2 * N + 2) := by759  induction Ps with760  | nil => simp [stream]761  | cons P Ps ih =>762    have e : stream (P :: Ps) = dtoks P ++ stream Ps := by simp [stream]763    rw [e, List.length_append, dtoks_length, hP P (by simp), ih (fun Q hQ => hP Q (by simp [hQ])),764      List.length_cons, Nat.add_mul, Nat.one_mul]765    omega766767theorem brun_length (B r : Nat) (v : Nat → Bool) : ∀ ts : List Tok,768    (brun B r v ts).2.length ≤ ts.length := by769  intro ts770  induction ts generalizing v with771  | nil => simp [brun]772  | cons t ts ih =>773    simp only [brun, List.length_append, List.length_cons]774    have := ih (bstep B r v t).1775    cases (bstep B r v t).2 <;> simp [Option.toList] <;> omega776777/-- ONE BOARD (bit level): from the all-zero vector, the 2N + 2 updates for a board P778    with N < 2^r heaps of B bits output the summary and then `decisionMove P`, which by779    `Controller.decision_correct` is legal, reaches nim-sum 0 from every nonzero position,780    and is `none` exactly on terminal boards. -/781theorem bits_one_board {B r : Nat} (P : List Nat) (hN : P.length < 2 ^ r) (hw : Width B P) :782    (brun B r (sbits B r cinit) (dtoks P)).2 = [COut.summary (nimSum P) none, COut.move (decisionMove P)] := by783  have h := bits_stream (B := B) hN [P] (by simp [hw])784  simpa [stream, ctrlOuts, decisionMove] using h785786/-! ## Memory and resource bounds -/787788/-- Number of state wires. -/789def stateWidth (B r : Nat) : Nat := 4 + 5 * B + 3 * r790791theorem sbits_beyond (B r : Nat) (s : CState) (j : Nat) (hj : stateWidth B r ≤ j) : sbits B r s j = false := by792  unfold stateWidth at hj793  simp (disch := omega) only [sbits, layout, if_neg]794795theorem nextC_beyond (B r : Nat) (j : Nat) (hj : stateWidth B r ≤ j) : nextC B r j = const false := by796  unfold stateWidth at hj797  simp (disch := omega) only [nextC, layout, if_neg]798799/-- With r = log₂N + 1 the counter never overflows; memory is 7 + 5B + 3·log₂N bits. -/800theorem counter_width (N : Nat) : N < 2 ^ (N.log2 + 1) ∧ stateWidth B (N.log2 + 1) = 7 + 5 * B + 3 * N.log2 := by801  refine ⟨Nat.lt_log2_self, ?_⟩802  unfold stateWidth; omega803804theorem layout_forall {α : Type} (P : α → Prop) {B r : Nat} {d m : α} {acc prev : Nat → α}805    {valid : α} {sig idx : Nat → α} {selF : α} {selI selV : Nat → α} {fnzF : α} {fnzI fnzV : Nat → α}806    (hd : P d) (hm : P m) (hacc : ∀ k < B, P (acc k)) (hprev : ∀ k < B, P (prev k))807    (hvalid : P valid) (hsig : ∀ k < B, P (sig k)) (hidx : ∀ q < r, P (idx q))808    (hselF : P selF) (hselI : ∀ q < r, P (selI q)) (hselV : ∀ k < B, P (selV k))809    (hfnzF : P fnzF) (hfnzI : ∀ q < r, P (fnzI q)) (hfnzV : ∀ k < B, P (fnzV k)) (j : Nat) :810    P (layout B r d m acc prev valid sig idx selF selI selV fnzF fnzI fnzV j) := by811  simp only [layout]812  by_cases h1 : j = 0813  · simp only [if_pos h1]; exact hm814  by_cases h2 : j < 1 + B815  · simp only [if_neg h1, if_pos h2]; exact hacc _ (by omega)816  by_cases h3 : j < 1 + 2 * B817  · simp only [if_neg h1, if_neg h2, if_pos h3]; exact hprev _ (by omega)818  by_cases h4 : j = 1 + 2 * B819  · simp only [if_neg h1, if_neg h2, if_neg h3, if_pos h4]; exact hvalid820  by_cases h5 : j < 2 + 3 * B821  · simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_pos h5]; exact hsig _ (by omega)822  by_cases h6 : j < 2 + 3 * B + r823  · simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_pos h6]; exact hidx _ (by omega)824  by_cases h7 : j = 2 + 3 * B + r825  · simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_neg h6, if_pos h7]; exact hselF826  by_cases h8 : j < 3 + 3 * B + 2 * r827  · simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_neg h6, if_neg h7, if_pos h8]; exact hselI _ (by omega)828  by_cases h9 : j < 3 + 4 * B + 2 * r829  · simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_neg h6, if_neg h7, if_neg h8, if_pos h9]; exact hselV _ (by omega)830  by_cases h10 : j = 3 + 4 * B + 2 * r831  · simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_neg h6, if_neg h7, if_neg h8, if_neg h9, if_pos h10]; exact hfnzF832  by_cases h11 : j < 4 + 4 * B + 3 * r833  · simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_neg h6, if_neg h7, if_neg h8, if_neg h9, if_neg h10, if_pos h11]; exact hfnzI _ (by omega)834  by_cases h12 : j < 4 + 5 * B + 3 * r835  · simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_neg h6, if_neg h7, if_neg h8, if_neg h9, if_neg h10, if_neg h11, if_pos h12]; exact hfnzV _ (by omega)836  simp only [if_neg h1, if_neg h2, if_neg h3, if_neg h4, if_neg h5, if_neg h6, if_neg h7, if_neg h8, if_neg h9, if_neg h10, if_neg h11, if_neg h12]; exact hd837838section Resources839open AC0.Circ840841theorem size_and_le' {cs : List Circ} {S : Nat} (h : ∀ c ∈ cs, size c ≤ S) :842    size (and cs) ≤ cs.length * S + 1 := by843  simp only [size_and]; have := sum_le_len_mul h; omega844845theorem size_or_le' {cs : List Circ} {S : Nat} (h : ∀ c ∈ cs, size c ≤ S) :846    size (or cs) ≤ cs.length * S + 1 := by847  simp only [size_or]; have := sum_le_len_mul h; omega848849theorem maxInput_and_le {cs : List Circ} {M : Nat} (h : ∀ c ∈ cs, maxInput c ≤ M) :850    maxInput (and cs) ≤ M := by851  simp only [maxInput_and]; apply listMax_le; intro a ha852  obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha; exact h c hc853854theorem maxInput_or_le {cs : List Circ} {M : Nat} (h : ∀ c ∈ cs, maxInput c ≤ M) :855    maxInput (or cs) ≤ M := by856  simp only [maxInput_or]; apply listMax_le; intro a ha857  obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ha; exact h c hc858859def cancSize (B : Nat) : Nat := B * (2 * B + 3) + 1860861variable (B r : Nat)862863theorem size_cancC : size (cancC B r) ≤ cancSize B := by864  unfold cancC cancSize865  have := size_or_le' (S := 2 * B + 3) (cs := (List.range B).map (fun k => and ([input (2 + 2 * B + k), xI B r k] ++866    (List.range (B - 1 - k)).map (fun t => not (input (2 + 2 * B + (k + 1 + t))))))) (by867      intro c hc868      obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hc869      have hk' := List.mem_range.mp hk870      have h2 := size_and_le' (S := 2) (cs := [input (2 + 2 * B + k), xI B r k] ++871        (List.range (B - 1 - k)).map (fun t => not (input (2 + 2 * B + (k + 1 + t))))) (by872          intro c hc873          simp only [List.mem_append, List.mem_cons, List.mem_map, List.mem_range] at hc874          rcases hc with (rfl | rfl | h) | ⟨t, _, rfl⟩875          · simp876          · simp [xI]877          · simp at h878          · simp)879      simp only [List.length_append, List.length_cons, List.length_nil, List.length_map,880        List.length_range] at h2881      have : (B - 1 - k + 2) * 2 + 1 ≤ 2 * B + 3 := by omega882      omega)883  simpa using this884885theorem depth_cancC : depth (cancC B r) ≤ 3 := by886  unfold cancC887  apply depth_or_le; intro c hc888  obtain ⟨k, _, rfl⟩ := List.mem_map.mp hc889  apply depth_and_le; intro c hc890  simp only [List.mem_append, List.mem_cons, List.mem_map, List.mem_range] at hc891  rcases hc with (rfl | rfl | h) | ⟨t, _, rfl⟩892  · simp893  · simp [xI]894  · simp at h895  · simp896897theorem max_cancC : maxInput (cancC B r) ≤ 6 + 6 * B + 3 * r := by898  unfold cancC899  apply maxInput_or_le; intro c hc900  obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hc901  have hk' := List.mem_range.mp hk902  apply maxInput_and_le; intro c hc903  simp only [List.mem_append, List.mem_cons, List.mem_map, List.mem_range] at hc904  rcases hc with (rfl | rfl | h) | ⟨t, ht, rfl⟩905  · simp; omega906  · simp [xI]; omega907  · simp at h908  · simp; omega909910theorem size_nzC : size (nzC B r) ≤ B + 1 := by911  unfold nzC912  have := size_or_le' (S := 1) (cs := (List.range B).map (fun k => xI B r k)) (by913    intro c hc; obtain ⟨k, _, rfl⟩ := List.mem_map.mp hc; simp [xI])914  simpa using this915916theorem depth_nzC : depth (nzC B r) ≤ 1 := by917  unfold nzC; apply depth_or_le; intro c hc; obtain ⟨k, _, rfl⟩ := List.mem_map.mp hc; simp [xI]918919theorem max_nzC : maxInput (nzC B r) ≤ 6 + 6 * B + 3 * r := by920  unfold nzC; apply maxInput_or_le; intro c hc; obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hc921  have := List.mem_range.mp hk; simp [xI]; omega922923theorem size_decC (k : Nat) : size (decC B r k) ≤ 4 * k + 9 := by924  unfold decC xor2925  have := size_and_le' (S := 2) (cs := (List.range k).map (fun t => not (xI B r t))) (by926    intro c hc; obtain ⟨t, _, rfl⟩ := List.mem_map.mp hc; simp [xI])927  simp only [List.length_map, List.length_range] at this928  generalize and ((List.range k).map (fun t => not (xI B r t))) = A at this ⊢929  simp only [size_or, size_and, size_not, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, xI,930    size_input]931  omega932933theorem depth_decC (k : Nat) : depth (decC B r k) ≤ 5 := by934  unfold decC xor2935  have h : depth (and ((List.range k).map (fun t => not (xI B r t)))) ≤ 2 := by936    apply depth_and_le; intro c hc; obtain ⟨t, _, rfl⟩ := List.mem_map.mp hc; simp [xI]937  generalize and ((List.range k).map (fun t => not (xI B r t))) = A at h ⊢938  simp only [depth_or, depth_and, depth_not, List.map_cons, List.map_nil, listMax, List.foldr_cons,939    List.foldr_nil, xI, depth_input]940  omega941942theorem max_decC {k : Nat} (hk : k < B) : maxInput (decC B r k) ≤ 6 + 6 * B + 3 * r := by943  unfold decC xor2944  have h : maxInput (and ((List.range k).map (fun t => not (xI B r t)))) ≤ 6 + 6 * B + 3 * r := by945    apply maxInput_and_le; intro c hc; obtain ⟨t, ht, rfl⟩ := List.mem_map.mp hc946    have := List.mem_range.mp ht; simp [xI]; omega947  generalize and ((List.range k).map (fun t => not (xI B r t))) = A at h ⊢948  simp only [maxInput_or, maxInput_and, maxInput_not, List.map_cons, List.map_nil, listMax,949    List.foldr_cons, List.foldr_nil, xI, maxInput_input]950  omega951952theorem size_incC (q : Nat) : size (incC B q) ≤ 2 * q + 9 := by953  unfold incC xor2954  have := size_and_le' (S := 1) (cs := (List.range q).map (fun t => input (2 + 3 * B + t))) (by955    intro c hc; obtain ⟨t, _, rfl⟩ := List.mem_map.mp hc; simp)956  simp only [List.length_map, List.length_range] at this957  generalize and ((List.range q).map (fun t => input (2 + 3 * B + t))) = A at this ⊢958  simp only [size_or, size_and, size_not, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil,959    size_input]960  omega961962theorem depth_incC (q : Nat) : depth (incC B q) ≤ 5 := by963  unfold incC xor2964  have h : depth (and ((List.range q).map (fun t => input (2 + 3 * B + t)))) ≤ 1 := by965    apply depth_and_le; intro c hc; obtain ⟨t, _, rfl⟩ := List.mem_map.mp hc; simp966  generalize and ((List.range q).map (fun t => input (2 + 3 * B + t))) = A at h ⊢967  simp only [depth_or, depth_and, depth_not, List.map_cons, List.map_nil, listMax, List.foldr_cons,968    List.foldr_nil, depth_input]969  omega970971theorem max_incC {q : Nat} (hq : q < r) : maxInput (incC B q) ≤ 6 + 6 * B + 3 * r := by972  unfold incC xor2973  have h : maxInput (and ((List.range q).map (fun t => input (2 + 3 * B + t)))) ≤ 6 + 6 * B + 3 * r := by974    apply maxInput_and_le; intro c hc; obtain ⟨t, ht, rfl⟩ := List.mem_map.mp hc975    have := List.mem_range.mp ht; simp; omega976  generalize and ((List.range q).map (fun t => input (2 + 3 * B + t))) = A at h ⊢977  simp only [maxInput_or, maxInput_and, maxInput_not, List.map_cons, List.map_nil, listMax,978    List.foldr_cons, List.foldr_nil, maxInput_input]979  omega980981/-- Uniform size bound for every next-state formula. -/982def cellSize (B r : Nat) : Nat := cancSize B + 5 * B + 2 * r + 40983984/-- Every next-state formula has depth ≤ 8, size ≤ cellSize B r and reads only the985    6 + 6B + 3r input wires (state wires and token wires). -/986theorem nextC_resources (j : Nat) :987    size (nextC B r j) ≤ cellSize B r ∧ depth (nextC B r j) ≤ 8 ∧988      maxInput (nextC B r j) ≤ 6 + 6 * B + 3 * r := by989  have c1 := size_cancC B r990  have c2 := depth_cancC B r991  have c3 := max_cancC B r992  have n1 := size_nzC B r993  have n2 := depth_nzC B r994  have n3 := max_nzC B r995  unfold nextC996  refine layout_forall (fun c => size c ≤ cellSize B r ∧ depth c ≤ 8 ∧ maxInput c ≤ 6 + 6 * B + 3 * r)997    ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ j998  · simp [cellSize]999  · simp [modeN, Rc, Wc, Ec, Mc, listMax, cellSize] <;> omega1000  · intro k hk; simp [accN, Rc, Wc, Ec, Mc, xI, xor2, listMax, cellSize] <;> omega1001  · intro k hk; simp [prevN, mux, Rc, Wc, Ec, Mc, listMax, cellSize] <;> omega1002  · simp [validN, Rc, Wc, Ec, Mc, listMax, cellSize] <;> omega1003  · intro k hk; simp [sigN, mux, Rc, Wc, Ec, Mc, listMax, cellSize] <;> omega1004  · intro q hq1005    have i1 := size_incC B q; have i2 := depth_incC B q; have i3 := max_incC B r hq1006    simp [idxN, mux, Rc, Wc, Mc, listMax, cellSize] <;> omega1007  · simp [selFN, Rc, Wc, Mc, listMax, cellSize] <;> omega1008  · intro q hq; simp [selIN, Rc, Wc, Mc, listMax, cellSize] <;> omega1009  · intro k hk; simp [selVN, Rc, Wc, Mc, xI, xor2, listMax, cellSize] <;> omega1010  · simp [fnzFN, Rc, Wc, Mc, listMax, cellSize] <;> omega1011  · intro q hq; simp [fnzIN, Rc, Wc, Mc, listMax, cellSize] <;> omega1012  · intro k hk1013    have d1 := size_decC B r k; have d2 := depth_decC B r k; have d3 := max_decC B r hk1014    simp [fnzVN, Rc, Wc, Mc, listMax, cellSize] <;> omega10151016/-- The output wires: summary flag, B summary bits, B difference bits, difference-valid1017    flag, move flag, move-valid flag, r move-index bits, B move-value bits. -/1018def outC (B r : Nat) : List Circ :=1019  [sumOutC B r] ++ (List.range B).map sumBitC ++ (List.range B).map (diffBitC B) ++1020    [diffValidC B, moveOutC B r, moveValidC B r] ++ (List.range r).map (moveIC B r) ++1021    (List.range B).map (moveVC B r)10221023theorem outC_length : (outC B r).length = 4 + 3 * B + r := by1024  simp [outC]; omega10251026theorem outC_resources : ∀ c ∈ outC B r, size c ≤ 16 ∧ depth c ≤ 3 ∧ maxInput c ≤ 6 + 6 * B + 3 * r := by1027  intro c hc1028  simp only [outC, List.mem_append, List.mem_cons, List.mem_map, List.mem_range, List.not_mem_nil,1029    or_false] at hc1030  rcases hc with (((((rfl | ⟨k, hk, rfl⟩) | ⟨k, hk, rfl⟩) | (rfl | rfl | rfl)) | ⟨q, hq, rfl⟩) | ⟨k, hk, rfl⟩)1031  · simp [sumOutC, Ec, Mc, listMax] <;> omega1032  · simp [sumBitC] <;> omega1033  · simp [diffBitC, xor2, listMax] <;> omega1034  · simp [diffValidC] <;> omega1035  · simp [moveOutC, Ec, Mc, listMax] <;> omega1036  · simp [moveValidC, listMax] <;> omega1037  · simp [moveIC, mux, listMax] <;> omega1038  · simp [moveVC, mux, listMax] <;> omega10391040/-- PER-UPDATE CIRCUIT: 4 + 5B + 3r next-state formulas and 4 + 3B + r output formulas,1041    all of depth ≤ 8, over 6 + 6B + 3r input wires; total size at most1042    (4 + 5B + 3r)·cellSize + 16·(4 + 3B + r), where cellSize = B(2B+3) + 5B + 2r + 41. -/1043theorem per_update_size :1044    ((List.range (stateWidth B r)).map (fun j => size (nextC B r j))).sum +1045      ((outC B r).map size).sum ≤ stateWidth B r * cellSize B r + 16 * (4 + 3 * B + r) := by1046  have h1 := sum_le_len_mul (cs := (List.range (stateWidth B r)).map (nextC B r)) (S := cellSize B r) (by1047    intro c hc; obtain ⟨j, _, rfl⟩ := List.mem_map.mp hc; exact (nextC_resources B r j).1)1048  have h2 := sum_le_len_mul (cs := outC B r) (S := 16) (fun c hc => (outC_resources B r c hc).1)1049  simp only [List.map_map, List.length_map, List.length_range, outC_length] at h1 h21050  have e : (List.map (fun j => size (nextC B r j)) (List.range (stateWidth B r))) =1051      List.map (size ∘ nextC B r) (List.range (stateWidth B r)) := rfl1052  rw [e]1053  omega10541055/-- The summary mechanism (mode, acc, prev, valid) has constant size per bit, hence O(B)1056    in total; the quadratic term of cellSize comes only from the cancellation test. -/1057theorem summary_resources (k : Nat) :1058    size (modeN B r) ≤ 18 ∧ size (accN B r k) ≤ 35 ∧ size (prevN B r k) ≤ 25 ∧ size (validN B r) ≤ 13 := by1059  refine ⟨?_, ?_, ?_, ?_⟩ <;> simp [modeN, accN, prevN, validN, mux, Rc, Wc, Ec, Mc, xI, xor2]10601061end Resources106210631064/-! ## Axiom audit -/10651066#print axioms layout_map1067#print axioms layout_congr1068#print axioms e_mode1069#print axioms e_acc1070#print axioms e_prev1071#print axioms e_valid1072#print axioms e_sig1073#print axioms e_idx1074#print axioms e_selF1075#print axioms e_selI1076#print axioms e_selV1077#print axioms e_fnzF1078#print axioms e_fnzI1079#print axioms e_fnzV1080#print axioms e_row1081#print axioms e_rst1082#print axioms e_x1083#print axioms testBit_succ1084#print axioms top_bit1085#print axioms canc_iff1086#print axioms pos_iff_bitLE1087#print axioms ev_inc1088#print axioms ev_canc1089#print axioms ev_nz1090#print axioms ev_dec1091#print axioms f_mode1092#print axioms f_acc1093#print axioms f_prev1094#print axioms f_valid1095#print axioms f_sig1096#print axioms f_idx1097#print axioms f_selF1098#print axioms f_selI1099#print axioms f_selV1100#print axioms f_fnzF1101#print axioms f_fnzI1102#print axioms f_fnzV1103#print axioms step_state1104#print axioms step_out1105#print axioms step_refines1106#print axioms decodeS_sbits1107#print axioms brun_append1108#print axioms brun_refines1109#print axioms self_mem_crunStates1110#print axioms allDec_of_fits1111#print axioms tok_bound_stream1112#print axioms bits_stream1113#print axioms inp_row1114#print axioms inp_rst1115#print axioms bstep_reset1116#print axioms bits_games1117#print axioms reachable_lossless1118#print axioms dtoks_length1119#print axioms stream_length1120#print axioms brun_length1121#print axioms bits_one_board1122#print axioms sbits_beyond1123#print axioms nextC_beyond1124#print axioms counter_width1125#print axioms layout_forall1126#print axioms size_and_le'1127#print axioms size_or_le'1128#print axioms maxInput_and_le1129#print axioms maxInput_or_le1130#print axioms size_cancC1131#print axioms depth_cancC1132#print axioms max_cancC1133#print axioms size_nzC1134#print axioms depth_nzC1135#print axioms max_nzC1136#print axioms size_decC1137#print axioms depth_decC1138#print axioms max_decC1139#print axioms size_incC1140#print axioms depth_incC1141#print axioms max_incC1142#print axioms nextC_resources1143#print axioms outC_length1144#print axioms outC_resources1145#print axioms per_update_size1146#print axioms summary_resources1147end ControllerBits1148end NimAudit