Additional tests (#116)

Depends on #115 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 8, 2023 · bfcd165 · bfcd165
1 parent f627a24
commit bfcd165
Show file tree

Hide file tree

Showing 3 changed files with 84 additions and 19 deletions.
diff --git a/tests/Tests.dfy b/tests/Tests.dfy
@@ -7,15 +7,24 @@ module Tests {
   import Rationals
   import Coin
   import Uniform
+  import UniformPowerOfTwo
   import Bernoulli
   import BernoulliExpNeg
   import DiscreteLaplace
   import DiscreteGaussian
+  import Helper
 
   function Abs(x: real): real {
     if x < 0.0 then -x else x
   }
 
+  function natToString(n: nat): string {
+    match n
+    case 0 => "0" case 1 => "1" case 2 => "2" case 3 => "3" case 4 => "4"
+    case 5 => "5" case 6 => "6" case 7 => "7" case 8 => "8" case 9 => "9"
+    case _ => natToString(n / 10) + natToString(n % 10)
+  }
+
   method testBernoulliIsWithin4SigmaOfTrueMean(
     n: nat,
     empiricalSum: real,
@@ -39,7 +48,7 @@ module Tests {
     var empiricalMean := empiricalSum / n as real;
     var diff := Abs(empiricalMean - trueMean);
     var threshold := 4.0 * 4.0 * trueVariance / n as real;
-    if diff * diff > threshold {
+    if diff * diff >= threshold {
       print "Test failed: ", description, "\n";
       print "Difference between empirical and true mean: ", diff, "\n";
       print "squared difference: ", diff * diff, "\n";
@@ -48,7 +57,6 @@ module Tests {
     expect diff * diff < threshold, "Empirical mean should be within 3 sigma of true mean. This individual test may fail with probability of about 6.3e-5.";
   }
 
-
   method TestCoin(n: nat, r: Coin.Interface.Trait)
     requires n > 0
     modifies r
@@ -63,25 +71,40 @@ module Tests {
     testBernoulliIsWithin4SigmaOfTrueMean(n, t as real, 0.5, "p(true)");
   }
 
-  method TestUniform(n: nat, r: Uniform.Interface.Trait)
+  method TestUniformPowerOfTwo(n: nat, u: nat, r: UniformPowerOfTwo.Interface.Trait)
     decreases *
     requires n > 0
+    requires u > 0
     modifies r
   {
-    var a := 0;
-    var b := 0;
-    var c := 0;
+    var k := Helper.Log2Floor(u);
+    var a := new nat[Helper.Power(2, k)](i => 0);
     for i := 0 to n {
-      var k := r.UniformSample(3);
-      match k {
-        case 0 => a := a + 1;
-        case 1 => b := b + 1;
-        case 2 => c := c + 1;
-      }
+      var l := r.UniformPowerOfTwoSample(u);
+      expect 0 <= l < Helper.Power(2, k), "sample not in the right bound";
+      a[l] := a[l] + 1;
+    }
+    for i := 0 to Helper.Power(2, k) {
+      testBernoulliIsWithin4SigmaOfTrueMean(n, a[i] as real, 1.0 / (Helper.Power(2, k) as real), "p(" + natToString(i) + ")");
+    }
+  }
+
+  method TestUniform(n: nat, u: nat, r: Uniform.Interface.Trait)
+    decreases *
+    requires n > 0
+    requires u > 0
+    modifies r
+  {
+    var k := Helper.Log2Floor(u);
+    var a := new nat[u](i => 0);
+    for i := 0 to n {
+      var l := r.UniformSample(u);
+      expect 0 <= l < u, "sample not in the right bound";
+      a[l] := a[l] + 1;
+    }
+    for i := 0 to u {
+      testBernoulliIsWithin4SigmaOfTrueMean(n, a[i] as real, 1.0 / (u as real), "p(" + natToString(i) + ")");
     }
-    testBernoulliIsWithin4SigmaOfTrueMean(n, a as real, 1.0 / 3.0, "p(0)");
-    testBernoulliIsWithin4SigmaOfTrueMean(n, b as real, 1.0 / 3.0, "p(1)");
-    testBernoulliIsWithin4SigmaOfTrueMean(n, c as real, 1.0 / 3.0, "p(2)");
   }
 
   method TestUniformInterval(n: nat, r: Uniform.Interface.Trait)

diff --git a/tests/TestsExternUniformPowerOfTwo.dfy b/tests/TestsExternUniformPowerOfTwo.dfy
@@ -12,11 +12,32 @@ module TestsExternUniform {
     Tests.TestCoin(1_000_000, r);
   }
 
-  method {:test} TestUniform()
+  method {:test} TestUniformPowerOfTwo_10()
     decreases *
   {
     var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
-    Tests.TestUniform(1_000_000, r);
+    Tests.TestUniformPowerOfTwo(1_000_000, 10, r);
+  }
+
+  method {:test} TestUniformPowerOfTwo_100()
+    decreases *
+  {
+    var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
+    Tests.TestUniformPowerOfTwo(1_000_000, 100, r);
+  }
+
+  method {:test} TestUniform_10()
+    decreases *
+  {
+    var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
+    Tests.TestUniform(1_000_000, 10, r);
+  }
+
+  method {:test} TestUniform_100()
+    decreases *
+  {
+    var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
+    Tests.TestUniform(1_000_000, 100, r);
   }
 
   method {:test} TestUniformInterval()

diff --git a/tests/TestsFoundational.dfy b/tests/TestsFoundational.dfy
@@ -12,11 +12,32 @@ module TestsFoundational {
     Tests.TestCoin(1_000_000, r);
   }
 
-  method {:test} TestUniform()
+  method {:test} TestUniformPowerOfTwo_10()
     decreases *
   {
     var r := new DafnyVMC.DRandomFoundational();
-    Tests.TestUniform(1_000_000, r);
+    Tests.TestUniformPowerOfTwo(1_000_000, 10, r);
+  }
+
+  method {:test} TestUniformPowerOfTwo_100()
+    decreases *
+  {
+    var r := new DafnyVMC.DRandomFoundational();
+    Tests.TestUniformPowerOfTwo(1_000_000, 100, r);
+  }
+
+  method {:test} TestUniform_10()
+    decreases *
+  {
+    var r := new DafnyVMC.DRandomFoundational();
+    Tests.TestUniform(1_000_000, 10, r);
+  }
+
+  method {:test} TestUniform_100()
+    decreases *
+  {
+    var r := new DafnyVMC.DRandomFoundational();
+    Tests.TestUniform(1_000_000, 100, r);
   }
 
   method {:test} TestUniformInterval()