feat(crypto): prove generated-key GSW security from exact decision LWE

Complexity.lean

@@ -1276,6 +1276,7 @@ public import Complexity.Crypto.Computational.Commitment
 public import Complexity.Crypto.Computational.Encryption.Basic
 public import Complexity.Crypto.Computational.Encryption.Circular
 public import Complexity.Crypto.Computational.Encryption.PolyTime
+public import Complexity.Crypto.Computational.Encryption.PublicKeyReplacement
 public import Complexity.Crypto.Computational.GGM.Circuit
 public import Complexity.Crypto.Computational.GGM.Evaluation
 public import Complexity.Crypto.Computational.GGM.Expansion
@@ -1316,10 +1317,13 @@ public import Complexity.Crypto.Computational.Homomorphic.GSW.Basic
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Decoding
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Gadget
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Hiding
+public import Complexity.Crypto.Computational.Homomorphic.GSW.LWE
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Noise
+public import Complexity.Crypto.Computational.Homomorphic.GSW.Parameters
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Sampling
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Sampling.Randomness
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Sampling.Serialized
+public import Complexity.Crypto.Computational.Homomorphic.GSW.Security
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.Correctness
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.PolyTime
@@ -1348,6 +1352,7 @@ public import Complexity.Crypto.Computational.Homomorphic.Leveled.Security
 public import Complexity.Crypto.Computational.Homomorphic.Refresh
 public import Complexity.Crypto.Computational.Hybrid.SavedPrediction
 public import Complexity.Crypto.Computational.Hybrid.Sequence
+public import Complexity.Crypto.Computational.LWE.Basic
 public import Complexity.Crypto.Computational.OneWay
 public import Complexity.Crypto.Computational.OneWay.BPP
 public import Complexity.Crypto.Computational.OneWay.Collision
@@ -1411,6 +1416,7 @@ public import Complexity.Crypto.Game.Hybrid
 public import Complexity.Crypto.Game.Statistical
 public import Complexity.Crypto.Negligible
 public import Complexity.Crypto.Negligible.Basic
+public import Complexity.Crypto.Negligible.Dyadic
 public import Complexity.Crypto.Primitives.PRG.Circuit
 public import Complexity.Crypto.Primitives.PRG.Game
 public import Complexity.Crypto.Primitives.PRG.NextBit

Complexity/Crypto/Computational/Encryption/PublicKeyReplacement.lean

