staking_config - [mainnet]

Provides the configuration for staking and rewards

use 0x1::error;
use 0x1::features;
use 0x1::fixed_point64;
use 0x1::math_fixed64;
use 0x1::system_addresses;
use 0x1::timestamp;

Constants

const MAX_U64: u128 = 18446744073709551615;

The function has been deprecated.

const EDEPRECATED_FUNCTION: u64 = 10;

Denominator of number in basis points. 1 bps(basis points) = 0.01%.

const BPS_DENOMINATOR: u64 = 10000;

The function is disabled or hasn’t been enabled.

const EDISABLED_FUNCTION: u64 = 11;

Specified start time of last rewards rate period is invalid, which must be not late than the current timestamp.

const EINVALID_LAST_REWARDS_RATE_PERIOD_START: u64 = 7;

Specified min rewards rate is invalid, which must be within [0, rewards_rate].

const EINVALID_MIN_REWARDS_RATE: u64 = 6;

Specified rewards rate is invalid, which must be within [0, MAX_REWARDS_RATE].

const EINVALID_REWARDS_RATE: u64 = 5;

Specified rewards rate decrease rate is invalid, which must be not greater than BPS_DENOMINATOR.

const EINVALID_REWARDS_RATE_DECREASE_RATE: u64 = 8;

Specified rewards rate period is invalid. It must be larger than 0 and cannot be changed if configured.

const EINVALID_REWARDS_RATE_PERIOD: u64 = 9;

Specified stake range is invalid. Max must be greater than min.

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;

Stake lockup duration cannot be zero.

const EZERO_LOCKUP_DURATION: u64 = 1;

Reward rate denominator cannot be zero.

const EZERO_REWARDS_RATE_DENOMINATOR: u64 = 2;

Limit the maximum value of rewards_rate in order to avoid any arithmetic overflow.

const MAX_REWARDS_RATE: u64 = 1000000;

1 year => 365 * 24 * 60 * 60

const ONE_YEAR_IN_SECS: u64 = 31536000;

Resources

`StakingConfig`

Validator set configurations that will be stored with the @aptos_framework account.

struct StakingConfig has copy, drop, key

Fields

minimum_stake: u64
maximum_stake: u64
recurring_lockup_duration_secs: u64
allow_validator_set_change: bool
rewards_rate: u64
rewards_rate_denominator: u64
voting_power_increase_limit: u64

`StakingRewardsConfig`

Staking reward configurations that will be stored with the @aptos_framework account.

struct StakingRewardsConfig has copy, drop, key

Fields

rewards_rate: fixed_point64::FixedPoint64
min_rewards_rate: fixed_point64::FixedPoint64
rewards_rate_period_in_secs: u64
last_rewards_rate_period_start_in_secs: u64
rewards_rate_decrease_rate: fixed_point64::FixedPoint64

Functions

`initialize`

Only called during genesis.

public(friend) fun initialize(aptos_framework: &signer, minimum_stake: u64, maximum_stake: u64, recurring_lockup_duration_secs: u64, allow_validator_set_change: bool, rewards_rate: u64, rewards_rate_denominator: u64, voting_power_increase_limit: u64)

Implementation

public(friend) fun initialize(
    aptos_framework: &signer,
    minimum_stake: u64,
    maximum_stake: u64,
    recurring_lockup_duration_secs: u64,
    allow_validator_set_change: bool,
    rewards_rate: u64,
    rewards_rate_denominator: u64,
    voting_power_increase_limit: u64,
) {
    system_addresses::assert_aptos_framework(aptos_framework);

    // This can fail genesis but is necessary so that any misconfigurations can be corrected before genesis succeeds
    validate_required_stake(minimum_stake, maximum_stake);

    assert!(recurring_lockup_duration_secs > 0, error::invalid_argument(EZERO_LOCKUP_DURATION));
    assert!(
        rewards_rate_denominator > 0,
        error::invalid_argument(EZERO_REWARDS_RATE_DENOMINATOR),
    );
    assert!(
        voting_power_increase_limit > 0 && voting_power_increase_limit <= 50,
        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,
        recurring_lockup_duration_secs,
        allow_validator_set_change,
        rewards_rate,
        rewards_rate_denominator,
        voting_power_increase_limit,
    });

    // Initialize StakingRewardsConfig with the given rewards_rate and rewards_rate_denominator,
    // while setting min_rewards_rate and rewards_rate_decrease_rate to 0.
    initialize_rewards(
        aptos_framework,
        fixed_point64::create_from_rational((rewards_rate as u128), (rewards_rate_denominator as u128)),
        fixed_point64::create_from_rational(0, 1000),
        ONE_YEAR_IN_SECS,
        0,
        fixed_point64::create_from_rational(0, 1000),
    );
}

