From 458556fffdecff258b487773d6651e5498a7ccd0 Mon Sep 17 00:00:00 2001 From: Stefan Zetzsche <120379523+stefan-aws@users.noreply.github.com> Date: Thu, 14 Mar 2024 16:39:47 +0000 Subject: [PATCH 1/2] Update readme (#165) 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 | 60 +++++++++++++++++++++++++++++------ docs/dafny/ExamplesRandom.dfy | 2 +- 2 files changed, 52 insertions(+), 10 deletions(-) diff --git a/README.md b/README.md index 3eca5386..3de7b00a 100644 --- a/README.md +++ b/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 ``` diff --git a/docs/dafny/ExamplesRandom.dfy b/docs/dafny/ExamplesRandom.dfy index 041f1ad0..be8658e3 100644 --- a/docs/dafny/ExamplesRandom.dfy +++ b/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 { From ece20eeacc01bc55d7f597f04f264654c69f3f17 Mon Sep 17 00:00:00 2001 From: Stefan Zetzsche <120379523+stefan-aws@users.noreply.github.com> Date: Thu, 14 Mar 2024 16:52:57 +0000 Subject: [PATCH 2/2] Remove {:vcs_split_on_every_assert} (#166) 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). Co-authored-by: John Tristan --- src/Util/FisherYates/Correctness.dfy | 42 +++++++++++++--------------- 1 file changed, 19 insertions(+), 23 deletions(-) diff --git a/src/Util/FisherYates/Correctness.dfy b/src/Util/FisherYates/Correctness.dfy index 266bb88c..f5c3bb8c 100644 --- a/src/Util/FisherYates/Correctness.dfy +++ b/src/Util/FisherYates/Correctness.dfy @@ -576,7 +576,23 @@ module FisherYates.Correctness { reveal DecomposeE; } - lemma {:vcs_split_on_every_assert} ProbabilityOfE(xs: seq, ys: seq, p: seq, i: nat, j: nat, h: Monad.Hurd, A: iset, e: iset, e': iset) + lemma ProbabilityOfESimplifyFractions(xs: seq, ys: seq, p: seq, i: nat, j: nat, h: Monad.Hurd, A: iset, e: iset, e': iset) + 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(xs: seq, ys: seq, p: seq, i: nat, j: nat, h: Monad.Hurd, A: iset, e: iset, e': iset) + 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(xs: seq, ys: seq, p: seq, i: nat, j: nat, h: Monad.Hurd, A: iset, e: iset, e': iset) 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);