-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add model and state correctness property of BernoulliExpNeg (#87)
<small>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).</small>
- Loading branch information
Showing
7 changed files
with
194 additions
and
20 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,20 @@ | ||
| /******************************************************************************* | ||
| * Copyright by the contributors to the Dafny Project | ||
| * SPDX-License-Identifier: MIT | ||
| *******************************************************************************/ | ||
|
|
||
| module BernoulliExpNeg.Correctness { | ||
| import Rationals | ||
| import Exponential | ||
| import RandomNumberGenerator | ||
| import Independence | ||
| import Model | ||
|
|
||
| lemma {:axiom} Correctness(gamma: Rationals.Rational) | ||
| requires 0 <= gamma.numer | ||
| ensures RandomNumberGenerator.mu(iset s | Model.Sample(gamma)(s).0) == Exponential.Exp(-Rationals.ToReal(gamma)) | ||
|
|
||
| lemma {:axiom} SampleIsIndepFn(gamma: Rationals.Rational) | ||
| requires 0 <= gamma.numer | ||
| ensures Independence.IsIndepFn(Model.Sample(gamma)) | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,76 @@ | ||
| /******************************************************************************* | ||
| * Copyright by the contributors to the Dafny Project | ||
| * SPDX-License-Identifier: MIT | ||
| *******************************************************************************/ | ||
|
|
||
| module BernoulliExpNeg.Model { | ||
| import Rationals | ||
| import Uniform | ||
| import Monad | ||
| import WhileAndUntil | ||
| import BernoulliModel = Bernoulli.Model | ||
|
|
||
| function Sample(gamma: Rationals.Rational): Monad.Hurd<bool> | ||
| requires gamma.denom != 0 | ||
| requires gamma.numer >= 0 | ||
| { | ||
| Monad.Bind( | ||
| GammaReductionLoop(gamma), | ||
| (bgamma: (bool, Rationals.Rational)) => | ||
| if bgamma.0 then | ||
| SampleGammaLe1(bgamma.1) | ||
| else | ||
| Monad.Return(false) | ||
| ) | ||
| } | ||
|
|
||
| function GammaReductionLoop(gamma: Rationals.Rational): Monad.Hurd<(bool, Rationals.Rational)> | ||
| requires gamma.numer >= 0 | ||
| { | ||
| assume {:axiom} false; // assume termination | ||
| WhileAndUntil.ProbWhile( | ||
| (bgamma: (bool, Rationals.Rational)) => bgamma.0 && bgamma.1.denom <= bgamma.1.numer, | ||
| GammaReductionLoopIter, | ||
| (true, gamma) | ||
| ) | ||
| } | ||
|
|
||
| function GammaReductionLoopIter(bgamma: (bool, Rationals.Rational)): Monad.Hurd<(bool, Rationals.Rational)> | ||
| requires bgamma.1.numer >= 0 | ||
| { | ||
| Monad.Bind( | ||
| SampleGammaLe1(Rationals.Int(1)), | ||
| b' => Monad.Return((b', Rationals.Rational(bgamma.1.numer - bgamma.1.denom, bgamma.1.denom))) | ||
| ) | ||
| } | ||
|
|
||
| function SampleGammaLe1(gamma: Rationals.Rational): Monad.Hurd<bool> | ||
| { | ||
| if 0 <= gamma.numer <= gamma.denom | ||
| then Monad.Bind( | ||
| GammaLe1Loop(gamma, (true, 0)), | ||
| (ak: (bool, nat)) => Monad.Return(ak.1 % 2 == 1) | ||
| ) | ||
| else Monad.Return(false) // to keep this function total, we return a dummy value here | ||
| } | ||
|
|
||
| function GammaLe1Loop(gamma: Rationals.Rational, ak: (bool, nat)): Monad.Hurd<(bool, nat)> | ||
| requires 0 <= gamma.numer <= gamma.denom | ||
| { | ||
| assume {:axiom} false; // assume termination | ||
| WhileAndUntil.ProbWhile( | ||
| (ak: (bool, nat)) => ak.0, | ||
| (ak: (bool, nat)) => GammaLe1LoopIter(gamma, ak), | ||
| ak | ||
| ) | ||
| } | ||
|
|
||
| function GammaLe1LoopIter(gamma: Rationals.Rational, ak: (bool, nat)): Monad.Hurd<(bool, nat)> | ||
| requires 0 <= gamma.numer <= gamma.denom | ||
| { | ||
| Monad.Bind( | ||
| BernoulliModel.Sample(gamma.numer, (ak.1 + 1) * gamma.denom), | ||
| (a': bool) => Monad.Return((a', ak.1 + 1)) | ||
| ) | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,52 @@ | ||
| module Exponential { | ||
| ghost function {:axiom} Exp(x: real): real | ||
|
|
||
| lemma {:axiom} FunctionalEquation(x: real, y: real) | ||
| ensures Exp(x + y) == Exp(x) * Exp(y) | ||
|
|
||
| lemma {:axiom} Increasing(x: real, y: real) | ||
| requires x < y | ||
| ensures Exp(x) < Exp(y) | ||
|
|
||
| lemma {:axiom} EvalOne() | ||
| ensures 2.718281828 <= Exp(1.0) <= 2.718281829 | ||
|
|
||
| lemma Positive(x: real) | ||
| ensures Exp(x) > 0.0 | ||
| { | ||
| assert Exp(x) >= 0.0 by { | ||
| var sqrt := Exp(x / 2.0); | ||
| calc { | ||
| Exp(x); | ||
| { FunctionalEquation(x / 2.0, x / 2.0); } | ||
| sqrt * sqrt; | ||
| >= | ||
| 0.0; | ||
| } | ||
| } | ||
| if Exp(x) == 0.0 { | ||
| calc { | ||
| 0.0; | ||
| Exp(x); | ||
| < { Increasing(x, x + 1.0); } | ||
| Exp(x + 1.0); | ||
| { FunctionalEquation(x, 1.0); } | ||
| Exp(x) * Exp(1.0); | ||
| == | ||
| 0.0; | ||
| } | ||
| } | ||
| } | ||
|
|
||
| lemma EvalZero() | ||
| ensures Exp(0.0) == 1.0 | ||
| { | ||
| var one := Exp(0.0); | ||
| assert one > 0.0 by { | ||
| Positive(0.0); | ||
| } | ||
| assert one * one == one by { | ||
| FunctionalEquation(0.0, 0.0); | ||
| } | ||
| } | ||
| } |