-
Notifications
You must be signed in to change notification settings - Fork 3.7k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[Spec] Added specs for module gas_schedule & aptos_coin & chain_id & …
…chain_status. (#5771) * Updated the spec of gas_schedule * add aptos_coin & chain_id & chain_status spec * Generate spec doc * Updated chain_status.spec.move * Updated chain_status.spec.move * Generate spec doc Co-authored-by: yoyoping <[email protected]> Co-authored-by: tiutiutiu <[email protected]>
- Loading branch information
3 people
authored
Dec 13, 2022
1 parent
a2e4dc6
commit 8072655
Showing
10 changed files
with
374 additions
and
10 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
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
43 changes: 43 additions & 0 deletions
43
aptos-move/framework/aptos-framework/sources/aptos_coin.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,43 @@ | ||
| spec aptos_framework::aptos_coin { | ||
| spec module { | ||
| pragma verify = true; | ||
| pragma aborts_if_is_strict; | ||
| } | ||
|
|
||
| spec initialize { | ||
| pragma aborts_if_is_partial; | ||
| let addr = signer::address_of(aptos_framework); | ||
| ensures exists<MintCapStore>(addr); | ||
| ensures exists<coin::CoinInfo<AptosCoin>>(addr); | ||
| } | ||
|
|
||
| spec destroy_mint_cap { | ||
| let addr = signer::address_of(aptos_framework); | ||
| aborts_if addr != @aptos_framework; | ||
| aborts_if !exists<MintCapStore>(@aptos_framework); | ||
| } | ||
|
|
||
| // Test function,not needed verify. | ||
| spec configure_accounts_for_test { | ||
| pragma verify = false; | ||
| } | ||
|
|
||
| // Only callable in tests and testnets.not needed verify. | ||
| spec mint { | ||
| pragma verify = false; | ||
| } | ||
|
|
||
| // Only callable in tests and testnets.not needed verify. | ||
| spec delegate_mint_capability { | ||
| pragma verify = false; | ||
| } | ||
|
|
||
| // Only callable in tests and testnets.not needed verify. | ||
| spec claim_mint_capability(account: &signer) { | ||
| pragma verify = false; | ||
| } | ||
|
|
||
| spec find_delegation(addr: address): Option<u64> { | ||
| aborts_if !exists<Delegations>(@core_resources); | ||
| } | ||
| } |
Oops, something went wrong.