Rename lots of stuff

audit.log

@@ -1,5 +1,5 @@
 src/Distributions/BernoulliExpNeg/Correctness.dfy(13,17): Correctness: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(17,17): SampleIsIndepFn: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/BernoulliExpNeg/Correctness.dfy(17,17): SampleIsIndep: Declaration has explicit `{:axiom}` attribute. 
 src/Distributions/BernoulliExpNeg/Implementation.dfy(34,6): BernoulliExpNegSample: Definition has `assume {:axiom}` statement in body. 
 src/Distributions/BernoulliExpNeg/Implementation.dfy(52,6): BernoulliExpNegSampleCaseLe1: Definition has `assume {:axiom}` statement in body. 
 src/Distributions/BernoulliExpNeg/Model.dfy(30,4): GammaReductionLoop: Definition has `assume {:axiom}` statement in body. 
@@ -10,25 +10,23 @@ src/Math/Exponential.dfy(11,17): EvalOne: Declaration has explicit `{:axiom}` at
 src/Math/Exponential.dfy(2,26): Exp: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Exponential.dfy(4,17): FunctionalEquation: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Exponential.dfy(7,17): Increasing: 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(28,27): IsIndepFn: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(34,17): IsIndepFnImpliesFstMeasurableBool: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(38,17): IsIndepFnImpliesFstMeasurableNat: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(42,17): IsIndepFnImpliesSndMeasurable: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(46,17): IsIndepFnImpliesIsIndepFunction: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(51,17): DeconstructIsIndepFn: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(55,17): ReturnIsIndepFn: Declaration has explicit `{:axiom}` attribute. 
+src/Math/Measures.dfy(150,17): CountableSumOfZeroesIsZero: Declaration has explicit `{:axiom}` attribute. 
+src/Math/Measures.dfy(25,4): CountableSum: Definition has `assume {:axiom}` statement in body. 
+src/ProbabilisticProgramming/Independence.dfy(28,27): IsIndep: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Independence.dfy(34,17): IsIndepImpliesFstMeasurableBool: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Independence.dfy(38,17): IsIndepImpliesFstMeasurableNat: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Independence.dfy(42,17): IsIndepImpliesSndMeasurable: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Independence.dfy(46,17): IsIndepImpliesIsIndepFunction: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Independence.dfy(51,17): CoinIsIndep: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Independence.dfy(55,17): ReturnIsIndep: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/Independence.dfy(59,17): IndepFnIsCompositional: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Monad.dfy(136,17): TailIsRNG: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Monad.dfy(140,17): HeadIsMeasurable: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Monad.dfy(147,17): MeasureHeadDrop: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Monad.dfy(153,17): TailIsMeasurePreserving: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/RandomNumberGenerator.dfy(13,21): IsRNG: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/RandomNumberGenerator.dfy(27,17): RNGHasMeasure: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/WhileAndUntil.dfy(165,17): EnsureProbWhileTerminates: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/WhileAndUntil.dfy(171,17): ProbUntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/WhileAndUntil.dfy(183,17): ProbUntilAsBind: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/WhileAndUntil.dfy(197,4): EnsureProbUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body. 
-src/ProbabilisticProgramming/WhileAndUntil.dfy(207,8): ProbWhileIsIndepFn: Definition has `assume {:axiom}` statement in body. 
-src/ProbabilisticProgramming/WhileAndUntil.dfy(39,4): ProbWhile: Definition has `assume {:axiom}` statement in body. 
+src/ProbabilisticProgramming/Loops.dfy(165,17): EnsureWhileTerminates: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Loops.dfy(171,17): UntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Loops.dfy(183,17): UntilAsBind: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Loops.dfy(197,4): EnsureUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body. 
+src/ProbabilisticProgramming/Loops.dfy(207,8): WhileIsIndep: Definition has `assume {:axiom}` statement in body. 
+src/ProbabilisticProgramming/Loops.dfy(39,4): While: Definition has `assume {:axiom}` statement in body. 
+src/ProbabilisticProgramming/Monad.dfy(134,17): CoinHasProbOneHalf: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Monad.dfy(141,17): MeasureHeadDrop: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Monad.dfy(147,17): TailIsMeasurePreserving: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/Randomness.dfy(25,17): ProbIsProbabilityMeasure: Declaration has explicit `{:axiom}` attribute. 

