diff --git a/Complexity.lean b/Complexity.lean index d76bc905b..de0031853 100644 --- a/Complexity.lean +++ b/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 diff --git a/Complexity/Computability/Circuit/Boolean/CarrySave/Reduce.lean b/Complexity/Computability/Circuit/Boolean/CarrySave/Reduce.lean new file mode 100644 index 000000000..69d91c4da --- /dev/null +++ b/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 diff --git a/Complexity/Computability/Circuit/Boolean/CarrySave/Reduce/PolyTime.lean b/Complexity/Computability/Circuit/Boolean/CarrySave/Reduce/PolyTime.lean new file mode 100644 index 000000000..6f1b2c4b7 --- /dev/null +++ b/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 diff --git a/Complexity/Computability/Circuit/Boolean/Modular/InnerProduct.lean b/Complexity/Computability/Circuit/Boolean/Modular/InnerProduct.lean new file mode 100644 index 000000000..7c3435ce1 --- /dev/null +++ b/Complexity/Computability/Circuit/Boolean/Modular/InnerProduct.lean @@ -0,0 +1,115 @@ +/- +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.Modular.Multiply +public import Complexity.Foundations.Data.BitString.Block + +/-! +# Modular inner products of unsigned word arrays + +Inputs are the complete first array followed by the complete second array, each in consecutive +least-significant-first word blocks. Products run in parallel, then a balanced carry-save tree +and one carry-lookahead addition compute the sum. The theorem applies to arbitrary raw words. + +## Main definitions + +* `Cslib.Circuits.Boolean.Modular.innerProduct`: the complete modular inner-product circuit. + +## Main results + +* `Cslib.Circuits.Boolean.Modular.val_eval_innerProduct`: exact modular inner-product semantics. +* `Cslib.Circuits.Boolean.Modular.depth_innerProduct_le`: logarithmic depth in count and width. + +## References + +This is the selected-row arithmetic used by [Gentry, Sahai and Waters][GentrySahaiWaters2013], +Sections 3.1 and 3.4, with the modular multiplier and carry-save bounds proved in companion files. +-/ + +public section + +namespace Cslib.Circuits.Boolean.Modular + +open BitString +open scoped BigOperators + +variable {k w : ℕ} + +/-- Read the same word position from each of the two input arrays. -/ +private def innerProductInputs (k w : ℕ) (j : Fin k) : Fin (w + w) → Fin (k * w + k * w) := + Fin.addCases (fun i => Fin.castAdd (k * w) (finProdFinEquiv (j, i))) + (fun i => Fin.natAdd (k * w) (finProdFinEquiv (j, i))) + +private theorem append_comp_innerProductInputs (j : Fin k) (a b : BitString (k * w)) : + Fin.append a b ∘ innerProductInputs k w j = Fin.append (block a j) (block b j) := by + funext i + refine Fin.addCases (fun h => ?_) (fun h => ?_) i <;> + simp only [Function.comp_apply, innerProductInputs, Fin.addCases_left, Fin.addCases_right, + Fin.append_left, Fin.append_right, block_apply] + +/-- One modular product of corresponding word blocks. -/ +private def innerProductTerm (k w : ℕ) (j : Fin k) : Circuit signature (k * w + k * w) w := + (multiply w).comp (Circuit.wiring signature (innerProductInputs k w j)) + +private theorem val_eval_innerProductTerm (j : Fin k) (a b : BitString (k * w)) : + (BitString.equivFin w ((innerProductTerm k w j).eval interpretation (Fin.append a b)) : ℕ) = + ((BitString.equivFin w (block a j) : ℕ) * (BitString.equivFin w (block b j) : ℕ)) % + 2 ^ w := by + rw [innerProductTerm, Circuit.eval_comp, Circuit.eval_wiring, append_comp_innerProductInputs, + val_eval_multiply] + +/-- Compute all word products in parallel, then sum their carry-save representations. -/ +def innerProduct (k w : ℕ) : Circuit signature (k * w + k * w) w := + sumPairs (k * w + k * w) w + (List.ofFn fun j : Fin k => pairWithZero (innerProductTerm k w j)) + +/-- Exact inner-product value, including empty arrays and zero-width words. -/ +theorem val_eval_innerProduct (a b : BitString (k * w)) : + (BitString.equivFin w ((innerProduct k w).eval interpretation (Fin.append a b)) : ℕ) = + (∑ j : Fin k, (BitString.equivFin w (block a j) : ℕ) * + (BitString.equivFin w (block b j) : ℕ)) % 2 ^ w := by + rw [innerProduct, val_eval_sumPairs] + simp only [List.map_ofFn, Function.comp_def, pairVal_eval_pairWithZero, + val_eval_innerProductTerm, Nat.mod_mod, List.sum_ofFn] + rw [← Finset.sum_nat_mod] + +/-- Both multiplication and the sum tree have logarithmic depth in their respective widths. -/ +theorem depth_innerProduct_le (k w : ℕ) : + (innerProduct k w).depth ≤ + 17 + 16 * Nat.clog 2 (w + 1) + 12 * Nat.clog 2 k := by + have h := depth_sumPairs_le + (List.ofFn fun j : Fin k => pairWithZero (innerProductTerm k w j)) + (D := 9 + 14 * Nat.clog 2 (w + 1)) (by + intro C hC + obtain ⟨j, rfl⟩ := List.mem_ofFn.mp hC + apply (depth_pairWithZero_le _).trans + apply max_le _ (by omega) + exact (Circuit.depth_comp_le _ _).trans (by + simp only [Circuit.depth_wiring, add_zero] + exact depth_multiply_le w)) + simp only [List.length_ofFn] at h + have he : max (9 + 14 * Nat.clog 2 (w + 1)) 1 = + 9 + 14 * Nat.clog 2 (w + 1) := max_eq_left (by omega) + rw [he] at h + exact h.trans (by omega) + +/-- Every product, fallback, pair-reduction gate and final addition is charged. -/ +theorem size_innerProduct_le (k w : ℕ) : + (innerProduct k w).size ≤ 105 * (k + 1) * (w + 1) ^ 2 := by + have h := size_sumPairs_le + (List.ofFn fun j : Fin k => pairWithZero (innerProductTerm k w j)) + simp only [List.map_ofFn, Function.comp_def, size_pairWithZero, innerProductTerm, + Circuit.size_comp, Circuit.size_wiring, zero_add, List.sum_ofFn, List.length_ofFn] at h + have hs : (∑ _j : Fin k, ((multiply w).size + 1)) ≤ k * (63 * (w + 1) ^ 2 + 1) := by + simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, smul_eq_mul] + exact Nat.mul_le_mul_left k (Nat.add_le_add_right (size_multiply_le w) 1) + apply h.trans + nlinarith [Nat.zero_le (k * w), Nat.zero_le (k * w ^ 2)] + +end Cslib.Circuits.Boolean.Modular diff --git a/Complexity/Computability/Circuit/Boolean/Modular/InnerProduct/PolyTime.lean b/Complexity/Computability/Circuit/Boolean/Modular/InnerProduct/PolyTime.lean new file mode 100644 index 000000000..c9909f94d --- /dev/null +++ b/Complexity/Computability/Circuit/Boolean/Modular/InnerProduct/PolyTime.lean @@ -0,0 +1,130 @@ +/- +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.Modular.InnerProduct +import all Complexity.Computability.Circuit.Boolean.Modular.InnerProduct +public import Complexity.Computability.Circuit.Boolean.Modular.Multiply.PolyTime +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 modular inner-product generation + +Unary array count and word width generate all block selectors, complete product circuits and the +balanced sum. Binary wire numbers and every generated code list are charged. + +## Main results + +* `Cslib.Circuits.Boolean.Modular.innerProductCode_eq_code`: exact raw and typed code agreement. +* `Cslib.Circuits.Boolean.Modular.computableInPolyTime_innerProduct`: native generation. +-/ + +public section + +namespace Cslib.Circuits.Boolean.Modular + +open Turing.MultiTapeTM ComputableTidilyInPolyTime + +local notation "Code" => List (Op × List ℕ) × List ℕ + +/-- Raw input selectors for the corresponding block of two complete word arrays. -/ +private def innerProductInputsCode (k w j : ℕ) : Code := + ([], (List.range w).map (fun i => j * w + i) ++ + (List.range w).map (fun i => k * w + (j * w + i))) + +private theorem innerProductInputsCode_eq {k w : ℕ} (j : Fin k) : + innerProductInputsCode k w j.val = + (Circuit.wiring signature (innerProductInputs k w j)).code := by + apply Prod.ext + · rfl + change _ = List.ofFn (fun i => (innerProductInputs k w j i).val) + rw [List.ofFn_add] + have hl : (fun i : Fin w => (innerProductInputs k w j (Fin.castAdd w i)).val) = + (fun i : Fin w => j.val * w + i.val) := by + funext i + simp only [innerProductInputs, Fin.addCases_left, Fin.val_castAdd] + simp [finProdFinEquiv, Nat.add_comm, Nat.mul_comm] + have hr : (fun i : Fin w => (innerProductInputs k w j (Fin.natAdd w i)).val) = + (fun i : Fin w => k * w + (j.val * w + i.val)) := by + funext i + simp only [innerProductInputs, Fin.addCases_right, Fin.val_natAdd] + simp [finProdFinEquiv, Nat.add_comm, Nat.mul_comm] + change _ ++ _ = List.ofFn (fun i : Fin w => + (innerProductInputs k w j (Fin.castAdd w i)).val) ++ _ + rw [hl, hr] + congr 1 <;> apply List.ext_getElem (by simp) <;> intro i hi hi' <;> simp + +/-- Generate every product and its zero carry-save companion before the complete sum. -/ +def innerProductCode (k w : ℕ) : Code := + sumPairsCode (k * w + k * w) w ((List.range k).map fun j => + pairWithZeroCode (k * w + k * w) w + (compCode (k * w + k * w) (multiplyCode w) (innerProductInputsCode k w j))) + +/-- Gate-for-gate agreement includes empty arrays and zero-width words. -/ +theorem innerProductCode_eq_code (k w : ℕ) : + innerProductCode k w = (innerProduct k w).code := by + have he : (List.range k).map (fun j => pairWithZeroCode (k * w + k * w) w + (compCode (k * w + k * w) (multiplyCode w) (innerProductInputsCode k w j))) = + (List.ofFn fun j : Fin k => pairWithZero (innerProductTerm k w j)).map Circuit.code := by + rw [List.map_ofFn] + apply List.ext_getElem (by simp) + intro j hj hj' + simp only [List.getElem_map, List.getElem_range, List.getElem_ofFn] + rw [multiplyCode_eq_code, innerProductInputsCode_eq ⟨j, by simpa using hj⟩, + compCode_code, pairWithZeroCode_eq_code] + rfl + rw [innerProductCode, he, sumPairsCode_eq_code] + rfl + +/-- The full constructor is uniform in unary count and width. -/ +@[fun_prop] theorem computableInPolyTime_innerProduct : + ComputableInPolyTime (fun p : ℕ × ℕ => (innerProduct p.1 p.2).code) + (encPair encUnary encUnary) encCode := by + have hw : ComputableTidilyInPolyTime (fun p : (ℕ × ℕ) × ℕ => p.1.2) + (encPair (encPair encUnary encUnary) encUnary) encUnary := by fun_prop + have hk : ComputableTidilyInPolyTime (fun p : (ℕ × ℕ) × ℕ => p.1.1) + (encPair (encPair encUnary encUnary) encUnary) encNat := by fun_prop + have hj : ComputableTidilyInPolyTime (fun p : (ℕ × ℕ) × ℕ => p.2) + (encPair (encPair encUnary encUnary) encUnary) encNat := by fun_prop + have hw' := unary_to_binary.comp hw + have hwire : ComputableTidilyInPolyTime + (fun p : ((ℕ × ℕ) × ℕ) × ℕ => p.1.2 * p.1.1.2 + p.2) + (encPair (encPair (encPair encUnary encUnary) encUnary) encUnary) encNat := by fun_prop + have hwire' : ComputableTidilyInPolyTime + (fun p : ((ℕ × ℕ) × ℕ) × ℕ => p.1.1.1 * p.1.1.2 + + (p.1.2 * p.1.1.2 + p.2)) + (encPair (encPair (encPair encUnary encUnary) encUnary) encUnary) encNat := by fun_prop + have hin : ComputableTidilyInPolyTime + (fun p : (ℕ × ℕ) × ℕ => innerProductInputsCode p.1.1 p.1.2 p.2) + (encPair (encPair encUnary encUnary) encUnary) encCode := + (const (encMid := encList encGate) []).prod + (listAppend' (mapWith hwire id' (range.comp hw)) + (mapWith hwire' id' (range.comp hw))) + have hleaf : ComputableTidilyInPolyTime + (fun p : (ℕ × ℕ) × ℕ => pairWithZeroCode (p.1.1 * p.1.2 + p.1.1 * p.1.2) + p.1.2 (compCode (p.1.1 * p.1.2 + p.1.1 * p.1.2) + (multiplyCode p.1.2) (innerProductInputsCode p.1.1 p.1.2 p.2))) + (encPair (encPair encUnary encUnary) encUnary) encCode := by + apply ComputableInPolyTime.tidy + apply computableInPolyTime_pairWithZeroCode (.of_tidy (by fun_prop)) (.of_tidy hw) + apply ComputableInPolyTime.of_tidy + apply computableTidilyInPolyTime_compCode (by fun_prop) _ hin + simpa only [multiplyCode_eq_code, Function.comp_def] using + computableInPolyTime_multiply.tidy.comp hw + have h := computableInPolyTime_sumPairsCode + (show ComputableInPolyTime (fun p : ℕ × ℕ => p.1 * p.2 + p.1 * p.2) + (encPair encUnary encUnary) encNat from .of_tidy (by fun_prop)) + (.of_tidy (snd _ _)) + (.of_tidy (mapWith hleaf id' (range.comp (fst _ _)))) + simpa only [← innerProductCode_eq_code, innerProductCode, Function.comp_def] using h + +end Cslib.Circuits.Boolean.Modular diff --git a/Complexity/Computability/Circuit/Boolean/Modular/Multiply.lean b/Complexity/Computability/Circuit/Boolean/Modular/Multiply.lean new file mode 100644 index 000000000..606c061ba --- /dev/null +++ b/Complexity/Computability/Circuit/Boolean/Modular/Multiply.lean @@ -0,0 +1,83 @@ +/- +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.Modular.PartialProduct +import Mathlib.Tactic.Ring + +/-! +# Logarithmic-depth modular multiplication + +All shifted partial products are generated in parallel, reduced along the existing half-split +carry-save tree, and finished by carry lookahead. The result is the product modulo `2 ^ w` on +every pair of words. Width zero uses the actual empty carry-save fallback and finishing circuit. + +## Main definitions + +* `Cslib.Circuits.Boolean.Modular.multiply`: the complete unsigned modular multiplier. + +## Main results + +* `Cslib.Circuits.Boolean.Modular.val_eval_multiply`: exact multiplication modulo `2 ^ w`. +* `Cslib.Circuits.Boolean.Modular.depth_multiply_le`: depth at most `9 + 14 * clog 2 (w + 1)`. +* `Cslib.Circuits.Boolean.Modular.size_multiply_le`: at most `63 * (w + 1)^2` gates. + +## References + +Binary partial products and carry-save reduction follow [Vollmer, Chapter 1][Vollmer1999]; +parallel-prefix finishing follows [Ladner and Fischer][LadnerFischer1980]. +-/ + +public section + +namespace Cslib.Circuits.Boolean.Modular + +open BitString +open scoped BigOperators + +variable {w : ℕ} + +/-- Reduce all shifted partial products and finish their sum with carry lookahead. -/ +def multiply (w : ℕ) : Circuit signature (w + w) w := + sumPairs (w + w) w (List.ofFn fun i : Fin w => pairWithZero (partialProduct w i)) + +/-- The circuit computes the modular product of arbitrary input words. -/ +theorem val_eval_multiply (a b : BitString w) : + (BitString.equivFin w ((multiply w).eval interpretation (Fin.append a b)) : ℕ) = + ((BitString.equivFin w a : ℕ) * (BitString.equivFin w b : ℕ)) % 2 ^ w := by + rw [multiply, val_eval_sumPairs] + simp only [List.map_ofFn, Function.comp_def, pairVal_eval_pairWithZero, + val_eval_partialProduct, List.sum_ofFn] + have ht (i : Fin w) : + (if b i then ((BitString.equivFin w a : ℕ) * 2 ^ i.val) % 2 ^ w else 0) % 2 ^ w = + ((BitString.equivFin w a : ℕ) * ((b i).toNat * 2 ^ i.val)) % 2 ^ w := by + cases b i <;> simp + simp_rw [ht] + rw [← Finset.sum_nat_mod, ← Finset.mul_sum, ← BitString.val_equivFin_eq_sum] + +/-- The balanced pair tree uses one-level leaves and logarithmic-depth finishing. -/ +theorem depth_multiply_le (w : ℕ) : + (multiply w).depth ≤ 9 + 14 * Nat.clog 2 (w + 1) := by + have h := depth_sumPairs_le + (List.ofFn fun i : Fin w => pairWithZero (partialProduct w i)) (D := 1) (by + intro C hC + obtain ⟨i, rfl⟩ := List.mem_ofFn.mp hC + exact (depth_pairWithZero_le _).trans (max_le (depth_partialProduct_le i) le_rfl)) + simp only [List.length_ofFn, max_self] at h + have hm : Nat.clog 2 w ≤ Nat.clog 2 (w + 1) := Nat.clog_mono_right 2 (Nat.le_succ w) + exact h.trans (by omega) + +/-- Every partial product and every carry-save gate is charged. -/ +theorem size_multiply_le (w : ℕ) : (multiply w).size ≤ 63 * (w + 1) ^ 2 := by + have h := size_sumPairs_le (List.ofFn fun i : Fin w => pairWithZero (partialProduct w i)) + simp only [List.map_ofFn, Function.comp_def, size_pairWithZero, size_partialProduct, + List.sum_ofFn, Finset.sum_const, Finset.card_univ, Fintype.card_fin, smul_eq_mul, + List.length_ofFn] at h + exact h.trans (by nlinarith) + +end Cslib.Circuits.Boolean.Modular diff --git a/Complexity/Computability/Circuit/Boolean/Modular/Multiply/PolyTime.lean b/Complexity/Computability/Circuit/Boolean/Modular/Multiply/PolyTime.lean new file mode 100644 index 000000000..314df0587 --- /dev/null +++ b/Complexity/Computability/Circuit/Boolean/Modular/Multiply/PolyTime.lean @@ -0,0 +1,72 @@ +/- +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.Modular.Multiply +import all Complexity.Computability.Circuit.Boolean.Modular.Multiply +public import Complexity.Computability.Circuit.Boolean.Modular.PartialProduct.PolyTime +public import Complexity.Computability.Circuit.Boolean.CarrySave.Reduce.PolyTime +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 modular multiplier generation + +All shifted partial products, balanced carry-save gates and the final adder are generated from +unary width. The output is the full existing circuit code, including unused fallback gates. + +## Main results + +* `Cslib.Circuits.Boolean.Modular.multiplyCode_eq_code`: exact code agreement. +* `Cslib.Circuits.Boolean.Modular.computableInPolyTime_multiply`: uniform native generation. +-/ + +public section + +namespace Cslib.Circuits.Boolean.Modular + +open Turing.MultiTapeTM ComputableTidilyInPolyTime + +/-- Generate the complete modular multiplier, preserving the half-split reduction topology. -/ +def multiplyCode (w : ℕ) : List (Op × List ℕ) × List ℕ := + sumPairsCode (w + w) w ((List.range w).map fun i => + pairWithZeroCode (w + w) w (partialProductCode w i)) + +/-- Raw generation agrees gate-for-gate with the total typed modular multiplier. -/ +theorem multiplyCode_eq_code (w : ℕ) : multiplyCode w = (multiply w).code := by + have he : (List.range w).map (fun i => + pairWithZeroCode (w + w) w (partialProductCode w i)) = + (List.ofFn fun i : Fin w => pairWithZero (partialProduct w i)).map Circuit.code := by + rw [List.map_ofFn] + apply List.ext_getElem (by simp) + intro i hi hi' + simp only [List.getElem_map, List.getElem_range, List.getElem_ofFn] + rw [partialProductCode_eq_code ⟨i, by simpa using hi⟩, pairWithZeroCode_eq_code] + rfl + rw [multiplyCode, he, sumPairsCode_eq_code] + rfl + +/-- Generation is native polynomial-time in unary width, charging the complete binary code. -/ +@[fun_prop] theorem computableInPolyTime_multiply : + ComputableInPolyTime (fun w => (multiply w).code) encUnary encCode := by + have hl : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => + pairWithZeroCode (p.1 + p.1) p.1 (partialProductCode p.1 p.2)) + (encPair encUnary encUnary) encCode := by + exact (computableInPolyTime_pairWithZeroCode + (.of_tidy (by fun_prop)) (.of_tidy (by fun_prop)) + computableInPolyTime_partialProductCode).tidy + have h := computableInPolyTime_sumPairsCode + (show ComputableInPolyTime (fun w : ℕ => w + w) encUnary encNat from + .of_tidy (by fun_prop)) + (.of_tidy id') (.of_tidy (mapWith hl id' range)) + simpa only [← multiplyCode_eq_code, multiplyCode] using h + +end Cslib.Circuits.Boolean.Modular diff --git a/Complexity/Computability/Circuit/Boolean/Modular/PartialProduct.lean b/Complexity/Computability/Circuit/Boolean/Modular/PartialProduct.lean new file mode 100644 index 000000000..ba025b0ad --- /dev/null +++ b/Complexity/Computability/Circuit/Boolean/Modular/PartialProduct.lean @@ -0,0 +1,100 @@ +/- +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 + +/-! +# Shifted partial products of unsigned words + +One circuit layer selects the shifted first word by one bit of the second word. Bits shifted +past the output width are discarded; this computes a modular partial product on every input. + +## Main definitions + +* `Cslib.Circuits.Boolean.Modular.partialProduct`: a shifted partial-product word. + +## Main results + +* `Cslib.Circuits.Boolean.Modular.val_eval_partialProduct`: its exact unsigned modular value. +* `Cslib.Circuits.Boolean.Modular.depth_partialProduct_le`: one circuit layer suffices. + +## References + +The carry-save multiplication construction is standard binary partial-product arithmetic; +see [Vollmer, Chapter 1][Vollmer1999]. +-/ + +public section + +namespace Cslib.Circuits.Boolean.Modular + +open BitString + +variable {w : ℕ} + +/-- Each retained product digit is one AND gate; lower shifted-out positions are false. -/ +private def partialProductBit (w : ℕ) (i j : Fin w) : Formula signature (w + w) := + if h : i.val ≤ j.val then + (Formula.input (Fin.castAdd w ⟨j.val - i.val, by omega⟩)).and + (.input (Fin.natAdd w i)) + else .const false + +/-- Multiply the first word by the `i`th bit of the second word, shifted by `i`. -/ +def partialProduct (w : ℕ) (i : Fin w) : Circuit signature (w + w) w := + Circuit.pi fun j => (partialProductBit w i j).toCircuit + +private theorem eval_partialProduct (i j : Fin w) (a b : BitString w) : + (partialProduct w i).eval interpretation (Fin.append a b) j = + if h : i.val ≤ j.val then a ⟨j.val - i.val, by omega⟩ && b i else false := by + by_cases h : i.val ≤ j.val + · simp only [partialProduct, Circuit.eval_pi, Formula.eval_toCircuit, partialProductBit, + h, ↓reduceDIte, Formula.eval_and, Formula.eval_input, Fin.append_left, Fin.append_right] + · simp only [partialProduct, Circuit.eval_pi, Formula.eval_toCircuit, partialProductBit, + h, ↓reduceDIte, Formula.eval_const] + +/-- The circuit word agrees with the corresponding truncated `BitVec` shift. -/ +private theorem word_eval_partialProduct (i : Fin w) (a b : BitString w) : + word ((partialProduct w i).eval interpretation (Fin.append a b)) = + if b i then word a <<< i.val else 0 := by + apply BitVec.eq_of_getLsbD_eq + intro j hj + rw [getLsbD_word _ ⟨j, hj⟩, eval_partialProduct] + by_cases h : i.val ≤ j + · have hji : j - i.val < w := by omega + have hbit := getLsbD_word a ⟨j - i.val, hji⟩ + cases b i <;> simp_all + · have hij : j < i.val := Nat.lt_of_not_ge h + cases b i <;> simp_all + +/-- Unsigned value of one shifted partial product, including overflow truncation. -/ +theorem val_eval_partialProduct (i : Fin w) (a b : BitString w) : + (BitString.equivFin w ((partialProduct w i).eval interpretation (Fin.append a b)) : ℕ) = + if b i then ((BitString.equivFin w a : ℕ) * 2 ^ i.val) % 2 ^ w else 0 := by + rw [← toNat_word_eq_equivFin, word_eval_partialProduct] + split_ifs + · rw [BitVec.toNat_shiftLeft, Nat.shiftLeft_eq, toNat_word_eq_equivFin] + · rfl + +/-- Exactly one gate per output bit, including the false low positions. -/ +@[simp] theorem size_partialProduct (i : Fin w) : (partialProduct w i).size = w := by + simp only [partialProduct, Circuit.size_pi, Formula.size_toCircuit] + have h (j : Fin w) : (partialProductBit w i j).size = 1 := by + unfold partialProductBit + split_ifs <;> simp + simp only [h, Finset.sum_const, Finset.card_univ, Fintype.card_fin, smul_eq_mul, mul_one] + +/-- All product digits are produced in parallel at depth one. -/ +theorem depth_partialProduct_le (i : Fin w) : (partialProduct w i).depth ≤ 1 := by + apply Circuit.depth_pi_le + intro j + apply (Formula.depth_toCircuit_le _).trans + unfold partialProductBit + split_ifs <;> simp + +end Cslib.Circuits.Boolean.Modular diff --git a/Complexity/Computability/Circuit/Boolean/Modular/PartialProduct/PolyTime.lean b/Complexity/Computability/Circuit/Boolean/Modular/PartialProduct/PolyTime.lean new file mode 100644 index 000000000..74c665af0 --- /dev/null +++ b/Complexity/Computability/Circuit/Boolean/Modular/PartialProduct/PolyTime.lean @@ -0,0 +1,114 @@ +/- +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.Modular.PartialProduct +import all Complexity.Computability.Circuit.Boolean.Modular.PartialProduct +public import Complexity.Computability.Circuit.Boolean.CodeTemplate +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 partial-product generation + +The complete shifted word is generated from unary width and shift. Every emitted gate and binary +wire is charged. Out-of-range raw shifts have total behavior; the exact circuit theorem uses a +valid shift. + +## Main results + +* `Cslib.Circuits.Boolean.Modular.partialProductCode_eq_code`: exact typed-circuit agreement. +* `Cslib.Circuits.Boolean.Modular.computableInPolyTime_partialProductCode`: native generation. +-/ + +public section + +namespace Cslib.Circuits.Boolean.Modular + +open Turing.MultiTapeTM ComputableTidilyInPolyTime + +variable {w : ℕ} + +/-- Code for one retained product digit or its zero fallback. -/ +private def partialProductBitCode (w i j : ℕ) : List (Op × List ℕ) × List ℕ := + if i ≤ j then formulaCode (w + w) + ((Formula.input (n := 2) 0).and (.input 1)) ![j - i, w + i] + else ([(.const false, [])], [w + w]) + +/-- Generate all retained shifted product digits, including the zero lower positions. -/ +def partialProductCode (w i : ℕ) : List (Op × List ℕ) × List ℕ := + appendCodes (w + w) ((List.range w).map (partialProductBitCode w i)) + +private theorem partialProductBitCode_eq (i j : Fin w) : + partialProductBitCode w i.val j.val = (partialProductBit w i j).toCircuit.code := by + by_cases h : i.val ≤ j.val + · let wires : Fin 2 → Fin (w + w) := + ![Fin.castAdd w ⟨j.val - i.val, by omega⟩, Fin.natAdd w i] + have he : (fun k => (wires k).val) = ![j.val - i.val, w + i.val] := by + funext k + fin_cases k <;> rfl + have ht := formulaCode_eq_code ((Formula.input (n := 2) 0).and (.input 1)) wires + rw [he] at ht + have hf : (((Formula.input (n := 2) 0).and (.input 1)).rename wires) = + partialProductBit w i j := by + simp only [partialProductBit, h, ↓reduceDIte, Formula.rename, Formula.and, + Formula.gate_bind] + congr 1 + funext k + fin_cases k <;> rfl + rw [hf] at ht + simpa only [partialProductBitCode, h, ↓reduceIte] using ht + · simp only [partialProductBitCode, partialProductBit, h, ↓reduceIte, ↓reduceDIte] + rfl + +/-- Native generation retains exactly the existing parallel partial-product circuit. -/ +theorem partialProductCode_eq_code (i : Fin w) : + partialProductCode w i.val = (partialProduct w i).code := by + have he : (List.range w).map (partialProductBitCode w i.val) = + List.ofFn (fun j : Fin w => (partialProductBit w i j).toCircuit.code) := by + apply List.ext_getElem (by simp) + intro j hj hj' + simpa only [List.getElem_map, List.getElem_range, List.getElem_ofFn] using + partialProductBitCode_eq i ⟨j, by simpa using hj⟩ + rw [partialProductCode, he, appendCodes_code] + rfl + +/-- The full raw partial-product code is generated uniformly in unary width and shift. -/ +theorem computableInPolyTime_partialProductCode : + ComputableInPolyTime (fun p : ℕ × ℕ => partialProductCode p.1 p.2) + (encPair encUnary encUnary) encCode := by + apply ComputableInPolyTime.of_tidy + have hw : ComputableTidilyInPolyTime (fun p : (ℕ × ℕ) × ℕ => p.1.1) + (encPair (encPair encUnary encUnary) encUnary) encNat := by fun_prop + have hi : ComputableTidilyInPolyTime (fun p : (ℕ × ℕ) × ℕ => p.1.2) + (encPair (encPair encUnary encUnary) encUnary) encNat := by fun_prop + have hj : ComputableTidilyInPolyTime (fun p : (ℕ × ℕ) × ℕ => p.2) + (encPair (encPair encUnary encUnary) encUnary) encNat := by fun_prop + have ht : ComputableTidilyInPolyTime (fun p : (ℕ × ℕ) × ℕ => + formulaCode (p.1.1 + p.1.1) + ((Formula.input (n := 2) 0).and (.input 1)) ![p.2 - p.1.2, p.1.1 + p.1.2]) + (encPair (encPair encUnary encUnary) encUnary) encCode := by + apply computableTidilyInPolyTime_formulaCode _ (by fun_prop) + intro k + fin_cases k + · change ComputableTidilyInPolyTime (fun p : (ℕ × ℕ) × ℕ => p.2 - p.1.2) _ encNat + fun_prop + · change ComputableTidilyInPolyTime (fun p : (ℕ × ℕ) × ℕ => p.1.1 + p.1.2) _ encNat + fun_prop + have hb : ComputableTidilyInPolyTime + (fun p : (ℕ × ℕ) × ℕ => partialProductBitCode p.1.1 p.1.2 p.2) + (encPair (encPair encUnary encUnary) encUnary) encCode := by + unfold partialProductBitCode + fun_prop + exact computableTidilyInPolyTime_appendCodes (by fun_prop) + (mapWith hb id' (range.comp (fst _ _))) + +end Cslib.Circuits.Boolean.Modular diff --git a/Complexity/Computability/Circuit/Boolean/Modular/Subtract.lean b/Complexity/Computability/Circuit/Boolean/Modular/Subtract.lean new file mode 100644 index 000000000..2eadad95a --- /dev/null +++ b/Complexity/Computability/Circuit/Boolean/Modular/Subtract.lean @@ -0,0 +1,117 @@ +/- +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 + +/-! +# Modular subtraction with carry lookahead + +Subtract by complementing the second word and supplying an incoming carry of one. The output +discards the final carry, so underflow wraps modulo `2 ^ w` instead of truncated subtraction. + +## Main definitions + +* `Cslib.Circuits.Boolean.Modular.subtract`: the modular subtraction circuit. + +## Main results + +* `Cslib.Circuits.Boolean.Modular.val_eval_subtract`: exact modular subtraction on all words. +* `Cslib.Circuits.Boolean.Modular.depth_subtract_le`: depth at most `8 + 2 * clog 2 (w + 1)`. + +## References + +Parallel-prefix finishing follows [Ladner and Fischer][LadnerFischer1980]. +-/ + +public section + +namespace Cslib.Circuits.Boolean.Modular + +open BitString + +variable {w : ℕ} + +/-- Keep the first word, complement the second word in parallel, and append a true carry. -/ +private def subtractInputs (w : ℕ) : Circuit signature (w + w) (w + w + 1) := + ((Circuit.wiring signature (Fin.castAdd w)).append + (Circuit.pi fun i : Fin w => (Formula.input (Fin.natAdd w i)).not.toCircuit)).append + (Circuit.oneGate (.const true) Fin.elim0) + +@[simp] private theorem eval_subtractInputs (a b : BitString w) : + (subtractInputs w).eval interpretation (Fin.append a b) = + Fin.append (Fin.append a (fun i => !b i)) (fun _ => true) := by + simp only [subtractInputs, Circuit.eval_append, Circuit.eval_wiring, Circuit.eval_pi, + Formula.eval_toCircuit, Formula.eval_not, Formula.eval_input, Fin.append_right] + congr 2 + funext i + exact Fin.append_left a b i + +@[simp] private theorem size_subtractInputs (w : ℕ) : (subtractInputs w).size = w + 1 := by + simp [subtractInputs] + +private theorem depth_subtractInputs_le (w : ℕ) : (subtractInputs w).depth ≤ 1 := by + apply (Circuit.depth_append_le _ _).trans + apply max_le + · apply (Circuit.depth_append_le _ _).trans + apply max_le (by simp) + apply Circuit.depth_pi_le + intro i + exact (Formula.depth_toCircuit_le _).trans (by simp) + · simp + +/-- Discard the carry-out after adding the first word, the second word's complement and one. -/ +def subtract (w : ℕ) : Circuit signature (w + w) w := + (Circuit.wiring signature (fun i : Fin w => i.castSucc)).comp + ((carryLookahead w).comp (subtractInputs w)) + +private theorem val_not (b : BitString w) : + (BitString.equivFin w (fun i => !b i) : ℕ) = 2 ^ w - 1 - (BitString.equivFin w b : ℕ) := by + have h : word (fun i => !b i) = ~~~word b := by + apply BitVec.eq_of_getLsbD_eq + intro i hi + simp only [getLsbD_word _ ⟨i, hi⟩, BitVec.getLsbD_not, hi, decide_true, Bool.true_and] + have hv := congrArg BitVec.toNat h + simpa only [toNat_word_eq_equivFin, BitVec.toNat_not] using hv + +/-- Modular subtraction, expressed without a truncated natural subtraction of the inputs. -/ +theorem val_eval_subtract (a b : BitString w) : + (BitString.equivFin w ((subtract w).eval interpretation (Fin.append a b)) : ℕ) = + (2 ^ w - (BitString.equivFin w b : ℕ) + (BitString.equivFin w a : ℕ)) % 2 ^ w := by + have h := val_eval_carryLookahead a (fun i => !b i) true + rw [BitString.val_equivFin_succ] at h + have hm := congrArg (· % 2 ^ w) h + rw [Nat.add_mul_mod_self_right] at hm + have he : (subtract w).eval interpretation (Fin.append a b) = + Fin.init ((carryLookahead w).eval interpretation + (Fin.append (Fin.append a (fun i => !b i)) (fun _ => true))) := by + simp only [subtract, Circuit.eval_comp, Circuit.eval_wiring, eval_subtractInputs] + rfl + rw [he] + have hb := (BitString.equivFin w b).isLt + rw [val_not, Bool.toNat_true] at hm + have hv : (BitString.equivFin w a : ℕ) + + (2 ^ w - 1 - (BitString.equivFin w b : ℕ)) + 1 = + 2 ^ w - (BitString.equivFin w b : ℕ) + (BitString.equivFin w a : ℕ) := by omega + rw [hv] at hm + exact (Nat.mod_eq_of_lt (BitString.equivFin w _).isLt).symm.trans hm + +theorem depth_subtract_le (w : ℕ) : + (subtract w).depth ≤ 8 + 2 * Nat.clog 2 (w + 1) := by + have h := (Circuit.depth_comp_le (carryLookahead w) (subtractInputs w)).trans + (Nat.add_le_add (depth_carryLookahead_le w) (depth_subtractInputs_le w)) + apply (Circuit.depth_comp_le _ _).trans + simp only [Circuit.depth_wiring, zero_add] + omega + +theorem size_subtract_le (w : ℕ) : (subtract w).size ≤ 21 * (w + 1) ^ 2 := by + have h := size_carryLookahead_le w + simp only [subtract, Circuit.size_comp, Circuit.size_wiring, size_subtractInputs] + nlinarith + +end Cslib.Circuits.Boolean.Modular diff --git a/Complexity/Computability/Circuit/Boolean/Modular/Subtract/PolyTime.lean b/Complexity/Computability/Circuit/Boolean/Modular/Subtract/PolyTime.lean new file mode 100644 index 000000000..abc17a1c9 --- /dev/null +++ b/Complexity/Computability/Circuit/Boolean/Modular/Subtract/PolyTime.lean @@ -0,0 +1,122 @@ +/- +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.Modular.Subtract +import all Complexity.Computability.Circuit.Boolean.Modular.Subtract +public import Complexity.Computability.Circuit.Boolean.CarryLookahead.PolyTime +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 modular subtraction generation + +The complete complement-plus-carry construction is generated from unary width. All circuit gates, +wire references and output selectors are charged. + +## Main results + +* `Cslib.Circuits.Boolean.Modular.subtractCode_eq_code`: exact generated code. +* `Cslib.Circuits.Boolean.Modular.computableInPolyTime_subtract`: native constructor. +-/ + +public section + +namespace Cslib.Circuits.Boolean.Modular + +open Turing.MultiTapeTM ComputableTidilyInPolyTime + +local notation "Code" => List (Op × List ℕ) × List ℕ + +private def notCode (w i : ℕ) : Code := + formulaCode (w + w) (Formula.input (n := 1) 0).not (fun _ => w + i) + +private theorem notCode_eq {w : ℕ} (i : Fin w) : + notCode w i.val = (Formula.input (Fin.natAdd w i)).not.toCircuit.code := by + have h := formulaCode_eq_code (Formula.input (n := 1) 0).not + (fun _ => Fin.natAdd w i) + exact h + +private theorem firstCode_eq (w : ℕ) : + ([], List.range w) = (Circuit.wiring signature (Fin.castAdd w : Fin w → Fin (w + w))).code := by + apply Prod.ext + · rfl + · apply List.ext_getElem (by simp [Circuit.code, Circuit.wiring]) + intro i hi hi' + simp [Circuit.code, Circuit.wiring] + +private theorem outputCode_eq (w : ℕ) : + ([], List.range w) = + (Circuit.wiring signature (fun i : Fin w => i.castSucc)).code := by + apply Prod.ext + · rfl + · apply List.ext_getElem (by simp [Circuit.code, Circuit.wiring]) + intro i hi hi' + simp [Circuit.code, Circuit.wiring] + +private def inputsCode (w : ℕ) : Code := + appendCode (w + w) + (appendCode (w + w) ([], List.range w) + (appendCodes (w + w) ((List.range w).map (notCode w)))) + ([(.const true, [])], [w + w]) + +private theorem inputsCode_eq (w : ℕ) : inputsCode w = (subtractInputs w).code := by + have he : (List.range w).map (notCode w) = + List.ofFn (fun i : Fin w => (Formula.input (Fin.natAdd w i)).not.toCircuit.code) := by + apply List.ext_getElem (by simp) + intro i hi hi' + simpa only [List.getElem_map, List.getElem_range, List.getElem_ofFn] using + notCode_eq ⟨i, by simpa using hi⟩ + have ht : ([(Op.const true, [])], [w + w]) = + (Circuit.oneGate (σ := signature) (n := w + w) (.const true) Fin.elim0).code := rfl + rw [inputsCode, he, firstCode_eq, ht, appendCodes_code, appendCode_code, appendCode_code] + rfl + +/-- Generate the full modular subtractor, including the shared carry and discarded carry-out. -/ +def subtractCode (w : ℕ) : Code := + private_decl% (compCode (w + w) ([], List.range w) + (compCode (w + w) (carryLookahead w).code (inputsCode w))) + +/-- Raw generation preserves the complete typed subtractor. -/ +theorem subtractCode_eq_code (w : ℕ) : subtractCode w = (subtract w).code := by + change compCode (w + w) ([], List.range w) + (compCode (w + w) (carryLookahead w).code (inputsCode w)) = _ + rw [inputsCode_eq, outputCode_eq, compCode_code, compCode_code] + rfl + +/-- Full generation is polynomial-time in unary width, including binary gate and output indices. -/ +@[fun_prop] theorem computableInPolyTime_subtract : + ComputableInPolyTime (fun w => (subtract w).code) encUnary encCode := by + apply ComputableInPolyTime.of_tidy + have hn : ComputableTidilyInPolyTime (fun w : ℕ => w + w) encUnary encNat := by fun_prop + have hr : ComputableTidilyInPolyTime (fun w : ℕ => ([], List.range w)) encUnary encCode := + by + simpa only [Function.comp_def, List.map_id_fun', id_eq] using + (const (encMid := encList encGate) []).prod (unary_to_binary.map.comp range) + have hnot : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => notCode p.1 p.2) + (encPair encUnary encUnary) encCode := by + apply computableTidilyInPolyTime_formulaCode _ (by fun_prop) + intro i + change ComputableTidilyInPolyTime (fun p : ℕ × ℕ => p.1 + p.2) _ encNat + fun_prop + have ht : ComputableTidilyInPolyTime (fun w : ℕ => ([(Op.const true, [])], [w + w])) + encUnary encCode := (const _).prod (hn.cons' (const [])) + have hi := computableTidilyInPolyTime_appendCode hn + (computableTidilyInPolyTime_appendCode hn hr + (computableTidilyInPolyTime_appendCodes hn (mapWith hnot id' range))) ht + have h := computableTidilyInPolyTime_compCode hn hr + (computableTidilyInPolyTime_compCode hn computableTidilyInPolyTime_carryLookahead hi) + simp_rw [← subtractCode_eq_code] + change ComputableTidilyInPolyTime (fun w => compCode (w + w) ([], List.range w) + (compCode (w + w) (carryLookahead w).code (inputsCode w))) encUnary encCode + simpa only [inputsCode, Function.comp_def, List.map_id_fun', id_eq] using h + +end Cslib.Circuits.Boolean.Modular diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/DecryptionCircuit.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/DecryptionCircuit.lean new file mode 100644 index 000000000..96c3086e6 --- /dev/null +++ b/Complexity/Crypto/Computational/Homomorphic/GSW/DecryptionCircuit.lean @@ -0,0 +1,282 @@ +/- +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.Crypto.Computational.Homomorphic.GSW.Serialized.Evaluation +public import Complexity.Computability.Circuit.Boolean.Modular.InnerProduct +public import Complexity.Computability.Circuit.Boolean.Modular.Subtract +import Complexity.Foundations.Data.Nat.Bits +import Mathlib.Data.List.GetD + +/-! +# Selected-row GSW decryption circuits + +The input order is the complete serialized secret followed by the complete serialized ciphertext. +The row selected by the existing total decoder is used on every input, without a key-generation +or noise hypothesis. Arithmetic circuits preserve residues modulo the word modulus. + +## Main definitions + +* `Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.inputWidth`: the complete raw input length. +* `Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.circuit`: the actual total raw-input decryptor. + +## Main results + +* `Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.correct`: agreement with serialized decryption + on every well-sized raw input, including widths zero and one and both half-open decoder ties. +* `Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.depth_circuit_le`: explicit logarithmic depth. +* `Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.size_circuit_le`: explicit polynomial gate count. + +## References + +* [C. Gentry, A. Sahai, B. Waters][GentrySahaiWaters2013], Sections 3.1 and 3.4. +* [C. Gentry][Gentry2009], Definition 4: augmented decryption takes all key and ciphertext bits. +-/ + +public section + +namespace Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit + +open Cslib.Circuits Cslib.Circuits.Boolean Cslib.BitString +open scoped BigOperators + +variable {n w : ℕ} + +/-- Secret bits precede all square-matrix ciphertext bits. -/ +abbrev inputWidth (n w : ℕ) : ℕ := n * w + ((n + 1) * w) * ((n + 1) * w) + +/-- Interpret the raw first block with the same total decoder as the serialized scheme. -/ +private def inputSecret (x : BitString (inputWidth n w)) : Fin n → ZMod (2 ^ w) := + decodeSecret n w (List.ofFn (fstBits x)) + +/-- Interpret every raw ciphertext bit, including ciphertexts outside encryption support. -/ +private def inputCiphertext (x : BitString (inputWidth n w)) : Ciphertext n w := + decodeCiphertext n w (List.ofFn (sndBits x)) + +private theorem inputSecret_apply (x : BitString (inputWidth n w)) (j : Fin n) : + inputSecret x j = ((BitString.equivFin w (block (fstBits x) j) : ℕ) : ZMod (2 ^ w)) := by + simp only [inputSecret, decodeSecret, Cslib.Matrix.ofBinary_apply, + Cslib.Matrix.binaryEntry, Fin.val_zero, zero_mul, zero_add, + listRow_eq_ofFn w j, ofList_ofFn, Nat.foldr_bit_ofFn, BitString.val_equivFin_eq_sum] + +/-- Recompose any row's binary word by the same place values as the circuit word convention. -/ +private theorem rowWord_cast (C : Ciphertext n w) (row : Fin (n + 1) × Fin w) (j : Fin (n + 1)) : + ((BitString.equivFin w (fun l => C row (j, l)) : ℕ) : ZMod (2 ^ w)) = + recomposeMatrix w (bitMatrix (ZMod (2 ^ w)) C) row j := by + simp only [BitString.val_equivFin_eq_sum, Nat.cast_sum, Nat.cast_mul, Nat.cast_pow, + Nat.cast_ofNat, recomposeMatrix, bitCompose, bitMatrix_apply] + +private theorem inputCiphertext_apply (x : BitString (inputWidth n w)) + (i j : Fin (n + 1)) (k l : Fin w) : + inputCiphertext x (i, k) (j, l) = x (Fin.natAdd (n * w) + (finProdFinEquiv (finProdFinEquiv (i, k), finProdFinEquiv (j, l)))) := by + rw [inputCiphertext, decodeCiphertext_apply] + let p := finProdFinEquiv (finProdFinEquiv (i, k), finProdFinEquiv (j, l)) + have hp : (i.val * w + k.val) * ((n + 1) * w) + j.val * w + l.val = p.val := by + simp only [p, finProdFinEquiv, Equiv.coe_fn_mk, Fin.val_mk] + ring + rw [hp, List.getD_eq_getElem _ _ (by simp), List.getElem_ofFn] + rfl + +/-- The selected row is the last binary digit of the leading expanded-secret coordinate. -/ +private def selectedRow (n w : ℕ) (hw : 0 < w) : Fin (n + 1) × Fin w := + (0, ⟨w - 1, by omega⟩) + +/-- Wire one selected-row word directly out of the complete ciphertext input. -/ +private def rowInputs (n w : ℕ) (hw : 0 < w) (j : Fin (n + 1)) : + Fin w → Fin (inputWidth n w) := + fun l => Fin.natAdd (n * w) + (finProdFinEquiv (finProdFinEquiv (selectedRow n w hw), finProdFinEquiv (j, l))) + +private theorem eval_rowInputs (x : BitString (inputWidth n w)) (hw : 0 < w) (j : Fin (n + 1)) : + (Circuit.wiring signature (rowInputs n w hw j)).eval interpretation x = + fun l => inputCiphertext x (selectedRow n w hw) (j, l) := by + funext l + rw [Circuit.eval_wiring] + exact (inputCiphertext_apply x 0 j ⟨w - 1, by omega⟩ l).symm + +/-- Consecutive selected-row words paired with the unexpanded secret, omitting column zero. -/ +private def rowTail (x : BitString (inputWidth n w)) (hw : 0 < w) : BitString (n * w) := + fun i => inputCiphertext x (selectedRow n w hw) + ((finProdFinEquiv.symm i).1.succ, (finProdFinEquiv.symm i).2) + +private theorem block_rowTail (x : BitString (inputWidth n w)) (hw : 0 < w) (j : Fin n) : + block (rowTail x hw) j = fun l => inputCiphertext x (selectedRow n w hw) (j.succ, l) := by + funext l + simp only [rowTail, block, Equiv.symm_apply_apply] + +/-- Feed the complete secret and the non-leading selected-row words to the inner product. -/ +private def productInputs (n w : ℕ) (hw : 0 < w) : Fin (n * w + n * w) → Fin (inputWidth n w) := + Fin.append (m := n * w) (n := n * w) + (Fin.castAdd (((n + 1) * w) * ((n + 1) * w))) + (fun i => rowInputs n w hw (finProdFinEquiv.symm i).1.succ (finProdFinEquiv.symm i).2) + +private theorem append_comp_productInputs (x : BitString (inputWidth n w)) (hw : 0 < w) : + x ∘ productInputs n w hw = Fin.append (fstBits x) (rowTail x hw) := by + funext i + refine Fin.addCases (fun j => ?_) (fun j => ?_) i + · simp only [Function.comp_apply, productInputs, Fin.append_left, fstBits] + · simp only [Function.comp_apply, productInputs, Fin.append_right, rowTail] + exact (inputCiphertext_apply x 0 (finProdFinEquiv.symm j).1.succ + ⟨w - 1, by omega⟩ (finProdFinEquiv.symm j).2).symm + +/-- The actual selected-row modular inner product, reading directly from raw inputs. -/ +private def productSum (n w : ℕ) (hw : 0 < w) : Circuit signature (inputWidth n w) w := + (Modular.innerProduct n w).comp (Circuit.wiring signature (productInputs n w hw)) + +private theorem productSum_cast (x : BitString (inputWidth n w)) (hw : 0 < w) : + ((BitString.equivFin w ((productSum n w hw).eval interpretation x) : ℕ) : ZMod (2 ^ w)) = + ∑ j : Fin n, recomposeMatrix w (bitMatrix (ZMod (2 ^ w)) (inputCiphertext x)) + (selectedRow n w hw) j.succ * inputSecret x j := by + rw [productSum, Circuit.eval_comp, Circuit.eval_wiring, append_comp_productInputs, + Modular.val_eval_innerProduct, ZMod.natCast_mod, Nat.cast_sum] + apply Finset.sum_congr rfl + intro j _ + rw [Nat.cast_mul, ← inputSecret_apply, block_rowTail, rowWord_cast, mul_comm] + +/-- Subtract the selected row's inner product from its leading word, modulo `2 ^ w`. -/ +private def phase (n w : ℕ) (hw : 0 < w) : Circuit signature (inputWidth n w) w := + (Modular.subtract w).comp + ((Circuit.wiring signature (rowInputs n w hw 0)).append (productSum n w hw)) + +/-- The raw circuit phase is exactly the original selected-row residue on every input. -/ +private theorem phase_cast (x : BitString (inputWidth n w)) (hw : 0 < w) : + ((BitString.equivFin w ((phase n w hw).eval interpretation x) : ℕ) : ZMod (2 ^ w)) = + decryptionPhase (inputSecret x) (inputCiphertext x) (selectedRow n w hw) := by + let a := (Circuit.wiring signature (rowInputs n w hw 0)).eval interpretation x + let b := (productSum n w hw).eval interpretation x + have ha : ((BitString.equivFin w a : ℕ) : ZMod (2 ^ w)) = + recomposeMatrix w (bitMatrix (ZMod (2 ^ w)) (inputCiphertext x)) (selectedRow n w hw) 0 := by + dsimp only [a] + rw [eval_rowInputs] + exact rowWord_cast _ _ _ + have hb := productSum_cast x hw + change ((BitString.equivFin w b : ℕ) : ZMod (2 ^ w)) = _ at hb + have hv : (BitString.equivFin w ((phase n w hw).eval interpretation x) : ℕ) = + (2 ^ w - (BitString.equivFin w b : ℕ) + (BitString.equivFin w a : ℕ)) % 2 ^ w := by + simpa only [phase, Circuit.eval_comp, Circuit.eval_append] using Modular.val_eval_subtract a b + rw [hv, ZMod.natCast_mod, Nat.cast_add, + Nat.cast_sub (Nat.le_of_lt (BitString.equivFin w b).isLt), ZMod.natCast_self] + simp only [ha, hb, decryptionPhase, sub_eq_add_neg, add_comm, zero_add] + +private theorem testBit_wordValue (x : BitString w) (i : Fin w) : + (BitString.equivFin w x : ℕ).testBit i.val = x i := by + simpa only [BitVec.getLsbD, toNat_word_eq_equivFin] using getLsbD_word x i + +/-- Implement the actual width-zero, width-one and top-two-bit decoder cases. -/ +private def decodeWord (w : ℕ) : Circuit signature w 1 := + if h₀ : w = 0 then Circuit.oneGate (.const false) Fin.elim0 + else if h₁ : w = 1 then Circuit.wiring signature (fun _ => ⟨0, by omega⟩) + else ((Formula.input ⟨w - 1, by omega⟩).xor (.input ⟨w - 2, by omega⟩)).toCircuit + +/-- The scalar decoder is computed on every modular word, including both quarter ties. -/ +private theorem eval_decodeWord (x : BitString w) : + (decodeWord w).eval interpretation x 0 = + decode w ((BitString.equivFin w x : ℕ) : ZMod (2 ^ w)) := by + have hv : (((BitString.equivFin w x : ℕ) : ZMod (2 ^ w)).val) = + (BitString.equivFin w x : ℕ) := by + rw [ZMod.val_natCast, Nat.mod_eq_of_lt (BitString.equivFin w x).isLt] + by_cases h₀ : w = 0 + · subst w + simp [decodeWord, interpretation] + · by_cases h₁ : w = 1 + · subst w + simp only [decodeWord, Nat.one_ne_zero, ↓reduceDIte, Circuit.eval_wiring, + Function.comp_apply, decode_one, hv] + exact (testBit_wordValue x 0).symm + · have hw : 2 ≤ w := by omega + rw [decode_eq_xor_highBits hw, hv] + simp only [decodeWord, h₀, h₁, ↓reduceDIte, Formula.eval_toCircuit, + Formula.eval_xor, Formula.eval_input] + rw [testBit_wordValue x ⟨w - 1, by omega⟩, + testBit_wordValue x ⟨w - 2, by omega⟩] + +private theorem depth_decodeWord_le (w : ℕ) : (decodeWord w).depth ≤ 3 := by + unfold decodeWord + split_ifs + · simp + · simp + · exact (Formula.depth_toCircuit_le _).trans + ((Formula.depth_xor_le _ _).trans (by simp)) + +private theorem size_decodeWord_le (w : ℕ) : (decodeWord w).size ≤ 5 := by + unfold decodeWord + split_ifs <;> simp + +/-- The actual total GSW decryptor, with all raw secret and ciphertext bits as inputs. -/ +def circuit (n w : ℕ) : Circuit signature (inputWidth n w) 1 := + if hw : 0 < w then (decodeWord w).comp (phase n w hw) + else Circuit.oneGate (.const false) Fin.elim0 + +/-- All raw inputs agree with typed GSW decryption, without generation or noise hypotheses. -/ +private theorem eval_circuit (x : BitString (inputWidth n w)) : + (circuit n w).eval interpretation x 0 = decrypt (inputSecret x) (inputCiphertext x) := by + by_cases hw : 0 < w + · rw [circuit, dite_eq_left hw, Circuit.eval_comp, eval_decodeWord, phase_cast x hw, + decrypt_eq_decode_decryptionPhase hw] + rfl + · have hz : w = 0 := by omega + subst w + simp [circuit, interpretation] + +/-- The selected-row construction has logarithmic depth in both parameter dimensions. -/ +theorem depth_circuit_le (n w : ℕ) : + (circuit n w).depth ≤ 28 + 18 * Nat.clog 2 (w + 1) + 12 * Nat.clog 2 n := by + have hp : ∀ hw, (productSum n w hw).depth ≤ + 17 + 16 * Nat.clog 2 (w + 1) + 12 * Nat.clog 2 n := by + intro hw + exact (Circuit.depth_comp_le _ _).trans (by + simpa only [Circuit.depth_wiring, add_zero] using Modular.depth_innerProduct_le n w) + have hphase : ∀ hw, (phase n w hw).depth ≤ + 25 + 18 * Nat.clog 2 (w + 1) + 12 * Nat.clog 2 n := by + intro hw + have ha := Circuit.depth_append_le + (Circuit.wiring signature (rowInputs n w hw 0)) (productSum n w hw) + simp only [Circuit.depth_wiring, zero_max] at ha + have hc := Circuit.depth_comp_le (Modular.subtract w) + ((Circuit.wiring signature (rowInputs n w hw 0)).append (productSum n w hw)) + have hs := Modular.depth_subtract_le w + have hi := hp hw + change (phase n w hw).depth ≤ _ at hc + omega + unfold circuit + split_ifs with hw + · have hc := Circuit.depth_comp_le (decodeWord w) (phase n w hw) + have hd := depth_decodeWord_le w + have hp := hphase hw + omega + · simp only [Circuit.depth_oneGate] + omega + +/-- Polynomial gate count includes all unused fallback gates in the balanced construction. -/ +theorem size_circuit_le (n w : ℕ) : + (circuit n w).size ≤ 131 * (n + 1) * (w + 1) ^ 2 := by + unfold circuit + split_ifs with hw + · simp only [Circuit.size_comp, phase, productSum, Circuit.size_append, + Circuit.size_wiring, zero_add] + have hd := size_decodeWord_le w + have hs := Modular.size_subtract_le w + have hi := Modular.size_innerProduct_le n w + nlinarith [Nat.zero_le n, Nat.zero_le (n * w), Nat.zero_le (n * w ^ 2)] + · simp only [Circuit.size_oneGate] + nlinarith [Nat.zero_le n, Nat.zero_le (n * w), Nat.zero_le (n * w ^ 2)] + +/-- The serialized contract required by generic refresh: every well-sized raw pair is covered. -/ +theorem correct (n w : ℕ) (secret ciphertext : List Bool) + (hs : secret.length = n * w) + (hc : ciphertext.length = ((n + 1) * w) * ((n + 1) * w)) : + (circuit n w).eval interpretation (ofList (inputWidth n w) (secret ++ ciphertext)) 0 = + decryptSerialized n w secret ciphertext := by + change (circuit n w).eval interpretation + (ofList (n * w + ((n + 1) * w) * ((n + 1) * w)) (secret ++ ciphertext)) 0 = _ + rw [ofList_append hs hc, eval_circuit, decryptSerialized_eq] + simp only [inputSecret, inputCiphertext, fstBits_append, sndBits_append, + ofFn_ofList hs, ofFn_ofList hc] + +end Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/DecryptionCircuit/Parameters.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/DecryptionCircuit/Parameters.lean new file mode 100644 index 000000000..fc606feb5 --- /dev/null +++ b/Complexity/Crypto/Computational/Homomorphic/GSW/DecryptionCircuit/Parameters.lean @@ -0,0 +1,82 @@ +/- +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.Crypto.Computational.Homomorphic.GSW.DecryptionCircuit +public import Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters +public import Complexity.Crypto.Computational.Homomorphic.Circuit +public import Complexity.Computability.Circuit.Boolean.Layered.Compile + +/-! +# Concrete depth fit for GSW decryption + +The complete raw-input decryptor and its two-copy NAND augmentation compile to fewer layers than +`DepthParameters.depthBudget`, for every security parameter. This is an arithmetic budget result; +it does not assume or establish LWE hardness or circular security. + +## Main results + +* `Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.layers_augment_le_depthBudget`: the actual + augmented circuit's layer count fits the existing GSW parameter family. +-/ + +public section + +namespace Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit + +open Circuits Circuits.Boolean + +private theorem clog_width_le (security : ℕ) : + Nat.clog 2 (DepthParameters.width security + 1) ≤ + 15 + 2 * DepthParameters.logSize security := by + let t := DepthParameters.logSize security + have ht : t ≤ 2 ^ t := Nat.le_of_lt Nat.lt_two_pow_self + have hs : t ^ 2 ≤ (2 ^ t) ^ 2 := Nat.pow_le_pow_left ht 2 + apply Nat.clog_le_of_le_pow + change 16384 * t ^ 2 + 1 ≤ 2 ^ (15 + 2 * t) + have he : 2 ^ (15 + 2 * t) = 32768 * (2 ^ t) ^ 2 := by + rw [pow_add, mul_comm 2 t, pow_mul] + norm_num + rw [he] + have hp : 0 < (2 ^ t) ^ 2 := by positivity + omega + +/-- The NAND extension adds at most two De Morgan levels to the complete raw decryptor. -/ +theorem depth_augment_le (n w : ℕ) : + (augmentNand (circuit n w)).depth ≤ + 30 + 18 * Nat.clog 2 (w + 1) + 12 * Nat.clog 2 n := by + have hn : nandCircuit.depth ≤ 2 := by decide + have hp : ((circuit n w).parallel (circuit n w)).depth ≤ (circuit n w).depth := by + unfold Circuit.parallel + apply (Circuit.depth_append_le _ _).trans + apply max_le <;> exact (Circuit.depth_comp_le _ _).trans (by simp) + have hc := Circuit.depth_comp_le nandCircuit ((circuit n w).parallel (circuit n w)) + have hd := depth_circuit_le n w + change (augmentNand (circuit n w)).depth ≤ _ at hc + omega + +/-- Two microlevels per De Morgan level, including the actual NAND augmentation, fit the budget. -/ +theorem layers_augment_le_depthBudget (security : ℕ) : + (Layered.compile + (inputWidth (Parameters.dimension security) (DepthParameters.width security) + + inputWidth (Parameters.dimension security) (DepthParameters.width security)) + (augmentNand + (circuit (Parameters.dimension security) (DepthParameters.width security))).code).1.length ≤ + DepthParameters.depthBudget security := by + rw [Layered.length_compile] + have hd := depth_augment_le (Parameters.dimension security) (DepthParameters.width security) + have hw := clog_width_le security + have hn : Nat.clog 2 (Parameters.dimension security) ≤ DepthParameters.logSize security := by + have hm := Nat.clog_mono_right (b := 2) (show security + 1 ≤ security + 2 by omega) + unfold Parameters.dimension DepthParameters.logSize + omega + have ht := DepthParameters.two_le_logSize security + unfold DepthParameters.depthBudget + omega + +end Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/DecryptionCircuit/PolyTime.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/DecryptionCircuit/PolyTime.lean new file mode 100644 index 000000000..6d8e16b10 --- /dev/null +++ b/Complexity/Crypto/Computational/Homomorphic/GSW/DecryptionCircuit/PolyTime.lean @@ -0,0 +1,253 @@ +/- +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.Crypto.Computational.Homomorphic.GSW.DecryptionCircuit +import all Complexity.Crypto.Computational.Homomorphic.GSW.DecryptionCircuit +public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain +public import Complexity.Computability.Circuit.Boolean.Modular.InnerProduct.PolyTime +public import Complexity.Computability.Circuit.Boolean.Modular.Subtract.PolyTime +public import Complexity.Computability.Circuit.Boolean.Layered.Compile.PolyTime +public import Complexity.Crypto.Computational.Homomorphic.Circuit.PolyTime +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 complete GSW decryption circuits + +Unary dimension and word width generate the full code of the actual raw-input decryptor, without +an assumed generator or runtime certificate. All matrix selectors and arithmetic circuits are +charged, even on inputs outside key-generation or encryption support. + +## Main results + +* `Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.code_eq_code`: exact generated code. +* `Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.computableInPolyTime_code`: public generator. +-/ + +public section + +namespace Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit + +open Circuits Circuits.Boolean +open Turing.MultiTapeTM ComputableTidilyInPolyTime + +local notation "Code" => List (Op × List ℕ) × List ℕ + +private def rowCode (n w : ℕ) : Code := + ([], (List.range w).map fun i => n * w + (w - 1) * ((n + 1) * w) + i) + +private theorem rowCode_eq (n w : ℕ) (hw : 0 < w) : + rowCode n w = (Circuit.wiring signature (rowInputs n w hw 0)).code := by + apply Prod.ext + · rfl + · apply List.ext_getElem (by simp [rowCode, Circuit.code, Circuit.wiring]) + intro i hi hi' + simp [rowCode, Circuit.code, Circuit.wiring, rowInputs, selectedRow, + finProdFinEquiv, Nat.mul_comm, Nat.add_comm, Nat.add_left_comm] + +private def productInputsCode (n w : ℕ) : Code := + ([], List.range (n * w) ++ (List.range (n * w)).map + (fun i => n * w + (w - 1) * ((n + 1) * w) + (w + i))) + +private theorem tail_val (n w : ℕ) (hw : 0 < w) (i : Fin (n * w)) : + (rowInputs n w hw (finProdFinEquiv.symm i).1.succ + (finProdFinEquiv.symm i).2).val = + n * w + (w - 1) * ((n + 1) * w) + (w + i.val) := by + have he := congrArg Fin.val (finProdFinEquiv.apply_symm_apply i) + simp only [finProdFinEquiv, Equiv.coe_fn_mk, Fin.val_mk] at he + simp only [rowInputs, selectedRow, Fin.val_natAdd, finProdFinEquiv, Equiv.coe_fn_mk, + Fin.val_zero, Fin.val_succ] + nlinarith [he] + +private theorem productInputsCode_eq (n w : ℕ) (hw : 0 < w) : + productInputsCode n w = (Circuit.wiring signature (productInputs n w hw)).code := by + apply Prod.ext + · rfl + change _ = List.ofFn (fun i => (productInputs n w hw i).val) + rw [List.ofFn_add] + have hl : (fun i : Fin (n * w) => + (productInputs n w hw (Fin.castAdd (n * w) i)).val) = (fun i => i.val) := by + funext i + simp only [productInputs, Fin.append_left, Fin.val_castAdd] + have hr : (fun i : Fin (n * w) => + (productInputs n w hw (Fin.natAdd (n * w) i)).val) = + (fun i => n * w + (w - 1) * ((n + 1) * w) + (w + i.val)) := by + funext i + simp only [productInputs, Fin.append_right] + exact tail_val n w hw i + change _ ++ _ = List.ofFn (fun i : Fin (n * w) => + (productInputs n w hw (Fin.castAdd (n * w) i)).val) ++ _ + rw [hl, hr] + congr 1 <;> apply List.ext_getElem (by simp) <;> intro i hi hi' <;> simp + +private def decoderCode (w : ℕ) : Code := + if w = 0 then ([(.const false, [])], [w]) + else if w = 1 then ([], [0]) + else formulaCode w ((Formula.input (n := 2) 0).xor (.input 1)) ![w - 1, w - 2] + +private theorem decoderCode_eq (w : ℕ) : decoderCode w = (decodeWord w).code := by + by_cases h₀ : w = 0 + · subst w + rfl + · by_cases h₁ : w = 1 + · subst w + rfl + · let wires : Fin 2 → Fin w := ![⟨w - 1, by omega⟩, ⟨w - 2, by omega⟩] + have he : (fun i => (wires i).val) = ![w - 1, w - 2] := by + funext i + fin_cases i <;> rfl + have ht := formulaCode_eq_code ((Formula.input (n := 2) 0).xor (.input 1)) wires + rw [he] at ht + have hf : (((Formula.input (n := 2) 0).xor (.input 1)).rename wires) = + (Formula.input ⟨w - 1, by omega⟩).xor (.input ⟨w - 2, by omega⟩) := by + simp only [Formula.rename, Formula.xor, Formula.and, Formula.or, Formula.not, + Formula.gate_bind] + congr 1 + funext i + fin_cases i <;> simp only [Matrix.cons_val_zero', Matrix.cons_val_succ', + Formula.gate_bind] + all_goals + congr 1 + funext j + fin_cases j <;> simp only [Matrix.cons_val_zero', Matrix.cons_val_succ', + Formula.gate_bind, Formula.input_bind, wires] + all_goals congr 1 + all_goals + funext k + fin_cases k + simp only [Matrix.cons_val_zero', Formula.input_bind, Matrix.cons_val_zero, + Matrix.cons_val_one] + rw [hf] at ht + simpa only [decoderCode, decodeWord, h₀, h₁, ↓reduceIte, ↓reduceDIte] using ht + +/-- Generate the full selected-row GSW decryptor, including width-zero fallback behavior. -/ +def code (n w : ℕ) : Code := + private_decl% (if w = 0 then ([(.const false, [])], [inputWidth n w]) + else compCode (inputWidth n w) (decoderCode w) + (compCode (inputWidth n w) (Modular.subtractCode w) + (appendCode (inputWidth n w) (rowCode n w) + (compCode (inputWidth n w) (Modular.innerProductCode n w) + (productInputsCode n w))))) + +/-- The native constructor returns every gate and designated output of the actual circuit. -/ +theorem code_eq_code (n w : ℕ) : code n w = (circuit n w).code := by + by_cases hw : 0 < w + · change (if w = 0 then _ else _) = _ + rw [ite_eq_right (by omega : w ≠ 0), decoderCode_eq, Modular.subtractCode_eq_code, + rowCode_eq n w hw, Modular.innerProductCode_eq_code, productInputsCode_eq n w hw, + compCode_code, appendCode_code, compCode_code, compCode_code] + rw [circuit, dite_eq_left hw] + rfl + · have hz : w = 0 := by omega + subst w + rfl + +private theorem native_rowCode : + ComputableTidilyInPolyTime (fun p : ℕ × ℕ => rowCode p.1 p.2) + (encPair encUnary encUnary) encCode := by + have hwire : ComputableTidilyInPolyTime (fun p : (ℕ × ℕ) × ℕ => + p.1.1 * p.1.2 + (p.1.2 - 1) * ((p.1.1 + 1) * p.1.2) + p.2) + (encPair (encPair encUnary encUnary) encUnary) encNat := by fun_prop + exact (const (encMid := encList encGate) []).prod + (mapWith hwire id' (range.comp (snd _ _))) + +private theorem native_productInputsCode : + ComputableTidilyInPolyTime (fun p : ℕ × ℕ => productInputsCode p.1 p.2) + (encPair encUnary encUnary) encCode := by + have hlen : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => p.1 * p.2) + (encPair encUnary encUnary) encUnary := by fun_prop + have hwire : ComputableTidilyInPolyTime (fun p : (ℕ × ℕ) × ℕ => + p.1.1 * p.1.2 + (p.1.2 - 1) * ((p.1.1 + 1) * p.1.2) + (p.1.2 + p.2)) + (encPair (encPair encUnary encUnary) encUnary) encNat := by fun_prop + have hr : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => List.range (p.1 * p.2)) + (encPair encUnary encUnary) (encList encNat) := by + simpa only [Function.comp_def, List.map_id_fun', id_eq] using + unary_to_binary.map.comp (range.comp hlen) + exact (const (encMid := encList encGate) []).prod + (listAppend' hr (mapWith hwire id' (range.comp hlen))) + +private theorem native_decoderCode : + ComputableTidilyInPolyTime decoderCode encUnary encCode := by + have hw : ComputableTidilyInPolyTime (fun w : ℕ => w) encUnary encNat := unary_to_binary + have ht : ComputableTidilyInPolyTime (fun w : ℕ => + formulaCode w ((Formula.input (n := 2) 0).xor (.input 1)) ![w - 1, w - 2]) + encUnary encCode := by + apply computableTidilyInPolyTime_formulaCode _ hw + intro i + fin_cases i + · change ComputableTidilyInPolyTime (fun w : ℕ => w - 1) _ encNat + fun_prop + · change ComputableTidilyInPolyTime (fun w : ℕ => w - 2) _ encNat + fun_prop + unfold decoderCode + fun_prop + +private theorem native_code : + ComputableTidilyInPolyTime (fun p : ℕ × ℕ => code p.1 p.2) + (encPair encUnary encUnary) encCode := by + have hn : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => inputWidth p.1 p.2) + (encPair encUnary encUnary) encNat := by fun_prop + have hi : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => Modular.innerProductCode p.1 p.2) + (encPair encUnary encUnary) encCode := by + simpa only [Modular.innerProductCode_eq_code] using + Modular.computableInPolyTime_innerProduct.tidy + have hs : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => Modular.subtractCode p.2) + (encPair encUnary encUnary) encCode := by + simpa only [Modular.subtractCode_eq_code, Function.comp_def] using + Modular.computableInPolyTime_subtract.tidy.comp (snd _ _) + have hd := native_decoderCode.comp (snd encUnary encUnary) + have hbody := computableTidilyInPolyTime_compCode hn hd + (computableTidilyInPolyTime_compCode hn hs + (computableTidilyInPolyTime_appendCode hn native_rowCode + (computableTidilyInPolyTime_compCode hn hi native_productInputsCode))) + change ComputableTidilyInPolyTime (fun p : ℕ × ℕ => + if p.2 = 0 then ([(Op.const false, [])], [inputWidth p.1 p.2]) + else compCode (inputWidth p.1 p.2) (decoderCode p.2) + (compCode (inputWidth p.1 p.2) (Modular.subtractCode p.2) + (appendCode (inputWidth p.1 p.2) (rowCode p.1 p.2) + (compCode (inputWidth p.1 p.2) (Modular.innerProductCode p.1 p.2) + (productInputsCode p.1 p.2))))) _ _ + fun_prop + +/-- One native polynomial-time algorithm generates the full decryptor from unary parameters. -/ +theorem computableInPolyTime_code : + ComputableInPolyTime (fun p : ℕ × ℕ => code p.1 p.2) + (encPair encUnary encUnary) encCode := native_code.computableInPolyTime + +private theorem native_circuit : + ComputableTidilyInPolyTime (fun p : ℕ × ℕ => + (⟨inputWidth p.1 p.2, circuit p.1 p.2⟩ : Σ m, Circuit signature m 1)) + (encPair encUnary encUnary) (encCircuit 1) := by + have hn : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => inputWidth p.1 p.2) + (encPair encUnary encUnary) encUnary := by fun_prop + exact (hn.prod native_code).of_enc_eq (fun p => by + simp only [encCircuit_apply, code_eq_code]) + +/-- Generate the actual circuit together with its unary input arity in native polynomial time. -/ +theorem computableInPolyTime_circuit : + ComputableInPolyTime (fun p : ℕ × ℕ => + (⟨inputWidth p.1 p.2, circuit p.1 p.2⟩ : Σ m, Circuit signature m 1)) + (encPair encUnary encUnary) (encCircuit 1) := native_circuit.computableInPolyTime + +/-- Generate the complete layered NAND augmentation, including its schedule and selectors. -/ +theorem computableInPolyTime_layeredAugment : + ComputableInPolyTime (fun p : ℕ × ℕ => + Layered.compile (inputWidth p.1 p.2 + inputWidth p.1 p.2) + (augmentNand (circuit p.1 p.2)).code) + (encPair encUnary encUnary) Layered.encCompiled := by + have ha := computableTidilyInPolyTime_augmentNand.comp native_circuit + have hview : ComputableTidilyInPolyTime + (fun D : Σ m, Circuit signature m 1 => (D.1, D.2.code)) + (encCircuit 1) (encPair encUnary encCode) := .of_eq fun _ => rfl + have hv := hview.comp ha + exact (Layered.computableTidilyInPolyTime_compile hv.fst' hv.snd').computableInPolyTime + +end Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit diff --git a/ComplexityTests.lean b/ComplexityTests.lean index 7b0cee993..4d4768a52 100644 --- a/ComplexityTests.lean +++ b/ComplexityTests.lean @@ -89,6 +89,7 @@ import ComplexityTests.Crypto.FixedKeySecurity import ComplexityTests.Crypto.GMWPointwise import ComplexityTests.Crypto.GSW import ComplexityTests.Crypto.GSWDecryption +import ComplexityTests.Crypto.GSWDecryptionCircuit import ComplexityTests.Crypto.GSWDepthParameters import ComplexityTests.Crypto.GSWEvaluation import ComplexityTests.Crypto.GSWHiding diff --git a/ComplexityTests/Crypto/GSWDecryptionCircuit.lean b/ComplexityTests/Crypto/GSWDecryptionCircuit.lean new file mode 100644 index 000000000..2c42144e0 --- /dev/null +++ b/ComplexityTests/Crypto/GSWDecryptionCircuit.lean @@ -0,0 +1,156 @@ +/- +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.Crypto.Computational.Homomorphic.GSW.DecryptionCircuit.Parameters +import Complexity.Crypto.Computational.Homomorphic.GSW.DecryptionCircuit.PolyTime +import Complexity.Computability.Circuit.Boolean.Layered.Compile.Correctness +import Complexity.Computability.Circuit.Boolean.Layered.Compile.Size + +/-! Total raw-input decryption, decoder ties, modular wraparound and uniform native generators. -/ + +namespace ComplexityTests.Crypto.GSWDecryptionCircuit + +open Cslib Cslib.Circuits Cslib.Circuits.Boolean Cslib.Crypto.Homomorphic +open Cslib.Crypto.Homomorphic.GSW +open Turing.MultiTapeTM + +-- A shifted partial product can be prepared for the carry-save reducer through plain APIs. +example : ComputableInPolyTime (fun p : ℕ × ℕ => + pairWithZeroCode (p.1 + p.1) p.1 (Modular.partialProductCode p.1 p.2)) + (encPair encUnary encUnary) encCode := + computableInPolyTime_pairWithZeroCode (by fun_prop) (by fun_prop) + Modular.computableInPolyTime_partialProductCode + +-- The reducer charges a runtime-supplied complete leaf list and a binary input arity. +example : ComputableInPolyTime + (fun p : (ℕ × ℕ) × List (List (Op × List ℕ) × List ℕ) => + sumPairsCode p.1.1 p.1.2 p.2) + (encPair (encPair encNat encUnary) (encList encCode)) encCode := + computableInPolyTime_sumPairsCode + ((ComputableInPolyTime.fst encNat encUnary).comp + (ComputableInPolyTime.fst _ _)) + ((ComputableInPolyTime.snd encNat encUnary).comp + (ComputableInPolyTime.fst _ _)) + (ComputableInPolyTime.snd _ _) + +private def secret : List Bool := [true, false] +-- Selected row is row 1. Its words are 3 and 2; secret 1 gives phase 1 (the lower tie). +private def lowerTie : List Bool := + [false, false, false, false, true, true, false, true, + false, false, false, false, false, false, false, false] +-- Words 1 and 2 give phase -1 = 3 modulo 4 (the excluded upper tie). +private def upperTie : List Bool := + [false, false, false, false, true, false, false, true, + false, false, false, false, false, false, false, false] + +example : (DecryptionCircuit.circuit 1 2).eval interpretation + (BitString.ofList 18 (secret ++ lowerTie)) 0 = true := by + rw [DecryptionCircuit.correct 1 2 secret lowerTie rfl rfl] + decide + +example : (DecryptionCircuit.circuit 1 2).eval interpretation + (BitString.ofList 18 (secret ++ upperTie)) 0 = false := by + rw [DecryptionCircuit.correct 1 2 secret upperTie rfl rfl] + decide + +-- Width one uses the sole phase bit, and zero width has the actual total false semantics. +example : (DecryptionCircuit.circuit 1 1).eval interpretation + (BitString.ofList 5 ([false] ++ [true, true, false, false])) 0 = true := by + rw [DecryptionCircuit.correct 1 1 [false] [true, true, false, false] rfl rfl] + decide + +example : (DecryptionCircuit.circuit 4 0).eval interpretation (BitString.ofList 0 []) 0 = + false := by + rw [show ([] : List Bool) = [] ++ [] from rfl, + DecryptionCircuit.correct 4 0 [] [] rfl rfl] + decide + +example : (BitString.equivFin 2 ((Modular.multiply 2).eval interpretation + (Fin.append ![true, true] ![true, true])) : ℕ) = 1 := by + rw [Modular.val_eval_multiply] + decide + +example : (BitString.equivFin 2 ((Modular.subtract 2).eval interpretation + (Fin.append ![true, false] ![false, true])) : ℕ) = 3 := by + rw [Modular.val_eval_subtract] + decide + +-- Empty and zero-width arrays are included in the same arithmetic theorem. +example : (BitString.equivFin 3 ((Modular.innerProduct 0 3).eval interpretation + (Fin.append Fin.elim0 Fin.elim0)) : ℕ) = 0 := by + rw [Modular.val_eval_innerProduct] + simp + +example : ComputableInPolyTime (fun p : ℕ × ℕ => DecryptionCircuit.code p.1 p.2) + (encPair encUnary encUnary) encCode := DecryptionCircuit.computableInPolyTime_code + +example : ComputableInPolyTime (fun security => + DecryptionCircuit.code (Parameters.dimension security) (DepthParameters.width security)) + encUnary encCode := + (DecryptionCircuit.computableInPolyTime_code.tidy.comp + (Parameters.computableTidilyInPolyTime_dimension.prod + DepthParameters.computableTidilyInPolyTime_width)).computableInPolyTime + +example : DecryptionCircuit.code 1 2 = (DecryptionCircuit.circuit 1 2).code := + DecryptionCircuit.code_eq_code 1 2 + +example : ∀ security, (Layered.compile + (DecryptionCircuit.inputWidth (Parameters.dimension security) (DepthParameters.width security) + + DecryptionCircuit.inputWidth (Parameters.dimension security) (DepthParameters.width security)) + (augmentNand (DecryptionCircuit.circuit (Parameters.dimension security) + (DepthParameters.width security))).code).1.length ≤ DepthParameters.depthBudget security := + DecryptionCircuit.layers_augment_le_depthBudget + +example : Layered.select (Layered.eval (secret ++ lowerTie) + (Layered.compile 18 (DecryptionCircuit.circuit 1 2).code).1) + (Layered.compile 18 (DecryptionCircuit.circuit 1 2).code).2 = [true] := by + have h := Layered.select_eval_compile (DecryptionCircuit.circuit 1 2) + (BitString.ofList 18 (secret ++ lowerTie)) + have hv : (DecryptionCircuit.circuit 1 2).eval interpretation + (BitString.ofList 18 (secret ++ lowerTie)) 0 = true := by + rw [DecryptionCircuit.correct 1 2 secret lowerTie rfl rfl] + decide + have he : List.ofFn (BitString.ofList (DecryptionCircuit.inputWidth 1 2) + (secret ++ lowerTie)) = secret ++ lowerTie := BitString.ofFn_ofList rfl + rw [he] at h + simpa only [List.ofFn_succ, List.ofFn_zero, List.map_nil, List.cons_append, + List.nil_append, hv] using h + +-- The compiler's full encoded-size bound applies to the actual augmented circuit, not a +-- supplied bound field. Its depth and gate count have the independent explicit bounds above. +example (n w : ℕ) : + let D := augmentNand (DecryptionCircuit.circuit n w) + let width := DecryptionCircuit.inputWidth n w + DecryptionCircuit.inputWidth n w + 3 * D.size + let bits := Nat.log2 width + 1 + (Layered.encCompiled (Layered.compile + (DecryptionCircuit.inputWidth n w + DecryptionCircuit.inputWidth n w) D.code)).length ≤ + 4 * D.depth * (2 * width * (6 * bits + 21) + 1) + (2 * bits + 1) + 1 := + by simpa only [one_mul] using + Layered.length_encCompiled_compile_le (augmentNand (DecryptionCircuit.circuit n w)) + +/-- info: 'Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.correct' depends on axioms: +[propext, Classical.choice, Quot.sound] -/ +#guard_msgs in +#print axioms DecryptionCircuit.correct + +/-- info: 'Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.computableInPolyTime_code' depends on axioms: [propext, + Classical.choice, + Quot.sound] -/ +#guard_msgs in +#print axioms DecryptionCircuit.computableInPolyTime_code + +/-- info: 'Cslib.Circuits.Boolean.Modular.computableInPolyTime_innerProduct' depends on axioms: +[propext, Classical.choice, Quot.sound] -/ +#guard_msgs (whitespace := lax) in +#print axioms Modular.computableInPolyTime_innerProduct + +/-- info: 'Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.layers_augment_le_depthBudget' depends on axioms: [propext, + Classical.choice, + Quot.sound] -/ +#guard_msgs in +#print axioms DecryptionCircuit.layers_augment_le_depthBudget + +end ComplexityTests.Crypto.GSWDecryptionCircuit diff --git a/ROADMAP.md b/ROADMAP.md index ea11743cc..c53e52e53 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -268,16 +268,24 @@ existing developments, source credit and saved branches remain available for a f unary parameter routines. Only the modulus is returned in binary. Its [security corollary](Complexity/Crypto/Computational/Homomorphic/GSW/DepthParameters/Security.lean) assumes decision LWE for this exact new family; the earlier family's hardness premise is - insufficient. The actual augmented-decryption circuit still has to be constructed and proved - to fit `L`; this arithmetic result does not establish bootstrappability. - Full native circuit evaluation, shallow decryption circuits, bootstrappability with compatible - parameters and the concrete FHE instantiation remain open in #486. The earlier parameter family + insufficient. The [actual selected-row decryptor](Complexity/Crypto/Computational/Homomorphic/GSW/DecryptionCircuit.lean) + computes total serialized decryption on every well-sized raw secret/ciphertext pair, including + widths zero and one. Its depth is at most `28 + 18*clog₂(w+1) + 12*clog₂(n)` and its gate + count at most `131*(n+1)*(w+1)²`. The [native generator](Complexity/Crypto/Computational/Homomorphic/GSW/DecryptionCircuit/PolyTime.lean) + charges all arithmetic, indexing, wiring and complete layered NAND augmentation. + The [parameter fit](Complexity/Crypto/Computational/Homomorphic/GSW/DecryptionCircuit/Parameters.lean) + proves that the actual augmented circuit, with two NAND microlevels per De Morgan level, + fits `L` at every security parameter. [Checked clients](ComplexityTests/Crypto/GSWDecryptionCircuit.lean) + include both decoder ties, negative wraparound, boundary widths and a uniform family generator. + These circuit results do not establish bootstrappability or transfer a hardness premise. + Full native circuit evaluation, bootstrappability with compatible parameters and the concrete + FHE instantiation remain open in #486. The earlier parameter family proves fresh and one-NAND correctness; it does not yet supply the augmented-decryption circuit or the separate joint circular-security assumption needed for the fixed-key endpoint. The [code-composition API](Complexity/Computability/Circuit/Boolean/CodeComposition.lean) provides a native polynomial-time constructor for shared-input blocks with different gate counts, checked against the existing carry-save circuit without padding. This supports the - shallow-decryption generator in #528; that full circuit and its certificate remain open. + complete shallow-decryption generator in #528. [Native carry-save generators](Complexity/Computability/Circuit/Boolean/CarrySave/PolyTime.lean) construct the exact existing three-to-two and four-to-two reducers from unary width, including all binary references and the unequal carry-bit blocks. @@ -285,8 +293,7 @@ existing developments, source credit and saved branches remain available for a f constructs the exact existing half-split tree from the complete native leaf-code list, binary input arity and native operator/fallback codes. Its polynomial certificate charges all interval-table rows and wire encodings, including dead gates and malformed raw data. - This completes the balanced-construction prerequisite #543; the actual shallow-decryption - circuit, its native generator and parameter fit remain the separate #528 objective. + This completes the balanced-construction prerequisite #543 used by the complete #528 decryptor. 4. **Completeness of oblivious transfer.** In the ideal oblivious-transfer hybrid model, every polynomial-time multiparty functionality admits a protocol secure against static malicious corruptions, with security defined by real/ideal simulation and allowing abort, under the @@ -869,7 +876,8 @@ batches. 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. + these arithmetic circuits. The complete GSW shallow-decryption circuit and native constructor + are described above; stronger logspace and DLOGTIME uniformity 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