Differential Privacy

This file defines a notion of a differential private system.

def NonZeroNQ {T : Type u_1} {U : Type u_2} (nq : List T → SLang U) : Prop

Equations

• NonZeroNQ nq = ∀ (l : List T) (n : U), nq l n ≠ 0

def NonTopSum {T : Type u_1} {U : Type u_2} (nq : List T → SLang U) : Prop

Equations

• NonTopSum nq = ∀ (l : List T), ∑' (n : U), nq l n ≠ ⊤

@[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 → SLang U)

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

Product of mechanisms.

Note that the second mechanism does not depend on the output of the first; this is in currently in contrast to the notions of composition found in the DP literature.

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) : SLang 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)

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

Abstract definition of a differentially private systemm.

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

  Notion of differential privacy with a paramater (ε-DP, ε-zCDP, etc)

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

  Noise mechanism (eg. Laplace, Discrete Gaussian, etc) Paramaterized by a query, sensitivity, and the numerator/denominator ofa (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 differentially 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) (ε₁ ε₂ ε₃ ε₄ : ℕ+), SLang.DPSystem.prop m₁ (↑↑ε₁ / ↑↑ε₂) → SLang.DPSystem.prop m₂ (↑↑ε₃ / ↑↑ε₄) → SLang.DPSystem.prop (SLang.privCompose m₁ m₂) (↑↑ε₁ / ↑↑ε₂ + ↑↑ε₃ / ↑↑ε₄)

  Notion of privacy composes by addition.

• postprocess_prop : ∀ {V U : Type} [inst : MeasurableSpace U] [inst_1 : Countable U] [inst : DiscreteMeasurableSpace U] [inst : Inhabited U] {pp : U → V}, Function.Surjective pp → ∀ (m : SLang.Mechanism T U) (ε₁ ε₂ : ℕ+), SLang.DPSystem.prop m (↑↑ε₁ / ↑↑ε₂) → SLang.DPSystem.prop (SLang.privPostProcess m pp) (↑↑ε₁ / ↑↑ε₂)

  Notion of privacy is invariant under post-processing.

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 differentially 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) (ε₁ : ℕ+) (ε₂ : ℕ+) (ε₃ : ℕ+) (ε₄ : ℕ+) : SLang.DPSystem.prop m₁ (↑↑ε₁ / ↑↑ε₂) → SLang.DPSystem.prop m₂ (↑↑ε₃ / ↑↑ε₄) → SLang.DPSystem.prop (SLang.privCompose m₁ m₂) (↑↑ε₁ / ↑↑ε₂ + ↑↑ε₃ / ↑↑ε₄)

Notion of privacy 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} : Function.Surjective pp → ∀ (m : SLang.Mechanism T U) (ε₁ ε₂ : ℕ+), SLang.DPSystem.prop m (↑↑ε₁ / ↑↑ε₂) → SLang.DPSystem.prop (SLang.privPostProcess m pp) (↑↑ε₁ / ↑↑ε₂)

Notion of privacy is invariant under post-processing.

@[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 → SLang A) : (fun (l : List T) => (p l).probBind fun (a : U) => (q l).probBind fun (b : V) => h a b) = fun (l : List T) => (SLang.privCompose p q l).probBind fun (z : U × V) => h z.1 z.2

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

theorem SLang.privCompose_NonTopSum {T : Type} {U : Type} {V : Type} {nq1 : List T → SLang U} {nq2 : List T → SLang V} (nt1 : NonTopSum nq1) (nt2 : NonTopSum nq2) : NonTopSum (SLang.privCompose nq1 nq2)

Composed queries are normalizable.

theorem SLang.privCompose_NonZeroNQ {T : Type} {U : Type} {V : Type} {nq1 : List T → SLang U} {nq2 : List T → SLang V} (nn1 : NonZeroNQ nq1) (nn2 : NonZeroNQ nq2) : NonZeroNQ (SLang.privCompose nq1 nq2)

All outputs of a composed query have nonzero probability.

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

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

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

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

theorem SLang.privPostProcess_NonZeroNQ {T : Type} {U : Type} {V : Type} {nq : List T → SLang U} {f : U → V} (nn : NonZeroNQ nq) (sur : Function.Surjective f) : NonZeroNQ (SLang.privPostProcess nq f)

theorem SLang.privPostProcess_NonTopSum {T : Type} {U : Type} {V : Type} {nq : List T → SLang U} (f : U → V) (nt : NonTopSum nq) : NonTopSum (SLang.privPostProcess nq f)