diff --git a/Cslib.lean b/Cslib.lean
index 34a0d27bef..31e2bfac6b 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -57,6 +57,9 @@ public import Cslib.Computability.URM.Defs
 public import Cslib.Computability.URM.Execution
 public import Cslib.Computability.URM.StandardForm
 public import Cslib.Computability.URM.StraightLine
+public import Cslib.Crypto.Primitives.PRG.Asymptotic
+public import Cslib.Crypto.Primitives.PRG.Basic
+public import Cslib.Crypto.Primitives.PRG.Defs
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Basic
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption
diff --git a/Cslib/Crypto/Primitives/PRG/Asymptotic.lean b/Cslib/Crypto/Primitives/PRG/Asymptotic.lean
new file mode 100644
index 0000000000..6e83058a24
--- /dev/null
+++ b/Cslib/Crypto/Primitives/PRG/Asymptotic.lean
@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+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
+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.
+
+If the range test is admissible and the seed space is eventually at most half the output
+space, security is impossible: the advantage is eventually at least one half. In particular,
+no family stretching bitstrings by at least one bit is secure against arbitrary adversaries.
+Mere strict cardinality expansion for arbitrary finite spaces would not give this constant
+gap, which is why the asymptotic theorem states the quantitative hypothesis explicitly.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.PRG
+
+open Filter
+open scoped Topology
+
+/-- A security-parameter-indexed collection of deterministic generators. -/
+abbrev Family (Seed Output : ℕ → Type*) := ∀ n, Generator (Seed n) (Output n)
+
+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, Admissible adversary →
+    Asymptotics.SuperpolynomialDecay atTop (fun n : ℕ => (n : ℝ))
+      (fun n => (G n).advantage (adversary n))
+
+/-- 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) (hsub : ∀ adversary, Restricted adversary → Admissible adversary) :
+    G.Secure Restricted := fun adversary ha => h adversary (hsub adversary ha)
+
+/-- A constant positive lower bound on the range test's advantage rules out security. -/
+theorem not_secure_of_rangeAdversary (G : Family Seed Output)
+    {Admissible : (∀ n, Adversary (Output n)) → Prop}
+    (ha : Admissible (fun n => (G n).rangeAdversary))
+    {δ : ℝ} (hδ : 0 < δ)
+    (hgap : ∀ᶠ n in atTop,
+      δ ≤ 1 - Fintype.card (Seed n) / (Fintype.card (Output n) : ℝ)) :
+    ¬ G.Secure Admissible := by
+  intro h
+  have hlim : Tendsto (fun n => (G n).advantage (G n).rangeAdversary) atTop (𝓝 0) := by
+    simpa using h _ ha 0
+  have hle : δ ≤ 0 := ge_of_tendsto hlim (hgap.mono fun n hn =>
+    hn.trans (G n).one_sub_card_div_le_advantage_rangeAdversary)
+  exact hδ.not_ge hle
+
+/-- If the output space is eventually at least twice as large as the seed space,
+then security against arbitrary adversaries is impossible. -/
+theorem not_secure_of_two_mul_card_le (G : Family Seed Output)
+    (hsize : ∀ᶠ n in atTop, 2 * Fintype.card (Seed n) ≤ Fintype.card (Output n)) :
+    ¬ G.Secure (fun _ => True) := by
+  apply G.not_secure_of_rangeAdversary trivial (δ := 1 / 2) (by norm_num)
+  filter_upwards [hsize] with n hn
+  have hpos : (0 : ℝ) < Fintype.card (Output n) := by exact_mod_cast Fintype.card_pos
+  have hcard : 2 * (Fintype.card (Seed n) : ℝ) ≤ Fintype.card (Output n) := by
+    exact_mod_cast hn
+  have hratio : Fintype.card (Seed n) / (Fintype.card (Output n) : ℝ) ≤ 1 / 2 :=
+    (div_le_iff₀ hpos).mpr (by linarith)
+  linarith
+
+/-- No bitstring generator family stretching by at least one bit is secure against
+arbitrary adversaries, even when stretching is only required eventually. -/
+theorem not_secure_of_bitstring_stretch {seedLength outputLength : ℕ → ℕ}
+    (G : Family (fun n => Fin (seedLength n) → Bool) (fun n => Fin (outputLength n) → Bool))
+    (hstretch : ∀ᶠ n in atTop, seedLength n < outputLength n) :
+    ¬ G.Secure (fun _ => True) := by
+  apply G.not_secure_of_two_mul_card_le
+  filter_upwards [hstretch] with n hn
+  simp only [Fintype.card_fun, Fintype.card_bool, Fintype.card_fin]
+  calc
+    2 * 2 ^ seedLength n = 2 ^ (seedLength n + 1) := by rw [pow_succ, mul_comm]
+    _ ≤ 2 ^ outputLength n := Nat.pow_le_pow_right (by decide) hn
+
+/-- No family that eventually stretches bitstrings is secure against arbitrary adversaries. -/
+theorem not_exists_secure_bitstring_stretch {seedLength outputLength : ℕ → ℕ}
+    (hstretch : ∀ᶠ n in atTop, seedLength n < outputLength n) :
+    ¬ ∃ G : Family (fun n => Fin (seedLength n) → Bool)
+      (fun n => Fin (outputLength n) → Bool), G.Secure (fun _ => True) := by
+  rintro ⟨G, hG⟩
+  exact G.not_secure_of_bitstring_stretch hstretch hG
+
+/-- The impossibility of stretching against arbitrary adversaries, using `BitVec`. -/
+theorem not_secure_of_bitVec_stretch {seedLength outputLength : ℕ → ℕ}
+    (G : Family (fun n => BitVec (seedLength n)) (fun n => BitVec (outputLength n)))
+    (hstretch : ∀ᶠ n in atTop, seedLength n < outputLength n) :
+    ¬ G.Secure (fun _ => True) := by
+  apply G.not_secure_of_two_mul_card_le
+  filter_upwards [hstretch] with n hn
+  simp only [← FinEnum.card_eq_fintypeCard, FinEnum.card_bitVec]
+  calc
+    2 * 2 ^ seedLength n = 2 ^ (seedLength n + 1) := by rw [pow_succ, mul_comm]
+    _ ≤ 2 ^ outputLength n := Nat.pow_le_pow_right (by decide) hn
+
+/-- There is no secure expanding `BitVec` generator family against arbitrary adversaries. -/
+theorem not_exists_secure_bitVec_stretch {seedLength outputLength : ℕ → ℕ}
+    (hstretch : ∀ᶠ n in atTop, seedLength n < outputLength n) :
+    ¬ ∃ G : Family (fun n => BitVec (seedLength n)) (fun n => BitVec (outputLength n)),
+      G.Secure (fun _ => True) := by
+  rintro ⟨G, hG⟩
+  exact G.not_secure_of_bitVec_stretch hstretch hG
+
+end Family
+end Cslib.Crypto.PRG
diff --git a/Cslib/Crypto/Primitives/PRG/Basic.lean b/Cslib/Crypto/Primitives/PRG/Basic.lean
new file mode 100644
index 0000000000..3f8328c6f0
--- /dev/null
+++ b/Cslib/Crypto/Primitives/PRG/Basic.lean
@@ -0,0 +1,158 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Crypto.Primitives.PRG.Defs
+
+/-!
+# Pseudorandom generators against arbitrary adversaries
+
+The range-membership test accepts every generated output, whereas it accepts a uniform
+output with probability `|range G| / |Output|`. Its advantage is therefore at least
+`1 - |Seed| / |Output|`. This proves that an expanding generator cannot have zero
+advantage against arbitrary adversaries, and gives a quantitative obstruction for
+every smaller error bound. No injectivity assumption on the generator is needed.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.PRG.Generator
+
+open scoped NNReal
+
+variable {Seed Output : Type*}
+
+/-- An unbounded adversary tests whether its input is in the generator's range.
+It is not assumed to be admissible for a computationally restricted class. -/
+noncomputable def rangeAdversary (G : Generator Seed Output) : Adversary Output := by
+  classical
+  exact fun output => PMF.pure (decide (output ∈ Set.range G))
+
+variable [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output]
+
+/-- Advantage is nonnegative. -/
+theorem advantage_nonneg (G : Generator Seed Output) (adversary : Adversary Output) :
+    0 ≤ G.advantage adversary := abs_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)]
+
+/-- 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
+
+/-- 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
+  simp [advantage, realExperiment, idealExperiment, PMF.bind_const]
+
+/-- A generator with exactly uniform output is secure with zero error 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
+  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
+  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
+
+/-- Enlarging the allowed advantage preserves security. -/
+theorem Secure.mono {G : Generator Seed Output} {Admissible : Adversary Output → Prop} :
+    Monotone (G.Secure Admissible) :=
+  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)
+
+omit [Fintype Output] [Nonempty Output] in
+/-- The range test always accepts a generated output. -/
+@[simp]
+theorem realExperiment_rangeAdversary (G : Generator Seed Output) :
+    G.realExperiment G.rangeAdversary = PMF.pure true := by
+  simp [realExperiment, outputDist, PMF.bind_map, rangeAdversary, Function.comp_def,
+    PMF.bind_const]
+
+omit [Fintype Seed] [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 =
+      Nat.card (Set.range G) / (Fintype.card Output : ℝ) := by
+  classical
+  simp only [idealExperiment, rangeAdversary, PMF.bind_apply, PMF.pure_apply,
+    PMF.uniformOfFintype_apply, tsum_fintype]
+  simp only [mul_ite, mul_one, mul_zero, eq_comm (a := true), decide_eq_true_eq]
+  rw [← Finset.sum_filter]
+  simp [Nat.card_eq_fintype_card, Fintype.card_subtype, div_eq_mul_inv]
+
+/-- The exact advantage of the range-membership adversary. -/
+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 :=
+    (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]
+  rw [abs_of_nonneg (sub_nonneg.mpr hprob), idealExperiment_rangeAdversary]
+
+/-- Every generator has an unbounded distinguisher with advantage at least
+`1 - |Seed| / |Output|`. Collisions can only improve this attack. -/
+theorem one_sub_card_div_le_advantage_rangeAdversary (G : Generator Seed Output) :
+    1 - Fintype.card Seed / (Fintype.card Output : ℝ) ≤
+      G.advantage G.rangeAdversary := by
+  classical
+  rw [advantage_rangeAdversary]
+  have hcard : Nat.card (Set.range G) ≤ Fintype.card Seed := by
+    simpa using Fintype.card_range_le G
+  gcongr
+
+/-- Security is impossible below the range-test bound whenever that test is admissible. -/
+theorem not_secure_of_rangeAdversary (G : Generator Seed Output)
+    {Admissible : Adversary Output → Prop} {ε : ℝ≥0}
+    (ha : Admissible G.rangeAdversary)
+    (hε : (ε : ℝ) < 1 - Fintype.card Seed / (Fintype.card Output : ℝ)) :
+    ¬ G.Secure Admissible ε := by
+  intro h
+  exact (hε.trans_le G.one_sub_card_div_le_advantage_rangeAdversary).not_ge (h _ ha)
+
+/-- 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
+  apply G.not_secure_of_rangeAdversary trivial
+  have hpos : (0 : ℝ) < Fintype.card Output := by exact_mod_cast Fintype.card_pos
+  have hlt : (Fintype.card Seed : ℝ) < Fintype.card Output := by exact_mod_cast hG
+  simpa using sub_pos.mpr ((div_lt_one hpos).mpr hlt)
+
+/-- There is no expanding, perfectly secure generator against arbitrary adversaries. -/
+theorem not_exists_isExpanding_secure_zero :
+    ¬ ∃ G : Generator Seed Output, G.IsExpanding ∧ G.Secure (fun _ => True) 0 := by
+  rintro ⟨G, hG, hsecure⟩
+  exact G.not_secure_zero_of_isExpanding hG hsecure
+
+end Cslib.Crypto.PRG.Generator
diff --git a/Cslib/Crypto/Primitives/PRG/Defs.lean b/Cslib/Crypto/Primitives/PRG/Defs.lean
new file mode 100644
index 0000000000..24e1988b8a
--- /dev/null
+++ b/Cslib/Crypto/Primitives/PRG/Defs.lean
@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Probability.Distributions.Uniform
+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
+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.
+
+`Generator.IsExpanding` records the cardinality condition separately from security.
+In particular, a generator need not expand, and an expanding generator need not be secure.
+
+## References
+
+* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*,
+  Version 0.6][BonehShoup2023], Section 3.1.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.PRG
+
+open scoped NNReal
+
+/-- A deterministic generator with seed space `Seed` and output space `Output`.
+Efficiency, expansion, and security are separate properties. -/
+@[ext]
+structure Generator (Seed Output : Type*) where
+  /-- Generate an output from a seed. -/
+  toFun : Seed → Output
+
+/-- A randomized statistical test on the output space. -/
+abbrev Adversary (Output : Type*) := Output → PMF Bool
+
+namespace Generator
+
+variable {Seed Output : Type*}
+
+instance : FunLike (Generator Seed Output) Seed Output where
+  coe G := G.toFun
+  coe_injective _ _ h := Generator.ext h
+
+@[simp]
+theorem coe_mk (f : Seed → Output) : ⇑(Generator.mk f) = f := rfl
+
+/-- A generator expands when its output space is strictly larger than its seed space. -/
+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]
+
+/-- 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. -/
+noncomputable def realExperiment (G : Generator Seed Output)
+    (adversary : Adversary Output) : PMF Bool :=
+  G.outputDist.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
+
+/-- 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|
+
+/-- 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 ≤ ε
+
+end Generator
+end Cslib.Crypto.PRG
diff --git a/Cslib/Crypto/README.md b/Cslib/Crypto/README.md
index 75ffac5366..8f404c092f 100644
--- a/Cslib/Crypto/README.md
+++ b/Cslib/Crypto/README.md
@@ -19,6 +19,24 @@ The aim is to build end-to-end models where cryptographic operations appear insi
 
 To this end, we expect to leverage the combination of `Crypto` and [Languages](../Languages) to define and formally reason about security protocols. CSLib's common semantics APIs connecting [Languages](../Languages) and [Logics](../Logics) should enable such reasoning.
 
