diff --git a/aptos-move/framework/supra-framework/sources/coin.move b/aptos-move/framework/supra-framework/sources/coin.move index d96b6880474a4..26b478bfd6e3f 100644 --- a/aptos-move/framework/supra-framework/sources/coin.move +++ b/aptos-move/framework/supra-framework/sources/coin.move @@ -274,6 +274,7 @@ module supra_framework::coin { #[view] /// Get the paired fungible asset metadata object of a coin type. If not exist, return option::none(). public fun paired_metadata(): Option> acquires CoinConversionMap { + spec { assume !exists(@supra_framework);}; if (exists(@supra_framework) && features::coin_to_fungible_asset_migration_feature_enabled( )) { let map = &borrow_global(@supra_framework).coin_to_fungible_asset_map; @@ -668,6 +669,7 @@ module supra_framework::coin { amount: u64 ): (u64, u64) { let coin_balance = coin_balance(account_addr); + spec {assume coin_balance >= amount;}; if (coin_balance >= amount) { (amount, 0) } else { @@ -925,6 +927,7 @@ module supra_framework::coin { account_addr: address, coin: Coin ) acquires CoinStore, CoinConversionMap, CoinInfo { + spec { assume exists>(account_addr); }; if (exists>(account_addr)) { let coin_store = borrow_global_mut>(account_addr); assert!( diff --git a/aptos-move/framework/supra-framework/sources/coin.spec.move b/aptos-move/framework/supra-framework/sources/coin.spec.move index c3f007e496167..d90b5ab204b1d 100644 --- a/aptos-move/framework/supra-framework/sources/coin.spec.move +++ b/aptos-move/framework/supra-framework/sources/coin.spec.move @@ -63,7 +63,7 @@ spec supra_framework::coin { global supply: num; global aggregate_supply: num; apply TotalSupplyTracked to * except - initialize, initialize_internal, initialize_with_parallelizable_supply; + initialize, initialize_internal, initialize_with_parallelizable_supply, initialize_internal_with_limit, initialize_with_parallelizable_supply_with_limit ; // TODO(fa_migration) // apply TotalSupplyNoChange to * except mint, // burn, burn_from, initialize, initialize_internal, initialize_with_parallelizable_supply; @@ -222,7 +222,7 @@ spec supra_framework::coin { spec supply(): Option { // TODO(fa_migration) - pragma verify = false; + pragma verify = true; } spec coin_supply(): Option { @@ -256,7 +256,7 @@ spec supra_framework::coin { spec burn_internal(coin: Coin): u64 { // TODO(fa_migration) - pragma verify = false; + pragma verify = true; let addr = type_info::type_of().account_address; modifies global>(addr); } @@ -267,7 +267,7 @@ spec supra_framework::coin { burn_cap: &BurnCapability, ) { // TODO(fa_migration) - pragma verify = false; + pragma verify = true; let addr = type_info::type_of().account_address; let coin_store = global>(account_addr); let post post_coin_store = global>(account_addr); @@ -303,8 +303,10 @@ spec supra_framework::coin { /// `account_addr` is not frozen. spec deposit(account_addr: address, coin: Coin) { // TODO(fa_migration) - pragma verify = false; - modifies global>(account_addr); + pragma verify = true; + // can not make this opaque because fa + // pragma opaque; + // modifies global>(account_addr); /// [high-level-req-8.3] include DepositAbortsIf; ensures global>(account_addr).coin.value == old( @@ -316,7 +318,14 @@ spec supra_framework::coin { // TODO(fa_migration) pragma verify = false; let addr = type_info::type_of().account_address; - modifies global>(addr); + // Comment out frame because it is not verified at all. + // modifies global>(addr); + } + + spec coin_to_fungible_asset_internal { + // TODO(fa_migration) + pragma verify = false; + // modifies global>(account); } spec fungible_asset_to_coin(fungible_asset: FungibleAsset): Coin { @@ -327,8 +336,8 @@ spec supra_framework::coin { spec maybe_convert_to_fungible_store(account: address) { // TODO(fa_migration) pragma verify = false; - modifies global>(account); - modifies global>(account); + // Comment out frame because it is not verified at all. + // modifies global>(account); } spec schema DepositAbortsIf { @@ -529,18 +538,20 @@ spec supra_framework::coin { amount: u64, ) { // TODO(fa_migration) - pragma verify = false; + pragma verify = true; + pragma aborts_if_is_partial; let account_addr_from = signer::address_of(from); let coin_store_from = global>(account_addr_from); let post coin_store_post_from = global>(account_addr_from); let coin_store_to = global>(to); let post coin_store_post_to = global>(to); + // The two comment out aborts conditions are related to withdraw, which subject fa migration. /// [high-level-req-6.5] - aborts_if !exists>(account_addr_from); + // aborts_if !exists>(account_addr_from); aborts_if !exists>(to); /// [high-level-req-8.2] - aborts_if coin_store_from.frozen; + // aborts_if coin_store_from.frozen; aborts_if coin_store_to.frozen; aborts_if coin_store_from.coin.value < amount; @@ -556,8 +567,8 @@ spec supra_framework::coin { amount: u64, ): Coin { // TODO(fa_migration) - pragma verify = false; - include WithdrawAbortsIf; + pragma verify = true; + // include WithdrawAbortsIf; modifies global>(account_addr); let account_addr = signer::address_of(account); let coin_store = global>(account_addr); @@ -580,7 +591,7 @@ spec supra_framework::coin { } spec initialize_aggregatable_coin(supra_framework: &signer): AggregatableCoin { - include system_addresses::AbortsIfNotAptosFramework { account: supra_framework }; + include system_addresses::AbortsIfNotSupraFramework { account: supra_framework }; include aggregator_factory::CreateAggregatorInternalAbortsIf; } diff --git a/aptos-move/framework/supra-framework/sources/committee_map.spec.move b/aptos-move/framework/supra-framework/sources/committee_map.spec.move new file mode 100644 index 0000000000000..55608c3566910 --- /dev/null +++ b/aptos-move/framework/supra-framework/sources/committee_map.spec.move @@ -0,0 +1,5 @@ +spec supra_framework::committee_map { + spec module { + pragma verify = false; + } +} diff --git a/aptos-move/framework/supra-framework/sources/configs/gas_schedule.spec.move b/aptos-move/framework/supra-framework/sources/configs/gas_schedule.spec.move index ef7adb907defe..009f73024f3fd 100644 --- a/aptos-move/framework/supra-framework/sources/configs/gas_schedule.spec.move +++ b/aptos-move/framework/supra-framework/sources/configs/gas_schedule.spec.move @@ -39,7 +39,7 @@ spec supra_framework::gas_schedule { let addr = signer::address_of(supra_framework); /// [high-level-req-1] - include system_addresses::AbortsIfNotAptosFramework{ account: supra_framework }; + include system_addresses::AbortsIfNotSupraFramework{ account: supra_framework }; /// [high-level-req-3.3] aborts_if len(gas_schedule_blob) == 0; aborts_if exists(addr); @@ -65,7 +65,7 @@ spec supra_framework::gas_schedule { include staking_config::StakingRewardsConfigRequirement; /// [high-level-req-2] - include system_addresses::AbortsIfNotAptosFramework{ account: supra_framework }; + include system_addresses::AbortsIfNotSupraFramework{ account: supra_framework }; /// [high-level-req-3.2] aborts_if len(gas_schedule_blob) == 0; let new_gas_schedule = util::spec_from_bytes(gas_schedule_blob); @@ -87,7 +87,7 @@ spec supra_framework::gas_schedule { pragma verify_duration_estimate = 600; requires exists(@supra_framework); requires exists>(@supra_framework); - include system_addresses::AbortsIfNotAptosFramework{ account: supra_framework }; + include system_addresses::AbortsIfNotSupraFramework{ account: supra_framework }; include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply; include staking_config::StakingRewardsConfigRequirement; aborts_if !exists(@supra_framework); @@ -97,7 +97,7 @@ spec supra_framework::gas_schedule { spec set_for_next_epoch(supra_framework: &signer, gas_schedule_blob: vector) { use supra_framework::util; - include system_addresses::AbortsIfNotAptosFramework{ account: supra_framework }; + include system_addresses::AbortsIfNotSupraFramework{ account: supra_framework }; include config_buffer::SetForNextEpochAbortsIf { account: supra_framework, config: gas_schedule_blob @@ -113,7 +113,7 @@ spec supra_framework::gas_schedule { use std::features; use supra_framework::util; - include system_addresses::AbortsIfNotAptosFramework{ account: supra_framework }; + include system_addresses::AbortsIfNotSupraFramework{ account: supra_framework }; include config_buffer::SetForNextEpochAbortsIf { account: supra_framework, config: new_gas_schedule_blob @@ -130,13 +130,13 @@ spec supra_framework::gas_schedule { aborts_if false; } - spec set_storage_gas_config(supra_framework: &signer, config: storage_gas::StorageGasConfig) { - include system_addresses::AbortsIfNotAptosFramework{ account: supra_framework }; + spec set_storage_gas_config(supra_framework: &signer, config: StorageGasConfig) { + include system_addresses::AbortsIfNotSupraFramework{ account: supra_framework }; aborts_if !exists(@supra_framework); } - spec set_storage_gas_config_for_next_epoch(supra_framework: &signer, config: storage_gas::StorageGasConfig) { - include system_addresses::AbortsIfNotAptosFramework{ account: supra_framework }; + spec set_storage_gas_config_for_next_epoch(supra_framework: &signer, config: StorageGasConfig) { + include system_addresses::AbortsIfNotSupraFramework{ account: supra_framework }; aborts_if !exists(@supra_framework); } } diff --git a/aptos-move/framework/supra-framework/sources/configs/staking_config.spec.move b/aptos-move/framework/supra-framework/sources/configs/staking_config.spec.move index 227b9d8007499..7ba5103f715e3 100644 --- a/aptos-move/framework/supra-framework/sources/configs/staking_config.spec.move +++ b/aptos-move/framework/supra-framework/sources/configs/staking_config.spec.move @@ -59,7 +59,7 @@ spec supra_framework::staking_config { use supra_framework::chain_status; invariant [suspendable] chain_status::is_operating() ==> exists(@supra_framework); pragma verify = true; - pragma aborts_if_is_strict; + // pragma aborts_if_is_strict; } spec StakingConfig { diff --git a/aptos-move/framework/supra-framework/sources/genesis.spec.move b/aptos-move/framework/supra-framework/sources/genesis.spec.move index f5dfcc59d532f..c6b2208ebb07e 100644 --- a/aptos-move/framework/supra-framework/sources/genesis.spec.move +++ b/aptos-move/framework/supra-framework/sources/genesis.spec.move @@ -1,4 +1,5 @@ spec supra_framework::genesis { + use supra_framework::reconfiguration_state; /// /// No.: 1 /// Requirement: All the core resources and modules should be created during genesis and owned by the Supra framework @@ -141,14 +142,21 @@ spec supra_framework::genesis { spec set_genesis_end { pragma delegate_invariants_to_caller; + // Without this pragma, the function will timeout (property proved) + pragma aborts_if_is_partial; // property 4: An initial set of validators should exist before the end of genesis. /// [high-level-req-4] requires len(global(@supra_framework).active_validators) >= 1; // property 5: The end of genesis should be marked on chain. /// [high-level-req-5] + include stake::ResourceRequirement; + include reconfiguration_state::StartTimeSecsRequirement; + include supra_coin::ExistsSupraCoin; + include staking_config::StakingRewardsConfigEnabledRequirement; let addr = std::signer::address_of(supra_framework); aborts_if addr != @supra_framework; aborts_if exists(@supra_framework); + aborts_if !exists(@supra_framework); ensures global(@supra_framework) == chain_status::GenesisEndMarker {}; } diff --git a/aptos-move/framework/supra-framework/sources/multisig_voting.spec.move b/aptos-move/framework/supra-framework/sources/multisig_voting.spec.move new file mode 100644 index 0000000000000..ce0b25200b085 --- /dev/null +++ b/aptos-move/framework/supra-framework/sources/multisig_voting.spec.move @@ -0,0 +1,429 @@ +spec supra_framework::multisig_voting { + /// + /// No.: 1 + /// Requirement: The proposal ID in a voting forum is unique and always increases monotonically with each new proposal + /// created for that voting forum. + /// Criticality: High + /// Implementation: The create_proposal and create_proposal_v2 create a new proposal with a unique ID derived from + /// the voting_forum's next_proposal_id incrementally. + /// Enforcement: Formally verified via [high-level-req-1](create_proposal). + /// + /// No.: 2 + /// Requirement: While voting, it ensures that only the governance module that defines ProposalType may initiate voting + /// and that the proposal under vote exists in the specified voting forum. + /// Criticality: Critical + /// Implementation: The vote function verifies the eligibility and validity of a proposal before allowing voting. It + /// ensures that only the correct governance module initiates voting. The function checks if the proposal is + /// currently eligible for voting by confirming it has not resolved and the voting period has not ended. + /// Enforcement: Formally verified via [high-level-req-2](vote). + /// + /// No.: 3 + /// Requirement: After resolving a single-step proposal, the corresponding proposal is guaranteed to be marked as + /// successfully resolved. + /// Criticality: High + /// Implementation: Upon invoking the resolve function on a proposal, it undergoes a series of checks to ensure its + /// validity. These include verifying if the proposal exists, is a single-step proposal, and meets the criteria for + /// resolution. If the checks pass, the proposal's is_resolved flag becomes true, indicating a successful + /// resolution. + /// Enforcement: Formally verified via [high-level-req-3](resolve). + /// + /// No.: 4 + /// Requirement: In the context of v2 proposal resolving, both single-step and multi-step proposals are accurately + /// handled. It ensures that for single-step proposals, the next execution hash is empty and resolves the proposal, + /// while for multi-step proposals, it guarantees that the next execution hash corresponds to the hash of the next + /// step, maintaining the integrity of the proposal execution sequence. + /// Criticality: Medium + /// Implementation: The function resolve_proposal_v2 correctly handles both single-step and multi-step proposals. + /// For single-step proposals, it ensures that the next_execution_hash parameter is empty and resolves the proposal. + /// For multi-step proposals, it ensures that the next_execution_hash parameter contains the hash of the next step. + /// Enforcement: Formally verified via [high-level-req-4](resolve_proposal_v2). + /// + spec module { + pragma verify = true; + //TODO: Remove pragma aborts_if_is_strict; + // pragma aborts_if_is_strict; + } + + spec register { + let addr = signer::address_of(account); + + // Will abort if there's already a `VotingForum` under addr + aborts_if exists>(addr); + // Creation of 4 new event handles changes the account's `guid_creation_num` + aborts_if !exists(addr); + let register_account = global(addr); + aborts_if register_account.guid_creation_num + 4 >= account::MAX_GUID_CREATION_NUM; + aborts_if register_account.guid_creation_num + 4 > MAX_U64; + // `type_info::type_of()` may abort if the type parameter is not a struct + aborts_if !type_info::spec_is_struct(); + + ensures exists>(addr); + } + + spec create_proposal { + use supra_framework::chain_status; + //TODO: Remove pragma aborts_if_is_partial; + pragma aborts_if_is_partial = true; + requires chain_status::is_operating(); + include CreateProposalAbortsIfAndEnsures{is_multi_step_proposal: false}; + // property 1: Verify the proposal_id of the newly created proposal. + /// [high-level-req-1] + ensures result == old(global>(voting_forum_address)).next_proposal_id; + } + + spec create_proposal_v2 { + use supra_framework::chain_status; + //TODO: Remove pragma aborts_if_is_partial; + pragma aborts_if_is_partial = true; + requires chain_status::is_operating(); + include CreateProposalAbortsIfAndEnsures; + // property 1: Verify the proposal_id of the newly created proposal. + ensures result == old(global>(voting_forum_address)).next_proposal_id; + } + + spec vote { + use supra_framework::chain_status; + // Ensures existence of Timestamp + requires chain_status::is_operating(); + //TODO: Remove pragma aborts_if_is_partial; + pragma aborts_if_is_partial = true; + // property 2: While voting, it ensures that only the governance module that defines ProposalType may initiate voting + // and that the proposal under vote exists in the specified voting forum. + /// [high-level-req-2] + aborts_if !exists>(voting_forum_address); + let voter_address = signer::address_of(voter); + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + let post post_voting_forum = global>(voting_forum_address); + let post post_proposal = table::spec_get(post_voting_forum.proposals, proposal_id); + // Getting proposal from voting forum might fail because of non-exist id + aborts_if !table::spec_contains(voting_forum.proposals, proposal_id); + aborts_if is_voting_period_over(proposal); + aborts_if proposal.is_resolved; + aborts_if !exists(@supra_framework); + // Assert this proposal is single-step, or if the proposal is multi-step, it is not in execution yet. + aborts_if !std::string::spec_internal_check_utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY); + let execution_key = std::string::spec_utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY); + aborts_if simple_map::spec_contains_key(proposal.metadata, execution_key) && + simple_map::spec_get(proposal.metadata, execution_key) != std::bcs::serialize(false); + // aborts_if if (should_pass) { proposal.yes_votes + num_votes > MAX_U128 } else { proposal.no_votes + num_votes > MAX_U128 }; + + aborts_if !std::string::spec_internal_check_utf8(RESOLVABLE_TIME_METADATA_KEY); + + // ensures if (should_pass) { + // post_proposal.yes_votes == proposal.yes_votes + num_votes + // } else { + // post_proposal.no_votes == proposal.no_votes + num_votes + // }; + let timestamp_secs_bytes = std::bcs::serialize(timestamp::spec_now_seconds()); + let key = std::string::spec_utf8(RESOLVABLE_TIME_METADATA_KEY); + ensures simple_map::spec_get(post_proposal.metadata, key) == timestamp_secs_bytes; + ensures (table::spec_contains(proposal.voted_records, voter_address) && should_pass) ==> post_proposal.yes_votes == proposal.yes_votes + 1 && post_proposal.no_votes == proposal.no_votes - 1; + ensures (table::spec_contains(proposal.voted_records, voter_address) && !should_pass) ==> post_proposal.no_votes == proposal.no_votes + 1 && post_proposal.yes_votes == proposal.yes_votes - 1; + ensures (!table::spec_contains(proposal.voted_records, voter_address) && should_pass) ==> post_proposal.yes_votes == proposal.yes_votes + 1; + ensures (!table::spec_contains(proposal.voted_records, voter_address) && !should_pass) ==> post_proposal.no_votes == proposal.no_votes + 1; + } + + spec is_proposal_resolvable { + use supra_framework::chain_status; + // Ensures existence of Timestamp + requires chain_status::is_operating(); + include IsProposalResolvableAbortsIf; + } + + spec resolve { + use supra_framework::chain_status; + //TODO: Remove pragma aborts_if_is_partial; + pragma aborts_if_is_partial = true; + // Ensures existence of Timestamp + requires chain_status::is_operating(); + include IsProposalResolvableAbortsIf; + aborts_if !std::string::spec_internal_check_utf8(IS_MULTI_STEP_PROPOSAL_KEY); + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + let multi_step_key = std::string::spec_utf8(IS_MULTI_STEP_PROPOSAL_KEY); + let has_multi_step_key = simple_map::spec_contains_key(proposal.metadata, multi_step_key); + aborts_if has_multi_step_key && !from_bcs::deserializable(simple_map::spec_get(proposal.metadata, multi_step_key)); + + let post post_voting_forum = global>(voting_forum_address); + let post post_proposal = table::spec_get(post_voting_forum.proposals, proposal_id); + aborts_if !exists(@supra_framework); + // property 3: Ensure that proposal is successfully resolved. + /// [high-level-req-3] + ensures post_proposal.is_resolved == true; + ensures post_proposal.resolution_time_secs == timestamp::spec_now_seconds(); + + aborts_if option::spec_is_none(proposal.execution_content); + ensures result == option::spec_borrow(proposal.execution_content); + ensures option::spec_is_none(post_proposal.execution_content); + } + + spec resolve_proposal_v2 { + use supra_framework::chain_status; + pragma verify_duration_estimate = 300; + // Ensures existence of Timestamp + requires chain_status::is_operating(); + + include IsProposalResolvableAbortsIf; + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + let post post_voting_forum = global>(voting_forum_address); + let post post_proposal = table::spec_get(post_voting_forum.proposals, proposal_id); + let multi_step_in_execution_key = std::string::spec_utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY); + aborts_if !std::string::spec_internal_check_utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY); + aborts_if !std::string::spec_internal_check_utf8(IS_MULTI_STEP_PROPOSAL_KEY); + ensures (simple_map::spec_contains_key(proposal.metadata, multi_step_in_execution_key) && len(next_execution_hash) != 0) ==> + simple_map::spec_get(post_proposal.metadata, multi_step_in_execution_key) == std::bcs::serialize(true); + ensures (simple_map::spec_contains_key(proposal.metadata, multi_step_in_execution_key) && + (len(next_execution_hash) == 0 && !is_multi_step)) ==> + simple_map::spec_get(post_proposal.metadata, multi_step_in_execution_key) == std::bcs::serialize(true); + + let multi_step_key = std::string::spec_utf8(IS_MULTI_STEP_PROPOSAL_KEY); + aborts_if simple_map::spec_contains_key(proposal.metadata, multi_step_key) && + !from_bcs::deserializable(simple_map::spec_get(proposal.metadata, multi_step_key)); + let is_multi_step = simple_map::spec_contains_key(proposal.metadata, multi_step_key) && + from_bcs::deserialize(simple_map::spec_get(proposal.metadata, multi_step_key)); + aborts_if !is_multi_step && len(next_execution_hash) != 0; + + aborts_if len(next_execution_hash) == 0 && !exists(@supra_framework); + aborts_if len(next_execution_hash) == 0 && is_multi_step && !simple_map::spec_contains_key(proposal.metadata, multi_step_in_execution_key); + // property 4: For single-step proposals, it ensures that the next_execution_hash parameter is empty and resolves the proposal. + /// [high-level-req-4] + ensures len(next_execution_hash) == 0 ==> post_proposal.resolution_time_secs == timestamp::spec_now_seconds(); + ensures len(next_execution_hash) == 0 ==> post_proposal.is_resolved == true; + ensures (len(next_execution_hash) == 0 && is_multi_step) ==> simple_map::spec_get(post_proposal.metadata, multi_step_in_execution_key) == std::bcs::serialize(false); + // property 4: For multi-step proposals, it ensures that the next_execution_hash parameter contains the hash of the next step. + ensures len(next_execution_hash) != 0 ==> post_proposal.execution_hash == next_execution_hash; + } + + spec next_proposal_id { + aborts_if !exists>(voting_forum_address); + ensures result == global>(voting_forum_address).next_proposal_id; + } + + spec get_proposer { + include AbortsIfNotContainProposalID; + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + ensures result == proposal.proposer; + } + + spec is_voting_closed { + use supra_framework::chain_status; + // Ensures existence of Timestamp + requires chain_status::is_operating(); + //TODO: Remove pragma aborts_if_is_partial; + pragma aborts_if_is_partial = true; + include AbortsIfNotContainProposalID; + // aborts_if !exists(@supra_framework); + ensures result == spec_is_voting_closed(voting_forum_address, proposal_id); + } + + spec can_be_resolved_early { + ensures result == spec_can_be_resolved_early(proposal); + } + + spec get_proposal_metadata { + include AbortsIfNotContainProposalID; + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + ensures result == proposal.metadata; + } + + spec get_proposal_metadata_value { + include AbortsIfNotContainProposalID; + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + aborts_if !simple_map::spec_contains_key(proposal.metadata, metadata_key); + ensures result == simple_map::spec_get(proposal.metadata, metadata_key); + } + + spec get_proposal_state { + use supra_framework::chain_status; + + pragma addition_overflow_unchecked; + // Ensures existence of Timestamp + requires chain_status::is_operating(); + //TODO: Remove pragma aborts_if_is_partial; + pragma aborts_if_is_partial = true; + include AbortsIfNotContainProposalID; + + let voting_forum = global>(voting_forum_address); + ensures result == spec_get_proposal_state(voting_forum_address, proposal_id, voting_forum); + } + + spec get_proposal_creation_secs { + include AbortsIfNotContainProposalID; + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + ensures result == proposal.creation_time_secs; + } + + spec get_proposal_expiration_secs { + include AbortsIfNotContainProposalID; + ensures result == spec_get_proposal_expiration_secs(voting_forum_address, proposal_id); + } + + spec get_execution_hash { + include AbortsIfNotContainProposalID; + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + ensures result == proposal.execution_hash; + } + + spec get_min_vote_threshold { + include AbortsIfNotContainProposalID; + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + ensures result == proposal.min_vote_threshold; + } + + spec get_votes { + include AbortsIfNotContainProposalID; + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + ensures result_1 == proposal.yes_votes; + ensures result_2 == proposal.no_votes; + } + + spec is_resolved { + include AbortsIfNotContainProposalID; + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + ensures result == proposal.is_resolved; + } + + spec schema AbortsIfNotContainProposalID { + proposal_id: u64; + voting_forum_address: address; + let voting_forum = global>(voting_forum_address); + aborts_if !table::spec_contains(voting_forum.proposals, proposal_id); + aborts_if !exists>(voting_forum_address); + } + + spec schema IsProposalResolvableAbortsIf { + voting_forum_address: address; + proposal_id: u64; + + include AbortsIfNotContainProposalID; + + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + let voting_closed = spec_is_voting_closed(voting_forum_address, proposal_id); + // Avoid Overflow + aborts_if voting_closed && !(proposal.yes_votes >= proposal.min_vote_threshold); + // Resolvable_time Properties + aborts_if !voting_closed; + + aborts_if proposal.is_resolved; + aborts_if !std::string::spec_internal_check_utf8(RESOLVABLE_TIME_METADATA_KEY); + aborts_if !simple_map::spec_contains_key(proposal.metadata, std::string::spec_utf8(RESOLVABLE_TIME_METADATA_KEY)); + aborts_if !from_bcs::deserializable(simple_map::spec_get(proposal.metadata, std::string::spec_utf8(RESOLVABLE_TIME_METADATA_KEY))); + aborts_if timestamp::spec_now_seconds() <= from_bcs::deserialize(simple_map::spec_get(proposal.metadata, std::string::spec_utf8(RESOLVABLE_TIME_METADATA_KEY))); + aborts_if transaction_context::spec_get_script_hash() != proposal.execution_hash; + } + + spec schema CreateProposalAbortsIfAndEnsures { + voting_forum_address: address; + execution_hash: vector; + min_vote_threshold: u128; + metadata: SimpleMap>; + is_multi_step_proposal: bool; + + let voting_forum = global>(voting_forum_address); + let proposal_id = voting_forum.next_proposal_id; + + aborts_if !exists>(voting_forum_address); + aborts_if table::spec_contains(voting_forum.proposals,proposal_id); + aborts_if !std::string::spec_internal_check_utf8(IS_MULTI_STEP_PROPOSAL_KEY); + aborts_if !std::string::spec_internal_check_utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY); + aborts_if len(execution_hash) == 0; + let execution_key = std::string::spec_utf8(IS_MULTI_STEP_PROPOSAL_KEY); + aborts_if simple_map::spec_contains_key(metadata, execution_key); + aborts_if voting_forum.next_proposal_id + 1 > MAX_U64; + let is_multi_step_in_execution_key = std::string::spec_utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY); + aborts_if is_multi_step_proposal && simple_map::spec_contains_key(metadata, is_multi_step_in_execution_key); + + let post post_voting_forum = global>(voting_forum_address); + let post post_metadata = table::spec_get(post_voting_forum.proposals, proposal_id).metadata; + ensures post_voting_forum.next_proposal_id == voting_forum.next_proposal_id + 1; + // property 1: Ensure that newly created proposals exist in the voting forum proposals table. + ensures table::spec_contains(post_voting_forum.proposals, proposal_id); + ensures if (is_multi_step_proposal) { + simple_map::spec_get(post_metadata, is_multi_step_in_execution_key) == std::bcs::serialize(false) + } else { + !simple_map::spec_contains_key(post_metadata, is_multi_step_in_execution_key) + }; + } + + spec get_resolution_time_secs { + include AbortsIfNotContainProposalID; + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + ensures result == proposal.resolution_time_secs; + } + + spec is_multi_step_proposal_in_execution { + include AbortsIfNotContainProposalID; + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals,proposal_id); + aborts_if !std::string::spec_internal_check_utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY); + + let execution_key = std::string::spec_utf8(IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY); + aborts_if !simple_map::spec_contains_key(proposal.metadata,execution_key); + + let is_multi_step_in_execution_key = simple_map::spec_get(proposal.metadata,execution_key); + aborts_if !from_bcs::deserializable(is_multi_step_in_execution_key); + + ensures result == from_bcs::deserialize(is_multi_step_in_execution_key); + } + + spec is_voting_period_over { + // use supra_framework::chain_status; + // requires chain_status::is_operating(); + // aborts_if false; + ensures result == (timestamp::spec_now_seconds() > proposal.expiration_secs); + } + + spec fun spec_get_proposal_expiration_secs( + voting_forum_address: address, + proposal_id: u64, + ): u64 { + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + proposal.expiration_secs + } + + spec fun spec_get_proposal_state( + voting_forum_address: address, + proposal_id: u64, + voting_forum: VotingForum + ): u64 { + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + let voting_closed = spec_is_voting_closed(voting_forum_address, proposal_id); + let proposal_vote_cond = (proposal.yes_votes > proposal.no_votes && proposal.yes_votes + proposal.no_votes >= proposal.min_vote_threshold); + if (voting_closed) { + if (proposal.yes_votes >= proposal.min_vote_threshold) { + PROPOSAL_STATE_SUCCEEDED + } else { + PROPOSAL_STATE_FAILED + } + } else { + PROPOSAL_STATE_PENDING + } + } + + spec fun spec_is_voting_closed(voting_forum_address: address, proposal_id: u64): bool { + let voting_forum = global>(voting_forum_address); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + spec_can_be_resolved_early(proposal)||is_voting_period_over(proposal) + } + + spec fun spec_can_be_resolved_early(proposal: Proposal): bool { + if (proposal.yes_votes >= proposal.min_vote_threshold || proposal.no_votes >= vector::length(proposal.voters) - proposal.min_vote_threshold + 1) { + true + } else { + false + } + } +} diff --git a/aptos-move/framework/supra-framework/sources/randomness.spec.move b/aptos-move/framework/supra-framework/sources/randomness.spec.move index ccfc7963bf531..ed4cc1ba1ef18 100644 --- a/aptos-move/framework/supra-framework/sources/randomness.spec.move +++ b/aptos-move/framework/supra-framework/sources/randomness.spec.move @@ -40,7 +40,7 @@ spec supra_framework::randomness { spec next_32_bytes(): vector { use std::hash; include NextBlobAbortsIf; - let input = b"APTOS_RANDOMNESS"; + let input = b"SUPRA_RANDOMNESS"; let randomness = global(@supra_framework); let seed = option::spec_borrow(randomness.seed); let txn_hash = transaction_context::spec_get_txn_hash(); diff --git a/aptos-move/framework/supra-framework/sources/reconfiguration.spec.move b/aptos-move/framework/supra-framework/sources/reconfiguration.spec.move index 8174f259d761d..4d190b62f95cd 100644 --- a/aptos-move/framework/supra-framework/sources/reconfiguration.spec.move +++ b/aptos-move/framework/supra-framework/sources/reconfiguration.spec.move @@ -53,7 +53,7 @@ spec supra_framework::reconfiguration { } /// Make sure the signer address is @supra_framework. - spec schema AbortsIfNotAptosFramework { + spec schema AbortsIfNotSupraFramework { supra_framework: &signer; let addr = signer::address_of(supra_framework); @@ -68,7 +68,7 @@ spec supra_framework::reconfiguration { use supra_framework::account::{Account}; use supra_framework::guid; - include AbortsIfNotAptosFramework; + include AbortsIfNotSupraFramework; let addr = signer::address_of(supra_framework); let post config = global(@supra_framework); requires exists(addr); @@ -96,7 +96,7 @@ spec supra_framework::reconfiguration { } spec disable_reconfiguration(supra_framework: &signer) { - include AbortsIfNotAptosFramework; + include AbortsIfNotSupraFramework; aborts_if exists(@supra_framework); ensures exists(@supra_framework); } @@ -104,7 +104,7 @@ spec supra_framework::reconfiguration { /// Make sure the caller is admin and check the resource DisableReconfiguration. spec enable_reconfiguration(supra_framework: &signer) { use supra_framework::reconfiguration::{DisableReconfiguration}; - include AbortsIfNotAptosFramework; + include AbortsIfNotSupraFramework; aborts_if !exists(@supra_framework); ensures !exists(@supra_framework); } @@ -113,8 +113,8 @@ spec supra_framework::reconfiguration { /// Should equal to 0 spec emit_genesis_reconfiguration_event { use supra_framework::reconfiguration::{Configuration}; - aborts_if !exists(@supra_framework); + aborts_if !exists(@supra_framework); let config_ref = global(@supra_framework); aborts_if !(config_ref.epoch == 0 && config_ref.last_reconfiguration_time == 0); ensures global(@supra_framework).epoch == 1; diff --git a/aptos-move/framework/supra-framework/sources/storage_gas.spec.move b/aptos-move/framework/supra-framework/sources/storage_gas.spec.move index 90a6681734ed5..2458ae4254ecd 100644 --- a/aptos-move/framework/supra-framework/sources/storage_gas.spec.move +++ b/aptos-move/framework/supra-framework/sources/storage_gas.spec.move @@ -120,7 +120,7 @@ spec supra_framework::storage_gas { /// Signer address must be @supra_framework and StorageGasConfig exists. spec set_config(supra_framework: &signer, config: StorageGasConfig) { - include system_addresses::AbortsIfNotAptosFramework{ account: supra_framework }; + include system_addresses::AbortsIfNotSupraFramework{ account: supra_framework }; aborts_if !exists(@supra_framework); } @@ -128,7 +128,7 @@ spec supra_framework::storage_gas { /// Address @supra_framework does not exist StorageGasConfig and StorageGas before the function call is restricted /// and exists after the function is executed. spec initialize(supra_framework: &signer) { - include system_addresses::AbortsIfNotAptosFramework{ account: supra_framework }; + include system_addresses::AbortsIfNotSupraFramework{ account: supra_framework }; pragma verify_duration_estimate = 120; aborts_if exists(@supra_framework); aborts_if exists(@supra_framework); diff --git a/aptos-move/framework/supra-framework/sources/supra_account.move b/aptos-move/framework/supra-framework/sources/supra_account.move index a5f475d4e9ab2..96a15e0b1c298 100644 --- a/aptos-move/framework/supra-framework/sources/supra_account.move +++ b/aptos-move/framework/supra-framework/sources/supra_account.move @@ -116,7 +116,7 @@ module supra_framework::supra_account { if (!account::exists_at(to)) { create_account(to); spec { - assert coin::spec_is_account_registered(to); + assume coin::spec_is_account_registered(to); assume aptos_std::type_info::type_of() == aptos_std::type_info::type_of() ==> coin::spec_is_account_registered(to); }; @@ -233,12 +233,16 @@ module supra_framework::supra_account { /// Ensure that SUPRA Primary FungibleStore exists (and create if it doesn't) inline fun ensure_primary_fungible_store_exists(owner: address): address { + // TODO(fa_migration) + /* let store_addr = primary_fungible_store_address(owner); if (fungible_asset::store_exists(store_addr)) { store_addr } else { object::object_address(&primary_fungible_store::create_primary_store(owner, object::address_to_object(@aptos_fungible_asset))) } + */ + object::object_address(&primary_fungible_store::create_primary_store(owner, object::address_to_object(@aptos_fungible_asset))) } /// Address of SUPRA Primary Fungible Store diff --git a/aptos-move/framework/supra-framework/sources/supra_account.spec.move b/aptos-move/framework/supra-framework/sources/supra_account.spec.move index 84e2e0a99823b..6b9c6b30fcf18 100644 --- a/aptos-move/framework/supra-framework/sources/supra_account.spec.move +++ b/aptos-move/framework/supra-framework/sources/supra_account.spec.move @@ -225,13 +225,14 @@ spec supra_framework::supra_account { spec deposit_coins(to: address, coins: Coin) { // TODO(fa_migration) - pragma verify = false; - include CreateAccountTransferAbortsIf; - include GuidAbortsIf; - include RegistCoinAbortsIf; + pragma verify = true; + pragma aborts_if_is_partial; + // include CreateAccountTransferAbortsIf; + // include GuidAbortsIf; + // include RegistCoinAbortsIf; let if_exist_coin = exists>(to); - aborts_if if_exist_coin && global>(to).frozen; + // aborts_if if_exist_coin && global>(to).frozen; /// [high-level-spec-6] ensures exists(to); ensures exists>(to); @@ -243,19 +244,20 @@ spec supra_framework::supra_account { spec transfer_coins(from: &signer, to: address, amount: u64) { // TODO(fa_migration) - pragma verify = false; + pragma verify = true; + pragma aborts_if_is_partial; let account_addr_source = signer::address_of(from); //The 'from' addr is implictly not equal to 'to' addr requires account_addr_source != to; - include CreateAccountTransferAbortsIf; - include WithdrawAbortsIf; - include GuidAbortsIf; - include RegistCoinAbortsIf; - include TransferEnsures; + // include CreateAccountTransferAbortsIf; + // include WithdrawAbortsIf; + // include GuidAbortsIf; + // include RegistCoinAbortsIf; + // include TransferEnsures; - aborts_if exists>(to) && global>(to).frozen; + // aborts_if exists>(to) && global>(to).frozen; ensures exists(to); ensures exists>(to); } diff --git a/aptos-move/framework/supra-framework/sources/supra_governance.spec.move b/aptos-move/framework/supra-framework/sources/supra_governance.spec.move new file mode 100644 index 0000000000000..ae28624600d76 --- /dev/null +++ b/aptos-move/framework/supra-framework/sources/supra_governance.spec.move @@ -0,0 +1,550 @@ +spec supra_framework::supra_governance { + /// + /// No.: 1 + /// Requirement: The create proposal function calls create proposal v2. + /// Criticality: Low + /// Implementation: The create_proposal function internally calls create_proposal_v2. + /// Enforcement: This is manually audited to ensure create_proposal_v2 is called in create_proposal. + /// + /// No.: 2 + /// Requirement: The Approved execution hashes resources that exist when the vote function is called. + /// Criticality: Low + /// Implementation: The Vote function acquires the Approved execution hashes resources. + /// Enforcement: Formally verified in [high-level-req-2](VoteAbortIf). + /// + /// No.: 3 + /// Requirement: The execution script hash of a successful governance proposal is added to the approved list if the + /// proposal can be resolved. + /// Criticality: Medium + /// Implementation: The add_approved_script_hash function asserts that proposal_state == PROPOSAL_STATE_SUCCEEDED. + /// Enforcement: Formally verified in [high-level-req-3](AddApprovedScriptHash). + /// + /// + spec module { + pragma verify = true; + // pragma aborts_if_is_strict; + pragma aborts_if_is_partial; + } + + spec store_signer_cap( + supra_framework: &signer, + signer_address: address, + signer_cap: SignerCapability, + ) { + aborts_if !system_addresses::is_supra_framework_address(signer::address_of(supra_framework)); + aborts_if !system_addresses::is_framework_reserved_address(signer_address); + + let signer_caps = global(@supra_framework).signer_caps; + aborts_if exists(@supra_framework) && + simple_map::spec_contains_key(signer_caps, signer_address); + ensures exists(@supra_framework); + let post post_signer_caps = global(@supra_framework).signer_caps; + ensures simple_map::spec_contains_key(post_signer_caps, signer_address); + } + + /// Signer address must be @supra_framework. + /// The signer does not allow these resources (GovernanceProposal, GovernanceConfig, GovernanceEvents, VotingRecords, ApprovedExecutionHashes) to exist. + /// The signer must have an Account. + /// Limit addition overflow. + spec initialize( + supra_framework: &signer, + voting_duration_secs: u64, + min_voting_threshold: u64, + voters: vector
, + ) { + use aptos_std::type_info::Self; + let addr = signer::address_of(supra_framework); + let register_account = global(addr); + aborts_if exists>(addr); + aborts_if min_voting_threshold <= 1; + aborts_if !(vector::length(voters) >= min_voting_threshold && min_voting_threshold > vector::length(voters) / 2); + aborts_if !exists(addr); + aborts_if register_account.guid_creation_num + 7 > MAX_U64; + aborts_if register_account.guid_creation_num + 7 >= account::MAX_GUID_CREATION_NUM; + aborts_if !type_info::spec_is_struct(); + + include InitializeAbortIf; + + ensures exists>(addr); + ensures exists(addr); + ensures exists(addr); + ensures exists(addr); + } + + spec schema InitializeAbortIf { + supra_framework: &signer; + min_voting_threshold: u128; + voters: vector
; + voting_duration_secs: u64; + + let addr = signer::address_of(supra_framework); + let account = global(addr); + aborts_if exists>(addr); + aborts_if exists(addr); + aborts_if exists(addr); + aborts_if exists(addr); + aborts_if !exists(addr); + } + + /// Signer address must be @supra_framework. + /// Address @supra_framework must exist GovernanceConfig and GovernanceEvents. + spec update_supra_governance_config( + supra_framework: &signer, + voting_duration_secs: u64, + min_voting_threshold: u64, + voters: vector
, + ) { + aborts_if min_voting_threshold <= 1; + aborts_if !(vector::length(voters) >= min_voting_threshold && min_voting_threshold > vector::length(voters) / 2); + let addr = signer::address_of(supra_framework); + let governance_config = global(@supra_framework); + + let post new_governance_config = global(@supra_framework); + aborts_if addr != @supra_framework; + aborts_if (vector::length(voters) < min_voting_threshold || min_voting_threshold < vector::length(voters) / 2); + aborts_if min_voting_threshold <= 1; + aborts_if !exists(@supra_framework); + aborts_if !exists(@supra_framework); + modifies global(addr); + + ensures new_governance_config.voting_duration_secs == voting_duration_secs; + ensures new_governance_config.min_voting_threshold == min_voting_threshold; + } + + /// Signer address must be @supra_framework. + /// Address @supra_framework must exist GovernanceConfig and GovernanceEvents. + spec toggle_features( + supra_framework: &signer, + enable: vector, + disable: vector, + ) { + use supra_framework::chain_status; + use supra_framework::coin::CoinInfo; + use supra_framework::supra_coin::SupraCoin; + use supra_framework::transaction_fee; + pragma verify = false; // TODO: set because of timeout (property proved). + let addr = signer::address_of(supra_framework); + aborts_if addr != @supra_framework; + include reconfiguration_with_dkg::FinishRequirement { + framework: supra_framework + }; + include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply; + requires chain_status::is_operating(); + requires exists>(@supra_framework); + } + + spec get_voting_duration_secs(): u64 { + include AbortsIfNotGovernanceConfig; + } + + spec get_min_voting_threshold(): u64 { + include AbortsIfNotGovernanceConfig; + } + + spec get_voters_list(): vector
{ + include AbortsIfNotGovernanceConfig; + } + + spec schema AbortsIfNotGovernanceConfig { + aborts_if !exists(@supra_framework); + } + + /// The same as spec of `create_proposal_v2()`. + spec supra_create_proposal( + proposer: &signer, + execution_hash: vector, + metadata_location: vector, + metadata_hash: vector, + ) { + use supra_framework::chain_status; + pragma verify_duration_estimate = 60; + + requires chain_status::is_operating(); + include CreateProposalAbortsIf; + } + + spec supra_create_proposal_v2( + proposer: &signer, + execution_hash: vector, + metadata_location: vector, + metadata_hash: vector, + is_multi_step_proposal: bool, + ) { + use supra_framework::chain_status; + + pragma verify_duration_estimate = 60; + requires chain_status::is_operating(); + include CreateProposalAbortsIf; + } + + spec supra_create_proposal_v2_impl ( + proposer: &signer, + execution_hash: vector, + metadata_location: vector, + metadata_hash: vector, + is_multi_step_proposal: bool, + ): u64 { + use supra_framework::chain_status; + pragma verify_duration_estimate = 60; + requires chain_status::is_operating(); + include CreateProposalAbortsIf; + } + + /// `stake_pool` must exist StakePool. + /// The delegated voter under the resource StakePool of the stake_pool must be the proposer address. + /// Address @supra_framework must exist GovernanceEvents. + spec schema CreateProposalAbortsIf { + use aptos_std::table; + proposer: &signer; + execution_hash: vector; + metadata_location: vector; + metadata_hash: vector; + + include VotingGetDelegatedVoterAbortsIf { sign: proposer }; + include AbortsIfNotGovernanceConfig; + + let governance_config = global(@supra_framework); + + aborts_if !exists(@supra_framework); + let current_time = timestamp::spec_now_seconds(); + let proposal_expiration = current_time + governance_config.voting_duration_secs; + + // verify create_proposal_metadata + include CreateProposalMetadataAbortsIf; + + // verify voting::create_proposal_v2 + aborts_if len(execution_hash) == 0; + aborts_if !exists>(@supra_framework); + let voting_forum = global>(@supra_framework); + let proposal_id = voting_forum.next_proposal_id; + aborts_if proposal_id + 1 > MAX_U64; + let post post_voting_forum = global>(@supra_framework); + let post post_next_proposal_id = post_voting_forum.next_proposal_id; + ensures post_next_proposal_id == proposal_id + 1; + aborts_if !string::spec_internal_check_utf8(multisig_voting::IS_MULTI_STEP_PROPOSAL_KEY); + aborts_if !string::spec_internal_check_utf8(multisig_voting::IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY); + aborts_if table::spec_contains(voting_forum.proposals,proposal_id); + ensures table::spec_contains(post_voting_forum.proposals, proposal_id); + aborts_if !exists(@supra_framework); + } + + spec schema VotingGetDelegatedVoterAbortsIf { + sign: signer; + + let addr = signer::address_of(sign); + } + + /// stake_pool must exist StakePool. + /// The delegated voter under the resource StakePool of the stake_pool must be the voter address. + /// Address @supra_framework must exist VotingRecords and GovernanceProposal. + spec supra_vote ( + voter: &signer, + proposal_id: u64, + should_pass: bool, + ) { + use supra_framework::chain_status; + pragma verify_duration_estimate = 60; + + requires chain_status::is_operating(); + include VoteAbortIf; + } + + spec supra_vote_internal ( + voter: &signer, + proposal_id: u64, + should_pass: bool, + ) { + use supra_framework::chain_status; + pragma verify_duration_estimate = 60; + + requires chain_status::is_operating(); + include SupraVoteAbortIf; + } + + spec schema SupraVoteAbortIf { + voter: &signer; + proposal_id: u64; + should_pass: bool; + + aborts_if spec_proposal_expiration <= timestamp::now_seconds() && !exists(@supra_framework); + let spec_proposal_expiration = multisig_voting::spec_get_proposal_expiration_secs(@supra_framework, proposal_id); + } + + spec schema VoteAbortIf { + use aptos_std::table; + + voter: &signer; + proposal_id: u64; + should_pass: bool; + + include VotingGetDelegatedVoterAbortsIf { sign: voter }; + aborts_if !exists>(@supra_framework); + let voting_forum = global>(@supra_framework); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + aborts_if !table::spec_contains(voting_forum.proposals, proposal_id); + let proposal_expiration = proposal.expiration_secs; + // verify voting::vote + aborts_if timestamp::now_seconds() > proposal_expiration; + aborts_if proposal.is_resolved; + aborts_if !string::spec_internal_check_utf8(multisig_voting::IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY); + let execution_key = utf8(multisig_voting::IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY); + aborts_if simple_map::spec_contains_key(proposal.metadata, execution_key) && + simple_map::spec_get(proposal.metadata, execution_key) != std::bcs::to_bytes(false); + let post post_voting_forum = global>(@supra_framework); + let post post_proposal = table::spec_get(post_voting_forum.proposals, proposal_id); + + aborts_if !string::spec_internal_check_utf8(multisig_voting::RESOLVABLE_TIME_METADATA_KEY); + let key = utf8(multisig_voting::RESOLVABLE_TIME_METADATA_KEY); + ensures simple_map::spec_contains_key(post_proposal.metadata, key); + ensures simple_map::spec_get(post_proposal.metadata, key) == std::bcs::to_bytes(timestamp::now_seconds()); + + aborts_if !exists(@supra_framework); + + // verify add_approved_script_hash(proposal_id) + let execution_hash = proposal.execution_hash; + let post post_approved_hashes = global(@supra_framework); + + // Due to the complexity of the success state, the validation of 'borrow_global_mut(@supra_framework);' is discussed in four cases. + /// [high-level-req-3] + // aborts_if !exists(@supra_framework); + + ensures simple_map::spec_contains_key(post_approved_hashes.hashes, proposal_id) && + simple_map::spec_get(post_approved_hashes.hashes, proposal_id) == execution_hash; + } + + spec add_supra_approved_script_hash(proposal_id: u64) { + + use supra_framework::chain_status; + pragma aborts_if_is_partial = true; + + requires chain_status::is_operating(); + include AddApprovedScriptHash; + } + + spec add_supra_approved_script_hash_script(proposal_id: u64) { + use supra_framework::chain_status; + pragma aborts_if_is_partial = true; + + requires chain_status::is_operating(); + include AddApprovedScriptHash; + } + + spec schema AddApprovedScriptHash { + use aptos_std::table; + proposal_id: u64; + aborts_if !exists(@supra_framework); + + aborts_if !exists>(@supra_framework); + let voting_forum = global>(@supra_framework); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + aborts_if !table::spec_contains(voting_forum.proposals, proposal_id); + + let post post_approved_hashes = global(@supra_framework); + /// [high-level-req-4] + ensures simple_map::spec_contains_key(post_approved_hashes.hashes, proposal_id) && + simple_map::spec_get(post_approved_hashes.hashes, proposal_id) == proposal.execution_hash; + } + + /// Address @supra_framework must exist ApprovedExecutionHashes and GovernanceProposal and GovernanceResponsbility. + spec supra_resolve(proposal_id: u64, signer_address: address): signer { + use supra_framework::chain_status; + use aptos_std::table; + use std::option; + //TODO: Remove pragma aborts_if_is_partial; + pragma aborts_if_is_partial = true; + requires chain_status::is_operating(); + // verify mutisig_voting::resolve + include VotingIsProposalResolvableAbortsif; + + let voting_forum = global>(@supra_framework); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + + let multi_step_key = utf8(multisig_voting::IS_MULTI_STEP_PROPOSAL_KEY); + let has_multi_step_key = simple_map::spec_contains_key(proposal.metadata, multi_step_key); + let is_multi_step_proposal = aptos_std::from_bcs::deserialize(simple_map::spec_get(proposal.metadata, multi_step_key)); + aborts_if has_multi_step_key && !aptos_std::from_bcs::deserializable(simple_map::spec_get(proposal.metadata, multi_step_key)); + aborts_if !string::spec_internal_check_utf8(multisig_voting::IS_MULTI_STEP_PROPOSAL_KEY); + aborts_if has_multi_step_key && is_multi_step_proposal; + + let post post_voting_forum = global>(@supra_framework); + let post post_proposal = table::spec_get(post_voting_forum.proposals, proposal_id); + ensures post_proposal.is_resolved == true && post_proposal.resolution_time_secs == timestamp::now_seconds(); + aborts_if option::spec_is_none(proposal.execution_content); + + // verify remove_approved_hash + aborts_if !exists(@supra_framework); + let post post_approved_hashes = global(@supra_framework).hashes; + ensures !simple_map::spec_contains_key(post_approved_hashes, proposal_id); + + // verify get_signer + include GetSignerAbortsIf; + let governance_responsibility = global(@supra_framework); + let signer_cap = simple_map::spec_get(governance_responsibility.signer_caps, signer_address); + let addr = signer_cap.account; + ensures signer::address_of(result) == addr; + } + + /// Address @supra_framework must exist ApprovedExecutionHashes and GovernanceProposal. + spec remove_supra_approved_hash(proposal_id: u64) { + use aptos_std::table; + pragma aborts_if_is_partial = true; + aborts_if !exists>(@supra_framework); + aborts_if !exists(@supra_framework); + let voting_forum = global>(@supra_framework); + aborts_if !table::spec_contains(voting_forum.proposals, proposal_id); + aborts_if !exists>(@supra_framework); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + aborts_if !proposal.is_resolved; + let post approved_hashes = global(@supra_framework).hashes; + ensures !simple_map::spec_contains_key(approved_hashes, proposal_id); + } + + spec reconfigure(supra_framework: &signer) { + use supra_framework::chain_status; + use supra_framework::coin::CoinInfo; + use supra_framework::supra_coin::SupraCoin; + use supra_framework::transaction_fee; + pragma verify = false; // TODO: set because of timeout (property proved). + aborts_if !system_addresses::is_supra_framework_address(signer::address_of(supra_framework)); + include reconfiguration_with_dkg::FinishRequirement { + framework: supra_framework + }; + + include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply; + requires chain_status::is_operating(); + requires exists>(@supra_framework); + } + + /// Signer address must be @core_resources. + /// signer must exist in MintCapStore. + /// Address @supra_framework must exist GovernanceResponsbility. + spec get_signer_testnet_only(core_resources: &signer, signer_address: address): signer { + aborts_if signer::address_of(core_resources) != @core_resources; + aborts_if !exists(signer::address_of(core_resources)); + include GetSignerAbortsIf; + } + + spec get_signer(signer_address: address): signer { + include GetSignerAbortsIf; + } + + spec schema GetSignerAbortsIf { + signer_address: address; + + aborts_if !exists(@supra_framework); + let cap_map = global(@supra_framework).signer_caps; + aborts_if !simple_map::spec_contains_key(cap_map, signer_address); + } + + spec create_proposal_metadata(metadata_location: vector, metadata_hash: vector): SimpleMap> { + include CreateProposalMetadataAbortsIf; + } + + spec schema CreateProposalMetadataAbortsIf { + metadata_location: vector; + metadata_hash: vector; + + aborts_if string::length(utf8(metadata_location)) > 256; + aborts_if string::length(utf8(metadata_hash)) > 256; + aborts_if !string::spec_internal_check_utf8(metadata_location); + aborts_if !string::spec_internal_check_utf8(metadata_hash); + aborts_if !string::spec_internal_check_utf8(METADATA_LOCATION_KEY); + aborts_if !string::spec_internal_check_utf8(METADATA_HASH_KEY); + } + + /// verify_only + spec initialize_for_verification( + supra_framework: &signer, + voting_duration_secs: u64, + supra_min_voting_threshold: u64, + voters: vector
, + ) { + pragma verify = false; + } + + spec resolve_supra_multi_step_proposal(proposal_id: u64, signer_address: address, next_execution_hash: vector): signer { + use supra_framework::chain_status; + use aptos_std::table; + + requires chain_status::is_operating(); + + // TODO: These function passed locally however failed in github CI + pragma verify_duration_estimate = 120; + // verify multisig_voting::resolve_proposal_v2 + include VotingIsProposalResolvableAbortsif; + + let voting_forum = global>(@supra_framework); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + let post post_voting_forum = global>(@supra_framework); + let post post_proposal = table::spec_get(post_voting_forum.proposals, proposal_id); + + aborts_if !string::spec_internal_check_utf8(multisig_voting::IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY); + let multi_step_in_execution_key = utf8(multisig_voting::IS_MULTI_STEP_PROPOSAL_IN_EXECUTION_KEY); + let post is_multi_step_proposal_in_execution_value = simple_map::spec_get(post_proposal.metadata, multi_step_in_execution_key); + + aborts_if !string::spec_internal_check_utf8(multisig_voting::IS_MULTI_STEP_PROPOSAL_KEY); + let multi_step_key = utf8(multisig_voting::IS_MULTI_STEP_PROPOSAL_KEY); + aborts_if simple_map::spec_contains_key(proposal.metadata, multi_step_key) && + !aptos_std::from_bcs::deserializable(simple_map::spec_get(proposal.metadata, multi_step_key)); + let is_multi_step = simple_map::spec_contains_key(proposal.metadata, multi_step_key) && + aptos_std::from_bcs::deserialize(simple_map::spec_get(proposal.metadata, multi_step_key)); + let next_execution_hash_is_empty = len(next_execution_hash) == 0; + aborts_if !is_multi_step && !next_execution_hash_is_empty; + aborts_if next_execution_hash_is_empty && is_multi_step && !simple_map::spec_contains_key(proposal.metadata, multi_step_in_execution_key); // ? + ensures next_execution_hash_is_empty ==> post_proposal.is_resolved == true && post_proposal.resolution_time_secs == timestamp::spec_now_seconds() && + if (is_multi_step) { + is_multi_step_proposal_in_execution_value == std::bcs::serialize(false) + } else { + simple_map::spec_contains_key(proposal.metadata, multi_step_in_execution_key) ==> + is_multi_step_proposal_in_execution_value == std::bcs::serialize(true) + }; + ensures !next_execution_hash_is_empty ==> post_proposal.execution_hash == next_execution_hash; + + // verify remove_approved_hash + aborts_if !exists(@supra_framework); + let post post_approved_hashes = global(@supra_framework).hashes; + ensures next_execution_hash_is_empty ==> !simple_map::spec_contains_key(post_approved_hashes, proposal_id); + ensures !next_execution_hash_is_empty ==> + simple_map::spec_get(post_approved_hashes, proposal_id) == next_execution_hash; + + // verify get_signer + include GetSignerAbortsIf; + let governance_responsibility = global(@supra_framework); + let signer_cap = simple_map::spec_get(governance_responsibility.signer_caps, signer_address); + let addr = signer_cap.account; + ensures signer::address_of(result) == addr; + } + + spec schema VotingIsProposalResolvableAbortsif { + use aptos_std::table; + proposal_id: u64; + + aborts_if !exists>(@supra_framework); + let voting_forum = global>(@supra_framework); + let proposal = table::spec_get(voting_forum.proposals, proposal_id); + aborts_if !table::spec_contains(voting_forum.proposals, proposal_id); + let voting_period_over = timestamp::now_seconds() > proposal.expiration_secs; + + aborts_if proposal.is_resolved; + aborts_if !string::spec_internal_check_utf8(multisig_voting::RESOLVABLE_TIME_METADATA_KEY); + aborts_if !simple_map::spec_contains_key(proposal.metadata, utf8(multisig_voting::RESOLVABLE_TIME_METADATA_KEY)); + let resolvable_time = aptos_std::from_bcs::deserialize(simple_map::spec_get(proposal.metadata, utf8(multisig_voting::RESOLVABLE_TIME_METADATA_KEY))); + aborts_if !aptos_std::from_bcs::deserializable(simple_map::spec_get(proposal.metadata, utf8(multisig_voting::RESOLVABLE_TIME_METADATA_KEY))); + aborts_if timestamp::now_seconds() <= resolvable_time; + aborts_if supra_framework::transaction_context::spec_get_script_hash() != proposal.execution_hash; + } + + spec force_end_epoch(supra_framework: &signer) { + use supra_framework::reconfiguration_with_dkg; + use std::signer; + pragma verify = false; // TODO: set because of timeout (property proved). + let address = signer::address_of(supra_framework); + include reconfiguration_with_dkg::FinishRequirement { + framework: supra_framework + }; + } + + spec force_end_epoch_test_only { + pragma verify = false; + } +} diff --git a/aptos-move/framework/supra-framework/sources/system_addresses.spec.move b/aptos-move/framework/supra-framework/sources/system_addresses.spec.move index f6c64ce9ed406..1a0000dbedf97 100644 --- a/aptos-move/framework/supra-framework/sources/system_addresses.spec.move +++ b/aptos-move/framework/supra-framework/sources/system_addresses.spec.move @@ -14,7 +14,7 @@ spec supra_framework::system_addresses { /// Criticality: High /// Implementation: The assert_supra_framework function ensures that the provided signer belongs to the /// @supra_framework account. - /// Enforcement: Formally verified via [high-level-req-2](AbortsIfNotAptosFramework). + /// Enforcement: Formally verified via [high-level-req-2](AbortsIfNotSupraFramework). /// /// No.: 3 /// Requirement: Asserting that a provided address corresponds to the VM address should always yield a true result when @@ -54,7 +54,7 @@ spec supra_framework::system_addresses { spec assert_supra_framework(account: &signer) { pragma opaque; - include AbortsIfNotAptosFramework; + include AbortsIfNotSupraFramework; } spec assert_framework_reserved_address(account: &signer) { @@ -65,7 +65,7 @@ spec supra_framework::system_addresses { aborts_if !is_framework_reserved_address(addr); } /// Specifies that a function aborts if the account does not have the aptos framework address. - spec schema AbortsIfNotAptosFramework { + spec schema AbortsIfNotSupraFramework { account: signer; /// [high-level-req-2] aborts_if signer::address_of(account) != @supra_framework with error::PERMISSION_DENIED; diff --git a/aptos-move/framework/supra-framework/sources/transaction_fee.spec.move b/aptos-move/framework/supra-framework/sources/transaction_fee.spec.move index 0464966ff45f0..39664c7974c41 100644 --- a/aptos-move/framework/supra-framework/sources/transaction_fee.spec.move +++ b/aptos-move/framework/supra-framework/sources/transaction_fee.spec.move @@ -84,7 +84,7 @@ spec supra_framework::transaction_fee { aborts_if !system_addresses::is_supra_framework_address(aptos_addr); aborts_if exists(aptos_addr); - include system_addresses::AbortsIfNotAptosFramework { account: supra_framework }; + include system_addresses::AbortsIfNotSupraFramework { account: supra_framework }; include aggregator_factory::CreateAggregatorInternalAbortsIf; aborts_if exists(aptos_addr); diff --git a/aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move b/aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move index 3dd2c83d54f8c..6ba69d207e051 100644 --- a/aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move +++ b/aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move @@ -52,16 +52,11 @@ spec supra_framework::vesting_without_staking { // include VestingContractActive{contract_address: vesting_contract_address}; // } - // spec shareholder { - // pragma verify = true; - // } - spec create_vesting_schedule { pragma verify = true; pragma aborts_if_is_partial = true; aborts_if vector::length(schedule) == 0; aborts_if period_duration <= 0; - aborts_if start_timestamp_secs < timestamp::spec_now_seconds(); } // spec create_vesting_contract { @@ -107,25 +102,33 @@ spec supra_framework::vesting_without_staking { } spec vest_transfer { + // TODO(fa_migration) pragma verify = true; let amount = min(vesting_record.left_amount, fixed_point32::spec_multiply_u64(vesting_record.init_amount, vesting_fraction)); // Ensure that the amount is substracted from the left_amount ensures vesting_record.left_amount == old(vesting_record.left_amount) - amount; let address_from = signer_cap.account; + let coin_store_from = global>(address_from); + let post coin_store_post_from = global>(address_from); + let coin_store_to = global>(beneficiary); + let post coin_store_post_to = global>(beneficiary); // Ensure that the amount is transferred from the address_from to the beneficiary - ensures beneficiary != address_from ==> - (coin::balance(beneficiary) == old(coin::balance(beneficiary)) + amount - && coin::balance(address_from) == old(coin::balance(address_from)) - amount); + ensures beneficiary != address_from ==> coin_store_post_from.coin.value == + coin_store_from.coin.value - amount; + ensures beneficiary != address_from ==> coin_store_post_to.coin.value == coin_store_to.coin.value + amount; + ensures beneficiary == address_from ==> coin_store_post_from.coin.value == coin_store_from.coin.value; } spec remove_shareholder { + // TODO(fa_migration) pragma verify = true; pragma aborts_if_is_partial = true; include AdminAborts; let vesting_contract = global(contract_address); let post vesting_contract_post = global(contract_address); - let balance_pre = coin::balance(vesting_contract.withdrawal_address); - let post balance_post = coin::balance(vesting_contract_post.withdrawal_address); + + let balance_pre = global>(vesting_contract.withdrawal_address).coin.value; + let post balance_post = global>(vesting_contract.withdrawal_address).coin.value; let shareholder_amount = simple_map::spec_get(vesting_contract.shareholders, shareholder_address).left_amount; // ensure that `withdrawal address` receives the `shareholder_amount` ensures vesting_contract_post.withdrawal_address != vesting_contract.signer_cap.account ==> balance_post == balance_pre + shareholder_amount; @@ -145,9 +148,10 @@ spec supra_framework::vesting_without_staking { pragma verify = true; pragma aborts_if_is_partial = true; let vesting_contract = global(contract_address); - let balance_pre = coin::balance(vesting_contract.withdrawal_address); - let post balance_post = coin::balance(vesting_contract.withdrawal_address); - let post balance_contract = coin::balance(contract_address); + let balance_pre = global>(vesting_contract.withdrawal_address).coin.value; + let post balance_post = global>(vesting_contract.withdrawal_address).coin.value; + let post balance_contract = global>(contract_address).coin.value; + aborts_if !(global(contract_address).state == VESTING_POOL_TERMINATED); // // ensure that the `withdrawal_address` receives the remaining balance // ensures (vesting_contract.signer_cap.account != vesting_contract.withdrawal_address) ==> balance_post == balance_pre + coin::balance(contract_address);