Enable Custom Uniform Sampling for Shuffling

build/java/run.sh

@@ -1,3 +1,3 @@
 #1/bin/bash
-
-java -classpath build/java/DafnyVMC.jar docs/java/BuildTest.java
+javac -classpath "build/java/DafnyVMC.jar:docs/java/" docs/java/CustomFisherYates.java docs/java/CustomFisherYatesFaulty.java
+java -classpath "build/java/DafnyVMC.jar:docs/java/" docs/java/BuildTest.java 

docs/java/BuildTest.java

@@ -1,25 +1,35 @@
-import java.security.SecureRandom;
 import java.math.BigInteger;
 import java.util.Arrays;
 
-import DafnyVMC.Random;
-
-class Check {
+public class BuildTest {
     public static void main(String[] args) {
         BigInteger[] arr1 = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)};
+        BigInteger[] arr1_custom = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)};
+        BigInteger[] arr1_faulty = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)};
         int[] arr2 = {0, 1, 2};
+        int[] arr2_custom = {0, 1, 2};
+        int[] arr2_faulty = {0, 1, 2};
         String[] arr3 = {"aa", "bb", "cc"};
+        String[] arr3_custom = {"aa", "bb", "cc"};
+        String[] arr3_faulty = {"aa", "bb", "cc"};
         char[] arr4 = {'a', 'b', 'c'};
+        char[] arr4_custom = {'a', 'b', 'c'};
+        char[] arr4_faulty = {'a', 'b', 'c'};
         boolean[] arr5 = {true, false, false, true};
+        boolean[] arr5_custom = {true, false, false, true};
+        boolean[] arr5_faulty = {true, false, false, true};
         long[] arr6 = {111111L, 333333L, 999999L};
+        long[] arr6_custom = {111111L, 333333L, 999999L};
+        long[] arr6_faulty = {111111L, 333333L, 999999L};
         short[] arr7 = {-3, 0, 3};
+        short[] arr7_custom = {-3, 0, 3};
+        short[] arr7_faulty = {-3, 0, 3};
         BigInteger num = BigInteger.valueOf(3);
         BigInteger den = BigInteger.valueOf(5);
-
-        /* STANDARD RNG */
-        System.out.println("\nSTANDARD RNG TESTS\n");
-
+
         DafnyVMC.Random r = new DafnyVMC.Random();
+        CustomFisherYates r_custom = new CustomFisherYates();
+        CustomFisherYatesFaulty r_faulty = new CustomFisherYatesFaulty();
 
         System.out.println("Example of Uniform sampling");
         System.out.println(r.UniformSample(BigInteger.valueOf(4)));
