Upgrade to SampCert v1.1.0 (#179)

By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).
dafny-lang · Aug 15, 2024 · 8b8a158 · 8b8a158
1 parent 7539092
commit 8b8a158
Show file tree

Hide file tree

Showing 7 changed files with 77 additions and 14 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -6,4 +6,4 @@
 	url = https://github.com/IBM/differential-privacy-library/
 [submodule "SampCert"]
 	path = SampCert
-	url = git@github.com:leanprover/SampCert.git
+	url = https://github.com/leanprover/SampCert
diff --git a/SampCert b/SampCert
diff --git a/docs/dafny/ExamplesRandom.dfy b/docs/dafny/ExamplesRandom.dfy
@@ -105,7 +105,7 @@ module Examples {
     count1 := 0;
     countneg1 := 0;
     for i := 0 to n {
-      var u := r.DiscreteGaussianSample(7, 5);
+      var u := r.DiscreteGaussianSample(7, 5, 7);
       match u {
         case -1 => countneg1 := countneg1 + 1;
         case 0 => count0 := count0 + 1;

diff --git a/src/DafnyVMCTrait.dfy b/src/DafnyVMCTrait.dfy
@@ -174,6 +174,20 @@ module DafnyVMCTrait {
       o := (B,V);
     }
 
+    method {:verify false} DiscreteLaplaceSampleLoop' (num: pos, den: pos)
+      returns (o: (bool,nat))
+      modifies this
+      decreases *
+    {
+      var U := DiscreteLaplaceSampleLoopIn1(num);
+      var v := DiscreteLaplaceSampleLoopIn2(1, 1);
+      var V := v - 1;
+      var X := U + num * V;
+      var Y := X / den;
+      var B := BernoulliSample(1, 2);
+      o := (B,Y);
+    }
+
     method {:verify false} DiscreteLaplaceSample (num: pos, den: pos)
       returns (o: int)
       modifies this
@@ -190,20 +204,50 @@ module DafnyVMCTrait {
       o := Z;
     }
 
-    method {:verify false} DiscreteGaussianSampleLoop (num: pos, den: pos, t: pos)
+    method {:verify false} DiscreteLaplaceSampleOptimized (num: pos, den: pos)
+      returns (o: int)
+      modifies this
+      decreases *
+    {
+      var x := DiscreteLaplaceSampleLoop'(num, den);
+      while ! (! (x.0 == true && x.1 == 0))
+        decreases *
+      {
+        x := DiscreteLaplaceSampleLoop'(num, den);
+      }
+      var r := x;
+      var Z := if r.0 == true then - (r.1) else r.1;
+      o := Z;
+    }
+
+    method {:verify false} DiscreteLaplaceSampleMixed (num: pos, den: pos, mix: nat)
+      returns (o: int)
+      modifies this
+      decreases *
+    {
+      if num <= den * mix {
+        var v := DiscreteLaplaceSample(num, den);
+        o := v;
+      } else {
+        var v := DiscreteLaplaceSampleOptimized(num, den);
+        o := v;
+      }
+    }
+
+    method {:verify false} DiscreteGaussianSampleLoop (num: pos, den: pos, t: pos, mix: nat)
       returns (o: (int,bool))
       modifies this
       decreases *
     {
-      var Y := DiscreteLaplaceSample(t, 1);
-      var y := (if Y < 0 then -Y else Y);
-      var n := ((if y * t * den - num < 0 then -y * t * den - num else y * t * den - num)) * ((if y * t * den - num < 0 then -y * t * den - num else y * t * den - num));
+      var Y := DiscreteLaplaceSampleMixed(t, 1, mix);
+      var y := (if Y < 0 then -(Y) else (Y));
+      var n := ((if y * t * den - num < 0 then -(y * t * den - num) else (y * t * den - num))) * ((if y * t * den - num < 0 then -(y * t * den - num) else (y * t * den - num)));
       var d := 2 * num * (t) * (t) * den;
       var C := BernoulliExpNegSample(n, d);
       o := (Y,C);
     }
 
-    method {:verify false} DiscreteGaussianSample (num: pos, den: pos)
+    method {:verify false} DiscreteGaussianSample (num: pos, den: pos, mix: nat)
       returns (o: int)
       modifies this
       decreases *
@@ -212,11 +256,11 @@ module DafnyVMCTrait {
       var t := ti + 1;
       var num := (num) * (num);
       var den := (den) * (den);
-      var x := DiscreteGaussianSampleLoop(num, den, t);
+      var x := DiscreteGaussianSampleLoop(num, den, t, mix);
       while ! (x.1)
         decreases *
       {
-        x := DiscreteGaussianSampleLoop(num, den, t);
+        x := DiscreteGaussianSampleLoop(num, den, t, mix);
       }
       var r := x;
       o := r.0;

diff --git a/src/interop/java/Full/Random.java b/src/interop/java/Full/Random.java
@@ -78,12 +78,28 @@ public boolean BernoulliExpNegSample(java.math.BigInteger num, java.math.BigInte
     return DafnyVMCTrait._Companion_RandomTrait.BernoulliExpNegSample(this, num, den);
   }
 
-  public dafny.Tuple2<java.math.BigInteger, Boolean> DiscreteGaussianSampleLoop(java.math.BigInteger num, java.math.BigInteger den, java.math.BigInteger t) {
-    return DafnyVMCTrait._Companion_RandomTrait.DiscreteGaussianSampleLoop(this, num, den, t);
+  public dafny.Tuple2<java.math.BigInteger, Boolean> DiscreteGaussianSampleLoop(java.math.BigInteger num, java.math.BigInteger den, java.math.BigInteger t, java.math.BigInteger mix) {
+    return DafnyVMCTrait._Companion_RandomTrait.DiscreteGaussianSampleLoop(this, num, den, t, mix);
+  }
+
+  public java.math.BigInteger DiscreteGaussianSample(java.math.BigInteger num, java.math.BigInteger den, java.math.BigInteger mix) {
+    return DafnyVMCTrait._Companion_RandomTrait.DiscreteGaussianSample(this, num, den, mix);
   }
 
   public java.math.BigInteger DiscreteGaussianSample(java.math.BigInteger num, java.math.BigInteger den) {
-    return DafnyVMCTrait._Companion_RandomTrait.DiscreteGaussianSample(this, num, den);
+    return DafnyVMCTrait._Companion_RandomTrait.DiscreteGaussianSample(this, num, den, BigInteger.valueOf(7));
+  }
+
+  public dafny.Tuple2<Boolean, java.math.BigInteger> DiscreteLaplaceSampleLoop_k(java.math.BigInteger num, java.math.BigInteger den) {
+    return DafnyVMCTrait._Companion_RandomTrait.DiscreteLaplaceSampleLoop_k(this, num, den);
+  }
+
+  public java.math.BigInteger DiscreteLaplaceSampleMixed(java.math.BigInteger num, java.math.BigInteger den, java.math.BigInteger mix) {
+    return DafnyVMCTrait._Companion_RandomTrait.DiscreteLaplaceSampleMixed(this, num, den, mix);
+  }
+
+  public java.math.BigInteger DiscreteLaplaceSampleOptimized(java.math.BigInteger num, java.math.BigInteger den) {
+    return DafnyVMCTrait._Companion_RandomTrait.DiscreteLaplaceSampleOptimized(this, num, den);
   }
 
   public dafny.Tuple2<java.math.BigInteger, Boolean> DiscreteLaplaceSampleLoopIn1Aux(java.math.BigInteger t) {

diff --git a/src/interop/py/Full/Random.py b/src/interop/py/Full/Random.py
@@ -15,4 +15,7 @@ def Shuffle(self, xs):
     a = ArrayFromList(xs)
     DafnyVMCPart.Random.Shuffle(self, a)
     return list(a)
+
+  def DiscreteGaussianSample(self, num, denom):
+     return DafnyVMCPart.Random.DiscreteGaussianSample(self, num, denom, 7)
 
diff --git a/tests/Tests.dfy b/tests/Tests.dfy
@@ -229,7 +229,7 @@ module Tests {
     for i := 0 to n
       invariant -2 in counts && -1 in counts && 0 in counts && 1 in counts && 2 in counts
     {
-      var u := r.DiscreteGaussianSample(7, 5);
+      var u := r.DiscreteGaussianSample(7, 5, 7);
       sum := sum + u;
       if u !in counts {
         counts := counts[ u := 1 ];