diff --git a/SampCert.lean b/SampCert.lean
index 55d9f9b0..1e1285dc 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
 
 /-
@@ -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
@@ -40,8 +40,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
 
diff --git a/SampCert/DifferentialPrivacy/Abstract.lean b/SampCert/DifferentialPrivacy/Abstract.lean
index 84d7fb13..7fc52d73 100644
--- a/SampCert/DifferentialPrivacy/Abstract.lean
+++ b/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
-  -/
-  prop_mono {m : Mechanism T Z} {ε₁ ε₂: NNReal} (Hε : ε₁ ≤ ε₂) (H : prop m ε₁) : prop m ε₂
-  /--
-  A noise mechanism (eg. Laplace, Discrete Gaussian, etc)
-  Paramaterized by a query, sensitivity, and a (rational) security paramater.
+  For any ε', this definition of DP implies (ε', δ)-approximate-DP for all δ
   -/
-  noise : Query T ℤ → (sensitivity : ℕ+) → (num : ℕ+) → (den : ℕ+) → Mechanism T ℤ
+  prop_adp [DiscProbSpace Z] {m : Mechanism T Z} : ∀ (δ : NNReal) (_ : 0 < δ) (ε' : NNReal),
+    (prop m (of_app_dp δ ε') -> ApproximateDP m ε' δ)
   /--
-  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,38 @@ 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) ε
+
+
+-- /-
+-- 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/Generic.lean b/SampCert/DifferentialPrivacy/Generic.lean
index be8e333c..8c46773e 100644
--- a/SampCert/DifferentialPrivacy/Generic.lean
+++ b/SampCert/DifferentialPrivacy/Generic.lean
@@ -13,25 +13,53 @@ import SampCert.Foundations.Basic
 This file defines an abstract system of differentially private operators.
 -/
 
-noncomputable section
-
-open Classical Nat Int Real ENNReal
 
 namespace SLang
 
+
 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) : PMF (U × V) := do
+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)
 
-lemma compose_sum_rw_adaptive (nq1 : List T → PMF U) (nq2 : U -> List T → PMF V) (u : U) (v : V) (l : List T) :
+/--
+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
+
+
+
+
+noncomputable section
+
+open Classical Nat Int Real ENNReal
+
+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 → 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
@@ -70,24 +98,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]
@@ -218,4 +230,6 @@ lemma condition_to_subset (f : U → V) (g : U → ENNReal) (x : V) :
     simp
   rw [B]
 
+end
+
 end SLang
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/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/Mechanism/Properties.lean b/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean
index addf1b2f..950208a4 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) (HN : laplace_pureDP_noise_priv ε₁ ε₂ ε) (bounded_sensitivity : sensitivity query Δ) :
+    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/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/Pure/System.lean b/SampCert/DifferentialPrivacy/Pure/System.lean
index 00e16cd0..c6a7a786 100644
--- a/SampCert/DifferentialPrivacy/Pure/System.lean
+++ b/SampCert/DifferentialPrivacy/Pure/System.lean
@@ -21,14 +21,22 @@ 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
+  of_app_dp := pure_of_adp
   prop_adp := pure_ApproximateDP
   prop_mono := PureDP_mono
+  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_prop := privNoisedQueryPure_DP
-  adaptive_compose_prop := PureDP_ComposeAdaptive'
-  postprocess_prop := PureDP_PostProcess
-  const_prop := PureDP_privConst
+  noise_priv := laplace_pureDP_noise_priv
+  noise_prop := by
+    intros; apply privNoisedQueryPure_DP <;> trivial
 
 end SLang
diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean
index 2cf226d8..dc94cd09 100644
--- a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean
+++ b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean
@@ -13,16 +13,15 @@ import SampCert.DifferentialPrivacy.Queries.BoundedSum.Code
 This file defines a differentially private bounded mean query.
 -/
 
-noncomputable section
-
 namespace SLang
 
 variable [dps : DPSystem ℕ]
+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/BoundedMean/Properties.lean b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean
index 775a6435..abed30ab 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
@@ -30,14 +31,20 @@ lemma budget_split (ε₁ ε₂ : ℕ+) :
 /--
 DP bound for noised mean.
 -/