@@ -39,78 +49,86 @@ public static void main(String[] args) {
         System.out.println("Example of Fisher-Yates: BigInteger");
         r.Shuffle(arr1);
         System.out.println(Arrays.toString(arr1));
+
+        System.out.println("Example of custom Fisher-Yates: BigInteger");
+        r_custom.Shuffle(arr1_custom);
+        System.out.println(Arrays.toString(arr1_custom));
+
+        System.out.println("Example of faulty custom Fisher-Yates: BigInteger");
+        r_faulty.Shuffle(arr1_faulty);
+        System.out.println(Arrays.toString(arr1_faulty));
 
         System.out.println("Example of Fisher-Yates: int");
         r.Shuffle(arr2);
         System.out.println(Arrays.toString(arr2));
 
+        System.out.println("Example of custom Fisher-Yates: int");
+        r_custom.Shuffle(arr2_custom);
+        System.out.println(Arrays.toString(arr2_custom));
+
+        System.out.println("Example of faulty custom Fisher-Yates: int");
+        r_faulty.Shuffle(arr2_faulty);
+        System.out.println(Arrays.toString(arr2_faulty));
+
         System.out.println("Example of Fisher-Yates: String");
         r.Shuffle(arr3);
         System.out.println(Arrays.toString(arr3));
 
+        System.out.println("Example of custom Fisher-Yates: String");
+        r_custom.Shuffle(arr3_custom);
+        System.out.println(Arrays.toString(arr3_custom));
+
+        System.out.println("Example of faulty custom Fisher-Yates: String");
+        r_faulty.Shuffle(arr3_faulty);
+        System.out.println(Arrays.toString(arr3_faulty));
+
         System.out.println("Example of Fisher-Yates: char");
         r.Shuffle(arr4);
         System.out.println(Arrays.toString(arr4));
 
+        System.out.println("Example of custom Fisher-Yates: char");
+        r_custom.Shuffle(arr4_custom);
+        System.out.println(Arrays.toString(arr4_custom));
+
+        System.out.println("Example of faulty custom Fisher-Yates: char");
+        r_faulty.Shuffle(arr4_faulty);
+        System.out.println(Arrays.toString(arr4_faulty));
+
         System.out.println("Example of Fisher-Yates: boolean");
         r.Shuffle(arr5);
         System.out.println(Arrays.toString(arr5));
 
+        System.out.println("Example of custom Fisher-Yates: boolean");
+        r_custom.Shuffle(arr5_custom);
+        System.out.println(Arrays.toString(arr5_custom));
+
+        System.out.println("Example of faulty custom Fisher-Yates: boolean");
+        r_faulty.Shuffle(arr5_faulty);
+        System.out.println(Arrays.toString(arr5_faulty));
+
         System.out.println("Example of Fisher-Yates: long");
         r.Shuffle(arr6);
         System.out.println(Arrays.toString(arr6));
 
+        System.out.println("Example of custom Fisher-Yates: long");
+        r_custom.Shuffle(arr6_custom);
+        System.out.println(Arrays.toString(arr6_custom));
+
+        System.out.println("Example of faulty custom Fisher-Yates: long");
+        r_faulty.Shuffle(arr6_faulty);
+        System.out.println(Arrays.toString(arr6_faulty));
+
         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\n");
-
-        SecureRandom rng = new SecureRandom();
-        DafnyVMC.Random t = new DafnyVMC.Random(() -> rng);
-
-        System.out.println("Example of Uniform sampling");
-        System.out.println(t.UniformSample(BigInteger.valueOf(4)));
-
-        System.out.println("Example of Bernoulli sampling");
-        System.out.println(t.BernoulliSample(num,den));
-
-        System.out.println("Example of BernoulliExpNeg sampling");
-        System.out.println(r.BernoulliExpNegSample(num,den));
-
-        System.out.println("Example of DiscreteGaussian sampling");
-        System.out.println(t.DiscreteGaussianSample(num,den));
+        System.out.println("Example of custom Fisher-Yates: short");
+        r_custom.Shuffle(arr7_custom);
+        System.out.println(Arrays.toString(arr7_custom));
 
-        System.out.println("Example of DiscreteLaplace sampling");
-        System.out.println(t.DiscreteLaplaceSample(num,den));
-
-        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));
+        System.out.println("Example of faulty custom Fisher-Yates: short");
+        r_faulty.Shuffle(arr7_faulty);
+        System.out.println(Arrays.toString(arr7_faulty));
     }
-}
+}
+

docs/java/CustomFisherYates.java

@@ -0,0 +1,89 @@
+import Uniform.Interface.TraitMinus;
+import Uniform.Interface.Trait;
+import java.math.BigInteger;
+import java.security.SecureRandom;
+import java.util.Random;
+import dafny.TypeDescriptor;
+
+class CustomUniformSampleMinus implements Uniform.Interface.TraitMinus {
+  static ThreadLocal<SecureRandom> rng;
+
+  public CustomUniformSampleMinus() {
+      CustomUniformSampleMinus.rng = ThreadLocal.withInitial(CustomUniformSampleMinus::createSecureRandom);
+  }
+
+  private static final SecureRandom createSecureRandom() {
+      final SecureRandom rng = new SecureRandom();
+      // Required for proper initialization
+      rng.nextBoolean(); 
+      return rng;
+  }
+
+  public BigInteger UniformPowerOfTwoSample(BigInteger n) {
+      if (n.compareTo(BigInteger.ONE) < 0) {
+        throw new IllegalArgumentException("n must be positive");
+      }
+
+      return new BigInteger(n.bitLength()-1, rng.get());
+  }
+
+  public BigInteger UniformSample(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;    
+  }
+}
+
+class CustomUniform extends CustomUniformSampleMinus implements Uniform.Interface.Trait {
+  public java.math.BigInteger UniformIntervalSample(java.math.BigInteger a, java.math.BigInteger b) {
+    return Uniform.Interface._Companion_Trait.UniformIntervalSample(this, a, b);
+  }
+}
+
+
+class CustomFisherYatesMinus extends CustomUniform implements FisherYates.Implementation.Trait {
+  public <__T> void Shuffle(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a) {
+    FisherYates.Implementation._Companion_Trait.Shuffle(_td___T, this, a);
+  }
+
+  public <__T> void Swap(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a, java.math.BigInteger i, java.math.BigInteger j) {
+    FisherYates.Implementation._Companion_Trait.Swap(_td___T, this, a, i, j);
+  }
+}
+
+public class CustomFisherYates extends CustomFisherYatesMinus {
+  public void Shuffle(BigInteger[] arr) {
+    this.Shuffle(TypeDescriptor.BIG_INTEGER, arr);
+  }
+
+  public void Shuffle(int[] arr) {
+    this.Shuffle(TypeDescriptor.INT, arr);
+  }
+
+  public void Shuffle(String[] arr) {
+    this.Shuffle(TypeDescriptor.CHAR_ARRAY, arr);
+  }
+
+  public void Shuffle(char[] arr) {
+    this.Shuffle(TypeDescriptor.CHAR, arr);
+  }
+
+  public void Shuffle(boolean[] arr) {
+    this.Shuffle(TypeDescriptor.BOOLEAN, arr);
+  }
+
+  public void Shuffle(long[] arr) {
+    this.Shuffle(TypeDescriptor.LONG, arr);
+  }
+
+  public void Shuffle(short[] arr) {
+    this.Shuffle(TypeDescriptor.SHORT, arr);
+  }
+}

