format and audit

Author: stefan-aws

audit.log

@@ -1,6 +1,7 @@
 src/Distributions/BernoulliExpNeg/Correctness.dfy(13,17): Correctness: Declaration has explicit `{:axiom}` attribute. 
 src/Distributions/BernoulliExpNeg/Correctness.dfy(17,17): SampleIsIndep: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/BernoulliExpNeg/Model.dfy(104,17): GammaLe1LoopTerminatesAlmostSurely: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/BernoulliExpNeg/Equivalence.dfy(80,37): EnsureCaseLe1PostCondition: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/BernoulliExpNeg/Equivalence.dfy(85,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/Math/Analysis/Reals.dfy(35,17): LeastUpperBoundProperty: Declaration has explicit `{:axiom}` attribute. 
@@ -10,17 +11,18 @@ src/Math/Exponential.dfy(4,17): FunctionalEquation: Declaration has explicit `{:
 src/Math/Exponential.dfy(7,17): Increasing: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Measures.dfy(169,17): CountableSumOfZeroesIsZero: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Measures.dfy(25,4): CountableSum: Definition has `assume {:axiom}` statement in body. 
-src/ProbabilisticProgramming/Independence.dfy(28,27): IsIndep: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(34,17): IsIndepImpliesMeasurableBool: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(38,17): IsIndepImpliesMeasurableNat: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(43,17): IsIndepImpliesIsIndepFunction: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(48,17): CoinIsIndep: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(52,17): ReturnIsIndep: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(56,17): BindIsIndep: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Loops.dfy(311,17): EnsureWhileTerminates: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Loops.dfy(317,17): UntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Loops.dfy(349,4): EnsureUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body. 
-src/ProbabilisticProgramming/Loops.dfy(372,4): WhileIsIndep: Definition has `assume {:axiom}` statement in body. 
+src/ProbabilisticProgramming/Monad.dfy(249,27): IsIndep: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Monad.dfy(255,17): IsIndepImpliesMeasurableBool: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Monad.dfy(259,17): IsIndepImpliesMeasurableNat: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Monad.dfy(264,17): IsIndepImpliesIsIndepFunction: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Monad.dfy(269,17): CoinIsIndep: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Monad.dfy(273,17): ReturnIsIndep: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Monad.dfy(277,17): BindIsIndep: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Monad.dfy(348,4): AboutWhile: Definition has `assume {:axiom}` statement in body. 
+src/ProbabilisticProgramming/Monad.dfy(600,17): EnsureWhileTerminates: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Monad.dfy(606,17): UntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Monad.dfy(638,4): EnsureUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body. 
+src/ProbabilisticProgramming/Monad.dfy(661,4): WhileIsIndep: Definition has `assume {:axiom}` statement in body. 
 src/ProbabilisticProgramming/RandomSource.dfy(52,17): ProbIsProbabilityMeasure: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/RandomSource.dfy(56,17): CoinHasProbOneHalf: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/RandomSource.dfy(63,17): MeasureHeadDrop: Declaration has explicit `{:axiom}` attribute. 

src/Distributions/Uniform/Model.dfy

@@ -37,50 +37,50 @@ module Uniform.Model {
     Monad.Map(Sample(b - a), x => a + x)
   }
 
-/*   lemma SampleTerminates(n: nat)
-    requires n > 0
-    ensures
-      && Independence.IsIndep(Proposal(n))
-      && Quantifier.WithPosProb(Loops.ProposalIsAccepted(Proposal(n), Accept(n)))
-      && Loops.UntilTerminatesAlmostSurely(Proposal(n), Accept(n))
-  {
-    assert Independence.IsIndep(Proposal(n)) by {
-      UniformPowerOfTwo.Correctness.SampleIsIndep(2 * n);
-    }
-    var e := iset s | Loops.ProposalIsAccepted(Proposal(n), Accept(n))(s);
-    assert e in Rand.eventSpace by {
-      var ltN := iset m: nat | m < n;
-      var resultsLtN := Monad.ResultsWithValueIn(ltN);
-      assert e == Measures.PreImage(UniformPowerOfTwo.Model.Sample(2 * n), resultsLtN);
-      assert Measures.PreImage(UniformPowerOfTwo.Model.Sample(2 * n), resultsLtN) in Rand.eventSpace by {
-        assert Independence.IsIndep(UniformPowerOfTwo.Model.Sample(2 * n)) by {
-          UniformPowerOfTwo.Correctness.SampleIsIndep(2 * n);
-        }
-        assert Measures.IsMeasurable(Rand.eventSpace, Monad.natResultEventSpace, UniformPowerOfTwo.Model.Sample(2 * n)) by {
-          Independence.IsIndepImpliesMeasurableNat(UniformPowerOfTwo.Model.Sample(2 * n));
-        }
-        assert resultsLtN in Monad.natResultEventSpace by {
-          Monad.LiftInEventSpaceToResultEventSpace(ltN, Measures.natEventSpace);
-        }
+  /*   lemma SampleTerminates(n: nat)
+      requires n > 0
+      ensures
+        && Independence.IsIndep(Proposal(n))
+        && Quantifier.WithPosProb(Loops.ProposalIsAccepted(Proposal(n), Accept(n)))
+        && Loops.UntilTerminatesAlmostSurely(Proposal(n), Accept(n))
+    {
+      assert Independence.IsIndep(Proposal(n)) by {
+        UniformPowerOfTwo.Correctness.SampleIsIndep(2 * n);
       }
-    }
-    assert Quantifier.WithPosProb(Loops.ProposalIsAccepted(Proposal(n), Accept(n))) by {
-      assert Rand.prob(e) > 0.0 by {
-        assert e == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n);
-        assert n <= Helper.Power(2, Helper.Log2Floor(2 * n)) by {
-          Helper.NLtPower2Log2FloorOf2N(n);
+      var e := iset s | Loops.ProposalIsAccepted(Proposal(n), Accept(n))(s);
+      assert e in Rand.eventSpace by {
+        var ltN := iset m: nat | m < n;
+        var resultsLtN := Monad.ResultsWithValueIn(ltN);
+        assert e == Measures.PreImage(UniformPowerOfTwo.Model.Sample(2 * n), resultsLtN);
+        assert Measures.PreImage(UniformPowerOfTwo.Model.Sample(2 * n), resultsLtN) in Rand.eventSpace by {
+          assert Independence.IsIndep(UniformPowerOfTwo.Model.Sample(2 * n)) by {
+            UniformPowerOfTwo.Correctness.SampleIsIndep(2 * n);
+          }
+          assert Measures.IsMeasurable(Rand.eventSpace, Monad.natResultEventSpace, UniformPowerOfTwo.Model.Sample(2 * n)) by {
+            Independence.IsIndepImpliesMeasurableNat(UniformPowerOfTwo.Model.Sample(2 * n));
+          }
+          assert resultsLtN in Monad.natResultEventSpace by {
+            Monad.LiftInEventSpaceToResultEventSpace(ltN, Measures.natEventSpace);
+          }
         }
-        calc {
-          Rand.prob(e);
-        == { UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(2 * n, n); }
-          n as real / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real);
-        >
-          0.0;
+      }
+      assert Quantifier.WithPosProb(Loops.ProposalIsAccepted(Proposal(n), Accept(n))) by {
+        assert Rand.prob(e) > 0.0 by {
+          assert e == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n);
+          assert n <= Helper.Power(2, Helper.Log2Floor(2 * n)) by {
+            Helper.NLtPower2Log2FloorOf2N(n);
+          }
+          calc {
+            Rand.prob(e);
+          == { UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(2 * n, n); }
+            n as real / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real);
+          >
+            0.0;
+          }
         }
       }
-    }
-    assert Loops.UntilTerminatesAlmostSurely(Proposal(n), Accept(n)) by {
-      Loops.EnsureUntilTerminates(Proposal(n), Accept(n));
-    }
-  } */
+      assert Loops.UntilTerminatesAlmostSurely(Proposal(n), Accept(n)) by {
+        Loops.EnsureUntilTerminates(Proposal(n), Accept(n));
+      }
+    } */
 }

src/ProbabilisticProgramming/Monad.dfy

@@ -341,7 +341,7 @@ module Monad {
   }
 
   lemma AboutWhile<A>(condition: A -> bool, body: A -> Hurd<A>, init: A)
-    ensures 
+    ensures
       var f := While(condition, body, init);
       forall s: Rand.Bitstream :: !condition(init) ==> f(s) == Return(init)(s)
   {