feat(crypto): uniform decryption circuit generator for leveled FHE (#1104)

Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean

@@ -26,12 +26,12 @@ The security premise is decision LWE for exactly this family: secret dimension `
 centered-binomial noise of width `λ + 1`, and the quasi-polynomial modulus `2 ^ (16384 * t ^ 2)`
 with `t = 1 + ⌈log₂ (λ + 2)⌉`.
 
-* **Leveled FHE.** One polynomial-size decryption circuit family, one natively computable
-  decryption algorithm and fixed polynomial widths are chosen first. Then every polynomially
-  bounded depth family is covered by an actual scheme with that decryption algorithm, assuming
-  only decision LWE [Gentry2009, Definition 3 and Theorem 3]. Security is asymptotic IND-CPA, a
-  consequence of [Gentry2009, Theorem 4] without its exact loss. Native certificates are uniform
-  for each depth family; key generation reads only the unary security parameter.
+* **Leveled FHE.** One uniformly generated polynomial-size decryption circuit family, one natively
+  computable decryption algorithm and fixed polynomial widths are chosen first. Then every
+  polynomially bounded depth family is covered by an actual scheme with that decryption algorithm,
+  assuming only decision LWE [Gentry2009, Definition 3 and Theorem 3]. Security is asymptotic
+  IND-CPA, a consequence of [Gentry2009, Theorem 4] without its exact loss. Native certificates are
+  uniform for each depth family; key generation reads only the unary security parameter.
 * **Fully homomorphic encryption.** The one-key self-loop construction evaluates every circuit,
   assuming decision LWE for this family *and* the separate one-key circular-security assumption
   `Encryption.CircularSecure` for the base scheme [Gentry2009, Section 2, the self-loop
@@ -43,6 +43,8 @@ concrete-security loss.
 
 ## Main results
 
+* `Cslib.Crypto.Homomorphic.GSW.DepthParameters.exists_leveled_decrypt_circuits`: uniformly
+  generated polynomial-size decryption circuits for the leveled GSW scheme across all budgets.
 * `Cslib.Crypto.Homomorphic.GSW.DepthParameters.exists_leveled_of_decisionLWE`: leveled FHE.
 * `Cslib.Crypto.Homomorphic.GSW.DepthParameters.fullyHomomorphic_of_decisionLWE_of_circularSecure`:
   FHE under the additional circular-security assumption.
@@ -61,8 +63,34 @@ namespace Cslib.Crypto.Homomorphic.GSW.DepthParameters
 open Circuits Probability Turing.MultiTapeTM
 open Parameters (dimension noise)
 
+/-- The leveled GSW scheme's complete tagged decryption algorithm has a uniformly generated family
+of polynomial-size circuits on the derived widths
+`(3 * secretWidth k + 1) + (ciphertextWidth k + 1)`, shared across all depth budgets and requiring
+no computational assumption. -/
+theorem exists_leveled_decrypt_circuits :
+    ∃ circuits : ∀ k, Circuit Boolean.signature
+        ((3 * secretWidth k + 1) + (ciphertextWidth k + 1)) 1,
+      ComputableInPolyTime
+        (fun k => (⟨_, circuits k⟩ : Σ m, Circuit Boolean.signature m 1))
+        encUnary (Boolean.encCircuit 1) ∧
+      PolynomiallyBounded (fun k => (circuits k).size) ∧
+      ∀ (budget : ℕ → ℕ) k (sk ciphertext : List Bool),
+        sk.length = 3 * secretWidth k + 1 →
+        ciphertext.length = ciphertextWidth k + 1 →
+        (circuits k).eval Boolean.interpretation
+            (BitString.ofList ((3 * secretWidth k + 1) + (ciphertextWidth k + 1))
+              (sk ++ ciphertext)) 0 =
+          (Leveled.scheme decryptionCircuits budget).decrypt k sk ciphertext := by
+  have hsecret : ComputableInPolyTime secretWidth encUnary encUnary := by
+    have := Parameters.computableInPolyTime_dimension
+    have := computableInPolyTime_width
+    unfold secretWidth
+    fun_prop
+  exact Leveled.exists_uniform_decrypt_circuits decryptionCircuits
+    computableInPolyTime_decryptionCircuits hsecret
+
 /-- Leveled FHE from GSW under decision LWE for this family, with quasi-polynomial modulus.
-One polynomial-size circuit family computes the common decryption algorithm
+One uniformly generated polynomial-size circuit family computes the common decryption algorithm
 `Leveled.decrypt decryptionCircuits`, which is natively computable, and the key and ciphertext
 widths are fixed polynomials; all of these are chosen before the depth. Every polynomially
 bounded depth family is then covered by an actual scheme with an efficiently computable budget
@@ -73,6 +101,9 @@ theorem exists_leveled_of_decisionLWE
     (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) (noise k))) :
     ∃ circuits : ∀ k, Circuit Boolean.signature
         ((3 * secretWidth k + 1) + (ciphertextWidth k + 1)) 1,
+      ComputableInPolyTime
+        (fun k => (⟨_, circuits k⟩ : Σ m, Circuit Boolean.signature m 1))
+        encUnary (Boolean.encCircuit 1) ∧
       PolynomiallyBounded (fun k => (circuits k).size) ∧
       (∀ k (sk ciphertext : List Bool), sk.length = 3 * secretWidth k + 1 →
         ciphertext.length = ciphertextWidth k + 1 →
@@ -108,12 +139,12 @@ theorem exists_leveled_of_decisionLWE
           Encryption.INDCPA (Leveled.scheme decryptionCircuits budget).keyGen
             (Leveled.scheme decryptionCircuits budget).encrypt := by
   have hD := computableInPolyTime_decryptionCircuits
-  obtain ⟨circuits, hsize, hcircuits⟩ := Leveled.exists_decrypt_circuits decryptionCircuits hD
+  obtain ⟨circuits, hgen, hsize, hcircuits⟩ := exists_leveled_decrypt_circuits
   have hdecrypt := (Leveled.computableInPolyTime_scheme_decrypt decryptionCircuits hD
     (fun _ => 0))
   obtain ⟨hsecret, hciphertext⟩ := Leveled.polynomiallyBounded_widths decryptionCircuits hD
-  refine ⟨circuits, hsize, fun k sk c hsk hc => hcircuits (fun _ => 0) k sk c hsk hc, hdecrypt,
-    hsecret, hciphertext, fun depth hdepth => ?_⟩
+  refine ⟨circuits, hgen, hsize, fun k sk c hsk hc => hcircuits (fun _ => 0) k sk c hsk hc,
+    hdecrypt, hsecret, hciphertext, fun depth hdepth => ?_⟩
   obtain ⟨budget, hbudget, hle, hcorrect, hpermitted, hwidth, -, -, hkeyGen, hencrypt, -,
       hevaluate, hsecure⟩ :=
     Leveled.exists_scheme_of_polynomiallyBounded decryptionCircuits correct fixedWidth

Complexity/Crypto/Computational/Homomorphic/Leveled/Bootstrapping.lean

@@ -19,9 +19,11 @@ the same constructed scheme. This module assembles correctness, budget-independe
 widths and security without assuming those conclusions for the output scheme. Native certificates
 for its algorithms remain available in `Leveled.PolyTime`.
 
-`Leveled.exists_decrypt_circuits` and `Leveled.exists_decrypt_parameter_bound` give one decryption
-circuit family and one parameter-only resource bound shared by all budgets. These include the
-complete tagged decoder and are chosen independently of the requested depth family.
+`Leveled.exists_decrypt_circuits`, `Leveled.exists_uniform_decrypt_circuits` and
+`Leveled.exists_decrypt_parameter_bound` give one decryption circuit family (with a native
+polynomial-time circuit generator when `secretWidth` is computable in polynomial time in unary) and
+one parameter-only resource bound shared by all budgets. These include the complete tagged decoder
+and are chosen independently of the requested depth family.
 
 The contract evaluates fresh ciphertexts under an efficiently computed unary depth budget. It
 does not promise arbitrary reuse of evaluated wrapper ciphertexts, circuit privacy, a concrete

Complexity/Crypto/Computational/Homomorphic/Leveled/Compactness.lean

@@ -9,6 +9,7 @@ module
 
 public import Complexity.Crypto.Computational.Homomorphic.Leveled.PolyTime
 import Complexity.Computability.Circuit.Boolean.PolynomialTime
+import Complexity.Computability.Complexity.Problems.CircuitValue.Compilation
 
 /-!
 # Compact decryption for the leveled construction
@@ -21,13 +22,18 @@ parameter together cost four gates.
 
 The resulting family depends only on the security parameter, not on the depth budget. It agrees
 with decryption on all words of the prescribed lengths, including malformed secret-key encodings.
-This establishes the common-decryption-circuit condition in Gentry's Definition 3. The conclusion
-is a nonuniform existence theorem; it does not supply a circuit generator.
+This establishes the common-decryption-circuit condition in Gentry's Definition 3. When the base
+secret width is also computable in polynomial time in unary, `exists_uniform_decrypt_circuits`
+compiles the native decryption algorithm via `CircuitValue.exists_uniformCircuitFamily` to provide
+a native polynomial-time circuit generator.
 
 ## Main results
 
 * `Cslib.Crypto.Homomorphic.Leveled.exists_decrypt_circuits`: polynomial-size circuits for the
   complete tagged decryption algorithm, with one family shared by every depth budget.
+* `Cslib.Crypto.Homomorphic.Leveled.exists_uniform_decrypt_circuits`: uniformly generated
+  polynomial-size circuits for the complete tagged decryption algorithm when `secretWidth` is
+  computable in polynomial time in unary.
 * `Cslib.Crypto.Homomorphic.Leveled.exists_decrypt_parameter_bound`: a native time and space bound
   depending only on the security parameter at the prescribed widths, shared by every budget.
 
@@ -88,7 +94,8 @@ include hD in
 /-- The actual decoder, tag selection and base-circuit evaluation have polynomial-size circuits
 on the derived key and ciphertext widths. One circuit family works for every depth budget, and
 its specification includes every word of those widths, without a support or validity premise.
-This is nonuniform circuit existence, not a circuit-generation certificate. -/
+This is nonuniform circuit existence, not a circuit-generation certificate; see
+`exists_uniform_decrypt_circuits` when `secretWidth` is computable in polynomial time in unary. -/
 theorem exists_decrypt_circuits :
     ∃ circuits : ∀ n, Circuit Boolean.signature
         ((3 * secretWidth n + 1) + (ciphertextWidth n + 1)) 1,
@@ -134,4 +141,80 @@ theorem exists_decrypt_circuits :
     rw [hparameter]
     exact (hdecryptL (n, sk, ciphertext)).symm
 
+include hD in
+/-- When the base secret width is computable in polynomial time in unary, the actual decoder, tag
+selection and base-circuit evaluation have a uniformly generated family of polynomial-size circuits
+on the derived key and ciphertext widths. One circuit family and one native polynomial-time
+generator work for every depth budget, and the specification covers all words of the prescribed
+widths, without a support or validity premise. Since `hD` determines only the sum
+`secretWidth n + ciphertextWidth n`, computing the wrapper arity
+`(3 * secretWidth n + 1) + (ciphertextWidth n + 1)` and the split point between the secret key and
+ciphertext uses `hsecret`. -/
+theorem exists_uniform_decrypt_circuits
+    (hsecret : ComputableInPolyTime secretWidth encUnary encUnary) :
+    ∃ circuits : ∀ n, Circuit Boolean.signature
+        ((3 * secretWidth n + 1) + (ciphertextWidth n + 1)) 1,
+      ComputableInPolyTime
+        (fun n => (⟨_, circuits n⟩ : Σ m, Circuit Boolean.signature m 1))
+        encUnary (Boolean.encCircuit 1) ∧
+      PolynomiallyBounded (fun n => (circuits n).size) ∧
+      ∀ (budget : ℕ → ℕ) n (sk ciphertext : List Bool),
+        sk.length = 3 * secretWidth n + 1 →
+        ciphertext.length = ciphertextWidth n + 1 →
+        (circuits n).eval Boolean.interpretation
+            (BitString.ofList ((3 * secretWidth n + 1) + (ciphertextWidth n + 1))
+              (sk ++ ciphertext)) 0 =
+          (scheme D budget).decrypt n sk ciphertext := by
+  have hview : ComputableTidilyInPolyTime
+      (fun c : Σ m, Circuit Boolean.signature m 1 => (c.1, c.2.code))
+      (Boolean.encCircuit 1) (encPair encUnary Boolean.encCode) := .of_eq fun _ => rfl
+  have htotal : ComputableTidilyInPolyTime
+      (fun n => secretWidth n + ciphertextWidth n) encUnary encUnary :=
+    hview.fst'.comp hD.tidy
+  have hsec : ComputableTidilyInPolyTime secretWidth encUnary encUnary := hsecret.tidy
+  have hciph : ComputableTidilyInPolyTime ciphertextWidth encUnary encUnary := by
+    simpa only [Nat.add_sub_cancel_left] using
+      (show ComputableTidilyInPolyTime
+        (fun n => (secretWidth n + ciphertextWidth n) - secretWidth n) encUnary encUnary by
+        fun_prop)
+  let K := fun n => 3 * secretWidth n + 1
+  let W := fun n => K n + (ciphertextWidth n + 1)
+  have hK : ComputableTidilyInPolyTime K encUnary encUnary := by dsimp [K]; fun_prop
+  have hW : ComputableTidilyInPolyTime W encUnary encUnary := by dsimp [W]; fun_prop
+  let decryptConcat (p : ℕ × List Bool) : Bool :=
+    decrypt D p.1 (p.2.take (K p.1)) (p.2.drop (K p.1))
+  have hdecryptConcat : ComputableInPolyTime decryptConcat (encPair encUnary encBits) encBool := by
+    have hklen : ComputableTidilyInPolyTime (fun p : ℕ × List Bool => K p.1)
+        (encPair encUnary encBits) encUnary :=
+      hK.comp (ComputableTidilyInPolyTime.fst encUnary encBits)
+    have hw : ComputableTidilyInPolyTime (Prod.snd : ℕ × List Bool → List Bool)
+        (encPair encUnary encBits) encBits :=
+      ComputableTidilyInPolyTime.snd encUnary encBits
+    exact computableInPolyTime_decrypt D hD
+      (.of_tidy (ComputableTidilyInPolyTime.fst encUnary encBits))
+      (.of_tidy (ComputableTidilyInPolyTime.bitsTakeWithInput hw hklen))
+      (.of_tidy (ComputableTidilyInPolyTime.bitsDropWithInput hw hklen))
+  let F (p : ℕ × List Bool) : List Bool := [decryptConcat p]
+  have hF : ComputableInPolyTime F (encPair encUnary encBits) encBits :=
+    .of_tidy (hdecryptConcat.tidy.of_enc_eq fun _ => rfl)
+  obtain ⟨circuits, hcode, hcorrect⟩ :=
+    Complexity.CircuitValue.exists_uniformCircuitFamily
+      (n := W) (m := fun _ => 1) (.of_tidy hW) (by fun_prop) hF
+  have hgen : ComputableInPolyTime
+      (fun n => (⟨W n, circuits n⟩ : Σ m, Circuit Boolean.signature m 1))
+      encUnary (Boolean.encCircuit 1) :=
+    .of_tidy ((hW.prod hcode.tidy).of_enc_eq fun n => by simp only [Boolean.encCircuit_apply])
+  have hsize : PolynomiallyBounded (fun n => (circuits n).size) := by
+    have hlength : PolynomiallyBounded (fun n => (circuits n).code.1.length) :=
+      ((ComputableTidilyInPolyTime.length_list Boolean.encGate).comp
+        hcode.tidy.fst').polynomiallyBounded
+    exact hlength.mono_of_le fun n => (Circuit.length_code_fst (circuits n)).ge
+  refine ⟨circuits, hgen, hsize, ?_⟩
+  intro budget n sk ciphertext hsk hciphertext
+  have hwlen : (sk ++ ciphertext).length = W n := by simp [W, K, hsk, hciphertext]
+  have h := hcorrect n (BitString.ofList (W n) (sk ++ ciphertext)) 0
+  simp only [F, decryptConcat, K, BitString.ofFn_ofList hwlen, List.take_left' hsk,
+    List.drop_left' hsk, Fin.val_zero, List.getD_cons_zero] at h
+  exact h
+
 end Cslib.Crypto.Homomorphic.Leveled

ComplexityTests/Abstracts/GSWFHETests.lean

@@ -29,21 +29,27 @@ example (c e : ℕ) :
       Encoding.encUnary Encoding.encUnary :=
   CryptographyBridge.polyTime_iff.mpr (by fun_prop)
 
-/-- `leveled` yields both a depth-indexed scheme family `E` with joint polynomial runtime in
-`(security, d)` (`NativeInDepth E`) and, for every unary-polynomial depth budget `budget`, a scheme
-`S` obtained by substituting `d = budget security` into `E`. -/
+/-- `leveled` yields a uniformly generated decryption circuit family `circuit`, a depth-indexed
+scheme family `E` with joint polynomial runtime in `(security, d)` (`NativeInDepth E`) and, for
+every unary-polynomial depth budget `budget`, a scheme `S` obtained by substituting
+`d = budget security` into `E`. -/
 example (hLWE : DecisionLWE) :
     ∃ (circuit : ∀ security, Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature
         ((3 * secretWidth security + 1) + (ciphertextWidth security + 1)) 1)
       (E : ℕ → Cslib.Crypto.Homomorphic.Scheme),
+      Computation.PolyTime
+        (fun security =>
+          (⟨(3 * secretWidth security + 1) + (ciphertextWidth security + 1), circuit security⟩ :
+            Σ k, Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature k 1))
+        Encoding.encUnary (Cslib.Circuits.Boolean.encCircuit 1) ∧
       NativeInDepth E ∧
       ∀ d : ℕ,
         DecryptsWith (E d) (fun security => 3 * secretWidth security + 1)
           (fun security => ciphertextWidth security + 1) circuit ∧
         Homomorphic (E d) (fun _ C => C.2.depth ≤ d) ∧
         ChosenMessageSecure (E d) := by
-  obtain ⟨circuit, E, -, -, -, hjoint, hd, -⟩ := leveled hLWE
-  exact ⟨circuit, E, hjoint, fun d => ⟨(hd d).2.2.1, (hd d).2.2.2.1, (hd d).2.2.2.2.2.2⟩⟩
+  obtain ⟨circuit, E, hgen, -, -, -, hjoint, hd, -⟩ := leveled hLWE
+  exact ⟨circuit, E, hgen, hjoint, fun d => ⟨(hd d).2.2.1, (hd d).2.2.2.1, (hd d).2.2.2.2.2.2⟩⟩
 
 /-- `unframe` reads back a framed word, whatever follows it. -/
 theorem unframe_frame_append (u v : List Bool) : unframe (Encoding.frame u ++ v) = u := by

ComplexityTests/Crypto/Bootstrapping.lean

@@ -97,6 +97,21 @@ example : ∃ budget : ℕ → ℕ,
       hevaluate hD spikedDepth_bounded
   exact ⟨budget, hbudget, by simpa [spikedDepth] using hdom 0, hdom, hcorrect, hsecurity⟩
 
+-- Without a separate computability hypothesis on `secretWidth`, `exists_decrypt_circuits` still
+-- gives a single polynomial-size decryption circuit family across all budgets.
+example :
+    ∃ circuits : ∀ n, Circuit Boolean.signature
+        ((3 * secretWidth n + 1) + (ciphertextWidth n + 1)) 1,
+      PolynomiallyBounded (fun n => (circuits n).size) ∧
+      ∀ (budget : ℕ → ℕ) n (sk ciphertext : List Bool),
+        sk.length = 3 * secretWidth n + 1 →
+        ciphertext.length = ciphertextWidth n + 1 →
+        (circuits n).eval Boolean.interpretation
+            (BitString.ofList ((3 * secretWidth n + 1) + (ciphertextWidth n + 1))
+              (sk ++ ciphertext)) 0 =
+          (Leveled.scheme D budget).decrypt n sk ciphertext :=
+  Leveled.exists_decrypt_circuits D hD
+
 end ConditionalSecurity
 
 -- This fixture is insecure. These are concrete instances of every non-security input
@@ -133,15 +148,18 @@ example : ∃ (time space : ℕ × List Bool × List Bool → ℕ) (bound : ℕ
       time (n, sk, ciphertext) ≤ bound n ∧ space (n, sk, ciphertext) ≤ bound n :=
   Leveled.exists_decrypt_parameter_bound decryptionCircuits (.of_tidy circuits_poly)
 
--- The same polynomial-size circuit family implements the complete decoder and tag selection
--- for every budget, not only the base XOR circuit or only supported secrets.
+-- The same uniformly generated polynomial-size circuit family implements the complete decoder
+-- and tag selection for every budget, not only the base XOR circuit or only supported secrets.
 example : ∃ circuits : ℕ → Circuit Boolean.signature 7 1,
+    ComputableInPolyTime
+      (fun n => (⟨7, circuits n⟩ : Σ m, Circuit Boolean.signature m 1))
+      encUnary (Boolean.encCircuit 1) ∧
     PolynomiallyBounded (fun n => (circuits n).size) ∧
     ∀ (budget : ℕ → ℕ) n (sk ciphertext : List Bool),
       sk.length = 4 → ciphertext.length = 3 →
       (circuits n).eval Boolean.interpretation (BitString.ofList 7 (sk ++ ciphertext)) 0 =
         (Leveled.scheme decryptionCircuits budget).decrypt n sk ciphertext :=
-  Leveled.exists_decrypt_circuits decryptionCircuits (.of_tidy circuits_poly)
+  Leveled.exists_uniform_decrypt_circuits decryptionCircuits (.of_tidy circuits_poly) (by fun_prop)
 
 private def malformedSecret : List Bool := [true, true, true, true]
 
@@ -152,14 +170,18 @@ example : malformedSecret.length = 4 ∧
   decide +kernel
 
 example : ∃ circuits : ℕ → Circuit Boolean.signature 7 1,
+    ComputableInPolyTime
+      (fun n => (⟨7, circuits n⟩ : Σ m, Circuit Boolean.signature m 1))
+      encUnary (Boolean.encCircuit 1) ∧
     PolynomiallyBounded (fun n => (circuits n).size) ∧
     ∀ (budget : ℕ → ℕ) n,
       (circuits n).eval Boolean.interpretation
           (BitString.ofList 7 (malformedSecret ++ [true, true, false])) 0 =
         (Leveled.scheme decryptionCircuits budget).decrypt n malformedSecret
           [true, true, false] := by
-  obtain ⟨circuits, hsize, hcorrect⟩ :=
-    Leveled.exists_decrypt_circuits decryptionCircuits (.of_tidy circuits_poly)
-  exact ⟨circuits, hsize, fun budget n => hcorrect budget n _ _ rfl rfl⟩
+  obtain ⟨circuits, hgen, hsize, hcorrect⟩ :=
+    Leveled.exists_uniform_decrypt_circuits decryptionCircuits (.of_tidy circuits_poly)
+      (by fun_prop)
+  exact ⟨circuits, hgen, hsize, fun budget n => hcorrect budget n _ _ rfl rfl⟩
 
 end ComplexityTests.Bootstrapping