Enable Custom Extern Uniform (#164)

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).

build/java/run_samplers.sh

@@ -1,3 +1,4 @@
 #1/bin/bash
 
-java -classpath build/java/DafnyVMC.jar docs/java/TestSamplers.java
+java -classpath build/java/DafnyVMC.jar docs/java/TestSamplers.java
+java -classpath build/java/DafnyVMC.jar docs/java/CustomTestSamplers.java

build/java/run_shuffling.sh

@@ -1,3 +1,4 @@
 #1/bin/bash
 
-java -classpath build/java/DafnyVMC.jar docs/java/TestShuffling.java
+java -classpath build/java/DafnyVMC.jar docs/java/TestShuffling.java
+java -classpath build/java/DafnyVMC.jar docs/java/CustomTestShuffling.java

build/py/run_samplers.sh

@@ -1,3 +1,4 @@
 #1/bin/bash
 
-PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestSamplers.py
+PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestSamplers.py 
+PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/CustomTestSamplers.py

build/py/run_shuffling.sh

@@ -1,3 +1,4 @@
 #1/bin/bash
 
-PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestShuffling.py
+PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestShuffling.py 
+PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/CustomTestShuffling.py

docs/java/CustomTestSamplers.java

@@ -0,0 +1,116 @@
+import java.security.SecureRandom;
+import java.math.BigInteger;
+import java.util.Arrays;
+
+import DafnyVMC.Random;
+
+class CustomTestSamplers {
+
+    public static void main(String[] args) {
+
+            /* STANDARD RNG */
+            System.out.println("\n STANDARD RNG TESTS WITH CUSTOM UNIFORM\n");
+
+            DafnyVMC.CustomRandom r = new DafnyVMC.CustomRandom();
+
+            for (int a = 1; a < 1000; a++) {
+                BigInteger i = BigInteger.valueOf(a);
+
+                System.out.println("Testing Uniform(" + a + ")");
+                System.out.println(r.UniformSample(i));
+
+                for (int b = 1; b <= 1000; b++) {
+                    BigInteger j = BigInteger.valueOf(b);
+
+                    System.out.println("Testing Bernoulli(" + a + "/" + b + ")");
+                    System.out.println(r.BernoulliSample(i, j));
+
+                    System.out.println("Testing BernoulliExpNeg(" + a + "/" + b + ")");
+                    System.out.println(r.BernoulliExpNegSample(i, j));
+
+                    System.out.println("Testing DiscreteGaussian(" + a + "/" + b + ")");
+                    System.out.println(r.DiscreteGaussianSample(i, j));
+
+                    System.out.println("Testing DiscreteLaPlace(" + a + "/" + b + ")");
+                    System.out.println(r.DiscreteLaplaceSample(i, j));
+                }
+            }
+
+            // Edge cases
+
+            BigInteger k = BigInteger.valueOf(1000000);
+            BigInteger l = BigInteger.valueOf(1);
+
+            System.out.println("Testing Bernoulli(1000000, 1)");
+            System.out.println(r.BernoulliSample(k, l));
+            System.out.println("Testing Bernoulli(1, 1000000)");
+            System.out.println(r.BernoulliSample(l, k));
+
+            System.out.println("Testing BernoulliExpNeg(1000000, 1)");
+            System.out.println(r.BernoulliExpNegSample(k, l));
+            System.out.println("Testing BernoulliExpNeg(1, 1000000)");
+            System.out.println(r.BernoulliExpNegSample(l, k));
+
+            System.out.println("Testing DiscreteGaussianSample(1000000, 1)");
+            System.out.println(r.DiscreteGaussianSample(k, l));
+            System.out.println("Testing DiscreteGaussianSample(1, 1000000)");
+            System.out.println(r.DiscreteGaussianSample(l, k));
+
+            System.out.println("Testing DiscreteLaplace(1000000, 1)");
+            System.out.println(r.DiscreteLaplaceSample(k, l));
+            System.out.println("Testing DiscreteLaplace(1, 1000000)");
+            System.out.println(r.DiscreteLaplaceSample(l, k));
+
+            /* CUSTOM RNG */
+            System.out.println("\nCUSTOM RNG TESTS WITH CUSTOM UNIFORM\n");
+
+            SecureRandom rng = new SecureRandom();
+            DafnyVMC.CustomRandom t = new DafnyVMC.CustomRandom(() -> rng);
+
+            for (int a = 1; a < 1000; a++) {
+                BigInteger i = BigInteger.valueOf(a);
+                System.out.println("Testing Uniform(" + a + ")");
+                System.out.println(t.UniformSample(i));
+
+                for (int b = 1; b <= 1000; b++) {
+                    BigInteger j = BigInteger.valueOf(b);
+                    System.out.println("Testing Bernoulli(" + a + "/" + b + ")");
+                    System.out.println(t.BernoulliSample(i, j));
+
+                    System.out.println("Testing BernoulliExpNeg(" + a + "/" + b + ")");
+                    System.out.println(t.BernoulliExpNegSample(i, j));
+
+                    System.out.println("Testing DiscreteGaussian(" + a + "/" + b + ")");
+                    System.out.println(t.DiscreteGaussianSample(i, j));
+
+                    System.out.println("Testing DiscreteLaPlace(" + a + "/" + b + ")");
+                    System.out.println(t.DiscreteLaplaceSample(i, j));
+                }
+            }
+
+
+            // Edge cases
+
+            System.out.println("Testing Bernoulli(1000000, 1)");
+            System.out.println(t.BernoulliSample(k, l));
+            System.out.println("Testing Bernoulli(1, 1000000)");
+            System.out.println(t.BernoulliSample(l, k));
+
+            System.out.println("Testing BernoulliExpNeg(1000000, 1)");
+            System.out.println(t.BernoulliExpNegSample(k, l));
+            System.out.println("Testing BernoulliExpNeg(1, 1000000)");
+            System.out.println(t.BernoulliExpNegSample(l, k));
+
+            System.out.println("Testing DiscreteGaussianSample(1000000, 1)");
+            System.out.println(t.DiscreteGaussianSample(k, l));
+            System.out.println("Testing DiscreteGaussianSample(1, 1000000)");
+            System.out.println(t.DiscreteGaussianSample(l, k));
+
+            System.out.println("Testing DiscreteLaplace(1000000, 1)");
+            System.out.println(t.DiscreteLaplaceSample(k, l));
+            System.out.println("Testing DiscreteLaplace(1, 1000000)");
+            System.out.println(t.DiscreteLaplaceSample(l, k));
+
+
+    }
+}

