From 266953e9bd19e4fd181466c36a0f99a0a5cb7a9f Mon Sep 17 00:00:00 2001 From: Xinding Wei Date: Wed, 19 Apr 2023 13:05:16 -0700 Subject: [PATCH] Refactor reward rate calculation --- aptos-move/e2e-move-tests/src/tests/stake.rs | 27 ++++++++++-- .../aptos-framework/doc/gas_schedule.md | 2 +- .../framework/aptos-framework/doc/stake.md | 25 ++++------- .../aptos-framework/doc/staking_config.md | 42 +++++++++++++++---- .../sources/configs/gas_schedule.spec.move | 2 +- .../sources/configs/staking_config.move | 27 +++++++++--- .../sources/configs/staking_config.spec.move | 10 ++--- .../sources/delegation_pool.move | 38 +++++++++++++++++ .../aptos-framework/sources/stake.move | 39 ++++++++--------- .../aptos-framework/sources/stake.spec.move | 2 +- .../framework/move-stdlib/doc/features.md | 6 +-- .../sources/configs/features.spec.move | 4 +- 12 files changed, 153 insertions(+), 71 deletions(-) diff --git a/aptos-move/e2e-move-tests/src/tests/stake.rs b/aptos-move/e2e-move-tests/src/tests/stake.rs index a19295b60aa25..bc4490a3eeccf 100644 --- a/aptos-move/e2e-move-tests/src/tests/stake.rs +++ b/aptos-move/e2e-move-tests/src/tests/stake.rs @@ -245,13 +245,12 @@ fn test_staking_rewards() { rewards_rate_denominator, ); - // Another 0.5 year passed. Rewards rate halves. New rewards rate is 0.5% every epoch. + // Another 0.5 year passed. Rewards rate halves. New rewards after this epoch rate is 0.5% every epoch. // Both validators propose a block in the current epoch. Both should receive rewards. harness.new_block_with_metadata(validator_1_address, vec![]); harness.new_block_with_metadata(validator_2_address, vec![]); harness.fast_forward(one_year_in_secs / 2); harness.new_epoch(); - rewards_rate = rewards_rate * rewards_rate_decrease_rate_bps / bps_denominator; update_stake_amount_and_assert_with_errors( &mut harness, &mut stake_amount_1, @@ -266,12 +265,32 @@ fn test_staking_rewards() { rewards_rate, rewards_rate_denominator, ); + rewards_rate = rewards_rate * rewards_rate_decrease_rate_bps / bps_denominator; + // Another new epoch, both validators receive rewards in 0.5% every epoch. // Another year passed. Rewards rate halves but it cannot be lower than 0.3%. - // New rewards rate is 0.3% every epoch. + // New rewards rate of the next epoch is 0.3% every epoch. + harness.new_block_with_metadata(validator_1_address, vec![]); + harness.new_block_with_metadata(validator_2_address, vec![]); + harness.fast_forward(one_year_in_secs); + harness.new_epoch(); + update_stake_amount_and_assert_with_errors( + &mut harness, + &mut stake_amount_1, + validator_1_address, + rewards_rate, + rewards_rate_denominator, + ); + update_stake_amount_and_assert_with_errors( + &mut harness, + &mut stake_amount_2, + validator_2_address, + rewards_rate, + rewards_rate_denominator, + ); + // Validator 1 misses one proposal but has one successful so they receive half of the rewards. harness.new_block_with_metadata(validator_1_address, vec![index_1]); - harness.fast_forward(one_year_in_secs); harness.new_epoch(); rewards_rate = min_rewards_rate / 2; update_stake_amount_and_assert_with_errors( diff --git a/aptos-move/framework/aptos-framework/doc/gas_schedule.md b/aptos-move/framework/aptos-framework/doc/gas_schedule.md index 7a517f58c6b08..7200399046e40 100644 --- a/aptos-move/framework/aptos-framework/doc/gas_schedule.md +++ b/aptos-move/framework/aptos-framework/doc/gas_schedule.md @@ -319,7 +319,7 @@ This can be called by on-chain governance to update the gas schedule. -
pragma timeout = 60;
+
pragma timeout = 100;
 requires exists<stake::ValidatorFees>(@aptos_framework);
 requires exists<CoinInfo<AptosCoin>>(@aptos_framework);
 include system_addresses::AbortsIfNotAptosFramework{ account: aptos_framework };
