Implementation, testing, and examples of Fisher-Yates (#137)

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

README.md

@@ -2,28 +2,54 @@
 
 The `DafnyVMC` module introduces utils for probabilistic reasoning in Dafny. At the moment, the API is intentionally limited in scope, and only supports compilation to Java. For the future, we plan to extend both the functionality and the range of supported languages.
 
-There are two ways to use the library:
-- The trait `DRandomFoundational` only needs fair coin flips as a primitive.
-- The trait `DRandomExternUniformPowerOfTwo` also uses an external implementation of uniformly distributed random numbers.
+## Java API Example
 
-To run the examples in the `docs` directory, use one of the following commands:
+```java
+import DafnyVMC.Random;
+import java.math.BigInteger;
+import java.util.Arrays;
+
+class Test {
+  public static void main(String[] args) {
+    DafnyVMC.Random r = new DafnyVMC.Random();
+
+    System.out.println("Example of Fisher-Yates shuffling");
+    char[] arr = {'a', 'b', 'c'};
+    r.Shuffle(arr);
+    System.out.println(Arrays.toString(arr));
+
+    System.out.println("Example of Bernoulli sampling");
+    Rationals.Rational gamma = new Rationals.Rational(BigInteger.valueOf(3), BigInteger.valueOf(5));
+    System.out.println(r.BernoulliSample(gamma));
+  }
+}
+```
+
+## Dafny Examples
+
+To run the examples in the `docs/dafny` directory, use the following commands:
 
 ```bash
-# Java Examples Foundational
-$ dafny build docs/dafny/ExamplesFoundational.dfy --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniformPowerOfTwo.java dfyconfig.toml --no-verify
-$ java -jar docs/dafny/ExamplesFoundational.jar
-# Java Examples ExternUniformPowerOfTwo
-$ dafny build docs/dafny/ExamplesExternUniformPowerOfTwo.dfy --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniformPowerOfTwo.java dfyconfig.toml --no-verify
-$ java -jar docs/dafny/ExamplesExternUniformPowerOfTwo.jar
+$ dafny build docs/dafny/ExamplesRandom.dfy --target:java src/interop/java/Full/Random.java src/interop/java/Part/Random.java dfyconfig.toml --no-verify
+$ java -jar docs/dafny/ExamplesRandom.jar
 ```
 
-# Testing
+## Java Examples
 
-To run the statistical tests in the `tests` diretory, use one of the following commands:
+To run the examples in the `docs/java` directory, use the following commands:
 
 ```bash
-# Java Tests Foundational
-$ dafny test --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniformPowerOfTwo.java tests/TestsFoundational.dfy tests/Tests.dfy dfyconfig.toml --no-verify
-# Java Tests ExternUniformPowerOfTwo
-$ dafny test --target:java src/interop/java/DRandomCoin.java src/interop/java/DRandomUniformPowerOfTwo.java tests/TestsExternUniformPowerOfTwo.dfy tests/Tests.dfy dfyconfig.toml --no-verify
+$ bash scripts/build.sh 
+$ bash build/java/run.sh  
 ```
+
+## Dafny Testing
+
+To run the statistical tests in the `tests` directory, use the following commands:
+
+```bash
+$ dafny test --target:java src/interop/java/Full/Random.java src/interop/java/Part/Random.java tests/TestsRandom.dfy tests/Tests.dfy dfyconfig.toml --no-verify
+```
+
+
+

audit.log

@@ -1,3 +1,4 @@
+src/DafnyVMC.dfy(23,6): UniformPowerOfTwoSample: Definition has `assume {:axiom}` statement in body. 
 src/Distributions/Bernoulli/Correctness.dfy(59,17): BernoulliCorrectnessCaseFalse: Declaration has explicit `{:axiom}` attribute. 
 src/Distributions/BernoulliExpNeg/Correctness.dfy(228,6): CorrectnessLe1: Definition has `assume {:axiom}` statement in body. 
 src/Distributions/BernoulliExpNeg/Correctness.dfy(251,17): SampleLe1IsIndep: Declaration has explicit `{:axiom}` attribute. 
@@ -16,11 +17,9 @@ src/Distributions/BernoulliExpNeg/Model.dfy(161,8): Le1LoopDivergenceProbability
 src/Distributions/BernoulliExpNeg/Model.dfy(162,8): Le1LoopDivergenceProbabilityBound: Definition has `assume {:axiom}` statement in body. 
 src/Distributions/BernoulliExpNeg/Model.dfy(185,10): Le1LoopDivergenceProbabilityBound: Definition has `assume {:axiom}` statement in body. 
 src/Distributions/BernoulliExpNeg/Model.dfy(71,17): Le1LoopIterCorrectness: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/Coin/Interface.dfy(21,6): CoinSample: Definition has `assume {:axiom}` statement in body. 
 src/Distributions/DiscreteLaplace/Correctness.dfy(37,17): Correctness: Declaration has explicit `{:axiom}` attribute. 
 src/Distributions/DiscreteLaplace/Model.dfy(89,17): SampleInnerLoopTerminatesAlmostSurely: Declaration has explicit `{:axiom}` attribute. 
 src/Distributions/DiscreteLaplace/Model.dfy(93,17): SampleLoopTerminatesAlmostSurely: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/UniformPowerOfTwo/Implementation.dfy(42,6): UniformPowerOfTwoSample: Definition has `assume {:axiom}` statement in body. 
 src/Math/Analysis/Limits.dfy(126,17): Sandwich: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Analysis/Reals.dfy(35,17): LeastUpperBoundProperty: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Exponential.dfy(55,17): ExpSeriesConverges: Declaration has explicit `{:axiom}` attribute. 

build/java/run.sh

@@ -1,3 +1,3 @@
 #1/bin/bash
 
-java -classpath build/java/Dafny-VMC.jar docs/java/BuildTest.java
+java -classpath build/java/DafnyVMC.jar docs/java/BuildTest.java

dfyconfig.toml

@@ -1,5 +1,4 @@
 includes = ["src/**/*.dfy"]
-excludes = []
 
 [options]
-enforce-determinism = true
+enforce-determinism = false

docs/dafny/ExamplesExternUniformPowerOfTwo.dfy → docs/dafny/ExamplesRandom.dfy

@@ -3,15 +3,16 @@
  *  SPDX-License-Identifier: MIT
  *******************************************************************************/
 
-module RandomExamples.ExternUniform {
+module Examples {
   import Rationals
   import DafnyVMC
+  import Helper
 
   method Main()
     decreases *
   {
     var n := 100000;
-    var r: DafnyVMC.DRandomExternUniformPowerOfTwo := new DafnyVMC.DRandomExternUniformPowerOfTwo();
+    var r: DafnyVMC.Random := new DafnyVMC.Random();
 
     var t := 0;
     for i := 0 to n {
@@ -124,5 +125,15 @@ module RandomExamples.ExternUniform {
     // https://www.wolframalpha.com/input?i=ReplaceAll%5BE%5E%28-x%5E2+%2F+%282+*%CF%83%5E2%29%29+%2F+Sum%5BE%5E%28-y%5E2%2F%282+%CF%83%5E2%29%29%2C+%7By%2C+-Infinity%2C+Infinity%7D%5D%2C+%7Bx+-%3E+0%2C+%CF%83+-%3E+1.4%7D%5D
     // https://www.wolframalpha.com/input?i=ReplaceAll%5BE%5E%28-x%5E2+%2F+%282+*%CF%83%5E2%29%29+%2F+Sum%5BE%5E%28-y%5E2%2F%282+%CF%83%5E2%29%29%2C+%7By%2C+-Infinity%2C+Infinity%7D%5D%2C+%7Bx+-%3E+1%2C+%CF%83+-%3E+1.4%7D%5D
     print "Estimated probabilities for DiscreteGaussianSample(1.4): ", count0 as real / n as real, " (should be around 0.284959) and ", count1 as real / n as real, ", ", countneg1 as real / n as real, " (should both be around 0.220797)\n";
+
+    // Fisher-Yates Example
+    print "Ten permutations of 012: ";
+    var arr: array<nat> := new nat[3](i => i); // [0, 1, 2]
+    for i := 0 to 10 {
+      var arrCopy := arr;
+      r.Shuffle(arrCopy);
+      print Helper.SeqToString(arrCopy[..], Helper.NatToString), ", ";
+    }
+    print "\n";
   }
 }

docs/dafny/index.html

@@ -2,6 +2,4 @@
 <br>
 <a href="dafny-doc/index.html">Dafny documentation</a>
 <br>
-<a href="ExamplesFoundational.dfy">Example using the foundational uniform sampler</a>
-<br>
-<a href="ExamplesExternUniform.dfy">Example using the extern uniform sampler</a>
+<a href="ExamplesRandom.dfy">Example using the foundational uniform sampler</a>