Uniform as primitive

audit.log

@@ -1,21 +1,11 @@
-src/DafnyVMC.dfy(28,6): UniformPowerOfTwoSample: Definition has `assume {:axiom}` statement in body. 
-src/Math/Analysis/Limits.dfy(126,17): Sandwich: Declaration has explicit `{:axiom}` attribute. 
-src/Math/Analysis/Reals.dfy(35,17): LeastUpperBoundProperty: Declaration has explicit `{:axiom}` attribute. 
-src/Math/Measures.dfy(125,17): ProbabilityLe1: Declaration has explicit `{:axiom}` attribute. 
-src/Math/Measures.dfy(130,17): IsMonotonic: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(105,17): BindIsIndep: Declaration has explicit `{:axiom}` attribute. 
+src/DafnyVMC.dfy(30,6): UniformSample: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/Uniform/Correctness.dfy(31,17): UniformFullCorrectness: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/Uniform/Correctness.dfy(37,17): SampleIsIndep: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/Uniform/Model.dfy(18,33): Sample: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/Uniform/Model.dfy(31,17): SampleCoin: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/Uniform/Model.dfy(34,17): SampleBound: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/Independence.dfy(30,27): IsIndep: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/Independence.dfy(55,6): ResultsIndependent: Definition has `assume {:axiom}` statement in body. 
-src/ProbabilisticProgramming/Independence.dfy(59,17): IsIndepImpliesMeasurableBool: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(77,17): IsIndepImpliesMeasurableNat: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(82,17): IsIndepImpliesIsIndepFunction: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(87,17): CoinIsIndep: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(91,17): ReturnIsIndep: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Loops.dfy(361,17): EnsureWhileTerminates: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Loops.dfy(371,17): UntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Loops.dfy(404,4): EnsureUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body. 
-src/ProbabilisticProgramming/Loops.dfy(427,4): WhileIsIndep: Definition has `assume {:axiom}` statement in body. 
+src/ProbabilisticProgramming/Independence.dfy(60,17): IsIndepImpliesIsIndepFunction: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Independence.dfy(64,17): MapIsIndep: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/RandomSource.dfy(50,17): ProbIsProbabilityMeasure: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/RandomSource.dfy(54,17): CoinHasProbOneHalf: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/RandomSource.dfy(61,17): MeasureHeadDrop: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/RandomSource.dfy(67,17): TailIsMeasurePreserving: Declaration has explicit `{:axiom}` attribute. 

src/DafnyVMC.dfy