-theorem privNoisedBoundedMean_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) :
-  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
-  rw [budget_split]
-  apply dps.compose_prop
+  apply dps.compose_prop ?SC1
   · apply privNoisedBoundedSum_DP
+    apply HP_half
   · apply privNoisedCount_DP
+    apply HP_half
+
+  case SC1 =>
+    ring_nf
+    simp [div_mul]
 
 end SLang
diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean b/SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean
index 12a37d7a..1396256d 100644
--- a/SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean
+++ b/SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean
@@ -14,11 +14,10 @@ import Init.Data.Int.Order
 This file defines a differentially private bounded sum query.
 -/
 
-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 +29,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..3e14c7a4 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.
@@ -84,9 +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
-  apply dps.noise_prop
+theorem privNoisedBoundedSum_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) (ε : NNReal) (HP : dpn.noise_priv ε₁ ε₂ ε) :
+    dps.prop (privNoisedBoundedSum U ε₁ ε₂) ε := by
+  apply dpn.noise_prop HP
   apply exactBoundedSum_sensitivity
 
 end SLang
diff --git a/SampCert/DifferentialPrivacy/Queries/Count/Code.lean b/SampCert/DifferentialPrivacy/Queries/Count/Code.lean
index a94db31e..f9bf360f 100644
--- a/SampCert/DifferentialPrivacy/Queries/Count/Code.lean
+++ b/SampCert/DifferentialPrivacy/Queries/Count/Code.lean
@@ -11,12 +11,11 @@ import SampCert.DifferentialPrivacy.Abstract
 This file defines a differentially private noising of an exact length query.
 -/
 
-noncomputable section
-
 namespace SLang
 
 variable {T : Type}
 variable [dps : DPSystem T]
+variable [dpn : DPNoise dps]
 
 /--
 Query to count the size of the input list.
@@ -27,6 +26,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..c961280f 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
@@ -44,9 +45,10 @@ theorem exactCount_1_sensitive :
 The noised counting query satisfies DP property
 -/
 @[simp]
-theorem privNoisedCount_DP (ε₁ ε₂ : ℕ+) :
-  dps.prop (privNoisedCount ε₁ ε₂) ((ε₁ : NNReal) / ε₂) := by
-  apply dps.noise_prop
+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
diff --git a/SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean b/SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean
index 553cdedc..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
@@ -87,6 +85,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 +97,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..9eeffd35 100644
--- a/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean
+++ b/SampCert/DifferentialPrivacy/Queries/Histogram/Properties.lean
@@ -21,139 +21,71 @@ namespace SLang
 
 variable {T : Type}
 variable [dps : DPSystem T]
+variable [dpn : DPNoise dps]
 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)
+variable (ε₁ ε₂ : ℕ+) (ε : NNReal) (HN_bin : dpn.noise_priv ε₁ (ε₂ * numBins) (ε / numBins))
 
 /-
 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
 -/
-lemma privNoisedBinCount_DP (ε₁ ε₂ : ℕ+) (b : Fin numBins) :
-  dps.prop (privNoisedBinCount numBins B ε₁ ε₂ b) (ε₁ / ((ε₂ * numBins : PNat))) := by
+lemma privNoisedBinCount_DP  (b : Fin numBins) :
+  dps.prop (privNoisedBinCount numBins B ε₁ ε₂ b) (ε / numBins) := by
   unfold privNoisedBinCount
-  apply dps.noise_prop
+  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 (n : ℕ) (Hn : n < 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]
-    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]
-  · 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)
+    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 arithmetic => simp; ring_nf
 
 /--
 DP bound for a noised histogram
 -/
-lemma privNoisedHistogram_DP (ε₁ ε₂ : ℕ+) :
-  dps.prop (privNoisedHistogram numBins B ε₁ ε₂) (ε₁ / ε₂) := by
+lemma privNoisedHistogram_DP :
+  dps.prop (privNoisedHistogram numBins B ε₁ ε₂) ε := by
   unfold privNoisedHistogram
   apply (DPSystem_prop_ext _ ?HEq ?Hdp)
-  case Hdp => apply privNoisedHistogramAux_DP
-  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'
-
+  case Hdp => apply privNoisedHistogramAux_DP; apply HN_bin
+  case HEq => simp [predBins, mul_div_left_comm]
 
 /--
 DP bound for the thresholding maximum
 -/