@@ -0,0 +1,147 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Crypto.Computational.Basic
+public import Complexity.Crypto.Computational.Encryption.Basic
+import Complexity.Probability.PMF
+import Complexity.Tactic.PPT
+
+/-!
+# Replacing the public-key distribution in chosen-message security
+
+One uniform distinguisher samples a hidden fair challenge bit after the adversary has chosen its
+messages and saved state. It runs the actual encryption and guessing stages, then returns the
+guess XOR the hidden bit. Comparing this same distinguisher on two public-key distributions
+controls the change in their chosen-message gaps, with an exact factor of two.
+
+## Main definitions
+
+* `publicKeyGame`: the chosen-message experiment for a specified public-key law.
+* `keyDistinguisher`: the single reduction, preserving the adversary's saved state.
+
+## Main results
+
+* `eval_game_eq_publicKeyGame`: the actual encryption game uses its public-key marginal.
+* `isPPT_keyDistinguisher`: native strict PPT composition of the actual reduction.
+* `probability_keyDistinguisher`: the exact affine identity for the signed chosen-message gap.
+* `advantage_publicKeyGame_le`: quantitative public-key replacement with loss two.
+
+## References
+
+* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*][BonehShoup2023],
+  Section 11.2, for the chosen-message experiment and game-reduction method.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.Encryption
+
+open Probability Turing.MultiTapeTM
+
+/-- Run the chosen-message experiment with a specified public-key distribution. The complete
+state returned by message selection is passed unchanged to guessing. -/
+noncomputable def publicKeyGame (keys : PMF (List Bool))
+    (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool))
+    (adversary : Adversary) (bit : Bool) (security : ℕ) : Game := do
+  let pk ← keys
+  let choice ← ProbComp.eval (adversary.choose security pk)
+  let ciphertext ← ProbComp.eval
+    (encrypt security pk (if bit then choice.1.2 else choice.1.1))
+  ProbComp.eval (adversary.guess security choice.2 ciphertext)
+
+/-- An honest key generator contributes precisely its public-key marginal. -/
+theorem eval_game_eq_publicKeyGame (keyGen : ℕ → ProbComp (List Bool × List Bool))
+    (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool))
+    (adversary : Adversary) (bit : Bool) (security : ℕ) :
+    ProbComp.eval (game keyGen encrypt adversary bit security) =
+      publicKeyGame ((ProbComp.eval (keyGen security)).map Prod.fst)
+        encrypt adversary bit security := eval_game keyGen encrypt adversary bit security
+
+/-- A single uniform distinguisher with its own hidden fair challenge bit. The adversary sees
+only the supplied public key and the actual challenge ciphertext, with its saved state retained. -/
+noncomputable def keyDistinguisher
+    (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool))
+    (adversary : Adversary) : Distinguisher := fun security pk => do
+  let choice ← adversary.choose security pk
+  let bit ← ProbComp.uniform Bool
+  let ciphertext ← encrypt security pk (if bit then choice.1.2 else choice.1.1)
+  let guess ← adversary.guess security choice.2 ciphertext
+  return guess ^^ bit
+
+/-- The reduction is one uniform strict PPT program when encryption and both adversary stages
+are certified on their complete inputs. -/
+theorem isPPT_keyDistinguisher
+    {encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)} {adversary : Adversary}
+    (hencrypt : IsPPTOn (encPair encUnary (encPair encBits encBool)) encBits
+      (fun input => encrypt input.1 input.2.1 input.2.2))
+    (hadversary : adversary.IsPPT) : IsPPT encBool (keyDistinguisher encrypt adversary) := by
+  have hchoose := hadversary.choose
+  have hguess := hadversary.guess
+  unfold keyDistinguisher
+  ppt
+
+/-- The hidden-bit experiment averages the two chosen-message games, complementing the second.
+No finiteness or independence assumption is imposed on the saved state. -/
+theorem distinguishingGame_keyDistinguisher (keys : PMF (List Bool))
+    (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool))
+    (adversary : Adversary) (security : ℕ) :
+    distinguishingGame keys (keyDistinguisher encrypt adversary security) = (do
+      let bit ← PMF.uniformOfFintype Bool
+      (publicKeyGame keys encrypt adversary bit security).map (fun guess => guess ^^ bit)) := by
+  simp only [distinguishingGame, keyDistinguisher, publicKeyGame, ProbComp.eval_bind,
+    ProbComp.eval_uniform, ProbComp.eval_pure, PMF.monad_bind_eq_bind, PMF.map_bind]
+  rw [PMF.bind_comm]
+  congr 1
+  funext pk
+  rw [PMF.bind_comm]
+  rfl
+
+/-- Acceptance is one half plus half the signed chosen-message gap. -/
+theorem probability_keyDistinguisher (keys : PMF (List Bool))
+    (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool))
+    (adversary : Adversary) (security : ℕ) :
+    (Game.succProbability
+      (distinguishingGame keys (keyDistinguisher encrypt adversary security)) : ℝ) =
+      (1 + (Game.succProbability (publicKeyGame keys encrypt adversary false security) : ℝ) -
+        Game.succProbability (publicKeyGame keys encrypt adversary true security)) / 2 := by
+  rw [distinguishingGame_keyDistinguisher]
+  simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal,
+    PMF.monad_bind_eq_bind, PMF.bind_apply_toReal, Fintype.sum_bool,
+    PMF.uniformOfFintype_apply, Fintype.card_bool]
+  norm_num [PMF.toReal_false_eq_one_sub]
+  ring
+
+/-- Replacing the public-key law costs at most twice the advantage of one uniform hidden-bit
+distinguisher, plus the chosen-message advantage under the replacement law. -/
+theorem advantage_publicKeyGame_le (real ideal : PMF (List Bool))
+    (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool))
+    (adversary : Adversary) (security : ℕ) :
+    Game.advantage (publicKeyGame real encrypt adversary false security)
+      (publicKeyGame real encrypt adversary true security) ≤
+        2 * Game.advantage
+          (distinguishingGame real (keyDistinguisher encrypt adversary security))
+          (distinguishingGame ideal (keyDistinguisher encrypt adversary security)) +
+            Game.advantage (publicKeyGame ideal encrypt adversary false security)
+              (publicKeyGame ideal encrypt adversary true security) := by
+  apply NNReal.coe_le_coe.mp
+  simp only [NNReal.coe_add, NNReal.coe_mul, NNReal.coe_ofNat, Game.coe_advantage,
+    probability_keyDistinguisher]
+  have h := abs_sub_le
+    ((Game.succProbability (publicKeyGame real encrypt adversary false security) : ℝ) -
+      Game.succProbability (publicKeyGame real encrypt adversary true security))
+    ((Game.succProbability (publicKeyGame ideal encrypt adversary false security) : ℝ) -
+      Game.succProbability (publicKeyGame ideal encrypt adversary true security)) 0
+  have hscale (a b c d : ℝ) :
+      2 * |(1 + a - b) / 2 - (1 + c - d) / 2| = |(a - b) - (c - d)| := by
+    calc
+      _ = |2 * ((1 + a - b) / 2 - (1 + c - d) / 2)| := by rw [abs_mul]; norm_num
+      _ = _ := by congr 1; ring
+  simpa only [hscale, sub_zero] using h
+
+end Cslib.Crypto.Encryption

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

