Fix sign flag for SignedInteger64 zero (#191)

* resolve #147 * remove unnecessary conversions
starcoinorg · Oct 31, 2022 · 722a298 · 722a298
1 parent fce8707
commit 722a298
Show file tree

Hide file tree

Showing 11 changed files with 66 additions and 42 deletions.
diff --git a/build/StarcoinFramework/bytecode_modules/SignedInteger64.mv b/build/StarcoinFramework/bytecode_modules/SignedInteger64.mv
diff --git a/build/StarcoinFramework/docs/SignedInteger64.md b/build/StarcoinFramework/docs/SignedInteger64.md
@@ -73,7 +73,7 @@ Multiply a u64 integer by a signed integer number.
 
 <pre><code><b>public</b> <b>fun</b> <a href="SignedInteger64.md#0x1_SignedInteger64_multiply_u64">multiply_u64</a>(num: u64, multiplier: <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a>): <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> {
     <b>let</b> product = multiplier.value * num;
-    <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> { value: (product <b>as</b> u64), is_negative: multiplier.is_negative }
+    <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> { value: product, is_negative: multiplier.is_negative }
 }
 </code></pre>
 
@@ -111,7 +111,7 @@ Divide a u64 integer by a signed integer number.
 
 <pre><code><b>public</b> <b>fun</b> <a href="SignedInteger64.md#0x1_SignedInteger64_divide_u64">divide_u64</a>(num: u64, divisor: <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a>): <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> {
     <b>let</b> quotient = num / divisor.value;
-    <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> { value: (quotient <b>as</b> u64), is_negative: divisor.is_negative }
+    <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> { value: quotient, is_negative: divisor.is_negative }
 }
 </code></pre>
 
@@ -150,14 +150,14 @@ Sub: <code>num - minus</code>
 <pre><code><b>public</b> <b>fun</b> <a href="SignedInteger64.md#0x1_SignedInteger64_sub_u64">sub_u64</a>(num: u64, minus: <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a>): <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> {
     <b>if</b> (minus.is_negative) {
         <b>let</b> result = num + minus.value;
-        <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> { value: (result <b>as</b> u64), is_negative: <b>false</b> }
+        <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> { value: result, is_negative: <b>false</b> }
     } <b>else</b> {
-        <b>if</b> (num &gt; minus.value)  {
+        <b>if</b> (num &gt;= minus.value) {
             <b>let</b> result = num - minus.value;
-            <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> { value: (result <b>as</b> u64), is_negative: <b>false</b> }
+            <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> { value: result, is_negative: <b>false</b> }
         }<b>else</b> {
             <b>let</b> result = minus.value - num;
-            <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> { value: (result <b>as</b> u64), is_negative: <b>true</b> }
+            <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> { value: result, is_negative: <b>true</b> }
         }
     }
 }
@@ -197,16 +197,16 @@ Add: <code>num + addend</code>
 
 <pre><code><b>public</b> <b>fun</b> <a href="SignedInteger64.md#0x1_SignedInteger64_add_u64">add_u64</a>(num: u64, addend: <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a>): <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> {
     <b>if</b> (addend.is_negative) {
-       <b>if</b> (num &gt; addend.value)  {
-           <b>let</b> result = num - addend.value;
-           <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> { value: (result <b>as</b> u64), is_negative: <b>false</b> }
-       }<b>else</b> {
-           <b>let</b> result = addend.value - num;
-           <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> { value: (result <b>as</b> u64), is_negative: <b>true</b> }
-       }
+        <b>if</b> (num &gt;= addend.value) {
+            <b>let</b> result = num - addend.value;
+            <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> { value: result, is_negative: <b>false</b> }
+        }<b>else</b> {
+            <b>let</b> result = addend.value - num;
+            <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> { value: result, is_negative: <b>true</b> }
+        }
     } <b>else</b> {
-         <b>let</b> result = num + addend.value;
-         <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> { value: (result <b>as</b> u64), is_negative: <b>false</b> }
+        <b>let</b> result = num + addend.value;
+        <a href="SignedInteger64.md#0x1_SignedInteger64">SignedInteger64</a> { value: result, is_negative: <b>false</b> }
     }
 }
 </code></pre>

diff --git a/build/StarcoinFramework/source_maps/SignedInteger64.mvsm b/build/StarcoinFramework/source_maps/SignedInteger64.mvsm
diff --git a/integration-tests/signed_integer/add.exp b/integration-tests/signed_integer/add.exp
@@ -1,7 +1,7 @@
 processed 3 tasks
 
-task 2 'run'. lines 5-26:
+task 2 'run'. lines 5-41:
 {
-  "gas_used": 54451,
+  "gas_used": 100723,
   "status": "Executed"
 }
diff --git a/integration-tests/signed_integer/add.move b/integration-tests/signed_integer/add.move
@@ -22,5 +22,20 @@ fun main() {
     let i2 = SignedInteger64::create_from_raw_value(0, false);
     let z2 = SignedInteger64::add_u64(100, copy i2);
     assert!(SignedInteger64::get_value(z2) == 100, 6);
+
+    let i3 = SignedInteger64::create_from_raw_value(1, true);
+    let z3 = SignedInteger64::add_u64(1, i3);
+    assert!(SignedInteger64::get_value(copy z3) == 0, 7);
+    assert!(SignedInteger64::is_negative(z3) == false, 8);
+
+    let i4 = SignedInteger64::create_from_raw_value(0, true);
+    let z4 = SignedInteger64::add_u64(0, i4);
+    assert!(SignedInteger64::get_value(copy z4) == 0, 9);
+    assert!(SignedInteger64::is_negative(z4) == false, 10);
+
+    let i5 = SignedInteger64::create_from_raw_value(0, false);
+    let z5 = SignedInteger64::add_u64(0, i5);
+    assert!(SignedInteger64::get_value(copy z5) == 0, 11);
+    assert!(SignedInteger64::is_negative(z5) == false, 12);
 }
 }
diff --git a/integration-tests/signed_integer/add_overflow.exp b/integration-tests/signed_integer/add_overflow.exp
@@ -12,7 +12,7 @@ task 2 'run'. lines 5-16:
         }
       },
       "function": 0,
