remove dead code

audit.log

@@ -1,23 +1,9 @@
 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/Model.dfy(19,33): Sample: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/UniformPowerOfTwo/Model.dfy(19,20): 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,7 +21,7 @@ module {:extern "DafnyVMCPart"} DafnyVMC {
 
     method UniformPowerOfTwoSample(n: nat) returns (u: nat)
       requires n >= 1
-      modifies this
+      modifies `s
       ensures UniformPowerOfTwo.Model.Sample(n)(old(s)) == Monad.Result(u, s)
     {
       u := DafnyVMCPartMaterial.Random.ExternUniformPowerOfTwoSample(n);

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

@@ -17,9 +17,8 @@ module Coin.Implementation {
     {
       var x := UniformPowerOfTwoSample(2);
       b := if x == 1 then true else false;
-      reveal UniformPowerOfTwo.Model.Sample();
     }
 
   }
 
-}
+}

src/Distributions/Coin/Interface.dfy

@@ -16,4 +16,4 @@ module Coin.Interface {
       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
 
   /************

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
 
   /************