working example

audit.log

@@ -1,2 +1,3 @@
+src/DafnyVMC.dfy(35,27): UniformSample32: Declaration has `{:verify false}` attribute. 
 src/Distributions/Uniform/Model.dfy(19,26): Sample: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/RandomSource.dfy(50,17): ProbIsProbabilityMeasure: Declaration has explicit `{:axiom}` attribute. 

build/java/run_samplers.sh

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

build/java/run_shuffling.sh

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

docs/java/CustomTestShuffling.java → docs/java/TestShuffling32.java

@@ -4,7 +4,7 @@
 
 import DafnyVMC.Random;
 
-class CustomTestShuffling {
+class TestShuffling32 {
     public static void main(String[] args) {
         BigInteger[] arr1 = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)};
         int[] arr2 = {0, 1, 2};
@@ -18,68 +18,68 @@ public static void main(String[] args) {
         /* STANDARD RNG */
         System.out.println("\nSTANDARD RNG TESTS WITH CUSTOM UNIFORM\n");
 
-        DafnyVMC.CustomRandom r = new DafnyVMC.CustomRandom();
+        DafnyVMC.Random r = new DafnyVMC.Random();
 
         System.out.println("Example of Fisher-Yates: BigInteger");
-        r.Shuffle(arr1);
+        r.Shuffle32(arr1);
         System.out.println(Arrays.toString(arr1));
 
         System.out.println("Example of Fisher-Yates: int");
-        r.Shuffle(arr2);
+        r.Shuffle32(arr2);
         System.out.println(Arrays.toString(arr2));
 
         System.out.println("Example of Fisher-Yates: String");
-        r.Shuffle(arr3);
+        r.Shuffle32(arr3);
         System.out.println(Arrays.toString(arr3));
 
         System.out.println("Example of Fisher-Yates: char");
-        r.Shuffle(arr4);
+        r.Shuffle32(arr4);
         System.out.println(Arrays.toString(arr4));
 
         System.out.println("Example of Fisher-Yates: boolean");
-        r.Shuffle(arr5);
+        r.Shuffle32(arr5);
         System.out.println(Arrays.toString(arr5));
 
         System.out.println("Example of Fisher-Yates: long");
-        r.Shuffle(arr6);
+        r.Shuffle32(arr6);
         System.out.println(Arrays.toString(arr6));
 
         System.out.println("Example of Fisher-Yates: short");
-        r.Shuffle(arr7);
+        r.Shuffle32(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);
+        DafnyVMC.Random t = new DafnyVMC.Random(() -> rng);
 
         System.out.println("Example of Fisher-Yates: BigInteger");
-        t.Shuffle(arr1);
+        t.Shuffle32(arr1);
         System.out.println(Arrays.toString(arr1));
 
         System.out.println("Example of Fisher-Yates: int");
-        t.Shuffle(arr2);
+        t.Shuffle32(arr2);
         System.out.println(Arrays.toString(arr2));
 
         System.out.println("Example of Fisher-Yates: String");
-        t.Shuffle(arr3);
+        t.Shuffle32(arr3);
         System.out.println(Arrays.toString(arr3));
 
         System.out.println("Example of Fisher-Yates: char");
-        t.Shuffle(arr4);
+        t.Shuffle32(arr4);
         System.out.println(Arrays.toString(arr4));
 
         System.out.println("Example of Fisher-Yates: boolean");
-        t.Shuffle(arr5);
+        t.Shuffle32(arr5);
         System.out.println(Arrays.toString(arr5));
 
         System.out.println("Example of Fisher-Yates: long");
-        t.Shuffle(arr6);
+        t.Shuffle32(arr6);
         System.out.println(Arrays.toString(arr6));
 
         System.out.println("Example of Fisher-Yates: short");
-        t.Shuffle(arr7);
+        t.Shuffle32(arr7);
         System.out.println(Arrays.toString(arr7));
     }
 }

docs/py/CustomTestShuffling.py → docs/py/TestShuffling32.py

@@ -10,26 +10,26 @@ def main():
     # STANDARD RNG
     print("\nSTANDARD RNG TESTS WITH CUSTOM UNIFORM\n")
 
-    r = DafnyVMC.CustomRandom()
+    r = DafnyVMC.Random()
 
     print("Example of Fisher-Yates: int")
-    arr1 = r.Shuffle(arr1)
+    arr1 = r.Shuffle32(arr1)
     print(arr1)
 
     print("Example of Fisher-Yates: float")
-    arr2 = r.Shuffle(arr2)
+    arr2 = r.Shuffle32(arr2)
     print(arr2)
 
     print("Example of Fisher-Yates: str")
-    arr3 = r.Shuffle(arr3)
+    arr3 = r.Shuffle32(arr3)
     print(arr3)
 
     print("Example of Fisher-Yates: char/str")
-    arr4 = r.Shuffle(arr4)
+    arr4 = r.Shuffle32(arr4)
     print(arr4)
 
     print("Example of Fisher-Yates: boolean")
-    arr5 = r.Shuffle(arr5)
+    arr5 = r.Shuffle32(arr5)
     print(arr5)
 
 if __name__ == "__main__":

scripts/build.sh

@@ -16,7 +16,7 @@ fi
 
 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
+  $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
 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/DafnyVMC.dfy

@@ -4,9 +4,13 @@
  *******************************************************************************/
 
 module {:extern} DafnyVMCPartMaterial {
+  import opened Pos
+
   class {:extern} Random {
     // For running Dafny native testing with standard SecureRandom rng
     static method {:extern "UniformPowerOfTwoSample"} ExternUniformPowerOfTwoSample(n: nat) returns (u: nat)
+
+    static method {:extern "UniformSample32"} ExternUniformSample32(n: pos32) returns (u: nat32)
   }
 }
 
@@ -15,6 +19,8 @@ module {:extern "DafnyVMCPart"} DafnyVMC {
   import DafnyVMCPartMaterial
   import Monad
   import UniformPowerOfTwo
+  import Uniform
+  import opened Pos
 
   class Random extends DafnyVMCTrait.RandomTrait {
     constructor {:extern} ()
@@ -25,6 +31,15 @@ module {:extern "DafnyVMCPart"} DafnyVMC {
     {
       u := DafnyVMCPartMaterial.Random.ExternUniformPowerOfTwoSample(n);
     }
+
+    method {:verify false} UniformSample32(n: pos32) returns (u: nat32)
+      modifies `s
+      decreases *
+      ensures u < n
+      ensures Uniform.Model.Sample(n as nat)(old(s)) == Monad.Result(u as nat, s)
+    {
+      u := DafnyVMCPartMaterial.Random.ExternUniformSample32(n);
+    }
   }
 
 }

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, FisherYates.Implementation.Trait32 {
 
     method {:verify false} UniformSample (n: pos)
       returns (o: nat)

src/Util/FisherYates/Interface.dfy

@@ -23,7 +23,7 @@ module FisherYates.Interface {
       decreases *
       modifies `s, a
       requires a.Length < 0x8000_0000
-      //ensures Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s)
+      ensures Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s)
 
   }
 }