From 9568c0ea7092011f37b6d67b24aecf899966a6be Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Mon, 6 Nov 2023 10:57:52 -0500 Subject: [PATCH] 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 | 4 +- src/Distributions/Bernoulli/Correctness.dfy | 10 +-- src/Distributions/Bernoulli/Model.dfy | 3 +- .../BernoulliExpNeg/Equivalence.dfy | 2 +- src/Distributions/BernoulliExpNeg/Model.dfy | 12 ++-- .../DiscreteLaplace/Implementation.dfy | 2 +- .../DiscreteLaplace/Interface.dfy | 4 +- src/Distributions/Uniform/Interface.dfy | 2 +- src/ProbabilisticProgramming/Independence.dfy | 10 +++ src/ProbabilisticProgramming/Loops.dfy | 65 +++++++++---------- 10 files changed, 57 insertions(+), 57 deletions(-) diff --git a/audit.log b/audit.log index ae474d2e..2ca7acef 100644 --- a/audit.log +++ b/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. diff --git a/src/Distributions/Bernoulli/Correctness.dfy b/src/Distributions/Bernoulli/Correctness.dfy index e4fb0d87..33951bf5 100644 --- a/src/Distributions/Bernoulli/Correctness.dfy +++ b/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(); } diff --git a/src/Distributions/Bernoulli/Model.dfy b/src/Distributions/Bernoulli/Model.dfy index 6d5ee0bf..7782a987 100644 --- a/src/Distributions/Bernoulli/Model.dfy +++ b/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) } } diff --git a/src/Distributions/BernoulliExpNeg/Equivalence.dfy b/src/Distributions/BernoulliExpNeg/Equivalence.dfy index 05e51d44..cf63ccf2 100644 --- a/src/Distributions/BernoulliExpNeg/Equivalence.dfy +++ b/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); diff --git a/src/Distributions/BernoulliExpNeg/Model.dfy b/src/Distributions/BernoulliExpNeg/Model.dfy index 5186033e..5d6c91e5 100644 --- a/src/Distributions/BernoulliExpNeg/Model.dfy +++ b/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 { diff --git a/src/Distributions/DiscreteLaplace/Implementation.dfy b/src/Distributions/DiscreteLaplace/Implementation.dfy index 7cc70a9d..b15e39b3 100644 --- a/src/Distributions/DiscreteLaplace/Implementation.dfy +++ b/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; } diff --git a/src/Distributions/DiscreteLaplace/Interface.dfy b/src/Distributions/DiscreteLaplace/Interface.dfy index a7d8f143..7b2be999 100644 --- a/src/Distributions/DiscreteLaplace/Interface.dfy +++ b/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) diff --git a/src/Distributions/Uniform/Interface.dfy b/src/Distributions/Uniform/Interface.dfy index 42b53c1a..1095581b 100644 --- a/src/Distributions/Uniform/Interface.dfy +++ b/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 diff --git a/src/ProbabilisticProgramming/Independence.dfy b/src/ProbabilisticProgramming/Independence.dfy index 546d9d2c..e025de51 100644 --- a/src/ProbabilisticProgramming/Independence.dfy +++ b/src/ProbabilisticProgramming/Independence.dfy @@ -52,6 +52,16 @@ module Independence { lemma {:axiom} ReturnIsIndep(x: T) ensures IsIndep(Monad.Return(x)) + lemma MapIsIndep(f: Monad.Hurd, 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(f: Monad.Hurd, g: A -> Monad.Hurd) requires IsIndep(f) diff --git a/src/ProbabilisticProgramming/Loops.dfy b/src/ProbabilisticProgramming/Loops.dfy index 7b1fdf98..8ef80d64 100644 --- a/src/ProbabilisticProgramming/Loops.dfy +++ b/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(condition: A -> bool, body: A -> Monad.Hurd, init: A): (f: Monad.Hurd) - ensures forall s: Rand.Bitstream :: !condition(init) ==> f(s) == Monad.Return(init)(s) + opaque ghost function While(condition: A -> bool, body: A -> Monad.Hurd): (loop: A -> Monad.Hurd) + 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(proposal: Monad.Hurd, accept: A -> bool): (f: Monad.Hurd) + ghost function Until(proposal: Monad.Hurd, accept: A -> bool): (f: Monad.Hurd) 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(body: A -> Monad.Hurd, condition: A -> bool, init: A): (Rand.Bitstream -> bool) { @@ -115,13 +115,13 @@ module Loops { proposal(s).Satisfies(accept) } - ghost function UntilLoopResultIsAccepted(proposal: Monad.Hurd, accept: A -> bool): (Rand.Bitstream -> bool) + ghost function UntilLoopResultIsAccepted(proposal: Monad.Hurd, accept: A -> bool): (Rand.Bitstream -> bool) requires UntilTerminatesAlmostSurely(proposal, accept) { (s: Rand.Bitstream) => Until(proposal, accept)(s).Satisfies(accept) } - ghost function UntilLoopResultHasProperty(proposal: Monad.Hurd, accept: A -> bool, property: A -> bool): iset + ghost function UntilLoopResultHasProperty(proposal: Monad.Hurd, accept: A -> bool, property: A -> bool): iset 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(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream, fuel: nat, loop: Monad.Result, unrolled: Monad.Result) + lemma WhileUnrollIfTerminates(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream, fuel: nat, loop: Monad.Result, unrolled: Monad.Result) 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(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream, loop: Monad.Result, unrolled: Monad.Result) 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(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream) + lemma WhileUnroll(condition: A -> bool, body: A -> Monad.Hurd, 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(condition: A -> bool, body: A -> Monad.Hurd, 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)); } }