From 84a5691a92f54d3a7c3e1e99c5873dccc3c2fff8 Mon Sep 17 00:00:00 2001 From: Teng Zhang Date: Mon, 25 Sep 2023 16:05:11 -0700 Subject: [PATCH] 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 {