Remove dead code

audit.log

@@ -1,23 +1,8 @@
-src/DafnyVMC.dfy(28,6): UniformPowerOfTwoSample: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/Uniform/Correctness.dfy(34,17): UniformFullCorrectness: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/Uniform/Model.dfy(21,33): Sample: Declaration has explicit `{:axiom}` attribute. 
-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/Distributions/Uniform/Correctness.dfy(31,17): UniformFullCorrectness: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/Uniform/Correctness.dfy(36,17): SampleCoin: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/Uniform/Model.dfy(19,33): Sample: 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

@@ -21,11 +21,9 @@ module {:extern "DafnyVMCPart"} DafnyVMC {
 
     method UniformPowerOfTwoSample(n: nat) returns (u: nat)
       requires n >= 1
-      modifies this
-      ensures UniformPowerOfTwo.Model.Sample(n)(old(s)) == Monad.Result(u, s)
+      modifies `s
     {
       u := DafnyVMCPartMaterial.Random.ExternUniformPowerOfTwoSample(n);
-      assume {:axiom} false; // assume correctness of extern implementation
     }
   }
 

src/DafnyVMCTrait.dfy

@@ -7,7 +7,7 @@ module DafnyVMCTrait {
 
   import opened Pos
 
-  trait {:termination false} RandomTrait extends  UniformPowerOfTwo.Implementation.Trait, FisherYates.Implementation.Trait {
+  trait {:termination false} RandomTrait extends  UniformPowerOfTwo.Interface.Trait, FisherYates.Implementation.Trait {
 
     method {:verify false} UniformSample (n: pos)
       returns (o: nat)

src/Distributions/Bitstream/Interface.dfy

@@ -0,0 +1,12 @@
+/*******************************************************************************
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
+
+module Bitstream.Interface {
+  import Rand
+
+  trait {:termination false} Trait {
+    ghost var s: Rand.Bitstream
+  }
+}

src/Distributions/Coin/Implementation.dfy

@@ -7,19 +7,20 @@ 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.Correctness.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
 
   /************
@@ -36,6 +33,9 @@ module Uniform.Correctness {
     ensures SampleEquals(n, i) in Rand.eventSpace
     ensures Rand.prob(SampleEquals(n, i)) == 1.0 / (n as real)
 
+  lemma {:axiom} SampleCoin(s: Rand.Bitstream)
+    ensures Model.Sample(2)(s)== Monad.Coin(s).Map(b => if b then 1 else 0)
+
   // Correctness theorem for Model.IntervalSample
   lemma UniformFullIntervalCorrectness(a: int, b: int, i: int)
     requires a <= i < b

src/Distributions/Uniform/Interface.dfy

@@ -5,12 +5,11 @@
 
 module Uniform.Interface {
   import Monad
-  import Coin
   import Model
-  import UniformPowerOfTwo
   import Pos
+  import Bitstream
 
-  trait {:termination false} Trait extends UniformPowerOfTwo.Interface.Trait {
+  trait {:termination false} Trait extends Bitstream.Interface.Trait {
 
     method UniformSample(n: Pos.pos) returns (u: nat)
       modifies `s

src/Distributions/Uniform/Model.dfy

@@ -7,10 +7,8 @@ module Uniform.Model {
   import Measures
   import NatArith
   import Rand
-  import Quantifier
   import Monad
   import Independence
-  import Loops
   import UniformPowerOfTwo
 
   /************