diff --git a/docs/java/BuildTest.java b/docs/java/BuildTest.java index c7f64faf..920fb3cf 100644 --- a/docs/java/BuildTest.java +++ b/docs/java/BuildTest.java @@ -24,6 +24,57 @@ public static void main(String[] args) { 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(); + + System.out.println("Example of Coin sampling"); + System.out.println(r.CoinSample()); + + System.out.println("Example of Uniform sampling"); + System.out.println(r.UniformSample(BigInteger.valueOf(4))); + + System.out.println("Example of Bernoulli sampling"); + System.out.println(r.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(r.DiscreteGaussianSample(gamma)); + + System.out.println("Example of DiscreteLaplace sampling"); + System.out.println(r.DiscreteLaplaceSample(gamma)); + + 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\n"); diff --git a/src/interop/java/Full/Random.java b/src/interop/java/Full/Random.java index 51b95c1b..3e2600a6 100644 --- a/src/interop/java/Full/Random.java +++ b/src/interop/java/Full/Random.java @@ -2,19 +2,40 @@ import dafny.TypeDescriptor; import java.math.BigInteger; +import java.security.SecureRandom; import java.util.function.Function; public class Random implements DafnyVMCTrait.RandomTrait { static Function unif; + public Random() { + ThreadLocal rng = ThreadLocal.withInitial(Random::createSecureRandom); + Random.unif = n -> UniformPowerOfTwoSample(n, rng); + } + public Random(Function unif) { Random.unif = unif; } + private static final SecureRandom createSecureRandom() { + final SecureRandom rng = new SecureRandom(); + // Required for proper initialization + rng.nextBoolean(); + return rng; + } + public BigInteger UniformPowerOfTwoSample(BigInteger n) { return unif.apply(n); } + public BigInteger UniformPowerOfTwoSample(BigInteger n, ThreadLocal rng) { + if (n.compareTo(BigInteger.ONE) < 0) { + throw new IllegalArgumentException("n must be positive"); + } + + return new BigInteger(n.bitLength()-1, rng.get()); + } + public java.math.BigInteger UniformIntervalSample(java.math.BigInteger a, java.math.BigInteger b) { return Uniform.Interface._Companion_Trait.UniformIntervalSample(this, a, b); }