Extern UniformPowerOfTwo (#114)

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).
dafny-lang · Nov 7, 2023 · ee83a0e · ee83a0e
1 parent b21286d
commit ee83a0e
Show file tree

Hide file tree

Showing 14 changed files with 67 additions and 79 deletions.
diff --git a/audit.log b/audit.log
@@ -2,7 +2,7 @@ src/Distributions/BernoulliExpNeg/Correctness.dfy(13,17): Correctness: Declarati
 src/Distributions/BernoulliExpNeg/Correctness.dfy(17,17): SampleIsIndep: Declaration has explicit `{:axiom}` attribute. 
 src/Distributions/BernoulliExpNeg/Model.dfy(102,17): GammaLe1LoopTerminatesAlmostSurely: Declaration has explicit `{:axiom}` attribute. 
 src/Distributions/Coin/Interface.dfy(21,6): CoinSample: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/Uniform/Implementation.dfy(47,6): UniformSample: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/UniformPowerOfTwo/Implementation.dfy(42,6): UniformPowerOfTwoSample: Definition has `assume {:axiom}` statement in body. 
 src/Math/Analysis/Reals.dfy(35,17): LeastUpperBoundProperty: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Exponential.dfy(11,17): EvalOne: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Exponential.dfy(2,26): Exp: Declaration has explicit `{:axiom}` attribute. 

diff --git a/docs/csharp/BuildTest.cs b/docs/csharp/BuildTest.cs
@@ -1,3 +1,3 @@
 using DafnyVMC;
 
