Pure and zero concentrated adaptive composition

SampCert/DifferentialPrivacy/Abstract.lean

@@ -10,110 +10,140 @@ import SampCert.Foundations.Basic
 /-!
 # Differential Privacy
 
-This file defines a notion of a differential private system.
+This file defines an abstract system of differentially private operators.
 -/
 
 noncomputable section
 
 open Classical Nat Int Real ENNReal
 
-def NonZeroNQ (nq : List T → SLang U) :=
+/--
+A mechanism is nonzero on its entire domain
+-/
+def NonZeroNQ (nq : List T → PMF U) :=
   ∀ l : List T, ∀ n : U, nq l n ≠ 0
 
-def NonTopSum (nq : List T → SLang U) :=
-  ∀ l : List T, ∑' n : U, nq l n ≠ ⊤
-
 namespace SLang
 
 abbrev Query (T U : Type) := List T → U
-abbrev Mechanism (T U : Type) := List T → SLang U
+
+abbrev Mechanism (T U : Type) := List T → PMF U
 
 /--
-Product of mechanisms.
+General (value-dependent) composition of mechanisms
+-/
+def privComposeAdaptive (nq1 : Mechanism T U) (nq2 : U -> Mechanism T V) (l : List T) : SLang (U × V) := do
+  let A <- nq1 l
+  let B <- nq2 A l
+  return (A, B)
+
+
+lemma compose_sum_rw_adaptive (nq1 : List T → SLang U) (nq2 : U -> List T → SLang 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
+    split
+    · simp
+    · aesop
+  have hrw2 : ∀ (a : U), (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) = (nq1 l u * (∑' (a_1 : V), if u = a ∧ v = a_1 then nq2 u l a_1 else 0)) := by
+    intro a
+    split
+    · aesop
+    · aesop
+  rw [tsum_congr hrw1]
+  rw [tsum_congr hrw2]
+  clear hrw1 hrw2
+  rw [ENNReal.tsum_mul_left]
+  congr 1
+  rw [<- ENNReal.tsum_prod]
+  have hrw3 : ∀ (p : U × V), (if u = p.1 ∧ v = p.2 then nq2 u l p.2 else 0) = nq2 u l v * (if p = (u, v) then 1 else 0) := by
+    intro p
+    split
+    · aesop
+    · aesop
+  rw [tsum_congr hrw3]
+  rw [ENNReal.tsum_mul_left]
+  rw [tsum_ite_eq]
+  exact MulOneClass.mul_one (nq2 u l v)
+
+
+/--
+Chain rule relating the adaptive composition definitions
+
+The joint distribution decomposes into the conditional and marginal (ie, nq1 l) distributions
+-/
+lemma privComposeChainRule (nq1 : Mechanism T U) (nq2 : U -> Mechanism T V) (l : List T) :
+  ∀ (u : U), ∀ (v : V), privComposeAdaptive nq1 nq2 l (u, v) = nq1 l u * nq2 u l v := by
+  intros u v
+  rw [<- compose_sum_rw_adaptive]
+  simp [privComposeAdaptive]
 
-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.
+/--
+Product of mechanisms.
 -/
-def privCompose (nq1 : Mechanism T U) (nq2 : Mechanism T V) (l : List T) : SLang (U × V) := do
+def privCompose (nq1 : Mechanism T U) (nq2 : Mechanism T V) (l : List T) : PMF (U × V) := do
   let A ← nq1 l
   let B ← nq2 l
   return (A,B)
 
 /--
 Mechanism obtained by applying a post-processing function to a mechanism.
 -/
-def privPostProcess (nq : Mechanism T U) (pp : U → V) (l : List T) : SLang V := do
+def privPostProcess (nq : Mechanism T U) (pp : U → V) (l : List T) : PMF V := do
   let A ← nq l
   return pp A
 
-
 /--
 Abstract definition of a differentially private systemm.
 -/
 class DPSystem (T : Type) where
   /--
-  Notion of differential privacy with a paramater (ε-DP, ε-zCDP, etc)
+  Differential privacy proposition, with one real paramater (ε-DP, ε-zCDP, etc)
   -/
   prop : Mechanism T Z → ℝ → Prop
   /--
-  Noise mechanism (eg. Laplace, Discrete Gaussian, etc)
-  Paramaterized by a query, sensitivity, and the numerator/denominator ofa (rational) security paramater.
+  A noise mechanism (eg. Laplace, Discrete Gaussian, etc)
+  Paramaterized by a query, sensitivity, and a (rational) security paramater.
   -/
-  noise : Query T ℤ → ℕ+ → ℕ+ → ℕ+ → Mechanism T ℤ
+  noise : Query T ℤ → (sensitivity : ℕ+) → (num : ℕ+) → (den : ℕ+) → Mechanism T ℤ
   /--
-  Adding noise to a query makes it differentially private.
+  Adding noise to a query makes it private.
   -/
   noise_prop : ∀ q : List T → ℤ, ∀ Δ εn εd : ℕ+, sensitivity q Δ → prop (noise q Δ εn εd) (εn / εd)
   /--
-  Notion of privacy composes by addition.
+  Privacy composes by addition.
   -/
   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₂ : Mechanism T V, ∀ ε₁ ε₂ ε₃ ε₄ : ℕ+,
     prop m₁ (ε₁ / ε₂) → prop m₂ (ε₃ / ε₄) → prop (privCompose m₁ m₂) ((ε₁ / ε₂) + (ε₃ / ε₄))
+  /-
+  Uniformity conditions for adaptive composition
+  -/
+  -- adaptive_unif_prop {U : Type} : (U -> Mechanism T Z) -> Prop
+  /-
+  Notion of privacy 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, ∀ ε₁ ε₂ ε₃ ε₄ : ℕ+,
+  --  prop m₁ (ε₁ / ε₂) → (∀ u, prop (m₂ u) (ε₃ / ε₄)) -> adaptive_unif_prop m₂ → prop (privComposeAdaptive m₁ m₂) ((ε₁ / ε₂) + (ε₃ / ε₄))
+  /--
+  Requirement for postcomposition to hold.
+  -/
+  postprocess_prop_f : {U V : Type} -> (f : U -> V) -> Prop
   /--
-  Notion of privacy is invariant under post-processing.
+  Privacy is invariant under post-processing.
   -/
-  postprocess_prop : {U : Type} → [MeasurableSpace U] → [Countable U] → [DiscreteMeasurableSpace U] → [Inhabited U] → { pp : U → V } → Function.Surjective pp → ∀ m : Mechanism T U, ∀ ε₁ ε₂ : ℕ+,
+  postprocess_prop : {U : Type} → [MeasurableSpace U] → [Countable U] → [DiscreteMeasurableSpace U] → [Inhabited U] → { pp : U → V } → postprocess_prop_f pp → ∀ m : Mechanism T U, ∀ ε₁ ε₂ : ℕ+,
    prop m (ε₁ / ε₂) → prop (privPostProcess m pp) (ε₁ / ε₂)
 
 @[simp]
-lemma bind_bind_indep (p : Mechanism T U) (q : Mechanism T V) (h : U → V → SLang A)  :
-  (fun l => (p l).probBind (fun a : U => (q l).probBind fun b : V => h a b))
-    =
-  fun l => (privCompose p q l).probBind (fun z => h z.1 z.2) := by
+lemma bind_bind_indep (p : Mechanism T U) (q : Mechanism T V) (h : U → V → PMF A) :
+    (fun l => (p l) >>= (fun a : U => (q l) >>= fun b : V => h a b)) =
+    fun l => (privCompose p q l) >>= (fun z => h z.1 z.2) := by
   ext l x
   simp [privCompose, tsum_prod']
-  apply tsum_congr
-  intro b
-  rw [← ENNReal.tsum_mul_left]
-  apply tsum_congr
-  intro c
-  rw [← mul_assoc]
-  congr 1
-  rw [tsum_eq_single b]
-  . congr 1
-    rw [tsum_eq_single c]
-    . simp
-    . intro b' h1
-      simp
-      intro h2
-      subst h2
-      contradiction
-  . intro b' h1
-    rw [tsum_eq_single c]
-    . simp
-      intro h2
-      subst h2
-      contradiction
-    . intro b'' h2
-      simp
-      intro h3 h4
-      subst h3
-      subst h4
-      contradiction
 
-lemma compose_sum_rw (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 := by
-  have A : ∀ a : U, ∀ b : U, (∑' (a_1 : V), if b = a ∧ c = a_1 then nq2 l a_1 else 0) = if b = a then (∑' (a_1 : V), if c = a_1 then nq2 l a_1 else 0) else 0 := by
+lemma compose_sum_rw (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 := by
+  have A : ∀ a : U, ∀ b : U, (∑' (a_1 : V), if b = a ∧ c = a_1 then nq2 a_1 else 0) = if b = a then (∑' (a_1 : V), if c = a_1 then nq2 a_1 else 0) else 0 := by
     intro x  y
     split
     . rename_i h
@@ -131,7 +161,7 @@ lemma compose_sum_rw (nq1 : List T → SLang U) (nq2 : List T → SLang V) (b :
     rw [A]
   rw [ENNReal.tsum_eq_add_tsum_ite b]
   simp
-  have B : ∀ x : U, (if x = b then 0 else if b = x then nq1 l x * ∑' (a_1 : V), if c = a_1 then nq2 l a_1 else 0 else 0) = 0 := by
+  have B : ∀ x : U, (if x = b then 0 else if b = x then nq1 x * ∑' (a_1 : V), if c = a_1 then nq2 a_1 else 0 else 0) = 0 := by
     intro x
     split
     . simp
@@ -150,7 +180,7 @@ lemma compose_sum_rw (nq1 : List T → SLang U) (nq2 : List T → SLang V) (b :
   congr 1
   rw [ENNReal.tsum_eq_add_tsum_ite c]
   simp
-  have C :∀ x : V,  (if x = c then 0 else if c = x then nq2 l x else 0) = 0 := by
+  have C :∀ x : V,  (if x = c then 0 else if c = x then nq2 x else 0) = 0 := by
     intro x
     split
     . simp
@@ -167,47 +197,11 @@ lemma compose_sum_rw (nq1 : List T → SLang U) (nq2 : List T → SLang V) (b :
     rw [C]
   simp
 
-/--
-Composed queries are normalizable.
--/
-theorem privCompose_NonTopSum {nq1 : List T → SLang U} {nq2 : List T → SLang V} (nt1 : NonTopSum nq1) (nt2 : NonTopSum nq2) :
-  NonTopSum (privCompose nq1 nq2) := by
-  simp [NonTopSum] at *
-  intro l
-  replace nt1 := nt1 l
-  replace nt2 := nt2 l
-  simp [privCompose]
-  rw [ENNReal.tsum_prod']
-  conv =>
-    right
-    left
-    right
-    intro a
-    right
-    intro b
-    simp
-    rw [compose_sum_rw]
-  conv =>
-    right
-    left
-    right
-    intro a
-    rw [ENNReal.tsum_mul_left]
-  rw [ENNReal.tsum_mul_right]
-  rw [mul_eq_top]
-  intro H
-  cases H
-  . rename_i H
-    cases H
-    contradiction
-  . rename_i H
-    cases H
-    contradiction
 
 /--
 All outputs of a composed query have nonzero probability.
 -/
-theorem privCompose_NonZeroNQ {nq1 : List T → SLang U} {nq2 : List T → SLang V} (nn1 : NonZeroNQ nq1) (nn2 : NonZeroNQ nq2) :
+theorem privCompose_NonZeroNQ {nq1 : Mechanism T U} {nq2 : Mechanism T V} (nn1 : NonZeroNQ nq1) (nn2 : NonZeroNQ nq2) :
   NonZeroNQ (privCompose nq1 nq2) := by
   simp [NonZeroNQ] at *
   intro l a b
@@ -216,6 +210,9 @@ theorem privCompose_NonZeroNQ {nq1 : List T → SLang U} {nq2 : List T → SLang
   simp [privCompose]
   exists a
 
+/--
+Partition series into fibers. `g` maps an element to its fiber.
+-/
 theorem ENNReal.HasSum_fiberwise {f : T → ENNReal} {a : ENNReal} (hf : HasSum f a) (g : T → V) :
     HasSum (fun c : V ↦ ∑' b : g ⁻¹' {c}, f b) a := by
   let A := (Equiv.sigmaFiberEquiv g)
@@ -229,6 +226,9 @@ theorem ENNReal.HasSum_fiberwise {f : T → ENNReal} {a : ENNReal} (hf : HasSum
   . rfl
   . apply ENNReal.summable
 
+/--
+Partition series into fibers. `g` maps an element to its fiber.
+-/
 theorem ENNReal.tsum_fiberwise (p : T → ENNReal) (f : T → V) :
   ∑' (x : V), ∑' (b : (f ⁻¹' {x})), p b
     = ∑' i : T, p i := by
@@ -237,6 +237,9 @@ theorem ENNReal.tsum_fiberwise (p : T → ENNReal) (f : T → V) :
   apply Summable.hasSum
   exact ENNReal.summable
 
+/--
+Rewrite a series into a sum over fibers. `f` maps an element into its fiber.
+-/
 theorem fiberwisation (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 := by
@@ -271,7 +274,11 @@ lemma condition_to_subset (f : U → V) (g : U → ENNReal) (x : V) :
     simp
   rw [B]
 
-theorem privPostProcess_NonZeroNQ {nq : List T → SLang U} {f : U → V} (nn : NonZeroNQ nq) (sur : Function.Surjective f) :
+
+/--
+Postprocessing by a surjection preserves `NonZeroNQ`.
+-/
+theorem privPostProcess_NonZeroNQ {nq : Mechanism T U} {f : U → V} (nn : NonZeroNQ nq) (sur : Function.Surjective f) :
   NonZeroNQ (privPostProcess nq f) := by
   simp [NonZeroNQ, Function.Surjective, privPostProcess] at *
   intros l n
@@ -283,26 +290,4 @@ theorem privPostProcess_NonZeroNQ {nq : List T → SLang U} {f : U → V} (nn :
   . rw [h]
   . apply nn
 
-theorem privPostProcess_NonTopSum {nq : List T → SLang U} (f : U → V) (nt : NonTopSum nq) :
-  NonTopSum (privPostProcess nq f) := by
-  simp [NonTopSum, privPostProcess] at *
-  intros l
-  have nt := nt l
-  rw [← ENNReal.tsum_fiberwise _ f] at nt
-  conv =>
-    right
-    left
-    right
-    intro n
-    rw [condition_to_subset]
-  have A : ∀ x : V, f ⁻¹' {x} = {y | x = f y} := by
-    aesop
-  conv =>
-    right
-    left
-    right
-    intro x
-    rw [← A]
-  trivial
-
 end SLang

SampCert/DifferentialPrivacy/Neighbours.lean

@@ -7,16 +7,31 @@ Authors: Jean-Baptiste Tristan
 /-!
 # Neighbours
 
-This file defines the notion of neighbouring lists, in order to define a notion of sensitivity.
+This file defines neighbouring lists.
 -/
 
 
 variable {T : Type}
 
 /--
-The notion of "difference" between lists for differential privacy.
+Lists which differ by the inclusion or modification of an element.
+
+This is SampCert's private property.
 -/
 inductive Neighbour (l₁ l₂ : List T) : Prop where
   | Addition : l₁ = a ++ b → l₂ = a ++ [n] ++ b → Neighbour l₁ l₂
   | Deletion : l₁ = a ++ [n] ++ b → l₂ = a ++ b → Neighbour l₁ l₂
   | Update : l₁ = a ++ [n] ++ b → l₂ = a ++ [m] ++ b -> Neighbour l₁ l₂
+
+
+/--
+Neighbour relation is symmetric.
+-/
+def Neighbour_symm (l₁ l₂ : List T) (H : Neighbour l₁ l₂) : Neighbour l₂ l₁ := by
+  cases H
+  · rename_i _ _ _ Hl1 Hl2
+    exact Neighbour.Deletion Hl2 Hl1
+  · rename_i _ _ _ Hl1 Hl2
+    exact Neighbour.Addition Hl2 Hl1
+  · rename_i _ _ _ _ Hl1 Hl2
+    exact Neighbour.Update Hl2 Hl1