feat(circuit): construct uniform logarithmic-depth binary addition

Complexity.lean

@@ -125,9 +125,12 @@ public import Complexity.Computability.Circuit.Boolean.BinaryCost
 public import Complexity.Computability.Circuit.Boolean.BitBlast
 public import Complexity.Computability.Circuit.Boolean.BoundedError
 public import Complexity.Computability.Circuit.Boolean.Broadcast
+public import Complexity.Computability.Circuit.Boolean.CarryLookahead
+public import Complexity.Computability.Circuit.Boolean.CarryLookahead.PolyTime
 public import Complexity.Computability.Circuit.Boolean.CarrySave
 public import Complexity.Computability.Circuit.Boolean.CodeComposition
 public import Complexity.Computability.Circuit.Boolean.CodeSubstitution
+public import Complexity.Computability.Circuit.Boolean.CodeTemplate
 public import Complexity.Computability.Circuit.Boolean.CompareSwap
 public import Complexity.Computability.Circuit.Boolean.Comparison
 public import Complexity.Computability.Circuit.Boolean.Conondeterministic
@@ -141,6 +144,7 @@ public import Complexity.Computability.Circuit.Boolean.DuplicateFlags
 public import Complexity.Computability.Circuit.Boolean.ElementDistinctness
 public import Complexity.Computability.Circuit.Boolean.Encoding
 public import Complexity.Computability.Circuit.Boolean.Encoding.Certificate
+public import Complexity.Computability.Circuit.Boolean.EncodingSize
 public import Complexity.Computability.Circuit.Boolean.Equality
 public import Complexity.Computability.Circuit.Boolean.EvaluationTime
 public import Complexity.Computability.Circuit.Boolean.FanInTwo

