[Spec] Added specs for module block & aptos_account & state_storage #5478
Conversation
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
junkil-park
reviewed
Nov 9, 2022
| spec aptos_framework::aptos_account { | ||
| spec module { | ||
| pragma verify = true; | ||
| pragma aborts_if_is_strict; |
There was a problem hiding this comment.
I am wondering why aborts_if_is_strict is here?
There was a problem hiding this comment.
This is to ensure all the functions are verified in this module.
junkil-park
reviewed
Nov 9, 2022
| @@ -1,20 +1,39 @@ | |||
| spec aptos_framework::state_storage { | |||
| spec module { | |||
| use aptos_std::chain_status; | |||
| pragma verify = true; | |||
| pragma aborts_if_is_strict; | |||
There was a problem hiding this comment.
Same question. I am wondering why aborts_if_is_strict is here?
There was a problem hiding this comment.
This is to ensure all the functions are verified in this module.
0xOutOfGas
requested review from
junkil-park
and removed request for
rahxephon89
movekevin
reviewed
Nov 11, 2022
| aptos_framework: &signer, | ||
| new_epoch_interval: u64, | ||
| ) { | ||
| include Update_epoch_interval_microsecs; |
There was a problem hiding this comment.
Not: Why capitalize here? And other places as well
There was a problem hiding this comment.
Changed naming style to camelcase.
There was a problem hiding this comment.
Yeah, a convention is that schema names are in camelcase without _. I see this is corrected in the newer commit pushed.
junkil-park
reviewed
Nov 14, 2022
| // TODO: temporary mockup. | ||
| pragma opaque; | ||
| aborts_if false; | ||
| } | ||
|
|
||
| spec on_reconfig { |
There was a problem hiding this comment.
Could you add the comment that this function is supposed to abort always because it has been deprecated?
junkil-park
reviewed
Nov 14, 2022
| aborts_if addr != @aptos_framework; | ||
| aborts_if new_epoch_interval <= 0; | ||
| aborts_if !exists<BlockResource>(addr); | ||
| ensures exists<BlockResource>(addr); |
There was a problem hiding this comment.
What's the reason for this to be re-ensured?
There was a problem hiding this comment.
The ensures here is indeed inappropriate. It has been re-modified.
junkil-park
approved these changes
Nov 14, 2022
movekevin
approved these changes
Nov 14, 2022
…eginning() and modify the inappropriate ensures of update_epoch_interval_microsecs()
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
✅ Forge suite
|
✅ Forge suite
|
areshand
pushed a commit
to areshand/aptos-core-1
that referenced
this pull request
Dec 18, 2022
…ptos-labs#5478) * add account.move,coin.move spec * remove coin.spec.move aborts_if_is_strict * update specs for account.move and coin.move * update account.move,coin.move spec * add account.move,coin.move spec comments * Merge aptos:main * Generate account.move.coin.move spec doc * Trim coin.move spec trailing whitespace * add spec for aptos_account & block & state_storage * Generate aptos_account & block & state_storage spec * Changed schema naming style for block and aptos_account to camelcase * Remove the aborts if false of get_state_storage_usage_only_at_epoch_beginning() and modify the inappropriate ensures of update_epoch_interval_microsecs() Co-authored-by: tiutiutiu <qiu971009@gmail.com> Co-authored-by: 英雄造时势 <zhangping_ymd@outlook.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description
This is a part of spec work for Aptos Framework from MoveBit, we updated below files/modules in this PR:
Test Plan
This change is