From b178344d6d24ef2e4d9d4ae5f86fc55809a0b373 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 09:32:07 -0400 Subject: [PATCH 01/30] fix adaptive composition --- .../ZeroConcentrated/AdaptiveComposition.lean | 42 ++----------------- .../ZeroConcentrated/DP.lean | 35 +++++++++------- .../Mechanism/Properties.lean | 3 ++ 3 files changed, 27 insertions(+), 53 deletions(-) diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean index ac102d93..73417a5e 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean @@ -131,50 +131,14 @@ theorem privComposeAdaptive_zCDPBound {nq1 : List T → PMF U} {nq2 : U -> List zCDPBound (privComposeAdaptive nq1 nq2) (ε₁ + ε₂) := by rw [zCDPBound] intro α Hα l₁ l₂ Hneighbours - -- This step is loose - apply (@LE.le.trans _ _ _ (ENNReal.ofReal (1/2 * (ε₁)^2 * α + 1/2 * (ε₂)^2 * α : ℝ)) _ _ ?case_sq) - case case_sq => - apply ofReal_le_ofReal - -- Binomial bound - rw [add_sq] - rw [<- right_distrib] - apply (mul_le_mul_of_nonneg_right _ ?goal1) - case goal1 => linarith - rw [<- left_distrib] - apply (mul_le_mul_of_nonneg_left _ ?goal1) - case goal1 => linarith - apply add_le_add_right - have hrw : ε₁ ^ 2 = ε₁ ^ 2 + 0 := by linarith - conv => - lhs - rw [hrw] - clear hrw - apply add_le_add_left - refine mul_nonneg ?bc.bc.ha Hε₂ - refine mul_nonneg ?G Hε₁ - simp -- Rewrite the upper bounds in terms of Renyi divergences of nq1/nq2 rw [zCDPBound] at h1 -- have marginal_ub := h1 α Hα l₁ l₂ Hneighbours - have conditional_ub : (⨆ (u : U), RenyiDivergence (nq2 u l₁) (nq2 u l₂) α ≤ ENNReal.ofReal (1 / 2 * ε₂ ^ 2 * α)) := - ciSup_le fun x => h2 x α Hα l₁ l₂ Hneighbours + have conditional_ub : (⨆ (u : U), RenyiDivergence (nq2 u l₁) (nq2 u l₂) α) ≤ ENNReal.ofReal ε₂ := -- ENNReal.ofReal (1 / 2 * ε₂ ^ 2 * α)) := + iSup_le fun i => h2 i α Hα l₁ l₂ Hneighbours apply (@LE.le.trans _ _ _ (RenyiDivergence (nq1 l₁) (nq1 l₂) α + ⨆ (u : U), RenyiDivergence (nq2 u l₁) (nq2 u l₂) α) _ _ ?case_alg) case case_alg => - rw [ENNReal.ofReal_add ?G1 ?G2] - case G1 => - simp - apply mul_nonneg - · apply mul_nonneg - · simp - · exact sq_nonneg ε₁ - · linarith - case G2 => - simp - apply mul_nonneg - · apply mul_nonneg - · simp - · exact sq_nonneg ε₂ - · linarith + rw [ENNReal.ofReal_add Hε₁ Hε₂] exact _root_.add_le_add (h1 α Hα l₁ l₂ Hneighbours) conditional_ub exact privComposeAdaptive_renyi_bound Hα Hneighbours HAC1 HAC2 diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean index f51ad1aa..b0a96b60 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean @@ -44,7 +44,7 @@ satisfying this bound are ``ε``-DP). -/ def zCDPBound (q : List T → PMF U) (ε : ℝ) : Prop := ∀ α : ℝ, 1 < α → ∀ l₁ l₂ : List T, Neighbour l₁ l₂ → - RenyiDivergence (q l₁) (q l₂) α ≤ ENNReal.ofReal ((1/2) * ε ^ 2 * α) + RenyiDivergence (q l₁) (q l₂) α ≤ ENNReal.ofReal ε /-- All neighbouring queries are absolutely continuous @@ -63,18 +63,19 @@ lemma zCDP_mono {m : List T -> PMF U} {ε₁ ε₂ : NNReal} (H : ε₁ ≤ ε · assumption · rw [zCDPBound] at * intro α Hα l₁ l₂ N - apply (@le_trans _ _ _ (ENNReal.ofReal (1 / 2 * ↑ε₁ ^ 2 * α)) _ (Hε α Hα l₁ l₂ N)) - apply ENNReal.coe_mono - refine (Real.toNNReal_le_toNNReal_iff ?a.hp).mpr ?a.a - · apply mul_nonneg - · apply mul_nonneg - · simp - · simp - · linarith - · repeat rw [mul_assoc] - apply (mul_le_mul_iff_of_pos_left (by simp)).mpr - apply (mul_le_mul_iff_of_pos_right (by linarith)).mpr - apply pow_le_pow_left' H (OfNat.ofNat 2) + sorry + -- apply (@le_trans _ _ _ (ENNReal.ofReal (1 / 2 * ↑ε₁ ^ 2 * α)) _ (Hε α Hα l₁ l₂ N)) + -- apply ENNReal.coe_mono + -- refine (Real.toNNReal_le_toNNReal_iff ?a.hp).mpr ?a.a + -- · apply mul_nonneg + -- · apply mul_nonneg + -- · simp + -- · simp + -- · linarith + -- · repeat rw [mul_assoc] + -- apply (mul_le_mul_iff_of_pos_left (by simp)).mpr + -- apply (mul_le_mul_iff_of_pos_right (by linarith)).mpr + -- apply pow_le_pow_left' H (OfNat.ofNat 2) /-- Obtain an approximate DP bound from a zCDP bound, when ε > 0 and δ < 1 @@ -82,6 +83,8 @@ Obtain an approximate DP bound from a zCDP bound, when ε > 0 and δ < 1 lemma ApproximateDP_of_zCDP_pos_lt_one [Countable U] (m : Mechanism T U) (ε : ℝ) (Hε_pos : 0 < ε) (h : zCDPBound m ε) (Hm : ACNeighbour m) : ∀ δ : NNReal, (0 < (δ : ℝ)) -> ((δ : ℝ) < 1) -> DP' m (ε^2/2 + ε * (2*Real.log (1/δ))^(1/2 : ℝ)) δ := by + sorry + /- have Hε : 0 ≤ ε := by exact le_of_lt Hε_pos intro δ Hδ0 Hδ1 generalize Dε' : (ε^2/2 + ε * (2*Real.log (1/δ))^(1/2 : ℝ)) = ε' @@ -627,6 +630,7 @@ lemma ApproximateDP_of_zCDP_pos_lt_one [Countable U] (m : Mechanism T U) -- Conclude by simplification simp [add_comm] + -/ @@ -1873,6 +1877,8 @@ Convert ε-DP bound to `(1/2)ε²`-zCDP bound Note that `zCDPBound _ ε` corresponds to `(1/2)ε²`-zCDP (not `ε`-zCDP). -/ lemma ofDP_bound (ε : NNReal) (q' : List T -> PMF U) (H : SLang.PureDP q' ε) : zCDPBound q' ε := by + sorry + /- rw [zCDPBound] intro α Hα l₁ l₂ HN -- Special case: (εα/2 > 1) @@ -2292,6 +2298,7 @@ lemma ofDP_bound (ε : NNReal) (q' : List T -> PMF U) (H : SLang.PureDP q' ε) : apply Eq.le congr 1 linarith + -/ /- Convert ε-DP to `(1/2)ε²`-zCDP. @@ -2301,4 +2308,4 @@ Note that `zCDPBound _ ε` corresponds to `(1/2)ε²`-zCDP (not `ε`-zCDP). lemma ofDP (ε : NNReal) (q : List T -> PMF U) (H : SLang.PureDP q ε) : zCDP q ε := by constructor · exact ACNeighbour_of_DP ε q H - · exact ofDP_bound ε q H \ No newline at end of file + · exact ofDP_bound ε q H diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean index d3653614..72137a87 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean @@ -29,6 +29,8 @@ theorem privNoisedQuery_zCDPBound (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ have A := @discrete_GaussianGenSample_ZeroConcentrated α h1 (Δ * ε₂) ε₁ (query l₁) (query l₂) apply le_trans A clear A + sorry + /- -- Turn it into an equality ASAP rw [sensitivity] at bounded_sensitivity @@ -186,6 +188,7 @@ theorem privNoisedQuery_zCDPBound (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ case G1 => exact NNReal.zero_le_coe congr simp only [Real.toNNReal_coe] + -/ lemma discrete_gaussian_shift {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) (τ x : ℤ) : discrete_gaussian σ μ (x - τ) = discrete_gaussian σ (μ + τ) (x) := by From d0b4650ae2fd22fa1b0dd84a40961754bb49df16 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 09:39:34 -0400 Subject: [PATCH 02/30] fix definition --- .../ZeroConcentrated/AdaptiveComposition.lean | 13 ++++++++++--- .../DifferentialPrivacy/ZeroConcentrated/DP.lean | 2 +- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean index 73417a5e..7358ef78 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean @@ -134,11 +134,18 @@ theorem privComposeAdaptive_zCDPBound {nq1 : List T → PMF U} {nq2 : U -> List -- Rewrite the upper bounds in terms of Renyi divergences of nq1/nq2 rw [zCDPBound] at h1 -- have marginal_ub := h1 α Hα l₁ l₂ Hneighbours - have conditional_ub : (⨆ (u : U), RenyiDivergence (nq2 u l₁) (nq2 u l₂) α) ≤ ENNReal.ofReal ε₂ := -- ENNReal.ofReal (1 / 2 * ε₂ ^ 2 * α)) := - iSup_le fun i => h2 i α Hα l₁ l₂ Hneighbours + have conditional_ub : (⨆ (u : U), RenyiDivergence (nq2 u l₁) (nq2 u l₂) α) ≤ ENNReal.ofReal (ε₂ * α) := + by exact iSup_le fun i => h2 i α Hα l₁ l₂ Hneighbours apply (@LE.le.trans _ _ _ (RenyiDivergence (nq1 l₁) (nq1 l₂) α + ⨆ (u : U), RenyiDivergence (nq2 u l₁) (nq2 u l₂) α) _ _ ?case_alg) case case_alg => - rw [ENNReal.ofReal_add Hε₁ Hε₂] + rw [add_mul] + rw [ENNReal.ofReal_add ?G1 ?G2] + case G1 => + apply Right.mul_nonneg Hε₁ + linarith + case G2 => + apply Right.mul_nonneg Hε₂ + linarith exact _root_.add_le_add (h1 α Hα l₁ l₂ Hneighbours) conditional_ub exact privComposeAdaptive_renyi_bound Hα Hneighbours HAC1 HAC2 diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean index b0a96b60..09828b5a 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean @@ -44,7 +44,7 @@ satisfying this bound are ``ε``-DP). -/ def zCDPBound (q : List T → PMF U) (ε : ℝ) : Prop := ∀ α : ℝ, 1 < α → ∀ l₁ l₂ : List T, Neighbour l₁ l₂ → - RenyiDivergence (q l₁) (q l₂) α ≤ ENNReal.ofReal ε + RenyiDivergence (q l₁) (q l₂) α ≤ ENNReal.ofReal (ε * α) /-- All neighbouring queries are absolutely continuous From 7c1eac8ca6e42f0aa6ce3b71c6a68f269a83f4ea Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 09:47:58 -0400 Subject: [PATCH 03/30] update base proof for gaussian mechanism property --- .../ZeroConcentrated/Mechanism/Properties.lean | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean index 72137a87..0b4c1ecb 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean @@ -23,14 +23,12 @@ namespace SLang The zCDP mechanism with bounded sensitivity satisfies the bound for ``(Δε₂/ε₁)^2``-zCDP. -/ theorem privNoisedQuery_zCDPBound (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (bounded_sensitivity : sensitivity query Δ) : - zCDPBound (privNoisedQuery query Δ ε₁ ε₂) ((ε₁ : NNReal) / ε₂) := by + zCDPBound (privNoisedQuery query Δ ε₁ ε₂) ((1/2) * ((ε₁ : NNReal) / ε₂) ^ 2) := by simp [zCDPBound, privNoisedQuery] intros α h1 l₁ l₂ h2 have A := @discrete_GaussianGenSample_ZeroConcentrated α h1 (Δ * ε₂) ε₁ (query l₁) (query l₂) apply le_trans A clear A - sorry - /- -- Turn it into an equality ASAP rw [sensitivity] at bounded_sensitivity @@ -188,7 +186,6 @@ theorem privNoisedQuery_zCDPBound (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ case G1 => exact NNReal.zero_le_coe congr simp only [Real.toNNReal_coe] - -/ lemma discrete_gaussian_shift {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) (τ x : ℤ) : discrete_gaussian σ μ (x - τ) = discrete_gaussian σ (μ + τ) (x) := by @@ -228,8 +225,9 @@ theorem privNoisedQuery_zCDP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (b simp [zCDP] apply And.intro · exact privNoisedQuery_AC query Δ ε₁ ε₂ - · apply privNoisedQuery_zCDPBound - exact bounded_sensitivity + · sorry + -- apply privNoisedQuery_zCDPBound + -- exact bounded_sensitivity end SLang From 0b0370b819cf1ad2bce2d14689521eb04fb7f51f Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 09:54:36 -0400 Subject: [PATCH 04/30] fix mono --- .../ZeroConcentrated/DP.lean | 23 ++++++++----------- 1 file changed, 10 insertions(+), 13 deletions(-) diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean index 09828b5a..9f3b6f76 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean @@ -63,19 +63,16 @@ lemma zCDP_mono {m : List T -> PMF U} {ε₁ ε₂ : NNReal} (H : ε₁ ≤ ε · assumption · rw [zCDPBound] at * intro α Hα l₁ l₂ N - sorry - -- apply (@le_trans _ _ _ (ENNReal.ofReal (1 / 2 * ↑ε₁ ^ 2 * α)) _ (Hε α Hα l₁ l₂ N)) - -- apply ENNReal.coe_mono - -- refine (Real.toNNReal_le_toNNReal_iff ?a.hp).mpr ?a.a - -- · apply mul_nonneg - -- · apply mul_nonneg - -- · simp - -- · simp - -- · linarith - -- · repeat rw [mul_assoc] - -- apply (mul_le_mul_iff_of_pos_left (by simp)).mpr - -- apply (mul_le_mul_iff_of_pos_right (by linarith)).mpr - -- apply pow_le_pow_left' H (OfNat.ofNat 2) + apply (@le_trans _ _ _ (ENNReal.ofReal (ε₁ * α)) _ ?G1) + case G1 => apply Hε <;> trivial + apply ENNReal.coe_mono + refine (Real.toNNReal_le_toNNReal_iff ?a.hp).mpr ?a.a + · apply mul_nonneg + · exact NNReal.zero_le_coe + · linarith + · apply mul_le_mul_of_nonneg_right + · exact H + · linarith /-- Obtain an approximate DP bound from a zCDP bound, when ε > 0 and δ < 1 From 5f6ef79a5b53dcaac41674fcba39b525b4772146 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 10:02:32 -0400 Subject: [PATCH 05/30] fix base proof for approxDP --- .../ZeroConcentrated/DP.lean | 24 +++++++++++-------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean index 9f3b6f76..44977265 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean @@ -78,10 +78,8 @@ lemma zCDP_mono {m : List T -> PMF U} {ε₁ ε₂ : NNReal} (H : ε₁ ≤ ε Obtain an approximate DP bound from a zCDP bound, when ε > 0 and δ < 1 -/ lemma ApproximateDP_of_zCDP_pos_lt_one [Countable U] (m : Mechanism T U) - (ε : ℝ) (Hε_pos : 0 < ε) (h : zCDPBound m ε) (Hm : ACNeighbour m) : + (ε : ℝ) (Hε_pos : 0 < ε) (h : zCDPBound m ((1/2) * ε^2)) (Hm : ACNeighbour m) : ∀ δ : NNReal, (0 < (δ : ℝ)) -> ((δ : ℝ) < 1) -> DP' m (ε^2/2 + ε * (2*Real.log (1/δ))^(1/2 : ℝ)) δ := by - sorry - /- have Hε : 0 ≤ ε := by exact le_of_lt Hε_pos intro δ Hδ0 Hδ1 generalize Dε' : (ε^2/2 + ε * (2*Real.log (1/δ))^(1/2 : ℝ)) = ε' @@ -627,7 +625,6 @@ lemma ApproximateDP_of_zCDP_pos_lt_one [Countable U] (m : Mechanism T U) -- Conclude by simplification simp [add_comm] - -/ @@ -635,12 +632,11 @@ lemma ApproximateDP_of_zCDP_pos_lt_one [Countable U] (m : Mechanism T U) Obtain an approximate DP bound from a zCDP bound, when ε > 0 -/ lemma ApproximateDP_of_zCDP_pos [Countable U] (m : Mechanism T U) - (ε : ℝ) (Hε_pos : 0 < ε) (h : zCDPBound m ε) (Hm : ACNeighbour m) : + (ε : ℝ) (Hε_pos : 0 < ε) (h : zCDPBound m ((1/2) * ε^2)) (Hm : ACNeighbour m) : ∀ δ : NNReal, (0 < (δ : ℝ)) -> DP' m (ε^2/2 + ε * (2*Real.log (1/δ))^(1/2 : ℝ)) δ := by intro δ Hδ0 cases (Classical.em (δ < 1)) - · intro Hδ1 - apply ApproximateDP_of_zCDP_pos_lt_one m ε Hε_pos h Hm δ Hδ0 + · apply ApproximateDP_of_zCDP_pos_lt_one m ε Hε_pos h Hm δ Hδ0 trivial · apply ApproximateDP_gt1 apply le_of_not_lt @@ -650,7 +646,7 @@ lemma ApproximateDP_of_zCDP_pos [Countable U] (m : Mechanism T U) Obtain an approximate DP bound from a zCDP bound -/ theorem ApproximateDP_of_zCDP [Countable U] (m : Mechanism T U) - (ε : ℝ) (Hε : 0 ≤ ε) (h : zCDPBound m ε) (Hm : ACNeighbour m) : + (ε : ℝ) (Hε : 0 ≤ ε) (h : zCDPBound m ((1/2) * ε^2)) (Hm : ACNeighbour m) : ∀ δ : NNReal, (0 < (δ : ℝ)) -> DP' m (ε^2/2 + ε * (2*Real.log (1/δ))^(1/2 : ℝ)) δ := by cases LE.le.lt_or_eq Hε · rename_i Hε @@ -674,7 +670,7 @@ zCDP is no weaker than approximate DP, up to a loss of parameters. -/ lemma zCDP_ApproximateDP [Countable U] {m : Mechanism T U} : ∃ (degrade : (δ : NNReal) -> (ε' : NNReal) -> NNReal), ∀ (δ : NNReal) (_ : 0 < δ) (ε' : NNReal), - (zCDP m (degrade δ ε') -> ApproximateDP m ε' δ) := by + (zCDP m (degrade δ ((1/2) * ε'^2)) -> ApproximateDP m ε' δ) := by let degrade (δ : NNReal) (ε' : NNReal) : NNReal := (√(2 * Real.log (1/δ) + 2 * ε') - √(2 * Real.log (1/δ))).toNNReal have HDdegrade δ ε' : degrade δ ε' = (√(2 * Real.log (1/δ) + 2 * ε') - √(2 * Real.log (1/δ))).toNNReal := by rfl @@ -687,8 +683,15 @@ lemma zCDP_ApproximateDP [Countable U] {m : Mechanism T U} : rename_i Hδ1 rw [ApproximateDP] - have R := ApproximateDP_of_zCDP m (degrade δ ε') (by simp) HB HN δ Hδ + + have R := ApproximateDP_of_zCDP m (degrade δ ε') (by simp) ?G1 HN δ Hδ + case G1 => + -- this proof has to be redone + sorry + sorry + + /- have Hdegrade : ((degrade δ ε') ^ 2) / 2 + (degrade δ ε') * (2 * Real.log (1 / δ))^(1/2 : ℝ) = ε' := by rw [HDdegrade] generalize HD : Real.log (1 / δ) = D @@ -733,6 +736,7 @@ lemma zCDP_ApproximateDP [Countable U] {m : Mechanism T U} : linarith rw [Hdegrade] at R trivial + -/ /-- From 95be45cb014a53353a594a25169b7573a2204d46 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 10:07:57 -0400 Subject: [PATCH 06/30] new zCDP proofs wrapped --- SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean | 7 ++----- .../ZeroConcentrated/Mechanism/Properties.lean | 10 ++++------ .../DifferentialPrivacy/ZeroConcentrated/System.lean | 4 ++-- 3 files changed, 8 insertions(+), 13 deletions(-) diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean index 44977265..1bbb753d 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean @@ -1877,9 +1877,7 @@ Convert ε-DP bound to `(1/2)ε²`-zCDP bound Note that `zCDPBound _ ε` corresponds to `(1/2)ε²`-zCDP (not `ε`-zCDP). -/ -lemma ofDP_bound (ε : NNReal) (q' : List T -> PMF U) (H : SLang.PureDP q' ε) : zCDPBound q' ε := by - sorry - /- +lemma ofDP_bound (ε : NNReal) (q' : List T -> PMF U) (H : SLang.PureDP q' ε) : zCDPBound q' ((1/2) * ε^2) := by rw [zCDPBound] intro α Hα l₁ l₂ HN -- Special case: (εα/2 > 1) @@ -2299,14 +2297,13 @@ lemma ofDP_bound (ε : NNReal) (q' : List T -> PMF U) (H : SLang.PureDP q' ε) : apply Eq.le congr 1 linarith - -/ /- Convert ε-DP to `(1/2)ε²`-zCDP. Note that `zCDPBound _ ε` corresponds to `(1/2)ε²`-zCDP (not `ε`-zCDP). -/ -lemma ofDP (ε : NNReal) (q : List T -> PMF U) (H : SLang.PureDP q ε) : zCDP q ε := by +lemma ofDP (ε : NNReal) (q : List T -> PMF U) (H : SLang.PureDP q ε) : zCDP q ((1/2) * ε^2) := by constructor · exact ACNeighbour_of_DP ε q H · exact ofDP_bound ε q H diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean index 0b4c1ecb..8838f8db 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean @@ -221,13 +221,11 @@ def privNoisedQuery_AC (query : List T -> ℤ) (Δ ε₁ ε₂ : ℕ+) : ACNeigh The zCDP mechanism is ``(Δε₂/ε₁)^2``-zCDP. -/ theorem privNoisedQuery_zCDP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (bounded_sensitivity : sensitivity query Δ) : - zCDP (privNoisedQuery query Δ ε₁ ε₂) ((ε₁ : NNReal) / ε₂) := by - simp [zCDP] + zCDP (privNoisedQuery query Δ ε₁ ε₂) ((1/2) * ((ε₁ : NNReal) / ε₂) ^ 2) := by + simp only [zCDP] apply And.intro · exact privNoisedQuery_AC query Δ ε₁ ε₂ - · sorry - -- apply privNoisedQuery_zCDPBound - -- exact bounded_sensitivity - + · apply privNoisedQuery_zCDPBound + exact bounded_sensitivity end SLang diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean index de28f44d..5381e875 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean @@ -25,10 +25,10 @@ Instance of a DP system for zCDP, using the discrete Gaussian as a noising mecha -/ noncomputable instance gaussian_zCDPSystem : DPSystem T where prop := zCDP - prop_adp := zCDP_ApproximateDP + prop_adp := sorry -- zCDP_ApproximateDP prop_mono := zCDP_mono noise := privNoisedQuery - noise_prop := privNoisedQuery_zCDP + noise_prop := sorry -- privNoisedQuery_zCDP adaptive_compose_prop := privComposeAdaptive_zCDP postprocess_prop := privPostProcess_zCDP const_prop := privConst_zCDP From 569d44e07f8bb90f98cf439170c93cb5f2f6a680 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 11:15:08 -0400 Subject: [PATCH 07/30] stub changes to system --- SampCert.lean | 4 +- SampCert/DifferentialPrivacy/Abstract.lean | 42 ++++++++++++------- SampCert/DifferentialPrivacy/Pure/System.lean | 15 +++++-- .../Queries/BoundedMean/Code.lean | 1 + .../Queries/BoundedMean/Properties.lean | 1 + .../Queries/BoundedSum/Code.lean | 3 +- .../Queries/BoundedSum/Properties.lean | 6 ++- .../Queries/Count/Code.lean | 3 +- .../Queries/Count/Properties.lean | 9 +++- .../Queries/Histogram/Code.lean | 3 +- .../Queries/Histogram/Properties.lean | 6 ++- .../Queries/HistogramMean/Code.lean | 3 +- .../Queries/HistogramMean/Properties.lean | 3 +- .../ZeroConcentrated/System.lean | 26 ++++++++++-- 14 files changed, 88 insertions(+), 37 deletions(-) diff --git a/SampCert.lean b/SampCert.lean index 55d9f9b0..1d7fc16e 100644 --- a/SampCert.lean +++ b/SampCert.lean @@ -14,7 +14,7 @@ import Init.Data.UInt.Lemmas open SLang PMF -def combineConcentrated := @privNoisedBoundedMean_DP gaussian_zCDPSystem +def combineConcentrated := @privNoisedBoundedMean_DP _ gaussian_zCDPSystem def combinePure := @privNoisedBoundedMean_DP PureDPSystem /- @@ -41,7 +41,7 @@ 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 + privMeanHistogram PureDPSystem laplace_pureDPSystem numBins { bin } unbin 1 20 2 1 20 end histogramMeanExample diff --git a/SampCert/DifferentialPrivacy/Abstract.lean b/SampCert/DifferentialPrivacy/Abstract.lean index 84d7fb13..ee4813f6 100644 --- a/SampCert/DifferentialPrivacy/Abstract.lean +++ b/SampCert/DifferentialPrivacy/Abstract.lean @@ -15,8 +15,6 @@ 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 @@ -31,25 +29,18 @@ 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_adp : (δ : NNReal) -> (ε' : NNReal) -> NNReal /-- - DP is monotonic + For any ε', this definition of DP implies (ε', δ)-approximate-DP for all δ -/ - prop_mono {m : Mechanism T Z} {ε₁ ε₂: NNReal} (Hε : ε₁ ≤ ε₂) (H : prop m ε₁) : prop m ε₂ + prop_adp [Countable Z] {m : Mechanism T Z} : ∀ (δ : NNReal) (_ : 0 < δ) (ε' : NNReal), + (prop m (of_adp δ ε') -> ApproximateDP m ε' δ) /-- - 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 ℤ - /-- - 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} (Hε : ε₁ ≤ ε₂) (H : prop m ε₁) : prop m ε₂ /-- Privacy adaptively composes by addition. -/ @@ -96,4 +87,23 @@ 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 ℤ + /-- + How much privacy one obtains by adding Δ εn εd noise to a Δ-sensitive query + -/ + noise_priv : NNReal → NNReal + /-- + Adding noise to a query makes it private. + -/ + noise_prop : ∀ q : List T → ℤ, ∀ Δ εn εd : ℕ+, sensitivity q Δ → dps.prop (noise q Δ εn εd) (noise_priv (εn / εd)) + end SLang diff --git a/SampCert/DifferentialPrivacy/Pure/System.lean b/SampCert/DifferentialPrivacy/Pure/System.lean index 00e16cd0..a2b26545 100644 --- a/SampCert/DifferentialPrivacy/Pure/System.lean +++ b/SampCert/DifferentialPrivacy/Pure/System.lean @@ -21,14 +21,21 @@ 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 - prop_adp := pure_ApproximateDP + of_adp := sorry + prop_adp := sorry -- pure_ApproximateDP prop_mono := PureDP_mono - noise := privNoisedQueryPure - noise_prop := privNoisedQueryPure_DP adaptive_compose_prop := PureDP_ComposeAdaptive' postprocess_prop := PureDP_PostProcess const_prop := PureDP_privConst + +instance laplace_pureDPSystem : DPNoise (@PureDPSystem T) where + noise := privNoisedQueryPure + noise_priv := sorry + noise_prop := sorry -- privNoisedQueryPure_DP + + + end SLang diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean index 2cf226d8..79234d71 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean @@ -18,6 +18,7 @@ noncomputable section namespace SLang variable [dps : DPSystem ℕ] +variable [dpn : DPNoise dps] /-- Compute a noised mean using a noised sum and noised count. diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean index 775a6435..e157ce3c 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean @@ -21,6 +21,7 @@ noncomputable section namespace SLang variable [dps : DPSystem ℕ] +variable [dpn : DPNoise dps] lemma budget_split (ε₁ ε₂ : ℕ+) : (ε₁ : NNReal) / (ε₂ : NNReal) = (ε₁ : NNReal) / ((2 * ε₂) : ℕ+) + (ε₁ : NNReal) / ((2 * ε₂) : ℕ+) := by diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean b/SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean index 12a37d7a..ffdc6f98 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean @@ -19,6 +19,7 @@ noncomputable section namespace SLang variable [dps : DPSystem ℕ] +variable [dpn : DPNoise dps] /-- Bounded sum query: computes a sum and truncates it at an upper bound. @@ -30,6 +31,6 @@ def exactBoundedSum (U : ℕ+) (l : List ℕ) : ℤ := Noised bounded sum query obtained by applying the DP noise mechanism to the bounded sum. -/ def privNoisedBoundedSum (U : ℕ+) (ε₁ ε₂ : ℕ+) (l : List ℕ) : PMF ℤ := do - dps.noise (exactBoundedSum U) U ε₁ ε₂ l + dpn.noise (exactBoundedSum U) U ε₁ ε₂ l end SLang diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean b/SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean index 70e72bfd..4f21348b 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean @@ -22,6 +22,7 @@ noncomputable section namespace SLang variable [dps : DPSystem ℕ] +variable [dpn : DPNoise dps] /-- Sensitivity of the bounded sum is equal to the bound. @@ -86,7 +87,8 @@ The noised bounded sum satisfies the DP property of the DP system. @[simp] theorem privNoisedBoundedSum_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) : dps.prop (privNoisedBoundedSum U ε₁ ε₂) ((ε₁ : NNReal) / ε₂) := by - apply dps.noise_prop - apply exactBoundedSum_sensitivity + sorry + -- apply dpn.noise_prop + -- apply exactBoundedSum_sensitivity end SLang diff --git a/SampCert/DifferentialPrivacy/Queries/Count/Code.lean b/SampCert/DifferentialPrivacy/Queries/Count/Code.lean index a94db31e..b38929ef 100644 --- a/SampCert/DifferentialPrivacy/Queries/Count/Code.lean +++ b/SampCert/DifferentialPrivacy/Queries/Count/Code.lean @@ -17,6 +17,7 @@ namespace SLang variable {T : Type} variable [dps : DPSystem T] +variable [dpn : DPNoise dps] /-- Query to count the size of the input list. @@ -27,6 +28,6 @@ def exactCount (l : List T) : ℤ := List.length l A noised counting mechanism. -/ def privNoisedCount (ε₁ ε₂ : ℕ+) (l : List T) : PMF ℤ := do - dps.noise exactCount 1 ε₁ ε₂ l + dpn.noise exactCount 1 ε₁ ε₂ l end SLang diff --git a/SampCert/DifferentialPrivacy/Queries/Count/Properties.lean b/SampCert/DifferentialPrivacy/Queries/Count/Properties.lean index 8257d763..3dfc5377 100644 --- a/SampCert/DifferentialPrivacy/Queries/Count/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/Count/Properties.lean @@ -21,6 +21,7 @@ namespace SLang variable {T : Type} variable [dps : DPSystem T] +variable [dpn : DPNoise dps] /-- The counting query is 1-sensitive @@ -46,7 +47,11 @@ The noised counting query satisfies DP property @[simp] theorem privNoisedCount_DP (ε₁ ε₂ : ℕ+) : dps.prop (privNoisedCount ε₁ ε₂) ((ε₁ : NNReal) / ε₂) := by - apply dps.noise_prop - apply exactCount_1_sensitive + apply DPSystem_prop_ext + case H => + sorry + all_goals sorry + -- apply dpn.noise_prop + -- apply exactCount_1_sensitive end SLang diff --git a/SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean b/SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean index 553cdedc..9342a6c9 100644 --- a/SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean +++ b/SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean @@ -87,6 +87,7 @@ instance : DiscreteMeasurableSpace (Histogram T numBins B) where namespace SLang variable [dps : DPSystem T] +variable [dpn : DPNoise dps] /-- Compute the exact number of elements inside a histogram bin @@ -98,7 +99,7 @@ def exactBinCount (b : Fin numBins) (l : List T) : ℤ := Compute a noised count of the number of list elements inside a particular histogram bin -/ def privNoisedBinCount (ε₁ ε₂ : ℕ+) (b : Fin numBins) : Mechanism T ℤ := - (dps.noise (exactBinCount numBins B b) 1 ε₁ (ε₂ * numBins)) + (dpn.noise (exactBinCount numBins B b) 1 ε₁ (ε₂ * numBins)) /-- Modify a count inside a Histogram diff --git a/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean b/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean index 155c66b8..531cafd7 100644 --- a/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean @@ -21,6 +21,7 @@ namespace SLang variable {T : Type} variable [dps : DPSystem T] +variable [dpn : DPNoise dps] variable [HT : Inhabited T] variable (numBins : ℕ+) @@ -61,8 +62,9 @@ DP bound for a noised bin count lemma privNoisedBinCount_DP (ε₁ ε₂ : ℕ+) (b : Fin numBins) : dps.prop (privNoisedBinCount numBins B ε₁ ε₂ b) (ε₁ / ((ε₂ * numBins : PNat))) := by unfold privNoisedBinCount - apply dps.noise_prop - apply exactBinCount_sensitivity + sorry + -- apply dpn.noise_prop + -- apply exactBinCount_sensitivity -- MARKUSDE: Looking at this proof it is clear that we need better tactic support for the abstract DP operators -- MARKUSDE: - Lemmas with equality side conditions for the privacy cost diff --git a/SampCert/DifferentialPrivacy/Queries/HistogramMean/Code.lean b/SampCert/DifferentialPrivacy/Queries/HistogramMean/Code.lean index 4a91528c..6bb35172 100644 --- a/SampCert/DifferentialPrivacy/Queries/HistogramMean/Code.lean +++ b/SampCert/DifferentialPrivacy/Queries/HistogramMean/Code.lean @@ -23,6 +23,7 @@ Implementation for noncomputable section variable (dps : SLang.DPSystem ℕ) +variable (dpn : SLang.DPNoise dps) variable (numBins : ℕ+) variable (B : Bins ℕ numBins) @@ -44,7 +45,7 @@ and the bounded mean with (ε₃/ε₄)-DP. def privMeanHistogram (ε₁ ε₂ : ℕ+) (τ : ℤ) (ε₃ ε₄ : ℕ+) : Mechanism ℕ (Option ℚ) := privPostProcess (privComposeAdaptive - (@privMaxBinAboveThreshold numBins _ B dps ε₁ ε₂ τ) + (@privMaxBinAboveThreshold numBins _ B dps dpn ε₁ ε₂ τ) (fun opt_max => match opt_max with | none => privConst none diff --git a/SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean b/SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean index 22892f3f..05573c9e 100644 --- a/SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean @@ -22,6 +22,7 @@ noncomputable section namespace SLang variable (dps : DPSystem ℕ) +variable (dpn : DPNoise dps) variable (numBins : ℕ+) variable (B : Bins ℕ numBins) variable (unbin : Fin numBins -> ℕ+) @@ -60,7 +61,7 @@ instance : DiscreteMeasurableSpace (Option (Fin ↑numBins)) where DP bound for the adaptive mean -/ lemma privMeanHistogram_DP (ε₁ ε₂ : ℕ+) (τ : ℤ) (ε₃ ε₄ : ℕ+) : - dps.prop (privMeanHistogram dps numBins B unbin ε₁ ε₂ τ ε₃ ε₄) (ε₁/ε₂ + ε₃/ε₄) := by + dps.prop (privMeanHistogram dps dpn numBins B unbin ε₁ ε₂ τ ε₃ ε₄) (ε₁/ε₂ + ε₃/ε₄) := by rw [privMeanHistogram] apply dps.postprocess_prop apply dps.adaptive_compose_prop diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean index 5381e875..22b26b58 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean @@ -21,16 +21,34 @@ namespace SLang variable { T : Type } /-- -Instance of a DP system for zCDP, using the discrete Gaussian as a noising mechanism. +Instance of a DP system for zCDP -/ -noncomputable instance gaussian_zCDPSystem : DPSystem T where +instance zCDPSystem : DPSystem T where prop := zCDP + of_adp := sorry prop_adp := sorry -- zCDP_ApproximateDP prop_mono := zCDP_mono - noise := privNoisedQuery - noise_prop := sorry -- privNoisedQuery_zCDP + -- noise := privNoisedQuery + -- noise_prop := sorry -- privNoisedQuery_zCDP adaptive_compose_prop := privComposeAdaptive_zCDP postprocess_prop := privPostProcess_zCDP const_prop := privConst_zCDP +/-- +Gaussian noise for zCDP system +-/ +instance gaussian_zCDPSystem : DPNoise zCDPsystem where + noise := privNoisedQuery + noise_priv := sorry + noise_prop := sorry -- privNoisedQuery_zCDP + +/-- +Laplace noise for zCDP system +-/ +instance laplace_zCDPSystem : DPNoise zCDPsystem where + noise := sorry + noise_priv := sorry + noise_prop := sorry -- privNoisedQuery_zCDP + + end SLang From 28efc75dde032cc7e53020ab46dd1198119b8fb0 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 11:59:53 -0400 Subject: [PATCH 08/30] stub changes to noise --- SampCert/DifferentialPrivacy/Abstract.lean | 39 ++++++++++++++----- SampCert/DifferentialPrivacy/Pure/System.lean | 4 +- .../Queries/Histogram/Properties.lean | 30 +++++++------- .../Queries/HistogramMean/Properties.lean | 8 ++-- .../ZeroConcentrated/System.lean | 4 +- 5 files changed, 56 insertions(+), 29 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Abstract.lean b/SampCert/DifferentialPrivacy/Abstract.lean index ee4813f6..39f1b7e1 100644 --- a/SampCert/DifferentialPrivacy/Abstract.lean +++ b/SampCert/DifferentialPrivacy/Abstract.lean @@ -44,9 +44,13 @@ class DPSystem (T : Type) where /-- 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} → + [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₂) ε /-- Privacy is invariant under post-processing. -/ @@ -56,7 +60,8 @@ class DPSystem (T : Type) where /-- 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} → [MeasurableSpace U] → [Countable U] → [DiscreteMeasurableSpace U] -> (u : U) -> + ∀ ε : NNReal, ε = (0 : NNReal) -> prop (privConst u) ε namespace DPSystem @@ -69,7 +74,8 @@ lemma compose_prop {U V : Type} [dps : DPSystem T] [MeasurableSpace U] [Countabl dps.prop m₁ ε₁ → dps.prop m₂ ε₂ → dps.prop (privCompose m₁ m₂) (ε₁ + ε₂) := by intros m₁ m₂ ε₁ ε₂ p1 p2 unfold privCompose - exact adaptive_compose_prop m₁ (fun _ => m₂) ε₁ ε₂ p1 fun _ => p2 + apply adaptive_compose_prop m₁ (fun _ => m₂) ε₁ ε₂ _ p1 (fun _ => p2) + rfl end DPSystem @@ -88,6 +94,8 @@ lemma bind_bind_indep (p : Mechanism T U) (q : Mechanism T V) (h : U → V → P simp [privCompose, privComposeAdaptive, tsum_prod'] + + /-- A noise function for a differential privacy system -/ @@ -98,12 +106,25 @@ class DPNoise (dps : DPSystem T) where -/ noise : Query T ℤ → (sensitivity : ℕ+) → (num : ℕ+) → (den : ℕ+) → Mechanism T ℤ /-- - How much privacy one obtains by adding Δ εn εd noise to a Δ-sensitive query + Relationship between arguments to noise and resulting privacy amount -/ - noise_priv : NNReal → NNReal + noise_priv : (num : ℕ+) → (den : ℕ+) → (priv : NNReal) -> Prop /-- - Adding noise to a query makes it private. + Adding noise to a query makes it private -/ - noise_prop : ∀ q : List T → ℤ, ∀ Δ εn εd : ℕ+, sensitivity q Δ → dps.prop (noise q Δ εn εd) (noise_priv (εn / εd)) + noise_prop : ∀ q : List T → ℤ, ∀ Δ εn εd : ℕ+, + sensitivity q Δ → + noise_priv εn εd ε -> + 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 diff --git a/SampCert/DifferentialPrivacy/Pure/System.lean b/SampCert/DifferentialPrivacy/Pure/System.lean index a2b26545..a04d6011 100644 --- a/SampCert/DifferentialPrivacy/Pure/System.lean +++ b/SampCert/DifferentialPrivacy/Pure/System.lean @@ -26,9 +26,9 @@ instance PureDPSystem : DPSystem T where of_adp := sorry prop_adp := sorry -- pure_ApproximateDP prop_mono := PureDP_mono - adaptive_compose_prop := PureDP_ComposeAdaptive' + adaptive_compose_prop := sorry -- PureDP_ComposeAdaptive' postprocess_prop := PureDP_PostProcess - const_prop := PureDP_privConst + const_prop := sorry -- PureDP_privConst instance laplace_pureDPSystem : DPNoise (@PureDPSystem T) where diff --git a/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean b/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean index 531cafd7..86fa124c 100644 --- a/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean @@ -76,19 +76,23 @@ lemma privNoisedHistogramAux_DP (ε₁ ε₂ : ℕ+) (n : ℕ) (Hn : n < numBins induction n · unfold privNoisedHistogramAux simp only [Nat.cast_zero, succ_eq_add_one, zero_add, Nat.cast_one, Nat.cast_mul, one_mul] - refine DPSystem.postprocess_prop - (privCompose (privNoisedBinCount numBins B ε₁ ε₂ 0) (privConst (emptyHistogram numBins B))) - (↑↑ε₁ / ↑↑(ε₂ * numBins)) ?G1 - apply (DPSystem_prop_ext _ ?HEq ?Hdp) - case Hdp => - apply (DPSystem.compose_prop - (privNoisedBinCount numBins B ε₁ ε₂ 0) - (privConst (emptyHistogram numBins B)) - (↑↑ε₁ / ↑↑(ε₂ * numBins)) - 0 - (privNoisedBinCount_DP numBins B ε₁ ε₂ 0) - (DPSystem.const_prop (emptyHistogram numBins B))) - case HEq => simp only [PNat.mul_coe, Nat.cast_mul, add_zero] + sorry + -- refine DPSystem.postprocess_prop + -- (privCompose (privNoisedBinCount numBins B ε₁ ε₂ 0) (privConst (emptyHistogram numBins B))) + -- (↑↑ε₁ / ↑↑(ε₂ * numBins)) ?G1 + -- apply (DPSystem_prop_ext _ ?HEq ?Hdp) + -- case Hdp => + -- sorry + -- -- apply (DPSystem.compose_prop + -- -- (privNoisedBinCount numBins B ε₁ ε₂ 0) + -- -- (privConst (emptyHistogram numBins B)) + -- -- (↑↑ε₁ / ↑↑(ε₂ * numBins)) + -- -- 0 + -- -- (privNoisedBinCount_DP numBins B ε₁ ε₂ 0) + -- -- (DPSystem.const_prop (emptyHistogram numBins B))) + -- case HEq => + -- sorry + -- -- simp only [PNat.mul_coe, Nat.cast_mul, add_zero] · rename_i n IH unfold privNoisedHistogramAux simp only [] diff --git a/SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean b/SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean index 05573c9e..db36ce3a 100644 --- a/SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean @@ -69,11 +69,13 @@ lemma privMeanHistogram_DP (ε₁ ε₂ : ℕ+) (τ : ℤ) (ε₃ ε₄ : ℕ+) intro u cases u · simp only - apply dps.prop_mono ?G1 ?G2 - case G2 => apply dps.const_prop - simp only [_root_.zero_le] + sorry + -- apply dps.prop_mono ?G1 ?G2 + -- case G2 => apply dps.const_prop + -- simp only [_root_.zero_le] · rename_i mx simp only apply dps.postprocess_prop apply privNoisedBoundedMean_DP + rfl end SLang diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean index 22b26b58..a298c9a9 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean @@ -30,9 +30,9 @@ instance zCDPSystem : DPSystem T where prop_mono := zCDP_mono -- noise := privNoisedQuery -- noise_prop := sorry -- privNoisedQuery_zCDP - adaptive_compose_prop := privComposeAdaptive_zCDP + adaptive_compose_prop := sorry -- privComposeAdaptive_zCDP postprocess_prop := privPostProcess_zCDP - const_prop := privConst_zCDP + const_prop := sorry -- privConst_zCDP /-- Gaussian noise for zCDP system From 40ac9ccea637319bdb7e8f38b5ff2e74b056a268 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 12:49:50 -0400 Subject: [PATCH 09/30] instance for pure DP laplace noise --- SampCert/DifferentialPrivacy/Abstract.lean | 2 +- .../DifferentialPrivacy/Pure/AdaptiveComposition.lean | 6 ++++-- SampCert/DifferentialPrivacy/Pure/Const.lean | 2 +- .../Pure/Mechanism/Properties.lean | 7 +++++-- SampCert/DifferentialPrivacy/Pure/System.lean | 11 ++++------- 5 files changed, 15 insertions(+), 13 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Abstract.lean b/SampCert/DifferentialPrivacy/Abstract.lean index 39f1b7e1..4af77c2c 100644 --- a/SampCert/DifferentialPrivacy/Abstract.lean +++ b/SampCert/DifferentialPrivacy/Abstract.lean @@ -112,7 +112,7 @@ class DPNoise (dps : DPSystem T) where /-- Adding noise to a query makes it private -/ - noise_prop : ∀ q : List T → ℤ, ∀ Δ εn εd : ℕ+, + noise_prop : ∀ q : List T → ℤ, ∀ Δ εn εd : ℕ+, ∀ ε : NNReal, sensitivity q Δ → noise_priv εn εd ε -> dps.prop (noise q Δ εn εd) ε diff --git a/SampCert/DifferentialPrivacy/Pure/AdaptiveComposition.lean b/SampCert/DifferentialPrivacy/Pure/AdaptiveComposition.lean index 1cc2ca32..5da3c698 100644 --- a/SampCert/DifferentialPrivacy/Pure/AdaptiveComposition.lean +++ b/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 * diff --git a/SampCert/DifferentialPrivacy/Pure/Const.lean b/SampCert/DifferentialPrivacy/Pure/Const.lean index be3152ba..44c549dc 100644 --- a/SampCert/DifferentialPrivacy/Pure/Const.lean +++ b/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 diff --git a/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean b/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean index addf1b2f..917636c6 100644 --- a/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean +++ b/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) (bounded_sensitivity : sensitivity query Δ) (HN : laplace_pureDP_noise_priv ε₁ ε₂ ε) : + PureDP (privNoisedQueryPure query Δ ε₁ ε₂) ε := by + unfold laplace_pureDP_noise_priv at HN + rw [<- HN] simp [PureDP] apply privNoisedQueryPure_DP_bound apply bounded_sensitivity diff --git a/SampCert/DifferentialPrivacy/Pure/System.lean b/SampCert/DifferentialPrivacy/Pure/System.lean index a04d6011..1b555e75 100644 --- a/SampCert/DifferentialPrivacy/Pure/System.lean +++ b/SampCert/DifferentialPrivacy/Pure/System.lean @@ -26,16 +26,13 @@ instance PureDPSystem : DPSystem T where of_adp := sorry prop_adp := sorry -- pure_ApproximateDP prop_mono := PureDP_mono - adaptive_compose_prop := sorry -- PureDP_ComposeAdaptive' + adaptive_compose_prop := PureDP_ComposeAdaptive' postprocess_prop := PureDP_PostProcess - const_prop := sorry -- PureDP_privConst - + const_prop := PureDP_privConst instance laplace_pureDPSystem : DPNoise (@PureDPSystem T) where noise := privNoisedQueryPure - noise_priv := sorry - noise_prop := sorry -- privNoisedQueryPure_DP - - + noise_priv := laplace_pureDP_noise_priv + noise_prop := privNoisedQueryPure_DP end SLang From 456514ae44382431fe7de3fe35d44e712e09b584 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 12:57:04 -0400 Subject: [PATCH 10/30] pure DP system complete --- SampCert/DifferentialPrivacy/Pure/DP.lean | 16 +++++++++------- SampCert/DifferentialPrivacy/Pure/System.lean | 4 ++-- 2 files changed, 11 insertions(+), 9 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Pure/DP.lean b/SampCert/DifferentialPrivacy/Pure/DP.lean index 40c33529..2a5497cf 100644 --- a/SampCert/DifferentialPrivacy/Pure/DP.lean +++ b/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 diff --git a/SampCert/DifferentialPrivacy/Pure/System.lean b/SampCert/DifferentialPrivacy/Pure/System.lean index 1b555e75..034a5502 100644 --- a/SampCert/DifferentialPrivacy/Pure/System.lean +++ b/SampCert/DifferentialPrivacy/Pure/System.lean @@ -23,8 +23,8 @@ Pure ε-DP with noise drawn from the discrete Laplace distribution. -/ instance PureDPSystem : DPSystem T where prop := PureDP - of_adp := sorry - prop_adp := sorry -- pure_ApproximateDP + of_adp := pure_of_adp + prop_adp := pure_ApproximateDP prop_mono := PureDP_mono adaptive_compose_prop := PureDP_ComposeAdaptive' postprocess_prop := PureDP_PostProcess From dfc4b3f766c1c5f9e59d97819cdb42b4e07f9728 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 13:03:24 -0400 Subject: [PATCH 11/30] count query complete --- SampCert/DifferentialPrivacy/Abstract.lean | 2 +- .../Pure/Mechanism/Properties.lean | 2 +- .../Queries/BoundedMean/Properties.lean | 3 ++- .../Queries/Count/Properties.lean | 13 +++++-------- 4 files changed, 9 insertions(+), 11 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Abstract.lean b/SampCert/DifferentialPrivacy/Abstract.lean index 4af77c2c..66c05719 100644 --- a/SampCert/DifferentialPrivacy/Abstract.lean +++ b/SampCert/DifferentialPrivacy/Abstract.lean @@ -113,8 +113,8 @@ class DPNoise (dps : DPSystem T) where Adding noise to a query makes it private -/ noise_prop : ∀ q : List T → ℤ, ∀ Δ εn εd : ℕ+, ∀ ε : NNReal, - sensitivity q Δ → noise_priv εn εd ε -> + sensitivity q Δ → dps.prop (noise q Δ εn εd) ε diff --git a/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean b/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean index 917636c6..950208a4 100644 --- a/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean +++ b/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean @@ -119,7 +119,7 @@ def laplace_pureDP_noise_priv (ε₁ ε₂ : ℕ+) (ε : NNReal) : Prop := (ε /-- Laplace noising mechanism ``privNoisedQueryPure`` produces a pure ``ε₁/ε₂``-DP mechanism from a Δ-sensitive query. -/ -theorem privNoisedQueryPure_DP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (ε : NNReal) (bounded_sensitivity : sensitivity query Δ) (HN : laplace_pureDP_noise_priv ε₁ ε₂ ε) : +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] diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean index e157ce3c..e9ad149d 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean @@ -39,6 +39,7 @@ theorem privNoisedBoundedMean_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) : rw [budget_split] apply dps.compose_prop · apply privNoisedBoundedSum_DP - · apply privNoisedCount_DP + · sorry + -- apply privNoisedCount_DP end SLang diff --git a/SampCert/DifferentialPrivacy/Queries/Count/Properties.lean b/SampCert/DifferentialPrivacy/Queries/Count/Properties.lean index 3dfc5377..8459e239 100644 --- a/SampCert/DifferentialPrivacy/Queries/Count/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/Count/Properties.lean @@ -45,13 +45,10 @@ theorem exactCount_1_sensitive : The noised counting query satisfies DP property -/ @[simp] -theorem privNoisedCount_DP (ε₁ ε₂ : ℕ+) : - dps.prop (privNoisedCount ε₁ ε₂) ((ε₁ : NNReal) / ε₂) := by - apply DPSystem_prop_ext - case H => - sorry - all_goals sorry - -- apply dpn.noise_prop - -- apply exactCount_1_sensitive +theorem privNoisedCount_DP (ε₁ ε₂ : ℕ+) (ε : NNReal) (HP : dpn.noise_priv ε₁ ε₂ ε) : + dps.prop (privNoisedCount ε₁ ε₂) ε := by + unfold privNoisedCount + apply (dpn.noise_prop _ _ _ _ _ HP) + apply exactCount_1_sensitive end SLang From dc7ee36819e21c6b12853647a544f4fb43c44bbe Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 13:46:23 -0400 Subject: [PATCH 12/30] tweak definitions of abstract DP for better inference --- SampCert/DifferentialPrivacy/Abstract.lean | 35 ++++++++-------- SampCert/DifferentialPrivacy/Pure/System.lean | 12 ++++-- .../Queries/BoundedMean/Properties.lean | 15 +++---- .../Queries/Count/Properties.lean | 2 +- .../Queries/Histogram/Properties.lean | 41 ++++++++++--------- .../ZeroConcentrated/System.lean | 4 +- 6 files changed, 58 insertions(+), 51 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Abstract.lean b/SampCert/DifferentialPrivacy/Abstract.lean index 66c05719..7bef65ae 100644 --- a/SampCert/DifferentialPrivacy/Abstract.lean +++ b/SampCert/DifferentialPrivacy/Abstract.lean @@ -40,29 +40,29 @@ class DPSystem (T : Type) where /-- DP is monotonic -/ - prop_mono {m : Mechanism T Z} {ε₁ ε₂: NNReal} (Hε : ε₁ ≤ ε₂) (H : prop m ε₁) : prop m ε₂ + 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, + 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₂) ε /-- 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} [MeasurableSpace U] [Countable U] [DiscreteMeasurableSpace U] [Inhabited 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) -> - ∀ ε : NNReal, ε = (0 : NNReal) -> prop (privConst u) ε - + const_prop {U : Type} [MeasurableSpace U] [Countable U] [DiscreteMeasurableSpace U] {u : U} {ε : NNReal} : + ε = (0 : NNReal) -> prop (privConst u) ε namespace DPSystem @@ -70,12 +70,13 @@ 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 + {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 - apply adaptive_compose_prop m₁ (fun _ => m₂) ε₁ ε₂ _ p1 (fun _ => p2) - rfl + apply adaptive_compose_prop p1 (fun _ => p2) + trivial end DPSystem @@ -112,7 +113,7 @@ class DPNoise (dps : DPSystem T) where /-- Adding noise to a query makes it private -/ - noise_prop : ∀ q : List T → ℤ, ∀ Δ εn εd : ℕ+, ∀ ε : NNReal, + noise_prop {q : List T → ℤ} {Δ εn εd : ℕ+} {ε : NNReal} : noise_priv εn εd ε -> sensitivity q Δ → dps.prop (noise q Δ εn εd) ε diff --git a/SampCert/DifferentialPrivacy/Pure/System.lean b/SampCert/DifferentialPrivacy/Pure/System.lean index 034a5502..a8667cf6 100644 --- a/SampCert/DifferentialPrivacy/Pure/System.lean +++ b/SampCert/DifferentialPrivacy/Pure/System.lean @@ -26,13 +26,17 @@ instance PureDPSystem : DPSystem T where of_adp := pure_of_adp prop_adp := pure_ApproximateDP prop_mono := PureDP_mono - adaptive_compose_prop := PureDP_ComposeAdaptive' - postprocess_prop := PureDP_PostProcess - const_prop := PureDP_privConst + 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_priv := laplace_pureDP_noise_priv - noise_prop := privNoisedQueryPure_DP + noise_prop := by + intros; apply privNoisedQueryPure_DP <;> trivial end SLang diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean index e9ad149d..fa2441c3 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean @@ -34,12 +34,13 @@ DP bound for noised mean. theorem privNoisedBoundedMean_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) : dps.prop (privNoisedBoundedMean U ε₁ ε₂) ((ε₁ : NNReal) / ε₂) := by unfold privNoisedBoundedMean - rw [bind_bind_indep] - apply dps.postprocess_prop - rw [budget_split] - apply dps.compose_prop - · apply privNoisedBoundedSum_DP - · sorry - -- apply privNoisedCount_DP + sorry + -- rw [bind_bind_indep] + -- apply dps.postprocess_prop + -- rw [budget_split] + -- apply dps.compose_prop + -- · apply privNoisedBoundedSum_DP + -- · sorry + -- -- apply privNoisedCount_DP end SLang diff --git a/SampCert/DifferentialPrivacy/Queries/Count/Properties.lean b/SampCert/DifferentialPrivacy/Queries/Count/Properties.lean index 8459e239..c961280f 100644 --- a/SampCert/DifferentialPrivacy/Queries/Count/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/Count/Properties.lean @@ -48,7 +48,7 @@ The noised counting query satisfies DP property theorem privNoisedCount_DP (ε₁ ε₂ : ℕ+) (ε : NNReal) (HP : dpn.noise_priv ε₁ ε₂ ε) : dps.prop (privNoisedCount ε₁ ε₂) ε := by unfold privNoisedCount - apply (dpn.noise_prop _ _ _ _ _ HP) + apply dpn.noise_prop HP apply exactCount_1_sensitive end SLang diff --git a/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean b/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean index 86fa124c..655c2230 100644 --- a/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean @@ -96,26 +96,27 @@ lemma privNoisedHistogramAux_DP (ε₁ ε₂ : ℕ+) (n : ℕ) (Hn : n < numBins · rename_i n IH unfold privNoisedHistogramAux simp only [] - refine DPSystem.postprocess_prop - (privCompose (privNoisedBinCount numBins B ε₁ ε₂ ↑(n + 1)) - (privNoisedHistogramAux numBins B ε₁ ε₂ n (privNoisedHistogramAux.proof_2 numBins n Hn))) - (↑(n + 1).succ * (↑↑ε₁ / ↑↑(ε₂ * numBins))) ?succ.a - apply (@DPSystem_prop_ext _ _ _ (?C1 + ?C2) _ _ ?HCeq ?Hdp) - case Hdp => - refine - (DPSystem.compose_prop - (privNoisedBinCount numBins B ε₁ ε₂ ↑(n + 1)) - (privNoisedHistogramAux numBins B ε₁ ε₂ n _) (↑↑ε₁ / ↑↑(ε₂ * numBins)) (↑n.succ * (↑↑ε₁ / ↑↑(ε₂ * numBins))) ?X ?Y) - case X => exact privNoisedBinCount_DP numBins B ε₁ ε₂ ↑(n + 1) - case Y => apply IH - generalize (ε₁.val.cast / (ε₂ * numBins).val.cast : NNReal) = A - conv => - enter [1, 1] - rw [Eq.symm (one_mul A)] - rw [<- add_mul] - congr - simp only [succ_eq_add_one, Nat.cast_add, Nat.cast_one] - exact AddCommMagma.add_comm (OfNat.ofNat 1) (n.cast + OfNat.ofNat 1) + sorry + -- refine DPSystem.postprocess_prop + -- (privCompose (privNoisedBinCount numBins B ε₁ ε₂ ↑(n + 1)) + -- (privNoisedHistogramAux numBins B ε₁ ε₂ n (privNoisedHistogramAux.proof_2 numBins n Hn))) + -- (↑(n + 1).succ * (↑↑ε₁ / ↑↑(ε₂ * numBins))) ?succ.a + -- apply (@DPSystem_prop_ext _ _ _ (?C1 + ?C2) _ _ ?HCeq ?Hdp) + -- case Hdp => + -- refine + -- (DPSystem.compose_prop + -- (privNoisedBinCount numBins B ε₁ ε₂ ↑(n + 1)) + -- (privNoisedHistogramAux numBins B ε₁ ε₂ n _) (↑↑ε₁ / ↑↑(ε₂ * numBins)) (↑n.succ * (↑↑ε₁ / ↑↑(ε₂ * numBins))) ?X ?Y) + -- case X => exact privNoisedBinCount_DP numBins B ε₁ ε₂ ↑(n + 1) + -- case Y => apply IH + -- generalize (ε₁.val.cast / (ε₂ * numBins).val.cast : NNReal) = A + -- conv => + -- enter [1, 1] + -- rw [Eq.symm (one_mul A)] + -- rw [<- add_mul] + -- congr + -- simp only [succ_eq_add_one, Nat.cast_add, Nat.cast_one] + -- exact AddCommMagma.add_comm (OfNat.ofNat 1) (n.cast + OfNat.ofNat 1) /-- DP bound for a noised histogram diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean index a298c9a9..840aa94b 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean @@ -27,11 +27,11 @@ instance zCDPSystem : DPSystem T where prop := zCDP of_adp := sorry prop_adp := sorry -- zCDP_ApproximateDP - prop_mono := zCDP_mono + prop_mono := sorry -- zCDP_mono -- noise := privNoisedQuery -- noise_prop := sorry -- privNoisedQuery_zCDP adaptive_compose_prop := sorry -- privComposeAdaptive_zCDP - postprocess_prop := privPostProcess_zCDP + postprocess_prop := sorry -- privPostProcess_zCDP const_prop := sorry -- privConst_zCDP /-- From 00e2ef644be4bc30f53040584051da0d114e29fc Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 13:50:33 -0400 Subject: [PATCH 13/30] cleanup bounded sum abstract proof --- .../Queries/BoundedSum/Properties.lean | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean b/SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean index 4f21348b..c4778f53 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean @@ -85,10 +85,9 @@ theorem exactBoundedSum_sensitivity (U : ℕ+) : sensitivity (exactBoundedSum U) The noised bounded sum satisfies the DP property of the DP system. -/ @[simp] -theorem privNoisedBoundedSum_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) : - dps.prop (privNoisedBoundedSum U ε₁ ε₂) ((ε₁ : NNReal) / ε₂) := by - sorry - -- apply dpn.noise_prop - -- apply exactBoundedSum_sensitivity +theorem privNoisedBoundedSum_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) (HP : dpn.noise_priv ε₁ ε₂ (ε₁ / ε₂)) : + dps.prop (privNoisedBoundedSum U ε₁ ε₂) ((ε₁ : NNReal) / ε₂) := by + apply dpn.noise_prop HP + apply exactBoundedSum_sensitivity end SLang From be8cfd4b975807c532f9274045e4cf5be145e323 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 15:19:54 -0400 Subject: [PATCH 14/30] update bounded mean --- .../Queries/BoundedMean/Properties.lean | 25 ++++++++++++------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean index fa2441c3..367c088a 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean @@ -31,16 +31,23 @@ lemma budget_split (ε₁ ε₂ : ℕ+) : /-- DP bound for noised mean. -/ -theorem privNoisedBoundedMean_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) : +theorem privNoisedBoundedMean_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) + (HP_half : dpn.noise_priv ε₁ (2 * ε₂) (ε₁ / ↑(2 * ε₂))) : dps.prop (privNoisedBoundedMean U ε₁ ε₂) ((ε₁ : NNReal) / ε₂) := by unfold privNoisedBoundedMean - sorry - -- rw [bind_bind_indep] - -- apply dps.postprocess_prop - -- rw [budget_split] - -- apply dps.compose_prop - -- · apply privNoisedBoundedSum_DP - -- · sorry - -- -- apply privNoisedCount_DP + rw [bind_bind_indep] + apply dps.postprocess_prop + apply dps.compose_prop ?SC1 + · apply privNoisedBoundedSum_DP + apply HP_half + · apply privNoisedCount_DP + apply HP_half + + case SC1 => + -- Arithmetic + ring_nf + rw [div_mul] + congr + simp end SLang From b064656cf8955555f0cf2a86928ecf56faa9974d Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 15:40:56 -0400 Subject: [PATCH 15/30] Histogram update --- .../Queries/Histogram/Properties.lean | 116 +++++------------- .../Queries/HistogramMean/Properties.lean | 9 +- 2 files changed, 39 insertions(+), 86 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean b/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean index 655c2230..50e6580f 100644 --- a/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean @@ -27,9 +27,6 @@ variable [HT : Inhabited T] variable (numBins : ℕ+) variable (B : Bins T numBins) --- def exactBinCount (b : Fin num_bins) (l : List T) : ℤ := --- List.length (List.filter (fun v => B.bin v = b) l) - /- exactBinCount is 1-sensitive -/ @@ -59,108 +56,63 @@ theorem exactBinCount_sensitivity (b : Fin numBins) : sensitivity (exactBinCount /-- DP bound for a noised bin count -/ -lemma privNoisedBinCount_DP (ε₁ ε₂ : ℕ+) (b : Fin numBins) : - dps.prop (privNoisedBinCount numBins B ε₁ ε₂ b) (ε₁ / ((ε₂ * numBins : PNat))) := by +lemma privNoisedBinCount_DP (ε₁ ε₂ : ℕ+) (ε : NNReal) (b : Fin numBins) + (HN_bin : dpn.noise_priv ε₁ (ε₂ * numBins) (ε / numBins)) : + dps.prop (privNoisedBinCount numBins B ε₁ ε₂ b) (ε / numBins) := by unfold privNoisedBinCount - sorry - -- apply dpn.noise_prop - -- apply exactBinCount_sensitivity + apply dpn.noise_prop HN_bin + apply exactBinCount_sensitivity --- MARKUSDE: Looking at this proof it is clear that we need better tactic support for the abstract DP operators --- MARKUSDE: - Lemmas with equality side conditions for the privacy cost /-- DP bound for intermediate steps in the histogram calculation. -/ -lemma privNoisedHistogramAux_DP (ε₁ ε₂ : ℕ+) (n : ℕ) (Hn : n < numBins) : - dps.prop (privNoisedHistogramAux numBins B ε₁ ε₂ n Hn) (n.succ * (ε₁ / (ε₂ * numBins : PNat))) := by +lemma privNoisedHistogramAux_DP (ε₁ ε₂ : ℕ+) (ε : NNReal) (n : ℕ) (Hn : n < numBins) + (HN_bin : dpn.noise_priv ε₁ (ε₂ * numBins) (ε / numBins)) : + dps.prop (privNoisedHistogramAux numBins B ε₁ ε₂ n Hn) (n.succ * (ε / numBins)) := by induction n · unfold privNoisedHistogramAux simp only [Nat.cast_zero, succ_eq_add_one, zero_add, Nat.cast_one, Nat.cast_mul, one_mul] - sorry - -- refine DPSystem.postprocess_prop - -- (privCompose (privNoisedBinCount numBins B ε₁ ε₂ 0) (privConst (emptyHistogram numBins B))) - -- (↑↑ε₁ / ↑↑(ε₂ * numBins)) ?G1 - -- apply (DPSystem_prop_ext _ ?HEq ?Hdp) - -- case Hdp => - -- sorry - -- -- apply (DPSystem.compose_prop - -- -- (privNoisedBinCount numBins B ε₁ ε₂ 0) - -- -- (privConst (emptyHistogram numBins B)) - -- -- (↑↑ε₁ / ↑↑(ε₂ * numBins)) - -- -- 0 - -- -- (privNoisedBinCount_DP numBins B ε₁ ε₂ 0) - -- -- (DPSystem.const_prop (emptyHistogram numBins B))) - -- case HEq => - -- sorry - -- -- simp only [PNat.mul_coe, Nat.cast_mul, add_zero] + apply DPSystem.postprocess_prop + apply DPSystem.compose_prop ?SC1 + · apply privNoisedBinCount_DP + apply HN_bin + · apply DPSystem.const_prop + rfl + case SC1 => simp only [add_zero] · rename_i n IH unfold privNoisedHistogramAux simp only [] - sorry - -- refine DPSystem.postprocess_prop - -- (privCompose (privNoisedBinCount numBins B ε₁ ε₂ ↑(n + 1)) - -- (privNoisedHistogramAux numBins B ε₁ ε₂ n (privNoisedHistogramAux.proof_2 numBins n Hn))) - -- (↑(n + 1).succ * (↑↑ε₁ / ↑↑(ε₂ * numBins))) ?succ.a - -- apply (@DPSystem_prop_ext _ _ _ (?C1 + ?C2) _ _ ?HCeq ?Hdp) - -- case Hdp => - -- refine - -- (DPSystem.compose_prop - -- (privNoisedBinCount numBins B ε₁ ε₂ ↑(n + 1)) - -- (privNoisedHistogramAux numBins B ε₁ ε₂ n _) (↑↑ε₁ / ↑↑(ε₂ * numBins)) (↑n.succ * (↑↑ε₁ / ↑↑(ε₂ * numBins))) ?X ?Y) - -- case X => exact privNoisedBinCount_DP numBins B ε₁ ε₂ ↑(n + 1) - -- case Y => apply IH - -- generalize (ε₁.val.cast / (ε₂ * numBins).val.cast : NNReal) = A - -- conv => - -- enter [1, 1] - -- rw [Eq.symm (one_mul A)] - -- rw [<- add_mul] - -- congr - -- simp only [succ_eq_add_one, Nat.cast_add, Nat.cast_one] - -- exact AddCommMagma.add_comm (OfNat.ofNat 1) (n.cast + OfNat.ofNat 1) + apply DPSystem.postprocess_prop + apply DPSystem.compose_prop ?SC1 + · apply privNoisedBinCount_DP + apply HN_bin + · apply IH + case SC1 => + simp + ring_nf /-- DP bound for a noised histogram -/ -lemma privNoisedHistogram_DP (ε₁ ε₂ : ℕ+) : - dps.prop (privNoisedHistogram numBins B ε₁ ε₂) (ε₁ / ε₂) := by +lemma privNoisedHistogram_DP (ε₁ ε₂ : ℕ+) (ε : NNReal) (HN_bin : dpn.noise_priv ε₁ (ε₂ * numBins) (ε / numBins)) : + dps.prop (privNoisedHistogram numBins B ε₁ ε₂) ε := by unfold privNoisedHistogram apply (DPSystem_prop_ext _ ?HEq ?Hdp) - case Hdp => apply privNoisedHistogramAux_DP + case Hdp => + apply privNoisedHistogramAux_DP + apply HN_bin case HEq => - simp - rw [division_def] - rw [division_def] - rw [mul_inv] - conv => - enter [1, 2] - rw [<- mul_assoc] - rw [mul_comm] - generalize (ε₁.val.cast * ε₂.val.cast⁻¹ : NNReal) = A - rw [<- mul_assoc] - conv => - enter [2] - rw [Eq.symm (one_mul A)] - congr - unfold predBins - cases numBins - rename_i n' Hn' - simp only [PNat.natPred_eq_pred, pred_eq_sub_one, cast_tsub, Nat.cast_one, PNat.mk_coe] - rw [tsub_add_eq_max] - rw [max_eq_left (one_le_cast.mpr Hn')] - apply mul_inv_cancel - intro HK - simp_all - rw [HK] at Hn' - cases Hn' - + simp [predBins] + simp [mul_div_left_comm] /-- DP bound for the thresholding maximum -/ -lemma privMaxBinAboveThreshold_DP (ε₁ ε₂ : ℕ+) (τ : ℤ) : - dps.prop (privMaxBinAboveThreshold numBins B ε₁ ε₂ τ) (ε₁ / ε₂) := by - rw [privMaxBinAboveThreshold] +lemma privMaxBinAboveThreshold_DP (ε₁ ε₂ : ℕ+) (ε : NNReal) (τ : ℤ) (HN_bin : dpn.noise_priv ε₁ (ε₂ * numBins) (ε / numBins)) : + dps.prop (privMaxBinAboveThreshold numBins B ε₁ ε₂ τ) ε := by + unfold privMaxBinAboveThreshold apply dps.postprocess_prop apply privNoisedHistogram_DP + apply HN_bin end SLang diff --git a/SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean b/SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean index db36ce3a..344400e0 100644 --- a/SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean @@ -73,9 +73,10 @@ lemma privMeanHistogram_DP (ε₁ ε₂ : ℕ+) (τ : ℤ) (ε₃ ε₄ : ℕ+) -- apply dps.prop_mono ?G1 ?G2 -- case G2 => apply dps.const_prop -- simp only [_root_.zero_le] - · rename_i mx - simp only - apply dps.postprocess_prop - apply privNoisedBoundedMean_DP + · sorry + -- rename_i mx + -- simp only + -- apply dps.postprocess_prop + -- apply privNoisedBoundedMean_DP rfl end SLang From edec41666fc1e8dd6cf9aaf5f5e2d6517427d4ee Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 15:52:00 -0400 Subject: [PATCH 16/30] historgram mean update --- .../Queries/BoundedMean/Properties.lean | 11 +++---- .../Queries/BoundedSum/Properties.lean | 4 +-- .../Queries/HistogramMean/Properties.lean | 32 ++++++++++--------- 3 files changed, 23 insertions(+), 24 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean index 367c088a..abed30ab 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean @@ -31,9 +31,9 @@ lemma budget_split (ε₁ ε₂ : ℕ+) : /-- DP bound for noised mean. -/ -theorem privNoisedBoundedMean_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) - (HP_half : dpn.noise_priv ε₁ (2 * ε₂) (ε₁ / ↑(2 * ε₂))) : - dps.prop (privNoisedBoundedMean U ε₁ ε₂) ((ε₁ : NNReal) / ε₂) := by +theorem privNoisedBoundedMean_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) (ε : NNReal) + (HP_half : dpn.noise_priv ε₁ (2 * ε₂) (ε / 2)) : + dps.prop (privNoisedBoundedMean U ε₁ ε₂) ε := by unfold privNoisedBoundedMean rw [bind_bind_indep] apply dps.postprocess_prop @@ -44,10 +44,7 @@ theorem privNoisedBoundedMean_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) apply HP_half case SC1 => - -- Arithmetic ring_nf - rw [div_mul] - congr - simp + simp [div_mul] end SLang diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean b/SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean index c4778f53..3e14c7a4 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean @@ -85,8 +85,8 @@ theorem exactBoundedSum_sensitivity (U : ℕ+) : sensitivity (exactBoundedSum U) The noised bounded sum satisfies the DP property of the DP system. -/ @[simp] -theorem privNoisedBoundedSum_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) (HP : dpn.noise_priv ε₁ ε₂ (ε₁ / ε₂)) : - dps.prop (privNoisedBoundedSum U ε₁ ε₂) ((ε₁ : NNReal) / ε₂) := by +theorem privNoisedBoundedSum_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) (ε : NNReal) (HP : dpn.noise_priv ε₁ ε₂ ε) : + dps.prop (privNoisedBoundedSum U ε₁ ε₂) ε := by apply dpn.noise_prop HP apply exactBoundedSum_sensitivity diff --git a/SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean b/SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean index 344400e0..6d15c8fd 100644 --- a/SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean @@ -57,26 +57,28 @@ instance : DiscreteMeasurableSpace (Option (Fin ↑numBins)) where forall_measurableSet := by simp only [MeasurableSpace.measurableSet_top, implies_true] -/- +/-- DP bound for the adaptive mean -/ -lemma privMeanHistogram_DP (ε₁ ε₂ : ℕ+) (τ : ℤ) (ε₃ ε₄ : ℕ+) : - dps.prop (privMeanHistogram dps dpn numBins B unbin ε₁ ε₂ τ ε₃ ε₄) (ε₁/ε₂ + ε₃/ε₄) := by +lemma privMeanHistogram_DP (ε₁ ε₂ : ℕ+) (τ : ℤ) (ε₃ ε₄ : ℕ+) (εA εB : NNReal) + (HN_A : dpn.noise_priv ε₁ (ε₂ * numBins) (εA / numBins)) + (HN_B : dpn.noise_priv ε₃ (2 * ε₄) (εB / 2)): + dps.prop (privMeanHistogram dps dpn numBins B unbin ε₁ ε₂ τ ε₃ ε₄) (εA + εB) := by rw [privMeanHistogram] apply dps.postprocess_prop apply dps.adaptive_compose_prop · apply privMaxBinAboveThreshold_DP - intro u - cases u - · simp only - sorry - -- apply dps.prop_mono ?G1 ?G2 - -- case G2 => apply dps.const_prop - -- simp only [_root_.zero_le] - · sorry - -- rename_i mx - -- simp only - -- apply dps.postprocess_prop - -- apply privNoisedBoundedMean_DP + apply HN_A + · intro u + cases u + · simp only [] + apply (@DPSystem.prop_mono _ _ _ _ 0 εB _) + · apply dps.const_prop + rfl + · apply _root_.zero_le + · simp only [] + apply dps.postprocess_prop + apply privNoisedBoundedMean_DP + apply HN_B rfl end SLang From 592cdea5f116ee7b8fb3a12c7db6bc8283caa010 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 16:11:17 -0400 Subject: [PATCH 17/30] instances for zCDP (except approx DP) --- SampCert.lean | 2 +- .../ZeroConcentrated/System.lean | 52 +++++++++++++------ 2 files changed, 37 insertions(+), 17 deletions(-) diff --git a/SampCert.lean b/SampCert.lean index 1d7fc16e..ebafb641 100644 --- a/SampCert.lean +++ b/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 /- diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean index 840aa94b..89c50e06 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean @@ -27,28 +27,48 @@ instance zCDPSystem : DPSystem T where prop := zCDP of_adp := sorry prop_adp := sorry -- zCDP_ApproximateDP - prop_mono := sorry -- zCDP_mono - -- noise := privNoisedQuery - -- noise_prop := sorry -- privNoisedQuery_zCDP - adaptive_compose_prop := sorry -- privComposeAdaptive_zCDP - postprocess_prop := sorry -- privPostProcess_zCDP - const_prop := sorry -- privConst_zCDP + prop_mono := by + intro _ _ _ _ H HZ + apply zCDP_mono H HZ + adaptive_compose_prop := by + intros _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HZ HZ2 Hε + rw [<- Hε] + apply privComposeAdaptive_zCDP + apply HZ + apply HZ2 + postprocess_prop := by + intros _ _ _ _ _ _ _ _ _ HZ + apply privPostProcess_zCDP + apply HZ + const_prop := by + intros _ _ _ _ _ _ Hε + rw [Hε] + apply privConst_zCDP + +def gaussian_zCDP_noise_priv (ε₁ ε₂ : ℕ+) (ε : NNReal) : Prop := (1/2) * ((ε₁ : NNReal) / ε₂)^2 ≤ ε /-- Gaussian noise for zCDP system -/ -instance gaussian_zCDPSystem : DPNoise zCDPsystem where +instance gaussian_zCDPSystem (T : Type) : DPNoise (@zCDPSystem T) where noise := privNoisedQuery - noise_priv := sorry - noise_prop := sorry -- privNoisedQuery_zCDP + noise_priv := gaussian_zCDP_noise_priv + noise_prop := by + intros _ _ _ _ _ H HS + apply DPSystem.prop_mono ?G1 + · simp [DPSystem.prop] + apply privNoisedQuery_zCDP + apply HS + · apply H -/-- -Laplace noise for zCDP system --/ -instance laplace_zCDPSystem : DPNoise zCDPsystem where - noise := sorry - noise_priv := sorry - noise_prop := sorry -- privNoisedQuery_zCDP + +-- /- +-- Laplace noise for zCDP system? +-- -/ +-- instance laplace_zCDPSystem (T : Type) : DPNoise (@zCDPSystem T) where +-- noise := sorry +-- noise_priv := sorry +-- noise_prop := sorry -- privNoisedQuery_zCDP end SLang From e746f4695f5ad83a3ec1167f0d05d36f7b9e4ea5 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 28 Oct 2024 18:57:10 -0400 Subject: [PATCH 18/30] checkpoint --- .../ZeroConcentrated/DP.lean | 85 +++++++++++++++---- .../ZeroConcentrated/System.lean | 7 +- 2 files changed, 73 insertions(+), 19 deletions(-) diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean index 1bbb753d..a30d2b49 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean @@ -665,31 +665,82 @@ theorem ApproximateDP_of_zCDP [Countable U] (m : Mechanism T U) case G2 => exact Hm l₁ l₂ HN simp + +def D (δ : NNReal) : Real := (2 * Real.log (1 / δ)) ^ ((1 : ℝ) / (2 : ℝ)) + +def ε (ε' : NNReal) (δ : NNReal) : NNReal := + Real.toNNReal ((-2 * D δ + .sqrt ((2 * D δ) ^ 2 + 8 * ε')) / 2) ^ ((1 : ℝ) / (2 : ℝ)) + +lemma eqε (ε' δ : NNReal) (H : δ < 1) : ε' = ((ε ε' δ)^2) / (2 : NNReal) + ε ε' δ * D δ := by + sorry + +/-- +Pure privacy bound required to obtain (ε, δ)-approximate DP +-/ +def zCDP_of_adp (δ : NNReal) (ε' : NNReal) : NNReal := (1/2) * ((ε ε' δ)^2) + -- (√(2 * Real.log (1/δ) + 2 * ε) - √(2 * Real.log (1/δ))).toNNReal + /-- zCDP is no weaker than approximate DP, up to a loss of parameters. -/ lemma zCDP_ApproximateDP [Countable U] {m : Mechanism T U} : - ∃ (degrade : (δ : NNReal) -> (ε' : NNReal) -> NNReal), ∀ (δ : NNReal) (_ : 0 < δ) (ε' : NNReal), - (zCDP m (degrade δ ((1/2) * ε'^2)) -> ApproximateDP m ε' δ) := by - let degrade (δ : NNReal) (ε' : NNReal) : NNReal := - (√(2 * Real.log (1/δ) + 2 * ε') - √(2 * Real.log (1/δ))).toNNReal - have HDdegrade δ ε' : degrade δ ε' = (√(2 * Real.log (1/δ) + 2 * ε') - √(2 * Real.log (1/δ))).toNNReal := by rfl - exists degrade - intro δ Hδ ε' ⟨ HN , HB ⟩ - + ∀ (δ : NNReal) (_ : 0 < δ) (ε' : NNReal), + (zCDP m (zCDP_of_adp δ ε') -> ApproximateDP m ε' δ) := by + intro δ Hδ ε' H cases Classical.em (1 ≤ δ) · rename_i Hδ1 exact ApproximateDP_gt1 m (↑ε') Hδ1 - rename_i Hδ1 - rw [ApproximateDP] - - - have R := ApproximateDP_of_zCDP m (degrade δ ε') (by simp) ?G1 HN δ Hδ - case G1 => - -- this proof has to be redone - sorry - sorry + simp at Hδ1 + unfold ApproximateDP + + unfold zCDP_of_adp at H + rcases H with ⟨ H1, H2 ⟩ + have X := ApproximateDP_of_zCDP m (ε ε' δ) ?G1 H2 H1 δ Hδ + case G1 => exact NNReal.zero_le_coe + rw [eqε ε' δ Hδ1] + -- We have this, basically. + unfold D + simp_all + + + + -- #check ApproximateDP_of_zCDP + -- have X := ApproximateDP_of_zCDP m ((2 * zCDP_of_adp δ ε') ^ ((1 : Real) / 2)) ?G1 ?G2 ?G3 δ Hδ + -- case G1 => + -- apply Real.rpow_nonneg + -- apply mul_nonneg + -- · simp + -- · exact NNReal.zero_le_coe + -- case G2 => + -- ring_nf + -- -- True + -- sorry + -- case G3 => + -- cases H + -- trivial + + -- have X1 : (2 * (zCDP_of_adp δ ε')) ^ (1 / 2)) ^ 2 / 2 = (zCDP_of_adp δ ε') : Real := by sorry + -- rw [X1] + -- clear X1 + + -- let degrade (δ : NNReal) (ε' : NNReal) : NNReal := + -- (√(2 * Real.log (1/δ) + 2 * ε') - √(2 * Real.log (1/δ))).toNNReal + -- have HDdegrade δ ε' : degrade δ ε' = (√(2 * Real.log (1/δ) + 2 * ε') - √(2 * Real.log (1/δ))).toNNReal := by rfl + -- exists degrade + -- intro δ Hδ ε' ⟨ HN , HB ⟩ + + + -- rename_i Hδ1 + -- rw [ApproximateDP] + + + + -- have R := ApproximateDP_of_zCDP m (degrade δ ε') (by simp) ?G1 HN δ Hδ + -- case G1 => + -- -- this proof has to be redone + -- sorry + -- sorry /- have Hdegrade : ((degrade δ ε') ^ 2) / 2 + (degrade δ ε') * (2 * Real.log (1 / δ))^(1/2 : ℝ) = ε' := by diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean index 89c50e06..fc794fad 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean @@ -16,6 +16,8 @@ import SampCert.DifferentialPrivacy.ZeroConcentrated.Const This file contains an instance of an abstract DP system associated to the discrete gaussian mechanisms. -/ +noncomputable section + namespace SLang variable { T : Type } @@ -25,8 +27,9 @@ Instance of a DP system for zCDP -/ instance zCDPSystem : DPSystem T where prop := zCDP - of_adp := sorry - prop_adp := sorry -- zCDP_ApproximateDP + of_adp := zCDP_of_adp + prop_adp := by + intros; apply zCDP_ApproximateDP <;> assumption prop_mono := by intro _ _ _ _ H HZ apply zCDP_mono H HZ From 4ea177b494ec805c93059e29cbf5dfe7b7a2ae27 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 29 Oct 2024 11:41:55 -0400 Subject: [PATCH 19/30] zCDP degrade --- .../ZeroConcentrated/DP.lean | 144 ++++++------------ 1 file changed, 48 insertions(+), 96 deletions(-) diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean index a30d2b49..5edf10ea 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean @@ -665,20 +665,58 @@ theorem ApproximateDP_of_zCDP [Countable U] (m : Mechanism T U) case G2 => exact Hm l₁ l₂ HN simp +namespace zCDP_of_adp_def def D (δ : NNReal) : Real := (2 * Real.log (1 / δ)) ^ ((1 : ℝ) / (2 : ℝ)) -def ε (ε' : NNReal) (δ : NNReal) : NNReal := - Real.toNNReal ((-2 * D δ + .sqrt ((2 * D δ) ^ 2 + 8 * ε')) / 2) ^ ((1 : ℝ) / (2 : ℝ)) +def ε (ε' : NNReal) (δ : NNReal) : NNReal := Real.toNNReal (-D δ + discrim (OfNat.ofNat 2)⁻¹ (D δ) (-↑ε') ^ (2 : ℝ)⁻¹) -lemma eqε (ε' δ : NNReal) (H : δ < 1) : ε' = ((ε ε' δ)^2) / (2 : NNReal) + ε ε' δ * D δ := by - sorry +lemma eqε (ε' δ : NNReal) (H0 : 0 < δ) (H1 : δ < 1) : ε' = ((ε ε' δ)^2) / (2 : NNReal) + ε ε' δ * D δ := by + suffices (((1 : ℝ) / (2 : ℝ)) * (ε ε' δ) * (ε ε' δ) + D δ * ε ε' δ + (- ε')) = 0 by + simp_all + rw [add_neg_eq_zero] at this + rw [<- this] + ring_nf + + have Hle : 0 < D δ ^ 2 + 4 * (OfNat.ofNat 2)⁻¹ * ε' := by + apply Right.add_pos_of_pos_of_nonneg + · apply sq_pos_of_pos + unfold D + apply Real.rpow_pos_of_pos + apply mul_pos <;> simp + exact Real.log_neg H0 H1 + · simp + + apply (@quadratic_eq_zero_iff Real _ _ _ _ _ ?Ga ((discrim (OfNat.ofNat 1 / OfNat.ofNat 2) (D δ) (-ε'.toReal)) ^ ((1 : ℝ) / (2 : ℝ))) ?Gs ((ε ε' δ).toReal)).mpr + case Ga => simp + case Gs => + rw [<- Real.rpow_add ?Gadd] + case Gadd => + simp [discrim] + apply Hle + rw [add_halves] + simp + left + simp + unfold ε + apply Real.coe_toNNReal + simp [discrim] + apply nonneg_le_nonneg_of_sq_le_sq + · apply Real.rpow_nonneg + exact le_of_lt Hle + rw [<- Real.rpow_add Hle] + rw [<- one_div] + rw [add_halves] + simp + rw [<- sq] + simp + +end zCDP_of_adp_def /-- Pure privacy bound required to obtain (ε, δ)-approximate DP -/ -def zCDP_of_adp (δ : NNReal) (ε' : NNReal) : NNReal := (1/2) * ((ε ε' δ)^2) - -- (√(2 * Real.log (1/δ) + 2 * ε) - √(2 * Real.log (1/δ))).toNNReal +def zCDP_of_adp (δ : NNReal) (ε' : NNReal) : NNReal := (1/2) * ((zCDP_of_adp_def.ε ε' δ)^2) /-- zCDP is no weaker than approximate DP, up to a loss of parameters. @@ -686,7 +724,7 @@ zCDP is no weaker than approximate DP, up to a loss of parameters. lemma zCDP_ApproximateDP [Countable U] {m : Mechanism T U} : ∀ (δ : NNReal) (_ : 0 < δ) (ε' : NNReal), (zCDP m (zCDP_of_adp δ ε') -> ApproximateDP m ε' δ) := by - intro δ Hδ ε' H + intro δ Hδ0 ε' H cases Classical.em (1 ≤ δ) · rename_i Hδ1 exact ApproximateDP_gt1 m (↑ε') Hδ1 @@ -696,100 +734,14 @@ lemma zCDP_ApproximateDP [Countable U] {m : Mechanism T U} : unfold zCDP_of_adp at H rcases H with ⟨ H1, H2 ⟩ - have X := ApproximateDP_of_zCDP m (ε ε' δ) ?G1 H2 H1 δ Hδ + have X := ApproximateDP_of_zCDP m (zCDP_of_adp_def.ε ε' δ) ?G1 H2 H1 δ Hδ0 case G1 => exact NNReal.zero_le_coe - rw [eqε ε' δ Hδ1] - -- We have this, basically. - unfold D + rw [zCDP_of_adp_def.eqε ε' δ Hδ0 Hδ1] + unfold zCDP_of_adp_def.D simp_all - -- #check ApproximateDP_of_zCDP - -- have X := ApproximateDP_of_zCDP m ((2 * zCDP_of_adp δ ε') ^ ((1 : Real) / 2)) ?G1 ?G2 ?G3 δ Hδ - -- case G1 => - -- apply Real.rpow_nonneg - -- apply mul_nonneg - -- · simp - -- · exact NNReal.zero_le_coe - -- case G2 => - -- ring_nf - -- -- True - -- sorry - -- case G3 => - -- cases H - -- trivial - - -- have X1 : (2 * (zCDP_of_adp δ ε')) ^ (1 / 2)) ^ 2 / 2 = (zCDP_of_adp δ ε') : Real := by sorry - -- rw [X1] - -- clear X1 - - -- let degrade (δ : NNReal) (ε' : NNReal) : NNReal := - -- (√(2 * Real.log (1/δ) + 2 * ε') - √(2 * Real.log (1/δ))).toNNReal - -- have HDdegrade δ ε' : degrade δ ε' = (√(2 * Real.log (1/δ) + 2 * ε') - √(2 * Real.log (1/δ))).toNNReal := by rfl - -- exists degrade - -- intro δ Hδ ε' ⟨ HN , HB ⟩ - - - -- rename_i Hδ1 - -- rw [ApproximateDP] - - - - -- have R := ApproximateDP_of_zCDP m (degrade δ ε') (by simp) ?G1 HN δ Hδ - -- case G1 => - -- -- this proof has to be redone - -- sorry - -- sorry - - /- - have Hdegrade : ((degrade δ ε') ^ 2) / 2 + (degrade δ ε') * (2 * Real.log (1 / δ))^(1/2 : ℝ) = ε' := by - rw [HDdegrade] - generalize HD : Real.log (1 / δ) = D - have HDnn : 0 ≤ D := by - rw [<- HD] - apply Real.log_nonneg - apply one_le_one_div Hδ - exact le_of_not_ge Hδ1 - simp only [Real.coe_toNNReal'] - rw [max_eq_left ?G1] - case G1 => - apply sub_nonneg_of_le - apply Real.sqrt_le_sqrt - simp - rw [sub_sq'] - rw [Real.sq_sqrt ?G1] - case G1 => - apply add_nonneg - · simp - trivial - · simp - rw [Real.sq_sqrt ?G1] - case G1 => - simp - trivial - rw [← Real.sqrt_eq_rpow] - rw [mul_sub_right_distrib] - rw [<- sq] - rw [Real.sq_sqrt ?G1] - case G1 => - simp - trivial - generalize HW : √(2 * D + 2 * ↑ε') * √(2 * D) = W - conv => - enter [1, 1, 1, 2] - rw [mul_assoc] - rw [HW] - rw [sub_div] - rw [add_div] - rw [add_div] - simp - linarith - rw [Hdegrade] at R - trivial - -/ - - /-- Pure DP bound implies absolute continuity -/ From de517ba80ee59401cfbe99c9b1fb4e1537c220c1 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Wed, 30 Oct 2024 10:07:24 -0400 Subject: [PATCH 20/30] simplify abstract DP presentation further with typeclass synonym --- SampCert/DifferentialPrivacy/Abstract.lean | 31 +++++++++++++++---- .../ZeroConcentrated/System.lean | 6 ++-- 2 files changed, 28 insertions(+), 9 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Abstract.lean b/SampCert/DifferentialPrivacy/Abstract.lean index 7bef65ae..93480da3 100644 --- a/SampCert/DifferentialPrivacy/Abstract.lean +++ b/SampCert/DifferentialPrivacy/Abstract.lean @@ -19,6 +19,27 @@ 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. -/ @@ -45,9 +66,7 @@ class DPSystem (T : Type) where /-- 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] + 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) ε₂) -> ε₁ + ε₂ = ε -> @@ -55,13 +74,13 @@ class DPSystem (T : Type) where /-- Privacy is invariant under post-processing. -/ - postprocess_prop {U : Type} [MeasurableSpace U] [Countable U] [DiscreteMeasurableSpace U] [Inhabited U] + 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} {ε : NNReal} : + const_prop {U : Type} [DiscProbSpace U] {u : U} {ε : NNReal} : ε = (0 : NNReal) -> prop (privConst u) ε namespace DPSystem @@ -69,7 +88,7 @@ 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] : +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 diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean index fc794fad..e9501786 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean @@ -34,17 +34,17 @@ instance zCDPSystem : DPSystem T where intro _ _ _ _ H HZ apply zCDP_mono H HZ adaptive_compose_prop := by - intros _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ HZ HZ2 Hε + intros _ _ _ _ _ _ _ _ _ HZ HZ2 Hε rw [<- Hε] apply privComposeAdaptive_zCDP apply HZ apply HZ2 postprocess_prop := by - intros _ _ _ _ _ _ _ _ _ HZ + intros _ _ _ _ _ _ HZ apply privPostProcess_zCDP apply HZ const_prop := by - intros _ _ _ _ _ _ Hε + intros _ _ _ _ Hε rw [Hε] apply privConst_zCDP From 22416518a296a18c32ecd52480c456947b0970b8 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Sat, 2 Nov 2024 13:13:10 -0400 Subject: [PATCH 21/30] shorten histogram proofs --- .../Queries/Histogram/Properties.lean | 61 ++++++------------- 1 file changed, 17 insertions(+), 44 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean b/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean index 50e6580f..5cbee3f0 100644 --- a/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean @@ -32,26 +32,10 @@ exactBinCount is 1-sensitive -/ theorem exactBinCount_sensitivity (b : Fin numBins) : sensitivity (exactBinCount numBins B b) 1 := by rw [sensitivity] - intros l₁ l₂ HN - cases HN - · rename_i l₁' l₂' v' Hl₁ Hl₂ - rw [ Hl₁, Hl₂ ] - rw [exactBinCount, exactBinCount] - simp [List.filter_cons] - aesop - · rename_i l₁' v' l₂' Hl₁ Hl₂ - rw [ Hl₁, Hl₂ ] - rw [exactBinCount, exactBinCount] - simp [List.filter_cons] - aesop - · rename_i l₁' v₁' l₂' v₂' Hl₁ Hl₂ - rw [ Hl₁, Hl₂ ] - rw [exactBinCount, exactBinCount] - simp [List.filter_cons] - -- There has to be a better way - cases (Classical.em (B.bin v₁' = b)) <;> cases (Classical.em (B.bin v₂' = b)) - all_goals (rename_i Hrw1 Hrw2) - all_goals (simp [Hrw1, Hrw2]) + intros _ _ H + cases H + all_goals simp_all [exactBinCount, exactBinCount, List.filter_cons] + all_goals aesop /-- DP bound for a noised bin count @@ -71,25 +55,18 @@ lemma privNoisedHistogramAux_DP (ε₁ ε₂ : ℕ+) (ε : NNReal) (n : ℕ) (Hn dps.prop (privNoisedHistogramAux numBins B ε₁ ε₂ n Hn) (n.succ * (ε / numBins)) := by induction n · unfold privNoisedHistogramAux - simp only [Nat.cast_zero, succ_eq_add_one, zero_add, Nat.cast_one, Nat.cast_mul, one_mul] - apply DPSystem.postprocess_prop - apply DPSystem.compose_prop ?SC1 - · apply privNoisedBinCount_DP - apply HN_bin - · apply DPSystem.const_prop - rfl - case SC1 => simp only [add_zero] - · rename_i n IH - unfold privNoisedHistogramAux - simp only [] - apply DPSystem.postprocess_prop - apply DPSystem.compose_prop ?SC1 - · apply privNoisedBinCount_DP - apply HN_bin + simp + apply dps.postprocess_prop + apply dps.compose_prop (AddLeftCancelMonoid.add_zero _) + · apply privNoisedBinCount_DP; apply HN_bin + · apply dps.const_prop; rfl + · rename_i _ IH + simp [privNoisedHistogramAux] + apply dps.postprocess_prop + apply dps.compose_prop ?arithmetic + · apply privNoisedBinCount_DP; apply HN_bin · apply IH - case SC1 => - simp - ring_nf + case arithmetic => simp; ring_nf /-- DP bound for a noised histogram @@ -98,12 +75,8 @@ lemma privNoisedHistogram_DP (ε₁ ε₂ : ℕ+) (ε : NNReal) (HN_bin : dpn.no dps.prop (privNoisedHistogram numBins B ε₁ ε₂) ε := by unfold privNoisedHistogram apply (DPSystem_prop_ext _ ?HEq ?Hdp) - case Hdp => - apply privNoisedHistogramAux_DP - apply HN_bin - case HEq => - simp [predBins] - simp [mul_div_left_comm] + case Hdp => apply privNoisedHistogramAux_DP; apply HN_bin + case HEq => simp [predBins, mul_div_left_comm] /-- DP bound for the thresholding maximum From dc787efec776d52f67e42025817867da428acd89 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Sat, 2 Nov 2024 13:58:03 -0400 Subject: [PATCH 22/30] histogram: move epsilons to variable --- .../Queries/Histogram/Properties.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean b/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean index 5cbee3f0..9eeffd35 100644 --- a/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean @@ -27,6 +27,8 @@ variable [HT : Inhabited T] variable (numBins : ℕ+) variable (B : Bins T numBins) +variable (ε₁ ε₂ : ℕ+) (ε : NNReal) (HN_bin : dpn.noise_priv ε₁ (ε₂ * numBins) (ε / numBins)) + /- exactBinCount is 1-sensitive -/ @@ -40,8 +42,7 @@ theorem exactBinCount_sensitivity (b : Fin numBins) : sensitivity (exactBinCount /-- DP bound for a noised bin count -/ -lemma privNoisedBinCount_DP (ε₁ ε₂ : ℕ+) (ε : NNReal) (b : Fin numBins) - (HN_bin : dpn.noise_priv ε₁ (ε₂ * numBins) (ε / numBins)) : +lemma privNoisedBinCount_DP (b : Fin numBins) : dps.prop (privNoisedBinCount numBins B ε₁ ε₂ b) (ε / numBins) := by unfold privNoisedBinCount apply dpn.noise_prop HN_bin @@ -50,8 +51,7 @@ lemma privNoisedBinCount_DP (ε₁ ε₂ : ℕ+) (ε : NNReal) (b : Fin numBins) /-- DP bound for intermediate steps in the histogram calculation. -/ -lemma privNoisedHistogramAux_DP (ε₁ ε₂ : ℕ+) (ε : NNReal) (n : ℕ) (Hn : n < numBins) - (HN_bin : dpn.noise_priv ε₁ (ε₂ * numBins) (ε / numBins)) : +lemma privNoisedHistogramAux_DP (n : ℕ) (Hn : n < numBins) : dps.prop (privNoisedHistogramAux numBins B ε₁ ε₂ n Hn) (n.succ * (ε / numBins)) := by induction n · unfold privNoisedHistogramAux @@ -71,7 +71,7 @@ lemma privNoisedHistogramAux_DP (ε₁ ε₂ : ℕ+) (ε : NNReal) (n : ℕ) (Hn /-- DP bound for a noised histogram -/ -lemma privNoisedHistogram_DP (ε₁ ε₂ : ℕ+) (ε : NNReal) (HN_bin : dpn.noise_priv ε₁ (ε₂ * numBins) (ε / numBins)) : +lemma privNoisedHistogram_DP : dps.prop (privNoisedHistogram numBins B ε₁ ε₂) ε := by unfold privNoisedHistogram apply (DPSystem_prop_ext _ ?HEq ?Hdp) @@ -81,7 +81,7 @@ lemma privNoisedHistogram_DP (ε₁ ε₂ : ℕ+) (ε : NNReal) (HN_bin : dpn.no /-- DP bound for the thresholding maximum -/ -lemma privMaxBinAboveThreshold_DP (ε₁ ε₂ : ℕ+) (ε : NNReal) (τ : ℤ) (HN_bin : dpn.noise_priv ε₁ (ε₂ * numBins) (ε / numBins)) : +lemma privMaxBinAboveThreshold_DP (τ : ℤ) : dps.prop (privMaxBinAboveThreshold numBins B ε₁ ε₂ τ) ε := by unfold privMaxBinAboveThreshold apply dps.postprocess_prop From 1b8cf409b0717173783c804ff228a87ebbe808c1 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 5 Nov 2024 10:18:35 -0500 Subject: [PATCH 23/30] define SPMF --- SampCert/DifferentialPrivacy/Generic.lean | 55 +++++++++++++++++++++-- 1 file changed, 52 insertions(+), 3 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Generic.lean b/SampCert/DifferentialPrivacy/Generic.lean index be8e333c..f4a64acd 100644 --- a/SampCert/DifferentialPrivacy/Generic.lean +++ b/SampCert/DifferentialPrivacy/Generic.lean @@ -13,16 +13,63 @@ import SampCert.Foundations.Basic This file defines an abstract system of differentially private operators. -/ -noncomputable section - -open Classical Nat Int Real ENNReal namespace SLang +/- +A SPMF is a SLang program that is a also proper distribution +-/ +abbrev SPMF.{u} (α : Type u) : Type u := { f : SLang α // HasSum f 1 } + +instance : Coe (SPMF α) (SLang α) where + coe a := a.1 + +instance : Coe (SPMF α) (PMF α) where + coe a := ⟨ a.1, a.2 ⟩ + + + +def SPMF_pure (a : α) : SPMF α := + ⟨ probPure a, + by + have H : PMF.pure a = probPure a := by + unfold probPure + simp [DFunLike.coe, PMF.instFunLike, PMF.pure] + rw [<- H] + cases (PMF.pure a) + simp [DFunLike.coe, PMF.instFunLike] + trivial ⟩ + +def SPMF_bind (p : SPMF α) (q : α -> SPMF β) : SPMF β := + ⟨ probBind p (fun x => q x), + by + have H : (probBind p (fun x => q x)) = (PMF.bind p q) := by + unfold probBind + simp [DFunLike.coe, PMF.instFunLike, PMF.bind] + rw [H] + cases (PMF.bind p q) + simp [DFunLike.coe, PMF.instFunLike] + trivial ⟩ + +instance : Monad SPMF where + pure := SPMF_pure + bind := SPMF_bind + abbrev Query (T U : Type) := List T → U abbrev Mechanism (T U : Type) := List T → PMF U + + + + + + + +noncomputable section + +open Classical Nat Int Real ENNReal + /-- General (value-dependent) composition of mechanisms -/ @@ -218,4 +265,6 @@ lemma condition_to_subset (f : U → V) (g : U → ENNReal) (x : V) : simp rw [B] +end + end SLang From e4a2f4658baed613fbd50aeb8fe397946aef8fb8 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 5 Nov 2024 10:24:05 -0500 Subject: [PATCH 24/30] SPMF: generic --- SampCert/DifferentialPrivacy/Generic.lean | 59 +++++++++++++---------- 1 file changed, 33 insertions(+), 26 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Generic.lean b/SampCert/DifferentialPrivacy/Generic.lean index f4a64acd..6d82cbf3 100644 --- a/SampCert/DifferentialPrivacy/Generic.lean +++ b/SampCert/DifferentialPrivacy/Generic.lean @@ -29,6 +29,7 @@ instance : Coe (SPMF α) (PMF α) where +@[simp] def SPMF_pure (a : α) : SPMF α := ⟨ probPure a, by @@ -40,6 +41,7 @@ def SPMF_pure (a : α) : SPMF α := simp [DFunLike.coe, PMF.instFunLike] trivial ⟩ +@[simp] def SPMF_bind (p : SPMF α) (q : α -> SPMF β) : SPMF β := ⟨ probBind p (fun x => q x), by @@ -55,13 +57,37 @@ instance : Monad SPMF where pure := SPMF_pure bind := SPMF_bind + + 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) : SPMF (U × V) := do + let A <- nq1 l + let B <- nq2 A l + return (A, B) +/-- +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 @@ -70,15 +96,12 @@ noncomputable section open Classical Nat Int Real ENNReal -/-- -General (value-dependent) composition of mechanisms --/ -def privComposeAdaptive (nq1 : Mechanism T U) (nq2 : U -> Mechanism T V) (l : List T) : PMF (U × V) := do - let A <- nq1 l - let B <- nq2 A l - return (A, B) +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 → PMF U) (nq2 : U -> List T → PMF V) (u : U) (v : V) (l : List T) : + +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 @@ -117,24 +140,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] From e023a0faebef6af7a3cf11db55941c4b7700ab01 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 5 Nov 2024 10:30:06 -0500 Subject: [PATCH 25/30] postprocessing --- SampCert/DifferentialPrivacy/Pure/Postprocessing.lean | 1 + .../DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean | 3 +-- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Pure/Postprocessing.lean b/SampCert/DifferentialPrivacy/Pure/Postprocessing.lean index 4e57529a..8621724a 100644 --- a/SampCert/DifferentialPrivacy/Pure/Postprocessing.lean +++ b/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 diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean index 6ebaacb2..782dc5c6 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean @@ -37,6 +37,7 @@ def privPostProcess_AC {f : U -> V} (nq : Mechanism T U) (Hac : ACNeighbour nq) intro l₁ l₂ Hn v have Hac := Hac l₁ l₂ Hn simp [privPostProcess] + simp [DFunLike.coe, SPMF.instFunLike] intro Hppz i fi apply Hac apply Hppz @@ -575,8 +576,6 @@ theorem privPostProcess_zCDPBound {nq : Mechanism T U} {ε : ℝ} apply inv_nonneg_of_nonneg linarith apply elog_mono_le.mp - simp [PMF.bind, PMF.pure] - simp [PMF.instFunLike] apply privPostPocess_DP_pre · exact fun l => PMF.hasSum_coe_one (nq l) · exact h1 From 1b861657a1c33d16067e834b29f2f36401fe2834 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 5 Nov 2024 10:34:08 -0500 Subject: [PATCH 26/30] update queries to be computable --- SampCert.lean | 2 +- SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean | 4 +--- SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean | 2 -- SampCert/DifferentialPrivacy/Queries/Count/Code.lean | 2 -- SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean | 2 -- SampCert/DifferentialPrivacy/Queries/HistogramMean/Code.lean | 2 -- 6 files changed, 2 insertions(+), 12 deletions(-) diff --git a/SampCert.lean b/SampCert.lean index ebafb641..be2abe77 100644 --- a/SampCert.lean +++ b/SampCert.lean @@ -40,7 +40,7 @@ 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 ℚ) := +def combineMeanHistogram : Mechanism ℕ (Option ℚ) := privMeanHistogram PureDPSystem laplace_pureDPSystem numBins { bin } unbin 1 20 2 1 20 end histogramMeanExample diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean index 79234d71..dc94cd09 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean @@ -13,8 +13,6 @@ import SampCert.DifferentialPrivacy.Queries.BoundedSum.Code This file defines a differentially private bounded mean query. -/ -noncomputable section - namespace SLang variable [dps : DPSystem ℕ] @@ -23,7 +21,7 @@ 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 diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean b/SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean index ffdc6f98..1396256d 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean @@ -14,8 +14,6 @@ import Init.Data.Int.Order This file defines a differentially private bounded sum query. -/ -noncomputable section - namespace SLang variable [dps : DPSystem ℕ] diff --git a/SampCert/DifferentialPrivacy/Queries/Count/Code.lean b/SampCert/DifferentialPrivacy/Queries/Count/Code.lean index b38929ef..f9bf360f 100644 --- a/SampCert/DifferentialPrivacy/Queries/Count/Code.lean +++ b/SampCert/DifferentialPrivacy/Queries/Count/Code.lean @@ -11,8 +11,6 @@ import SampCert.DifferentialPrivacy.Abstract This file defines a differentially private noising of an exact length query. -/ -noncomputable section - namespace SLang variable {T : Type} diff --git a/SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean b/SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean index 9342a6c9..eb6f25aa 100644 --- a/SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean +++ b/SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean @@ -24,8 +24,6 @@ structure Bins (T : Type) (num_bins : ℕ) where ## Private Histograms -/ -noncomputable section - variable (numBins : ℕ+) def predBins : ℕ := numBins.natPred diff --git a/SampCert/DifferentialPrivacy/Queries/HistogramMean/Code.lean b/SampCert/DifferentialPrivacy/Queries/HistogramMean/Code.lean index 6bb35172..51546d49 100644 --- a/SampCert/DifferentialPrivacy/Queries/HistogramMean/Code.lean +++ b/SampCert/DifferentialPrivacy/Queries/HistogramMean/Code.lean @@ -20,8 +20,6 @@ Implementation for ## Compute the mean using a histogram to compute the noisy max -/ -noncomputable section - variable (dps : SLang.DPSystem ℕ) variable (dpn : SLang.DPNoise dps) variable (numBins : ℕ+) From b806c8bd9257cb361aac7ae679c25de4790eb531 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 5 Nov 2024 10:47:08 -0500 Subject: [PATCH 27/30] move SPMF to SLang --- SampCert/DifferentialPrivacy/Generic.lean | 42 ---------------------- SampCert/SLang.lean | 43 ++++++++++++++++++++++- 2 files changed, 42 insertions(+), 43 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Generic.lean b/SampCert/DifferentialPrivacy/Generic.lean index 6d82cbf3..8c46773e 100644 --- a/SampCert/DifferentialPrivacy/Generic.lean +++ b/SampCert/DifferentialPrivacy/Generic.lean @@ -16,48 +16,6 @@ This file defines an abstract system of differentially private operators. namespace SLang -/- -A SPMF is a SLang program that is a also proper distribution --/ -abbrev SPMF.{u} (α : Type u) : Type u := { f : SLang α // HasSum f 1 } - -instance : Coe (SPMF α) (SLang α) where - coe a := a.1 - -instance : Coe (SPMF α) (PMF α) where - coe a := ⟨ a.1, a.2 ⟩ - - - -@[simp] -def SPMF_pure (a : α) : SPMF α := - ⟨ probPure a, - by - have H : PMF.pure a = probPure a := by - unfold probPure - simp [DFunLike.coe, PMF.instFunLike, PMF.pure] - rw [<- H] - cases (PMF.pure a) - simp [DFunLike.coe, PMF.instFunLike] - trivial ⟩ - -@[simp] -def SPMF_bind (p : SPMF α) (q : α -> SPMF β) : SPMF β := - ⟨ probBind p (fun x => q x), - by - have H : (probBind p (fun x => q x)) = (PMF.bind p q) := by - unfold probBind - simp [DFunLike.coe, PMF.instFunLike, PMF.bind] - rw [H] - cases (PMF.bind p q) - simp [DFunLike.coe, PMF.instFunLike] - trivial ⟩ - -instance : Monad SPMF where - pure := SPMF_pure - bind := SPMF_bind - - abbrev Query (T U : Type) := List T → U diff --git a/SampCert/SLang.lean b/SampCert/SLang.lean index 5566b5fb..85be3cdb 100644 --- a/SampCert/SLang.lean +++ b/SampCert/SLang.lean @@ -144,11 +144,52 @@ def probUntil (body : SLang T) (cond : T → Bool) : SLang T := do let v ← body probWhile (λ v : T => ¬ cond v) (λ _ : T => body) v + +/- +A SPMF is a SLang program that is a also proper distribution +-/ +abbrev SPMF.{u} (α : Type u) : Type u := { f : SLang α // HasSum f 1 } + +instance : Coe (SPMF α) (SLang α) where + coe a := a.1 + +instance : Coe (SPMF α) (PMF α) where + coe a := ⟨ a.1, a.2 ⟩ + + +@[simp] +def SPMF_pure (a : α) : SPMF α := + ⟨ probPure a, + by + have H : PMF.pure a = probPure a := by + unfold probPure + simp [DFunLike.coe, PMF.instFunLike, PMF.pure] + rw [<- H] + cases (PMF.pure a) + simp [DFunLike.coe, PMF.instFunLike] + trivial ⟩ + +@[simp] +def SPMF_bind (p : SPMF α) (q : α -> SPMF β) : SPMF β := + ⟨ probBind p (fun x => q x), + by + have H : (probBind p (fun x => q x)) = (PMF.bind p q) := by + unfold probBind + simp [DFunLike.coe, PMF.instFunLike, PMF.bind] + rw [H] + cases (PMF.bind p q) + simp [DFunLike.coe, PMF.instFunLike] + trivial ⟩ + +instance : Monad SPMF where + pure := SPMF_pure + bind := SPMF_bind + end SLang namespace PMF @[extern "my_run"] -opaque run (c : PMF T) : IO T +opaque run (c : SLang.SPMF T) : IO T end PMF From f75fe5a62ec2384f942ecee7e2dc016ed4a30383 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 5 Nov 2024 11:56:50 -0500 Subject: [PATCH 28/30] query tests --- SampCert.lean | 4 +- SampCert/Samplers/Uniform/Properties.lean | 2 +- Test.lean | 62 ++++++++++++++++++++++- 3 files changed, 64 insertions(+), 4 deletions(-) diff --git a/SampCert.lean b/SampCert.lean index be2abe77..1e1285dc 100644 --- a/SampCert.lean +++ b/SampCert.lean @@ -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 @@ -41,7 +41,7 @@ Return an upper bound on the bin value, clipped to 2^(1 + numBins) def unbin (n : Fin numBins) : ℕ+ := 2 ^ (1 + n.val) def combineMeanHistogram : Mechanism ℕ (Option ℚ) := - privMeanHistogram PureDPSystem laplace_pureDPSystem numBins { bin } unbin 1 20 2 1 20 + privMeanHistogram PureDPSystem laplace_pureDPSystem numBins { bin := example_bin } unbin 1 20 2 1 20 end histogramMeanExample diff --git a/SampCert/Samplers/Uniform/Properties.lean b/SampCert/Samplers/Uniform/Properties.lean index fd7539bf..21a85d48 100644 --- a/SampCert/Samplers/Uniform/Properties.lean +++ b/SampCert/Samplers/Uniform/Properties.lean @@ -249,7 +249,7 @@ theorem UniformSample_HasSum_1 (n : PNat) : /-- Conversion of ``UniformSample`` from a ``SLang`` term to a ``PMF``. -/ -noncomputable def UniformSample_PMF (n : PNat) : PMF ℕ := ⟨ UniformSample n , UniformSample_HasSum_1 n⟩ +def UniformSample_PMF (n : PNat) : SPMF ℕ := ⟨ UniformSample n , UniformSample_HasSum_1 n⟩ /-- Evaluation of ``UniformSample`` on ``ℕ`` guarded by its support, when inside the support. diff --git a/Test.lean b/Test.lean index 930ddeb8..c30f3493 100644 --- a/Test.lean +++ b/Test.lean @@ -6,6 +6,7 @@ Authors: Jean-Baptiste Tristan import SampCert import SampCert.SLang import SampCert.Samplers.Gaussian.Properties +import Init.Data.Float open SLang Std Int Array PMF @@ -173,7 +174,61 @@ def test (num den : ℕ+) (mix numSamples : ℕ) (threshold : Float) : IO Unit : IO.println s!"Kolmogorov distance = {D}" -def main : IO Unit := do +def query_tests : IO Unit := do + -- Generate list of 1000 numbers from 0 to 15 + let samples := 10000 + let unif_ub := 10 + let data : List ℕ <- List.mapM (fun _ => run <| (SLang.UniformSample_PMF unif_ub)) (List.replicate samples 0) + + let num : ℕ+ := 9 + let den : ℕ+ := 2 + let num_trials := 5 + + IO.println s!"[query] testing pure ({(num : ℕ)} / {(den : ℕ)})-DP queries" + IO.println s!"data := {samples} uniform samples of [0, {(unif_ub : ℕ)}): {(data.take 20)}..." + IO.println "" + + for i in [:num_trials] do + let ct <- run <| @privNoisedCount _ PureDPSystem laplace_pureDPSystem num den data + IO.println s!"#{i} count: {ct}" + IO.println "" + + let sum_bound : ℕ+ := 10 + for i in [:num_trials] do + let bs <- run <| @privNoisedBoundedSum PureDPSystem laplace_pureDPSystem sum_bound num den data + IO.println s!"#{i} bounded sum (bound = {(sum_bound : ℕ)}): {bs}" + IO.println "" + + for i in [:num_trials] do + let bs <- run <| @privNoisedBoundedMean PureDPSystem laplace_pureDPSystem sum_bound num den data + let float_bs := Float.div (Float.ofInt bs.1) (Float.ofInt bs.2) + IO.println s!"#{i} bounded mean (bound = {(sum_bound : ℕ)}): {bs} (~{float_bs})" + IO.println "" + + for i in [:num_trials] do + let h <- run <| @privNoisedHistogram numBins _ { bin := example_bin } PureDPSystem laplace_pureDPSystem num den data + let h' : List ℤ := h.count.toList.take 25 + IO.println s!"#{i} histogram : {h'}..." + IO.println "" + + let thresh := 100 + for i in [:num_trials] do + let m <- run <| @privMaxBinAboveThreshold numBins _ { bin := example_bin } PureDPSystem laplace_pureDPSystem num den thresh data + IO.println s!"#{i} max bin above threshold (threshold = {(thresh : ℤ)}): {m}" + IO.println "" + + let τ := 100 + for i in [:num_trials] do + let m <- run <| @privMeanHistogram PureDPSystem laplace_pureDPSystem numBins { bin := example_bin } unbin num den τ num den data + let m_float := + match m with + | none => none + | some bs => some (Float.div (Float.ofInt bs.1) (Float.ofInt bs.2)) + IO.println s!"#{i} (0.5x-privacy) histogram mean, τ = {τ}: {m} (~{m_float})" + IO.println "" + +def statistical_tests : IO Unit := do + IO.println s!"[samplers] statistical tests" let tests : List (ℕ+ × ℕ+ × ℕ) := [ -- (1,1,0), (1,1,7), @@ -188,3 +243,8 @@ def main : IO Unit := do for (num,den,mix) in tests do IO.println s!"num = {(num : ℕ)}, den = {(den : ℕ)}, mix = {mix}" test num den mix 100000 0.1 + + +def main : IO Unit := do + query_tests + statistical_tests From 0884bac8a25018a2935584bd366bd4a895365484 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 12 Nov 2024 11:10:11 -0500 Subject: [PATCH 29/30] rename adp -> app_dp --- SampCert/DifferentialPrivacy/Abstract.lean | 4 ++-- SampCert/DifferentialPrivacy/Pure/System.lean | 2 +- SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Abstract.lean b/SampCert/DifferentialPrivacy/Abstract.lean index 93480da3..04c56591 100644 --- a/SampCert/DifferentialPrivacy/Abstract.lean +++ b/SampCert/DifferentialPrivacy/Abstract.lean @@ -52,12 +52,12 @@ class DPSystem (T : Type) where /-- Definition of DP is well-formed: Privacy parameter required to obtain (ε', δ)-approximate DP -/ - of_adp : (δ : NNReal) -> (ε' : NNReal) -> NNReal + of_app_dp : (δ : NNReal) -> (ε' : NNReal) -> NNReal /-- For any ε', this definition of DP implies (ε', δ)-approximate-DP for all δ -/ prop_adp [Countable Z] {m : Mechanism T Z} : ∀ (δ : NNReal) (_ : 0 < δ) (ε' : NNReal), - (prop m (of_adp δ ε') -> ApproximateDP m ε' δ) + (prop m (of_app_dp δ ε') -> ApproximateDP m ε' δ) /-- DP is monotonic -/ diff --git a/SampCert/DifferentialPrivacy/Pure/System.lean b/SampCert/DifferentialPrivacy/Pure/System.lean index a8667cf6..c6a7a786 100644 --- a/SampCert/DifferentialPrivacy/Pure/System.lean +++ b/SampCert/DifferentialPrivacy/Pure/System.lean @@ -23,7 +23,7 @@ Pure ε-DP with noise drawn from the discrete Laplace distribution. -/ instance PureDPSystem : DPSystem T where prop := PureDP - of_adp := pure_of_adp + of_app_dp := pure_of_adp prop_adp := pure_ApproximateDP prop_mono := PureDP_mono adaptive_compose_prop := by diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean index e9501786..7849dad5 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean @@ -27,7 +27,7 @@ Instance of a DP system for zCDP -/ instance zCDPSystem : DPSystem T where prop := zCDP - of_adp := zCDP_of_adp + of_app_dp := zCDP_of_adp prop_adp := by intros; apply zCDP_ApproximateDP <;> assumption prop_mono := by From 6372ea04f9471fb98fc309fa6da85b2898b74610 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 12 Nov 2024 11:11:26 -0500 Subject: [PATCH 30/30] Countable -> DiscProbSpace --- SampCert/DifferentialPrivacy/Abstract.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SampCert/DifferentialPrivacy/Abstract.lean b/SampCert/DifferentialPrivacy/Abstract.lean index 04c56591..7fc52d73 100644 --- a/SampCert/DifferentialPrivacy/Abstract.lean +++ b/SampCert/DifferentialPrivacy/Abstract.lean @@ -56,7 +56,7 @@ class DPSystem (T : Type) where /-- For any ε', this definition of DP implies (ε', δ)-approximate-DP for all δ -/ - prop_adp [Countable Z] {m : Mechanism T Z} : ∀ (δ : NNReal) (_ : 0 < δ) (ε' : NNReal), + prop_adp [DiscProbSpace Z] {m : Mechanism T Z} : ∀ (δ : NNReal) (_ : 0 < δ) (ε' : NNReal), (prop m (of_app_dp δ ε') -> ApproximateDP m ε' δ) /-- DP is monotonic