format fix

aptos-labs · Oct 9, 2024 · d468098 · d468098
1 parent fb65a38
commit d468098
Show file tree

Hide file tree

Showing 6 changed files with 4 additions and 79 deletions.
diff --git a/aptos-move/framework/aptos-framework/doc/stake.md b/aptos-move/framework/aptos-framework/doc/stake.md
@@ -5836,76 +5836,6 @@ Returns validator's next epoch voting power, including pending_active, active, a
 
 
 
-
-<a id="0x1_stake_ResourceRequirement"></a>
-
-
-<pre><code><b>schema</b> <a href="stake.md#0x1_stake_ResourceRequirement">ResourceRequirement</a> {
-    <b>requires</b> <b>exists</b>&lt;<a href="stake.md#0x1_stake_AptosCoinCapabilities">AptosCoinCapabilities</a>&gt;(@aptos_framework);
-    <b>requires</b> <b>exists</b>&lt;<a href="stake.md#0x1_stake_ValidatorPerformance">ValidatorPerformance</a>&gt;(@aptos_framework);
-    <b>requires</b> <b>exists</b>&lt;<a href="stake.md#0x1_stake_ValidatorSet">ValidatorSet</a>&gt;(@aptos_framework);
-    <b>requires</b> <b>exists</b>&lt;StakingConfig&gt;(@aptos_framework);
-    <b>requires</b> <b>exists</b>&lt;StakingRewardsConfig&gt;(@aptos_framework) || !<a href="../../aptos-stdlib/../move-stdlib/doc/features.md#0x1_features_spec_periodical_reward_rate_decrease_enabled">features::spec_periodical_reward_rate_decrease_enabled</a>();
-    <b>requires</b> <b>exists</b>&lt;<a href="timestamp.md#0x1_timestamp_CurrentTimeMicroseconds">timestamp::CurrentTimeMicroseconds</a>&gt;(@aptos_framework);
-    <b>requires</b> <b>exists</b>&lt;<a href="stake.md#0x1_stake_ValidatorFees">ValidatorFees</a>&gt;(@aptos_framework);
-}
-</code></pre>
-
-
-
-
-<a id="0x1_stake_spec_get_reward_rate_1"></a>
-
-
-<pre><code><b>fun</b> <a href="stake.md#0x1_stake_spec_get_reward_rate_1">spec_get_reward_rate_1</a>(config: StakingConfig): num {
-   <b>if</b> (<a href="../../aptos-stdlib/../move-stdlib/doc/features.md#0x1_features_spec_periodical_reward_rate_decrease_enabled">features::spec_periodical_reward_rate_decrease_enabled</a>()) {
-       <b>let</b> epoch_rewards_rate = <b>global</b>&lt;<a href="staking_config.md#0x1_staking_config_StakingRewardsConfig">staking_config::StakingRewardsConfig</a>&gt;(@aptos_framework).rewards_rate;
-       <b>if</b> (epoch_rewards_rate.value == 0) {
-           0
-       } <b>else</b> {
-           <b>let</b> denominator_0 = aptos_std::fixed_point64::spec_divide_u128(<a href="staking_config.md#0x1_staking_config_MAX_REWARDS_RATE">staking_config::MAX_REWARDS_RATE</a>, epoch_rewards_rate);
-           <b>let</b> denominator = <b>if</b> (denominator_0 &gt; <a href="stake.md#0x1_stake_MAX_U64">MAX_U64</a>) {
-               <a href="stake.md#0x1_stake_MAX_U64">MAX_U64</a>
-           } <b>else</b> {
-               denominator_0
-           };
-           <b>let</b> nominator = aptos_std::fixed_point64::spec_multiply_u128(denominator, epoch_rewards_rate);
-           nominator
-       }
-   } <b>else</b> {
-           config.rewards_rate
-   }
-}
-</code></pre>
-
-
-
-
-<a id="0x1_stake_spec_get_reward_rate_2"></a>
-
-
-<pre><code><b>fun</b> <a href="stake.md#0x1_stake_spec_get_reward_rate_2">spec_get_reward_rate_2</a>(config: StakingConfig): num {
-   <b>if</b> (<a href="../../aptos-stdlib/../move-stdlib/doc/features.md#0x1_features_spec_periodical_reward_rate_decrease_enabled">features::spec_periodical_reward_rate_decrease_enabled</a>()) {
-       <b>let</b> epoch_rewards_rate = <b>global</b>&lt;<a href="staking_config.md#0x1_staking_config_StakingRewardsConfig">staking_config::StakingRewardsConfig</a>&gt;(@aptos_framework).rewards_rate;
-       <b>if</b> (epoch_rewards_rate.value == 0) {
-           1
-       } <b>else</b> {
-           <b>let</b> denominator_0 = aptos_std::fixed_point64::spec_divide_u128(<a href="staking_config.md#0x1_staking_config_MAX_REWARDS_RATE">staking_config::MAX_REWARDS_RATE</a>, epoch_rewards_rate);
-           <b>let</b> denominator = <b>if</b> (denominator_0 &gt; <a href="stake.md#0x1_stake_MAX_U64">MAX_U64</a>) {
-               <a href="stake.md#0x1_stake_MAX_U64">MAX_U64</a>
-           } <b>else</b> {
-               denominator_0
-           };
-           denominator
-       }
-   } <b>else</b> {
-           config.rewards_rate_denominator
-   }
-}
-</code></pre>
-
-
-
 <a id="@Specification_1_update_stake_pool"></a>
 
 ### Function `update_stake_pool`

