Skip to content

Commit

Permalink
Prove remaining {:axiom}s in Uniform
Browse files Browse the repository at this point in the history
  • Loading branch information
@fzaiser
fzaiser committed Oct 6, 2023
1 parent 580885a commit 1769c5e
Show file tree
Hide file tree
Showing 5 changed files with 107 additions and 33 deletions.
3 changes: 1 addition & 2 deletions audit.log
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,7 @@ src/Distributions/BernoulliExpNeg/Implementation.dfy(52,6): BernoulliExpNegSampl
src/Distributions/BernoulliExpNeg/Model.dfy(30,4): GammaReductionLoop: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Model.dfy(60,4): GammaLe1Loop: Definition has `assume {:axiom}` statement in body.
src/Distributions/Coin/Interface.dfy(20,6): CoinSample: Definition has `assume {:axiom}` statement in body.
src/Distributions/Uniform/Correctness.dfy(165,17): SampleIsIndepFn: Declaration has explicit `{:axiom}` attribute.
src/Distributions/Uniform/Implementation.dfy(43,6): UniformSample: Definition has `assume {:axiom}` statement in body.
src/Distributions/Uniform/Model.dfy(34,17): SampleTerminates: Declaration has explicit `{:axiom}` attribute.
src/Math/Exponential.dfy(11,17): EvalOne: Declaration has explicit `{:axiom}` attribute.
src/Math/Exponential.dfy(2,26): Exp: Declaration has explicit `{:axiom}` attribute.
src/Math/Exponential.dfy(4,17): FunctionalEquation: Declaration has explicit `{:axiom}` attribute.
Expand All @@ -32,4 +30,5 @@ src/ProbabilisticProgramming/WhileAndUntil.dfy(165,17): EnsureProbWhileTerminate
src/ProbabilisticProgramming/WhileAndUntil.dfy(171,17): ProbUntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute.
src/ProbabilisticProgramming/WhileAndUntil.dfy(183,17): ProbUntilAsBind: Declaration has explicit `{:axiom}` attribute.
src/ProbabilisticProgramming/WhileAndUntil.dfy(197,4): EnsureProbUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body.
src/ProbabilisticProgramming/WhileAndUntil.dfy(207,8): ProbWhileIsIndepFn: Definition has `assume {:axiom}` statement in body.
src/ProbabilisticProgramming/WhileAndUntil.dfy(39,4): ProbWhile: Definition has `assume {:axiom}` statement in body.
26 changes: 11 additions & 15 deletions src/Distributions/Uniform/Correctness.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -99,26 +99,13 @@ module Uniform.Correctness {
UniformPowerOfTwo.Correctness.UnifCorrectness2(2 * n, i);
}

lemma Power2Log2Helper(n: nat)
requires n >= 1
ensures n < Helper.Power(2, Helper.Log2Floor(2 * n))
{
calc {
n;
< { Helper.Power2OfLog2Floor(n); }
Helper.Power(2, Helper.Log2Floor(n) + 1);
== { Helper.Log2FloorDef(n); }
Helper.Power(2, Helper.Log2Floor(2 * n));
}
}