`reward_rate`

Return the reward rate of this epoch as a tuple (numerator, denominator).

#[view]
public fun reward_rate(): (u64, u64)

Implementation

public fun reward_rate(): (u64, u64) acquires StakingRewardsConfig, StakingConfig {
    get_reward_rate(borrow_global<StakingConfig>(@aptos_framework))
}

`initialize_rewards`

Initialize rewards configurations. Can only be called as part of the Aptos governance proposal process established by the AptosGovernance module.

public fun initialize_rewards(aptos_framework: &signer, rewards_rate: fixed_point64::FixedPoint64, min_rewards_rate: fixed_point64::FixedPoint64, rewards_rate_period_in_secs: u64, last_rewards_rate_period_start_in_secs: u64, rewards_rate_decrease_rate: fixed_point64::FixedPoint64)

Implementation

public fun initialize_rewards(
    aptos_framework: &signer,
    rewards_rate: FixedPoint64,
    min_rewards_rate: FixedPoint64,
    rewards_rate_period_in_secs: u64,
    last_rewards_rate_period_start_in_secs: u64,
    rewards_rate_decrease_rate: FixedPoint64,
) {
    system_addresses::assert_aptos_framework(aptos_framework);

    validate_rewards_config(
        rewards_rate,
        min_rewards_rate,
        rewards_rate_period_in_secs,
        rewards_rate_decrease_rate,
    );
    assert!(
        timestamp::now_seconds() >= last_rewards_rate_period_start_in_secs,
        error::invalid_argument(EINVALID_LAST_REWARDS_RATE_PERIOD_START)
    );

    move_to(aptos_framework, StakingRewardsConfig {
        rewards_rate,
        min_rewards_rate,
        rewards_rate_period_in_secs,
        last_rewards_rate_period_start_in_secs,
        rewards_rate_decrease_rate,
    });
}

`get`

public fun get(): staking_config::StakingConfig

Implementation

public fun get(): StakingConfig acquires StakingConfig {
    *borrow_global<StakingConfig>(@aptos_framework)
}

`get_allow_validator_set_change`

Return whether validator set changes are allowed

public fun get_allow_validator_set_change(config: &staking_config::StakingConfig): bool

Implementation

public fun get_allow_validator_set_change(config: &StakingConfig): bool {
    config.allow_validator_set_change
}

`get_required_stake`

Return the required min/max stake.

public fun get_required_stake(config: &staking_config::StakingConfig): (u64, u64)

Implementation

public fun get_required_stake(config: &StakingConfig): (u64, u64) {
    (config.minimum_stake, config.maximum_stake)
}

`get_recurring_lockup_duration`

Return the recurring lockup duration that every validator is automatically renewed for (unless they unlock and withdraw all funds).

public fun get_recurring_lockup_duration(config: &staking_config::StakingConfig): u64

Implementation

public fun get_recurring_lockup_duration(config: &StakingConfig): u64 {
    config.recurring_lockup_duration_secs
}

`get_reward_rate`

Return the reward rate of this epoch.

public fun get_reward_rate(config: &staking_config::StakingConfig): (u64, u64)

Implementation

public fun get_reward_rate(config: &StakingConfig): (u64, u64) acquires StakingRewardsConfig {
    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)
    }
}

`get_voting_power_increase_limit`

Return the joining limit %.

public fun get_voting_power_increase_limit(config: &staking_config::StakingConfig): u64

Implementation

public fun get_voting_power_increase_limit(config: &StakingConfig): u64 {
    config.voting_power_increase_limit
}

`calculate_and_save_latest_epoch_rewards_rate`

Calculate and save the latest rewards rate.

