From 4d98998a310093d5ee555a71ee97c67041a0f784 Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Wed, 3 Jul 2024 23:24:24 -0400 Subject: [PATCH 01/10] Don't verify committee_map --- .../supra-framework/sources/committee_map.spec.move | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 aptos-move/framework/supra-framework/sources/committee_map.spec.move diff --git a/aptos-move/framework/supra-framework/sources/committee_map.spec.move b/aptos-move/framework/supra-framework/sources/committee_map.spec.move new file mode 100644 index 0000000000000..55608c3566910 --- /dev/null +++ b/aptos-move/framework/supra-framework/sources/committee_map.spec.move @@ -0,0 +1,5 @@ +spec supra_framework::committee_map { + spec module { + pragma verify = false; + } +} From 18fb78f3e48dc50270d83897bf949e84b6468cce Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Thu, 4 Jul 2024 00:45:09 -0400 Subject: [PATCH 02/10] Add spec for initialization --- .../sources/delegation_pool.spec.move | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move index 4cfe89b4100b2..e9f97bd71df3a 100644 --- a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move +++ b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move @@ -93,4 +93,24 @@ spec supra_framework::delegation_pool { // TODO: verification disabled until this module is specified. pragma verify=false; } + + spec initialize_delegation_pool { + pragma verify = true; + include stake::ResourceRequirement; + /// No.1 Requirement: Every DelegationPool has only one corresponding StakePool stored at the same address. + /// a resource account is created from the "owner" signer to host the delegation pool resource and own the underlying stake pool + let owner_address = signer::address_of(owner); + let seed = spec_create_resource_account_seed(delegation_pool_creation_seed); + let resource_address = account::spec_create_resource_address(owner_address, seed); + ensures exists(owner_address); + ensures exists(resource_address); + // ensures exists(resource_address); + } + + spec fun spec_create_resource_account_seed( + delegation_pool_creation_seed: vector, + ): vector { + let seed = concat(MODULE_SALT, delegation_pool_creation_seed); + seed + } } From aab8f757d4e50b3b204d4e5d74091589b670808c Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Mon, 8 Jul 2024 22:01:29 -0400 Subject: [PATCH 03/10] Spec for create_resource_account_seed --- .../sources/delegation_pool.spec.move | 47 +++++++++++++++++-- 1 file changed, 42 insertions(+), 5 deletions(-) diff --git a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move index e9f97bd71df3a..2030617d3e16c 100644 --- a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move +++ b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move @@ -97,14 +97,22 @@ spec supra_framework::delegation_pool { spec initialize_delegation_pool { pragma verify = true; include stake::ResourceRequirement; - /// No.1 Requirement: Every DelegationPool has only one corresponding StakePool stored at the same address. - /// a resource account is created from the "owner" signer to host the delegation pool resource and own the underlying stake pool + /// [high-level-req-1] let owner_address = signer::address_of(owner); let seed = spec_create_resource_account_seed(delegation_pool_creation_seed); let resource_address = account::spec_create_resource_address(owner_address, seed); - ensures exists(owner_address); - ensures exists(resource_address); - // ensures exists(resource_address); + ensures exists(TRACE(owner_address)); + // ensures exists(resource_address); + // ensures exists(TRACE(resource_address)); + /// [high-level-req-2] + let signer_address = global(resource_address).stake_pool_signer_cap.account; + let pool_address_in_owner = global(TRACE(owner_address)).pool_address; + // ensures TRACE(signer_address) == TRACE(pool_address_in_owner); + } + + spec create_resource_account_seed { + pragma verify = true; + ensures result == spec_create_resource_account_seed(delegation_pool_creation_seed); } spec fun spec_create_resource_account_seed( @@ -113,4 +121,33 @@ spec supra_framework::delegation_pool { let seed = concat(MODULE_SALT, delegation_pool_creation_seed); seed } + + spec enable_partial_governance_voting { + let delegation_pool = borrow_global(pool_address); + } + + spec amount_to_shares_to_redeem { + /// return pool_u64::shares(shares_pool, shareholder) if coins_amount >= pool_u64::balance(shares_pool, shareholder) + /// else return pool_u64::amount_to_shares(shares_pool, coins_amount) + pragma verify = true; + // pragma opaque; + // ensures coins_amount >= pool_u64::balance(shares_pool, shareholder) ==> + // result == pool_u64::shares(shares_pool, shareholder); + // ensures coins_amount < pool_u64::balance(shares_pool, shareholder) ==> + // result == pool_u64::amount_to_shares(shares_pool, coins_amount); + } + + spec coins_to_redeem_to_ensure_min_stake { + pragma verify = true; + // let src_balance = pool_u64::balance(src_shares_pool, shareholder); + // let redeemed_coins = pool_u64::shares_to_amount( + // src_shares_pool, + // amount_to_shares_to_redeem(src_shares_pool, shareholder, amount) + // ); + // ensures src_balance - redeemed_coins < MIN_COINS_ON_SHARES_POOL ==> result == src_balance; + } + + spec coins_to_transfer_to_ensure_min_stake { + + } } From 2babdd961ca79999de2a5e033236a9ae4b49125b Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Mon, 8 Jul 2024 22:16:00 -0400 Subject: [PATCH 04/10] Spec for `get_used_voting_power` --- .../sources/delegation_pool.spec.move | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move index 2030617d3e16c..07f7853213f51 100644 --- a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move +++ b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move @@ -110,6 +110,18 @@ spec supra_framework::delegation_pool { // ensures TRACE(signer_address) == TRACE(pool_address_in_owner); } + spec get_used_voting_power { + pragma verify = true; + pragma opaque; + let votes = governance_records.votes; + let key = VotingRecordKey { + voter, + proposal_id, + }; + ensures smart_table::spec_contains(votes, key) ==> result == smart_table::spec_get(votes, key) + && (!smart_table::spec_contains(votes, key)) ==> result == 0; + } + spec create_resource_account_seed { pragma verify = true; ensures result == spec_create_resource_account_seed(delegation_pool_creation_seed); @@ -150,4 +162,8 @@ spec supra_framework::delegation_pool { spec coins_to_transfer_to_ensure_min_stake { } + + spec update_governanace_records_for_redeem_pending_inactive_shares { + + } } From 1235516d67e55b40d120c5ccf76ed7af67199e88 Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Mon, 8 Jul 2024 22:22:07 -0400 Subject: [PATCH 05/10] Spec for `pending_inactive_shares_pool` --- .../supra-framework/sources/delegation_pool.spec.move | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move index 07f7853213f51..c94ecd4046dd9 100644 --- a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move +++ b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move @@ -159,6 +159,13 @@ spec supra_framework::delegation_pool { // ensures src_balance - redeemed_coins < MIN_COINS_ON_SHARES_POOL ==> result == src_balance; } + spec pending_inactive_shares_pool { + pragma verify = true; + pragma opaque; + /// ensure the result is equal to the pending_inactive_shares_pool of the pool in the current lockup cycle + ensures result == table::spec_get(pool.inactive_shares, pool.observed_lockup_cycle); + } + spec coins_to_transfer_to_ensure_min_stake { } From 1d41940ac21bf3c9492f6f7cc910f1525c54a2bb Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Mon, 8 Jul 2024 22:23:53 -0400 Subject: [PATCH 06/10] Spec for `pending_inactive_shares_pool_mut` --- .../supra-framework/sources/delegation_pool.spec.move | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move index c94ecd4046dd9..c1f197c0b1ba7 100644 --- a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move +++ b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move @@ -159,6 +159,13 @@ spec supra_framework::delegation_pool { // ensures src_balance - redeemed_coins < MIN_COINS_ON_SHARES_POOL ==> result == src_balance; } + spec pending_inactive_shares_pool_mut { + pragma verify = true; + pragma opaque; + /// ensure the result is equal to the pending_inactive_shares_pool of the pool in the current lockup cycle + ensures result == table::spec_get(pool.inactive_shares, pool.observed_lockup_cycle); + } + spec pending_inactive_shares_pool { pragma verify = true; pragma opaque; From 7566560866d217a7f39774f47fc36b30f56b764a Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Mon, 8 Jul 2024 22:43:05 -0400 Subject: [PATCH 07/10] Spec for `olc_with_index` --- .../supra-framework/sources/delegation_pool.spec.move | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move index c1f197c0b1ba7..1bd22ad23828a 100644 --- a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move +++ b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move @@ -173,6 +173,13 @@ spec supra_framework::delegation_pool { ensures result == table::spec_get(pool.inactive_shares, pool.observed_lockup_cycle); } + spec olc_with_index { + pragma verify = true; + pragma opaque; + /// ensure the result is equal to the observed lockup cycle with the given index + ensures result == ObservedLockupCycle{index}; + } + spec coins_to_transfer_to_ensure_min_stake { } From d240eb5b1f78263b2b02bdf855105b9ece52b41b Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Mon, 8 Jul 2024 23:33:18 -0400 Subject: [PATCH 08/10] Spec for `amount_to_shares_to_redeem` --- .../sources/delegation_pool.spec.move | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move index 1bd22ad23828a..a1ce1e4d39242 100644 --- a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move +++ b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move @@ -139,14 +139,16 @@ spec supra_framework::delegation_pool { } spec amount_to_shares_to_redeem { - /// return pool_u64::shares(shares_pool, shareholder) if coins_amount >= pool_u64::balance(shares_pool, shareholder) - /// else return pool_u64::amount_to_shares(shares_pool, coins_amount) pragma verify = true; - // pragma opaque; - // ensures coins_amount >= pool_u64::balance(shares_pool, shareholder) ==> - // result == pool_u64::shares(shares_pool, shareholder); - // ensures coins_amount < pool_u64::balance(shares_pool, shareholder) ==> - // result == pool_u64::amount_to_shares(shares_pool, coins_amount); + pragma opaque; + let num_shares = pool_u64::spec_shares(shares_pool, shareholder); + let total_coins = shares_pool.total_coins; + let balance = pool_u64::spec_shares_to_amount_with_total_coins(shares_pool, num_shares, total_coins); + let amount_to_share = pool_u64::spec_amount_to_shares_with_total_coins(shares_pool, coins_amount, total_coins); + /// ensures result is pool_u64::shares(shares_pool, shareholder) if coins_amount >= pool_u64::balance(shares_pool, shareholder) + /// else pool_u64::amount_to_shares(shares_pool, coins_amount) + ensures coins_amount >= balance ==> result == num_shares + && coins_amount < balance ==> result == amount_to_share; } spec coins_to_redeem_to_ensure_min_stake { From 4f69e960dff540fa8a78052c2681c5d09fcb089e Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Tue, 9 Jul 2024 23:26:16 -0400 Subject: [PATCH 09/10] Make `create_resource_account_seed` spec opaque --- .../framework/supra-framework/sources/delegation_pool.spec.move | 1 + 1 file changed, 1 insertion(+) diff --git a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move index a1ce1e4d39242..605e0175361d0 100644 --- a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move +++ b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move @@ -124,6 +124,7 @@ spec supra_framework::delegation_pool { spec create_resource_account_seed { pragma verify = true; + pragma opaque; ensures result == spec_create_resource_account_seed(delegation_pool_creation_seed); } From f4aba7d2f5a5951a7eac0213aad2ee234e547fe7 Mon Sep 17 00:00:00 2001 From: axiongsupra Date: Thu, 18 Jul 2024 22:27:35 -0400 Subject: [PATCH 10/10] Move the spec from normal delegation pool to pbo delegation pool --- .../sources/delegation_pool.spec.move | 97 ---------------- .../sources/pbo_delegation_pool.spec.move | 104 ++++++++++++++++++ 2 files changed, 104 insertions(+), 97 deletions(-) diff --git a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move index 605e0175361d0..4cfe89b4100b2 100644 --- a/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move +++ b/aptos-move/framework/supra-framework/sources/delegation_pool.spec.move @@ -93,101 +93,4 @@ spec supra_framework::delegation_pool { // TODO: verification disabled until this module is specified. pragma verify=false; } - - spec initialize_delegation_pool { - pragma verify = true; - include stake::ResourceRequirement; - /// [high-level-req-1] - let owner_address = signer::address_of(owner); - let seed = spec_create_resource_account_seed(delegation_pool_creation_seed); - let resource_address = account::spec_create_resource_address(owner_address, seed); - ensures exists(TRACE(owner_address)); - // ensures exists(resource_address); - // ensures exists(TRACE(resource_address)); - /// [high-level-req-2] - let signer_address = global(resource_address).stake_pool_signer_cap.account; - let pool_address_in_owner = global(TRACE(owner_address)).pool_address; - // ensures TRACE(signer_address) == TRACE(pool_address_in_owner); - } - - spec get_used_voting_power { - pragma verify = true; - pragma opaque; - let votes = governance_records.votes; - let key = VotingRecordKey { - voter, - proposal_id, - }; - ensures smart_table::spec_contains(votes, key) ==> result == smart_table::spec_get(votes, key) - && (!smart_table::spec_contains(votes, key)) ==> result == 0; - } - - spec create_resource_account_seed { - pragma verify = true; - pragma opaque; - ensures result == spec_create_resource_account_seed(delegation_pool_creation_seed); - } - - spec fun spec_create_resource_account_seed( - delegation_pool_creation_seed: vector, - ): vector { - let seed = concat(MODULE_SALT, delegation_pool_creation_seed); - seed - } - - spec enable_partial_governance_voting { - let delegation_pool = borrow_global(pool_address); - } - - spec amount_to_shares_to_redeem { - pragma verify = true; - pragma opaque; - let num_shares = pool_u64::spec_shares(shares_pool, shareholder); - let total_coins = shares_pool.total_coins; - let balance = pool_u64::spec_shares_to_amount_with_total_coins(shares_pool, num_shares, total_coins); - let amount_to_share = pool_u64::spec_amount_to_shares_with_total_coins(shares_pool, coins_amount, total_coins); - /// ensures result is pool_u64::shares(shares_pool, shareholder) if coins_amount >= pool_u64::balance(shares_pool, shareholder) - /// else pool_u64::amount_to_shares(shares_pool, coins_amount) - ensures coins_amount >= balance ==> result == num_shares - && coins_amount < balance ==> result == amount_to_share; - } - - spec coins_to_redeem_to_ensure_min_stake { - pragma verify = true; - // let src_balance = pool_u64::balance(src_shares_pool, shareholder); - // let redeemed_coins = pool_u64::shares_to_amount( - // src_shares_pool, - // amount_to_shares_to_redeem(src_shares_pool, shareholder, amount) - // ); - // ensures src_balance - redeemed_coins < MIN_COINS_ON_SHARES_POOL ==> result == src_balance; - } - - spec pending_inactive_shares_pool_mut { - pragma verify = true; - pragma opaque; - /// ensure the result is equal to the pending_inactive_shares_pool of the pool in the current lockup cycle - ensures result == table::spec_get(pool.inactive_shares, pool.observed_lockup_cycle); - } - - spec pending_inactive_shares_pool { - pragma verify = true; - pragma opaque; - /// ensure the result is equal to the pending_inactive_shares_pool of the pool in the current lockup cycle - ensures result == table::spec_get(pool.inactive_shares, pool.observed_lockup_cycle); - } - - spec olc_with_index { - pragma verify = true; - pragma opaque; - /// ensure the result is equal to the observed lockup cycle with the given index - ensures result == ObservedLockupCycle{index}; - } - - spec coins_to_transfer_to_ensure_min_stake { - - } - - spec update_governanace_records_for_redeem_pending_inactive_shares { - - } } diff --git a/aptos-move/framework/supra-framework/sources/pbo_delegation_pool.spec.move b/aptos-move/framework/supra-framework/sources/pbo_delegation_pool.spec.move index c582e62fd71d3..7d0ab0fb8cabd 100644 --- a/aptos-move/framework/supra-framework/sources/pbo_delegation_pool.spec.move +++ b/aptos-move/framework/supra-framework/sources/pbo_delegation_pool.spec.move @@ -93,4 +93,108 @@ spec supra_framework::pbo_delegation_pool { // TODO: verification disabled until this module is specified. pragma verify = false; } + + spec initialize_delegation_pool { + pragma verify = true; + include stake::ResourceRequirement; + /// [high-level-req-1] + let owner_address = signer::address_of(owner); + let seed = spec_create_resource_account_seed(delegation_pool_creation_seed); + let resource_address = account::spec_create_resource_address(owner_address, seed); + ensures exists(TRACE(owner_address)); + // ensures exists(resource_address); + // ensures exists(TRACE(resource_address)); + /// [high-level-req-2] + let signer_address = global(resource_address).stake_pool_signer_cap.account; + let pool_address_in_owner = global(TRACE(owner_address)).pool_address; + // ensures TRACE(signer_address) == TRACE(pool_address_in_owner); + } + + spec get_used_voting_power { + pragma verify = true; + pragma opaque; + let votes = governance_records.votes; + let key = VotingRecordKey { + voter, + proposal_id, + }; + ensures smart_table::spec_contains(votes, key) ==> result == smart_table::spec_get(votes, key) + && (!smart_table::spec_contains(votes, key)) ==> result == 0; + } + + spec create_resource_account_seed { + pragma verify = true; + pragma opaque; + ensures result == spec_create_resource_account_seed(delegation_pool_creation_seed); + } + + spec fun spec_create_resource_account_seed( + delegation_pool_creation_seed: vector, + ): vector { + let seed = concat(MODULE_SALT, delegation_pool_creation_seed); + seed + } + + spec enable_partial_governance_voting { + let delegation_pool = borrow_global(pool_address); + } + + spec amount_to_shares_to_redeem { + pragma verify = true; + pragma opaque; + let num_shares = pool_u64::spec_shares(shares_pool, shareholder); + let total_coins = shares_pool.total_coins; + let balance = pool_u64::spec_shares_to_amount_with_total_coins(shares_pool, num_shares, total_coins); + let amount_to_share = pool_u64::spec_amount_to_shares_with_total_coins(shares_pool, coins_amount, total_coins); + /// ensures result is pool_u64::shares(shares_pool, shareholder) if coins_amount >= pool_u64::balance(shares_pool, shareholder) + /// else pool_u64::amount_to_shares(shares_pool, coins_amount) + ensures coins_amount >= balance ==> result == num_shares + && coins_amount < balance ==> result == amount_to_share; + } + + spec coins_to_redeem_to_ensure_min_stake { + pragma verify = true; + // let src_balance = pool_u64::balance(src_shares_pool, shareholder); + // let redeemed_coins = pool_u64::shares_to_amount( + // src_shares_pool, + // amount_to_shares_to_redeem(src_shares_pool, shareholder, amount) + // ); + // ensures src_balance - redeemed_coins < MIN_COINS_ON_SHARES_POOL ==> result == src_balance; + } + + spec pending_inactive_shares_pool_mut { + pragma verify = true; + pragma opaque; + /// ensure the result is equal to the pending_inactive_shares_pool of the pool in the current lockup cycle + ensures result == table::spec_get(pool.inactive_shares, pool.observed_lockup_cycle); + } + + spec pending_inactive_shares_pool { + pragma verify = true; + pragma opaque; + /// ensure the result is equal to the pending_inactive_shares_pool of the pool in the current lockup cycle + ensures result == table::spec_get(pool.inactive_shares, pool.observed_lockup_cycle); + } + + spec olc_with_index { + pragma verify = true; + pragma opaque; + /// ensure the result is equal to the observed lockup cycle with the given index + ensures result == ObservedLockupCycle{index}; + } + + spec coins_to_transfer_to_ensure_min_stake { + + } + + spec update_governanace_records_for_redeem_pending_inactive_shares { + + } + + spec buy_in_active_shares { + pragma verify = true; + let new_shares = pool_u64::amount_to_shares(pool.active_shares, coins_amount); + + ensures new_shares == 0 ==> result == 0; + } }