feat(crypto): construct native shallow GSW decryption circuits

Complexity.lean

@@ -130,6 +130,8 @@ 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.CarrySave.PolyTime
+public import Complexity.Computability.Circuit.Boolean.CarrySave.Reduce
+public import Complexity.Computability.Circuit.Boolean.CarrySave.Reduce.PolyTime
 public import Complexity.Computability.Circuit.Boolean.CodeComposition
 public import Complexity.Computability.Circuit.Boolean.CodeSubstitution
 public import Complexity.Computability.Circuit.Boolean.CodeTemplate
@@ -255,6 +257,14 @@ public import Complexity.Computability.Circuit.Boolean.Metric
 public import Complexity.Computability.Circuit.Boolean.Minterms
 public import Complexity.Computability.Circuit.Boolean.ModGates
 public import Complexity.Computability.Circuit.Boolean.ModMajority
+public import Complexity.Computability.Circuit.Boolean.Modular.InnerProduct
+public import Complexity.Computability.Circuit.Boolean.Modular.InnerProduct.PolyTime
+public import Complexity.Computability.Circuit.Boolean.Modular.Multiply
+public import Complexity.Computability.Circuit.Boolean.Modular.Multiply.PolyTime
+public import Complexity.Computability.Circuit.Boolean.Modular.PartialProduct
+public import Complexity.Computability.Circuit.Boolean.Modular.PartialProduct.PolyTime
+public import Complexity.Computability.Circuit.Boolean.Modular.Subtract
+public import Complexity.Computability.Circuit.Boolean.Modular.Subtract.PolyTime
 public import Complexity.Computability.Circuit.Boolean.Multiplicity
 public import Complexity.Computability.Circuit.Boolean.NaturalProof
 public import Complexity.Computability.Circuit.Boolean.NaturalProof.Generator
@@ -1330,6 +1340,9 @@ public import Complexity.Crypto.Computational.Homomorphic.FixedKey.Security
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Basic
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Decoding
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Decryption
+public import Complexity.Crypto.Computational.Homomorphic.GSW.DecryptionCircuit
+public import Complexity.Crypto.Computational.Homomorphic.GSW.DecryptionCircuit.Parameters
+public import Complexity.Crypto.Computational.Homomorphic.GSW.DecryptionCircuit.PolyTime
 public import Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters
 public import Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters.Security
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Gadget

Complexity/Computability/Circuit/Boolean/CarrySave/Reduce.lean