public(friend) fun calculate_and_save_latest_epoch_rewards_rate(): fixed_point64::FixedPoint64

Implementation

public(friend) fun calculate_and_save_latest_epoch_rewards_rate(): FixedPoint64 acquires StakingRewardsConfig {
    assert!(features::periodical_reward_rate_decrease_enabled(), error::invalid_state(EDISABLED_FUNCTION));
    let staking_rewards_config = calculate_and_save_latest_rewards_config();
    staking_rewards_config.rewards_rate
}

`calculate_and_save_latest_rewards_config`

Calculate and return the up-to-date StakingRewardsConfig.

fun calculate_and_save_latest_rewards_config(): staking_config::StakingRewardsConfig

Implementation

fun calculate_and_save_latest_rewards_config(): StakingRewardsConfig acquires StakingRewardsConfig {
    let staking_rewards_config = borrow_global_mut<StakingRewardsConfig>(@aptos_framework);
    let current_time_in_secs = timestamp::now_seconds();
    assert!(
        current_time_in_secs >= staking_rewards_config.last_rewards_rate_period_start_in_secs,
        error::invalid_argument(EINVALID_LAST_REWARDS_RATE_PERIOD_START)
    );
    if (current_time_in_secs - staking_rewards_config.last_rewards_rate_period_start_in_secs < staking_rewards_config.rewards_rate_period_in_secs) {
        return *staking_rewards_config
    };
    // Rewards rate decrease rate cannot be greater than 100%. Otherwise rewards rate will be negative.
    assert!(
        fixed_point64::ceil(staking_rewards_config.rewards_rate_decrease_rate) <= 1,
        error::invalid_argument(EINVALID_REWARDS_RATE_DECREASE_RATE)
    );
    let new_rate = math_fixed64::mul_div(
        staking_rewards_config.rewards_rate,
        fixed_point64::sub(
            fixed_point64::create_from_u128(1),
            staking_rewards_config.rewards_rate_decrease_rate,
        ),
        fixed_point64::create_from_u128(1),
    );
    new_rate = fixed_point64::max(new_rate, staking_rewards_config.min_rewards_rate);

    staking_rewards_config.rewards_rate = new_rate;
    staking_rewards_config.last_rewards_rate_period_start_in_secs =
        staking_rewards_config.last_rewards_rate_period_start_in_secs +
        staking_rewards_config.rewards_rate_period_in_secs;
    return *staking_rewards_config
}

`update_required_stake`

Update the min and max stake amounts. Can only be called as part of the Aptos governance proposal process established by the AptosGovernance module.

public fun update_required_stake(aptos_framework: &signer, minimum_stake: u64, maximum_stake: u64)

Implementation

public fun update_required_stake(
    aptos_framework: &signer,
    minimum_stake: u64,
    maximum_stake: u64,
) acquires StakingConfig {
    system_addresses::assert_aptos_framework(aptos_framework);
    validate_required_stake(minimum_stake, maximum_stake);

    let staking_config = borrow_global_mut<StakingConfig>(@aptos_framework);
    staking_config.minimum_stake = minimum_stake;
    staking_config.maximum_stake = maximum_stake;
}

`update_recurring_lockup_duration_secs`

Update the recurring lockup duration. Can only be called as part of the Aptos governance proposal process established by the AptosGovernance module.

public fun update_recurring_lockup_duration_secs(aptos_framework: &signer, new_recurring_lockup_duration_secs: u64)

Implementation

public fun update_recurring_lockup_duration_secs(
    aptos_framework: &signer,
    new_recurring_lockup_duration_secs: u64,
) acquires StakingConfig {
    assert!(new_recurring_lockup_duration_secs > 0, error::invalid_argument(EZERO_LOCKUP_DURATION));
    system_addresses::assert_aptos_framework(aptos_framework);

    let staking_config = borrow_global_mut<StakingConfig>(@aptos_framework);
    staking_config.recurring_lockup_duration_secs = new_recurring_lockup_duration_secs;
}

`update_rewards_rate`

DEPRECATING Update the rewards rate. Can only be called as part of the Aptos governance proposal process established by the AptosGovernance module.