-DRandomExternUniform d = new DRandomExternUniform();
+DRandomExternUniformPowerOfTwo d = new DRandomExternUniformPowerOfTwo();
diff --git a/docs/dafny/ExamplesExternUniform.dfy → ...dafny/ExamplesExternUniformPowerOfTwo.dfy b/docs/dafny/ExamplesExternUniform.dfy → ...dafny/ExamplesExternUniformPowerOfTwo.dfy
@@ -11,7 +11,7 @@ module RandomExamples.ExternUniform {
     decreases *
   {
     var n := 100000;
-    var r: DafnyVMC.DRandomExternUniform := new DafnyVMC.DRandomExternUniform();
+    var r: DafnyVMC.DRandomExternUniformPowerOfTwo := new DafnyVMC.DRandomExternUniformPowerOfTwo();
 
     var t := 0;
     for i := 0 to n {

diff --git a/docs/java/BuildTest.java b/docs/java/BuildTest.java
@@ -3,7 +3,7 @@
 
 class Check {
     public static void main(String[] args) {
-        DRandomExternUniform d = new DRandomExternUniform();
+        DRandomExternUniformPowerOfTwo d = new DRandomExternUniformPowerOfTwo();
         System.out.println(d.UniformSample(BigInteger.valueOf(4))); 
     }
 }
diff --git a/scripts/build.sh b/scripts/build.sh
@@ -14,4 +14,4 @@ then
   exit 1
 fi
 
-$DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG src/Dafny-VMC.dfy -o build/$TARGET_LANG/Dafny-VMC dfyconfig.toml --no-verify
+$DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG src/Dafny-VMC.dfy -o build/$TARGET_LANG/Dafny-VMC dfyconfig.toml --no-verify
diff --git a/scripts/test.sh b/scripts/test.sh
@@ -16,14 +16,14 @@ fi
 
 echo Running $TARGET_LANG tests...
 echo "Running tests/TestsFoundational.dfy:"
-time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG tests/TestsFoundational.dfy tests/Tests.dfy dfyconfig.toml --no-verify
+time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG tests/TestsFoundational.dfy tests/Tests.dfy dfyconfig.toml --no-verify
 echo "Running tests/TestsExternUniform.dfy:"
-time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG tests/TestsExternUniform.dfy tests/Tests.dfy dfyconfig.toml  --no-verify
+time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG tests/TestsExternUniformPowerOfTwo.dfy tests/Tests.dfy dfyconfig.toml  --no-verify
 
 echo Running $TARGET_LANG documentation...
 
 echo "Building docs/dafny/ExamplesFoundational.dfy..." 
-$DAFNY build docs/dafny/ExamplesFoundational.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG dfyconfig.toml --no-verify
+$DAFNY build docs/dafny/ExamplesFoundational.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG dfyconfig.toml --no-verify
 echo "Executing compiled docs/dafny/ExamplesFoundational.dfy:" 
 if [ "$TARGET_LANG" = "cs" ]
 then
@@ -32,12 +32,12 @@ else
   java -jar docs/dafny/ExamplesFoundational.jar
 fi
 
-echo "Building docs/dafny/ExamplesExternUniform.dfy..." 
-$DAFNY build docs/dafny/ExamplesExternUniform.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG dfyconfig.toml --no-verify
-echo "Executing compiled docs/dafny/ExamplesExternUniform.dfy:" 
+echo "Building docs/dafny/ExamplesExternUniformPowerOfTwo.dfy..." 
+$DAFNY build docs/dafny/ExamplesExternUniformPowerOfTwo.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG dfyconfig.toml --no-verify
+echo "Executing compiled docs/dafny/ExamplesExternUniformPowerOfTwo.dfy:" 
 if [ "$TARGET_LANG" = "cs" ]
 then
-  dotnet docs/dafny/ExamplesExternUniform.dll
+  dotnet docs/dafny/ExamplesExternUniformPowerOfTwo.dll
 else
-  java -jar docs/dafny/ExamplesExternUniform.jar
+  java -jar docs/dafny/ExamplesExternUniformPowerOfTwo.jar
 fi
diff --git a/scripts/verify.sh b/scripts/verify.sh
@@ -9,4 +9,4 @@ then
 fi
 
 echo Verifying the proofs...
-time $DAFNY verify dfyconfig.toml docs/dafny/ExamplesExternUniform.dfy docs/dafny/ExamplesFoundational.dfy tests/Tests.dfy tests/TestsExternUniform.dfy tests/TestsFoundational.dfy --resource-limit 20000 # 20M resource usage
+time $DAFNY verify dfyconfig.toml docs/dafny/ExamplesExternUniformPowerOfTwo.dfy docs/dafny/ExamplesFoundational.dfy tests/Tests.dfy tests/TestsExternUniformPowerOfTwo.dfy tests/TestsFoundational.dfy --resource-limit 20000 # 20M resource usage
diff --git a/src/Dafny-VMC.dfy b/src/Dafny-VMC.dfy
@@ -16,7 +16,7 @@ module DafnyVMC {
     constructor {:extern} ()
   }
 
-  class DRandomExternUniform extends Coin.Interface.Trait, UniformPowerOfTwo.Implementation.Trait, Bernoulli.Implementation.Trait, Uniform.Implementation.TraitExtern, BernoulliExpNeg.Implementation.Trait, DiscreteGaussian.Implementation.Trait, DiscreteLaplace.Implementation.Trait {
+  class DRandomExternUniformPowerOfTwo extends Coin.Interface.Trait, UniformPowerOfTwo.Implementation.TraitExtern, Bernoulli.Implementation.Trait, Uniform.Implementation.TraitFoundational, BernoulliExpNeg.Implementation.Trait, DiscreteGaussian.Implementation.Trait, DiscreteLaplace.Implementation.Trait {
     constructor {:extern} ()
   }
 }
diff --git a/src/Distributions/Uniform/Implementation.dfy b/src/Distributions/Uniform/Implementation.dfy
@@ -32,19 +32,4 @@ module Uniform.Implementation {
       reveal Model.Sample();
     }
   }
-
-  method {:extern "DRandomUniform", "Uniform"} ExternUniformSample(n: nat) returns (u: nat)
-
-  trait {:termination false} TraitExtern extends Interface.Trait {
-    method UniformSample(n: nat) returns (u: nat)
-      modifies this
-      decreases *
-      requires n > 0
-      ensures u < n
-      ensures Model.Sample(n)(old(s)) == Monad.Result(u, s)
-    {
-      u := ExternUniformSample(n);
-      assume {:axiom} false; // assume correctness of extern implementation
-    }
-  }
 }
diff --git a/src/Distributions/UniformPowerOfTwo/Implementation.dfy b/src/Distributions/UniformPowerOfTwo/Implementation.dfy
@@ -29,4 +29,17 @@ module UniformPowerOfTwo.Implementation {
       Equivalence.SampleCorrespondence(n, old(s));
     }
   }
+
+  method {:extern "DRandomUniformPowerOfTwo", "UniformPowerOfTwo"} ExternUniformPowerOfTwoSample(n: nat) returns (u: nat)
+
+  trait {:termination false} TraitExtern extends Interface.Trait {
+    method UniformPowerOfTwoSample(n: nat) returns (u: nat)
+      requires n >= 1
+      modifies this
+      ensures Model.Sample(n)(old(s)) == Monad.Result(u, s)
+    {
+      u := ExternUniformPowerOfTwoSample(n);
+      assume {:axiom} false; // assume correctness of extern implementation
+    }
+  }
 }