src/Distributions/Bernoulli/Correctness.dfy

@@ -4,10 +4,10 @@
  *******************************************************************************/
 
 module Bernoulli.Correctness {
-  import MeasureTheory
+  import Measures
   import Helper
   import Uniform
-  import RandomNumberGenerator
+  import Random
   import Independence
   import Monad
   import Model
@@ -16,21 +16,21 @@ module Bernoulli.Correctness {
    Lemmas
   *******/
 
-  lemma SampleIsIndepFn(m: nat, n: nat)
+  lemma SampleIsIndep(m: nat, n: nat)
     requires n != 0
     requires m <= n
-    ensures Independence.IsIndepFn(Model.Sample(m, n))
+    ensures Independence.IsIndep(Model.Sample(m, n))
   {
     var f := Uniform.Model.Sample(n);
     var g := (k: nat) => Monad.Return(k < m);
 
-    assert Independence.IsIndepFn(f) by {
-      Uniform.Correctness.SampleIsIndepFn(n);
+    assert Independence.IsIndep(f) by {
+      Uniform.Correctness.SampleIsIndep(n);
     }
 
-    assert forall k: nat :: Independence.IsIndepFn(g(k)) by {
-      forall k: nat ensures Independence.IsIndepFn(g(k)) {
-        Independence.ReturnIsIndepFn(k < m);
+    assert forall k: nat :: Independence.IsIndep(g(k)) by {
+      forall k: nat ensures Independence.IsIndep(g(k)) {
+        Independence.ReturnIsIndep(k < m);
       }
     }
 
@@ -43,8 +43,8 @@ module Bernoulli.Correctness {
     requires m <= n
     ensures
       var e := iset s | Model.Sample(m, n)(s).0;
-      && e in RandomNumberGenerator.event_space
-      && RandomNumberGenerator.mu(e) == m as real / n as real
+      && e in Random.eventSpace
+      && Random.Prob(e) == m as real / n as real
   {
     var e := iset s | Model.Sample(m, n)(s).0;
 
@@ -59,10 +59,10 @@ module Bernoulli.Correctness {
         }
       }
 
-      assert e in RandomNumberGenerator.event_space && RandomNumberGenerator.mu(e) == 0.0 by {
-        RandomNumberGenerator.RNGHasMeasure();
-        assert MeasureTheory.IsSigmaAlgebra(RandomNumberGenerator.event_space, RandomNumberGenerator.sample_space);
-        assert MeasureTheory.IsPositive(RandomNumberGenerator.event_space, RandomNumberGenerator.mu);
+      assert e in Random.eventSpace && Random.Prob(e) == 0.0 by {
+        Random.ProbIsProbabilityMeasure();
+        assert Measures.IsSigmaAlgebra(Random.eventSpace, Random.sampleSpace);
+        assert Measures.IsPositive(Random.eventSpace, Random.Prob);
       }
     } else {
       var e1 := iset s | Uniform.Model.Sample(n)(s).0 == m-1;
@@ -84,12 +84,12 @@ module Bernoulli.Correctness {
         e1 + e2;
       }
 
-      assert A1: e1 in RandomNumberGenerator.event_space && RandomNumberGenerator.mu(e1) == 1.0 / (n as real) by {
+      assert A1: e1 in Random.eventSpace && Random.Prob(e1) == 1.0 / (n as real) by {
         Uniform.Correctness.UniformFullCorrectness(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 {
+      assert A2: e2 in Random.eventSpace && Random.Prob(e2) == (m-1) as real / n as real by {
         BernoulliCorrectness(m-1, n);
       }
 
@@ -102,11 +102,11 @@ module Bernoulli.Correctness {
       }
 
       calc {
-        RandomNumberGenerator.mu(e);
+        Random.Prob(e);
         { assert e == e1 + e2; }
-        RandomNumberGenerator.mu(e1 + e2);
-        { reveal A1; reveal A2; 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);
+        Random.Prob(e1 + e2);
+        { reveal A1; reveal A2; assert e1 * e2 == iset{}; Random.ProbIsProbabilityMeasure(); Measures.PosCountAddImpliesAdd(Random.eventSpace, Random.sampleSpace, Random.Prob); assert Measures.IsAdditive(Random.eventSpace, Random.Prob); }
+        Random.Prob(e1) + Random.Prob(e2);
         { reveal A1; reveal A2; }
         (1.0 / n as real) + ((m-1) as real / n as real);
         { reveal A3; }
@@ -116,11 +116,11 @@ module Bernoulli.Correctness {
         m as real / n as real;
       }
 
-      assert e in RandomNumberGenerator.event_space by {
-        RandomNumberGenerator.RNGHasMeasure();
+      assert e in Random.eventSpace by {
+        Random.ProbIsProbabilityMeasure();
         reveal A1;
         reveal A2;
-        MeasureTheory.BinaryUnion(RandomNumberGenerator.event_space, RandomNumberGenerator.sample_space, e1, e2);
+        Measures.BinaryUnion(Random.eventSpace, Random.sampleSpace, e1, e2);
       }
     }
   }

src/Distributions/BernoulliExpNeg/Correctness.dfy

@@ -6,15 +6,15 @@
 module BernoulliExpNeg.Correctness {
   import Rationals
   import Exponential
-  import RandomNumberGenerator
+  import Random
   import Independence
   import Model
 
   lemma {:axiom} Correctness(gamma: Rationals.Rational)
     requires 0 <= gamma.numer
-    ensures RandomNumberGenerator.mu(iset s | Model.Sample(gamma)(s).0) == Exponential.Exp(-Rationals.ToReal(gamma))
+    ensures Random.Prob(iset s | Model.Sample(gamma)(s).0) == Exponential.Exp(-Rationals.ToReal(gamma))
 
-  lemma {:axiom} SampleIsIndepFn(gamma: Rationals.Rational)
+  lemma {:axiom} SampleIsIndep(gamma: Rationals.Rational)
     requires 0 <= gamma.numer
-    ensures Independence.IsIndepFn(Model.Sample(gamma))
+    ensures Independence.IsIndep(Model.Sample(gamma))
 }

src/Distributions/BernoulliExpNeg/Model.dfy

@@ -7,7 +7,7 @@ module BernoulliExpNeg.Model {
   import Rationals
   import Uniform
   import Monad
-  import WhileAndUntil
+  import Loops
   import BernoulliModel = Bernoulli.Model
 
   function Sample(gamma: Rationals.Rational): Monad.Hurd<bool>
@@ -28,7 +28,7 @@ module BernoulliExpNeg.Model {
     requires gamma.numer >= 0
   {
     assume {:axiom} false; // assume termination
-    WhileAndUntil.ProbWhile(
+    Loops.While(
       (bgamma: (bool, Rationals.Rational)) => bgamma.0 && bgamma.1.denom <= bgamma.1.numer,
       GammaReductionLoopIter,
       (true, gamma)
@@ -58,7 +58,7 @@ module BernoulliExpNeg.Model {
     requires 0 <= gamma.numer <= gamma.denom
   {
     assume {:axiom} false; // assume termination
-    WhileAndUntil.ProbWhile(
+    Loops.While(
       (ak: (bool, nat)) => ak.0,
       (ak: (bool, nat)) => GammaLe1LoopIter(gamma, ak),
       ak

src/Distributions/Coin/Interface.dfy

@@ -4,13 +4,13 @@
  *******************************************************************************/
 
 module Coin.Interface {
-  import RandomNumberGenerator
+  import Random
   import Model
 
   method {:extern "DRandomCoin", "Coin"} ExternCoinSample() returns (b: bool)
 
   trait {:termination false} Trait {
-    ghost var s: RandomNumberGenerator.RNG
+    ghost var s: Random.Bitstream
 
     method CoinSample() returns (b: bool)
       modifies this

src/Distributions/Coin/Model.dfy

@@ -4,10 +4,10 @@
  *******************************************************************************/
 
 module Coin.Model {
-  import RandomNumberGenerator
+  import Random
   import Monad
 
-  function Sample(s: RandomNumberGenerator.RNG): (bool, RandomNumberGenerator.RNG) {
-    Monad.Deconstruct(s)
+  function Sample(s: Random.Bitstream): (bool, Random.Bitstream) {
+    Monad.Coin(s)
   }
 }