Skip to content

Commit 81b8ff4

Browse files
cosandreistefanescu
cos
and
andreistefanescu
authored
Full formal verification (#4)
* Full formal specifications for the entire library Co-authored-by: Andrei Stefanescu <[email protected]> * light report * . * . * . * . * Update README.md --------- Co-authored-by: Andrei Stefanescu <[email protected]>
1 parent 8a534bd commit 81b8ff4

21 files changed

+3261
-10
lines changed

‎.gitignore‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,6 @@
66
node_modules
77
/.vscode
88
/.DS_Store
9-
/.env
9+
/.env
10+
*.log.*
11+
output/

‎Move.toml‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,5 @@ name = "IntegerLibrary"
55
version = "1.0.1"
66
published-at = "0xab5e63352d0f05881bdfa1631cc0f7fc1669175a00d608828a924df481a9e4bd"
77

8-
[dependencies]
9-
Sui = { git = "https://github.com/MystenLabs/sui.git", subdir = "crates/sui-framework/packages/sui-framework", rev = "mainnet-v1.48.2" }
10-
118
[addresses]
129
integer_library = "0x03637b7b60978ef4389124f7683456f0050ab015a0590d52b6e6cadb342af34a"

‎README.md‎

Lines changed: 642 additions & 0 deletions
Large diffs are not rendered by default.

‎sources/i128.move‎

Lines changed: 11 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -97,12 +97,17 @@ module integer_library::i128 {
9797
}
9898

9999
public fun overflowing_sub(num1: I128, num2: I128): (I128, bool) {
100-
let sub_num = wrapping_add(I128 {
101-
bits: u128_neg(num2.bits)
102-
}, from(1));
103-
let sum = wrapping_add(num1, sub_num);
104-
let overflow = (sign(num1) & sign(sub_num) & u8_neg(sign(sum))) + (u8_neg(sign(num1)) & u8_neg(sign(sub_num)) & sign(sum));
105-
(sum, overflow != 0)
100+
let diff = wrapping_sub(num1, num2);
101+
let overflow = if (sign(num1) != sign(num2)) {
102+
if (sign(num1) != sign(diff)) {
103+
true
104+
} else {
105+
false
106+
}
107+
} else {
108+
false
109+
};
110+
(diff, overflow)
106111
}
107112

108113
public fun mul(num1: I128, num2: I128): I128 {

‎specs-bv/Move.lock‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
# @generated by Move, please check-in and do not edit manually.
2+
3+
[move]
4+
version = 3
5+
manifest_digest = "BC4FE2501E5714DD8780B061932D369DCC8BFB79C46BCADD3F0CD18558FFDD06"
6+
deps_digest = "F8BBB0CCB2491CA29A3DF03D6F92277A4F3574266507ACD77214D37ECA3F3082"
7+
dependencies = [
8+
{ id = "SuiProver", name = "SuiProver" },
9+
]
10+
11+
[[move.package]]
12+
id = "MoveStdlib"
13+
source = { git = "https://github.com/asymptotic-code/sui.git", rev = "next", subdir = "crates/sui-framework/packages/move-stdlib" }
14+
15+
[[move.package]]
16+
id = "Prover"
17+
source = { git = "https://github.com/asymptotic-code/sui-prover.git", rev = "main", subdir = "packages/prover" }
18+
19+
dependencies = [
20+
{ id = "MoveStdlib", name = "MoveStdlib" },
21+
]
22+
23+
[[move.package]]
24+
id = "Sui"
25+
source = { git = "https://github.com/asymptotic-code/sui.git", rev = "next", subdir = "crates/sui-framework/packages/sui-framework" }
26+
27+
dependencies = [
28+
{ id = "MoveStdlib", name = "MoveStdlib" },
29+
]
30+
31+
[[move.package]]
32+
id = "SuiProver"
33+
source = { git = "https://github.com/asymptotic-code/sui-prover.git", rev = "main", subdir = "packages/sui-prover" }
34+
35+
dependencies = [
36+
{ id = "SuiSpecs", name = "SuiSpecs" },
37+
]
38+
39+
[[move.package]]
40+
id = "SuiSpecs"
41+
source = { git = "https://github.com/asymptotic-code/sui-prover.git", rev = "main", subdir = "packages/sui-framework-specs" }
42+
43+
dependencies = [
44+
{ id = "Prover", name = "Prover" },
45+
{ id = "Sui", name = "Sui" },
46+
]

‎specs-bv/Move.toml‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
# mainnet
2+
# -------------------------------
3+
[package]
4+
name = "IntegerLibrarySpecsBV"
5+
edition = "2024.beta"
6+
7+
[addresses]
8+
integer_library_specs_bv = "0x0"

‎specs-bv/prelude_extra.bpl‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
procedure {:inline 1} $0_i32_ashr($t0: bv32, $t1: bv32) returns ($ret0: bv32) {
2+
$ret0 := $AShr'Bv32'($t0, $t1);
3+
}
4+
5+
procedure {:inline 1} $0_i64_ashr($t0: bv64, $t1: bv64) returns ($ret0: bv64) {
6+
$ret0 := $AShr'Bv64'($t0, $t1);
7+
}
8+
9+
procedure {:inline 1} $0_i128_ashr($t0: bv128, $t1: bv128) returns ($ret0: bv128) {
10+
$ret0 := $AShr'Bv128'($t0, $t1);
11+
}
12+

‎specs-bv/sources/i128.move‎

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
module integer_library_specs_bv::i128;
2+
3+
#[spec_only]
4+
use prover::prover::{ensures, asserts, invariant};
5+
6+
public struct I128 has copy, drop, store {
7+
bits: u128,
8+
}
9+
10+
public fun wrapping_add(num1: I128, num2: I128): I128 {
11+
let mut sum = num1.bits ^ num2.bits;
12+
let mut carry = (num1.bits & num2.bits) << 1;
13+
invariant!(|| {
14+
ensures(
15+
((num1.bits as u256) + (num2.bits as u256)) % (1 << 128) == ((sum as u256) + (carry as u256)) % (1 << 128),
16+
);
17+
});
18+
while (carry != 0) {
19+
let a = sum;
20+
let b = carry;
21+
sum = a ^ b;
22+
carry = (a & b) << 1;
23+
};
24+
I128 {
25+
bits: sum,
26+
}
27+
}
28+
29+
/*
30+
✅ Computes `num1 + num2` with wrapping overflow.
31+
⏮️ The function does not abort.
32+
*/
33+
#[spec(prove, target = wrapping_add)]
34+
public fun wrapping_add_spec(num1: I128, num2: I128): I128 {
35+
let result = wrapping_add(num1, num2);
36+
ensures(result.bits == (((num1.bits as u256) + (num2.bits as u256)) % (1 << 128)) as u128);
37+
result
38+
}
39+
40+
public fun shr(v: I128, shift: u8): I128 {
41+
if (shift == 0) {
42+
return v
43+
};
44+
let mask = 0xffffffffffffffffffffffffffffffff << (128 - shift);
45+
if (sign(v) == 1) {
46+
return I128 {
47+
bits: (v.bits >> shift) | mask,
48+
}
49+
};
50+
I128 {
51+
bits: v.bits >> shift,
52+
}
53+
}
54+
55+
public fun sign(v: I128): u8 {
56+
((v.bits >> 127) as u8)
57+
}
58+
59+
public native fun ashr(x: u128, y: u128): u128;
60+
61+
/*
62+
✅ Computes arithmetic right shift `v >> shift`.
63+
⏮️ The function aborts unless `shift < 128`.
64+
*/
65+
#[spec(prove, target = shr)]
66+
public fun shr_spec(v: I128, shift: u8): I128 {
67+
asserts(shift < 128);
68+
let result = shr(v, shift);
69+
ensures(result.bits == ashr(v.bits, shift as u128));
70+
result
71+
}

‎specs-bv/sources/i32.move‎

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
module integer_library_specs_bv::i32;
2+
3+
#[spec_only]
4+
use prover::prover::{ensures, asserts, invariant};
5+
6+
public struct I32 has copy, drop, store {
7+
bits: u32,
8+
}
9+
10+
public fun wrapping_add(num1: I32, num2: I32): I32 {
11+
let mut sum = num1.bits ^ num2.bits;
12+
let mut carry = (num1.bits & num2.bits) << 1;
13+
invariant!(|| {
14+
ensures(
15+
((num1.bits as u64) + (num2.bits as u64)) % (1 << 32) == ((sum as u64) + (carry as u64)) % (1 << 32),
16+
);
17+
});
18+
while (carry != 0) {
19+
let a = sum;
20+
let b = carry;
21+
sum = a ^ b;
22+
carry = (a & b) << 1;
23+
};
24+
I32 {
25+
bits: sum,
26+
}
27+
}
28+
29+
/*
30+
✅ Computes `num1 + num2` with wrapping overflow.
31+
⏮️ The function does not abort.
32+
*/
33+
#[spec(prove, target = wrapping_add)]
34+
public fun wrapping_add_spec(num1: I32, num2: I32): I32 {
35+
let result = wrapping_add(num1, num2);
36+
ensures(result.bits == (((num1.bits as u64) + (num2.bits as u64)) % (1 << 32)) as u32);
37+
result
38+
}
39+
40+
public fun shr(v: I32, shift: u8): I32 {
41+
if (shift == 0) {
42+
return v
43+
};
44+
let mask = 0xffffffff << (32 - shift);
45+
if (sign(v) == 1) {
46+
return I32 {
47+
bits: (v.bits >> shift) | mask,
48+
}
49+
};
50+
I32 {
51+
bits: v.bits >> shift,
52+
}
53+
}
54+
55+
public fun sign(v: I32): u8 {
56+
((v.bits >> 31) as u8)
57+
}
58+
59+
public native fun ashr(x: u32, y: u32): u32;
60+
61+
/*
62+
✅ Computes arithmetic right shift `v >> shift`.
63+
⏮️ The function aborts unless `shift < 32`.
64+
*/
65+
#[spec(prove, target = shr)]
66+
public fun shr_spec(v: I32, shift: u8): I32 {
67+
asserts(shift < 32);
68+
let result = shr(v, shift);
69+
ensures(result.bits == ashr(v.bits, shift as u32));
70+
result
71+
}

‎specs-bv/sources/i64.move‎

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
module integer_library_specs_bv::i64;
2+
3+
#[spec_only]
4+
use prover::prover::{ensures, asserts, invariant};
5+
6+
public struct I64 has copy, drop, store {
7+
bits: u64,
8+
}
9+
10+
public fun wrapping_add(num1: I64, num2: I64): I64 {
11+
let mut sum = num1.bits ^ num2.bits;
12+
let mut carry = (num1.bits & num2.bits) << 1;
13+
invariant!(|| {
14+
ensures(
15+
((num1.bits as u128) + (num2.bits as u128)) % (1 << 64) == ((sum as u128) + (carry as u128)) % (1 << 64),
16+
);
17+
});
18+
while (carry != 0) {
19+
let a = sum;
20+
let b = carry;
21+
sum = a ^ b;
22+
carry = (a & b) << 1;
23+
};
24+
I64 {
25+
bits: sum,
26+
}
27+
}
28+
29+
/*
30+
✅ Computes `num1 + num2` with wrapping overflow.
31+
⏮️ The function does not abort.
32+
*/
33+
#[spec(prove, target = wrapping_add)]
34+
public fun wrapping_add_spec(num1: I64, num2: I64): I64 {
35+
let result = wrapping_add(num1, num2);
36+
ensures(result.bits == (((num1.bits as u128) + (num2.bits as u128)) % (1 << 64)) as u64);
37+
result
38+
}
39+
40+
public fun shr(v: I64, shift: u8): I64 {
41+
if (shift == 0) {
42+
return v
43+
};
44+
let mask = 0xffffffffffffffff << (64 - shift);
45+
if (sign(v) == 1) {
46+
return I64 {
47+
bits: (v.bits >> shift) | mask,
48+
}
49+
};
50+
I64 {
51+
bits: v.bits >> shift,
52+
}
53+
}
54+
55+
public fun sign(v: I64): u8 {
56+
((v.bits >> 63) as u8)
57+
}
58+
59+
public native fun ashr(x: u64, y: u64): u64;
60+
61+
/*
62+
✅ Computes arithmetic right shift `v >> shift`.
63+
⏮️ The function aborts unless `shift < 64`.
64+
*/
65+
#[spec(prove, target = shr)]
66+
public fun shr_spec(v: I64, shift: u8): I64 {
67+
asserts(shift < 64);
68+
let result = shr(v, shift);
69+
ensures(result.bits == ashr(v.bits, shift as u64));
70+
result
71+
}

0 commit comments

Comments
 (0)