Merge pull request #5 from leanprover/ConcentratedBound

New package for VMC

FastExtract.lean

@@ -5,3 +5,6 @@ Authors: Jean-Baptiste Tristan
 -/
 
 import SampCert.Extraction
+import SampCert.Extractor.Print
+
+#print_dafny_exports

SampCert/Extraction.lean

@@ -6,7 +6,6 @@ Authors: Jean-Baptiste Tristan
 
 import SampCert.Extractor.Export
 import SampCert.Extractor.Align
-import SampCert.Extractor.Print
 import SampCert.Samplers.Uniform.Code
 import SampCert.Samplers.Bernoulli.Code
 import SampCert.Samplers.BernoulliNegativeExponential.Code
@@ -30,5 +29,3 @@ attribute [export_dafny] DiscreteLaplaceSampleLoop
 attribute [export_dafny] DiscreteLaplaceSample
 attribute [export_dafny] DiscreteGaussianSampleLoop
 attribute [export_dafny] DiscreteGaussianSample
-
-#print_dafny_exports

SampCert/Extractor/VMC.lean

@@ -0,0 +1,40 @@
+/-
+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
+-/
+
+import Lean
+import SampCert.Extractor.Extension
+
+open System IO.FS
+
+namespace Lean.ToDafny
+
+def destination : String := "../src/DafnyVMCTrait.dfy"
+
+def writeLn (ln : String) : IO Unit := do
+  let h ← Handle.mk destination Mode.append
+  h.putStr "\n"
+  h.putStr ln
+  h.putStr "\n"
+
+elab "#print_vmc_exports" : command => do
+  writeFile destination ""
+  writeLn "module DafnyVMCTrait {"
+  writeLn "  import UniformPowerOfTwo"
+  writeLn "  import FisherYates"
+  writeLn "  import opened Pos"
+  writeLn "  import Uniform"
+
+  writeLn "  trait {:termination false} RandomTrait extends  UniformPowerOfTwo.Interface.Trait, FisherYates.Implementation.Trait, Uniform.Interface.Trait {\n"
+
+  let { decls, .. } := extension.getState (← getEnv)
+  for decl in decls.reverse do
+    --IO.println decl
+    let h ← Handle.mk destination Mode.append
+    h.putStr decl
+  writeLn "}"
+  writeLn "}"
+
+end Lean.ToDafny

VMC.lean

@@ -0,0 +1,16 @@
+/-
+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
+-/
+
+import SampCert.Samplers.Uniform.Basic
+import SampCert.Samplers.Bernoulli.Basic
+import SampCert.Samplers.BernoulliNegativeExponential.Basic
+import SampCert.Samplers.Laplace.Basic
+import SampCert.Samplers.Gaussian.Basic
+import SampCert.DiffPrivacy.ConcentratedBound
+import SampCert.Extraction
+import SampCert.Extractor.VMC
+
+#print_vmc_exports

lakefile.lean

@@ -11,3 +11,5 @@ require mathlib from git
 lean_lib «SampCert» where
 
 lean_lib «FastExtract» where
+
+lean_lib «VMC» where