Fix build

SampCert.lean

@@ -8,6 +8,7 @@ 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.Approximate.DP
 import SampCert.Samplers.Gaussian.Properties
 import Init.Data.UInt.Lemmas

SampCert/DifferentialPrivacy/Queries/UnboundedMax/Basic.lean

@@ -1,10 +1,13 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jean-Baptiste Tristan
+Authors: Markus de Medeiros
 -/
 
 -- import SampCert.DifferentialPrivacy.Queries.UnboundedMax.Code
--- import SampCert.DifferentialPrivacy.Queries.UnboundedMax.Properties
+
+import SampCert.DifferentialPrivacy.Queries.UnboundedMax.Properties
+import SampCert.DifferentialPrivacy.Queries.UnboundedMax.Privacy
+
 -- import SampCert.DifferentialPrivacy.Queries.UnboundedMax.Pure
 -- import SampCert.DifferentialPrivacy.Queries.UnboundedMax.ZeroConcentrated

SampCert/DifferentialPrivacy/Queries/UnboundedMax/Privacy.lean

@@ -204,8 +204,8 @@ lemma DS0 (H : Neighbour L1 L2) : ((exactDiffSum 0 L1) : ℝ) - (exactDiffSum 0
     sorry
 
 
-
-lemma sv8_privMax_pmf_DP (ε : NNReal) (Hε : ε = ε₁ / ε₂) : PureDPSystem.prop (@sv9_privMax_pmf PureDPSystem ε₁ ε₂) ε := by
+lemma sv8_privMax_pmf_DP (ε : NNReal) (Hε : ε = ε₁ / ε₂) :
+    PureDPSystem.prop (@sv9_privMax_pmf PureDPSystem laplace_pureDPSystem ε₁ ε₂) ε := by
   -- Unfold DP definitions
   simp [DPSystem.prop]
   apply singleton_to_event
@@ -264,7 +264,7 @@ lemma sv8_privMax_pmf_DP (ε : NNReal) (Hε : ε = ε₁ / ε₂) : PureDPSystem
       simp [cov_τ]
       rw [mul_assoc]
       apply ENNReal.mul_left_mono
-      simp [privNoiseGuess, privNoiseZero, DPSystem.noise, privNoisedQueryPure]
+      simp [privNoiseGuess, privNoiseZero, DPNoise.noise, privNoisedQueryPure]
       apply le_trans
       · apply laplace_inequality_sub
       rw  [mul_comm]
@@ -470,8 +470,7 @@ lemma sv8_privMax_pmf_DP (ε : NNReal) (Hε : ε = ε₁ / ε₂) : PureDPSystem
         have _ := @exactDiffSum_nonpos (point + 1) [n2]
         linarith
 
-    simp [privNoiseThresh, privNoiseGuess,
-         privNoiseZero, DPSystem.noise, privNoisedQueryPure]
+    simp [privNoiseThresh, privNoiseGuess, privNoiseZero, DPNoise.noise, privNoisedQueryPure]
 
     -- Apply the Laplace inequalities
     apply le_trans