feat(Crypto): relate security games to statistical distance

Cslib.lean

@@ -101,10 +101,12 @@ public import Cslib.Computability.URM.StandardForm
 public import Cslib.Computability.URM.StraightLine
 public import Cslib.Crypto.Game
 public import Cslib.Crypto.Game.Hybrid
+public import Cslib.Crypto.Game.Statistical
 public import Cslib.Crypto.Negligible
 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.Primitives.PRG.Statistical
 public import Cslib.Crypto.Protocols.Commitment.Basic
 public import Cslib.Crypto.Protocols.Commitment.Defs
 public import Cslib.Crypto.Protocols.Commitment.Scheme

Cslib/Crypto/Game/Statistical.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.Crypto.Game
+public import Cslib.Probability.StatisticalDistance
+
+/-!
+# Statistical security and Boolean games
+
+For Boolean experiments, distinguishing advantage is exactly statistical distance. A randomized
+test cannot increase this distance, even on an infinite sample type. Consequently statistically
+indistinguishable ensembles are secure against every family of tests, with no efficiency assumption.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto
+
+open Probability.PMF
+open scoped NNReal
+
+/-- The absolute difference of acceptance probabilities is precisely statistical distance
+for Boolean experiments. -/
+theorem Game.advantage_eq_dist (real ideal : Game) : advantage real ideal = dist real ideal := by
+  have hfalse (p : PMF Bool) : (p false).toReal = 1 - (p true).toReal := by
+    rw [← sum_toReal p, Fintype.sum_bool, add_sub_cancel_left]
+  rw [dist_eq, Fintype.sum_bool, hfalse, hfalse, sub_sub_sub_cancel_left,
+    abs_sub_comm (ideal true).toReal, add_self_div_two]
+
+/-- No randomized Boolean test distinguishes better than the statistical distance. -/
+theorem Game.advantage_bind_le_dist {α : Type*} (real ideal : PMF α) (test : α → Game) :
+    advantage (real.bind test) (ideal.bind test) ≤ dist real ideal :=
+  (advantage_eq_dist _ _).trans_le (dist_bind_le real ideal test)
+
+/-- A statistical-closeness bound is an advantage bound for every randomized test. -/
+theorem Game.advantage_le_of_statisticallyClose {α : Type*} {real ideal : PMF α} {ε : ℝ≥0}
+    (h : StatisticallyClose real ideal ε) (test : α → Game) :
+    advantage (real.bind test) (ideal.bind test) ≤ ε :=
+  (advantage_bind_le_dist real ideal test).trans h
+
+/-- Two discrete ensembles are statistically indistinguishable when their statistical distance
+is negligible. Neither their ambient type nor their supports need be finite. -/
+def StatisticallyIndistinguishable {α : ℕ → Type*} (X Y : ∀ n, PMF (α n)) : Prop :=
+  Negligible (fun n => dist (X n) (Y n))
+
+namespace StatisticallyIndistinguishable
+
+variable {α β : ℕ → Type*} {X Y Z : ∀ n, PMF (α n)}
+
+/-- An ensemble is statistically indistinguishable from itself. -/
+theorem refl (X : ∀ n, PMF (α n)) : StatisticallyIndistinguishable X X := by
+  simp [StatisticallyIndistinguishable]
+
+/-- Statistical indistinguishability is symmetric. -/
+theorem symm (h : StatisticallyIndistinguishable X Y) : StatisticallyIndistinguishable Y X := by
+  simpa [StatisticallyIndistinguishable, dist_comm] using h
+
+/-- Statistical errors add across a game hop. -/
+theorem trans (hXY : StatisticallyIndistinguishable X Y)
+    (hYZ : StatisticallyIndistinguishable Y Z) : StatisticallyIndistinguishable X Z :=
+  negligible_of_le (hXY.add hYZ) (fun _ => dist_nonneg) (fun _ => dist_triangle _ _ _)
+
+/-- Arbitrary randomized postprocessing preserves statistical indistinguishability. -/
+theorem bind (h : StatisticallyIndistinguishable X Y) (kernel : ∀ n, α n → PMF (β n)) :
+    StatisticallyIndistinguishable (fun n => (X n).bind (kernel n))
+      (fun n => (Y n).bind (kernel n)) :=
+  negligible_of_le h (fun _ => dist_nonneg) (fun _ => dist_bind_le _ _ _)
+
+/-- Deterministic postprocessing preserves statistical indistinguishability. -/
+theorem map (h : StatisticallyIndistinguishable X Y) (f : ∀ n, α n → β n) :
+    StatisticallyIndistinguishable (fun n => (X n).map (f n)) (fun n => (Y n).map (f n)) :=
+  negligible_of_le h (fun _ => dist_nonneg) (fun _ => dist_map_le _ _ _)
+
+/-- Statistical indistinguishability implies security against any chosen class of tests.
+The test may depend arbitrarily on the security parameter. -/
+theorem secure (h : StatisticallyIndistinguishable X Y) {Adversary : Type*}
+    (test : Adversary → (n : ℕ) → α n → Game) (Admissible : Adversary → Prop) :
+    Game.Secure (fun adversary n => (X n).bind (test adversary n))
+      (fun adversary n => (Y n).bind (test adversary n)) Admissible := fun _ _ =>
+  negligible_of_le h (fun _ => Game.advantage_nonneg _ _)
+    (fun _ => Game.advantage_bind_le_dist _ _ _)
+
+end StatisticallyIndistinguishable
+end Cslib.Crypto

