lemma as postcondition

audit.log

@@ -1,8 +1,6 @@
 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/Correctness.dfy(62,17): SampleIsIndep: Declaration has explicit `{:axiom}` attribute. 
 src/Distributions/Uniform/Model.dfy(21,33): Sample: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/Uniform/Model.dfy(35,17): SampleBound: 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/Distributions/Uniform/Correctness.dfy

@@ -59,9 +59,10 @@ module Uniform.Correctness {
   }
 
   // Equation (4.10)
-  lemma {:axiom} SampleIsIndep(n: nat)
+  lemma SampleIsIndep(n: nat)
     requires n > 0
     ensures Independence.IsIndep(Model.Sample(n))
+  {}
 
   lemma IntervalSampleIsIndep(a: int, b: int)
     requires a < b

src/Distributions/Uniform/Model.dfy

@@ -18,8 +18,10 @@ module Uniform.Model {
   ************/
 
   // Definition 49
-  opaque ghost function {:axiom} Sample(n: nat): Monad.Hurd<nat>
+  opaque ghost function {:axiom} Sample(n: nat): (h: Monad.Hurd<nat>)
     requires n > 0
+    ensures Independence.IsIndep(h)
+    ensures forall s :: h(s).Result? ==> 0 <= h(s).value < n
 
   ghost function IntervalSample(a: int, b: int): (f: Monad.Hurd<int>)
     requires a < b
@@ -31,11 +33,11 @@ module Uniform.Model {
    Lemmas
   *******/
 
-
-  lemma {:axiom} SampleBound(n: nat, s: Rand.Bitstream)
+  lemma SampleBound(n: nat, s: Rand.Bitstream)
     requires n > 0
     requires Sample(n)(s).Result?
     ensures 0 <= Sample(n)(s).value < n
+  {}
 
   lemma IntervalSampleBound(a: int, b: int, s: Rand.Bitstream)
     requires a < b