diff --git a/aptos-move/framework/aptos-framework/doc/account.md b/aptos-move/framework/aptos-framework/doc/account.md
index 516ad6d386558..5a74228946a5b 100644
--- a/aptos-move/framework/aptos-framework/doc/account.md
+++ b/aptos-move/framework/aptos-framework/doc/account.md
@@ -63,6 +63,8 @@
- [Function `revoke_rotation_capability`](#@Specification_1_revoke_rotation_capability)
- [Function `revoke_any_rotation_capability`](#@Specification_1_revoke_any_rotation_capability)
- [Function `offer_signer_capability`](#@Specification_1_offer_signer_capability)
+ - [Function `is_signer_capability_offered`](#@Specification_1_is_signer_capability_offered)
+ - [Function `get_signer_capability_offer_for`](#@Specification_1_get_signer_capability_offer_for)
- [Function `revoke_signer_capability`](#@Specification_1_revoke_signer_capability)
- [Function `revoke_any_signer_capability`](#@Specification_1_revoke_any_signer_capability)
- [Function `create_authorized_signer`](#@Specification_1_create_authorized_signer)
@@ -2308,6 +2310,40 @@ The authentication scheme is ED25519_SCHEME and MULTI_ED25519_SCHEME.
+
+
+### Function `is_signer_capability_offered`
+
+
+public fun is_signer_capability_offered(account_addr: address): bool
+
+
+
+
+
+aborts_if !exists<Account>(account_addr);
+
+
+
+
+
+
+### Function `get_signer_capability_offer_for`
+
+
+public fun get_signer_capability_offer_for(account_addr: address): address
+
+
+
+
+
+aborts_if !exists<Account>(account_addr);
+let account_resource = global<Account>(account_addr);
+aborts_if len(account_resource.signer_capability_offer.for.vec) == 0;
+
+
+
+
### Function `revoke_signer_capability`
diff --git a/aptos-move/framework/aptos-framework/doc/code.md b/aptos-move/framework/aptos-framework/doc/code.md
index d274d1c5a974a..63a51bd7a63f4 100644
--- a/aptos-move/framework/aptos-framework/doc/code.md
+++ b/aptos-move/framework/aptos-framework/doc/code.md
@@ -28,6 +28,12 @@ This module supports functionality related to code management.
- [Function `request_publish`](#0x1_code_request_publish)
- [Function `request_publish_with_allowed_deps`](#0x1_code_request_publish_with_allowed_deps)
- [Specification](#@Specification_1)
+ - [Function `initialize`](#@Specification_1_initialize)
+ - [Function `publish_package`](#@Specification_1_publish_package)
+ - [Function `publish_package_txn`](#@Specification_1_publish_package_txn)
+ - [Function `check_upgradability`](#@Specification_1_check_upgradability)
+ - [Function `check_coexistence`](#@Specification_1_check_coexistence)
+ - [Function `check_dependencies`](#@Specification_1_check_dependencies)
- [Function `request_publish`](#@Specification_1_request_publish)
- [Function `request_publish_with_allowed_deps`](#@Specification_1_request_publish_with_allowed_deps)
@@ -888,6 +894,106 @@ Native function to initiate module loading, including a list of allowed dependen
+pragma verify = true;
+pragma aborts_if_is_strict;
+
+
+
+
+
+
+### Function `initialize`
+
+
+fun initialize(aptos_framework: &signer, package_owner: &signer, metadata: code::PackageMetadata)
+
+
+
+
+
+let aptos_addr = signer::address_of(aptos_framework);
+let owner_addr = signer::address_of(package_owner);
+aborts_if !system_addresses::is_aptos_framework_address(aptos_addr);
+ensures exists<PackageRegistry>(owner_addr);
+
+
+
+
+
+
+### Function `publish_package`
+
+
+public fun publish_package(owner: &signer, pack: code::PackageMetadata, code: vector<vector<u8>>)
+
+
+
+
+
+pragma verify = false;
+
+
+
+
+
+
+### Function `publish_package_txn`
+
+
+public entry fun publish_package_txn(owner: &signer, metadata_serialized: vector<u8>, code: vector<vector<u8>>)
+
+
+
+
+
+pragma verify = false;
+
+
+
+
+
+
+### Function `check_upgradability`
+
+
+fun check_upgradability(old_pack: &code::PackageMetadata, new_pack: &code::PackageMetadata, new_modules: &vector<string::String>)
+
+
+
+
+
+pragma verify = false;
+
+
+
+
+
+
+### Function `check_coexistence`
+
+
+fun check_coexistence(old_pack: &code::PackageMetadata, new_modules: &vector<string::String>)
+
+
+
+
+
+pragma verify = false;
+
+
+
+
+
+
+### Function `check_dependencies`
+
+
+fun check_dependencies(publish_address: address, pack: &code::PackageMetadata): vector<code::AllowedDep>
+
+
+
+
+
pragma verify = false;
diff --git a/aptos-move/framework/aptos-framework/doc/resource_account.md b/aptos-move/framework/aptos-framework/doc/resource_account.md
index f75f7c856ed73..cc79514ad8b79 100644
--- a/aptos-move/framework/aptos-framework/doc/resource_account.md
+++ b/aptos-move/framework/aptos-framework/doc/resource_account.md
@@ -82,6 +82,12 @@ module.resource_signer_cap = option::some(resource_signer_cap);
- [Function `create_resource_account_and_publish_package`](#0x1_resource_account_create_resource_account_and_publish_package)
- [Function `rotate_account_authentication_key_and_store_capability`](#0x1_resource_account_rotate_account_authentication_key_and_store_capability)
- [Function `retrieve_resource_account_cap`](#0x1_resource_account_retrieve_resource_account_cap)
+- [Specification](#@Specification_3)
+ - [Function `create_resource_account`](#@Specification_3_create_resource_account)
+ - [Function `create_resource_account_and_fund`](#@Specification_3_create_resource_account_and_fund)
+ - [Function `create_resource_account_and_publish_package`](#@Specification_3_create_resource_account_and_publish_package)
+ - [Function `rotate_account_authentication_key_and_store_capability`](#@Specification_3_rotate_account_authentication_key_and_store_capability)
+ - [Function `retrieve_resource_account_cap`](#@Specification_3_retrieve_resource_account_cap)
use 0x1::account;
@@ -364,5 +370,120 @@ the SignerCapability.
+
+
+## Specification
+
+
+
+pragma verify = true;
+pragma aborts_if_is_strict;
+
+
+
+
+
+
+### Function `create_resource_account`
+
+
+public entry fun create_resource_account(origin: &signer, seed: vector<u8>, optional_auth_key: vector<u8>)
+
+
+
+
+
+pragma verify = false;
+
+
+
+
+
+
+### Function `create_resource_account_and_fund`
+
+
+public entry fun create_resource_account_and_fund(origin: &signer, seed: vector<u8>, optional_auth_key: vector<u8>, fund_amount: u64)
+
+
+
+
+
+pragma verify = false;
+
+
+
+
+
+
+### Function `create_resource_account_and_publish_package`
+
+
+public entry fun create_resource_account_and_publish_package(origin: &signer, seed: vector<u8>, metadata_serialized: vector<u8>, code: vector<vector<u8>>)
+
+
+
+
+
+pragma verify = false;
+
+
+
+
+
+
+### Function `rotate_account_authentication_key_and_store_capability`
+
+
+fun rotate_account_authentication_key_and_store_capability(origin: &signer, resource: signer, resource_signer_cap: account::SignerCapability, optional_auth_key: vector<u8>)
+
+
+
+
+
+let resource_addr = signer::address_of(resource);
+include RotateAccountAuthenticationKeyAndStoreCapabilityAbortsIf;
+
+
+
+
+
+
+
+
+schema RotateAccountAuthenticationKeyAndStoreCapabilityAbortsIf {
+ origin: signer;
+ resource_addr: address;
+ optional_auth_key: vector<u8>;
+ let origin_addr = signer::address_of(origin);
+ let container = global<Container>(origin_addr);
+ let get = len(optional_auth_key) == 0;
+ aborts_if get && !exists<Account>(origin_addr);
+ aborts_if exists<Container>(origin_addr) && simple_map::spec_contains_key(container.store, resource_addr);
+ aborts_if get && !(exists<Account>(resource_addr) && len(global<Account>(origin_addr).authentication_key) == 32);
+ aborts_if !get && !(exists<Account>(resource_addr) && len(optional_auth_key) == 32);
+}
+
+
+
+
+
+
+### Function `retrieve_resource_account_cap`
+
+
+public fun retrieve_resource_account_cap(resource: &signer, source_addr: address): account::SignerCapability
+
+
+
+
+
+aborts_if !exists<Container>(source_addr);
+let resource_addr = signer::address_of(resource);
+let container = borrow_global_mut<Container>(source_addr);
+aborts_if !simple_map::spec_contains_key(container.store, resource_addr);
+aborts_if !exists<account::Account>(resource_addr);
+
+
[move-book]: https://move-language.github.io/move/introduction.html
diff --git a/aptos-move/framework/aptos-framework/doc/staking_contract.md b/aptos-move/framework/aptos-framework/doc/staking_contract.md
index 51c8b55673706..3f6fe9321d326 100644
--- a/aptos-move/framework/aptos-framework/doc/staking_contract.md
+++ b/aptos-move/framework/aptos-framework/doc/staking_contract.md
@@ -84,6 +84,7 @@ pool.
- [Function `add_stake`](#@Specification_1_add_stake)
- [Function `update_voter`](#@Specification_1_update_voter)
- [Function `reset_lockup`](#@Specification_1_reset_lockup)
+ - [Function `update_commision`](#@Specification_1_update_commision)
- [Function `request_commission`](#@Specification_1_request_commission)
- [Function `request_commission_internal`](#@Specification_1_request_commission_internal)
- [Function `unlock_stake`](#@Specification_1_unlock_stake)
@@ -2155,6 +2156,22 @@ Only active validator can update locked_until_secs.
+
+
+### Function `update_commision`
+
+
+public entry fun update_commision(staker: &signer, operator: address, new_commission_percentage: u64)
+
+
+
+
+
+pragma verify = false;
+
+
+
+
### Function `request_commission`
diff --git a/aptos-move/framework/aptos-framework/doc/staking_proxy.md b/aptos-move/framework/aptos-framework/doc/staking_proxy.md
index d49edc1e3f8cf..78894f68acf11 100644
--- a/aptos-move/framework/aptos-framework/doc/staking_proxy.md
+++ b/aptos-move/framework/aptos-framework/doc/staking_proxy.md
@@ -14,6 +14,14 @@
- [Function `set_staking_contract_voter`](#0x1_staking_proxy_set_staking_contract_voter)
- [Function `set_stake_pool_voter`](#0x1_staking_proxy_set_stake_pool_voter)
- [Specification](#@Specification_0)
+ - [Function `set_operator`](#@Specification_0_set_operator)
+ - [Function `set_voter`](#@Specification_0_set_voter)
+ - [Function `set_vesting_contract_operator`](#@Specification_0_set_vesting_contract_operator)
+ - [Function `set_staking_contract_operator`](#@Specification_0_set_staking_contract_operator)
+ - [Function `set_stake_pool_operator`](#@Specification_0_set_stake_pool_operator)
+ - [Function `set_vesting_contract_voter`](#@Specification_0_set_vesting_contract_voter)
+ - [Function `set_staking_contract_voter`](#@Specification_0_set_staking_contract_voter)
+ - [Function `set_stake_pool_voter`](#@Specification_0_set_stake_pool_voter)
use 0x1::signer;
@@ -259,7 +267,202 @@
-pragma verify = false;
+pragma verify = true;
+pragma aborts_if_is_strict;
+
+
+
+
+
+
+### Function `set_operator`
+
+
+public entry fun set_operator(owner: &signer, old_operator: address, new_operator: address)
+
+
+
+Aborts if conditions of SetStakePoolOperator are not met
+
+
+pragma aborts_if_is_partial;
+include SetStakePoolOperator;
+
+
+
+
+
+
+### Function `set_voter`
+
+
+public entry fun set_voter(owner: &signer, operator: address, new_voter: address)
+
+
+
+Aborts if conditions of SetStackingContractVoter and SetStackPoolVoterAbortsIf are not met
+
+
+pragma aborts_if_is_partial;
+include SetStakingContractVoter;
+include SetStakePoolVoterAbortsIf;
+
+
+
+
+
+
+### Function `set_vesting_contract_operator`
+
+
+public entry fun set_vesting_contract_operator(owner: &signer, old_operator: address, new_operator: address)
+
+
+
+
+
+pragma aborts_if_is_partial;
+
+
+
+
+
+
+### Function `set_staking_contract_operator`
+
+
+public entry fun set_staking_contract_operator(owner: &signer, old_operator: address, new_operator: address)
+
+
+
+
+
+pragma aborts_if_is_partial;
+let owner_address = signer::address_of(owner);
+let store = borrow_global<Store>(owner_address);
+let staking_contract_exists = exists<Store>(owner_address) && simple_map::spec_contains_key(store.staking_contracts, old_operator);
+
+
+
+
+
+
+### Function `set_stake_pool_operator`
+
+
+public entry fun set_stake_pool_operator(owner: &signer, new_operator: address)
+
+
+
+Aborts if stake_pool is exists and when OwnerCapability or stake_pool_exists
+One of them are not exists
+
+
+include SetStakePoolOperator;
+
+
+
+
+
+
+
+
+schema SetStakePoolOperator {
+ owner: &signer;
+ new_operator: address;
+ let owner_address = signer::address_of(owner);
+ let ownership_cap = borrow_global<stake::OwnerCapability>(owner_address);
+ let pool_address = ownership_cap.pool_address;
+ aborts_if stake::stake_pool_exists(owner_address) && !(exists<stake::OwnerCapability>(owner_address) && stake::stake_pool_exists(pool_address));
+}
+
+
+
+
+
+
+### Function `set_vesting_contract_voter`
+
+
+public entry fun set_vesting_contract_voter(owner: &signer, operator: address, new_voter: address)
+
+
+
+
+
+pragma aborts_if_is_partial;
+
+
+
+
+
+
+### Function `set_staking_contract_voter`
+
+
+public entry fun set_staking_contract_voter(owner: &signer, operator: address, new_voter: address)
+
+
+
+
+
+include SetStakingContractVoter;
+
+
+
+Make sure staking_contract_exists first
+Then abort if the resource is not exist
+
+
+
+
+
+schema SetStakingContractVoter {
+ owner: &signer;
+ operator: address;
+ new_voter: address;
+ let owner_address = signer::address_of(owner);
+ let staker = owner_address;
+ let store = global<Store>(staker);
+ let staking_contract_exists = exists<Store>(staker) && simple_map::spec_contains_key(store.staking_contracts, operator);
+ let staker_address = owner_address;
+ let staking_contract = simple_map::spec_get(store.staking_contracts, operator);
+ let pool_address = staking_contract.pool_address;
+ aborts_if staking_contract_exists && !exists<stake::StakePool>(pool_address);
+ aborts_if staking_contract_exists && !exists<stake::StakePool>(staking_contract.owner_cap.pool_address);
+}
+
+
+
+
+
+
+### Function `set_stake_pool_voter`
+
+
+public entry fun set_stake_pool_voter(owner: &signer, new_voter: address)
+
+
+
+
+
+include SetStakePoolVoterAbortsIf;
+
+
+
+
+
+
+
+
+schema SetStakePoolVoterAbortsIf {
+ owner: &signer;
+ new_voter: address;
+ let owner_address = signer::address_of(owner);
+ let ownership_cap = global<stake::OwnerCapability>(owner_address);
+ let pool_address = ownership_cap.pool_address;
+ aborts_if stake::stake_pool_exists(owner_address) && !(exists<stake::OwnerCapability>(owner_address) && stake::stake_pool_exists(pool_address));
+}
diff --git a/aptos-move/framework/aptos-framework/sources/account.spec.move b/aptos-move/framework/aptos-framework/sources/account.spec.move
index 74c01087871a9..23c5a233a9885 100644
--- a/aptos-move/framework/aptos-framework/sources/account.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/account.spec.move
@@ -254,6 +254,16 @@ spec aptos_framework::account {
modifies global(source_address);
}
+ spec is_signer_capability_offered(account_addr: address): bool {
+ aborts_if !exists(account_addr);
+ }
+
+ spec get_signer_capability_offer_for(account_addr: address): address {
+ aborts_if !exists(account_addr);
+ let account_resource = global(account_addr);
+ aborts_if len(account_resource.signer_capability_offer.for.vec) == 0;
+ }
+
/// The Account existed under the signer.
/// The value of signer_capability_offer.for of Account resource under the signer is to_be_revoked_address.
spec revoke_signer_capability(account: &signer, to_be_revoked_address: address) {
diff --git a/aptos-move/framework/aptos-framework/sources/code.spec.move b/aptos-move/framework/aptos-framework/sources/code.spec.move
index 27b30f0311253..a71136e7ff335 100644
--- a/aptos-move/framework/aptos-framework/sources/code.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/code.spec.move
@@ -1,6 +1,7 @@
spec aptos_framework::code {
spec module {
- pragma verify = false;
+ pragma verify = true;
+ pragma aborts_if_is_strict;
}
spec request_publish {
@@ -12,4 +13,37 @@ spec aptos_framework::code {
// TODO: temporary mockup.
pragma opaque;
}
+
+ spec initialize(aptos_framework: &signer, package_owner: &signer, metadata: PackageMetadata) {
+ let aptos_addr = signer::address_of(aptos_framework);
+ let owner_addr = signer::address_of(package_owner);
+ aborts_if !system_addresses::is_aptos_framework_address(aptos_addr);
+
+ ensures exists(owner_addr);
+ }
+
+ spec publish_package(owner: &signer, pack: PackageMetadata, code: vector>) {
+ // TODO: Can't verify `check_upgradability` in while loop.
+ pragma verify = false;
+ }
+
+ spec publish_package_txn {
+ // TODO: Calls `publish_package`.`
+ pragma verify = false;
+ }
+
+ spec check_upgradability(old_pack: &PackageMetadata, new_pack: &PackageMetadata, new_modules: &vector) {
+ // TODO: loop too deep.
+ pragma verify = false;
+ }
+
+ spec check_dependencies(publish_address: address, pack: &PackageMetadata): vector {
+ // TODO: loop too deep.
+ pragma verify = false;
+ }
+
+ spec check_coexistence(old_pack: &PackageMetadata, new_modules: &vector) {
+ // TODO: loop too deep.
+ pragma verify = false;
+ }
}
diff --git a/aptos-move/framework/aptos-framework/sources/resource_account.spec.move b/aptos-move/framework/aptos-framework/sources/resource_account.spec.move
new file mode 100644
index 0000000000000..6d3edd0ca55de
--- /dev/null
+++ b/aptos-move/framework/aptos-framework/sources/resource_account.spec.move
@@ -0,0 +1,73 @@
+spec aptos_framework::resource_account {
+ spec module {
+ pragma verify = true;
+ pragma aborts_if_is_strict;
+ }
+
+ spec create_resource_account(
+ origin: &signer,
+ seed: vector,
+ optional_auth_key: vector,
+ ) {
+ // TODO: Could not verify `rotate_account_authentication_key_and_store_capability` because can't get `resource` and `resource_signer_cap`.
+ pragma verify = false;
+ }
+
+ spec create_resource_account_and_fund(
+ origin: &signer,
+ seed: vector,
+ optional_auth_key: vector,
+ fund_amount: u64,
+ ) {
+ // TODO: Could not verify `rotate_account_authentication_key_and_store_capability` because can't get `resource` and `resource_signer_cap`.
+ pragma verify = false;
+ }
+
+ spec create_resource_account_and_publish_package(
+ origin: &signer,
+ seed: vector,
+ metadata_serialized: vector,
+ code: vector>,
+ ) {
+ // TODO: Calls `code::publish_package_txn`.
+ pragma verify = false;
+ }
+
+ spec rotate_account_authentication_key_and_store_capability(
+ origin: &signer,
+ resource: signer,
+ resource_signer_cap: account::SignerCapability,
+ optional_auth_key: vector,
+ ) {
+ let resource_addr = signer::address_of(resource);
+ include RotateAccountAuthenticationKeyAndStoreCapabilityAbortsIf;
+ }
+
+ spec schema RotateAccountAuthenticationKeyAndStoreCapabilityAbortsIf {
+ use aptos_framework::account::{Account};
+ origin: signer;
+ resource_addr: address;
+ optional_auth_key: vector;
+
+ let origin_addr = signer::address_of(origin);
+ let container = global(origin_addr);
+ let get = len(optional_auth_key) == 0;
+
+ aborts_if get && !exists(origin_addr);
+ aborts_if exists(origin_addr) && simple_map::spec_contains_key(container.store, resource_addr);
+ aborts_if get && !(exists(resource_addr) && len(global(origin_addr).authentication_key) == 32);
+ aborts_if !get && !(exists(resource_addr) && len(optional_auth_key) == 32);
+ }
+
+ spec retrieve_resource_account_cap(
+ resource: &signer,
+ source_addr: address,
+ ) : account::SignerCapability {
+ aborts_if !exists(source_addr);
+ let resource_addr = signer::address_of(resource);
+
+ let container = borrow_global_mut(source_addr);
+ aborts_if !simple_map::spec_contains_key(container.store, resource_addr);
+ aborts_if !exists(resource_addr);
+ }
+}
diff --git a/aptos-move/framework/aptos-framework/sources/staking_contract.spec.move b/aptos-move/framework/aptos-framework/sources/staking_contract.spec.move
index a90d1713aef66..ab6bd9e2e8731 100644
--- a/aptos-move/framework/aptos-framework/sources/staking_contract.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/staking_contract.spec.move
@@ -108,6 +108,11 @@ spec aptos_framework::staking_contract {
include IncreaseLockupWithCapAbortsIf{staker: staker_address};
}
+ spec update_commision (staker: &signer, operator: address, new_commission_percentage: u64) {
+ // TODO: Call `distribute_internal`
+ pragma verify = false;
+ }
+
/// Only staker or operator can call this.
spec request_commission(account: &signer, staker: address, operator: address) {
// TODO: Call `update_distribution_pool`
diff --git a/aptos-move/framework/aptos-framework/sources/staking_proxy.spec.move b/aptos-move/framework/aptos-framework/sources/staking_proxy.spec.move
index 4c14199c7b710..e30f467be967b 100644
--- a/aptos-move/framework/aptos-framework/sources/staking_proxy.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/staking_proxy.spec.move
@@ -1,5 +1,104 @@
spec aptos_framework::staking_proxy {
spec module {
- pragma verify = false;
+ pragma verify = true;
+ pragma aborts_if_is_strict;
+ }
+
+ /// Aborts if conditions of SetStakePoolOperator are not met
+ spec set_operator(owner: &signer, old_operator: address, new_operator: address) {
+ // TODO: set_vesting_contract_operator and set_staking_contract_operator too complicated.
+ pragma aborts_if_is_partial;
+ include SetStakePoolOperator;
+ }
+
+ /// Aborts if conditions of SetStackingContractVoter and SetStackPoolVoterAbortsIf are not met
+ spec set_voter(owner: &signer, operator: address, new_voter: address) {
+ // TODO: set_vesting_contract_voter too complicated.
+ pragma aborts_if_is_partial;
+ include SetStakingContractVoter;
+ include SetStakePoolVoterAbortsIf;
+ }
+
+ spec set_vesting_contract_operator(owner: &signer, old_operator: address, new_operator: address) {
+ // TODO: can't verify update_voter in while loop.
+ pragma aborts_if_is_partial;
+ }
+
+ spec set_staking_contract_operator(owner: &signer, old_operator: address, new_operator: address) {
+ use aptos_framework::staking_contract::{Store};
+ use aptos_framework::simple_map;
+ // TODO: Timeout & staking_contract::switch_operator.
+ pragma aborts_if_is_partial;
+
+ let owner_address = signer::address_of(owner);
+ let store = borrow_global(owner_address);
+ let staking_contract_exists = exists(owner_address) && simple_map::spec_contains_key(store.staking_contracts, old_operator);
+ }
+
+ spec set_vesting_contract_voter(owner: &signer, operator: address, new_voter: address) {
+ // TODO: The update_voter function logic is too complicated in the while loop
+ pragma aborts_if_is_partial;
+ }
+
+ /// Aborts if stake_pool is exists and when OwnerCapability or stake_pool_exists
+ /// One of them are not exists
+ spec set_stake_pool_operator(owner: &signer, new_operator: address) {
+ include SetStakePoolOperator;
+ }
+
+ spec schema SetStakePoolOperator {
+ owner: &signer;
+ new_operator: address;
+
+ let owner_address = signer::address_of(owner);
+ let ownership_cap = borrow_global(owner_address);
+ let pool_address = ownership_cap.pool_address;
+ aborts_if stake::stake_pool_exists(owner_address) && !(exists(owner_address) && stake::stake_pool_exists(pool_address));
+ }
+
+ spec set_staking_contract_voter(owner: &signer, operator: address, new_voter: address) {
+ include SetStakingContractVoter;
+ }
+
+ /// Make sure staking_contract_exists first
+ /// Then abort if the resource is not exist
+ spec schema SetStakingContractVoter {
+ use aptos_std::simple_map;
+ use aptos_framework::staking_contract::{Store};
+
+ owner: &signer;
+ operator: address;
+ new_voter: address;
+
+
+ let owner_address = signer::address_of(owner);
+ let staker = owner_address;
+ let store = global(staker);
+
+ // in staking_contract_exists
+ let staking_contract_exists = exists(staker) && simple_map::spec_contains_key(store.staking_contracts, operator);
+
+ // in update_voter
+ let staker_address = owner_address;
+ let staking_contract = simple_map::spec_get(store.staking_contracts, operator);
+ let pool_address = staking_contract.pool_address;
+
+ aborts_if staking_contract_exists && !exists(pool_address);
+ aborts_if staking_contract_exists && !exists(staking_contract.owner_cap.pool_address);
+
+ }
+
+ spec set_stake_pool_voter(owner: &signer, new_voter: address) {
+ include SetStakePoolVoterAbortsIf;
+ }
+
+ spec schema SetStakePoolVoterAbortsIf {
+ owner: &signer;
+ new_voter: address;
+
+ let owner_address = signer::address_of(owner);
+ let ownership_cap = global(owner_address);
+ let pool_address = ownership_cap.pool_address;
+ aborts_if stake::stake_pool_exists(owner_address) && !(exists(owner_address) && stake::stake_pool_exists(pool_address));
}
}