From beca2efb0dea50778656fb44f910f8c8dc94a612 Mon Sep 17 00:00:00 2001 From: Stefan Zetzsche <120379523+stefan-aws@users.noreply.github.com> Date: Fri, 29 Sep 2023 14:34:40 +0200 Subject: [PATCH] Remove ghost where possible and run formatter (#59) 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). Co-authored-by: John Tristan --- src/Distributions/Base/Interface.dfy | 6 +- src/Distributions/Base/Model.dfy | 6 +- src/Distributions/Bernoulli/Correctness.dfy | 8 +- .../Bernoulli/Implementation.dfy | 6 +- src/Distributions/Bernoulli/Interface.dfy | 6 +- src/Distributions/Bernoulli/Model.dfy | 16 ++-- .../BernoulliExpNeg/Implementation.dfy | 6 +- .../BernoulliExpNeg/Interface.dfy | 8 +- .../BernoulliRational/Correctness.dfy | 6 +- .../BernoulliRational/Implementation.dfy | 8 +- .../BernoulliRational/Interface.dfy | 8 +- src/Distributions/BernoulliRational/Model.dfy | 6 +- .../DiscreteGaussian/Implementation.dfy | 6 +- .../DiscreteGaussian/Interface.dfy | 6 +- .../DiscreteLaplace/Implementation.dfy | 6 +- .../DiscreteLaplace/Interface.dfy | 6 +- src/Distributions/Geometric/Correctness.dfy | 8 +- .../Geometric/Implementation.dfy | 6 +- src/Distributions/Geometric/Interface.dfy | 6 +- src/Distributions/Geometric/Model.dfy | 8 +- src/Distributions/Uniform/Implementation.dfy | 6 +- src/Distributions/Uniform/Interface.dfy | 6 +- src/Distributions/Uniform/Model.dfy | 6 +- .../UniformPowerOfTwo/Correctness.dfy | 80 +++++++++---------- .../UniformPowerOfTwo/Implementation.dfy | 6 +- .../UniformPowerOfTwo/Interface.dfy | 6 +- src/Distributions/UniformPowerOfTwo/Model.dfy | 6 +- src/Math/Helper.dfy | 10 +-- src/Math/MeasureTheory.dfy | 22 ++--- src/ProbabilisticProgramming/Independence.dfy | 8 +- src/ProbabilisticProgramming/Quantifier.dfy | 6 +- .../RandomNumberGenerator.dfy | 6 +- .../WhileAndUntil.dfy | 18 ++--- tests/Tests.dfy | 6 +- tests/TestsExternUniform.dfy | 8 +- tests/TestsFoundational.dfy | 8 +- 36 files changed, 172 insertions(+), 178 deletions(-) diff --git a/src/Distributions/Base/Interface.dfy b/src/Distributions/Base/Interface.dfy index 72766ddf..19a478bf 100644 --- a/src/Distributions/Base/Interface.dfy +++ b/src/Distributions/Base/Interface.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy" include "Model.dfy" diff --git a/src/Distributions/Base/Model.dfy b/src/Distributions/Base/Model.dfy index 3ebd0ec9..0c833f30 100644 --- a/src/Distributions/Base/Model.dfy +++ b/src/Distributions/Base/Model.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy" include "../../ProbabilisticProgramming/Monad.dfy" diff --git a/src/Distributions/Bernoulli/Correctness.dfy b/src/Distributions/Bernoulli/Correctness.dfy index 981bd332..3ad807d7 100644 --- a/src/Distributions/Bernoulli/Correctness.dfy +++ b/src/Distributions/Bernoulli/Correctness.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../Math/MeasureTheory.dfy" include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy" @@ -13,7 +13,7 @@ module BernoulliCorrectness { import RandomNumberGenerator import Independence import BernoulliModel - + /******* Lemmas *******/ diff --git a/src/Distributions/Bernoulli/Implementation.dfy b/src/Distributions/Bernoulli/Implementation.dfy index 5a797227..45620781 100644 --- a/src/Distributions/Bernoulli/Implementation.dfy +++ b/src/Distributions/Bernoulli/Implementation.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../Math/MeasureTheory.dfy" include "Interface.dfy" diff --git a/src/Distributions/Bernoulli/Interface.dfy b/src/Distributions/Bernoulli/Interface.dfy index f714fb1a..27a5d07b 100644 --- a/src/Distributions/Bernoulli/Interface.dfy +++ b/src/Distributions/Bernoulli/Interface.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../Base/Interface.dfy" include "Model.dfy" diff --git a/src/Distributions/Bernoulli/Model.dfy b/src/Distributions/Bernoulli/Model.dfy index 6844e881..c93cd412 100644 --- a/src/Distributions/Bernoulli/Model.dfy +++ b/src/Distributions/Bernoulli/Model.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../Math/MeasureTheory.dfy" include "../../ProbabilisticProgramming/Monad.dfy" @@ -16,15 +16,9 @@ module BernoulliModel { var f := (b: bool) => if b then - if p <= 0.5 then - Monad.Return(false) - else - ProbBernoulli(2.0 * p - 1.0) + (if p <= 0.5 then Monad.Return(false) else ProbBernoulli(2.0 * p - 1.0)) else - if p <= 0.5 then - ProbBernoulli(2.0 * p) - else - Monad.Return(true); + (if p <= 0.5 then ProbBernoulli(2.0 * p) else Monad.Return(true)); Monad.Bind(Monad.Deconstruct, f) } } diff --git a/src/Distributions/BernoulliExpNeg/Implementation.dfy b/src/Distributions/BernoulliExpNeg/Implementation.dfy index 89d7291b..660c3efe 100644 --- a/src/Distributions/BernoulliExpNeg/Implementation.dfy +++ b/src/Distributions/BernoulliExpNeg/Implementation.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../Bernoulli/Interface.dfy" include "Interface.dfy" diff --git a/src/Distributions/BernoulliExpNeg/Interface.dfy b/src/Distributions/BernoulliExpNeg/Interface.dfy index e41624e1..f78cf989 100644 --- a/src/Distributions/BernoulliExpNeg/Interface.dfy +++ b/src/Distributions/BernoulliExpNeg/Interface.dfy @@ -1,13 +1,13 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../Bernoulli/Interface.dfy" module BernoulliExpNegInterface { import BernoulliInterface - + trait {:termination false} IBernoulliExpNeg extends BernoulliInterface.IBernoulli { method BernoulliExpNeg(gamma: real) returns (c: bool) diff --git a/src/Distributions/BernoulliRational/Correctness.dfy b/src/Distributions/BernoulliRational/Correctness.dfy index 81bfd883..9bfda219 100644 --- a/src/Distributions/BernoulliRational/Correctness.dfy +++ b/src/Distributions/BernoulliRational/Correctness.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../Math/MeasureTheory.dfy" include "../../Math/Helper.dfy" diff --git a/src/Distributions/BernoulliRational/Implementation.dfy b/src/Distributions/BernoulliRational/Implementation.dfy index ba672828..b9d9655a 100644 --- a/src/Distributions/BernoulliRational/Implementation.dfy +++ b/src/Distributions/BernoulliRational/Implementation.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "Interface.dfy" include "Model.dfy" @@ -12,7 +12,7 @@ module BernoulliRationalImplementation { trait {:termination false} TBernoulliRational extends BernoulliRationalInterface.IBernoulliRational { - method BernoulliRational(m: nat, n: nat) returns (c: bool) + method BernoulliRational(m: nat, n: nat) returns (c: bool) modifies this decreases * requires n != 0 diff --git a/src/Distributions/BernoulliRational/Interface.dfy b/src/Distributions/BernoulliRational/Interface.dfy index 8f9c4010..f883bf51 100644 --- a/src/Distributions/BernoulliRational/Interface.dfy +++ b/src/Distributions/BernoulliRational/Interface.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../Uniform/Interface.dfy" include "Model.dfy" @@ -9,7 +9,7 @@ include "Model.dfy" module BernoulliRationalInterface { import UniformInterface import BernoulliRationalModel - + trait {:termination false} IBernoulliRational extends UniformInterface.IUniform { method BernoulliRational(m: nat, n: nat) returns (c: bool) diff --git a/src/Distributions/BernoulliRational/Model.dfy b/src/Distributions/BernoulliRational/Model.dfy index 734254db..617fe913 100644 --- a/src/Distributions/BernoulliRational/Model.dfy +++ b/src/Distributions/BernoulliRational/Model.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../Uniform/Model.dfy" include "../../ProbabilisticProgramming/Monad.dfy" diff --git a/src/Distributions/DiscreteGaussian/Implementation.dfy b/src/Distributions/DiscreteGaussian/Implementation.dfy index 5819f861..66cc2e07 100644 --- a/src/Distributions/DiscreteGaussian/Implementation.dfy +++ b/src/Distributions/DiscreteGaussian/Implementation.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "Interface.dfy" diff --git a/src/Distributions/DiscreteGaussian/Interface.dfy b/src/Distributions/DiscreteGaussian/Interface.dfy index a162ad6a..5f036d2f 100644 --- a/src/Distributions/DiscreteGaussian/Interface.dfy +++ b/src/Distributions/DiscreteGaussian/Interface.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../BernoulliExpNeg/Interface.dfy" include "../DiscreteLaplace/Interface.dfy" diff --git a/src/Distributions/DiscreteLaplace/Implementation.dfy b/src/Distributions/DiscreteLaplace/Implementation.dfy index 42c5f036..e5fb839e 100644 --- a/src/Distributions/DiscreteLaplace/Implementation.dfy +++ b/src/Distributions/DiscreteLaplace/Implementation.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "Interface.dfy" diff --git a/src/Distributions/DiscreteLaplace/Interface.dfy b/src/Distributions/DiscreteLaplace/Interface.dfy index 6520125e..99092226 100644 --- a/src/Distributions/DiscreteLaplace/Interface.dfy +++ b/src/Distributions/DiscreteLaplace/Interface.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../Bernoulli/Interface.dfy" include "../Uniform/Interface.dfy" diff --git a/src/Distributions/Geometric/Correctness.dfy b/src/Distributions/Geometric/Correctness.dfy index 01f8e315..8fa837a8 100644 --- a/src/Distributions/Geometric/Correctness.dfy +++ b/src/Distributions/Geometric/Correctness.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../Math/Helper.dfy" include "../../ProbabilisticProgramming/Monad.dfy" @@ -20,7 +20,7 @@ module GeometricCorrectness { /******* Lemmas *******/ - + // Equation (4.19) lemma {:axiom} ProbGeometricIsIndepFn() ensures Independence.IsIndepFn(GeometricModel.ProbGeometric()) diff --git a/src/Distributions/Geometric/Implementation.dfy b/src/Distributions/Geometric/Implementation.dfy index 772f225c..55184afb 100644 --- a/src/Distributions/Geometric/Implementation.dfy +++ b/src/Distributions/Geometric/Implementation.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../ProbabilisticProgramming/Monad.dfy" include "Interface.dfy" diff --git a/src/Distributions/Geometric/Interface.dfy b/src/Distributions/Geometric/Interface.dfy index 3ce96882..32ee6619 100644 --- a/src/Distributions/Geometric/Interface.dfy +++ b/src/Distributions/Geometric/Interface.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../ProbabilisticProgramming/Monad.dfy" include "../Base/Interface.dfy" diff --git a/src/Distributions/Geometric/Model.dfy b/src/Distributions/Geometric/Model.dfy index d0e2b3a5..e15c8cc6 100644 --- a/src/Distributions/Geometric/Model.dfy +++ b/src/Distributions/Geometric/Model.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../ProbabilisticProgramming/Monad.dfy" include "../../ProbabilisticProgramming/WhileAndUntil.dfy" @@ -19,7 +19,7 @@ module GeometricModel { Monad.Bind(g, f) } - // Equation (4.17) + // Equation (4.17) function ProbGeometricIter(t: (bool, int)): (f: Monad.Hurd<(bool, int)>) ensures forall s :: f(s) == ((Monad.Head(s), t.1 + 1), Monad.Tail(s)) { diff --git a/src/Distributions/Uniform/Implementation.dfy b/src/Distributions/Uniform/Implementation.dfy index 457848a4..e51b3310 100644 --- a/src/Distributions/Uniform/Implementation.dfy +++ b/src/Distributions/Uniform/Implementation.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../UniformPowerOfTwo/Interface.dfy" include "../UniformPowerOfTwo/Implementation.dfy" diff --git a/src/Distributions/Uniform/Interface.dfy b/src/Distributions/Uniform/Interface.dfy index 1c083605..2ab201fd 100644 --- a/src/Distributions/Uniform/Interface.dfy +++ b/src/Distributions/Uniform/Interface.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../Base/Interface.dfy" include "../UniformPowerOfTwo/Interface.dfy" diff --git a/src/Distributions/Uniform/Model.dfy b/src/Distributions/Uniform/Model.dfy index 149ed9a6..c9c171f1 100644 --- a/src/Distributions/Uniform/Model.dfy +++ b/src/Distributions/Uniform/Model.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy" include "../../ProbabilisticProgramming/Monad.dfy" diff --git a/src/Distributions/UniformPowerOfTwo/Correctness.dfy b/src/Distributions/UniformPowerOfTwo/Correctness.dfy index 1e00dbbb..9f2ee5aa 100644 --- a/src/Distributions/UniformPowerOfTwo/Correctness.dfy +++ b/src/Distributions/UniformPowerOfTwo/Correctness.dfy @@ -196,38 +196,38 @@ module UniformPowerOfTwoCorrectness { ensures UnifIsCorrect(n, 1, m) { calc { + RandomNumberGenerator.mu(iset s | UniformPowerOfTwoModel.ProbUnif(n)(s).0 == m); + == { ProbUnifCaseSplit(n, m); } + RandomNumberGenerator.mu(iset s | 2*UniformPowerOfTwoModel.ProbUnif(n / 2)(s).0 + 1 == m) / 2.0; + == { assert (iset s | 2*UniformPowerOfTwoModel.ProbUnif(n / 2)(s).0 + 1 == m) == (iset s {:trigger 1 == m} | 1 == m); } + RandomNumberGenerator.mu(iset s {:trigger 1 == m} | 1 == m) / 2.0; + } + if m < Helper.Power(2, 1) { + assert m == 1; + calc { RandomNumberGenerator.mu(iset s | UniformPowerOfTwoModel.ProbUnif(n)(s).0 == m); - == { ProbUnifCaseSplit(n, m); } - RandomNumberGenerator.mu(iset s | 2*UniformPowerOfTwoModel.ProbUnif(n / 2)(s).0 + 1 == m) / 2.0; - == { assert (iset s | 2*UniformPowerOfTwoModel.ProbUnif(n / 2)(s).0 + 1 == m) == (iset s {:trigger 1 == m} | 1 == m); } + == RandomNumberGenerator.mu(iset s {:trigger 1 == m} | 1 == m) / 2.0; + == { assert (iset s: RandomNumberGenerator.RNG {:trigger 1 == m} | 1 == m) == (iset s {:trigger true} | true); } + RandomNumberGenerator.mu(iset s {:trigger true} | true) / 2.0; + == { RandomNumberGenerator.RNGHasMeasure(); Helper.DivisionSubstituteAlternativeReal(2.0, RandomNumberGenerator.mu(iset s {:trigger true} | true), 1.0); } + 1.0 / 2.0; + == + 1.0 / (Helper.Power(2, 1) as real); + } + } else { + assert m != 1; + calc { + RandomNumberGenerator.mu(iset s: RandomNumberGenerator.RNG | UniformPowerOfTwoModel.ProbUnif(n)(s).0 == m); + == + RandomNumberGenerator.mu(iset s: RandomNumberGenerator.RNG {:trigger 1 == m} | 1 == m) / 2.0; + == { assert (iset s: RandomNumberGenerator.RNG {:trigger 1 == m} | 1 == m) == iset{}; } + RandomNumberGenerator.mu(iset {}) / 2.0; + == { RandomNumberGenerator.RNGHasMeasure(); } + 0.0 / 2.0; + == + 0.0; } - if m < Helper.Power(2, 1) { - assert m == 1; - calc { - RandomNumberGenerator.mu(iset s | UniformPowerOfTwoModel.ProbUnif(n)(s).0 == m); - == - RandomNumberGenerator.mu(iset s {:trigger 1 == m} | 1 == m) / 2.0; - == { assert (iset s: RandomNumberGenerator.RNG {:trigger 1 == m} | 1 == m) == (iset s {:trigger true} | true); } - RandomNumberGenerator.mu(iset s {:trigger true} | true) / 2.0; - == { RandomNumberGenerator.RNGHasMeasure(); Helper.DivisionSubstituteAlternativeReal(2.0, RandomNumberGenerator.mu(iset s {:trigger true} | true), 1.0); } - 1.0 / 2.0; - == - 1.0 / (Helper.Power(2, 1) as real); - } - } else { - assert m != 1; - calc { - RandomNumberGenerator.mu(iset s: RandomNumberGenerator.RNG | UniformPowerOfTwoModel.ProbUnif(n)(s).0 == m); - == - RandomNumberGenerator.mu(iset s: RandomNumberGenerator.RNG {:trigger 1 == m} | 1 == m) / 2.0; - == { assert (iset s: RandomNumberGenerator.RNG {:trigger 1 == m} | 1 == m) == iset{}; } - RandomNumberGenerator.mu(iset {}) / 2.0; - == { RandomNumberGenerator.RNGHasMeasure(); } - 0.0 / 2.0; - == - 0.0; - } } } @@ -315,13 +315,13 @@ module UniformPowerOfTwoCorrectness { ensures (1.0 / Helper.Power(2, k) as real) / 2.0 == 1.0 / (Helper.Power(2, k + 1) as real) { calc { - (1.0 / Helper.Power(2, k) as real) / 2.0; - == { Helper.DivDivToDivMul(1.0, Helper.Power(2, k) as real, 2.0); } - 1.0 / (Helper.Power(2, k) as real * 2.0); - == { Helper.NatMulNatToReal(Helper.Power(2, k), 2); } - 1.0 / (Helper.Power(2, k) * 2) as real; - == - 1.0 / (Helper.Power(2, k + 1) as real); + (1.0 / Helper.Power(2, k) as real) / 2.0; + == { Helper.DivDivToDivMul(1.0, Helper.Power(2, k) as real, 2.0); } + 1.0 / (Helper.Power(2, k) as real * 2.0); + == { Helper.NatMulNatToReal(Helper.Power(2, k), 2); } + 1.0 / (Helper.Power(2, k) * 2) as real; + == + 1.0 / (Helper.Power(2, k + 1) as real); } } @@ -366,13 +366,13 @@ module UniformPowerOfTwoCorrectness { forall s ensures f(s) in e <==> g(s) in e' { calc { f(s) in e; - <==> { assert f(s) == UniformPowerOfTwoModel.ProbUnif(n)(s).1; } + <==> { assert f(s) == UniformPowerOfTwoModel.ProbUnif(n)(s).1; } UniformPowerOfTwoModel.ProbUnif(n)(s).1 in e; - <==> { ProbUnifTailDecompose(n, s); } + <==> { ProbUnifTailDecompose(n, s); } Monad.Tail(UniformPowerOfTwoModel.ProbUnif(n / 2)(s).1) in e; - <==> + <==> UniformPowerOfTwoModel.ProbUnif(n / 2)(s).1 in e'; - <==> { assert UniformPowerOfTwoModel.ProbUnif(n / 2)(s).1 == g(s); } + <==> { assert UniformPowerOfTwoModel.ProbUnif(n / 2)(s).1 == g(s); } g(s) in e'; } } diff --git a/src/Distributions/UniformPowerOfTwo/Implementation.dfy b/src/Distributions/UniformPowerOfTwo/Implementation.dfy index 69f15771..a82f88a7 100644 --- a/src/Distributions/UniformPowerOfTwo/Implementation.dfy +++ b/src/Distributions/UniformPowerOfTwo/Implementation.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "Interface.dfy" include "Model.dfy" diff --git a/src/Distributions/UniformPowerOfTwo/Interface.dfy b/src/Distributions/UniformPowerOfTwo/Interface.dfy index 60635558..936196ae 100644 --- a/src/Distributions/UniformPowerOfTwo/Interface.dfy +++ b/src/Distributions/UniformPowerOfTwo/Interface.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../Base/Interface.dfy" include "Model.dfy" diff --git a/src/Distributions/UniformPowerOfTwo/Model.dfy b/src/Distributions/UniformPowerOfTwo/Model.dfy index 6a123240..6b68cb3f 100644 --- a/src/Distributions/UniformPowerOfTwo/Model.dfy +++ b/src/Distributions/UniformPowerOfTwo/Model.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../../ProbabilisticProgramming/RandomNumberGenerator.dfy" include "../../ProbabilisticProgramming/Monad.dfy" diff --git a/src/Math/Helper.dfy b/src/Math/Helper.dfy index affbff01..06619d35 100644 --- a/src/Math/Helper.dfy +++ b/src/Math/Helper.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ module Helper { /************ @@ -123,9 +123,9 @@ module Helper { { calc { a * c + b; - == + == a * c + (a * (b / a) + b % a); - == + == a * (c + b / a) + b % a; } DivModIsUnique(a * c + b, a, c + b / a, b % a); diff --git a/src/Math/MeasureTheory.dfy b/src/Math/MeasureTheory.dfy index 89f76d35..bd9c168b 100644 --- a/src/Math/MeasureTheory.dfy +++ b/src/Math/MeasureTheory.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ module MeasureTheory { /************ @@ -21,7 +21,7 @@ module MeasureTheory { iset n: nat | n >= i, x <- f(n) :: x } - ghost function CountableSum(f: nat -> real, i: nat := 0): real { + function CountableSum(f: nat -> real, i: nat := 0): real { assume {:axiom} false; f(i) + CountableSum(f, i+1) } @@ -71,7 +71,7 @@ module MeasureTheory { } // Definition 13 - ghost predicate AreIndepEvents(event_space: iset>, mu: iset -> real, e1: iset, e2: iset) { + predicate AreIndepEvents(event_space: iset>, mu: iset -> real, e1: iset, e2: iset) { && (e1 in event_space) && (e2 in event_space) && (mu(e1 * e2) == mu(e1) * mu(e2)) @@ -107,13 +107,13 @@ module MeasureTheory { } calc { CountableSum((n: nat) => mu(f(n))) - == + == mu(f(0)) + CountableSum((n: nat) => mu(f(n)), 1) - == + == mu(f(0)) + mu(f(1)) + CountableSum((n: nat) => mu(f(n)), 2) - == + == mu(e1) + mu(e2) + CountableSum((n: nat) => mu(f(n)), 2) - == + == mu(e1) + mu(e2); } } @@ -142,9 +142,9 @@ module MeasureTheory { assert CountableUnion(f) == e1 + e2 by { calc { CountableUnion(f); - == { CountableUnionSplit(f, 0); } + == { CountableUnionSplit(f, 0); } e1 + CountableUnion(f, 1); - == { CountableUnionSplit(f, 1); } + == { CountableUnionSplit(f, 1); } e1 + e2; } } diff --git a/src/ProbabilisticProgramming/Independence.dfy b/src/ProbabilisticProgramming/Independence.dfy index ccedfae5..9aa773d2 100644 --- a/src/ProbabilisticProgramming/Independence.dfy +++ b/src/ProbabilisticProgramming/Independence.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "RandomNumberGenerator.dfy" include "Monad.dfy" @@ -29,7 +29,7 @@ module Independence { } // Definition 35 - ghost predicate {:axiom} IsIndepFn(f: Monad.Hurd) + predicate {:axiom} IsIndepFn(f: Monad.Hurd) ensures IsIndepFunction(f) ensures MeasureTheory.IsMeasurable(RandomNumberGenerator.event_space, RandomNumberGenerator.event_space, s => f(s).1) diff --git a/src/ProbabilisticProgramming/Quantifier.dfy b/src/ProbabilisticProgramming/Quantifier.dfy index 4062b335..80aa5254 100644 --- a/src/ProbabilisticProgramming/Quantifier.dfy +++ b/src/ProbabilisticProgramming/Quantifier.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "RandomNumberGenerator.dfy" diff --git a/src/ProbabilisticProgramming/RandomNumberGenerator.dfy b/src/ProbabilisticProgramming/RandomNumberGenerator.dfy index a57a8eb1..4ab3b098 100644 --- a/src/ProbabilisticProgramming/RandomNumberGenerator.dfy +++ b/src/ProbabilisticProgramming/RandomNumberGenerator.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "../Math/MeasureTheory.dfy" diff --git a/src/ProbabilisticProgramming/WhileAndUntil.dfy b/src/ProbabilisticProgramming/WhileAndUntil.dfy index 2426e21e..167cb436 100644 --- a/src/ProbabilisticProgramming/WhileAndUntil.dfy +++ b/src/ProbabilisticProgramming/WhileAndUntil.dfy @@ -1,7 +1,7 @@ /******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ include "Monad.dfy" include "Quantifier.dfy" @@ -32,8 +32,8 @@ module WhileAndUntil { // Definition 39 / True iff mu(iset s | ProbWhile(c, b, a)(s) terminates) == 1 ghost predicate ProbWhileTerminates(b: A -> Monad.Hurd, c: A -> bool) { - var P := (a: A) => - (s: RandomNumberGenerator.RNG) => exists n :: !c(ProbWhileCut(c, b, n, a)(s).0); + var P := (a: A) => + (s: RandomNumberGenerator.RNG) => exists n :: !c(ProbWhileCut(c, b, n, a)(s).0); forall a :: Quantifier.ForAllStar(P(a)) } @@ -48,12 +48,12 @@ module WhileAndUntil { Monad.Return(a) } - method ProbWhileImperative(c: A -> bool, b: A -> Monad.Hurd, a: A, s: RandomNumberGenerator.RNG) returns (t: (A, RandomNumberGenerator.RNG)) + method ProbWhileImperative(c: A -> bool, b: A -> Monad.Hurd, a: A, s: RandomNumberGenerator.RNG) returns (t: (A, RandomNumberGenerator.RNG)) requires ProbWhileTerminates(b, c) ensures ProbWhile(c, b, a)(s) == t decreases * { - while c(a) + while c(a) decreases * { var (a, s) := b(a)(s); @@ -61,7 +61,7 @@ module WhileAndUntil { return (a, s); } - method ProbWhileImperativeAlternative(c: A -> bool, b: A -> Monad.Hurd, a: A, s: RandomNumberGenerator.RNG) returns (t: (A, RandomNumberGenerator.RNG)) + method ProbWhileImperativeAlternative(c: A -> bool, b: A -> Monad.Hurd, a: A, s: RandomNumberGenerator.RNG) returns (t: (A, RandomNumberGenerator.RNG)) requires ProbWhileTerminates(b, c) ensures ProbWhile(c, b, a)(s) == t decreases * @@ -86,7 +86,7 @@ module WhileAndUntil { // Definition 44 function ProbUntil(b: Monad.Hurd, c: A -> bool): (f: Monad.Hurd) requires ProbUntilTerminates(b, c) - ensures + ensures var c' := (a: A) => !c(a); var b' := (a: A) => b; forall s :: f(s) == ProbWhile(c', b', b(s).0)(b(s).1) diff --git a/tests/Tests.dfy b/tests/Tests.dfy index 5308cb96..18e25d42 100644 --- a/tests/Tests.dfy +++ b/tests/Tests.dfy @@ -3,9 +3,9 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ - include "../src/Dafny-VMC.dfy" +include "../src/Dafny-VMC.dfy" - module Tests { +module Tests { import BaseInterface import UniformInterface import GeometricInterface @@ -267,4 +267,4 @@ var varianceBound := 1.4 * 1.4; // variance of DiscreteGaussian(1.4) is < 1.4^2 testEmpiricalIsWithin4SigmaOfTrueMean(n, sum as real, 0.0, varianceBound, "mean"); } - } +} diff --git a/tests/TestsExternUniform.dfy b/tests/TestsExternUniform.dfy index 54bb2c41..8770f80a 100644 --- a/tests/TestsExternUniform.dfy +++ b/tests/TestsExternUniform.dfy @@ -3,8 +3,8 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ - include "../src/Dafny-VMC.dfy" - include "Tests.dfy" +include "../src/Dafny-VMC.dfy" +include "Tests.dfy" module TestsExternUniform { import DafnyVMC @@ -48,14 +48,14 @@ module TestsExternUniform { { var r := new DafnyVMC.DRandomExternUniform(); Tests.TestBernoulliRational2(1_000_000, r); - } + } method {:test} TestBernoulliRational3() decreases * { var r := new DafnyVMC.DRandomExternUniform(); Tests.TestBernoulliRational3(1_000_000, r); - } + } method {:test} TestBernoulli() decreases * diff --git a/tests/TestsFoundational.dfy b/tests/TestsFoundational.dfy index 5c09ffee..0c2cf3f6 100644 --- a/tests/TestsFoundational.dfy +++ b/tests/TestsFoundational.dfy @@ -3,8 +3,8 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ - include "../src/Dafny-VMC.dfy" - include "Tests.dfy" +include "../src/Dafny-VMC.dfy" +include "Tests.dfy" module TestsFoundational { import DafnyVMC @@ -48,14 +48,14 @@ module TestsFoundational { { var r := new DafnyVMC.DRandomFoundational(); Tests.TestBernoulliRational2(1_000_000, r); - } + } method {:test} TestBernoulliRational3() decreases * { var r := new DafnyVMC.DRandomFoundational(); Tests.TestBernoulliRational3(1_000_000, r); - } + } method {:test} TestBernoulli() decreases *