-      "code_offset": 42
+      "code_offset": 40
     }
   }
 }
diff --git a/integration-tests/signed_integer/divide.exp b/integration-tests/signed_integer/divide.exp
@@ -2,6 +2,6 @@ processed 3 tasks
 
 task 2 'run'. lines 5-26:
 {
-  "gas_used": 53261,
+  "gas_used": 53253,
   "status": "Executed"
 }
diff --git a/integration-tests/signed_integer/multiply.exp b/integration-tests/signed_integer/multiply.exp
@@ -2,6 +2,6 @@ processed 3 tasks
 
 task 2 'run'. lines 5-23:
 {
-  "gas_used": 45726,
+  "gas_used": 45720,
   "status": "Executed"
 }
diff --git a/integration-tests/signed_integer/sub.exp b/integration-tests/signed_integer/sub.exp
@@ -1,7 +1,7 @@
 processed 3 tasks
 
-task 2 'run'. lines 5-26:
+task 2 'run'. lines 5-36:
 {
-  "gas_used": 54451,
+  "gas_used": 84861,
   "status": "Executed"
 }
diff --git a/integration-tests/signed_integer/sub.move b/integration-tests/signed_integer/sub.move
@@ -22,5 +22,15 @@ fun main() {
     let i2 = SignedInteger64::create_from_raw_value(100, true);
     let z2 = SignedInteger64::sub_u64(100, copy i2);
     assert!(SignedInteger64::get_value(z2) == 200, 6);
+
+    let i3 = SignedInteger64::create_from_raw_value(0, true);
+    let z3 = SignedInteger64::sub_u64(0, i3);
+    assert!(SignedInteger64::get_value(copy z3) == 0, 1);
+    assert!(SignedInteger64::is_negative(z3) == false, 2);
+
+    let i4 = SignedInteger64::create_from_raw_value(0, false);
+    let z4 = SignedInteger64::sub_u64(0, i4);
+    assert!(SignedInteger64::get_value(copy z4) == 0, 1);
+    assert!(SignedInteger64::is_negative(z4) == false, 2);
 }
 }
diff --git a/sources/SignedInteger64.move b/sources/SignedInteger64.move
@@ -16,43 +16,44 @@ module SignedInteger64 {
     /// Multiply a u64 integer by a signed integer number.
     public fun multiply_u64(num: u64, multiplier: SignedInteger64): SignedInteger64 {
         let product = multiplier.value * num;
-        SignedInteger64 { value: (product as u64), is_negative: multiplier.is_negative }
+        SignedInteger64 { value: product, is_negative: multiplier.is_negative }
     }
 
     /// Divide a u64 integer by a signed integer number.
     public fun divide_u64(num: u64, divisor: SignedInteger64): SignedInteger64 {
         let quotient = num / divisor.value;
-        SignedInteger64 { value: (quotient as u64), is_negative: divisor.is_negative }
+        SignedInteger64 { value: quotient, is_negative: divisor.is_negative }
     }
 
     /// Sub: `num - minus`
     public fun sub_u64(num: u64, minus: SignedInteger64): SignedInteger64 {
         if (minus.is_negative) {
             let result = num + minus.value;
-            SignedInteger64 { value: (result as u64), is_negative: false }
+            SignedInteger64 { value: result, is_negative: false }
         } else {
-            if (num > minus.value)  {
+            if (num >= minus.value) {
                 let result = num - minus.value;
-                SignedInteger64 { value: (result as u64), is_negative: false }
+                SignedInteger64 { value: result, is_negative: false }
             }else {
                 let result = minus.value - num;
-                SignedInteger64 { value: (result as u64), is_negative: true }
+                SignedInteger64 { value: result, is_negative: true }
             }
         }
     }
+
     /// Add: `num + addend`
     public fun add_u64(num: u64, addend: SignedInteger64): SignedInteger64 {
         if (addend.is_negative) {
-           if (num > addend.value)  {
-               let result = num - addend.value;
-               SignedInteger64 { value: (result as u64), is_negative: false }
-           }else {
-               let result = addend.value - num;
-               SignedInteger64 { value: (result as u64), is_negative: true }
-           }
+            if (num >= addend.value) {
+                let result = num - addend.value;
+                SignedInteger64 { value: result, is_negative: false }
+            }else {
+                let result = addend.value - num;
+                SignedInteger64 { value: result, is_negative: true }
+            }
         } else {
-             let result = num + addend.value;
-             SignedInteger64 { value: (result as u64), is_negative: false }
+            let result = num + addend.value;
+            SignedInteger64 { value: result, is_negative: false }
         }
     }
 
@@ -73,10 +74,8 @@ module SignedInteger64 {
 
     // **************** SPECIFICATIONS ****************
 
-
-
     spec multiply_u64 {
-       aborts_if multiplier.value * num > max_u64();
+        aborts_if multiplier.value * num > max_u64();
     }
 
     spec divide_u64 {
@@ -88,7 +87,7 @@ module SignedInteger64 {
     }
 
     spec add_u64 {
-       aborts_if !addend.is_negative && num + addend.value > max_u64();
+        aborts_if !addend.is_negative && num + addend.value > max_u64();
     }
 
     spec create_from_raw_value {
@@ -105,6 +104,6 @@ module SignedInteger64 {
         aborts_if false;
         ensures result == num.is_negative;
     }
-}
 
 }
+}