@@ -6,25 +6,27 @@
 module {:extern} DafnyVMCPartMaterial {
   class {:extern} Random {
     // For running Dafny native testing with standard SecureRandom rng
-    static method {:extern "UniformPowerOfTwoSample"} ExternUniformPowerOfTwoSample(n: nat) returns (u: nat)
+    static method {:extern "UniformSample"} ExternUniformSample(n: nat) returns (u: nat)
   }
 }
 
 module {:extern "DafnyVMCPart"} DafnyVMC {
   import DafnyVMCTrait
   import DafnyVMCPartMaterial
   import Monad
-  import UniformPowerOfTwo
+  import Uniform
+  import Pos
 
   class Random extends DafnyVMCTrait.RandomTrait {
     constructor {:extern} ()
 
-    method UniformPowerOfTwoSample(n: nat) returns (u: nat)
-      requires n >= 1
-      modifies this
-      ensures UniformPowerOfTwo.Model.Sample(n)(old(s)) == Monad.Result(u, s)
+    method UniformSample(n: Pos.pos) returns (u: nat)
+      modifies `s
+      decreases *
+      ensures u < n
+      ensures Uniform.Model.Sample(n)(old(s)) == Monad.Result(u, s)
     {
-      u := DafnyVMCPartMaterial.Random.ExternUniformPowerOfTwoSample(n);
+      u := DafnyVMCPartMaterial.Random.ExternUniformSample(n);
       assume {:axiom} false; // assume correctness of extern implementation
     }
   }

src/DafnyVMCTrait.dfy

@@ -1,32 +1,17 @@
 
 module DafnyVMCTrait {
 
-  import UniformPowerOfTwo
+  import Uniform
 
   import FisherYates
 
   import opened Pos
 
-  trait {:termination false} RandomTrait extends  UniformPowerOfTwo.Implementation.Trait, FisherYates.Implementation.Trait {
-
-    method {:verify false} UniformSample (n: pos)
-      returns (o: nat)
-      modifies this
-      decreases *
-    {
-      var x := UniformPowerOfTwoSample(2 * n);
-      while ! (x < n)
-        decreases *
-      {
-        x := UniformPowerOfTwoSample(2 * n);
-      }
-      var r := x;
-      o := r;
-    }
+  trait {:termination false} RandomTrait extends Uniform.Interface.Trait, FisherYates.Implementation.Trait {
 
     method {:verify false} BernoulliSample (num: nat, den: pos)
       returns (o: bool)
-      requires num <= den 
+      requires num <= den
       modifies this
       decreases *
     {
@@ -36,7 +21,7 @@ module DafnyVMCTrait {
 
     method {:verify false} BernoulliExpNegSampleUnitLoop (num: nat, den: pos, state: (bool,pos))
       returns (o: (bool,pos))
-      requires num <= den 
+      requires num <= den
       modifies this
       decreases *
     {
@@ -46,7 +31,7 @@ module DafnyVMCTrait {
 
     method {:verify false} BernoulliExpNegSampleUnitAux (num: nat, den: pos)
       returns (o: nat)
-      requires num <= den 
+      requires num <= den
       modifies this
       decreases *
     {
@@ -62,7 +47,7 @@ module DafnyVMCTrait {
 
     method {:verify false} BernoulliExpNegSampleUnit (num: nat, den: pos)
       returns (o: bool)
-      requires num <= den 
+      requires num <= den
       modifies this
       decreases *
     {
@@ -140,7 +125,7 @@ module DafnyVMCTrait {
 
     method {:verify false} DiscreteLaplaceSampleLoopIn2Aux (num: nat, den: pos, K: (bool,pos))
       returns (o: (bool,pos))
-      requires num <= den 
+      requires num <= den
       modifies this
       decreases *
     {
@@ -226,6 +211,6 @@ module DafnyVMCTrait {
     }
 
 
-}
+  }
 
 }

src/Distributions/Coin/Implementation.dfy

@@ -7,17 +7,18 @@ module Coin.Implementation {
   import Model
   import Monad
   import Interface
-  import UniformPowerOfTwo
+  import Uniform
 
   trait {:termination false} Trait extends Interface.Trait {
 
     method CoinSample() returns (b: bool)
       modifies `s
+      decreases *
       ensures Model.Sample(old(s)) == Monad.Result(b, s)
     {
-      var x := UniformPowerOfTwoSample(2);
+      var x := UniformSample(2);
       b := if x == 1 then true else false;
-      reveal UniformPowerOfTwo.Model.Sample();
+      Uniform.Model.SampleCoin(old(s));
     }
 
   }

src/Distributions/Coin/Interface.dfy

@@ -7,12 +7,13 @@ module Coin.Interface {
   import Monad
   import Rand
   import Model
-  import UniformPowerOfTwo
+  import Uniform
 
-  trait {:termination false} Trait extends UniformPowerOfTwo.Interface.Trait {
+  trait {:termination false} Trait extends Uniform.Interface.Trait {
 
     method CoinSample() returns (b: bool)
       modifies `s
+      decreases *
       ensures Model.Sample(old(s)) == Monad.Result(b, s)
 
   }

src/Distributions/Uniform/Correctness.dfy

@@ -9,10 +9,7 @@ module Uniform.Correctness {
   import Monad
   import Independence
   import Rand
-  import Quantifier
-  import Loops
   import Measures
-  import UniformPowerOfTwo
   import Model
 
   /************
@@ -31,108 +28,15 @@ module Uniform.Correctness {
 
   // Correctness theorem for Model.Sample
   // Equation (4.12) / PROB_BERN_UNIFORM
-  lemma UniformFullCorrectness(n: nat, i: nat)
+  lemma {:axiom} UniformFullCorrectness(n: nat, i: nat)
     requires 0 <= i < n
     ensures SampleEquals(n, i) in Rand.eventSpace
     ensures Rand.prob(SampleEquals(n, i)) == 1.0 / (n as real)
-  {
-    var equalsI := (x: nat) => x == i;
-
-    assert Independence.IsIndep(Model.Proposal(n)) && Quantifier.WithPosProb(Loops.ProposalIsAccepted(Model.Proposal(n), Model.Accept(n))) by {
-      Model.SampleTerminates(n);
-    }
-
-    Loops.UntilProbabilityFraction(Model.Proposal(n), Model.Accept(n), equalsI);
-    var eventResultEqualsI := Loops.UntilLoopResultHasProperty(Model.Proposal(n), Model.Accept(n), equalsI);
-    var eventProposalAcceptedAndEqualsI := Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), equalsI);
-    var proposalAccepted := Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n));
-
-    assert Fraction: Rand.prob(eventResultEqualsI) == Rand.prob(eventProposalAcceptedAndEqualsI) / Rand.prob(proposalAccepted);
-
-    assert Eq: eventResultEqualsI == SampleEquals(n, i) by {
-      forall s ensures s in eventResultEqualsI <==> s in SampleEquals(n, i) {
-        reveal Model.Sample();
-        assert s in eventResultEqualsI <==> s in SampleEquals(n, i);
-      }
-    }
-
-    assert SampleEquals(n, i) in Rand.eventSpace by {
-      reveal Eq;
-    }
-
-    assert Rand.prob(SampleEquals(n, i)) == 1.0 / (n as real) by {
-      calc {
-        Rand.prob(SampleEquals(n, i));
-        { reveal Eq; }
-        Rand.prob(eventResultEqualsI);
-        { reveal Fraction; }
-        Rand.prob(eventProposalAcceptedAndEqualsI) / Rand.prob(proposalAccepted);
-        { ProbabilityProposalAcceptedAndEqualsI(n, i); }
-        (1.0 / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real)) / Rand.prob(proposalAccepted);
-        { ProbabilityProposalAccepted(n); }
-        (1.0 / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real)) / ((n as real) / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real));
-        { RealArith.SimplifyFractions(1.0, n as real, NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real); }
-        1.0 / (n as real);
-      }
-    }
-  }
-
-  lemma ProbabilityProposalAcceptedAndEqualsI(n: nat, i: nat)
-    requires 0 <= i < n
-    ensures
-      Rand.prob(Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i)) == 1.0 / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real)
-  {
-    var e := Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i);
-    var nextPowerOfTwo := NatArith.Power(2, NatArith.Log2Floor(2 * n));
-    assert iBound: i < nextPowerOfTwo by {
-      calc {
-        i;
-      <
-        n;
-      < { NatArith.NLtPower2Log2FloorOf2N(n); }
-        nextPowerOfTwo;
-      }
-    }
-    assert setEq: Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i) == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i) by {
-      forall s ensures s in e <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i {
-        assert s in e <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i;
-      }
-    }
-    calc {
-      Rand.prob(Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i));
-      { reveal setEq; }
-      Rand.prob(iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i);
-      { reveal iBound; UniformPowerOfTwo.Correctness.UnifCorrectness2(2 * n, i); }
-      1.0 / (nextPowerOfTwo as real);
-    }
-  }
 
-  lemma ProbabilityProposalAccepted(n: nat)
-    requires n >= 1
-    ensures
-      Rand.prob(Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real)
-  {
-    var e := Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n));
-    assert n < NatArith.Power(2, NatArith.Log2Floor(2 * n)) by { NatArith.NLtPower2Log2FloorOf2N(n); }
-    assert Equal: e == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n) by {
-      forall s ensures s in e <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n {
-        calc {
-          s in e;
-          Model.Accept(n)(Model.Proposal(n)(s).value);
-          UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n;
-        }
-      }
-    }
-    assert Rand.prob(Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real) by {
-      calc {
-        Rand.prob(e);
-        { reveal Equal; }
-        Rand.prob(iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n);
-        { UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(2 * n, n); }
-        (n as real) / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real);
-      }
-    }
-  }
+  // Equation (4.10)
+  lemma {:axiom} SampleIsIndep(n: nat)
+    requires n > 0
+    ensures Independence.IsIndep(Model.Sample(n))
 
   // Correctness theorem for Model.IntervalSample
   lemma UniformFullIntervalCorrectness(a: int, b: int, i: int)
@@ -156,21 +60,6 @@ module Uniform.Correctness {
     }
   }
 
-  // Equation (4.10)
-  lemma SampleIsIndep(n: nat)
-    requires n > 0
-    ensures Independence.IsIndep(Model.Sample(n))
-  {
-    assert Independence.IsIndep(Model.Proposal(n)) by {
-      UniformPowerOfTwo.Correctness.SampleIsIndep(2 * n);
-    }
-    assert Loops.UntilTerminatesAlmostSurely(Model.Proposal(n), Model.Accept(n)) by {
-      Model.SampleTerminates(n);
-    }
-    Loops.UntilIsIndep(Model.Proposal(n), Model.Accept(n));
-    reveal Model.Sample();
-  }
-
   lemma IntervalSampleIsIndep(a: int, b: int)
     requires a < b
     ensures Independence.IsIndep(Model.IntervalSample(a, b))

src/Distributions/Uniform/Interface.dfy

@@ -5,17 +5,17 @@
 
 module Uniform.Interface {
   import Monad
-  import Coin
   import Model
-  import UniformPowerOfTwo
   import Pos
+  import Rand
 
-  trait {:termination false} Trait extends UniformPowerOfTwo.Interface.Trait {
+  trait {:termination false} Trait {
+
+    ghost var s: Rand.Bitstream
 
     method UniformSample(n: Pos.pos) returns (u: nat)
       modifies `s
       decreases *
-      requires n > 0
       ensures u < n
       ensures Model.Sample(n)(old(s)) == Monad.Result(u, s)