diff --git a/build/StarcoinFramework/bytecode_modules/Compare.mv b/build/StarcoinFramework/bytecode_modules/Compare.mv
index cb60f4b6..9fc383b4 100644
Binary files a/build/StarcoinFramework/bytecode_modules/Compare.mv and b/build/StarcoinFramework/bytecode_modules/Compare.mv differ
diff --git a/build/StarcoinFramework/bytecode_modules/U256.mv b/build/StarcoinFramework/bytecode_modules/U256.mv
index 0d9c2da9..f93df531 100644
Binary files a/build/StarcoinFramework/bytecode_modules/U256.mv and b/build/StarcoinFramework/bytecode_modules/U256.mv differ
diff --git a/build/StarcoinFramework/docs/Compare.md b/build/StarcoinFramework/docs/Compare.md
index a2f8b58a..cd7ba32c 100644
--- 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.
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
};
@@ -147,16 +150,18 @@ Keep this in mind when using this function to compare addresses.
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
@@ -177,44 +182,6 @@ Keep this in mind when using this function to compare addresses.
-
-
-
-
-## Function `cmp_u8`
-
-
-
-fun cmp_u8(i1: u8, i2: u8): u8
-
-
-
-
-
-Implementation
-
-
-fun cmp_u8(i1: u8, i2: u8): u8 {
- if (i1 == i2) EQUAL
- else if (i1 < i2) LESS_THAN
- else GREATER_THAN
-}
-
-
-
-
-
-
-
-Specification
-
-
-
-aborts_if false;
-
-
-
-
diff --git a/build/StarcoinFramework/docs/U256.md b/build/StarcoinFramework/docs/U256.md
index 4236f4d3..4abb01ba 100644
--- 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)
-use 0x1::Arith;
-use 0x1::Errors;
+use 0x1::Errors;
use 0x1::Vector;
@@ -678,79 +675,6 @@ vector should always has two elements.
-
-
-
-
-## Function `add_nocarry`
-
-move implementation of native_add.
-
-
-fun add_nocarry(a: &mut U256::U256, b: &U256::U256)
-
-
-
-
-
-Implementation
-
-
-fun add_nocarry(a: &mut U256, b: &U256) {
- let carry = 0;
- let idx = 0;
- let len = (WORD as u64);
- while (idx < len) {
- let a_bit = Vector::borrow_mut(&mut a.bits, idx);
- let b_bit = Vector::borrow(&b.bits, idx);
- *a_bit = StarcoinFramework::Arith::adc(*a_bit, *b_bit, &mut carry);
- idx = idx + 1;
- };
-
- // check overflow
- assert!(carry == 0, 100);
-}
-
-
-
-
-
-
-
-
-## Function `sub_noborrow`
-
-move implementation of native_sub.
-
-
-fun sub_noborrow(a: &mut U256::U256, b: &U256::U256)
-
-
-
-
-
-Implementation
-
-
-fun sub_noborrow(a: &mut U256, b: &U256) {
- let borrow = 0;
- let idx = 0;
- let len = (WORD as u64);
- while (idx < len) {
- let a_bit = Vector::borrow_mut(&mut a.bits, idx);
- let b_bit = Vector::borrow(&b.bits, idx);
- *a_bit = StarcoinFramework::Arith::sbb(*a_bit, *b_bit, &mut borrow);
- idx = idx + 1;
- };
-
- // check overflow
- assert!(borrow == 0, 100);
-
-}
-
-
-
-
diff --git a/build/StarcoinFramework/source_maps/Arith.mvsm b/build/StarcoinFramework/source_maps/Arith.mvsm
index 2d86c319..2d249cc2 100644
Binary files a/build/StarcoinFramework/source_maps/Arith.mvsm and b/build/StarcoinFramework/source_maps/Arith.mvsm differ
diff --git a/build/StarcoinFramework/source_maps/Compare.mvsm b/build/StarcoinFramework/source_maps/Compare.mvsm
index 025b4156..27000bfa 100644
Binary files a/build/StarcoinFramework/source_maps/Compare.mvsm and b/build/StarcoinFramework/source_maps/Compare.mvsm differ
diff --git a/build/StarcoinFramework/source_maps/U256.mvsm b/build/StarcoinFramework/source_maps/U256.mvsm
index b552ee0e..78433b97 100644
Binary files a/build/StarcoinFramework/source_maps/U256.mvsm and b/build/StarcoinFramework/source_maps/U256.mvsm differ
diff --git a/integration-tests/compare/compare.exp b/integration-tests/compare/compare.exp
index 2b4cd345..51489a97 100644
--- 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
index 96a080a3..c562a041 100644
--- 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
index 3e25c777..15697dd5 100644
--- 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
index 45e20df5..41110b9b 100644
--- 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,16 +62,18 @@ 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
@@ -75,22 +81,10 @@ module Compare {
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
diff --git a/sources/U256.move b/sources/U256.move
index 6c70e296..f83dfdfb 100644
--- a/sources/U256.move
+++ b/sources/U256.move
@@ -378,115 +378,6 @@ module U256 {
assert!(compare(&Self::pow(copy a, d), &from_u64(1)) == EQUAL, 0);
}
- /// move implementation of native_add.
- fun add_nocarry(a: &mut U256, b: &U256) {
- let carry = 0;
- let idx = 0;
- let len = (WORD as u64);
- while (idx < len) {
- let a_bit = Vector::borrow_mut(&mut a.bits, idx);
- let b_bit = Vector::borrow(&b.bits, idx);
- *a_bit = StarcoinFramework::Arith::adc(*a_bit, *b_bit, &mut carry);
- idx = idx + 1;
- };
-
- // check overflow
- assert!(carry == 0, 100);
- }
-
- // TODO: MVP find false examples that violate the spec
- // spec add_nocarry {
- // aborts_if value_of_U256(a) + value_of_U256(b) >= P64 * P64 * P64 * P64;
- // ensures value_of_U256(a) == value_of_U256(old(a)) + value_of_U256(b);
- // }
-
- #[test]
- #[expected_failure]
- fun test_add_nocarry_overflow() {
- let va = Vector::empty();
- Vector::push_back(&mut va, 15891);
- Vector::push_back(&mut va, 0);
- Vector::push_back(&mut va, 0);
- Vector::push_back(&mut va, 0);
-
- let vb = Vector::empty();
- Vector::push_back(&mut vb, 18446744073709535725);
- Vector::push_back(&mut vb, 18446744073709551615);
- Vector::push_back(&mut vb, 18446744073709551615);
- Vector::push_back(&mut vb, 18446744073709551615);
-
- let a = U256 { bits: va };
- let b = U256 { bits: vb };
- add_nocarry(&mut a, &b); // MVP thinks this won't abort
- }
-
- #[test]
- fun test_add_nocarry_like_native_1() {
- let va = Vector::empty();
- Vector::push_back(&mut va, 15891);
- Vector::push_back(&mut va, 0);
- Vector::push_back(&mut va, 0);
- Vector::push_back(&mut va, 0);
-
- let vb = Vector::empty();
- Vector::push_back(&mut vb, 18446744073709535724);
- Vector::push_back(&mut vb, 18446744073709551615);
- Vector::push_back(&mut vb, 18446744073709551615);
- Vector::push_back(&mut vb, 18446744073709551615);
-
- let a1 = U256 { bits: va };
- let a2 = copy a1;
- let b = U256 { bits: vb };
- add_nocarry(&mut a1, &b);
- native_add(&mut a2, &b);
- assert!(compare(&a1, &a2) == EQUAL, 0); // MVP thinks this doesn't hold
- }
-
- #[test]
- fun test_add_nocarry_like_native_2() {
- let va = Vector::empty();
- Vector::push_back(&mut va, 26962);
- Vector::push_back(&mut va, 24464);
- Vector::push_back(&mut va, 6334);
- Vector::push_back(&mut va, 19169);
-
- let vb = Vector::empty();
- Vector::push_back(&mut vb, 29358);
- Vector::push_back(&mut vb, 26500);
- Vector::push_back(&mut vb, 15724);
- Vector::push_back(&mut vb, 11478);
-
- let a1 = U256 { bits: va };
- let a2 = copy a1;
- let b = U256 { bits: vb };
- add_nocarry(&mut a1, &b); // MVP thinks this abort
- native_add(&mut a2, &b);
- assert!(compare(&a1, &a2) == EQUAL, 0);
- }
-
- /// move implementation of native_sub.
- fun sub_noborrow(a: &mut U256, b: &U256) {
- let borrow = 0;
- let idx = 0;
- let len = (WORD as u64);
- while (idx < len) {
- let a_bit = Vector::borrow_mut(&mut a.bits, idx);
- let b_bit = Vector::borrow(&b.bits, idx);
- *a_bit = StarcoinFramework::Arith::sbb(*a_bit, *b_bit, &mut borrow);
- idx = idx + 1;
- };
-
- // check overflow
- assert!(borrow == 0, 100);
-
- }
-
- // TODO: Similar situation with `add_nocarry`
- // spec sub_noborrow {
- // aborts_if value_of_U256(a) < value_of_U256(b);
- // ensures value_of_U256(a) == value_of_U256(old(a)) - value_of_U256(b);
- // }
-
native fun from_bytes(data: &vector, be: bool): U256;
native fun native_add(a: &mut U256, b: &U256);
native fun native_sub(a: &mut U256, b: &U256);