@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Crypto.Computational.LWE.Basic
+public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.Correctness
+
+/-!
+# The decision-LWE distribution of generated GSW public keys
+
+The public marginal of the actual key generator is exactly the decision-LWE law with independent
+centered-binomial errors reduced modulo `2 ^ w`. The joint key generator still retains its secret;
+the equality below exposes only the public marginal, as required by the security experiment.
+
+## Main definitions
+
+* `noiseLaw`: the precise modular error law supplied to the decision-LWE hypothesis.
+
+## Main results
+
+* `eval_errorVector_mod`: independently sampled integer errors give the independent modular law.
+* `eval_keyGen_publicMatrix`: the actual generated public matrix has the stated decision-LWE law.
+* `eval_keyGenSerialized_publicWord`: the serialized key generator exposes that exact word ensemble.
+
+## References
+
+* [C. Gentry, A. Sahai and B. Waters, *Homomorphic Encryption from Learning with Errors:
+  Conceptually-Simpler, Asymptotically-Faster, Attribute-Based*, Section 3.1][GentrySahaiWaters2013]
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.Homomorphic.GSW
+
+open Probability
+
+/-- Reduce the difference of two independent `η`-bit counts modulo the actual modulus. -/
+noncomputable def noiseLaw (w η : ℕ) : PMF (ZMod (2 ^ w)) :=
+  (ProbComp.eval (sampleCenteredBinomial η)).map (fun error : ℤ => (error : ZMod (2 ^ w)))
+
+/-- Reducing independent integer errors preserves the complete independent modular error law. -/
+theorem eval_errorVector_mod (m w η : ℕ) :
+    (ProbComp.eval (OracleComp.replicateFin m (sampleCenteredBinomial η))).map
+      (fun error i => (error i : ZMod (2 ^ w))) =
+        PMF.pi (fun _ : Fin m => noiseLaw w η) := by
+  rw [← ProbComp.eval_replicateFin_map_coords, ProbComp.eval_replicateFin]
+  simp only [noiseLaw, ProbComp.eval_map]
+
+/-- The generated public matrix is an exact decision-LWE sample. This equality neither reveals
+the generated secret nor asserts that any parameter or error family is computationally hard. -/
+theorem eval_keyGen_publicMatrix (n m w η : ℕ) :
+    (ProbComp.eval (keyGen n m w η)).map Prod.fst =
+      LWE.publicMatrixLaw n m w (noiseLaw w η) := by
+  simp only [keyGen, ProbComp.eval_bind, ProbComp.eval_pure, eval_sampleKeyInputs,
+    PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind,
+    PMF.map_bind, PMF.pure_map, LWE.publicMatrixLaw]
+  rw [← eval_errorVector_mod m w η]
+  simp only [PMF.bind_map, Function.comp_def]
+  rfl
+
+/-- Encoding the actual public marginal gives the exact word ensemble in the hardness
+hypothesis, with no secret or error coordinates appended to the adversary's input. -/
+theorem eval_keyGen_publicWord (n m w η : ℕ → ℕ) (security : ℕ) :
+    (ProbComp.eval (keyGen (n security) (m security) (w security) (η security))).map
+      (fun keys => Matrix.toBinary keys.1) =
+        LWE.realEnsemble n m w (fun k => noiseLaw (w k) (η k)) security := by
+  rw [LWE.realEnsemble, ← eval_keyGen_publicMatrix, PMF.map_comp]
+  rfl
+
+/-- The actual serialized key generator has precisely the public marginal used by decision LWE.
+The encoded secret is discarded before the distinguisher is called. -/
+theorem eval_keyGenSerialized_publicWord (n m w η : ℕ → ℕ) (security : ℕ) :
+    (ProbComp.eval
+      (keyGenSerialized (n security) (m security) (w security) (η security))).map Prod.fst =
+        LWE.realEnsemble n m w (fun k => noiseLaw (w k) (η k)) security := by
+  rw [eval_keyGenSerialized, PMF.map_comp]
+  exact eval_keyGen_publicWord n m w η security
+
+end Cslib.Crypto.Homomorphic.GSW