From d46809832aadffe3ef13bbaa212716c8a67aa2af Mon Sep 17 00:00:00 2001 From: Teng Zhang Date: Wed, 9 Oct 2024 14:27:21 -0700 Subject: [PATCH] format fix --- .../framework/aptos-framework/doc/stake.md | 70 ------------------- .../sources/permissioned_signer.spec.move | 4 +- .../aptos-framework/sources/stake.spec.move | 3 - .../sources/staking_proxy.spec.move | 2 - .../framework/aptos-stdlib/doc/smart_table.md | 2 +- .../data_structures/smart_table.spec.move | 2 +- 6 files changed, 4 insertions(+), 79 deletions(-) diff --git a/aptos-move/framework/aptos-framework/doc/stake.md b/aptos-move/framework/aptos-framework/doc/stake.md index 4f0787a0f0343e..a742ff15e4672e 100644 --- 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 - - - - -
schema ResourceRequirement {
-    requires exists<AptosCoinCapabilities>(@aptos_framework);
-    requires exists<ValidatorPerformance>(@aptos_framework);
-    requires exists<ValidatorSet>(@aptos_framework);
-    requires exists<StakingConfig>(@aptos_framework);
-    requires exists<StakingRewardsConfig>(@aptos_framework) || !features::spec_periodical_reward_rate_decrease_enabled();
-    requires exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework);
-    requires exists<ValidatorFees>(@aptos_framework);
-}
-
- - - - - - - -
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` diff --git a/aptos-move/framework/aptos-framework/sources/permissioned_signer.spec.move b/aptos-move/framework/aptos-framework/sources/permissioned_signer.spec.move index a48353af7e62e1..b065a8d97e70b0 100644 --- 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 index a3c2f5cf6ebb37..203d168c95ccb1 100644 --- 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(owner_address); ensures exists(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(pool_address); let post validator_info = global(pool_address); modifies global(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(pool_address); let post validator_info = global(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 index 5c3bda7784349e..9ca3bf3021bd9f 100644 --- 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 index 332646552eb049..5ac1b438b3563d 100644 --- 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; 
pragma verify = false;
 pragma opaque;
-aborts_if false;
+aborts_if [abstract] 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 18d0cc53056d6f..ef1fd26ba58141 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 @@ -31,7 +31,7 @@ spec aptos_std::smart_table { spec clear(self: &mut SmartTable) { pragma verify = false; pragma opaque; - aborts_if false; + aborts_if [abstract] false; } spec split_one_bucket(self: &mut SmartTable) {