From 6bcf55dc4d0158a1b06a3b9e1a245e1d13ff46d3 Mon Sep 17 00:00:00 2001 From: John Tristan Date: Thu, 29 Feb 2024 11:50:06 -0500 Subject: [PATCH 1/2] Improved loop for parameters of Bernoulli expneg greater than 1 (#157) 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). --- src/DafnyVMCTrait.dfy | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/DafnyVMCTrait.dfy b/src/DafnyVMCTrait.dfy index cf60dfd0..ab198d06 100644 --- a/src/DafnyVMCTrait.dfy +++ b/src/DafnyVMCTrait.dfy @@ -83,8 +83,12 @@ module DafnyVMCTrait { o := true; } else { var B := BernoulliExpNegSampleUnit(1, 1); - var R := BernoulliExpNegSampleGenLoop(iter - 1); - o := B == true && R == true; + if ! (B == true) { + o := B; + } else { + var R := BernoulliExpNegSampleGenLoop(iter - 1); + o := R; + } } } From a2f6207183346ffbc8a04a7521fa6d8b4c50c40f Mon Sep 17 00:00:00 2001 From: Stefan Zetzsche <120379523+stefan-aws@users.noreply.github.com> Date: Thu, 29 Feb 2024 19:55:51 +0000 Subject: [PATCH 2/2] Additional testing (#158) 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). --- .github/workflows/build_java.yml | 3 +- .github/workflows/build_py.yml | 3 +- build/java/run.sh | 3 - build/java/run_samplers.sh | 3 + build/java/run_shuffling.sh | 3 + build/py/run.sh | 3 - build/py/run_samplers.sh | 3 + build/py/run_shuffling.sh | 3 + docs/java/TestSamplers.java | 116 ++++++++++++++++++ .../{BuildTest.java => TestShuffling.java} | 37 +----- docs/py/TestSamplers.py | 49 ++++++++ docs/py/{BuildTest.py => TestShuffling.py} | 17 --- 12 files changed, 184 insertions(+), 59 deletions(-) delete mode 100755 build/java/run.sh create mode 100755 build/java/run_samplers.sh create mode 100755 build/java/run_shuffling.sh delete mode 100755 build/py/run.sh create mode 100755 build/py/run_samplers.sh create mode 100755 build/py/run_shuffling.sh create mode 100644 docs/java/TestSamplers.java rename docs/java/{BuildTest.java => TestShuffling.java} (66%) create mode 100644 docs/py/TestSamplers.py rename docs/py/{BuildTest.py => TestShuffling.py} (62%) diff --git a/.github/workflows/build_java.yml b/.github/workflows/build_java.yml index c8a13168..0138e326 100644 --- a/.github/workflows/build_java.yml +++ b/.github/workflows/build_java.yml @@ -12,4 +12,5 @@ jobs: - uses: actions/checkout@v4 - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny TARGET_LANG=java bash scripts/build.sh - - run: build/java/run.sh + - run: build/java/run_samplers.sh + - run: build/java/run_shuffling.sh diff --git a/.github/workflows/build_py.yml b/.github/workflows/build_py.yml index 88f8329e..229aacbe 100644 --- a/.github/workflows/build_py.yml +++ b/.github/workflows/build_py.yml @@ -12,4 +12,5 @@ jobs: - uses: actions/checkout@v4 - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny TARGET_LANG=py bash scripts/build.sh - - run: build/py/run.sh + - run: build/py/run_samplers.sh + - run: build/py/run_shuffling.sh diff --git a/build/java/run.sh b/build/java/run.sh deleted file mode 100755 index ff6bdcad..00000000 --- a/build/java/run.sh +++ /dev/null @@ -1,3 +0,0 @@ -#1/bin/bash - -java -classpath build/java/DafnyVMC.jar docs/java/BuildTest.java \ No newline at end of file diff --git a/build/java/run_samplers.sh b/build/java/run_samplers.sh new file mode 100755 index 00000000..5354cb89 --- /dev/null +++ b/build/java/run_samplers.sh @@ -0,0 +1,3 @@ +#1/bin/bash + +java -classpath build/java/DafnyVMC.jar docs/java/TestSamplers.java \ No newline at end of file diff --git a/build/java/run_shuffling.sh b/build/java/run_shuffling.sh new file mode 100755 index 00000000..5f5e14cf --- /dev/null +++ b/build/java/run_shuffling.sh @@ -0,0 +1,3 @@ +#1/bin/bash + +java -classpath build/java/DafnyVMC.jar docs/java/TestShuffling.java \ No newline at end of file diff --git a/build/py/run.sh b/build/py/run.sh deleted file mode 100755 index ca896e6e..00000000 --- a/build/py/run.sh +++ /dev/null @@ -1,3 +0,0 @@ -#1/bin/bash - -PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/BuildTest.py \ No newline at end of file diff --git a/build/py/run_samplers.sh b/build/py/run_samplers.sh new file mode 100755 index 00000000..e27e2b6d --- /dev/null +++ b/build/py/run_samplers.sh @@ -0,0 +1,3 @@ +#1/bin/bash + +PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestSamplers.py \ No newline at end of file diff --git a/build/py/run_shuffling.sh b/build/py/run_shuffling.sh new file mode 100755 index 00000000..a1eaf731 --- /dev/null +++ b/build/py/run_shuffling.sh @@ -0,0 +1,3 @@ +#1/bin/bash + +PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestShuffling.py \ No newline at end of file diff --git a/docs/java/TestSamplers.java b/docs/java/TestSamplers.java new file mode 100644 index 00000000..212e812b --- /dev/null +++ b/docs/java/TestSamplers.java @@ -0,0 +1,116 @@ +import java.security.SecureRandom; +import java.math.BigInteger; +import java.util.Arrays; + +import DafnyVMC.Random; + +class TestSamplers { + + public static void main(String[] args) { + + /* STANDARD RNG */ + System.out.println("\nSTANDARD RNG TESTS\n"); + + DafnyVMC.Random r = new DafnyVMC.Random(); + + for (int a = 1; a < 1000; a++) { + BigInteger i = BigInteger.valueOf(a); + + System.out.println("Testing Uniform(" + a + ")"); + System.out.println(r.UniformSample(i)); + + for (int b = 1; b <= 1000; b++) { + BigInteger j = BigInteger.valueOf(b); + + System.out.println("Testing Bernoulli(" + a + "/" + b + ")"); + System.out.println(r.BernoulliSample(i, j)); + + System.out.println("Testing BernoulliExpNeg(" + a + "/" + b + ")"); + System.out.println(r.BernoulliExpNegSample(i, j)); + + System.out.println("Testing DiscreteGaussian(" + a + "/" + b + ")"); + System.out.println(r.DiscreteGaussianSample(i, j)); + + System.out.println("Testing DiscreteLaPlace(" + a + "/" + b + ")"); + System.out.println(r.DiscreteLaplaceSample(i, j)); + } + } + + // Edge cases + + BigInteger k = BigInteger.valueOf(1000000); + BigInteger l = BigInteger.valueOf(1); + + System.out.println("Testing Bernoulli(1000000, 1)"); + System.out.println(r.BernoulliSample(k, l)); + System.out.println("Testing Bernoulli(1, 1000000)"); + System.out.println(r.BernoulliSample(l, k)); + + System.out.println("Testing BernoulliExpNeg(1000000, 1)"); + System.out.println(r.BernoulliExpNegSample(k, l)); + System.out.println("Testing BernoulliExpNeg(1, 1000000)"); + System.out.println(r.BernoulliExpNegSample(l, k)); + + System.out.println("Testing DiscreteGaussianSample(1000000, 1)"); + System.out.println(r.DiscreteGaussianSample(k, l)); + System.out.println("Testing DiscreteGaussianSample(1, 1000000)"); + System.out.println(r.DiscreteGaussianSample(l, k)); + + System.out.println("Testing DiscreteLaplace(1000000, 1)"); + System.out.println(r.DiscreteLaplaceSample(k, l)); + System.out.println("Testing DiscreteLaplace(1, 1000000)"); + System.out.println(r.DiscreteLaplaceSample(l, k)); + + /* CUSTOM RNG */ + System.out.println("\nCUSTOM RNG TESTS\n"); + + SecureRandom rng = new SecureRandom(); + DafnyVMC.Random t = new DafnyVMC.Random(() -> rng); + + for (int a = 1; a < 1000; a++) { + BigInteger i = BigInteger.valueOf(a); + System.out.println("Testing Uniform(" + a + ")"); + System.out.println(t.UniformSample(i)); + + for (int b = 1; b <= 1000; b++) { + BigInteger j = BigInteger.valueOf(b); + System.out.println("Testing Bernoulli(" + a + "/" + b + ")"); + System.out.println(t.BernoulliSample(i, j)); + + System.out.println("Testing BernoulliExpNeg(" + a + "/" + b + ")"); + System.out.println(t.BernoulliExpNegSample(i, j)); + + System.out.println("Testing DiscreteGaussian(" + a + "/" + b + ")"); + System.out.println(t.DiscreteGaussianSample(i, j)); + + System.out.println("Testing DiscreteLaPlace(" + a + "/" + b + ")"); + System.out.println(t.DiscreteLaplaceSample(i, j)); + } + } + + + // Edge cases + + System.out.println("Testing Bernoulli(1000000, 1)"); + System.out.println(t.BernoulliSample(k, l)); + System.out.println("Testing Bernoulli(1, 1000000)"); + System.out.println(t.BernoulliSample(l, k)); + + System.out.println("Testing BernoulliExpNeg(1000000, 1)"); + System.out.println(t.BernoulliExpNegSample(k, l)); + System.out.println("Testing BernoulliExpNeg(1, 1000000)"); + System.out.println(t.BernoulliExpNegSample(l, k)); + + System.out.println("Testing DiscreteGaussianSample(1000000, 1)"); + System.out.println(t.DiscreteGaussianSample(k, l)); + System.out.println("Testing DiscreteGaussianSample(1, 1000000)"); + System.out.println(t.DiscreteGaussianSample(l, k)); + + System.out.println("Testing DiscreteLaplace(1000000, 1)"); + System.out.println(t.DiscreteLaplaceSample(k, l)); + System.out.println("Testing DiscreteLaplace(1, 1000000)"); + System.out.println(t.DiscreteLaplaceSample(l, k)); + + + } +} \ No newline at end of file diff --git a/docs/java/BuildTest.java b/docs/java/TestShuffling.java similarity index 66% rename from docs/java/BuildTest.java rename to docs/java/TestShuffling.java index 2c64a04d..3574d94e 100644 --- a/docs/java/BuildTest.java +++ b/docs/java/TestShuffling.java @@ -4,7 +4,7 @@ import DafnyVMC.Random; -class Check { +class TestShuffling { public static void main(String[] args) { BigInteger[] arr1 = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)}; int[] arr2 = {0, 1, 2}; @@ -13,28 +13,12 @@ public static void main(String[] args) { boolean[] arr5 = {true, false, false, true}; long[] arr6 = {111111L, 333333L, 999999L}; short[] arr7 = {-3, 0, 3}; - BigInteger num = BigInteger.valueOf(3); - BigInteger den = BigInteger.valueOf(5); + /* STANDARD RNG */ System.out.println("\nSTANDARD RNG TESTS\n"); - - DafnyVMC.Random r = new DafnyVMC.Random(); - - 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(num,den)); - - System.out.println("Example of BernoulliExpNeg sampling"); - System.out.println(r.BernoulliExpNegSample(num,den)); - - System.out.println("Example of DiscreteGaussian sampling"); - System.out.println(r.DiscreteGaussianSample(num,den)); - System.out.println("Example of DiscreteLaplace sampling"); - System.out.println(r.DiscreteLaplaceSample(num,den)); + DafnyVMC.Random r = new DafnyVMC.Random(); System.out.println("Example of Fisher-Yates: BigInteger"); r.Shuffle(arr1); @@ -70,21 +54,6 @@ public static void main(String[] args) { SecureRandom rng = new SecureRandom(); DafnyVMC.Random t = new DafnyVMC.Random(() -> rng); - 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(num,den)); - - System.out.println("Example of BernoulliExpNeg sampling"); - System.out.println(r.BernoulliExpNegSample(num,den)); - - System.out.println("Example of DiscreteGaussian sampling"); - System.out.println(t.DiscreteGaussianSample(num,den)); - - System.out.println("Example of DiscreteLaplace sampling"); - System.out.println(t.DiscreteLaplaceSample(num,den)); - System.out.println("Example of Fisher-Yates: BigInteger"); t.Shuffle(arr1); System.out.println(Arrays.toString(arr1)); diff --git a/docs/py/TestSamplers.py b/docs/py/TestSamplers.py new file mode 100644 index 00000000..c46642a7 --- /dev/null +++ b/docs/py/TestSamplers.py @@ -0,0 +1,49 @@ +import DafnyVMC + +def main(): + + # STANDARD RNG + print("\nSTANDARD RNG TESTS\n") + + r = DafnyVMC.Random() + + for i in range(1, 1000): + print("Testing Uniform("+str(i)+")") + print(r.UniformSample(i)) + + for j in range(1, 1000): + print("Testing Bernoulli("+str(i)+"/"+str(j)+")\n") + print(r.BernoulliSample(i, j), end="\n") + + print("Testing BernoulliExpNeg("+str(i)+"/"+str(j)+")\n") + print(r.BernoulliExpNegSample(i, j), end="\n") + + print("Testing DiscreteGaussian("+str(i)+"/"+str(j)+")\n") + print(r.DiscreteGaussianSample(i, j), end="\n") + + print("Testing DiscreteLaPlace("+str(i)+"/"+str(j)+")\n") + print(r.DiscreteLaplaceSample(i, j), end="\n") + + # Edge cases + print("Testing Bernoulli(1000000, 1)\n") + print(r.BernoulliSample(1000000, 1), end="\n") + print("Testing Bernoulli(1, 1000000)\n") + print(r.BernoulliSample(1, 1000000), end="\n") + + print("Testing BernoulliExpNeg(1000000, 1)\n") + print(r.BernoulliExpNegSample(1000000, 1), end="\n") + print("Testing BernoulliExpNeg(1, 1000000)\n") + print(r.BernoulliExpNegSample(1, 1000000), end="\n") + + print("Testing DiscreteGaussianSample(1000000, 1)\n") + print(r.DiscreteGaussianSample(1000000, 1), end="\n") + print("Testing DiscreteGaussianSample(1, 1000000)\n") + print(r.DiscreteGaussianSample(1, 1000000), end="\n") + + print("Testing DiscreteLaplace(1000000, 1)\n") + print(r.DiscreteLaplaceSample(1000000, 1), end="\n") + print("Testing DiscreteLaplace(1, 1000000)\n") + print(r.DiscreteLaplaceSample(1, 1000000), end="\n") + +if __name__ == "__main__": + main() \ No newline at end of file diff --git a/docs/py/BuildTest.py b/docs/py/TestShuffling.py similarity index 62% rename from docs/py/BuildTest.py rename to docs/py/TestShuffling.py index 0d9ee953..b00e2037 100644 --- a/docs/py/BuildTest.py +++ b/docs/py/TestShuffling.py @@ -6,29 +6,12 @@ def main(): arr3 = ["aa", "bb", "cc"] arr4 = ['a', 'b', 'c'] arr5 = [True, False, False, True] - num = 3 - den = 5 # STANDARD RNG print("\nSTANDARD RNG TESTS\n") r = DafnyVMC.Random() - print("Example of Uniform sampling") - print(r.UniformSample(4)) - - print("Example of Bernoulli sampling") - print(r.BernoulliSample(num,den)) - - print("Example of BernoulliExpNeg sampling") - print(r.BernoulliExpNegSample(num,den)) - - print("Example of DiscreteGaussian sampling") - print(r.DiscreteGaussianSample(num,den)) - - print("Example of DiscreteLaplace sampling") - print(r.DiscreteLaplaceSample(num,den)) - print("Example of Fisher-Yates: int") arr1 = r.Shuffle(arr1) print(arr1)