-
Notifications
You must be signed in to change notification settings - Fork 3.6k
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
[Spec] Added specs for module gas_schedule & aptos_coin & chain_id & chain_status. #5771
Conversation
spec set_genesis_end { | ||
pragma verify = false; | ||
} | ||
|
||
spec schema RequiresIsOperating { | ||
requires is_operating(); | ||
requires !is_operating(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why is this negated?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@junkil-park Sorry, this was a mistake. Fixed.
@@ -1,6 +1,10 @@ | |||
spec aptos_framework::util { | |||
spec from_bytes { | |||
spec from_bytes<T>(bytes: vector<u8>): T { | |||
// TODO: temporary mockup. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This comment line can be deleted.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have deleted this.
This PR looks good overall. I left some comments. |
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
✅ Forge suite
|
✅ Forge suite
|
…chain_status. (aptos-labs#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 <zhangping_ymd@outlook.com> Co-authored-by: tiutiutiu <qiu971009@gmail.com>
Description
This is a part of spec work for Aptos Framework from MoveBit, we updated below files/modules in this PR:
Test Plan
aptos move prove --package-dir ./aptos-framework