chore: bump mathlib to be31cde, fix breaking changes

Cslib.lean

@@ -121,6 +121,7 @@ public import Cslib.Foundations.Control.Monad.IsMonadHom
 public import Cslib.Foundations.Control.Monad.IsMonadHom.List
 public import Cslib.Foundations.Data.BiTape
 public import Cslib.Foundations.Data.BitString
+public import Cslib.Foundations.Data.BitVec
 public import Cslib.Foundations.Data.DecidableEqZero
 public import Cslib.Foundations.Data.FinFun.Basic
 public import Cslib.Foundations.Data.FinFun.Update
@@ -253,6 +254,6 @@ public import Cslib.MachineLearning.PACLearning.Defs
 public import Cslib.MachineLearning.PACLearning.VCDimension
 public import Cslib.MachineLearning.PACLearning.VersionSpace
 public import Cslib.MachineLearning.PACLearning.VersionSpaceLattice
-public import Cslib.Probability.PMF
+public import Cslib.Probability.Measure
 public import Cslib.Probability.StatisticalDistance
 public import Cslib.Tactic.GrindAttrs

Cslib/Crypto/Primitives/PRG/Asymptotic.lean

@@ -7,6 +7,7 @@ Authors: Samuel Schlesinger
 module
 
 public import Cslib.Crypto.Primitives.PRG.Basic
+public import Cslib.Foundations.Data.BitVec
 public import Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
 public import Mathlib.Data.FinEnum
 
@@ -41,6 +42,8 @@ abbrev Family (Seed Output : ℕ → Type*) := ∀ n, Generator (Seed n) (Output
 namespace Family
 
 variable {Seed Output : ℕ → Type*}
+variable [∀ n, MeasurableSpace (Seed n)]
+variable [∀ n, MeasurableSpace (Output n)]
 variable [∀ n, Fintype (Seed n)] [∀ n, Nonempty (Seed n)]
 variable [∀ n, Fintype (Output n)] [∀ n, Nonempty (Output n)]
 
@@ -80,6 +83,7 @@ theorem SecureWithError.secure {G : Family Seed Output}
 
 section RangeTests
 
+variable [∀ n, MeasurableSingletonClass (Seed n)] [∀ n, MeasurableSingletonClass (Output n)]
 variable [∀ n, DecidableEq (Output n)]
 
 /-- A non-negligible lower bound on the fraction of outputs outside the image rules out

Cslib/Crypto/Primitives/PRG/Basic.lean

@@ -22,12 +22,16 @@ every smaller error bound. No injectivity assumption on the generator is needed.
 
 namespace Cslib.Crypto.PRG.Generator
 
+open MeasureTheory ProbabilityTheory Cslib.Probability.Measure
 open scoped NNReal
 
 variable {Seed Output : Type*}
 
+variable [MeasurableSpace Seed] [MeasurableSingletonClass Seed]
+variable [MeasurableSpace Output] [MeasurableSingletonClass Output]
 variable [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output]
 
+omit [MeasurableSingletonClass Seed] [MeasurableSingletonClass Output] in
 /-- Advantage is nonnegative. -/
 theorem advantage_nonneg (G : Generator Seed Output) (adversary : Adversary Output) :
     0 ≤ G.advantage adversary := abs_nonneg _
@@ -36,47 +40,54 @@ theorem advantage_nonneg (G : Generator Seed Output) (adversary : Adversary Outp
 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)
+    (prob_le_one (μ := G.realExperiment adversary) (s := {true}))
   have hideal := ENNReal.toReal_mono ENNReal.one_ne_top
-    (PMF.coe_le_one (idealExperiment adversary) true)
+    (prob_le_one (μ := idealExperiment adversary) (s := {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)]
+  · 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
 
+omit [MeasurableSingletonClass Output] in
 /-- A test whose output distribution is independent of its input has zero advantage. -/
 @[simp]
-theorem advantage_const (G : Generator Seed Output) (p : PMF Bool) :
+theorem advantage_const (G : Generator Seed Output) (p : ProbabilityMeasure Bool) :
     G.advantage (fun _ => p) = 0 := by
-  simp [advantage, realExperiment, idealExperiment, PMF.bind_const]
+  simp [advantage, realExperiment, idealExperiment, Measure.bind_const]
 
+omit [MeasurableSingletonClass Seed] [MeasurableSingletonClass Output] in
 /-- 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)
+    (hG : G.outputDist = 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
+    G.Secure (fun _ => True) 0 ↔ G.outputDist = 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
-
+  apply Measure.ext_of_singleton
+  intro output
+  apply (ENNReal.toReal_eq_toReal_iff' (measure_ne_top _ _) (measure_ne_top _ _)).mp
+  simpa [advantage, realExperiment, idealExperiment, Adversary.ofPure,
+    Measure.bind_dirac_eq_map _ (measurable_of_countable _),
+    Measure.map_apply (measurable_of_countable _), Set.preimage, sub_eq_zero] using
+    h (Adversary.ofPure (fun x => decide (x = output))) trivial
+
+omit [MeasurableSingletonClass Seed] [MeasurableSingletonClass Output] in
 /-- 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εδ)
 
+omit [MeasurableSingletonClass Seed] [MeasurableSingletonClass Output] in
 /-- 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}
@@ -95,37 +106,50 @@ def rangeTest (G : Generator Seed Output) (output : Output) : Bool :=
 omit [Nonempty Seed] [Fintype Output] [Nonempty Output] in
 /-- The deterministic adversary that tests membership in the generator's range. -/
 noncomputable def rangeAdversary (G : Generator Seed Output) : Adversary Output :=
-  fun output => PMF.pure (G.rangeTest output)
+  Adversary.ofPure G.rangeTest
 
 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, rangeTest, Function.comp_def,
-    PMF.bind_const]
-
-omit [Nonempty Seed] in
+    G.realExperiment G.rangeAdversary = Measure.dirac true := by
+  have htest : Measurable G.rangeTest := by
+    change Measurable (fun output => decide (∃ seed, G seed = output))
+    simpa using
+      (measurable_const.ite (Set.finite_range G).measurableSet measurable_const :
+        Measurable (fun output => if output ∈ Set.range G then true else false))
+  simp only [realExperiment, outputDist, rangeAdversary, Adversary.ofPure,
+    Measure.coe_toProbabilityMeasure]
+  rw [Measure.bind_dirac_eq_map _ htest, Measure.map_map htest (measurable_of_countable G)]
+  have h : (G.rangeTest ∘ G) = fun _ => true := by
+    funext seed
+    simp [rangeTest]
+  simp [h]
+
+omit [Nonempty Seed] [MeasurableSpace Seed] [MeasurableSingletonClass 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 {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]
-  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]
+  classical
+  simp only [idealExperiment, rangeAdversary, Adversary.ofPure,
+    Measure.coe_toProbabilityMeasure]
+  rw [Measure.bind_dirac_eq_map _ (measurable_of_countable _),
+    Measure.map_apply (measurable_of_countable _) (measurableSet_singleton true)]
+  simp [uniformOn_univ, Measure.count_apply_finite _ (Set.toFinite _),
+    rangeTest, Set.preimage,
+    Fintype.card_subtype, Nat.card_eq_fintype_card, ENNReal.toReal_div]
 
 /-- 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 _ _)
