audit and format

dafny-lang · Mar 4, 2024 · 5dbea10 · 5dbea10
1 parent 79e9093
commit 5dbea10
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 7 deletions.
diff --git a/audit.log b/audit.log
@@ -1,4 +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/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. 

diff --git a/src/DafnyVMCTrait.dfy b/src/DafnyVMCTrait.dfy
@@ -26,7 +26,7 @@ module DafnyVMCTrait {
 
     method {:verify false} BernoulliSample (num: nat, den: pos)
       returns (o: bool)
-      requires num <= den 
+      requires num <= den
       modifies this
       decreases *
     {
@@ -36,7 +36,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 +46,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 +62,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 +140,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 +226,6 @@ module DafnyVMCTrait {
     }
 
 
-}
+  }
 
 }
diff --git a/src/Distributions/Uniform/Model.dfy b/src/Distributions/Uniform/Model.dfy
@@ -31,7 +31,7 @@ module Uniform.Model {
    Lemmas
   *******/
 
-  
+
   lemma {:axiom} SampleBound(n: nat, s: Rand.Bitstream)
     requires n > 0
     requires Sample(n)(s).Result?