Remove quantifier in postconditions (#144)

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).

Author: stefan-aws

audit.log

@@ -1,15 +1,15 @@
 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(228,6): CorrectnessLe1: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(336,17): Le1SeriesConvergesToExpNeg: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(401,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(402,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(409,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(410,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(414,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(415,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(605,8): Le1LoopCorrectnessEq: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(606,8): Le1LoopCorrectnessEq: Definition has `assume {:axiom}` statement in body. 
+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. 
@@ -35,12 +35,12 @@ 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(376,17): EnsureWhileTerminates: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Loops.dfy(381,17): EnsureWhileTerminatesAlmostSurelyViaLimit: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Loops.dfy(399,17): WhileProbabilityViaLimit: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Loops.dfy(416,17): UntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Loops.dfy(448,4): EnsureUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body. 
-src/ProbabilisticProgramming/Loops.dfy(471,4): WhileIsIndep: Definition has `assume {:axiom}` statement in body. 
+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/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. 

src/Distributions/BernoulliExpNeg/Correctness.dfy

@@ -19,6 +19,7 @@ module BernoulliExpNeg.Correctness {
   import Loops
   import Bernoulli
   import Model
+  import Uniform
 
   lemma Correctness(gamma: Rationals.Rational)
     requires 0 <= gamma.numer
@@ -301,7 +302,16 @@ module BernoulliExpNeg.Correctness {
     assert denom >= 1;
     var eventTrue := Monad.BitstreamsWithValueIn(Model.Le1LoopIter(gamma)((true, k)), iset{(true, k')});
     var eventTrue2 := iset s | Bernoulli.Model.Sample(gamma.numer, denom)(s).Equals(true);
-    assert eventTrue == eventTrue2;
+    assert eventTrue == eventTrue2 by {
+      forall s
+        ensures s in eventTrue <==> s in eventTrue2
+      {
+        reveal Bernoulli.Model.Sample();
+        if Uniform.Model.Sample(denom)(s).Result? {
+          Uniform.Model.SampleBound(denom, s);
+        }
+      }
+    }
     assert Rand.prob(eventTrue2) == gamma.numer as real / denom as real by {
       Bernoulli.Correctness.BernoulliCorrectness(gamma.numer, denom, true);
       reveal Bernoulli.Correctness.BernoulliMass();

src/Distributions/BernoulliExpNeg/Equivalence.dfy

@@ -88,7 +88,7 @@ module BernoulliExpNeg.Equivalence {
       Model.Le1Loop(gamma)((true, 0))(oldS);
       { reveal CaseLe1LoopInvariant(); }
       Model.Le1Loop(gamma)((false, k))(s);
-      { reveal Model.Le1Loop(); }
+      { reveal Model.Le1Loop(); Loops.WhileInitialConditionNegated(Model.Le1LoopCondition, Model.Le1LoopIter(gamma), (false, k), s); }
       Monad.Result((false, k), s);
     }
   }

src/Distributions/Uniform/Equivalence.dfy

@@ -17,4 +17,16 @@ module Uniform.Equivalence {
     reveal Model.Sample();
     Loops.UntilUnroll(Model.Proposal(n), Model.Accept(n), s);
   }
+
+  lemma SampleLifts(n: nat, u: nat, oldS: Rand.Bitstream, prevS: Rand.Bitstream, s: Rand.Bitstream)
+    requires n > 0
+    requires Model.Sample(n)(oldS) == Model.Sample(n)(prevS)
+    requires Monad.Result(u, s) == Model.Proposal(n)(prevS)
+    requires Model.Accept(n)(u)
+    ensures Model.Sample(n)(oldS) == Monad.Result(u, s)
+  {
+    reveal Model.Sample();
+    Model.SampleTerminates(n);
+    Loops.UntilUnroll(Model.Proposal(n), Model.Accept(n), prevS);
+  }
 }

src/Distributions/Uniform/Implementation.dfy

@@ -9,6 +9,7 @@ module Uniform.Implementation {
   import Model
   import Interface
   import Equivalence
+  import Loops
 
   trait {:termination false} Trait extends Interface.Trait {
     method UniformSample(n: nat) returns (u: nat)
@@ -29,7 +30,7 @@ module Uniform.Implementation {
         prevS := s;
         u := UniformPowerOfTwoSample(2 * n);
       }
-      reveal Model.Sample();
+      Equivalence.SampleLifts(n, u, old(s), prevS, s);
     }
   }
 }

src/Distributions/Uniform/Model.dfy

@@ -13,10 +13,13 @@ module Uniform.Model {
   import Loops
   import UniformPowerOfTwo
 
+  /************
+   Definitions
+  ************/
+
   // Definition 49
-  opaque ghost function Sample(n: nat): (f: Monad.Hurd<nat>)
+  opaque ghost function Sample(n: nat): Monad.Hurd<nat>
     requires n > 0
-    ensures forall s | f(s).Result? :: 0 <= f(s).value < n
   {
     SampleTerminates(n);
     Loops.Until(Proposal(n), Accept(n))
@@ -36,11 +39,14 @@ module Uniform.Model {
 
   ghost function IntervalSample(a: int, b: int): (f: Monad.Hurd<int>)
     requires a < b
-    ensures forall s | f(s).Result? :: a <= f(s).value <= b
   {
     Monad.Map(Sample(b - a), x => a + x)
   }
 
+  /*******
+   Lemmas
+  *******/
+
   lemma SampleTerminates(n: nat)
     requires n > 0
     ensures
@@ -87,4 +93,23 @@ module Uniform.Model {
       Loops.EnsureUntilTerminates(Proposal(n), Accept(n));
     }
   }
+
+  lemma SampleBound(n: nat, s: Rand.Bitstream)
+    requires n > 0
+    requires Sample(n)(s).Result?
+    ensures 0 <= Sample(n)(s).value < n
+  {
+    reveal Sample();
+    SampleTerminates(n);
+    Loops.UntilResultIsAccepted(Proposal(n), Accept(n), s);
+  }
+
+  lemma IntervalSampleBound(a: int, b: int, s: Rand.Bitstream)
+    requires a < b
+    requires IntervalSample(a, b)(s).Result?
+    ensures a <= IntervalSample(a, b)(s).value < b
+  {
+    SampleBound(b-a, s);
+  }
+
 }

src/ProbabilisticProgramming/Loops.dfy

@@ -49,27 +49,15 @@ module Loops {
   // This definition is opaque because the details are not very useful.
   // For proofs, use the lemma `WhileUnroll`.
   // Equation (3.25), but modified to use `Monad.Diverging` instead of HOL's `arb` in case of nontermination
-  opaque ghost function While<A(!new)>(condition: A -> bool, body: A -> Monad.Hurd<A>): (loop: A -> Monad.Hurd<A>)
-    ensures forall s: Rand.Bitstream, init: A :: !condition(init) ==> loop(init)(s) == Monad.Return(init)(s)
-    ensures forall s: Rand.Bitstream, init: A | loop(init)(s).Result? :: !condition(loop(init)(s).value)
-  {
-    var f :=
-      (init: A) =>
-        (s: Rand.Bitstream) =>
-          if WhileTerminatesOn(condition, body, init, s)
-          then
-            var fuel := LeastFuel(condition, body, init, s);
-            WhileCut(condition, body, init, fuel)(s)
-          else
-            Monad.Diverging;
-    assert forall s: Rand.Bitstream, init: A :: !condition(init) ==> f(init)(s) == Monad.Return(init)(s) by {
-      forall s: Rand.Bitstream, init: A ensures !condition(init) ==> f(init)(s) == Monad.Return(init)(s) {
-        if !condition(init) {
-          assert WhileCutTerminatesWithFuel(condition, body, init, s)(0);
-        }
-      }
-    }
-    f
+  opaque ghost function While<A(!new)>(condition: A -> bool, body: A -> Monad.Hurd<A>): A -> Monad.Hurd<A> {
+    (init: A) =>
+      (s: Rand.Bitstream) =>
+        if WhileTerminatesOn(condition, body, init, s)
+        then
+          var fuel := LeastFuel(condition, body, init, s);
+          WhileCut(condition, body, init, fuel)(s)
+        else
+          Monad.Diverging
   }
 
   ghost function LeastFuel<A>(condition: A -> bool, body: A -> Monad.Hurd<A>, init: A, s: Rand.Bitstream): (fuel: nat)
@@ -103,14 +91,8 @@ module Loops {
   // Definition of until loops (rejection sampling).
   // For proofs, use the lemma `UntilUnroll`.
   // Definition 44
-  ghost function Until<A(!new)>(proposal: Monad.Hurd<A>, accept: A -> bool): (f: Monad.Hurd<A>)
+  ghost function Until<A(!new)>(proposal: Monad.Hurd<A>, accept: A -> bool): Monad.Hurd<A>
     requires UntilTerminatesAlmostSurely(proposal, accept)
-    ensures
-      var reject := (a: A) => !accept(a);
-      var body := (a: A) => proposal;
-      forall s :: f(s) == proposal(s).Bind(While(reject, body))
-    ensures
-      forall s | f(s).Result? :: accept(f(s).value)
   {
     reveal While();
     var reject := (a: A) => !accept(a);
@@ -261,6 +243,7 @@ module Loops {
           unrolled;
         }
     } else {
+      WhileInitialConditionNegated(condition, body, init, s);
       calc {
         loop;
         Monad.Result(init, s);
@@ -276,6 +259,9 @@ module Loops {
     ensures loop == unrolled == Monad.Diverging
   {
     reveal While();
+    if !condition(init) {
+      WhileInitialConditionNegated(condition, body, init, s);
+    }
     match body(init)(s)
     case Diverging =>
       assert unrolled == Monad.Diverging;
@@ -432,6 +418,7 @@ module Loops {
   {
     var reject := (a: A) => !accept(a);
     var body := (a: A) => proposal;
+    UntilAsWhile(proposal, accept, s);
     match proposal(s)
     case Diverging =>
     case Result(init, s') => WhileUnroll(reject, body, init, s');
@@ -483,4 +470,37 @@ module Loops {
     }
     Independence.BindIsIndep(proposal, While(reject, body));
   }
+
+  lemma WhileNegatesCondition<A>(condition: A -> bool, body: A -> Monad.Hurd<A>, init: A, s: Rand.Bitstream)
+    requires While(condition, body)(init)(s).Result?
+    ensures !condition(While(condition, body)(init)(s).value)
+  {
+    reveal While();
+  }
+
+  lemma WhileInitialConditionNegated<A>(condition: A -> bool, body: A -> Monad.Hurd<A>, init: A, s: Rand.Bitstream)
+    requires !condition(init)
+    ensures While(condition, body)(init)(s) == Monad.Return(init)(s)
+  {
+    reveal While();
+    assert WhileCutTerminatesWithFuel(condition, body, init, s)(0);
+  }
+
+  lemma UntilResultIsAccepted<A>(proposal: Monad.Hurd<A>, accept: A -> bool, s: Rand.Bitstream)
+    requires UntilTerminatesAlmostSurely(proposal, accept)
+    requires Until(proposal, accept)(s).Result?
+    ensures accept(Until(proposal, accept)(s).value)
+  {
+    reveal While();
+  }
+
+  lemma UntilAsWhile<A>(proposal: Monad.Hurd<A>, accept: A -> bool, s: Rand.Bitstream)
+    requires UntilTerminatesAlmostSurely(proposal, accept)
+    ensures
+      var reject := (a: A) => !accept(a);
+      var body := (a: A) => proposal;
+      Until(proposal, accept)(s) == proposal(s).Bind(While(reject, body))
+  {
+    reveal While();
+  }
 }

src/Util/FisherYates/Correctness.dfy

@@ -269,6 +269,7 @@ module FisherYates.Correctness {
           var zs := Model.Shuffle(xs, i)(s).value;
           assert zs[i..] == p[i..];
           var k := Uniform.Model.IntervalSample(i, |xs|)(s).value;
+          Uniform.Model.IntervalSampleBound(i, |xs|, s);
           var s' := Uniform.Model.IntervalSample(i, |xs|)(s).rest;
           assert s in Monad.BitstreamsWithValueIn(h, A) by {
             var ys' := Model.Swap(xs, i, k);

src/Util/FisherYates/Model.dfy

@@ -20,9 +20,10 @@ module FisherYates.Model {
   {
     (s: Rand.Bitstream) =>
       if |xs[i..]| > 1 then
-        var (j, s) :- Uniform.Model.IntervalSample(i, |xs|)(s);
+        var (j, s') :- Uniform.Model.IntervalSample(i, |xs|)(s);
+        assert i <= j < |xs| by { Uniform.Model.IntervalSampleBound(i, |xs|, s); }
         var ys := Swap(xs, i, j);
-        Shuffle(ys, i + 1)(s)
+        Shuffle(ys, i + 1)(s')
       else
         Monad.Return(xs)(s)
   }