From 8fb80e3a3dde771013d247037510ac36672df3bf Mon Sep 17 00:00:00 2001
From: stefan-aws <stefanze@amazon.com>
Date: Wed, 21 Feb 2024 15:53:44 +0000
Subject: [PATCH] remove changes to uniform interface

---
 src/Distributions/Uniform/Interface.dfy | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/Distributions/Uniform/Interface.dfy b/src/Distributions/Uniform/Interface.dfy
index 3d6f1d7a..d8415730 100644
--- a/src/Distributions/Uniform/Interface.dfy
+++ b/src/Distributions/Uniform/Interface.dfy
@@ -4,33 +4,33 @@
  *******************************************************************************/
 
 module Uniform.Interface {
-  import UniformPowerOfTwo
   import Monad
   import Coin
   import Model
+  import UniformPowerOfTwo
   import Pos
 
   trait {:termination false} Trait extends UniformPowerOfTwo.Interface.Trait {
 
-    method UniformSample(n: Pos.pos) returns (o: nat)
+    method UniformSample(n: Pos.pos) returns (u: nat)
       modifies `s
       decreases *
       requires n > 0
-      ensures o < n
-      ensures Model.Sample(n)(old(s)) == Monad.Result(o, s)
+      ensures u < n
+      ensures Model.Sample(n)(old(s)) == Monad.Result(u, s)
 
-    method UniformIntervalSample(a: int, b: int) returns (o: int)
+    method UniformIntervalSample(a: int, b: int) returns (u: int)
       modifies `s
       decreases *
       requires a < b
-      ensures a <= o < b
-      ensures Model.IntervalSample(a, b)(old(s)) == Monad.Result(o, s)
+      ensures a <= u < b
+      ensures Model.IntervalSample(a, b)(old(s)) == Monad.Result(u, s)
     {
       var v := UniformSample(b - a);
       assert Model.Sample(b-a)(old(s)) == Monad.Result(v, s);
       assert Model.IntervalSample(a, b)(old(s)) == Monad.Result(a + v, s);
-      o := a + v;
+      u := a + v;
     }
 
   }
-}
+}
\ No newline at end of file