public fun update_rewards_rate(aptos_framework: &signer, new_rewards_rate: u64, new_rewards_rate_denominator: u64)

Implementation

public fun update_rewards_rate(
    aptos_framework: &signer,
    new_rewards_rate: u64,
    new_rewards_rate_denominator: u64,
) acquires StakingConfig {
    assert!(!features::periodical_reward_rate_decrease_enabled(), error::invalid_state(EDEPRECATED_FUNCTION));
    system_addresses::assert_aptos_framework(aptos_framework);
    assert!(
        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;
}

`update_rewards_config`

public fun update_rewards_config(aptos_framework: &signer, rewards_rate: fixed_point64::FixedPoint64, min_rewards_rate: fixed_point64::FixedPoint64, rewards_rate_period_in_secs: u64, rewards_rate_decrease_rate: fixed_point64::FixedPoint64)

Implementation

public fun update_rewards_config(
    aptos_framework: &signer,
    rewards_rate: FixedPoint64,
    min_rewards_rate: FixedPoint64,
    rewards_rate_period_in_secs: u64,
    rewards_rate_decrease_rate: FixedPoint64,
) acquires StakingRewardsConfig {
    system_addresses::assert_aptos_framework(aptos_framework);

    validate_rewards_config(
        rewards_rate,
        min_rewards_rate,
        rewards_rate_period_in_secs,
        rewards_rate_decrease_rate,
    );

    let staking_rewards_config = borrow_global_mut<StakingRewardsConfig>(@aptos_framework);
    // Currently rewards_rate_period_in_secs is not allowed to be changed because this could bring complicated
    // logics. At the moment the argument is just a placeholder for future use.
    assert!(
        rewards_rate_period_in_secs == staking_rewards_config.rewards_rate_period_in_secs,
        error::invalid_argument(EINVALID_REWARDS_RATE_PERIOD),
    );
    staking_rewards_config.rewards_rate = rewards_rate;
    staking_rewards_config.min_rewards_rate = min_rewards_rate;
    staking_rewards_config.rewards_rate_period_in_secs = rewards_rate_period_in_secs;
    staking_rewards_config.rewards_rate_decrease_rate = rewards_rate_decrease_rate;
}

`update_voting_power_increase_limit`

Update the joining limit %. Can only be called as part of the Aptos governance proposal process established by the AptosGovernance module.

public fun update_voting_power_increase_limit(aptos_framework: &signer, new_voting_power_increase_limit: u64)

Implementation

public fun update_voting_power_increase_limit(
    aptos_framework: &signer,
    new_voting_power_increase_limit: u64,
) acquires StakingConfig {
    system_addresses::assert_aptos_framework(aptos_framework);
    assert!(
        new_voting_power_increase_limit > 0 && new_voting_power_increase_limit <= 50,
        error::invalid_argument(EINVALID_VOTING_POWER_INCREASE_LIMIT),
    );

    let staking_config = borrow_global_mut<StakingConfig>(@aptos_framework);
    staking_config.voting_power_increase_limit = new_voting_power_increase_limit;
}

`validate_required_stake`

fun validate_required_stake(minimum_stake: u64, maximum_stake: u64)

Implementation

fun validate_required_stake(minimum_stake: u64, maximum_stake: u64) {
    assert!(minimum_stake <= maximum_stake && maximum_stake > 0, error::invalid_argument(EINVALID_STAKE_RANGE));
}

`validate_rewards_config`

fun validate_rewards_config(rewards_rate: fixed_point64::FixedPoint64, min_rewards_rate: fixed_point64::FixedPoint64, rewards_rate_period_in_secs: u64, rewards_rate_decrease_rate: fixed_point64::FixedPoint64)

Implementation

fun validate_rewards_config(
    rewards_rate: FixedPoint64,
    min_rewards_rate: FixedPoint64,
    rewards_rate_period_in_secs: u64,
    rewards_rate_decrease_rate: FixedPoint64,
) {
    // Bound rewards rate to avoid arithmetic overflow.
    assert!(
        less_or_equal(rewards_rate, fixed_point64::create_from_u128((1u128))),
        error::invalid_argument(EINVALID_REWARDS_RATE)
    );
    assert!(
        less_or_equal(min_rewards_rate, rewards_rate),
        error::invalid_argument(EINVALID_MIN_REWARDS_RATE)
    );
    // Rewards rate decrease rate cannot be greater than 100%. Otherwise rewards rate will be negative.
    assert!(
        fixed_point64::ceil(rewards_rate_decrease_rate) <= 1,
        error::invalid_argument(EINVALID_REWARDS_RATE_DECREASE_RATE)
    );
    // This field, rewards_rate_period_in_secs must be greater than 0.
    // TODO: rewards_rate_period_in_secs should be longer than the epoch duration but reading epoch duration causes a circular dependency.
    assert!(
        rewards_rate_period_in_secs > 0,
        error::invalid_argument(EINVALID_REWARDS_RATE_PERIOD),
    );
}

Specification

High-level Requirements

No.	Requirement	Criticality	Implementation	Enforcement
1	The ability to initialize the staking config and staking rewards resources, as well as the ability to update the staking config and staking rewards should only be available to the Aptos framework account.	Medium	The function initialize and initialize_rewards are used to initialize the StakingConfig and StakingRewardConfig resources. Updating the resources, can be done using the update_required_stake, update_recurring_lockup_duration_secs, update_rewards_rate, update_rewards_config, update_voting_power_increase_limit functions, which ensure that the signer is aptos_framework using the assert_aptos_framework function.	Verified via initialize, initialize_rewards, update_required_stake, update_recurring_lockup_duration_secs, update_rewards_rate, update_rewards_config, and update_voting_power_increase_limit.
2	The voting power increase, in a staking config resource, should always be greater than 0 and less or equal to 50.	High	During the initialization and update of the staking config, the value of voting_power_increase_limit is ensured to be in the range of (0 to 50].	Ensured via initialize and update_voting_power_increase_limit. Formally verified via StakingConfig.
3	The recurring lockup duration, in a staking config resource, should always be greater than 0.	Medium	During the initialization and update of the staking config, the value of recurring_lockup_duration_secs is ensured to be greater than 0.	Ensured via initialize and update_recurring_lockup_duration_secs. Formally verified via StakingConfig.
4	The calculation of rewards should not be possible if the last reward rate period just started.	High	The function calculate_and_save_latest_rewards_config ensures that last_rewards_rate_period_start_in_secs is greater or equal to the current timestamp.	Formally verified in StakingRewardsConfigEnabledRequirement.
5	The rewards rate should always be less than or equal to 100%.	High	When initializing and updating the rewards rate, it is ensured that the rewards_rate is less or equal to MAX_REWARDS_RATE, otherwise rewards rate will be negative.	Verified via StakingConfig.
6	The reward rate's denominator should never be 0.	High	While initializing and updating the rewards rate, rewards_rate_denominator is ensured to be greater than 0.	Verified via StakingConfig.
7	The reward rate's nominator and dominator ratio should always be less or equal to 1.	High	When initializing and updating the rewards rate, it is ensured that rewards_rate is less or equal to rewards_rate_denominator.	Verified via StakingConfig.

Module-level Specification

invariant [suspendable] chain_status::is_operating() ==> exists<StakingConfig>(@aptos_framework);
invariant [suspendable] chain_status::is_operating() ==> exists<StakingRewardsConfig>(@aptos_framework);
pragma verify = true;
pragma aborts_if_is_strict;

`StakingConfig`

struct StakingConfig has copy, drop, key

minimum_stake: u64
maximum_stake: u64
recurring_lockup_duration_secs: u64
allow_validator_set_change: bool
rewards_rate: u64
rewards_rate_denominator: u64
voting_power_increase_limit: u64

// This enforces high-level requirement 5:
invariant rewards_rate <= MAX_REWARDS_RATE;
// This enforces high-level requirement 6:
invariant rewards_rate_denominator > 0;
// This enforces high-level requirement 7:
invariant rewards_rate <= rewards_rate_denominator;
// This enforces high-level requirement 3:
invariant recurring_lockup_duration_secs > 0;
// This enforces high-level requirement 2:
invariant voting_power_increase_limit > 0 && voting_power_increase_limit <= 50;

`StakingRewardsConfig`

struct StakingRewardsConfig has copy, drop, key

rewards_rate: fixed_point64::FixedPoint64
min_rewards_rate: fixed_point64::FixedPoint64
rewards_rate_period_in_secs: u64
last_rewards_rate_period_start_in_secs: u64
rewards_rate_decrease_rate: fixed_point64::FixedPoint64

invariant fixed_point64::spec_less_or_equal(
    rewards_rate,
    fixed_point64::spec_create_from_u128((1u128)));
invariant fixed_point64::spec_less_or_equal(min_rewards_rate, rewards_rate);
invariant rewards_rate_period_in_secs > 0;
invariant fixed_point64::spec_ceil(rewards_rate_decrease_rate) <= 1;

`initialize`

public(friend) fun initialize(aptos_framework: &signer, minimum_stake: u64, maximum_stake: u64, recurring_lockup_duration_secs: u64, allow_validator_set_change: bool, rewards_rate: u64, rewards_rate_denominator: u64, voting_power_increase_limit: u64)

Caller must be @aptos_framework. The maximum_stake must be greater than maximum_stake in the range of Specified stake and the maximum_stake greater than zero. The rewards_rate_denominator must greater than zero. Only this %0-%50 of current total voting power is allowed to join the validator set in each epoch. The 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/rewards_rate_denominator <= 1. StakingConfig does not exist under the aptos_framework before creating it.

let addr = signer::address_of(aptos_framework);
requires exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework);
// This enforces high-level requirement 1:
aborts_if addr != @aptos_framework;
aborts_if minimum_stake > maximum_stake || maximum_stake == 0;
// This enforces high-level requirement 3:
aborts_if recurring_lockup_duration_secs == 0;
aborts_if rewards_rate_denominator == 0;
// This enforces high-level requirement 2:
aborts_if voting_power_increase_limit == 0 || voting_power_increase_limit > 50;
aborts_if rewards_rate > MAX_REWARDS_RATE;
aborts_if rewards_rate > rewards_rate_denominator;
aborts_if exists<StakingConfig>(addr);
aborts_if exists<StakingRewardsConfig>(addr);
ensures exists<StakingConfig>(addr);
ensures exists<StakingRewardsConfig>(addr);

