refactor(Crypto/PRG): allow explicit seed and ideal distributions

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 can reuse these experiments.
 
 `SecureWithError` bounds every admissible family's advantage at parameter `n` by `ε n`.
 A negligible bound implies `Secure`.
@@ -41,65 +44,61 @@ 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
 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
   intro h
   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. -/

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, 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

Cslib/Crypto/Primitives/PRG/Defs.lean

@@ -6,15 +6,19 @@ 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 +62,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

Cslib/Crypto/README.md

@@ -33,16 +33,20 @@ 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
 asymptotic security when the range-test family is admissible. The executable `rangeTest`
 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