diff --git a/aptos-move/framework/aptos-framework/doc/aptos_governance.md b/aptos-move/framework/aptos-framework/doc/aptos_governance.md index 4598f8c382bbb..096f644954041 100644 --- a/aptos-move/framework/aptos-framework/doc/aptos_governance.md +++ b/aptos-move/framework/aptos-framework/doc/aptos_governance.md @@ -2153,6 +2153,7 @@ Limit addition overflow. 
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/doc/stake.md b/aptos-move/framework/aptos-framework/doc/stake.md
index f8fd44e48c764..4f0787a0f0343 100644
--- a/aptos-move/framework/aptos-framework/doc/stake.md
+++ b/aptos-move/framework/aptos-framework/doc/stake.md
@@ -4750,59 +4750,6 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-
-
-
-
-
fun spec_get_reward_rate_1(config: StakingConfig): num {
-   if (features::spec_periodical_reward_rate_decrease_enabled()) {
-       let epoch_rewards_rate = global<staking_config::StakingRewardsConfig>(@aptos_framework).rewards_rate;
-       if (epoch_rewards_rate.value == 0) {
-           0
-       } else {
-           let denominator_0 = aptos_std::fixed_point64::spec_divide_u128(staking_config::MAX_REWARDS_RATE, epoch_rewards_rate);
-           let denominator = if (denominator_0 > MAX_U64) {
-               MAX_U64
-           } else {
-               denominator_0
-           };
-           let nominator = aptos_std::fixed_point64::spec_multiply_u128(denominator, epoch_rewards_rate);
-           nominator
-       }
-   } else {
-           config.rewards_rate
-   }
-}
-

-
-
-
-
-
-
-
-
fun spec_get_reward_rate_2(config: StakingConfig): num {
-   if (features::spec_periodical_reward_rate_decrease_enabled()) {
-       let epoch_rewards_rate = global<staking_config::StakingRewardsConfig>(@aptos_framework).rewards_rate;
-       if (epoch_rewards_rate.value == 0) {
-           1
-       } else {
-           let denominator_0 = aptos_std::fixed_point64::spec_divide_u128(staking_config::MAX_REWARDS_RATE, epoch_rewards_rate);
-           let denominator = if (denominator_0 > MAX_U64) {
-               MAX_U64
-           } else {
-               denominator_0
-           };
-           denominator
-       }
-   } else {
-           config.rewards_rate_denominator
-   }
-}
-

-
-
-
 
 
 ### Resource `ValidatorSet`
@@ -5075,6 +5022,11 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
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 {
@@ -5106,7 +5058,10 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-
let pubkey_from_pop = bls12381::spec_public_key_from_bytes_with_pop(
+
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)
 );
@@ -5145,6 +5100,9 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
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);
@@ -5163,7 +5121,9 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-
aborts_if permissioned_signer::spec_is_permissioned_signer(owner);
+
include AbortsIfSignerPermissionStake {
+    s: owner
+};
 let owner_address = signer::address_of(owner);
 aborts_if exists<OwnerCapability>(owner_address);
 ensures exists<OwnerCapability>(owner_address);
@@ -5224,8 +5184,11 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-
pragma verify_duration_estimate = 120;
+
pragma verify = false;
 pragma aborts_if_is_partial;
+include AbortsIfSignerPermissionStake {
+    s: owner
+};
 aborts_if reconfiguration_state::spec_is_in_progress();
 include ResourceRequirement;
 include AddStakeAbortsIfAndEnsures;
@@ -5245,7 +5208,7 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
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();
@@ -5290,7 +5253,9 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-
aborts_if permissioned_signer::spec_is_permissioned_signer(operator);
+
include AbortsIfSignerPermissionStake {
+    s: 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();
@@ -5320,7 +5285,9 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-
aborts_if permissioned_signer::spec_is_permissioned_signer(operator);
+
include AbortsIfSignerPermissionStake {
+    s: operator
+};
 let pre_stake_pool = global<StakePool>(pool_address);
 let post validator_info = global<ValidatorConfig>(pool_address);
 modifies global<ValidatorConfig>(pool_address);
@@ -5376,6 +5343,9 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
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);
@@ -5453,6 +5423,9 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
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);
@@ -5499,6 +5472,9 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
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);
@@ -5877,6 +5853,59 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
+
+
+
+
+
fun spec_get_reward_rate_1(config: StakingConfig): num {
+   if (features::spec_periodical_reward_rate_decrease_enabled()) {
+       let epoch_rewards_rate = global<staking_config::StakingRewardsConfig>(@aptos_framework).rewards_rate;
+       if (epoch_rewards_rate.value == 0) {
+           0
+       } else {
+           let denominator_0 = aptos_std::fixed_point64::spec_divide_u128(staking_config::MAX_REWARDS_RATE, epoch_rewards_rate);
+           let denominator = if (denominator_0 > MAX_U64) {
+               MAX_U64
+           } else {
+               denominator_0
+           };
+           let nominator = aptos_std::fixed_point64::spec_multiply_u128(denominator, epoch_rewards_rate);
+           nominator
+       }
+   } else {
+           config.rewards_rate
+   }
+}
+

+
+
+
+
+
+
+
+
fun spec_get_reward_rate_2(config: StakingConfig): num {
+   if (features::spec_periodical_reward_rate_decrease_enabled()) {
+       let epoch_rewards_rate = global<staking_config::StakingRewardsConfig>(@aptos_framework).rewards_rate;
+       if (epoch_rewards_rate.value == 0) {
+           1
+       } else {
+           let denominator_0 = aptos_std::fixed_point64::spec_divide_u128(staking_config::MAX_REWARDS_RATE, epoch_rewards_rate);
+           let denominator = if (denominator_0 > MAX_U64) {
+               MAX_U64
+           } else {
+               denominator_0
+           };
+           denominator
+       }
+   } else {
+           config.rewards_rate_denominator
+   }
+}
+