`reward_rate`

#[view]
public fun reward_rate(): (u64, u64)

let config = global<StakingConfig>(@aptos_framework);
aborts_if !exists<StakingConfig>(@aptos_framework);
include StakingRewardsConfigRequirement;
ensures (features::spec_periodical_reward_rate_decrease_enabled() &&
    (global<StakingRewardsConfig>(@aptos_framework).rewards_rate.value as u64) != 0) ==>
    result_1 <= MAX_REWARDS_RATE && result_2 <= MAX_U64;

`initialize_rewards`

public fun initialize_rewards(aptos_framework: &signer, rewards_rate: fixed_point64::FixedPoint64, min_rewards_rate: fixed_point64::FixedPoint64, rewards_rate_period_in_secs: u64, last_rewards_rate_period_start_in_secs: u64, rewards_rate_decrease_rate: fixed_point64::FixedPoint64)

Caller must be @aptos_framework. last_rewards_rate_period_start_in_secs cannot be later than now. Abort at any condition in StakingRewardsConfigValidationAborts. StakingRewardsConfig does not exist under the aptos_framework before creating it.

pragma verify_duration_estimate = 120;
requires exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework);
let addr = signer::address_of(aptos_framework);
// This enforces high-level requirement 1:
aborts_if addr != @aptos_framework;
aborts_if last_rewards_rate_period_start_in_secs > timestamp::spec_now_seconds();
include StakingRewardsConfigValidationAbortsIf;
aborts_if exists<StakingRewardsConfig>(addr);
ensures exists<StakingRewardsConfig>(addr);

