forked from aptos-labs/aptos-core
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[Spec] Specs for math64, math128 and type_info (aptos-labs#5341)
- Specified the `math64` and `math128` modules - Updated the spec of `type_info` - `type_of` and `type_name` are natively supported by Prover now. - added a `[verify_only]` function to test the feature TODO: - the `pow` functions have non trivial loops, which still need abort-conditions and loop invariants.
- Loading branch information
1 parent
8958b01
commit 40ffbdf
Showing
9 changed files
with
314 additions
and
32 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
36 changes: 36 additions & 0 deletions
36
aptos-move/framework/aptos-stdlib/sources/math128.spec.move
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,36 @@ | ||
| spec aptos_std::math128 { | ||
|
|
||
| spec max(a: u128, b: u128): u128 { | ||
| aborts_if false; | ||
| ensures a >= b ==> result == a; | ||
| ensures a < b ==> result == b; | ||
| } | ||
|
|
||
| spec min(a: u128, b: u128): u128 { | ||
| aborts_if false; | ||
| ensures a < b ==> result == a; | ||
| ensures a >= b ==> result == b; | ||
| } | ||
|
|
||
| spec average(a: u128, b: u128): u128 { | ||
| pragma opaque; | ||
| aborts_if false; | ||
| ensures result == (a + b) / 2; | ||
| } | ||
|
|
||
| spec pow(n: u128, e: u128): u128 { | ||
| pragma opaque; | ||
| // TODO: verify the spec. | ||
| aborts_if [abstract] spec_pow(n, e) > MAX_U128; | ||
| ensures [abstract] result == spec_pow(n, e); | ||
| } | ||
|
|
||
| spec fun spec_pow(e: u128, n: u128): u128 { | ||
| if (e == 0) { | ||
| 1 | ||
| } | ||
| else { | ||
| n * spec_pow(n, e-1) | ||
| } | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
36 changes: 36 additions & 0 deletions
36
aptos-move/framework/aptos-stdlib/sources/math64.spec.move
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,36 @@ | ||
| spec aptos_std::math64 { | ||
|
|
||
| spec max(a: u64, b: u64): u64 { | ||
| aborts_if false; | ||
| ensures a >= b ==> result == a; | ||
| ensures a < b ==> result == b; | ||
| } | ||
|
|
||
| spec min(a: u64, b: u64): u64 { | ||
| aborts_if false; | ||
| ensures a < b ==> result == a; | ||
| ensures a >= b ==> result == b; | ||
| } | ||
|
|
||
| spec average(a: u64, b: u64): u64 { | ||
| pragma opaque; | ||
| aborts_if false; | ||
| ensures result == (a + b) / 2; | ||
| } | ||
|
|
||
| spec pow(n: u64, e: u64): u64 { | ||
| pragma opaque; | ||
| // TODO: verify the spec. | ||
| aborts_if [abstract] spec_pow(n, e) > MAX_U64; | ||
| ensures [abstract] result == spec_pow(n, e); | ||
| } | ||
|
|
||
| spec fun spec_pow(e: u64, n: u64): u64 { | ||
| if (e == 0) { | ||
| 1 | ||
| } | ||
| else { | ||
| n * spec_pow(n, e-1) | ||
| } | ||
| } | ||
| } |
Oops, something went wrong.