From 0d548936c1c49e649eea5bf36fd01b7f29b5cbb6 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 14 Feb 2024 03:14:21 +0000 Subject: [PATCH 01/10] skeleton --- docs/java/BuildTest.java | 62 ++++--------------------- docs/java/CustomUniformSample.java | 40 ++++++++++++++++ src/Distributions/Uniform/Interface.dfy | 7 ++- src/Util/FisherYates/Implementation.dfy | 4 +- src/Util/FisherYates/Interface.dfy | 2 +- src/interop/java/Full/Random.java | 26 +++++------ 6 files changed, 71 insertions(+), 70 deletions(-) create mode 100644 docs/java/CustomUniformSample.java diff --git a/docs/java/BuildTest.java b/docs/java/BuildTest.java index f048cdf1..70e6bffd 100644 --- a/docs/java/BuildTest.java +++ b/docs/java/BuildTest.java @@ -3,6 +3,8 @@ import java.util.Arrays; import DafnyVMC.Random; +import Uniform.Interface.TraitMinus; +import Uniform.Interface.Trait; class Check { public static void main(String[] args) { @@ -19,6 +21,7 @@ public static void main(String[] args) { System.out.println("\nSTANDARD RNG TESTS\n"); DafnyVMC.Random r = new DafnyVMC.Random(); + Uniform.Interface.Trait t = (Uniform.Interface.Trait) new CustomUniformSample(); System.out.println("Example of Coin sampling"); System.out.println(r.CoinSample()); @@ -41,6 +44,10 @@ 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 Fisher-Yates: BigInteger"); + // r.Shuffle(arr1, t); + // System.out.println(Arrays.toString(arr1)); System.out.println("Example of Fisher-Yates: int"); r.Shuffle(arr2); @@ -65,57 +72,6 @@ public static void main(String[] args) { 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 Coin sampling"); - System.out.println(t.CoinSample()); - - 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(gamma)); - - System.out.println("Example of BernoulliExpNeg sampling"); - System.out.println(r.BernoulliExpNegSample(gamma)); - - System.out.println("Example of DiscreteGaussian sampling"); - System.out.println(t.DiscreteGaussianSample(gamma)); - - System.out.println("Example of DiscreteLaplace sampling"); - System.out.println(t.DiscreteLaplaceSample(gamma)); - - 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/java/CustomUniformSample.java b/docs/java/CustomUniformSample.java new file mode 100644 index 00000000..33f514ba --- /dev/null +++ b/docs/java/CustomUniformSample.java @@ -0,0 +1,40 @@ +import java.security.SecureRandom; +import java.math.BigInteger; +import Uniform.Interface.TraitMinus; + + +public class CustomUniformSample implements Uniform.Interface.TraitMinus { + static ThreadLocal rng; + + public CustomUniformSample() { + CustomUniformSample.rng = ThreadLocal.withInitial(CustomUniformSample::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; + } +} \ No newline at end of file diff --git a/src/Distributions/Uniform/Interface.dfy b/src/Distributions/Uniform/Interface.dfy index 617175cd..ecf57346 100644 --- a/src/Distributions/Uniform/Interface.dfy +++ b/src/Distributions/Uniform/Interface.dfy @@ -9,7 +9,7 @@ module Uniform.Interface { import Model import UniformPowerOfTwo - trait {:termination false} Trait extends UniformPowerOfTwo.Interface.Trait { + trait {:termination false} TraitMinus extends UniformPowerOfTwo.Interface.Trait { method UniformSample(n: nat) returns (u: nat) modifies `s @@ -18,6 +18,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 * @@ -32,4 +36,5 @@ module Uniform.Interface { } } + } diff --git a/src/Util/FisherYates/Implementation.dfy b/src/Util/FisherYates/Implementation.dfy index 20a1b5b1..8220bfd1 100644 --- a/src/Util/FisherYates/Implementation.dfy +++ b/src/Util/FisherYates/Implementation.dfy @@ -12,7 +12,7 @@ module FisherYates.Implementation { trait {:termination false} Trait extends Interface.Trait { - method Shuffle(a: array) + method Shuffle(a: array, t: Uniform.Interface.Trait := this) decreases * modifies `s, a ensures Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s) @@ -23,7 +23,7 @@ module FisherYates.Implementation { invariant Equivalence.LoopInvariant(prevI, i, a, prevASeq, old(a[..]), old(s), prevS, s) { prevI, prevASeq, prevS := i, a[..], s; // ghost - var j := UniformIntervalSample(i, a.Length); + var j := t.UniformIntervalSample(i, a.Length); assert prevASeq == a[..]; // ghost Swap(a, i, j); } diff --git a/src/Util/FisherYates/Interface.dfy b/src/Util/FisherYates/Interface.dfy index 1571870d..6fc1c611 100644 --- a/src/Util/FisherYates/Interface.dfy +++ b/src/Util/FisherYates/Interface.dfy @@ -10,7 +10,7 @@ module FisherYates.Interface { trait {:termination false} Trait extends Uniform.Interface.Trait { - method Shuffle(a: array) + method Shuffle(a: array, t: Uniform.Interface.Trait := this) decreases * modifies `s, a ensures Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s) diff --git a/src/interop/java/Full/Random.java b/src/interop/java/Full/Random.java index 29862596..356498d6 100644 --- a/src/interop/java/Full/Random.java +++ b/src/interop/java/Full/Random.java @@ -12,10 +12,6 @@ public Random() { this.rng = ThreadLocal.withInitial(Random::createSecureRandom); } - public Random(Supplier supplier) { - this.rng = ThreadLocal.withInitial(supplier); - } - private static final SecureRandom createSecureRandom() { final SecureRandom rng = new SecureRandom(); // Required for proper initialization @@ -71,36 +67,40 @@ public java.math.BigInteger DiscreteLaplaceSample(Rationals.Rational scale) { return DiscreteLaplace.Implementation._Companion_Trait.DiscreteLaplaceSample(this, scale); } - 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 Shuffle(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a, Uniform.Interface.Trait t) { + FisherYates.Implementation._Companion_Trait.Shuffle(_td___T, this, a, t); } public void Shuffle(BigInteger[] arr) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BIG_INTEGER, this, arr); + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BIG_INTEGER, this, arr, this); + } + + public void Shuffle(BigInteger[] arr, Uniform.Interface.TraitMinus t) { + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BIG_INTEGER, this, arr, (Uniform.Interface.Trait) t); } public void Shuffle(int[] arr) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.INT, this, arr); + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.INT, this, arr, this); } public void Shuffle(String[] arr) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR_ARRAY, this, arr); + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR_ARRAY, this, arr, this); } public void Shuffle(char[] arr) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR, this, arr); + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR, this, arr, this); } public void Shuffle(boolean[] arr) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BOOLEAN, this, arr); + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BOOLEAN, this, arr, this); } public void Shuffle(long[] arr) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.LONG, this, arr); + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.LONG, this, arr, this); } public void Shuffle(short[] arr) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.SHORT, this, arr); + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.SHORT, this, arr, this); } public <__T> void Swap(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a, java.math.BigInteger i, java.math.BigInteger j) { From d16111520a8af16f94e4ecaf4471b2d33e38b8f9 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 14 Feb 2024 13:53:47 +0000 Subject: [PATCH 02/10] make the build work --- build/java/run.sh | 4 +- docs/java/BuildTest.java | 39 +++++++++++++---- docs/java/CustomUniformSample.java | 67 +++++++++++++++++------------- src/interop/java/Full/Random.java | 28 ++++++++++++- 4 files changed, 95 insertions(+), 43 deletions(-) diff --git a/build/java/run.sh b/build/java/run.sh index ff6bdcad..48b8fd31 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/CustomUniformSample.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 70e6bffd..8169c10d 100644 --- a/docs/java/BuildTest.java +++ b/docs/java/BuildTest.java @@ -6,7 +6,7 @@ import Uniform.Interface.TraitMinus; import Uniform.Interface.Trait; -class Check { +public class BuildTest { public static void main(String[] args) { BigInteger[] arr1 = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)}; int[] arr2 = {0, 1, 2}; @@ -16,12 +16,9 @@ public static void main(String[] args) { long[] arr6 = {111111L, 333333L, 999999L}; short[] arr7 = {-3, 0, 3}; Rationals.Rational gamma = new Rationals.Rational(BigInteger.valueOf(3), BigInteger.valueOf(5)); - - /* STANDARD RNG */ - System.out.println("\nSTANDARD RNG TESTS\n"); - + DafnyVMC.Random r = new DafnyVMC.Random(); - Uniform.Interface.Trait t = (Uniform.Interface.Trait) new CustomUniformSample(); + Uniform.Interface.Trait t = new CustomUniformSample(); System.out.println("Example of Coin sampling"); System.out.println(r.CoinSample()); @@ -45,33 +42,57 @@ public static void main(String[] args) { r.Shuffle(arr1); System.out.println(Arrays.toString(arr1)); - System.out.println("Example of Fisher-Yates: BigInteger"); - // r.Shuffle(arr1, t); - // System.out.println(Arrays.toString(arr1)); + System.out.println("Example of custom Fisher-Yates: BigInteger"); + r.Shuffle(arr1, t); + 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 custom Fisher-Yates: int"); + r.Shuffle(arr2, t); + 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 custom Fisher-Yates: String"); + r.Shuffle(arr3, t); + 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 custom Fisher-Yates: char"); + r.Shuffle(arr4, t); + 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 custom Fisher-Yates: boolean"); + r.Shuffle(arr5, t); + 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 custom Fisher-Yates: long"); + r.Shuffle(arr6, t); + System.out.println(Arrays.toString(arr6)); + System.out.println("Example of Fisher-Yates: short"); r.Shuffle(arr7); System.out.println(Arrays.toString(arr7)); + + System.out.println("Example of custom Fisher-Yates: short"); + r.Shuffle(arr7, t); + System.out.println(Arrays.toString(arr7)); } } diff --git a/docs/java/CustomUniformSample.java b/docs/java/CustomUniformSample.java index 33f514ba..8ecb3f0d 100644 --- a/docs/java/CustomUniformSample.java +++ b/docs/java/CustomUniformSample.java @@ -1,40 +1,47 @@ -import java.security.SecureRandom; -import java.math.BigInteger; import Uniform.Interface.TraitMinus; +import Uniform.Interface.Trait; +import java.math.BigInteger; +import java.security.SecureRandom; +import java.util.Random; +class CustomUniformSampleMinus implements Uniform.Interface.TraitMinus { + static ThreadLocal rng; -public class CustomUniformSample implements Uniform.Interface.TraitMinus { - static ThreadLocal rng; - - public CustomUniformSample() { - CustomUniformSample.rng = ThreadLocal.withInitial(CustomUniformSample::createSecureRandom); - } + 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; - } + 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) { + 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"); } - return new BigInteger(n.bitLength()-1, rng.get()); - } + BigInteger sampleValue; + do { + sampleValue = UniformPowerOfTwoSample(n); + } while (sampleValue.compareTo(n) >= 0); - 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; - } + return sampleValue; + } +} + +public class CustomUniformSample 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); + } } \ No newline at end of file diff --git a/src/interop/java/Full/Random.java b/src/interop/java/Full/Random.java index 356498d6..393489c6 100644 --- a/src/interop/java/Full/Random.java +++ b/src/interop/java/Full/Random.java @@ -75,34 +75,58 @@ public void Shuffle(BigInteger[] arr) { FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BIG_INTEGER, this, arr, this); } - public void Shuffle(BigInteger[] arr, Uniform.Interface.TraitMinus t) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BIG_INTEGER, this, arr, (Uniform.Interface.Trait) t); + public void Shuffle(BigInteger[] arr, Uniform.Interface.Trait t) { + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BIG_INTEGER, this, arr, t); } public void Shuffle(int[] arr) { FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.INT, this, arr, this); } + public void Shuffle(int[] arr, Uniform.Interface.Trait t) { + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.INT, this, arr, t); + } + public void Shuffle(String[] arr) { FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR_ARRAY, this, arr, this); } + public void Shuffle(String[] arr, Uniform.Interface.Trait t) { + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR_ARRAY, this, arr, t); + } + public void Shuffle(char[] arr) { FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR, this, arr, this); } + public void Shuffle(char[] arr, Uniform.Interface.Trait t) { + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR, this, arr, t); + } + public void Shuffle(boolean[] arr) { FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BOOLEAN, this, arr, this); } + public void Shuffle(boolean[] arr, Uniform.Interface.Trait t) { + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BOOLEAN, this, arr, t); + } + public void Shuffle(long[] arr) { FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.LONG, this, arr, this); } + public void Shuffle(long[] arr, Uniform.Interface.Trait t) { + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.LONG, this, arr, t); + } + public void Shuffle(short[] arr) { FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.SHORT, this, arr, this); } + public void Shuffle(short[] arr, Uniform.Interface.Trait t) { + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.SHORT, this, arr, t); + } + 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); } From 6e282dbfa4029f6d712f3f51ba2d39dbc02f5f04 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 14 Feb 2024 14:26:44 +0000 Subject: [PATCH 03/10] Fix proof of equivalence and format --- src/DafnyVMCTrait.dfy | 12 ++++++------ src/Distributions/Uniform/Interface.dfy | 2 +- src/Util/FisherYates/Implementation.dfy | 6 +++--- src/Util/FisherYates/Interface.dfy | 4 ++-- 4 files changed, 12 insertions(+), 12 deletions(-) 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/Uniform/Interface.dfy b/src/Distributions/Uniform/Interface.dfy index fbbf08fb..94be42e7 100644 --- a/src/Distributions/Uniform/Interface.dfy +++ b/src/Distributions/Uniform/Interface.dfy @@ -22,7 +22,7 @@ module Uniform.Interface { } trait {:termination false} Trait extends TraitMinus { - + method UniformIntervalSample(a: int, b: int) returns (u: int) modifies `s decreases * diff --git a/src/Util/FisherYates/Implementation.dfy b/src/Util/FisherYates/Implementation.dfy index 8220bfd1..727e9fe2 100644 --- a/src/Util/FisherYates/Implementation.dfy +++ b/src/Util/FisherYates/Implementation.dfy @@ -14,13 +14,13 @@ module FisherYates.Implementation { method Shuffle(a: array, t: Uniform.Interface.Trait := this) decreases * - modifies `s, a - ensures Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s) + modifies this, a, t + ensures (t == this) ==> 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 - invariant Equivalence.LoopInvariant(prevI, i, a, prevASeq, old(a[..]), old(s), prevS, s) + invariant (t == this) ==> Equivalence.LoopInvariant(prevI, i, a, prevASeq, old(a[..]), old(s), prevS, s) { prevI, prevASeq, prevS := i, a[..], s; // ghost var j := t.UniformIntervalSample(i, a.Length); diff --git a/src/Util/FisherYates/Interface.dfy b/src/Util/FisherYates/Interface.dfy index 6fc1c611..f02d92ab 100644 --- a/src/Util/FisherYates/Interface.dfy +++ b/src/Util/FisherYates/Interface.dfy @@ -12,8 +12,8 @@ module FisherYates.Interface { method Shuffle(a: array, t: Uniform.Interface.Trait := this) decreases * - modifies `s, a - ensures Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s) + modifies this, a, t + ensures (t == this) ==> Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s) } } \ No newline at end of file From a526616f857a55de1c63de1a34b7cc4b6ec5c00e Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 21 Feb 2024 17:31:31 +0000 Subject: [PATCH 04/10] add faulty example --- build/java/run.sh | 2 +- docs/java/BuildTest.java | 6 ++++ docs/java/CustomUniformSampleFaulty.java | 30 +++++++++++++++++++ src/Distributions/Bitstream/Interface.dfy | 12 ++++++++ src/Distributions/Uniform/Interface.dfy | 3 +- .../UniformPowerOfTwo/Interface.dfy | 5 ++-- 6 files changed, 53 insertions(+), 5 deletions(-) create mode 100644 docs/java/CustomUniformSampleFaulty.java create mode 100644 src/Distributions/Bitstream/Interface.dfy diff --git a/build/java/run.sh b/build/java/run.sh index 48b8fd31..bc262468 100755 --- a/build/java/run.sh +++ b/build/java/run.sh @@ -1,3 +1,3 @@ #1/bin/bash -javac -classpath "build/java/DafnyVMC.jar:docs/java/" docs/java/CustomUniformSample.java +javac -classpath "build/java/DafnyVMC.jar:docs/java/" docs/java/CustomUniformSample.java docs/java/CustomUniformSampleFaulty.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 7edab271..03970c41 100644 --- a/docs/java/BuildTest.java +++ b/docs/java/BuildTest.java @@ -9,6 +9,7 @@ public class BuildTest { public static void main(String[] args) { BigInteger[] arr1 = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)}; + BigInteger[] arr1b = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)}; int[] arr2 = {0, 1, 2}; String[] arr3 = {"aa", "bb", "cc"}; char[] arr4 = {'a', 'b', 'c'}; @@ -20,6 +21,7 @@ public static void main(String[] args) { DafnyVMC.Random r = new DafnyVMC.Random(); Uniform.Interface.Trait t = new CustomUniformSample(); + Uniform.Interface.Trait t_faulty = new CustomUniformSampleFaulty(); System.out.println("Example of Uniform sampling"); System.out.println(r.UniformSample(BigInteger.valueOf(4))); @@ -43,6 +45,10 @@ public static void main(String[] args) { System.out.println("Example of custom Fisher-Yates: BigInteger"); r.Shuffle(arr1, t); System.out.println(Arrays.toString(arr1)); + + System.out.println("Example of faulty custom Fisher-Yates: BigInteger"); + r.Shuffle(arr1b, t_faulty); + System.out.println(Arrays.toString(arr1b)); System.out.println("Example of Fisher-Yates: int"); r.Shuffle(arr2); diff --git a/docs/java/CustomUniformSampleFaulty.java b/docs/java/CustomUniformSampleFaulty.java new file mode 100644 index 00000000..59c62883 --- /dev/null +++ b/docs/java/CustomUniformSampleFaulty.java @@ -0,0 +1,30 @@ +import Uniform.Interface.TraitMinus; +import Uniform.Interface.Trait; +import java.math.BigInteger; +import java.security.SecureRandom; +import java.util.Random; + +class CustomUniformSampleFaultyMinus implements Uniform.Interface.TraitMinus { + static ThreadLocal rng; + + public CustomUniformSampleFaultyMinus() { + CustomUniformSampleFaultyMinus.rng = ThreadLocal.withInitial(CustomUniformSampleFaultyMinus::createSecureRandom); + } + + private static final SecureRandom createSecureRandom() { + final SecureRandom rng = new SecureRandom(); + // Required for proper initialization + rng.nextBoolean(); + return rng; + } + + public BigInteger UniformSample(BigInteger n) { + return BigInteger.valueOf(0); // Faulty; only for demonstration purposes + } +} + +public class CustomUniformSampleFaulty 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); + } +} \ No newline at end of file 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 94be42e7..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} TraitMinus extends UniformPowerOfTwo.Interface.Trait { + trait {:termination false} TraitMinus extends Bitstream.Interface.Trait { method UniformSample(n: Pos.pos) returns (u: nat) modifies `s 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 From d2d449760c55b82683c67b968893d741f453a298 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 21 Feb 2024 17:32:54 +0000 Subject: [PATCH 05/10] minimal faulty example --- docs/java/CustomUniformSampleFaulty.java | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/docs/java/CustomUniformSampleFaulty.java b/docs/java/CustomUniformSampleFaulty.java index 59c62883..c76aaa2b 100644 --- a/docs/java/CustomUniformSampleFaulty.java +++ b/docs/java/CustomUniformSampleFaulty.java @@ -5,19 +5,6 @@ import java.util.Random; class CustomUniformSampleFaultyMinus implements Uniform.Interface.TraitMinus { - static ThreadLocal rng; - - public CustomUniformSampleFaultyMinus() { - CustomUniformSampleFaultyMinus.rng = ThreadLocal.withInitial(CustomUniformSampleFaultyMinus::createSecureRandom); - } - - private static final SecureRandom createSecureRandom() { - final SecureRandom rng = new SecureRandom(); - // Required for proper initialization - rng.nextBoolean(); - return rng; - } - public BigInteger UniformSample(BigInteger n) { return BigInteger.valueOf(0); // Faulty; only for demonstration purposes } From 51c873890f5193a007c576f0295b7116081adc90 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 21 Feb 2024 17:34:24 +0000 Subject: [PATCH 06/10] remove imports --- docs/java/CustomUniformSampleFaulty.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/docs/java/CustomUniformSampleFaulty.java b/docs/java/CustomUniformSampleFaulty.java index c76aaa2b..d6ec88fe 100644 --- a/docs/java/CustomUniformSampleFaulty.java +++ b/docs/java/CustomUniformSampleFaulty.java @@ -1,8 +1,6 @@ import Uniform.Interface.TraitMinus; import Uniform.Interface.Trait; import java.math.BigInteger; -import java.security.SecureRandom; -import java.util.Random; class CustomUniformSampleFaultyMinus implements Uniform.Interface.TraitMinus { public BigInteger UniformSample(BigInteger n) { From efa003f6e3dcc10f9e1e0ca405a0f2557debd795 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 21 Feb 2024 21:06:19 +0000 Subject: [PATCH 07/10] simpler api --- build/java/run.sh | 2 +- docs/java/BuildTest.java | 80 +++++++++++++------ docs/java/CustomFIsherYatesFaulty.java | 58 ++++++++++++++ ...formSample.java => CustomFisherYates.java} | 46 ++++++++++- docs/java/CustomUniformSampleFaulty.java | 15 ---- src/Util/FisherYates/Implementation.dfy | 10 +-- src/Util/FisherYates/Interface.dfy | 6 +- src/interop/java/Full/Random.java | 46 +++-------- 8 files changed, 176 insertions(+), 87 deletions(-) create mode 100644 docs/java/CustomFIsherYatesFaulty.java rename docs/java/{CustomUniformSample.java => CustomFisherYates.java} (52%) delete mode 100644 docs/java/CustomUniformSampleFaulty.java diff --git a/build/java/run.sh b/build/java/run.sh index bc262468..94fd5695 100755 --- a/build/java/run.sh +++ b/build/java/run.sh @@ -1,3 +1,3 @@ #1/bin/bash -javac -classpath "build/java/DafnyVMC.jar:docs/java/" docs/java/CustomUniformSample.java docs/java/CustomUniformSampleFaulty.java +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 03970c41..6c570dcb 100644 --- a/docs/java/BuildTest.java +++ b/docs/java/BuildTest.java @@ -1,27 +1,35 @@ -import java.security.SecureRandom; import java.math.BigInteger; import java.util.Arrays; -import DafnyVMC.Random; -import Uniform.Interface.TraitMinus; -import Uniform.Interface.Trait; - public class BuildTest { public static void main(String[] args) { BigInteger[] arr1 = {BigInteger.valueOf(0), BigInteger.valueOf(1), BigInteger.valueOf(2)}; - BigInteger[] arr1b = {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); DafnyVMC.Random r = new DafnyVMC.Random(); - Uniform.Interface.Trait t = new CustomUniformSample(); - Uniform.Interface.Trait t_faulty = new CustomUniformSampleFaulty(); + 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))); @@ -43,60 +51,84 @@ public static void main(String[] args) { System.out.println(Arrays.toString(arr1)); System.out.println("Example of custom Fisher-Yates: BigInteger"); - r.Shuffle(arr1, t); - System.out.println(Arrays.toString(arr1)); + r_custom.Shuffle(arr1_custom); + System.out.println(Arrays.toString(arr1_custom)); System.out.println("Example of faulty custom Fisher-Yates: BigInteger"); - r.Shuffle(arr1b, t_faulty); - System.out.println(Arrays.toString(arr1b)); + 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.Shuffle(arr2, t); - System.out.println(Arrays.toString(arr2)); + 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.Shuffle(arr3, t); - System.out.println(Arrays.toString(arr3)); + 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.Shuffle(arr4, t); - System.out.println(Arrays.toString(arr4)); + 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.Shuffle(arr5, t); - System.out.println(Arrays.toString(arr5)); + 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.Shuffle(arr6, t); - System.out.println(Arrays.toString(arr6)); + 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)); System.out.println("Example of custom Fisher-Yates: short"); - r.Shuffle(arr7, t); - System.out.println(Arrays.toString(arr7)); + r_custom.Shuffle(arr7_custom); + System.out.println(Arrays.toString(arr7_custom)); + + System.out.println("Example of faulty custom Fisher-Yates: short"); + r_faulty.Shuffle(arr7_faulty); + System.out.println(Arrays.toString(arr7_faulty)); } } 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/docs/java/CustomUniformSample.java b/docs/java/CustomFisherYates.java similarity index 52% rename from docs/java/CustomUniformSample.java rename to docs/java/CustomFisherYates.java index 8ecb3f0d..1d3b12b6 100644 --- a/docs/java/CustomUniformSample.java +++ b/docs/java/CustomFisherYates.java @@ -3,6 +3,7 @@ import java.math.BigInteger; import java.security.SecureRandom; import java.util.Random; +import dafny.TypeDescriptor; class CustomUniformSampleMinus implements Uniform.Interface.TraitMinus { static ThreadLocal rng; @@ -40,8 +41,49 @@ public BigInteger UniformSample(BigInteger n) { } } -public class CustomUniformSample extends CustomUniformSampleMinus implements Uniform.Interface.Trait { +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); } -} \ No newline at end of file +} + + +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/CustomUniformSampleFaulty.java b/docs/java/CustomUniformSampleFaulty.java deleted file mode 100644 index d6ec88fe..00000000 --- a/docs/java/CustomUniformSampleFaulty.java +++ /dev/null @@ -1,15 +0,0 @@ -import Uniform.Interface.TraitMinus; -import Uniform.Interface.Trait; -import java.math.BigInteger; - -class CustomUniformSampleFaultyMinus implements Uniform.Interface.TraitMinus { - public BigInteger UniformSample(BigInteger n) { - return BigInteger.valueOf(0); // Faulty; only for demonstration purposes - } -} - -public class CustomUniformSampleFaulty 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); - } -} \ No newline at end of file diff --git a/src/Util/FisherYates/Implementation.dfy b/src/Util/FisherYates/Implementation.dfy index 727e9fe2..20a1b5b1 100644 --- a/src/Util/FisherYates/Implementation.dfy +++ b/src/Util/FisherYates/Implementation.dfy @@ -12,18 +12,18 @@ module FisherYates.Implementation { trait {:termination false} Trait extends Interface.Trait { - method Shuffle(a: array, t: Uniform.Interface.Trait := this) + method Shuffle(a: array) decreases * - modifies this, a, t - ensures (t == this) ==> Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s) + modifies `s, a + 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 - invariant (t == this) ==> Equivalence.LoopInvariant(prevI, i, a, prevASeq, old(a[..]), old(s), prevS, s) + invariant Equivalence.LoopInvariant(prevI, i, a, prevASeq, old(a[..]), old(s), prevS, s) { prevI, prevASeq, prevS := i, a[..], s; // ghost - var j := t.UniformIntervalSample(i, a.Length); + var j := UniformIntervalSample(i, a.Length); assert prevASeq == a[..]; // ghost Swap(a, i, j); } diff --git a/src/Util/FisherYates/Interface.dfy b/src/Util/FisherYates/Interface.dfy index f02d92ab..1571870d 100644 --- a/src/Util/FisherYates/Interface.dfy +++ b/src/Util/FisherYates/Interface.dfy @@ -10,10 +10,10 @@ module FisherYates.Interface { trait {:termination false} Trait extends Uniform.Interface.Trait { - method Shuffle(a: array, t: Uniform.Interface.Trait := this) + method Shuffle(a: array) decreases * - modifies this, a, t - ensures (t == this) ==> Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s) + modifies `s, a + ensures Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s) } } \ No newline at end of file diff --git a/src/interop/java/Full/Random.java b/src/interop/java/Full/Random.java index 7a0c60f0..a186e8ca 100644 --- a/src/interop/java/Full/Random.java +++ b/src/interop/java/Full/Random.java @@ -95,64 +95,36 @@ public java.math.BigInteger DiscreteLaplaceSample(java.math.BigInteger num, java return DafnyVMCTrait._Companion_RandomTrait.DiscreteLaplaceSample(this, num, den); } - public <__T> void Shuffle(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a, Uniform.Interface.Trait t) { - FisherYates.Implementation._Companion_Trait.Shuffle(_td___T, this, a, t); + public <__T> void Shuffle(dafny.TypeDescriptor<__T> _td___T, java.lang.Object a) { + FisherYates.Implementation._Companion_Trait.Shuffle(_td___T, this, a); } public void Shuffle(BigInteger[] arr) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BIG_INTEGER, this, arr, this); - } - - public void Shuffle(BigInteger[] arr, Uniform.Interface.Trait t) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BIG_INTEGER, this, arr, t); + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BIG_INTEGER, this, arr); } public void Shuffle(int[] arr) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.INT, this, arr, this); - } - - public void Shuffle(int[] arr, Uniform.Interface.Trait t) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.INT, this, arr, t); + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.INT, this, arr); } public void Shuffle(String[] arr) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR_ARRAY, this, arr, this); - } - - public void Shuffle(String[] arr, Uniform.Interface.Trait t) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR_ARRAY, this, arr, t); + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR_ARRAY, this, arr); } public void Shuffle(char[] arr) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR, this, arr, this); - } - - public void Shuffle(char[] arr, Uniform.Interface.Trait t) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR, this, arr, t); + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.CHAR, this, arr); } public void Shuffle(boolean[] arr) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BOOLEAN, this, arr, this); - } - - public void Shuffle(boolean[] arr, Uniform.Interface.Trait t) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BOOLEAN, this, arr, t); + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.BOOLEAN, this, arr); } public void Shuffle(long[] arr) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.LONG, this, arr, this); - } - - public void Shuffle(long[] arr, Uniform.Interface.Trait t) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.LONG, this, arr, t); + FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.LONG, this, arr); } public void Shuffle(short[] arr) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.SHORT, this, arr, this); - } - - public void Shuffle(short[] arr, Uniform.Interface.Trait t) { - FisherYates.Implementation._Companion_Trait.Shuffle(TypeDescriptor.SHORT, this, arr, t); + 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) { From fbd3f5e7076c86204cce39ca4f164689362c9523 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 21 Feb 2024 21:11:20 +0000 Subject: [PATCH 08/10] add back constructor with supplier argument --- src/interop/java/Full/Random.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/interop/java/Full/Random.java b/src/interop/java/Full/Random.java index a186e8ca..94b38f75 100644 --- a/src/interop/java/Full/Random.java +++ b/src/interop/java/Full/Random.java @@ -12,6 +12,10 @@ public Random() { this.rng = ThreadLocal.withInitial(Random::createSecureRandom); } + public Random(Supplier supplier) { + this.rng = ThreadLocal.withInitial(supplier); + } + private static final SecureRandom createSecureRandom() { final SecureRandom rng = new SecureRandom(); // Required for proper initialization From a2ebf0e89142cd554f9f77c22949060ef561241b Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 21 Feb 2024 21:16:39 +0000 Subject: [PATCH 09/10] remove file with typo --- docs/java/CustomFIsherYatesFaulty.java | 58 -------------------------- 1 file changed, 58 deletions(-) delete mode 100644 docs/java/CustomFIsherYatesFaulty.java diff --git a/docs/java/CustomFIsherYatesFaulty.java b/docs/java/CustomFIsherYatesFaulty.java deleted file mode 100644 index 82fb57ea..00000000 --- a/docs/java/CustomFIsherYatesFaulty.java +++ /dev/null @@ -1,58 +0,0 @@ -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); - } -} From 20faba2ae1a9b445f672bba2639cfd04b86ba2e2 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 21 Feb 2024 21:17:19 +0000 Subject: [PATCH 10/10] readd file --- docs/java/CustomFisherYatesFaulty.java | 58 ++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) create mode 100644 docs/java/CustomFisherYatesFaulty.java 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); + } +}