diff --git a/aptos-move/framework/aptos-framework/doc/stake.md b/aptos-move/framework/aptos-framework/doc/stake.md
index 07ea058c2f324..a722065d4c8b7 100644
--- a/aptos-move/framework/aptos-framework/doc/stake.md
+++ b/aptos-move/framework/aptos-framework/doc/stake.md
@@ -3060,6 +3060,11 @@ power.
 
         validator_index = validator_index + 1;
     };
+
+    if (features::periodical_reward_rate_decrease_enabled()) {
+        // Update rewards rate after reward distribution.
+        staking_config::calculate_and_save_latest_epoch_rewards_rate();
+    };
 }
 
@@ -3102,23 +3107,7 @@ This function shouldn't abort. assume cur_validator_perf.successful_proposals + cur_validator_perf.failed_proposals <= MAX_U64; }; let num_total_proposals = cur_validator_perf.successful_proposals + cur_validator_perf.failed_proposals; - let (rewards_rate, rewards_rate_denominator) = if (features::periodical_reward_rate_decrease_enabled()) { - let epoch_rewards_rate = staking_config::calculate_and_save_latest_epoch_rewards_rate(); - if (fixed_point64::is_zero(epoch_rewards_rate)) { - (0u64, 1u64) - } else { - // Maximize denominator for higher precision. - // Restriction: nominator <= MAX_REWARDS_RATE && denominator <= MAX_U64 - let denominator = fixed_point64::divide_u128((MAX_REWARDS_RATE as u128), epoch_rewards_rate); - if (denominator > MAX_U64) { - denominator = MAX_U64 - }; - let nominator = (fixed_point64::multiply_u128(denominator, epoch_rewards_rate) as u64); - (nominator, (denominator as u64)) - } - } else { - staking_config::get_reward_rate(staking_config) - }; + let (rewards_rate, rewards_rate_denominator) = staking_config::get_reward_rate(staking_config); let rewards_active = distribute_rewards( &mut stake_pool.active, num_successful_proposals, @@ -4229,7 +4218,7 @@ Returns validator's next epoch voting power, including pending_active, active, a requires exists<ValidatorPerformance>(@aptos_framework); requires exists<ValidatorSet>(@aptos_framework); requires exists<StakingConfig>(@aptos_framework); - requires exists<StakingRewardsConfig>(@aptos_framework) || !features::spec_reward_rate_decrease_enabled(); + requires exists<StakingRewardsConfig>(@aptos_framework) || !features::spec_periodical_reward_rate_decrease_enabled(); requires exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework); requires exists<ValidatorFees>(@aptos_framework); } diff --git a/aptos-move/framework/aptos-framework/doc/staking_config.md b/aptos-move/framework/aptos-framework/doc/staking_config.md index a51a8da3c4f64..93e01653c96ce 100644 --- a/aptos-move/framework/aptos-framework/doc/staking_config.md +++ b/aptos-move/framework/aptos-framework/doc/staking_config.md @@ -175,6 +175,15 @@ Staking reward configurations that will be stored with the @aptos_framework acco ## Constants + + + + +
const MAX_U64: u128 = 18446744073709551615;
+
+ + + Denominator of number in basis points. 1 bps(basis points) = 0.01%. @@ -536,8 +545,7 @@ withdraw all funds). ## Function `get_reward_rate` -DEPRECATING -Return the reward rate. +Return the reward rate of this epoch.
public fun get_reward_rate(config: &staking_config::StakingConfig): (u64, u64)
@@ -549,9 +557,25 @@ Return the reward rate.
 Implementation
 
 
