Differential Privacy

This file defines an abstract system of differentially private operators.

class SLang.DiscProbSpace (T : Type) : Type

Typeclass synonym for the classes we use for probaility

• instMeasurableSpace : MeasurableSpace T
• instCountable : Countable T
• instDiscreteMeasurableSpace : DiscreteMeasurableSpace T
• instInhabited : Inhabited T

@[implicit_reducible]

instance SLang.instMeasurableSpaceOfDiscProbSpace {T : Type} [idps : DiscProbSpace T] : MeasurableSpace T

Equations

• SLang.instMeasurableSpaceOfDiscProbSpace = SLang.DiscProbSpace.instMeasurableSpace

instance SLang.instCountableOfDiscProbSpace {T : Type} [idps : DiscProbSpace T] : Countable T

instance SLang.instDiscreteMeasurableSpace {T : Type} [idps : DiscProbSpace T] : DiscreteMeasurableSpace T

@[implicit_reducible]

instance SLang.instInhabitedOfDiscProbSpace {T : Type} [idps : DiscProbSpace T] : Inhabited T

Equations

• SLang.instInhabitedOfDiscProbSpace = SLang.DiscProbSpace.instInhabited

@[implicit_reducible]

instance SLang.instDiscProbSpaceOfCountableOfDiscreteMeasurableSpaceOfInhabited {T : Type} [im : MeasurableSpace T] [ic : Countable T] [idm : DiscreteMeasurableSpace T] [ii : Inhabited T] : DiscProbSpace T

Equations

• SLang.instDiscProbSpaceOfCountableOfDiscreteMeasurableSpaceOfInhabited = { instMeasurableSpace := im, instCountable := ic, instDiscreteMeasurableSpace := idm, instInhabited := ii }

class SLang.DPSystem (T : Type) : Type 1

Abstract definition of a differentially private systemm.

• prop {Z : Type} : Mechanism T Z → NNReal → Prop

  Differential privacy proposition, with one real parameter (ε-DP, ε-zCDP, etc)

• of_app_dp (δ ε' : NNReal) : NNReal

  Definition of DP is well-formed: Privacy parameter required to obtain (ε', δ)-approximate DP

• prop_adp {Z : Type} [DiscProbSpace Z] {m : Mechanism T Z} (δ : NNReal) : 0 < δ → ∀ (ε' : NNReal), prop m (of_app_dp T δ ε') → ApproximateDP m (↑ε') δ

  For any ε', this definition of DP implies (ε', δ)-approximate-DP for all δ

• prop_mono {Z : Type} {m : Mechanism T Z} {ε₁ ε₂ : NNReal} : ε₁ ≤ ε₂ → prop m ε₁ → prop m ε₂

  DP is monotonic

• adaptive_compose_prop {U V : Type} [DiscProbSpace U] [DiscProbSpace V] {m₁ : Mechanism T U} {m₂ : U → Mechanism T V} {ε₁ ε₂ ε : NNReal} : prop m₁ ε₁ → (∀ (u : U), prop (m₂ u) ε₂) → ε₁ + ε₂ = ε → prop (privComposeAdaptive m₁ m₂) ε

  Privacy adaptively composes by addition.

• postprocess_prop {V U : Type} [DiscProbSpace U] {pp : U → V} {m : Mechanism T U} {ε : NNReal} : prop m ε → prop (privPostProcess m pp) ε

  Privacy is invariant under post-processing.

• const_prop {U : Type} [DiscProbSpace U] {u : U} {ε : NNReal} : ε = 0 → prop (privConst u) ε

  Constant query is 0-DP

theorem SLang.DPSystem.compose_prop {T U V : Type} [dps : DPSystem T] [DiscProbSpace U] [DiscProbSpace V] {m₁ : Mechanism T U} {m₂ : Mechanism T V} {ε₁ ε₂ ε : NNReal} : ε₁ + ε₂ = ε → prop m₁ ε₁ → prop m₂ ε₂ → prop (privCompose m₁ m₂) ε

theorem SLang.DPSystem_prop_ext {T U : Type} [dps : DPSystem T] {ε₁ ε₂ : NNReal} (m : Mechanism T U) (Hε : ε₁ = ε₂) (H : DPSystem.prop m ε₁) : DPSystem.prop m ε₂

@[simp]

theorem SLang.bind_bind_indep {T U V A : Type} (p : Mechanism T U) (q : Mechanism T V) (h : U → V → PMF A) : (fun (l : List T) => do let a ← p l let b ← q l h a b) = fun (l : List T) => do let z ← privCompose p q l h z.1 z.2

class SLang.DPNoise {T : Type} (dps : DPSystem T) : Type

A noise function for a differential privacy system

• noise : Query T ℤ → (sensitivity num den : ℕ+) → Mechanism T ℤ

  A noise mechanism (eg. Laplace, Discrete Gaussian, etc) Paramaterized by a query, sensitivity, and a (rational) security paramater.

• noise_priv (num den : ℕ+) (priv : NNReal) : Prop

  Relationship between arguments to noise and resulting privacy amount

• noise_prop {q : List T → ℤ} {Δ εn εd : ℕ+} {ε : NNReal} : noise_priv dps εn εd ε → sensitivity q ↑Δ → DPSystem.prop (noise dps q Δ εn εd) ε

  Adding noise to a query makes it private

class SLang.DPPar (T : Type) extends SLang.DPSystem T : Type 1

• prop {Z : Type} : Mechanism T Z → NNReal → Prop
• of_app_dp (δ ε' : NNReal) : NNReal
• prop_adp {Z : Type} [DiscProbSpace Z] {m : Mechanism T Z} (δ : NNReal) : 0 < δ → ∀ (ε' : NNReal), prop m (of_app_dp T δ ε') → ApproximateDP m (↑ε') δ
• prop_mono {Z : Type} {m : Mechanism T Z} {ε₁ ε₂ : NNReal} : ε₁ ≤ ε₂ → prop m ε₁ → prop m ε₂
• adaptive_compose_prop {U V : Type} [DiscProbSpace U] [DiscProbSpace V] {m₁ : Mechanism T U} {m₂ : U → Mechanism T V} {ε₁ ε₂ ε : NNReal} : prop m₁ ε₁ → (∀ (u : U), prop (m₂ u) ε₂) → ε₁ + ε₂ = ε → prop (privComposeAdaptive m₁ m₂) ε
• postprocess_prop {V U : Type} [DiscProbSpace U] {pp : U → V} {m : Mechanism T U} {ε : NNReal} : prop m ε → prop (privPostProcess m pp) ε
• const_prop {U : Type} [DiscProbSpace U] {u : U} {ε : NNReal} : ε = 0 → prop (privConst u) ε
• prop_par {U V : Type} {m1 : Mechanism T U} {m2 : Mechanism T V} {ε₁ ε₂ ε : NNReal} : ε = max ε₁ ε₂ → ∀ (f : T → Bool), DPSystem.prop m1 ε₁ → DPSystem.prop m2 ε₂ → DPSystem.prop (privParCompose m1 m2 f) ε