Merge branch 'main' into documentation

README.md

@@ -1,8 +1,10 @@
 # VMC: a Library for Verified Monte Carlo Algorithms
 
-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.
+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 and Python. For the future, we plan to extend both the functionality and the range of supported languages.
 
-## Java API Example
+## Java
+
+### Java API
 
 ```java
 import DafnyVMC.Random;
@@ -26,31 +28,71 @@ class Test {
 }
 ```
 
-## Dafny Examples
+### Java Examples
 
-To run the examples in the `docs/dafny` directory, use the following commands:
+To run the examples in the `docs/java` directory, use the following commands:
+
+```bash
+$ export TARGET_LANG=java
+$ bash scripts/build.sh
+$ bash build/java/run_samplers.sh
+$ bash build/java/run_shuffling.sh
+```
+
+To run the tests in the `docs/dafny` directory, use the following commands:
 
 ```bash
 $ 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
 ```
 
-## Java Examples
+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
+```
+
+## Python
+
+### Python API
+
+```py
+import DafnyVMC
+
+def main():
+  r = DafnyVMC.Random()
+
+  print("Example of Fisher-Yates shuffling")
+  arr = ['a', 'b', 'c']
+  arr = r.Shuffle(arr)
+  print(arr)
+
+  print("Example of Bernoulli sampling")
+  print(r.BernoulliSample(3, 5))
+```
+
+### Python Examples
 
 To run the examples in the `docs/java` directory, use the following commands:
 
 ```bash
-$ export TARGET_LANG=java
+$ export TARGET_LANG=py
 $ bash scripts/build.sh
-$ bash build/java/run.sh 
+$ bash build/py/run_samplers.sh
+$ bash build/py/run_shuffling.sh
 ```
 
-## Dafny Testing
+To run the tests in the `docs/dafny` directory, use the following commands:
+
+```bash
+$ dafny build docs/dafny/ExamplesRandom.dfy --target:py src/interop/py/Full/Random.py src/interop/py/Part/Random.py dfyconfig.toml --no-verify
+$ python3 docs/dafny/ExamplesRandom-py/__main__.py
+```
 
 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
+$ dafny test --target:py src/interop/py/Full/Random.py src/interop/py/Part/Random.py tests/TestsRandom.dfy tests/Tests.dfy dfyconfig.toml --no-verify
 ```
 
 

docs/dafny/ExamplesRandom.dfy

@@ -73,7 +73,7 @@ module Examples {
       }
     }
 
-    print "Estimated parameter for BernoulliSample(5, 5): ", (t as real) / (n as real), " (should be around 1.0\n";
+    print "Estimated parameter for BernoulliSample(5, 5): ", (t as real) / (n as real), " (should be around 1.0)\n";
 
     t := 0;
     for i := 0 to n {

src/Util/FisherYates/Correctness.dfy

@@ -576,7 +576,23 @@ module FisherYates.Correctness {
     reveal DecomposeE;
   }
 
-  lemma {:vcs_split_on_every_assert} ProbabilityOfE<T(!new)>(xs: seq<T>, ys: seq<T>, p: seq<T>, i: nat, j: nat, h: Monad.Hurd<int>, A: iset<int>, e: iset<Rand.Bitstream>, e': iset<Rand.Bitstream>)
+  lemma ProbabilityOfESimplifyFractions<T(!new)>(xs: seq<T>, ys: seq<T>, p: seq<T>, i: nat, j: nat, h: Monad.Hurd<int>, A: iset<int>, e: iset<Rand.Bitstream>, e': iset<Rand.Bitstream>)
+    requires |xs| - i > 1
+    ensures (1.0 / ((|xs|-i) as real)) * (1.0 /  NatArith.FactorialTraditional((|xs|-i)-1) as real) == (1.0 * 1.0) / (((|xs|-i) as real) * (NatArith.FactorialTraditional(|xs|-(i+1)) as real))
+  {
+    var denom := NatArith.FactorialTraditional(|xs|-(i+1)) as real;
+    RealArith.SimplifyFractionsMultiplication(1.0, (|xs|-i) as real, 1.0, denom);
+  }
+
+  lemma ProbabilityOfEAsRealOfMult<T(!new)>(xs: seq<T>, ys: seq<T>, p: seq<T>, i: nat, j: nat, h: Monad.Hurd<int>, A: iset<int>, e: iset<Rand.Bitstream>, e': iset<Rand.Bitstream>)
+    requires |xs| - i > 1
+    ensures (((|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1)) as real) != 0.0
+    ensures 1.0 / (((|xs|-i) as real) * NatArith.FactorialTraditional(|xs|-(i+1)) as real) == 1.0 / (((|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1)) as real)
+  {
+    RealArith.AsRealOfMultiplication(|xs|-i, NatArith.FactorialTraditional((|xs|-i)-1));
+  }
+
+  lemma ProbabilityOfE<T(!new)>(xs: seq<T>, ys: seq<T>, p: seq<T>, i: nat, j: nat, h: Monad.Hurd<int>, A: iset<int>, e: iset<Rand.Bitstream>, e': iset<Rand.Bitstream>)
     requires i <= |xs|
     requires i <= |p|
     requires forall a, b | i <= a < b < |xs| :: xs[a] != xs[b]
@@ -626,26 +642,6 @@ module FisherYates.Correctness {
       RealArith.MultiplicationInvariance(1.0 / ((|xs|-i) as real), frac, frac2);
     }
 
-    assert SimplifyFractionsMultiplicationLifted: (1.0 / ((|xs|-i) as real)) * frac2 == (1.0 * 1.0) / (((|xs|-i) as real) * denom) by {
-      assert |xs|-i > 1;
-      RealArith.SimplifyFractionsMultiplication(1.0, (|xs|-i) as real, 1.0, denom);
-    }
-
-    assert AsRealOfMultiplicationLifted: 1.0 / (((|xs|-i) as real) * denom) == 1.0 / (((|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1)) as real) by {
-      assert ((|xs|-i) as real) * denom == ((|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1)) as real by {
-        RealArith.AsRealOfMultiplication(|xs|-i, NatArith.FactorialTraditional((|xs|-i)-1));
-      }
-    }
-
-    assert NonZero: (((|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1)) as real) != 0.0 by {
-      assert |xs|-i != 0;
-      assert NatArith.FactorialTraditional((|xs|-i)-1) != 0;
-    }
-
-    assert NonZeroDenom: denom != 0.0 by {
-      assert NatArith.FactorialTraditional((|xs|-i)-1) != 0;
-    }
-
     calc {
       Rand.prob(e);
       { reveal DecomposeE; }
@@ -660,11 +656,11 @@ module FisherYates.Correctness {
       (1.0 / ((|xs|-i) as real)) * frac;
       { reveal FracLifted; }
       (1.0 / ((|xs|-i) as real)) * frac2;
-      { reveal SimplifyFractionsMultiplicationLifted; reveal NonZeroDenom; }
+      { ProbabilityOfESimplifyFractions(xs, ys, p, i, j, h, A, e, e'); }
       (1.0 * 1.0) / (((|xs|-i) as real) * denom);
       { assert 1.0 * 1.0 == 1.0; }
       1.0 / (((|xs|-i) as real) * denom);
-      { reveal AsRealOfMultiplicationLifted; reveal NonZero; }
+      { ProbabilityOfEAsRealOfMult(xs, ys, p, i, j, h, A, e, e'); }
       1.0 / (((|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1)) as real);
       { assert (|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1) == NatArith.FactorialTraditional(|xs|-i) by { reveal NatArith.FactorialTraditional(); } }
       1.0 / (NatArith.FactorialTraditional(|xs|-i) as real);