Restructure definitions of DP

SampCert.lean

@@ -14,7 +14,7 @@ import Init.Data.UInt.Lemmas
 
 open SLang PMF
 
-def combineConcentrated := @privNoisedBoundedMean_DP gaussian_zCDPSystem
+def combineConcentrated := @privNoisedBoundedMean_DP zCDPSystem
 def combinePure := @privNoisedBoundedMean_DP PureDPSystem
 
 /-
@@ -27,7 +27,7 @@ def numBins : ℕ+ := 64
 /-
 Bin the infinite type ℕ with clipping
 -/
-def bin (n : ℕ) : Fin numBins :=
+def example_bin (n : ℕ) : Fin numBins :=
   { val := min (Nat.log 2 n) (PNat.natPred numBins),
     isLt := by
       apply min_lt_iff.mpr
@@ -40,8 +40,8 @@ Return an upper bound on the bin value, clipped to 2^(1 + numBins)
 -/
 def unbin (n : Fin numBins) : ℕ+ := 2 ^ (1 + n.val)
 
-noncomputable def combineMeanHistogram : Mechanism ℕ (Option ℚ) :=
-  privMeanHistogram PureDPSystem numBins { bin } unbin 1 20 2 1 20
+def combineMeanHistogram : Mechanism ℕ (Option ℚ) :=
+  privMeanHistogram PureDPSystem laplace_pureDPSystem numBins { bin := example_bin } unbin 1 20 2 1 20
 
 end histogramMeanExample
 

SampCert/DifferentialPrivacy/Abstract.lean

@@ -15,12 +15,31 @@ import SampCert.DifferentialPrivacy.Approximate.DP
 This file defines an abstract system of differentially private operators.
 -/
 
-noncomputable section
-
 open Classical Nat Int Real ENNReal
 
 namespace SLang
 
+/--
+Typeclass synonym for the classes we use for probaility
+-/
+class DiscProbSpace (T : Type) where
+  instMeasurableSpace : MeasurableSpace T
+  instCountable : Countable T
+  instDiscreteMeasurableSpace : DiscreteMeasurableSpace T
+  instInhabited : Inhabited T
+
+-- Typeclass inference to- and from- the synonym
+instance [idps : DiscProbSpace T] : MeasurableSpace T := idps.instMeasurableSpace
+instance [idps : DiscProbSpace T] : Countable T := idps.instCountable
+instance [idps : DiscProbSpace T] : DiscreteMeasurableSpace T := idps.instDiscreteMeasurableSpace
+instance [idps : DiscProbSpace T] : Inhabited T := idps.instInhabited
+
+instance [im : MeasurableSpace T] [ic : Countable T] [idm : DiscreteMeasurableSpace T] [ii : Inhabited T] : DiscProbSpace T where
+  instMeasurableSpace := im
+  instCountable := ic
+  instDiscreteMeasurableSpace := idm
+  instInhabited := ii
+
 /--
 Abstract definition of a differentially private systemm.
 -/
@@ -31,54 +50,52 @@ class DPSystem (T : Type) where
   prop : Mechanism T Z → NNReal → Prop
 
   /--
-  For any δ, prop implies ``ApproximateDP δ ε`` up to a sufficient degradation
-  of the privacy parameter.
+  Definition of DP is well-formed: Privacy parameter required to obtain (ε', δ)-approximate DP
   -/
-  prop_adp [Countable Z] {m : Mechanism T Z} :
-    ∃ (degrade : (δ : NNReal) -> (ε' : NNReal) -> NNReal), ∀ (δ : NNReal) (_ : 0 < δ) (ε' : NNReal),
-    (prop m (degrade δ ε') -> ApproximateDP m ε' δ)
+  of_app_dp : (δ : NNReal) -> (ε' : NNReal) -> NNReal
   /--
-  DP is monotonic
-  -/
-  prop_mono {m : Mechanism T Z} {ε₁ ε₂: NNReal} (Hε : ε₁ ≤ ε₂) (H : prop m ε₁) : prop m ε₂
-  /--
-  A noise mechanism (eg. Laplace, Discrete Gaussian, etc)
-  Paramaterized by a query, sensitivity, and a (rational) security paramater.
+  For any ε', this definition of DP implies (ε', δ)-approximate-DP for all δ
   -/
-  noise : Query T ℤ → (sensitivity : ℕ+) → (num : ℕ+) → (den : ℕ+) → Mechanism T ℤ
+  prop_adp [DiscProbSpace Z] {m : Mechanism T Z} : ∀ (δ : NNReal) (_ : 0 < δ) (ε' : NNReal),
+    (prop m (of_app_dp δ ε') -> ApproximateDP m ε' δ)
   /--
-  Adding noise to a query makes it private.
+  DP is monotonic
   -/
-  noise_prop : ∀ q : List T → ℤ, ∀ Δ εn εd : ℕ+, sensitivity q Δ → prop (noise q Δ εn εd) (εn / εd)
+  prop_mono {m : Mechanism T Z} {ε₁ ε₂: NNReal} :
+    ε₁ ≤ ε₂ -> prop m ε₁ -> prop m ε₂
   /--
   Privacy adaptively composes by addition.
   -/
-  adaptive_compose_prop : {U V : Type} → [MeasurableSpace U] → [Countable U] → [DiscreteMeasurableSpace U] → [Inhabited U] → [MeasurableSpace V] → [Countable V] → [DiscreteMeasurableSpace V] → [Inhabited V] → ∀ m₁ : Mechanism T U, ∀ m₂ : U -> Mechanism T V,
-    ∀ ε₁ ε₂ : NNReal,
-    prop m₁ ε₁ → (∀ u, prop (m₂ u) ε₂) -> prop (privComposeAdaptive m₁ m₂) (ε₁ + ε₂)
+  adaptive_compose_prop {U V : Type} [DiscProbSpace U] [DiscProbSpace V]
+    {m₁ : Mechanism T U} {m₂ : U -> Mechanism T V} {ε₁ ε₂ ε : NNReal} :
+    prop m₁ ε₁ → (∀ u, prop (m₂ u) ε₂) ->
+    ε₁ + ε₂ = ε ->
+    prop (privComposeAdaptive m₁ m₂) ε
   /--
   Privacy is invariant under post-processing.
   -/
-  postprocess_prop : {U : Type} → [MeasurableSpace U] → [Countable U] → [DiscreteMeasurableSpace U] → [Inhabited U] → { pp : U → V } →
-    ∀ m : Mechanism T U, ∀ ε : NNReal,
-   prop m ε → prop (privPostProcess m pp) ε
+  postprocess_prop {U : Type} [DiscProbSpace U]
+    { pp : U → V } {m : Mechanism T U} {ε : NNReal} :
+    prop m ε → prop (privPostProcess m pp) ε
   /--
   Constant query is 0-DP
   -/
-  const_prop : {U : Type} → [MeasurableSpace U] → [Countable U] → [DiscreteMeasurableSpace U] -> (u : U) -> prop (privConst u) (0 : NNReal)
-
+  const_prop {U : Type} [DiscProbSpace U] {u : U} {ε : NNReal} :
+    ε = (0 : NNReal) -> prop (privConst u) ε
 
 namespace DPSystem
 
 /-
 Non-adaptive privacy composes by addition.
 -/
-lemma compose_prop {U V : Type} [dps : DPSystem T] [MeasurableSpace U] [Countable U] [DiscreteMeasurableSpace U] [Inhabited U] [MeasurableSpace V] [Countable V] [DiscreteMeasurableSpace V] [Inhabited V] :
-    ∀ m₁ : Mechanism T U, ∀ m₂ : Mechanism T V, ∀ ε₁ ε₂ : NNReal,
-    dps.prop m₁ ε₁ → dps.prop m₂ ε₂ → dps.prop (privCompose m₁ m₂) (ε₁ + ε₂) := by
-  intros m₁ m₂ ε₁ ε₂ p1 p2
+lemma compose_prop {U V : Type} [dps : DPSystem T] [DiscProbSpace U] [DiscProbSpace V] :
+    {m₁ : Mechanism T U} -> {m₂ : Mechanism T V} ->  {ε₁ ε₂ ε : NNReal} ->
+    (ε₁ + ε₂ = ε) ->
+    dps.prop m₁ ε₁ → dps.prop m₂ ε₂ → dps.prop (privCompose m₁ m₂) ε := by
+  intros _ _ _ _ _ _ p1 p2
   unfold privCompose
-  exact adaptive_compose_prop m₁ (fun _ => m₂) ε₁ ε₂ p1 fun _ => p2
+  apply adaptive_compose_prop p1 (fun _ => p2)
+  trivial
 
 end DPSystem
 
@@ -96,4 +113,38 @@ lemma bind_bind_indep (p : Mechanism T U) (q : Mechanism T V) (h : U → V → P
   ext l x
   simp [privCompose, privComposeAdaptive, tsum_prod']
 
+
+
+
+/--
+A noise function for a differential privacy system
+-/
+class DPNoise (dps : DPSystem T) where
+  /--
+  A noise mechanism (eg. Laplace, Discrete Gaussian, etc)
+  Paramaterized by a query, sensitivity, and a (rational) security paramater.
+  -/
+  noise : Query T ℤ → (sensitivity : ℕ+) → (num : ℕ+) → (den : ℕ+) → Mechanism T ℤ
+  /--
+  Relationship between arguments to noise and resulting privacy amount
+  -/
+  noise_priv : (num : ℕ+) → (den : ℕ+) → (priv : NNReal) -> Prop
+  /--
+  Adding noise to a query makes it private
+  -/
+  noise_prop {q : List T → ℤ} {Δ εn εd : ℕ+} {ε : NNReal} :
+    noise_priv εn εd ε ->
+    sensitivity q Δ →
+    dps.prop (noise q Δ εn εd) ε
+
+
+-- /-
+-- A DPNoise instance for when the arguments to noise_prop can be computed dynamically
+-- -/
+-- class DPNoiseDynamic {dps : DPSystem T} (dpn : DPNoise dps) where
+--   compute_factor : (ε : NNReal) -> (ℕ+ × ℕ+)
+--   compute_factor_spec : ∀ ε : NNReal, dpn.noise_priv (compute_factor ε).1 (compute_factor ε).2 ε
+
+
+
 end SLang

SampCert/DifferentialPrivacy/Generic.lean

@@ -13,25 +13,53 @@ import SampCert.Foundations.Basic
 This file defines an abstract system of differentially private operators.
 -/
 
-noncomputable section
-
-open Classical Nat Int Real ENNReal
 
 namespace SLang
 
+
 abbrev Query (T U : Type) := List T → U
 
-abbrev Mechanism (T U : Type) := List T → PMF U
+abbrev Mechanism (T U : Type) := List T → SPMF U
 
 /--
 General (value-dependent) composition of mechanisms
 -/
-def privComposeAdaptive (nq1 : Mechanism T U) (nq2 : U -> Mechanism T V) (l : List T) : PMF (U × V) := do
+def privComposeAdaptive (nq1 : Mechanism T U) (nq2 : U -> Mechanism T V) (l : List T) : SPMF (U × V) := do
   let A <- nq1 l
   let B <- nq2 A l
   return (A, B)
 
-lemma compose_sum_rw_adaptive (nq1 : List T → PMF U) (nq2 : U -> List T → PMF V) (u : U) (v : V) (l : List T) :
+/--
+Product of mechanisms.
+-/
+def privCompose (nq1 : Mechanism T U) (nq2 : Mechanism T V) (l : List T) : SPMF (U × V) :=
+  privComposeAdaptive nq1 (fun _ => nq2) l
+
+/--
+Mechanism obtained by applying a post-processing function to a mechanism.
+-/
+def privPostProcess (nq : Mechanism T U) (pp : U → V) (l : List T) : SPMF V := do
+  let A ← nq l
+  return pp A
+
+/--
+Constant mechanism
+-/
+def privConst (u : U) : Mechanism T U := fun _ => SPMF_pure u
+
+
+
+
+noncomputable section
+
+open Classical Nat Int Real ENNReal
+
+instance SPMF.instFunLike : FunLike (SPMF α) α ℝ≥0∞ where
+  coe p a := p.1 a
+  coe_injective' _ _ h := Subtype.eq h
+
+
+lemma compose_sum_rw_adaptive (nq1 : List T → SPMF U) (nq2 : U -> List T → SPMF V) (u : U) (v : V) (l : List T) :
   (∑' (a : U), nq1 l a * ∑' (a_1 : V), if u = a ∧ v = a_1 then nq2 a l a_1 else 0) = nq1 l u * nq2 u l v := by
   have hrw1 : ∀ (a : U), nq1 l a * (∑' (a_1 : V), if u = a ∧ v = a_1 then nq2 a l a_1 else 0) = if (u = a) then (nq1 l a * ∑' (a_1 : V), if u = a ∧ v = a_1 then nq2 a l a_1 else 0) else 0 := by
     intro a
@@ -70,24 +98,8 @@ lemma privComposeChainRule (nq1 : Mechanism T U) (nq2 : U -> Mechanism T V) (l :
   intros u v
   rw [<- compose_sum_rw_adaptive]
   simp [privComposeAdaptive]
+  simp [SPMF.instFunLike]
 
-/--
-Product of mechanisms.
--/
-def privCompose (nq1 : Mechanism T U) (nq2 : Mechanism T V) (l : List T) : PMF (U × V) :=
-  privComposeAdaptive nq1 (fun _ => nq2) l
-
-/--
-Mechanism obtained by applying a post-processing function to a mechanism.
--/
-def privPostProcess (nq : Mechanism T U) (pp : U → V) (l : List T) : PMF V := do
-  let A ← nq l
-  return pp A
-
-/--
-Constant mechanism
--/
-def privConst (u : U) : Mechanism T U := fun _ => PMF.pure u
 
 
 -- @[simp]
@@ -218,4 +230,6 @@ lemma condition_to_subset (f : U → V) (g : U → ENNReal) (x : V) :
     simp
   rw [B]
 
+end
+
 end SLang

SampCert/DifferentialPrivacy/Pure/AdaptiveComposition.lean

@@ -18,8 +18,10 @@ variable [Hu : Nonempty U]
 namespace SLang
 
 -- Better proof for Pure DP adaptive composition
-theorem PureDP_ComposeAdaptive' (nq1 : List T → PMF U) (nq2 : U -> List T → PMF V) (ε₁ ε₂ : NNReal) (h1 : PureDP nq1 ε₁)  (h2 : ∀ u : U, PureDP (nq2 u) ε₂) :
-  PureDP (privComposeAdaptive nq1 nq2) (ε₁ + ε₂) := by
+theorem PureDP_ComposeAdaptive' (nq1 : List T → PMF U) (nq2 : U -> List T → PMF V) (ε₁ ε₂ ε : NNReal) (h1 : PureDP nq1 ε₁)  (h2 : ∀ u : U, PureDP (nq2 u) ε₂) (Hε : ε₁ + ε₂ = ε ) :
+  PureDP (privComposeAdaptive nq1 nq2) ε := by
+  rw [<- Hε]
+  clear ε Hε
   simp [PureDP] at *
   rw [event_eq_singleton] at *
   simp [DP_singleton] at *

SampCert/DifferentialPrivacy/Pure/Const.lean

@@ -32,7 +32,7 @@ theorem privConst_DP_Bound {u : U} : DP (privConst u : Mechanism T U) 0 := by
 /--
 ``privComposeAdaptive`` satisfies zCDP
 -/
-theorem PureDP_privConst : ∀ (u : U),  PureDP (privConst u : Mechanism T U) (0 : NNReal) := by
+theorem PureDP_privConst : ∀ (u : U) (ε : NNReal), (ε = 0) -> PureDP (privConst u : Mechanism T U) ε := by
   simp [PureDP] at *
   apply privConst_DP_Bound
 

SampCert/DifferentialPrivacy/Pure/DP.lean

@@ -111,19 +111,21 @@ theorem ApproximateDP_of_DP (m : Mechanism T U) (ε : ℝ) (h : DP m ε) :
   apply le_trans h
   simp
 
+/--
+Pure privacy bound required to obtain (ε, δ)-approximate DP
+-/
+def pure_of_adp (_ : NNReal) (ε : NNReal) : NNReal := ε
+
 /--
 Pure DP is no weaker than approximate DP, up to a loss of parameters
 -/
 lemma pure_ApproximateDP [Countable U] {m : Mechanism T U} :
-    ∃ (degrade : (δ : NNReal) -> (ε' : NNReal) -> NNReal), ∀ (δ : NNReal) (_ : 0 < δ) (ε' : NNReal),
-     (DP m (degrade δ ε') -> ApproximateDP m ε' δ) := by
-  let degrade (_ : NNReal) (ε' : NNReal) : NNReal := ε'
-  exists degrade
-  intro δ _ ε' HDP
+  ∀ (δ : NNReal) (_ : 0 < δ) (ε' : NNReal),
+     DP m (pure_of_adp δ ε') -> ApproximateDP m ε' δ := by
+  intro _ _ _ HDP
   rw [ApproximateDP]
   apply ApproximateDP_of_DP
-  have R1 : degrade δ ε' = ε' := by simp
-  rw [R1] at HDP
+  simp [pure_of_adp] at HDP
   trivial
 
 end SLang

SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean

@@ -114,12 +114,15 @@ theorem privNoisedQueryPure_DP_bound (query : List T → ℤ) (Δ ε₁ ε₂ :
           exact (add_lt_add_iff_right 1).mpr A
     · apply exp_pos
 
+def laplace_pureDP_noise_priv (ε₁ ε₂ : ℕ+) (ε : NNReal) : Prop := (ε₁ : NNReal) / ε₂ = ε
 
 /--
 Laplace noising mechanism ``privNoisedQueryPure`` produces a pure ``ε₁/ε₂``-DP mechanism from a Δ-sensitive query.
 -/
-theorem privNoisedQueryPure_DP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (bounded_sensitivity : sensitivity query Δ) :
-  PureDP (privNoisedQueryPure query Δ ε₁ ε₂) ((ε₁ : NNReal) / ε₂) := by
+theorem privNoisedQueryPure_DP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (ε : NNReal) (HN : laplace_pureDP_noise_priv ε₁ ε₂ ε) (bounded_sensitivity : sensitivity query Δ) :
+    PureDP (privNoisedQueryPure query Δ ε₁ ε₂) ε := by
+  unfold laplace_pureDP_noise_priv at HN
+  rw [<- HN]
   simp [PureDP]
   apply privNoisedQueryPure_DP_bound
   apply bounded_sensitivity

SampCert/DifferentialPrivacy/Pure/Postprocessing.lean

@@ -29,6 +29,7 @@ lemma privPostProcess_DP_bound {nq : Mechanism T U} {ε : NNReal} (h : PureDP nq
   replace h := h l₁ l₂ neighbours
   simp [privPostProcess]
   apply ENNReal.div_le_of_le_mul
+  simp [SPMF.instFunLike]
   rw [← ENNReal.tsum_mul_left]
   apply tsum_le_tsum _ ENNReal.summable (by aesop)
   intro i

SampCert/DifferentialPrivacy/Pure/System.lean

@@ -21,14 +21,22 @@ variable { T : Type }
 /--
 Pure ε-DP with noise drawn from the discrete Laplace distribution.
 -/
-noncomputable instance PureDPSystem : DPSystem T where
+instance PureDPSystem : DPSystem T where
   prop := PureDP
+  of_app_dp := pure_of_adp
   prop_adp := pure_ApproximateDP
   prop_mono := PureDP_mono
+  adaptive_compose_prop := by
+    intros; apply PureDP_ComposeAdaptive' <;> trivial
+  postprocess_prop := by
+    intros; apply PureDP_PostProcess; trivial
+  const_prop := by
+    intros; apply PureDP_privConst; trivial
+
+instance laplace_pureDPSystem : DPNoise (@PureDPSystem T) where
   noise := privNoisedQueryPure
-  noise_prop := privNoisedQueryPure_DP
-  adaptive_compose_prop := PureDP_ComposeAdaptive'
-  postprocess_prop := PureDP_PostProcess
-  const_prop := PureDP_privConst
+  noise_priv := laplace_pureDP_noise_priv
+  noise_prop := by
+    intros; apply privNoisedQueryPure_DP <;> trivial
 
 end SLang

SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean

@@ -13,16 +13,15 @@ import SampCert.DifferentialPrivacy.Queries.BoundedSum.Code
 This file defines a differentially private bounded mean query.
 -/
 
-noncomputable section
-
 namespace SLang
 
 variable [dps : DPSystem ℕ]
+variable [dpn : DPNoise dps]
 
 /--
 Compute a noised mean using a noised sum and noised count.
 -/
-def privNoisedBoundedMean (U : ℕ+) (ε₁ ε₂ : ℕ+) (l : List ℕ) : PMF ℚ := do
+def privNoisedBoundedMean (U : ℕ+) (ε₁ ε₂ : ℕ+) (l : List ℕ) : SPMF ℚ := do
   let S ← privNoisedBoundedSum U ε₁ (2 * ε₂) l
   let C ← privNoisedCount ε₁ (2 * ε₂) l
   return S / C