Clean up UniformCorrectness and WhileAndUntil

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. 

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 {

src/Distributions/Uniform/Correctness.dfy

@@ -28,7 +28,7 @@ module Uniform.Correctness {
    Definitions
   ************/
 
-  ghost function UniformFullCorrectnessHelper(n: nat, i: nat): iset<RandomNumberGenerator.RNG>
+  ghost function SampleEquals(n: nat, i: nat): iset<RandomNumberGenerator.RNG>
     requires 0 <= i < n
   {
     iset s | Model.Sample(n)(s).0 == i
@@ -42,92 +42,105 @@ 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);
       }
     }
   }
 
+  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;

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<nat>
+    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<int>)
     requires a < 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);
         }
       }
     }

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