docs/java/CustomTestShuffling.java

@@ -0,0 +1,85 @@
+import java.security.SecureRandom;
+import java.math.BigInteger;
+import java.util.Arrays;
+
+import DafnyVMC.Random;
+
+class CustomTestShuffling {
+    public static void main(String[] args) {
+        BigInteger[] arr1 = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)};
+        int[] arr2 = {0, 1, 2};
+        String[] arr3 = {"aa", "bb", "cc"};
+        char[] arr4 = {'a', 'b', 'c'};
+        boolean[] arr5 = {true, false, false, true};
+        long[] arr6 = {111111L, 333333L, 999999L};
+        short[] arr7 = {-3, 0, 3};
+
+
+        /* STANDARD RNG */
+        System.out.println("\nSTANDARD RNG TESTS WITH CUSTOM UNIFORM\n");
+
+        DafnyVMC.CustomRandom r = new DafnyVMC.CustomRandom();
+
+        System.out.println("Example of Fisher-Yates: BigInteger");
+        r.Shuffle(arr1);
+        System.out.println(Arrays.toString(arr1));
+
+        System.out.println("Example of Fisher-Yates: int");
+        r.Shuffle(arr2);
+        System.out.println(Arrays.toString(arr2));
+
+        System.out.println("Example of Fisher-Yates: String");
+        r.Shuffle(arr3);
+        System.out.println(Arrays.toString(arr3));
+
+        System.out.println("Example of Fisher-Yates: char");
+        r.Shuffle(arr4);
+        System.out.println(Arrays.toString(arr4));
+
+        System.out.println("Example of Fisher-Yates: boolean");
+        r.Shuffle(arr5);
+        System.out.println(Arrays.toString(arr5));
+
+        System.out.println("Example of Fisher-Yates: long");
+        r.Shuffle(arr6);
+        System.out.println(Arrays.toString(arr6));
+
+        System.out.println("Example of Fisher-Yates: short");
+        r.Shuffle(arr7);
+        System.out.println(Arrays.toString(arr7));
+
+        /* CUSTOM RNG */
+        System.out.println("\nCUSTOM RNG TESTS WITH CUSTOM UNIFORM\n");
+
+        SecureRandom rng = new SecureRandom();
+        DafnyVMC.CustomRandom t = new DafnyVMC.CustomRandom(() -> rng);
+
+        System.out.println("Example of Fisher-Yates: BigInteger");
+        t.Shuffle(arr1);
+        System.out.println(Arrays.toString(arr1));
+
+        System.out.println("Example of Fisher-Yates: int");
+        t.Shuffle(arr2);
+        System.out.println(Arrays.toString(arr2));
+
+        System.out.println("Example of Fisher-Yates: String");
+        t.Shuffle(arr3);
+        System.out.println(Arrays.toString(arr3));
+
+        System.out.println("Example of Fisher-Yates: char");
+        t.Shuffle(arr4);
+        System.out.println(Arrays.toString(arr4));
+
+        System.out.println("Example of Fisher-Yates: boolean");
+        t.Shuffle(arr5);
+        System.out.println(Arrays.toString(arr5));
+
+        System.out.println("Example of Fisher-Yates: long");
+        t.Shuffle(arr6);
+        System.out.println(Arrays.toString(arr6));
+
+        System.out.println("Example of Fisher-Yates: short");
+        t.Shuffle(arr7);
+        System.out.println(Arrays.toString(arr7));
+    }
+}

