Paper changes

Dockerfile

@@ -0,0 +1,40 @@
+FROM xtrm0/dafny
+
+USER root
+
+RUN apt-get update && apt-get install curl git g++ vim python3-pip -y && apt-get clean
+
+RUN pip install matplotlib scipy tqdm diffprivlib
+
+# create a non-root user
+RUN useradd -m lean
+
+USER lean
+
+WORKDIR /home/lean
+
+SHELL ["/bin/bash", "-c"]
+
+ENV PATH="/home/lean/.elan/bin:/home/lean/.local/bin:$PATH"
+
+RUN mkdir SampCert
+
+COPY --chown=lean . ./SampCert/
+
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none && \
+    . ~/.profile && \
+    elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}') && \
+    elan default stable
+
+RUN cd SampCert/ && \
+    lake exe cache get
+
+RUN cd SampCert/ && \
+    lake build
+
+RUN cd SampCert/ && \
+    lake build FastExtract && \
+    dafny build --target:py Tests/SampCert.dfy Tests/Random.py Tests/testing-kolmogorov-discretegaussian.py Tests/testing-kolmogorov-discretelaplace.py Tests/IBM/discretegauss.py Tests/benchmarks.py -o Tests/SampCert.dfy
+
+RUN cd SampCert && \
+    lake build test

REPRODUCING.md

@@ -0,0 +1,91 @@
+# SampCert Artifact
+
+Our artifact consists of 
+- The Lean 4 source code for SampCert, including all proofs mentioned in the paper, and a code extractor used to translate the samplers into Python. 
+- A script to benchmark the extracted SampCert samplers against other DP implementations.
+- A script to profile the number of bytes consumed by the discrete Gaussian sampler.
+- A script to run statistical tests on the extracted SampCert samplers. 
+- A Lean 4 program to run statistical tests on the SampCert samplers and example DP queries, using the Lean FFI. 
+
+## Building
+
+To build and enter the artifact, run the following commands (**from the root directory of the artifact**).
+```
+docker build --platform linux/amd64 -t sampcert .
+docker run -it --platform linux/amd64 --name sampcert sampcert /bin/bash
+```
+This will compile our Lean code, and extract the implementation of our samplers used by our Large Cloud Provider. 
+We have tested that this image builds and runs on a 2023 M2 Macbook Pro, Ubuntu Linux, and within WSL. 
+If running this docker image on a ARM system, please ensure that Rosetta2 virtualization is enabled.
+
+Alternatively, you can load our prebuilt docker image using 
+```
+docker image load -i sampcert-image.tar 
+docker run -it --platform linux/amd64 --name sampcert sampcert /bin/bash
+```
+
+
+## The Lean code
+
+The file `SampCert.lean` is the top-level file in the project. 
+To check that `definition-name` code is sorry-free, one can add the line 
+```
+#print axioms definition-name
+```
+to any file and recompile with `lake build` (**from inside the SampCert directory**). 
+For example, uncommenting `-- #print axioms combineMeanHistogram` at the bottom of `SampCert.lean` will print 
+```
+[2165/2166] Built SampCert
+info: ././././SampCert.lean:75:0: 'combineMeanHistogram' depends on axioms: [propext, Classical.choice, Quot.sound]
+```
+which does not include the axiom `sorryAx`, indicating that the definition and proof is closed. 
+
+The file ``paper_mapping.md`` includes a table that lists all of the definitions from our paper. 
+
+## Benchmarks
+
+To reproduce our benchmarks (figure 4), run the following command from (**the home directory, inside the artifact**): 
+```
+sh SampCert/Tests/run_benchmark.sh
+```
+This command will save a reproduction of figure 4 to the home directory. It can be accessed by running the following command (**from outside of the container**).
+```
+docker cp sampcert:/home/lean/GaussianBenchmarks.pdf .
+```
+
+To profile the number of bytes of entropy consumed, we have a version of the code instrumented with logging on a separate branch (``git diff main..PLDI25-profiling`` will show you the differences). 
+To produce a figure that counts the number of bytes of entropy consumed, run the following (**from the SampCert directory**):
+```
+git checkout PLDI25-profiling
+lake build profile
+LD_LIBRARY_PATH=.lake/build/lib/ python3 profile.py 
+```
+To view the profile, it can be copied out of the container by executing the following (**from outside of the container**):
+```
+docker cp sampcert:/home/lean/SampCert/GaussianProfile.pdf .
+```
+
+
+## Statistical Tests: Extracted samplers
+
+To check that our extracted samplers execute and sample from the correct distribution, we have included a K-S test.
+To run the tests on the extracted versions, run the following (**from the home directory, on the main branch**):
+```
+python3 SampCert/Tests/SampCert-py/testing-kolmogorov-discretegaussian.py
+python3 SampCert/Tests/SampCert-py/testing-kolmogorov-discretelaplace.py
+```
+The script reports `Test passed!` when the kolmogorov distance between the computed and ideal CDF is within `0.02`. 
+
+
+## Tests: FFI samplers
+
+To demonstrate our claim that our code can be executed within Lean using the C FFI we have rewritten the K-S test, as well as several example queries, inside the file `Test.lean`. 
+To run that file, execute the command (**from the SampCert directory, on the main branch**)
+```
+lake exe test
+```
+
+This will do the following:
+- Execute our implementation of the sparse vector technique on randomly generated sample data 
+- Execute our noised histogram query, and histogram mean queries, on randomly generated sample data,
+- Preform statistical tests on our implementation of the discrete Gaussian, and report the Kolmogorov distance as above. 

