From 774b43dd885592fa144eb52d25a81f9b939b4b2a Mon Sep 17 00:00:00 2001 From: Zorrot Chen Date: Mon, 21 Aug 2023 00:40:24 +0800 Subject: [PATCH] [Spec] update spec for vesting.move (#9115) * new vesting * new vesting * init * fix comment * fix md * add comment * add head * add func total_accumulated_rewards time * rm boogie * fixed timeout * close timeout function's verification * rust lint fix * del head --------- Co-authored-by: chan-bing --- .../framework/aptos-framework/doc/vesting.md | 284 +++++++++++++++--- .../aptos-framework/sources/vesting.spec.move | 237 +++++++++++++-- 2 files changed, 453 insertions(+), 68 deletions(-) diff --git a/aptos-move/framework/aptos-framework/doc/vesting.md b/aptos-move/framework/aptos-framework/doc/vesting.md index c96f22981224e..ddff724ef6d07 100644 --- a/aptos-move/framework/aptos-framework/doc/vesting.md +++ b/aptos-move/framework/aptos-framework/doc/vesting.md @@ -2899,27 +2899,41 @@ This address should be deterministic for the same admin and vesting contract cre -
pragma verify = false;
-include ActiveVestingContractAbortsIf<VestingContract>{contract_address: vesting_contract_address};
-let vesting_contract = global<VestingContract>(vesting_contract_address);
-let staker = vesting_contract_address;
-let operator = vesting_contract.staking.operator;
-let staking_contracts = global<staking_contract::Store>(staker).staking_contracts;
-let staking_contract = simple_map::spec_get(staking_contracts, operator);
-aborts_if !exists<staking_contract::Store>(staker);
-aborts_if !simple_map::spec_contains_key(staking_contracts, operator);
-let pool_address = staking_contract.pool_address;
-let stake_pool = borrow_global<stake::StakePool>(pool_address);
-let active = coin::value(stake_pool.active);
-let pending_active = coin::value(stake_pool.pending_active);
-let total_active_stake = active + pending_active;
-let accumulated_rewards = total_active_stake - staking_contract.principal;
-let commission_amount = accumulated_rewards * staking_contract.commission_percentage / 100;
-aborts_if !exists<stake::StakePool>(pool_address);
-aborts_if active + pending_active > MAX_U64;
-aborts_if total_active_stake < staking_contract.principal;
-aborts_if accumulated_rewards * staking_contract.commission_percentage > MAX_U64;
-aborts_if (vesting_contract.remaining_grant + commission_amount) > total_active_stake;
+
pragma verify_duration_estimate = 300;
+include TotalAccumulatedRewardsAbortsIf;
+

+
+
+
+
+
+
+
+
schema TotalAccumulatedRewardsAbortsIf {
+    vesting_contract_address: address;
+    requires staking_contract.commission_percentage >= 0 && staking_contract.commission_percentage <= 100;
+    include ActiveVestingContractAbortsIf<VestingContract>{contract_address: vesting_contract_address};
+    let vesting_contract = global<VestingContract>(vesting_contract_address);
+    let staker = vesting_contract_address;
+    let operator = vesting_contract.staking.operator;
+    let staking_contracts = global<staking_contract::Store>(staker).staking_contracts;
+    let staking_contract = simple_map::spec_get(staking_contracts, operator);
+    aborts_if !exists<staking_contract::Store>(staker);
+    aborts_if !simple_map::spec_contains_key(staking_contracts, operator);
+    let pool_address = staking_contract.pool_address;
+    let stake_pool = global<stake::StakePool>(pool_address);
+    let active = coin::value(stake_pool.active);
+    let pending_active = coin::value(stake_pool.pending_active);
+    let total_active_stake = active + pending_active;
+    let accumulated_rewards = total_active_stake - staking_contract.principal;
+    let commission_amount = accumulated_rewards * staking_contract.commission_percentage / 100;
+    aborts_if !exists<stake::StakePool>(pool_address);
+    aborts_if active + pending_active > MAX_U64;
+    aborts_if total_active_stake < staking_contract.principal;
+    aborts_if accumulated_rewards * staking_contract.commission_percentage > MAX_U64;
+    aborts_if (vesting_contract.remaining_grant + commission_amount) > total_active_stake;
+    aborts_if total_active_stake < vesting_contract.remaining_grant;
+}
 

 
 
@@ -2937,6 +2951,26 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
pragma verify = false;
+pragma verify_duration_estimate = 1000;
+include TotalAccumulatedRewardsAbortsIf;
+let vesting_contract = global<VestingContract>(vesting_contract_address);
+let operator = vesting_contract.staking.operator;
+let staking_contracts = global<staking_contract::Store>(vesting_contract_address).staking_contracts;
+let staking_contract = simple_map::spec_get(staking_contracts, operator);
+let pool_address = staking_contract.pool_address;
+let stake_pool = global<stake::StakePool>(pool_address);
+let active = coin::value(stake_pool.active);
+let pending_active = coin::value(stake_pool.pending_active);
+let total_active_stake = active + pending_active;
+let accumulated_rewards = total_active_stake - staking_contract.principal;
+let commission_amount = accumulated_rewards * staking_contract.commission_percentage / 100;
+let total_accumulated_rewards = total_active_stake - vesting_contract.remaining_grant - commission_amount;
+let shareholder = spec_shareholder(vesting_contract_address, shareholder_or_beneficiary);
+let pool = vesting_contract.grant_pool;
+let shares = pool_u64::spec_shares(pool, shareholder);
+aborts_if pool.total_coins > 0 && pool.total_shares > 0
+    && (shares * total_accumulated_rewards) / pool.total_shares > MAX_U64;
+ensures result == pool_u64::spec_shares_to_amount_with_total_coins(pool, shares, total_accumulated_rewards);
 

 
 
@@ -2958,6 +2992,15 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
+
+
+
+
+
fun spec_shareholder(vesting_contract_address: address, shareholder_or_beneficiary: address): address;
+

+
+
+
 
 
 ### Function `shareholder`
@@ -2970,7 +3013,9 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
-
include ActiveVestingContractAbortsIf<VestingContract>{contract_address: vesting_contract_address};
+
pragma opaque;
+include ActiveVestingContractAbortsIf<VestingContract>{contract_address: vesting_contract_address};
+ensures [abstract] result == spec_shareholder(vesting_contract_address, shareholder_or_beneficiary);
 

 
 
@@ -3006,6 +3051,11 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
pragma verify = false;
+aborts_if withdrawal_address == @aptos_framework || withdrawal_address == @vm_reserved;
+aborts_if !exists<account::Account>(withdrawal_address);
+aborts_if !exists<coin::CoinStore<AptosCoin>>(withdrawal_address);
+aborts_if len(shareholders) == 0;
+aborts_if simple_map::spec_len(buy_ins) != len(shareholders);
 

 
 
@@ -3022,6 +3072,32 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
pragma verify = false;
+include UnlockRewardsAbortsIf;
+

+
+
+
+
+
+
+
+
schema UnlockRewardsAbortsIf {
+    contract_address: address;
+    include TotalAccumulatedRewardsAbortsIf { vesting_contract_address: contract_address };
+    let vesting_contract = global<VestingContract>(contract_address);
+    let operator = vesting_contract.staking.operator;
+    let staking_contracts = global<staking_contract::Store>(contract_address).staking_contracts;
+    let staking_contract = simple_map::spec_get(staking_contracts, operator);
+    let pool_address = staking_contract.pool_address;
+    let stake_pool = global<stake::StakePool>(pool_address);
+    let active = coin::value(stake_pool.active);
+    let pending_active = coin::value(stake_pool.pending_active);
+    let total_active_stake = active + pending_active;
+    let accumulated_rewards = total_active_stake - staking_contract.principal;
+    let commission_amount = accumulated_rewards * staking_contract.commission_percentage / 100;
+    let amount = total_active_stake - vesting_contract.remaining_grant - commission_amount;
+    include UnlockStakeAbortsIf { vesting_contract, amount };
+}
 

 
 
@@ -3038,6 +3114,8 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
pragma verify = false;
+aborts_if len(contract_addresses) == 0;
+include PreconditionAbortsIf;
 

 
 
@@ -3054,6 +3132,7 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
pragma verify = false;
+include UnlockRewardsAbortsIf;
 

 
 
@@ -3070,6 +3149,21 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
pragma verify = false;
+aborts_if len(contract_addresses) == 0;
+include PreconditionAbortsIf;
+

+
+
+
+
+
+
+
+
schema PreconditionAbortsIf {
+    contract_addresses: vector<address>;
+    requires forall i in 0..len(contract_addresses): simple_map::spec_get(global<staking_contract::Store>(contract_addresses[i]).staking_contracts, global<VestingContract>(contract_addresses[i]).staking.operator).commission_percentage >= 0
+        && simple_map::spec_get(global<staking_contract::Store>(contract_addresses[i]).staking_contracts, global<VestingContract>(contract_addresses[i]).staking.operator).commission_percentage <= 100;
+}
 

 
 
@@ -3086,6 +3180,9 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
pragma verify = false;
+include ActiveVestingContractAbortsIf<VestingContract>;
+let vesting_contract = global<VestingContract>(contract_address);
+include WithdrawStakeAbortsIf { vesting_contract };
 

 
 
@@ -3102,6 +3199,7 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
pragma verify = false;
+aborts_if len(contract_addresses) == 0;
 

 
 
@@ -3118,6 +3216,9 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
pragma verify = false;
+include ActiveVestingContractAbortsIf<VestingContract>;
+let vesting_contract = global<VestingContract>(contract_address);
+include WithdrawStakeAbortsIf { vesting_contract };
 

 
 
@@ -3133,10 +3234,11 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
-
pragma aborts_if_is_partial;
-include VerifyAdminAbortsIf;
+
pragma verify = false;
 let vesting_contract = global<VestingContract>(contract_address);
 aborts_if vesting_contract.state != VESTING_POOL_TERMINATED;
+include VerifyAdminAbortsIf;
+include WithdrawStakeAbortsIf { vesting_contract };
 

 
 
@@ -3152,8 +3254,17 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
-
pragma aborts_if_is_partial;
+
pragma verify = false;
 include VerifyAdminAbortsIf;
+let vesting_contract = global<VestingContract>(contract_address);
+let acc = vesting_contract.signer_cap.account;
+let old_operator = vesting_contract.staking.operator;
+include staking_contract::ContractExistsAbortsIf { staker: acc, operator: old_operator };
+let store = global<staking_contract::Store>(acc);
+let staking_contracts = store.staking_contracts;
+aborts_if simple_map::spec_contains_key(staking_contracts, new_operator);
+let staking_contract = simple_map::spec_get(staking_contracts, old_operator);
+include DistributeInternalAbortsIf { staker: acc, operator: old_operator, staking_contract, distribute_events: store.distribute_events };
 

 
 
@@ -3205,14 +3316,17 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
-
pragma aborts_if_is_partial;
-aborts_if !exists<VestingContract>(contract_address);
-let vesting_contract1 = global<VestingContract>(contract_address);
-aborts_if signer::address_of(admin) != vesting_contract1.admin;
-let operator = vesting_contract1.staking.operator;
-let staker = vesting_contract1.signer_cap.account;
-include staking_contract::ContractExistsAbortsIf;
-include staking_contract::IncreaseLockupWithCapAbortsIf;
+
aborts_if !exists<VestingContract>(contract_address);
+let vesting_contract = global<VestingContract>(contract_address);
+aborts_if signer::address_of(admin) != vesting_contract.admin;
+let operator = vesting_contract.staking.operator;
+let staker = vesting_contract.signer_cap.account;
+include staking_contract::ContractExistsAbortsIf {staker, operator};
+include staking_contract::IncreaseLockupWithCapAbortsIf {staker, operator};
+let store = global<staking_contract::Store>(staker);
+let staking_contract = simple_map::spec_get(store.staking_contracts, operator);
+let pool_address = staking_contract.owner_cap.pool_address;
+aborts_if !exists<stake::StakePool>(vesting_contract.staking.pool_address);
 

 
 
@@ -3248,10 +3362,17 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
-
pragma aborts_if_is_partial;
-aborts_if !exists<VestingContract>(contract_address);
-let post vesting_contract = global<VestingContract>(contract_address);
-ensures !simple_map::spec_contains_key(vesting_contract.beneficiaries,shareholder);
+
aborts_if !exists<VestingContract>(contract_address);
+let addr = signer::address_of(account);
+let vesting_contract = global<VestingContract>(contract_address);
+aborts_if addr != vesting_contract.admin && !std::string::spec_internal_check_utf8(ROLE_BENEFICIARY_RESETTER);
+aborts_if addr != vesting_contract.admin && !exists<VestingAccountManagement>(contract_address);
+let roles = global<VestingAccountManagement>(contract_address).roles;
+let role = std::string::spec_utf8(ROLE_BENEFICIARY_RESETTER);
+aborts_if addr != vesting_contract.admin && !simple_map::spec_contains_key(roles, role);
+aborts_if addr != vesting_contract.admin && addr != simple_map::spec_get(roles, role);
+let post post_vesting_contract = global<VestingContract>(contract_address);
+ensures !simple_map::spec_contains_key(post_vesting_contract.beneficiaries,shareholder);
 

 
 
@@ -3361,21 +3482,29 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
-
pragma verify=false;
-pragma aborts_if_is_partial;
+
pragma verify_duration_estimate = 300;
 let admin_addr = signer::address_of(admin);
 let admin_store = global<AdminStore>(admin_addr);
 let seed = bcs::to_bytes(admin_addr);
 let nonce = bcs::to_bytes(admin_store.nonce);
-let first = concat(seed,nonce);
-let second = concat(first,VESTING_POOL_SALT);
-let end = concat(second,contract_creation_seed);
+let first = concat(seed, nonce);
+let second = concat(first, VESTING_POOL_SALT);
+let end = concat(second, contract_creation_seed);
 let resource_addr = account::spec_create_resource_address(admin_addr, end);
 aborts_if !exists<AdminStore>(admin_addr);
 aborts_if len(account::ZERO_AUTH_KEY) != 32;
 aborts_if admin_store.nonce + 1 > MAX_U64;
 let ea = account::exists_at(resource_addr);
 include if (ea) account::CreateResourceAccountAbortsIf else account::CreateAccountAbortsIf {addr: resource_addr};
+let acc = global<account::Account>(resource_addr);
+let post post_acc = global<account::Account>(resource_addr);
+aborts_if !exists<coin::CoinStore<AptosCoin>>(resource_addr) && !aptos_std::type_info::spec_is_struct<AptosCoin>();
+aborts_if !exists<coin::CoinStore<AptosCoin>>(resource_addr) && ea && acc.guid_creation_num + 2 > MAX_U64;
+aborts_if !exists<coin::CoinStore<AptosCoin>>(resource_addr) && ea && acc.guid_creation_num + 2 >= account::MAX_GUID_CREATION_NUM;
+ensures exists<account::Account>(resource_addr) && post_acc.authentication_key == account::ZERO_AUTH_KEY &&
+        exists<coin::CoinStore<AptosCoin>>(resource_addr);
+ensures signer::address_of(result_1) == resource_addr;
+ensures result_2.account == resource_addr;
 

 
 
@@ -3440,6 +3569,25 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
pragma verify = false;
+include UnlockStakeAbortsIf;
+

+
+
+
+
+
+
+
+
schema UnlockStakeAbortsIf {
+    vesting_contract: &VestingContract;
+    amount: u64;
+    let acc = vesting_contract.signer_cap.account;
+    let operator = vesting_contract.staking.operator;
+    include amount != 0 ==> staking_contract::ContractExistsAbortsIf { staker: acc, operator };
+    let store = global<staking_contract::Store>(acc);
+    let staking_contract = simple_map::spec_get(store.staking_contracts, operator);
+    include amount != 0 ==> DistributeInternalAbortsIf { staker: acc, operator, staking_contract, distribute_events: store.distribute_events };
+}
 

 
 
@@ -3456,6 +3604,58 @@ This address should be deterministic for the same admin and vesting contract cre
 
 
 
pragma verify = false;
+include WithdrawStakeAbortsIf;
+

+
+
+
+
+
+
+
+
schema WithdrawStakeAbortsIf {
+    vesting_contract: &VestingContract;
+    contract_address: address;
+    let operator = vesting_contract.staking.operator;
+    include staking_contract::ContractExistsAbortsIf { staker: contract_address, operator };
+    let store = global<staking_contract::Store>(contract_address);
+    let staking_contract = simple_map::spec_get(store.staking_contracts, operator);
+    include DistributeInternalAbortsIf { staker: contract_address, operator, staking_contract, distribute_events: store.distribute_events };
+}
+

+
+
+
+
+
+
+
+
schema DistributeInternalAbortsIf {
+    staker: address;
+    operator: address;
+    staking_contract: staking_contract::StakingContract;
+    distribute_events: EventHandle<staking_contract::DistributeEvent>;
+    let pool_address = staking_contract.pool_address;
+    aborts_if !exists<stake::StakePool>(pool_address);
+    let stake_pool = global<stake::StakePool>(pool_address);
+    let inactive = stake_pool.inactive.value;
+    let pending_inactive = stake_pool.pending_inactive.value;
+    aborts_if inactive + pending_inactive > MAX_U64;
+    let total_potential_withdrawable = inactive + pending_inactive;
+    let pool_address_1 = staking_contract.owner_cap.pool_address;
+    aborts_if !exists<stake::StakePool>(pool_address_1);
+    let stake_pool_1 = global<stake::StakePool>(pool_address_1);
+    aborts_if !exists<stake::ValidatorSet>(@aptos_framework);
+    let validator_set = global<stake::ValidatorSet>(@aptos_framework);
+    let inactive_state = !stake::spec_contains(validator_set.pending_active, pool_address_1)
+        && !stake::spec_contains(validator_set.active_validators, pool_address_1)
+        && !stake::spec_contains(validator_set.pending_inactive, pool_address_1);
+    let inactive_1 = stake_pool_1.inactive.value;
+    let pending_inactive_1 = stake_pool_1.pending_inactive.value;
+    let new_inactive_1 = inactive_1 + pending_inactive_1;
+    aborts_if inactive_state && timestamp::spec_now_seconds() >= stake_pool_1.locked_until_secs
+        && inactive_1 + pending_inactive_1 > MAX_U64;
+}
 

 
 
diff --git a/aptos-move/framework/aptos-framework/sources/vesting.spec.move b/aptos-move/framework/aptos-framework/sources/vesting.spec.move
index ad205948f494e..eaaf73c14f249 100644
--- a/aptos-move/framework/aptos-framework/sources/vesting.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/vesting.spec.move
@@ -45,8 +45,19 @@ spec aptos_framework::vesting {
     }
 
     spec total_accumulated_rewards(vesting_contract_address: address): u64 {
-        // TODO: Verification out of resources/timeout
-        pragma verify = false;
+        pragma verify_duration_estimate = 300;
+
+        include TotalAccumulatedRewardsAbortsIf;
+    }
+
+    spec schema TotalAccumulatedRewardsAbortsIf {
+        vesting_contract_address: address;
+
+        // Note: commission percentage should not be under 0 or higher than 100, cause it's a percentage number
+        // This requirement will solve the timeout issue of total_accumulated_rewards
+        // However, accumulated_rewards is still timeout
+        requires staking_contract.commission_percentage >= 0 && staking_contract.commission_percentage <= 100;
+
         include ActiveVestingContractAbortsIf{contract_address: vesting_contract_address};
         let vesting_contract = global(vesting_contract_address);
 
@@ -59,7 +70,7 @@ spec aptos_framework::vesting {
         aborts_if !simple_map::spec_contains_key(staking_contracts, operator);
 
         let pool_address = staking_contract.pool_address;
-        let stake_pool = borrow_global(pool_address);
+        let stake_pool = global(pool_address);
         let active = coin::value(stake_pool.active);
         let pending_active = coin::value(stake_pool.pending_active);
         let total_active_stake = active + pending_active;
@@ -69,20 +80,51 @@ spec aptos_framework::vesting {
         aborts_if active + pending_active > MAX_U64;
         aborts_if total_active_stake < staking_contract.principal;
         aborts_if accumulated_rewards * staking_contract.commission_percentage > MAX_U64;
+        // This two item both contribute to the timeout
         aborts_if (vesting_contract.remaining_grant + commission_amount) > total_active_stake;
+        aborts_if total_active_stake < vesting_contract.remaining_grant;
     }
 
     spec accumulated_rewards(vesting_contract_address: address, shareholder_or_beneficiary: address): u64 {
-        // TODO: Uses `total_accumulated_rewards` which is not verified.
+        // TODO: A severe timeout can not be resolved.
         pragma verify = false;
+        pragma verify_duration_estimate = 1000;
+
+        // This schema lead to timeout
+        include TotalAccumulatedRewardsAbortsIf;
+
+        let vesting_contract = global(vesting_contract_address);
+        let operator = vesting_contract.staking.operator;
+        let staking_contracts = global(vesting_contract_address).staking_contracts;
+        let staking_contract = simple_map::spec_get(staking_contracts, operator);
+        let pool_address = staking_contract.pool_address;
+        let stake_pool = global(pool_address);
+        let active = coin::value(stake_pool.active);
+        let pending_active = coin::value(stake_pool.pending_active);
+        let total_active_stake = active + pending_active;
+        let accumulated_rewards = total_active_stake - staking_contract.principal;
+        let commission_amount = accumulated_rewards * staking_contract.commission_percentage / 100;
+        let total_accumulated_rewards = total_active_stake - vesting_contract.remaining_grant - commission_amount;
+
+        let shareholder = spec_shareholder(vesting_contract_address, shareholder_or_beneficiary);
+        let pool = vesting_contract.grant_pool;
+        let shares = pool_u64::spec_shares(pool, shareholder);
+        aborts_if pool.total_coins > 0 && pool.total_shares > 0
+            && (shares * total_accumulated_rewards) / pool.total_shares > MAX_U64;
+
+        ensures result == pool_u64::spec_shares_to_amount_with_total_coins(pool, shares, total_accumulated_rewards);
     }
 
     spec shareholders(vesting_contract_address: address): vector
 {
         include ActiveVestingContractAbortsIf{contract_address: vesting_contract_address};
     }
 
+    spec fun spec_shareholder(vesting_contract_address: address, shareholder_or_beneficiary: address): address;
+
     spec shareholder(vesting_contract_address: address, shareholder_or_beneficiary: address): address {
+        pragma opaque;
         include ActiveVestingContractAbortsIf{contract_address: vesting_contract_address};
+        ensures [abstract] result == spec_shareholder(vesting_contract_address, shareholder_or_beneficiary);
     }
 
     spec create_vesting_schedule(
@@ -99,49 +141,102 @@ spec aptos_framework::vesting {
     spec create_vesting_contract {
         // TODO: Data invariant does not hold.
         pragma verify = false;
+        aborts_if withdrawal_address == @aptos_framework || withdrawal_address == @vm_reserved;
+        aborts_if !exists(withdrawal_address);
+        aborts_if !exists>(withdrawal_address);
+        aborts_if len(shareholders) == 0;
+        aborts_if simple_map::spec_len(buy_ins) != len(shareholders);
     }
 
     spec unlock_rewards(contract_address: address) {
         // TODO: Calls `unlock_stake` which is not verified.
+        // Current verification times out.
         pragma verify = false;
+        include UnlockRewardsAbortsIf;
+    }
+
+    spec schema UnlockRewardsAbortsIf {
+        contract_address: address;
+
+        // Cause timeout here
+        include TotalAccumulatedRewardsAbortsIf { vesting_contract_address: contract_address };
+
+        let vesting_contract = global(contract_address);
+        let operator = vesting_contract.staking.operator;
+        let staking_contracts = global(contract_address).staking_contracts;
+        let staking_contract = simple_map::spec_get(staking_contracts, operator);
+        let pool_address = staking_contract.pool_address;
+        let stake_pool = global(pool_address);
+        let active = coin::value(stake_pool.active);
+        let pending_active = coin::value(stake_pool.pending_active);
+        let total_active_stake = active + pending_active;
+        let accumulated_rewards = total_active_stake - staking_contract.principal;
+        let commission_amount = accumulated_rewards * staking_contract.commission_percentage / 100;
+        let amount = total_active_stake - vesting_contract.remaining_grant - commission_amount;
+
+        include UnlockStakeAbortsIf { vesting_contract, amount };
     }
 
     spec unlock_rewards_many(contract_addresses: vector
) {
         // TODO: Calls `unlock_rewards` in loop.
         pragma verify = false;
+        aborts_if len(contract_addresses) == 0;
+        include PreconditionAbortsIf;
     }
 
     spec vest(contract_address: address) {
         // TODO: Calls `staking_contract::distribute` which is not verified.
         pragma verify = false;
+        include UnlockRewardsAbortsIf;
     }
 
     spec vest_many(contract_addresses: vector
) {
         // TODO: Calls `vest` in loop.
         pragma verify = false;
+        aborts_if len(contract_addresses) == 0;
+        include PreconditionAbortsIf;
+    }
+
+    spec schema PreconditionAbortsIf {
+        contract_addresses: vector
;
+
+        requires forall i in 0..len(contract_addresses): simple_map::spec_get(global(contract_addresses[i]).staking_contracts, global(contract_addresses[i]).staking.operator).commission_percentage >= 0
+            && simple_map::spec_get(global(contract_addresses[i]).staking_contracts, global(contract_addresses[i]).staking.operator).commission_percentage <= 100;
     }
 
     spec distribute(contract_address: address) {
         // TODO: Can't handle abort in loop.
         pragma verify = false;
+        include ActiveVestingContractAbortsIf;
+
+        let vesting_contract = global(contract_address);
+        include WithdrawStakeAbortsIf { vesting_contract };
     }
 
     spec distribute_many(contract_addresses: vector
) {
         // TODO: Calls `distribute` in loop.
         pragma verify = false;
+        aborts_if len(contract_addresses) == 0;
     }
 
     spec terminate_vesting_contract(admin: &signer, contract_address: address) {
         // TODO: Calls `staking_contract::distribute` which is not verified.
         pragma verify = false;
+        include ActiveVestingContractAbortsIf;
+
+        let vesting_contract = global(contract_address);
+        include WithdrawStakeAbortsIf { vesting_contract };
     }
 
     spec admin_withdraw(admin: &signer, contract_address: address) {
         // TODO: Calls `withdraw_stake` which is not verified.
-        pragma aborts_if_is_partial;
-        include VerifyAdminAbortsIf;
+        pragma verify = false;
+
         let vesting_contract = global(contract_address);
         aborts_if vesting_contract.state != VESTING_POOL_TERMINATED;
+
+        include VerifyAdminAbortsIf;
+        include WithdrawStakeAbortsIf { vesting_contract };
     }
 
     spec update_operator(
@@ -151,8 +246,20 @@ spec aptos_framework::vesting {
         commission_percentage: u64,
     ) {
         // TODO: Calls `staking_contract::switch_operator` which is not verified.
-        pragma aborts_if_is_partial;
+        pragma verify = false;
+
         include VerifyAdminAbortsIf;
+
+        let vesting_contract = global(contract_address);
+        let acc = vesting_contract.signer_cap.account;
+        let old_operator = vesting_contract.staking.operator;
+        include staking_contract::ContractExistsAbortsIf { staker: acc, operator: old_operator };
+        let store = global(acc);
+        let staking_contracts = store.staking_contracts;
+        aborts_if simple_map::spec_contains_key(staking_contracts, new_operator);
+
+        let staking_contract = simple_map::spec_get(staking_contracts, old_operator);
+        include DistributeInternalAbortsIf { staker: acc, operator: old_operator, staking_contract, distribute_events: store.distribute_events };
     }
 
     spec update_operator_with_same_commission(
@@ -181,17 +288,20 @@ spec aptos_framework::vesting {
         admin: &signer,
         contract_address: address,
     ) {
-        // TODO: Unable to handle abort from `stake::assert_stake_pool_exists`.
-        pragma aborts_if_is_partial;
         aborts_if !exists(contract_address);
-        let vesting_contract1 = global(contract_address);
-        aborts_if signer::address_of(admin) != vesting_contract1.admin;
+        let vesting_contract = global(contract_address);
+        aborts_if signer::address_of(admin) != vesting_contract.admin;
 
-        let operator = vesting_contract1.staking.operator;
-        let staker = vesting_contract1.signer_cap.account;
+        let operator = vesting_contract.staking.operator;
+        let staker = vesting_contract.signer_cap.account;
+
+        include staking_contract::ContractExistsAbortsIf {staker, operator};
+        include staking_contract::IncreaseLockupWithCapAbortsIf {staker, operator};
 
-        include staking_contract::ContractExistsAbortsIf;
-        include staking_contract::IncreaseLockupWithCapAbortsIf;
+        let store = global(staker);
+        let staking_contract = simple_map::spec_get(store.staking_contracts, operator);
+        let pool_address = staking_contract.owner_cap.pool_address;
+        aborts_if !exists(vesting_contract.staking.pool_address);
     }
 
     spec set_beneficiary(
@@ -212,11 +322,19 @@ spec aptos_framework::vesting {
         contract_address: address,
         shareholder: address,
     ) {
-        // TODO: The abort of functions on either side of a logical operator can not be handled.
-        pragma aborts_if_is_partial;
         aborts_if !exists(contract_address);
-        let post vesting_contract = global(contract_address);
-        ensures !simple_map::spec_contains_key(vesting_contract.beneficiaries,shareholder);
+
+        let addr = signer::address_of(account);
+        let vesting_contract = global(contract_address);
+        aborts_if addr != vesting_contract.admin && !std::string::spec_internal_check_utf8(ROLE_BENEFICIARY_RESETTER);
+        aborts_if addr != vesting_contract.admin && !exists(contract_address);
+        let roles = global(contract_address).roles;
+        let role = std::string::spec_utf8(ROLE_BENEFICIARY_RESETTER);
+        aborts_if addr != vesting_contract.admin && !simple_map::spec_contains_key(roles, role);
+        aborts_if addr != vesting_contract.admin && addr != simple_map::spec_get(roles, role);
+
+        let post post_vesting_contract = global(contract_address);
+        ensures !simple_map::spec_contains_key(post_vesting_contract.beneficiaries,shareholder);
     }
 
     spec set_management_role(
@@ -259,18 +377,15 @@ spec aptos_framework::vesting {
         admin: &signer,
         contract_creation_seed: vector,
     ): (signer, SignerCapability) {
-        // TODO: disabled due to timeout
-        pragma verify=false;
-        // TODO: Could not verify `coin::register` because can't get the `account_signer`.
-        pragma aborts_if_is_partial;
+        pragma verify_duration_estimate = 300;
         let admin_addr = signer::address_of(admin);
         let admin_store = global(admin_addr);
         let seed = bcs::to_bytes(admin_addr);
         let nonce = bcs::to_bytes(admin_store.nonce);
 
-        let first = concat(seed,nonce);
-        let second = concat(first,VESTING_POOL_SALT);
-        let end = concat(second,contract_creation_seed);
+        let first = concat(seed, nonce);
+        let second = concat(first, VESTING_POOL_SALT);
+        let end = concat(second, contract_creation_seed);
 
         let resource_addr = account::spec_create_resource_address(admin_addr, end);
         aborts_if !exists(admin_addr);
@@ -278,6 +393,16 @@ spec aptos_framework::vesting {
         aborts_if admin_store.nonce + 1 > MAX_U64;
         let ea = account::exists_at(resource_addr);
         include if (ea) account::CreateResourceAccountAbortsIf else account::CreateAccountAbortsIf {addr: resource_addr};
+
+        let acc = global(resource_addr);
+        let post post_acc = global(resource_addr);
+        aborts_if !exists>(resource_addr) && !aptos_std::type_info::spec_is_struct();
+        aborts_if !exists>(resource_addr) && ea && acc.guid_creation_num + 2 > MAX_U64;
+        aborts_if !exists>(resource_addr) && ea && acc.guid_creation_num + 2 >= account::MAX_GUID_CREATION_NUM;
+        ensures exists(resource_addr) && post_acc.authentication_key == account::ZERO_AUTH_KEY &&
+                exists>(resource_addr);
+        ensures signer::address_of(result_1) == resource_addr;
+        ensures result_2.account == resource_addr;
     }
 
     spec verify_admin(admin: &signer, vesting_contract: &VestingContract) {
@@ -295,11 +420,71 @@ spec aptos_framework::vesting {
     spec unlock_stake(vesting_contract: &VestingContract, amount: u64) {
         // TODO: Calls `staking_contract::unlock_stake` which is not verified.
         pragma verify = false;
+        include UnlockStakeAbortsIf;
+    }
+
+    spec schema UnlockStakeAbortsIf {
+        vesting_contract: &VestingContract;
+        amount: u64;
+
+        // verify staking_contract::unlock_stake()
+        let acc = vesting_contract.signer_cap.account;
+        let operator = vesting_contract.staking.operator;
+        include amount != 0 ==> staking_contract::ContractExistsAbortsIf { staker: acc, operator };
+
+        // verify staking_contract::distribute_internal()
+        let store = global(acc);
+        let staking_contract = simple_map::spec_get(store.staking_contracts, operator);
+        include amount != 0 ==> DistributeInternalAbortsIf { staker: acc, operator, staking_contract, distribute_events: store.distribute_events };
     }
 
     spec withdraw_stake(vesting_contract: &VestingContract, contract_address: address): Coin {
         // TODO: Calls `staking_contract::distribute` which is not verified.
         pragma verify = false;
+        include WithdrawStakeAbortsIf;
+    }
+
+    spec schema WithdrawStakeAbortsIf {
+        vesting_contract: &VestingContract;
+        contract_address: address;
+
+        let operator = vesting_contract.staking.operator;
+        include staking_contract::ContractExistsAbortsIf { staker: contract_address, operator };
+
+        // verify staking_contract::distribute_internal()
+        let store = global(contract_address);
+        let staking_contract = simple_map::spec_get(store.staking_contracts, operator);
+        include DistributeInternalAbortsIf { staker: contract_address, operator, staking_contract, distribute_events: store.distribute_events };
+    }
+
+    spec schema DistributeInternalAbortsIf {
+        staker: address;    // The verification below does not contain the loop in staking_contract::update_distribution_pool().
+        operator: address;
+        staking_contract: staking_contract::StakingContract;
+        distribute_events: EventHandle;
+
+        let pool_address = staking_contract.pool_address;
+        aborts_if !exists(pool_address);
+        let stake_pool = global(pool_address);
+        let inactive = stake_pool.inactive.value;
+        let pending_inactive = stake_pool.pending_inactive.value;
+        aborts_if inactive + pending_inactive > MAX_U64;
+
+        // verify stake::withdraw_with_cap()
+        let total_potential_withdrawable = inactive + pending_inactive;
+        let pool_address_1 = staking_contract.owner_cap.pool_address;
+        aborts_if !exists(pool_address_1);
+        let stake_pool_1 = global(pool_address_1);
+        aborts_if !exists(@aptos_framework);
+        let validator_set = global(@aptos_framework);
+        let inactive_state = !stake::spec_contains(validator_set.pending_active, pool_address_1)
+            && !stake::spec_contains(validator_set.active_validators, pool_address_1)
+            && !stake::spec_contains(validator_set.pending_inactive, pool_address_1);
+        let inactive_1 = stake_pool_1.inactive.value;
+        let pending_inactive_1 = stake_pool_1.pending_inactive.value;
+        let new_inactive_1 = inactive_1 + pending_inactive_1;
+        aborts_if inactive_state && timestamp::spec_now_seconds() >= stake_pool_1.locked_until_secs
+            && inactive_1 + pending_inactive_1 > MAX_U64;
     }
 
     spec get_beneficiary(contract: &VestingContract, shareholder: address): address {