docs/py/CustomTestSamplers.py

@@ -0,0 +1,49 @@
+import DafnyVMC
+
+def main():
+
+    # STANDARD RNG
+    print("\nSTANDARD RNG TESTS WITH CUSTOM UNIFORM \n")
+
+    r = DafnyVMC.CustomRandom()
+
+    for i in range(1, 1000): 
+        print("Testing Uniform("+str(i)+")")
+        print(r.UniformSample(i))
+
+        for j in range(1, 1000):
+            print("Testing Bernoulli("+str(i)+"/"+str(j)+")\n")
+            print(r.BernoulliSample(i, j), end="\n")
+
+            print("Testing BernoulliExpNeg("+str(i)+"/"+str(j)+")\n")
+            print(r.BernoulliExpNegSample(i, j), end="\n")
+
+            print("Testing DiscreteGaussian("+str(i)+"/"+str(j)+")\n")
+            print(r.DiscreteGaussianSample(i, j), end="\n")
+
+            print("Testing DiscreteLaPlace("+str(i)+"/"+str(j)+")\n")
+            print(r.DiscreteLaplaceSample(i, j), end="\n")
+
+        # Edge cases    
+        print("Testing Bernoulli(1000000, 1)\n")
+        print(r.BernoulliSample(1000000, 1), end="\n")
+        print("Testing Bernoulli(1, 1000000)\n")
+        print(r.BernoulliSample(1, 1000000), end="\n")
+
+        print("Testing BernoulliExpNeg(1000000, 1)\n")
+        print(r.BernoulliExpNegSample(1000000, 1), end="\n")
+        print("Testing BernoulliExpNeg(1, 1000000)\n")
+        print(r.BernoulliExpNegSample(1, 1000000), end="\n")
+
+        print("Testing DiscreteGaussianSample(1000000, 1)\n")
+        print(r.DiscreteGaussianSample(1000000, 1), end="\n")
+        print("Testing DiscreteGaussianSample(1, 1000000)\n")
+        print(r.DiscreteGaussianSample(1, 1000000), end="\n")
+
+        print("Testing DiscreteLaplace(1000000, 1)\n")
+        print(r.DiscreteLaplaceSample(1000000, 1), end="\n")
+        print("Testing DiscreteLaplace(1, 1000000)\n")
+        print(r.DiscreteLaplaceSample(1, 1000000), end="\n")
+
+if __name__ == "__main__":
+    main()

