Differential Privacy

This file defines an abstract system of differentially private operators.

@[reducible, inline]

abbrev SLang.Query (T : Type) (U : Type) : Type

Equations

• SLang.Query T U = (List T → U)

@[reducible, inline]

abbrev SLang.Mechanism (T : Type) (U : Type) : Type

Equations

• SLang.Mechanism T U = (List T → PMF U)

def SLang.privComposeAdaptive {T : Type} {U : Type} {V : Type} (nq1 : SLang.Mechanism T U) (nq2 : U → SLang.Mechanism T V) (l : List T) : PMF (U × V)

General (value-dependent) composition of mechanisms

Equations

• SLang.privComposeAdaptive nq1 nq2 l = do let A ← nq1 l let B ← nq2 A l pure (A, B)

theorem SLang.compose_sum_rw_adaptive {T : Type u_1} {U : Type u_2} {V : Type u_3} (nq1 : List T → PMF U) (nq2 : U → List T → PMF 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

theorem SLang.privComposeChainRule {T : Type} {U : Type} {V : Type} (nq1 : SLang.Mechanism T U) (nq2 : U → SLang.Mechanism T V) (l : List T) (u : U) (v : V) : (SLang.privComposeAdaptive nq1 nq2 l) (u, v) = (nq1 l) u * (nq2 u l) v

Chain rule relating the adaptive composition definitions

The joint distribution decomposes into the conditional and marginal (ie, nq1 l) distributions

def SLang.privCompose {T : Type} {U : Type} {V : Type} (nq1 : SLang.Mechanism T U) (nq2 : SLang.Mechanism T V) (l : List T) : PMF (U × V)

Product of mechanisms.

Equations

• SLang.privCompose nq1 nq2 l = do let A ← nq1 l let B ← nq2 l pure (A, B)

def SLang.privPostProcess {T : Type} {U : Type} {V : Type} (nq : SLang.Mechanism T U) (pp : U → V) (l : List T) : PMF V

Mechanism obtained by applying a post-processing function to a mechanism.

Equations

• SLang.privPostProcess nq pp l = do let A ← nq l pure (pp A)

def SLang.privConst {U : Type} {T : Type} (u : U) : SLang.Mechanism T U

Constant mechanism

Equations

• SLang.privConst u x = PMF.pure u

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

Abstract definition of a differentially private systemm.

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

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

• prop_mono : ∀ {Z : Type} {m : SLang.Mechanism T Z} {ε₁ ε₂ : NNReal}, ε₁ ≤ ε₂ → SLang.DPSystem.prop m ε₁ → SLang.DPSystem.prop m ε₂

  DP is monotonic

• noise : SLang.Query T ℤ → ℕ+ → ℕ+ → ℕ+ → SLang.Mechanism T ℤ

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

• noise_prop : ∀ (q : List T → ℤ) (Δ εn εd : ℕ+), sensitivity q ↑Δ → SLang.DPSystem.prop (SLang.DPSystem.noise q Δ εn εd) (↑↑εn / ↑↑εd)

  Adding noise to a query makes it private.

• compose_prop : ∀ {U V : Type} [inst : MeasurableSpace U] [inst_1 : Countable U] [inst : DiscreteMeasurableSpace U] [inst : Inhabited U] [inst : MeasurableSpace V] [inst_2 : Countable V] [inst : DiscreteMeasurableSpace V] [inst : Inhabited V] (m₁ : SLang.Mechanism T U) (m₂ : SLang.Mechanism T V) (ε₁ ε₂ : NNReal), SLang.DPSystem.prop m₁ ε₁ → SLang.DPSystem.prop m₂ ε₂ → SLang.DPSystem.prop (SLang.privCompose m₁ m₂) (ε₁ + ε₂)

  Privacy composes by addition.

• adaptive_compose_prop : ∀ {U V : Type} [inst : MeasurableSpace U] [inst_1 : Countable U] [inst : DiscreteMeasurableSpace U] [inst : Inhabited U] [inst : MeasurableSpace V] [inst_2 : Countable V] [inst : DiscreteMeasurableSpace V] [inst : Inhabited V] (m₁ : SLang.Mechanism T U) (m₂ : U → SLang.Mechanism T V) (ε₁ ε₂ : NNReal), SLang.DPSystem.prop m₁ ε₁ → (∀ (u : U), SLang.DPSystem.prop (m₂ u) ε₂) → SLang.DPSystem.prop (SLang.privComposeAdaptive m₁ m₂) (ε₁ + ε₂)

  Privacy adaptively composes by addition.

• postprocess_prop : ∀ {V U : Type} [inst : MeasurableSpace U] [inst_1 : Countable U] [inst : DiscreteMeasurableSpace U] [inst : Inhabited U] {pp : U → V} (m : SLang.Mechanism T U) (ε : NNReal), SLang.DPSystem.prop m ε → SLang.DPSystem.prop (SLang.privPostProcess m pp) ε

  Privacy is invariant under post-processing.

• const_prop : ∀ {U : Type} [inst : MeasurableSpace U] [inst_1 : Countable U] [inst : DiscreteMeasurableSpace U] (u : U), SLang.DPSystem.prop (SLang.privConst u) 0

  Constant query is 0-DP

theorem SLang.DPSystem.prop_mono {T : Type} [self : SLang.DPSystem T] {Z : Type} {m : SLang.Mechanism T Z} {ε₁ : NNReal} {ε₂ : NNReal} (Hε : ε₁ ≤ ε₂) (H : SLang.DPSystem.prop m ε₁) : SLang.DPSystem.prop m ε₂

DP is monotonic

theorem SLang.DPSystem.noise_prop {T : Type} [self : SLang.DPSystem T] (q : List T → ℤ) (Δ : ℕ+) (εn : ℕ+) (εd : ℕ+) : sensitivity q ↑Δ → SLang.DPSystem.prop (SLang.DPSystem.noise q Δ εn εd) (↑↑εn / ↑↑εd)

Adding noise to a query makes it private.

theorem SLang.DPSystem.compose_prop {T : Type} [self : SLang.DPSystem T] {U : Type} {V : Type} [MeasurableSpace U] [Countable U] [DiscreteMeasurableSpace U] [Inhabited U] [MeasurableSpace V] [Countable V] [DiscreteMeasurableSpace V] [Inhabited V] (m₁ : SLang.Mechanism T U) (m₂ : SLang.Mechanism T V) (ε₁ : NNReal) (ε₂ : NNReal) : SLang.DPSystem.prop m₁ ε₁ → SLang.DPSystem.prop m₂ ε₂ → SLang.DPSystem.prop (SLang.privCompose m₁ m₂) (ε₁ + ε₂)

Privacy composes by addition.

theorem SLang.DPSystem.adaptive_compose_prop {T : Type} [self : SLang.DPSystem T] {U : Type} {V : Type} [MeasurableSpace U] [Countable U] [DiscreteMeasurableSpace U] [Inhabited U] [MeasurableSpace V] [Countable V] [DiscreteMeasurableSpace V] [Inhabited V] (m₁ : SLang.Mechanism T U) (m₂ : U → SLang.Mechanism T V) (ε₁ : NNReal) (ε₂ : NNReal) : SLang.DPSystem.prop m₁ ε₁ → (∀ (u : U), SLang.DPSystem.prop (m₂ u) ε₂) → SLang.DPSystem.prop (SLang.privComposeAdaptive m₁ m₂) (ε₁ + ε₂)

Privacy adaptively composes by addition.

theorem SLang.DPSystem.postprocess_prop {T : Type} [self : SLang.DPSystem T] {V : Type} {U : Type} [MeasurableSpace U] [Countable U] [DiscreteMeasurableSpace U] [Inhabited U] {pp : U → V} (m : SLang.Mechanism T U) (ε : NNReal) : SLang.DPSystem.prop m ε → SLang.DPSystem.prop (SLang.privPostProcess m pp) ε

Privacy is invariant under post-processing.

theorem SLang.DPSystem.const_prop {T : Type} [self : SLang.DPSystem T] {U : Type} [MeasurableSpace U] [Countable U] [DiscreteMeasurableSpace U] (u : U) : SLang.DPSystem.prop (SLang.privConst u) 0

Constant query is 0-DP

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

@[simp]

theorem SLang.bind_bind_indep {T : Type} {U : Type} {V : Type} {A : Type} (p : SLang.Mechanism T U) (q : SLang.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 ← SLang.privCompose p q l h z.1 z.2

theorem SLang.compose_sum_rw {U : Type u_1} {V : Type u_2} (nq1 : U → ENNReal) (nq2 : V → ENNReal) (b : U) (c : V) : (∑' (a : U), nq1 a * ∑' (a_1 : V), if b = a ∧ c = a_1 then nq2 a_1 else 0) = nq1 b * nq2 c

theorem SLang.ENNReal.HasSum_fiberwise {T : Type u_1} {V : Type u_2} {f : T → ENNReal} {a : ENNReal} (hf : HasSum f a) (g : T → V) : HasSum (fun (c : V) => ∑' (b : ↑(g ⁻¹' {c})), f ↑b) a

Partition series into fibers. g maps an element to its fiber.

theorem SLang.ENNReal.tsum_fiberwise {T : Type u_1} {V : Type u_2} (p : T → ENNReal) (f : T → V) : ∑' (x : V) (b : ↑(f ⁻¹' {x})), p ↑b = ∑' (i : T), p i

Partition series into fibers. g maps an element to its fiber.

theorem SLang.fiberwisation {T : Type u_1} {V : Type u_2} (p : T → ENNReal) (f : T → V) : ∑' (i : T), p i = ∑' (x : V), if {a : T | x = f a} = ∅ then 0 else ∑' (i : ↑{a : T | x = f a}), p ↑i

Rewrite a series into a sum over fibers. f maps an element into its fiber.

theorem SLang.condition_to_subset {U : Type u_1} {V : Sort u_2} (f : U → V) (g : U → ENNReal) (x : V) : (∑' (a : U), if x = f a then g a else 0) = ∑' (a : ↑{a : U | x = f a}), g ↑a