+## Pseudorandom generators
+
+[`Primitives/PRG`](Primitives/PRG) formalizes Boneh and Shoup's Attack Game 3.1 using
+PMFs. `Generator.Secure G Admissible ε` bounds the distinguishing advantage of every
+admissible randomized test. `Family.Secure` requires negligible advantage for each
+admissible adversary family, using Mathlib's `SuperpolynomialDecay`. The caller supplies
+`Admissible`; these definitions do not by themselves assert computational efficiency.
+
+The range-membership adversary has advantage at least `1 - |Seed| / |Output|`.
+Consequently, strictly expanding generators cannot have zero error against arbitrary
+adversaries, and bitstring generator families stretching by at least one bit cannot have
+negligible advantage against arbitrary adversary families. The latter statement also
+allows stretching to hold only eventually. The identity generator provides a nonexpanding
+example with zero advantage.
+
+Zero-error security against all tests is equivalent to exactly uniform output.
+The bitstring impossibility theorem is available for both `Fin n → Bool` and `BitVec n`.
+
 ## Plans and notes
 
 - We plan on developing applied calculi and logics for modelling and reasoning about security protocols.
diff --git a/CslibTests.lean b/CslibTests.lean
index 94af0f1566..68feece4ed 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -18,5 +18,6 @@ import CslibTests.MLL
 import CslibTests.Modal
 import CslibTests.Modal.Ideal
 import CslibTests.Modal.Stlc