Cslib/Crypto/Primitives/PRG/Statistical.lean

@@ -0,0 +1,47 @@
+/-
+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.Asymptotic
+public import Cslib.Crypto.Game.Statistical
+
+/-!
+# Statistical bounds for pseudorandom-generator games
+
+The same statistical-distance bound controls every randomized test, on finite or infinite
+sample types. The family theorem is a direct instance of the common semantic game calculus.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.PRG
+
+open Probability.PMF
+open scoped NNReal
+
+/-- Every test's advantage is bounded by the statistical distance of generated and ideal samples. -/
+theorem Generator.advantage_le_dist {Seed Output : Type*} (G : Generator Seed Output)
+    (adversary : Adversary Output) (seed : PMF Seed) (ideal : PMF Output) :
+    G.advantage adversary seed ideal ≤ dist (G.outputDist seed) ideal :=
+  Game.advantage_bind_le_dist _ _ _
+
+/-- A statistical bound gives concrete security for any chosen class of adversaries. -/
+theorem Generator.secure_of_statisticallyClose {Seed Output : Type*} (G : Generator Seed Output)
+    {seed : PMF Seed} {ideal : PMF Output} {ε : ℝ≥0}
+    (h : StatisticallyClose (G.outputDist seed) ideal ε) (Admissible : Adversary Output → Prop) :
+    G.Secure Admissible ε seed ideal :=
+  fun adversary _ => (G.advantage_le_dist adversary seed ideal).trans h
+
+/-- Negligible statistical distance implies asymptotic security for every test family. -/
+theorem Family.secure_of_statisticallyIndistinguishable {Seed Output : ℕ → Type*}
+    (G : Family Seed Output) {seed : ∀ n, PMF (Seed n)} {ideal : ∀ n, PMF (Output n)}
+    (h : StatisticallyIndistinguishable (fun n => (G n).outputDist (seed n)) ideal)
+    (Admissible : (∀ n, Adversary (Output n)) → Prop) :
+    G.Secure Admissible seed ideal :=
+  h.secure (fun adversary => adversary) Admissible
+
+end Cslib.Crypto.PRG

Cslib/Crypto/README.md

@@ -26,6 +26,8 @@ parameters, with zero, comparison, and polynomial-loss bounds.
 [`Game`](Game.lean) gives the acceptance probability, distinguishing advantage and negligible
 security of Boolean experiments.
 [`Game/Hybrid`](Game/Hybrid.lean) supplies hybrid arguments with polynomially many hops.
+[`Game/Statistical`](Game/Statistical.lean) identifies Boolean advantage with statistical
+distance, so a statistical approximation can be one hop of a computational argument.
 
 ## Pseudorandom generators
 

CslibTests/PRG.lean

@@ -4,13 +4,32 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
 
-import Cslib.Crypto.Primitives.PRG.Asymptotic
+import Cslib.Crypto.Primitives.PRG.Statistical
 
 open Cslib.Crypto.PRG Filter
 open scoped NNReal Topology
 
 namespace CslibTests.PRG
 
+open Cslib.Crypto Cslib.Probability.PMF
+
+-- Statistical distance and its security consequences need no finite ambient type.
+example : dist (PMF.pure (0 : ℕ)) (PMF.pure 1) = 1 := by
+  apply dist_eq_one_of_disjoint_support
+  simp
+
+example (p q : PMF ℕ) {ε : ℝ≥0} (h : StatisticallyClose p q ε) :
+    (Generator.mk (id : ℕ → ℕ)).Secure (fun _ => True) ε p q := by
+  apply Generator.secure_of_statisticallyClose
+  simpa [Generator.outputDist, PMF.map_id] using h
+
+-- The same asymptotic theorem handles sample spaces depending on the parameter.
+example (samples : ∀ n : ℕ, PMF (Fin (n + 1))) :
+    Family.Secure (fun n => Generator.mk (id : Fin (n + 1) → Fin (n + 1)))
+      (fun _ => True) samples samples := by
+  apply Family.secure_of_statisticallyIndistinguishable
+  simpa [Generator.outputDist, PMF.map_id] using StatisticallyIndistinguishable.refl samples
+
 -- 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