Skip to content

Commit

Permalink
staking_contract spec
Browse files Browse the repository at this point in the history
  • Loading branch information
@rahxephon89
rahxephon89 committed Sep 27, 2023
1 parent 92fbdcb commit 84a5691
Show file tree
Hide file tree
Showing 2 changed files with 18 additions and 27 deletions.
12 changes: 2 additions & 10 deletions aptos-move/framework/aptos-framework/doc/staking_contract.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.


<pre><code><b>pragma</b> verify = <b>false</b>;
<pre><code><b>pragma</b> verify_duration_estimate = 120;
<b>pragma</b> aborts_if_is_partial;
<b>include</b> <a href="staking_contract.md#0x1_staking_contract_PreconditionsInCreateContract">PreconditionsInCreateContract</a>;
<b>let</b> amount = coins.value;
<b>include</b> <a href="staking_contract.md#0x1_staking_contract_Create_Staking_Contract_With_Coins_Abortsif">Create_Staking_Contract_With_Coins_Abortsif</a> { amount };
Expand Down Expand Up @@ -2657,18 +2658,9 @@ a staking_contract exists for the staker/operator pair.
<b>aborts_if</b> !<b>exists</b>&lt;<a href="staking_contract.md#0x1_staking_contract_Store">Store</a>&gt;(staker_address) && !<b>exists</b>&lt;<a href="account.md#0x1_account_Account">account::Account</a>&gt;(staker_address);
<b>aborts_if</b> !<b>exists</b>&lt;<a href="staking_contract.md#0x1_staking_contract_Store">Store</a>&gt;(staker_address) && <a href="account.md#0x1_account">account</a>.guid_creation_num + 9 &gt;= <a href="account.md#0x1_account_MAX_GUID_CREATION_NUM">account::MAX_GUID_CREATION_NUM</a>;
<b>ensures</b> <b>exists</b>&lt;<a href="staking_contract.md#0x1_staking_contract_Store">Store</a>&gt;(staker_address);
<b>let</b> store = <b>global</b>&lt;<a href="staking_contract.md#0x1_staking_contract_Store">Store</a>&gt;(staker_address);
<b>let</b> staking_contracts = store.staking_contracts;
<b>aborts_if</b> <a href="../../aptos-stdlib/doc/simple_map.md#0x1_simple_map_spec_contains_key">simple_map::spec_contains_key</a>(staking_contracts, operator);
<b>let</b> seed_0 = <a href="../../aptos-stdlib/../move-stdlib/doc/bcs.md#0x1_bcs_to_bytes">bcs::to_bytes</a>(staker_address);
<b>let</b> seed_1 = concat(concat(concat(seed_0, <a href="../../aptos-stdlib/../move-stdlib/doc/bcs.md#0x1_bcs_to_bytes">bcs::to_bytes</a>(operator)), <a href="staking_contract.md#0x1_staking_contract_SALT">SALT</a>), contract_creation_seed);
<b>let</b> resource_addr = <a href="account.md#0x1_account_spec_create_resource_address">account::spec_create_resource_address</a>(staker_address, seed_1);
<b>include</b> <a href="staking_contract.md#0x1_staking_contract_CreateStakePoolAbortsIf">CreateStakePoolAbortsIf</a> {resource_addr};
<b>include</b> <a href="staking_contract.md#0x1_staking_contract_StakeAddStakeWithCapAbortsIf">StakeAddStakeWithCapAbortsIf</a>{ pool_address: resource_addr };
<b>let</b> <b>post</b> post_store = <b>global</b>&lt;<a href="staking_contract.md#0x1_staking_contract_Store">Store</a>&gt;(staker_address);
<b>let</b> <b>post</b> post_staking_contracts = post_store.staking_contracts;
<b>ensures</b> <a href="../../aptos-stdlib/doc/simple_map.md#0x1_simple_map_spec_contains_key">simple_map::spec_contains_key</a>(post_staking_contracts, operator);
<b>ensures</b> amount != 0 ==&gt; <a href="../../aptos-stdlib/doc/simple_map.md#0x1_simple_map_spec_contains_key">simple_map::spec_contains_key</a>(post_staking_contracts, operator);
}
</code></pre>

Expand Down
33 changes: 16 additions & 17 deletions aptos-move/framework/aptos-framework/sources/staking_contract.spec.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,8 +74,8 @@ spec aptos_framework::staking_contract {
commission_percentage: u64,
contract_creation_seed: vector<u8>,
): 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;
Expand Down Expand Up @@ -385,24 +385,23 @@ spec aptos_framework::staking_contract {
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);

// 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<Store>(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<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);
}

spec schema StakeAddStakeWithCapAbortsIf {
Expand Down

0 comments on commit 84a5691

Please sign in to comment.