diff --git a/Complexity/Crypto/Computational/DiscreteLog.lean b/Complexity/Crypto/Computational/DiscreteLog.lean
index 2fe3e9bc4a..da8d0e75ea 100644
--- a/Complexity/Crypto/Computational/DiscreteLog.lean
+++ b/Complexity/Crypto/Computational/DiscreteLog.lean
@@ -15,6 +15,7 @@ public import Complexity.Crypto.Game
 public import Mathlib.Algebra.Field.ZMod
 public import Mathlib.Algebra.Module.Defs
 import Complexity.Probability.PMF
+import Mathlib.SetTheory.Cardinal.Finite
 
 /-!
 # The discrete-logarithm assumption
@@ -47,6 +48,9 @@ public, and an adversary's running time may depend on their length.
 
 * `Cslib.Crypto.PrimeOrderGroupFamily.smul_generator_injective`: a discrete logarithm modulo `q`
   is unique.
+* `Cslib.Crypto.PrimeOrderGroupFamily.smul_generator_surjective`,
+  `Cslib.Crypto.PrimeOrderGroupFamily.smul_generator_bijective`: the generator map is bijective.
+* `Cslib.Crypto.PrimeOrderGroupFamily.uniform_smul_generator_add`: the one-time group mask.
 
 ## References
 
@@ -122,6 +126,33 @@ theorem smul_generator_injective (d : F.Desc) :
     Function.Injective fun α : ZMod (F.order d) => α • F.generator d :=
   smul_left_injective (ZMod (F.order d)) (F.generator_ne_zero d)
 
+/-- Every element of `F.Carrier d` is a scalar multiple of the generator: `α ↦ α • g` is
+surjective. -/
+theorem smul_generator_surjective (d : F.Desc) :
+    Function.Surjective fun α : ZMod (F.order d) => α • F.generator d := by
+  have : Finite (F.Carrier d) :=
+    Nat.finite_of_card_ne_zero (by rw [F.card_carrier d]; exact (F.prime_order d).ne_zero)
+  exact ((F.smul_generator_injective d).bijective_of_nat_card_le
+    (by rw [F.card_carrier, Nat.card_zmod])).2
+
+/-- The scalar map `α ↦ α • g` is a bijection between `ZMod (F.order d)` and `F.Carrier d`. -/
+theorem smul_generator_bijective (d : F.Desc) :
+    Function.Bijective fun α : ZMod (F.order d) => α • F.generator d :=
+  ⟨F.smul_generator_injective d, F.smul_generator_surjective d⟩
+
+/-- **One-time group mask**: for any group element `m : F.Carrier d`, masking `m` by `γ • g` for a
+uniform `γ : ZMod (F.order d)` has the same distribution as `γ • g` itself. -/
+theorem uniform_smul_generator_add {α : Type*} (d : F.Desc) (m : F.Carrier d)
+    (f : F.Carrier d → PMF α) :
+    ((PMF.uniformOfFintype (ZMod (F.order d))).bind fun γ => f (γ • F.generator d + m)) =
+      (PMF.uniformOfFintype (ZMod (F.order d))).bind fun γ => f (γ • F.generator d) := by
+  obtain ⟨μ, rfl⟩ := F.smul_generator_surjective d m
+  simp only [← add_smul]
+  change (PMF.uniformOfFintype (ZMod (F.order d))).bind
+      ((fun γ => f (γ • F.generator d)) ∘ Equiv.addRight μ) =
+    (PMF.uniformOfFintype (ZMod (F.order d))).bind (fun γ => f (γ • F.generator d))
+  rw [← PMF.bind_map, PMF.uniformOfFintype_map_equiv]
+
 /-- The discrete-logarithm experiment ([BonehShoup2023], Attack Game 10.4): draw a description
 and a uniform `α`, give the adversary the description and the encoding of `α • g`, and accept
 when the binary number it outputs is `α` modulo `q`. -/
diff --git a/Complexity/Crypto/Computational/ElGamal.lean b/Complexity/Crypto/Computational/ElGamal.lean
index 2848a7696f..eef342c864 100644
--- a/Complexity/Crypto/Computational/ElGamal.lean
+++ b/Complexity/Crypto/Computational/ElGamal.lean
@@ -14,8 +14,6 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Pl
 import Complexity.Crypto.Negligible.Basic
 import Complexity.Probability.PMF
 import Complexity.Tactic.PPT
-import Mathlib.Data.Fintype.Card
-import Mathlib.SetTheory.Cardinal.Finite
 
 /-!
 # ElGamal encryption and IND-CPA security under DDH
@@ -65,9 +63,6 @@ assumptions are hypotheses, not theorems.
   `Cslib.Crypto.PrimeOrderGroupFamily.decodeElGamal_encode`: decryption correctness.
 * `Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_decodeElGamal`: encoded decryption is
   computable in polynomial time.
-* `Cslib.Crypto.PrimeOrderGroupFamily.smul_generator_surjective`,
-  `Cslib.Crypto.PrimeOrderGroupFamily.uniform_smul_generator_add`: `α ↦ α • g` is surjective and
-  `γ • g + m` is uniformly distributed over `F.Carrier d`.
 * `Cslib.Crypto.PrimeOrderGroupFamily.advantage_elGamalCPAGame_le`,
   `Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_elGamalToDDHDistinguisher`,
   `Cslib.Crypto.PrimeOrderGroupFamily.DDH.elGamalINDCPA`: ElGamal IND-CPA security for bit
