fix spec

aptos-labs · Nov 18, 2024 · 881aa71 · 881aa71
1 parent f619e44
commit 881aa71
Show file tree

Hide file tree

Showing 8 changed files with 190 additions and 335 deletions.
diff --git a/aptos-move/framework/aptos-framework/doc/aptos_governance.md b/aptos-move/framework/aptos-framework/doc/aptos_governance.md
@@ -2156,6 +2156,7 @@ Limit addition overflow.
 
 <pre><code><b>let</b> addr = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(aptos_framework);
 <b>let</b> register_account = <b>global</b>&lt;<a href="account.md#0x1_account_Account">account::Account</a>&gt;(addr);
+<b>aborts_if</b> <a href="permissioned_signer.md#0x1_permissioned_signer_spec_is_permissioned_signer">permissioned_signer::spec_is_permissioned_signer</a>(aptos_framework);
 <b>aborts_if</b> <b>exists</b>&lt;<a href="voting.md#0x1_voting_VotingForum">voting::VotingForum</a>&lt;GovernanceProposal&gt;&gt;(addr);
 <b>aborts_if</b> !<b>exists</b>&lt;<a href="account.md#0x1_account_Account">account::Account</a>&gt;(addr);
 <b>aborts_if</b> register_account.guid_creation_num + 7 &gt; <a href="aptos_governance.md#0x1_aptos_governance_MAX_U64">MAX_U64</a>;