-
public fun get_reward_rate(config: &StakingConfig): (u64, u64) {
-    assert!(!features::periodical_reward_rate_decrease_enabled(), EDEPRECATED_FUNCTION);
-    (config.rewards_rate, config.rewards_rate_denominator)
+
public fun get_reward_rate(config: &StakingConfig): (u64, u64) acquires StakingRewardsConfig {
+    let (rewards_rate, rewards_rate_denominator) = if (features::periodical_reward_rate_decrease_enabled()) {
+        let epoch_rewards_rate = borrow_global<StakingRewardsConfig>(@aptos_framework).rewards_rate;
+        if (fixed_point64::is_zero(epoch_rewards_rate)) {
+            (0u64, 1u64)
+        } else {
+            // Maximize denominator for higher precision.
+            // Restriction: nominator <= MAX_REWARDS_RATE && denominator <= MAX_U64
+            let denominator = fixed_point64::divide_u128((MAX_REWARDS_RATE as u128), epoch_rewards_rate);
+            if (denominator > MAX_U64) {
+                denominator = MAX_U64
+            };
+            let nominator = (fixed_point64::multiply_u128(denominator, epoch_rewards_rate) as u64);
+            (nominator, (denominator as u64))
+        }
+    } else {
+        (config.rewards_rate, config.rewards_rate_denominator)
+    };
+    (rewards_rate, rewards_rate_denominator)
 }
 
@@ -1146,7 +1170,7 @@ StakingRewardsConfig does not exist under the aptos_framework before creating it -
aborts_if features::spec_reward_rate_decrease_enabled();
+
include StakingRewardsConfigRequirement;
 
@@ -1163,7 +1187,7 @@ StakingRewardsConfig does not exist under the aptos_framework before creating it
aborts_if !exists<StakingRewardsConfig>(@aptos_framework);
-aborts_if !features::spec_reward_rate_decrease_enabled();
+aborts_if !features::spec_periodical_reward_rate_decrease_enabled();
 include StakingRewardsConfigRequirement;
 
@@ -1180,7 +1204,7 @@ StakingRewardsConfig does not exist under the aptos_framework before creating it -
requires features::spec_reward_rate_decrease_enabled();
+
requires features::spec_periodical_reward_rate_decrease_enabled();
 include StakingRewardsConfigRequirement;
 aborts_if !exists<StakingRewardsConfig>(@aptos_framework);
 
@@ -1247,7 +1271,7 @@ The rewards_rate which is the numerator is limited to be < rewards_rate/rewards_rate_denominator <= 1. -
aborts_if features::spec_reward_rate_decrease_enabled();
+
aborts_if features::spec_periodical_reward_rate_decrease_enabled();
 let addr = signer::address_of(aptos_framework);
 aborts_if addr != @aptos_framework;
 aborts_if new_rewards_rate_denominator <= 0;
diff --git a/aptos-move/framework/aptos-framework/sources/configs/gas_schedule.spec.move b/aptos-move/framework/aptos-framework/sources/configs/gas_schedule.spec.move
index 801003eeeab09..277211405cd9d 100644
--- a/aptos-move/framework/aptos-framework/sources/configs/gas_schedule.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/configs/gas_schedule.spec.move
@@ -44,7 +44,7 @@ spec aptos_framework::gas_schedule {
         use aptos_framework::transaction_fee;
         use aptos_framework::staking_config;
 
-        pragma timeout = 60;
+        pragma timeout = 100;
 
         requires exists(@aptos_framework);
         requires exists>(@aptos_framework);
diff --git a/aptos-move/framework/aptos-framework/sources/configs/staking_config.move b/aptos-move/framework/aptos-framework/sources/configs/staking_config.move
index 3d2f09a88526f..64c52bdc546ec 100644
--- a/aptos-move/framework/aptos-framework/sources/configs/staking_config.move
+++ b/aptos-move/framework/aptos-framework/sources/configs/staking_config.move
@@ -42,6 +42,8 @@ module aptos_framework::staking_config {
     /// 1 year => 365 * 24 * 60 * 60
     const ONE_YEAR_IN_SECS: u64 = 31536000;
 
+    const MAX_U64: u128 = 18446744073709551615;
+
 
     /// Validator set configurations that will be stored with the @aptos_framework account.
     struct StakingConfig has copy, drop, key {
@@ -184,11 +186,26 @@ module aptos_framework::staking_config {
         config.recurring_lockup_duration_secs
     }
 
-    /// DEPRECATING
-    /// Return the reward rate.
-    public fun get_reward_rate(config: &StakingConfig): (u64, u64) {
-        assert!(!features::periodical_reward_rate_decrease_enabled(), EDEPRECATED_FUNCTION);
-        (config.rewards_rate, config.rewards_rate_denominator)
+    /// Return the reward rate of this epoch.
+    public fun get_reward_rate(config: &StakingConfig): (u64, u64) acquires StakingRewardsConfig {
+        let (rewards_rate, rewards_rate_denominator) = if (features::periodical_reward_rate_decrease_enabled()) {
+            let epoch_rewards_rate = borrow_global(@aptos_framework).rewards_rate;
+            if (fixed_point64::is_zero(epoch_rewards_rate)) {
+                (0u64, 1u64)
+            } else {
+                // Maximize denominator for higher precision.
+                // Restriction: nominator <= MAX_REWARDS_RATE && denominator <= MAX_U64
+                let denominator = fixed_point64::divide_u128((MAX_REWARDS_RATE as u128), epoch_rewards_rate);
+                if (denominator > MAX_U64) {
+                    denominator = MAX_U64
+                };
+                let nominator = (fixed_point64::multiply_u128(denominator, epoch_rewards_rate) as u64);
+                (nominator, (denominator as u64))
+            }
+        } else {
+            (config.rewards_rate, config.rewards_rate_denominator)
+        };
+        (rewards_rate, rewards_rate_denominator)
     }
 
     /// Return the joining limit %.
diff --git a/aptos-move/framework/aptos-framework/sources/configs/staking_config.spec.move b/aptos-move/framework/aptos-framework/sources/configs/staking_config.spec.move
index 2e1f2fa3b711a..db443e31eb9cc 100644
--- a/aptos-move/framework/aptos-framework/sources/configs/staking_config.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/configs/staking_config.spec.move
@@ -79,17 +79,17 @@ spec aptos_framework::staking_config {
     }
 
     spec get_reward_rate(config: &StakingConfig): (u64, u64) {
-        aborts_if features::spec_reward_rate_decrease_enabled();
+        include StakingRewardsConfigRequirement;
     }
 
     spec calculate_and_save_latest_epoch_rewards_rate(): FixedPoint64 {
         aborts_if !exists(@aptos_framework);
-        aborts_if !features::spec_reward_rate_decrease_enabled();
+        aborts_if !features::spec_periodical_reward_rate_decrease_enabled();
         include StakingRewardsConfigRequirement;
     }
 
     spec calculate_and_save_latest_rewards_config(): StakingRewardsConfig {
-        requires features::spec_reward_rate_decrease_enabled();
+        requires features::spec_periodical_reward_rate_decrease_enabled();
         include StakingRewardsConfigRequirement;
         aborts_if !exists(@aptos_framework);
     }
@@ -134,7 +134,7 @@ spec aptos_framework::staking_config {
         new_rewards_rate_denominator: u64,
     ) {
         use std::signer;
-        aborts_if features::spec_reward_rate_decrease_enabled();
+        aborts_if features::spec_periodical_reward_rate_decrease_enabled();
         let addr = signer::address_of(aptos_framework);
         aborts_if addr != @aptos_framework;
         aborts_if new_rewards_rate_denominator <= 0;
@@ -209,7 +209,7 @@ spec aptos_framework::staking_config {
 
     spec schema StakingRewardsConfigRequirement {
         requires exists(@aptos_framework);
-        include features::spec_reward_rate_decrease_enabled() ==> StakingRewardsConfigEnabledRequirement;
+        include features::spec_periodical_reward_rate_decrease_enabled() ==> StakingRewardsConfigEnabledRequirement;
     }
 
     spec schema StakingRewardsConfigEnabledRequirement {
diff --git a/aptos-move/framework/aptos-framework/sources/delegation_pool.move b/aptos-move/framework/aptos-framework/sources/delegation_pool.move
index e1ce68580d1c3..c505f2ea8a7d3 100644
--- a/aptos-move/framework/aptos-framework/sources/delegation_pool.move
+++ b/aptos-move/framework/aptos-framework/sources/delegation_pool.move
@@ -990,6 +990,10 @@ module aptos_framework::delegation_pool {
 
     #[test_only]
     use aptos_framework::reconfiguration;
+    #[test_only]
+    use aptos_std::fixed_point64;
+    #[test_only]
+    use aptos_framework::timestamp::fast_forward_seconds;
 
     #[test_only]
     const CONSENSUS_KEY_1: vector = x"8a54b92288d4ba5073d3a52e80cc00ae9fbbc1cc5b433b46089b7804c38a76f00fc64746c7685ee628fc2d0b929c2294";
@@ -1317,6 +1321,40 @@ module aptos_framework::delegation_pool {
         // stakes should remain the same - `Self::get_stake` correctly calculates them
         synchronize_delegation_pool(pool_address);
         assert_delegation(delegator1_address, pool_address, 11201699216002, 0, 2000000000000);
+
+        let reward_period_start_time_in_sec = timestamp::now_seconds();
+        // Enable rewards rate decrease. Initially rewards rate is still 1% every epoch. Rewards rate halves every year.
+        let one_year_in_secs: u64 = 31536000;
+        staking_config::initialize_rewards(
+            aptos_framework,
+            fixed_point64::create_from_rational(2, 100),
+            fixed_point64::create_from_rational(6, 1000),
+            one_year_in_secs,
+            reward_period_start_time_in_sec,
+            fixed_point64::create_from_rational(50, 100),
+        );
+        features::change_feature_flags(aptos_framework, vector[features::get_periodical_reward_rate_decrease_feature()], vector[]);
+
+        // add more stake from delegator 1
+        stake::mint(delegator1, 20000 * ONE_APT);
+        let delegator1_pending_inactive: u64;
+        (delegator1_active, _, delegator1_pending_inactive) = get_stake(pool_address, delegator1_address);
+        fee = get_add_stake_fee(pool_address, 20000 * ONE_APT);
+        add_stake(delegator1, pool_address, 20000 * ONE_APT);
+
+        assert_delegation(delegator1_address, pool_address, delegator1_active + 20000 * ONE_APT - fee, 0, delegator1_pending_inactive);
+
+        // delegator 1 unlocks his entire newly added stake
+        unlock(delegator1, pool_address, 20000 * ONE_APT - fee);
+        end_aptos_epoch();
+        // delegator 1 should own previous 11201699216002 active * ~1.01253 and 20000 * ~1.01253 + 20000 coins pending_inactive
+        assert_delegation(delegator1_address, pool_address, 11342056366822, 0, 4025059974939);
+
+        // stakes should remain the same - `Self::get_stake` correctly calculates them
+        synchronize_delegation_pool(pool_address);
+        assert_delegation(delegator1_address, pool_address, 11342056366822, 0, 4025059974939);
+
+        fast_forward_seconds(one_year_in_secs);
     }
 
     #[test(aptos_framework = @aptos_framework, validator = @0x123, delegator = @0x010)]
diff --git a/aptos-move/framework/aptos-framework/sources/stake.move b/aptos-move/framework/aptos-framework/sources/stake.move
index 5af09daa0a4cd..0a83bec2c047e 100644
--- a/aptos-move/framework/aptos-framework/sources/stake.move
+++ b/aptos-move/framework/aptos-framework/sources/stake.move
@@ -1141,6 +1141,11 @@ module aptos_framework::stake {
 
             validator_index = validator_index + 1;
         };
+
+        if (features::periodical_reward_rate_decrease_enabled()) {
+            // Update rewards rate after reward distribution.
+            staking_config::calculate_and_save_latest_epoch_rewards_rate();
+        };
     }
 
     /// Update individual validator's stake pool
@@ -1163,23 +1168,7 @@ module aptos_framework::stake {
             assume cur_validator_perf.successful_proposals + cur_validator_perf.failed_proposals <= MAX_U64;
         };
         let num_total_proposals = cur_validator_perf.successful_proposals + cur_validator_perf.failed_proposals;
-        let (rewards_rate, rewards_rate_denominator) = if (features::periodical_reward_rate_decrease_enabled()) {
-            let epoch_rewards_rate = staking_config::calculate_and_save_latest_epoch_rewards_rate();
-            if (fixed_point64::is_zero(epoch_rewards_rate)) {
-                (0u64, 1u64)
-            } else {
-                // Maximize denominator for higher precision.
-                // Restriction: nominator <= MAX_REWARDS_RATE && denominator <= MAX_U64
-                let denominator = fixed_point64::divide_u128((MAX_REWARDS_RATE as u128), epoch_rewards_rate);
-                if (denominator > MAX_U64) {
-                    denominator = MAX_U64
-                };
-                let nominator = (fixed_point64::multiply_u128(denominator, epoch_rewards_rate) as u64);
-                (nominator, (denominator as u64))
-            }
-        } else {
-            staking_config::get_reward_rate(staking_config)
-        };
+        let (rewards_rate, rewards_rate_denominator) = staking_config::get_reward_rate(staking_config);
         let rewards_active = distribute_rewards(
             &mut stake_pool.active,
             num_successful_proposals,
@@ -1372,6 +1361,7 @@ module aptos_framework::stake {
     #[test_only]
     use aptos_framework::aptos_coin;
     use aptos_std::bls12381::proof_of_possession_from_bytes;
+    #[test_only]
     use aptos_std::fixed_point64;
 
     #[test_only]
@@ -2465,17 +2455,22 @@ module aptos_framework::stake {
         // For some reason, this epoch is very long. It has been 1 year since genesis when the epoch ends.
         timestamp::fast_forward_seconds(one_year_in_secs - EPOCH_DURATION * 3);
         end_epoch();
-        // Rewards rate has halved. Validator 1 and validator 2 should receive rewards at rewards rate = 0.5% every epoch.
-        assert_validator_state(validator_1_address, 1015, 0, 0, 0, 1);
-        assert_validator_state(validator_2_address, 10150, 0, 0, 0, 0);
+        // Validator 1 and validator 2 should still receive rewards at rewards rate = 1% every epoch. Rewards rate has halved after this epoch.
+        assert_validator_state(validator_1_address, 1020, 0, 0, 0, 1);
+        assert_validator_state(validator_2_address, 10200, 0, 0, 0, 0);
 
         // For some reason, this epoch is also very long. One year passed.
         timestamp::fast_forward_seconds(one_year_in_secs - EPOCH_DURATION);
+        end_epoch();
+        // Validator 1 and validator 2 should still receive rewards at rewards rate = 0.5% every epoch. Rewards rate has halved after this epoch.
+        assert_validator_state(validator_1_address, 1025, 0, 0, 0, 1);
+        assert_validator_state(validator_2_address, 10250, 0, 0, 0, 0);
+
         end_epoch();
         // Rewards rate has halved but cannot become lower than min_rewards_rate.
         // Validator 1 and validator 2 should receive rewards at rewards rate = 0.3% every epoch.
-        assert_validator_state(validator_1_address, 1018, 0, 0, 0, 1);
-        assert_validator_state(validator_2_address, 10180, 0, 0, 0, 0);
+        assert_validator_state(validator_1_address, 1028, 0, 0, 0, 1);
+        assert_validator_state(validator_2_address, 10280, 0, 0, 0, 0);
     }
 
     #[test(aptos_framework = @aptos_framework, validator = @0x123)]
diff --git a/aptos-move/framework/aptos-framework/sources/stake.spec.move b/aptos-move/framework/aptos-framework/sources/stake.spec.move
index a3b65abaf4392..1e59cd3968458 100644
--- a/aptos-move/framework/aptos-framework/sources/stake.spec.move
+++ b/aptos-move/framework/aptos-framework/sources/stake.spec.move
@@ -348,7 +348,7 @@ spec aptos_framework::stake {
         requires exists(@aptos_framework);
         requires exists(@aptos_framework);
         requires exists(@aptos_framework);
-        requires exists(@aptos_framework) || !features::spec_reward_rate_decrease_enabled();
+        requires exists(@aptos_framework) || !features::spec_periodical_reward_rate_decrease_enabled();
         requires exists(@aptos_framework);
         requires exists(@aptos_framework);
     }
diff --git a/aptos-move/framework/move-stdlib/doc/features.md b/aptos-move/framework/move-stdlib/doc/features.md
index b93db105c3f15..06feaf83ece60 100644
--- a/aptos-move/framework/move-stdlib/doc/features.md
+++ b/aptos-move/framework/move-stdlib/doc/features.md
@@ -1114,7 +1114,7 @@ Helper to check whether a feature flag is enabled.
 
 
pragma opaque;
 aborts_if [abstract] false;
-ensures [abstract] result == spec_reward_rate_decrease_enabled();
+ensures [abstract] result == spec_periodical_reward_rate_decrease_enabled();
 
@@ -1194,10 +1194,10 @@ Helper to check whether a feature flag is enabled. - + -
fun spec_reward_rate_decrease_enabled(): bool {
+
fun spec_periodical_reward_rate_decrease_enabled(): bool {
    spec_is_enabled(PERIODICAL_REWARD_RATE_DECREASE)
 }
 
diff --git a/aptos-move/framework/move-stdlib/sources/configs/features.spec.move b/aptos-move/framework/move-stdlib/sources/configs/features.spec.move index ca8cfda1d6cd4..696926524685b 100644 --- a/aptos-move/framework/move-stdlib/sources/configs/features.spec.move +++ b/aptos-move/framework/move-stdlib/sources/configs/features.spec.move @@ -37,14 +37,14 @@ spec std::features { spec fun spec_is_enabled(feature: u64): bool; - spec fun spec_reward_rate_decrease_enabled(): bool { + spec fun spec_periodical_reward_rate_decrease_enabled(): bool { spec_is_enabled(PERIODICAL_REWARD_RATE_DECREASE) } spec periodical_reward_rate_decrease_enabled { pragma opaque; aborts_if [abstract] false; - ensures [abstract] result == spec_reward_rate_decrease_enabled(); + ensures [abstract] result == spec_periodical_reward_rate_decrease_enabled(); } spec fun spec_partial_governance_voting_enabled(): bool {