Complexity/Computability/Circuit/Boolean/CodeTemplate.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Circuit.Boolean.CodeComposition
+public import Complexity.Computability.Circuit.Boolean.Formula
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Pi
+
+/-!
+# Uniform instantiation of fixed Boolean formula templates
+
+The formula is fixed, while the target input count and its selected binary input references may
+vary. The certificate constructs the actual code of the renamed formula. It does not use a
+finite encoding of circuits at a fixed width. Variable-size families of instances can use
+`appendCodes` after providing their uniform scalar generator.
+
+## Main definitions
+
+* `Cslib.Circuits.Boolean.formulaCode`: the actual code of a fixed formula at selected wires.
+
+## Main results
+
+* `Cslib.Circuits.Boolean.formulaCode_eq_code`: exact agreement with typed instantiation.
+* `Cslib.Circuits.Boolean.computableTidilyInPolyTime_formulaCode`: instantiate a fixed formula
+  at efficiently computed input wires.
+-/
+
+@[expose] public section
+
+namespace Cslib.Circuits.Boolean
+
+open Turing.MultiTapeTM ComputableTidilyInPolyTime
+
+/-- Instantiate a formula at raw wire numbers. This algorithm is total even when a selected
+wire is outside the declared input count; its typed correctness theorem requires valid wires. -/
+def formulaCode {m : ℕ} (n : ℕ) (F : Formula signature m) (wires : Fin m → ℕ) :
+    List (Op × List ℕ) × List ℕ :=
+  match F with
+  | .input i => ([], [wires i])
+  | .gate op args => compCode n (Circuit.oneGate (σ := signature) op id).code
+      (appendCodes n (List.ofFn fun i => formulaCode n (args i) wires))
+
+/-- Instantiating valid input wires constructs exactly the renamed formula's circuit code. -/
+theorem formulaCode_eq_code {n m : ℕ} (F : Formula signature m) (wires : Fin m → Fin n) :
+    formulaCode n F (fun i => (wires i).val) = (F.rename wires).toCircuit.code := by
+  induction F with
+  | input i => rfl
+  | gate op args ih =>
+    simp only [formulaCode, ih, appendCodes_code, compCode_code,
+      Formula.rename, Formula.gate_bind, Formula.toCircuit]
+
+/-- A fixed formula's full instantiated code is polynomial-time in the target input count and
+its selected binary wire numbers. This is uniform in every target width and reference. -/
+theorem computableTidilyInPolyTime_formulaCode {α : Type} {enc : α ↪ List Bool}
+    {n : α → ℕ} {m : ℕ} (F : Formula signature m) {wires : α → Fin m → ℕ}
+    (hn : ComputableTidilyInPolyTime n enc encNat)
+    (hwires : ∀ i, ComputableTidilyInPolyTime (fun a => wires a i) enc encNat) :
+    ComputableTidilyInPolyTime (fun a => formulaCode (n a) F (wires a)) enc encCode := by
+  induction F with
+  | input i => exact (const []).prod ((hwires i).cons' (const []))
+  | gate op args ih =>
+    exact computableTidilyInPolyTime_compCode hn
+      (const (Circuit.oneGate (σ := signature) op id).code)
+      (computableTidilyInPolyTime_appendCodes hn (ofFn (fun i => ih i)))
+
+end Cslib.Circuits.Boolean

Complexity/Computability/Circuit/Boolean/EncodingSize.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Circuit.Boolean.Encoding
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LinearSpaceArith
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
+
+/-!
+# Bounding the complete binary encoding of a circuit
+
+A circuit's typed wires bound every binary reference by its input and gate counts. This gives a
+polynomial bound on its complete serialized code, including gate tags, outputs and framing.
+It is useful for certifying circuit-construction loops whose intermediate circuits have bounded
+size, without making a claim about the complexity of the functions those circuits compute.
+
+## Main results
+
+* `Cslib.Circuits.Boolean.length_encCode_le`: a bound in the input, output and gate counts.
+-/
+
+@[expose] public section
+
+namespace Cslib.Circuits.Boolean
+
+open Turing.MultiTapeTM
+
+/-- The full code of a typed De Morgan circuit has polynomially bounded encoded length. -/
+theorem length_encCode_le {n m : ℕ} (c : Circuit signature n m) :
+    (encCode c.code).length ≤
+      2 * c.size * (23 + 8 * (n + c.size)) + 1 + m * (2 * (n + c.size) + 1) := by
+  have hgate (line : Line signature n c.size) :
+      (encGate line.code).length ≤ 11 + 4 * (n + c.size) := by
+    have hop : (encOp line.op).length ≤ 4 := by
+      cases line.op with
+      | const b => cases b <;> decide
+      | _ => decide
+    have hargs : (encList encNat line.code.2).length ≤ 2 * (2 * (n + c.size) + 1) := by
+      have h := length_encList_le encNat line.code.2 (b := n + c.size) (fun i hi => by
+        obtain ⟨j, rfl⟩ := List.mem_ofFn.mp hi
+        exact (length_encNat_le_self _).trans (Wire.toNat_lt (line.wires j)).le)
+      have ha : line.code.2.length ≤ 2 := by
+        rw [Line.length_code_snd]
+        cases line.op <;> simp
+      exact h.trans (Nat.mul_le_mul_right _ ha)
+    simp only [encGate, length_encPair, Line.code_fst]
+    omega
+  have hgates : (encList encGate c.code.1).length ≤ c.size * (23 + 8 * (n + c.size)) := by
+    have h := length_encList_le encGate c.code.1 (b := 11 + 4 * (n + c.size)) (fun g hg => by
+      rw [Circuit.code, Program.code_eq_ofFn_lines] at hg
+      obtain ⟨j, rfl⟩ := List.mem_ofFn.mp hg
+      exact hgate (c.program.lines j))
+    rw [show c.code.1.length = c.size from Program.length_code c.program] at h
+    nlinarith
+  have houtputs : (encList encNat c.code.2).length ≤ m * (2 * (n + c.size) + 1) := by
+    have h := length_encList_le encNat c.code.2 (b := n + c.size) (fun i hi => by
+      obtain ⟨j, rfl⟩ := List.mem_ofFn.mp hi
+      exact (length_encNat_le_self _).trans (Wire.toNat_lt (c.outputs j)).le)
+    simpa [Circuit.code] using h
+  simp only [encCode, length_encPair]
+  nlinarith
+
+end Cslib.Circuits.Boolean

Complexity/Computability/Circuit/Boolean/Word.lean

@@ -10,6 +10,7 @@ module
 public import Complexity.Init
 public import Complexity.Computability.Circuit.Boolean.Synthesis
 public import Complexity.Computability.Circuit.Iteration
+public import Complexity.Foundations.Data.BitString.Basic
 public import Init.Data.BitVec.Bitblast
 public import Mathlib.Data.List.OfFn
 
@@ -74,6 +75,35 @@ theorem getLsbD_word (bits : BitString w) (i : Fin w) :
 theorem word_getLsbD (a : BitVec w) : word (fun i : Fin w => a.getLsbD i.val) = a :=
   BitVec.eq_of_getLsbD_eq fun i hi => getLsbD_word _ ⟨i, hi⟩
 
+/-- The word representation and the bit-string numbering use the same unsigned value. -/
+theorem toNat_word_eq_equivFin {w : ℕ} (x : BitString w) :
+    (word x).toNat = (BitString.equivFin w x : ℕ) := by
+  induction w with
+  | zero =>
+    have h := (BitString.equivFin 0 x).isLt
+    simp only [pow_zero, Nat.lt_one_iff] at h
+    have hx := (word x).isLt
+    simp only [pow_zero, Nat.lt_one_iff] at hx
+    exact hx.trans h.symm
+  | succ w ih =>
+    have heq : x = Fin.cons (x 0) (fun i => x i.succ) := by
+      funext i
+      induction i using Fin.cases <;> rfl
+    rw [heq, BitString.val_equivFin_cons]
+    have hw : word (Fin.cons (x 0) (fun i => x i.succ)) =
+        (word (fun i => x i.succ)).concat (x 0) := by
+      apply BitVec.eq_of_getLsbD_eq
+      intro i hi
+      rw [getLsbD_word _ ⟨i, hi⟩, BitVec.getLsbD_concat]
+      cases i with
+      | zero => simp
+      | succ i =>
+        simp only [Nat.add_eq_zero_iff, Nat.one_ne_zero, and_false, ite_false,
+          Nat.add_sub_cancel]
+        exact (getLsbD_word (fun i => x i.succ) ⟨i, by omega⟩).symm
+    rw [hw, BitVec.toNat_concat, ih]
+    omega
+
 /-- The coordinate functions of a word-valued function. -/
 def wordWires (a : BitString n → BitVec w) : Set (BooleanFunction n) :=
   Set.range fun i : Fin w => fun x => (a x).getLsbD i.val

ComplexityTests.lean

@@ -63,6 +63,7 @@ import ComplexityTests.BooleanHierarchyPH
 import ComplexityTests.Broadcast
 import ComplexityTests.CNF
 import ComplexityTests.CNFPolyTime
+import ComplexityTests.CarryLookahead
 import ComplexityTests.CircuitCertificate
 import ComplexityTests.CircuitEvaluation
 import ComplexityTests.CircuitHamming.Approximation

ComplexityTests/CarryLookahead.lean

@@ -0,0 +1,149 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.Circuit.Boolean.CarryLookahead.PolyTime
+
+/-!
+# Carry-lookahead arithmetic and uniform generation clients
+
+The examples distinguish significance order, preserve carry-in at width zero, exercise a
+non-power-of-two propagation chain, and finish an existing carry-save reduction. Runtime clients
+generate complete binary circuit codes at growing widths and at arbitrary binary scan distances.
+-/
+
+namespace ComplexityTests.CarryLookahead
+
+open Cslib Cslib.Circuits Cslib.Circuits.Boolean
+open Turing.MultiTapeTM ComputableTidilyInPolyTime
+
+-- At width zero the carry is the sole output, whereas the modular output is empty.
+example (c : Bool) :
+    (carryLookahead 0).eval interpretation (fun _ => c) = fun _ => c := by
+  funext i
+  fin_cases i
+  cases c <;> rfl
+
+example : (carryLookaheadAdd 0).eval interpretation Fin.elim0 = Fin.elim0 := by
+  funext i
+  exact i.elim0
+
+-- Low generate/high kill and low kill/high generate must not be interchanged.
+example : (carryLookahead 2).eval interpretation
+    (Fin.append (Fin.append ![true, false] ![true, false]) (fun _ => false)) =
+      ![false, true, false] := by
+  apply (BitString.equivFin 3).injective
+  apply Fin.ext
+  rw [val_eval_carryLookahead]
+  decide
+
+example : (carryLookahead 2).eval interpretation
+    (Fin.append (Fin.append ![false, true] ![false, true]) (fun _ => false)) =
+      ![false, false, true] := by
+  apply (BitString.equivFin 3).injective
+  apply Fin.ext
+  rw [val_eval_carryLookahead]
+  decide
+
+-- Five is not a power of two: carry-in crosses all five positions and becomes the output carry.
+example : (carryLookahead 5).eval interpretation
+    (Fin.append (Fin.append (fun _ => true) (fun _ => false)) (fun _ => true)) =
+      ![false, false, false, false, false, true] := by
+  apply (BitString.equivFin 6).injective
+  apply Fin.ext
+  rw [val_eval_carryLookahead]
+  decide
+
+-- The same overflow is discarded by the modular interface.
+example : (BitString.equivFin 5 ((carryLookaheadAdd 5).eval interpretation
+    (Fin.append (fun _ => true) ![true, false, false, false, false])) : ℕ) = 0 := by
+  rw [val_eval_carryLookaheadAdd]
+  decide
+
+-- An inactive round retains every summary even at a large binary-encoded distance.
+example : (Cslib.Circuits.Boolean.CarryLookahead.step 3 (2 ^ 100)).eval interpretation
+    ![true, false, true, false, true, false] = ![true, false, true, false, true, false] := by
+  funext i
+  fin_cases i <;>
+    simp only [Cslib.Circuits.Boolean.CarryLookahead.step,
+      Circuit.eval_append, Circuit.eval_pi, Formula.eval_toCircuit,
+      Formula.eval_or, Formula.eval_and, Formula.eval_input,
+      Cslib.Circuits.Boolean.CarryLookahead.generateFormula,
+      Cslib.Circuits.Boolean.CarryLookahead.propagateFormula,
+      Cslib.Circuits.Boolean.CarryLookahead.neighbour,
+      Formula.eval_or, Formula.eval_and, Formula.eval_input] <;> decide
+
+-- The replacement finishes an existing 4-to-2 carry-save circuit, with every input arbitrary.
+example (w : ℕ) (p q : BitString (w + w)) :
+    pairVal (((carryLookaheadFinish w).comp (csa4to2 w)).eval interpretation
+      (Fin.append p q)) % 2 ^ w = (pairVal p + pairVal q) % 2 ^ w ∧
+    BitString.sndBits (((carryLookaheadFinish w).comp (csa4to2 w)).eval interpretation
+      (Fin.append p q)) = (fun _ => false) := by
+  exact ⟨pairVal_eval_carryLookaheadFinish_csa4to2_mod p q,
+    by rw [Circuit.eval_comp]; exact sndBits_eval_carryLookaheadFinish _⟩
+
+example (w : ℕ) : (carryLookaheadAdd w).depth ≤ 8 * (Nat.clog 2 (w + 1) + 1) ∧
+    (carryLookaheadAdd w).size ≤ 21 * (w + 1) ^ 2 :=
+  ⟨depth_carryLookaheadAdd_le_log w, size_carryLookaheadAdd_le w⟩
+
+-- The actual generated code is accepted by the ordinary checked circuit decoder.
+example (w : ℕ) : Circuit.ofCode (σ := signature) (w + w + 1) (w + 1) (carryLookahead w).code =
+    some (carryLookahead w) := Circuit.ofCode_code _
+
+/-- A single native algorithm generates full adder codes at an unbounded computed width. -/
+theorem growingWidth_polynomialTime :
+    ComputableTidilyInPolyTime (fun k : ℕ => (carryLookahead (2 * k + 1)).code)
+      encUnary encCode :=
+  computableTidilyInPolyTime_carryLookahead.comp (by fun_prop)
+
+/-- The modular and carry-save finishing generators are also uniform in the unary width. -/
+theorem modularAndFinish_polynomialTime :
+    ComputableTidilyInPolyTime (fun w => ((carryLookaheadAdd w).code,
+      (carryLookaheadFinish w).code)) encUnary (encPair encCode encCode) :=
+  computableTidilyInPolyTime_carryLookaheadAdd.prod
+    computableTidilyInPolyTime_carryLookaheadFinish
+
+/-- Distances are binary and need not be polynomially bounded as natural numbers. -/
+theorem arbitraryDistance_polynomialTime :
+    ComputableTidilyInPolyTime
+      (fun p : ℕ × ℕ => Cslib.Circuits.Boolean.CarryLookahead.stepCode p.1 p.2)
+      (encPair encUnary encNat) encCode :=
+  Cslib.Circuits.Boolean.CarryLookahead.computableTidilyInPolyTime_stepCode
+    (fst _ _) (snd _ _)
+
+/-- info: 'Cslib.Circuits.Boolean.val_eval_carryLookahead' depends on axioms:
+[propext, Classical.choice, Quot.sound] -/
+#guard_msgs in
+#print axioms Cslib.Circuits.Boolean.val_eval_carryLookahead
+/-- info: 'Cslib.Circuits.Boolean.depth_carryLookahead_le_log' depends on axioms:
+[propext, Classical.choice, Quot.sound] -/
+#guard_msgs in
+#print axioms Cslib.Circuits.Boolean.depth_carryLookahead_le_log
+/-- info: 'Cslib.Circuits.Boolean.size_carryLookahead_le' depends on axioms:
+[propext, Classical.choice, Quot.sound] -/
+#guard_msgs in
+#print axioms Cslib.Circuits.Boolean.size_carryLookahead_le
+/-- info: 'Cslib.Circuits.Boolean.pairVal_eval_carryLookaheadFinish_csa4to2_mod' depends on axioms: [propext,
+ Classical.choice,
+ Quot.sound] -/
+#guard_msgs in
+#print axioms Cslib.Circuits.Boolean.pairVal_eval_carryLookaheadFinish_csa4to2_mod
+/-- info: 'Cslib.Circuits.Boolean.computableTidilyInPolyTime_carryLookahead' depends on axioms: [propext,
+ Classical.choice,
+ Quot.sound] -/
+#guard_msgs in
+#print axioms Cslib.Circuits.Boolean.computableTidilyInPolyTime_carryLookahead
+/-- info: 'Cslib.Circuits.Boolean.computableTidilyInPolyTime_carryLookaheadAdd' depends on axioms: [propext,
+ Classical.choice,
+ Quot.sound] -/
+#guard_msgs in
+#print axioms Cslib.Circuits.Boolean.computableTidilyInPolyTime_carryLookaheadAdd
+/-- info: 'Cslib.Circuits.Boolean.computableTidilyInPolyTime_carryLookaheadFinish' depends on axioms: [propext,
+ Classical.choice,
+ Quot.sound] -/
+#guard_msgs in
+#print axioms Cslib.Circuits.Boolean.computableTidilyInPolyTime_carryLookaheadFinish
+
+end ComplexityTests.CarryLookahead

ROADMAP.md

@@ -843,6 +843,15 @@ batches.
      now certifies construction of circuit codes from encoded instances, with separately
      prescribed unary input/output widths. Its proof reuses the uniform tableau writer,
      prefix hardwiring and shared-input circuit composition; it establishes no depth bound.
+     The [carry-lookahead adder](Complexity/Computability/Circuit/Boolean/CarryLookahead.lean)
+     computes exact unsigned addition with carry-in and carry-out at every width, including zero.
+     Its depth is at most `7 + 2*ceil(log₂(w+1))`, with polynomial size and every gate charged.
+     The modular version has depth at most `8 + 2*ceil(log₂(w+1))`; a carry-save finishing client
+     preserves the existing 4-to-2 reducer's value modulo `2^w` and clears its second word.
+     The [native generators](Complexity/Computability/Circuit/Boolean/CarryLookahead/PolyTime.lean)
+     construct the complete binary gate/output codes from unary width, reusing fixed formula
+     templates and shared-input code assembly. This establishes polynomial-time uniformity for
+     these arithmetic circuits; stronger uniformity and shallow cryptographic decryption remain open.
      Define logspace and DLOGTIME uniformity with explicit gate-address, direct-connection and
      input encodings. Certify circuit generation and evaluation and the relevant machine-to-
      circuit simulations, preserving size, depth and construction-resource bounds. Prove

references.bib

@@ -6,6 +6,18 @@ @misc{LeanCanny2026
   note = {Source revision 2a50a2ee00ae0699cc3f0c2bff5100c4687d2d8e}
 }
 
+@article{LadnerFischer1980,
+  author = {Ladner, Richard E. and Fischer, Michael J.},
+  title = {Parallel Prefix Computation},
+  journal = {Journal of the ACM},
+  volume = {27},
+  number = {4},
+  pages = {831--838},
+  year = {1980},
+  doi = {10.1145/322217.322232},
+  url = {https://doi.org/10.1145/322217.322232}
+}
+
 @article{MorenoRivera2016,
   author = {Moreno, Rutilo and Rivera, Luis Manuel},
   title = {Blocks in Cycles and {$k$}-Commuting Permutations},