-
Notifications
You must be signed in to change notification settings - Fork 8
Ensured that the Supra protocol configuration settings are stored in the Move state. #84
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
Changes from 1 commit
05c67bf
24c1596
c3b2495
617e383
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
- Loading branch information
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,83 @@ | ||
spec supra_framework::supra_config { | ||
/// <high-level-req> | ||
/// No.: 1 | ||
/// Requirement: During genesis, the Supra framework account should be assigned the supra config resource. | ||
/// Criticality: Medium | ||
/// Implementation: The supra_config::initialize function calls the assert_supra_framework function to ensure | ||
/// that the signer is the supra_framework and then assigns the SupraConfig resource to it. | ||
/// Enforcement: Formally verified via [high-level-req-1](initialize). | ||
/// | ||
/// No.: 2 | ||
/// Requirement: Only aptos framework account is allowed to update the supra protocol configuration. | ||
/// Criticality: Medium | ||
/// Implementation: The supra_config::set function ensures that the signer is supra_framework. | ||
/// Enforcement: Formally verified via [high-level-req-2](set). | ||
/// | ||
/// No.: 3 | ||
/// Requirement: Only a valid configuration can be used during initialization and update. | ||
/// 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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Curious: What does this check do? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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. |
||
} | ||
} | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. @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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. As we discussed, I'll raise a new issue so that @axiongsupra can double check. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. @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. |
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.
Should this be Supra framework?
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.
Yes. I didn't update the docs very carefully. We'll have to update that in future PR.