Added round.

daizhen228 · Aug 26, 2022 · 5fd04fa · 5fd04fa
1 parent 6534505
commit 5fd04fa
Show file tree

Hide file tree

Showing 2 changed files with 50 additions and 15 deletions.
diff --git a/language/move-stdlib/sources/fixed_point32.move b/language/move-stdlib/sources/fixed_point32.move
@@ -215,26 +215,21 @@ module std::fixed_point32 {
         FixedPoint32 {value: val << 32}
     }
 
-    public fun as_u64(number: FixedPoint32): u64 {
-        number.value >> 32
-    }
-    spec as_u64 {
-        pragma opaque;
-        aborts_if false;
-        ensures result == spec_as_u64(number);
-    }
-    spec fun spec_as_u64(val: FixedPoint32): u64 {
-        val.value >> 32
-    }
-
     public fun floor(num: FixedPoint32): u64 {
         num.value >> 32
     }
     spec floor {
         pragma opaque;
         aborts_if false;
-        let one = 1 << 32;
-        ensures ((num.value - one) >> 32) <= result && result <= (num.value >> 32);
+        ensures result == spec_floor(num);
+    }
+    spec fun spec_floor(val: FixedPoint32): u64 {
+        let fractional = val.value % (1 << 32);
+        if (fractional == 0) {
+            val.value >> 32
+        } else {
+            (val.value - fractional) >> 32
+        }
     }
 
     public fun ceil(num: FixedPoint32): u64 {
@@ -248,8 +243,41 @@ module std::fixed_point32 {
     spec ceil {
         pragma opaque;
         aborts_if false;
+        ensures result == spec_ceil(num);
+    }
+    spec fun spec_ceil(val: FixedPoint32): u64 {
+        let fractional = val.value % (1 << 32);
+        let one = 1 << 32;
+        if (fractional == 0) {
+            val.value >> 32
+        } else {
+            (val.value - fractional + one) >> 32
+        }
+    }
+
+    public fun round(num: FixedPoint32): u64 {
+        let floored_num = floor(num);
+        let bounary = (floored_num << 32) + ((1 << 32) / 2);
+        if (num.value < bounary) {
+            floored_num
+        } else {
+            ceil(num)
+        }
+    }
+    spec round {
+        pragma opaque;
+        aborts_if false;
+        ensures result == spec_round(num);
+    }
+    spec fun spec_round(val: FixedPoint32): u64 {
+        let fractional = val.value % (1 << 32);
+        let boundary = (1 << 32) / 2;
         let one = 1 << 32;
-        ensures (num.value >> 32) <= result && result <= ((num.value + one) >> 32);
+        if (fractional < boundary) {
+            (val.value - fractional) >> 32
+        } else {
+            (val.value - fractional + one) >> 32
+        }
     }
 
     // **************** SPECIFICATIONS ****************

diff --git a/language/move-stdlib/tests/fixedpoint32_tests.move b/language/move-stdlib/tests/fixedpoint32_tests.move
@@ -145,4 +145,11 @@ module std::fixed_point32_tests {
         let val = fixed_point32::ceil(point_five);
         assert!(val == 1, 0);
     }
+
+    #[test]
+    fun round_can_return_the_correct_number_one() {
+        let point_five = fixed_point32::create_from_rational(1, 2); // 0.5
+        let val = fixed_point32::round(point_five);
+        assert!(val == 1, 0);
+    }
 }