From dede21031777672e6bf54cd455131ebb5a470729 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Wed, 4 Oct 2023 17:26:35 -0400 Subject: [PATCH 1/9] Simplify the definitions and fix proofs --- src/Distributions/Uniform/Correctness.dfy | 78 +++++-------- src/Distributions/Uniform/Implementation.dfy | 11 +- src/Distributions/Uniform/Model.dfy | 4 +- .../UniformPowerOfTwo/Correctness.dfy | 94 ++++++++-------- .../UniformPowerOfTwo/Implementation.dfy | 4 +- .../UniformPowerOfTwo/Interface.dfy | 2 + src/Distributions/UniformPowerOfTwo/Model.dfy | 104 ++++++++++-------- 7 files changed, 145 insertions(+), 152 deletions(-) diff --git a/src/Distributions/Uniform/Correctness.dfy b/src/Distributions/Uniform/Correctness.dfy index 0870ef5c..2549125c 100644 --- a/src/Distributions/Uniform/Correctness.dfy +++ b/src/Distributions/Uniform/Correctness.dfy @@ -40,7 +40,7 @@ module UniformCorrectness { // Correctness theorem for Model.Sample // Equation (4.12) / PROB_BERN_UNIFORM - lemma UniformFullCorrectness(n: nat, i: nat) + lemma {:vcs_split_on_every_assert} UniformFullCorrectness(n: nat, i: nat) requires 0 <= i < n ensures var e := UniformFullCorrectnessHelper(n, i); @@ -48,11 +48,11 @@ module UniformCorrectness { && RandomNumberGenerator.mu(e) == 1.0 / (n as real) { var e := UniformFullCorrectnessHelper(n, i); - var p := (s: RandomNumberGenerator.RNG) => UniformPowerOfTwo.Model.Sample(n-1)(s).0 < n; - var q := (s: RandomNumberGenerator.RNG) => UniformPowerOfTwo.Model.Sample(n-1)(s).0 == i; - var e1 := iset s {:trigger UniformPowerOfTwo.Model.Sample(n-1)(s).0} | UniformPowerOfTwo.Model.Sample(n-1)(s).0 == i; - var e2 := iset s {:trigger UniformPowerOfTwo.Model.Sample(n-1)(s).0} | UniformPowerOfTwo.Model.Sample(n-1)(s).0 < n; - var b := UniformPowerOfTwo.Model.Sample(n-1); + 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; @@ -70,59 +70,31 @@ module UniformCorrectness { assert x.0 == e; assert x.1 == e1 by { - assert forall s :: d(b(s).0) && c(b(s).0) <==> (UniformPowerOfTwo.Model.Sample(n-1)(s).0 == i); + assert forall s :: d(b(s).0) && c(b(s).0) <==> (UniformPowerOfTwo.Model.Sample(2 * n)(s).0 == i); } assert x.2 == e2 by { - assert forall s :: c(b(s).0) <==> UniformPowerOfTwo.Model.Sample(n-1)(s).0 < n; + assert forall s :: c(b(s).0) <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n; } assert RandomNumberGenerator.mu(e) == 1.0 / (n as real) by { - assert n >= 1; - if n == 1 { - assert RandomNumberGenerator.mu(e1) == 1.0 by { - assert e1 == iset s | true; - RandomNumberGenerator.RNGHasMeasure(); - } - - assert RandomNumberGenerator.mu(e2) == (n as real) by { - Helper.Log2LowerSuc(n-1); - UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(n-1, n); - assert Helper.Power(2, Helper.Log2(n-1)) == 1; - } - - calc { - RandomNumberGenerator.mu(e); - RandomNumberGenerator.mu(e1) / RandomNumberGenerator.mu(e2); - 1.0 / (n as real); - } - } else { - assert RandomNumberGenerator.mu(e1) == 1.0 / (Helper.Power(2, Helper.Log2(n-1)) as real) by { - calc { - i; - < { assert i < n; } - n; - <= { Helper.Log2LowerSuc(n-1); } - Helper.Power(2, Helper.Log2(n-1)); - } - assert RandomNumberGenerator.mu(e1) == if i < Helper.Power(2, Helper.Log2(n-1)) then 1.0 / (Helper.Power(2, Helper.Log2(n-1)) as real) else 0.0 by { - UniformPowerOfTwo.Correctness.UnifCorrectness2(n-1, i); - } - } - assert RandomNumberGenerator.mu(e2) == (n as real) / (Helper.Power(2, Helper.Log2(n-1)) as real) by { - assert n <= Helper.Power(2, Helper.Log2(n-1)) by { - Helper.Log2LowerSuc(n-1); - } - UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(n-1, n); - } - calc { - RandomNumberGenerator.mu(e); - { assert e == x.0; assert e1 == x.1; assert e2 == x.2; assert RandomNumberGenerator.mu(x.0) == RandomNumberGenerator.mu(x.1) / RandomNumberGenerator.mu(x.2); } - RandomNumberGenerator.mu(e1) / RandomNumberGenerator.mu(e2); - { assert RandomNumberGenerator.mu(e1) == 1.0 / (Helper.Power(2, Helper.Log2(n-1)) as real); assert RandomNumberGenerator.mu(e2) == (n as real) / (Helper.Power(2, Helper.Log2(n-1)) as real); } - (1.0 / (Helper.Power(2, Helper.Log2(n-1)) as real)) / ((n as real) / (Helper.Power(2, Helper.Log2(n-1)) as real)); - { Helper.SimplifyFractions(1.0, n as real, Helper.Power(2, Helper.Log2(n-1)) as real); } - 1.0 / (n as real); + assert RandomNumberGenerator.mu(e1) == 1.0 / (Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) as real) by { + assert i < Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) by { + UniformPowerOfTwo.Model.Power2OfLog2Floor(n); } + UniformPowerOfTwo.Correctness.UnifCorrectness2(2 * n, i); + } + assert RandomNumberGenerator.mu(e2) == (n as real) / (Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) as real) by { + assert n < Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) by { UniformPowerOfTwo.Model.Power2OfLog2Floor(n); } + UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(2 * n, n); + } + calc { + RandomNumberGenerator.mu(e); + { assert e == x.0; assert e1 == x.1; assert e2 == x.2; assert RandomNumberGenerator.mu(x.0) == RandomNumberGenerator.mu(x.1) / RandomNumberGenerator.mu(x.2); } + RandomNumberGenerator.mu(e1) / RandomNumberGenerator.mu(e2); + { assert RandomNumberGenerator.mu(e1) == 1.0 / (Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) as real); assert RandomNumberGenerator.mu(e2) == (n as real) / (Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) as real); } + (1.0 / (Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) as real)) / ((n as real) / (Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) as real)); + { Helper.SimplifyFractions(1.0, n as real, Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) as real); } + 1.0 / (n as real); } } } diff --git a/src/Distributions/Uniform/Implementation.dfy b/src/Distributions/Uniform/Implementation.dfy index 49cb35b1..a19dd0d6 100644 --- a/src/Distributions/Uniform/Implementation.dfy +++ b/src/Distributions/Uniform/Implementation.dfy @@ -20,14 +20,15 @@ module UniformImplementation { ensures u < n ensures Model.Sample(n)(old(s)) == (u, s) { - assume {:axiom} false; - u := UniformPowerOfTwoSample(n-1); + ghost var prev_s := s; + u := UniformPowerOfTwoSample(2 * n); while u >= n decreases * - invariant Model.Sample(n)(old(s)) == UniformPowerOfTwo.Model.Sample(n-1)(old(s)) - invariant (u, s) == UniformPowerOfTwo.Model.Sample(n-1)(old(s)) + invariant Model.Sample(n)(old(s)) == Model.Sample(n)(prev_s) + invariant (u, s) == UniformPowerOfTwo.Model.Sample(2 * n)(prev_s) { - u := UniformPowerOfTwoSample(n-1); + prev_s := s; + u := UniformPowerOfTwoSample(2 * n); } } } diff --git a/src/Distributions/Uniform/Model.dfy b/src/Distributions/Uniform/Model.dfy index be1c8937..dfb8e884 100644 --- a/src/Distributions/Uniform/Model.dfy +++ b/src/Distributions/Uniform/Model.dfy @@ -23,14 +23,14 @@ module UniformModel { requires n > 0 { SampleTerminates(n); - WhileAndUntil.ProbUntil(UniformPowerOfTwo.Model.Sample(n-1), (x: nat) => x < n) + WhileAndUntil.ProbUntil(UniformPowerOfTwo.Model.Sample(2 * n), (x: nat) => x < n) } lemma {:axiom} SampleTerminates(n: nat) requires n > 0 ensures - var b := UniformPowerOfTwo.Model.Sample(n - 1); + var b := UniformPowerOfTwo.Model.Sample(2 * n); var c := (x: nat) => x < n; && Independence.IsIndepFn(b) && Quantifier.ExistsStar(WhileAndUntil.Helper2(b, c)) diff --git a/src/Distributions/UniformPowerOfTwo/Correctness.dfy b/src/Distributions/UniformPowerOfTwo/Correctness.dfy index 6e59313e..0ed3b774 100644 --- a/src/Distributions/UniformPowerOfTwo/Correctness.dfy +++ b/src/Distributions/UniformPowerOfTwo/Correctness.dfy @@ -27,12 +27,14 @@ module UniformPowerOfTwoCorrectness { ************/ ghost predicate UnifIsCorrect(n: nat, k: nat, m: nat) - requires (n == 0 && k == 0) || (k != 0 && Helper.Power(2, k - 1) <= n < Helper.Power(2, k)) + requires Helper.Power(2, k) <= n < Helper.Power(2, k + 1) { RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m) == if m < Helper.Power(2, k) then 1.0 / (Helper.Power(2, k) as real) else 0.0 } - function Sample1(n: nat): RandomNumberGenerator.RNG -> RandomNumberGenerator.RNG { + function Sample1(n: nat): RandomNumberGenerator.RNG -> RandomNumberGenerator.RNG + requires n >= 1 + { (s: RandomNumberGenerator.RNG) => Model.Sample(n)(s).1 } @@ -44,13 +46,14 @@ module UniformPowerOfTwoCorrectness { // In contrast to UnifCorrectness, this lemma does not follow // the thesis, but models PROB_BERN_UNIF of the HOL implementation. lemma UnifCorrectness2(n: nat, m: nat) + requires n >= 1 ensures var e := iset s | Model.Sample(n)(s).0 == m; && e in RandomNumberGenerator.event_space - && RandomNumberGenerator.mu(e) == if m < Helper.Power(2, Helper.Log2(n)) then 1.0 / (Helper.Power(2, Helper.Log2(n)) as real) else 0.0 + && RandomNumberGenerator.mu(e) == if m < Helper.Power(2, Model.Log2Floor(n)) then 1.0 / (Helper.Power(2, Model.Log2Floor(n)) as real) else 0.0 { var e := iset s | Model.Sample(n)(s).0 == m; - var k := Helper.Log2(n); + var k := Model.Log2Floor(n); assert e in RandomNumberGenerator.event_space by { assert iset{m} in MeasureTheory.natEventSpace; @@ -65,12 +68,12 @@ module UniformPowerOfTwoCorrectness { } if k == 0 { - assert n == 0; + assert n == 1; UnifCorrectness(n, k); assert UnifIsCorrect(n, k, m); } else { - assert n != 0; - Helper.Log2BothSides(n); + assert n > 1; + Model.Power2OfLog2Floor(n); UnifCorrectness(n, k); assert UnifIsCorrect(n, k, m); } @@ -78,11 +81,12 @@ module UniformPowerOfTwoCorrectness { // See PROB_BERN_UNIF_LT in HOL implementation. lemma UnifCorrectness2Inequality(n: nat, m: nat) - requires m <= Helper.Power(2, Helper.Log2(n)) + requires n >= 1 + requires m <= Helper.Power(2, Model.Log2Floor(n)) ensures var e := iset s | Model.Sample(n)(s).0 < m; && e in RandomNumberGenerator.event_space - && RandomNumberGenerator.mu(e) == (m as real) / (Helper.Power(2, Helper.Log2(n)) as real) + && RandomNumberGenerator.mu(e) == (m as real) / (Helper.Power(2, Model.Log2Floor(n)) as real) { var e := iset s | Model.Sample(n)(s).0 < m; @@ -110,11 +114,11 @@ module UniformPowerOfTwoCorrectness { { assert e1 * e2 == iset{}; RandomNumberGenerator.RNGHasMeasure(); MeasureTheory.PosCountAddImpliesAdd(RandomNumberGenerator.event_space, RandomNumberGenerator.sample_space, RandomNumberGenerator.mu); assert MeasureTheory.IsAdditive(RandomNumberGenerator.event_space, RandomNumberGenerator.mu); } RandomNumberGenerator.mu(e1) + RandomNumberGenerator.mu(e2); { UnifCorrectness2(n, m-1); UnifCorrectness2Inequality(n, m-1); } - (1.0 / (Helper.Power(2, Helper.Log2(n)) as real)) + (((m-1) as real) / (Helper.Power(2, Helper.Log2(n)) as real)); - { Helper.AdditionOfFractions(1.0, (m-1) as real, Helper.Power(2, Helper.Log2(n)) as real); } - (1.0 + (m-1) as real) / (Helper.Power(2, Helper.Log2(n)) as real); + (1.0 / (Helper.Power(2, Model.Log2Floor(n)) as real)) + (((m-1) as real) / (Helper.Power(2, Model.Log2Floor(n)) as real)); + { Helper.AdditionOfFractions(1.0, (m-1) as real, Helper.Power(2, Model.Log2Floor(n)) as real); } + (1.0 + (m-1) as real) / (Helper.Power(2, Model.Log2Floor(n)) as real); { assert 1.0 + (m-1) as real == (m as real); } - (m as real) / (Helper.Power(2, Helper.Log2(n)) as real); + (m as real) / (Helper.Power(2, Model.Log2Floor(n)) as real); } } } @@ -123,22 +127,21 @@ module UniformPowerOfTwoCorrectness { // In contrast to UnifCorrectness2, this lemma follows equation (4.8) // instead of the HOL implementation. lemma UnifCorrectness(n: nat, k: nat) - requires (n == 0 && k == 0) || (k != 0 && Helper.Power(2, k - 1) <= n < Helper.Power(2, k)) + requires Helper.Power(2, k) <= n < Helper.Power(2, k + 1) ensures forall m: nat :: UnifIsCorrect(n, k, m) { forall m: nat ensures UnifIsCorrect(n, k, m) { - if (n == 0 && k == 0) { - UnifCorrectnessCaseNZeroKZero(m); + if (n == 1 && k == 0) { + UnifCorrectnessCaseNOneKZero(m); } else { - assert (k != 0 && Helper.Power(2, k - 1) <= n < Helper.Power(2, k)); assert n > 0; assert n > 1 ==> n / 2 > 0; - if k - 2 < 0 { + if k == 0 { assert 0 < k < 2; assert k == 1; assert Helper.Power(2, k) == 2; - assert 0 < n < 2; - assert n == 1; + assert 2 <= n < 4; + assert n == 2; assert n / 2 == 0; if m % 2 == 0 { UnifCorrectnessCaseKOneMEven(n, m); @@ -147,8 +150,7 @@ module UniformPowerOfTwoCorrectness { UnifCorrectnessCaseKOneMOdd(n, m); } } else { - assert Helper.Power(2, k - 1) / 2 <= n / 2 < Helper.Power(2, k) / 2; - assert Helper.Power(2, k - 2) <= n / 2 < Helper.Power(2, k - 1); + assert Helper.Power(2, k - 1) <= n / 2 < Helper.Power(2, k); var u := m / 2; if m % 2 == 0 { UnifCorrectnessCaseKGreaterOneMEven(n, k, m); @@ -160,21 +162,21 @@ module UniformPowerOfTwoCorrectness { } } - lemma UnifCorrectnessCaseNZeroKZero(m: nat) - ensures UnifIsCorrect(0, 0, m) + lemma UnifCorrectnessCaseNOneKZero(m: nat) + ensures UnifIsCorrect(1, 0, m) { assert Helper.Power(2, 0) == 1; if m == 0 { - assert (iset s | Model.Sample(0)(s).0 == m) == (iset s | true); + assert (iset s | Model.Sample(1)(s).0 == m) == (iset s | true); RandomNumberGenerator.RNGHasMeasure(); } else { - assert (iset s | Model.Sample(0)(s).0 == m) == iset{}; + assert (iset s | Model.Sample(1)(s).0 == m) == iset{}; RandomNumberGenerator.RNGHasMeasure(); } } lemma UnifCorrectnessCaseKOneMEven(n: nat, m: nat) - requires 1 <= n < 2 + requires 2 <= n < 4 requires m % 2 == 0 ensures UnifIsCorrect(n, 1, m) { @@ -217,7 +219,7 @@ module UniformPowerOfTwoCorrectness { } lemma UnifCorrectnessCaseKOneMOdd(n: nat, m: nat) - requires 1 <= n < 2 + requires 2 <= n < 4 requires m % 2 == 1 ensures UnifIsCorrect(n, 1, m) { @@ -258,8 +260,8 @@ module UniformPowerOfTwoCorrectness { } lemma UnifCorrectnessCaseKGreaterOneMEven(n: nat, k: nat, m: nat) - requires k >= 2 - requires Helper.Power(2, k - 1) <= n < Helper.Power(2, k) + requires k >= 1 + requires Helper.Power(2, k) <= n < Helper.Power(2, k + 1) requires m % 2 == 0 ensures UnifIsCorrect(n, k, m) { @@ -298,8 +300,8 @@ module UniformPowerOfTwoCorrectness { } lemma UnifCorrectnessCaseKGreaterOneMOdd(n: nat, k: nat, m: nat) - requires k >= 2 - requires Helper.Power(2, k - 1) <= n < Helper.Power(2, k) + requires k >= 1 + requires Helper.Power(2, k) <= n < Helper.Power(2, k + 1) requires m % 2 == 1 ensures UnifIsCorrect(n, k, m) { @@ -339,11 +341,12 @@ module UniformPowerOfTwoCorrectness { // Equation (4.7) lemma SampleIsIndepFn(n: nat) + requires n >= 1 decreases n ensures Independence.IsIndepFn(Model.Sample(n)) { var fn := Model.Sample(n); - if n == 0 { + if n == 1 { Independence.ReturnIsIndepFn(0 as nat); } else { assert Independence.IsIndepFn(Model.Sample(n / 2)) by { @@ -362,6 +365,7 @@ module UniformPowerOfTwoCorrectness { } lemma SampleIsMeasurePreserving(n: nat) + requires n >= 1 ensures MeasureTheory.IsMeasurePreserving(RandomNumberGenerator.event_space, RandomNumberGenerator.mu, RandomNumberGenerator.event_space, RandomNumberGenerator.mu, Sample1(n)) { var f := Sample1(n); @@ -370,8 +374,7 @@ module UniformPowerOfTwoCorrectness { Independence.IsIndepFnImpliesSndMeasurable(Model.Sample(n)); assert Independence.IsIndepFn(Model.Sample(n)); } - var g := Sample1(n / 2); - if n == 0 { + if n == 1 { forall e | e in RandomNumberGenerator.event_space ensures RandomNumberGenerator.mu(MeasureTheory.PreImage(f, e)) == RandomNumberGenerator.mu(e) { forall s: RandomNumberGenerator.RNG ensures f(s) == s { assert f(s) == s; @@ -380,6 +383,7 @@ module UniformPowerOfTwoCorrectness { } assert MeasureTheory.IsMeasurePreserving(RandomNumberGenerator.event_space, RandomNumberGenerator.mu, RandomNumberGenerator.event_space, RandomNumberGenerator.mu, f); } else { + var g := Sample1(n / 2); forall e | e in RandomNumberGenerator.event_space ensures RandomNumberGenerator.mu(MeasureTheory.PreImage(f, e)) == RandomNumberGenerator.mu(e) { var e' := (iset s | Monad.Tail(s) in e); assert e' in RandomNumberGenerator.event_space by { @@ -424,7 +428,7 @@ module UniformPowerOfTwoCorrectness { } lemma SampleTailDecompose(n: nat, s: RandomNumberGenerator.RNG) - requires n != 0 + requires n >= 2 ensures Model.Sample(n)(s).1 == Monad.Tail(Model.Sample(n / 2)(s).1) { var (a, s') := Model.Sample(n / 2)(s); @@ -449,7 +453,7 @@ module UniformPowerOfTwoCorrectness { } lemma SampleCorrectnessIff(n: nat, s: RandomNumberGenerator.RNG, m: nat) - requires n > 0 + requires n >= 2 ensures var a := Model.Sample(n / 2)(s).0; var b := Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; @@ -476,7 +480,7 @@ module UniformPowerOfTwoCorrectness { lemma SampleCorrectnessEvenCaseIff(n: nat, s: RandomNumberGenerator.RNG, m: nat) requires m % 2 == 0 - requires n > 0 + requires n >= 2 ensures var a := Model.Sample(n / 2)(s).0; var b := Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; @@ -505,7 +509,7 @@ module UniformPowerOfTwoCorrectness { lemma SampleOddCaseIff(n: nat, s: RandomNumberGenerator.RNG, m: nat) requires m % 2 == 1 - requires n > 0 + requires n >= 2 ensures var a := Model.Sample(n / 2)(s).0; var b := Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; @@ -531,7 +535,7 @@ module UniformPowerOfTwoCorrectness { lemma SampleEvenCaseSetEquality(n: nat, m: nat) requires m % 2 == 0 - requires n > 0 + requires n >= 2 ensures var b_of := (s: RandomNumberGenerator.RNG) => Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; var a_of := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).0; @@ -546,7 +550,7 @@ module UniformPowerOfTwoCorrectness { lemma SampleOddCaseSetEquality(n: nat, m: nat) requires m % 2 == 1 - requires n > 0 + requires n >= 2 ensures var b_of := (s: RandomNumberGenerator.RNG) => Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; var a_of := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).0; @@ -559,9 +563,9 @@ module UniformPowerOfTwoCorrectness { } } - lemma SampleEvenCase(n: nat, m: nat) + lemma {:vcs_split_on_every_assert} SampleEvenCase(n: nat, m: nat) requires m % 2 == 0 - requires n > 0 + requires n >= 2 ensures RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m) == RandomNumberGenerator.mu(iset s | 2*Model.Sample(n / 2)(s).0 == m) / 2.0 { var a_of := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).0; @@ -662,7 +666,7 @@ module UniformPowerOfTwoCorrectness { lemma SampleOddCase(n: nat, m: nat) requires m % 2 == 1 - requires n > 0 + requires n >= 2 ensures RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m) == RandomNumberGenerator.mu(iset s | 2*Model.Sample(n / 2)(s).0 + 1 == m) / 2.0 { var a_of := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).0; @@ -751,7 +755,7 @@ module UniformPowerOfTwoCorrectness { } lemma SampleCaseSplit(n: nat, m: nat) - requires n > 0 + requires n >= 2 ensures RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m) == if m % 2 == 0 then RandomNumberGenerator.mu(iset s | 2*Model.Sample(n / 2)(s).0 == m) / 2.0 else RandomNumberGenerator.mu(iset s | 2*Model.Sample(n / 2)(s).0 + 1 == m) / 2.0 { if m % 2 == 0 { diff --git a/src/Distributions/UniformPowerOfTwo/Implementation.dfy b/src/Distributions/UniformPowerOfTwo/Implementation.dfy index 172de766..50c33ed3 100644 --- a/src/Distributions/UniformPowerOfTwo/Implementation.dfy +++ b/src/Distributions/UniformPowerOfTwo/Implementation.dfy @@ -12,13 +12,15 @@ module UniformPowerOfTwoImplementation { trait {:termination false} Trait extends Interface.Trait { method UniformPowerOfTwoSample(n: nat) returns (u: nat) + requires n >= 1 modifies this ensures Model.Sample(n)(old(s)) == (u, s) { u := 0; var n' := n; - while n' > 0 + while n' > 1 + invariant n' >= 1 invariant Model.SampleTailRecursive(n)(old(s)) == Model.SampleTailRecursive(n', u)(s) { var b := CoinSample(); diff --git a/src/Distributions/UniformPowerOfTwo/Interface.dfy b/src/Distributions/UniformPowerOfTwo/Interface.dfy index a94f86e8..4b34ced9 100644 --- a/src/Distributions/UniformPowerOfTwo/Interface.dfy +++ b/src/Distributions/UniformPowerOfTwo/Interface.dfy @@ -12,7 +12,9 @@ module UniformPowerOfTwoInterface { trait {:termination false} Trait extends Coin.Interface.Trait { + // The return value u is uniformly distributed between 0 <= u < 2^k where 2^k <= n < 2^(k + 1). method UniformPowerOfTwoSample(n: nat) returns (u: nat) + requires n >= 1 modifies this ensures Model.Sample(n)(old(s)) == (u, s) diff --git a/src/Distributions/UniformPowerOfTwo/Model.dfy b/src/Distributions/UniformPowerOfTwo/Model.dfy index 00e01e5e..0d6216e7 100644 --- a/src/Distributions/UniformPowerOfTwo/Model.dfy +++ b/src/Distributions/UniformPowerOfTwo/Model.dfy @@ -26,9 +26,12 @@ module UniformPowerOfTwoModel { Monad.Bind(Monad.Deconstruct, UnifStepHelper(m)) } - // Definition 48 - function Sample(n: nat): (h: Monad.Hurd) { - if n == 0 then + // Adapted from Definition 48 (see issue #79 for the reason of the modification) + // The return value u is uniformly distributed between 0 <= u < 2^k where 2^k <= n < 2^(k + 1). + function Sample(n: nat): (h: Monad.Hurd) + requires n >= 1 + { + if n == 1 then Monad.Return(0) else Monad.Bind(Sample(n/2), UnifStep) @@ -36,10 +39,10 @@ module UniformPowerOfTwoModel { // A tail recursive version of Sample, closer to the imperative implementation function SampleTailRecursive(n: nat, u: nat := 0): Monad.Hurd - decreases n + requires n >= 1 { (s: RandomNumberGenerator.RNG) => - if n == 0 then + if n == 1 then (u, s) else SampleTailRecursive(n / 2, if Monad.Head(s) then 2*u + 1 else 2*u)(Monad.Tail(s)) @@ -47,43 +50,52 @@ module UniformPowerOfTwoModel { // Equivalence of Sample and its tail-recursive version lemma SampleCorrespondence(n: nat, s: RandomNumberGenerator.RNG) + requires n >= 1 ensures SampleTailRecursive(n)(s) == Sample(n)(s) { - if n == 0 { + if n == 1 { assert SampleTailRecursive(n)(s) == Sample(n)(s); } else { - var k := Helper.Log2(n); - assert Power2(k - 1) <= n < Power2(k) by { Power2OfLog2(n); } + var k := Log2Floor(n); + assert Helper.Power(2, k) <= n < Helper.Power(2, k + 1) by { Power2OfLog2Floor(n); } calc { SampleTailRecursive(n)(s); - { SampleTailRecursiveEqualIfSameLog2Floor(n, Power2(k - 1), k, 0, s); } - SampleTailRecursive(Power2(k - 1))(s); - Monad.Bind(Sample(Power2(-1)), (u: nat) => SampleTailRecursive(Power2(k - 1), u))(s); - { RelateWithTailRecursive(k - 1, k, s); } - Sample(Power2(k - 1))(s); - { SampleEqualIfSameLog2Floor(n, Power2(k - 1), k, s); } + { SampleTailRecursiveEqualIfSameLog2Floor(n, Helper.Power(2, k), k, 0, s); } + SampleTailRecursive(Helper.Power(2, k))(s); + Monad.Bind(Sample(Helper.Power(2, 0)), (u: nat) => SampleTailRecursive(Helper.Power(2, k), u))(s); + { RelateWithTailRecursive(k, 0, s); } + Sample(Helper.Power(2, k))(s); + { SampleEqualIfSameLog2Floor(n, Helper.Power(2, k), k, s); } Sample(n)(s); } } } - // A version of Power(2, k) extended to negative k's. - function Power2(k: int): nat { - if k < 0 then 0 else if k == 0 then 1 else Power2(k - 1) * 2 + function Log2Floor(n: nat): nat + requires n >= 1 + decreases n + { + if n < 2 + then 0 + else Log2Floor(n / 2) + 1 } - lemma Power2Greater1(k: nat) - ensures Power2(k) >= 1 + lemma PowerGreater0(base: nat, exponent: nat) + requires base >= 2 + ensures Helper.Power(base, exponent) >= 1 {} - lemma Power2OfLog2(n: nat) - ensures Power2(Helper.Log2(n) - 1) <= n < Power2(Helper.Log2(n)) + lemma Power2OfLog2Floor(n: nat) + requires n >= 1 + ensures Helper.Power(2, Log2Floor(n)) <= n < Helper.Power(2, Log2Floor(n) + 1) {} // All numbers between consecutive powers of 2 behave the same as arguments to SampleTailRecursive lemma SampleTailRecursiveEqualIfSameLog2Floor(m: nat, n: nat, k: nat, u: nat, s: RandomNumberGenerator.RNG) - requires Power2(k - 1) <= m < Power2(k) - requires Power2(k - 1) <= n < Power2(k) + requires m >= 1 + requires n >= 1 + requires Helper.Power(2, k) <= m < Helper.Power(2, k + 1) + requires Helper.Power(2, k) <= n < Helper.Power(2, k + 1) ensures SampleTailRecursive(m, u)(s) == SampleTailRecursive(n, u)(s) { if k == 0 { @@ -103,8 +115,10 @@ module UniformPowerOfTwoModel { // All numbers between consecutive powers of 2 behave the same as arguments to Sample lemma SampleEqualIfSameLog2Floor(m: nat, n: nat, k: nat, s: RandomNumberGenerator.RNG) - requires Power2(k - 1) <= m < Power2(k) - requires Power2(k - 1) <= n < Power2(k) + requires m >= 1 + requires n >= 1 + requires Helper.Power(2, k) <= m < Helper.Power(2, k + 1) + requires Helper.Power(2, k) <= n < Helper.Power(2, k + 1) ensures Sample(m)(s) == Sample(n)(s) { if k == 0 { @@ -123,35 +137,33 @@ module UniformPowerOfTwoModel { } // The induction invariant for the equivalence proof (generalized version of SampleCorrespondence) - lemma RelateWithTailRecursive(k: nat, l: nat, s: RandomNumberGenerator.RNG) - requires l <= k + 1 + lemma RelateWithTailRecursive(l: nat, m: nat, s: RandomNumberGenerator.RNG) decreases l - ensures Monad.Bind(Sample(Power2(k - l)), (u: nat) => SampleTailRecursive(Power2(l - 1), u))(s) == Sample(Power2(k))(s) + ensures Monad.Bind(Sample(Helper.Power(2, m)), (u: nat) => SampleTailRecursive(Helper.Power(2, l), u))(s) == Sample(Helper.Power(2, m + l))(s) { if l == 0 { calc { - Monad.Bind(Sample(Power2(k - l)), (u: nat) => SampleTailRecursive(Power2(l - 1), u))(s); - (var (u, s') := Sample(Power2(k - l))(s); SampleTailRecursive(0, u)(s')); - Sample(Power2(k))(s); + Monad.Bind(Sample(Helper.Power(2, m)), (u: nat) => SampleTailRecursive(Helper.Power(2, l), u))(s); + (var (u, s') := Sample(Helper.Power(2, m))(s); SampleTailRecursive(1, u)(s')); + Sample(Helper.Power(2, m + l))(s); } } else { - var k' := k - l; - assert Ineq1: Power2(l - 1) >= 1 by { Power2Greater1(l - 1); } - assert Power2(k - l + 1) >= 1 by { Power2Greater1(k - l + 1); } + assert Ineq1: Helper.Power(2, l) >= 1 by { PowerGreater0(2, l); } + assert Helper.Power(2, m) >= 1 by { PowerGreater0(2, m); } calc { - Monad.Bind(Sample(Power2(k - l)), (u: nat) => SampleTailRecursive(Power2(l - 1), u))(s); - (var (u, s') := Sample(Power2(k - l))(s); SampleTailRecursive(Power2(l - 1), u)(s')); + Monad.Bind(Sample(Helper.Power(2, m)), (u: nat) => SampleTailRecursive(Helper.Power(2, l), u))(s); + (var (u, s') := Sample(Helper.Power(2, m))(s); SampleTailRecursive(Helper.Power(2, l), u)(s')); { reveal Ineq1; } - (var (u, s') := Sample(Power2(k - l))(s); - SampleTailRecursive(Power2(l - 1) / 2, if Monad.Head(s') then 2 * u + 1 else 2 * u)(Monad.Tail(s'))); - { assert Power2(k - l + 1) / 2 == Power2(k - l); } - (var (u', s') := Monad.Bind(Sample(Power2(k - l)), UnifStep)(s); - SampleTailRecursive(Power2(l - 2), u')(s')); - (var (u', s') := Sample(Power2(k - l + 1))(s); - SampleTailRecursive(Power2(l - 2), u')(s')); - Monad.Bind(Sample(Power2(k - l + 1)), (u: nat) => SampleTailRecursive(Power2(l - 2), u))(s); - { RelateWithTailRecursive(k, l - 1, s); } - Sample(Power2(k))(s); + (var (u, s') := Sample(Helper.Power(2, m))(s); + SampleTailRecursive(Helper.Power(2, l) / 2, if Monad.Head(s') then 2 * u + 1 else 2 * u)(Monad.Tail(s'))); + { assert Helper.Power(2, m + 1) / 2 == Helper.Power(2, m); } + (var (u', s') := Monad.Bind(Sample(Helper.Power(2, m)), UnifStep)(s); + SampleTailRecursive(Helper.Power(2, l - 1), u')(s')); + (var (u', s') := Sample(Helper.Power(2, m + 1))(s); + SampleTailRecursive(Helper.Power(2, l - 1), u')(s')); + Monad.Bind(Sample(Helper.Power(2, m + 1)), (u: nat) => SampleTailRecursive(Helper.Power(2, l - 1), u))(s); + { RelateWithTailRecursive(l - 1, m + 1, s); } + Sample(Helper.Power(2, m + l))(s); } } } From 9b219646a4b8f02a6b24b02d8847a3ba491eed0d Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Wed, 4 Oct 2023 17:38:43 -0400 Subject: [PATCH 2/9] Cleanup helper --- src/Distributions/Uniform/Correctness.dfy | 16 +- .../UniformPowerOfTwo/Correctness.dfy | 18 +- src/Distributions/UniformPowerOfTwo/Model.dfy | 27 +-- src/Math/Helper.dfy | 211 ++---------------- 4 files changed, 36 insertions(+), 236 deletions(-) diff --git a/src/Distributions/Uniform/Correctness.dfy b/src/Distributions/Uniform/Correctness.dfy index 2549125c..58f4634b 100644 --- a/src/Distributions/Uniform/Correctness.dfy +++ b/src/Distributions/Uniform/Correctness.dfy @@ -77,23 +77,23 @@ module UniformCorrectness { } assert RandomNumberGenerator.mu(e) == 1.0 / (n as real) by { - assert RandomNumberGenerator.mu(e1) == 1.0 / (Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) as real) by { - assert i < Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) by { - UniformPowerOfTwo.Model.Power2OfLog2Floor(n); + assert 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 { + Helper.Power2OfLog2Floor(n); } UniformPowerOfTwo.Correctness.UnifCorrectness2(2 * n, i); } - assert RandomNumberGenerator.mu(e2) == (n as real) / (Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) as real) by { - assert n < Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) by { UniformPowerOfTwo.Model.Power2OfLog2Floor(n); } + assert 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); } UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(2 * n, n); } calc { RandomNumberGenerator.mu(e); { assert e == x.0; assert e1 == x.1; assert e2 == x.2; assert RandomNumberGenerator.mu(x.0) == RandomNumberGenerator.mu(x.1) / RandomNumberGenerator.mu(x.2); } RandomNumberGenerator.mu(e1) / RandomNumberGenerator.mu(e2); - { assert RandomNumberGenerator.mu(e1) == 1.0 / (Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) as real); assert RandomNumberGenerator.mu(e2) == (n as real) / (Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) as real); } - (1.0 / (Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) as real)) / ((n as real) / (Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) as real)); - { Helper.SimplifyFractions(1.0, n as real, Helper.Power(2, UniformPowerOfTwo.Model.Log2Floor(2 * n)) as real); } + { assert RandomNumberGenerator.mu(e1) == 1.0 / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real); assert RandomNumberGenerator.mu(e2) == (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real); } + (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); } } diff --git a/src/Distributions/UniformPowerOfTwo/Correctness.dfy b/src/Distributions/UniformPowerOfTwo/Correctness.dfy index 0ed3b774..a34bea1f 100644 --- a/src/Distributions/UniformPowerOfTwo/Correctness.dfy +++ b/src/Distributions/UniformPowerOfTwo/Correctness.dfy @@ -50,10 +50,10 @@ module UniformPowerOfTwoCorrectness { ensures var e := iset s | Model.Sample(n)(s).0 == m; && e in RandomNumberGenerator.event_space - && RandomNumberGenerator.mu(e) == if m < Helper.Power(2, Model.Log2Floor(n)) then 1.0 / (Helper.Power(2, Model.Log2Floor(n)) as real) else 0.0 + && RandomNumberGenerator.mu(e) == if m < Helper.Power(2, Helper.Log2Floor(n)) then 1.0 / (Helper.Power(2, Helper.Log2Floor(n)) as real) else 0.0 { var e := iset s | Model.Sample(n)(s).0 == m; - var k := Model.Log2Floor(n); + var k := Helper.Log2Floor(n); assert e in RandomNumberGenerator.event_space by { assert iset{m} in MeasureTheory.natEventSpace; @@ -73,7 +73,7 @@ module UniformPowerOfTwoCorrectness { assert UnifIsCorrect(n, k, m); } else { assert n > 1; - Model.Power2OfLog2Floor(n); + Helper.Power2OfLog2Floor(n); UnifCorrectness(n, k); assert UnifIsCorrect(n, k, m); } @@ -82,11 +82,11 @@ module UniformPowerOfTwoCorrectness { // See PROB_BERN_UNIF_LT in HOL implementation. lemma UnifCorrectness2Inequality(n: nat, m: nat) requires n >= 1 - requires m <= Helper.Power(2, Model.Log2Floor(n)) + requires m <= Helper.Power(2, Helper.Log2Floor(n)) ensures var e := iset s | Model.Sample(n)(s).0 < m; && e in RandomNumberGenerator.event_space - && RandomNumberGenerator.mu(e) == (m as real) / (Helper.Power(2, Model.Log2Floor(n)) as real) + && RandomNumberGenerator.mu(e) == (m as real) / (Helper.Power(2, Helper.Log2Floor(n)) as real) { var e := iset s | Model.Sample(n)(s).0 < m; @@ -114,11 +114,11 @@ module UniformPowerOfTwoCorrectness { { assert e1 * e2 == iset{}; RandomNumberGenerator.RNGHasMeasure(); MeasureTheory.PosCountAddImpliesAdd(RandomNumberGenerator.event_space, RandomNumberGenerator.sample_space, RandomNumberGenerator.mu); assert MeasureTheory.IsAdditive(RandomNumberGenerator.event_space, RandomNumberGenerator.mu); } RandomNumberGenerator.mu(e1) + RandomNumberGenerator.mu(e2); { UnifCorrectness2(n, m-1); UnifCorrectness2Inequality(n, m-1); } - (1.0 / (Helper.Power(2, Model.Log2Floor(n)) as real)) + (((m-1) as real) / (Helper.Power(2, Model.Log2Floor(n)) as real)); - { Helper.AdditionOfFractions(1.0, (m-1) as real, Helper.Power(2, Model.Log2Floor(n)) as real); } - (1.0 + (m-1) as real) / (Helper.Power(2, Model.Log2Floor(n)) as real); + (1.0 / (Helper.Power(2, Helper.Log2Floor(n)) as real)) + (((m-1) as real) / (Helper.Power(2, Helper.Log2Floor(n)) as real)); + { Helper.AdditionOfFractions(1.0, (m-1) as real, Helper.Power(2, Helper.Log2Floor(n)) as real); } + (1.0 + (m-1) as real) / (Helper.Power(2, Helper.Log2Floor(n)) as real); { assert 1.0 + (m-1) as real == (m as real); } - (m as real) / (Helper.Power(2, Model.Log2Floor(n)) as real); + (m as real) / (Helper.Power(2, Helper.Log2Floor(n)) as real); } } } diff --git a/src/Distributions/UniformPowerOfTwo/Model.dfy b/src/Distributions/UniformPowerOfTwo/Model.dfy index 0d6216e7..be09358c 100644 --- a/src/Distributions/UniformPowerOfTwo/Model.dfy +++ b/src/Distributions/UniformPowerOfTwo/Model.dfy @@ -56,8 +56,8 @@ module UniformPowerOfTwoModel { if n == 1 { assert SampleTailRecursive(n)(s) == Sample(n)(s); } else { - var k := Log2Floor(n); - assert Helper.Power(2, k) <= n < Helper.Power(2, k + 1) by { Power2OfLog2Floor(n); } + var k := Helper.Log2Floor(n); + assert Helper.Power(2, k) <= n < Helper.Power(2, k + 1) by { Helper.Power2OfLog2Floor(n); } calc { SampleTailRecursive(n)(s); { SampleTailRecursiveEqualIfSameLog2Floor(n, Helper.Power(2, k), k, 0, s); } @@ -71,25 +71,6 @@ module UniformPowerOfTwoModel { } } - function Log2Floor(n: nat): nat - requires n >= 1 - decreases n - { - if n < 2 - then 0 - else Log2Floor(n / 2) + 1 - } - - lemma PowerGreater0(base: nat, exponent: nat) - requires base >= 2 - ensures Helper.Power(base, exponent) >= 1 - {} - - lemma Power2OfLog2Floor(n: nat) - requires n >= 1 - ensures Helper.Power(2, Log2Floor(n)) <= n < Helper.Power(2, Log2Floor(n) + 1) - {} - // All numbers between consecutive powers of 2 behave the same as arguments to SampleTailRecursive lemma SampleTailRecursiveEqualIfSameLog2Floor(m: nat, n: nat, k: nat, u: nat, s: RandomNumberGenerator.RNG) requires m >= 1 @@ -148,8 +129,8 @@ module UniformPowerOfTwoModel { Sample(Helper.Power(2, m + l))(s); } } else { - assert Ineq1: Helper.Power(2, l) >= 1 by { PowerGreater0(2, l); } - assert Helper.Power(2, m) >= 1 by { PowerGreater0(2, m); } + assert Ineq1: Helper.Power(2, l) >= 1 by { Helper.PowerGreater0(2, l); } + assert Helper.Power(2, m) >= 1 by { Helper.PowerGreater0(2, m); } calc { Monad.Bind(Sample(Helper.Power(2, m)), (u: nat) => SampleTailRecursive(Helper.Power(2, l), u))(s); (var (u, s') := Sample(Helper.Power(2, m))(s); SampleTailRecursive(Helper.Power(2, l), u)(s')); diff --git a/src/Math/Helper.dfy b/src/Math/Helper.dfy index 17e25328..c24c91a0 100644 --- a/src/Math/Helper.dfy +++ b/src/Math/Helper.dfy @@ -8,22 +8,6 @@ module Helper { Definitions ************/ - function Abs(x: real): real { - if x < 0.0 then - -x - else - x - } - - function RealPower(b: real, n: nat): (p: real) - ensures b > 0.0 ==> p > 0.0 - { - match n - case 0 => 1.0 - case 1 => b - case _ => b * RealPower(b, n - 1) - } - function Power(b: nat, n: nat): (p: nat) ensures b > 0 ==> p > 0 { @@ -33,12 +17,13 @@ module Helper { case _ => b * Power(b, n - 1) } - // See LOG2_ML - function Log2(n: nat): nat { - if n == 0 then - 0 - else - Log2(n / 2) + 1 + function Log2Floor(n: nat): nat + requires n >= 1 + decreases n + { + if n < 2 + then 0 + else Log2Floor(n / 2) + 1 } @@ -46,45 +31,12 @@ module Helper { Lemmas *******/ - lemma NatDivisionHelper(a: nat, b: nat) - requires b != 0 - ensures a / b == (a as real / b as real).Floor - { - assert a == (a / b) * b + (a % b); - assert a as real == (a / b) as real * b as real + (a % b) as real; - assert a as real / b as real == (a / b) as real + (a % b) as real / b as real; - } - - lemma DivisionByOne(x: real) - ensures x / (1 as real) == x - ensures x / 1.0 == x - {} - - lemma DivisionSubstitute(x: real, a: real, b: real) - requires a == b - requires a != 0.0 && b != 0.0 - ensures x / a == x / b - {} - - lemma DivisionSubstituteAlternative(n: nat, a: nat, b: nat) - requires a == b - requires n != 0 - ensures a / n == b / n - {} - lemma DivisionSubstituteAlternativeReal(x: real, a: real, b: real) requires a == b requires x != 0.0 ensures a / x == b / x {} - lemma SmallDivMod(n: nat, m: nat) - requires m > 0 - requires n < m - ensures n / m == 0 - ensures n % m == n - {} - lemma DivModAddDenominator(n: nat, m: nat) requires m > 0 ensures (n + m) / m == n / m + 1 @@ -124,143 +76,19 @@ module Helper { DivModIsUnique(a * c + b, a, c + b / a, b % a); } - lemma MultiplicationSubstitute(x: real, a: real, b: real) - requires a == b - ensures a * x == b * x - {} - - lemma InverseSubstitute(x: real, y: real) - requires x != 0.0 - requires y != 0.0 - requires x == y - ensures 1.0 / x == 1.0 / y - {} - lemma DivisionByTwo(x: real) ensures 0.5 * x == x / 2.0 {} - lemma RealAssoc(x: real, y: real) - requires y != 0.0 - ensures (x * y) / y == x - { - calc { - (x * y) / y; - == - x * (y / y); - == { assert y / y == 1.0; } - x * 1.0; - == - x; - } - } - - lemma NatAssoc(a: nat, b: nat) - requires b != 0 - ensures ((a as real) * (b as real)) / (b as real) == (a as real) - { - RealAssoc(a as real, b as real); - } - - lemma NatDivision(a: nat, b: nat) - requires b != 0 - ensures (a * b) / b == a - { - calc { - (a * b) / b; - == { NatDivisionHelper(a * b, b); } - ((a * b) as real / b as real).Floor; - == { assert (a * b) as real == (a as real) * (b as real); } - (((a as real) * (b as real)) / (b as real)).Floor; - == { NatAssoc(a, b); } - ((a as real)).Floor; - == - a; - } - } - - lemma PowerDivision(b: nat, n: int) - requires b != 0 && n >= 1 - ensures Power(b, n) / b == Power(b, n - 1) - { - if n == 1 { - calc { - Power(b, n) / b; - == - b / b; - == - 1; - == - Power(b, 0); - == - Power(b, n - 1); - } - } else { - calc { - Power(b, n) / b; - == { } - (b * Power(b, n - 1)) / b; - == { } - (Power(b, n - 1) * b) / b; - == { NatDivision(Power(b, n - 1), b); } - Power(b, n - 1); - } - } - } - - // // See DivMod.dfy in StdLib - // lemma DivDecreases(n: nat, d: nat) - // requires n != 0 - // requires 1 < d - // ensures n / d < n - // { - // calc { - // n / d; - // == { LemmaAboutNatDivision(n, d); } - // (n as real / d as real).Floor; - // < { assert n as real / d as real < n as real / 1 as real; } - // (n as real / 1 as real).Floor; - // == - // (n as real).Floor; - // == - // n; - // } - // } + lemma PowerGreater0(base: nat, exponent: nat) + requires base >= 1 + ensures Power(base, exponent) >= 1 + {} - lemma LemmaDivisionByTwo(n: nat) - requires n != 0 - ensures n / 2 <= n - 1 - { - if n == 1 { - calc { - n / 2; - == - 1 / 2; - == - 0; - == - n - 1; - } - } else { - calc { - n / 2; - == - (n as real / 2 as real).Floor; - == - ((n - 1 + 1) as real / 2 as real).Floor; - == - (((n - 1) as real / 2 as real) + (1 as real / 2 as real)).Floor; - <= - (((n - 1) as real / 2 as real) + 1.0).Floor; - == - ((n - 1) as real / 2 as real).Floor + 1; - <= - n - 2 + 1; - == - n - 1; - } - } - } + lemma Power2OfLog2Floor(n: nat) + requires n >= 1 + ensures Power(2, Log2Floor(n)) <= n < Power(2, Log2Floor(n) + 1) + {} lemma AdditionOfFractions(x: real, y: real, z: real) requires z != 0.0 @@ -277,15 +105,6 @@ module Helper { ensures (x * y) as real == (x as real) * (y as real) {} - lemma Log2LowerSuc(n: nat) - ensures n + 1 <= Power(2, Log2(n)) - {} - - lemma Log2BothSides(n: nat) - requires n != 0 - ensures Power(2, Log2(n) - 1) <= n < Power(2, Log2(n)) - {} - lemma SimplifyFractions(x: real, y: real, z: real) requires z != 0.0 requires y != 0.0 From 67882c61df3cd8a5aaf8cd8cf2660d543ae13fb2 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Wed, 4 Oct 2023 18:59:14 -0400 Subject: [PATCH 3/9] Reduce resource usage of `UniformFullCorrectness` --- src/Distributions/Uniform/Correctness.dfy | 63 +++++++++++++++++------ src/Math/Helper.dfy | 5 ++ 2 files changed, 51 insertions(+), 17 deletions(-) diff --git a/src/Distributions/Uniform/Correctness.dfy b/src/Distributions/Uniform/Correctness.dfy index 58f4634b..65ee8863 100644 --- a/src/Distributions/Uniform/Correctness.dfy +++ b/src/Distributions/Uniform/Correctness.dfy @@ -40,12 +40,10 @@ module UniformCorrectness { // Correctness theorem for Model.Sample // Equation (4.12) / PROB_BERN_UNIFORM - lemma {:vcs_split_on_every_assert} UniformFullCorrectness(n: nat, i: nat) + lemma UniformFullCorrectness(n: nat, i: nat) requires 0 <= i < n - ensures - var e := UniformFullCorrectnessHelper(n, i); - && e in RandomNumberGenerator.event_space - && RandomNumberGenerator.mu(e) == 1.0 / (n as real) + ensures UniformFullCorrectnessHelper(n, i) in RandomNumberGenerator.event_space + ensures RandomNumberGenerator.mu(UniformFullCorrectnessHelper(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; @@ -66,32 +64,63 @@ module UniformCorrectness { var x := WhileAndUntil.ConstructEvents(b, c, d); WhileAndUntil.ProbUntilProbabilityFraction(b, c, d); - assert RandomNumberGenerator.mu(x.0) == RandomNumberGenerator.mu(x.1) / RandomNumberGenerator.mu(x.2); + assert Fraction: RandomNumberGenerator.mu(x.0) == RandomNumberGenerator.mu(x.1) / RandomNumberGenerator.mu(x.2); - assert x.0 == e; - assert x.1 == e1 by { - assert forall s :: d(b(s).0) && c(b(s).0) <==> (UniformPowerOfTwo.Model.Sample(2 * n)(s).0 == i); + 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 x.2 == e2 by { - assert forall s :: c(b(s).0) <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n; + + 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 RandomNumberGenerator.mu(e) == 1.0 / (n as real) by { - assert RandomNumberGenerator.mu(e1) == 1.0 / (Helper.Power(2, Helper.Log2Floor(2 * 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 { - Helper.Power2OfLog2Floor(n); + 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 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); } + 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); } calc { RandomNumberGenerator.mu(e); - { assert e == x.0; assert e1 == x.1; assert e2 == x.2; assert RandomNumberGenerator.mu(x.0) == RandomNumberGenerator.mu(x.1) / RandomNumberGenerator.mu(x.2); } + { reveal X0; reveal X1; reveal X2; reveal Fraction; } RandomNumberGenerator.mu(e1) / RandomNumberGenerator.mu(e2); - { assert RandomNumberGenerator.mu(e1) == 1.0 / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real); assert RandomNumberGenerator.mu(e2) == (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real); } + { reveal ProbE1; reveal ProbE2; } (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); diff --git a/src/Math/Helper.dfy b/src/Math/Helper.dfy index c24c91a0..44b2da49 100644 --- a/src/Math/Helper.dfy +++ b/src/Math/Helper.dfy @@ -26,6 +26,11 @@ module Helper { else Log2Floor(n / 2) + 1 } + lemma Log2FloorDef(n: nat) + requires n >= 1 + ensures Log2Floor(2 * n) == Log2Floor(n) + 1 + {} + /******* Lemmas From 783b477e525f0346783168aef6b8868990814af9 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Wed, 4 Oct 2023 19:29:20 -0400 Subject: [PATCH 4/9] Simplify UniformPowerOfTwo --- .../UniformPowerOfTwo/Correctness.dfy | 140 ++---------------- 1 file changed, 15 insertions(+), 125 deletions(-) diff --git a/src/Distributions/UniformPowerOfTwo/Correctness.dfy b/src/Distributions/UniformPowerOfTwo/Correctness.dfy index a34bea1f..77f893ae 100644 --- a/src/Distributions/UniformPowerOfTwo/Correctness.dfy +++ b/src/Distributions/UniformPowerOfTwo/Correctness.dfy @@ -131,142 +131,37 @@ module UniformPowerOfTwoCorrectness { ensures forall m: nat :: UnifIsCorrect(n, k, m) { forall m: nat ensures UnifIsCorrect(n, k, m) { - if (n == 1 && k == 0) { - UnifCorrectnessCaseNOneKZero(m); + assert n >= 1 by { Helper.PowerGreater0(2, k); } + if k == 0 { + UnifCorrectnessCaseNOne(m); } else { - assert n > 0; - assert n > 1 ==> n / 2 > 0; - if k == 0 { - assert 0 < k < 2; - assert k == 1; - assert Helper.Power(2, k) == 2; - assert 2 <= n < 4; - assert n == 2; - assert n / 2 == 0; - if m % 2 == 0 { - UnifCorrectnessCaseKOneMEven(n, m); - } else { - assert m % 2 == 1; - UnifCorrectnessCaseKOneMOdd(n, m); - } + if m % 2 == 0 { + UnifCorrectnessCaseMEven(n, k, m / 2); } else { - assert Helper.Power(2, k - 1) <= n / 2 < Helper.Power(2, k); - var u := m / 2; - if m % 2 == 0 { - UnifCorrectnessCaseKGreaterOneMEven(n, k, m); - } else { - UnifCorrectnessCaseKGreaterOneMOdd(n, k, m); - } + UnifCorrectnessCaseMOdd(n, k, m / 2); } } } } - lemma UnifCorrectnessCaseNOneKZero(m: nat) + lemma UnifCorrectnessCaseNOne(m: nat) ensures UnifIsCorrect(1, 0, m) { assert Helper.Power(2, 0) == 1; if m == 0 { - assert (iset s | Model.Sample(1)(s).0 == m) == (iset s | true); - RandomNumberGenerator.RNGHasMeasure(); + assert (iset s | Model.Sample(1)(s).0 == m) == (iset s); } else { assert (iset s | Model.Sample(1)(s).0 == m) == iset{}; - RandomNumberGenerator.RNGHasMeasure(); - } - } - - lemma UnifCorrectnessCaseKOneMEven(n: nat, m: nat) - requires 2 <= n < 4 - requires m % 2 == 0 - ensures UnifIsCorrect(n, 1, m) - { - calc { - RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); - == { SampleCaseSplit(n, m); } - RandomNumberGenerator.mu(iset s | 2*Model.Sample(n / 2)(s).0 == m) / 2.0; - == { assert (iset s | 2*Model.Sample(n / 2)(s).0 == m) == (iset s | 0 == m); } - RandomNumberGenerator.mu(iset s | 0 == m) / 2.0; - } - if m < Helper.Power(2, 1) { - assert m == 0; - calc { - RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); - == - RandomNumberGenerator.mu(iset s | 0 == m) / 2.0; - == { assert (iset s: RandomNumberGenerator.RNG | 0 == m) == (iset s | true); } - RandomNumberGenerator.mu(iset s | true) / 2.0; - == { RandomNumberGenerator.RNGHasMeasure(); } - 1.0 / 2.0; - == - 1.0 / (2 as real); - == { assert Helper.Power(2, 1) == 2; } - 1.0 / (Helper.Power(2, 1) as real); - } - } else { - assert m != 0; - calc { - RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); - == - RandomNumberGenerator.mu(iset s | 0 == m) / 2.0; - == { assert (iset s: RandomNumberGenerator.RNG | 0 == m) == iset{}; } - RandomNumberGenerator.mu(iset {}) / 2.0; - == { RandomNumberGenerator.RNGHasMeasure(); } - 0.0 / 2.0; - == - 0.0; - } } + RandomNumberGenerator.RNGHasMeasure(); } - lemma UnifCorrectnessCaseKOneMOdd(n: nat, m: nat) - requires 2 <= n < 4 - requires m % 2 == 1 - ensures UnifIsCorrect(n, 1, m) - { - calc { - RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); - == { SampleCaseSplit(n, m); } - RandomNumberGenerator.mu(iset s | 2*Model.Sample(n / 2)(s).0 + 1 == m) / 2.0; - == { assert (iset s | 2*Model.Sample(n / 2)(s).0 + 1 == m) == (iset s | 1 == m); } - RandomNumberGenerator.mu(iset s | 1 == m) / 2.0; - } - if m < Helper.Power(2, 1) { - assert m == 1; - calc { - RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); - == - RandomNumberGenerator.mu(iset s | 1 == m) / 2.0; - == { assert (iset s: RandomNumberGenerator.RNG | 1 == m) == (iset s | true); } - RandomNumberGenerator.mu(iset s | true) / 2.0; - == { RandomNumberGenerator.RNGHasMeasure(); Helper.DivisionSubstituteAlternativeReal(2.0, RandomNumberGenerator.mu(iset s | 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 | Model.Sample(n)(s).0 == m); - == - RandomNumberGenerator.mu(iset s: RandomNumberGenerator.RNG | 1 == m) / 2.0; - == { assert (iset s: RandomNumberGenerator.RNG | 1 == m) == iset{}; } - RandomNumberGenerator.mu(iset {}) / 2.0; - == { RandomNumberGenerator.RNGHasMeasure(); } - 0.0 / 2.0; - == - 0.0; - } - } - } - - lemma UnifCorrectnessCaseKGreaterOneMEven(n: nat, k: nat, m: nat) + lemma UnifCorrectnessCaseMEven(n: nat, k: nat, u: nat) requires k >= 1 requires Helper.Power(2, k) <= n < Helper.Power(2, k + 1) - requires m % 2 == 0 - ensures UnifIsCorrect(n, k, m) + ensures UnifIsCorrect(n, k, 2 * u) { - var u := m / 2; - assert m == 2 * u; + var m := 2 * u; calc { RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); == { SampleCaseSplit(n, m); } @@ -276,7 +171,6 @@ module UniformPowerOfTwoCorrectness { } 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); } @@ -295,18 +189,15 @@ module UniformPowerOfTwoCorrectness { 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; - assert UnifIsCorrect(n / 2, k - 1, u); } } - lemma UnifCorrectnessCaseKGreaterOneMOdd(n: nat, k: nat, m: nat) + lemma UnifCorrectnessCaseMOdd(n: nat, k: nat, u: nat) requires k >= 1 requires Helper.Power(2, k) <= n < Helper.Power(2, k + 1) - requires m % 2 == 1 - ensures UnifIsCorrect(n, k, m) + ensures UnifIsCorrect(n, k, 2 * u + 1) { - var u := m / 2; - assert m == 2 * u + 1; + var m := 2 * u + 1; calc { RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); == { SampleCaseSplit(n, m); } @@ -335,7 +226,6 @@ module UniformPowerOfTwoCorrectness { 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; - assert UnifIsCorrect(n, k, m); } } From 963562ef92b3eb57254566ddb181ce7b6f8b1ee0 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Wed, 4 Oct 2023 20:14:12 -0400 Subject: [PATCH 5/9] SImplify UniformPowerOfTwo further --- .../UniformPowerOfTwo/Correctness.dfy | 375 +++--------------- 1 file changed, 65 insertions(+), 310 deletions(-) diff --git a/src/Distributions/UniformPowerOfTwo/Correctness.dfy b/src/Distributions/UniformPowerOfTwo/Correctness.dfy index 77f893ae..3d6863f9 100644 --- a/src/Distributions/UniformPowerOfTwo/Correctness.dfy +++ b/src/Distributions/UniformPowerOfTwo/Correctness.dfy @@ -66,17 +66,9 @@ module UniformPowerOfTwoCorrectness { } assert e == preimage; } - - if k == 0 { - assert n == 1; - UnifCorrectness(n, k); - assert UnifIsCorrect(n, k, m); - } else { - assert n > 1; - Helper.Power2OfLog2Floor(n); - UnifCorrectness(n, k); - assert UnifIsCorrect(n, k, m); - } + Helper.Power2OfLog2Floor(n); + UnifCorrectness(n, k); + assert UnifIsCorrect(n, k, m); } // See PROB_BERN_UNIF_LT in HOL implementation. @@ -133,102 +125,47 @@ module UniformPowerOfTwoCorrectness { forall m: nat ensures UnifIsCorrect(n, k, m) { assert n >= 1 by { Helper.PowerGreater0(2, k); } if k == 0 { - UnifCorrectnessCaseNOne(m); + if m == 0 { + assert (iset s | Model.Sample(1)(s).0 == m) == (iset s); + } else { + assert (iset s | Model.Sample(1)(s).0 == m) == iset{}; + } + RandomNumberGenerator.RNGHasMeasure(); } else { - if m % 2 == 0 { - UnifCorrectnessCaseMEven(n, k, m / 2); + var u := m / 2; + calc { + RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); + == { SampleCaseSplit(n, m); } + RandomNumberGenerator.mu(iset s | 2 * Model.Sample(n / 2)(s).0 + (m % 2) == m) / 2.0; + == { assert (iset s | 2 * Model.Sample(n / 2)(s).0 + (m % 2) == m) == (iset s | Model.Sample(n / 2)(s).0 == u); } + RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == u) / 2.0; + } + 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); + == + RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == u) / 2.0; + == + (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 { - UnifCorrectnessCaseMOdd(n, k, m / 2); + assert u >= Helper.Power(2, k - 1); + 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; } } } } - lemma UnifCorrectnessCaseNOne(m: nat) - ensures UnifIsCorrect(1, 0, m) - { - assert Helper.Power(2, 0) == 1; - if m == 0 { - assert (iset s | Model.Sample(1)(s).0 == m) == (iset s); - } else { - assert (iset s | Model.Sample(1)(s).0 == m) == iset{}; - } - RandomNumberGenerator.RNGHasMeasure(); - } - - lemma UnifCorrectnessCaseMEven(n: nat, k: nat, u: nat) - requires k >= 1 - requires Helper.Power(2, k) <= n < Helper.Power(2, k + 1) - ensures UnifIsCorrect(n, k, 2 * u) - { - var m := 2 * u; - calc { - RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); - == { SampleCaseSplit(n, m); } - RandomNumberGenerator.mu(iset s | 2 * Model.Sample(n / 2)(s).0 == m) / 2.0; - == { assert (iset s | 2 * Model.Sample(n / 2)(s).0 == m) == (iset s | Model.Sample(n / 2)(s).0 == u); } - RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == u) / 2.0; - } - 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 { - UnifCorrectness(n / 2, k - 1); - assert UnifIsCorrect(n / 2, k - 1, u); - } - calc { - RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); - == - RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == u) / 2.0; - == - (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 / 2, k - 1, u); - } else { - assert u >= Helper.Power(2, k - 1); - 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; - } - } - - lemma UnifCorrectnessCaseMOdd(n: nat, k: nat, u: nat) - requires k >= 1 - requires Helper.Power(2, k) <= n < Helper.Power(2, k + 1) - ensures UnifIsCorrect(n, k, 2 * u + 1) - { - var m := 2 * u + 1; - calc { - RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); - == { SampleCaseSplit(n, m); } - RandomNumberGenerator.mu(iset s | 2 * Model.Sample(n / 2)(s).0 + 1 == m) / 2.0; - == { assert (iset s | 2 * Model.Sample(n / 2)(s).0 + 1 == m) == (iset s | Model.Sample(n / 2)(s).0 == u); } - RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == u) / 2.0; - } - 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); - == - RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == u) / 2.0; - == - (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); - 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; - } - } - // Equation (4.7) lemma SampleIsIndepFn(n: nat) requires n >= 1 @@ -342,14 +279,12 @@ module UniformPowerOfTwoCorrectness { } } - lemma SampleCorrectnessIff(n: nat, s: RandomNumberGenerator.RNG, m: nat) + lemma SampleIff(n: nat, s: RandomNumberGenerator.RNG, m: nat) requires n >= 2 ensures var a := Model.Sample(n / 2)(s).0; var b := Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; - Model.Sample(n)(s).0 == m - <==> - (b && 2*a + 1 == m) || (!b && 2*a == m) + Model.Sample(n)(s).0 == m <==> (2*a + (if b then 1 else 0) == m) { var (a, s') := Model.Sample(n / 2)(s); var (b, s'') := Monad.Deconstruct(s'); @@ -368,218 +303,49 @@ module UniformPowerOfTwoCorrectness { } } - lemma SampleCorrectnessEvenCaseIff(n: nat, s: RandomNumberGenerator.RNG, m: nat) - requires m % 2 == 0 - requires n >= 2 - ensures - var a := Model.Sample(n / 2)(s).0; - var b := Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; - Model.Sample(n)(s).0 == m <==> (!b && 2*a == m) - { - var a: nat := Model.Sample(n / 2)(s).0; - var b := Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; - if Model.Sample(n)(s).0 == m { - if (b && 2*a + 1 == m) { - assert m % 2 == 1 by { - Helper.DivModAddMultiple(2, 1, a); - } - assert m % 2 == 0; - assert false; - } - assert !(b && 2*a + 1 == m) ==> (!b && 2*a == m) by { - SampleCorrectnessIff(n, s, m); - assert (b && 2*a + 1 == m) || (!b && 2*a == m); - } - } - if (!b && 2*a == m) { - assert (b && 2*a + 1 == m) || (!b && 2*a == m); - assert Model.Sample(n)(s).0 == m by { SampleCorrectnessIff(n, s, m); } - } - } - - lemma SampleOddCaseIff(n: nat, s: RandomNumberGenerator.RNG, m: nat) - requires m % 2 == 1 - requires n >= 2 - ensures - var a := Model.Sample(n / 2)(s).0; - var b := Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; - Model.Sample(n)(s).0 == m <==> (b && 2*a + 1 == m) - { - var a := Model.Sample(n / 2)(s).0; - var b := Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; - if Model.Sample(n)(s).0 == m { - if (!b && 2*a == m) { - assert m % 2 == 0 by { assert m / 2 == a; } - assert m % 2 == 1; - } - assert !(!b && 2*a == m) ==> (b && 2*a + 1 == m) by { - SampleCorrectnessIff(n, s, m); - assert (b && 2*a + 1 == m) || (!b && 2*a == m); - } - } - if (b && 2*a + 1 == m) { - assert (b && 2*a + 1 == m) || (!b && 2*a == m); - assert Model.Sample(n)(s).0 == m by { SampleCorrectnessIff(n, s, m); } - } - } - - lemma SampleEvenCaseSetEquality(n: nat, m: nat) - requires m % 2 == 0 + lemma SampleSetEquality(n: nat, m: nat) requires n >= 2 ensures var b_of := (s: RandomNumberGenerator.RNG) => Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; var a_of := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).0; - (iset s | Model.Sample(n)(s).0 == m) == (iset s | !b_of(s) && 2*a_of(s) == m) + (iset s | Model.Sample(n)(s).0 == m) == (iset s | 2*a_of(s) + (if b_of(s) then 1 else 0) == m) { var b_of := (s: RandomNumberGenerator.RNG) => Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; var a_of := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).0; - forall s ensures Model.Sample(n)(s).0 == m <==> (!b_of(s) && 2*a_of(s) == m) { - SampleCorrectnessEvenCaseIff(n, s, m); + forall s ensures Model.Sample(n)(s).0 == m <==> (2 * a_of(s) + (if b_of(s) then 1 else 0) == m) { + SampleIff(n, s, m); } } - lemma SampleOddCaseSetEquality(n: nat, m: nat) - requires m % 2 == 1 - requires n >= 2 - ensures - var b_of := (s: RandomNumberGenerator.RNG) => Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; - var a_of := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).0; - (iset s | Model.Sample(n)(s).0 == m) == (iset s | b_of(s) && 2*a_of(s) + 1 == m) - { - var b_of := (s: RandomNumberGenerator.RNG) => Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; - var a_of := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).0; - forall s ensures Model.Sample(n)(s).0 == m <==> (b_of(s) && 2*a_of(s) + 1 == m) { - SampleOddCaseIff(n, s, m); - } - } - - lemma {:vcs_split_on_every_assert} SampleEvenCase(n: nat, m: nat) - requires m % 2 == 0 - requires n >= 2 - ensures RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m) == RandomNumberGenerator.mu(iset s | 2*Model.Sample(n / 2)(s).0 == m) / 2.0 - { - var a_of := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).0; - var b_of := (s: RandomNumberGenerator.RNG) => Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; - var A: iset := (iset x | 2*x == m); - var E: iset := (iset s | Monad.Deconstruct(s).0 == false); - var f := Sample1(n / 2); - - var e1 := (iset s | Sample1(n / 2)(s) in E); - var e2 := (iset s | Model.Sample(n / 2)(s).0 in A); - - assert Eq1: (iset s | !b_of(s)) == e1 by { - forall s ensures !b_of(s) <==> Model.Sample(n / 2)(s).1 in E { - } - } - - assert Eq2: (iset s | 2*a_of(s) == m) == e2 by { - forall s ensures 2*a_of(s) == m <==> Model.Sample(n / 2)(s).0 in A { - } - } - - assert Eq3: (iset s | 2*a_of(s) == m) == (iset s | 2*Model.Sample(n / 2)(s).0 == m) by { - forall s ensures 2*a_of(s) == m <==> 2*Model.Sample(n / 2)(s).0 == m { - } - } - - assert Eq4: e1 == MeasureTheory.PreImage(Sample1(n / 2), E) by { - forall s ensures Model.Sample(n / 2)(s).1 in E <==> f(s) in E { - } - } - - assert EMeasure: E in RandomNumberGenerator.event_space && RandomNumberGenerator.mu(E) == 0.5 by { - assert E == (iset s | Monad.Head(s) == false); - Monad.HeadIsMeasurable(false); - } - - assert Indep: RandomNumberGenerator.mu(e1 * e2) == RandomNumberGenerator.mu(e1) * RandomNumberGenerator.mu(e2) by { - assert e1 == (iset s | Model.Sample(n / 2)(s).1 in E) by { - forall s ensures s in e1 <==> Model.Sample(n / 2)(s).1 in E { - } - } - assert MeasureTheory.AreIndepEvents(RandomNumberGenerator.event_space, RandomNumberGenerator.mu, e1, e2) by { - assert Independence.IsIndepFunction(Model.Sample(n / 2)) by { - assert Independence.IsIndepFn(Model.Sample(n / 2)) by { - SampleIsIndepFn(n / 2); - } - Independence.IsIndepFnImpliesIsIndepFunction(Model.Sample(n / 2)); - } - assert E in RandomNumberGenerator.event_space by { reveal EMeasure; } - assert Independence.IsIndepFunctionCondition(Model.Sample(n / 2), A, E); - } - Independence.AreIndepEventsConjunctElimination(e1, e2); - } - - assert Prob: 0.5 == RandomNumberGenerator.mu(e1) by { - calc { - 0.5; - == { reveal EMeasure; } - RandomNumberGenerator.mu(E); - == { reveal EMeasure; SampleIsMeasurePreserving(n / 2); } - RandomNumberGenerator.mu(MeasureTheory.PreImage(Sample1(n / 2), E)); - == { reveal Eq4; } - RandomNumberGenerator.mu(e1); - } - } - - assert Inter: (iset s | !b_of(s) && 2*a_of(s) == m) == (iset s | !b_of(s)) * (iset s | 2*a_of(s) == m) by { - forall s ensures !b_of(s) && 2*a_of(s) == m <==> !b_of(s) && 2*a_of(s) == m { - } - } - - assert MulSub: RandomNumberGenerator.mu(e1) * RandomNumberGenerator.mu(e2) == 0.5 * RandomNumberGenerator.mu(e2) by { - reveal EMeasure; - assert RandomNumberGenerator.mu(e1) == 0.5 by { reveal Prob; } - assert RandomNumberGenerator.mu(e1) == 0.5 ==> RandomNumberGenerator.mu(e1) * RandomNumberGenerator.mu(e2) == 0.5 * RandomNumberGenerator.mu(e2); - } - - calc { - RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); - == { SampleEvenCaseSetEquality(n, m); } - RandomNumberGenerator.mu(iset s | !b_of(s) && 2*a_of(s) == m); - == { reveal Inter; } - RandomNumberGenerator.mu((iset s | !b_of(s)) * (iset s | 2*a_of(s) == m)); - == { reveal Eq1; reveal Eq2; } - RandomNumberGenerator.mu(e1 * e2); - == { reveal Indep; } - RandomNumberGenerator.mu(e1) * RandomNumberGenerator.mu(e2); - == { reveal MulSub; } - 0.5 * RandomNumberGenerator.mu(e2); - == { Helper.DivisionByTwo(RandomNumberGenerator.mu(e2)); } - RandomNumberGenerator.mu(e2) / 2.0; - == { reveal Eq2; } - RandomNumberGenerator.mu(iset s | 2*a_of(s) == m) / 2.0; - == { reveal Eq3; } - RandomNumberGenerator.mu(iset s | 2*Model.Sample(n / 2)(s).0 == m) / 2.0; - } - } - - lemma SampleOddCase(n: nat, m: nat) - requires m % 2 == 1 + lemma SampleCaseSplit(n: nat, m: nat) requires n >= 2 - ensures RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m) == RandomNumberGenerator.mu(iset s | 2*Model.Sample(n / 2)(s).0 + 1 == m) / 2.0 + ensures RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m) == RandomNumberGenerator.mu(iset s | 2 * Model.Sample(n / 2)(s).0 + m % 2 == m) / 2.0 { var a_of := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).0; var b_of := (s: RandomNumberGenerator.RNG) => Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; - var A: iset := (iset x | 2*x + 1 == m); - var E: iset := (iset s | Monad.Deconstruct(s).0 == true); + var A: iset := (iset x | 2*x + m % 2 == m); + var E: iset := (iset s | Monad.Deconstruct(s).0 <==> m % 2 == 1); var f := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).1; var e1 := (iset s | Model.Sample(n / 2)(s).1 in E); var e2 := (iset s | Model.Sample(n / 2)(s).0 in A); - assert Eq1: (iset s | b_of(s)) == e1 by { - forall s ensures b_of(s) <==> Model.Sample(n / 2)(s).1 in E { + assert Eq1: (iset s | b_of(s) <==> m % 2 == 1) == e1 by { + forall s ensures (b_of(s) <==> m % 2 == 1) <==> Model.Sample(n / 2)(s).1 in E { } } - assert Eq2: (iset s | 2*a_of(s) + 1 == m) == e2 by { - forall s ensures 2*a_of(s) + 1 == m <==> Model.Sample(n / 2)(s).0 in A { + assert Eq2: (iset s | 2*a_of(s) + m % 2 == m) == e2 by { + forall s ensures 2*a_of(s) + m % 2 == m <==> Model.Sample(n / 2)(s).0 in A { } } - assert Eq3: (iset s | 2*a_of(s) + 1 == m) == (iset s | 2*Model.Sample(n / 2)(s).0 + 1 == m) by { - forall s ensures 2*a_of(s) + 1 == m <==> 2*Model.Sample(n / 2)(s).0 + 1 == m { + assert SplitEvent: (iset s | 2*a_of(s) + (if b_of(s) then 1 else 0) == m) == (iset s | b_of(s) <==> m % 2 == 1) * (iset s | 2*a_of(s) + m % 2 == m) by { + assume false; + } + + assert Eq3: (iset s | 2*a_of(s) + m % 2 == m) == (iset s | 2*Model.Sample(n / 2)(s).0 + m % 2 == m) by { + forall s ensures 2*a_of(s) + m % 2 == m <==> 2*Model.Sample(n / 2)(s).0 + m % 2 == m { } } @@ -589,8 +355,8 @@ module UniformPowerOfTwoCorrectness { } assert E in RandomNumberGenerator.event_space && RandomNumberGenerator.mu(E) == 0.5 by { - assert E == (iset s | Monad.Head(s) == true); - Monad.HeadIsMeasurable(true); + assert E == (iset s | Monad.Head(s) == (m % 2 == 1)); + Monad.HeadIsMeasurable(m % 2 == 1); } assert Indep: RandomNumberGenerator.mu(e1 * e2) == RandomNumberGenerator.mu(e1) * RandomNumberGenerator.mu(e2) by { @@ -625,10 +391,10 @@ module UniformPowerOfTwoCorrectness { calc { RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); - == { SampleOddCaseSetEquality(n, m); } - RandomNumberGenerator.mu(iset s | b_of(s) && 2*a_of(s) + 1 == m); - == { assert (iset s | b_of(s) && 2*a_of(s) + 1 == m) == (iset s | b_of(s)) * (iset s | 2*a_of(s) + 1 == m); } - RandomNumberGenerator.mu((iset s | b_of(s)) * (iset s | 2*a_of(s) + 1 == m)); + == { SampleSetEquality(n, m); } + RandomNumberGenerator.mu(iset s | 2*a_of(s) + (if b_of(s) then 1 else 0) == m); + == { reveal SplitEvent; } + RandomNumberGenerator.mu((iset s | b_of(s) <==> m % 2 == 1) * (iset s | 2*a_of(s) + m % 2 == m)); == { reveal Eq1; reveal Eq2; } RandomNumberGenerator.mu(e1 * e2); == { reveal Indep; } @@ -638,20 +404,9 @@ module UniformPowerOfTwoCorrectness { == RandomNumberGenerator.mu(e2) / 2.0; == { reveal Eq2; } - RandomNumberGenerator.mu(iset s | 2*a_of(s) + 1 == m) / 2.0; + RandomNumberGenerator.mu(iset s | 2*a_of(s) + m % 2 == m) / 2.0; == { reveal Eq3; } - RandomNumberGenerator.mu(iset s | 2*Model.Sample(n / 2)(s).0 + 1 == m) / 2.0; - } - } - - lemma SampleCaseSplit(n: nat, m: nat) - requires n >= 2 - ensures RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m) == if m % 2 == 0 then RandomNumberGenerator.mu(iset s | 2*Model.Sample(n / 2)(s).0 == m) / 2.0 else RandomNumberGenerator.mu(iset s | 2*Model.Sample(n / 2)(s).0 + 1 == m) / 2.0 - { - if m % 2 == 0 { - SampleEvenCase(n, m); - } else { - SampleOddCase(n, m); + RandomNumberGenerator.mu(iset s | 2*Model.Sample(n / 2)(s).0 + m % 2 == m) / 2.0; } } From a6221db9908a0bf3fa0f148f089d1c3819bf5c46 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Thu, 5 Oct 2023 10:30:52 -0400 Subject: [PATCH 6/9] Remove assume false --- audit.log | 5 +-- .../UniformPowerOfTwo/Correctness.dfy | 44 +++++++++---------- 2 files changed, 23 insertions(+), 26 deletions(-) diff --git a/audit.log b/audit.log index 3bec936d..2a7e0f02 100644 --- a/audit.log +++ b/audit.log @@ -1,7 +1,6 @@ src/Distributions/Coin/Interface.dfy(23,6): CoinSample: Definition has `assume {:axiom}` statement in body. -src/Distributions/Uniform/Correctness.dfy(153,17): SampleIsIndepFn: Declaration has explicit `{:axiom}` attribute. -src/Distributions/Uniform/Implementation.dfy(23,6): UniformSample: Definition has `assume {:axiom}` statement in body. -src/Distributions/Uniform/Implementation.dfy(46,6): UniformSample: Definition has `assume {:axiom}` statement in body. +src/Distributions/Uniform/Correctness.dfy(154,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/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. diff --git a/src/Distributions/UniformPowerOfTwo/Correctness.dfy b/src/Distributions/UniformPowerOfTwo/Correctness.dfy index 3d6863f9..60495865 100644 --- a/src/Distributions/UniformPowerOfTwo/Correctness.dfy +++ b/src/Distributions/UniformPowerOfTwo/Correctness.dfy @@ -319,33 +319,37 @@ module UniformPowerOfTwoCorrectness { lemma SampleCaseSplit(n: nat, m: nat) requires n >= 2 - ensures RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m) == RandomNumberGenerator.mu(iset s | 2 * Model.Sample(n / 2)(s).0 + m % 2 == m) / 2.0 + ensures RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m) == RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == m / 2) / 2.0 { var a_of := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).0; var b_of := (s: RandomNumberGenerator.RNG) => Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; - var A: iset := (iset x | 2*x + m % 2 == m); - var E: iset := (iset s | Monad.Deconstruct(s).0 <==> m % 2 == 1); + var A: iset := (iset x | x == m / 2); + var E: iset := (iset s | m % 2 == if Monad.Deconstruct(s).0 then 1 else 0); var f := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).1; var e1 := (iset s | Model.Sample(n / 2)(s).1 in E); var e2 := (iset s | Model.Sample(n / 2)(s).0 in A); + var e3 := (iset s | 2*a_of(s) + (if b_of(s) then 1 else 0) == m); - assert Eq1: (iset s | b_of(s) <==> m % 2 == 1) == e1 by { - forall s ensures (b_of(s) <==> m % 2 == 1) <==> Model.Sample(n / 2)(s).1 in E { + assert SplitEvent: e3 == e1 * e2 by { + forall s ensures s in e3 <==> s in e1 && s in e2 { + calc { + s in e3; + 2*a_of(s) + (if b_of(s) then 1 else 0) == m; + (m % 2 == if b_of(s) then 1 else 0) && a_of(s) == m / 2; + s in e1 && s in e2; + } } } - assert Eq2: (iset s | 2*a_of(s) + m % 2 == m) == e2 by { - forall s ensures 2*a_of(s) + m % 2 == m <==> Model.Sample(n / 2)(s).0 in A { + assert Eq2: (iset s | a_of(s) == m / 2) == e2 by { + forall s ensures a_of(s) == m / 2 <==> Model.Sample(n / 2)(s).0 in A { } } - assert SplitEvent: (iset s | 2*a_of(s) + (if b_of(s) then 1 else 0) == m) == (iset s | b_of(s) <==> m % 2 == 1) * (iset s | 2*a_of(s) + m % 2 == m) by { - assume false; - } - - assert Eq3: (iset s | 2*a_of(s) + m % 2 == m) == (iset s | 2*Model.Sample(n / 2)(s).0 + m % 2 == m) by { - forall s ensures 2*a_of(s) + m % 2 == m <==> 2*Model.Sample(n / 2)(s).0 + m % 2 == m { + assert Eq3: (iset s | a_of(s) == m / 2) == (iset s | Model.Sample(n / 2)(s).0 == m / 2) by { + forall s ensures a_of(s) == m / 2 <==> Model.Sample(n / 2)(s).0 == m / 2 { + assert a_of(s) == Model.Sample(n / 2)(s).0; } } @@ -385,28 +389,22 @@ module UniformPowerOfTwoCorrectness { } } - assert Prob2: RandomNumberGenerator.mu(e1) * RandomNumberGenerator.mu(e2) == 0.5 * RandomNumberGenerator.mu(e2) by { - reveal Prob; - } - calc { RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); == { SampleSetEquality(n, m); } - RandomNumberGenerator.mu(iset s | 2*a_of(s) + (if b_of(s) then 1 else 0) == m); + RandomNumberGenerator.mu(e3); == { reveal SplitEvent; } - RandomNumberGenerator.mu((iset s | b_of(s) <==> m % 2 == 1) * (iset s | 2*a_of(s) + m % 2 == m)); - == { reveal Eq1; reveal Eq2; } RandomNumberGenerator.mu(e1 * e2); == { reveal Indep; } RandomNumberGenerator.mu(e1) * RandomNumberGenerator.mu(e2); - == { reveal Prob2; } + == { reveal Prob; } 0.5 * RandomNumberGenerator.mu(e2); == RandomNumberGenerator.mu(e2) / 2.0; == { reveal Eq2; } - RandomNumberGenerator.mu(iset s | 2*a_of(s) + m % 2 == m) / 2.0; + RandomNumberGenerator.mu(iset s | a_of(s) == m / 2) / 2.0; == { reveal Eq3; } - RandomNumberGenerator.mu(iset s | 2*Model.Sample(n / 2)(s).0 + m % 2 == m) / 2.0; + RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == m / 2) / 2.0; } } From 7117da7304e6c6589b47da4655c1e20101c5fea4 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Thu, 5 Oct 2023 10:39:06 -0400 Subject: [PATCH 7/9] inline --- .../UniformPowerOfTwo/Correctness.dfy | 49 +++++++------------ 1 file changed, 19 insertions(+), 30 deletions(-) diff --git a/src/Distributions/UniformPowerOfTwo/Correctness.dfy b/src/Distributions/UniformPowerOfTwo/Correctness.dfy index 60495865..8e55fcd9 100644 --- a/src/Distributions/UniformPowerOfTwo/Correctness.dfy +++ b/src/Distributions/UniformPowerOfTwo/Correctness.dfy @@ -135,7 +135,7 @@ module UniformPowerOfTwoCorrectness { var u := m / 2; calc { RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); - == { SampleCaseSplit(n, m); } + == { SampleProbRecursiveHalf(n, m); } RandomNumberGenerator.mu(iset s | 2 * Model.Sample(n / 2)(s).0 + (m % 2) == m) / 2.0; == { assert (iset s | 2 * Model.Sample(n / 2)(s).0 + (m % 2) == m) == (iset s | Model.Sample(n / 2)(s).0 == u); } RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == u) / 2.0; @@ -279,30 +279,6 @@ module UniformPowerOfTwoCorrectness { } } - lemma SampleIff(n: nat, s: RandomNumberGenerator.RNG, m: nat) - requires n >= 2 - ensures - var a := Model.Sample(n / 2)(s).0; - var b := Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; - Model.Sample(n)(s).0 == m <==> (2*a + (if b then 1 else 0) == m) - { - var (a, s') := Model.Sample(n / 2)(s); - var (b, s'') := Monad.Deconstruct(s'); - calc { - Model.Sample(n)(s).0; - == - Monad.Bind(Model.Sample(n / 2), Model.UnifStep)(s).0; - == - Model.UnifStep(a)(s').0; - == - Monad.Bind(Monad.Deconstruct, b => Monad.Return(if b then 2*a + 1 else 2*a))(s').0; - == - Monad.Return(if b then 2*a + 1 else 2*a)(s'').0; - == - if b then 2*a + 1 else 2*a; - } - } - lemma SampleSetEquality(n: nat, m: nat) requires n >= 2 ensures @@ -313,11 +289,25 @@ module UniformPowerOfTwoCorrectness { var b_of := (s: RandomNumberGenerator.RNG) => Monad.Deconstruct(Model.Sample(n / 2)(s).1).0; var a_of := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).0; forall s ensures Model.Sample(n)(s).0 == m <==> (2 * a_of(s) + (if b_of(s) then 1 else 0) == m) { - SampleIff(n, s, m); + var (a, s') := Model.Sample(n / 2)(s); + var (b, s'') := Monad.Deconstruct(s'); + calc { + Model.Sample(n)(s).0; + == + Monad.Bind(Model.Sample(n / 2), Model.UnifStep)(s).0; + == + Model.UnifStep(a)(s').0; + == + Monad.Bind(Monad.Deconstruct, b => Monad.Return(if b then 2*a + 1 else 2*a))(s').0; + == + Monad.Return(if b then 2*a + 1 else 2*a)(s'').0; + == + if b then 2*a + 1 else 2*a; + } } } - lemma SampleCaseSplit(n: nat, m: nat) + lemma SampleProbRecursiveHalf(n: nat, m: nat) requires n >= 2 ensures RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m) == RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == m / 2) / 2.0 { @@ -377,7 +367,7 @@ module UniformPowerOfTwoCorrectness { Independence.AreIndepEventsConjunctElimination(e1, e2); } - assert Prob: 0.5 == RandomNumberGenerator.mu(e1) by { + assert ProbE1: 0.5 == RandomNumberGenerator.mu(e1) by { calc { 0.5; == @@ -397,7 +387,7 @@ module UniformPowerOfTwoCorrectness { RandomNumberGenerator.mu(e1 * e2); == { reveal Indep; } RandomNumberGenerator.mu(e1) * RandomNumberGenerator.mu(e2); - == { reveal Prob; } + == { reveal ProbE1; } 0.5 * RandomNumberGenerator.mu(e2); == RandomNumberGenerator.mu(e2) / 2.0; @@ -407,5 +397,4 @@ module UniformPowerOfTwoCorrectness { RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == m / 2) / 2.0; } } - } From 04e42b8f32aab04558747214c717d6f300c97ed7 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Thu, 5 Oct 2023 10:46:24 -0400 Subject: [PATCH 8/9] format --- src/Distributions/Uniform/Correctness.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Distributions/Uniform/Correctness.dfy b/src/Distributions/Uniform/Correctness.dfy index 65ee8863..7982286b 100644 --- a/src/Distributions/Uniform/Correctness.dfy +++ b/src/Distributions/Uniform/Correctness.dfy @@ -99,11 +99,11 @@ module UniformCorrectness { assert i < Helper.Power(2, Helper.Log2Floor(2 * n)) by { calc { i; - < + < n; - < { Helper.Power2OfLog2Floor(n); } + < { Helper.Power2OfLog2Floor(n); } Helper.Power(2, Helper.Log2Floor(n) + 1); - == { reveal Log2Double; } + == { reveal Log2Double; } Helper.Power(2, Helper.Log2Floor(2 * n)); } } From f491ea23d1de37dbc254f4e6bc886cc5b525903a Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Thu, 5 Oct 2023 11:12:54 -0400 Subject: [PATCH 9/9] fix timeout --- src/Distributions/UniformPowerOfTwo/Correctness.dfy | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/Distributions/UniformPowerOfTwo/Correctness.dfy b/src/Distributions/UniformPowerOfTwo/Correctness.dfy index 8e55fcd9..1909c457 100644 --- a/src/Distributions/UniformPowerOfTwo/Correctness.dfy +++ b/src/Distributions/UniformPowerOfTwo/Correctness.dfy @@ -131,14 +131,11 @@ module UniformPowerOfTwoCorrectness { assert (iset s | Model.Sample(1)(s).0 == m) == iset{}; } RandomNumberGenerator.RNGHasMeasure(); + assert UnifIsCorrect(n, k, m); } else { var u := m / 2; - calc { - RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); - == { SampleProbRecursiveHalf(n, m); } - RandomNumberGenerator.mu(iset s | 2 * Model.Sample(n / 2)(s).0 + (m % 2) == m) / 2.0; - == { assert (iset s | 2 * Model.Sample(n / 2)(s).0 + (m % 2) == m) == (iset s | Model.Sample(n / 2)(s).0 == u); } - RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == u) / 2.0; + 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); } 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 { @@ -148,7 +145,7 @@ module UniformPowerOfTwoCorrectness { } calc { RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m); - == + == { reveal Recursive; } RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == u) / 2.0; == (1.0 / Helper.Power(2, k - 1) as real) / 2.0; @@ -158,6 +155,7 @@ module UniformPowerOfTwoCorrectness { 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;