SampCert.lean

@@ -8,13 +8,17 @@ import SampCert.DifferentialPrivacy.Queries.Histogram.Basic
 import SampCert.DifferentialPrivacy.ZeroConcentrated.System
 import SampCert.DifferentialPrivacy.Pure.System
 import SampCert.DifferentialPrivacy.Queries.HistogramMean.Properties
+import SampCert.DifferentialPrivacy.Queries.UnboundedMax.Basic
+import SampCert.DifferentialPrivacy.Queries.ParHistogram.Basic
+import SampCert.DifferentialPrivacy.Queries.Sparse.Basic
+import SampCert.DifferentialPrivacy.Queries.AboveThresh.Basic
 import SampCert.DifferentialPrivacy.Approximate.DP
 import SampCert.Samplers.Gaussian.Properties
 import Init.Data.UInt.Lemmas
 
 open SLang PMF
 
-def combineConcentrated := @privNoisedBoundedMean_DP gaussian_zCDPSystem
+def combineConcentrated := @privNoisedBoundedMean_DP zCDPSystem
 def combinePure := @privNoisedBoundedMean_DP PureDPSystem
 
 /-
@@ -27,7 +31,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
@@ -40,8 +44,8 @@ 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
+def combineMeanHistogram : Mechanism ℕ (Option ℚ) :=
+  privMeanHistogram PureDPSystem laplace_pureDPSystem numBins { bin := example_bin } unbin 1 20 2 1 20
 
 end histogramMeanExample
 
@@ -69,3 +73,5 @@ def DiscreteGaussianSampleGet (num den : UInt32) (mix: UInt32) : UInt32 := Id.ru
   else
     let z : IO ℤ ← run <| DiscreteGaussianPMF ⟨ num.toNat , UInt32.toNa_of_non_zero h₁ ⟩ ⟨ den.toNat , UInt32.toNa_of_non_zero h₂ ⟩ mix.toNat
     return DirtyIOGet z
+
+-- #print axioms combineMeanHistogram 

SampCert/DifferentialPrivacy/Abstract.lean

@@ -15,12 +15,31 @@ 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
 
+/--
+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.
 -/
@@ -31,54 +50,52 @@ 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_app_dp : (δ : 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 [DiscProbSpace Z] {m : Mechanism T Z} : ∀ (δ : NNReal) (_ : 0 < δ) (ε' : NNReal),
+    (prop m (of_app_dp δ ε') -> 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} :
+    ε₁ ≤ ε₂ -> 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,
-    prop m₁ ε₁ → (∀ u, prop (m₂ u) ε₂) -> prop (privComposeAdaptive m₁ m₂) (ε₁ + ε₂)
+  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) ε₂) ->
+    ε₁ + ε₂ = ε ->
+    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} [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) -> prop (privConst u) (0 : NNReal)
-
+  const_prop {U : Type} [DiscProbSpace U] {u : U} {ε : NNReal} :
+    ε = (0 : NNReal) -> prop (privConst u) ε
 
 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
+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
+  intros _ _ _ _ _ _ p1 p2
   unfold privCompose
-  exact adaptive_compose_prop m₁ (fun _ => m₂) ε₁ ε₂ p1 fun _ => p2
+  apply adaptive_compose_prop p1 (fun _ => p2)
+  trivial
 
 end DPSystem
 
@@ -96,4 +113,30 @@ 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 ℤ
+  /--
+  Relationship between arguments to noise and resulting privacy amount
+  -/
+  noise_priv : (num : ℕ+) → (den : ℕ+) → (priv : NNReal) -> Prop
+  /--
+  Adding noise to a query makes it private
+  -/
+  noise_prop {q : List T → ℤ} {Δ εn εd : ℕ+} {ε : NNReal} :
+    noise_priv εn εd ε ->
+    sensitivity q Δ →
+    dps.prop (noise q Δ εn εd) ε
+
+
+class DPPar (T : Type) extends (DPSystem T) where
+  prop_par {m1 : Mechanism T U} {m2 : Mechanism T V} {ε₁ ε₂ ε : NNReal} :
+    ε = max ε₁ ε₂ -> ∀f, prop m1 ε₁ -> prop m2 ε₂ -> prop (privParCompose m1 m2 f) ε
+
 end SLang

SampCert/DifferentialPrivacy/Approximate/DP.lean

@@ -6,9 +6,6 @@ Authors: Jean-Baptiste Tristan
 import SampCert.SLang
 import SampCert.DifferentialPrivacy.Generic
 import SampCert.DifferentialPrivacy.Neighbours
--- import SampCert.DifferentialPrivacy.Pure.DP
--- import SampCert.DifferentialPrivacy.ZeroConcentrated.DP
--- import SampCert.Util.Log
 
 noncomputable section