diff --git a/audit.log b/audit.log index dd17732c..369366a0 100644 --- a/audit.log +++ b/audit.log @@ -1,2 +1,3 @@ src/Distributions/Uniform/Model.dfy(18,26): Sample: Declaration has explicit `{:axiom}` attribute. -src/ProbabilisticProgramming/RandomSource.dfy(50,17): ProbIsProbabilityMeasure: Declaration has explicit `{:axiom}` attribute. +src/DafnyVMC.dfy(35,27): UniformSample32: Declaration has `{:verify false}` attribute. +src/ProbabilisticProgramming/RandomSource.dfy(50,17): ProbIsProbabilityMeasure: Declaration has explicit `{:axiom}` attribute. \ No newline at end of file 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..5f5e14cf 100755 --- a/build/java/run_shuffling.sh +++ b/build/java/run_shuffling.sh @@ -1,4 +1,3 @@ #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/TestShuffling.java \ No newline at end of file diff --git a/build/py/run_samplers.sh b/build/py/run_samplers.sh index 24264a03..9dcf986b 100755 --- a/build/py/run_samplers.sh +++ b/build/py/run_samplers.sh @@ -1,4 +1,3 @@ #1/bin/bash -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 +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 index bb7db895..be7c5ec2 100755 --- a/build/py/run_shuffling.sh +++ b/build/py/run_shuffling.sh @@ -1,4 +1,3 @@ #1/bin/bash -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 +PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestShuffling.py \ No newline at end of file diff --git a/docs/dafny/ExamplesRandom.dfy b/docs/dafny/ExamplesRandom.dfy index be8658e3..59eff1ec 100644 --- a/docs/dafny/ExamplesRandom.dfy +++ b/docs/dafny/ExamplesRandom.dfy @@ -118,7 +118,7 @@ module Examples { // 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 + // Fisher-Yates Shuffle Example print "Ten permutations of 012: "; var arr: array := new nat[3](i => i); // [0, 1, 2] for i := 0 to 10 { 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/CustomTestShuffling.java deleted file mode 100644 index e5642287..00000000 --- a/docs/java/CustomTestShuffling.java +++ /dev/null @@ -1,85 +0,0 @@ -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 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/CustomTestShuffling.py deleted file mode 100644 index 62e4d832..00000000 --- a/docs/py/CustomTestShuffling.py +++ /dev/null @@ -1,36 +0,0 @@ -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 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..e188c943 100644 --- a/src/DafnyVMCTrait.dfy +++ b/src/DafnyVMCTrait.dfy @@ -5,9 +5,11 @@ module DafnyVMCTrait { import FisherYates + import Uniform + 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, Uniform.Interface.Trait { method {:verify false} UniformSample (n: pos) returns (o: nat) diff --git a/src/Distributions/Uniform/Interface.dfy b/src/Distributions/Uniform/Interface.dfy index 2cb1d4d4..e71aae85 100644 --- a/src/Distributions/Uniform/Interface.dfy +++ b/src/Distributions/Uniform/Interface.dfy @@ -6,15 +6,14 @@ module Uniform.Interface { import Monad import Model - import Pos + import opened Pos import Bitstream trait {:termination false} Trait extends Bitstream.Interface.Trait { - method UniformSample(n: Pos.pos) returns (u: nat) + method UniformSample(n: pos) returns (u: nat) modifies `s decreases * - requires n > 0 ensures u < n ensures Model.Sample(n)(old(s)) == Monad.Result(u, s) @@ -32,4 +31,28 @@ module Uniform.Interface { } } + + trait {:termination false} Trait32 extends Bitstream.Interface.Trait { + + method UniformSample32(n: pos32) returns (u: nat32) + modifies `s + decreases * + ensures u < n + ensures Model.Sample(n as nat)(old(s)) == Monad.Result(u as nat, s) + + method UniformIntervalSample32(a: int32, b: int32) returns (u: int32) + modifies `s + decreases * + requires 0 < b as int - a as int < 0x8000_0000 + ensures a <= u < b + ensures Model.IntervalSample(a as int, b as int)(old(s)) == Monad.Result(u as int, s) + { + var v := UniformSample32(b-a); + assert Model.Sample(b as int - a as int)(old(s)) == Monad.Result(v as nat, s); + assert Model.IntervalSample(a as int, b as int)(old(s)) == Monad.Result(a as int + v as int, s); + u := a + v; + } + + } + } diff --git a/src/Util/FisherYates/Equivalence.dfy b/src/Util/FisherYates/Equivalence.dfy index 98fbf7ba..b8415b96 100644 --- a/src/Util/FisherYates/Equivalence.dfy +++ b/src/Util/FisherYates/Equivalence.dfy @@ -7,14 +7,15 @@ module FisherYates.Equivalence { import Model import Rand import Monad + import opened Pos - ghost predicate LoopInvariant(prevI: nat, i: nat, a: array, prevASeq: seq, oldASeq: seq, oldS: Rand.Bitstream, prevS: Rand.Bitstream, s: Rand.Bitstream) + ghost predicate LoopInvariant(prevI: nat32, i: nat32, a: array, prevASeq: seq, oldASeq: seq, oldS: Rand.Bitstream, prevS: Rand.Bitstream, s: Rand.Bitstream) reads a { - && prevI <= |prevASeq| - && i <= a.Length - 1 - && Model.Shuffle(oldASeq)(oldS) == Model.Shuffle(prevASeq, prevI)(prevS) - && Model.Shuffle(prevASeq, prevI)(prevS) == Model.Shuffle(a[..], i)(s) + && prevI as nat <= |prevASeq| + && i as nat <= a.Length - 1 + && Model.Shuffle(oldASeq)(oldS) == Model.Shuffle(prevASeq, prevI as nat)(prevS) + && Model.Shuffle(prevASeq, prevI as nat)(prevS) == Model.Shuffle(a[..], i as nat)(s) } lemma ShuffleElseClause(a: array, oldASeq: seq, oldS: Rand.Bitstream, s: Rand.Bitstream) diff --git a/src/Util/FisherYates/Implementation.dfy b/src/Util/FisherYates/Implementation.dfy index d0f4f63d..803b3848 100644 --- a/src/Util/FisherYates/Implementation.dfy +++ b/src/Util/FisherYates/Implementation.dfy @@ -9,21 +9,24 @@ module FisherYates.Implementation { import Model import Uniform import Equivalence + import opened Pos trait {:termination false} Trait extends Interface.Trait { - method Shuffle(a: array) + method {:vcs_split_on_every_assert} Shuffle(a: array) decreases * modifies `s, a + requires a.Length < 0x8000_0000 ensures Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s) { - ghost var prevI, prevASeq, prevS := 0, a[..], s; // ghost - if a.Length > 1 { - for i := 0 to a.Length - 1 + ghost var prevI, prevASeq, prevS := 0 as int32, a[..], s; // ghost + + if (a.Length as nat32) > (1 as nat32) { + for i: nat32 := (0 as nat32) to (a.Length as nat32) - (1 as nat32) invariant Equivalence.LoopInvariant(prevI, i, a, prevASeq, old(a[..]), old(s), prevS, s) // ghost { prevI, prevASeq, prevS := i, a[..], s; // ghost - var j := UniformIntervalSample(i, a.Length); + var j := UniformIntervalSample32(i, a.Length as nat32); assert prevASeq == a[..]; // ghost Swap(a, i, j); } @@ -33,12 +36,12 @@ module FisherYates.Implementation { } - method Swap(a: array, i: nat, j: nat) + method Swap(a: array, i: nat32, j: nat32) modifies a requires i <= j - requires 0 <= i < a.Length - requires 0 <= j < a.Length - ensures Model.Swap(old(a[..]), i, j) == a[..] + requires 0 <= i as nat < a.Length + requires 0 <= j as nat < a.Length + ensures Model.Swap(old(a[..]), i as nat, j as nat) == a[..] ensures old(s) == s { a[i], a[j] := a[j], a[i]; diff --git a/src/Util/FisherYates/Interface.dfy b/src/Util/FisherYates/Interface.dfy index 1571870d..ad3f75ee 100644 --- a/src/Util/FisherYates/Interface.dfy +++ b/src/Util/FisherYates/Interface.dfy @@ -8,11 +8,12 @@ module FisherYates.Interface { import Model import Monad - trait {:termination false} Trait extends Uniform.Interface.Trait { + trait {:termination false} Trait extends Uniform.Interface.Trait32 { method Shuffle(a: array) decreases * modifies `s, a + requires a.Length < 0x8000_0000 ensures Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s) } diff --git a/src/Util/Pos.dfy b/src/Util/Pos.dfy index 15b8ee37..a0664741 100644 --- a/src/Util/Pos.dfy +++ b/src/Util/Pos.dfy @@ -1,6 +1,12 @@ module Pos { - type pos = x : nat | x > 0 witness 1 + newtype int32 = x: int | -0x8000_0000 <= x < 0x8000_0000 + + type pos = x: nat | x > 0 witness 1 + + type nat32 = x: int32 | x >= 0 witness 1 + + type pos32 = x: nat32 | x > 0 witness 1 } \ 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..a20d96d6 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); } @@ -70,7 +82,6 @@ public dafny.Tuple2 DiscreteGaussianSampleLoop(ja return DafnyVMCTrait._Companion_RandomTrait.DiscreteGaussianSampleLoop(this, num, den, t); } - public java.math.BigInteger DiscreteGaussianSample(java.math.BigInteger num, java.math.BigInteger den) { return DafnyVMCTrait._Companion_RandomTrait.DiscreteGaussianSample(this, num, den); } @@ -131,7 +142,7 @@ public void Shuffle(short[] arr) { FisherYates.Implementation._Companion_Trait.Shuffle(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) { + public <__T> void Swap(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a, int i, int j) { FisherYates.Implementation._Companion_Trait.Swap(_td___T, this, a, i, j); } 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..a7f86306 100644 --- a/src/interop/py/Full/Random.py +++ b/src/interop/py/Full/Random.py @@ -15,7 +15,4 @@ 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 + \ 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 diff --git a/tests/Tests.dfy b/tests/Tests.dfy index 6c131ef3..cfd6a0b0 100644 --- a/tests/Tests.dfy +++ b/tests/Tests.dfy @@ -282,6 +282,7 @@ module Tests { modifies r modifies a requires n > 0 + requires a.Length < 0x8000_0000 { var a := new (T, nat)[a.Length](i reads a requires 0 <= i < a.Length => (a[i], i)); var numberOfPermutations: nat := NatArith.FactorialTraditional(a.Length);