+import CslibTests.PRG
 import CslibTests.Reduction
 import CslibTests.StatefulProcesses
diff --git a/CslibTests/PRG.lean b/CslibTests/PRG.lean
new file mode 100644
index 0000000000..c6dc1e8a4b
--- /dev/null
+++ b/CslibTests/PRG.lean
@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Cslib.Crypto.Primitives.PRG.Asymptotic
+
+open Cslib.Crypto.PRG
+open scoped NNReal
+
+namespace CslibTests.PRG
+
+-- Generators support ordinary function application and extensionality.
+example {Seed Output : Type*} (G H : Generator Seed Output)
+    (h : ∀ seed, G seed = H seed) : G = H := DFunLike.ext G H h
+
+-- A nonexpanding generator can be perfectly secure, even against randomized tests.
+example : (Generator.mk (id : Bool → Bool)).Secure (fun _ => True) 0 := by
+  apply Generator.secure_zero_of_outputDist_eq
+  exact PMF.map_id _
+
+-- The game-based definition recovers distribution equality without an error term.
+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
+
+example (G : Generator Bool (Bool × Bool)) (Admissible : Adversary (Bool × Bool) → Prop)
+    {ε δ : ℝ≥0} (hεδ : ε ≤ δ) (h : G.Secure Admissible ε) : G.Secure Admissible δ :=
+  Generator.Secure.mono hεδ h
+
+-- Admissibility can express an actual restricted class: tests ignoring their input.
+example (G : Generator Bool (Bool × Bool)) :
+    G.Secure (fun adversary => ∃ p : PMF Bool, adversary = fun _ => p) 0 := by
+  rintro adversary ⟨p, rfl⟩
+  simp
+
+-- Repeating a bit expands, and the range attack has exactly one-half advantage.
+example : (Generator.mk (fun b : Bool => (b, b))).advantage
+    (Generator.mk (fun b : Bool => (b, b))).rangeAdversary = 1 / 2 := by
+  norm_num [Generator.advantage_rangeAdversary, Nat.card_eq_fintype_card]
+
+-- Collisions strengthen the attack: the range, not the number of seeds, determines advantage.
+example : (Generator.mk (fun _ : Bool => (false, false))).advantage
+    (Generator.mk (fun _ : Bool => (false, false))).rangeAdversary = 3 / 4 := by
+  rw [Generator.advantage_rangeAdversary]
+  norm_num [Set.range_const]
+
+-- The finite impossibility theorem applies without choosing any implementation.
+example : ¬ ∃ G : Generator Bool (Bool × Bool), G.Secure (fun _ => True) 0 := by
+  rintro ⟨G, hG⟩
+  exact G.not_secure_zero_of_isExpanding (by simp [Generator.IsExpanding]) hG
+
+-- The asymptotic definition admits the identity family.
+example : Family.Secure (fun n => Generator.mk (id : (Fin n → Bool) → (Fin n → Bool)))
+    (fun _ => True) := by
+  intro adversary _
+  have hzero : ∀ n, (Generator.mk (id : (Fin n → Bool) → (Fin n → Bool))).advantage
+      (adversary n) = 0 := by
+    intro n
+    simp [Generator.advantage, Generator.realExperiment, Generator.idealExperiment,
+      Generator.outputDist, PMF.map_id]
+  simp only [hzero]
+  exact Asymptotics.superpolynomialDecay_zero _ _
+
+-- No n-to-(n+1)-bit generator resists arbitrary adversary families.
+example : ¬ ∃ G : Family (fun n => Fin n → Bool) (fun n => Fin (n + 1) → Bool),
+    G.Secure (fun _ => True) :=
+  Family.not_exists_secure_bitstring_stretch (Filter.Eventually.of_forall (by omega))
+
+-- The same result uses the BitVec representation of the existing one-time pad API.
+example : ¬ ∃ G : Family BitVec (fun n => BitVec (n + 1)), G.Secure (fun _ => True) :=
+  Family.not_exists_secure_bitVec_stretch (Filter.Eventually.of_forall (by omega))
+
+end CslibTests.PRG
diff --git a/references.bib b/references.bib
index 7fdb409d20..b63b276e4c 100644
--- a/references.bib
+++ b/references.bib
@@ -552,6 +552,14 @@ @book{AroraBarak09
   year         = {2009},
 }
 
+@misc{BonehShoup2023,
+  author       = {Dan Boneh and Victor Shoup},
+  title        = {A Graduate Course in Applied Cryptography},
+  year         = {2023},
+  note         = {Version 0.6},
+  url          = {https://crypto.stanford.edu/~dabo/cryptobook/BonehShoup_0_6.pdf}
+}
+
 @book{Papadimitriou94,
   title={Computational Complexity},
   author={Papadimitriou, Christos H.},