Module structure reorg

audit.log

@@ -1,10 +1,7 @@
 
 Auditing ./src/Dafny-VMC.dfy
 
-Auditing ./src/Distributions/Base/Interface.dfy
- Coin: Definition has `assume {:axiom}` statement in body. 
-
-Auditing ./src/Distributions/Base/Model.dfy
+Auditing ./src/Distributions/Bernoulli/Bernoulli.dfy
 
 Auditing ./src/Distributions/Bernoulli/Correctness.dfy
 
@@ -14,38 +11,55 @@ Auditing ./src/Distributions/Bernoulli/Interface.dfy
 
 Auditing ./src/Distributions/Bernoulli/Model.dfy
 
+Auditing ./src/Distributions/BernoulliExpNeg/BernoulliExpNeg.dfy
+
 Auditing ./src/Distributions/BernoulliExpNeg/Implementation.dfy
 
 Auditing ./src/Distributions/BernoulliExpNeg/Interface.dfy
 
+Auditing ./src/Distributions/Coin/Coin.dfy
+
+Auditing ./src/Distributions/Coin/Interface.dfy
+ CoinSample: Definition has `assume {:axiom}` statement in body. 
+
+Auditing ./src/Distributions/Coin/Model.dfy
+
+Auditing ./src/Distributions/DiscreteGaussian/DiscreteGaussian.dfy
+
 Auditing ./src/Distributions/DiscreteGaussian/Implementation.dfy
 
 Auditing ./src/Distributions/DiscreteGaussian/Interface.dfy
 
+Auditing ./src/Distributions/DiscreteLaplace/DiscreteLaplace.dfy
+
 Auditing ./src/Distributions/DiscreteLaplace/Implementation.dfy
 
 Auditing ./src/Distributions/DiscreteLaplace/Interface.dfy
 
 Auditing ./src/Distributions/Uniform/Correctness.dfy
- ProbUniformIsIndepFn: Declaration has explicit `{:axiom}` attribute. 
+ SampleIsIndepFn: Declaration has explicit `{:axiom}` attribute. 
 
 Auditing ./src/Distributions/Uniform/Implementation.dfy
- Uniform: Definition has `assume {:axiom}` statement in body. 
- Uniform: Definition has `assume {:axiom}` statement in body. 
+ UniformSample: Definition has `assume {:axiom}` statement in body. 
+ UniformSample: Definition has `assume {:axiom}` statement in body. 
 
 Auditing ./src/Distributions/Uniform/Interface.dfy
 
 Auditing ./src/Distributions/Uniform/Model.dfy
 
+Auditing ./src/Distributions/Uniform/Uniform.dfy
+
 Auditing ./src/Distributions/UniformPowerOfTwo/Correctness.dfy
 
 Auditing ./src/Distributions/UniformPowerOfTwo/Implementation.dfy
 
 Auditing ./src/Distributions/UniformPowerOfTwo/Interface.dfy
 
 Auditing ./src/Distributions/UniformPowerOfTwo/Model.dfy
- ProbUnifTerminates: Declaration has explicit `{:axiom}` attribute. 
- ProbUnifCorrespondence: Definition has `assume {:axiom}` statement in body. 
+ SampleTerminates: Declaration has explicit `{:axiom}` attribute. 
+ SampleCorrespondence: Definition has `assume {:axiom}` statement in body. 
+
+Auditing ./src/Distributions/UniformPowerOfTwo/UniformPowerOfTwo.dfy
 
 Auditing ./src/Math/Helper.dfy
 

docs/dafny/ExamplesExternUniform.dfy

