diff --git a/aptos-move/framework/aptos-framework/doc/aptos_governance.md b/aptos-move/framework/aptos-framework/doc/aptos_governance.md index 771a016546d69d..5e18eb9e03a7d6 100644 --- a/aptos-move/framework/aptos-framework/doc/aptos_governance.md +++ b/aptos-move/framework/aptos-framework/doc/aptos_governance.md @@ -61,7 +61,6 @@ on a proposal multiple times as long as the total voting power of these votes do - [Function `get_signer`](#0x1_aptos_governance_get_signer) - [Function `create_proposal_metadata`](#0x1_aptos_governance_create_proposal_metadata) - [Function `assert_voting_initialization`](#0x1_aptos_governance_assert_voting_initialization) -- [Function `initialize_for_verification`](#0x1_aptos_governance_initialize_for_verification) - [Specification](#@Specification_1) - [High-level Requirements](#high-level-req) - [Module-level Specification](#module-level-spec) @@ -96,7 +95,6 @@ on a proposal multiple times as long as the total voting power of these votes do - [Function `get_signer`](#@Specification_1_get_signer) - [Function `create_proposal_metadata`](#@Specification_1_create_proposal_metadata) - [Function `assert_voting_initialization`](#@Specification_1_assert_voting_initialization) - - [Function `initialize_for_verification`](#@Specification_1_initialize_for_verification) 
use 0x1::account;
@@ -1891,7 +1889,7 @@ Only called in testnet where the core resources account exists and has been gran
 
public fun get_signer_testnet_only(
     core_resources: &signer, signer_address: address): signer acquires GovernanceResponsbility {
     system_addresses::assert_core_resource(core_resources);
-    // Core resources account only has mint capability in tests/testnets.
+    // Core resources account only has mint capability in tests/testnets.
     assert!(aptos_coin::has_mint_capability(core_resources), error::unauthenticated(EUNAUTHORIZED));
     get_signer(signer_address)
 }
@@ -2020,36 +2018,6 @@ Return a signer for making changes to 0x1 as part of on-chain governance proposa
 
 
 
-
-
-
-
-## Function `initialize_for_verification`
-
-
-
-
#[verify_only]
-public fun initialize_for_verification(aptos_framework: &signer, min_voting_threshold: u128, required_proposer_stake: u64, voting_duration_secs: u64)
-

-
-
-
-

-Implementation
-
-
-
public fun initialize_for_verification(
-    aptos_framework: &signer,
-    min_voting_threshold: u128,
-    required_proposer_stake: u64,
-    voting_duration_secs: u64,
-) {
-    initialize(aptos_framework, min_voting_threshold, required_proposer_stake, voting_duration_secs);
-}
-

-
-
-
 

 
 
@@ -2156,6 +2124,7 @@ Limit addition overflow.
 
 
let addr = signer::address_of(aptos_framework);
 let register_account = global<account::Account>(addr);
+aborts_if permissioned_signer::spec_is_permissioned_signer(aptos_framework);
 aborts_if exists<voting::VotingForum<GovernanceProposal>>(addr);
 aborts_if !exists<account::Account>(addr);
 aborts_if register_account.guid_creation_num + 7 > MAX_U64;
@@ -3243,22 +3212,4 @@ pool_address must exist in StakePool.
 

 
 
-
-
-
-### Function `initialize_for_verification`
-
-
-
#[verify_only]
-public fun initialize_for_verification(aptos_framework: &signer, min_voting_threshold: u128, required_proposer_stake: u64, voting_duration_secs: u64)
-

-
-
-verify_only
-
-
-
pragma verify = false;
-

-
-
 [move-book]: https://aptos.dev/move/book/SUMMARY
diff --git a/aptos-move/framework/aptos-framework/doc/delegation_pool.md b/aptos-move/framework/aptos-framework/doc/delegation_pool.md
index 5f2efd48ccfec0..cdf828cc911135 100644
--- a/aptos-move/framework/aptos-framework/doc/delegation_pool.md
+++ b/aptos-move/framework/aptos-framework/doc/delegation_pool.md
@@ -2989,7 +2989,7 @@ The existing voter will be replaced. The function is permissionless.
 
     let delegation_pool = borrow_global<DelegationPool>(pool_address);
     let stake_pool_signer = retrieve_stake_pool_owner(delegation_pool);
-    // delegated_voter is managed by the stake pool itself, which signer capability is managed by DelegationPool.
+    // delegated_voter is managed by the stake pool itself, which signer capability is managed by DelegationPool.
     // So voting power of this stake pool can only be used through this module.
     stake::set_delegated_voter(&stake_pool_signer, signer::address_of(&stake_pool_signer));
 
diff --git a/aptos-move/framework/aptos-framework/doc/stake.md b/aptos-move/framework/aptos-framework/doc/stake.md
index d6939454878fe1..1cccd19b59539d 100644
--- a/aptos-move/framework/aptos-framework/doc/stake.md
+++ b/aptos-move/framework/aptos-framework/doc/stake.md
@@ -64,13 +64,8 @@ or if their stake drops below the min required, they would get removed at the en
 -  [Resource `Ghost$ghost_active_num`](#0x1_stake_Ghost$ghost_active_num)
 -  [Resource `Ghost$ghost_pending_inactive_num`](#0x1_stake_Ghost$ghost_pending_inactive_num)
 -  [Constants](#@Constants_0)
-<<<<<<< HEAD
-=======
--  [Function `initialize_validator_fees`](#0x1_stake_initialize_validator_fees)
--  [Function `add_transaction_fee`](#0x1_stake_add_transaction_fee)
 -  [Function `check_signer_permission`](#0x1_stake_check_signer_permission)
 -  [Function `grant_permission`](#0x1_stake_grant_permission)
->>>>>>> ad2ce2aa1c (framework permissions)
 -  [Function `get_lockup_secs`](#0x1_stake_get_lockup_secs)
 -  [Function `get_remaining_lockup_secs`](#0x1_stake_get_remaining_lockup_secs)
 -  [Function `get_stake`](#0x1_stake_get_stake)
@@ -1924,70 +1919,6 @@ Validator status enum. We can switch to proper enum later once Move supports it.
 
 
 
-<<<<<<< HEAD
-=======
-
-
-## Function `initialize_validator_fees`
-
-Initializes the resource storing information about collected transaction fees per validator.
-Used by transaction_fee.move to initialize fee collection and distribution.
-
-
-
public(friend) fun initialize_validator_fees(aptos_framework: &signer)
-

-
-
-
-

-Implementation
-
-
-
public(friend) fun initialize_validator_fees(aptos_framework: &signer) {
-    system_addresses::assert_aptos_framework(aptos_framework);
-    assert!(
-        !exists<ValidatorFees>(@aptos_framework),
-        error::already_exists(EFEES_TABLE_ALREADY_EXISTS)
-    );
-    move_to(aptos_framework, ValidatorFees { fees_table: table::new() });
-}
-

-
-
-
-

-
-
-
-## Function `add_transaction_fee`
-
-Stores the transaction fee collected to the specified validator address.
-
-
-
public(friend) fun add_transaction_fee(validator_addr: address, fee: coin::Coin<aptos_coin::AptosCoin>)
-

-
-
-
-

-Implementation
-
-
-
public(friend) fun add_transaction_fee(validator_addr: address, fee: Coin<AptosCoin>) acquires ValidatorFees {
-    let fees_table = &mut borrow_global_mut<ValidatorFees>(@aptos_framework).fees_table;
-    if (table::contains(fees_table, validator_addr)) {
-        let collected_fee = table::borrow_mut(fees_table, validator_addr);
-        coin::merge(collected_fee, fee);
-    } else {
-        table::add(fees_table, validator_addr, fee);
-    }
-}
-

-
-
-
-

-
 
 
 ## Function `check_signer_permission`
@@ -2041,7 +1972,6 @@ Grant permission to mutate staking on behalf of the master signer.
 
 
 
->>>>>>> ad2ce2aa1c (framework permissions)
 
 
 ## Function `get_lockup_secs`
@@ -4746,7 +4676,6 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-<<<<<<< HEAD
 
 
 
@@ -4803,8 +4732,6 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-=======
->>>>>>> ad2ce2aa1c (framework permissions)
 
 
 
@@ -5084,6 +5011,11 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
pragma verify_duration_estimate = 120;
+pragma verify = false;
+pragma aborts_if_is_partial;
+include AbortsIfSignerPermissionStake {
+    s: owner
+};
 include ResourceRequirement;
 let addr = signer::address_of(owner);
 ensures global<ValidatorConfig>(addr) == ValidatorConfig {
@@ -5115,7 +5047,10 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-
let pubkey_from_pop = bls12381::spec_public_key_from_bytes_with_pop(
+
include AbortsIfSignerPermissionStake {
+    s: account
+};
+let pubkey_from_pop = bls12381::spec_public_key_from_bytes_with_pop(
     consensus_pubkey,
     proof_of_possession_from_bytes(proof_of_possession)
 );
@@ -5154,6 +5089,9 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
pragma verify_duration_estimate = 300;
+include AbortsIfSignerPermissionStake {
+    s: owner
+};
 let owner_address = signer::address_of(owner);
 aborts_if !exists<OwnerCapability>(owner_address);
 ensures !exists<OwnerCapability>(owner_address);
@@ -5172,7 +5110,9 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-
aborts_if permissioned_signer::spec_is_permissioned_signer(owner);
+
include AbortsIfSignerPermissionStake {
+    s: owner
+};
 let owner_address = signer::address_of(owner);
 aborts_if exists<OwnerCapability>(owner_address);
 ensures exists<OwnerCapability>(owner_address);
@@ -5233,8 +5173,11 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-
pragma verify_duration_estimate = 120;
+
pragma verify = false;
 pragma aborts_if_is_partial;
+include AbortsIfSignerPermissionStake {
+    s: owner
+};
 aborts_if reconfiguration_state::spec_is_in_progress();
 include ResourceRequirement;
 include AddStakeAbortsIfAndEnsures;
@@ -5254,7 +5197,7 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
pragma disable_invariants_in_body;
-pragma verify_duration_estimate = 300;
+pragma verify = false;
 include ResourceRequirement;
 let amount = coins.value;
 aborts_if reconfiguration_state::spec_is_in_progress();
@@ -5299,7 +5242,9 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-
aborts_if permissioned_signer::spec_is_permissioned_signer(operator);
+
include AbortsIfSignerPermissionStake {
+    s: operator
+};
 let pre_stake_pool = global<StakePool>(pool_address);
 let post validator_info = global<ValidatorConfig>(pool_address);
 aborts_if reconfiguration_state::spec_is_in_progress();
@@ -5329,7 +5274,9 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-
aborts_if permissioned_signer::spec_is_permissioned_signer(operator);
+
include AbortsIfSignerPermissionStake {
+    s: operator
+};
 let pre_stake_pool = global<StakePool>(pool_address);
 let post validator_info = global<ValidatorConfig>(pool_address);
 modifies global<ValidatorConfig>(pool_address);
@@ -5386,6 +5333,9 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
pragma verify_duration_estimate = 60;
 pragma disable_invariants_in_body;
+include AbortsIfSignerPermissionStake {
+    s: operator
+};
 aborts_if !staking_config::get_allow_validator_set_change(staking_config::get());
 aborts_if !exists<StakePool>(pool_address);
 aborts_if !exists<ValidatorConfig>(pool_address);
@@ -5463,6 +5413,9 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
pragma verify = false;
+include AbortsIfSignerPermissionStake {
+    s: owner
+};
 aborts_if reconfiguration_state::spec_is_in_progress();
 let addr = signer::address_of(owner);
 let ownership_cap = global<OwnerCapability>(addr);
@@ -5509,6 +5462,9 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
pragma disable_invariants_in_body;
 requires chain_status::is_operating();
+include AbortsIfSignerPermissionStake {
+    s: operator
+};
 aborts_if reconfiguration_state::spec_is_in_progress();
 let config = staking_config::get();
 aborts_if !staking_config::get_allow_validator_set_change(config);
@@ -5645,251 +5601,6 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-
-
-
-
-
schema AddStakeWithCapAbortsIfAndEnsures {
-    owner_cap: OwnerCapability;
-    amount: u64;
-    let pool_address = owner_cap.pool_address;
-    aborts_if !exists<StakePool>(pool_address);
-    let config = global<staking_config::StakingConfig>(@aptos_framework);
-    let validator_set = global<ValidatorSet>(@aptos_framework);
-    let voting_power_increase_limit = config.voting_power_increase_limit;
-    let post post_validator_set = global<ValidatorSet>(@aptos_framework);
-    let update_voting_power_increase = amount != 0 && (spec_contains(validator_set.active_validators, pool_address)
-                                                       || spec_contains(validator_set.pending_active, pool_address));
-    aborts_if update_voting_power_increase && validator_set.total_joining_power + amount > MAX_U128;
-    ensures update_voting_power_increase ==> post_validator_set.total_joining_power == validator_set.total_joining_power + amount;
-    aborts_if update_voting_power_increase && validator_set.total_voting_power > 0
-            && validator_set.total_voting_power * voting_power_increase_limit > MAX_U128;
-    aborts_if update_voting_power_increase && validator_set.total_voting_power > 0
-            && validator_set.total_joining_power + amount > validator_set.total_voting_power * voting_power_increase_limit / 100;
-    let stake_pool = global<StakePool>(pool_address);
-    let post post_stake_pool = global<StakePool>(pool_address);
-    let value_pending_active = stake_pool.pending_active.value;
-    let value_active = stake_pool.active.value;
-    ensures amount != 0 && spec_is_current_epoch_validator(pool_address) ==> post_stake_pool.pending_active.value == value_pending_active + amount;
-    ensures amount != 0 && !spec_is_current_epoch_validator(pool_address) ==> post_stake_pool.active.value == value_active + amount;
-    let maximum_stake = config.maximum_stake;
-    let value_pending_inactive = stake_pool.pending_inactive.value;
-    let next_epoch_voting_power = value_pending_active + value_active + value_pending_inactive;
-    let voting_power = next_epoch_voting_power + amount;
-    aborts_if amount != 0 && voting_power > MAX_U64;
-    aborts_if amount != 0 && voting_power > maximum_stake;
-}
-

-
-
-
-
-
-
-
-
schema AddStakeAbortsIfAndEnsures {
-    owner: signer;
-    amount: u64;
-    let owner_address = signer::address_of(owner);
-    aborts_if !exists<OwnerCapability>(owner_address);
-    let owner_cap = global<OwnerCapability>(owner_address);
-    include AddStakeWithCapAbortsIfAndEnsures { owner_cap };
-}
-

-
-
-
-
-
-
-
-
fun spec_is_allowed(account: address): bool {
-   if (!exists<AllowedValidators>(@aptos_framework)) {
-       true
-   } else {
-       let allowed = global<AllowedValidators>(@aptos_framework);
-       contains(allowed.accounts, account)
-   }
-}
-

-
-
-
-
-
-
-
-
fun spec_find_validator(v: vector<ValidatorInfo>, addr: address): Option<u64>;
-

-
-
-
-
-
-
-
-
fun spec_validators_are_initialized(validators: vector<ValidatorInfo>): bool {
-   forall i in 0..len(validators):
-       spec_has_stake_pool(validators[i].addr) &&
-           spec_has_validator_config(validators[i].addr)
-}
-

-
-
-
-
-
-
-
-
fun spec_validators_are_initialized_addrs(addrs: vector<address>): bool {
-   forall i in 0..len(addrs):
-       spec_has_stake_pool(addrs[i]) &&
-           spec_has_validator_config(addrs[i])
-}
-

-
-
-
-
-
-
-
-
fun spec_validator_indices_are_valid(validators: vector<ValidatorInfo>): bool {
-   spec_validator_indices_are_valid_addr(validators, spec_validator_index_upper_bound()) &&
-       spec_validator_indices_are_valid_config(validators, spec_validator_index_upper_bound())
-}
-

-
-
-
-
-
-
-
-
fun spec_validator_indices_are_valid_addr(validators: vector<ValidatorInfo>, upper_bound: u64): bool {
-   forall i in 0..len(validators):
-       global<ValidatorConfig>(validators[i].addr).validator_index < upper_bound
-}
-

-
-
-
-
-
-
-
-
fun spec_validator_indices_are_valid_config(validators: vector<ValidatorInfo>, upper_bound: u64): bool {
-   forall i in 0..len(validators):
-       validators[i].config.validator_index < upper_bound
-}
-

-
-
-
-
-
-
-
-
fun spec_validator_indices_active_pending_inactive(validator_set: ValidatorSet): bool {
-   len(validator_set.pending_inactive) + len(validator_set.active_validators) == spec_validator_index_upper_bound()
-}
-

-
-
-
-
-
-
-
-
fun spec_validator_index_upper_bound(): u64 {
-   len(global<ValidatorPerformance>(@aptos_framework).validators)
-}
-

-
-
-
-
-
-
-
-
fun spec_has_stake_pool(a: address): bool {
-   exists<StakePool>(a)
-}
-

-
-
-
-
-
-
-
-
fun spec_has_validator_config(a: address): bool {
-   exists<ValidatorConfig>(a)
-}
-

-
-
-
-<<<<<<< HEAD
-=======
-
-
-
-
-
fun spec_rewards_amount(
-   stake_amount: u64,
-   num_successful_proposals: u64,
-   num_total_proposals: u64,
-   rewards_rate: u64,
-   rewards_rate_denominator: u64,
-): u64;
-

-
-
-
-
-
-
-
-
fun spec_contains(validators: vector<ValidatorInfo>, addr: address): bool {
-   exists i in 0..len(validators): validators[i].addr == addr
-}
-

-
-
-
-
-
-
-
-
fun spec_is_current_epoch_validator(pool_address: address): bool {
-   let validator_set = global<ValidatorSet>(@aptos_framework);
-   !spec_contains(validator_set.pending_active, pool_address)
-       && (spec_contains(validator_set.active_validators, pool_address)
-       || spec_contains(validator_set.pending_inactive, pool_address))
-}
-

-
-
-
-
-
-
-
-
schema ResourceRequirement {
-    requires exists<AptosCoinCapabilities>(@aptos_framework);
-    requires exists<ValidatorPerformance>(@aptos_framework);
-    requires exists<ValidatorSet>(@aptos_framework);
-    requires exists<StakingConfig>(@aptos_framework);
-    requires exists<StakingRewardsConfig>(@aptos_framework) || !features::spec_periodical_reward_rate_decrease_enabled();
-    requires exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework);
-    requires exists<ValidatorFees>(@aptos_framework);
-}
-

-
-
-
->>>>>>> ad2ce2aa1c (framework permissions)
 
 
 ### Function `update_stake_pool`
@@ -5940,6 +5651,19 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
+
+
+
+
schema AbortsIfSignerPermissionStake {
+    s: signer;
+    let perm = StakePermission {};
+    aborts_if !permissioned_signer::spec_check_permission_exists(s, perm);
+}
+

+
+
+
+
 
 
 
@@ -6014,6 +5738,7 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
pragma opaque;
 pragma verify_duration_estimate = 300;
+pragma verify = false;
 requires rewards_rate <= MAX_REWARDS_RATE;
 requires rewards_rate_denominator > 0;
 requires rewards_rate <= rewards_rate_denominator;
diff --git a/aptos-move/framework/aptos-framework/doc/staking_proxy.md b/aptos-move/framework/aptos-framework/doc/staking_proxy.md
index e8a756c4039fc3..a15a4684c34b18 100644
--- a/aptos-move/framework/aptos-framework/doc/staking_proxy.md
+++ b/aptos-move/framework/aptos-framework/doc/staking_proxy.md
@@ -20,6 +20,7 @@
 -  [Specification](#@Specification_1)
     -  [High-level Requirements](#high-level-req)
     -  [Module-level Specification](#module-level-spec)
+    -  [Function `grant_permission`](#@Specification_1_grant_permission)
     -  [Function `set_operator`](#@Specification_1_set_operator)
     -  [Function `set_voter`](#@Specification_1_set_voter)
     -  [Function `set_vesting_contract_operator`](#@Specification_1_set_vesting_contract_operator)
@@ -436,6 +437,25 @@ Grant permission to mutate staking on behalf of the master signer.
 
 
 
+
+
+### Function `grant_permission`
+
+
+
public fun grant_permission(master: &signer, permissioned_signer: &signer)
+

+
+
+
+
+
pragma aborts_if_is_partial;
+aborts_if !permissioned_signer::spec_is_permissioned_signer(permissioned_signer);
+aborts_if permissioned_signer::spec_is_permissioned_signer(master);
+aborts_if signer::address_of(master) != signer::address_of(permissioned_signer);
+

+
+
+
 
 
 ### Function `set_operator`
@@ -559,6 +579,12 @@ One of them are not exists
 
 
 
include SetStakePoolOperator;
+include AbortsIfSignerPermissionStakeProxy {
+    s: owner
+};
+include exists<stake::StakePool>(signer::address_of(owner)) ==> stake::AbortsIfSignerPermissionStake {
+    s:owner
+};
 

 
 
@@ -570,7 +596,9 @@ One of them are not exists
 
schema SetStakePoolOperator {
     owner: &signer;
     new_operator: address;
-    aborts_if permissioned_signer::spec_is_permissioned_signer(owner);
+    include AbortsIfSignerPermissionStakeProxy {
+        s: owner
+    };
     let owner_address = signer::address_of(owner);
     let ownership_cap = borrow_global<stake::OwnerCapability>(owner_address);
     let pool_address = ownership_cap.pool_address;
@@ -609,6 +637,9 @@ One of them are not exists
 
 
 
include SetStakingContractVoter;
+include AbortsIfSignerPermissionStakeProxy {
+    s: owner
+};
 

 
 
@@ -651,6 +682,12 @@ Then abort if the resource is not exist
 
 
 
include SetStakePoolVoterAbortsIf;
+include AbortsIfSignerPermissionStakeProxy {
+    s: owner
+};
+include exists<stake::StakePool>(signer::address_of(owner)) ==> stake::AbortsIfSignerPermissionStake {
+    s:owner
+};
 

 
 
@@ -662,7 +699,9 @@ Then abort if the resource is not exist
 
schema SetStakePoolVoterAbortsIf {
     owner: &signer;
     new_voter: address;
-    aborts_if permissioned_signer::spec_is_permissioned_signer(owner);
+    include AbortsIfSignerPermissionStakeProxy {
+        s: owner
+    };
     let owner_address = signer::address_of(owner);
     let ownership_cap = global<stake::OwnerCapability>(owner_address);
     let pool_address = ownership_cap.pool_address;
@@ -672,4 +711,17 @@ Then abort if the resource is not exist
 

 
 
+
+
+
+
+
+
schema AbortsIfSignerPermissionStakeProxy {
+    s: signer;
+    let perm = StakeProxyPermission {};
+    aborts_if !permissioned_signer::spec_check_permission_exists(s, perm);
+}
+

+
+
 [move-book]: https://aptos.dev/move/book/SUMMARY
diff --git a/aptos-move/framework/aptos-framework/sources/aptos_governance.spec.move b/aptos-move/framework/aptos-framework/sources/aptos_governance.spec.move
index 41e31d566be6fa..d9b06f67211a85 100644
--- a/aptos-move/framework/aptos-framework/sources/aptos_governance.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/aptos_governance.spec.move
@@ -63,6 +63,7 @@ spec aptos_framework::aptos_governance {
         let addr = signer::address_of(aptos_framework);
         let register_account = global(addr);
 
+        aborts_if permissioned_signer::spec_is_permissioned_signer(aptos_framework);
         aborts_if exists>(addr);
         aborts_if !exists(addr);
         aborts_if register_account.guid_creation_num + 7 > MAX_U64;
diff --git a/aptos-move/framework/aptos-framework/sources/stake.spec.move b/aptos-move/framework/aptos-framework/sources/stake.spec.move
index 8146baea0f3984..a4c3b4989bf37b 100644
--- a/aptos-move/framework/aptos-framework/sources/stake.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/stake.spec.move
@@ -125,6 +125,9 @@ spec aptos_framework::stake {
         network_addresses: vector,
         fullnode_addresses: vector,
     ){
+        include AbortsIfSignerPermissionStake {
+            s: account
+        };
         let pubkey_from_pop = bls12381::spec_public_key_from_bytes_with_pop(
             consensus_pubkey,
             proof_of_possession_from_bytes(proof_of_possession)
@@ -170,6 +173,9 @@ spec aptos_framework::stake {
         // This function casue timeout (property proved)
         pragma verify_duration_estimate = 60;
         pragma disable_invariants_in_body;
+        include AbortsIfSignerPermissionStake {
+            s: operator
+        };
         aborts_if !staking_config::get_allow_validator_set_change(staking_config::get());
         aborts_if !exists(pool_address);
         aborts_if !exists(pool_address);
@@ -223,6 +229,9 @@ spec aptos_framework::stake {
     {
         // TODO(fa_migration)
         pragma verify = false;
+        include AbortsIfSignerPermissionStake {
+            s: owner
+        };
         aborts_if reconfiguration_state::spec_is_in_progress();
         let addr = signer::address_of(owner);
         let ownership_cap = global(addr);
@@ -262,6 +271,9 @@ spec aptos_framework::stake {
     ) {
         pragma disable_invariants_in_body;
         requires chain_status::is_operating();
+        include AbortsIfSignerPermissionStake {
+            s: operator
+        };
         aborts_if reconfiguration_state::spec_is_in_progress();
         let config = staking_config::get();
         aborts_if !staking_config::get_allow_validator_set_change(config);
@@ -297,13 +309,19 @@ spec aptos_framework::stake {
     spec extract_owner_cap(owner: &signer): OwnerCapability {
         // TODO: set because of timeout (property proved)
         pragma verify_duration_estimate = 300;
+        include AbortsIfSignerPermissionStake {
+            s: owner
+        };
         let owner_address = signer::address_of(owner);
         aborts_if !exists(owner_address);
         ensures !exists(owner_address);
     }
 
     spec deposit_owner_cap(owner: &signer, owner_cap: OwnerCapability) {
-        aborts_if permissioned_signer::spec_is_permissioned_signer(owner);
+        include AbortsIfSignerPermissionStake {
+            s: owner
+        };
+        // aborts_if permissioned_signer::spec_is_permissioned_signer(owner);
         let owner_address = signer::address_of(owner);
         aborts_if exists(owner_address);
         ensures exists(owner_address);
@@ -352,7 +370,10 @@ spec aptos_framework::stake {
         new_network_addresses: vector,
         new_fullnode_addresses: vector,
     ) {
-        aborts_if permissioned_signer::spec_is_permissioned_signer(operator);
+        include AbortsIfSignerPermissionStake {
+            s: operator
+        };
+        // aborts_if permissioned_signer::spec_is_permissioned_signer(operator);
         let pre_stake_pool = global(pool_address);
         let post validator_info = global(pool_address);
         modifies global(pool_address);
@@ -399,7 +420,10 @@ spec aptos_framework::stake {
         new_consensus_pubkey: vector,
         proof_of_possession: vector,
     ) {
-        aborts_if permissioned_signer::spec_is_permissioned_signer(operator);
+        include AbortsIfSignerPermissionStake {
+            s: operator
+        };
+        // aborts_if permissioned_signer::spec_is_permissioned_signer(operator);
         let pre_stake_pool = global(pool_address);
         let post validator_info = global(pool_address);
         aborts_if reconfiguration_state::spec_is_in_progress();
@@ -505,6 +529,13 @@ spec aptos_framework::stake {
         };
     }
 
+    spec schema AbortsIfSignerPermissionStake {
+        use aptos_framework::permissioned_signer;
+        s: signer;
+        let perm = StakePermission {};
+        aborts_if !permissioned_signer::spec_check_permission_exists(s, perm);
+    }
+
     spec schema UpdateStakePoolAbortsIf {
         use aptos_std::type_info;
 
@@ -593,6 +624,7 @@ spec aptos_framework::stake {
         pragma opaque;
         // TODO: set because of timeout (property proved)
         pragma verify_duration_estimate = 300;
+        pragma verify = false;
         requires rewards_rate <= MAX_REWARDS_RATE;
         requires rewards_rate_denominator > 0;
         requires rewards_rate <= rewards_rate_denominator;
@@ -670,7 +702,7 @@ spec aptos_framework::stake {
 
     spec add_stake_with_cap {
         pragma disable_invariants_in_body;
-        pragma verify_duration_estimate = 300;
+        pragma verify = false;
         include ResourceRequirement;
         let amount = coins.value;
         aborts_if reconfiguration_state::spec_is_in_progress();
@@ -678,10 +710,13 @@ spec aptos_framework::stake {
     }
 
     spec add_stake {
-        // TODO: These function passed locally however failed in github CI
-        pragma verify_duration_estimate = 120;
+        // TODO: fix
+        pragma verify = false;
         // TODO(fa_migration)
         pragma aborts_if_is_partial;
+        include AbortsIfSignerPermissionStake {
+            s: owner
+        };
         aborts_if reconfiguration_state::spec_is_in_progress();
         include ResourceRequirement;
         include AddStakeAbortsIfAndEnsures;
@@ -695,7 +730,11 @@ spec aptos_framework::stake {
     ) {
         // TODO: These function failed in github CI
         pragma verify_duration_estimate = 120;
-
+        pragma verify = false;
+        pragma aborts_if_is_partial;
+        include AbortsIfSignerPermissionStake {
+            s: owner
+        };
         include ResourceRequirement;
         let addr = signer::address_of(owner);
         ensures global(addr) == ValidatorConfig {
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 d5b6ba29ad82e8..5c3bda7784349e 100644
--- a/aptos-move/framework/aptos-framework/sources/staking_proxy.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/staking_proxy.spec.move
@@ -44,6 +44,13 @@ spec aptos_framework::staking_proxy {
         pragma aborts_if_is_strict;
     }
 
+    spec grant_permission {
+        pragma aborts_if_is_partial;
+        aborts_if !permissioned_signer::spec_is_permissioned_signer(permissioned_signer);
+        aborts_if permissioned_signer::spec_is_permissioned_signer(master);
+        aborts_if signer::address_of(master) != signer::address_of(permissioned_signer);
+    }
+
     /// Aborts if conditions of SetStakePoolOperator are not met
     spec set_operator(owner: &signer, old_operator: address, new_operator: address) {
         pragma verify = false;
@@ -122,6 +129,12 @@ spec aptos_framework::staking_proxy {
     /// One of them are not exists
     spec set_stake_pool_operator(owner: &signer, new_operator: address) {
         include SetStakePoolOperator;
+        include AbortsIfSignerPermissionStakeProxy {
+            s: owner
+        };
+        include exists(signer::address_of(owner)) ==> stake::AbortsIfSignerPermissionStake {
+            s:owner
+        };
     }
 
     spec schema SetStakePoolOperator {
@@ -130,7 +143,9 @@ spec aptos_framework::staking_proxy {
         owner: &signer;
         new_operator: address;
 
-        aborts_if permissioned_signer::spec_is_permissioned_signer(owner);
+        include AbortsIfSignerPermissionStakeProxy {
+            s: owner
+        };
         let owner_address = signer::address_of(owner);
         let ownership_cap = borrow_global(owner_address);
         let pool_address = ownership_cap.pool_address;
@@ -140,6 +155,9 @@ spec aptos_framework::staking_proxy {
 
     spec set_staking_contract_voter(owner: &signer, operator: address, new_voter: address) {
         include SetStakingContractVoter;
+        include AbortsIfSignerPermissionStakeProxy {
+            s: owner
+        };
     }
 
     /// Make sure staking_contract_exists first
@@ -169,6 +187,12 @@ spec aptos_framework::staking_proxy {
 
     spec set_stake_pool_voter(owner: &signer, new_voter: address) {
         include SetStakePoolVoterAbortsIf;
+        include AbortsIfSignerPermissionStakeProxy {
+            s: owner
+        };
+        include exists(signer::address_of(owner)) ==> stake::AbortsIfSignerPermissionStake {
+            s:owner
+        };
     }
 
     spec schema SetStakePoolVoterAbortsIf {
@@ -177,11 +201,20 @@ spec aptos_framework::staking_proxy {
         owner: &signer;
         new_voter: address;
 
-        aborts_if permissioned_signer::spec_is_permissioned_signer(owner);
+        include AbortsIfSignerPermissionStakeProxy {
+            s: owner
+        };
         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));
         ensures stake::stake_pool_exists(owner_address) ==> global(pool_address).delegated_voter == new_voter;
     }
+
+    spec schema AbortsIfSignerPermissionStakeProxy {
+        use aptos_framework::permissioned_signer;
+        s: signer;
+        let perm = StakeProxyPermission {};
+        aborts_if !permissioned_signer::spec_check_permission_exists(s, perm);
+    }
 }
diff --git a/aptos-move/framework/aptos-stdlib/doc/smart_table.md b/aptos-move/framework/aptos-stdlib/doc/smart_table.md
index 83eb27ba47fff6..332646552eb049 100644
--- a/aptos-move/framework/aptos-stdlib/doc/smart_table.md
+++ b/aptos-move/framework/aptos-stdlib/doc/smart_table.md
@@ -1480,6 +1480,7 @@ map_spec_has_key = spec_contains;
 
 
pragma verify = false;
 pragma opaque;
+aborts_if [abstract] false;
 

 
 
@@ -1497,6 +1498,7 @@ map_spec_has_key = spec_contains;
 
 
pragma verify = false;
 pragma opaque;
+aborts_if false;
 

 
 
diff --git a/aptos-move/framework/aptos-stdlib/sources/data_structures/smart_table.spec.move b/aptos-move/framework/aptos-stdlib/sources/data_structures/smart_table.spec.move
index 4344eb2329efbd..18d0cc53056d6f 100644
--- a/aptos-move/framework/aptos-stdlib/sources/data_structures/smart_table.spec.move
+++ b/aptos-move/framework/aptos-stdlib/sources/data_structures/smart_table.spec.move
@@ -25,11 +25,13 @@ spec aptos_std::smart_table {
     spec destroy(self: SmartTable) {
         pragma verify = false;
         pragma opaque;
+        aborts_if [abstract] false;
     }
 
     spec clear(self: &mut SmartTable) {
         pragma verify = false;
         pragma opaque;
+        aborts_if false;
     }
 
     spec split_one_bucket(self: &mut SmartTable) {