lemma ProbabilityProposalAccepted(n: nat)
requires n >= 1
ensures
RandomNumberGenerator.mu(WhileAndUntil.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real)
{
var e := WhileAndUntil.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n));
assert n < Helper.Power(2, Helper.Log2Floor(2 * n)) by { Power2Log2Helper(n); }
assert n < Helper.Power(2, Helper.Log2Floor(2 * n)) by { Helper.NLtPower2Log2FloorOf2N(n); }
assert Equal: e == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n) by {
forall s ensures s in e <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n {
calc {
Expand Down Expand Up @@ -162,7 +149,16 @@ module Uniform.Correctness {
}

// Equation (4.10)
lemma {:axiom} SampleIsIndepFn(n: nat)
lemma SampleIsIndepFn(n: nat)
requires n > 0
ensures Independence.IsIndepFn(Model.Sample(n))
{
assert Independence.IsIndepFn(Model.Proposal(n)) by {
UniformPowerOfTwo.Correctness.SampleIsIndepFn(2 * n);
}
assert WhileAndUntil.ProbUntilTerminates(Model.Proposal(n), Model.Accept(n)) by {
Model.SampleTerminates(n);
}
WhileAndUntil.ProbUntilIsIndepFn(Model.Proposal(n), Model.Accept(n));
}
}
51 changes: 44 additions & 7 deletions src/Distributions/Uniform/Model.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@
*******************************************************************************/

module Uniform.Model {
import MeasureTheory
import Helper
import RandomNumberGenerator
import Quantifier
import Monad
Expand Down Expand Up @@ -31,18 +33,53 @@ module Uniform.Model {
(m: nat) => m < n
}

lemma {:axiom} SampleTerminates(n: nat)
requires n > 0
ensures
&& Independence.IsIndepFn(Proposal(n))
&& Quantifier.ExistsStar(WhileAndUntil.ProposalIsAccepted(Proposal(n), Accept(n)))
&& WhileAndUntil.ProbUntilTerminates(Proposal(n), Accept(n))

function IntervalSample(a: int, b: int): (f: Monad.Hurd<int>)
requires a < b
{
(s: RandomNumberGenerator.RNG) =>
var (x, s') := Sample(b - a)(s);
(a + x, s')
}

lemma SampleTerminates(n: nat)
requires n > 0
ensures
&& Independence.IsIndepFn(Proposal(n))
&& Quantifier.ExistsStar(WhileAndUntil.ProposalIsAccepted(Proposal(n), Accept(n)))
&& WhileAndUntil.ProbUntilTerminates(Proposal(n), Accept(n))
{
assert Independence.IsIndepFn(Proposal(n)) by {
UniformPowerOfTwo.Correctness.SampleIsIndepFn(2 * n);
}
var e := iset s | WhileAndUntil.ProposalIsAccepted(Proposal(n), Accept(n))(s);
assert e in RandomNumberGenerator.event_space by {
assert e == MeasureTheory.PreImage(s => UniformPowerOfTwo.Model.Sample(2 * n)(s).0, (iset m: nat | m < n));
assert MeasureTheory.PreImage(s => UniformPowerOfTwo.Model.Sample(2 * n)(s).0, (iset m: nat | m < n)) in RandomNumberGenerator.event_space by {
assert Independence.IsIndepFn(UniformPowerOfTwo.Model.Sample(2 * n)) by {
UniformPowerOfTwo.Correctness.SampleIsIndepFn(2 * n);
}
assert MeasureTheory.IsMeasurable(RandomNumberGenerator.event_space, MeasureTheory.natEventSpace, s => UniformPowerOfTwo.Model.Sample(2 * n)(s).0) by {
Independence.IsIndepFnImpliesFstMeasurableNat(UniformPowerOfTwo.Model.Sample(2 * n));
}
}
}
assert Quantifier.ExistsStar(WhileAndUntil.ProposalIsAccepted(Proposal(n), Accept(n))) by {
assert RandomNumberGenerator.mu(e) > 0.0 by {
assert e == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n);
assert n <= Helper.Power(2, Helper.Log2Floor(2 * n)) by {
Helper.NLtPower2Log2FloorOf2N(n);
}
calc {
RandomNumberGenerator.mu(e);
== { UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(2 * n, n); }
n as real / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real);
>
0.0;
}
}
}
assert WhileAndUntil.ProbUntilTerminates(Proposal(n), Accept(n)) by {
WhileAndUntil.EnsureProbUntilTerminates(Proposal(n), Accept(n));
}
}
}
13 changes: 13 additions & 0 deletions src/Math/Helper.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,6 +104,19 @@ module Helper {
ensures Power(2, Log2Floor(n)) <= n < Power(2, Log2Floor(n) + 1)
{}

lemma NLtPower2Log2FloorOf2N(n: nat)
requires n >= 1
ensures n < Power(2, Log2Floor(2 * n))
{
calc {
n;
< { Power2OfLog2Floor(n); }
Power(2, Log2Floor(n) + 1);
== { Log2FloorDef(n); }
Power(2, Log2Floor(2 * n));
}
}

lemma AdditionOfFractions(x: real, y: real, z: real)
requires z != 0.0
ensures (x / z) + (y / z) == (x + y) / z
Expand Down
47 changes: 38 additions & 9 deletions src/ProbabilisticProgramming/WhileAndUntil.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,15 +26,15 @@ module WhileAndUntil {
}

// Definition 39 / True iff mu(iset s | ProbWhile(condition, body, a)(s) terminates) == 1
ghost predicate ProbWhileTerminates<A(!new)>(body: A -> Monad.Hurd<A>, condition: A -> bool) {
ghost predicate ProbWhileTerminates<A(!new)>(condition: A -> bool, body: A -> Monad.Hurd<A>) {
var p := (a: A) =>
(s: RandomNumberGenerator.RNG) => exists n :: !condition(ProbWhileCut(condition, body, n, a)(s).0);
forall a :: Quantifier.ForAllStar(p(a))
}

// Theorem 38
function ProbWhile<A>(condition: A -> bool, body: A -> Monad.Hurd<A>, init: A): (f: Monad.Hurd<A>)
requires ProbWhileTerminates(body, condition)
requires ProbWhileTerminates(condition, body)
{
assume {:axiom} false;
if condition(init) then
Expand All @@ -44,7 +44,7 @@ module WhileAndUntil {
}

method ProbWhileImperative<A>(condition: A -> bool, body: A -> Monad.Hurd<A>, init: A, s: RandomNumberGenerator.RNG) returns (t: (A, RandomNumberGenerator.RNG))
requires ProbWhileTerminates(body, condition)
requires ProbWhileTerminates(condition, body)
ensures ProbWhile(condition, body, init)(s) == t
decreases *
{
Expand All @@ -57,7 +57,7 @@ module WhileAndUntil {
}

method ProbWhileImperativeAlternative<A>(condition: A -> bool, body: A -> Monad.Hurd<A>, init: A, s: RandomNumberGenerator.RNG) returns (t: (A, RandomNumberGenerator.RNG))
requires ProbWhileTerminates(body, condition)
requires ProbWhileTerminates(condition, body)
ensures ProbWhile(condition, body, init)(s) == t
decreases *
{
Expand All @@ -75,7 +75,7 @@ module WhileAndUntil {
ghost predicate ProbUntilTerminates<A(!new)>(proposal: Monad.Hurd<A>, accept: A -> bool) {
var reject := (a: A) => !accept(a);
var body := (a: A) => proposal;
ProbWhileTerminates(body, reject)
ProbWhileTerminates(reject, body)
}

// Definition 44
Expand Down Expand Up @@ -155,17 +155,17 @@ module WhileAndUntil {
assert Quantifier.ExistsStar(proposalIsAccepted);
assert (iset s | proposalIsAccepted(s)) == (iset s | WhileLoopExitsAfterOneIteration(body, reject, a)(s));
}
assert ProbWhileTerminates(body, reject) by {
EnsureProbWhileTerminates(body, reject);
assert ProbWhileTerminates(reject, body) by {
EnsureProbWhileTerminates(reject, body);
}
}
}

// (Equation 3.30) / Sufficient conditions for while-loop termination
lemma {:axiom} EnsureProbWhileTerminates<A(!new)>(body: A -> Monad.Hurd<A>, condition: A -> bool)
lemma {:axiom} EnsureProbWhileTerminates<A(!new)>(condition: A -> bool, body: A -> Monad.Hurd<A>)
requires forall a :: Independence.IsIndepFn(body(a))
requires forall a :: Quantifier.ExistsStar(WhileLoopExitsAfterOneIteration(body, condition, a))
ensures ProbWhileTerminates(body, condition)
ensures ProbWhileTerminates(condition, body)

// Theorem 45 (wrong!) / PROB_BERN_UNTIL (correct!)
lemma {:axiom} ProbUntilProbabilityFraction<A>(proposal: Monad.Hurd<A>, accept: A -> bool, d: A -> bool)
Expand Down Expand Up @@ -196,4 +196,33 @@ module WhileAndUntil {
EnsureProbUntilTerminates(proposal, accept);
assume {:axiom} Quantifier.ForAllStar(UntilLoopResultIsAccepted(proposal, accept));
}

lemma ProbWhileIsIndepFn<A(!new)>(condition: A -> bool, body: A -> Monad.Hurd<A>, init: A)
requires forall a: A :: Independence.IsIndepFn(body(a))
requires ProbWhileTerminates(condition, body)
ensures Independence.IsIndepFn(ProbWhile(condition, body, init))
{
if condition(init) {
forall a ensures Independence.IsIndepFn(ProbWhile(condition, body, a)) {
assume {:axiom} false; // assume termination
ProbWhileIsIndepFn(condition, body, a);
}
Independence.IndepFnIsCompositional(body(init), a => ProbWhile(condition, body, a));
} else {
Independence.ReturnIsIndepFn(init);
}
}

lemma ProbUntilIsIndepFn<A(!new)>(proposal: Monad.Hurd<A>, accept: A -> bool)
requires Independence.IsIndepFn(proposal)
requires ProbUntilTerminates(proposal, accept)
ensures Independence.IsIndepFn(ProbUntil(proposal, accept))
{
var reject := (a: A) => !accept(a);
var body := (a: A) => proposal;
forall init: A {
ProbWhileIsIndepFn(reject, body, init);
}
Independence.IndepFnIsCompositional(proposal, (init: A) => ProbWhile(reject, body, init));
}
}

0 comments on commit 1769c5e

Please sign in to comment.