docs/java/CustomFisherYatesFaulty.java

@@ -0,0 +1,58 @@
+import Uniform.Interface.TraitMinus;
+import Uniform.Interface.Trait;
+import java.math.BigInteger;
+import java.security.SecureRandom;
+import java.util.Random;
+import dafny.TypeDescriptor;
+
+class CustomUniformSampleFaultyMinus implements Uniform.Interface.TraitMinus {  
+  public BigInteger UniformSample(BigInteger n) {
+    return BigInteger.valueOf(0);
+  }
+}
+
+class CustomUniformFaulty extends CustomUniformSampleFaultyMinus implements Uniform.Interface.Trait {
+  public java.math.BigInteger UniformIntervalSample(java.math.BigInteger a, java.math.BigInteger b) {
+    return Uniform.Interface._Companion_Trait.UniformIntervalSample(this, a, b);
+  }
+}
+
+class CustomFisherYatesMinusFaulty extends CustomUniformFaulty implements FisherYates.Implementation.Trait {
+  public <__T> void Shuffle(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a) {
+    FisherYates.Implementation._Companion_Trait.Shuffle(_td___T, this, a);
+  }
+
+  public <__T> void Swap(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a, java.math.BigInteger i, java.math.BigInteger j) {
+    FisherYates.Implementation._Companion_Trait.Swap(_td___T, this, a, i, j);
+  }
+}
+
+public class CustomFisherYatesFaulty extends CustomFisherYatesMinusFaulty {
+  public void Shuffle(BigInteger[] arr) {
+    this.Shuffle(TypeDescriptor.BIG_INTEGER, arr);
+  }
+
+  public void Shuffle(int[] arr) {
+    this.Shuffle(TypeDescriptor.INT, arr);
+  }
+
+  public void Shuffle(String[] arr) {
+    this.Shuffle(TypeDescriptor.CHAR_ARRAY, arr);
+  }
+
+  public void Shuffle(char[] arr) {
+    this.Shuffle(TypeDescriptor.CHAR, arr);
+  }
+
+  public void Shuffle(boolean[] arr) {
+    this.Shuffle(TypeDescriptor.BOOLEAN, arr);
+  }
+
+  public void Shuffle(long[] arr) {
+    this.Shuffle(TypeDescriptor.LONG, arr);
+  }
+
+  public void Shuffle(short[] arr) {
+    this.Shuffle(TypeDescriptor.SHORT, arr);
+  }
+}

src/DafnyVMCTrait.dfy

@@ -26,7 +26,7 @@ module DafnyVMCTrait {
 
     method {:verify false} BernoulliSample (num: nat, den: pos)
       returns (o: bool)
-      requires num <= den 
+      requires num <= den
       modifies this
       decreases *
     {
@@ -36,7 +36,7 @@ module DafnyVMCTrait {
 
     method {:verify false} BernoulliExpNegSampleUnitLoop (num: nat, den: pos, state: (bool,pos))
       returns (o: (bool,pos))
-      requires num <= den 
+      requires num <= den
       modifies this
       decreases *
     {
@@ -46,7 +46,7 @@ module DafnyVMCTrait {
 
     method {:verify false} BernoulliExpNegSampleUnitAux (num: nat, den: pos)
       returns (o: nat)
-      requires num <= den 
+      requires num <= den
       modifies this
       decreases *
     {
@@ -62,7 +62,7 @@ module DafnyVMCTrait {
 
     method {:verify false} BernoulliExpNegSampleUnit (num: nat, den: pos)
       returns (o: bool)
-      requires num <= den 
+      requires num <= den
       modifies this
       decreases *
     {
@@ -136,7 +136,7 @@ module DafnyVMCTrait {
 
     method {:verify false} DiscreteLaplaceSampleLoopIn2Aux (num: nat, den: pos, K: (bool,pos))
       returns (o: (bool,pos))
-      requires num <= den 
+      requires num <= den
       modifies this
       decreases *
     {
@@ -222,6 +222,6 @@ module DafnyVMCTrait {
     }
 
 
-}
+  }
 
 }