Proposition 5.13A constant-depth recurrent update computes the nim-sum after N row updates and reports consecutive differences

95/-- FOLD INVARIANT.  From any state with empty accumulator, for ANY finite sequence96    of positions (empty positions allowed): the t-th output is97    (sigma(P_t), Delta) where Delta = prev XOR sigma(P_1) if the starting state is98    valid (none otherwise) for t = 1 and sigma(P_{t-1}) XOR sigma(P_t) for t ≥ 2;99    the final state retains the last summary with valid = true and acc = 0. -/100theorem fold_invariant (s : State) (hs : s.acc = 0) (Ps : List (List Nat)) :101    run s (serialize Ps) = (expectedState s Ps, expectedOuts s.valid s.prev Ps) := by102  induction Ps generalizing s with103  | nil => simp [serialize, run, expectedState, expectedOuts]104  | cons P Ps ih =>105    have e : serialize (P :: Ps) = (P.map Token.row ++ [Token.sep]) ++ serialize Ps := by106      simp [serialize]107    rw [e, run_append, run_position, hs, Nat.zero_xor]108    rw [ih ⟨0, nimSum P, true⟩ rfl]109    simp [expectedState, expectedOuts]

173theorem stream_reports_delta (Q Q' : List Nat) (Ps : List (List Nat)) :174    expectedOuts false 0 (Q :: Q' :: Ps) =175      ⟨nimSum Q, none⟩ :: ⟨nimSum Q', some (nimSum Q ^^^ nimSum Q')⟩ ::176        expectedOuts true (nimSum Q') Ps := by177  simp [expectedOuts]

422/-- PER-UPDATE CIRCUIT CORRECTNESS (k < B): the circuits compute the new state bits423    and, at a separator, the output bits. -/424theorem circuit_update {B k : Nat} (hk : k < B) (s : State) (t : Token) :425    eval (encode B s t) (accC B k) = (step s t).1.acc.testBit k ∧426    eval (encode B s t) (prevC B k) = (step s t).1.prev.testBit k ∧427    eval (encode B s t) (validC B) = (step s t).1.valid ∧428    (t = Token.sep → eval (encode B s t) (input k) = s.acc.testBit k ∧429      eval (encode B s t) (diffC B k) = (s.prev ^^^ s.acc).testBit k ∧430      eval (encode B s t) (diffValidC B) = s.valid) := by431  cases t with432  | row x =>433    simp only [accC, prevC, validC, eval_and, eval_or, eval_not, eval_input, eval_xorC,434      List.all_cons, List.all_nil, List.any_cons, List.any_nil, enc_acc hk, enc_prev hk,435      enc_valid, enc_tag, enc_x hk, step, Nat.testBit_xor]436    refine ⟨by simp, by simp, by simp, fun h => by cases h⟩437  | sep =>438    simp only [accC, prevC, validC, diffC, diffValidC, eval_and, eval_or, eval_not, eval_input,439      eval_xorC, List.all_cons, List.all_nil, List.any_cons, List.any_nil, enc_acc hk,440      enc_prev hk, enc_valid, enc_tag, step, Nat.testBit_xor, Nat.zero_testBit]441    refine ⟨by simp, by simp, by simp, fun _ => ⟨by simp, by simp, by simp⟩⟩

458/-- STATE-BIT THEOREM: 2B+1 bits suffice, and the per-update circuit maps the bit459    encoding of a B-bit state to the bit encoding of its successor. -/460theorem circuit_step_correct {B : Nat} {s : State} {t : Token} (hs : StateWidth B s)461    (ht : TokenWidth B t) :462    stateOfBits B (fun j =>463        if j < B then eval (encode B s t) (accC B j)464        else if j < 2 * B then eval (encode B s t) (prevC B (j - B))465        else eval (encode B s t) (validC B)) = (step s t).1 := by466  have hw := step_width hs ht467  unfold stateOfBits468  have h1 : ofBits B (fun k => if k < B then eval (encode B s t) (accC B k)469      else if k < 2 * B then eval (encode B s t) (prevC B (k - B))470      else eval (encode B s t) (validC B)) = (step s t).1.acc := by471    apply ofBits_testBit_eq hw.1472    intro k hk473    simp only [hk, if_true]474    exact (circuit_update hk s t).1475  have h2 : ofBits B (fun k => if B + k < B then eval (encode B s t) (accC B (B + k))476      else if B + k < 2 * B then eval (encode B s t) (prevC B (B + k - B))477      else eval (encode B s t) (validC B)) = (step s t).1.prev := by478    apply ofBits_testBit_eq hw.2479    intro k hk480    simp only [show ¬ B + k < B by omega, show B + k < 2 * B by omega, if_true, if_false,481      show B + k - B = k by omega]482    exact (circuit_update hk s t).2.1483  have h3 : (if 2 * B < B then eval (encode B s t) (accC B (2 * B))484      else if 2 * B < 2 * B then eval (encode B s t) (prevC B (2 * B - B))485      else eval (encode B s t) (validC B)) = (step s t).1.valid := by486    simp only [show ¬ 2 * B < B by omega, Nat.lt_irrefl, if_false]487    cases t <;> simp [validC, enc_valid, enc_tag, step]488  simp only []489  rw [h1, h2, h3]

491/-- Per-update circuit resources: depth ≤ 4, total size ≤ 28 B + 8 for all492    state and output bits (constant depth, O(B) size). -/493theorem circuit_resources (B k : Nat) :494    depth (accC B k) ≤ 4 ∧ depth (prevC B k) ≤ 4 ∧ depth (validC B) ≤ 4 ∧495    depth (diffC B k) ≤ 4 ∧ depth (diffValidC B) ≤ 4 ∧496    size (accC B k) + size (prevC B k) + size (diffC B k) ≤ 28 ∧497    size (validC B) + size (diffValidC B) ≤ 8 := by498  simp [accC, prevC, validC, diffC, diffValidC, xorC, listMax]

511theorem xorNet_correct (a b : Bool) :512    evalNet xorNet (fun j => if j = 0 then a else if j = 1 then b else false) 0 = xor a b := by513  cases a <;> cases b <;> decide