-lemma privMaxBinAboveThreshold_DP (ε₁ ε₂ : ℕ+) (τ : ℤ) :
-  dps.prop (privMaxBinAboveThreshold numBins B ε₁ ε₂ τ) (ε₁ / ε₂) := by
-  rw [privMaxBinAboveThreshold]
+lemma privMaxBinAboveThreshold_DP (τ : ℤ) :
+  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/Code.lean b/SampCert/DifferentialPrivacy/Queries/HistogramMean/Code.lean
index 4a91528c..51546d49 100644
--- a/SampCert/DifferentialPrivacy/Queries/HistogramMean/Code.lean
+++ b/SampCert/DifferentialPrivacy/Queries/HistogramMean/Code.lean
@@ -20,9 +20,8 @@ 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 : ℕ+)
 variable (B : Bins ℕ numBins)
 
@@ -44,7 +43,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..6d15c8fd 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 -> ℕ+)
@@ -56,23 +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 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
-    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
+    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
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean
index ac102d93..7358ef78 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean
@@ -131,50 +131,21 @@ 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 (ε₂ * α) :=
+    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 [add_mul]
     rw [ENNReal.ofReal_add ?G1 ?G2]
     case G1 =>
-      simp
-      apply mul_nonneg
-      · apply mul_nonneg
-        · simp
-        · exact sq_nonneg ε₁
-      · linarith
+      apply Right.mul_nonneg Hε₁
+      linarith
     case G2 =>
-      simp
-      apply mul_nonneg
-      · apply mul_nonneg
-        · simp
-        · exact sq_nonneg ε₂
-      · linarith
+      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 f51ad1aa..5edf10ea 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,24 +63,22 @@ 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 (@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
-      · apply mul_nonneg
-        · simp
-        · simp
+      · exact NNReal.zero_le_coe
+      · linarith
+    · apply mul_le_mul_of_nonneg_right
+      · exact H
       · 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
 -/
 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
   have Hε : 0 ≤ ε := by exact le_of_lt Hε_pos
   intro δ Hδ0 Hδ1
@@ -634,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
@@ -649,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ε
@@ -668,70 +665,81 @@ 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 (-D δ + discrim (OfNat.ofNat 2)⁻¹ (D δ) (-↑ε') ^ (2 : ℝ)⁻¹)
+
+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) * ((zCDP_of_adp_def.ε ε' δ)^2)
+
 /--
 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
-  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δ0 ε' 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) HB HN δ Hδ
+  simp at Hδ1
+  unfold ApproximateDP
+
+  unfold zCDP_of_adp at H
+  rcases H with ⟨ H1, H2 ⟩
+  have X := ApproximateDP_of_zCDP m (zCDP_of_adp_def.ε ε' δ) ?G1 H2 H1 δ Hδ0
+  case G1 => exact NNReal.zero_le_coe
+  rw [zCDP_of_adp_def.eqε ε' δ Hδ0 Hδ1]
+  unfold zCDP_of_adp_def.D
+  simp_all
 
-  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
 
 
 /--
@@ -1872,7 +1880,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
+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)
@@ -2298,7 +2306,7 @@ 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
\ 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..8838f8db 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean
@@ -23,7 +23,7 @@ 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₂)
@@ -221,12 +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 Δ ε₁ ε₂
   · apply privNoisedQuery_zCDPBound
     exact bounded_sensitivity
 
-
 end SLang
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
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean
index de28f44d..7849dad5 100644
--- a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean
+++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean
@@ -16,21 +16,62 @@ 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 }
 
 /--
-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
-  prop_adp := zCDP_ApproximateDP
-  prop_mono := zCDP_mono
+  of_app_dp := zCDP_of_adp
+  prop_adp := by
+    intros; apply zCDP_ApproximateDP <;> assumption
+  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 (T : Type) : DPNoise (@zCDPSystem T) where
   noise := privNoisedQuery
-  noise_prop := privNoisedQuery_zCDP
-  adaptive_compose_prop := privComposeAdaptive_zCDP
-  postprocess_prop := privPostProcess_zCDP
-  const_prop := privConst_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 (T : Type) : DPNoise (@zCDPSystem T) where
+--   noise := sorry
+--   noise_priv := sorry
+--   noise_prop := sorry -- privNoisedQuery_zCDP
+
 
 end SLang
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
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