Simplify UniformPowerOfTwo

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. 

src/Distributions/Uniform/Correctness.dfy

@@ -42,17 +42,15 @@ module Uniform.Correctness {
   // Equation (4.12) / PROB_BERN_UNIFORM
   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(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;
 
@@ -66,63 +64,66 @@ module Uniform.Correctness {
 
     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(n-1)(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 x.2 == e2 by {
-      assert forall s :: c(b(s).0) <==> UniformPowerOfTwo.Model.Sample(n-1)(s).0 < n;
+    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 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 Log2Double: Helper.Log2Floor(2 * n) == Helper.Log2Floor(n) + 1 by { Helper.Log2FloorDef(n); }
 
-        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;
-        }
+    assert UniformFullCorrectnessHelper(n, i) in RandomNumberGenerator.event_space by {
+      reveal X0;
+    }
 
-        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 {
+    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;
-          < { 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);
+          < { Helper.Power2OfLog2Floor(n); }
+            Helper.Power(2, Helper.Log2Floor(n) + 1);
+          == { reveal Log2Double; }
+            Helper.Power(2, Helper.Log2Floor(2 * n));
           }
         }
-        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);
+        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);
+      }
+      calc {
+        RandomNumberGenerator.mu(e);
+        { reveal X0; reveal X1; reveal X2; reveal Fraction; }
+        RandomNumberGenerator.mu(e1) / RandomNumberGenerator.mu(e2);
+        { 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);
       }
     }
   }

src/Distributions/Uniform/Implementation.dfy

@@ -20,14 +20,15 @@ module Uniform.Implementation {
       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);
       }
     }
   }

src/Distributions/Uniform/Model.dfy

@@ -23,14 +23,14 @@ module Uniform.Model {
     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))