Ensured that the Supra protocol configuration settings are stored in the Move state. #84
Conversation
This file contains hidden or 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
… flow. Also added a script to run the unit tests that we care about.
… length requirements enforced in the SC.
sjoshisupra
requested changes
Sep 26, 2024
aptos-move/framework/supra-framework/sources/configs/supra_config.move
Outdated
Show resolved
Hide resolved
Comment on lines
18
to
83
| /// Criticality: Medium | ||
| /// Implementation: Both the initialize and set functions validate the config by ensuring its length to be greater | ||
| /// than 0. | ||
| /// Enforcement: Formally verified via [high-level-req-3.1](initialize) and [high-level-req-3.2](set). | ||
| /// </high-level-req> | ||
| /// | ||
| spec module { | ||
| use supra_framework::chain_status; | ||
| pragma verify = true; | ||
| pragma aborts_if_is_strict; | ||
| invariant [suspendable] chain_status::is_operating() ==> exists<SupraConfig>(@supra_framework); | ||
| } | ||
|
|
||
| /// Ensure caller is admin. | ||
| /// Aborts if StateStorageUsage already exists. | ||
| spec initialize(supra_framework: &signer, config: vector<u8>) { | ||
| use std::signer; | ||
| let addr = signer::address_of(supra_framework); | ||
| /// [high-level-req-1] | ||
| aborts_if !system_addresses::is_supra_framework_address(addr); | ||
| aborts_if exists<SupraConfig>(@supra_framework); | ||
| /// [high-level-req-3.1] | ||
| aborts_if !(len(config) > 0); | ||
| ensures global<SupraConfig>(addr) == SupraConfig { config }; | ||
| } | ||
|
|
||
| /// Ensure the caller is admin and `SupraConfig` should exist. | ||
| /// When setting now time must be later than last_reconfiguration_time. | ||
| spec set(account: &signer, config: vector<u8>) { | ||
| use supra_framework::chain_status; | ||
| use supra_framework::timestamp; | ||
| use std::signer; | ||
| use supra_framework::stake; | ||
| use supra_framework::coin::CoinInfo; | ||
| use supra_framework::supra_coin::SupraCoin; | ||
| use supra_framework::transaction_fee; | ||
| use supra_framework::staking_config; | ||
|
|
||
| // TODO: set because of timeout (property proved) | ||
| pragma verify_duration_estimate = 600; | ||
| include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply; | ||
| include staking_config::StakingRewardsConfigRequirement; | ||
| let addr = signer::address_of(account); | ||
| /// [high-level-req-2] | ||
| aborts_if !system_addresses::is_supra_framework_address(addr); | ||
| aborts_if !exists<SupraConfig>(@supra_framework); | ||
| /// [high-level-req-3.2] | ||
| aborts_if !(len(config) > 0); | ||
|
|
||
| requires chain_status::is_genesis(); | ||
| requires timestamp::spec_now_microseconds() >= reconfiguration::last_reconfiguration_time(); | ||
| requires exists<stake::ValidatorFees>(@supra_framework); | ||
| requires exists<CoinInfo<SupraCoin>>(@supra_framework); | ||
| ensures global<SupraConfig>(@supra_framework).config == config; | ||
| } | ||
|
|
||
| spec set_for_next_epoch(account: &signer, config: vector<u8>) { | ||
| include config_buffer::SetForNextEpochAbortsIf; | ||
| } | ||
|
|
||
| spec on_new_epoch(framework: &signer) { | ||
| requires @supra_framework == std::signer::address_of(framework); | ||
| include config_buffer::OnNewEpochRequirement<SupraConfig>; | ||
| aborts_if false; | ||
| } | ||
| } |
There was a problem hiding this comment.
@isaacdoidge did you run the prover on this? If not, perhaps this file can be dropped for now or file an issue and assign it to @axiongsupra who will rewrite (if necessary) the specs.
There was a problem hiding this comment.
I changed the values that should have needed to change according to the modifications that I made to the contract. What command do I use to run the prover?
There was a problem hiding this comment.
As we discussed, I'll raise a new issue so that @axiongsupra can double check.
There was a problem hiding this comment.
@isaacdoidge @sjoshisupra I confirm the prover works fine with the spec if I merge #63. I will looking to the details and see whether the property is correct.
sjoshisupra
approved these changes
Sep 26, 2024
supra-yoga
reviewed
Sep 26, 2024
| /// Enforcement: Formally verified via [high-level-req-1](initialize). | ||
| /// | ||
| /// No.: 2 | ||
| /// Requirement: Only aptos framework account is allowed to update the supra protocol configuration. |
There was a problem hiding this comment.
Suggested change
| /// Requirement: Only aptos framework account is allowed to update the supra protocol configuration. | |
| /// Requirement: Only supra framework account is allowed to update the supra protocol configuration. |
Should this be Supra framework?
There was a problem hiding this comment.
Yes. I didn't update the docs very carefully. We'll have to update that in future PR.
| spec on_new_epoch(framework: &signer) { | ||
| requires @supra_framework == std::signer::address_of(framework); | ||
| include config_buffer::OnNewEpochRequirement<SupraConfig>; | ||
| aborts_if false; |
There was a problem hiding this comment.
Not sure tbh. I just copied the spec for consensus_config and changed it in the same way that I changed the contract itself. @axiongsupra will double check to make sure everything's alright.
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.
See #83. Copied
consensus_config.moveand removed the unnecessary methods but otherwise made only minor changes to the contract. Its documentation can be improved in a future PR. I have integrated this change intosmr-moonshotand confirmed that it works as expected.