+  have hprob : (idealExperiment G.rangeAdversary {true}).toReal ≤ 1 := by
+    exact_mod_cast ENNReal.toReal_mono ENNReal.one_ne_top
+      (prob_le_one (μ := idealExperiment G.rangeAdversary) (s := {true}))
   rw [advantage, realExperiment_rangeAdversary]
-  simp only [PMF.pure_apply, ↓reduceIte, ENNReal.toReal_one]
+  simp only [Measure.dirac_apply_of_mem (Set.mem_singleton true), ENNReal.toReal_one]
   rw [abs_of_nonneg (sub_nonneg.mpr hprob), idealExperiment_rangeAdversary]
 
 /-- Every generator has an unbounded distinguisher with advantage at least

Cslib/Crypto/Primitives/PRG/Defs.lean

@@ -6,9 +6,7 @@ Authors: Samuel Schlesinger
 
 module
 
-public import Cslib.Init
-public import Mathlib.Probability.Distributions.Uniform
-public import Mathlib.Probability.ProbabilityMassFunction.Constructions
+public import Cslib.Probability.Measure
 
 /-!
 # Pseudorandom generators: games and concrete security
@@ -31,6 +29,7 @@ In particular, a generator need not expand, and an expanding generator need not
 
 namespace Cslib.Crypto.PRG
 
+open MeasureTheory ProbabilityTheory Cslib.Probability.Measure
 open scoped NNReal
 
 /-- A deterministic generator with seed space `Seed` and output space `Output`.
@@ -41,7 +40,11 @@ structure Generator (Seed Output : Type*) where
   toFun : Seed → Output
 
 /-- A randomized statistical test on the output space. -/
-abbrev Adversary (Output : Type*) := Output → PMF Bool
+abbrev Adversary (Output : Type*) := Output → ProbabilityMeasure Bool
+
+/-- A deterministic Boolean test, viewed as a randomized adversary. -/
+noncomputable def Adversary.ofPure {Output : Type*} (f : Output → Bool) : Adversary Output :=
+  fun output => (Measure.dirac (f output)).toProbabilityMeasure
 
 namespace Generator
 
@@ -58,25 +61,40 @@ 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 [MeasurableSpace Seed] [MeasurableSingletonClass Seed]
+variable [MeasurableSpace Output] [MeasurableSingletonClass 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
+noncomputable def outputDist (G : Generator Seed Output) : Measure Output :=
+  (uniformOfFintype Seed : Measure Seed).map G
+
+instance (G : Generator Seed Output) : IsProbabilityMeasure G.outputDist :=
+  (Measure.isProbabilityMeasure_map_iff (measurable_of_countable G).aemeasurable).2 inferInstance
 
 /-- 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
+    (adversary : Adversary Output) : Measure Bool :=
+  G.outputDist.bind (fun output => (adversary output : Measure Bool))
+
+omit [Fintype Output] in
+instance [Countable Output] (G : Generator Seed Output) (adversary : Adversary Output) :
+    IsProbabilityMeasure (G.realExperiment adversary) :=
+  isProbabilityMeasure_bind (measurable_of_countable _).aemeasurable
+    (Filter.Eventually.of_forall fun _ => inferInstance)
 
 /-- 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
+noncomputable def idealExperiment (adversary : Adversary Output) : Measure Bool :=
+  (uniformOfFintype Output : Measure Output).bind (fun output => (adversary output : Measure Bool))
+
+instance (adversary : Adversary Output) : IsProbabilityMeasure (idealExperiment adversary) :=
+  isProbabilityMeasure_bind (measurable_of_countable _).aemeasurable
+    (Filter.Eventually.of_forall fun _ => inferInstance)
 
 /-- 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|
+  |(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.