`get`

public fun get(): staking_config::StakingConfig

aborts_if !exists<StakingConfig>(@aptos_framework);

`get_reward_rate`

public fun get_reward_rate(config: &staking_config::StakingConfig): (u64, u64)

include StakingRewardsConfigRequirement;
ensures (features::spec_periodical_reward_rate_decrease_enabled() &&
    (global<StakingRewardsConfig>(@aptos_framework).rewards_rate.value as u64) != 0) ==>
        result_1 <= MAX_REWARDS_RATE && result_2 <= MAX_U64;

`calculate_and_save_latest_epoch_rewards_rate`

public(friend) fun calculate_and_save_latest_epoch_rewards_rate(): fixed_point64::FixedPoint64

pragma verify_duration_estimate = 120;
aborts_if !exists<StakingRewardsConfig>(@aptos_framework);
aborts_if !features::spec_periodical_reward_rate_decrease_enabled();
include StakingRewardsConfigRequirement;

`calculate_and_save_latest_rewards_config`

fun calculate_and_save_latest_rewards_config(): staking_config::StakingRewardsConfig

pragma verify_duration_estimate = 120;
requires features::spec_periodical_reward_rate_decrease_enabled();
include StakingRewardsConfigRequirement;
aborts_if !exists<StakingRewardsConfig>(@aptos_framework);

