Merge branch 'main' into benchmarks

dafny-lang · Mar 18, 2024 · 6ac6d44 · 6ac6d44
2 parents e0c7f16 + 28f5169
commit 6ac6d44
Show file tree

Hide file tree

Showing 24 changed files with 109 additions and 365 deletions.
diff --git a/audit.log b/audit.log
@@ -1,2 +1,3 @@
+src/DafnyVMC.dfy(35,27): UniformSample32: Declaration has `{:verify false}` attribute. 
 src/Distributions/Uniform/Model.dfy(19,26): Sample: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/RandomSource.dfy(50,17): ProbIsProbabilityMeasure: Declaration has explicit `{:axiom}` attribute. 
diff --git a/build/java/run_samplers.sh b/build/java/run_samplers.sh
@@ -1,4 +1,3 @@
 #1/bin/bash
 
-java -classpath build/java/DafnyVMC.jar docs/java/TestSamplers.java
-java -classpath build/java/DafnyVMC.jar docs/java/CustomTestSamplers.java
+java -classpath build/java/DafnyVMC.jar docs/java/TestSamplers.java
diff --git a/build/java/run_shuffling.sh b/build/java/run_shuffling.sh
@@ -1,4 +1,3 @@
 #1/bin/bash
 
-java -classpath build/java/DafnyVMC.jar docs/java/TestShuffling.java
-java -classpath build/java/DafnyVMC.jar docs/java/CustomTestShuffling.java
+java -classpath build/java/DafnyVMC.jar docs/java/TestShuffling.java
diff --git a/build/py/run_samplers.sh b/build/py/run_samplers.sh
@@ -1,4 +1,3 @@
 #1/bin/bash
 
-PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestSamplers.py 
-PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/CustomTestSamplers.py
+PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestSamplers.py 
diff --git a/build/py/run_shuffling.sh b/build/py/run_shuffling.sh
@@ -1,4 +1,3 @@
 #1/bin/bash
 
-PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestShuffling.py 
-PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/CustomTestShuffling.py
+PYTHONPATH=.:build/py/DafnyVMC-py python3 docs/py/TestShuffling.py 
diff --git a/docs/dafny/ExamplesRandom.dfy b/docs/dafny/ExamplesRandom.dfy
@@ -118,7 +118,7 @@ module Examples {
     // https://www.wolframalpha.com/input?i=ReplaceAll%5BE%5E%28-x%5E2+%2F+%282+*%CF%83%5E2%29%29+%2F+Sum%5BE%5E%28-y%5E2%2F%282+%CF%83%5E2%29%29%2C+%7By%2C+-Infinity%2C+Infinity%7D%5D%2C+%7Bx+-%3E+1%2C+%CF%83+-%3E+1.4%7D%5D
     print "Estimated probabilities for DiscreteGaussianSample(1.4): ", count0 as real / n as real, " (should be around 0.284959) and ", count1 as real / n as real, ", ", countneg1 as real / n as real, " (should both be around 0.220797)\n";
 
-    // Fisher-Yates Example
+    // Fisher-Yates Shuffle Example
     print "Ten permutations of 012: ";
     var arr: array<nat> := new nat[3](i => i); // [0, 1, 2]
     for i := 0 to 10 {

diff --git a/docs/java/CustomTestSamplers.java b/docs/java/CustomTestSamplers.java
diff --git a/docs/java/CustomTestShuffling.java b/docs/java/CustomTestShuffling.java
diff --git a/docs/py/CustomTestSamplers.py b/docs/py/CustomTestSamplers.py
diff --git a/docs/py/CustomTestShuffling.py b/docs/py/CustomTestShuffling.py
diff --git a/scripts/build.sh b/scripts/build.sh
@@ -16,7 +16,7 @@ fi
 
 if [ "$TARGET_LANG" = "java" ]
 then
-  $DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Full/CustomRandom.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG -o build/$TARGET_LANG/DafnyVMC dfyconfig.toml --no-verify
+  $DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG -o build/$TARGET_LANG/DafnyVMC dfyconfig.toml --no-verify
 else
   $DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG -o build/$TARGET_LANG/DafnyVMC dfyconfig.toml --no-verify
 fi
diff --git a/src/DafnyVMC.dfy b/src/DafnyVMC.dfy
@@ -4,9 +4,13 @@
  *******************************************************************************/
 
 module {:extern} DafnyVMCPartMaterial {
+  import opened Pos
+
   class {:extern} Random {
     // For running Dafny native testing with standard SecureRandom rng
     static method {:extern "UniformPowerOfTwoSample"} ExternUniformPowerOfTwoSample(n: nat) returns (u: nat)
+
+    static method {:extern "UniformSample32"} ExternUniformSample32(n: pos32) returns (u: nat32)
   }
 }
 
@@ -15,6 +19,8 @@ module {:extern "DafnyVMCPart"} DafnyVMC {
   import DafnyVMCPartMaterial
   import Monad
   import UniformPowerOfTwo
+  import Uniform
+  import opened Pos
 
   class Random extends DafnyVMCTrait.RandomTrait {
     constructor {:extern} ()
@@ -25,6 +31,15 @@ module {:extern "DafnyVMCPart"} DafnyVMC {
     {
       u := DafnyVMCPartMaterial.Random.ExternUniformPowerOfTwoSample(n);
     }
+
+    method {:verify false} UniformSample32(n: pos32) returns (u: nat32)
+      modifies `s
+      decreases *
+      ensures u < n
+      ensures Uniform.Model.Sample(n as nat)(old(s)) == Monad.Result(u as nat, s)
+    {
+      u := DafnyVMCPartMaterial.Random.ExternUniformSample32(n);
+    }
   }
 
 }