@@ -0,0 +1,150 @@
+/-
+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.CarryLookahead
+
+/-!
+# Balanced sums of carry-save pairs
+
+The existing half-split circuit tree reduces any list of carry-save pairs. Its value is their
+sum modulo `2 ^ w`, including the empty list. One carry-lookahead addition finishes the result.
+These are the arithmetic reductions used by modular multiplication and GSW's selected-row product.
+
+## Main definitions
+
+* `Cslib.Circuits.Boolean.reducePairs`: balanced four-to-two reduction on shared inputs.
+* `Cslib.Circuits.Boolean.sumPairs`: reduction followed by logarithmic-depth addition.
+
+## Main results
+
+* `Cslib.Circuits.Boolean.pairVal_eval_reducePairs_mod`: the sum of the supplied pair values.
+* `Cslib.Circuits.Boolean.val_eval_sumPairs`: the resulting modular word.
+* `Cslib.Circuits.Boolean.depth_reducePairs_le`: depth is logarithmic in the number of pairs.
+
+## References
+
+The underlying carry-save construction and source credit are in `Boolean.CarrySave`;
+parallel-prefix finishing follows [Ladner and Fischer][LadnerFischer1980].
+-/
+
+public section
+
+namespace Cslib.Circuits.Boolean
+
+open BitString
+
+variable {n w : ℕ}
+
+/-- Put an ordinary word into carry-save form, with a shared false gate for the second word. -/
+def pairWithZero (C : Circuit signature n w) : Circuit signature n (w + w) :=
+  C.append ((Circuit.wiring signature (fun _ : Fin w => (0 : Fin 1))).comp
+    (Circuit.oneGate (.const false) Fin.elim0))
+
+@[simp] theorem eval_pairWithZero (C : Circuit signature n w) (x : BitString n) :
+    (pairWithZero C).eval interpretation x =
+      Fin.append (C.eval interpretation x) (fun _ => false) := by
+  simp only [pairWithZero, Circuit.eval_append, Circuit.eval_comp, Circuit.eval_wiring]
+  rfl
+
+theorem pairVal_eval_pairWithZero (C : Circuit signature n w) (x : BitString n) :
+    pairVal ((pairWithZero C).eval interpretation x) =
+      (BitString.equivFin w (C.eval interpretation x) : ℕ) := by
+  rw [eval_pairWithZero, pairVal_append, val_equivFin_false, Nat.add_zero]
+
+@[simp] theorem size_pairWithZero (C : Circuit signature n w) :
+    (pairWithZero C).size = C.size + 1 := by
+  simp [pairWithZero]
+
+theorem depth_pairWithZero_le (C : Circuit signature n w) :
+    (pairWithZero C).depth ≤ max C.depth 1 := by
+  refine (Circuit.depth_append_le _ _).trans (max_le_max le_rfl ?_)
+  exact (Circuit.depth_comp_le _ _).trans (by simp)
+
+/-- Reduce carry-save pairs along the existing half-split tree; the empty sum is zero. -/
+def reducePairs (n w : ℕ) (cs : List (Circuit signature n (w + w))) :
+    Circuit signature n (w + w) :=
+  Circuit.balanced (csa4to2 w) (zeroPairCircuit n w) cs
+
+/-- The reduction preserves the complete sum modulo the word modulus. -/
+theorem pairVal_eval_reducePairs_mod (cs : List (Circuit signature n (w + w)))
+    (x : BitString n) :
+    pairVal ((reducePairs n w cs).eval interpretation x) % 2 ^ w =
+      (cs.map fun C => pairVal (C.eval interpretation x) % 2 ^ w).sum % 2 ^ w := by
+  rw [reducePairs, Circuit.eval_balanced]
+  exact List.balancedFold_induction
+    (op := fun u v : BitString (w + w) => (csa4to2 w).eval interpretation (Fin.append u v))
+    (e := (zeroPairCircuit n w).eval interpretation x)
+    (f := fun C : Circuit signature n (w + w) => C.eval interpretation x)
+    (p := fun (l : List (Circuit signature n (w + w))) (u : BitString (w + w)) =>
+      pairVal u % 2 ^ w =
+      (l.map fun C => pairVal (C.eval interpretation x) % 2 ^ w).sum % 2 ^ w)
+    (by simp [pairVal, fstBits, sndBits]) (fun C => by simp)
+    (fun l₁ l₂ u v _ _ hu hv => by
+      rw [pairVal_eval_csa4to2_mod, Nat.add_mod, hu, hv, ← Nat.add_mod,
+        List.map_append, List.sum_append]) cs
+
+/-- Charge the fallback only for the empty sum and every reduction gate for nonempty sums. -/
+theorem size_reducePairs_le (cs : List (Circuit signature n (w + w))) :
+    (reducePairs n w cs).size ≤ 1 + (cs.map Circuit.size).sum + cs.length * (40 * w) := by
+  by_cases h : cs = []
+  · subst cs
+    simp [reducePairs, Circuit.balanced]
+  · rw [reducePairs, Circuit.size_balanced _ _ h]
+    have := Nat.mul_le_mul (Nat.sub_le cs.length 1) (size_csa4to2_le w)
+    omega
+
+/-- The pair tree adds twelve levels per half-split round to the deepest supplied circuit. -/
+theorem depth_reducePairs_le (cs : List (Circuit signature n (w + w))) {D : ℕ}
+    (hD : ∀ C ∈ cs, C.depth ≤ D) :
+    (reducePairs n w cs).depth ≤ max D 1 + 12 * Nat.clog 2 cs.length := by
+  refine (Circuit.depth_balanced_le _ _ (D := max D 1)
+    (fun C hC => (hD C hC).trans (Nat.le_max_left _ _))
+    (fun _ => depth_zeroPairCircuit_le.trans (Nat.le_max_right _ _))).trans ?_
+  exact Nat.add_le_add_left (Nat.mul_le_mul_right _ (depth_csa4to2_le w)) _
+
+/-- Finish a balanced carry-save sum as one unsigned modular word. -/
+def sumPairs (n w : ℕ) (cs : List (Circuit signature n (w + w))) : Circuit signature n w :=
+  (carryLookaheadAdd w).comp (reducePairs n w cs)
+
+/-- Finishing a carry-save word computes its value modulo `2 ^ w`. -/
+theorem val_eval_carryLookaheadAdd_pair (p : BitString (w + w)) :
+    (BitString.equivFin w ((carryLookaheadAdd w).eval interpretation p) : ℕ) =
+      pairVal p % 2 ^ w := by
+  have hp : Fin.append (fstBits p) (sndBits p) = p := by
+    ext i
+    induction i using Fin.addCases <;>
+      simp only [fstBits, sndBits, Fin.append_left, Fin.append_right, Function.comp_apply]
+  simpa only [hp, pairVal] using val_eval_carryLookaheadAdd (fstBits p) (sndBits p)
+
+/-- The final word equals the complete pair sum, reduced only modulo the word width. -/
+theorem val_eval_sumPairs (cs : List (Circuit signature n (w + w))) (x : BitString n) :
+    (BitString.equivFin w ((sumPairs n w cs).eval interpretation x) : ℕ) =
+      (cs.map fun C => pairVal (C.eval interpretation x) % 2 ^ w).sum % 2 ^ w := by
+  rw [sumPairs, Circuit.eval_comp, val_eval_carryLookaheadAdd_pair,
+    pairVal_eval_reducePairs_mod]
+
+/-- Polynomial gate bound retaining the sizes of the actual input circuits. -/
+theorem size_sumPairs_le (cs : List (Circuit signature n (w + w))) :
+    (sumPairs n w cs).size ≤
+      21 * (w + 1) ^ 2 + 1 + (cs.map Circuit.size).sum + cs.length * (40 * w) := by
+  have h₁ := size_carryLookaheadAdd_le w
+  have h₂ := size_reducePairs_le cs
+  simp only [sumPairs, Circuit.size_comp]
+  omega
+
+/-- Logarithmic finishing in addition to the balanced pair-reduction depth. -/
+theorem depth_sumPairs_le (cs : List (Circuit signature n (w + w))) {D : ℕ}
+    (hD : ∀ C ∈ cs, C.depth ≤ D) :
+    (sumPairs n w cs).depth ≤
+      8 + 2 * Nat.clog 2 (w + 1) + max D 1 + 12 * Nat.clog 2 cs.length := by
+  have h₁ := depth_carryLookaheadAdd_le w
+  have h₂ := depth_reducePairs_le cs hD
+  exact (Circuit.depth_comp_le _ _).trans (by omega)
+
+end Cslib.Circuits.Boolean

