From 893030cc8a7f191479ca168f640f73f2131c1d0d Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <sgschlesinger@gmail.com>
Date: Sun, 4 Oct 2026 00:44:02 -0400
Subject: [PATCH 1/2] refactor(Crypto/PRG): allow explicit seed and ideal
 distributions
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Generalizes the PRG experiments from #876 so that the seed and ideal distributions are explicit arguments. They are auto-params defaulting to `PMF.uniformOfFintype _`, so on finite types `G.Secure Admissible ε`, `Family.Secure`, and the existing results keep their meaning without changes at call sites. Computational definitions over infinite sample spaces, such as words, can now reuse these experiments.

Advantage and asymptotic security are now expressed through `Game` and `Negligible`. The `[Fintype]` and `[Nonempty]` instances move from the definitions to the results that need them, so callers that pass them explicitly need to drop them. `secure_zero_iff_outputDist_eq_uniform` becomes `secure_zero_iff_outputDist_eq`, which compares with the ideal distribution; a deprecated alias keeps the old name.
---
 Cslib/Crypto/Primitives/PRG/Asymptotic.lean | 57 ++++++++++----------
 Cslib/Crypto/Primitives/PRG/Basic.lean      | 60 +++++++++++----------
 Cslib/Crypto/Primitives/PRG/Defs.lean       | 46 +++++++++-------
 Cslib/Crypto/README.md                      |  8 ++-
 CslibTests/PRG.lean                         | 10 +++-
 5 files changed, 102 insertions(+), 79 deletions(-)

diff --git a/Cslib/Crypto/Primitives/PRG/Asymptotic.lean b/Cslib/Crypto/Primitives/PRG/Asymptotic.lean
index 7c9913b5b8..1d8a6b1330 100644
--- a/Cslib/Crypto/Primitives/PRG/Asymptotic.lean
+++ b/Cslib/Crypto/Primitives/PRG/Asymptotic.lean
@@ -7,18 +7,21 @@ Authors: Samuel Schlesinger
 module
 
 public import Cslib.Crypto.Primitives.PRG.Basic
-public import Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
 public import Mathlib.Data.FinEnum
 
 /-!
 # Asymptotic pseudorandom generator security
 
 Security for families of generators means negligible advantage for each admissible
-adversary family, following [BonehShoup2023], Definition 3.1. Negligibility uses Mathlib's
-`Asymptotics.SuperpolynomialDecay`. Admissibility is a predicate on the whole adversary
+adversary family, following [BonehShoup2023], Definition 3.1. Negligibility is
+`Cslib.Crypto.Negligible`, Mathlib's `Asymptotics.SuperpolynomialDecay` at natural parameters.
+Admissibility is a predicate on the whole adversary
 family, so a downstream computational model can express a uniform resource restriction.
 This model has a natural-number security parameter and no sampled public system parameters.
 Efficiency of generation and sampling is not asserted by these semantic definitions.
+Seed and ideal distributions can be supplied explicitly; their defaults are uniform on finite
+types. Security is stated through `Game.Secure`, so computational definitions over infinite
+sample spaces, such as words, can reuse these experiments.
 
 `SecureWithError` bounds every admissible family's advantage at parameter `n` by `ε n`.
 A negligible bound implies `Secure`.
