From 92fbdcb0c21bb02cd55b0d08259a128c0d98d77f Mon Sep 17 00:00:00 2001 From: Teng Zhang Date: Mon, 25 Sep 2023 14:49:45 -0700 Subject: [PATCH 1/2] fix spec --- .../aptos-framework/doc/aptos_governance.md | 75 +-------- .../framework/aptos-framework/doc/stake.md | 150 ++++++++++++++++-- .../sources/aptos_governance.spec.move | 3 +- .../aptos-framework/sources/stake.spec.move | 54 +++---- 4 files changed, 164 insertions(+), 118 deletions(-) diff --git a/aptos-move/framework/aptos-framework/doc/aptos_governance.md b/aptos-move/framework/aptos-framework/doc/aptos_governance.md index e9b9b12ad24a8..048f320585033 100644 --- a/aptos-move/framework/aptos-framework/doc/aptos_governance.md +++ b/aptos-move/framework/aptos-framework/doc/aptos_governance.md @@ -2064,79 +2064,6 @@ The same as spec of - - -
schema CreateProposalAbortsIf {
-    proposer: &signer;
-    stake_pool: address;
-    execution_hash: vector<u8>;
-    metadata_location: vector<u8>;
-    metadata_hash: vector<u8>;
-    include VotingGetDelegatedVoterAbortsIf { sign: proposer };
-    include AbortsIfNotGovernanceConfig;
-    include GetVotingPowerAbortsIf { pool_address: stake_pool };
-    let staking_config = global<staking_config::StakingConfig>(@aptos_framework);
-    let allow_validator_set_change = staking_config.allow_validator_set_change;
-    let stake_pool_res = global<stake::StakePool>(stake_pool);
-    let stake_balance_0 = stake_pool_res.active.value + stake_pool_res.pending_active.value + stake_pool_res.pending_inactive.value;
-    let stake_balance_1 = stake_pool_res.active.value + stake_pool_res.pending_inactive.value;
-    let stake_balance_2 = 0;
-    let governance_config = global<GovernanceConfig>(@aptos_framework);
-    let required_proposer_stake = governance_config.required_proposer_stake;
-    aborts_if allow_validator_set_change && stake_balance_0 < required_proposer_stake;
-    aborts_if !allow_validator_set_change && stake::spec_is_current_epoch_validator(stake_pool) && stake_balance_1 < required_proposer_stake;
-    aborts_if !allow_validator_set_change && !stake::spec_is_current_epoch_validator(stake_pool) && stake_balance_2 < required_proposer_stake;
-    aborts_if !exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework);
-    let current_time = timestamp::spec_now_seconds();
-    let proposal_expiration = current_time + governance_config.voting_duration_secs;
-    aborts_if stake_pool_res.locked_until_secs < proposal_expiration;
-    include CreateProposalMetadataAbortsIf;
-    let addr = aptos_std::type_info::type_of<AptosCoin>().account_address;
-    aborts_if !exists<coin::CoinInfo<AptosCoin>>(addr);
-    let maybe_supply = global<coin::CoinInfo<AptosCoin>>(addr).supply;
-    let supply = option::spec_borrow(maybe_supply);
-    let total_supply = aptos_framework::optional_aggregator::optional_aggregator_value(supply);
-    let early_resolution_vote_threshold_value = total_supply / 2 + 1;
-    aborts_if option::spec_is_some(maybe_supply) && governance_config.min_voting_threshold > early_resolution_vote_threshold_value;
-    aborts_if len(execution_hash) <= 0;
-    aborts_if !exists<voting::VotingForum<GovernanceProposal>>(@aptos_framework);
-    let voting_forum = global<voting::VotingForum<GovernanceProposal>>(@aptos_framework);
-    let proposal_id = voting_forum.next_proposal_id;
-    aborts_if proposal_id + 1 > MAX_U64;
-    let post post_voting_forum = global<voting::VotingForum<GovernanceProposal>>(@aptos_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(voting::IS_MULTI_STEP_PROPOSAL_KEY);
-    aborts_if !string::spec_internal_check_utf8(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<GovernanceEvents>(@aptos_framework);
-}
-
- - - - - - - -
schema VotingGetDelegatedVoterAbortsIf {
-    stake_pool: address;
-    sign: signer;
-    let addr = signer::address_of(sign);
-    let stake_pool_res = global<stake::StakePool>(stake_pool);
-    aborts_if !exists<stake::StakePool>(stake_pool);
-    aborts_if stake_pool_res.delegated_voter != addr;
-}
-
- - @@ -2567,7 +2494,7 @@ Signer address must be @aptos_framework. Address @aptos_framework must exist GovernanceConfig and GovernanceEvents. -
pragma verify = false;
+
pragma verify_duration_estimate = 200;
 let addr = signer::address_of(aptos_framework);
 aborts_if addr != @aptos_framework;
 include transaction_fee::RequiresCollectedFeesPerValueLeqBlockAptosSupply;
diff --git a/aptos-move/framework/aptos-framework/doc/stake.md b/aptos-move/framework/aptos-framework/doc/stake.md
index 68e3dd5d5bbb7..1bfcdece8d34b 100644
--- a/aptos-move/framework/aptos-framework/doc/stake.md
+++ b/aptos-move/framework/aptos-framework/doc/stake.md
@@ -108,6 +108,7 @@ or if their stake drops below the min required, they would get removed at the en
 -  [Function `assert_owner_cap_exists`](#0x1_stake_assert_owner_cap_exists)
 -  [Function `copy_aptos_coin_mint_cap_for_storage_refund`](#0x1_stake_copy_aptos_coin_mint_cap_for_storage_refund)
 -  [Specification](#@Specification_1)
+    -  [Resource `ValidatorSet`](#@Specification_1_ValidatorSet)
     -  [Function `initialize_validator_fees`](#@Specification_1_initialize_validator_fees)
     -  [Function `add_transaction_fee`](#@Specification_1_add_transaction_fee)
     -  [Function `get_validator_state`](#@Specification_1_get_validator_state)
@@ -3630,16 +3631,114 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-
+
 
 
-
schema ConsensusInv {
-    invariant global<ValidatorSet>(@aptos_framework).consensus_scheme == 0;
+
fun spec_get_reward_rate_1(config: StakingConfig): num {
+   if (features::spec_periodical_reward_rate_decrease_enabled()) {
+       let epoch_rewards_rate = global<staking_config::StakingRewardsConfig>(@aptos_framework).rewards_rate;
+       if (epoch_rewards_rate.value == 0) {
+           0
+       } else {
+           let denominator_0 = aptos_std::fixed_point64::spec_divide_u128(staking_config::MAX_REWARDS_RATE, epoch_rewards_rate);
+           let denominator = if (denominator_0 > MAX_U64) {
+               MAX_U64
+           } else {
+               denominator_0
+           };
+           let nominator = aptos_std::fixed_point64::spec_multiply_u128(denominator, epoch_rewards_rate);
+           nominator
+       }
+   } else {
+           config.rewards_rate
+   }
+}
+

+
+
+
+
+
+
+
+
fun spec_get_reward_rate_2(config: StakingConfig): num {
+   if (features::spec_periodical_reward_rate_decrease_enabled()) {
+       let epoch_rewards_rate = global<staking_config::StakingRewardsConfig>(@aptos_framework).rewards_rate;
+       if (epoch_rewards_rate.value == 0) {
+           1
+       } else {
+           let denominator_0 = aptos_std::fixed_point64::spec_divide_u128(staking_config::MAX_REWARDS_RATE, epoch_rewards_rate);
+           let denominator = if (denominator_0 > MAX_U64) {
+               MAX_U64
+           } else {
+               denominator_0
+           };
+           denominator
+       }
+   } else {
+           config.rewards_rate_denominator
+   }
 }
 

 
 
 
+
+
+### Resource `ValidatorSet`
+
+
+
struct ValidatorSet has key
+

+
+
+
+

+

+consensus_scheme: u8
+

+

+
+

+

+active_validators: vector<stake::ValidatorInfo>
+

+

+
+

+

+pending_inactive: vector<stake::ValidatorInfo>
+

+

+
+

+

+pending_active: vector<stake::ValidatorInfo>
+

+

+
+

+

+total_voting_power: u128
+

+

+
+

+

+total_joining_power: u128
+

+

+
+

+

+
+
+
+
invariant consensus_scheme == 0;
+

+
+
+
 
 
 
@@ -3657,12 +3756,11 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
schema StakedValueNochange {
-    ensures forall addr: address where old(exists<StakePool>(addr)): {
-        let stake_pool = old(global<StakePool>(addr));
-        let post_stake_pool = global<StakePool>(addr);
-        stake_pool.active.value + stake_pool.inactive.value + stake_pool.pending_active.value + stake_pool.pending_inactive.value ==
-        post_stake_pool.active.value + post_stake_pool.inactive.value + post_stake_pool.pending_active.value + post_stake_pool.pending_inactive.value
-    };
+    pool_address: address;
+    let stake_pool = global<StakePool>(pool_address);
+    let post post_stake_pool = global<StakePool>(pool_address);
+    ensures stake_pool.active.value + stake_pool.inactive.value + stake_pool.pending_active.value + stake_pool.pending_inactive.value ==
+        post_stake_pool.active.value + post_stake_pool.inactive.value + post_stake_pool.pending_active.value + post_stake_pool.pending_inactive.value;
 }
 

 
@@ -3861,9 +3959,10 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
let pool_address = owner_cap.pool_address;
-let post stake_pool = global<StakePool>(pool_address);
+let post post_stake_pool = global<StakePool>(pool_address);
 modifies global<StakePool>(pool_address);
-ensures stake_pool.operator_address == new_operator;
+include StakedValueNochange;
+ensures post_stake_pool.operator_address == new_operator;
 

 
 
@@ -3880,10 +3979,11 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
let pool_address = owner_cap.pool_address;
-let post stake_pool = global<StakePool>(pool_address);
+let post post_stake_pool = global<StakePool>(pool_address);
+include StakedValueNochange;
 aborts_if !exists<StakePool>(pool_address);
 modifies global<StakePool>(pool_address);
-ensures stake_pool.delegated_voter == new_voter;
+ensures post_stake_pool.delegated_voter == new_voter;
 

 
 
@@ -3935,6 +4035,7 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
let pool_address = owner_cap.pool_address;
+include StakedValueNochange;
 aborts_if !stake_pool_exists(pool_address);
 let pre_stake_pool = global<StakePool>(pool_address);
 let post stake_pool = global<StakePool>(pool_address);
@@ -3964,6 +4065,7 @@ Returns validator's next epoch voting power, including pending_active, active, a
 aborts_if signer::address_of(operator) != pre_stake_pool.operator_address;
 aborts_if !exists<ValidatorConfig>(pool_address);
 modifies global<ValidatorConfig>(pool_address);
+include StakedValueNochange;
 ensures validator_info.consensus_pubkey == new_consensus_pubkey;
 

 
@@ -3983,6 +4085,7 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
let pre_stake_pool = global<StakePool>(pool_address);
 let post validator_info = global<ValidatorConfig>(pool_address);
 modifies global<ValidatorConfig>(pool_address);
+include StakedValueNochange;
 aborts_if !exists<StakePool>(pool_address);
 aborts_if !exists<ValidatorConfig>(pool_address);
 aborts_if signer::address_of(operator) != pre_stake_pool.operator_address;
@@ -4010,6 +4113,7 @@ Returns validator's next epoch voting power, including pending_active, active, a
 let now_seconds = timestamp::spec_now_seconds();
 let lockup = config.recurring_lockup_duration_secs;
 modifies global<StakePool>(pool_address);
+include StakedValueNochange;
 aborts_if !exists<StakePool>(pool_address);
 aborts_if pre_stake_pool.locked_until_secs >= lockup + now_seconds;
 aborts_if lockup + now_seconds > MAX_U64;
@@ -4036,6 +4140,7 @@ Returns validator's next epoch voting power, including pending_active, active, a
 let post stake_pool = global<StakePool>(pool_address);
 aborts_if amount != 0 && !exists<StakePool>(pool_address);
 modifies global<StakePool>(pool_address);
+include StakedValueNochange;
 let min_amount = aptos_std::math64::min(amount,pre_stake_pool.active.value);
 ensures stake_pool.active.value == pre_stake_pool.active.value - min_amount;
 ensures stake_pool.pending_inactive.value == pre_stake_pool.pending_inactive.value + min_amount;
@@ -4114,7 +4219,7 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-
pragma verify = false;
+
pragma verify_duration_estimate = 200;
 include ResourceRequirement;
 include staking_config::StakingRewardsConfigRequirement;
 aborts_if !exists<StakePool>(pool_address);
@@ -4533,4 +4638,21 @@ Returns validator's next epoch voting power, including pending_active, active, a
 

 
 
+
+
+
+
+
+
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);
+}
+

+
+
 [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 2b8b55cb48741..63f9b092d80e8 100644
--- a/aptos-move/framework/aptos-framework/sources/aptos_governance.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/aptos_governance.spec.move
@@ -109,8 +109,7 @@ spec aptos_framework::aptos_governance {
         use aptos_framework::aptos_coin::AptosCoin;
         use aptos_framework::transaction_fee;
 
-        // turn off becasue of timeout (property proved)
-        pragma verify = false;
+        pragma verify_duration_estimate = 200;
         let addr = signer::address_of(aptos_framework);
         aborts_if addr != @aptos_framework;
 
diff --git a/aptos-move/framework/aptos-framework/sources/stake.spec.move b/aptos-move/framework/aptos-framework/sources/stake.spec.move
index fe3049c56ec83..ca23aad99d75f 100644
--- a/aptos-move/framework/aptos-framework/sources/stake.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/stake.spec.move
@@ -11,27 +11,18 @@ spec aptos_framework::stake {
         invariant [suspendable] chain_status::is_operating() ==> exists(@aptos_framework);
         invariant [suspendable] chain_status::is_operating() ==> exists(@aptos_framework);
 
-        // property 1: the validator set resource stores consensus information for each validator.
-        // the consensus scheme remains consistent across all validators within the set.
-        // this property cause timeout (not proved)
-
-        // apply ConsensusInv to * except on_new_epoch;
-
         // property 2: The owner of a validator remains immutable.
         apply ValidatorOwnerNoChange to *;
 
-        // property 3: The total staked value in the stake pool should be constant (excluding adding and withdrawing operations).
-        // this property cause timeout (proved)
-
-        // apply StakedValueNochange to * except add_stake, add_stake_with_cap, withdraw, withdraw_with_cap, on_new_epoch, update_stake_pool;
-
         // ghost variable
         global ghost_valid_perf: ValidatorPerformance;
         global ghost_proposer_idx: Option;
     }
 
-    spec schema ConsensusInv{
-        invariant global(@aptos_framework).consensus_scheme == 0;
+    // property 1: the validator set resource stores consensus information for each validator.
+    // the consensus scheme remains consistent across all validators within the set.
+    spec ValidatorSet {
+        invariant consensus_scheme == 0;
     }
 
     spec schema ValidatorOwnerNoChange {
@@ -39,13 +30,13 @@ spec aptos_framework::stake {
             old(global(addr)).pool_address == global(addr).pool_address;
     }
 
+    // property 3: The total staked value in the stake pool should be constant (excluding adding and withdrawing operations).
     spec schema StakedValueNochange {
-        ensures forall addr: address where old(exists(addr)): {
-            let stake_pool = old(global(addr));
-            let post_stake_pool = global(addr);
-            stake_pool.active.value + stake_pool.inactive.value + stake_pool.pending_active.value + stake_pool.pending_inactive.value ==
-            post_stake_pool.active.value + post_stake_pool.inactive.value + post_stake_pool.pending_active.value + post_stake_pool.pending_inactive.value
-        };
+        pool_address: address;
+        let stake_pool = global(pool_address);
+        let post post_stake_pool = global(pool_address);
+        ensures stake_pool.active.value + stake_pool.inactive.value + stake_pool.pending_active.value + stake_pool.pending_inactive.value ==
+            post_stake_pool.active.value + post_stake_pool.inactive.value + post_stake_pool.pending_active.value + post_stake_pool.pending_inactive.value;
     }
 
     // A desired invariant for the validator set.
@@ -100,6 +91,7 @@ spec aptos_framework::stake {
         let post stake_pool = global(pool_address);
         aborts_if amount != 0 && !exists(pool_address);
         modifies global(pool_address);
+        include StakedValueNochange;
         let min_amount = aptos_std::math64::min(amount,pre_stake_pool.active.value);
 
         ensures stake_pool.active.value == pre_stake_pool.active.value - min_amount;
@@ -115,6 +107,7 @@ spec aptos_framework::stake {
         let now_seconds = timestamp::spec_now_seconds();
         let lockup = config.recurring_lockup_duration_secs;
         modifies global(pool_address);
+        include StakedValueNochange;
 
         aborts_if !exists(pool_address);
         aborts_if pre_stake_pool.locked_until_secs >= lockup + now_seconds;
@@ -134,6 +127,7 @@ spec aptos_framework::stake {
         let pre_stake_pool = global(pool_address);
         let post validator_info = global(pool_address);
         modifies global(pool_address);
+        include StakedValueNochange;
 
         // Only the true operator address can update the network and full node addresses of the validator.
         aborts_if !exists(pool_address);
@@ -146,13 +140,17 @@ spec aptos_framework::stake {
 
     spec set_operator_with_cap(owner_cap: &OwnerCapability, new_operator: address) {
         let pool_address = owner_cap.pool_address;
-        let post stake_pool = global(pool_address);
+        let post post_stake_pool = global(pool_address);
         modifies global(pool_address);
-        ensures stake_pool.operator_address == new_operator;
+        include StakedValueNochange;
+
+        ensures post_stake_pool.operator_address == new_operator;
     }
 
     spec reactivate_stake_with_cap(owner_cap: &OwnerCapability, amount: u64) {
         let pool_address = owner_cap.pool_address;
+        include StakedValueNochange;
+
         aborts_if !stake_pool_exists(pool_address);
 
         let pre_stake_pool = global(pool_address);
@@ -177,16 +175,18 @@ spec aptos_framework::stake {
         aborts_if signer::address_of(operator) != pre_stake_pool.operator_address;
         aborts_if !exists(pool_address);
         modifies global(pool_address);
+        include StakedValueNochange;
 
         ensures validator_info.consensus_pubkey == new_consensus_pubkey;
     }
 
     spec set_delegated_voter_with_cap(owner_cap: &OwnerCapability, new_voter: address) {
         let pool_address = owner_cap.pool_address;
-        let post stake_pool = global(pool_address);
+        let post post_stake_pool = global(pool_address);
+        include StakedValueNochange;
         aborts_if !exists(pool_address);
         modifies global(pool_address);
-        ensures stake_pool.delegated_voter == new_voter;
+        ensures post_stake_pool.delegated_voter == new_voter;
     }
 
     spec on_new_epoch {
@@ -214,9 +214,7 @@ spec aptos_framework::stake {
     }
 
     spec update_stake_pool {
-        // Can't verify becasue of timeout (properties proved)
-        // Takes 90s to verify
-        pragma verify = false;
+        pragma verify_duration_estimate = 200;
         include ResourceRequirement;
         include staking_config::StakingRewardsConfigRequirement;
         aborts_if !exists(pool_address);
@@ -547,8 +545,8 @@ spec aptos_framework::stake {
         requires exists(@aptos_framework);
     }
 
-    // Add helper function in staking_config lead to unexpected error
-    // So we write two helper functions here to describe function staking_config::get_reward_rate().
+    // Adding helper function in staking_config leads to an unexpected error
+    // So we write two helper functions here to model function staking_config::get_reward_rate().
     spec fun spec_get_reward_rate_1(config: StakingConfig): num {
         if (features::spec_periodical_reward_rate_decrease_enabled()) {
             let epoch_rewards_rate = global(@aptos_framework).rewards_rate;

From 84a5691a92f54d3a7c3e1e99c5873dccc3c2fff8 Mon Sep 17 00:00:00 2001
From: Teng Zhang 
Date: Mon, 25 Sep 2023 16:05:11 -0700
Subject: [PATCH 2/2] staking_contract spec

---
 .../aptos-framework/doc/staking_contract.md   | 12 ++-----
 .../sources/staking_contract.spec.move        | 33 +++++++++----------
 2 files changed, 18 insertions(+), 27 deletions(-)

diff --git a/aptos-move/framework/aptos-framework/doc/staking_contract.md b/aptos-move/framework/aptos-framework/doc/staking_contract.md
index 0b14d6d035d34..c0a7aa461a184 100644
--- a/aptos-move/framework/aptos-framework/doc/staking_contract.md
+++ b/aptos-move/framework/aptos-framework/doc/staking_contract.md
@@ -2164,7 +2164,8 @@ Initialize Store resource if this is the first time the staker has delegated to
 Cannot create the staking contract if it already exists.
 
 
-
pragma verify = false;
+
pragma verify_duration_estimate = 120;
+pragma aborts_if_is_partial;
 include PreconditionsInCreateContract;
 let amount = coins.value;
 include Create_Staking_Contract_With_Coins_Abortsif { amount };
@@ -2657,18 +2658,9 @@ a staking_contract exists for the staker/operator pair.
     aborts_if !exists<Store>(staker_address) && !exists<account::Account>(staker_address);
     aborts_if !exists<Store>(staker_address) && account.guid_creation_num + 9 >= account::MAX_GUID_CREATION_NUM;
     ensures exists<Store>(staker_address);
-    let store = global<Store>(staker_address);
-    let staking_contracts = store.staking_contracts;
-    aborts_if simple_map::spec_contains_key(staking_contracts, operator);
-    let seed_0 = bcs::to_bytes(staker_address);
-    let seed_1 = concat(concat(concat(seed_0, bcs::to_bytes(operator)), SALT), contract_creation_seed);
-    let resource_addr = account::spec_create_resource_address(staker_address, seed_1);
-    include CreateStakePoolAbortsIf {resource_addr};
-    include StakeAddStakeWithCapAbortsIf{ pool_address: resource_addr };
     let post post_store = global<Store>(staker_address);
     let post post_staking_contracts = post_store.staking_contracts;
     ensures simple_map::spec_contains_key(post_staking_contracts, operator);
-    ensures amount != 0 ==> simple_map::spec_contains_key(post_staking_contracts, operator);
 }
 

 
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 12f56135f152f..6eb1d33f95739 100644
--- a/aptos-move/framework/aptos-framework/sources/staking_contract.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/staking_contract.spec.move
@@ -74,8 +74,8 @@ spec aptos_framework::staking_contract {
         commission_percentage: u64,
         contract_creation_seed: vector,
     ): address {
-        // TODO: set because of timeout
-        pragma verify = false;
+        pragma verify_duration_estimate = 120;
+        pragma aborts_if_is_partial;
         include PreconditionsInCreateContract;
 
         let amount = coins.value;
@@ -385,24 +385,23 @@ spec aptos_framework::staking_contract {
         aborts_if !exists(staker_address) && !exists(staker_address);
         aborts_if !exists(staker_address) && account.guid_creation_num + 9 >= account::MAX_GUID_CREATION_NUM;
         ensures exists(staker_address);
-
-        let store = global(staker_address);
-        let staking_contracts = store.staking_contracts;
-        aborts_if simple_map::spec_contains_key(staking_contracts, operator);
-
-        // verify create_stake_pool()
-        let seed_0 = bcs::to_bytes(staker_address);
-        let seed_1 = concat(concat(concat(seed_0, bcs::to_bytes(operator)), SALT), contract_creation_seed);
-        let resource_addr = account::spec_create_resource_address(staker_address, seed_1);
-        include CreateStakePoolAbortsIf {resource_addr};
-
-        // verify stake::add_stake_with_cap()
-        include StakeAddStakeWithCapAbortsIf{ pool_address: resource_addr };
-
+        // TODO: need to investigate the timeout
+        // let store = global(staker_address);
+        // let staking_contracts = store.staking_contracts;
+        // aborts_if simple_map::spec_contains_key(staking_contracts, operator);
+        //
+        // // verify create_stake_pool()
+        // let seed_0 = bcs::to_bytes(staker_address);
+        // let seed_1 = concat(concat(concat(seed_0, bcs::to_bytes(operator)), SALT), contract_creation_seed);
+        // let resource_addr = account::spec_create_resource_address(staker_address, seed_1);
+        // include CreateStakePoolAbortsIf {resource_addr};
+        //
+        // // verify stake::add_stake_with_cap()
+        // include StakeAddStakeWithCapAbortsIf{ pool_address: resource_addr };
+        //
         let post post_store = global(staker_address);
         let post post_staking_contracts = post_store.staking_contracts;
         ensures simple_map::spec_contains_key(post_staking_contracts, operator);
-        ensures amount != 0 ==> simple_map::spec_contains_key(post_staking_contracts, operator);
     }
 
     spec schema StakeAddStakeWithCapAbortsIf {