+
+
+
 
 
 ### Function `update_stake_pool`
@@ -5934,6 +5963,19 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
+
+
+
+
schema AbortsIfSignerPermissionStake {
+    s: signer;
+    let perm = StakePermission {};
+    aborts_if !permissioned_signer::spec_check_permission_exists(s, perm);
+}
+

+
+
+
+
 
 
 
@@ -6009,6 +6051,7 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
pragma opaque;
 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;
diff --git a/aptos-move/framework/aptos-framework/doc/staking_proxy.md b/aptos-move/framework/aptos-framework/doc/staking_proxy.md
index e8a756c4039fc..a15a4684c34b1 100644
--- 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.
 
 
 
+
+
+### Function `grant_permission`
+
+
+
public fun grant_permission(master: &signer, permissioned_signer: &signer)
+

+
+
+
+
+
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);
+

+
+
+
 
 
 ### Function `set_operator`
@@ -559,6 +579,12 @@ One of them are not exists
 
 
 
include SetStakePoolOperator;
+include AbortsIfSignerPermissionStakeProxy {
+    s: owner
+};
+include exists<stake::StakePool>(signer::address_of(owner)) ==> stake::AbortsIfSignerPermissionStake {
+    s:owner
+};
 

 
 
@@ -570,7 +596,9 @@ One of them are not exists
 
schema SetStakePoolOperator {
     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;
@@ -609,6 +637,9 @@ One of them are not exists
 
 
 
include SetStakingContractVoter;
+include AbortsIfSignerPermissionStakeProxy {
+    s: owner
+};
 

 
 
@@ -651,6 +682,12 @@ Then abort if the resource is not exist
 
 
 
include SetStakePoolVoterAbortsIf;
+include AbortsIfSignerPermissionStakeProxy {
+    s: owner
+};
+include exists<stake::StakePool>(signer::address_of(owner)) ==> stake::AbortsIfSignerPermissionStake {
+    s:owner
+};
 

 
 
@@ -662,7 +699,9 @@ Then abort if the resource is not exist
 
schema SetStakePoolVoterAbortsIf {
     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;
@@ -672,4 +711,17 @@ Then abort if the resource is not exist
 

 
 
+
+
+
+
+
+
schema AbortsIfSignerPermissionStakeProxy {
+    s: signer;
+    let perm = StakeProxyPermission {};
+    aborts_if !permissioned_signer::spec_check_permission_exists(s, perm);
+}
+

+
+
 [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
index 4c0189023816c..c233266d5b887 100644
--- 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(addr);
 
+        aborts_if permissioned_signer::spec_is_permissioned_signer(aptos_framework);
         aborts_if exists>(addr);
         aborts_if !exists(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
index 3ed44f710fa41..a3c2f5cf6ebb3 100644
--- a/aptos-move/framework/aptos-framework/sources/stake.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/stake.spec.move
@@ -132,6 +132,9 @@ spec aptos_framework::stake {
         network_addresses: vector,
         fullnode_addresses: vector,
     ){
+        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)
@@ -177,6 +180,9 @@ spec aptos_framework::stake {
         // This function casue timeout (property proved)
         // pragma verify_duration_estimate = 120;
         pragma disable_invariants_in_body;
+        include AbortsIfSignerPermissionStake {
+            s: operator
+        };
         aborts_if !staking_config::get_allow_validator_set_change(staking_config::get());
         aborts_if !exists(pool_address);
         aborts_if !exists(pool_address);
@@ -230,6 +236,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(addr);
@@ -269,6 +278,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);
@@ -304,13 +316,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(owner_address);
         ensures !exists(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(owner_address);
         ensures exists(owner_address);
@@ -359,7 +377,10 @@ spec aptos_framework::stake {
         new_network_addresses: vector,
         new_fullnode_addresses: vector,
     ) {
-        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(pool_address);
         let post validator_info = global(pool_address);
         modifies global(pool_address);
@@ -406,7 +427,10 @@ spec aptos_framework::stake {
         new_consensus_pubkey: vector,
         proof_of_possession: vector,
     ) {
-        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(pool_address);
         let post validator_info = global(pool_address);
         aborts_if reconfiguration_state::spec_is_in_progress();
@@ -519,6 +543,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;
 
@@ -608,6 +639,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;
@@ -685,7 +717,7 @@ 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();
@@ -693,10 +725,13 @@ spec aptos_framework::stake {
     }
 
     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;
@@ -710,7 +745,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(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
index d5b6ba29ad82e..5c3bda7784349 100644
--- 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(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(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(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(owner_address);
         let pool_address = ownership_cap.pool_address;
         aborts_if stake::stake_pool_exists(owner_address) && !(exists(owner_address) && stake::stake_pool_exists(pool_address));
         ensures stake::stake_pool_exists(owner_address) ==> global(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
index 83eb27ba47fff..332646552eb04 100644
--- 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;
 
 
pragma verify = false;
 pragma opaque;
+aborts_if [abstract] false;
 

 
 
@@ -1497,6 +1498,7 @@ map_spec_has_key = spec_contains;
 
 
pragma verify = false;
 pragma opaque;
+aborts_if false;
 

 
 
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
index 4344eb2329efb..18d0cc53056d6 100644
--- 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(self: SmartTable) {
         pragma verify = false;
         pragma opaque;
+        aborts_if [abstract] false;
     }
 
     spec clear(self: &mut SmartTable) {
         pragma verify = false;
         pragma opaque;
+        aborts_if false;
     }
 
     spec split_one_bucket(self: &mut SmartTable) {