Limit the upper bound of rewards_rate

This commit adds assertions and a spec to ensure `rewards_rate <= 10000`,
and `rewards_rate <= rewards_rate_denominator`.

aptos-move/framework/aptos-framework/sources/configs/staking_config.move

@@ -14,9 +14,11 @@ module aptos_framework::staking_config {
     const EINVALID_STAKE_RANGE: u64 = 3;
     /// The voting power increase limit percentage must be within (0, 50].
     const EINVALID_VOTING_POWER_INCREASE_LIMIT: u64 = 4;
-    /// Specified rewards rate is invalid, which must be within [0, 100).
+    /// Specified rewards rate is invalid, which must be within [0, MAX_REWARDS_RATE].
     const EINVALID_REWARDS_RATE: u64 = 5;
 
+    /// Limit the maximum value of `rewards_rate` in order to avoid any arithmetic overflow.
+    const MAX_REWARDS_RATE: u64 = 10000;
 
     /// Validator set configurations that will be stored with the @aptos_framework account.
     struct StakingConfig has copy, drop, key {
@@ -68,6 +70,14 @@ module aptos_framework::staking_config {
             error::invalid_argument(EINVALID_VOTING_POWER_INCREASE_LIMIT),
         );
 
+        // `rewards_rate` which is the numerator is limited to be `<= MAX_REWARDS_RATE` in order to avoid the arithmetic
+        // overflow in the rewards calculation. `rewards_rate_denominator` can be adjusted to get the desired rewards
+        // rate (i.e., rewards_rate / rewards_rate_denominator).
+        assert!(rewards_rate <= MAX_REWARDS_RATE, error::invalid_argument(EINVALID_REWARDS_RATE));
+
+        // We assert that (rewards_rate / rewards_rate_denominator <= 1).
+        assert!(rewards_rate <= rewards_rate_denominator, error::invalid_argument(EINVALID_REWARDS_RATE));
+
         move_to(aptos_framework, StakingConfig {
             minimum_stake,
             maximum_stake,
@@ -149,6 +159,14 @@ module aptos_framework::staking_config {
             new_rewards_rate_denominator > 0,
             error::invalid_argument(EZERO_REWARDS_RATE_DENOMINATOR),
         );
+        // `rewards_rate` which is the numerator is limited to be `<= MAX_REWARDS_RATE` in order to avoid the arithmetic
+        // overflow in the rewards calculation. `rewards_rate_denominator` can be adjusted to get the desired rewards
+        // rate (i.e., rewards_rate / rewards_rate_denominator).
+        assert!(new_rewards_rate <= MAX_REWARDS_RATE, error::invalid_argument(EINVALID_REWARDS_RATE));
+
+        // We assert that (rewards_rate / rewards_rate_denominator <= 1).
+        assert!(new_rewards_rate <= new_rewards_rate_denominator, error::invalid_argument(EINVALID_REWARDS_RATE));
+
         let staking_config = borrow_global_mut<StakingConfig>(@aptos_framework);
         staking_config.rewards_rate = new_rewards_rate;
         staking_config.rewards_rate_denominator = new_rewards_rate_denominator;

aptos-move/framework/aptos-framework/sources/configs/staking_config.spec.move

@@ -3,4 +3,12 @@ spec aptos_framework::staking_config {
         use aptos_framework::chain_status;
         invariant chain_status::is_operating() ==> exists<StakingConfig>(@aptos_framework);
     }
+    spec StakingConfig {
+        // `rewards_rate` which is the numerator is limited to be `<= MAX_REWARDS_RATE` in order to avoid the arithmetic
+        // overflow in the rewards calculation. `rewards_rate_denominator` can be adjusted to get the desired rewards
+        // rate (i.e., rewards_rate / rewards_rate_denominator).
+        invariant rewards_rate <= MAX_REWARDS_RATE;
+        invariant rewards_rate_denominator > 0;
+        invariant rewards_rate <= rewards_rate_denominator;
+    }
 }

aptos-move/framework/aptos-framework/sources/stake.move

@@ -83,6 +83,12 @@ module aptos_framework::stake {
     /// https://github.com/aptos-labs/aptos-core/blob/main/crates/aptos-bitvec/src/lib.rs#L20
     const MAX_VALIDATOR_SET_SIZE: u64 = 65536;
 
+    /// Limit the maximum value of `rewards_rate` in order to avoid any arithmetic overflow.
+    const MAX_REWARDS_RATE: u64 = 10000;
+
+    /// The maximum value of u64 as u128.
+    const MAX_U64: u128 = 18446744073709551615;
+
     /// Capability that represents ownership and can be used to control the validator and the associated stake pool.
     /// Having this be separate from the signer for the account that the validator resources are hosted at allows
     /// modules to have control over a validator.
@@ -1158,6 +1164,12 @@ module aptos_framework::stake {
         rewards_rate: u64,
         rewards_rate_denominator: u64,
     ): u64 {
+        spec {
+            assume num_successful_proposals <= num_total_proposals;
+            // We assume that num_successful_proposals < 86400 (1 proposal per second in a day).
+            // Even in the worst case, the following condition must hold.
+            assume num_successful_proposals * MAX_REWARDS_RATE <= MAX_U64;
+        };
         // The rewards amount is equal to (stake amount * rewards rate * performance multiplier).
         // We do multiplication in u128 before division to avoid the overflow and minimize the rounding error.
         let rewards_numerator = (stake_amount as u128) * (rewards_rate as u128) * (num_successful_proposals as u128);

aptos-move/framework/aptos-framework/sources/stake.spec.move

@@ -53,6 +53,9 @@ spec aptos_framework::stake {
 
     spec distribute_rewards {
         include ResourceRequirement;
+        requires rewards_rate <= MAX_REWARDS_RATE;
+        requires rewards_rate_denominator > 0;
+        requires rewards_rate <= rewards_rate_denominator;
         aborts_if false;
         ensures old(stake.value) > 0 ==>
                 result == spec_rewards_amount(
@@ -74,13 +77,17 @@ spec aptos_framework::stake {
 
     spec calculate_rewards_amount {
         pragma opaque;
+        requires rewards_rate <= MAX_REWARDS_RATE;
+        requires rewards_rate_denominator > 0;
+        requires rewards_rate <= rewards_rate_denominator;
         ensures [concrete] (rewards_rate_denominator * num_total_proposals == 0) ==> result == 0;
-        ensures [concrete] (rewards_rate_denominator * num_total_proposals > 0) ==>
-            result == ((stake_amount * rewards_rate * num_successful_proposals) /
+        ensures [concrete] (rewards_rate_denominator * num_total_proposals > 0) ==> {
+            let amount = ((stake_amount * rewards_rate * num_successful_proposals) /
                 (rewards_rate_denominator * num_total_proposals));
-        // We assume that rewards_rate < 100 and num_successful_proposals < 86400 (1 proposal per second in a day).
-        // So, the multiplication in the reward formula should not overflow.
-        aborts_if [abstract] false;
+            result == amount
+        };
+        aborts_if false;
+
         // Used an uninterpreted spec function to avoid dealing with the arithmetic overflow and non-linear arithmetic.
         ensures [abstract] result == spec_rewards_amount(
             stake_amount,