Implementation-of-randomized-mechanisms

.vscode/c_cpp_properties.json

@@ -0,0 +1,20 @@
+{
+    "configurations": [
+        {
+            "name": "Win32",
+            "includePath": [
+                "${workspaceFolder}/**"
+            ],
+            "defines": [
+                "_DEBUG",
+                "UNICODE",
+                "_UNICODE"
+            ],
+            "compilerPath": "C:\\msys64\\ucrt64\\bin\\gcc.exe",
+            "cStandard": "c17",
+            "cppStandard": "gnu++17",
+            "intelliSenseMode": "windows-gcc-x64"
+        }
+    ],
+    "version": 4
+}

.vscode/settings.json

@@ -0,0 +1,3 @@
+{
+    "C_Cpp.errorSquiggles": "disabled"
+}

README.md

@@ -1,22 +1,72 @@
-# SampCert
+# Verifying Differential Privacy in Lean
 
-A verified implementation using [Lean](https://github.com/leanprover/lean4) and [Mathlib](https://github.com/leanprover-community/mathlib4) of randomized algorithms including [the discrete Gaussian sampler for differential privacy](https://arxiv.org/abs/2004.00010), key results in [zero concentrated differential privacy](https://arxiv.org/abs/1605.02065), and [some verified (unbounded) private queries](https://arxiv.org/pdf/1909.01917).
+The [SampCert](https://github.com/leanprover/SampCert) project (de Medeiros et al. 2024) was created to implement and formalize differential privacy notions in Lean. It provided support for various notions of differential privacy, a framework for implementing differentially private mechanisms via verified sampling algorithms, and implemented several differentially private algorithms, including the Gaussian and Laplace mechanisms.
 
-SampCert is deployed and used in the [AWS Clean Rooms Differential Privacy service](https://docs.aws.amazon.com/clean-rooms/latest/userguide/differential-privacy.html#dp-overview). SampCert proves deep properties about some of its randomized algorithm and makes heavy use of Mathlib. For example, we use theorems such as [the Poisson summation formula](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Fourier/PoissonSummation.html#Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay).
+We build upon SampCert, creating support for the local model using [Lean](https://lean-lang.org/) and the extensive [Mathlib](https://github.com/leanprover-community/mathlib4) library. We also implement the [randomized response](https://www.tandfonline.com/doi/abs/10.1080/01621459.1965.10480775) and [one-time basic RAPPOR](https://static.googleusercontent.com/media/research.google.com/en//pubs/archive/42852.pdf) mechanisms, as well as a more robust post-processing property for randomized mappings. We additionally move towards an implementation of the shuffle model.
 
-The principal developer of SampCert is [Jean-Baptiste Tristan](https://jtristan.github.io/). It is also developed by [Markus de Medeiros](https://www.markusde.ca/). 
+Our implementations are in `SampCert/DifferentialPrivacy/Pure`. Our additions are in the Local folder, Shuffle Model folder, and a few separate files in the Pure folder.
 
-Other people have contributed important ideas or tools for deployment including (in no particular order): Leo de Moura, Anjali Joshi, Joseph Tassarotti, Stefan Zetzsche, Aws Albharghouti, Muhammad Naveed, Tristan Ravitch, Fabian Zaiser, Tomas Skrivan.
+### Local
 
-To cite SampCert you can currently use the following reference:
-```
-@software{Tristan_SampCert_Verified_2024,
-author = {Tristan, Jean-Baptiste},
-doi = {10.5281/zenodo.11204806},
-month = may,
-title = {{SampCert : Verified Differential Privacy}},
-url = {https://github.com/leanprover/SampCert},
-version = {1.0.0},
-year = {2024}
-}
-```
+#### BinomialSample
+
+We implement and show normalization for a sampler for the Binomial distribution.
+
+#### LocalDP
+
+The files in this folder provide a variety of definitions to support the local model of differential privacy. We create a definition of differential privacy that is parametrized by a neighbour relation, thus generalizing the SampCert definition. For the local model, we use the `DP_withUpdateNeighbour` definition of neighboring datasets, which considers two lists to be neighbouring if they differ in the update of a single entry.
+
+We also show that if an $\epsilon$-local randomizer is extended to a dataset via monadic map, the resulting algorithm is $\epsilon$-differentially private. This is proven in `LocalDP_toDataset.`
+
+#### MultiBernoulli
+
+The files here implement and show normalization for the "multi-Bernoulli" distribution, which we define to be the distribution associated with flipping each entry of a list independently and with the same probability.
+
+#### RAPPOR
+
+In this folder, we provide an implementation of basic one-time RAPPOR and give a proof of differential privacy. The file `Definitions.lean` provides our implementation of RAPPOR. The file `Properties/DPProof.lean` provides a proof that our implementation of RAPPOR is differentially private.
+
+#### RandomizedResponse
+
+In this folder, we provide an implementation of randomized response and give a proof of differential privacy. The file `Definitions.lean` provides our implementation of randomized response. The file `Properties/DPProof.lean` provides a proof that our implementation of randomized response is differentially private.
+
+#### ProbabilityProduct.lean
+
+We show that the probability of generating a list of outputs is equal to the product of the probabilities of generating each output independently. This is used to prove our `LocalDP_toDataset` lemma.
+#### PushForward.lean
+
+We prove that the push-forward of a probability measure is a probability measure. A similar statement already exists in SampCert, but our rephrasing was slightly more convenient for our purposes.
+#### Reduction.lean
+
+We prove a helper lemma that is used in proving a local algorithm is DP. It allows us to reduce the problem to just considering the local randomizer.
+
+### Shuffle model
+
+This folder contains the implementation and properties of the shuffle model.
+
+#### Definitions.lean
+
+This contains the definition of the shuffle model. The definition `Shuffler` is the randomized permutation. We implement the shuffle algorithm with randomized response in `RRShuffle`, and provide a more general definition in `ShuffleAlgorithm`.
+
+#### Properties.lean
+
+This instantiates the shuffle algorithm as a PMF, and show that our algorithm for a random permutation that is indeed uniformly random. In the theorem `ShuffleAlgorithm_is_DP`, we show that shuffling the output of a differentially-private algorithm does not worsen the differential privacy bound. 
+
+#### ENNRealLemmaSuite.lean
+
+A significant challenge in our work was proving arithemetic statements over extended non-negative reals. Mathlib currently provides less support for arithmetic in the ENNReal type, so oftentimes we have to prove statements ourselves. These statements are in this file.
+
+#### LawfulMonadSLang.lean
+
+We instantiate SLang as a LawfulMonad. 
+
+#### Normalization.lean
+
+We prove a lemma showing that the mass of a distribution is preserved under monadic map. This is used for both of the local algorithms that we implemented.
+
+### RandomizedPostProcess.lean
+
+This file provides the Lean proof about the post-processing property of differential privacy: If there is an $\epsilon$-DP mechanism $M: X \rightarrow W$ and a (possibly randomized) mapping $F: W \rightarrow Z$, then $F \circ M$ is $\epsilon$-DP. The case where $F$ is deterministic is implemented in SampCert. We implement the case where $F$ is random. The result is in the lemma 
+``randPostProcess_DP_bound_with_UpdateNeighbour``.
+
+We would like to thank SampCert for motivating and being the basis for our project. We would also like to thank Google for sponsoring and mentoring this project, and the Institute of Pure and Applied Mathematics (IPAM) for supporting and hosting our work.

SampCert/DifferentialPrivacy/Neighbours.lean

@@ -16,14 +16,13 @@ variable {T : Type}
 /--
 Lists which differ by the inclusion or modification of an element.
 
-This is SampCert's private property. 
+This is SampCert's private property.
 -/
 inductive Neighbour (l₁ l₂ : List T) : Prop where
   | Addition : l₁ = a ++ b → l₂ = a ++ [n] ++ b → Neighbour l₁ l₂
   | Deletion : l₁ = a ++ [n] ++ b → l₂ = a ++ b → Neighbour l₁ l₂
   | Update : l₁ = a ++ [n] ++ b → l₂ = a ++ [m] ++ b -> Neighbour l₁ l₂
 
-
 /--
 Neighbour relation is symmetric.
 -/

SampCert/DifferentialPrivacy/Pure/Local/BinomialSample/Binomial.lean

@@ -0,0 +1,32 @@
+import SampCert.DifferentialPrivacy.Pure.Local.LocalDP.DPwithUpdateNeighbour
+import SampCert.DifferentialPrivacy.Pure.Local.MultiBernoulli.Code
+import SampCert.DifferentialPrivacy.Pure.Local.MultiBernoulli.Properties
+import SampCert.DifferentialPrivacy.Pure.Local.PushForward
+
+namespace SLang
+
+def BinomialSample (seed: MultiBernoulli.SeedType)(n:PNat) := do
+  let seeds := List.replicate n seed
+  let list ← MultiBernoulli.MultiBernoulliSample (seeds)
+  let k := List.count true list
+  return k
+
+theorem BinomialSample_norms [LawfulMonad SLang] (seed : MultiBernoulli.SeedType) (n : PNat) :
+  HasSum (BinomialSample seed n) 1 := by
+  rw [BinomialSample]
+  simp
+  unfold probBind
+  simp [Summable.hasSum_iff ENNReal.summable]
+  have h: (push_forward (MultiBernoulli.MultiBernoulliSample (List.replicate (↑n) seed))
+        (fun (a : List Bool) => (List.count true a))) = (fun (b : Nat) =>
+        (∑' (a : List Bool), if b = List.count true a then MultiBernoulli.MultiBernoulliSample
+        (List.replicate (↑n) seed) a else 0)) := by
+          unfold push_forward
+          rfl
+
+  rw [← h]
+  rw [push_forward_prob_is_prob]
+  simp [MultiBernoulli.MultiBernoulliSample_normalizes]
+
+  def BinomialSample_PMF [LawfulMonad SLang] (seed : MultiBernoulli.SeedType) (n : PNat) : PMF ℕ :=
+    ⟨BinomialSample seed n, BinomialSample_norms seed n⟩