feat(abstracts): formal abstract for fully homomorphic encryption from GSW (#486)

ComplexityTests/Abstracts/GSWFHETests.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+-- upstream: local-only (formal abstract tests)
+
+import ComplexityAbstracts.GSWFHEAbstract
+
+/-! # Clients of the GSW fully homomorphic encryption abstract
+
+The leveled theorem quantifies over depth budgets computable in unary polynomial time; every
+polynomial budget `c (security + 1) ^ e` qualifies, so the hypothesis is satisfiable. The
+abstract's framing decoders invert the shared framing, so the fixed algorithms read the keys the
+way their docstrings describe: the self-loop public key yields its GSW public key, the leveled
+public key its first key, and the leveled secret key its two endpoint keys. On a secret key of
+the GSW width, decryption of the joined word is GSW decryption.
+-/
+
+namespace ComplexityTests.Abstracts.GSWFHETests
+
+open ComplexityTests.Abstracts
+open ComplexityTests.Abstracts.GSWFHEAbstract
+
+/-- Every polynomial depth budget satisfies the hypothesis of `leveled`. -/
+example (c e : ℕ) :
+    Computation.PolyTime (fun security : ℕ => c * (security + 1) ^ e)
+      Encoding.encUnary Encoding.encUnary :=
+  CryptographyBridge.polyTime_iff.mpr (by fun_prop)
+
+/-- `unframe` reads back a framed word, whatever follows it. -/
+theorem unframe_frame_append (u v : List Bool) : unframe (Encoding.frame u ++ v) = u := by
+  induction u with
+  | nil => rfl
+  | cons b u ih =>
+    simp only [Encoding.frame, List.flatMap_cons, List.cons_append, List.nil_append,
+      List.append_assoc, unframe] at ih ⊢
+    rw [ih]
+
+/-- `dropFrame` returns what follows a framed word. -/
+theorem dropFrame_frame_append (u v : List Bool) : dropFrame (Encoding.frame u ++ v) = v := by
+  induction u with
+  | nil => rfl
+  | cons b u ih =>
+    simpa only [Encoding.frame, List.flatMap_cons, List.cons_append, List.nil_append,
+      List.append_assoc, dropFrame] using ih
+
+/-- Self-loop encryption uses the GSW public key of a self-loop public key. -/
+example (security : ℕ) (publicKey : List Bool) (encryptedKey : List (List Bool)) (bit : Bool) :
+    selfLoopEncryption security
+        (Encoding.encPair Encoding.encBits (Encoding.encList Encoding.encBits)
+          (publicKey, encryptedKey)) bit =
+      encryption security publicKey bit := by
+  simp only [selfLoopEncryption, Encoding.encPair, Encoding.encodePair, Encoding.encBits,
+    Function.Embedding.coeFn_mk, Function.Embedding.refl_apply, unframe_frame_append]
+
+/-- Leveled encryption uses the first public key of a framed list of public keys. -/
+example (security : ℕ) (first : List Bool) (rest : List (List Bool)) (links : List Bool)
+    (bit : Bool) :
+    leveledEncryption security
+        (Encoding.encPair (Encoding.encList Encoding.encBits) Encoding.encBits
+          (first :: rest, links)) bit =
+      (encryption security first bit).map (List.cons false) := by
+  simp only [leveledEncryption, Encoding.encPair, Encoding.encodePair, Encoding.encList,
+    Encoding.encodeList, Encoding.encBits, Function.Embedding.coeFn_mk,
+    Function.Embedding.refl_apply, Function.comp_apply, List.flatMap_cons,
+    unframe_frame_append]
+
+/-- On a GSW secret key of the right width, decryption of the joined word is GSW decryption. -/
+theorem decryptionWord_append (security : ℕ) (secret ciphertext : List Bool)
+    (hsecret : secret.length = secretWidth security) :
+    decryptionWord security (secret ++ ciphertext) = decryption security secret ciphertext := by
+  rw [decryptionWord, List.take_left' hsecret, List.drop_left' hsecret]
+
+/-- Leveled decryption of a fresh (`false`-tagged) ciphertext uses the first endpoint key, and of
+an evaluated (`true`-tagged) ciphertext the last. -/
+example (security : ℕ) (first last ciphertext : List Bool)
+    (hfirst : first.length = secretWidth security) (hlast : last.length = secretWidth security) :
+    leveledDecryption security (Encoding.encPair Encoding.encBits Encoding.encBits (first, last))
+        (false :: ciphertext) = decryption security first ciphertext ∧
+      leveledDecryption security (Encoding.encPair Encoding.encBits Encoding.encBits (first, last))
+        (true :: ciphertext) = decryption security last ciphertext := by
+  simp only [leveledDecryption, Encoding.encPair, Encoding.encodePair, Encoding.encBits,
+    Function.Embedding.coeFn_mk, Function.Embedding.refl_apply, List.headD_cons, List.tail_cons,
+    Bool.false_eq_true, ite_false, ite_true, unframe_frame_append, dropFrame_frame_append,
+    decryptionWord_append security _ _ hfirst, decryptionWord_append security _ _ hlast,
+    and_self]
+
+end ComplexityTests.Abstracts.GSWFHETests

ROADMAP.md

@@ -21,7 +21,7 @@ the FHE industrial context, the first-order design decisions and the repository'
 | Metacomplexity: time-bounded Kolmogorov complexity, partial MCSP, hardness magnification | [#798], audit [#884] |
 | Plain computability: delete the tidy calculus, keeping a machine-level kernel | [#862], from [#456] |
 | Consolidation: duplicates, accurate statements and docs, less churn | [#949], [#939] |
-| A concrete LWE-based fully homomorphic scheme | [#486] |
+| A concrete LWE-based fully homomorphic scheme | [#486]; follow-ups [#1104] |
 | Boneh–Shoup cryptography tracks; zero-knowledge architecture | [#640], [#643] |
 | Crypto frontier tracks: Kilian's succinct arguments, chosen-ciphertext security, signatures from one-way functions | [#999], [#1000], [#1001] |
 | OpenAI math TCS results: review Fortnow's rewrites and extract in-scope results | [#1002] |
@@ -33,7 +33,7 @@ Priorities live in this list and in the tiers of [#897].
 
 1. [Goldreich–Micali–Wigderson zero knowledge in full](#cryptographic-landmarks)
 2. [Rompel's signature theorem](#cryptographic-landmarks) ([#1001])
-3. [Gentry's bootstrapping, instantiated](#cryptographic-landmarks) ([#486])
+3. [Gentry's bootstrapping, instantiated](#cryptographic-landmarks) ([#486]; follow-ups [#1104])
 4. [Completeness of oblivious transfer](#cryptographic-landmarks)
 5. [Håstad's optimal MAX-E3SAT hardness](#approximation-and-pcp) ([#886])
 6. [Williams's NEXP ⊄ ACC⁰](#circuits-and-algebraic-complexity) ([#889])
@@ -63,9 +63,10 @@ Priorities live in this list and in the tiers of [#897].
 - **Gentry's bootstrapping, instantiated** ([#486]). GSW at its logarithmic-depth parameter
   family instantiates the generic theorem: leveled FHE under decision LWE with quasi-polynomial
   modulus for exactly that family, and FHE under the additional one-key circular-security
-  assumption. Open: the checked formal abstract of these endpoints, a uniform generator for the
-  leveled scheme's wrapper decryption circuits (uniform compactness), reuse of evaluated
-  ciphertexts as fresh inputs (multi-hop evaluation), and Gentry's exact concrete-security loss.
+  assumption. The checked formal abstract `gsw-fhe` states both endpoints with GSW's algorithms
+  written out. Open in [#1104]: a uniform generator for the leveled scheme's wrapper decryption
+  circuits (uniform compactness), reuse of evaluated ciphertexts as fresh inputs (multi-hop
+  evaluation), and Gentry's exact concrete-security loss.
 - **Completeness of oblivious transfer.** In the ideal OT-hybrid model, every polynomial-time
   multiparty functionality admits a protocol secure against static malicious corruptions, with
   real/ideal simulation and abort, under the standard communication assumptions.
@@ -480,3 +481,4 @@ not planned, not as proved.
 [#1000]: https://github.com/cslib-community/complexitylib/issues/1000
 [#1001]: https://github.com/cslib-community/complexitylib/issues/1001
 [#1002]: https://github.com/cslib-community/complexitylib/issues/1002
+[#1104]: https://github.com/cslib-community/complexitylib/issues/1104

abstracts/ComplexityAbstracts.lean

@@ -17,12 +17,15 @@ import ComplexityAbstracts.FaginAbstract
 import ComplexityAbstracts.FaginBridge
 import ComplexityAbstracts.FormulaBoundsAbstract
 import ComplexityAbstracts.FormulaBoundsBridge
+import ComplexityAbstracts.GSWFHEAbstract
+import ComplexityAbstracts.GSWFHEBridge
 import ComplexityAbstracts.GSWSecurityAbstract
 import ComplexityAbstracts.GSWSecurityBridge
 import ComplexityAbstracts.ImmermanSzelepcsenyiAbstract
 import ComplexityAbstracts.ImmermanSzelepcsenyiBridge
 import ComplexityAbstracts.PCPAbstract
 import ComplexityAbstracts.PCPBridge
+import ComplexityAbstracts.Randomized
 import ComplexityAbstracts.ResolutionAbstract
 import ComplexityAbstracts.ResolutionBridge
 import ComplexityAbstracts.SavitchAbstract

abstracts/ComplexityAbstracts/CryptographyAbstract.lean

@@ -9,6 +9,7 @@ Authors: Samuel Schlesinger
 import ComplexityAbstracts.Check
 import ComplexityAbstracts.Encoding
 import ComplexityAbstracts.Computation
+import ComplexityAbstracts.Randomized
 import ComplexityAbstracts.CryptographyBridge
 
 /-! # One-way functions, generators and adaptive pseudorandom functions
@@ -20,7 +21,9 @@ than its seed and computationally indistinguishable from uniform bits. The
 Goldreich–Goldwasser–Micali construction then produces a keyed function that looks like one
 consistently chosen random function even when each query depends on earlier answers.
 Existence of a one-way function remains a hypothesis; efficiency and security use uniform
-finite-control machines with strict polynomial bounds and independent fair coins.
+finite-control machines with strict polynomial bounds and independent fair coins. These
+conventions, `Randomized.StrictPPT`, `Randomized.Negligible` and `Randomized.Indistinguishable`,
+are the shared foundations displayed in the appendix.
 The definitions and theorem statements below specify the claim; Lean checks their proofs through
 `CryptographyBridge`. The audit allows only the listed foundational program, interpretation and
 machine modules across the implementation boundary, without importing a security definition.
@@ -40,51 +43,16 @@ as credited in `Complexity.Languages.Probabilistic.Basic`.
 
 namespace ComplexityTests.Abstracts.CryptographyAbstract
 
-/-- Exactly `n` independent fair bits, as a word of length `n`. -/
-noncomputable def uniformBits (n : ℕ) : PMF (List Bool) :=
-  (Cslib.Probability.PMF.uniformOfFintype (Fin n → Bool)).map List.ofFn
-
-/-- A uniformly strict polynomial-time probability law: one deterministic evaluator, supplied
-with polynomially many independent fair bits, realizes every input's law exactly. Its time
-includes reading the coin tape and writing the encoded output. Both evaluator and polynomial
-are fixed before the input. This also bounds every execution, rather than its expectation. -/
-def StrictPPT {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool)
-    (law : α → PMF β) : Prop :=
-  ∃ (c d : ℕ) (evaluate : α → List Bool → β),
-    Computation.PolyTime (fun p : α × List Bool => evaluate p.1 p.2)
-      (Encoding.encPair a Encoding.encBits) b ∧
-    ∀ x, law x = (uniformBits (c * ((a x).length + 1) ^ d)).map (evaluate x)
-
-/-- A nonnegative error is negligible if multiplication by every fixed power of the security
-parameter still tends to zero. The threshold and decay bound may depend on the whole adversary. -/
-def Negligible (ε : ℕ → NNReal) : Prop :=
-  ∀ k : ℕ, Filter.Tendsto (fun n : ℕ => (n : NNReal) ^ k * ε n)
-    Filter.atTop (nhds 0)
-
-/-- Probability that a Boolean experiment returns true. -/
-noncomputable def probability (p : PMF Bool) : NNReal := (p true).toNNReal
-
-/-- Every one uniform strict PPT test has negligible distinguishing advantage.
-The test receives the unary seed length and a sample. `bind` samples the word and then runs
-the test with independent coins; `nndist` is the absolute difference of success probabilities. -/
-def Indistinguishable (X Y : ℕ → PMF (List Bool)) : Prop :=
-  ∀ test : ℕ → List Bool → PMF Bool,
-    StrictPPT (Encoding.encPair Encoding.encUnary Encoding.encBits) Encoding.encBool
-      (fun p => test p.1 p.2) →
-    Negligible (fun n => nndist
-      (probability (do let sample ← X n; test n sample))
-      (probability (do let sample ← Y n; test n sample)))
-
 /-- A polynomial-time function is one-way if every strict PPT inverter, given unary `n` and
 `f(x)` for a uniform `n`-bit `x`, finds any preimage only with negligible probability.
 The candidate's length is unrestricted, and recovering the sampled `x` is unnecessary. -/
 def OneWay (f : List Bool → List Bool) : Prop :=
   Computation.PolyTime f Encoding.encBits Encoding.encBits ∧
     ∀ inverter : ℕ → List Bool → PMF (List Bool),
-      StrictPPT (Encoding.encPair Encoding.encUnary Encoding.encBits) Encoding.encBits
+      Randomized.StrictPPT (Encoding.encPair Encoding.encUnary Encoding.encBits) Encoding.encBits
         (fun p => inverter p.1 p.2) →
-      Negligible (fun n => probability (do
-        let x ← uniformBits n
+      Randomized.Negligible (fun n => Randomized.probability (do
+        let x ← Randomized.uniformBits n
         (inverter n (f x)).map fun candidate => f candidate == f x))
 
 /-- A deterministic polynomial-time generator has exact seed-dependent output length,
@@ -94,7 +62,8 @@ seed length. The function need not be injective. -/
 def PseudorandomGenerator (g : List Bool → List Bool) (length : ℕ → ℕ) : Prop :=
   Computation.PolyTime g Encoding.encBits Encoding.encBits ∧
     (∀ seed, (g seed).length = length seed.length) ∧ (∀ n, n < length n) ∧
-    Indistinguishable (fun n => (uniformBits n).map g) (fun n => uniformBits (length n))
+    Randomized.Indistinguishable (fun n => (Randomized.uniformBits n).map g)
+      (fun n => Randomized.uniformBits (length n))
 
 /-- **Håstad–Impagliazzo–Levin–Luby:** any uniform one-way function yields a deterministic
 uniform polynomial-time generator stretching every `n`-bit seed to `n+1` bits. The proof follows
@@ -169,7 +138,7 @@ with that key's function. Wrong-length queries return the empty word. The advers
 unary `n` and an empty auxiliary input. -/
 noncomputable def realPRF (family : List Bool → List Bool → List Bool)
     (adversary : ℕ → List Bool → OracleProgram Bool) (n : ℕ) : PMF Bool := do
-  let key ← uniformBits n
+  let key ← Randomized.uniformBits n
   evaluateOracle (adversary n [])
     (fun query => if query.length = n then family key query else [])
 
@@ -190,8 +159,8 @@ def PseudorandomFunction (family : List Bool → List Bool → List Bool) : Prop
     (Encoding.encPair Encoding.encBits Encoding.encBits) Encoding.encBits ∧
   (∀ key query, query.length = key.length → (family key query).length = key.length) ∧
   ∀ adversary : ℕ → List Bool → OracleProgram Bool, OraclePPT adversary →
-    Negligible (fun n => nndist (probability (realPRF family adversary n))
-      (probability (idealPRF adversary n)))
+    Randomized.Negligible (fun n => nndist (Randomized.probability (realPRF family adversary n))
+      (Randomized.probability (idealPRF adversary n)))
 
 /-- **One-way functions imply adaptive pseudorandom functions:** HILL, polynomial stretching
 and the Goldreich–Goldwasser–Micali tree construction give an efficient family satisfying the
@@ -217,11 +186,11 @@ abbrev OracleResponse : Sum ℕ (Unit × List Bool) → Type :=
   Cslib.probOracleSpec (fun _ : Unit × List Bool => List Bool)
 
 /--
-info: abstract audit passed for `ComplexityTests.Abstracts.CryptographyAbstract`: 21 root declarations, 254 dependencies checked
+info: abstract audit passed for `ComplexityTests.Abstracts.CryptographyAbstract`: 15 root declarations, 254 dependencies checked
 -/
 #guard_msgs (whitespace := lax) in
 #check_abstract ComplexityTests.Abstracts.CryptographyAbstract allowing [
-  ComplexityAbstracts.Encoding, ComplexityAbstracts.Computation,
+  ComplexityAbstracts.Encoding, ComplexityAbstracts.Computation, ComplexityAbstracts.Randomized,
   Complexity.Languages.Probabilistic.Basic,
   Complexity.Languages.Probabilistic.Oracle,
   Complexity.Languages.Probabilistic.Sum,

abstracts/ComplexityAbstracts/CryptographyBridge.lean

@@ -7,6 +7,7 @@ Authors: Samuel Schlesinger
 -- upstream: local-only (formal abstract library)
 
 import ComplexityAbstracts.CookLevinBridge
+import ComplexityAbstracts.Randomized
 import Complexity.Crypto.Computational.OneWayToPRG
 import Complexity.Crypto.Computational.PRGToOneWay
 import Complexity.Crypto.Computational.GoldreichLevin.HardCore
@@ -26,6 +27,7 @@ semantic interface with the library's strict fair-coin Turing-machine certificat
 namespace ComplexityTests.Abstracts.CryptographyBridge
 
 open Cslib Cslib.Probability Turing.MultiTapeTM
+open ComplexityTests.Abstracts.Randomized
 open scoped NNReal
 
 def frame (w : List Bool) : List Bool := w.flatMap (fun b => [true, b]) ++ [false]
@@ -54,15 +56,6 @@ theorem polyTime_iff {α β : Type} {f : α → β} {a : α ↪ List Bool} {b :
     PolyTime f a b ↔ ComputableTidilyInPolyTime f a b :=
   Turing.MultiTapeTM.computableTidilyInPolyTime_iff_exists_computableInTimeAndSpaceOfLength.symm
 
-noncomputable def uniformBits (n : ℕ) : PMF (List Bool) :=
-  (Cslib.Probability.PMF.uniformOfFintype (Fin n → Bool)).map List.ofFn
-
-def StrictPPT {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool)
-    (law : α → PMF β) : Prop :=
-  ∃ (c d : ℕ) (evaluate : α → List Bool → β),
-    PolyTime (fun p : α × List Bool => evaluate p.1 p.2) (pairEncoding a bitsEncoding) b ∧
-    ∀ x, law x = (uniformBits (c * ((a x).length + 1) ^ d)).map (evaluate x)
-
 theorem strictPPT_iff {α β : Type} {a : α ↪ List Bool} {b : β ↪ List Bool}
     {law : α → PMF β} :
     StrictPPT a b law ↔ ∃ program : α → ProbComp β,
@@ -85,24 +78,11 @@ theorem strictPPT_iff {α β : Type} {a : α ↪ List Bool} {b : β ↪ List Boo
     exact ⟨c, d, evaluate, polyTime_iff.mpr hevaluate,
       fun x => (hlaw x).symm.trans (heq x)⟩
 
-def Negligible (ε : ℕ → ℝ≥0) : Prop :=
-  ∀ k : ℕ, Filter.Tendsto (fun n : ℕ => (n : ℝ≥0) ^ k * ε n)
-    Filter.atTop (nhds 0)
-
-noncomputable def probability (p : PMF Bool) : ℝ≥0 := (p true).toNNReal
-
-def Indistinguishable (X Y : ℕ → PMF (List Bool)) : Prop :=
-  ∀ test : ℕ → List Bool → PMF Bool,
-    StrictPPT (pairEncoding unaryEncoding bitsEncoding) boolEncoding
-      (fun p => test p.1 p.2) →
-    Negligible (fun n => nndist (probability ((X n).bind (test n)))
-      (probability ((Y n).bind (test n))))
-
 theorem indistinguishable_iff {X Y : ℕ → PMF (List Bool)} :
     Indistinguishable X Y ↔ Crypto.ComputationallyIndistinguishable X Y := by
   rw [Crypto.computationallyIndistinguishable_iff_tests]
   have hadmissible (test : ℕ → List Bool → PMF Bool) :
-      StrictPPT (pairEncoding unaryEncoding bitsEncoding) boolEncoding
+      StrictPPT (Encoding.encPair Encoding.encUnary Encoding.encBits) Encoding.encBool
         (fun p => test p.1 p.2) ↔ Crypto.IsPPTTest test := by
     rw [strictPPT_iff]
     constructor
@@ -111,7 +91,7 @@ theorem indistinguishable_iff {X Y : ℕ → PMF (List Bool)} :
     · rintro ⟨program, hp, heq⟩
       exact ⟨fun p => program p.1 p.2, hp, fun p => heq p.1 p.2⟩
   simp only [Indistinguishable, hadmissible, Crypto.Game.Indistinguishable,
-    Crypto.Game.advantage, Crypto.Game.succProbability, probability,
+    Crypto.Game.advantage, Crypto.Game.succProbability, probability, PMF.monad_bind_eq_bind,
     Negligible, Crypto.Negligible, Asymptotics.SuperpolynomialDecay]
 
 def OneWay (f : List Bool → List Bool) : Prop :=