Various cleanups (#111)

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

audit.log

@@ -1,6 +1,6 @@
 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/Model.dfy(102,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. 
@@ -16,7 +16,7 @@ src/ProbabilisticProgramming/Independence.dfy(38,17): IsIndepImpliesMeasurableNa
 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/Independence.dfy(66,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/Distributions/Bernoulli/Correctness.dfy

@@ -22,19 +22,13 @@ module Bernoulli.Correctness {
     ensures Independence.IsIndep(Model.Sample(m, n))
   {
     var f := Uniform.Model.Sample(n);
-    var g := (k: nat) => Monad.Return(k < m);
+    var g := (k: nat) => 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);
-      }
-    }
-
-    Independence.BindIsIndep(f, g);
+    Independence.MapIsIndep(f, g);
     reveal Model.Sample();
   }
 

src/Distributions/Bernoulli/Model.dfy

@@ -12,8 +12,7 @@ module Bernoulli.Model {
     requires denom != 0
     requires numer <= denom
   {
-    // TODO: this should use Map instead of Bind
-    Monad.Bind(Uniform.Model.Sample(denom), (k: nat) => Monad.Return(k < numer))
+    Monad.Map(Uniform.Model.Sample(denom), (k: nat) => k < numer)
   }
 
 }

src/Distributions/BernoulliExpNeg/Equivalence.dfy

@@ -34,7 +34,7 @@ module BernoulliExpNeg.Equivalence {
     calc {
       Model.GammaLe1Loop(gamma)(ak)(s);
       { reveal Model.GammaLe1Loop(); }
-      Loops.While(Model.GammaLe1LoopCondition, Model.GammaLe1LoopIter(gamma), ak)(s);
+      Loops.While(Model.GammaLe1LoopCondition, Model.GammaLe1LoopIter(gamma))(ak)(s);
       { reveal Model.GammaLe1Loop();
         Loops.WhileUnroll(Model.GammaLe1LoopCondition, Model.GammaLe1LoopIter(gamma), ak, s); }
       Monad.Bind(Model.GammaLe1LoopIter(gamma)(ak), Model.GammaLe1Loop(gamma))(s);

src/Distributions/BernoulliExpNeg/Model.dfy

@@ -74,13 +74,11 @@ module BernoulliExpNeg.Model {
   opaque ghost function GammaLe1Loop(gamma: Rationals.Rational): ((bool, nat)) -> Monad.Hurd<(bool, nat)>
     requires 0 <= gamma.numer <= gamma.denom
   {
-    (ak: (bool, nat)) =>
-      GammaLe1LoopTerminatesAlmostSurely(gamma);
-      Loops.While(
-        GammaLe1LoopCondition,
-        GammaLe1LoopIter(gamma),
-        ak
-      )
+    GammaLe1LoopTerminatesAlmostSurely(gamma);
+    Loops.While(
+      GammaLe1LoopCondition,
+      GammaLe1LoopIter(gamma)
+    )
   }
 
   ghost function GammaLe1LoopCondition(ak: (bool, nat)): bool {

src/Distributions/DiscreteLaplace/Implementation.dfy

@@ -37,7 +37,7 @@ module DiscreteLaplace.Implementation {
         }
         var x := u + scale.numer * v;
         y := x / scale.denom;
-        b := BernoulliSample(Rationals.Rational(1, 2));
+        b := CoinSample();
       }
       z := if b then -y else y;
     }

src/Distributions/DiscreteLaplace/Interface.dfy

@@ -5,11 +5,11 @@
 
 module DiscreteLaplace.Interface {
   import Rationals
-  import Bernoulli
+  import Coin
   import Uniform
   import BernoulliExpNeg
 
-  trait {:termination false} Trait extends Bernoulli.Interface.Trait, Uniform.Interface.Trait, BernoulliExpNeg.Interface.Trait {
+  trait {:termination false} Trait extends Coin.Interface.Trait, Uniform.Interface.Trait, BernoulliExpNeg.Interface.Trait {
 
     // Based on Algorithm 2 in https://arxiv.org/pdf/2004.00010.pdf; unverified
     method DiscreteLaplaceSample(scale: Rationals.Rational) returns (z: int)

src/Distributions/Uniform/Interface.dfy

@@ -9,7 +9,7 @@ module Uniform.Interface {
   import Model
   import UniformPowerOfTwo
 
-  trait {:termination false} Trait extends Coin.Interface.Trait, UniformPowerOfTwo.Interface.Trait {
+  trait {:termination false} Trait extends UniformPowerOfTwo.Interface.Trait {
 
     method UniformSample(n: nat) returns (u: nat)
       modifies this

src/ProbabilisticProgramming/Independence.dfy

@@ -52,6 +52,16 @@ module Independence {
   lemma {:axiom} ReturnIsIndep<T>(x: T)
     ensures IsIndep(Monad.Return(x))
 
+  lemma MapIsIndep<A, B(!new)>(f: Monad.Hurd<A>, g: A -> B)
+    requires IsIndep(f)
+    ensures IsIndep(Monad.Map(f, g))
+  {
+    forall a: A ensures IsIndep(Monad.Return(g(a))) {
+      ReturnIsIndep(g(a));
+    }
+    BindIsIndep(f, (a: A) => Monad.Return(g(a)));
+  }
+
   // Equation (3.19)
   lemma {:axiom} BindIsIndep<A, B>(f: Monad.Hurd<A>, g: A -> Monad.Hurd<B>)
     requires IsIndep(f)

src/ProbabilisticProgramming/Loops.dfy

@@ -40,20 +40,20 @@ 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
-  // TODO: While(condition, body)(init) would be cleaner
-  opaque ghost function While<A>(condition: A -> bool, body: A -> Monad.Hurd<A>, init: A): (f: Monad.Hurd<A>)
-    ensures forall s: Rand.Bitstream :: !condition(init) ==> f(s) == Monad.Return(init)(s)
+  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)
   {
     var f :=
-      (s: Rand.Bitstream) =>
-        if WhileCutTerminates(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 :: !condition(init) ==> f(s) == Monad.Return(init)(s) by {
-      forall s: Rand.Bitstream ensures !condition(init) ==> f(s) == Monad.Return(init)(s) {
+      (init: A) =>
+        (s: Rand.Bitstream) =>
+          if WhileCutTerminates(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);
         }
@@ -93,16 +93,16 @@ module Loops {
   // Definition of until loops (rejection sampling).
   // For proofs, use the lemma `UntilUnroll`.
   // Definition 44
-  ghost function Until<A>(proposal: Monad.Hurd<A>, accept: A -> bool): (f: Monad.Hurd<A>)
+  ghost function Until<A(!new)>(proposal: Monad.Hurd<A>, accept: A -> bool): (f: 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(init => While(reject, body, init))
+      forall s :: f(s) == proposal(s).Bind(While(reject, body))
   {
     var reject := (a: A) => !accept(a);
     var body := (a: A) => proposal;
-    Monad.Bind(proposal, (a: A) => While(reject, body, a))
+    Monad.Bind(proposal, While(reject, body))
   }
 
   function WhileLoopExitsAfterOneIteration<A(!new)>(body: A -> Monad.Hurd<A>, condition: A -> bool, init: A): (Rand.Bitstream -> bool) {
@@ -115,13 +115,13 @@ module Loops {
       proposal(s).Satisfies(accept)
   }
 
-  ghost function UntilLoopResultIsAccepted<A>(proposal: Monad.Hurd<A>, accept: A -> bool): (Rand.Bitstream -> bool)
+  ghost function UntilLoopResultIsAccepted<A(!new)>(proposal: Monad.Hurd<A>, accept: A -> bool): (Rand.Bitstream -> bool)
     requires UntilTerminatesAlmostSurely(proposal, accept)
   {
     (s: Rand.Bitstream) => Until(proposal, accept)(s).Satisfies(accept)
   }
 
-  ghost function UntilLoopResultHasProperty<A>(proposal: Monad.Hurd<A>, accept: A -> bool, property: A -> bool): iset<Rand.Bitstream>
+  ghost function UntilLoopResultHasProperty<A(!new)>(proposal: Monad.Hurd<A>, accept: A -> bool, property: A -> bool): iset<Rand.Bitstream>
     requires UntilTerminatesAlmostSurely(proposal, accept)
   {
     iset s | Until(proposal, accept)(s).Satisfies(property)
@@ -192,8 +192,8 @@ module Loops {
     requires WhileCutTerminates(condition, body, init, s)
     requires condition(init)
     requires body(init)(s) == Monad.Result(init', s')
-    requires loop == While(condition, body, init)(s)
-    requires unrolled == While(condition, body, init')(s')
+    requires loop == While(condition, body)(init)(s)
+    requires unrolled == While(condition, body)(init')(s')
     ensures loop == unrolled
   {
     var fuel: nat := LeastFuel(condition, body, init, s);
@@ -218,11 +218,11 @@ module Loops {
     }
   }
 
-  lemma WhileUnrollIfTerminates<A>(condition: A -> bool, body: A -> Monad.Hurd<A>, init: A, s: Rand.Bitstream, fuel: nat, loop: Monad.Result<A>, unrolled: Monad.Result<A>)
+  lemma WhileUnrollIfTerminates<A(!new)>(condition: A -> bool, body: A -> Monad.Hurd<A>, init: A, s: Rand.Bitstream, fuel: nat, loop: Monad.Result<A>, unrolled: Monad.Result<A>)
     requires WhileCutTerminates(condition, body, init, s)
     requires fuel == LeastFuel(condition, body, init, s)
-    requires loop == While(condition, body, init)(s)
-    requires unrolled == (if condition(init) then Monad.Bind(body(init), (init': A) => While(condition, body, init')) else Monad.Return(init))(s)
+    requires loop == While(condition, body)(init)(s)
+    requires unrolled == (if condition(init) then Monad.Bind(body(init), While(condition, body)) else Monad.Return(init))(s)
     ensures loop == unrolled
   {
     if condition(init) {
@@ -240,7 +240,7 @@ module Loops {
         calc {
           loop;
           { WhileUnrollIfConditionSatisfied(condition, body, init, s, init', s', loop, unrolled); }
-          While(condition, body, init')(s');
+          While(condition, body)(init')(s');
           unrolled;
         }
     } else {
@@ -254,8 +254,8 @@ module Loops {
 
   lemma WhileUnrollIfDiverges<A>(condition: A -> bool, body: A -> Monad.Hurd<A>, init: A, s: Rand.Bitstream, loop: Monad.Result<A>, unrolled: Monad.Result<A>)
     requires !WhileCutTerminates(condition, body, init, s)
-    requires loop == While(condition, body, init)(s)
-    requires unrolled == (if condition(init) then Monad.Bind(body(init), (init': A) => While(condition, body, init')) else Monad.Return(init))(s)
+    requires loop == While(condition, body)(init)(s)
+    requires unrolled == (if condition(init) then Monad.Bind(body(init), While(condition, body)) else Monad.Return(init))(s)
     ensures loop == unrolled == Monad.Diverging
   {
     reveal While();
@@ -269,12 +269,12 @@ module Loops {
   }
 
   // Theorem 38
-  lemma WhileUnroll<A>(condition: A -> bool, body: A -> Monad.Hurd<A>, init: A, s: Rand.Bitstream)
+  lemma WhileUnroll<A(!new)>(condition: A -> bool, body: A -> Monad.Hurd<A>, init: A, s: Rand.Bitstream)
     requires WhileTerminatesAlmostSurely(condition, body)
-    ensures While(condition, body, init)(s) == (if condition(init) then Monad.Bind(body(init), (init': A) => While(condition, body, init')) else Monad.Return(init))(s)
+    ensures While(condition, body)(init)(s) == (if condition(init) then Monad.Bind(body(init), While(condition, body)) else Monad.Return(init))(s)
   {
-    var loop := While(condition, body, init)(s);
-    var unrolled := (if condition(init) then Monad.Bind(body(init), (init': A) => While(condition, body, init')) else Monad.Return(init))(s);
+    var loop := While(condition, body)(init)(s);
+    var unrolled := (if condition(init) then Monad.Bind(body(init), While(condition, body)) else Monad.Return(init))(s);
     assert loop == unrolled by {
       if WhileCutTerminates(condition, body, init, s) {
         var fuel: nat := LeastFuel(condition, body, init, s);
@@ -366,7 +366,7 @@ module Loops {
   lemma WhileIsIndep<A(!new)>(condition: A -> bool, body: A -> Monad.Hurd<A>, init: A)
     requires forall a: A :: Independence.IsIndep(body(a))
     requires WhileTerminatesAlmostSurely(condition, body)
-    ensures Independence.IsIndep(While(condition, body, init))
+    ensures Independence.IsIndep(While(condition, body)(init))
   {
     // To prove this, we need a definition of Independence.IsIndep
     assume {:axiom} false;
@@ -379,10 +379,9 @@ module Loops {
   {
     var reject := (a: A) => !accept(a);
     var body := (a: A) => proposal;
-    var f := (init: A) => While(reject, body, init);
-    forall init: A ensures Independence.IsIndep(f(init)) {
+    forall init: A ensures Independence.IsIndep(While(reject, body)(init)) {
       WhileIsIndep(reject, body, init);
     }
-    Independence.BindIsIndep(proposal, f);
+    Independence.BindIsIndep(proposal, While(reject, body));
   }
 }