Complexity/Computability/Circuit/Boolean/CarrySave/Reduce/PolyTime.lean

@@ -0,0 +1,116 @@
+/-
+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.CarrySave.Reduce
+import all Complexity.Computability.Circuit.Boolean.CarrySave.Reduce
+public import Complexity.Computability.Circuit.Boolean.CarrySave.PolyTime
+public import Complexity.Computability.Circuit.Boolean.CarryLookahead.PolyTime
+public import Complexity.Computability.Circuit.Boolean.BalancedCode
+public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
+
+/-!
+# Native generation of carry-save reductions
+
+The generator preserves the complete half-split reducer, its zero fallback and the final adder.
+Input counts and references are binary, word widths unary, and all supplied leaf code is charged.
+
+## Main results
+
+* `Cslib.Circuits.Boolean.sumPairsCode_eq_code`: exact reduction and final-adder code.
+* `Cslib.Circuits.Boolean.computableInPolyTime_sumPairsCode`: uniform native generation.
+-/
+
+public section
+
+namespace Cslib.Circuits.Boolean
+
+open Turing.MultiTapeTM ComputableTidilyInPolyTime
+
+local notation "Code" => List (Op × List ℕ) × List ℕ
+
+/-- One shared false gate with a complete repeated-output word. -/
+private def falseWordCode (n w : ℕ) : Code := ([(.const false, [])], List.replicate w n)
+
+private theorem falseWordCode_eq (n w : ℕ) :
+    falseWordCode n w =
+      ((Circuit.wiring signature (fun _ : Fin w => (0 : Fin 1))).comp
+        (Circuit.oneGate (n := n) (.const false) Fin.elim0)).code := by
+  apply Prod.ext
+  · rfl
+  change List.replicate w n = List.ofFn (fun _ : Fin w => n)
+  simp
+
+/-- Add the shared zero word to any supplied raw leaf code. -/
+def pairWithZeroCode (n w : ℕ) (C : Code) : Code :=
+  appendCode n C (falseWordCode n w)
+
+/-- Exact carry-save representation of the original leaf. -/
+theorem pairWithZeroCode_eq_code {n w : ℕ} (C : Circuit signature n w) :
+    pairWithZeroCode n w C.code = (pairWithZero C).code := by
+  rw [pairWithZeroCode, falseWordCode_eq, appendCode_code]
+  rfl
+
+/-- Generate the entire balanced sum and final carry-lookahead adder. -/
+def sumPairsCode (n w : ℕ) (leaves : List Code) : Code :=
+  compCode n (carryLookaheadAdd w).code
+    (balancedCode n (csa4to2 w).code (falseWordCode n (w + w)) leaves)
+
+/-- The raw generator preserves every original gate, fallback and output selector. -/
+theorem sumPairsCode_eq_code {n w : ℕ} (cs : List (Circuit signature n (w + w))) :
+    sumPairsCode n w (cs.map Circuit.code) = (sumPairs n w cs).code := by
+  rw [sumPairsCode, falseWordCode_eq, balancedCode_eq_code, compCode_code]
+  rfl
+
+/-- Shared zero words are generated in time polynomial in unary output width and binary arity. -/
+private theorem computableTidilyInPolyTime_falseWordCode
+    {α : Type} {enc : α ↪ List Bool} {n w : α → ℕ}
+    (hn : ComputableTidilyInPolyTime n enc encNat)
+    (hw : ComputableTidilyInPolyTime w enc encUnary) :
+    ComputableTidilyInPolyTime (fun a => falseWordCode (n a) (w a)) enc encCode := by
+  exact (const (encMid := encList encGate) [(Op.const false, [])]).prod
+    (replicate hw hn)
+
+/-- Pair generation charges all supplied leaf code. -/
+@[fun_prop] theorem computableInPolyTime_pairWithZeroCode
+    {α : Type} {enc : α ↪ List Bool} {n w : α → ℕ} {C : α → Code}
+    (hn : ComputableInPolyTime n enc encNat)
+    (hw : ComputableInPolyTime w enc encUnary)
+    (hC : ComputableInPolyTime C enc encCode) :
+    ComputableInPolyTime (fun a => pairWithZeroCode (n a) (w a) (C a)) enc encCode := by
+  have hn := hn.tidy
+  have hw := hw.tidy
+  have hC := hC.tidy
+  apply ComputableInPolyTime.of_tidy
+  unfold pairWithZeroCode
+  exact computableTidilyInPolyTime_appendCode hn hC
+    (computableTidilyInPolyTime_falseWordCode hn hw)
+
+/-- The native generator charges the complete leaf list and both reduction stages. -/
+@[fun_prop] theorem computableInPolyTime_sumPairsCode
+    {α : Type} {enc : α ↪ List Bool} {n w : α → ℕ} {cs : α → List Code}
+    (hn : ComputableInPolyTime n enc encNat)
+    (hw : ComputableInPolyTime w enc encUnary)
+    (hcs : ComputableInPolyTime cs enc (encList encCode)) :
+    ComputableInPolyTime (fun a => sumPairsCode (n a) (w a) (cs a)) enc encCode := by
+  have hn := hn.tidy
+  have hw := hw.tidy
+  have hcs := hcs.tidy
+  apply ComputableInPolyTime.of_tidy
+  unfold sumPairsCode
+  exact computableTidilyInPolyTime_compCode hn
+    (computableTidilyInPolyTime_carryLookaheadAdd.comp hw)
+    (computableTidilyInPolyTime_balancedCode hn
+      (computableTidilyInPolyTime_csa4to2.comp hw)
+      (computableTidilyInPolyTime_falseWordCode hn (by fun_prop)) hcs)
+
+end Cslib.Circuits.Boolean