diff --git a/aptos-move/framework/aptos-framework/doc/stake.md b/aptos-move/framework/aptos-framework/doc/stake.md
diff --git a/aptos-move/framework/aptos-framework/doc/staking_proxy.md b/aptos-move/framework/aptos-framework/doc/staking_proxy.md
@@ -20,6 +20,7 @@
 -  [Specification](#@Specification_1)
     -  [High-level Requirements](#high-level-req)
     -  [Module-level Specification](#module-level-spec)
+    -  [Function `grant_permission`](#@Specification_1_grant_permission)
     -  [Function `set_operator`](#@Specification_1_set_operator)
     -  [Function `set_voter`](#@Specification_1_set_voter)
     -  [Function `set_vesting_contract_operator`](#@Specification_1_set_vesting_contract_operator)
@@ -436,6 +437,25 @@ Grant permission to mutate staking on behalf of the master signer.
 
 
 
+<a id="@Specification_1_grant_permission"></a>
+
+### Function `grant_permission`
+
+
+<pre><code><b>public</b> <b>fun</b> <a href="staking_proxy.md#0x1_staking_proxy_grant_permission">grant_permission</a>(master: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>, <a href="permissioned_signer.md#0x1_permissioned_signer">permissioned_signer</a>: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>)
+</code></pre>
+
+
+
+
+<pre><code><b>pragma</b> aborts_if_is_partial;
+<b>aborts_if</b> !<a href="permissioned_signer.md#0x1_permissioned_signer_spec_is_permissioned_signer">permissioned_signer::spec_is_permissioned_signer</a>(<a href="permissioned_signer.md#0x1_permissioned_signer">permissioned_signer</a>);
+<b>aborts_if</b> <a href="permissioned_signer.md#0x1_permissioned_signer_spec_is_permissioned_signer">permissioned_signer::spec_is_permissioned_signer</a>(master);
+<b>aborts_if</b> <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(master) != <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(<a href="permissioned_signer.md#0x1_permissioned_signer">permissioned_signer</a>);
+</code></pre>
+
+
+
 <a id="@Specification_1_set_operator"></a>
 
 ### Function `set_operator`
@@ -559,6 +579,12 @@ One of them are not exists
 
 
 <pre><code><b>include</b> <a href="staking_proxy.md#0x1_staking_proxy_SetStakePoolOperator">SetStakePoolOperator</a>;
+<b>include</b> <a href="staking_proxy.md#0x1_staking_proxy_AbortsIfSignerPermissionStakeProxy">AbortsIfSignerPermissionStakeProxy</a> {
+    s: owner
+};
+<b>include</b> <b>exists</b>&lt;<a href="stake.md#0x1_stake_StakePool">stake::StakePool</a>&gt;(<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(owner)) ==&gt; <a href="stake.md#0x1_stake_AbortsIfSignerPermissionStake">stake::AbortsIfSignerPermissionStake</a> {
+    s:owner
+};
 </code></pre>
 
 
@@ -570,7 +596,9 @@ One of them are not exists
 <pre><code><b>schema</b> <a href="staking_proxy.md#0x1_staking_proxy_SetStakePoolOperator">SetStakePoolOperator</a> {
     owner: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>;
     new_operator: <b>address</b>;
-    <b>aborts_if</b> <a href="permissioned_signer.md#0x1_permissioned_signer_spec_is_permissioned_signer">permissioned_signer::spec_is_permissioned_signer</a>(owner);
+    <b>include</b> <a href="staking_proxy.md#0x1_staking_proxy_AbortsIfSignerPermissionStakeProxy">AbortsIfSignerPermissionStakeProxy</a> {
+        s: owner
+    };
     <b>let</b> owner_address = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(owner);
     <b>let</b> ownership_cap = <b>borrow_global</b>&lt;<a href="stake.md#0x1_stake_OwnerCapability">stake::OwnerCapability</a>&gt;(owner_address);
     <b>let</b> pool_address = ownership_cap.pool_address;
@@ -609,6 +637,9 @@ One of them are not exists
 
 
 <pre><code><b>include</b> <a href="staking_proxy.md#0x1_staking_proxy_SetStakingContractVoter">SetStakingContractVoter</a>;
+<b>include</b> <a href="staking_proxy.md#0x1_staking_proxy_AbortsIfSignerPermissionStakeProxy">AbortsIfSignerPermissionStakeProxy</a> {
+    s: owner
+};
 </code></pre>
 
 
@@ -651,6 +682,12 @@ Then abort if the resource is not exist
 
 
 <pre><code><b>include</b> <a href="staking_proxy.md#0x1_staking_proxy_SetStakePoolVoterAbortsIf">SetStakePoolVoterAbortsIf</a>;
+<b>include</b> <a href="staking_proxy.md#0x1_staking_proxy_AbortsIfSignerPermissionStakeProxy">AbortsIfSignerPermissionStakeProxy</a> {
+    s: owner
+};
+<b>include</b> <b>exists</b>&lt;<a href="stake.md#0x1_stake_StakePool">stake::StakePool</a>&gt;(<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(owner)) ==&gt; <a href="stake.md#0x1_stake_AbortsIfSignerPermissionStake">stake::AbortsIfSignerPermissionStake</a> {
+    s:owner
+};
 </code></pre>
 
 
@@ -662,7 +699,9 @@ Then abort if the resource is not exist
 <pre><code><b>schema</b> <a href="staking_proxy.md#0x1_staking_proxy_SetStakePoolVoterAbortsIf">SetStakePoolVoterAbortsIf</a> {
     owner: &<a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>;
     new_voter: <b>address</b>;
-    <b>aborts_if</b> <a href="permissioned_signer.md#0x1_permissioned_signer_spec_is_permissioned_signer">permissioned_signer::spec_is_permissioned_signer</a>(owner);
+    <b>include</b> <a href="staking_proxy.md#0x1_staking_proxy_AbortsIfSignerPermissionStakeProxy">AbortsIfSignerPermissionStakeProxy</a> {
+        s: owner
+    };
     <b>let</b> owner_address = <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(owner);
     <b>let</b> ownership_cap = <b>global</b>&lt;<a href="stake.md#0x1_stake_OwnerCapability">stake::OwnerCapability</a>&gt;(owner_address);
     <b>let</b> pool_address = ownership_cap.pool_address;
@@ -672,4 +711,17 @@ Then abort if the resource is not exist
 </code></pre>
 
 
+
+
+<a id="0x1_staking_proxy_AbortsIfSignerPermissionStakeProxy"></a>
+
+
+<pre><code><b>schema</b> <a href="staking_proxy.md#0x1_staking_proxy_AbortsIfSignerPermissionStakeProxy">AbortsIfSignerPermissionStakeProxy</a> {
+    s: <a href="../../aptos-stdlib/../move-stdlib/doc/signer.md#0x1_signer">signer</a>;
+    <b>let</b> perm = <a href="staking_proxy.md#0x1_staking_proxy_StakeProxyPermission">StakeProxyPermission</a> {};
+    <b>aborts_if</b> !<a href="permissioned_signer.md#0x1_permissioned_signer_spec_check_permission_exists">permissioned_signer::spec_check_permission_exists</a>(s, perm);
+}
+</code></pre>
+
+
 [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
@@ -63,6 +63,7 @@ spec aptos_framework::aptos_governance {
         let addr = signer::address_of(aptos_framework);
         let register_account = global<account::Account>(addr);
 
+        aborts_if permissioned_signer::spec_is_permissioned_signer(aptos_framework);
         aborts_if exists<voting::VotingForum<GovernanceProposal>>(addr);
         aborts_if !exists<account::Account>(addr);
         aborts_if register_account.guid_creation_num + 7 > MAX_U64;

diff --git a/aptos-move/framework/aptos-framework/sources/stake.spec.move b/aptos-move/framework/aptos-framework/sources/stake.spec.move
@@ -125,6 +125,9 @@ spec aptos_framework::stake {
         network_addresses: vector<u8>,
         fullnode_addresses: vector<u8>,
     ){
+        include AbortsIfSignerPermissionStake {
+            s: account
+        };
         let pubkey_from_pop = bls12381::spec_public_key_from_bytes_with_pop(
             consensus_pubkey,
             proof_of_possession_from_bytes(proof_of_possession)
@@ -170,6 +173,9 @@ spec aptos_framework::stake {
         // This function casue timeout (property proved)
         pragma verify_duration_estimate = 60;
         pragma disable_invariants_in_body;
+        include AbortsIfSignerPermissionStake {
+            s: operator
+        };
         aborts_if !staking_config::get_allow_validator_set_change(staking_config::get());
         aborts_if !exists<StakePool>(pool_address);
         aborts_if !exists<ValidatorConfig>(pool_address);
@@ -223,6 +229,9 @@ spec aptos_framework::stake {
     {
         // TODO(fa_migration)
         pragma verify = false;
+        include AbortsIfSignerPermissionStake {
+            s: owner
+        };
         aborts_if reconfiguration_state::spec_is_in_progress();
         let addr = signer::address_of(owner);
         let ownership_cap = global<OwnerCapability>(addr);
@@ -262,6 +271,9 @@ spec aptos_framework::stake {
     ) {
         pragma disable_invariants_in_body;
         requires chain_status::is_operating();
+        include AbortsIfSignerPermissionStake {
+            s: operator
+        };
         aborts_if reconfiguration_state::spec_is_in_progress();
         let config = staking_config::get();
         aborts_if !staking_config::get_allow_validator_set_change(config);
@@ -297,13 +309,19 @@ spec aptos_framework::stake {
     spec extract_owner_cap(owner: &signer): OwnerCapability {
         // TODO: set because of timeout (property proved)
         pragma verify_duration_estimate = 300;
+        include AbortsIfSignerPermissionStake {
+            s: owner
+        };
         let owner_address = signer::address_of(owner);
         aborts_if !exists<OwnerCapability>(owner_address);
         ensures !exists<OwnerCapability>(owner_address);
     }
 
     spec deposit_owner_cap(owner: &signer, owner_cap: OwnerCapability) {
-        aborts_if permissioned_signer::spec_is_permissioned_signer(owner);
+        include AbortsIfSignerPermissionStake {
+            s: owner
+        };
+        // aborts_if permissioned_signer::spec_is_permissioned_signer(owner);
         let owner_address = signer::address_of(owner);
         aborts_if exists<OwnerCapability>(owner_address);
         ensures exists<OwnerCapability>(owner_address);
@@ -352,7 +370,10 @@ spec aptos_framework::stake {
         new_network_addresses: vector<u8>,
         new_fullnode_addresses: vector<u8>,
     ) {
-        aborts_if permissioned_signer::spec_is_permissioned_signer(operator);
+        include AbortsIfSignerPermissionStake {
+            s: operator
+        };
+        // aborts_if permissioned_signer::spec_is_permissioned_signer(operator);
         let pre_stake_pool = global<StakePool>(pool_address);
         let post validator_info = global<ValidatorConfig>(pool_address);
         modifies global<ValidatorConfig>(pool_address);
@@ -399,7 +420,10 @@ spec aptos_framework::stake {
         new_consensus_pubkey: vector<u8>,
         proof_of_possession: vector<u8>,
     ) {
-        aborts_if permissioned_signer::spec_is_permissioned_signer(operator);
+        include AbortsIfSignerPermissionStake {
+            s: operator
+        };
+        // aborts_if permissioned_signer::spec_is_permissioned_signer(operator);
         let pre_stake_pool = global<StakePool>(pool_address);
         let post validator_info = global<ValidatorConfig>(pool_address);
         aborts_if reconfiguration_state::spec_is_in_progress();
@@ -505,6 +529,13 @@ spec aptos_framework::stake {
         };
     }
 
+    spec schema AbortsIfSignerPermissionStake {
+        use aptos_framework::permissioned_signer;
+        s: signer;
+        let perm = StakePermission {};
+        aborts_if !permissioned_signer::spec_check_permission_exists(s, perm);
+    }
+
     spec schema UpdateStakePoolAbortsIf {
         use aptos_std::type_info;
 
@@ -593,6 +624,7 @@ spec aptos_framework::stake {
         pragma opaque;
         // TODO: set because of timeout (property proved)
         pragma verify_duration_estimate = 300;
+        pragma verify = false;
         requires rewards_rate <= MAX_REWARDS_RATE;
         requires rewards_rate_denominator > 0;
         requires rewards_rate <= rewards_rate_denominator;
@@ -670,18 +702,21 @@ spec aptos_framework::stake {
 
     spec add_stake_with_cap {
         pragma disable_invariants_in_body;
-        pragma verify_duration_estimate = 300;
+        pragma verify = false;
         include ResourceRequirement;
         let amount = coins.value;
         aborts_if reconfiguration_state::spec_is_in_progress();
         include AddStakeWithCapAbortsIfAndEnsures { amount };
     }
 
     spec add_stake {
-        // TODO: These function passed locally however failed in github CI
-        pragma verify_duration_estimate = 120;
+        // TODO: fix
+        pragma verify = false;
         // TODO(fa_migration)
         pragma aborts_if_is_partial;
+        include AbortsIfSignerPermissionStake {
+            s: owner
+        };
         aborts_if reconfiguration_state::spec_is_in_progress();
         include ResourceRequirement;
         include AddStakeAbortsIfAndEnsures;
@@ -695,7 +730,11 @@ spec aptos_framework::stake {
     ) {
         // TODO: These function failed in github CI
         pragma verify_duration_estimate = 120;
-
+        pragma verify = false;
+        pragma aborts_if_is_partial;
+        include AbortsIfSignerPermissionStake {
+            s: owner
+        };
         include ResourceRequirement;
         let addr = signer::address_of(owner);
         ensures global<ValidatorConfig>(addr) == ValidatorConfig {

diff --git a/aptos-move/framework/aptos-framework/sources/staking_proxy.spec.move b/aptos-move/framework/aptos-framework/sources/staking_proxy.spec.move
@@ -44,6 +44,13 @@ spec aptos_framework::staking_proxy {
         pragma aborts_if_is_strict;
     }
 
+    spec grant_permission {
+        pragma aborts_if_is_partial;
+        aborts_if !permissioned_signer::spec_is_permissioned_signer(permissioned_signer);
+        aborts_if permissioned_signer::spec_is_permissioned_signer(master);
+        aborts_if signer::address_of(master) != signer::address_of(permissioned_signer);
+    }
+
     /// Aborts if conditions of SetStakePoolOperator are not met
     spec set_operator(owner: &signer, old_operator: address, new_operator: address) {
         pragma verify = false;
@@ -122,6 +129,12 @@ spec aptos_framework::staking_proxy {
     /// One of them are not exists
     spec set_stake_pool_operator(owner: &signer, new_operator: address) {
         include SetStakePoolOperator;
+        include AbortsIfSignerPermissionStakeProxy {
+            s: owner
+        };
+        include exists<stake::StakePool>(signer::address_of(owner)) ==> stake::AbortsIfSignerPermissionStake {
+            s:owner
+        };
     }
 
     spec schema SetStakePoolOperator {
@@ -130,7 +143,9 @@ spec aptos_framework::staking_proxy {
         owner: &signer;
         new_operator: address;
 
-        aborts_if permissioned_signer::spec_is_permissioned_signer(owner);
+        include AbortsIfSignerPermissionStakeProxy {
+            s: owner
+        };
         let owner_address = signer::address_of(owner);
         let ownership_cap = borrow_global<stake::OwnerCapability>(owner_address);
         let pool_address = ownership_cap.pool_address;
@@ -140,6 +155,9 @@ spec aptos_framework::staking_proxy {
 
     spec set_staking_contract_voter(owner: &signer, operator: address, new_voter: address) {
         include SetStakingContractVoter;
+        include AbortsIfSignerPermissionStakeProxy {
+            s: owner
+        };
     }
 
     /// Make sure staking_contract_exists first
@@ -169,6 +187,12 @@ spec aptos_framework::staking_proxy {
 
     spec set_stake_pool_voter(owner: &signer, new_voter: address) {
         include SetStakePoolVoterAbortsIf;
+        include AbortsIfSignerPermissionStakeProxy {
+            s: owner
+        };
+        include exists<stake::StakePool>(signer::address_of(owner)) ==> stake::AbortsIfSignerPermissionStake {
+            s:owner
+        };
     }
 
     spec schema SetStakePoolVoterAbortsIf {
@@ -177,11 +201,20 @@ spec aptos_framework::staking_proxy {
         owner: &signer;
         new_voter: address;
 
-        aborts_if permissioned_signer::spec_is_permissioned_signer(owner);
+        include AbortsIfSignerPermissionStakeProxy {
+            s: owner
+        };
         let owner_address = signer::address_of(owner);
         let ownership_cap = global<stake::OwnerCapability>(owner_address);
         let pool_address = ownership_cap.pool_address;
         aborts_if stake::stake_pool_exists(owner_address) && !(exists<stake::OwnerCapability>(owner_address) && stake::stake_pool_exists(pool_address));
         ensures stake::stake_pool_exists(owner_address) ==> global<stake::StakePool>(pool_address).delegated_voter == new_voter;
     }
+
+    spec schema AbortsIfSignerPermissionStakeProxy {
+        use aptos_framework::permissioned_signer;
+        s: signer;
+        let perm = StakeProxyPermission {};
+        aborts_if !permissioned_signer::spec_check_permission_exists(s, perm);
+    }
 }
diff --git a/aptos-move/framework/aptos-stdlib/doc/smart_table.md b/aptos-move/framework/aptos-stdlib/doc/smart_table.md
@@ -1480,6 +1480,7 @@ map_spec_has_key = spec_contains;
 
 <pre><code><b>pragma</b> verify = <b>false</b>;
 <b>pragma</b> opaque;
+<b>aborts_if</b> [abstract] <b>false</b>;
 </code></pre>
 
 
@@ -1497,6 +1498,7 @@ map_spec_has_key = spec_contains;
 
 <pre><code><b>pragma</b> verify = <b>false</b>;
 <b>pragma</b> opaque;
+<b>aborts_if</b> <b>false</b>;
 </code></pre>
 
 

diff --git a/aptos-move/framework/aptos-stdlib/sources/data_structures/smart_table.spec.move b/aptos-move/framework/aptos-stdlib/sources/data_structures/smart_table.spec.move
@@ -25,11 +25,13 @@ spec aptos_std::smart_table {
     spec destroy<K: drop, V: drop>(self: SmartTable<K, V>) {
         pragma verify = false;
         pragma opaque;
+        aborts_if [abstract] false;
     }
 
     spec clear<K: drop, V: drop>(self: &mut SmartTable<K, V>) {
         pragma verify = false;
         pragma opaque;
+        aborts_if false;
     }
 
     spec split_one_bucket<K, V>(self: &mut SmartTable<K, V>) {