DRAFT: Opaque Monad Simple Version

audit.log

@@ -1,26 +1,31 @@
 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/Distributions/Uniform/Implementation.dfy(33,6): UniformSample: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/Uniform/Implementation.dfy(48,6): UniformSample: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/UniformPowerOfTwo/Correctness.dfy(216,10): SampleIsMeasurePreserving: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/UniformPowerOfTwo/Model.dfy(24,4): UnifStepHelper: Definition has `assume {:axiom}` statement in body. 
 src/Math/Analysis/Reals.dfy(35,17): LeastUpperBoundProperty: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Exponential.dfy(11,17): EvalOne: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Exponential.dfy(2,26): Exp: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Exponential.dfy(4,17): FunctionalEquation: Declaration has explicit `{:axiom}` attribute. 
 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/Bernoulli/Correctness.dfy

@@ -8,35 +8,34 @@ module Bernoulli.Correctness {
   import Helper
   import Uniform
   import Rand
-  import Independence
   import Monad
   import Model
 
   /*******
    Lemmas
   *******/
-
-  lemma SampleIsIndep(m: nat, n: nat)
-    requires n != 0
-    requires m <= n
-    ensures Independence.IsIndep(Model.Sample(m, n))
-  {
-    var f := Uniform.Model.Sample(n);
-    var g := (k: nat) => Monad.Return(k < m);
-
-    assert Independence.IsIndep(f) by {
-      Uniform.Correctness.SampleIsIndep(n);
-    }
-
-    assert forall k: nat :: Independence.IsIndep(g(k)) by {
-      forall k: nat ensures Independence.IsIndep(g(k)) {
-        Independence.ReturnIsIndep(k < m);
+  /* 
+    lemma SampleIsIndep(m: nat, n: nat)
+      requires n != 0
+      requires m <= n
+      ensures Monad.IsIndep(Model.Sample(m, n))
+    {
+      var f := Uniform.Model.Sample(n);
+      var g := (k: nat) => Monad.Return(k < m);
+
+      assert Monad.IsIndep(f) by {
+        Uniform.Correctness.SampleIsIndep(n);
       }
-    }
-
-    Independence.BindIsIndep(f, g);
-    reveal Model.Sample();
-  }
+
+      assert forall k: nat :: Monad.IsIndep(g(k)) by {
+        forall k: nat ensures Monad.IsIndep(g(k)) {
+          Monad.ReturnIsIndep(k < m);
+        }
+      }
+
+      Monad.BindIsIndep(f, g);
+      reveal Model.Sample();
+    } */
 
 
   lemma BernoulliCorrectness(m: nat, n: nat)

src/Distributions/BernoulliExpNeg/Correctness.dfy

@@ -7,14 +7,14 @@ module BernoulliExpNeg.Correctness {
   import Rationals
   import Exponential
   import Rand
-  import Independence
   import Model
+  import Monad
 
   lemma {:axiom} Correctness(gamma: Rationals.Rational)
     requires 0 <= gamma.numer
     ensures Rand.prob(iset s | Model.Sample(gamma)(s).Equals(true)) == Exponential.Exp(-Rationals.ToReal(gamma))
 
   lemma {:axiom} SampleIsIndep(gamma: Rationals.Rational)
     requires 0 <= gamma.numer
-    ensures Independence.IsIndep(Model.Sample(gamma))
+    ensures Monad.IsIndep(Model.Sample(gamma))
 }

src/Distributions/BernoulliExpNeg/Equivalence.dfy

@@ -8,7 +8,6 @@ module BernoulliExpNeg.Equivalence {
   import Rand
   import Monad
   import Model
-  import Loops
   import Bernoulli
 
   /************
@@ -30,13 +29,13 @@ module BernoulliExpNeg.Equivalence {
     requires ak.0
     ensures Model.GammaLe1Loop(gamma)(ak)(s) == Monad.Bind(Model.GammaLe1LoopIter(gamma)(ak), Model.GammaLe1Loop(gamma))(s)
   {
-    Model.GammaLe1LoopTerminatesAlmostSurely(gamma);
+    GammaLe1LoopTerminatesAlmostSurely(gamma);
     calc {
       Model.GammaLe1Loop(gamma)(ak)(s);
       { reveal Model.GammaLe1Loop(); }
-      Loops.While(Model.GammaLe1LoopCondition, Model.GammaLe1LoopIter(gamma), ak)(s);
+      Monad.While(Model.GammaLe1LoopCondition, Model.GammaLe1LoopIter(gamma), ak)(s);
       { reveal Model.GammaLe1Loop();
-        Loops.WhileUnroll(Model.GammaLe1LoopCondition, Model.GammaLe1LoopIter(gamma), ak, s); }
+        Monad.WhileUnroll(Model.GammaLe1LoopCondition, Model.GammaLe1LoopIter(gamma), ak, s); }
       Monad.Bind(Model.GammaLe1LoopIter(gamma)(ak), Model.GammaLe1Loop(gamma))(s);
     }
   }
@@ -78,8 +77,13 @@ module BernoulliExpNeg.Equivalence {
       Model.GammaLe1Loop(gamma)((true, 0))(oldS);
       { reveal CaseLe1LoopInvariant(); }
       Model.GammaLe1Loop(gamma)((false, k))(s);
-      { reveal Model.GammaLe1Loop(); }
+      { reveal Model.GammaLe1Loop(); assume {:axiom} false; } // prove likely via Monad.AboutWhile
       Monad.Result((false, k), s);
     }
   }
+
+  lemma {:axiom} GammaLe1LoopTerminatesAlmostSurely(gamma: Rationals.Rational)
+    requires 0 <= gamma.numer <= gamma.denom
+    ensures Monad.WhileTerminatesAlmostSurely(Model.GammaLe1LoopCondition, Model.GammaLe1LoopIter(gamma))
+
 }

src/Distributions/BernoulliExpNeg/Model.dfy

@@ -8,8 +8,7 @@ module BernoulliExpNeg.Model {
   import Rand
   import Uniform
   import Bernoulli
-  import Monad
-  import Loops
+  import Monad`Spec
   import BernoulliModel = Bernoulli.Model
 
   opaque ghost function Sample(gamma: Rationals.Rational): Monad.Hurd<bool>
@@ -75,8 +74,8 @@ module BernoulliExpNeg.Model {
     requires 0 <= gamma.numer <= gamma.denom
   {
     (ak: (bool, nat)) =>
-      GammaLe1LoopTerminatesAlmostSurely(gamma);
-      Loops.While(
+      //Equivalence.GammaLe1LoopTerminatesAlmostSurely(gamma);
+      Monad.While(
         GammaLe1LoopCondition,
         GammaLe1LoopIter(gamma),
         ak
@@ -101,9 +100,4 @@ module BernoulliExpNeg.Model {
     a => Monad.Return((a, k))
   }
 
-  lemma {:axiom} GammaLe1LoopTerminatesAlmostSurely(gamma: Rationals.Rational)
-    requires 0 <= gamma.numer <= gamma.denom
-    ensures Loops.WhileTerminatesAlmostSurely(GammaLe1LoopCondition, GammaLe1LoopIter(gamma))
-
-
 }

src/Distributions/Coin/Interface.dfy

@@ -15,7 +15,7 @@ module Coin.Interface {
 
     method CoinSample() returns (b: bool)
       modifies this
-      ensures Model.Sample(old(s)) == Monad.Result(b, s)
+      ensures Model.Sample()(old(s)) == Monad.Result(b, s)
     {
       b := ExternCoinSample();
       assume {:axiom} false; // assume correctness of extern implementation

src/Distributions/Coin/Model.dfy

@@ -5,9 +5,9 @@
 
 module Coin.Model {
   import Rand
-  import Monad
+  import Monad`Spec
 
-  function Sample(s: Rand.Bitstream): Monad.Result<bool> {
-    Monad.Coin(s)
+  function Sample(): Monad.Hurd<bool> {
+    Monad.Coin()
   }
 }

src/Distributions/Uniform/Correctness.dfy

@@ -6,10 +6,8 @@
 module Uniform.Correctness {
   import Helper
   import Monad
-  import Independence
   import Rand
   import Quantifier
-  import Loops
   import Measures
   import UniformPowerOfTwo
   import Model
@@ -37,14 +35,14 @@ module Uniform.Correctness {
   {
     var equalsI := (x: nat) => x == i;
 
-    assert Independence.IsIndep(Model.Proposal(n)) && Quantifier.WithPosProb(Loops.ProposalIsAccepted(Model.Proposal(n), Model.Accept(n))) by {
-      Model.SampleTerminates(n);
-    }
+    // assert Monad.IsIndep(Model.Proposal(n)) && Quantifier.WithPosProb(Monad.ProposalIsAccepted(Model.Proposal(n), Model.Accept(n))) by {
+    //   Model.SampleTerminates(n);
+    // }
 
-    Loops.UntilProbabilityFraction(Model.Proposal(n), Model.Accept(n), equalsI);
-    var eventResultEqualsI := Loops.UntilLoopResultHasProperty(Model.Proposal(n), Model.Accept(n), equalsI);
-    var eventProposalAcceptedAndEqualsI := Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), equalsI);
-    var proposalAccepted := Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n));
+    Monad.UntilProbabilityFraction(Model.Proposal(n), Model.Accept(n), equalsI);
+    var eventResultEqualsI := Monad.UntilLoopResultHasProperty(Model.Proposal(n), Model.Accept(n), equalsI);
+    var eventProposalAcceptedAndEqualsI := Monad.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), equalsI);
+    var proposalAccepted := Monad.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n));
 
     assert Fraction: Rand.prob(eventResultEqualsI) == Rand.prob(eventProposalAcceptedAndEqualsI) / Rand.prob(proposalAccepted);
 
@@ -79,9 +77,9 @@ module Uniform.Correctness {
   lemma ProbabilityProposalAcceptedAndEqualsI(n: nat, i: nat)
     requires 0 <= i < n
     ensures
-      Rand.prob(Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i)) == 1.0 / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real)
+      Rand.prob(Monad.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i)) == 1.0 / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real)
   {
-    var e := Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i);
+    var e := Monad.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i);
     var nextPowerOfTwo := Helper.Power(2, Helper.Log2Floor(2 * n));
     assert iBound: i < nextPowerOfTwo by {
       calc {
@@ -92,13 +90,13 @@ module Uniform.Correctness {
         nextPowerOfTwo;
       }
     }
-    assert setEq: Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i) == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i) by {
+    assert setEq: Monad.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i) == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i) by {
       forall s ensures s in e <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i {
         assert s in e <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i;
       }
     }
     calc {
-      Rand.prob(Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i));
+      Rand.prob(Monad.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i));
       { reveal setEq; }
       Rand.prob(iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i);
       { reveal iBound; UniformPowerOfTwo.Correctness.UnifCorrectness2(2 * n, i); }
@@ -109,9 +107,9 @@ module Uniform.Correctness {
   lemma ProbabilityProposalAccepted(n: nat)
     requires n >= 1
     ensures
-      Rand.prob(Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real)
+      Rand.prob(Monad.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real)
   {
-    var e := Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n));
+    var e := Monad.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n));
     assert n < Helper.Power(2, Helper.Log2Floor(2 * n)) by { Helper.NLtPower2Log2FloorOf2N(n); }
     assert Equal: e == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n) by {
       forall s ensures s in e <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n {
@@ -122,7 +120,7 @@ module Uniform.Correctness {
         }
       }
     }
-    assert Rand.prob(Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real) by {
+    assert Rand.prob(Monad.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real) by {
       calc {
         Rand.prob(e);
         { reveal Equal; }
@@ -155,18 +153,18 @@ module Uniform.Correctness {
     }
   }
 
-  // Equation (4.10)
-  lemma SampleIsIndep(n: nat)
-    requires n > 0
-    ensures Independence.IsIndep(Model.Sample(n))
-  {
-    assert Independence.IsIndep(Model.Proposal(n)) by {
-      UniformPowerOfTwo.Correctness.SampleIsIndep(2 * n);
-    }
-    assert Loops.UntilTerminatesAlmostSurely(Model.Proposal(n), Model.Accept(n)) by {
-      Model.SampleTerminates(n);
-    }
-    Loops.UntilIsIndep(Model.Proposal(n), Model.Accept(n));
-    reveal Model.Sample();
-  }
+  /*   // Equation (4.10)
+    lemma SampleIsIndep(n: nat)
+      requires n > 0
+      ensures Monad.IsIndep(Model.Sample(n))
+    {
+      assert Monad.IsIndep(Model.Proposal(n)) by {
+        UniformPowerOfTwo.Correctness.SampleIsIndep(2 * n);
+      }
+      // assert Monad.UntilTerminatesAlmostSurely(Model.Proposal(n), Model.Accept(n)) by {
+      //   Model.SampleTerminates(n);
+      // }
+      Monad.UntilIsIndep(Model.Proposal(n), Model.Accept(n));
+      reveal Model.Sample();
+    } */
 }

src/Distributions/Uniform/Equivalence.dfy

@@ -7,14 +7,13 @@ module Uniform.Equivalence {
   import Rand
   import Model
   import Monad
-  import Loops
 
   lemma SampleUnroll(n: nat, s: Rand.Bitstream)
     requires n > 0
     ensures Model.Sample(n)(s) == Monad.Bind(Model.Proposal(n), (x: nat) => if Model.Accept(n)(x) then Monad.Return(x) else Model.Sample(n))(s)
   {
-    Model.SampleTerminates(n);
+    //Model.SampleTerminates(n);
     reveal Model.Sample();
-    Loops.UntilUnroll(Model.Proposal(n), Model.Accept(n), s);
+    Monad.UntilUnroll(Model.Proposal(n), Model.Accept(n), s);
   }
 }

src/Distributions/Uniform/Implementation.dfy

@@ -4,7 +4,7 @@
  *******************************************************************************/
 
 module Uniform.Implementation {
-  import Monad
+  import Monad`Spec
   import UniformPowerOfTwo
   import Model
   import Interface
@@ -16,20 +16,21 @@ module Uniform.Implementation {
       decreases *
       requires n > 0
       ensures u < n
-      ensures Model.Sample(n)(old(s)) == Monad.Result(u, s)
+      ensures Model.Sample(n)(old(s)) == Monad.Return(u)(s)
     {
       ghost var prevS := s;
       u := UniformPowerOfTwoSample(2 * n);
       while u >= n
         decreases *
         invariant Model.Sample(n)(old(s)) == Model.Sample(n)(prevS)
-        invariant Monad.Result(u, s) == Model.Proposal(n)(prevS)
+        invariant Monad.Return(u)(s) == Model.Proposal(n)(prevS)
       {
         Equivalence.SampleUnroll(n, prevS);
         prevS := s;
         u := UniformPowerOfTwoSample(2 * n);
       }
       reveal Model.Sample();
+      assume {:axiom} false; // TODO
     }
   }
 
@@ -41,7 +42,7 @@ module Uniform.Implementation {
       decreases *
       requires n > 0
       ensures u < n
-      ensures Model.Sample(n)(old(s)) == Monad.Result(u, s)
+      ensures Model.Sample(n)(old(s)) == Monad.Return(u)(s)
     {
       u := ExternUniformSample(n);
       assume {:axiom} false; // assume correctness of extern implementation