diff --git a/aptos-move/framework/aptos-framework/sources/permissioned_signer.spec.move b/aptos-move/framework/aptos-framework/sources/permissioned_signer.spec.move
@@ -78,8 +78,8 @@ spec aptos_framework::permissioned_signer {
     perm: PermKey
     ) {
 
-        use aptos_std::type_info;
-        use std::bcs;
+        // use aptos_std::type_info;
+        // use std::bcs;
         pragma aborts_if_is_partial;
         aborts_if !spec_is_permissioned_signer(permissioned);
         aborts_if spec_is_permissioned_signer(master);

diff --git a/aptos-move/framework/aptos-framework/sources/stake.spec.move b/aptos-move/framework/aptos-framework/sources/stake.spec.move
@@ -328,7 +328,6 @@ spec aptos_framework::stake {
         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);
@@ -380,7 +379,6 @@ spec aptos_framework::stake {
         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);
@@ -430,7 +428,6 @@ spec aptos_framework::stake {
         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();

diff --git a/aptos-move/framework/aptos-framework/sources/staking_proxy.spec.move b/aptos-move/framework/aptos-framework/sources/staking_proxy.spec.move
@@ -138,7 +138,6 @@ spec aptos_framework::staking_proxy {
     }
 
     spec schema SetStakePoolOperator {
-        use aptos_framework::permissioned_signer;
 
         owner: &signer;
         new_operator: address;
@@ -196,7 +195,6 @@ spec aptos_framework::staking_proxy {
     }
 
     spec schema SetStakePoolVoterAbortsIf {
-        use aptos_framework::permissioned_signer;
 
         owner: &signer;
         new_voter: address;

diff --git a/aptos-move/framework/aptos-stdlib/doc/smart_table.md b/aptos-move/framework/aptos-stdlib/doc/smart_table.md
@@ -1498,7 +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>;
+<b>aborts_if</b> [abstract] <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
@@ -31,7 +31,7 @@ spec aptos_std::smart_table {
     spec clear<K: drop, V: drop>(self: &mut SmartTable<K, V>) {
         pragma verify = false;
         pragma opaque;
-        aborts_if false;
+        aborts_if [abstract] false;
     }
 
     spec split_one_bucket<K, V>(self: &mut SmartTable<K, V>) {