Introducing NewVMC

audit.log

@@ -1,30 +1,6 @@
 src/DafnyVMC.dfy(23,6): UniformPowerOfTwoSample: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/Bernoulli/Correctness.dfy(59,17): BernoulliCorrectnessCaseFalse: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(229,6): CorrectnessLe1: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(346,17): Le1SeriesConvergesToExpNeg: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(411,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(412,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(419,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(420,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(424,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(425,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(615,8): Le1LoopCorrectnessEq: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(616,8): Le1LoopCorrectnessEq: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Model.dfy(112,10): Le1LoopTerminatesAlmostSurely: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Model.dfy(148,4): Le1LoopDivergenceProbabilityBound: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Model.dfy(161,8): Le1LoopDivergenceProbabilityBound: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Model.dfy(162,8): Le1LoopDivergenceProbabilityBound: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Model.dfy(185,10): Le1LoopDivergenceProbabilityBound: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Model.dfy(71,17): Le1LoopIterCorrectness: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/DiscreteLaplace/Correctness.dfy(37,17): Correctness: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/DiscreteLaplace/Model.dfy(89,17): SampleInnerLoopTerminatesAlmostSurely: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/DiscreteLaplace/Model.dfy(93,17): SampleLoopTerminatesAlmostSurely: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Analysis/Limits.dfy(126,17): Sandwich: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Analysis/Reals.dfy(35,17): LeastUpperBoundProperty: Declaration has explicit `{:axiom}` attribute. 
-src/Math/Exponential.dfy(55,17): ExpSeriesConverges: Declaration has explicit `{:axiom}` attribute. 
-src/Math/Exponential.dfy(58,17): FunctionalEquation: Declaration has explicit `{:axiom}` attribute. 
-src/Math/Exponential.dfy(61,17): Increasing: Declaration has explicit `{:axiom}` attribute. 
-src/Math/Exponential.dfy(65,17): EvalOne: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Measures.dfy(125,17): ProbabilityLe1: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Measures.dfy(130,17): IsMonotonic: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/Independence.dfy(105,17): BindIsIndep: Declaration has explicit `{:axiom}` attribute. 
@@ -35,12 +11,10 @@ src/ProbabilisticProgramming/Independence.dfy(77,17): IsIndepImpliesMeasurableNa
 src/ProbabilisticProgramming/Independence.dfy(82,17): IsIndepImpliesIsIndepFunction: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/Independence.dfy(87,17): CoinIsIndep: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/Independence.dfy(91,17): ReturnIsIndep: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Loops.dfy(362,17): EnsureWhileTerminates: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Loops.dfy(367,17): EnsureWhileTerminatesAlmostSurelyViaLimit: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Loops.dfy(385,17): WhileProbabilityViaLimit: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Loops.dfy(402,17): UntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Loops.dfy(435,4): EnsureUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body. 
-src/ProbabilisticProgramming/Loops.dfy(458,4): WhileIsIndep: Definition has `assume {:axiom}` statement in body. 
+src/ProbabilisticProgramming/Loops.dfy(361,17): EnsureWhileTerminates: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Loops.dfy(371,17): UntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Loops.dfy(404,4): EnsureUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body. 
+src/ProbabilisticProgramming/Loops.dfy(427,4): WhileIsIndep: Definition has `assume {:axiom}` statement in body. 
 src/ProbabilisticProgramming/RandomSource.dfy(50,17): ProbIsProbabilityMeasure: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/RandomSource.dfy(54,17): CoinHasProbOneHalf: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/RandomSource.dfy(61,17): MeasureHeadDrop: Declaration has explicit `{:axiom}` attribute. 

docs/dafny/ExamplesRandom.dfy

@@ -4,7 +4,6 @@
  *******************************************************************************/
 
 module Examples {
-  import Rationals
   import DafnyVMC
   import Helper
 
@@ -15,13 +14,6 @@ module Examples {
     var r: DafnyVMC.Random := new DafnyVMC.Random();
 
     var t := 0;
-    for i := 0 to n {
-      var b := r.CoinSample();
-      if b {
-        t := t + 1;
-      }
-    }
-    print "Estimated parameter for CoinSample(): ", (t as real) / (n as real), " (should be around 0.5)\n";
 
     var a := 0;
     var b := 0;
@@ -55,7 +47,7 @@ module Examples {
 
     t := 0;
     for i := 0 to n {
-      var b := r.BernoulliSample(Rationals.Rational(1, 5));
+      var b := r.BernoulliSample(1, 5);
       if b {
         t := t + 1;
       }
@@ -65,7 +57,7 @@ module Examples {
 
     t := 0;
     for i := 0 to n {
-      var b := r.BernoulliSample(Rationals.Rational(0, 5));
+      var b := r.BernoulliSample(0, 5);
       if b {
         t := t + 1;
       }
@@ -75,7 +67,7 @@ module Examples {
 
     t := 0;
     for i := 0 to n {
-      var b := r.BernoulliSample(Rationals.Rational(5, 5));
+      var b := r.BernoulliSample(5, 5);
       if b {
         t := t + 1;
       }
@@ -85,7 +77,7 @@ module Examples {
 
     t := 0;
     for i := 0 to n {
-      var u := r.BernoulliExpNegSample(Rationals.Rational(12381, 5377)); // about -ln(0.1)
+      var u := r.BernoulliExpNegSample(12381, 5377); // about -ln(0.1)
       if u {
         t := t + 1;
       }
@@ -96,7 +88,7 @@ module Examples {
     var count1 := 0;
     var countneg1 := 0;
     for i := 0 to n {
-      var u := r.DiscreteLaplaceSample(Rationals.Rational(7, 5));
+      var u := r.DiscreteLaplaceSample(7, 5);
       match u {
         case -1 => countneg1 := countneg1 + 1;
         case 0 => count0 := count0 + 1;
@@ -113,7 +105,7 @@ module Examples {
     count1 := 0;
     countneg1 := 0;
     for i := 0 to n {
-      var u := r.DiscreteGaussianSample(Rationals.Rational(7, 5));
+      var u := r.DiscreteGaussianSample(7, 5);
       match u {
         case -1 => countneg1 := countneg1 + 1;
         case 0 => count0 := count0 + 1;

docs/java/BuildTest.java

@@ -13,30 +13,28 @@ public static void main(String[] args) {
         boolean[] arr5 = {true, false, false, true};
         long[] arr6 = {111111L, 333333L, 999999L};
         short[] arr7 = {-3, 0, 3};
-        Rationals.Rational gamma = new Rationals.Rational(BigInteger.valueOf(3), BigInteger.valueOf(5));
+        BigInteger num = BigInteger.valueOf(3);
+        BigInteger den = BigInteger.valueOf(5);
 
         /* STANDARD RNG */
         System.out.println("\nSTANDARD RNG TESTS\n");
 
         DafnyVMC.Random r = new DafnyVMC.Random();
 
-        System.out.println("Example of Coin sampling");
-        System.out.println(r.CoinSample());
-
         System.out.println("Example of Uniform sampling");
         System.out.println(r.UniformSample(BigInteger.valueOf(4)));
 
         System.out.println("Example of Bernoulli sampling");
-        System.out.println(r.BernoulliSample(gamma));
+        System.out.println(r.BernoulliSample(num,den));
 
         System.out.println("Example of BernoulliExpNeg sampling");
-        System.out.println(r.BernoulliExpNegSample(gamma));
+        System.out.println(r.BernoulliExpNegSample(num,den));
 
         System.out.println("Example of DiscreteGaussian sampling");
-        System.out.println(r.DiscreteGaussianSample(gamma));
+        System.out.println(r.DiscreteGaussianSample(num,den));
 
         System.out.println("Example of DiscreteLaplace sampling");
-        System.out.println(r.DiscreteLaplaceSample(gamma));
+        System.out.println(r.DiscreteLaplaceSample(num,den));
 
         System.out.println("Example of Fisher-Yates: BigInteger");
         r.Shuffle(arr1);
@@ -72,23 +70,20 @@ public static void main(String[] args) {
         SecureRandom rng = new SecureRandom();
         DafnyVMC.Random t = new DafnyVMC.Random(() -> rng);
 
-        System.out.println("Example of Coin sampling");
-        System.out.println(t.CoinSample());
-
         System.out.println("Example of Uniform sampling");
         System.out.println(t.UniformSample(BigInteger.valueOf(4)));
 
         System.out.println("Example of Bernoulli sampling");
-        System.out.println(t.BernoulliSample(gamma));
+        System.out.println(t.BernoulliSample(num,den));
 
         System.out.println("Example of BernoulliExpNeg sampling");
-        System.out.println(r.BernoulliExpNegSample(gamma));
+        System.out.println(r.BernoulliExpNegSample(num,den));
 
         System.out.println("Example of DiscreteGaussian sampling");
-        System.out.println(t.DiscreteGaussianSample(gamma));
+        System.out.println(t.DiscreteGaussianSample(num,den));
 
         System.out.println("Example of DiscreteLaplace sampling");
-        System.out.println(t.DiscreteLaplaceSample(gamma));
+        System.out.println(t.DiscreteLaplaceSample(num,den));
 
         System.out.println("Example of Fisher-Yates: BigInteger");
         t.Shuffle(arr1);

scripts/audit.sh

@@ -8,4 +8,4 @@ then
   exit 1
 fi
 
-$DAFNY audit dfyconfig.toml | grep -v '{:termination false}\|{:extern}\|decreases *\|Dafny auditor completed\|Dafny program verifier\|No terms found to trigger on\|Compiled declaration has no body' | sed 's/Warning: //' | sed 's/Possible mitigation: .*//' | sed '/^$/d' | sort > audit.log
+$DAFNY audit dfyconfig.toml | grep -v '{:termination false}\|{:extern}\|decreases *\|DafnyVMCTrait\|Dafny auditor completed\|Dafny program verifier\|No terms found to trigger on\|Compiled declaration has no body' | sed 's/Warning: //' | sed 's/Possible mitigation: .*//' | sed '/^$/d' | sort > audit.log

scripts/checkformat.sh

@@ -10,4 +10,5 @@ fi
 
 echo "Checking the formatting of all Dafny files..."
 echo "Run \`DAFNY=dafny scripts/format.sh\` to fix any errors."
+$DAFNY format src/DafnyVMCTrait.dfy
 $DAFNY format --check dfyconfig.toml