Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix sign flag for SignedInteger64 zero #191

Merged
merged 2 commits into from
Oct 31, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Binary file modified build/StarcoinFramework/bytecode_modules/SignedInteger64.mv
Binary file not shown.
30 changes: 15 additions & 15 deletions build/StarcoinFramework/docs/SignedInteger64.md
Original file line number Diff line number Diff line change
Expand Up @@ -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>

Expand Down Expand Up @@ -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>

Expand Down Expand Up @@ -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> }
}
}
}
Expand Down Expand Up @@ -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>
Expand Down
Binary file modified build/StarcoinFramework/source_maps/SignedInteger64.mvsm
Binary file not shown.
4 changes: 2 additions & 2 deletions integration-tests/signed_integer/add.exp
Original file line number Diff line number Diff line change
@@ -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"
}
15 changes: 15 additions & 0 deletions integration-tests/signed_integer/add.move
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}
2 changes: 1 addition & 1 deletion integration-tests/signed_integer/add_overflow.exp
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ task 2 'run'. lines 5-16:
}
},
"function": 0,
"code_offset": 42
"code_offset": 40
}
}
}
2 changes: 1 addition & 1 deletion integration-tests/signed_integer/divide.exp
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,6 @@ processed 3 tasks

task 2 'run'. lines 5-26:
{
"gas_used": 53261,
"gas_used": 53253,
"status": "Executed"
}
2 changes: 1 addition & 1 deletion integration-tests/signed_integer/multiply.exp
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,6 @@ processed 3 tasks

task 2 'run'. lines 5-23:
{
"gas_used": 45726,
"gas_used": 45720,
"status": "Executed"
}
4 changes: 2 additions & 2 deletions integration-tests/signed_integer/sub.exp
Original file line number Diff line number Diff line change
@@ -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"
}
10 changes: 10 additions & 0 deletions integration-tests/signed_integer/sub.move
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}
39 changes: 19 additions & 20 deletions sources/SignedInteger64.move
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
}
}

Expand All @@ -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 {
Expand All @@ -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 {
Expand All @@ -105,6 +104,6 @@ module SignedInteger64 {
aborts_if false;
ensures result == num.is_negative;
}
}

}
}