diff --git a/src/interop/cs/DRandomUniform.cs → src/interop/cs/DRandomUniformPowerOfTwo.cs b/src/interop/cs/DRandomUniform.cs → src/interop/cs/DRandomUniformPowerOfTwo.cs
@@ -6,13 +6,13 @@
 using System;
 using System.Numerics;
 
-namespace Uniform_mImplementation {
+namespace UniformPowerOfTwo_mImplementation {
 
-    public class DRandomUniform {
+    public class DRandomUniformPowerOfTwo {
 
       private static Random r = new Random();
 
-      public static BigInteger Uniform(BigInteger n) {
+      public static BigInteger UniformPowerOfTwo(BigInteger n) {
         // `(Int64) n` throws an `OverflowException` if `n` is too large to fit in an `Int64`
         // see https://learn.microsoft.com/en-us/dotnet/api/system.numerics.biginteger.op_explicit?view=net-7.0#system-numerics-biginteger-op-explicit(system-numerics-biginteger)-system-int64
         return new BigInteger(r.NextInt64((Int64) n));

diff --git a/src/interop/java/DRandomUniform.java b/src/interop/java/DRandomUniform.java
diff --git a/src/interop/java/DRandomUniformPowerOfTwo.java b/src/interop/java/DRandomUniformPowerOfTwo.java
@@ -0,0 +1,27 @@
+package UniformPowerOfTwo_mImplementation;
+
+import java.security.SecureRandom;
+import java.math.BigInteger;
+import java.lang.Thread;
+
+public final class DRandomUniformPowerOfTwo {
+
+  private static final ThreadLocal<SecureRandom> RNG = ThreadLocal.withInitial(DRandomUniformPowerOfTwo::createSecureRandom);
+
+  private DRandomUniformPowerOfTwo() {} // Prevent instantiation
+
+  private static final SecureRandom   createSecureRandom() {
+    final SecureRandom rng = new SecureRandom();
+    // Required for proper initialization
+    rng.nextBoolean(); 
+    return rng;
+  }
+
+  public static BigInteger UniformPowerOfTwo(BigInteger n) {
+    if (n.compareTo(BigInteger.ONE) < 0) {
+      throw new IllegalArgumentException("n must be positive");
+    }
+
+    return new BigInteger(n.bitLength()-1, RNG.get());
+  }
+}
diff --git a/tests/TestsExternUniform.dfy → tests/TestsExternUniformPowerOfTwo.dfy b/tests/TestsExternUniform.dfy → tests/TestsExternUniformPowerOfTwo.dfy
@@ -8,63 +8,63 @@ module TestsExternUniform {
   import Tests
 
   method {:test} TestCoin() {
-    var r := new DafnyVMC.DRandomExternUniform();
+    var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
     Tests.TestCoin(1_000_000, r);
   }
 
   method {:test} TestUniform()
     decreases *
   {
-    var r := new DafnyVMC.DRandomExternUniform();
+    var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
     Tests.TestUniform(1_000_000, r);
   }
 
   method {:test} TestUniformInterval()
     decreases *
   {
-    var r := new DafnyVMC.DRandomExternUniform();
+    var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
     Tests.TestUniformInterval(1_000_000, r);
   }
 
   method {:test} TestBernoulli()
     decreases *
   {
-    var r := new DafnyVMC.DRandomExternUniform();
+    var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
     Tests.TestBernoulli(1_000_000, r);
   }
 
   method {:test} TestBernoulli2()
     decreases *
   {
-    var r := new DafnyVMC.DRandomExternUniform();
+    var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
     Tests.TestBernoulli2(1_000_000, r);
   }
 
   method {:test} TestBernoulli3()
     decreases *
   {
-    var r := new DafnyVMC.DRandomExternUniform();
+    var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
     Tests.TestBernoulli3(1_000_000, r);
   }
 
   method {:test} TestBernoulliExpNeg()
     decreases *
   {
-    var r := new DafnyVMC.DRandomExternUniform();
+    var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
     Tests.TestBernoulliExpNeg(1_000_000, r);
   }
 
   method {:test} TestDiscreteLaplace()
     decreases *
   {
-    var r := new DafnyVMC.DRandomExternUniform();
+    var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
     Tests.TestDiscreteLaplace(1_000_000, r);
   }
 
   method {:test} TestDiscreteGaussian()
     decreases *
   {
-    var r := new DafnyVMC.DRandomExternUniform();
+    var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
     Tests.TestDiscreteGaussian(1_000_000, r);
   }
 }