`update_required_stake`

public fun update_required_stake(aptos_framework: &signer, minimum_stake: u64, maximum_stake: u64)

Caller must be @aptos_framework. The maximum_stake must be greater than maximum_stake in the range of Specified stake and the maximum_stake greater than zero. The StakingConfig is under @aptos_framework.

let addr = signer::address_of(aptos_framework);
// This enforces high-level requirement 1:
aborts_if addr != @aptos_framework;
aborts_if minimum_stake > maximum_stake || maximum_stake == 0;
aborts_if !exists<StakingConfig>(@aptos_framework);
ensures global<StakingConfig>(@aptos_framework).minimum_stake == minimum_stake &&
    global<StakingConfig>(@aptos_framework).maximum_stake == maximum_stake;

`update_recurring_lockup_duration_secs`

public fun update_recurring_lockup_duration_secs(aptos_framework: &signer, new_recurring_lockup_duration_secs: u64)

Caller must be @aptos_framework. The new_recurring_lockup_duration_secs must greater than zero. The StakingConfig is under @aptos_framework.

let addr = signer::address_of(aptos_framework);
// This enforces high-level requirement 1:
aborts_if addr != @aptos_framework;
// This enforces high-level requirement 3:
aborts_if new_recurring_lockup_duration_secs == 0;
aborts_if !exists<StakingConfig>(@aptos_framework);
ensures global<StakingConfig>(@aptos_framework).recurring_lockup_duration_secs == new_recurring_lockup_duration_secs;

`update_rewards_rate`

public fun update_rewards_rate(aptos_framework: &signer, new_rewards_rate: u64, new_rewards_rate_denominator: u64)

Caller must be @aptos_framework. The new_rewards_rate_denominator must greater than zero. The StakingConfig is under @aptos_framework. The 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/rewards_rate_denominator <= 1.

aborts_if features::spec_periodical_reward_rate_decrease_enabled();
let addr = signer::address_of(aptos_framework);
// This enforces high-level requirement 1:
aborts_if addr != @aptos_framework;
aborts_if new_rewards_rate_denominator == 0;
aborts_if !exists<StakingConfig>(@aptos_framework);
aborts_if new_rewards_rate > MAX_REWARDS_RATE;
aborts_if new_rewards_rate > new_rewards_rate_denominator;
let post staking_config = global<StakingConfig>(@aptos_framework);
ensures staking_config.rewards_rate == new_rewards_rate;
ensures staking_config.rewards_rate_denominator == new_rewards_rate_denominator;

`update_rewards_config`

public fun update_rewards_config(aptos_framework: &signer, rewards_rate: fixed_point64::FixedPoint64, min_rewards_rate: fixed_point64::FixedPoint64, rewards_rate_period_in_secs: u64, rewards_rate_decrease_rate: fixed_point64::FixedPoint64)

Caller must be @aptos_framework. StakingRewardsConfig is under the @aptos_framework.