docs/py/CustomTestShuffling.py

@@ -0,0 +1,36 @@
+import DafnyVMC
+
+def main():
+    arr1 = [0, 1, 2]
+    arr2 = [float(0), float(1), float(2)]
+    arr3 = ["aa", "bb", "cc"]
+    arr4 = ['a', 'b', 'c']
+    arr5 = [True, False, False, True]
+
+    # STANDARD RNG
+    print("\nSTANDARD RNG TESTS WITH CUSTOM UNIFORM\n")
+
+    r = DafnyVMC.CustomRandom()
+
+    print("Example of Fisher-Yates: int")
+    arr1 = r.Shuffle(arr1)
+    print(arr1)
+
+    print("Example of Fisher-Yates: float")
+    arr2 = r.Shuffle(arr2)
+    print(arr2)
+
+    print("Example of Fisher-Yates: str")
+    arr3 = r.Shuffle(arr3)
+    print(arr3)
+
+    print("Example of Fisher-Yates: char/str")
+    arr4 = r.Shuffle(arr4)
+    print(arr4)
+
+    print("Example of Fisher-Yates: boolean")
+    arr5 = r.Shuffle(arr5)
+    print(arr5)
+
+if __name__ == "__main__":
+    main()

scripts/build.sh

@@ -14,4 +14,9 @@ then
   exit 1
 fi
 
-$DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG -o build/$TARGET_LANG/DafnyVMC dfyconfig.toml --no-verify
+if [ "$TARGET_LANG" = "java" ]
+then
+  $DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Full/CustomRandom.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG -o build/$TARGET_LANG/DafnyVMC dfyconfig.toml --no-verify
+else
+  $DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG -o build/$TARGET_LANG/DafnyVMC dfyconfig.toml --no-verify
+fi

src/DafnyVMCTrait.dfy

@@ -7,7 +7,7 @@ module DafnyVMCTrait {
 
   import opened Pos
 
-  trait {:termination false} RandomTrait extends  UniformPowerOfTwo.Interface.Trait, FisherYates.Implementation.Trait {
+  trait {:termination false} RandomTrait extends UniformPowerOfTwo.Interface.Trait, FisherYates.Implementation.Trait {
 
     method {:verify false} UniformSample (n: pos)
       returns (o: nat)

src/interop/java/Full/CustomRandom.java

@@ -0,0 +1,38 @@
+package DafnyVMC;
+
+import dafny.TypeDescriptor;
+import java.math.BigInteger;
+import java.security.SecureRandom;
+import java.util.function.Supplier;
+
+public class CustomRandom extends Random {
+  public CustomRandom() {
+    this.rng = ThreadLocal.withInitial(CustomRandom::createSecureRandom);
+  }
+
+  public CustomRandom(Supplier<SecureRandom> supplier) {
+    this.rng = ThreadLocal.withInitial(supplier);
+  }
+
+  private static final SecureRandom createSecureRandom() {
+    final SecureRandom rng = new SecureRandom();
+    // Required for proper initialization
+    rng.nextBoolean(); 
+    return rng;
+  }
+
+  @Override
+  public java.math.BigInteger UniformSample(java.math.BigInteger n) {
+    if (n.compareTo(BigInteger.ONE) < 0) {
+      throw new IllegalArgumentException("n must be positive");
+    }
+
+    BigInteger sampleValue;
+    do {
+      sampleValue = UniformPowerOfTwoSample(n);
+    } while (sampleValue.compareTo(n) >= 0);
+
+    return sampleValue;    
+  }
+
+}

src/interop/py/Full/Random.py

@@ -15,3 +15,7 @@ def Shuffle(self, xs):
     a = ArrayFromList(xs)
     DafnyVMCPart.Random.Shuffle(self, a)
     return list(a)
+
+class CustomRandom(Random):
+  def UniformSample(self, n):
+    return secrets.randbelow(n)