From 878dbe0a7471f22721908f0f6a5cc5784b12ad1a Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Tue, 12 Mar 2024 18:05:56 +0000 Subject: [PATCH] working example --- audit.log | 1 + build/java/run_samplers.sh | 3 +- build/java/run_shuffling.sh | 2 +- docs/java/CustomTestSamplers.java | 116 ------------------ ...estShuffling.java => TestShuffling32.java} | 34 ++--- docs/py/CustomTestSamplers.py | 49 -------- ...tomTestShuffling.py => TestShuffling32.py} | 12 +- scripts/build.sh | 2 +- src/DafnyVMC.dfy | 15 +++ src/DafnyVMCTrait.dfy | 2 +- src/Util/FisherYates/Interface.dfy | 2 +- src/interop/java/Full/CustomRandom.java | 38 ------ src/interop/java/Full/Random.java | 56 ++++++++- src/interop/java/Part/Random.java | 8 ++ src/interop/py/Full/Random.py | 8 +- src/interop/py/Part/Random.py | 5 +- 16 files changed, 113 insertions(+), 240 deletions(-) delete mode 100644 docs/java/CustomTestSamplers.java rename docs/java/{CustomTestShuffling.java => TestShuffling32.java} (82%) delete mode 100644 docs/py/CustomTestSamplers.py rename docs/py/{CustomTestShuffling.py => TestShuffling32.py} (78%) delete mode 100644 src/interop/java/Full/CustomRandom.java diff --git a/audit.log b/audit.log index ffd63227..5bda4eaf 100644 --- a/audit.log +++ b/audit.log @@ -1,2 +1,3 @@ +src/DafnyVMC.dfy(35,27): UniformSample32: Declaration has `{:verify false}` attribute. src/Distributions/Uniform/Model.dfy(19,26): Sample: Declaration has explicit `{:axiom}` attribute. src/ProbabilisticProgramming/RandomSource.dfy(50,17): ProbIsProbabilityMeasure: Declaration has explicit `{:axiom}` attribute. diff --git a/build/java/run_samplers.sh b/build/java/run_samplers.sh index 98dc3d55..5354cb89 100755 --- a/build/java/run_samplers.sh +++ b/build/java/run_samplers.sh @@ -1,4 +1,3 @@ #1/bin/bash -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 +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 index 1d7e0954..458da12e 100755 --- a/build/java/run_shuffling.sh +++ b/build/java/run_shuffling.sh @@ -1,4 +1,4 @@ #1/bin/bash 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 +java -classpath build/java/DafnyVMC.jar docs/java/TestShuffling32.java \ No newline at end of file diff --git a/docs/java/CustomTestSamplers.java b/docs/java/CustomTestSamplers.java deleted file mode 100644 index 3d34d0bd..00000000 --- a/docs/java/CustomTestSamplers.java +++ /dev/null @@ -1,116 +0,0 @@ -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/TestShuffling32.java similarity index 82% rename from docs/java/CustomTestShuffling.java rename to docs/java/TestShuffling32.java index e5642287..8fe8673c 100644 --- a/docs/java/CustomTestShuffling.java +++ b/docs/java/TestShuffling32.java @@ -4,7 +4,7 @@ import DafnyVMC.Random; -class CustomTestShuffling { +class TestShuffling32 { public static void main(String[] args) { BigInteger[] arr1 = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)}; int[] arr2 = {0, 1, 2}; @@ -18,68 +18,68 @@ public static void main(String[] args) { /* STANDARD RNG */ System.out.println("\nSTANDARD RNG TESTS WITH CUSTOM UNIFORM\n"); - DafnyVMC.CustomRandom r = new DafnyVMC.CustomRandom(); + DafnyVMC.Random r = new DafnyVMC.Random(); System.out.println("Example of Fisher-Yates: BigInteger"); - r.Shuffle(arr1); + r.Shuffle32(arr1); System.out.println(Arrays.toString(arr1)); System.out.println("Example of Fisher-Yates: int"); - r.Shuffle(arr2); + r.Shuffle32(arr2); System.out.println(Arrays.toString(arr2)); System.out.println("Example of Fisher-Yates: String"); - r.Shuffle(arr3); + r.Shuffle32(arr3); System.out.println(Arrays.toString(arr3)); System.out.println("Example of Fisher-Yates: char"); - r.Shuffle(arr4); + r.Shuffle32(arr4); System.out.println(Arrays.toString(arr4)); System.out.println("Example of Fisher-Yates: boolean"); - r.Shuffle(arr5); + r.Shuffle32(arr5); System.out.println(Arrays.toString(arr5)); System.out.println("Example of Fisher-Yates: long"); - r.Shuffle(arr6); + r.Shuffle32(arr6); System.out.println(Arrays.toString(arr6)); System.out.println("Example of Fisher-Yates: short"); - r.Shuffle(arr7); + r.Shuffle32(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); + DafnyVMC.Random t = new DafnyVMC.Random(() -> rng); System.out.println("Example of Fisher-Yates: BigInteger"); - t.Shuffle(arr1); + t.Shuffle32(arr1); System.out.println(Arrays.toString(arr1)); System.out.println("Example of Fisher-Yates: int"); - t.Shuffle(arr2); + t.Shuffle32(arr2); System.out.println(Arrays.toString(arr2)); System.out.println("Example of Fisher-Yates: String"); - t.Shuffle(arr3); + t.Shuffle32(arr3); System.out.println(Arrays.toString(arr3)); System.out.println("Example of Fisher-Yates: char"); - t.Shuffle(arr4); + t.Shuffle32(arr4); System.out.println(Arrays.toString(arr4)); System.out.println("Example of Fisher-Yates: boolean"); - t.Shuffle(arr5); + t.Shuffle32(arr5); System.out.println(Arrays.toString(arr5)); System.out.println("Example of Fisher-Yates: long"); - t.Shuffle(arr6); + t.Shuffle32(arr6); System.out.println(Arrays.toString(arr6)); System.out.println("Example of Fisher-Yates: short"); - t.Shuffle(arr7); + t.Shuffle32(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 deleted file mode 100644 index 0c683094..00000000 --- a/docs/py/CustomTestSamplers.py +++ /dev/null @@ -1,49 +0,0 @@ -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/TestShuffling32.py similarity index 78% rename from docs/py/CustomTestShuffling.py rename to docs/py/TestShuffling32.py index 62e4d832..d4a6deeb 100644 --- a/docs/py/CustomTestShuffling.py +++ b/docs/py/TestShuffling32.py @@ -10,26 +10,26 @@ def main(): # STANDARD RNG print("\nSTANDARD RNG TESTS WITH CUSTOM UNIFORM\n") - r = DafnyVMC.CustomRandom() + r = DafnyVMC.Random() print("Example of Fisher-Yates: int") - arr1 = r.Shuffle(arr1) + arr1 = r.Shuffle32(arr1) print(arr1) print("Example of Fisher-Yates: float") - arr2 = r.Shuffle(arr2) + arr2 = r.Shuffle32(arr2) print(arr2) print("Example of Fisher-Yates: str") - arr3 = r.Shuffle(arr3) + arr3 = r.Shuffle32(arr3) print(arr3) print("Example of Fisher-Yates: char/str") - arr4 = r.Shuffle(arr4) + arr4 = r.Shuffle32(arr4) print(arr4) print("Example of Fisher-Yates: boolean") - arr5 = r.Shuffle(arr5) + arr5 = r.Shuffle32(arr5) print(arr5) if __name__ == "__main__": diff --git a/scripts/build.sh b/scripts/build.sh index f52f9d08..28feac69 100755 --- a/scripts/build.sh +++ b/scripts/build.sh @@ -16,7 +16,7 @@ fi 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 + $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 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/DafnyVMC.dfy b/src/DafnyVMC.dfy index 0acd9ec6..63795dcf 100644 --- a/src/DafnyVMC.dfy +++ b/src/DafnyVMC.dfy @@ -4,9 +4,13 @@ *******************************************************************************/ module {:extern} DafnyVMCPartMaterial { + import opened Pos + class {:extern} Random { // For running Dafny native testing with standard SecureRandom rng static method {:extern "UniformPowerOfTwoSample"} ExternUniformPowerOfTwoSample(n: nat) returns (u: nat) + + static method {:extern "UniformSample32"} ExternUniformSample32(n: pos32) returns (u: nat32) } } @@ -15,6 +19,8 @@ module {:extern "DafnyVMCPart"} DafnyVMC { import DafnyVMCPartMaterial import Monad import UniformPowerOfTwo + import Uniform + import opened Pos class Random extends DafnyVMCTrait.RandomTrait { constructor {:extern} () @@ -25,6 +31,15 @@ module {:extern "DafnyVMCPart"} DafnyVMC { { u := DafnyVMCPartMaterial.Random.ExternUniformPowerOfTwoSample(n); } + + method {:verify false} UniformSample32(n: pos32) returns (u: nat32) + modifies `s + decreases * + ensures u < n + ensures Uniform.Model.Sample(n as nat)(old(s)) == Monad.Result(u as nat, s) + { + u := DafnyVMCPartMaterial.Random.ExternUniformSample32(n); + } } } \ No newline at end of file diff --git a/src/DafnyVMCTrait.dfy b/src/DafnyVMCTrait.dfy index 2d6c2e6e..f85c55a2 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, FisherYates.Implementation.Trait32 { method {:verify false} UniformSample (n: pos) returns (o: nat) diff --git a/src/Util/FisherYates/Interface.dfy b/src/Util/FisherYates/Interface.dfy index f2603bb7..87cc8954 100644 --- a/src/Util/FisherYates/Interface.dfy +++ b/src/Util/FisherYates/Interface.dfy @@ -23,7 +23,7 @@ module FisherYates.Interface { decreases * modifies `s, a requires a.Length < 0x8000_0000 - //ensures Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s) + ensures Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s) } } \ No newline at end of file diff --git a/src/interop/java/Full/CustomRandom.java b/src/interop/java/Full/CustomRandom.java deleted file mode 100644 index e96c7aac..00000000 --- a/src/interop/java/Full/CustomRandom.java +++ /dev/null @@ -1,38 +0,0 @@ -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/java/Full/Random.java b/src/interop/java/Full/Random.java index 94b38f75..5b7f61d6 100644 --- a/src/interop/java/Full/Random.java +++ b/src/interop/java/Full/Random.java @@ -6,14 +6,14 @@ import java.util.function.Supplier; public class Random implements DafnyVMCTrait.RandomTrait { - static ThreadLocal rng; + static ThreadLocal RNG; public Random() { - this.rng = ThreadLocal.withInitial(Random::createSecureRandom); + this.RNG = ThreadLocal.withInitial(Random::createSecureRandom); } public Random(Supplier supplier) { - this.rng = ThreadLocal.withInitial(supplier); + this.RNG = ThreadLocal.withInitial(supplier); } private static final SecureRandom createSecureRandom() { @@ -28,13 +28,25 @@ public BigInteger UniformPowerOfTwoSample(BigInteger n) { throw new IllegalArgumentException("n must be positive"); } - return new BigInteger(n.bitLength()-1, rng.get()); + return new BigInteger(n.bitLength()-1, RNG.get()); + } + + public int UniformSample32(int n) { + if (n <= 0) { + throw new IllegalArgumentException("n must be positive"); + } + + return RNG.get().nextInt(n); } public java.math.BigInteger UniformIntervalSample(java.math.BigInteger a, java.math.BigInteger b) { return Uniform.Interface._Companion_Trait.UniformIntervalSample(this, a, b); } + public int UniformIntervalSample32(int a, int b) { + return Uniform.Interface._Companion_Trait32.UniformIntervalSample32(this, a, b); + } + public java.math.BigInteger UniformSample(java.math.BigInteger n) { return DafnyVMCTrait._Companion_RandomTrait.UniformSample(this, n); } @@ -103,36 +115,72 @@ public <__T> void Shuffle(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a) FisherYates.Implementation._Companion_Trait.Shuffle(_td___T, this, a); } + public <__T> void Shuffle32(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a) { + FisherYates.Implementation._Companion_Trait32.Shuffle32(_td___T, this, a); + } + public void Shuffle(BigInteger[] arr) { FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BIG_INTEGER, this, arr); } + public void Shuffle32(BigInteger[] arr) { + FisherYates.Implementation._Companion_Trait32.Shuffle32(TypeDescriptor.BIG_INTEGER, this, arr); + } + public void Shuffle(int[] arr) { FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.INT, this, arr); } + public void Shuffle32(int[] arr) { + FisherYates.Implementation._Companion_Trait32.Shuffle32(TypeDescriptor.INT, this, arr); + } + public void Shuffle(String[] arr) { FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR_ARRAY, this, arr); } + public void Shuffle32(String[] arr) { + FisherYates.Implementation._Companion_Trait32.Shuffle32(TypeDescriptor.CHAR_ARRAY, this, arr); + } + public void Shuffle(char[] arr) { FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR, this, arr); } + public void Shuffle32(char[] arr) { + FisherYates.Implementation._Companion_Trait32.Shuffle32(TypeDescriptor.CHAR, this, arr); + } + public void Shuffle(boolean[] arr) { FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BOOLEAN, this, arr); } + public void Shuffle32(boolean[] arr) { + FisherYates.Implementation._Companion_Trait32.Shuffle32(TypeDescriptor.BOOLEAN, this, arr); + } + public void Shuffle(long[] arr) { FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.LONG, this, arr); } + public void Shuffle32(long[] arr) { + FisherYates.Implementation._Companion_Trait32.Shuffle32(TypeDescriptor.LONG, this, arr); + } + public void Shuffle(short[] arr) { FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.SHORT, this, arr); } + public void Shuffle32(short[] arr) { + FisherYates.Implementation._Companion_Trait32.Shuffle32(TypeDescriptor.SHORT, this, arr); + } + public <__T> void Swap(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a, java.math.BigInteger i, java.math.BigInteger j) { FisherYates.Implementation._Companion_Trait.Swap(_td___T, this, a, i, j); } + + public <__T> void Swap32(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a, int i, int j) { + FisherYates.Implementation._Companion_Trait32.Swap32(_td___T, this, a, i, j); + } } \ No newline at end of file diff --git a/src/interop/java/Part/Random.java b/src/interop/java/Part/Random.java index 7a31b8d3..0997b02e 100644 --- a/src/interop/java/Part/Random.java +++ b/src/interop/java/Part/Random.java @@ -24,4 +24,12 @@ public static BigInteger UniformPowerOfTwoSample(BigInteger n) { return new BigInteger(n.bitLength()-1, RNG.get()); } + + public static int UniformSample32(int n) { + if (n <= 0) { + throw new IllegalArgumentException("n must be positive"); + } + + return RNG.get().nextInt(n); + } } \ No newline at end of file diff --git a/src/interop/py/Full/Random.py b/src/interop/py/Full/Random.py index e1bd2dd3..66f854ef 100644 --- a/src/interop/py/Full/Random.py +++ b/src/interop/py/Full/Random.py @@ -16,6 +16,8 @@ def Shuffle(self, 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 + def Shuffle32(self, xs): + a = ArrayFromList(xs) + DafnyVMCPart.Random.Shuffle32(self, a) + return list(a) + \ No newline at end of file diff --git a/src/interop/py/Part/Random.py b/src/interop/py/Part/Random.py index 764c6d4a..b5a9d550 100644 --- a/src/interop/py/Part/Random.py +++ b/src/interop/py/Part/Random.py @@ -4,4 +4,7 @@ class Random: def UniformPowerOfTwoSample(n): - return secrets.randbits(n.bit_length()-1) \ No newline at end of file + return secrets.randbits(n.bit_length()-1) + + def UniformSample32(n): + return secrets.randbelow(n) \ No newline at end of file