pragma verify_duration_estimate = 120;
include StakingRewardsConfigRequirement;
let addr = signer::address_of(aptos_framework);
// This enforces high-level requirement 1:
aborts_if addr != @aptos_framework;
aborts_if global<StakingRewardsConfig>(@aptos_framework).rewards_rate_period_in_secs != rewards_rate_period_in_secs;
include StakingRewardsConfigValidationAbortsIf;
aborts_if !exists<StakingRewardsConfig>(addr);
let post staking_rewards_config = global<StakingRewardsConfig>(@aptos_framework);
ensures staking_rewards_config.rewards_rate == rewards_rate;
ensures staking_rewards_config.min_rewards_rate == min_rewards_rate;
ensures staking_rewards_config.rewards_rate_period_in_secs == rewards_rate_period_in_secs;
ensures staking_rewards_config.rewards_rate_decrease_rate == rewards_rate_decrease_rate;

`update_voting_power_increase_limit`

public fun update_voting_power_increase_limit(aptos_framework: &signer, new_voting_power_increase_limit: u64)

Caller must be @aptos_framework. Only this %0-%50 of current total voting power is allowed to join the validator set in each epoch. The StakingConfig is under @aptos_framework.

let addr = signer::address_of(aptos_framework);
// This enforces high-level requirement 1:
aborts_if addr != @aptos_framework;
// This enforces high-level requirement 2:
aborts_if new_voting_power_increase_limit == 0 || new_voting_power_increase_limit > 50;
aborts_if !exists<StakingConfig>(@aptos_framework);
ensures global<StakingConfig>(@aptos_framework).voting_power_increase_limit == new_voting_power_increase_limit;

`validate_required_stake`

fun validate_required_stake(minimum_stake: u64, maximum_stake: u64)

The maximum_stake must be greater than maximum_stake in the range of Specified stake and the maximum_stake greater than zero.

aborts_if minimum_stake > maximum_stake || maximum_stake == 0;

`validate_rewards_config`

fun validate_rewards_config(rewards_rate: fixed_point64::FixedPoint64, min_rewards_rate: fixed_point64::FixedPoint64, rewards_rate_period_in_secs: u64, rewards_rate_decrease_rate: fixed_point64::FixedPoint64)

Abort at any condition in StakingRewardsConfigValidationAborts.

include StakingRewardsConfigValidationAbortsIf;

rewards_rate must be within [0, 1]. min_rewards_rate must be not greater than rewards_rate. rewards_rate_period_in_secs must be greater than 0. rewards_rate_decrease_rate must be within [0,1].

schema StakingRewardsConfigValidationAbortsIf {
    rewards_rate: FixedPoint64;
    min_rewards_rate: FixedPoint64;
    rewards_rate_period_in_secs: u64;
    rewards_rate_decrease_rate: FixedPoint64;
    aborts_if fixed_point64::spec_greater(
        rewards_rate,
        fixed_point64::spec_create_from_u128((1u128)));
    aborts_if fixed_point64::spec_greater(min_rewards_rate, rewards_rate);
    aborts_if rewards_rate_period_in_secs == 0;
    aborts_if fixed_point64::spec_ceil(rewards_rate_decrease_rate) > 1;
}

schema StakingRewardsConfigRequirement {
    requires exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework);
    include features::spec_periodical_reward_rate_decrease_enabled() ==> StakingRewardsConfigEnabledRequirement;
}

schema StakingRewardsConfigEnabledRequirement {
    requires exists<StakingRewardsConfig>(@aptos_framework);
    let staking_rewards_config = global<StakingRewardsConfig>(@aptos_framework);
    let rewards_rate = staking_rewards_config.rewards_rate;
    let min_rewards_rate = staking_rewards_config.min_rewards_rate;
    let rewards_rate_period_in_secs = staking_rewards_config.rewards_rate_period_in_secs;
    let last_rewards_rate_period_start_in_secs = staking_rewards_config.last_rewards_rate_period_start_in_secs;
    let rewards_rate_decrease_rate = staking_rewards_config.rewards_rate_decrease_rate;
    requires fixed_point64::spec_less_or_equal(
        rewards_rate,
        fixed_point64::spec_create_from_u128((1u128)));
    requires fixed_point64::spec_less_or_equal(min_rewards_rate, rewards_rate);
    requires rewards_rate_period_in_secs > 0;
    // This enforces high-level requirement 4:
    requires last_rewards_rate_period_start_in_secs <= timestamp::spec_now_seconds();
    requires fixed_point64::spec_ceil(rewards_rate_decrease_rate) <= 1;
}