@@ -41,45 +44,44 @@ abbrev Family (Seed Output : ℕ → Type*) := ∀ n, Generator (Seed n) (Output
 namespace Family
 
 variable {Seed Output : ℕ → Type*}
-variable [∀ n, Fintype (Seed n)] [∀ n, Nonempty (Seed n)]
-variable [∀ n, Fintype (Output n)] [∀ n, Nonempty (Output n)]
 
 /-- Every admissible adversary family has negligible distinguishing advantage.
 The predicate can encode computational restrictions; `fun _ => True` permits all families. -/
 def Secure (G : Family Seed Output)
-    (Admissible : (∀ n, Adversary (Output n)) → Prop) : Prop :=
-  ∀ adversary_family, Admissible adversary_family →
-    Asymptotics.SuperpolynomialDecay atTop (fun n : ℕ => (n : ℝ))
-      (fun n => (G n).advantage (adversary_family n))
+    (Admissible : (∀ n, Adversary (Output n)) → Prop)
+    (seed : ∀ n, PMF (Seed n) := by intro n; exact PMF.uniformOfFintype _)
+    (ideal : ∀ n, PMF (Output n) := by intro n; exact PMF.uniformOfFintype _) : Prop :=
+  Game.Secure (fun adversary n => (G n).realExperiment (adversary n) (seed := seed n))
+    (fun adversary n => Generator.idealExperiment (adversary n) (ideal := ideal n)) Admissible
 
 /-- Restricting the admissible adversary families preserves asymptotic security. -/
 theorem Secure.of_admissible {G : Family Seed Output}
     {Admissible Restricted : (∀ n, Adversary (Output n)) → Prop}
-    (h : G.Secure Admissible)
+    {seed : ∀ n, PMF (Seed n)} {ideal : ∀ n, PMF (Output n)}
+    (h : G.Secure Admissible (seed := seed) (ideal := ideal))
     (hsub : ∀ adversary_family, Restricted adversary_family → Admissible adversary_family) :
-    G.Secure Restricted := fun adversary_family ha =>
-      h adversary_family (hsub adversary_family ha)
+    G.Secure Restricted (seed := seed) (ideal := ideal) := Game.Secure.of_admissible h hsub
 
 /-- Every admissible adversary family has advantage at most `ε n` at each parameter `n`. -/
 def SecureWithError (G : Family Seed Output)
-    (Admissible : (∀ n, Adversary (Output n)) → Prop) (ε : ℕ → ℝ≥0) : Prop :=
-  ∀ adversary_family, Admissible adversary_family →
-    ∀ n, (G n).advantage (adversary_family n) ≤ ε n
+    (Admissible : (∀ n, Adversary (Output n)) → Prop) (ε : ℕ → ℝ≥0)
+    (seed : ∀ n, PMF (Seed n) := by intro n; exact PMF.uniformOfFintype _)
+    (ideal : ∀ n, PMF (Output n) := by intro n; exact PMF.uniformOfFintype _) : Prop :=
+  Game.SecureWithError (fun adversary n => (G n).realExperiment (adversary n) (seed := seed n))
+    (fun adversary n => Generator.idealExperiment (adversary n) (ideal := ideal n)) Admissible ε
 
 /-- A negligible error bound implies asymptotic security. -/
 theorem SecureWithError.secure {G : Family Seed Output}
     {Admissible : (∀ n, Adversary (Output n)) → Prop} {ε : ℕ → ℝ≥0}
-    (h : G.SecureWithError Admissible ε)
-    (hε : Asymptotics.SuperpolynomialDecay atTop (fun n : ℕ => (n : ℝ))
-      (fun n => (ε n : ℝ))) : G.Secure Admissible := by
-  intro adversary_family ha
-  apply hε.trans_abs_le
-  intro n
-  simpa only [abs_of_nonneg ((G n).advantage_nonneg (adversary_family n)),
-    abs_of_nonneg (ε n).coe_nonneg] using h adversary_family ha n
+    {seed : ∀ n, PMF (Seed n)} {ideal : ∀ n, PMF (Output n)}
+    (h : G.SecureWithError Admissible ε (seed := seed) (ideal := ideal))
+    (hε : Negligible (fun n => (ε n : ℝ))) : G.Secure Admissible (seed := seed) (ideal := ideal) :=
+  Game.SecureWithError.secure h hε
 
 section RangeTests
 
+variable [∀ n, Fintype (Seed n)] [∀ n, Nonempty (Seed n)]
+variable [∀ n, Fintype (Output n)] [∀ n, Nonempty (Output n)]
 variable [∀ n, DecidableEq (Output n)]
 
 /-- A non-negligible lower bound on the fraction of outputs outside the image rules out
@@ -87,8 +89,7 @@ security whenever exhaustive range testing is admissible. -/
 theorem not_secure_of_rangeAdversary (G : Family Seed Output)
     {Admissible : (∀ n, Adversary (Output n)) → Prop}
     (ha : Admissible (fun n => (G n).rangeAdversary)) {δ : ℕ → ℝ≥0}
-    (hδ : ¬ Asymptotics.SuperpolynomialDecay atTop (fun n : ℕ => (n : ℝ))
-      (fun n => (δ n : ℝ)))
+    (hδ : ¬ Negligible (fun n => (δ n : ℝ)))
     (hgap : ∀ᶠ n in atTop,
       (δ n : ℝ) ≤ 1 - Nat.card (Set.range (G n)) / (Fintype.card (Output n) : ℝ)) :
     ¬ G.Secure Admissible := by
@@ -96,10 +97,8 @@ theorem not_secure_of_rangeAdversary (G : Family Seed Output)
   apply hδ
   apply (h _ ha).trans_eventually_abs_le
   filter_upwards [hgap] with n hn
-  change |(δ n : ℝ)| ≤ |(G n).advantage (G n).rangeAdversary|
-  rw [abs_of_nonneg (δ n).coe_nonneg, abs_of_nonneg ((G n).advantage_nonneg _),
-    Generator.advantage_rangeAdversary]
-  exact hn
+  exact abs_le_abs_of_nonneg (δ n).coe_nonneg
+    (hn.trans_eq (Generator.advantage_rangeAdversary (G n)).symm)
 
 /-- If outputs eventually outnumber seeds by a factor of two, admissibility of exhaustive
 seed enumeration and output comparison suffices to rule out security. -/
diff --git a/Cslib/Crypto/Primitives/PRG/Basic.lean b/Cslib/Crypto/Primitives/PRG/Basic.lean
index d6dd70d168..a562a6d8b4 100644
--- a/Cslib/Crypto/Primitives/PRG/Basic.lean
+++ b/Cslib/Crypto/Primitives/PRG/Basic.lean
@@ -26,65 +26,66 @@ open scoped NNReal
 
 variable {Seed Output : Type*}
 
-variable [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output]
+variable {seed : PMF Seed} {ideal : PMF Output}
 
 /-- Advantage is nonnegative. -/
 theorem advantage_nonneg (G : Generator Seed Output) (adversary : Adversary Output) :
-    0 ≤ G.advantage adversary := abs_nonneg _
+    0 ≤ G.advantage adversary (seed := seed) (ideal := ideal) := Game.advantage_nonneg _ _
 
 /-- Advantage is at most one, with the normalization of Attack Game 3.1. -/
 theorem advantage_le_one (G : Generator Seed Output) (adversary : Adversary Output) :
-    G.advantage adversary ≤ 1 := by
-  have hreal := ENNReal.toReal_mono ENNReal.one_ne_top
-    (PMF.coe_le_one (G.realExperiment adversary) true)
-  have hideal := ENNReal.toReal_mono ENNReal.one_ne_top
-    (PMF.coe_le_one (idealExperiment adversary) true)
-  simp only [ENNReal.toReal_one] at hreal hideal
-  apply abs_sub_le_iff.mpr
-  constructor
-  · linarith [@ENNReal.toReal_nonneg (idealExperiment adversary true)]
-  · linarith [@ENNReal.toReal_nonneg (G.realExperiment adversary true)]
+    G.advantage adversary (seed := seed) (ideal := ideal) ≤ 1 := Game.advantage_le_one _ _
 
 /-- Error one imposes no restriction on a generator. -/
 theorem secure_one (G : Generator Seed Output) (Admissible : Adversary Output → Prop) :
-    G.Secure Admissible 1 := fun adversary _ => G.advantage_le_one adversary
+    G.Secure Admissible 1 (seed := seed) (ideal := ideal) :=
+  fun adversary _ => G.advantage_le_one adversary
 
 /-- A test whose output distribution is independent of its input has zero advantage. -/
 @[simp]
 theorem advantage_const (G : Generator Seed Output) (p : PMF Bool) :
-    G.advantage (fun _ => p) = 0 := by
+    G.advantage (fun _ => p) (seed := seed) (ideal := ideal) = 0 := by
   simp [advantage, realExperiment, idealExperiment, PMF.bind_const]
 
-/-- A generator with exactly uniform output is secure with zero error against any tests. -/
+/-- Matching the ideal distribution gives zero-error security against any tests. -/
 theorem secure_zero_of_outputDist_eq (G : Generator Seed Output)
-    (hG : G.outputDist = PMF.uniformOfFintype Output)
-    (Admissible : Adversary Output → Prop) : G.Secure Admissible 0 := by
+    (hG : G.outputDist (seed := seed) = ideal)
+    (Admissible : Adversary Output → Prop) :
+    G.Secure Admissible 0 (seed := seed) (ideal := ideal) := by
   intro adversary _
   simp [advantage, realExperiment, idealExperiment, hG]
 
-/-- Zero-error security against arbitrary tests is equivalent to exactly uniform output. -/
-theorem secure_zero_iff_outputDist_eq_uniform (G : Generator Seed Output) :
-    G.Secure (fun _ => True) 0 ↔ G.outputDist = PMF.uniformOfFintype Output := by
+/-- Zero-error security against arbitrary tests is equivalent to matching the ideal distribution. -/
+theorem secure_zero_iff_outputDist_eq (G : Generator Seed Output) :
+    G.Secure (fun _ => True) 0 (seed := seed) (ideal := ideal) ↔
+      G.outputDist (seed := seed) = ideal := by
   classical
   refine ⟨fun h => ?_, fun h => G.secure_zero_of_outputDist_eq h _⟩
   ext output
   apply (ENNReal.toReal_eq_toReal_iff' (PMF.apply_ne_top _ _) (PMF.apply_ne_top _ _)).mp
-  simpa [advantage, realExperiment, idealExperiment, PMF.bind_apply, PMF.pure_apply,
-    sub_eq_zero] using h (fun x => PMF.pure (decide (x = output))) trivial
+  simpa [advantage, Game.winProbability, realExperiment, idealExperiment, PMF.bind_apply,
+    PMF.pure_apply, sub_eq_zero] using h (fun x => PMF.pure (decide (x = output))) trivial
+
+@[deprecated secure_zero_iff_outputDist_eq (since := "2026-10-03")]
+alias secure_zero_iff_outputDist_eq_uniform := secure_zero_iff_outputDist_eq
 
 /-- Enlarging the allowed advantage preserves security. -/
 theorem Secure.mono {G : Generator Seed Output} {Admissible : Adversary Output → Prop} :
-    Monotone (G.Secure Admissible) :=
+    Monotone (G.Secure Admissible (seed := seed) (ideal := ideal)) :=
   fun _ _ hεδ h adversary ha => (h adversary ha).trans (by exact_mod_cast hεδ)
 
 /-- Security against a larger class of adversaries implies security against a smaller class. -/
 theorem Secure.of_admissible {G : Generator Seed Output}
     {Admissible Restricted : Adversary Output → Prop} {ε : ℝ≥0}
-    (h : G.Secure Admissible ε) (hsub : ∀ adversary, Restricted adversary → Admissible adversary) :
-    G.Secure Restricted ε := fun adversary ha => h adversary (hsub adversary ha)
+    (h : G.Secure Admissible ε (seed := seed) (ideal := ideal))
+    (hsub : ∀ adversary, Restricted adversary → Admissible adversary) :
+    G.Secure Restricted ε (seed := seed) (ideal := ideal) :=
+  fun adversary ha => h adversary (hsub adversary ha)
 
 section RangeTests
 
+variable [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output]
+
 variable [DecidableEq Output]
 
 omit [Nonempty Seed] [Fintype Output] [Nonempty Output] in
@@ -109,7 +110,7 @@ omit [Nonempty Seed] in
 /-- The range test's acceptance probability under uniform sampling is the fraction
 of outputs in the range. -/
 theorem idealExperiment_rangeAdversary (G : Generator Seed Output) :
-    (idealExperiment G.rangeAdversary true).toReal =
+    (idealExperiment G.rangeAdversary (ideal := PMF.uniformOfFintype Output) true).toReal =
       Nat.card (Set.range G) / (Fintype.card Output : ℝ) := by
   simp only [idealExperiment, rangeAdversary, rangeTest, PMF.bind_apply, PMF.pure_apply,
     PMF.uniformOfFintype_apply, tsum_fintype]
@@ -121,11 +122,12 @@ theorem idealExperiment_rangeAdversary (G : Generator Seed Output) :
 theorem advantage_rangeAdversary (G : Generator Seed Output) :
     G.advantage G.rangeAdversary =
       1 - Nat.card (Set.range G) / (Fintype.card Output : ℝ) := by
-  have hprob : (idealExperiment G.rangeAdversary true).toReal ≤ 1 :=
+  have hprob :
+      (idealExperiment G.rangeAdversary (ideal := PMF.uniformOfFintype Output) true).toReal ≤ 1 :=
     (ENNReal.toReal_le_toReal (PMF.apply_ne_top _ _) ENNReal.one_ne_top).mpr
       (PMF.coe_le_one _ _)
   rw [advantage, realExperiment_rangeAdversary]
-  simp only [PMF.pure_apply, ↓reduceIte, ENNReal.toReal_one]
+  simp only [Game.advantage, Game.winProbability, PMF.pure_apply, ↓reduceIte, ENNReal.toReal_one]
   rw [abs_of_nonneg (sub_nonneg.mpr hprob), idealExperiment_rangeAdversary]
 
 /-- Every generator has an unbounded distinguisher with advantage at least
@@ -149,6 +151,8 @@ theorem not_secure_of_rangeAdversary (G : Generator Seed Output)
 
 end RangeTests
 
+variable [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output]
+
 /-- An expanding generator cannot be perfectly secure against arbitrary adversaries. -/
 theorem not_secure_zero_of_isExpanding (G : Generator Seed Output) (hG : G.IsExpanding) :
     ¬ G.Secure (fun _ => True) 0 := by
diff --git a/Cslib/Crypto/Primitives/PRG/Defs.lean b/Cslib/Crypto/Primitives/PRG/Defs.lean
index 24e1988b8a..1af04133f0 100644
--- a/Cslib/Crypto/Primitives/PRG/Defs.lean
+++ b/Cslib/Crypto/Primitives/PRG/Defs.lean
@@ -6,15 +6,20 @@ Authors: Samuel Schlesinger
 
 module
 
-public import Cslib.Init
-public import Mathlib.Probability.Distributions.Uniform
+public import Cslib.Crypto.Game
+-- The default-argument tactics use this import at their call sites.
+public import Mathlib.Probability.Distributions.Uniform -- shake: keep
 public import Mathlib.Probability.ProbabilityMassFunction.Constructions
 
 /-!
 # Pseudorandom generators: games and concrete security
 
 Attack Game 3.1 of [BonehShoup2023] compares a deterministic generator applied to a
-uniform seed with a uniform output. Adversaries are randomized Boolean tests. Security
+uniform seed with a uniform output. The experiments also accept explicit seed and ideal
+distributions, so the same definitions apply to infinite sample spaces and to intermediate
+distributions in reductions. Omitted distributions default to uniform sampling from the
+respective finite types.
+Adversaries are randomized Boolean tests. Security
 is relative to a caller-supplied predicate `Admissible`, with an explicit advantage bound.
 No computational model or efficiency assumption is built into the generator or the tests.
 
@@ -58,32 +63,37 @@ theorem coe_mk (f : Seed → Output) : ⇑(Generator.mk f) = f := rfl
 def IsExpanding [Fintype Seed] [Fintype Output] (_G : Generator Seed Output) : Prop :=
   Fintype.card Seed < Fintype.card Output
 
-variable [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output]
+/-- Apply the generator to a seed distribution, uniform by default on finite seed types. -/
+noncomputable def outputDist (G : Generator Seed Output)
+    (seed : PMF Seed := by exact PMF.uniformOfFintype _) : PMF Output :=
+  seed.map G
 
-/-- The distribution obtained by applying the generator to a uniform seed. -/
-noncomputable def outputDist (G : Generator Seed Output) : PMF Output :=
-  (PMF.uniformOfFintype Seed).map G
-
-/-- Experiment 0 of Attack Game 3.1: give the adversary a generated output. -/
+/-- Experiment 0 of Attack Game 3.1: generate from a seed, uniform by default. -/
 noncomputable def realExperiment (G : Generator Seed Output)
-    (adversary : Adversary Output) : PMF Bool :=
-  G.outputDist.bind adversary
+    (adversary : Adversary Output)
+    (seed : PMF Seed := by exact PMF.uniformOfFintype _) : Game :=
+  (G.outputDist (seed := seed)).bind adversary
 
-/-- Experiment 1 of Attack Game 3.1: give the adversary a uniform output. -/
-noncomputable def idealExperiment (adversary : Adversary Output) : PMF Bool :=
-  (PMF.uniformOfFintype Output).bind adversary
+/-- Experiment 1 of Attack Game 3.1: give the adversary an ideal sample, uniform by default. -/
+noncomputable def idealExperiment (adversary : Adversary Output)
+    (ideal : PMF Output := by exact PMF.uniformOfFintype _) : Game :=
+  ideal.bind adversary
 
 /-- The absolute difference of the probabilities of outputting `true` in the two
 experiments, as in Attack Game 3.1 of [BonehShoup2023]. -/
-noncomputable def advantage (G : Generator Seed Output) (adversary : Adversary Output) : ℝ :=
-  |(G.realExperiment adversary true).toReal - (idealExperiment adversary true).toReal|
+noncomputable def advantage (G : Generator Seed Output) (adversary : Adversary Output)
+    (seed : PMF Seed := by exact PMF.uniformOfFintype _)
+    (ideal : PMF Output := by exact PMF.uniformOfFintype _) : ℝ :=
+  Game.advantage (G.realExperiment adversary (seed := seed))
+    (idealExperiment adversary (ideal := ideal))
 
 /-- Concrete security against admissible adversaries. The predicate is supplied by the
 caller, for example to restrict tests to a chosen computational resource bound.
 Taking `Admissible := fun _ => True` allows arbitrary adversaries. -/
 def Secure (G : Generator Seed Output) (Admissible : Adversary Output → Prop)
-    (ε : ℝ≥0) : Prop :=
-  ∀ adversary, Admissible adversary → G.advantage adversary ≤ ε
+    (ε : ℝ≥0) (seed : PMF Seed := by exact PMF.uniformOfFintype _)
+    (ideal : PMF Output := by exact PMF.uniformOfFintype _) : Prop :=
+  ∀ adversary, Admissible adversary → G.advantage adversary (seed := seed) (ideal := ideal) ≤ ε
 
 end Generator
 end Cslib.Crypto.PRG
diff --git a/Cslib/Crypto/README.md b/Cslib/Crypto/README.md
index 4e3ab5d2e1..1b0f7d58d5 100644
--- a/Cslib/Crypto/README.md
+++ b/Cslib/Crypto/README.md
@@ -33,8 +33,11 @@ security of Boolean experiments.
 PMFs. `Generator.Secure G Admissible ε` bounds the distinguishing advantage of every
 admissible randomized test. `Family.SecureWithError` allows a parameter-dependent error bound;
 `Family.Secure` requires negligible advantage separately for each admissible family, using
-Mathlib's `SuperpolynomialDecay`. A negligible error bound implies this asymptotic notion.
+`Negligible`, Mathlib's `SuperpolynomialDecay` at natural parameters. A negligible error bound
+implies this asymptotic notion.
 The caller supplies `Admissible`; these definitions do not assert computational efficiency.
+The seed and ideal distributions are explicit parameters, defaulting to uniform sampling on
+finite types, so the same experiments apply to distributions on infinite types.
 
 The range-membership adversary has advantage exactly `1 - |range G| / |Output|`, and hence
 at least `1 - |Seed| / |Output|`. Any non-negligible lower bound on the image gap rules out
@@ -42,7 +45,8 @@ asymptotic security when the range-test family is admissible. The executable `ra
 requires `DecidableEq Output`. Bitstring families eventually stretching by at least one bit
 are consequently insecure against any class admitting this test, with both `Fin n → Bool`
 and `BitVec n` versions and nonexistence corollaries. Zero-error security against all tests
-is equivalent to exactly uniform output; the identity generator is a nonexpanding example.
+is equivalent to matching the ideal distribution; with the defaults, this means exactly uniform
+output. The identity generator is a nonexpanding example.
 
 ## Plans and notes
 
diff --git a/CslibTests/PRG.lean b/CslibTests/PRG.lean
index aaf4264efa..0a7c705189 100644
--- a/CslibTests/PRG.lean
+++ b/CslibTests/PRG.lean
@@ -20,11 +20,17 @@ example : (Generator.mk (id : Bool → Bool)).Secure (fun _ => True) 0 := by
   apply Generator.secure_zero_of_outputDist_eq
   exact PMF.map_id _
 
+-- Explicit distributions allow infinite ambient types and need not agree.
+example : (Generator.mk (id : ℕ → ℕ)).advantage (fun n => PMF.pure (decide (n = 0)))
+    (seed := PMF.pure 0) (ideal := PMF.pure 1) = 1 := by
+  simp [Generator.advantage, Generator.realExperiment, Generator.idealExperiment,
+    Generator.outputDist, Cslib.Crypto.Game.advantage, Cslib.Crypto.Game.winProbability]
+
 -- Zero-error security implies uniform output.
 example {Seed Output : Type*} [Fintype Seed] [Nonempty Seed]
     [Fintype Output] [Nonempty Output] (G : Generator Seed Output)
     (h : G.Secure (fun _ => True) 0) : G.outputDist = PMF.uniformOfFintype Output :=
-  G.secure_zero_iff_outputDist_eq_uniform.mp h
+  G.secure_zero_iff_outputDist_eq.mp h
 
 example (G : Generator Bool (Bool × Bool)) (Admissible : Adversary (Bool × Bool) → Prop)
     {ε δ : ℝ≥0} (hεδ : ε ≤ δ) (h : G.Secure Admissible ε) : G.Secure Admissible δ :=
@@ -64,7 +70,7 @@ example : Family.Secure (fun n => Generator.mk (id : (Fin n → Bool) → (Fin n
       (fun n => Generator.mk (id : (Fin n → Bool) → (Fin n → Bool)))
       (fun _ => True) (fun _ => 0) := by
     intro adversary_family _ n
-    simp [Generator.advantage, Generator.realExperiment, Generator.idealExperiment,
+    simp [Generator.realExperiment, Generator.idealExperiment,
       Generator.outputDist, PMF.map_id]
   exact h.secure (Asymptotics.superpolynomialDecay_zero _ _)
 

From 058e07b0ec415380866f4d1d8c4fea8f16830062 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <sgschlesinger@gmail.com>
Date: Sun, 4 Oct 2026 19:01:55 -0400
Subject: [PATCH 2/2] style(Crypto/PRG): trim simp arguments and reflow
 documentation

---
 Cslib/Crypto/Primitives/PRG/Asymptotic.lean | 2 +-
 Cslib/Crypto/Primitives/PRG/Basic.lean      | 4 ++--
 Cslib/Crypto/Primitives/PRG/Defs.lean       | 3 +--
 CslibTests/PRG.lean                         | 5 ++---
 4 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/Cslib/Crypto/Primitives/PRG/Asymptotic.lean b/Cslib/Crypto/Primitives/PRG/Asymptotic.lean
index 1d8a6b1330..1849839bfd 100644
--- a/Cslib/Crypto/Primitives/PRG/Asymptotic.lean
+++ b/Cslib/Crypto/Primitives/PRG/Asymptotic.lean
@@ -21,7 +21,7 @@ This model has a natural-number security parameter and no sampled public system
 Efficiency of generation and sampling is not asserted by these semantic definitions.
 Seed and ideal distributions can be supplied explicitly; their defaults are uniform on finite
 types. Security is stated through `Game.Secure`, so computational definitions over infinite
-sample spaces, such as words, can reuse these experiments.
+sample spaces can reuse these experiments.
 
 `SecureWithError` bounds every admissible family's advantage at parameter `n` by `ε n`.
 A negligible bound implies `Secure`.
diff --git a/Cslib/Crypto/Primitives/PRG/Basic.lean b/Cslib/Crypto/Primitives/PRG/Basic.lean
index a562a6d8b4..4eefc77970 100644
--- a/Cslib/Crypto/Primitives/PRG/Basic.lean
+++ b/Cslib/Crypto/Primitives/PRG/Basic.lean
@@ -63,8 +63,8 @@ theorem secure_zero_iff_outputDist_eq (G : Generator Seed Output) :
   refine ⟨fun h => ?_, fun h => G.secure_zero_of_outputDist_eq h _⟩
   ext output
   apply (ENNReal.toReal_eq_toReal_iff' (PMF.apply_ne_top _ _) (PMF.apply_ne_top _ _)).mp
-  simpa [advantage, Game.winProbability, realExperiment, idealExperiment, PMF.bind_apply,
-    PMF.pure_apply, sub_eq_zero] using h (fun x => PMF.pure (decide (x = output))) trivial
+  simpa [advantage, Game.winProbability, realExperiment, idealExperiment, sub_eq_zero] using
+    h (fun x => PMF.pure (decide (x = output))) trivial
 
 @[deprecated secure_zero_iff_outputDist_eq (since := "2026-10-03")]
 alias secure_zero_iff_outputDist_eq_uniform := secure_zero_iff_outputDist_eq
diff --git a/Cslib/Crypto/Primitives/PRG/Defs.lean b/Cslib/Crypto/Primitives/PRG/Defs.lean
index 1af04133f0..7d480a89b0 100644
--- a/Cslib/Crypto/Primitives/PRG/Defs.lean
+++ b/Cslib/Crypto/Primitives/PRG/Defs.lean
@@ -18,8 +18,7 @@ Attack Game 3.1 of [BonehShoup2023] compares a deterministic generator applied t
 uniform seed with a uniform output. The experiments also accept explicit seed and ideal
 distributions, so the same definitions apply to infinite sample spaces and to intermediate
 distributions in reductions. Omitted distributions default to uniform sampling from the
-respective finite types.
-Adversaries are randomized Boolean tests. Security
+respective finite types. Adversaries are randomized Boolean tests. Security
 is relative to a caller-supplied predicate `Admissible`, with an explicit advantage bound.
 No computational model or efficiency assumption is built into the generator or the tests.
 
diff --git a/CslibTests/PRG.lean b/CslibTests/PRG.lean
index 0a7c705189..b6ac6b7aac 100644
--- a/CslibTests/PRG.lean
+++ b/CslibTests/PRG.lean
@@ -24,7 +24,7 @@ example : (Generator.mk (id : Bool → Bool)).Secure (fun _ => True) 0 := by
 example : (Generator.mk (id : ℕ → ℕ)).advantage (fun n => PMF.pure (decide (n = 0)))
     (seed := PMF.pure 0) (ideal := PMF.pure 1) = 1 := by
   simp [Generator.advantage, Generator.realExperiment, Generator.idealExperiment,
-    Generator.outputDist, Cslib.Crypto.Game.advantage, Cslib.Crypto.Game.winProbability]
+    Generator.outputDist, Cslib.Crypto.Game.winProbability]
 
 -- Zero-error security implies uniform output.
 example {Seed Output : Type*} [Fintype Seed] [Nonempty Seed]
@@ -70,8 +70,7 @@ example : Family.Secure (fun n => Generator.mk (id : (Fin n → Bool) → (Fin n
       (fun n => Generator.mk (id : (Fin n → Bool) → (Fin n → Bool)))
       (fun _ => True) (fun _ => 0) := by
     intro adversary_family _ n
-    simp [Generator.realExperiment, Generator.idealExperiment,
-      Generator.outputDist, PMF.map_id]
+    simp [Generator.realExperiment, Generator.idealExperiment, Generator.outputDist]
   exact h.secure (Asymptotics.superpolynomialDecay_zero _ _)
 
 -- The inverse-polynomial gap 1 / (n + 2) rules out asymptotic security.