@@ -169,30 +164,6 @@ theorem computableInPolyTime_decodeElGamal :
   exact ComputableInPolyTime.of_tidy
     (F.computableInPolyTime_add.tidy.comp (hd.prod (he.prod hsmul)))
 
-/-! ### Surjectivity of the generator map and the one-time group mask -/
-
-/-- Every element of `F.Carrier d` is a scalar multiple of the generator: `α ↦ α • g` is
-surjective. -/
-theorem smul_generator_surjective (d : F.Desc) :
-    Function.Surjective fun α : ZMod (F.order d) => α • F.generator d := by
-  have : Finite (F.Carrier d) :=
-    Nat.finite_of_card_ne_zero (by rw [F.card_carrier d]; exact (F.prime_order d).ne_zero)
-  exact ((F.smul_generator_injective d).bijective_of_nat_card_le
-    (by rw [F.card_carrier, Nat.card_zmod])).2
-
-/-- **One-time group mask**: for any group element `m : F.Carrier d`, masking `m` by `γ • g` for a
-uniform `γ : ZMod (F.order d)` has the same distribution as `γ • g` itself. -/
-theorem uniform_smul_generator_add {α : Type*} (d : F.Desc) (m : F.Carrier d)
-    (f : F.Carrier d → PMF α) :
-    ((PMF.uniformOfFintype (ZMod (F.order d))).bind fun γ => f (γ • F.generator d + m)) =
-      (PMF.uniformOfFintype (ZMod (F.order d))).bind fun γ => f (γ • F.generator d) := by
-  obtain ⟨μ, rfl⟩ := F.smul_generator_surjective d m
-  simp only [← add_smul]
-  change (PMF.uniformOfFintype (ZMod (F.order d))).bind
-      ((fun γ => f (γ • F.generator d)) ∘ Equiv.addRight μ) =
-    (PMF.uniformOfFintype (ZMod (F.order d))).bind (fun γ => f (γ • F.generator d))
-  rw [← PMF.bind_map, PMF.uniformOfFintype_map_equiv]
-
 /-! ### Bit encryption and IND-CPA security under DDH -/
 
 /-- Embed a message bit `b : Bool` into `F.Carrier d` as `0` (for `false`) or `g` (for `true`). -/
diff --git a/ComplexityTests/Crypto/DiffieHellman.lean b/ComplexityTests/Crypto/DiffieHellman.lean
index d7277b35f7..dc85daba2b 100644
--- a/ComplexityTests/Crypto/DiffieHellman.lean
+++ b/ComplexityTests/Crypto/DiffieHellman.lean
@@ -26,7 +26,7 @@ open Cslib Cslib.Probability Cslib.Crypto Turing.MultiTapeTM
 open scoped NNReal
 
 /-- The Schnorr group of order `11` in `(ZMod 23)ˣ`, generated by `2`. -/
-def d23 : SchnorrGroup.Desc :=
+def d23 : schnorrGroups.Desc :=
   ⟨(23, 11, 2), ⟨by norm_num, by norm_num, by norm_num, by norm_num, by norm_num⟩⟩
 
 /-- `false` encodes as the identity residue `1` in `(ZMod 23)ˣ`, and `true` as the generator `2`. -/
@@ -73,6 +73,24 @@ example (setup : ℕ → PMF schnorrGroups.Desc) (hDDH : schnorrGroups.DDH setup
         (schnorrGroups.elGamalCPAGame setup trivialAdversary true n) :=
   hDDH.elGamalINDCPA trivialAdversary trivialAdversary_isPPT
 
+/-- Under DDH random self-reducibility on the concrete group `d23`, re-randomizing any real DDH
+tuple with secret exponents `(α, β) = (3, 5)` yields the uniform real DDH tuple distribution. -/
+example :
+    let α : ZMod (schnorrGroups.order d23) := 3
+    let β : ZMod (schnorrGroups.order d23) := 5
+    schnorrGroups.ddhRerandomizeLaw d23 (α • schnorrGroups.generator d23)
+      (β • schnorrGroups.generator d23) ((α * β) • schnorrGroups.generator d23) =
+        schnorrGroups.ddhRealTupleLaw d23 :=
+  schnorrGroups.ddhRerandomizeLaw_real d23 3 5
+
+/-- Under DDH random self-reducibility for any Schnorr group, re-randomizing any candidate non-DDH
+tuple `(α • g, β • g, γ • g)` with `γ ≠ α * β` yields the uniform ideal DDH tuple distribution. -/
+example (d : schnorrGroups.Desc) {α β γ : ZMod (schnorrGroups.order d)} (hγ : γ ≠ α * β) :
+    schnorrGroups.ddhRerandomizeLaw d (α • schnorrGroups.generator d)
+      (β • schnorrGroups.generator d) (γ • schnorrGroups.generator d) =
+        schnorrGroups.ddhIdealTupleLaw d :=
+  schnorrGroups.ddhRerandomizeLaw_ideal d hγ
+
 /-! ### Axioms -/
 
 /--