diff --git a/build/java/run_samplers.sh b/build/java/run_samplers.sh index 5354cb89..98dc3d55 100755 --- a/build/java/run_samplers.sh +++ b/build/java/run_samplers.sh @@ -1,3 +1,4 @@ #1/bin/bash -java -classpath build/java/DafnyVMC.jar docs/java/TestSamplers.java \ No newline at end of file +java -classpath build/java/DafnyVMC.jar docs/java/TestSamplers.java +java -classpath build/java/DafnyVMC.jar docs/java/CustomTestSamplers.java \ No newline at end of file diff --git a/build/java/run_shuffling.sh b/build/java/run_shuffling.sh index 5f5e14cf..1d7e0954 100755 --- a/build/java/run_shuffling.sh +++ b/build/java/run_shuffling.sh @@ -1,3 +1,4 @@ #1/bin/bash -java -classpath build/java/DafnyVMC.jar docs/java/TestShuffling.java \ No newline at end of file +java -classpath build/java/DafnyVMC.jar docs/java/TestShuffling.java +java -classpath build/java/DafnyVMC.jar docs/java/CustomTestShuffling.java \ No newline at end of file diff --git a/build/py/run_samplers.sh b/build/py/run_samplers.sh index e27e2b6d..24264a03 100755 --- a/build/py/run_samplers.sh +++ b/build/py/run_samplers.sh @@ -1,3 +1,4 @@ #1/bin/bash -PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestSamplers.py \ No newline at end of file +PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestSamplers.py +PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/CustomTestSamplers.py \ No newline at end of file diff --git a/build/py/run_shuffling.sh b/build/py/run_shuffling.sh index a1eaf731..bb7db895 100755 --- a/build/py/run_shuffling.sh +++ b/build/py/run_shuffling.sh @@ -1,3 +1,4 @@ #1/bin/bash -PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestShuffling.py \ No newline at end of file +PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestShuffling.py +PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/CustomTestShuffling.py \ No newline at end of file diff --git a/docs/java/CustomTestSamplers.java b/docs/java/CustomTestSamplers.java new file mode 100644 index 00000000..3d34d0bd --- /dev/null +++ b/docs/java/CustomTestSamplers.java @@ -0,0 +1,116 @@ +import java.security.SecureRandom; +import java.math.BigInteger; +import java.util.Arrays; + +import DafnyVMC.Random; + +class CustomTestSamplers { + + public static void main(String[] args) { + + /* STANDARD RNG */ + System.out.println("\n STANDARD RNG TESTS WITH CUSTOM UNIFORM\n"); + + DafnyVMC.CustomRandom r = new DafnyVMC.CustomRandom(); + + 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 WITH CUSTOM UNIFORM\n"); + + SecureRandom rng = new SecureRandom(); + DafnyVMC.CustomRandom t = new DafnyVMC.CustomRandom(() -> 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/CustomTestShuffling.java b/docs/java/CustomTestShuffling.java new file mode 100644 index 00000000..e5642287 --- /dev/null +++ b/docs/java/CustomTestShuffling.java @@ -0,0 +1,85 @@ +import java.security.SecureRandom; +import java.math.BigInteger; +import java.util.Arrays; + +import DafnyVMC.Random; + +class CustomTestShuffling { + public static void main(String[] args) { + 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}; + + + /* STANDARD RNG */ + System.out.println("\nSTANDARD RNG TESTS WITH CUSTOM UNIFORM\n"); + + DafnyVMC.CustomRandom r = new DafnyVMC.CustomRandom(); + + 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 WITH CUSTOM UNIFORM\n"); + + SecureRandom rng = new SecureRandom(); + DafnyVMC.CustomRandom t = new DafnyVMC.CustomRandom(() -> rng); + + 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/docs/py/CustomTestSamplers.py b/docs/py/CustomTestSamplers.py new file mode 100644 index 00000000..0c683094 --- /dev/null +++ b/docs/py/CustomTestSamplers.py @@ -0,0 +1,49 @@ +import DafnyVMC + +def main(): + + # STANDARD RNG + print("\nSTANDARD RNG TESTS WITH CUSTOM UNIFORM \n") + + r = DafnyVMC.CustomRandom() + + 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/CustomTestShuffling.py b/docs/py/CustomTestShuffling.py new file mode 100644 index 00000000..62e4d832 --- /dev/null +++ b/docs/py/CustomTestShuffling.py @@ -0,0 +1,36 @@ +import DafnyVMC + +def main(): + arr1 = [0, 1, 2] + arr2 = [float(0), float(1), float(2)] + arr3 = ["aa", "bb", "cc"] + arr4 = ['a', 'b', 'c'] + arr5 = [True, False, False, True] + + # STANDARD RNG + print("\nSTANDARD RNG TESTS WITH CUSTOM UNIFORM\n") + + r = DafnyVMC.CustomRandom() + + print("Example of Fisher-Yates: int") + arr1 = r.Shuffle(arr1) + print(arr1) + + print("Example of Fisher-Yates: float") + arr2 = r.Shuffle(arr2) + print(arr2) + + print("Example of Fisher-Yates: str") + arr3 = r.Shuffle(arr3) + print(arr3) + + print("Example of Fisher-Yates: char/str") + arr4 = r.Shuffle(arr4) + print(arr4) + + print("Example of Fisher-Yates: boolean") + arr5 = r.Shuffle(arr5) + print(arr5) + +if __name__ == "__main__": + main() \ No newline at end of file diff --git a/scripts/build.sh b/scripts/build.sh index 4f44749a..f52f9d08 100755 --- a/scripts/build.sh +++ b/scripts/build.sh @@ -14,4 +14,9 @@ then exit 1 fi -$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 +if [ "$TARGET_LANG" = "java" ] +then + $DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Full/CustomRandom.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG -o build/$TARGET_LANG/DafnyVMC dfyconfig.toml --no-verify +else + $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 +fi diff --git a/src/DafnyVMCTrait.dfy b/src/DafnyVMCTrait.dfy index e9b560f5..2d6c2e6e 100644 --- a/src/DafnyVMCTrait.dfy +++ b/src/DafnyVMCTrait.dfy @@ -7,7 +7,7 @@ module DafnyVMCTrait { import opened Pos - trait {:termination false} RandomTrait extends UniformPowerOfTwo.Interface.Trait, FisherYates.Implementation.Trait { + trait {:termination false} RandomTrait extends UniformPowerOfTwo.Interface.Trait, FisherYates.Implementation.Trait { method {:verify false} UniformSample (n: pos) returns (o: nat) diff --git a/src/interop/java/Full/CustomRandom.java b/src/interop/java/Full/CustomRandom.java new file mode 100644 index 00000000..e96c7aac --- /dev/null +++ b/src/interop/java/Full/CustomRandom.java @@ -0,0 +1,38 @@ +package DafnyVMC; + +import dafny.TypeDescriptor; +import java.math.BigInteger; +import java.security.SecureRandom; +import java.util.function.Supplier; + +public class CustomRandom extends Random { + public CustomRandom() { + this.rng = ThreadLocal.withInitial(CustomRandom::createSecureRandom); + } + + public CustomRandom(Supplier supplier) { + this.rng = ThreadLocal.withInitial(supplier); + } + + private static final SecureRandom createSecureRandom() { + final SecureRandom rng = new SecureRandom(); + // Required for proper initialization + rng.nextBoolean(); + return rng; + } + + @Override + public java.math.BigInteger UniformSample(java.math.BigInteger n) { + if (n.compareTo(BigInteger.ONE) < 0) { + throw new IllegalArgumentException("n must be positive"); + } + + BigInteger sampleValue; + do { + sampleValue = UniformPowerOfTwoSample(n); + } while (sampleValue.compareTo(n) >= 0); + + return sampleValue; + } + +} \ No newline at end of file diff --git a/src/interop/py/Full/Random.py b/src/interop/py/Full/Random.py index 286abdbd..e1bd2dd3 100644 --- a/src/interop/py/Full/Random.py +++ b/src/interop/py/Full/Random.py @@ -15,3 +15,7 @@ def Shuffle(self, xs): a = ArrayFromList(xs) DafnyVMCPart.Random.Shuffle(self, a) return list(a) + +class CustomRandom(Random): + def UniformSample(self, n): + return secrets.randbelow(n) \ No newline at end of file