fix cmp (#190)

* fix cmp * remove unused cmp_u8
starcoinorg · Oct 31, 2022 · fce8707 · fce8707
1 parent 64d754d
commit fce8707
Show file tree

Hide file tree

Showing 12 changed files with 35 additions and 259 deletions.
diff --git a/build/StarcoinFramework/bytecode_modules/Compare.mv b/build/StarcoinFramework/bytecode_modules/Compare.mv
diff --git a/build/StarcoinFramework/bytecode_modules/U256.mv b/build/StarcoinFramework/bytecode_modules/U256.mv
diff --git a/build/StarcoinFramework/docs/Compare.md b/build/StarcoinFramework/docs/Compare.md
@@ -8,7 +8,6 @@
 -  [Constants](#@Constants_0)
 -  [Function `cmp_bcs_bytes`](#0x1_Compare_cmp_bcs_bytes)
 -  [Function `cmp_bytes`](#0x1_Compare_cmp_bytes)
--  [Function `cmp_u8`](#0x1_Compare_cmp_u8)
 -  [Function `cmp_u64`](#0x1_Compare_cmp_u64)
 -  [Function `is_equal`](#0x1_Compare_is_equal)
 -  [Function `is_less_than`](#0x1_Compare_is_less_than)
@@ -103,7 +102,11 @@ Keep this in mind when using this function to compare addresses.
     <b>while</b> (i1 &gt; 0 && i2 &gt; 0) {
         i1 = i1 - 1;
         i2 = i2 - 1;
-        <b>let</b> elem_cmp = <a href="Compare.md#0x1_Compare_cmp_u8">cmp_u8</a>(*<a href="Vector.md#0x1_Vector_borrow">Vector::borrow</a>(v1, i1), *<a href="Vector.md#0x1_Vector_borrow">Vector::borrow</a>(v2, i2));
+        <b>let</b> v1 = *<a href="Vector.md#0x1_Vector_borrow">Vector::borrow</a>(v1, i1);
+        <b>let</b> v2 = *<a href="Vector.md#0x1_Vector_borrow">Vector::borrow</a>(v2, i2);
+        <b>let</b> elem_cmp = <b>if</b> (v1 == v2) <a href="Compare.md#0x1_Compare_EQUAL">EQUAL</a>
+            <b>else</b> <b>if</b> (v1 &lt; v2) <a href="Compare.md#0x1_Compare_LESS_THAN">LESS_THAN</a>
+            <b>else</b> <a href="Compare.md#0x1_Compare_GREATER_THAN">GREATER_THAN</a>;
         <b>if</b> (elem_cmp != 0) <b>return</b> elem_cmp
         // <b>else</b>, compare next element
     };
@@ -147,16 +150,18 @@ Keep this in mind when using this function to compare addresses.
     <b>let</b> l1 = <a href="Vector.md#0x1_Vector_length">Vector::length</a>(v1);
     <b>let</b> l2 = <a href="Vector.md#0x1_Vector_length">Vector::length</a>(v2);
     <b>let</b> len_cmp = <a href="Compare.md#0x1_Compare_cmp_u64">cmp_u64</a>(l1, l2);
-    <b>let</b> i1 = 0;
-    <b>let</b> i2 = 0;
-    <b>while</b> (i1 &lt; l1 && i2 &lt; l2) {
-        <b>let</b> elem_cmp = <a href="Compare.md#0x1_Compare_cmp_u8">cmp_u8</a>(*<a href="Vector.md#0x1_Vector_borrow">Vector::borrow</a>(v1, i1), *<a href="Vector.md#0x1_Vector_borrow">Vector::borrow</a>(v2, i2));
+    <b>let</b> i = 0;
+    <b>while</b> (i &lt; l1 && i &lt; l2) {
+        <b>let</b> v1 = *<a href="Vector.md#0x1_Vector_borrow">Vector::borrow</a>(v1, i);
+        <b>let</b> v2 = *<a href="Vector.md#0x1_Vector_borrow">Vector::borrow</a>(v2, i);
+        <b>let</b> elem_cmp = <b>if</b> (v1 == v2) <a href="Compare.md#0x1_Compare_EQUAL">EQUAL</a>
+            <b>else</b> <b>if</b> (v1 &lt; v2) <a href="Compare.md#0x1_Compare_LESS_THAN">LESS_THAN</a>
+            <b>else</b> <a href="Compare.md#0x1_Compare_GREATER_THAN">GREATER_THAN</a>;
         <b>if</b> (elem_cmp != 0) {
             <b>return</b> elem_cmp
         };
         // <b>else</b>, compare next element
-        i1 = i1 + 1;
-        i2 = i2 + 1;
+        i = i + 1;
     };
     // all compared elements equal; <b>use</b> length comparison <b>to</b> <b>break</b> the tie
     len_cmp
@@ -177,44 +182,6 @@ Keep this in mind when using this function to compare addresses.
 
 
 
-</details>
-
-<a name="0x1_Compare_cmp_u8"></a>
-
-## Function `cmp_u8`
-
-
-
-<pre><code><b>fun</b> <a href="Compare.md#0x1_Compare_cmp_u8">cmp_u8</a>(i1: u8, i2: u8): u8
-</code></pre>
-
-
-
-<details>
-<summary>Implementation</summary>
-
-
-<pre><code><b>fun</b> <a href="Compare.md#0x1_Compare_cmp_u8">cmp_u8</a>(i1: u8, i2: u8): u8 {
-    <b>if</b> (i1 == i2) <a href="Compare.md#0x1_Compare_EQUAL">EQUAL</a>
-    <b>else</b> <b>if</b> (i1 &lt; i2) <a href="Compare.md#0x1_Compare_LESS_THAN">LESS_THAN</a>
-    <b>else</b> <a href="Compare.md#0x1_Compare_GREATER_THAN">GREATER_THAN</a>
-}
-</code></pre>
-
-
-
-</details>
-
-<details>
-<summary>Specification</summary>
-
-
-
-<pre><code><b>aborts_if</b> <b>false</b>;
-</code></pre>
-
-
-
 </details>
 
 <a name="0x1_Compare_cmp_u64"></a>

diff --git a/build/StarcoinFramework/docs/U256.md b/build/StarcoinFramework/docs/U256.md
@@ -22,8 +22,6 @@ Implementation u256.
 -  [Function `div`](#0x1_U256_div)
 -  [Function `rem`](#0x1_U256_rem)
 -  [Function `pow`](#0x1_U256_pow)
--  [Function `add_nocarry`](#0x1_U256_add_nocarry)
--  [Function `sub_noborrow`](#0x1_U256_sub_noborrow)
 -  [Function `from_bytes`](#0x1_U256_from_bytes)
 -  [Function `native_add`](#0x1_U256_native_add)
 -  [Function `native_sub`](#0x1_U256_native_sub)
@@ -34,8 +32,7 @@ Implementation u256.
 -  [Module Specification](#@Module_Specification_1)
 
 
-<pre><code><b>use</b> <a href="U256.md#0x1_Arith">0x1::Arith</a>;
-<b>use</b> <a href="Errors.md#0x1_Errors">0x1::Errors</a>;
+<pre><code><b>use</b> <a href="Errors.md#0x1_Errors">0x1::Errors</a>;
 <b>use</b> <a href="Vector.md#0x1_Vector">0x1::Vector</a>;
 </code></pre>
 
@@ -678,79 +675,6 @@ vector should always has two elements.
 
 
 
-</details>
-
-<a name="0x1_U256_add_nocarry"></a>
-
-## Function `add_nocarry`
-
-move implementation of native_add.
-
-
-<pre><code><b>fun</b> <a href="U256.md#0x1_U256_add_nocarry">add_nocarry</a>(a: &<b>mut</b> <a href="U256.md#0x1_U256_U256">U256::U256</a>, b: &<a href="U256.md#0x1_U256_U256">U256::U256</a>)
-</code></pre>
-
-
-
-<details>
-<summary>Implementation</summary>
-
-
-<pre><code><b>fun</b> <a href="U256.md#0x1_U256_add_nocarry">add_nocarry</a>(a: &<b>mut</b> <a href="U256.md#0x1_U256">U256</a>, b: &<a href="U256.md#0x1_U256">U256</a>) {
-    <b>let</b> carry = 0;
-    <b>let</b> idx = 0;
-    <b>let</b> len = (<a href="U256.md#0x1_U256_WORD">WORD</a> <b>as</b> u64);
-    <b>while</b> (idx &lt; len) {
-        <b>let</b> a_bit = <a href="Vector.md#0x1_Vector_borrow_mut">Vector::borrow_mut</a>(&<b>mut</b> a.bits, idx);
-        <b>let</b> b_bit = <a href="Vector.md#0x1_Vector_borrow">Vector::borrow</a>(&b.bits, idx);
-        *a_bit = StarcoinFramework::Arith::adc(*a_bit, *b_bit, &<b>mut</b> carry);
-        idx = idx + 1;
-    };
-
-    // check overflow
-    <b>assert</b>!(carry == 0, 100);
-}
-</code></pre>
-
-
-
-</details>
-
-<a name="0x1_U256_sub_noborrow"></a>
-
-## Function `sub_noborrow`
-
-move implementation of native_sub.
-
-
-<pre><code><b>fun</b> <a href="U256.md#0x1_U256_sub_noborrow">sub_noborrow</a>(a: &<b>mut</b> <a href="U256.md#0x1_U256_U256">U256::U256</a>, b: &<a href="U256.md#0x1_U256_U256">U256::U256</a>)
-</code></pre>
-
-
-
-<details>
-<summary>Implementation</summary>
-
-
-<pre><code><b>fun</b> <a href="U256.md#0x1_U256_sub_noborrow">sub_noborrow</a>(a: &<b>mut</b> <a href="U256.md#0x1_U256">U256</a>, b: &<a href="U256.md#0x1_U256">U256</a>) {
-    <b>let</b> borrow = 0;
-    <b>let</b> idx = 0;
-    <b>let</b> len = (<a href="U256.md#0x1_U256_WORD">WORD</a> <b>as</b> u64);
-    <b>while</b> (idx &lt; len) {
-        <b>let</b> a_bit = <a href="Vector.md#0x1_Vector_borrow_mut">Vector::borrow_mut</a>(&<b>mut</b> a.bits, idx);
-        <b>let</b> b_bit = <a href="Vector.md#0x1_Vector_borrow">Vector::borrow</a>(&b.bits, idx);
-        *a_bit = StarcoinFramework::Arith::sbb(*a_bit, *b_bit, &<b>mut</b> borrow);
-        idx = idx + 1;
-    };
-
-    // check overflow
-    <b>assert</b>!(borrow == 0, 100);
-
-}
-</code></pre>
-
-
-
 </details>
 
 <a name="0x1_U256_from_bytes"></a>

diff --git a/build/StarcoinFramework/source_maps/Arith.mvsm b/build/StarcoinFramework/source_maps/Arith.mvsm
diff --git a/build/StarcoinFramework/source_maps/Compare.mvsm b/build/StarcoinFramework/source_maps/Compare.mvsm
diff --git a/build/StarcoinFramework/source_maps/U256.mvsm b/build/StarcoinFramework/source_maps/U256.mvsm
diff --git a/integration-tests/compare/compare.exp b/integration-tests/compare/compare.exp
@@ -2,6 +2,6 @@ processed 3 tasks
 
 task 2 'run'. lines 5-62:
 {
-  "gas_used": 2338303,
+  "gas_used": 1789891,
   "status": "Executed"
 }
diff --git a/integration-tests/incubator/SortedLinkedList.exp b/integration-tests/incubator/SortedLinkedList.exp
@@ -24,19 +24,19 @@ task 10 'run'. lines 293-303:
 
 task 11 'run'. lines 305-317:
 {
-  "gas_used": 359425,
+  "gas_used": 295841,
   "status": "Executed"
 }
 
 task 12 'run'. lines 319-331:
 {
-  "gas_used": 495218,
+  "gas_used": 399842,
   "status": "Executed"
 }
 
 task 13 'run'. lines 333-343:
 {
-  "gas_used": 595306,
+  "gas_used": 468138,
   "status": "Executed"
 }
 
@@ -72,19 +72,19 @@ task 19 'run'. lines 504-512:
 
 task 20 'run'. lines 514-523:
 {
-  "gas_used": 221094,
+  "gas_used": 213146,
   "status": "Executed"
 }
 
 task 21 'run'. lines 525-534:
 {
-  "gas_used": 259964,
+  "gas_used": 248042,
   "status": "Executed"
 }
 
 task 22 'run'. lines 536-545:
 {
-  "gas_used": 315232,
+  "gas_used": 299336,
   "status": "Executed"
 }
 

diff --git a/integration-tests/list/linked_list.exp b/integration-tests/list/linked_list.exp
@@ -8,7 +8,7 @@ task 9 'run'. lines 386-395:
 
 task 10 'run'. lines 397-410:
 {
-  "gas_used": 144048,
+  "gas_used": 136100,
   "status": "Executed"
 }
 

diff --git a/sources/Compare.move b/sources/Compare.move
@@ -46,7 +46,11 @@ module Compare {
         while (i1 > 0 && i2 > 0) {
             i1 = i1 - 1;
             i2 = i2 - 1;
-            let elem_cmp = cmp_u8(*Vector::borrow(v1, i1), *Vector::borrow(v2, i2));
+            let v1 = *Vector::borrow(v1, i1);
+            let v2 = *Vector::borrow(v2, i2);
+            let elem_cmp = if (v1 == v2) EQUAL
+                else if (v1 < v2) LESS_THAN
+                else GREATER_THAN;
             if (elem_cmp != 0) return elem_cmp
             // else, compare next element
         };
@@ -58,39 +62,29 @@ module Compare {
         let l1 = Vector::length(v1);
         let l2 = Vector::length(v2);
         let len_cmp = cmp_u64(l1, l2);
-        let i1 = 0;
-        let i2 = 0;
-        while (i1 < l1 && i2 < l2) {
-            let elem_cmp = cmp_u8(*Vector::borrow(v1, i1), *Vector::borrow(v2, i2));
+        let i = 0;
+        while (i < l1 && i < l2) {
+            let v1 = *Vector::borrow(v1, i);
+            let v2 = *Vector::borrow(v2, i);
+            let elem_cmp = if (v1 == v2) EQUAL
+                else if (v1 < v2) LESS_THAN
+                else GREATER_THAN;
             if (elem_cmp != 0) {
                 return elem_cmp
             };
             // else, compare next element
-            i1 = i1 + 1;
-            i2 = i2 + 1;
+            i = i + 1;
         };
         // all compared elements equal; use length comparison to break the tie
         len_cmp
     }
 
     spec cmp_bytes {
         pragma verify = false;
-        //cmp_u8(*Vector::borrow(v1, i1), *Vector::borrow(v2, i2)) is not covered
     }
 
     spec cmp_bcs_bytes {
         pragma verify = false;
-        //cmp_u8(*Vector::borrow(v1, i1), *Vector::borrow(v2, i2)) is not covered
-    }
-    // Compare two `u8`'s
-    fun cmp_u8(i1: u8, i2: u8): u8 {
-        if (i1 == i2) EQUAL
-        else if (i1 < i2) LESS_THAN
-        else GREATER_THAN
-    }
-
-    spec cmp_u8 {
-        aborts_if false;
     }
 
     // Compare two `u64`'s