diff --git a/audit.log b/audit.log index 2a7e0f02..0b9a0965 100644 --- a/audit.log +++ b/audit.log @@ -1,7 +1,7 @@ src/Distributions/Coin/Interface.dfy(23,6): CoinSample: Definition has `assume {:axiom}` statement in body. -src/Distributions/Uniform/Correctness.dfy(154,17): SampleIsIndepFn: Declaration has explicit `{:axiom}` attribute. +src/Distributions/Uniform/Correctness.dfy(167,17): SampleIsIndepFn: Declaration has explicit `{:axiom}` attribute. src/Distributions/Uniform/Implementation.dfy(47,6): UniformSample: Definition has `assume {:axiom}` statement in body. -src/Distributions/Uniform/Model.dfy(30,17): SampleTerminates: Declaration has explicit `{:axiom}` attribute. +src/Distributions/Uniform/Model.dfy(41,17): SampleTerminates: Declaration has explicit `{:axiom}` attribute. src/Math/MeasureTheory.dfy(150,17): CountableSumOfZeroesIsZero: Declaration has explicit `{:axiom}` attribute. src/Math/MeasureTheory.dfy(25,4): CountableSum: Definition has `assume {:axiom}` statement in body. src/ProbabilisticProgramming/Independence.dfy(32,27): IsIndepFn: Declaration has explicit `{:axiom}` attribute. @@ -18,8 +18,8 @@ src/ProbabilisticProgramming/Monad.dfy(150,17): MeasureHeadDrop: Declaration has src/ProbabilisticProgramming/Monad.dfy(156,17): TailIsMeasurePreserving: Declaration has explicit `{:axiom}` attribute. src/ProbabilisticProgramming/RandomNumberGenerator.dfy(15,21): IsRNG: Declaration has explicit `{:axiom}` attribute. src/ProbabilisticProgramming/RandomNumberGenerator.dfy(29,17): RNGHasMeasure: Declaration has explicit `{:axiom}` attribute. -src/ProbabilisticProgramming/WhileAndUntil.dfy(159,17): EnsureProbWhileTerminates: Declaration has explicit `{:axiom}` attribute. -src/ProbabilisticProgramming/WhileAndUntil.dfy(165,17): ProbUntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute. -src/ProbabilisticProgramming/WhileAndUntil.dfy(178,17): ProbUntilAsBind: Declaration has explicit `{:axiom}` attribute. -src/ProbabilisticProgramming/WhileAndUntil.dfy(192,4): EnsureProbUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body. +src/ProbabilisticProgramming/WhileAndUntil.dfy(170,17): EnsureProbWhileTerminates: Declaration has explicit `{:axiom}` attribute. +src/ProbabilisticProgramming/WhileAndUntil.dfy(176,17): ProbUntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute. +src/ProbabilisticProgramming/WhileAndUntil.dfy(188,17): ProbUntilAsBind: Declaration has explicit `{:axiom}` attribute. +src/ProbabilisticProgramming/WhileAndUntil.dfy(202,4): EnsureProbUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body. src/ProbabilisticProgramming/WhileAndUntil.dfy(44,4): ProbWhile: Definition has `assume {:axiom}` statement in body. diff --git a/src/Distributions/Bernoulli/Correctness.dfy b/src/Distributions/Bernoulli/Correctness.dfy index 33b0c90e..aa0c806b 100644 --- a/src/Distributions/Bernoulli/Correctness.dfy +++ b/src/Distributions/Bernoulli/Correctness.dfy @@ -94,7 +94,7 @@ module Bernoulli.Correctness { assert A1: e1 in RandomNumberGenerator.event_space && RandomNumberGenerator.mu(e1) == 1.0 / (n as real) by { Uniform.Correctness.UniformFullCorrectness(n, m-1); - assert e1 == Uniform.Correctness.UniformFullCorrectnessHelper(n, m-1); + assert e1 == Uniform.Correctness.SampleEquals(n, m-1); } assert A2: e2 in RandomNumberGenerator.event_space && RandomNumberGenerator.mu(e2) == (m-1) as real / n as real by { diff --git a/src/Distributions/Uniform/Correctness.dfy b/src/Distributions/Uniform/Correctness.dfy index 49bd0a79..90e8f905 100644 --- a/src/Distributions/Uniform/Correctness.dfy +++ b/src/Distributions/Uniform/Correctness.dfy @@ -28,7 +28,7 @@ module Uniform.Correctness { Definitions ************/ - ghost function UniformFullCorrectnessHelper(n: nat, i: nat): iset + ghost function SampleEquals(n: nat, i: nat): iset requires 0 <= i < n { iset s | Model.Sample(n)(s).0 == i @@ -42,85 +42,42 @@ module Uniform.Correctness { // Equation (4.12) / PROB_BERN_UNIFORM lemma UniformFullCorrectness(n: nat, i: nat) requires 0 <= i < n - ensures UniformFullCorrectnessHelper(n, i) in RandomNumberGenerator.event_space - ensures RandomNumberGenerator.mu(UniformFullCorrectnessHelper(n, i)) == 1.0 / (n as real) + ensures SampleEquals(n, i) in RandomNumberGenerator.event_space + ensures RandomNumberGenerator.mu(SampleEquals(n, i)) == 1.0 / (n as real) { - var e := UniformFullCorrectnessHelper(n, i); - var p := (s: RandomNumberGenerator.RNG) => UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n; - var q := (s: RandomNumberGenerator.RNG) => UniformPowerOfTwo.Model.Sample(2 * n)(s).0 == i; - var e1 := iset s {:trigger UniformPowerOfTwo.Model.Sample(2 * n)(s).0} | UniformPowerOfTwo.Model.Sample(2 * n)(s).0 == i; - var e2 := iset s {:trigger UniformPowerOfTwo.Model.Sample(2 * n)(s).0} | UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n; - var b := UniformPowerOfTwo.Model.Sample(2 * n); - var c := (x: nat) => x < n; - var d := (x: nat) => x == i; - - assert Independence.IsIndepFn(b) && Quantifier.ExistsStar(WhileAndUntil.Helper2(b, c)) by { + var equalsI := (x: nat) => x == i; + + assert Independence.IsIndepFn(Model.Proposal(n)) && Quantifier.ExistsStar(WhileAndUntil.ProposalIsAccepted(Model.Proposal(n), Model.Accept(n))) by { Model.SampleTerminates(n); } - assert WhileAndUntil.ProbUntilTerminates(b, c) by { - WhileAndUntil.ProbUntilProbabilityFraction(b, c, d); - } + WhileAndUntil.ProbUntilProbabilityFraction(Model.Proposal(n), Model.Accept(n), equalsI); + var eventResultEqualsI := WhileAndUntil.UntilLoopResultHasProperty(Model.Proposal(n), Model.Accept(n), equalsI); + var eventProposalAcceptedAndEqualsI := WhileAndUntil.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), equalsI); + var proposalAccepted := WhileAndUntil.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n)); - var x := WhileAndUntil.ConstructEvents(b, c, d); - WhileAndUntil.ProbUntilProbabilityFraction(b, c, d); - assert Fraction: RandomNumberGenerator.mu(x.0) == RandomNumberGenerator.mu(x.1) / RandomNumberGenerator.mu(x.2); + assert Fraction: RandomNumberGenerator.mu(eventResultEqualsI) == RandomNumberGenerator.mu(eventProposalAcceptedAndEqualsI) / RandomNumberGenerator.mu(proposalAccepted); - assert X0: x.0 == e; - assert X1: x.1 == e1 by { - forall s ensures s in x.1 <==> s in e1 { - calc { - s in x.1; - d(b(s).0) && c(b(s).0); - (UniformPowerOfTwo.Model.Sample(2 * n)(s).0 == i); - s in e1; - } - } - } - assert X2: x.2 == e2 by { - forall s ensures s in x.2 <==> s in e2 { - calc { - s in x.2; - c(b(s).0); - UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n; - s in e2; - } + assert Eq: eventResultEqualsI == SampleEquals(n, i) by { + forall s ensures s in eventResultEqualsI <==> s in SampleEquals(n, i) { + assert s in eventResultEqualsI <==> s in SampleEquals(n, i); } } - assert Log2Double: Helper.Log2Floor(2 * n) == Helper.Log2Floor(n) + 1 by { Helper.Log2FloorDef(n); } - - assert UniformFullCorrectnessHelper(n, i) in RandomNumberGenerator.event_space by { - reveal X0; + assert SampleEquals(n, i) in RandomNumberGenerator.event_space by { + reveal Eq; } - assert RandomNumberGenerator.mu(e) == 1.0 / (n as real) by { - assert ProbE1: RandomNumberGenerator.mu(e1) == 1.0 / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real) by { - assert i < Helper.Power(2, Helper.Log2Floor(2 * n)) by { - calc { - i; - < - n; - < { Helper.Power2OfLog2Floor(n); } - Helper.Power(2, Helper.Log2Floor(n) + 1); - == { reveal Log2Double; } - Helper.Power(2, Helper.Log2Floor(2 * n)); - } - } - UniformPowerOfTwo.Correctness.UnifCorrectness2(2 * n, i); - } - assert ProbE2: RandomNumberGenerator.mu(e2) == (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real) by { - assert n < Helper.Power(2, Helper.Log2Floor(2 * n)) by { - Helper.Power2OfLog2Floor(n); - reveal Log2Double; - } - UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(2 * n, n); - } + assert RandomNumberGenerator.mu(SampleEquals(n, i)) == 1.0 / (n as real) by { calc { - RandomNumberGenerator.mu(e); - { reveal X0; reveal X1; reveal X2; reveal Fraction; } - RandomNumberGenerator.mu(e1) / RandomNumberGenerator.mu(e2); - { reveal ProbE1; reveal ProbE2; } + RandomNumberGenerator.mu(SampleEquals(n, i)); + { reveal Eq; } + RandomNumberGenerator.mu(eventResultEqualsI); + { reveal Fraction; } + RandomNumberGenerator.mu(eventProposalAcceptedAndEqualsI) / RandomNumberGenerator.mu(proposalAccepted); + { ProbabilityProposalAcceptedAndEqualsI(n, i); } + (1.0 / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real)) / RandomNumberGenerator.mu(proposalAccepted); + { ProbabilityProposalAccepted(n); } (1.0 / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real)) / ((n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real)); { Helper.SimplifyFractions(1.0, n as real, Helper.Power(2, Helper.Log2Floor(2 * n)) as real); } 1.0 / (n as real); @@ -128,6 +85,62 @@ module Uniform.Correctness { } } + lemma ProbabilityProposalAcceptedAndEqualsI(n: nat, i: nat) + requires 0 <= i < n + ensures + var e := WhileAndUntil.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i); + RandomNumberGenerator.mu(e) == 1.0 / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real) + { + var e := WhileAndUntil.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i); + assert i < Helper.Power(2, Helper.Log2Floor(2 * n)) by { + calc { + i; + < + n; + < { Helper.Power2OfLog2Floor(n); } + Helper.Power(2, Helper.Log2Floor(n) + 1); + == { Helper.Log2FloorDef(n); } + Helper.Power(2, Helper.Log2Floor(2 * n)); + } + } + assert e == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).0 == i) by { + forall s ensures s in e <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).0 == i {} + } + UniformPowerOfTwo.Correctness.UnifCorrectness2(2 * n, i); + } + + lemma ProbabilityProposalAccepted(n: nat) + requires n >= 1 + ensures + var e := WhileAndUntil.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n)); + RandomNumberGenerator.mu(e) == (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real) + { + var e := WhileAndUntil.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n)); + calc { + n; + < { Helper.Power2OfLog2Floor(n); } + Helper.Power(2, Helper.Log2Floor(n) + 1); + == { Helper.Log2FloorDef(n); } + Helper.Power(2, Helper.Log2Floor(2 * 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 { + s in e; + Model.Accept(n)(Model.Proposal(n)(s).0); + UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n; + } + } + } + calc { + RandomNumberGenerator.mu(e); + { reveal Equal; } + RandomNumberGenerator.mu(iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n); + { UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(2 * n, n); } + (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real); + } + } + // Correctness theorem for Model.IntervalSample lemma UniformFullIntervalCorrectness(a: int, b: int, i: int) requires a <= i < b @@ -139,7 +152,7 @@ module Uniform.Correctness { assert 0 <= i - a < b - a by { assert a <= i < b; } - var e' := UniformFullCorrectnessHelper(b - a, i - a); + var e' := SampleEquals(b - a, i - a); assert e' in RandomNumberGenerator.event_space by { UniformFullCorrectness(b - a, i - a); } assert RandomNumberGenerator.mu(e') == (1.0 / ((b-a) as real)) by { UniformFullCorrectness(b - a, i - a); } var e := iset s | Model.IntervalSample(a, b)(s).0 == i; diff --git a/src/Distributions/Uniform/Model.dfy b/src/Distributions/Uniform/Model.dfy index b6200831..20181acd 100644 --- a/src/Distributions/Uniform/Model.dfy +++ b/src/Distributions/Uniform/Model.dfy @@ -23,18 +23,27 @@ module Uniform.Model { requires n > 0 { SampleTerminates(n); - WhileAndUntil.ProbUntil(UniformPowerOfTwo.Model.Sample(2 * n), (x: nat) => x < n) + WhileAndUntil.ProbUntil(Proposal(n), Accept(n)) } + function Proposal(n: nat): Monad.Hurd + requires n > 0 + { + UniformPowerOfTwo.Model.Sample(2 * n) + } + + function Accept(n: nat): nat -> bool + requires n > 0 + { + (m: nat) => m < n + } lemma {:axiom} SampleTerminates(n: nat) requires n > 0 ensures - var b := UniformPowerOfTwo.Model.Sample(2 * n); - var c := (x: nat) => x < n; - && Independence.IsIndepFn(b) - && Quantifier.ExistsStar(WhileAndUntil.Helper2(b, c)) - && WhileAndUntil.ProbUntilTerminates(b, c) + && 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) requires a < b diff --git a/src/Distributions/UniformPowerOfTwo/Correctness.dfy b/src/Distributions/UniformPowerOfTwo/Correctness.dfy index 53dc8168..d78ac383 100644 --- a/src/Distributions/UniformPowerOfTwo/Correctness.dfy +++ b/src/Distributions/UniformPowerOfTwo/Correctness.dfy @@ -134,31 +134,31 @@ module UniformPowerOfTwo.Correctness { assert UnifIsCorrect(n, k, m); } else { var u := m / 2; - assert Recursive: RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m) == RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == m / 2) / 2.0 by { - SampleProbRecursiveHalf(n, m); + assert RecursiveCorrect: UnifIsCorrect(n / 2, k - 1, m / 2) by { + UnifCorrectness(n / 2, k - 1); } if m < Helper.Power(2, k) { - assert RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == u) == 1.0 / (Helper.Power(2, k - 1) as real) by { - assert u < Helper.Power(2, k - 1); - UnifCorrectness(n / 2, k - 1); - assert UnifIsCorrect(n / 2, k - 1, u); - } calc { RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); - == { reveal Recursive; } + == { SampleProbRecursiveHalf(n, m); } RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == u) / 2.0; - == + == { reveal RecursiveCorrect; } (1.0 / Helper.Power(2, k - 1) as real) / 2.0; == { Helper.PowerOfTwoLemma(k - 1); } 1.0 / (Helper.Power(2, k) as real); } assert UnifIsCorrect(n, k, m); } else { - assert u >= Helper.Power(2, k - 1); - reveal Recursive; - UnifCorrectness(n / 2, k - 1); - assert UnifIsCorrect(n / 2, k - 1, u); - assert RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m) == 0.0; + calc { + RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); + == { SampleProbRecursiveHalf(n, m); } + RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == u) / 2.0; + == { reveal RecursiveCorrect; } + 0.0 / 2.0; + == + 0.0; + } + assert UnifIsCorrect(n, k, m); } } } diff --git a/src/Math/Helper.dfy b/src/Math/Helper.dfy index 44b2da49..69370083 100644 --- a/src/Math/Helper.dfy +++ b/src/Math/Helper.dfy @@ -100,6 +100,18 @@ module Helper { ensures (x / z) + (y / z) == (x + y) / z {} + lemma DivSubstituteDividend(x: real, y: real, z: real) + requires y != 0.0 + requires x == z + ensures x / y == z / y + {} + + lemma DivSubstituteDivisor(x: real, y: real, z: real) + requires y != 0.0 + requires y == z + ensures x / y == x / z + {} + lemma DivDivToDivMul(x: real, y: real, z: real) requires y != 0.0 requires z != 0.0 diff --git a/src/ProbabilisticProgramming/WhileAndUntil.dfy b/src/ProbabilisticProgramming/WhileAndUntil.dfy index 167cb436..3cdd821e 100644 --- a/src/ProbabilisticProgramming/WhileAndUntil.dfy +++ b/src/ProbabilisticProgramming/WhileAndUntil.dfy @@ -15,180 +15,190 @@ module WhileAndUntil { import RandomNumberGenerator /************ - Definitions + Definitions ************/ // Definition 37 - function ProbWhileCut(c: A -> bool, b: A -> Monad.Hurd, n: nat, a: A): Monad.Hurd { + function ProbWhileCut(condition: A -> bool, body: A -> Monad.Hurd, n: nat, init: A): Monad.Hurd { if n == 0 then - Monad.Return(a) + Monad.Return(init) else ( - if c(a) then - Monad.Bind(b(a), (a': A) => ProbWhileCut(c, b, n-1, a')) + if condition(init) then + Monad.Bind(body(init), (a: A) => ProbWhileCut(condition, body, n-1, a)) else - Monad.Return(a) + Monad.Return(init) ) } - // 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); - forall a :: Quantifier.ForAllStar(P(a)) + // Definition 39 / True iff mu(iset s | ProbWhile(condition, body, a)(s) terminates) == 1 + ghost predicate ProbWhileTerminates(body: A -> Monad.Hurd, condition: A -> bool) { + 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(c: A -> bool, b: A -> Monad.Hurd, a: A): (f: Monad.Hurd) - requires ProbWhileTerminates(b, c) + function ProbWhile(condition: A -> bool, body: A -> Monad.Hurd, init: A): (f: Monad.Hurd) + requires ProbWhileTerminates(body, condition) { assume {:axiom} false; - if c(a) then - Monad.Bind(b(a), (a': A) => ProbWhile(c, b, a')) + if condition(init) then + Monad.Bind(body(init), (a': A) => ProbWhile(condition, body, a')) else - Monad.Return(a) + Monad.Return(init) } - 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 + method ProbWhileImperative(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: RandomNumberGenerator.RNG) returns (t: (A, RandomNumberGenerator.RNG)) + requires ProbWhileTerminates(body, condition) + ensures ProbWhile(condition, body, init)(s) == t decreases * { - while c(a) + while condition(init) decreases * { - var (a, s) := b(a)(s); + var (a, s) := body(init)(s); } - return (a, s); + return (init, s); } - 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 + method ProbWhileImperativeAlternative(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: RandomNumberGenerator.RNG) returns (t: (A, RandomNumberGenerator.RNG)) + requires ProbWhileTerminates(body, condition) + ensures ProbWhile(condition, body, init)(s) == t decreases * { while true decreases * { - if !c(a) { - return (a, s); + if !condition(init) { + return (init, s); } else { - var (a, s) := b(a)(s); + var (a, s) := body(init)(s); } } } - ghost predicate ProbUntilTerminates(b: Monad.Hurd, c: A -> bool) { - var c' := (a: A) => !c(a); - var b' := (a: A) => b; - ProbWhileTerminates(b', c') + ghost predicate ProbUntilTerminates(proposal: Monad.Hurd, accept: A -> bool) { + var reject := (a: A) => !accept(a); + var body := (a: A) => proposal; + ProbWhileTerminates(body, reject) } // Definition 44 - function ProbUntil(b: Monad.Hurd, c: A -> bool): (f: Monad.Hurd) - requires ProbUntilTerminates(b, c) + function ProbUntil(proposal: Monad.Hurd, accept: A -> bool): (f: Monad.Hurd) + requires ProbUntilTerminates(proposal, accept) 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) + var reject := (a: A) => !accept(a); + var body := (a: A) => proposal; + forall s :: f(s) == ProbWhile(reject, body, proposal(s).0)(proposal(s).1) { - var c' := (a: A) => !c(a); - var b' := (a: A) => b; - Monad.Bind(b, (a: A) => ProbWhile(c', b', a)) + var reject := (a: A) => !accept(a); + var body := (a: A) => proposal; + Monad.Bind(proposal, (a: A) => ProbWhile(reject, body, a)) } - method ProbUntilImperative(b: Monad.Hurd, c: A -> bool, s: RandomNumberGenerator.RNG) returns (t: (A, RandomNumberGenerator.RNG)) - requires ProbUntilTerminates(b, c) - ensures t == ProbUntil(b, c)(s) + method ProbUntilImperative(proposal: Monad.Hurd, accept: A -> bool, s: RandomNumberGenerator.RNG) returns (t: (A, RandomNumberGenerator.RNG)) + requires ProbUntilTerminates(proposal, accept) + ensures t == ProbUntil(proposal, accept)(s) decreases * { - var c' := (a: A) => !c(a); - var b' := (a: A) => b; - t := ProbWhileImperative(c', b', b(s).0, b(s).1); + var reject := (a: A) => !accept(a); + var body := (a: A) => proposal; + t := ProbWhileImperative(reject, body, proposal(s).0, proposal(s).1); } - function Helper(b: A -> Monad.Hurd, c: A -> bool, a: A): (RandomNumberGenerator.RNG -> bool) { + function WhileLoopExitsAfterOneIteration(body: A -> Monad.Hurd, condition: A -> bool, init: A): (RandomNumberGenerator.RNG -> bool) { (s: RandomNumberGenerator.RNG) => - !c(b(a)(s).0) + !condition(body(init)(s).0) } - function Helper2(b: Monad.Hurd, c: A -> bool): (RandomNumberGenerator.RNG -> bool) { + function ProposalIsAccepted(proposal: Monad.Hurd, accept: A -> bool): (RandomNumberGenerator.RNG -> bool) { (s: RandomNumberGenerator.RNG) => - c(b(s).0) + accept(proposal(s).0) } - function Helper3(b: Monad.Hurd, c: A -> bool): (RandomNumberGenerator.RNG -> bool) - requires ProbUntilTerminates(b, c) + function UntilLoopResultIsAccepted(proposal: Monad.Hurd, accept: A -> bool): (RandomNumberGenerator.RNG -> bool) + requires ProbUntilTerminates(proposal, accept) { (s: RandomNumberGenerator.RNG) => - c(ProbUntil(b, c)(s).0) + accept(ProbUntil(proposal, accept)(s).0) } - ghost function ConstructEvents(b: Monad.Hurd, c: A -> bool, d: A -> bool): (x: (iset, iset, iset)) - requires ProbUntilTerminates(b, c) + ghost function UntilLoopResultHasProperty(proposal: Monad.Hurd, accept: A -> bool, property: A -> bool): iset + requires ProbUntilTerminates(proposal, accept) { - (iset s | d(ProbUntil(b, c)(s).0), iset s | d(b(s).0) && c(b(s).0), iset s | c(b(s).0)) + iset s | property(ProbUntil(proposal, accept)(s).0) } + ghost function ProposalIsAcceptedAndHasProperty(proposal: Monad.Hurd, accept: A -> bool, property: A -> bool): iset + { + iset s | property(proposal(s).0) && accept(proposal(s).0) + } + + ghost function ProposalAcceptedEvent(proposal: Monad.Hurd, accept: A -> bool): iset + { + iset s | accept(proposal(s).0) + } + + /******* - Lemmas + Lemmas *******/ - lemma EnsureProbUntilTerminates(b: Monad.Hurd, c: A -> bool) - requires Independence.IsIndepFn(b) - requires Quantifier.ExistsStar((s: RandomNumberGenerator.RNG) => c(b(s).0)) - ensures ProbUntilTerminates(b, c) + lemma EnsureProbUntilTerminates(proposal: Monad.Hurd, accept: A -> bool) + requires Independence.IsIndepFn(proposal) + requires Quantifier.ExistsStar((s: RandomNumberGenerator.RNG) => accept(proposal(s).0)) + ensures ProbUntilTerminates(proposal, accept) { - var c' := (a: A) => !c(a); - var b' := (a: A) => b; - var p := (s: RandomNumberGenerator.RNG) => c(b(s).0); - assert ProbUntilTerminates(b, c) by { - forall a: A ensures Independence.IsIndepFn(b'(a)) { - assert b'(a) == b; + var reject := (a: A) => !accept(a); + var body := (a: A) => proposal; + var proposalIsAccepted := (s: RandomNumberGenerator.RNG) => accept(proposal(s).0); + assert ProbUntilTerminates(proposal, accept) by { + forall a: A ensures Independence.IsIndepFn(body(a)) { + assert body(a) == proposal; } - forall a: A ensures Quantifier.ExistsStar(Helper(b', c', a)) { - assert Quantifier.ExistsStar(p); - assert (iset s | p(s)) == (iset s | Helper(b', c', a)(s)); + forall a: A ensures Quantifier.ExistsStar(WhileLoopExitsAfterOneIteration(body, reject, a)) { + assert Quantifier.ExistsStar(proposalIsAccepted); + assert (iset s | proposalIsAccepted(s)) == (iset s | WhileLoopExitsAfterOneIteration(body, reject, a)(s)); } - assert ProbWhileTerminates(b', c') by { - EnsureProbWhileTerminates(b', c'); + assert ProbWhileTerminates(body, reject) by { + EnsureProbWhileTerminates(body, reject); } } } // (Equation 3.30) / Sufficient conditions for while-loop termination - lemma {:axiom} EnsureProbWhileTerminates(b: A -> Monad.Hurd, c: A -> bool) - requires forall a :: Independence.IsIndepFn(b(a)) - requires forall a :: Quantifier.ExistsStar(Helper(b, c, a)) - ensures ProbWhileTerminates(b, c) + lemma {:axiom} EnsureProbWhileTerminates(body: A -> Monad.Hurd, condition: A -> bool) + requires forall a :: Independence.IsIndepFn(body(a)) + requires forall a :: Quantifier.ExistsStar(WhileLoopExitsAfterOneIteration(body, condition, a)) + ensures ProbWhileTerminates(body, condition) // Theorem 45 (wrong!) / PROB_BERN_UNTIL (correct!) - lemma {:axiom} ProbUntilProbabilityFraction(b: Monad.Hurd, c: A -> bool, d: A -> bool) - requires Independence.IsIndepFn(b) - requires Quantifier.ExistsStar(Helper2(b, c)) - ensures ProbUntilTerminates(b, c) + lemma {:axiom} ProbUntilProbabilityFraction(proposal: Monad.Hurd, accept: A -> bool, d: A -> bool) + requires Independence.IsIndepFn(proposal) + requires Quantifier.ExistsStar(ProposalIsAccepted(proposal, accept)) + ensures ProbUntilTerminates(proposal, accept) ensures - var x := ConstructEvents(b, c, d); - && x.0 in RandomNumberGenerator.event_space - && x.1 in RandomNumberGenerator.event_space - && x.2 in RandomNumberGenerator.event_space - && RandomNumberGenerator.mu(x.2) != 0.0 - && RandomNumberGenerator.mu(x.0) == RandomNumberGenerator.mu(x.1) / RandomNumberGenerator.mu(x.2) + && UntilLoopResultHasProperty(proposal, accept, d) in RandomNumberGenerator.event_space + && ProposalIsAcceptedAndHasProperty(proposal, accept, d) in RandomNumberGenerator.event_space + && ProposalAcceptedEvent(proposal, accept) in RandomNumberGenerator.event_space + && RandomNumberGenerator.mu(ProposalAcceptedEvent(proposal, accept)) != 0.0 + && RandomNumberGenerator.mu(UntilLoopResultHasProperty(proposal, accept, d)) == RandomNumberGenerator.mu(ProposalIsAcceptedAndHasProperty(proposal, accept, d)) / RandomNumberGenerator.mu(ProposalAcceptedEvent(proposal, accept)) // Equation (3.39) - lemma {:axiom} ProbUntilAsBind(b: Monad.Hurd, c: A -> bool, s: RandomNumberGenerator.RNG) - requires Independence.IsIndepFn(b) - requires Quantifier.ExistsStar(Helper2(b, c)) - ensures ProbUntilTerminates(b, c) - ensures ProbUntil(b, c) == Monad.Bind(b, (x: A) => if c(x) then Monad.Return(x) else ProbUntil(b, c)) + lemma {:axiom} ProbUntilAsBind(proposal: Monad.Hurd, accept: A -> bool, s: RandomNumberGenerator.RNG) + requires Independence.IsIndepFn(proposal) + requires Quantifier.ExistsStar(ProposalIsAccepted(proposal, accept)) + ensures ProbUntilTerminates(proposal, accept) + ensures ProbUntil(proposal, accept) == Monad.Bind(proposal, (x: A) => if accept(x) then Monad.Return(x) else ProbUntil(proposal, accept)) // Equation (3.40) - lemma EnsureProbUntilTerminatesAndForAll(b: Monad.Hurd, c: A -> bool) - requires Independence.IsIndepFn(b) - requires Quantifier.ExistsStar(Helper2(b, c)) - ensures ProbUntilTerminates(b, c) - ensures Quantifier.ForAllStar(Helper3(b, c)) + lemma EnsureProbUntilTerminatesAndForAll(proposal: Monad.Hurd, accept: A -> bool) + requires Independence.IsIndepFn(proposal) + requires Quantifier.ExistsStar(ProposalIsAccepted(proposal, accept)) + ensures ProbUntilTerminates(proposal, accept) + ensures Quantifier.ForAllStar(UntilLoopResultIsAccepted(proposal, accept)) { - EnsureProbUntilTerminates(b, c); - assume {:axiom} Quantifier.ForAllStar(Helper3(b, c)); + EnsureProbUntilTerminates(proposal, accept); + assume {:axiom} Quantifier.ForAllStar(UntilLoopResultIsAccepted(proposal, accept)); } -} \ No newline at end of file +}