From f80b32eb3b0d54090ddbf5059b16d20a8dab3f9b Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Wed, 28 Oct 2026 02:06:19 +0000
Subject: [PATCH 1/3] feat(crypto): uniform decryption circuit generator for
 leveled FHE (#1104)

---
 .../Homomorphic/GSW/FullyHomomorphic.lean     |  51 ++++++--
 .../Homomorphic/Leveled/Bootstrapping.lean    |   8 +-
 .../Homomorphic/Leveled/Compactness.lean      | 118 +++++++++++++++++-
 ComplexityTests/Abstracts/GSWFHETests.lean    |  16 ++-
 ComplexityTests/Crypto/Bootstrapping.lean     |  19 ++-
 .../Crypto/GSWFullyHomomorphic.lean           |  15 ++-
 ROADMAP.md                                    |   6 +-
 .../ComplexityAbstracts/GSWFHEAbstract.lean   |  24 +++-
 .../ComplexityAbstracts/GSWFHEBridge.lean     |  39 ++++--
 abstracts/README.md                           |   2 +-
 abstracts/catalogue.json                      |   2 +-
 11 files changed, 250 insertions(+), 50 deletions(-)

diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean
index fea6c76253..3786330221 100644
--- a/Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean
+++ b/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
diff --git a/Complexity/Crypto/Computational/Homomorphic/Leveled/Bootstrapping.lean b/Complexity/Crypto/Computational/Homomorphic/Leveled/Bootstrapping.lean
index bef514f164..edb88ec1c6 100644
--- a/Complexity/Crypto/Computational/Homomorphic/Leveled/Bootstrapping.lean
+++ b/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
diff --git a/Complexity/Crypto/Computational/Homomorphic/Leveled/Compactness.lean b/Complexity/Crypto/Computational/Homomorphic/Leveled/Compactness.lean
index af42d00d63..45dfd138d6 100644
--- a/Complexity/Crypto/Computational/Homomorphic/Leveled/Compactness.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/Leveled/Compactness.lean
@@ -8,7 +8,9 @@ module
 -- upstream: candidate
 
 public import Complexity.Crypto.Computational.Homomorphic.Leveled.PolyTime
+import Complexity.Computability.Circuit.Boolean.CodeSubstitution
 import Complexity.Computability.Circuit.Boolean.PolynomialTime
+import Complexity.Computability.Complexity.Problems.CircuitValue.Completeness
 
 /-!
 # Compact decryption for the leveled construction
@@ -21,13 +23,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 the uniform Boolean tableau constructor and prefix
+hardwiring 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.
 
@@ -134,4 +141,111 @@ 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))
+  obtain ⟨baseCircuits, hbaseCode, hbaseEval⟩ :=
+    Complexity.CircuitValue.exists_uniformCircuits hdecryptConcat
+  let r := fun n => frame (encUnary n)
+  let circuits (n : ℕ) : Circuit Boolean.signature (W n) 1 :=
+    Boolean.prefixCircuit (r n) (baseCircuits ((r n).length + W n))
+  have hframe : ComputableTidilyInPolyTime frame encBits encBits :=
+    .of_linear (.of_frame fun _ => rfl)
+  have hr : ComputableTidilyInPolyTime r encUnary encBits :=
+    hframe.comp (ComputableTidilyInPolyTime.encode encUnary)
+  have hN : ComputableTidilyInPolyTime (fun n => (r n).length + W n) encUnary encUnary := by
+    have hrlen : ComputableTidilyInPolyTime (fun n => (r n).length) encUnary encUnary :=
+      ComputableTidilyInPolyTime.length_bits.comp hr
+    fun_prop
+  have hcode : ComputableTidilyInPolyTime (fun n => (circuits n).code) encUnary Boolean.encCode := by
+    have hprefix := (Boolean.computableInPolyTime_prefixCode (.of_tidy hr)
+      (.of_tidy (ComputableTidilyInPolyTime.unary_to_binary.comp hW))
+      (hbaseCode.comp (.of_tidy hN))).tidy
+    exact hprefix.of_enc_eq fun n => by
+      rw [show (circuits n).code = _ from Boolean.code_prefixCircuit _ _]
+      rfl
+  have hgen : ComputableInPolyTime
+      (fun n => (⟨W n, circuits n⟩ : Σ m, Circuit Boolean.signature m 1))
+      encUnary (Boolean.encCircuit 1) :=
+    .of_tidy ((hW.prod hcode).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.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 hcorrectOfFn (p : ℕ × List Bool) (N : ℕ) (y : Fin N → Bool)
+      (hy : encPair encUnary encBits p = List.ofFn y) :
+      (baseCircuits N).eval Boolean.interpretation y 0 = decryptConcat p := by
+    have hN := congrArg List.length hy
+    simp only [List.length_ofFn] at hN
+    subst N
+    have hw : (fun i : Fin (encPair encUnary encBits p).length =>
+        (encPair encUnary encBits p)[i]) = y :=
+      List.ofFn_injective (List.ofFn_getElem.trans hy)
+    simpa only [hw] using hbaseEval p
+  let w := sk ++ ciphertext
+  have hwlen : w.length = W n := by simp [w, W, K, hsk, hciphertext]
+  have hin : encPair encUnary encBits (n, w) = r n ++ w := by
+    simp [r, encPair_apply, encBits_apply]
+  have hofFn : List.ofFn (Fin.append (fun i : Fin (r n).length => (r n)[i.val])
+      (BitString.ofList (W n) w)) = r n ++ w := by
+    rw [List.ofFn_fin_append, List.ofFn_getElem, BitString.ofFn_ofList hwlen]
+  change (Boolean.prefixCircuit (r n) (baseCircuits ((r n).length + W n))).eval
+    Boolean.interpretation (BitString.ofList (W n) w) 0 = decrypt D n sk ciphertext
+  rw [Boolean.eval_prefixCircuit,
+    hcorrectOfFn (n, w) ((r n).length + W n) _ (hin.trans hofFn.symm)]
+  simp only [decryptConcat, w, K, List.take_left' hsk, List.drop_left' hsk]
+
 end Cslib.Crypto.Homomorphic.Leveled
diff --git a/ComplexityTests/Abstracts/GSWFHETests.lean b/ComplexityTests/Abstracts/GSWFHETests.lean
index 4b1db89a27..198db8720e 100644
--- a/ComplexityTests/Abstracts/GSWFHETests.lean
+++ b/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
diff --git a/ComplexityTests/Crypto/Bootstrapping.lean b/ComplexityTests/Crypto/Bootstrapping.lean
index b455944898..41d9f6270c 100644
--- a/ComplexityTests/Crypto/Bootstrapping.lean
+++ b/ComplexityTests/Crypto/Bootstrapping.lean
@@ -133,15 +133,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 +155,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
diff --git a/ComplexityTests/Crypto/GSWFullyHomomorphic.lean b/ComplexityTests/Crypto/GSWFullyHomomorphic.lean
index af4a9ed19b..012960fa30 100644
--- a/ComplexityTests/Crypto/GSWFullyHomomorphic.lean
+++ b/ComplexityTests/Crypto/GSWFullyHomomorphic.lean
@@ -17,7 +17,7 @@ namespace ComplexityTests.Crypto.GSWFullyHomomorphic
 
 open Cslib Cslib.Crypto Cslib.Circuits Cslib.Circuits.Boolean Cslib.Crypto.Homomorphic
 open Cslib.Crypto.Homomorphic.GSW Cslib.Crypto.Homomorphic.GSW.DepthParameters
-open Cslib.Probability
+open Cslib.Probability Turing.MultiTapeTM
 open Parameters (dimension noise)
 
 -- At security parameter zero the base secret holds one 65536-bit residue, and a ciphertext is a
@@ -37,7 +37,7 @@ example (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k)
           ((Leveled.scheme decryptionCircuits budget).evaluate k keys.1 ⟨2, nandCircuit⟩
             inputs)).support,
         (Leveled.scheme decryptionCircuits budget).decrypt k keys.2 c = !(a && b) := by