@@ -19,18 +19,18 @@ module RandomExamples {
 
     var t := 0;
     for i := 0 to n {
-      var b := r.Coin();
+      var b := r.CoinSample();
       if b {
         t := t + 1;
       }
     }
-    print "Estimated parameter for Coin(): ", (t as real) / (n as real), " (should be around 0.5)\n";
+    print "Estimated parameter for CoinSample(): ", (t as real) / (n as real), " (should be around 0.5)\n";
 
     var a := 0;
     var b := 0;
     var c := 0;
     for i := 0 to n {
-      var k := r.Uniform(10);
+      var k := r.UniformSample(10);
       if k == 0 {
         a := a + 1;
       } else if k == 5 {
@@ -39,13 +39,13 @@ module RandomExamples {
         c := c + 1;
       }
     }
-    print "Estimated probabilities for Uniform(10): ", (a as real) / (n as real), "; " , (b as real) / (n as real), "; " , (c as real) / (n as real), " (each should be around 0.1)\n";
+    print "Estimated probabilities for UniformSample(10): ", (a as real) / (n as real), "; " , (b as real) / (n as real), "; " , (c as real) / (n as real), " (each should be around 0.1)\n";
 
     a := 0;
     b := 0;
     c := 0;
     for i := 0 to n {
-      var k := r.UniformInterval(7,10);
+      var k := r.UniformIntervalSample(7,10);
       if k == 7 {
         a := a + 1;
       } else if k == 8 {
@@ -54,52 +54,52 @@ module RandomExamples {
         c := c + 1;
       }
     }
-    print "Estimated probabilities for UniformInterval(7,10): ", (a as real) / (n as real), "; ", (b as real) / (n as real), "; " , (c as real) / (n as real), " (each should be around 0.33)\n";
+    print "Estimated probabilities for UniformIntervalSample(7,10): ", (a as real) / (n as real), "; ", (b as real) / (n as real), "; " , (c as real) / (n as real), " (each should be around 0.33)\n";
 
     t := 0;
     for i := 0 to n {
-      var b := r.Bernoulli(Rationals.Rational(1, 5));
+      var b := r.BernoulliSample(Rationals.Rational(1, 5));
       if b {
         t := t + 1;
       }
     }
 
-    print "Estimated parameter for Bernoulli(1, 5): ", (t as real) / (n as real), " (should be around 0.2)\n";
+    print "Estimated parameter for BernoulliSample(1, 5): ", (t as real) / (n as real), " (should be around 0.2)\n";
 
     t := 0;
     for i := 0 to n {
-      var b := r.Bernoulli(Rationals.Rational(0, 5));
+      var b := r.BernoulliSample(Rationals.Rational(0, 5));
       if b {
         t := t + 1;
       }
     }
 
-    print "Estimated parameter for Bernoulli(0, 5): ", (t as real) / (n as real), " (should be around 0.0)\n";
+    print "Estimated parameter for BernoulliSample(0, 5): ", (t as real) / (n as real), " (should be around 0.0)\n";
 
     t := 0;
     for i := 0 to n {
-      var b := r.Bernoulli(Rationals.Rational(5, 5));
+      var b := r.BernoulliSample(Rationals.Rational(5, 5));
       if b {
         t := t + 1;
       }
     }
 
-    print "Estimated parameter for Bernoulli(5, 5): ", (t as real) / (n as real), " (should be around 1.0\n";
+    print "Estimated parameter for BernoulliSample(5, 5): ", (t as real) / (n as real), " (should be around 1.0\n";
 
     t := 0;
     for i := 0 to n {
-      var u := r.BernoulliExpNeg(Rationals.Rational(12381, 5377)); // about -ln(0.1)
+      var u := r.BernoulliExpNegSample(Rationals.Rational(12381, 5377)); // about -ln(0.1)
       if u {
         t := t + 1;
       }
     }
-    print "Estimated parameter for BernoulliExpNeg(-ln(0.1)): ", (t as real) / (n as real), " (should be around 0.1)\n";
+    print "Estimated parameter for BernoulliExpNegSample(-ln(0.1)): ", (t as real) / (n as real), " (should be around 0.1)\n";
 
     var count0 := 0;
     var count1 := 0;
     var countneg1 := 0;
     for i := 0 to n {
-      var u := r.DiscreteLaplace(Rationals.Rational(7, 5));
+      var u := r.DiscreteLaplaceSample(Rationals.Rational(7, 5));
       match u {
         case -1 => countneg1 := countneg1 + 1;
         case 0 => count0 := count0 + 1;
@@ -110,13 +110,13 @@ module RandomExamples {
     // Reference values computed with Wolfram Alpha:
     // https://www.wolframalpha.com/input?i=ReplaceAll%5B%28E%5E%5B1%2Ft%5D+-+1%29+%2F+%28E%5E%5B1%2Ft%5D+%2B+1%29+*+E%5E%28-Abs%5Bx%5D%2Ft%29%2C+%7Bt+-%3E+7%2F5%2C+x+-%3E+0%7D%5D
     // https://www.wolframalpha.com/input?i=ReplaceAll%5B%28E%5E%5B1%2Ft%5D+-+1%29+%2F+%28E%5E%5B1%2Ft%5D+%2B+1%29+*+E%5E%28-Abs%5Bx%5D%2Ft%29%2C+%7Bt+-%3E+7%2F5%2C+x+-%3E+1%7D%5D
-    print "Estimated probabilities for DiscreteLaplace(7/5): ", count0 as real / n as real, " (should be around 0.3426949) and ", count1 as real / n as real, ", ", countneg1 as real / n as real, " (should both be around 0.1677634)\n";
+    print "Estimated probabilities for DiscreteLaplaceSample(7/5): ", count0 as real / n as real, " (should be around 0.3426949) and ", count1 as real / n as real, ", ", countneg1 as real / n as real, " (should both be around 0.1677634)\n";
 
     count0 := 0;
     count1 := 0;
     countneg1 := 0;
     for i := 0 to n {
-      var u := r.DiscreteGaussian(Rationals.Rational(7, 5));
+      var u := r.DiscreteGaussianSample(Rationals.Rational(7, 5));
       match u {
         case -1 => countneg1 := countneg1 + 1;
         case 0 => count0 := count0 + 1;
@@ -127,6 +127,6 @@ module RandomExamples {
     // Reference values computed with Wolfram Alpha:
     // 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+0%2C+%CF%83+-%3E+1.4%7D%5D
     // 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 DiscreteGaussian(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";
+    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";
   }
 }

docs/dafny/ExamplesFoundational.dfy

@@ -19,18 +19,18 @@ module RandomExamples {
 
     var t := 0;
     for i := 0 to n {
-      var b := r.Coin();
+      var b := r.CoinSample();
       if b {
         t := t + 1;
       }
     }
-    print "Estimated parameter for Coin(): ", (t as real) / (n as real), " (should be around 0.5)\n";
+    print "Estimated parameter for CoinSample(): ", (t as real) / (n as real), " (should be around 0.5)\n";
 
     var a := 0;
     var b := 0;
     var c := 0;
     for i := 0 to n {
-      var k := r.Uniform(10);
+      var k := r.UniformSample(10);
       if k == 0 {
         a := a + 1;
       } else if k == 5 {
@@ -39,13 +39,13 @@ module RandomExamples {
         c := c + 1;
       }
     }
-    print "Estimated probabilities for Uniform(10): ", (a as real) / (n as real), "; " , (b as real) / (n as real), "; " , (c as real) / (n as real), " (each should be around 0.1)\n";
+    print "Estimated probabilities for UniformSample(10): ", (a as real) / (n as real), "; " , (b as real) / (n as real), "; " , (c as real) / (n as real), " (each should be around 0.1)\n";
 
     a := 0;
     b := 0;
     c := 0;
     for i := 0 to n {
-      var k := r.UniformInterval(7,10);
+      var k := r.UniformIntervalSample(7,10);
       if k == 7 {
         a := a + 1;
       } else if k == 8 {
@@ -54,11 +54,11 @@ module RandomExamples {
         c := c + 1;
       }
     }
-    print "Estimated probabilities for UniformInterval(7,10): ", (a as real) / (n as real), "; ", (b as real) / (n as real), "; " , (c as real) / (n as real), " (each should be around 0.33)\n";
+    print "Estimated probabilities for UniformIntervalSample(7,10): ", (a as real) / (n as real), "; ", (b as real) / (n as real), "; " , (c as real) / (n as real), " (each should be around 0.33)\n";
 
     t := 0;
     for i := 0 to n {
-      var b := r.Bernoulli(Rationals.Rational(1, 5));
+      var b := r.BernoulliSample(Rationals.Rational(1, 5));
       if b {
         t := t + 1;
       }
@@ -68,38 +68,38 @@ module RandomExamples {
 
     t := 0;
     for i := 0 to n {
-      var b := r.Bernoulli(Rationals.Rational(0, 5));
+      var b := r.BernoulliSample(Rationals.Rational(0, 5));
       if b {
         t := t + 1;
       }
     }
 
-    print "Estimated parameter for Bernoulli(0/5): ", (t as real) / (n as real), " (should be around 0.0)\n";
+    print "Estimated parameter for BernoulliSample(0/5): ", (t as real) / (n as real), " (should be around 0.0)\n";
 
     t := 0;
     for i := 0 to n {
-      var b := r.Bernoulli(Rationals.Rational(5, 5));
+      var b := r.BernoulliSample(Rationals.Rational(5, 5));
       if b {
         t := t + 1;
       }
     }
 
-    print "Estimated parameter for Bernoulli(5/5): ", (t as real) / (n as real), " (should be around 1.0\n";
+    print "Estimated parameter for BernoulliSample(5/5): ", (t as real) / (n as real), " (should be around 1.0\n";
 
     t := 0;
     for i := 0 to n {
-      var u := r.BernoulliExpNeg(Rationals.Rational(12381, 5377)); // about -ln(0.1)
+      var u := r.BernoulliExpNegSample(Rationals.Rational(12381, 5377)); // about -ln(0.1)
       if u {
         t := t + 1;
       }
     }
-    print "Estimated parameter for BernoulliExpNeg(-ln(0.1)): ", (t as real) / (n as real), " (should be around 0.1)\n";
+    print "Estimated parameter for BernoulliExpNegSample(-ln(0.1)): ", (t as real) / (n as real), " (should be around 0.1)\n";
 
     var count0 := 0;
     var count1 := 0;
     var countneg1 := 0;
     for i := 0 to n {
-      var u := r.DiscreteLaplace(Rationals.Rational(7, 5));
+      var u := r.DiscreteLaplaceSample(Rationals.Rational(7, 5));
       match u {
         case -1 => countneg1 := countneg1 + 1;
         case 0 => count0 := count0 + 1;
@@ -110,13 +110,13 @@ module RandomExamples {
     // Reference values computed with Wolfram Alpha:
     // https://www.wolframalpha.com/input?i=ReplaceAll%5B%28E%5E%5B1%2Ft%5D+-+1%29+%2F+%28E%5E%5B1%2Ft%5D+%2B+1%29+*+E%5E%28-Abs%5Bx%5D%2Ft%29%2C+%7Bt+-%3E+7%2F5%2C+x+-%3E+0%7D%5D
     // https://www.wolframalpha.com/input?i=ReplaceAll%5B%28E%5E%5B1%2Ft%5D+-+1%29+%2F+%28E%5E%5B1%2Ft%5D+%2B+1%29+*+E%5E%28-Abs%5Bx%5D%2Ft%29%2C+%7Bt+-%3E+7%2F5%2C+x+-%3E+1%7D%5D
-    print "Estimated probabilities for DiscreteLaplace(7/5): ", count0 as real / n as real, " (should be around 0.3426949) and ", count1 as real / n as real, ", ", countneg1 as real / n as real, " (should both be around 0.1677634)\n";
+    print "Estimated probabilities for DiscreteLaplaceSample(7/5): ", count0 as real / n as real, " (should be around 0.3426949) and ", count1 as real / n as real, ", ", countneg1 as real / n as real, " (should both be around 0.1677634)\n";
 
     count0 := 0;
     count1 := 0;
     countneg1 := 0;
     for i := 0 to n {
-      var u := r.DiscreteGaussian(Rationals.Rational(7, 5));
+      var u := r.DiscreteGaussianSample(Rationals.Rational(7, 5));
       match u {
         case -1 => countneg1 := countneg1 + 1;
         case 0 => count0 := count0 + 1;
@@ -127,6 +127,6 @@ module RandomExamples {
     // Reference values computed with Wolfram Alpha:
     // 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+0%2C+%CF%83+-%3E+1.4%7D%5D
     // 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 DiscreteGaussian(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";
+    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";
   }
 }

docs/java/BuildTest.java

@@ -4,6 +4,6 @@
 class Check {
     public static void main(String[] args) {
         DRandomExternUniform d = new DRandomExternUniform();
-        System.out.println(d.Uniform(BigInteger.valueOf(4))); 
+        System.out.println(d.UniformSample(BigInteger.valueOf(4))); 
     }
 }

src/Dafny-VMC.dfy

@@ -5,29 +5,28 @@
 
 // RUN: %verify "%s"
 
-include "Distributions/Base/Interface.dfy"
-include "Distributions/Bernoulli/Implementation.dfy"
-include "Distributions/Bernoulli/Implementation.dfy"
-include "Distributions/BernoulliExpNeg/Implementation.dfy"
-include "Distributions/DiscreteGaussian/Implementation.dfy"
-include "Distributions/DiscreteLaplace/Implementation.dfy"
-include "Distributions/UniformPowerOfTwo/Implementation.dfy"
-include "Distributions/Uniform/Implementation.dfy"
+include "Distributions/Coin/Coin.dfy"
+include "Distributions/Bernoulli/Bernoulli.dfy"
+include "Distributions/BernoulliExpNeg/BernoulliExpNeg.dfy"
+include "Distributions/DiscreteGaussian/DiscreteGaussian.dfy"
+include "Distributions/DiscreteLaplace/DiscreteLaplace.dfy"
+include "Distributions/UniformPowerOfTwo/UniformPowerOfTwo.dfy"
+include "Distributions/Uniform/Uniform.dfy"
 
 module DafnyVMC {
-  import BaseInterface
-  import BernoulliImplementation
-  import UniformPowerOfTwoImplementation
-  import UniformImplementation
-  import BernoulliExpNegImplementation
-  import DiscreteGaussianImplementation
-  import DiscreteLaplaceImplementation
+  import Coin
+  import Bernoulli
+  import UniformPowerOfTwo
+  import Uniform
+  import BernoulliExpNeg
+  import DiscreteGaussian
+  import DiscreteLaplace
 
-  class DRandomFoundational extends BaseInterface.TBase, UniformPowerOfTwoImplementation.TUniformPowerOfTwo, BernoulliImplementation.TBernoulli, UniformImplementation.TUniformFoundational, BernoulliExpNegImplementation.TBernoulliExpNeg, DiscreteGaussianImplementation.TDiscreteGaussian, DiscreteLaplaceImplementation.TDiscreteLaplace {
+  class DRandomFoundational extends Coin.Interface.Trait, UniformPowerOfTwo.Implementation.Trait, Bernoulli.Implementation.Trait, Uniform.Implementation.TraitFoundational, BernoulliExpNeg.Implementation.Trait, DiscreteGaussian.Implementation.Trait, DiscreteLaplace.Implementation.Trait {
     constructor {:extern} ()
   }
 
-  class DRandomExternUniform extends BaseInterface.TBase, UniformPowerOfTwoImplementation.TUniformPowerOfTwo, BernoulliImplementation.TBernoulli, UniformImplementation.TUniformExtern, BernoulliExpNegImplementation.TBernoulliExpNeg, DiscreteGaussianImplementation.TDiscreteGaussian, DiscreteLaplaceImplementation.TDiscreteLaplace {
+  class DRandomExternUniform extends Coin.Interface.Trait, UniformPowerOfTwo.Implementation.Trait, Bernoulli.Implementation.Trait, Uniform.Implementation.TraitExtern, BernoulliExpNeg.Implementation.Trait, DiscreteGaussian.Implementation.Trait, DiscreteLaplace.Implementation.Trait {
     constructor {:extern} ()
   }
 }

src/Distributions/Bernoulli/Bernoulli.dfy

@@ -0,0 +1,11 @@
+include "Correctness.dfy"
+include "Implementation.dfy"
+include "Interface.dfy"
+include "Model.dfy"
+
+module Bernoulli {
+  import Interface = BernoulliInterface
+  import Implementation = BernoulliImplementation
+  import Correctness = BernoulliCorrectness
+  import Model = BernoulliModel
+}