Skip to content

Commit

Permalink
Java integer fix (#110)
Browse files Browse the repository at this point in the history
By submitting this pull request, I confirm that my contribution is made
under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).
  • Loading branch information
stefan-aws committed Nov 3, 2023
1 parent ecdc5e6 commit 8b21c7d
Showing 1 changed file with 19 additions and 7 deletions.
26 changes: 19 additions & 7 deletions src/interop/java/DRandomUniform.java
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,7 @@
import java.lang.Thread;

public final class DRandomUniform {

private static final ThreadLocal<SecureRandom> RNG = ThreadLocal.withInitial(DRandomUniform::createSecureRandom);

private DRandomUniform() {} // Prevent instantiation

private static final SecureRandom createSecureRandom() {
Expand All @@ -17,9 +15,23 @@ private static final SecureRandom createSecureRandom() {
return rng;
}

public static BigInteger Uniform(BigInteger n) {
// `n.intValueExact` will throw an `ArithmeticException` if `n` does not fit in an `int`.
// see https://docs.oracle.com/javase/8/docs/api/java/math/BigInteger.html#intValueExact--
return BigInteger.valueOf(RNG.get().nextInt(n.intValueExact()));
/**
* Sample a uniform value using rejection sampling between [0, n).
*
* @param n an integer (must be >= 1)
* @return a uniform value between 0 and n-1
* @throws IllegalArgumentException if `n` is less than 1
*/
public static BigInteger Uniform(final BigInteger n) {
if (n.compareTo(BigInteger.ONE) < 0) {
throw new IllegalArgumentException("n must be positive");
}

BigInteger sampleValue;
do {
sampleValue = new BigInteger(n.bitLength(), RNG.get());
} while (sampleValue.compareTo(n) >= 0);

return sampleValue;
}
}
}

0 comments on commit 8b21c7d

Please sign in to comment.