-  obtain ⟨-, -, -, -, -, -, hleveled⟩ := exists_leveled_of_decisionLWE hLWE
+  obtain ⟨-, -, -, -, -, -, -, hleveled⟩ := exists_leveled_of_decisionLWE hLWE
   obtain ⟨budget, -, -, -, hcorrect, hpermitted, -⟩ := hleveled _ (PolynomiallyBounded.const 2)
   refine ⟨budget, fun k keys hkeys a b inputs hinputs c hc => ?_⟩
   have h := hcorrect.decrypt_evaluate k keys hkeys ⟨2, nandCircuit⟩
@@ -46,10 +46,14 @@ example (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k)
   rfl
 
 /-- The schemes for two different depth families share one decryption algorithm, computed by one
-polynomial-size circuit family chosen before either depth, as in Gentry's Definition 3. -/
+uniformly generated polynomial-size circuit family chosen before either depth, as in Gentry's
+Definition 3. -/
 example (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) ∧
       ∃ shallow deep : ℕ → ℕ, (∀ k, 2 ≤ shallow k ∧ k ≤ deep k) ∧
         (Leveled.scheme decryptionCircuits shallow).decrypt =
@@ -58,10 +62,11 @@ example (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k)
           (circuits k).eval Boolean.interpretation
               (BitString.ofList ((3 * secretWidth k + 1) + (ciphertextWidth k + 1)) (sk ++ c)) 0 =
             (Leveled.scheme decryptionCircuits deep).decrypt k sk c := by
