diff --git a/README.md b/README.md index 04d62383..09ad9ed9 100644 --- a/README.md +++ b/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 +``` + + + diff --git a/audit.log b/audit.log index 36f00ebd..40477a91 100644 --- a/audit.log +++ b/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. diff --git a/build/java/run.sh b/build/java/run.sh index 92d163a6..ff6bdcad 100755 --- a/build/java/run.sh +++ b/build/java/run.sh @@ -1,3 +1,3 @@ #1/bin/bash -java -classpath build/java/Dafny-VMC.jar docs/java/BuildTest.java \ No newline at end of file +java -classpath build/java/DafnyVMC.jar docs/java/BuildTest.java \ No newline at end of file diff --git a/dfyconfig.toml b/dfyconfig.toml index 31f356c0..d38af7bd 100644 --- a/dfyconfig.toml +++ b/dfyconfig.toml @@ -1,5 +1,4 @@ includes = ["src/**/*.dfy"] -excludes = [] [options] -enforce-determinism = true +enforce-determinism = false \ No newline at end of file diff --git a/docs/dafny/ExamplesFoundational.dfy b/docs/dafny/ExamplesFoundational.dfy deleted file mode 100644 index 522ab89b..00000000 --- a/docs/dafny/ExamplesFoundational.dfy +++ /dev/null @@ -1,128 +0,0 @@ -/******************************************************************************* - * Copyright by the contributors to the Dafny Project - * SPDX-License-Identifier: MIT - *******************************************************************************/ - -module RandomExamples.Foundational { - import Rationals - import DafnyVMC - - method Main() - decreases * - { - var n := 100000; - var r: DafnyVMC.DRandomFoundational := new DafnyVMC.DRandomFoundational(); - - var t := 0; - for i := 0 to n { - var b := r.CoinSample(); - if b { - t := t + 1; - } - } - print "Estimated parameter for CoinSample(): ", (t as real) / (n as real), " (should be around 0.5)\n"; - - var a := 0; - var b := 0; - var c := 0; - for i := 0 to n { - var k := r.UniformSample(10); - if k == 0 { - a := a + 1; - } else if k == 5 { - b := b + 1; - } else if k == 9 { - c := c + 1; - } - } - print "Estimated probabilities for UniformSample(10): ", (a as real) / (n as real), "; " , (b as real) / (n as real), "; " , (c as real) / (n as real), " (each should be around 0.1)\n"; - - a := 0; - b := 0; - c := 0; - for i := 0 to n { - var k := r.UniformIntervalSample(7,10); - if k == 7 { - a := a + 1; - } else if k == 8 { - b := b + 1; - } else { - c := c + 1; - } - } - print "Estimated probabilities for UniformIntervalSample(7,10): ", (a as real) / (n as real), "; ", (b as real) / (n as real), "; " , (c as real) / (n as real), " (each should be around 0.33)\n"; - - t := 0; - for i := 0 to n { - var b := r.BernoulliSample(Rationals.Rational(1, 5)); - if b { - t := t + 1; - } - } - - print "Estimated parameter for Bernoulli(1/5): ", (t as real) / (n as real), " (should be around 0.2)\n"; - - t := 0; - for i := 0 to n { - var b := r.BernoulliSample(Rationals.Rational(0, 5)); - if b { - t := t + 1; - } - } - - print "Estimated parameter for BernoulliSample(0/5): ", (t as real) / (n as real), " (should be around 0.0)\n"; - - t := 0; - for i := 0 to n { - var b := r.BernoulliSample(Rationals.Rational(5, 5)); - if b { - t := t + 1; - } - } - - 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 { - var u := r.BernoulliExpNegSample(Rationals.Rational(12381, 5377)); // about -ln(0.1) - if u { - t := t + 1; - } - } - print "Estimated parameter for BernoulliExpNegSample(-ln(0.1)): ", (t as real) / (n as real), " (should be around 0.1)\n"; - - var count0 := 0; - var count1 := 0; - var countneg1 := 0; - for i := 0 to n { - var u := r.DiscreteLaplaceSample(Rationals.Rational(7, 5)); - match u { - case -1 => countneg1 := countneg1 + 1; - case 0 => count0 := count0 + 1; - case 1 => count1 := count1 + 1; - case _ => - } - } - // Reference values computed with Wolfram Alpha: - // https://www.wolframalpha.com/input?i=ReplaceAll%5B%28E%5E%5B1%2Ft%5D+-+1%29+%2F+%28E%5E%5B1%2Ft%5D+%2B+1%29+*+E%5E%28-Abs%5Bx%5D%2Ft%29%2C+%7Bt+-%3E+7%2F5%2C+x+-%3E+0%7D%5D - // https://www.wolframalpha.com/input?i=ReplaceAll%5B%28E%5E%5B1%2Ft%5D+-+1%29+%2F+%28E%5E%5B1%2Ft%5D+%2B+1%29+*+E%5E%28-Abs%5Bx%5D%2Ft%29%2C+%7Bt+-%3E+7%2F5%2C+x+-%3E+1%7D%5D - print "Estimated probabilities for DiscreteLaplaceSample(7/5): ", count0 as real / n as real, " (should be around 0.3426949) and ", count1 as real / n as real, ", ", countneg1 as real / n as real, " (should both be around 0.1677634)\n"; - - count0 := 0; - count1 := 0; - countneg1 := 0; - for i := 0 to n { - var u := r.DiscreteGaussianSample(Rationals.Rational(7, 5)); - match u { - case -1 => countneg1 := countneg1 + 1; - case 0 => count0 := count0 + 1; - case 1 => count1 := count1 + 1; - case _ => - } - } - // Reference values computed with Wolfram Alpha: - // 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"; - } -} diff --git a/docs/dafny/ExamplesExternUniformPowerOfTwo.dfy b/docs/dafny/ExamplesRandom.dfy similarity index 92% rename from docs/dafny/ExamplesExternUniformPowerOfTwo.dfy rename to docs/dafny/ExamplesRandom.dfy index 4f74ce6c..b33d1f89 100644 --- a/docs/dafny/ExamplesExternUniformPowerOfTwo.dfy +++ b/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 := 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"; } } diff --git a/docs/dafny/index.html b/docs/dafny/index.html index eb56a874..e14e17a7 100644 --- a/docs/dafny/index.html +++ b/docs/dafny/index.html @@ -2,6 +2,4 @@
Dafny documentation
-Example using the foundational uniform sampler -
-Example using the extern uniform sampler \ No newline at end of file +Example using the foundational uniform sampler \ No newline at end of file diff --git a/docs/java/BuildTest.java b/docs/java/BuildTest.java index 68dcc636..ce378efc 100644 --- a/docs/java/BuildTest.java +++ b/docs/java/BuildTest.java @@ -1,9 +1,121 @@ -import DafnyVMC.*; +import java.security.SecureRandom; import java.math.BigInteger; +import java.util.Arrays; + +import DafnyVMC.Random; class Check { public static void main(String[] args) { - DRandomExternUniformPowerOfTwo d = new DRandomExternUniformPowerOfTwo(); - System.out.println(d.UniformSample(BigInteger.valueOf(4))); + BigInteger[] arr1 = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)}; + int[] arr2 = {0, 1, 2}; + String[] arr3 = {"aa", "bb", "cc"}; + char[] arr4 = {'a', 'b', 'c'}; + boolean[] arr5 = {true, false, false, true}; + long[] arr6 = {111111L, 333333L, 999999L}; + short[] arr7 = {-3, 0, 3}; + Rationals.Rational gamma = new Rationals.Rational(BigInteger.valueOf(3), BigInteger.valueOf(5)); + + /* STANDARD RNG */ + System.out.println("\nSTANDARD RNG TESTS\n"); + + DafnyVMC.Random r = new DafnyVMC.Random(); + + System.out.println("Example of Coin sampling"); + System.out.println(r.CoinSample()); + + System.out.println("Example of Uniform sampling"); + System.out.println(r.UniformSample(BigInteger.valueOf(4))); + + System.out.println("Example of Bernoulli sampling"); + System.out.println(r.BernoulliSample(gamma)); + + System.out.println("Example of BernoulliExpNeg sampling"); + System.out.println(r.BernoulliExpNegSample(gamma)); + + System.out.println("Example of DiscreteGaussian sampling"); + System.out.println(r.DiscreteGaussianSample(gamma)); + + System.out.println("Example of DiscreteLaplace sampling"); + System.out.println(r.DiscreteLaplaceSample(gamma)); + + System.out.println("Example of Fisher-Yates: BigInteger"); + r.Shuffle(arr1); + System.out.println(Arrays.toString(arr1)); + + System.out.println("Example of Fisher-Yates: int"); + r.Shuffle(arr2); + System.out.println(Arrays.toString(arr2)); + + System.out.println("Example of Fisher-Yates: String"); + r.Shuffle(arr3); + System.out.println(Arrays.toString(arr3)); + + System.out.println("Example of Fisher-Yates: char"); + r.Shuffle(arr4); + System.out.println(Arrays.toString(arr4)); + + System.out.println("Example of Fisher-Yates: boolean"); + r.Shuffle(arr5); + System.out.println(Arrays.toString(arr5)); + + System.out.println("Example of Fisher-Yates: long"); + r.Shuffle(arr6); + System.out.println(Arrays.toString(arr6)); + + 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 Coin sampling"); + System.out.println(t.CoinSample()); + + 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(gamma)); + + System.out.println("Example of BernoulliExpNeg sampling"); + System.out.println(r.BernoulliExpNegSample(gamma)); + + System.out.println("Example of DiscreteGaussian sampling"); + System.out.println(t.DiscreteGaussianSample(gamma)); + + System.out.println("Example of DiscreteLaplace sampling"); + System.out.println(t.DiscreteLaplaceSample(gamma)); + + 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)); } } \ No newline at end of file diff --git a/scripts/build.sh b/scripts/build.sh index 40894139..4f44749a 100755 --- a/scripts/build.sh +++ b/scripts/build.sh @@ -14,4 +14,4 @@ then exit 1 fi -$DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG src/Dafny-VMC.dfy -o build/$TARGET_LANG/Dafny-VMC dfyconfig.toml --no-verify \ No newline at end of file +$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 \ No newline at end of file diff --git a/scripts/test.sh b/scripts/test.sh index ead74478..99b2bb56 100755 --- a/scripts/test.sh +++ b/scripts/test.sh @@ -15,25 +15,15 @@ then fi echo Running $TARGET_LANG tests... -echo "Running tests/TestsFoundational.dfy:" -time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG tests/TestsFoundational.dfy tests/Tests.dfy dfyconfig.toml --no-verify -echo "Running tests/TestsExternUniform.dfy:" -time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG tests/TestsExternUniformPowerOfTwo.dfy tests/Tests.dfy dfyconfig.toml --no-verify +echo "Running tests/TestsRandom.dfy:" +time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG tests/TestsRandom.dfy tests/Tests.dfy dfyconfig.toml --no-verify echo Running $TARGET_LANG documentation... -echo "Building docs/dafny/ExamplesFoundational.dfy..." -$DAFNY build docs/dafny/ExamplesFoundational.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG dfyconfig.toml --no-verify -echo "Executing compiled docs/dafny/ExamplesFoundational.dfy:" +echo "Building docs/dafny/ExamplesRandom.dfy..." +$DAFNY build docs/dafny/ExamplesRandom.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG dfyconfig.toml --no-verify +echo "Executing compiled docs/dafny/ExamplesRandom.dfy:" if [ "$TARGET_LANG" = "java" ] then - java -jar docs/dafny/ExamplesFoundational.jar -fi - -echo "Building docs/dafny/ExamplesExternUniformPowerOfTwo.dfy..." -$DAFNY build docs/dafny/ExamplesExternUniformPowerOfTwo.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG dfyconfig.toml --no-verify -echo "Executing compiled docs/dafny/ExamplesExternUniformPowerOfTwo.dfy:" -if [ "$TARGET_LANG" = "java" ] -then - java -jar docs/dafny/ExamplesExternUniformPowerOfTwo.jar + java -jar docs/dafny/ExamplesRandom.jar fi \ No newline at end of file diff --git a/scripts/verify.sh b/scripts/verify.sh index 606af896..36de5960 100755 --- a/scripts/verify.sh +++ b/scripts/verify.sh @@ -9,4 +9,4 @@ then fi echo Verifying the proofs... -time $DAFNY verify dfyconfig.toml docs/dafny/ExamplesExternUniformPowerOfTwo.dfy docs/dafny/ExamplesFoundational.dfy tests/Tests.dfy tests/TestsExternUniformPowerOfTwo.dfy tests/TestsFoundational.dfy --resource-limit 20000 # 20M resource usage +time $DAFNY verify dfyconfig.toml docs/dafny/ExamplesRandom.dfy tests/Tests.dfy tests/TestsRandom.dfy --resource-limit 20000 # 20M resource usage diff --git a/src/Dafny-VMC.dfy b/src/Dafny-VMC.dfy deleted file mode 100644 index f18daeb2..00000000 --- a/src/Dafny-VMC.dfy +++ /dev/null @@ -1,22 +0,0 @@ -/******************************************************************************* - * Copyright by the contributors to the Dafny Project - * SPDX-License-Identifier: MIT - *******************************************************************************/ - -module DafnyVMC { - import Coin - import Bernoulli - import UniformPowerOfTwo - import Uniform - import BernoulliExpNeg - import DiscreteGaussian - import DiscreteLaplace - - class DRandomFoundational extends Coin.Interface.Trait, UniformPowerOfTwo.Implementation.Trait, Bernoulli.Implementation.Trait, Uniform.Implementation.TraitFoundational, BernoulliExpNeg.Implementation.Trait, DiscreteGaussian.Implementation.Trait, DiscreteLaplace.Implementation.Trait { - constructor {:extern} () - } - - class DRandomExternUniformPowerOfTwo extends Coin.Interface.Trait, UniformPowerOfTwo.Implementation.TraitExtern, Bernoulli.Implementation.Trait, Uniform.Implementation.TraitFoundational, BernoulliExpNeg.Implementation.Trait, DiscreteGaussian.Implementation.Trait, DiscreteLaplace.Implementation.Trait { - constructor {:extern} () - } -} diff --git a/src/DafnyVMC.dfy b/src/DafnyVMC.dfy new file mode 100644 index 00000000..195a87eb --- /dev/null +++ b/src/DafnyVMC.dfy @@ -0,0 +1,27 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +module {:extern "DafnyVMCPart"} DafnyVMC { + import DafnyVMCTrait + import Monad + import UniformPowerOfTwo + + // For running Dafny native testing with standard SecureRandom rng + method {:extern "DafnyVMCPartMaterial.Random", "UniformPowerOfTwoSample"} ExternUniformPowerOfTwoSample(n: nat) returns (u: nat) + + class Random extends DafnyVMCTrait.RandomTrait { + constructor {:extern} () + + method UniformPowerOfTwoSample(n: nat) returns (u: nat) + requires n >= 1 + modifies this + ensures UniformPowerOfTwo.Model.Sample(n)(old(s)) == Monad.Result(u, s) + { + u := ExternUniformPowerOfTwoSample(n); + assume {:axiom} false; // assume correctness of extern implementation + } + } + +} \ No newline at end of file diff --git a/src/DafnyVMCTrait.dfy b/src/DafnyVMCTrait.dfy new file mode 100644 index 00000000..f5365a0c --- /dev/null +++ b/src/DafnyVMCTrait.dfy @@ -0,0 +1,19 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +module DafnyVMCTrait { + import Coin + import Bernoulli + import UniformPowerOfTwo + import Uniform + import BernoulliExpNeg + import DiscreteGaussian + import DiscreteLaplace + import FisherYates + import Monad + + trait {:termination false} RandomTrait extends Coin.Implementation.Trait, UniformPowerOfTwo.Implementation.Trait, Bernoulli.Implementation.Trait, Uniform.Implementation.Trait, BernoulliExpNeg.Implementation.Trait, DiscreteGaussian.Implementation.Trait, DiscreteLaplace.Implementation.Trait, FisherYates.Implementation.Trait { + } +} \ No newline at end of file diff --git a/src/Distributions/Coin/Implementation.dfy b/src/Distributions/Coin/Implementation.dfy new file mode 100644 index 00000000..d0ec31e4 --- /dev/null +++ b/src/Distributions/Coin/Implementation.dfy @@ -0,0 +1,25 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +module Coin.Implementation { + import Model + import Monad + import Interface + import UniformPowerOfTwo + + trait {:termination false} Trait extends Interface.Trait { + + method CoinSample() returns (b: bool) + modifies this + ensures Model.Sample(old(s)) == Monad.Result(b, s) + { + var x := UniformPowerOfTwoSample(2); + b := if x == 1 then true else false; + reveal UniformPowerOfTwo.Model.Sample(); + } + + } + +} diff --git a/src/Distributions/Coin/Interface.dfy b/src/Distributions/Coin/Interface.dfy index bad81b94..eca0c61b 100644 --- a/src/Distributions/Coin/Interface.dfy +++ b/src/Distributions/Coin/Interface.dfy @@ -7,19 +7,13 @@ module Coin.Interface { import Monad import Rand import Model + import UniformPowerOfTwo - method {:extern "Coin_mInterface.DRandomCoin", "Coin"} ExternCoinSample() returns (b: bool) - - trait {:termination false} Trait { - ghost var s: Rand.Bitstream + trait {:termination false} Trait extends UniformPowerOfTwo.Interface.Trait { method CoinSample() returns (b: bool) modifies this ensures Model.Sample(old(s)) == Monad.Result(b, s) - { - b := ExternCoinSample(); - assume {:axiom} false; // assume correctness of extern implementation - } } } diff --git a/src/Distributions/Uniform/Implementation.dfy b/src/Distributions/Uniform/Implementation.dfy index 49d3e1dd..2538c9e7 100644 --- a/src/Distributions/Uniform/Implementation.dfy +++ b/src/Distributions/Uniform/Implementation.dfy @@ -10,7 +10,7 @@ module Uniform.Implementation { import Interface import Equivalence - trait {:termination false} TraitFoundational extends Interface.Trait { + trait {:termination false} Trait extends Interface.Trait { method UniformSample(n: nat) returns (u: nat) modifies this decreases * diff --git a/src/Distributions/UniformPowerOfTwo/Equivalence.dfy b/src/Distributions/UniformPowerOfTwo/Equivalence.dfy deleted file mode 100644 index 4a16fe17..00000000 --- a/src/Distributions/UniformPowerOfTwo/Equivalence.dfy +++ /dev/null @@ -1,137 +0,0 @@ -/******************************************************************************* - * Copyright by the contributors to the Dafny Project - * SPDX-License-Identifier: MIT - *******************************************************************************/ - -module UniformPowerOfTwo.Equivalence { - import NatArith - import Rand - import Monad - import Model - - /************ - Definitions - ************/ - - // A tail recursive version of Sample, closer to the imperative implementation - function SampleTailRecursive(n: nat, u: nat := 0): Monad.Hurd - requires n >= 1 - { - (s: Rand.Bitstream) => - if n == 1 then - Monad.Result(u, s) - else - SampleTailRecursive(n / 2, if Rand.Head(s) then 2*u + 1 else 2*u)(Rand.Tail(s)) - } - - /******* - Lemmas - *******/ - - // Equivalence of Sample and its tail-recursive version - lemma SampleCorrespondence(n: nat, s: Rand.Bitstream) - requires n >= 1 - ensures SampleTailRecursive(n)(s) == Model.Sample(n)(s) - { - if n == 1 { - reveal Model.Sample(); - assert SampleTailRecursive(n)(s) == Model.Sample(n)(s); - } else { - var k := NatArith.Log2Floor(n); - assert NatArith.Power(2, k) <= n < NatArith.Power(2, k + 1) by { NatArith.Power2OfLog2Floor(n); } - calc { - SampleTailRecursive(n)(s); - { SampleTailRecursiveEqualIfSameLog2Floor(n, NatArith.Power(2, k), k, 0, s); } - SampleTailRecursive(NatArith.Power(2, k))(s); - Monad.Bind(Model.Sample(NatArith.Power(2, 0)), (u: nat) => SampleTailRecursive(NatArith.Power(2, k), u))(s); - { RelateWithTailRecursive(k, 0, s); } - Model.Sample(NatArith.Power(2, k))(s); - { SampleEqualIfSameLog2Floor(n, NatArith.Power(2, k), k, s); } - Model.Sample(n)(s); - } - } - } - - // All numbers between consecutive powers of 2 behave the same as arguments to SampleTailRecursive - lemma SampleTailRecursiveEqualIfSameLog2Floor(m: nat, n: nat, k: nat, u: nat, s: Rand.Bitstream) - requires m >= 1 - requires n >= 1 - requires NatArith.Power(2, k) <= m < NatArith.Power(2, k + 1) - requires NatArith.Power(2, k) <= n < NatArith.Power(2, k + 1) - ensures SampleTailRecursive(m, u)(s) == SampleTailRecursive(n, u)(s) - { - if k == 0 { - assert m == n; - } else { - assert 1 <= m; - assert 1 <= n; - calc { - SampleTailRecursive(m, u)(s); - SampleTailRecursive(m / 2, if Rand.Head(s) then 2*u + 1 else 2*u)(Rand.Tail(s)); - { SampleTailRecursiveEqualIfSameLog2Floor(m / 2, n / 2, k - 1, if Rand.Head(s) then 2*u + 1 else 2*u, Rand.Tail(s)); } - SampleTailRecursive(n / 2, if Rand.Head(s) then 2*u + 1 else 2*u)(Rand.Tail(s)); - SampleTailRecursive(n, u)(s); - } - } - } - - // All numbers between consecutive powers of 2 behave the same as arguments to Sample - lemma SampleEqualIfSameLog2Floor(m: nat, n: nat, k: nat, s: Rand.Bitstream) - requires m >= 1 - requires n >= 1 - requires NatArith.Power(2, k) <= m < NatArith.Power(2, k + 1) - requires NatArith.Power(2, k) <= n < NatArith.Power(2, k + 1) - ensures Model.Sample(m)(s) == Model.Sample(n)(s) - { - if k == 0 { - assert m == n; - } else { - assert 1 <= m; - assert 1 <= n; - calc { - Model.Sample(m)(s); - { reveal Model.Sample(); } - Monad.Bind(Model.Sample(m / 2), Model.UnifStep)(s); - { SampleEqualIfSameLog2Floor(m / 2, n / 2, k - 1, s); } - Monad.Bind(Model.Sample(n / 2), Model.UnifStep)(s); - { reveal Model.Sample(); } - Model.Sample(n)(s); - } - } - } - - // The induction invariant for the equivalence proof (generalized version of SampleCorrespondence) - lemma RelateWithTailRecursive(l: nat, m: nat, s: Rand.Bitstream) - decreases l - ensures Monad.Bind(Model.Sample(NatArith.Power(2, m)), (u: nat) => SampleTailRecursive(NatArith.Power(2, l), u))(s) == Model.Sample(NatArith.Power(2, m + l))(s) - { - if l == 0 { - calc { - Monad.Bind(Model.Sample(NatArith.Power(2, m)), (u: nat) => SampleTailRecursive(NatArith.Power(2, l), u))(s); - (var Result(u, s') := Model.Sample(NatArith.Power(2, m))(s); SampleTailRecursive(1, u)(s')); - Model.Sample(NatArith.Power(2, m + l))(s); - } - } else { - assert LGreaterZero: NatArith.Power(2, l) >= 1 by { NatArith.PowerGreater0(2, l); } - assert MGreaterZero: NatArith.Power(2, m) >= 1 by { NatArith.PowerGreater0(2, m); } - assert L1GreaterZero: NatArith.Power(2, l - 1) >= 1 by { NatArith.PowerGreater0(2, l - 1); } - calc { - Monad.Bind(Model.Sample(NatArith.Power(2, m)), (u: nat) => SampleTailRecursive(NatArith.Power(2, l), u))(s); - (var Result(u, s') := Model.Sample(NatArith.Power(2, m))(s); SampleTailRecursive(NatArith.Power(2, l), u)(s')); - { reveal LGreaterZero; } - (var Result(u, s') := Model.Sample(NatArith.Power(2, m))(s); - SampleTailRecursive(NatArith.Power(2, l) / 2, if Rand.Head(s') then 2 * u + 1 else 2 * u)(Rand.Tail(s'))); - { assert NatArith.Power(2, l) / 2 == NatArith.Power(2, l - 1); reveal L1GreaterZero; } - (var Result(u', s') := Monad.Bind(Model.Sample(NatArith.Power(2, m)), Model.UnifStep)(s); - SampleTailRecursive(NatArith.Power(2, l - 1), u')(s')); - { assert NatArith.Power(2, m + 1) / 2 == NatArith.Power(2, m); reveal Model.Sample(); } - (var Result(u', s') := Model.Sample(NatArith.Power(2, m + 1))(s); - SampleTailRecursive(NatArith.Power(2, l - 1), u')(s')); - Monad.Bind(Model.Sample(NatArith.Power(2, m + 1)), (u: nat) => SampleTailRecursive(NatArith.Power(2, l - 1), u))(s); - { RelateWithTailRecursive(l - 1, m + 1, s); } - Model.Sample(NatArith.Power(2, m + l))(s); - } - } - } - -} diff --git a/src/Distributions/UniformPowerOfTwo/Implementation.dfy b/src/Distributions/UniformPowerOfTwo/Implementation.dfy index 0de1d9ce..ce81bfaf 100644 --- a/src/Distributions/UniformPowerOfTwo/Implementation.dfy +++ b/src/Distributions/UniformPowerOfTwo/Implementation.dfy @@ -6,7 +6,6 @@ module UniformPowerOfTwo.Implementation { import Monad import Model - import Equivalence import Interface trait {:termination false} Trait extends Interface.Trait { @@ -14,32 +13,6 @@ module UniformPowerOfTwo.Implementation { requires n >= 1 modifies this ensures Model.Sample(n)(old(s)) == Monad.Result(u, s) - { - u := 0; - var n' := n; - while n' > 1 - invariant n' >= 1 - invariant Equivalence.SampleTailRecursive(n)(old(s)) == Equivalence.SampleTailRecursive(n', u)(s) - { - var b := CoinSample(); - u := if b then 2*u + 1 else 2*u; - n' := n' / 2; - } - Equivalence.SampleCorrespondence(n, old(s)); - } - } - - method {:extern "UniformPowerOfTwo_mImplementation.DRandomUniformPowerOfTwo", "UniformPowerOfTwo"} ExternUniformPowerOfTwoSample(n: nat) returns (u: nat) - - trait {:termination false} TraitExtern extends Interface.Trait { - method UniformPowerOfTwoSample(n: nat) returns (u: nat) - requires n >= 1 - modifies this - ensures Model.Sample(n)(old(s)) == Monad.Result(u, s) - { - u := ExternUniformPowerOfTwoSample(n); - assume {:axiom} false; // assume correctness of extern implementation - } } } diff --git a/src/Distributions/UniformPowerOfTwo/Interface.dfy b/src/Distributions/UniformPowerOfTwo/Interface.dfy index c7c410ae..17f78c62 100644 --- a/src/Distributions/UniformPowerOfTwo/Interface.dfy +++ b/src/Distributions/UniformPowerOfTwo/Interface.dfy @@ -5,10 +5,11 @@ module UniformPowerOfTwo.Interface { import Monad - import Coin import Model + import Rand - trait {:termination false} Trait extends Coin.Interface.Trait { + trait {:termination false} Trait { + ghost var s: Rand.Bitstream // The return value u is uniformly distributed between 0 <= u < 2^k where 2^k <= n < 2^(k + 1). method UniformPowerOfTwoSample(n: nat) returns (u: nat) diff --git a/src/Distributions/UniformPowerOfTwo/Model.dfy b/src/Distributions/UniformPowerOfTwo/Model.dfy index 06b48d97..eed5ede3 100644 --- a/src/Distributions/UniformPowerOfTwo/Model.dfy +++ b/src/Distributions/UniformPowerOfTwo/Model.dfy @@ -10,6 +10,11 @@ module UniformPowerOfTwo.Model { import Monad import Independence import Loops + import NatArith + + /************ + Definitions + ************/ // Adapted from Definition 48 (see issue #79 for the reason of the modification) // The return value u is uniformly distributed between 0 <= u < 2^k where 2^k <= n < 2^(k + 1). @@ -30,4 +35,126 @@ module UniformPowerOfTwo.Model { function UnifStep(m: nat): Monad.Hurd { Monad.Bind(Monad.Coin, UnifStepHelper(m)) } + + + // A tail recursive version of Sample + function SampleTailRecursive(n: nat, u: nat := 0): Monad.Hurd + requires n >= 1 + { + (s: Rand.Bitstream) => + if n == 1 then + Monad.Result(u, s) + else + SampleTailRecursive(n / 2, if Rand.Head(s) then 2*u + 1 else 2*u)(Rand.Tail(s)) + } + + /******* + Lemmas + *******/ + + // Equivalence of Sample and its tail-recursive version + lemma SampleCorrespondence(n: nat, s: Rand.Bitstream) + requires n >= 1 + ensures SampleTailRecursive(n)(s) == Sample(n)(s) + { + if n == 1 { + reveal Sample(); + assert SampleTailRecursive(n)(s) == Sample(n)(s); + } else { + var k := NatArith.Log2Floor(n); + assert NatArith.Power(2, k) <= n < NatArith.Power(2, k + 1) by { NatArith.Power2OfLog2Floor(n); } + calc { + SampleTailRecursive(n)(s); + { SampleTailRecursiveEqualIfSameLog2Floor(n, NatArith.Power(2, k), k, 0, s); } + SampleTailRecursive(NatArith.Power(2, k))(s); + Monad.Bind(Sample(NatArith.Power(2, 0)), (u: nat) => SampleTailRecursive(NatArith.Power(2, k), u))(s); + { RelateWithTailRecursive(k, 0, s); } + Sample(NatArith.Power(2, k))(s); + { SampleEqualIfSameLog2Floor(n, NatArith.Power(2, k), k, s); } + Sample(n)(s); + } + } + } + + // All numbers between consecutive powers of 2 behave the same as arguments to SampleTailRecursive + lemma SampleTailRecursiveEqualIfSameLog2Floor(m: nat, n: nat, k: nat, u: nat, s: Rand.Bitstream) + requires m >= 1 + requires n >= 1 + requires NatArith.Power(2, k) <= m < NatArith.Power(2, k + 1) + requires NatArith.Power(2, k) <= n < NatArith.Power(2, k + 1) + ensures SampleTailRecursive(m, u)(s) == SampleTailRecursive(n, u)(s) + { + if k == 0 { + assert m == n; + } else { + assert 1 <= m; + assert 1 <= n; + calc { + SampleTailRecursive(m, u)(s); + SampleTailRecursive(m / 2, if Rand.Head(s) then 2*u + 1 else 2*u)(Rand.Tail(s)); + { SampleTailRecursiveEqualIfSameLog2Floor(m / 2, n / 2, k - 1, if Rand.Head(s) then 2*u + 1 else 2*u, Rand.Tail(s)); } + SampleTailRecursive(n / 2, if Rand.Head(s) then 2*u + 1 else 2*u)(Rand.Tail(s)); + SampleTailRecursive(n, u)(s); + } + } + } + + // All numbers between consecutive powers of 2 behave the same as arguments to Sample + lemma SampleEqualIfSameLog2Floor(m: nat, n: nat, k: nat, s: Rand.Bitstream) + requires m >= 1 + requires n >= 1 + requires NatArith.Power(2, k) <= m < NatArith.Power(2, k + 1) + requires NatArith.Power(2, k) <= n < NatArith.Power(2, k + 1) + ensures Sample(m)(s) == Sample(n)(s) + { + if k == 0 { + assert m == n; + } else { + assert 1 <= m; + assert 1 <= n; + calc { + Sample(m)(s); + { reveal Sample(); } + Monad.Bind(Sample(m / 2), UnifStep)(s); + { SampleEqualIfSameLog2Floor(m / 2, n / 2, k - 1, s); } + Monad.Bind(Sample(n / 2), UnifStep)(s); + { reveal Sample(); } + Sample(n)(s); + } + } + } + + // The induction invariant for the equivalence proof (generalized version of SampleCorrespondence) + lemma RelateWithTailRecursive(l: nat, m: nat, s: Rand.Bitstream) + decreases l + ensures Monad.Bind(Sample(NatArith.Power(2, m)), (u: nat) => SampleTailRecursive(NatArith.Power(2, l), u))(s) == Sample(NatArith.Power(2, m + l))(s) + { + if l == 0 { + calc { + Monad.Bind(Sample(NatArith.Power(2, m)), (u: nat) => SampleTailRecursive(NatArith.Power(2, l), u))(s); + (var Result(u, s') := Sample(NatArith.Power(2, m))(s); SampleTailRecursive(1, u)(s')); + Sample(NatArith.Power(2, m + l))(s); + } + } else { + assert LGreaterZero: NatArith.Power(2, l) >= 1 by { NatArith.PowerGreater0(2, l); } + assert MGreaterZero: NatArith.Power(2, m) >= 1 by { NatArith.PowerGreater0(2, m); } + assert L1GreaterZero: NatArith.Power(2, l - 1) >= 1 by { NatArith.PowerGreater0(2, l - 1); } + calc { + Monad.Bind(Sample(NatArith.Power(2, m)), (u: nat) => SampleTailRecursive(NatArith.Power(2, l), u))(s); + (var Result(u, s') := Sample(NatArith.Power(2, m))(s); SampleTailRecursive(NatArith.Power(2, l), u)(s')); + { reveal LGreaterZero; } + (var Result(u, s') := Sample(NatArith.Power(2, m))(s); + SampleTailRecursive(NatArith.Power(2, l) / 2, if Rand.Head(s') then 2 * u + 1 else 2 * u)(Rand.Tail(s'))); + { assert NatArith.Power(2, l) / 2 == NatArith.Power(2, l - 1); reveal L1GreaterZero; } + (var Result(u', s') := Monad.Bind(Sample(NatArith.Power(2, m)), UnifStep)(s); + SampleTailRecursive(NatArith.Power(2, l - 1), u')(s')); + { assert NatArith.Power(2, m + 1) / 2 == NatArith.Power(2, m); reveal Sample(); } + (var Result(u', s') := Sample(NatArith.Power(2, m + 1))(s); + SampleTailRecursive(NatArith.Power(2, l - 1), u')(s')); + Monad.Bind(Sample(NatArith.Power(2, m + 1)), (u: nat) => SampleTailRecursive(NatArith.Power(2, l - 1), u))(s); + { RelateWithTailRecursive(l - 1, m + 1, s); } + Sample(NatArith.Power(2, m + l))(s); + } + } + } } diff --git a/src/Math/Helper.dfy b/src/Math/Helper.dfy index c00eddb4..3acd5378 100644 --- a/src/Math/Helper.dfy +++ b/src/Math/Helper.dfy @@ -8,6 +8,20 @@ module Helper { Definitions ************/ + function NatToString(n: nat): string { + match n + case 0 => "0" case 1 => "1" case 2 => "2" case 3 => "3" case 4 => "4" + case 5 => "5" case 6 => "6" case 7 => "7" case 8 => "8" case 9 => "9" + case _ => NatToString(n / 10) + NatToString(n % 10) + } + + function SeqToString(xs: seq, printer: T -> string): string { + if |xs| == 0 then + "" + else + printer(xs[0]) + SeqToString(xs[1..], printer) + } + /******* Lemmas *******/ diff --git a/src/Math/Permutations.dfy b/src/Math/Permutations.dfy new file mode 100644 index 00000000..a26eee5c --- /dev/null +++ b/src/Math/Permutations.dfy @@ -0,0 +1,50 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +module Permutations { + import NatArith + + /************ + Definitions + ************/ + + function NumberOfPermutationsOf(s: seq): nat { + |CalculateAllPermutationsOf(s)| + } + + function CalculateAllPermutationsOf(s: seq): (x: set>) + ensures forall p | p in x :: |p| == |s| + { + if |s| == 0 then + {s} + else + set p, i | p in CalculateAllPermutationsOf(s[1..]) && 0 <= i <= |s|-1 :: InsertAt(p, s[0], i) + } + + function InsertAt(s: seq, x: T, i: nat): seq + requires i <= |s| + { + s[..i] + [x] + s[i..] + } + + /******* + Lemmas + *******/ + + lemma CalculateAllPermutationsOfIsNonEmpty(s: seq) + ensures s in CalculateAllPermutationsOf(s) + ensures NumberOfPermutationsOf(s) > 0 + { + assert s in CalculateAllPermutationsOf(s) by { + if |s| == 0 { + } else { + assert s[1..] in CalculateAllPermutationsOf(s[1..]) by { + CalculateAllPermutationsOfIsNonEmpty(s[1..]); + } + assert InsertAt(s[1..], s[0], 0) == s; + } + } + } +} \ No newline at end of file diff --git a/src/Util/FisherYates/Implementation.dfy b/src/Util/FisherYates/Implementation.dfy new file mode 100644 index 00000000..f35efd61 --- /dev/null +++ b/src/Util/FisherYates/Implementation.dfy @@ -0,0 +1,22 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +module FisherYates.Implementation { + import Interface + + trait {:termination false} Trait extends Interface.Trait { + + method Shuffle(a: array) + decreases * + modifies this, a + { + for i := 0 to a.Length { + var j := UniformIntervalSample(i, a.Length); + a[i], a[j] := a[j], a[i]; + } + } + + } +} \ No newline at end of file diff --git a/src/Util/FisherYates/Interface.dfy b/src/Util/FisherYates/Interface.dfy new file mode 100644 index 00000000..7375474d --- /dev/null +++ b/src/Util/FisherYates/Interface.dfy @@ -0,0 +1,16 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +module FisherYates.Interface { + import Uniform + + trait {:termination false} Trait extends Uniform.Interface.Trait { + + method Shuffle(a: array) + decreases * + modifies this, a + + } +} \ No newline at end of file diff --git a/src/interop/java/DRandomCoin.java b/src/interop/java/DRandomCoin.java deleted file mode 100644 index aa1213cf..00000000 --- a/src/interop/java/DRandomCoin.java +++ /dev/null @@ -1,24 +0,0 @@ -package Coin_mInterface; - -import java.security.SecureRandom; -import java.math.BigInteger; -import java.lang.Thread; - -public final class DRandomCoin { - - private static final ThreadLocal RNG = ThreadLocal.withInitial(DRandomCoin::createSecureRandom); - - private DRandomCoin() {} // Prevent instantiation - - private static final SecureRandom createSecureRandom() { - final SecureRandom rng = new SecureRandom(); - // Required for proper initialization - rng.nextBoolean(); - return rng; - } - - public static boolean Coin() { - return RNG.get().nextBoolean(); - } - -} \ No newline at end of file diff --git a/src/interop/java/Full/Random.java b/src/interop/java/Full/Random.java new file mode 100644 index 00000000..18eec74e --- /dev/null +++ b/src/interop/java/Full/Random.java @@ -0,0 +1,104 @@ +package DafnyVMC; + +import dafny.TypeDescriptor; +import java.math.BigInteger; +import java.security.SecureRandom; + +public class Random implements DafnyVMCTrait.RandomTrait { + static ThreadLocal rng; + + public Random() { + this.rng = ThreadLocal.withInitial(Random::createSecureRandom); + } + + public Random(SecureRandom rng) { + this.rng = ThreadLocal.withInitial(() -> rng); + } + + 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 java.math.BigInteger UniformIntervalSample(java.math.BigInteger a, java.math.BigInteger b) { + return Uniform.Interface._Companion_Trait.UniformIntervalSample(this, a, b); + } + + public java.math.BigInteger UniformSample(java.math.BigInteger n) { + return Uniform.Implementation._Companion_Trait.UniformSample(this, n); + } + + public boolean CoinSample() { + return Coin.Implementation._Companion_Trait.CoinSample(this); + } + + public boolean BernoulliSample(Rationals.Rational p) { + return Bernoulli.Implementation._Companion_Trait.BernoulliSample(this, p); + } + + public boolean BernoulliExpNegSampleCaseLe1(Rationals.Rational gamma) { + return BernoulliExpNeg.Implementation._Companion_Trait.BernoulliExpNegSampleCaseLe1(this, gamma); + } + + public boolean BernoulliExpNegSample(Rationals.Rational gamma) { + return BernoulliExpNeg.Implementation._Companion_Trait.BernoulliExpNegSample(this, gamma); + } + + public java.math.BigInteger DiscreteGaussianSample(Rationals.Rational sigma) { + return DiscreteGaussian.Implementation._Companion_Trait.DiscreteGaussianSample(this, sigma); + } + + public dafny.Tuple2 DiscreteLaplaceSampleLoop(Rationals.Rational scale) { + return DiscreteLaplace.Implementation._Companion_Trait.DiscreteLaplaceSampleLoop(this, scale); + } + + public java.math.BigInteger DisceteLaplaceSampleInnerLoop() { + return DiscreteLaplace.Implementation._Companion_Trait.DisceteLaplaceSampleInnerLoop(this); + } + + public java.math.BigInteger DiscreteLaplaceSample(Rationals.Rational scale) { + return DiscreteLaplace.Implementation._Companion_Trait.DiscreteLaplaceSample(this, scale); + } + + public <__T> void Shuffle(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a) { + FisherYates.Implementation._Companion_Trait.Shuffle(_td___T, this, a); + } + + public void Shuffle(BigInteger[] arr) { + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BIG_INTEGER, this, arr); + } + + public void Shuffle(int[] arr) { + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.INT, this, arr); + } + + public void Shuffle(String[] arr) { + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR_ARRAY, this, arr); + } + + public void Shuffle(char[] arr) { + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR, this, arr); + } + + public void Shuffle(boolean[] arr) { + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BOOLEAN, this, arr); + } + + public void Shuffle(long[] arr) { + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.LONG, this, arr); + } + + public void Shuffle(short[] arr) { + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.SHORT, this, arr); + } +} \ No newline at end of file diff --git a/src/interop/java/DRandomUniformPowerOfTwo.java b/src/interop/java/Part/Random.java similarity index 58% rename from src/interop/java/DRandomUniformPowerOfTwo.java rename to src/interop/java/Part/Random.java index b295c921..7a31b8d3 100644 --- a/src/interop/java/DRandomUniformPowerOfTwo.java +++ b/src/interop/java/Part/Random.java @@ -1,23 +1,23 @@ -package UniformPowerOfTwo_mImplementation; +package DafnyVMCPartMaterial; import java.security.SecureRandom; import java.math.BigInteger; import java.lang.Thread; -public final class DRandomUniformPowerOfTwo { +public final class Random { - private static final ThreadLocal RNG = ThreadLocal.withInitial(DRandomUniformPowerOfTwo::createSecureRandom); + private static final ThreadLocal RNG = ThreadLocal.withInitial(Random::createSecureRandom); - private DRandomUniformPowerOfTwo() {} // Prevent instantiation + private Random() {} // Prevent instantiation - private static final SecureRandom createSecureRandom() { + private static final SecureRandom createSecureRandom() { final SecureRandom rng = new SecureRandom(); // Required for proper initialization rng.nextBoolean(); return rng; } - public static BigInteger UniformPowerOfTwo(BigInteger n) { + public static BigInteger UniformPowerOfTwoSample(BigInteger n) { if (n.compareTo(BigInteger.ONE) < 0) { throw new IllegalArgumentException("n must be positive"); } diff --git a/tests/Tests.dfy b/tests/Tests.dfy index 03811dc6..5c745e32 100644 --- a/tests/Tests.dfy +++ b/tests/Tests.dfy @@ -13,19 +13,12 @@ module Tests { import DiscreteLaplace import DiscreteGaussian import NatArith + import RealArith + import Permutations + import FisherYates + import Helper - function Abs(x: real): real { - if x < 0.0 then -x else x - } - - function NatToString(n: nat): string { - match n - case 0 => "0" case 1 => "1" case 2 => "2" case 3 => "3" case 4 => "4" - case 5 => "5" case 6 => "6" case 7 => "7" case 8 => "8" case 9 => "9" - case _ => NatToString(n / 10) + NatToString(n % 10) - } - - method TestBernoulliIsWithin4SigmaOfTrueMean( + method TestBernoulliIsWithin3SigmaOfTrueMean( n: nat, empiricalSum: real, successProb: real, @@ -33,10 +26,10 @@ module Tests { ) requires n > 0 { - TestEmpiricalIsWithin4SigmaOfTrueMean(n, empiricalSum, successProb, successProb * (1.0 - successProb), description); + TestEmpiricalIsWithin3SigmaOfTrueMean(n, empiricalSum, successProb, successProb * (1.0 - successProb), description); } - method TestEmpiricalIsWithin4SigmaOfTrueMean( + method TestEmpiricalIsWithin3SigmaOfTrueMean( n: nat, empiricalSum: real, trueMean: real, @@ -46,17 +39,17 @@ module Tests { requires n > 0 { var empiricalMean := empiricalSum / n as real; - var diff := Abs(empiricalMean - trueMean); - var threshold := 4.0 * 4.0 * trueVariance / n as real; - if diff * diff >= threshold { + var diff := RealArith.Abs(empiricalMean - trueMean); + var threshold := 3.0 * 3.0 * trueVariance; + if diff * diff > threshold { print "Test failed: ", description, "\n"; print "True mean: ", trueMean, "\n"; print "Empirical mean: ", empiricalMean, "\n"; print "Difference between empirical and true mean: ", diff, "\n"; print "squared difference: ", diff * diff, "\n"; - print "sigma squared: ", trueVariance / n as real, "\n"; + print "sigma squared: ", trueVariance, "\n"; } - expect diff * diff < threshold, "Empirical mean should be within 3 sigma of true mean. This individual test may fail with probability of about 6.3e-5."; + expect diff * diff <= threshold, "Empirical mean should be within 3 sigma of true mean. This individual test may fail with probability of about 6.3e-5."; } method TestCoin(n: nat, r: Coin.Interface.Trait) @@ -70,7 +63,7 @@ module Tests { t := t + 1; } } - TestBernoulliIsWithin4SigmaOfTrueMean(n, t as real, 0.5, "p(true)"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, t as real, 0.5, "p(true)"); } method TestUniformPowerOfTwo(n: nat, u: nat, r: UniformPowerOfTwo.Interface.Trait) @@ -90,9 +83,9 @@ module Tests { sum := sum + l; } for i := 0 to NatArith.Power(2, k) { - TestBernoulliIsWithin4SigmaOfTrueMean(n, a[i] as real, 1.0 / (m as real), "p(" + NatToString(i) + ")"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, a[i] as real, 1.0 / (m as real), "p(" + Helper.NatToString(i) + ")"); } - TestEmpiricalIsWithin4SigmaOfTrueMean(n, sum as real, (m - 1) as real / 2.0, (m * m - 1) as real / 12.0, "mean of UniformPowerOfTwo(" + NatToString(u) + ")"); + TestEmpiricalIsWithin3SigmaOfTrueMean(n, sum as real, (m - 1) as real / 2.0, (m * m - 1) as real / 12.0, "mean of UniformPowerOfTwo(" + Helper.NatToString(u) + ")"); } method TestUniformPowerOfTwoMean(n: nat, u: nat, r: UniformPowerOfTwo.Interface.Trait) @@ -109,7 +102,7 @@ module Tests { expect 0 <= l < m, "sample not in the right bound"; sum := sum + l; } - TestEmpiricalIsWithin4SigmaOfTrueMean(n, sum as real, (m - 1) as real / 2.0, (m * m - 1) as real / 12.0, "mean of UniformPowerOfTwo(" + NatToString(u) + ")"); + TestEmpiricalIsWithin3SigmaOfTrueMean(n, sum as real, (m - 1) as real / 2.0, (m * m - 1) as real / 12.0, "mean of UniformPowerOfTwo(" + Helper.NatToString(u) + ")"); } method TestUniform(n: nat, u: nat, r: Uniform.Interface.Trait) @@ -128,9 +121,9 @@ module Tests { sum := sum + l; } for i := 0 to u { - TestBernoulliIsWithin4SigmaOfTrueMean(n, a[i] as real, 1.0 / (u as real), "p(" + NatToString(i) + ")"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, a[i] as real, 1.0 / (u as real), "p(" + Helper.NatToString(i) + ")"); } - TestEmpiricalIsWithin4SigmaOfTrueMean(n, sum as real, (u - 1) as real / 2.0, (u * u - 1) as real / 12.0, "mean of Uniform(" + NatToString(u) + ")"); + TestEmpiricalIsWithin3SigmaOfTrueMean(n, sum as real, (u - 1) as real / 2.0, (u * u - 1) as real / 12.0, "mean of Uniform(" + Helper.NatToString(u) + ")"); } method TestUniformMean(n: nat, u: nat, r: Uniform.Interface.Trait) @@ -146,7 +139,7 @@ module Tests { expect 0 <= l < u, "sample not in the right bound"; sum := sum + l; } - TestEmpiricalIsWithin4SigmaOfTrueMean(n, sum as real, (u - 1) as real / 2.0, (u * u - 1) as real / 12.0, "mean of Uniform(" + NatToString(u) + ")"); + TestEmpiricalIsWithin3SigmaOfTrueMean(n, sum as real, (u - 1) as real / 2.0, (u * u - 1) as real / 12.0, "mean of Uniform(" + Helper.NatToString(u) + ")"); } method TestUniformInterval(n: nat, r: Uniform.Interface.Trait) @@ -165,9 +158,9 @@ module Tests { case 9 => c := c + 1; } } - TestBernoulliIsWithin4SigmaOfTrueMean(n, a as real, 1.0 / 3.0, "p(7)"); - TestBernoulliIsWithin4SigmaOfTrueMean(n, b as real, 1.0 / 3.0, "p(8)"); - TestBernoulliIsWithin4SigmaOfTrueMean(n, c as real, 1.0 / 3.0, "p(9)"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, a as real, 1.0 / 3.0, "p(7)"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, b as real, 1.0 / 3.0, "p(8)"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, c as real, 1.0 / 3.0, "p(9)"); } method TestBernoulli(n: nat, r: Bernoulli.Interface.Trait) @@ -182,7 +175,7 @@ module Tests { t := t + 1; } } - TestBernoulliIsWithin4SigmaOfTrueMean(n, t as real, 0.2, "p(true)"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, t as real, 0.2, "p(true)"); } method TestBernoulli2(n: nat, r: Bernoulli.Interface.Trait) @@ -227,7 +220,7 @@ module Tests { t := t + 1; } } - TestBernoulliIsWithin4SigmaOfTrueMean(n, t as real, 0.1, "p(true)"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, t as real, 0.1, "p(true)"); } method TestDiscreteLaplace(n: nat, r: DiscreteLaplace.Interface.Trait) @@ -252,13 +245,13 @@ module Tests { // https://www.wolframalpha.com/input?i=ReplaceAll%5B%28E%5E%5B1%2Ft%5D+-+1%29+%2F+%28E%5E%5B1%2Ft%5D+%2B+1%29+*+E%5E%28-Abs%5Bx%5D%2Ft%29%2C+%7Bt+-%3E+7%2F5%2C+x+-%3E+0%7D%5D // https://www.wolframalpha.com/input?i=ReplaceAll%5B%28E%5E%5B1%2Ft%5D+-+1%29+%2F+%28E%5E%5B1%2Ft%5D+%2B+1%29+*+E%5E%28-Abs%5Bx%5D%2Ft%29%2C+%7Bt+-%3E+7%2F5%2C+x+-%3E+1%7D%5D // https://www.wolframalpha.com/input?i=ReplaceAll%5B%28E%5E%5B1%2Ft%5D+-+1%29+%2F+%28E%5E%5B1%2Ft%5D+%2B+1%29+*+E%5E%28-Abs%5Bx%5D%2Ft%29%2C+%7Bt+-%3E+7%2F5%2C+x+-%3E+2%7D%5D - TestBernoulliIsWithin4SigmaOfTrueMean(n, counts[0] as real, 0.3426949, "p(0)"); - TestBernoulliIsWithin4SigmaOfTrueMean(n, counts[1] as real, 0.1677634, "p(1)"); - TestBernoulliIsWithin4SigmaOfTrueMean(n, counts[-1] as real, 0.1677634, "p(-1)"); - TestBernoulliIsWithin4SigmaOfTrueMean(n, counts[2] as real, 0.0821272, "p(2)"); - TestBernoulliIsWithin4SigmaOfTrueMean(n, counts[-2] as real, 0.0821272, "p(-2)"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, counts[0] as real, 0.3426949, "p(0)"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, counts[1] as real, 0.1677634, "p(1)"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, counts[-1] as real, 0.1677634, "p(-1)"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, counts[2] as real, 0.0821272, "p(2)"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, counts[-2] as real, 0.0821272, "p(-2)"); var variance := 3.7575005; // variance of DiscreteLaplace(7/5) is (2*exp(5/7))/(exp(5/7)-1)^2 - TestEmpiricalIsWithin4SigmaOfTrueMean(n, sum as real, 0.0, variance, "mean"); + TestEmpiricalIsWithin3SigmaOfTrueMean(n, sum as real, 0.0, variance, "mean"); } method TestDiscreteGaussian(n: nat, r: DiscreteGaussian.Interface.Trait) @@ -283,12 +276,46 @@ module Tests { // 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 // 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+2%2C+%CF%83+-%3E+1.4%7D%5D - TestBernoulliIsWithin4SigmaOfTrueMean(n, counts[0] as real, 0.284959, "p(0)"); - TestBernoulliIsWithin4SigmaOfTrueMean(n, counts[1] as real, 0.220797, "p(1)"); - TestBernoulliIsWithin4SigmaOfTrueMean(n, counts[-1] as real, 0.220797, "p(-1)"); - TestBernoulliIsWithin4SigmaOfTrueMean(n, counts[2] as real, 0.102713, "p(2)"); - TestBernoulliIsWithin4SigmaOfTrueMean(n, counts[-2] as real, 0.102713, "p(-2)"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, counts[0] as real, 0.284959, "p(0)"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, counts[1] as real, 0.220797, "p(1)"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, counts[-1] as real, 0.220797, "p(-1)"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, counts[2] as real, 0.102713, "p(2)"); + TestBernoulliIsWithin3SigmaOfTrueMean(n, counts[-2] as real, 0.102713, "p(-2)"); var varianceBound := 1.4 * 1.4; // variance of DiscreteGaussian(1.4) is < 1.4^2 - TestEmpiricalIsWithin4SigmaOfTrueMean(n, sum as real, 0.0, varianceBound, "mean"); + TestEmpiricalIsWithin3SigmaOfTrueMean(n, sum as real, 0.0, varianceBound, "mean"); + } + + // Shuffles an array `a` n-times and verifies that for each permutation that occurs x-times, roughly x/n == 1/|Permutations.NumberOfPermutationsOf(a[..])| + method TestFisherYates(n: nat, a: array, r: FisherYates.Interface.Trait, printer: T -> string) + decreases * + modifies r + modifies a + requires n > 0 + { + var aAsSeq: seq := a[..]; + var numberOfPermutations: nat := Permutations.NumberOfPermutationsOf(aAsSeq); + var numberOfObservedPermutations: map, nat> := map[]; + Permutations.CalculateAllPermutationsOfIsNonEmpty(aAsSeq); + + for i := 0 to n { + var aCopy := a; + r.Shuffle(aCopy); + var aCopyAsSeq := aCopy[..]; + if aCopyAsSeq in numberOfObservedPermutations { + numberOfObservedPermutations := numberOfObservedPermutations[aCopyAsSeq := numberOfObservedPermutations[aCopyAsSeq] + 1]; + } else { + numberOfObservedPermutations := numberOfObservedPermutations[aCopyAsSeq := 1]; + } + } + + var items := numberOfObservedPermutations.Items; + + while items != {} + decreases |items| + { + var item :| item in items; + items := items - {item}; + TestBernoulliIsWithin3SigmaOfTrueMean(n, item.1 as real, 1.0 / (numberOfPermutations as real), "p(" + Helper.SeqToString(item.0, printer) + ")"); + } } } diff --git a/tests/TestsFoundational.dfy b/tests/TestsFoundational.dfy deleted file mode 100644 index 92b2dd06..00000000 --- a/tests/TestsFoundational.dfy +++ /dev/null @@ -1,108 +0,0 @@ -/******************************************************************************* - * Copyright by the contributors to the Dafny Project - * SPDX-License-Identifier: MIT - *******************************************************************************/ - -module TestsFoundational { - import NatArith - import DafnyVMC - import Tests - - method {:test} TestCoin() { - var r := new DafnyVMC.DRandomFoundational(); - Tests.TestCoin(1_000_000, r); - } - - method {:test} TestUniformPowerOfTwo_10() - decreases * - { - var r := new DafnyVMC.DRandomFoundational(); - Tests.TestUniformPowerOfTwo(1_000_000, 10, r); - } - - method {:test} TestUniformPowerOfTwo_100() - decreases * - { - var r := new DafnyVMC.DRandomFoundational(); - Tests.TestUniformPowerOfTwo(1_000_000, 100, r); - } - - // Test arguments that don't fit in 64 bits: - method {:test} TestUniformPowerOfTwoMean_10Pow100() - decreases * - { - var r := new DafnyVMC.DRandomFoundational(); - Tests.TestUniformPowerOfTwoMean(100_000, NatArith.Power(10, 100), r); - } - - method {:test} TestUniform_10() - decreases * - { - var r := new DafnyVMC.DRandomFoundational(); - Tests.TestUniform(1_000_000, 10, r); - } - - method {:test} TestUniform_100() - decreases * - { - var r := new DafnyVMC.DRandomFoundational(); - Tests.TestUniform(1_000_000, 100, r); - } - - // Test arguments that don't fit in 64 bits: - method {:test} TestUniformMean_10Pow100() - decreases * - { - var r := new DafnyVMC.DRandomFoundational(); - Tests.TestUniformMean(100_000, NatArith.Power(10, 100), r); - } - - method {:test} TestUniformInterval() - decreases * - { - var r := new DafnyVMC.DRandomFoundational(); - Tests.TestUniformInterval(1_000_000, r); - } - - method {:test} TestBernoulli() - decreases * - { - var r := new DafnyVMC.DRandomFoundational(); - Tests.TestBernoulli(1_000_000, r); - } - - method {:test} TestBernoulli2() - decreases * - { - var r := new DafnyVMC.DRandomFoundational(); - Tests.TestBernoulli2(1_000_000, r); - } - - method {:test} TestBernoulli3() - decreases * - { - var r := new DafnyVMC.DRandomFoundational(); - Tests.TestBernoulli3(1_000_000, r); - } - - method {:test} TestBernoulliExpNeg() - decreases * - { - var r := new DafnyVMC.DRandomFoundational(); - Tests.TestBernoulliExpNeg(1_000_000, r); - } - - method {:test} TestDiscreteLaplace() - decreases * - { - var r := new DafnyVMC.DRandomFoundational(); - Tests.TestDiscreteLaplace(1_000_000, r); - } - - method {:test} TestDiscreteGaussian() - decreases * - { - var r := new DafnyVMC.DRandomFoundational(); - Tests.TestDiscreteGaussian(1_000_000, r); - } -} diff --git a/tests/TestsExternUniformPowerOfTwo.dfy b/tests/TestsRandom.dfy similarity index 50% rename from tests/TestsExternUniformPowerOfTwo.dfy rename to tests/TestsRandom.dfy index a9620861..193dd501 100644 --- a/tests/TestsExternUniformPowerOfTwo.dfy +++ b/tests/TestsRandom.dfy @@ -3,27 +3,28 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -module TestsExternUniform { +module TestsRandom { import NatArith import DafnyVMC + import Helper import Tests method {:test} TestCoin() { - var r := new DafnyVMC.DRandomExternUniformPowerOfTwo(); + var r := new DafnyVMC.Random(); Tests.TestCoin(1_000_000, r); } method {:test} TestUniformPowerOfTwo_10() decreases * { - var r := new DafnyVMC.DRandomExternUniformPowerOfTwo(); + var r := new DafnyVMC.Random(); Tests.TestUniformPowerOfTwo(1_000_000, 10, r); } method {:test} TestUniformPowerOfTwo_100() decreases * { - var r := new DafnyVMC.DRandomExternUniformPowerOfTwo(); + var r := new DafnyVMC.Random(); Tests.TestUniformPowerOfTwo(1_000_000, 100, r); } @@ -31,21 +32,21 @@ module TestsExternUniform { method {:test} TestUniformPowerOfTwoMean_10Pow100() decreases * { - var r := new DafnyVMC.DRandomExternUniformPowerOfTwo(); + var r := new DafnyVMC.Random(); Tests.TestUniformPowerOfTwoMean(100_000, NatArith.Power(10, 100), r); } method {:test} TestUniform_10() decreases * { - var r := new DafnyVMC.DRandomExternUniformPowerOfTwo(); + var r := new DafnyVMC.Random(); Tests.TestUniform(1_000_000, 10, r); } method {:test} TestUniform_100() decreases * { - var r := new DafnyVMC.DRandomExternUniformPowerOfTwo(); + var r := new DafnyVMC.Random(); Tests.TestUniform(1_000_000, 100, r); } @@ -53,7 +54,7 @@ module TestsExternUniform { method {:test} TestUniformMean_10Pow100() decreases * { - var r := new DafnyVMC.DRandomExternUniformPowerOfTwo(); + var r := new DafnyVMC.Random(); Tests.TestUniformMean(100_000, NatArith.Power(10, 100), r); } @@ -61,49 +62,98 @@ module TestsExternUniform { method {:test} TestUniformInterval() decreases * { - var r := new DafnyVMC.DRandomExternUniformPowerOfTwo(); + var r := new DafnyVMC.Random(); Tests.TestUniformInterval(1_000_000, r); } method {:test} TestBernoulli() decreases * { - var r := new DafnyVMC.DRandomExternUniformPowerOfTwo(); + var r := new DafnyVMC.Random(); Tests.TestBernoulli(1_000_000, r); } method {:test} TestBernoulli2() decreases * { - var r := new DafnyVMC.DRandomExternUniformPowerOfTwo(); + var r := new DafnyVMC.Random(); Tests.TestBernoulli2(1_000_000, r); } method {:test} TestBernoulli3() decreases * { - var r := new DafnyVMC.DRandomExternUniformPowerOfTwo(); + var r := new DafnyVMC.Random(); Tests.TestBernoulli3(1_000_000, r); } method {:test} TestBernoulliExpNeg() decreases * { - var r := new DafnyVMC.DRandomExternUniformPowerOfTwo(); + var r := new DafnyVMC.Random(); Tests.TestBernoulliExpNeg(1_000_000, r); } method {:test} TestDiscreteLaplace() decreases * { - var r := new DafnyVMC.DRandomExternUniformPowerOfTwo(); + var r := new DafnyVMC.Random(); Tests.TestDiscreteLaplace(1_000_000, r); } method {:test} TestDiscreteGaussian() decreases * { - var r := new DafnyVMC.DRandomExternUniformPowerOfTwo(); + var r := new DafnyVMC.Random(); Tests.TestDiscreteGaussian(1_000_000, r); } + + method {:test} TestFisherYatesIdentity() + decreases * + { + var a: array := new nat[4](i => i); // [0, 1, 2, 3] + var r := new DafnyVMC.Random(); + Tests.TestFisherYates(1_000_000, a, r, Helper.NatToString); + } + + method {:test} TestFisherYatesConstant() + decreases * + { + var a: array := new nat[4](i => 0); // [0, 0, 0, 0] + var r := new DafnyVMC.Random(); + Tests.TestFisherYates(1_000_000, a, r, Helper.NatToString); + } + + method {:test} TestFisherYatesMixed() + decreases * + { + var a: array := new nat[] [0, 1, 1, 2]; // [0, 1, 1, 2] + var r := new DafnyVMC.Random(); + Tests.TestFisherYates(1_000_000, a, r, Helper.NatToString); + } + + method {:test} TestFisherYatesLengthZero() + decreases * + { + var a: array := new nat[] []; // length 0 + var r := new DafnyVMC.Random(); + Tests.TestFisherYates(1_000_000, a, r, Helper.NatToString); + } + + method {:test} TestFisherYatesLengthOne() + decreases * + { + var a: array := new nat[] [0]; // length 1 + var r := new DafnyVMC.Random(); + Tests.TestFisherYates(1_000_000, a, r, Helper.NatToString); + } + + method {:test} TestFisherYatesLengthEven() + decreases * + { + var a: array := new nat[] [2, 1, 18, 2, 3, 4]; // length 6 + var r := new DafnyVMC.Random(); + Tests.TestFisherYates(1_000_000, a, r, Helper.NatToString); + } + }