diff --git a/build/java/run.sh b/build/java/run.sh index ff6bdcad..94fd5695 100755 --- a/build/java/run.sh +++ b/build/java/run.sh @@ -1,3 +1,3 @@ #1/bin/bash - -java -classpath build/java/DafnyVMC.jar docs/java/BuildTest.java \ No newline at end of file +javac -classpath "build/java/DafnyVMC.jar:docs/java/" docs/java/CustomFisherYates.java docs/java/CustomFisherYatesFaulty.java +java -classpath "build/java/DafnyVMC.jar:docs/java/" docs/java/BuildTest.java diff --git a/docs/java/BuildTest.java b/docs/java/BuildTest.java index 2c64a04d..6c570dcb 100644 --- a/docs/java/BuildTest.java +++ b/docs/java/BuildTest.java @@ -1,25 +1,35 @@ -import java.security.SecureRandom; import java.math.BigInteger; import java.util.Arrays; -import DafnyVMC.Random; - -class Check { +public class BuildTest { public static void main(String[] args) { BigInteger[] arr1 = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)}; + BigInteger[] arr1_custom = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)}; + BigInteger[] arr1_faulty = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)}; int[] arr2 = {0, 1, 2}; + int[] arr2_custom = {0, 1, 2}; + int[] arr2_faulty = {0, 1, 2}; String[] arr3 = {"aa", "bb", "cc"}; + String[] arr3_custom = {"aa", "bb", "cc"}; + String[] arr3_faulty = {"aa", "bb", "cc"}; char[] arr4 = {'a', 'b', 'c'}; + char[] arr4_custom = {'a', 'b', 'c'}; + char[] arr4_faulty = {'a', 'b', 'c'}; boolean[] arr5 = {true, false, false, true}; + boolean[] arr5_custom = {true, false, false, true}; + boolean[] arr5_faulty = {true, false, false, true}; long[] arr6 = {111111L, 333333L, 999999L}; + long[] arr6_custom = {111111L, 333333L, 999999L}; + long[] arr6_faulty = {111111L, 333333L, 999999L}; short[] arr7 = {-3, 0, 3}; + short[] arr7_custom = {-3, 0, 3}; + short[] arr7_faulty = {-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(); + CustomFisherYates r_custom = new CustomFisherYates(); + CustomFisherYatesFaulty r_faulty = new CustomFisherYatesFaulty(); System.out.println("Example of Uniform sampling"); System.out.println(r.UniformSample(BigInteger.valueOf(4))); @@ -39,78 +49,86 @@ public static void main(String[] args) { System.out.println("Example of Fisher-Yates: BigInteger"); r.Shuffle(arr1); System.out.println(Arrays.toString(arr1)); + + System.out.println("Example of custom Fisher-Yates: BigInteger"); + r_custom.Shuffle(arr1_custom); + System.out.println(Arrays.toString(arr1_custom)); + + System.out.println("Example of faulty custom Fisher-Yates: BigInteger"); + r_faulty.Shuffle(arr1_faulty); + System.out.println(Arrays.toString(arr1_faulty)); System.out.println("Example of Fisher-Yates: int"); r.Shuffle(arr2); System.out.println(Arrays.toString(arr2)); + System.out.println("Example of custom Fisher-Yates: int"); + r_custom.Shuffle(arr2_custom); + System.out.println(Arrays.toString(arr2_custom)); + + System.out.println("Example of faulty custom Fisher-Yates: int"); + r_faulty.Shuffle(arr2_faulty); + System.out.println(Arrays.toString(arr2_faulty)); + System.out.println("Example of Fisher-Yates: String"); r.Shuffle(arr3); System.out.println(Arrays.toString(arr3)); + System.out.println("Example of custom Fisher-Yates: String"); + r_custom.Shuffle(arr3_custom); + System.out.println(Arrays.toString(arr3_custom)); + + System.out.println("Example of faulty custom Fisher-Yates: String"); + r_faulty.Shuffle(arr3_faulty); + System.out.println(Arrays.toString(arr3_faulty)); + System.out.println("Example of Fisher-Yates: char"); r.Shuffle(arr4); System.out.println(Arrays.toString(arr4)); + System.out.println("Example of custom Fisher-Yates: char"); + r_custom.Shuffle(arr4_custom); + System.out.println(Arrays.toString(arr4_custom)); + + System.out.println("Example of faulty custom Fisher-Yates: char"); + r_faulty.Shuffle(arr4_faulty); + System.out.println(Arrays.toString(arr4_faulty)); + System.out.println("Example of Fisher-Yates: boolean"); r.Shuffle(arr5); System.out.println(Arrays.toString(arr5)); + System.out.println("Example of custom Fisher-Yates: boolean"); + r_custom.Shuffle(arr5_custom); + System.out.println(Arrays.toString(arr5_custom)); + + System.out.println("Example of faulty custom Fisher-Yates: boolean"); + r_faulty.Shuffle(arr5_faulty); + System.out.println(Arrays.toString(arr5_faulty)); + System.out.println("Example of Fisher-Yates: long"); r.Shuffle(arr6); System.out.println(Arrays.toString(arr6)); + System.out.println("Example of custom Fisher-Yates: long"); + r_custom.Shuffle(arr6_custom); + System.out.println(Arrays.toString(arr6_custom)); + + System.out.println("Example of faulty custom Fisher-Yates: long"); + r_faulty.Shuffle(arr6_faulty); + System.out.println(Arrays.toString(arr6_faulty)); + 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 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 custom Fisher-Yates: short"); + r_custom.Shuffle(arr7_custom); + System.out.println(Arrays.toString(arr7_custom)); - 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)); - - 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)); + System.out.println("Example of faulty custom Fisher-Yates: short"); + r_faulty.Shuffle(arr7_faulty); + System.out.println(Arrays.toString(arr7_faulty)); } -} \ No newline at end of file +} + diff --git a/docs/java/CustomFisherYates.java b/docs/java/CustomFisherYates.java new file mode 100644 index 00000000..1d3b12b6 --- /dev/null +++ b/docs/java/CustomFisherYates.java @@ -0,0 +1,89 @@ +import Uniform.Interface.TraitMinus; +import Uniform.Interface.Trait; +import java.math.BigInteger; +import java.security.SecureRandom; +import java.util.Random; +import dafny.TypeDescriptor; + +class CustomUniformSampleMinus implements Uniform.Interface.TraitMinus { + static ThreadLocal rng; + + public CustomUniformSampleMinus() { + CustomUniformSampleMinus.rng = ThreadLocal.withInitial(CustomUniformSampleMinus::createSecureRandom); + } + + 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 BigInteger UniformSample(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; + } +} + +class CustomUniform extends CustomUniformSampleMinus implements Uniform.Interface.Trait { + public java.math.BigInteger UniformIntervalSample(java.math.BigInteger a, java.math.BigInteger b) { + return Uniform.Interface._Companion_Trait.UniformIntervalSample(this, a, b); + } +} + + +class CustomFisherYatesMinus extends CustomUniform implements FisherYates.Implementation.Trait { + 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 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 class CustomFisherYates extends CustomFisherYatesMinus { + public void Shuffle(BigInteger[] arr) { + this.Shuffle(TypeDescriptor.BIG_INTEGER, arr); + } + + public void Shuffle(int[] arr) { + this.Shuffle(TypeDescriptor.INT, arr); + } + + public void Shuffle(String[] arr) { + this.Shuffle(TypeDescriptor.CHAR_ARRAY, arr); + } + + public void Shuffle(char[] arr) { + this.Shuffle(TypeDescriptor.CHAR, arr); + } + + public void Shuffle(boolean[] arr) { + this.Shuffle(TypeDescriptor.BOOLEAN, arr); + } + + public void Shuffle(long[] arr) { + this.Shuffle(TypeDescriptor.LONG, arr); + } + + public void Shuffle(short[] arr) { + this.Shuffle(TypeDescriptor.SHORT, arr); + } +} diff --git a/docs/java/CustomFisherYatesFaulty.java b/docs/java/CustomFisherYatesFaulty.java new file mode 100644 index 00000000..82fb57ea --- /dev/null +++ b/docs/java/CustomFisherYatesFaulty.java @@ -0,0 +1,58 @@ +import Uniform.Interface.TraitMinus; +import Uniform.Interface.Trait; +import java.math.BigInteger; +import java.security.SecureRandom; +import java.util.Random; +import dafny.TypeDescriptor; + +class CustomUniformSampleFaultyMinus implements Uniform.Interface.TraitMinus { + public BigInteger UniformSample(BigInteger n) { + return BigInteger.valueOf(0); + } +} + +class CustomUniformFaulty extends CustomUniformSampleFaultyMinus implements Uniform.Interface.Trait { + public java.math.BigInteger UniformIntervalSample(java.math.BigInteger a, java.math.BigInteger b) { + return Uniform.Interface._Companion_Trait.UniformIntervalSample(this, a, b); + } +} + +class CustomFisherYatesMinusFaulty extends CustomUniformFaulty implements FisherYates.Implementation.Trait { + 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 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 class CustomFisherYatesFaulty extends CustomFisherYatesMinusFaulty { + public void Shuffle(BigInteger[] arr) { + this.Shuffle(TypeDescriptor.BIG_INTEGER, arr); + } + + public void Shuffle(int[] arr) { + this.Shuffle(TypeDescriptor.INT, arr); + } + + public void Shuffle(String[] arr) { + this.Shuffle(TypeDescriptor.CHAR_ARRAY, arr); + } + + public void Shuffle(char[] arr) { + this.Shuffle(TypeDescriptor.CHAR, arr); + } + + public void Shuffle(boolean[] arr) { + this.Shuffle(TypeDescriptor.BOOLEAN, arr); + } + + public void Shuffle(long[] arr) { + this.Shuffle(TypeDescriptor.LONG, arr); + } + + public void Shuffle(short[] arr) { + this.Shuffle(TypeDescriptor.SHORT, arr); + } +} diff --git a/src/DafnyVMCTrait.dfy b/src/DafnyVMCTrait.dfy index cf60dfd0..2e85970e 100644 --- a/src/DafnyVMCTrait.dfy +++ b/src/DafnyVMCTrait.dfy @@ -26,7 +26,7 @@ module DafnyVMCTrait { method {:verify false} BernoulliSample (num: nat, den: pos) returns (o: bool) - requires num <= den + requires num <= den modifies this decreases * { @@ -36,7 +36,7 @@ module DafnyVMCTrait { method {:verify false} BernoulliExpNegSampleUnitLoop (num: nat, den: pos, state: (bool,pos)) returns (o: (bool,pos)) - requires num <= den + requires num <= den modifies this decreases * { @@ -46,7 +46,7 @@ module DafnyVMCTrait { method {:verify false} BernoulliExpNegSampleUnitAux (num: nat, den: pos) returns (o: nat) - requires num <= den + requires num <= den modifies this decreases * { @@ -62,7 +62,7 @@ module DafnyVMCTrait { method {:verify false} BernoulliExpNegSampleUnit (num: nat, den: pos) returns (o: bool) - requires num <= den + requires num <= den modifies this decreases * { @@ -136,7 +136,7 @@ module DafnyVMCTrait { method {:verify false} DiscreteLaplaceSampleLoopIn2Aux (num: nat, den: pos, K: (bool,pos)) returns (o: (bool,pos)) - requires num <= den + requires num <= den modifies this decreases * { @@ -222,6 +222,6 @@ module DafnyVMCTrait { } -} + } } diff --git a/src/Distributions/Bitstream/Interface.dfy b/src/Distributions/Bitstream/Interface.dfy new file mode 100644 index 00000000..5ebc77bb --- /dev/null +++ b/src/Distributions/Bitstream/Interface.dfy @@ -0,0 +1,12 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +module Bitstream.Interface { + import Rand + + trait {:termination false} Trait { + ghost var s: Rand.Bitstream + } +} diff --git a/src/Distributions/Uniform/Interface.dfy b/src/Distributions/Uniform/Interface.dfy index af2306a0..faac214c 100644 --- a/src/Distributions/Uniform/Interface.dfy +++ b/src/Distributions/Uniform/Interface.dfy @@ -4,13 +4,14 @@ *******************************************************************************/ module Uniform.Interface { + import Bitstream import Monad import Coin import Model import UniformPowerOfTwo import Pos - trait {:termination false} Trait extends UniformPowerOfTwo.Interface.Trait { + trait {:termination false} TraitMinus extends Bitstream.Interface.Trait { method UniformSample(n: Pos.pos) returns (u: nat) modifies `s @@ -19,6 +20,10 @@ module Uniform.Interface { ensures u < n ensures Model.Sample(n)(old(s)) == Monad.Result(u, s) + } + + trait {:termination false} Trait extends TraitMinus { + method UniformIntervalSample(a: int, b: int) returns (u: int) modifies `s decreases * @@ -33,4 +38,5 @@ module Uniform.Interface { } } + } diff --git a/src/Distributions/UniformPowerOfTwo/Interface.dfy b/src/Distributions/UniformPowerOfTwo/Interface.dfy index 77c6f356..b1c4fc6e 100644 --- a/src/Distributions/UniformPowerOfTwo/Interface.dfy +++ b/src/Distributions/UniformPowerOfTwo/Interface.dfy @@ -7,10 +7,9 @@ module UniformPowerOfTwo.Interface { import Monad import Model import Rand + import Bitstream - trait {:termination false} Trait { - ghost var s: Rand.Bitstream - + trait {:termination false} Trait extends Bitstream.Interface.Trait { // 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) requires n >= 1