-  obtain ⟨circuits, hsize, hcircuits, -, -, -, hleveled⟩ := exists_leveled_of_decisionLWE hLWE
+  obtain ⟨circuits, hgen, hsize, hcircuits, -, -, -, hleveled⟩ :=
+    exists_leveled_of_decisionLWE hLWE
   obtain ⟨shallow, -, hshallow, hdecShallow, -⟩ := hleveled _ (PolynomiallyBounded.const 2)
   obtain ⟨deep, -, hdeep, hdecDeep, -⟩ := hleveled _ PolynomiallyBounded.id
-  refine ⟨circuits, hsize, shallow, deep, fun k => ⟨hshallow k, hdeep k⟩,
+  refine ⟨circuits, hgen, hsize, shallow, deep, fun k => ⟨hshallow k, hdeep k⟩,
     hdecShallow.trans hdecDeep.symm, fun k sk c hsk hc => ?_⟩
   rw [hdecDeep]
   exact hcircuits k sk c hsk hc
diff --git a/ROADMAP.md b/ROADMAP.md
index 8fe3980541..7371b17b3d 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -77,9 +77,9 @@ Priorities live in this list and in the tiers of [#897].
 
 ### Modern fully homomorphic encryption
 
-Gentry's bootstrapping is instantiated with GSW ([#486]; formal abstract `gsw-fhe`). Its
-follow-ups ([#1104]) are a uniform generator for the leveled scheme's wrapper decryption circuits
-(uniform compactness), multi-hop evaluation, and Gentry's exact concrete-security loss together
+Gentry's bootstrapping is instantiated with GSW ([#486]; formal abstract `gsw-fhe`), including
+uniform compactness for the leveled wrapper decryption circuits and level-indexed multi-hop
+evaluation. Its remaining follow-up ([#1104]) is Gentry's exact concrete-security loss together
 with the `poly(ℓ, d)` running-time clause of his Theorem 4. Then develop these in reviewable
 milestones, reusing the finite sampling, gadget algebra, native certificates and game reductions
 where their hypotheses match. The [pre-rewrite FHE section][archive-fhe] maps the schemes to
diff --git a/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean b/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean
index c6ee74de14..5503c2b504 100644
--- a/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean
+++ b/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean
@@ -447,8 +447,9 @@ def ChosenMessageSecure (S : Cslib.Crypto.Homomorphic.Scheme) : Prop :=
 
 Gentry's Definition 3 asks for one decryption circuit shared by all depths, correctness for every
 circuit up to the depth, and algorithms polynomial in the parameter and the depth [Gentry2009,
-Definition 3]. In `leveled`, one polynomial-size circuit family `circuit` and one depth-indexed
-scheme family `E : ℕ → Cslib.Crypto.Homomorphic.Scheme` are chosen first. The family `E` satisfies
+Definition 3]. In `leveled`, one uniformly generated polynomial-size circuit family `circuit` and
+one depth-indexed scheme family `E : ℕ → Cslib.Crypto.Homomorphic.Scheme` are chosen first. The
+family `E` satisfies
 `NativeInDepth E`, so key generation, encryption, decryption and evaluation on
 `(1^security, 1^d, …)` each run on a single uniform machine with one runtime polynomial in
 `(security, d)` jointly, and at every fixed depth `d`, `E d` is correct for circuits of depth at
@@ -463,7 +464,8 @@ polynomially bounded depth `d(security) ≤ c (security + 1) ^ e` is covered by
 -/
 
 /-- **Leveled fully homomorphic encryption from decision LWE** [Gentry2009, Theorem 3]. One
-polynomial-size decryption circuit family `circuit` and one depth-indexed scheme family `E` satisfy
+uniformly generated polynomial-size decryption circuit family `circuit` and one depth-indexed
+scheme family `E` satisfy
 `NativeInDepth E` (one runtime polynomial in `(security, d)` jointly), and at every depth `d` and
 every unary-polynomial depth budget `budget` (via `d = budget security`), the first framed word of
 the first framed component of the public key and the first framed word of the secret key, the key
@@ -475,6 +477,11 @@ theorem leveled (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) ∧
       Cslib.PolynomiallyBounded (fun security => (circuit security).size) ∧
       Cslib.PolynomiallyBounded (fun security => 3 * secretWidth security + 1) ∧
       Cslib.PolynomiallyBounded (fun security => ciphertextWidth security + 1) ∧
@@ -511,11 +518,16 @@ theorem leveled (hLWE : DecisionLWE) :
 /-- **Fully homomorphic encryption from decision LWE and circular security** [Gentry2009,
 Definition 2 and Section 2]. There is a scheme whose key generation is the self-loop key and
 which encrypts and decrypts with GSW that is correct for every circuit, keeps GSW's widths,
-decrypts with polynomial-size circuits, has native algorithms and is IND-CPA, assuming decision
-LWE for this family and, separately, one-key circular security of GSW. -/
+decrypts with uniformly generated polynomial-size circuits, has native algorithms and is IND-CPA,
+assuming decision LWE for this family and, separately, one-key circular security of GSW. -/
 theorem fullyHomomorphic (hLWE : DecisionLWE) (hcircular : CircularSecure) :
     ∃ circuit : ∀ security, Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature
         (secretWidth security + ciphertextWidth security) 1,
+      Computation.PolyTime
+        (fun security =>
+          (⟨secretWidth security + ciphertextWidth security, circuit security⟩ :
+            Σ k, Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature k 1))
+        Encoding.encUnary (Cslib.Circuits.Boolean.encCircuit 1) ∧
       Cslib.PolynomiallyBounded (fun security => (circuit security).size) ∧
       Cslib.PolynomiallyBounded secretWidth ∧ Cslib.PolynomiallyBounded ciphertextWidth ∧
       ∃ S : Cslib.Crypto.Homomorphic.Scheme,
@@ -532,7 +544,7 @@ end ComplexityTests.Abstracts.GSWFHEAbstract
 
 /--
 info: abstract audit passed for `ComplexityTests.Abstracts.GSWFHEAbstract`: 46 root declarations,
-314 dependencies checked
+315 dependencies checked
 -/
 #guard_msgs (whitespace := lax) in
 #check_abstract ComplexityTests.Abstracts.GSWFHEAbstract allowing [
diff --git a/abstracts/ComplexityAbstracts/GSWFHEBridge.lean b/abstracts/ComplexityAbstracts/GSWFHEBridge.lean
index e669015546..951b0d2157 100644
--- a/abstracts/ComplexityAbstracts/GSWFHEBridge.lean
+++ b/abstracts/ComplexityAbstracts/GSWFHEBridge.lean
@@ -605,6 +605,11 @@ asserts, with one decryption circuit family chosen before the depth and budget.
 theorem leveled_witness (hLWE : DecisionLWE) :
     ∃ circuit : ∀ security, Circuits.Circuit Circuits.Boolean.signature
         ((3 * secretWidth security + 1) + (ciphertextWidth security + 1)) 1,
+      Computation.PolyTime
+        (fun security =>
+          (⟨(3 * secretWidth security + 1) + (ciphertextWidth security + 1), circuit security⟩ :
+            Σ k, Circuits.Circuit Circuits.Boolean.signature k 1))
+        Encoding.encUnary (Circuits.Boolean.encCircuit 1) ∧
       PolynomiallyBounded (fun security => (circuit security).size) ∧
       PolynomiallyBounded (fun security => 3 * secretWidth security + 1) ∧
       PolynomiallyBounded (fun security => ciphertextWidth security + 1) ∧
@@ -666,7 +671,7 @@ theorem leveled_witness (hLWE : DecisionLWE) :
   have hkeyGen := GSW.DepthParameters.isPPTOn_keyGen
   have hencrypt := GSW.DepthParameters.isPPTOn_encrypt
   have hevaluate := GSW.DepthParameters.isPPTOn_evaluate
-  obtain ⟨circuits, hsize, hcircuits⟩ := Leveled.exists_decrypt_circuits D hD
+  obtain ⟨circuits, hgen, hsize, hcircuits⟩ := GSW.DepthParameters.exists_leveled_decrypt_circuits
   obtain ⟨hsecret, hciphertext, hkgJoint, hencJoint, hdecJoint, hevalJoint⟩ :=
     Leveled.schemeFamily_spec D hkeyGen hencrypt hevaluate
       GSW.DepthParameters.computableInPolyTime_decryptionCircuits
@@ -702,7 +707,7 @@ theorem leveled_witness (hLWE : DecisionLWE) :
         (Leveled.computableInPolyTime_scheme_decrypt D hD budget)
         (Leveled.isPPTOn_scheme_evaluate hencrypt D hD hevaluate budget hb),
       chosenMessageSecure_of_indCPA hsecure⟩
-  refine ⟨circuits, hsize, hsecret, hciphertext,
+  refine ⟨circuits, CryptographyBridge.polyTime_iff.mpr hgen.tidy, hsize, hsecret, hciphertext,
     nativeInDepth_of hkgJoint hencJoint hdecJoint hevalJoint,
     fun d => hforBudget (fun _ => d) (by fun_prop),
     fun budget hbudget =>
@@ -712,7 +717,13 @@ theorem leveled_witness (hLWE : DecisionLWE) :
 /-- **The library's fixed-key scheme witnesses `fullyHomomorphic`**, with GSW's own decryption
 circuits `GSW.DepthParameters.decryptionCircuits.circuit`. -/
 theorem fullyHomomorphic_witness (hLWE : DecisionLWE) (hcircular : CircularSecure) :
-    PolynomiallyBounded
+    Computation.PolyTime
+        (fun security =>
+          (⟨secretWidth security + ciphertextWidth security,
+              GSW.DepthParameters.decryptionCircuits.circuit security⟩ :
+            Σ k, Circuits.Circuit Circuits.Boolean.signature k 1))
+        Encoding.encUnary (Circuits.Boolean.encCircuit 1) ∧
+      PolynomiallyBounded
         (fun security => (GSW.DepthParameters.decryptionCircuits.circuit security).size) ∧
       PolynomiallyBounded secretWidth ∧ PolynomiallyBounded ciphertextWidth ∧
       (∀ security, ProbComp.eval
@@ -731,7 +742,9 @@ theorem fullyHomomorphic_witness (hLWE : DecisionLWE) (hcircular : CircularSecur
       hdecrypt, hevaluate, hsecure⟩ :=
     GSW.DepthParameters.fullyHomomorphic_of_decisionLWE_of_circularSecure
       (decisionLWE_iff.mp hLWE) (circularSecure_iff.mp hcircular)
-  exact ⟨hsize, hsecret, hciphertext, fixedKey_keyGen, fixedKey_encryptsAndDecrypts,
+  exact ⟨CryptographyBridge.polyTime_iff.mpr
+      GSW.DepthParameters.computableInPolyTime_decryptionCircuits.tidy,
+    hsize, hsecret, hciphertext, fixedKey_keyGen, fixedKey_encryptsAndDecrypts,
     (FixedKey.decryptionCircuits GSW.DepthParameters.decryptionCircuits).correct,
     homomorphic_of_correct hcorrect fun security C _ => hpermitted security C,
     fixedWidths_of_fixedWidth hwidth fun security C _ => hpermitted security C,
@@ -748,6 +761,11 @@ theorem leveled {unframe dropFrame : List Bool → List Bool}
     ∃ (circuit : ∀ security, Circuits.Circuit Circuits.Boolean.signature
         ((3 * secretWidth security + 1) + (ciphertextWidth security + 1)) 1)
       (E : ℕ → Homomorphic.Scheme),
+      Computation.PolyTime
+        (fun security =>
+          (⟨(3 * secretWidth security + 1) + (ciphertextWidth security + 1), circuit security⟩ :
+            Σ k, Circuits.Circuit Circuits.Boolean.signature k 1))
+        Encoding.encUnary (Circuits.Boolean.encCircuit 1) ∧
       PolynomiallyBounded (fun security => (circuit security).size) ∧
       PolynomiallyBounded (fun security => 3 * secretWidth security + 1) ∧
       PolynomiallyBounded (fun security => ciphertextWidth security + 1) ∧
@@ -781,8 +799,8 @@ theorem leveled {unframe dropFrame : List Bool → List Bool}
           Native S ∧ ChosenMessageSecure S := by
   obtain rfl : unframe = Turing.MultiTapeTM.unframe := funext hunframe
   obtain rfl : dropFrame = Turing.MultiTapeTM.dropFrame := funext hdropFrame
-  obtain ⟨circuit, hsize, hsecret, hciphertext, hjoint, hd, hbudget⟩ := leveled_witness hLWE
-  exact ⟨circuit, _, hsize, hsecret, hciphertext, hjoint, hd, fun budget hb =>
+  obtain ⟨circuit, hgen, hsize, hsecret, hciphertext, hjoint, hd, hbudget⟩ := leveled_witness hLWE
+  exact ⟨circuit, _, hgen, hsize, hsecret, hciphertext, hjoint, hd, fun budget hb =>
     ⟨_, hbudget budget hb⟩⟩
 
 theorem fullyHomomorphic {unframe : List Bool → List Bool}
@@ -790,6 +808,11 @@ theorem fullyHomomorphic {unframe : List Bool → List Bool}
     (hLWE : DecisionLWE) (hcircular : CircularSecure) :
     ∃ circuit : ∀ security, Circuits.Circuit Circuits.Boolean.signature
         (secretWidth security + ciphertextWidth security) 1,
+      Computation.PolyTime
+        (fun security =>
+          (⟨secretWidth security + ciphertextWidth security, circuit security⟩ :
+            Σ k, Circuits.Circuit Circuits.Boolean.signature k 1))
+        Encoding.encUnary (Circuits.Boolean.encCircuit 1) ∧
       PolynomiallyBounded (fun security => (circuit security).size) ∧
       PolynomiallyBounded secretWidth ∧ PolynomiallyBounded ciphertextWidth ∧
       ∃ S : Homomorphic.Scheme,
@@ -800,7 +823,7 @@ theorem fullyHomomorphic {unframe : List Bool → List Bool}
         FixedWidths S (fun _ _ => True) secretWidth ciphertextWidth ∧
         Native S ∧ ChosenMessageSecure S := by
   obtain rfl : unframe = Turing.MultiTapeTM.unframe := funext hunframe
-  obtain ⟨hsize, hsecret, hciphertext, h⟩ := fullyHomomorphic_witness hLWE hcircular
-  exact ⟨_, hsize, hsecret, hciphertext, _, h⟩
+  obtain ⟨hgen, hsize, hsecret, hciphertext, h⟩ := fullyHomomorphic_witness hLWE hcircular
+  exact ⟨_, hgen, hsize, hsecret, hciphertext, _, h⟩
 
 end ComplexityTests.Abstracts.GSWFHEBridge
diff --git a/abstracts/README.md b/abstracts/README.md
index 3570835c96..b2e7015dd4 100644
--- a/abstracts/README.md
+++ b/abstracts/README.md
@@ -44,7 +44,7 @@ former paper/TeX index is retired; Git history retains its sources.
 | [Håstad and Razborov–Smolensky: parity resists shallow circuits](ComplexityAbstracts/ConstantDepthAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/constant-depth.pdf) | Explicit finite bounds, gate semantics and depth conventions; nonuniform lower bounds. |
 | [Formula lower bounds: parity and Andreev](ComplexityAbstracts/FormulaBoundsAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/formula-bounds.pdf) | De Morgan formulas, literal leaves, explicit block indexing and finite quantitative bounds; no general-circuit lower bound. |
 | [One-way functions yield pseudorandom generators and adaptive functions](ComplexityAbstracts/CryptographyAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/cryptography.pdf) | Uniform probabilistic polynomial time with explicit native evaluators, negligible advantage and full stateful oracle semantics; asymptotic security, not a concrete implementation audit. |
-| [Gentry and GSW: fully homomorphic encryption from LWE](ComplexityAbstracts/GSWFHEAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/gsw-fhe.pdf) | Explicit GSW algorithms at an LWE family with quasi-polynomial modulus, the GSW key law for the leveled scheme's fresh ciphertexts and Gentry's self-loop key; an existential evaluator, remaining key chain and decryption circuits with correctness, fixed widths, polynomial-size decryption circuits, native algorithms and IND-CPA; circular security as a separate hypothesis. |
+| [Gentry and GSW: fully homomorphic encryption from LWE](ComplexityAbstracts/GSWFHEAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/gsw-fhe.pdf) | Explicit GSW algorithms at an LWE family with quasi-polynomial modulus, the GSW key law for the leveled scheme's fresh ciphertexts and Gentry's self-loop key; an existential evaluator, remaining key chain and decryption circuits with correctness, fixed widths, uniformly generated polynomial-size decryption circuits, native algorithms and IND-CPA; circular security as a separate hypothesis. |
 | [Haken: pigeonhole formulas require long resolution proofs](ComplexityAbstracts/ResolutionAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/resolution.pdf) | The non-onto pigeonhole formula and a line-based resolution rule, with bound 2^(floor(n/24)); proof size is not solver runtime. |
 | [Communication: disjointness and inner product resist randomness](ComplexityAbstracts/CommunicationAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/communication.pdf) | Shared randomness, per-input error at most one third and explicit linear bounds; exact deterministic equality records the final-answer convention. |
 | [Sipser–Gács–Lautemann: BPP lies in the second polynomial level](ComplexityAbstracts/SipserLautemannAbstract.lean) · [PDF](https://www.cslib.io/complexitylib/abstracts/sipser-lautemann.pdf) | Fair random bits, explicit quantifier blocks and total native polynomial-time tests. |
diff --git a/abstracts/catalogue.json b/abstracts/catalogue.json
index 767bb3eca0..8f9d64158f 100644
--- a/abstracts/catalogue.json
+++ b/abstracts/catalogue.json
@@ -170,7 +170,7 @@
         "ComplexityTests.Abstracts.GSWFHEAbstract.fullyHomomorphic"
       ],
       "summary": "Bootstrapping the GSW scheme gives leveled fully homomorphic encryption from decision LWE, and fully homomorphic encryption under an additional circular-security assumption.",
-      "scope": "Explicit GSW key generation, encryption and decryption at a centered-binomial LWE family with quasi-polynomial modulus. The leveled scheme family E has joint native strict PPT runtime in (security, d) via NativeInDepth, its fresh-ciphertext key pair has the GSW key-generation law, and the fully homomorphic scheme's key generation is Gentry's self-loop key; the evaluator, the rest of the leveled keys and the decryption circuits are existential. Perfect correctness on fresh encryptions, fixed widths, polynomial-size decryption circuits, native strict PPT algorithms and asymptotic IND-CPA. Circular security is a separate hypothesis; no lattice hardness, circuit privacy, multi-hop evaluation or concrete loss.",
+      "scope": "Explicit GSW key generation, encryption and decryption at a centered-binomial LWE family with quasi-polynomial modulus. The leveled scheme family E has joint native strict PPT runtime in (security, d) via NativeInDepth, its fresh-ciphertext key pair has the GSW key-generation law, and the fully homomorphic scheme's key generation is Gentry's self-loop key; the evaluator, the rest of the leveled keys and the decryption circuits are existential. Perfect correctness on fresh encryptions, fixed widths, uniformly generated polynomial-size decryption circuits, native strict PPT algorithms and asymptotic IND-CPA. Circular security is a separate hypothesis; no lattice hardness, circuit privacy, multi-hop evaluation or concrete loss.",
       "namespace": "ComplexityTests.Abstracts.GSWFHEAbstract",
       "foundations": [
         "ComplexityAbstracts.Encoding",

From f3acaf0b4edf9936418cbcd8b3656616ce2e384f Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Wed, 28 Oct 2026 02:43:12 +0000
Subject: [PATCH 2/3] fix(crypto): update GSWFHEAbstract docstring and simplify
 exists_uniform_decrypt_circuits (#1104)

---
 .../Homomorphic/Leveled/Compactness.lean      | 67 +++++--------------
 ComplexityTests/Crypto/Bootstrapping.lean     | 15 +++++
 .../ComplexityAbstracts/GSWFHEAbstract.lean   | 17 +++--
 3 files changed, 43 insertions(+), 56 deletions(-)

diff --git a/Complexity/Crypto/Computational/Homomorphic/Leveled/Compactness.lean b/Complexity/Crypto/Computational/Homomorphic/Leveled/Compactness.lean
index 45dfd138d6..a139844ab7 100644
--- a/Complexity/Crypto/Computational/Homomorphic/Leveled/Compactness.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/Leveled/Compactness.lean
@@ -8,9 +8,8 @@ module
 -- upstream: candidate
 
 public import Complexity.Crypto.Computational.Homomorphic.Leveled.PolyTime
-import Complexity.Computability.Circuit.Boolean.CodeSubstitution
 import Complexity.Computability.Circuit.Boolean.PolynomialTime
-import Complexity.Computability.Complexity.Problems.CircuitValue.Completeness
+import Complexity.Computability.Complexity.Problems.CircuitValue.Compilation
 
 /-!
 # Compact decryption for the leveled construction
@@ -25,8 +24,8 @@ The resulting family depends only on the security parameter, not on the depth bu
 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. When the base
 secret width is also computable in polynomial time in unary, `exists_uniform_decrypt_circuits`
-compiles the native decryption algorithm via the uniform Boolean tableau constructor and prefix
-hardwiring to provide a native polynomial-time circuit generator.
+compiles the native decryption algorithm via `CircuitValue.exists_uniformCircuitFamily` to provide
+a native polynomial-time circuit generator.
 
 ## Main results
 
@@ -95,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,
@@ -194,58 +194,27 @@ theorem exists_uniform_decrypt_circuits
       (.of_tidy (ComputableTidilyInPolyTime.fst encUnary encBits))
       (.of_tidy (ComputableTidilyInPolyTime.bitsTakeWithInput hw hklen))
       (.of_tidy (ComputableTidilyInPolyTime.bitsDropWithInput hw hklen))
-  obtain ⟨baseCircuits, hbaseCode, hbaseEval⟩ :=
-    Complexity.CircuitValue.exists_uniformCircuits hdecryptConcat
-  let r := fun n => frame (encUnary n)
-  let circuits (n : ℕ) : Circuit Boolean.signature (W n) 1 :=
-    Boolean.prefixCircuit (r n) (baseCircuits ((r n).length + W n))
-  have hframe : ComputableTidilyInPolyTime frame encBits encBits :=
-    .of_linear (.of_frame fun _ => rfl)
-  have hr : ComputableTidilyInPolyTime r encUnary encBits :=
-    hframe.comp (ComputableTidilyInPolyTime.encode encUnary)
-  have hN : ComputableTidilyInPolyTime (fun n => (r n).length + W n) encUnary encUnary := by
-    have hrlen : ComputableTidilyInPolyTime (fun n => (r n).length) encUnary encUnary :=
-      ComputableTidilyInPolyTime.length_bits.comp hr
-    fun_prop
-  have hcode : ComputableTidilyInPolyTime (fun n => (circuits n).code) encUnary Boolean.encCode := by
-    have hprefix := (Boolean.computableInPolyTime_prefixCode (.of_tidy hr)
-      (.of_tidy (ComputableTidilyInPolyTime.unary_to_binary.comp hW))
-      (hbaseCode.comp (.of_tidy hN))).tidy
-    exact hprefix.of_enc_eq fun n => by
-      rw [show (circuits n).code = _ from Boolean.code_prefixCircuit _ _]
-      rfl
+  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).of_enc_eq fun n => by simp only [Boolean.encCircuit_apply])
+    .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.fst').polynomiallyBounded
+        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 hcorrectOfFn (p : ℕ × List Bool) (N : ℕ) (y : Fin N → Bool)
-      (hy : encPair encUnary encBits p = List.ofFn y) :
-      (baseCircuits N).eval Boolean.interpretation y 0 = decryptConcat p := by
-    have hN := congrArg List.length hy
-    simp only [List.length_ofFn] at hN
-    subst N
-    have hw : (fun i : Fin (encPair encUnary encBits p).length =>
-        (encPair encUnary encBits p)[i]) = y :=
-      List.ofFn_injective (List.ofFn_getElem.trans hy)
-    simpa only [hw] using hbaseEval p
-  let w := sk ++ ciphertext
-  have hwlen : w.length = W n := by simp [w, W, K, hsk, hciphertext]
-  have hin : encPair encUnary encBits (n, w) = r n ++ w := by
-    simp [r, encPair_apply, encBits_apply]
-  have hofFn : List.ofFn (Fin.append (fun i : Fin (r n).length => (r n)[i.val])
-      (BitString.ofList (W n) w)) = r n ++ w := by
-    rw [List.ofFn_fin_append, List.ofFn_getElem, BitString.ofFn_ofList hwlen]
-  change (Boolean.prefixCircuit (r n) (baseCircuits ((r n).length + W n))).eval
-    Boolean.interpretation (BitString.ofList (W n) w) 0 = decrypt D n sk ciphertext
-  rw [Boolean.eval_prefixCircuit,
-    hcorrectOfFn (n, w) ((r n).length + W n) _ (hin.trans hofFn.symm)]
-  simp only [decryptConcat, w, K, List.take_left' hsk, List.drop_left' hsk]
+  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
diff --git a/ComplexityTests/Crypto/Bootstrapping.lean b/ComplexityTests/Crypto/Bootstrapping.lean
index 41d9f6270c..b6ff272cd4 100644
--- a/ComplexityTests/Crypto/Bootstrapping.lean
+++ b/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
diff --git a/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean b/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean
index 5503c2b504..1bdeb5e365 100644
--- a/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean
+++ b/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean
@@ -36,8 +36,9 @@ own public key.
 scheme's keys and the polynomial-size decryption circuits. For `leveled` only the marginal law of
 the fresh-ciphertext key pair is fixed; the later keys of the chain, the encrypted links and their
 joint law with that pair are not. The theorems state that such machinery exists with elementary
-properties: correctness for the allowed circuits, fixed key and ciphertext widths, one decryption
-circuit family for all depths, native efficiency and IND-CPA security. These properties exclude
+properties: correctness for the allowed circuits, fixed key and ciphertext widths, one uniformly
+generated decryption circuit family for all depths, native efficiency and IND-CPA security. These
+properties exclude
 trivial witnesses. Decryption is the fixed GSW decryption, and evaluated ciphertexts have the fixed
 ciphertext width, so evaluation cannot leave the computation to decryption: it must output a word of
 that width that GSW decryption maps to the circuit's output. Nor can evaluation work in the clear.
@@ -70,11 +71,13 @@ each a foundational model:
 Lean checks every proof through `GSWFHEBridge`.
 
 The claims are perfect correctness on supported fresh encryptions, fixed key and ciphertext
-widths, polynomial-size decryption circuits, uniform native strict polynomial-time algorithms and
-asymptotic IND-CPA security against uniform classical adversaries. They do not include lattice
-hardness or a worst-case reduction, circuit privacy, evaluation of already evaluated ciphertexts,
-a uniform generator for the leveled decryption circuits, or the concrete loss of Gentry's
-Theorem 4.
+widths, uniformly generated polynomial-size decryption circuits, uniform native strict
+polynomial-time algorithms and asymptotic IND-CPA security against uniform classical adversaries.
+Uniform circuit generation means a single native machine that, on `1^security`, writes the
+decryption circuit's binary code `Cslib.Circuits.Boolean.encCircuit 1`, including its input arity,
+in time polynomial in `security`. The claims do not include lattice hardness or a worst-case
+reduction, circuit privacy, evaluation of already evaluated ciphertexts, or the concrete loss of
+Gentry's Theorem 4.
 
 ## References
 

From 33d76904c96ebb6cf434396ccb83f1efb253eadf Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Wed, 28 Oct 2026 06:52:11 +0000
Subject: [PATCH 3/3] chore(abstracts): update GSWFHEAbstract #guard_msgs
 dependency count after #1388 (#1104)

---
 abstracts/ComplexityAbstracts/GSWFHEAbstract.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean b/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean
index 1bdeb5e365..e842517c2f 100644
--- a/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean
+++ b/abstracts/ComplexityAbstracts/GSWFHEAbstract.lean
@@ -547,7 +547,7 @@ end ComplexityTests.Abstracts.GSWFHEAbstract
 
 /--
 info: abstract audit passed for `ComplexityTests.Abstracts.GSWFHEAbstract`: 46 root declarations,
-315 dependencies checked
+316 dependencies checked
 -/
 #guard_msgs (whitespace := lax) in
 #check_abstract ComplexityTests.Abstracts.GSWFHEAbstract allowing [