pool_address: address

active: coin::Coin<aptos_coin::AptosCoin>

inactive: coin::Coin<aptos_coin::AptosCoin>

pending_active: coin::Coin<aptos_coin::AptosCoin>

pending_inactive: coin::Coin<aptos_coin::AptosCoin>

locked_until_secs: u64

operator_address: address

delegated_voter: address

initialize_validator_events: event::EventHandle<stake::RegisterValidatorCandidateEvent>

set_operator_events: event::EventHandle<stake::SetOperatorEvent>

add_stake_events: event::EventHandle<stake::AddStakeEvent>

reactivate_stake_events: event::EventHandle<stake::ReactivateStakeEvent>

rotate_consensus_key_events: event::EventHandle<stake::RotateConsensusKeyEvent>

update_network_and_fullnode_addresses_events: event::EventHandle<stake::UpdateNetworkAndFullnodeAddressesEvent>

increase_lockup_events: event::EventHandle<stake::IncreaseLockupEvent>

join_validator_set_events: event::EventHandle<stake::JoinValidatorSetEvent>

distribute_rewards_events: event::EventHandle<stake::DistributeRewardsEvent>

unlock_stake_events: event::EventHandle<stake::UnlockStakeEvent>

withdraw_stake_events: event::EventHandle<stake::WithdrawStakeEvent>

leave_validator_set_events: event::EventHandle<stake::LeaveValidatorSetEvent>

consensus_pubkey: vector<u8>

network_addresses: vector<u8>

fullnode_addresses: vector<u8>

validator_index: u64

addr: address

voting_power: u64

config: stake::ValidatorConfig

consensus_scheme: u8

active_validators: vector<stake::ValidatorInfo>

pending_inactive: vector<stake::ValidatorInfo>

pending_active: vector<stake::ValidatorInfo>

total_voting_power: u128

total_joining_power: u128

pending_fee_by_validator: big_ordered_map::BigOrderedMap<u64, aggregator_v2::Aggregator<u64>>

pool_address: address

fee_amount: u64

mint_cap: coin::MintCapability<aptos_coin::AptosCoin>

successful_proposals: u64

failed_proposals: u64

validators: vector<stake::IndividualValidatorPerformance>

validator_set: stake::ValidatorSet

is_liveness_fallback: bool

pool_address: address

dummy_field: bool

pool_address: address

pool_address: address

old_operator: address

new_operator: address

pool_address: address

old_operator: address

new_operator: address

pool_address: address

amount_added: u64

pool_address: address

amount_added: u64

pool_address: address

amount: u64

pool_address: address

amount: u64

pool_address: address

old_consensus_pubkey: vector<u8>

new_consensus_pubkey: vector<u8>

pool_address: address

old_consensus_pubkey: vector<u8>

new_consensus_pubkey: vector<u8>

pool_address: address

old_network_addresses: vector<u8>

new_network_addresses: vector<u8>

old_fullnode_addresses: vector<u8>

new_fullnode_addresses: vector<u8>

pool_address: address

old_network_addresses: vector<u8>

new_network_addresses: vector<u8>

old_fullnode_addresses: vector<u8>

new_fullnode_addresses: vector<u8>

pool_address: address

old_locked_until_secs: u64

new_locked_until_secs: u64

pool_address: address

old_locked_until_secs: u64

new_locked_until_secs: u64

pool_address: address

pool_address: address

pool_address: address

rewards_amount: u64

pool_address: address

rewards_amount: u64

pool_address: address

amount_unlocked: u64

pool_address: address

amount_unlocked: u64

pool_address: address

amount_withdrawn: u64

pool_address: address

amount_withdrawn: u64

pool_address: address

pool_address: address

minimum_stake: u64

emergency_validator_count: u64

total_emergency_voting_power: u128

fees_table: table::Table<address, coin::Coin<aptos_coin::AptosCoin>>

accounts: vector<address>

v: stake::ValidatorPerformance

v: option::Option<u64>

v: u64

v: u64

inline fun check_stake_permission(s: &signer) {
    assert!(
        permissioned_signer::check_permission_exists(s, StakeManagementPermission {}),
        error::permission_denied(ENO_STAKE_PERMISSION)
    );
}

public fun grant_permission(
    master: &signer, permissioned_signer: &signer
) {
    permissioned_signer::authorize_unlimited(
        master, permissioned_signer, StakeManagementPermission {}
    )
}

public fun get_lockup_secs(pool_address: address): u64 acquires StakePool {
    assert_stake_pool_exists(pool_address);
    borrow_global<StakePool>(pool_address).locked_until_secs
}

public fun get_remaining_lockup_secs(pool_address: address): u64 acquires StakePool {
    assert_stake_pool_exists(pool_address);
    let lockup_time = borrow_global<StakePool>(pool_address).locked_until_secs;
    if (lockup_time <= timestamp::now_seconds()) { 0 }
    else {
        lockup_time - timestamp::now_seconds()
    }
}

public fun get_stake(pool_address: address): (u64, u64, u64, u64) acquires StakePool {
    assert_stake_pool_exists(pool_address);
    let stake_pool = borrow_global<StakePool>(pool_address);
    (
        coin::value(&stake_pool.active),
        coin::value(&stake_pool.inactive),
        coin::value(&stake_pool.pending_active),
        coin::value(&stake_pool.pending_inactive)
    )
}

public fun get_validator_state(pool_address: address): u64 acquires ValidatorSet {
    let validator_set = borrow_global<ValidatorSet>(@aptos_framework);
    if (find_validator(&validator_set.pending_active, pool_address).is_some()) {
        VALIDATOR_STATUS_PENDING_ACTIVE
    } else if (find_validator(&validator_set.active_validators, pool_address).is_some()) {
        VALIDATOR_STATUS_ACTIVE
    } else if (find_validator(&validator_set.pending_inactive, pool_address).is_some()) {
        VALIDATOR_STATUS_PENDING_INACTIVE
    } else {
        VALIDATOR_STATUS_INACTIVE
    }
}

public fun get_current_epoch_voting_power(
    pool_address: address
): u64 acquires StakePool, ValidatorSet {
    assert_stake_pool_exists(pool_address);
    let validator_state = get_validator_state(pool_address);
    // Both active and pending inactive validators can still vote in the current epoch.
    if (validator_state == VALIDATOR_STATUS_ACTIVE
        || validator_state == VALIDATOR_STATUS_PENDING_INACTIVE) {
        let active_stake =
            coin::value(&borrow_global<StakePool>(pool_address).active);
        let pending_inactive_stake =
            coin::value(&borrow_global<StakePool>(pool_address).pending_inactive);
        active_stake + pending_inactive_stake
    } else { 0 }
}

public fun get_delegated_voter(pool_address: address): address acquires StakePool {
    assert_stake_pool_exists(pool_address);
    borrow_global<StakePool>(pool_address).delegated_voter
}

public fun get_operator(pool_address: address): address acquires StakePool {
    assert_stake_pool_exists(pool_address);
    borrow_global<StakePool>(pool_address).operator_address
}

public fun get_owned_pool_address(owner_cap: &OwnerCapability): address {
    owner_cap.pool_address
}

public fun owner_cap_exists(owner: address): bool {
    exists<OwnerCapability>(owner)
}

public fun get_pool_address_for_owner(owner: address): address acquires OwnerCapability {
    assert_owner_cap_exists(owner);
    OwnerCapability[owner].pool_address
}

public fun get_validator_index(pool_address: address): u64 acquires ValidatorConfig {
    assert_stake_pool_exists(pool_address);
    borrow_global<ValidatorConfig>(pool_address).validator_index
}

public fun get_current_epoch_proposal_counts(
    validator_index: u64
): (u64, u64) acquires ValidatorPerformance {
    let validator_performances =
        &borrow_global<ValidatorPerformance>(@aptos_framework).validators;
    let validator_performance = validator_performances.borrow(validator_index);
    (
        validator_performance.successful_proposals,
        validator_performance.failed_proposals
    )
}

public fun get_validator_config(
    pool_address: address
): (vector<u8>, vector<u8>, vector<u8>) acquires ValidatorConfig {
    assert_stake_pool_exists(pool_address);
    let validator_config = borrow_global<ValidatorConfig>(pool_address);
    (
        validator_config.consensus_pubkey,
        validator_config.network_addresses,
        validator_config.fullnode_addresses
    )
}

public fun stake_pool_exists(addr: address): bool {
    exists<StakePool>(addr)
}

public fun get_pending_transaction_fee(): vector<u64> acquires PendingTransactionFee {
    let result = vector::empty();
    let fee_table =
        &borrow_global<PendingTransactionFee>(@aptos_framework).pending_fee_by_validator;
    let num_validators = fee_table.compute_length();
    let i = 0;
    while (i < num_validators) {
        result.push_back(fee_table.borrow(&i).read());
        i += 1;
    };

    result
}

public(friend) fun initialize(aptos_framework: &signer) {
    system_addresses::assert_aptos_framework(aptos_framework);

    move_to(
        aptos_framework,
        ValidatorSet {
            consensus_scheme: 0,
            active_validators: vector::empty(),
            pending_active: vector::empty(),
            pending_inactive: vector::empty(),
            total_voting_power: 0,
            total_joining_power: 0
        }
    );

    move_to(aptos_framework, ValidatorPerformance { validators: vector::empty() });
}

public(friend) fun store_aptos_coin_mint_cap(
    aptos_framework: &signer, mint_cap: MintCapability<AptosCoin>
) {
    system_addresses::assert_aptos_framework(aptos_framework);
    move_to(aptos_framework, AptosCoinCapabilities { mint_cap })
}

public fun remove_validators(
    aptos_framework: &signer, validators: &vector<address>
) acquires ValidatorSet {
    assert_reconfig_not_in_progress();
    system_addresses::assert_aptos_framework(aptos_framework);
    let validator_set = borrow_global_mut<ValidatorSet>(@aptos_framework);
    let active_validators = &mut validator_set.active_validators;
    let pending_inactive = &mut validator_set.pending_inactive;
    spec {
        update ghost_active_num = len(active_validators);
        update ghost_pending_inactive_num = len(pending_inactive);
    };
    let len_validators = validators.length();
    let i = 0;
    // Remove each validator from the validator set.
    while ({
        spec {
            invariant i <= len_validators;
            invariant spec_validators_are_initialized(active_validators);
            invariant spec_validator_indices_are_valid(active_validators);
            invariant spec_validators_are_initialized(pending_inactive);
            invariant spec_validator_indices_are_valid(pending_inactive);
            invariant ghost_active_num + ghost_pending_inactive_num
                == len(active_validators) + len(pending_inactive);
        };
        i < len_validators
    }) {
        let validator = validators[i];
        let validator_index = find_validator(active_validators, validator);
        if (validator_index.is_some()) {
            let validator_info =
                active_validators.swap_remove(*validator_index.borrow());
            pending_inactive.push_back(validator_info);
            spec {
                update ghost_active_num = ghost_active_num - 1;
                update ghost_pending_inactive_num = ghost_pending_inactive_num + 1;
            };
        };
        i += 1;
    };
}

public fun initialize_pending_transaction_fee(framework: &signer) {
    system_addresses::assert_aptos_framework(framework);

    if (!exists<PendingTransactionFee>(@aptos_framework)) {
        move_to(
            framework,
            PendingTransactionFee {
                // The max leaf order is set to 10 because there is a existing limitation that a
                // resource can only have 10 aggregators at max.
                pending_fee_by_validator: big_ordered_map::new_with_config(
                    5, 10, true
                )
            }
        );
    }
}

public fun set_transaction_fee_limit_per_epoch_per_pool(
    framework: &signer, limit_octa: u64
) {
    system_addresses::assert_aptos_framework(framework);

    let config = TransactionFeeConfig::V0 {
        max_fee_octa_allowed_per_epoch_per_pool: limit_octa
    };

    set_transaction_fee_config(framework, config);
}

public fun set_transaction_fee_config(
    framework: &signer, config: TransactionFeeConfig
) acquires TransactionFeeConfig {
    system_addresses::assert_aptos_framework(framework);

    if (exists<TransactionFeeConfig>(@aptos_framework)) {
        *borrow_global_mut<TransactionFeeConfig>(@aptos_framework) = config;
    } else {
        move_to(framework, config);
    }
}

public(friend) fun record_fee(
    vm: &signer,
    fee_distribution_validator_indices: vector<u64>,
    fee_amounts_octa: vector<u64>
) acquires PendingTransactionFee {
    // Operational constraint: can only be invoked by the VM.
    system_addresses::assert_vm(vm);

    assert!(
        fee_distribution_validator_indices.length() == fee_amounts_octa.length()
    );

    let num_validators_to_distribute = fee_distribution_validator_indices.length();
    let pending_fee = borrow_global_mut<PendingTransactionFee>(@aptos_framework);
    let i = 0;
    while (i < num_validators_to_distribute) {
        let validator_index = fee_distribution_validator_indices[i];
        let fee_octa = fee_amounts_octa[i];
        pending_fee.pending_fee_by_validator.borrow_mut(&validator_index).add(
            fee_octa
        );
        i += 1;
    }
}

public entry fun initialize_stake_owner(
    owner: &signer,
    initial_stake_amount: u64,
    operator: address,
    voter: address
) acquires AllowedValidators, OwnerCapability, StakePool, ValidatorSet {
    check_stake_permission(owner);
    initialize_owner(owner);
    move_to(
        owner,
        ValidatorConfig {
            consensus_pubkey: vector::empty(),
            network_addresses: vector::empty(),
            fullnode_addresses: vector::empty(),
            validator_index: 0
        }
    );

    if (initial_stake_amount > 0) {
        add_stake(owner, initial_stake_amount);
    };

    let account_address = signer::address_of(owner);
    if (account_address != operator) {
        set_operator(owner, operator)
    };
    if (account_address != voter) {
        set_delegated_voter(owner, voter)
    };
}

public entry fun initialize_validator(
    account: &signer,
    consensus_pubkey: vector<u8>,
    proof_of_possession: vector<u8>,
    network_addresses: vector<u8>,
    fullnode_addresses: vector<u8>
) acquires AllowedValidators {
    check_stake_permission(account);
    // Checks the public key has a valid proof-of-possession to prevent rogue-key attacks.
    let pubkey_from_pop =
        &bls12381::public_key_from_bytes_with_pop(
            consensus_pubkey,
            &proof_of_possession_from_bytes(proof_of_possession)
        );
    assert!(
        pubkey_from_pop.is_some(), error::invalid_argument(EINVALID_PUBLIC_KEY)
    );

    initialize_owner(account);
    move_to(
        account,
        ValidatorConfig {
            consensus_pubkey,
            network_addresses,
            fullnode_addresses,
            validator_index: 0
        }
    );
}

fun initialize_owner(owner: &signer) acquires AllowedValidators {
    check_stake_permission(owner);
    let owner_address = signer::address_of(owner);
    assert!(is_allowed(owner_address), error::not_found(EINELIGIBLE_VALIDATOR));
    assert!(
        !stake_pool_exists(owner_address),
        error::already_exists(EALREADY_REGISTERED)
    );

    move_to(
        owner,
        StakePool {
            active: coin::zero<AptosCoin>(),
            pending_active: coin::zero<AptosCoin>(),
            pending_inactive: coin::zero<AptosCoin>(),
            inactive: coin::zero<AptosCoin>(),
            locked_until_secs: 0,
            operator_address: owner_address,
            delegated_voter: owner_address,
            // Events.
            initialize_validator_events: account::new_event_handle<
                RegisterValidatorCandidateEvent>(owner),
            set_operator_events: account::new_event_handle<SetOperatorEvent>(owner),
            add_stake_events: account::new_event_handle<AddStakeEvent>(owner),
            reactivate_stake_events: account::new_event_handle<ReactivateStakeEvent>(
                owner
            ),
            rotate_consensus_key_events: account::new_event_handle<
                RotateConsensusKeyEvent>(owner),
            update_network_and_fullnode_addresses_events: account::new_event_handle<
                UpdateNetworkAndFullnodeAddressesEvent>(owner),
            increase_lockup_events: account::new_event_handle<IncreaseLockupEvent>(
                owner
            ),
            join_validator_set_events: account::new_event_handle<JoinValidatorSetEvent>(
                owner
            ),
            distribute_rewards_events: account::new_event_handle<DistributeRewardsEvent>(
                owner
            ),
            unlock_stake_events: account::new_event_handle<UnlockStakeEvent>(owner),
            withdraw_stake_events: account::new_event_handle<WithdrawStakeEvent>(owner),
            leave_validator_set_events: account::new_event_handle<
                LeaveValidatorSetEvent>(owner)
        }
    );

    move_to(owner, OwnerCapability { pool_address: owner_address });
}

public fun extract_owner_cap(owner: &signer): OwnerCapability acquires OwnerCapability {
    check_stake_permission(owner);
    let owner_address = signer::address_of(owner);
    assert_owner_cap_exists(owner_address);
    move_from<OwnerCapability>(owner_address)
}

public fun deposit_owner_cap(
    owner: &signer, owner_cap: OwnerCapability
) {
    check_stake_permission(owner);
    assert!(
        !exists<OwnerCapability>(signer::address_of(owner)),
        error::not_found(EOWNER_CAP_ALREADY_EXISTS)
    );
    move_to(owner, owner_cap);
}

public fun destroy_owner_cap(owner_cap: OwnerCapability) {
    let OwnerCapability { pool_address: _ } = owner_cap;
}

public entry fun set_operator(
    owner: &signer, new_operator: address
) acquires OwnerCapability, StakePool {
    check_stake_permission(owner);
    let owner_address = signer::address_of(owner);
    assert_owner_cap_exists(owner_address);
    let ownership_cap = borrow_global<OwnerCapability>(owner_address);
    set_operator_with_cap(ownership_cap, new_operator);
}

public fun set_operator_with_cap(
    owner_cap: &OwnerCapability, new_operator: address
) acquires StakePool {
    let pool_address = owner_cap.pool_address;
    assert_stake_pool_exists(pool_address);
    let stake_pool = borrow_global_mut<StakePool>(pool_address);
    let old_operator = stake_pool.operator_address;
    stake_pool.operator_address = new_operator;

    event::emit(SetOperator { pool_address, old_operator, new_operator });
}

public entry fun set_delegated_voter(
    owner: &signer, new_voter: address
) acquires OwnerCapability, StakePool {
    check_stake_permission(owner);
    let owner_address = signer::address_of(owner);
    assert_owner_cap_exists(owner_address);
    let ownership_cap = borrow_global<OwnerCapability>(owner_address);
    set_delegated_voter_with_cap(ownership_cap, new_voter);
}

public fun set_delegated_voter_with_cap(
    owner_cap: &OwnerCapability, new_voter: address
) acquires StakePool {
    let pool_address = owner_cap.pool_address;
    assert_stake_pool_exists(pool_address);
    let stake_pool = borrow_global_mut<StakePool>(pool_address);
    stake_pool.delegated_voter = new_voter;
}

public entry fun add_stake(
    owner: &signer, amount: u64
) acquires OwnerCapability, StakePool, ValidatorSet {
    check_stake_permission(owner);
    let owner_address = signer::address_of(owner);
    assert_owner_cap_exists(owner_address);
    let ownership_cap = borrow_global<OwnerCapability>(owner_address);
    add_stake_with_cap(ownership_cap, coin::withdraw<AptosCoin>(owner, amount));
}

public fun add_stake_with_cap(
    owner_cap: &OwnerCapability, coins: Coin<AptosCoin>
) acquires StakePool, ValidatorSet {
    assert_reconfig_not_in_progress();
    let pool_address = owner_cap.pool_address;
    assert_stake_pool_exists(pool_address);

    let amount = coin::value(&coins);
    if (amount == 0) {
        coin::destroy_zero(coins);
        return
    };

    // Only track and validate voting power increase for active and pending_active validator.
    // Pending_inactive validator will be removed from the validator set in the next epoch.
    // Inactive validator's total stake will be tracked when they join the validator set.
    let validator_set = borrow_global<ValidatorSet>(@aptos_framework);
    // Search directly rather using get_validator_state to save on unnecessary loops.
    if (find_validator(&validator_set.active_validators, pool_address).is_some()
        || find_validator(&validator_set.pending_active, pool_address).is_some()) {
        update_voting_power_increase(amount);
    };

    // Add to pending_active if it's a current validator because the stake is not counted until the next epoch.
    // Otherwise, the delegation can be added to active directly as the validator is also activated in the epoch.
    let stake_pool = borrow_global_mut<StakePool>(pool_address);
    if (is_current_epoch_validator(pool_address)) {
        coin::merge<AptosCoin>(&mut stake_pool.pending_active, coins);
    } else {
        coin::merge<AptosCoin>(&mut stake_pool.active, coins);
    };

    let (_, maximum_stake) =
        staking_config::get_required_stake(&staking_config::get());
    let voting_power = get_voting_power(stake_pool);
    assert!(
        voting_power <= maximum_stake, error::invalid_argument(ESTAKE_EXCEEDS_MAX)
    );

    event::emit(AddStake { pool_address, amount_added: amount });
}

public entry fun reactivate_stake(owner: &signer, amount: u64) acquires OwnerCapability, StakePool {
    check_stake_permission(owner);
    assert_reconfig_not_in_progress();
    let owner_address = signer::address_of(owner);
    assert_owner_cap_exists(owner_address);
    let ownership_cap = borrow_global<OwnerCapability>(owner_address);
    reactivate_stake_with_cap(ownership_cap, amount);
}

public fun reactivate_stake_with_cap(
    owner_cap: &OwnerCapability, amount: u64
) acquires StakePool {
    assert_reconfig_not_in_progress();
    let pool_address = owner_cap.pool_address;
    assert_stake_pool_exists(pool_address);

    // Cap the amount to reactivate by the amount in pending_inactive.
    let stake_pool = borrow_global_mut<StakePool>(pool_address);
    let total_pending_inactive = coin::value(&stake_pool.pending_inactive);
    amount = min(amount, total_pending_inactive);

    // Since this does not count as a voting power change (pending inactive still counts as voting power in the
    // current epoch), stake can be immediately moved from pending inactive to active.
    // We also don't need to check voting power increase as there's none.
    let reactivated_coins = coin::extract(&mut stake_pool.pending_inactive, amount);
    coin::merge(&mut stake_pool.active, reactivated_coins);

    event::emit(ReactivateStake { pool_address, amount });
}

public entry fun rotate_consensus_key(
    operator: &signer,
    pool_address: address,
    new_consensus_pubkey: vector<u8>,
    proof_of_possession: vector<u8>
) acquires StakePool, ValidatorConfig {
    check_stake_permission(operator);
    assert_reconfig_not_in_progress();
    assert_stake_pool_exists(pool_address);

    let stake_pool = borrow_global_mut<StakePool>(pool_address);
    assert!(
        signer::address_of(operator) == stake_pool.operator_address,
        error::unauthenticated(ENOT_OPERATOR)
    );

    assert!(
        exists<ValidatorConfig>(pool_address),
        error::not_found(EVALIDATOR_CONFIG)
    );
    let validator_info = borrow_global_mut<ValidatorConfig>(pool_address);
    let old_consensus_pubkey = validator_info.consensus_pubkey;
    // Checks the public key has a valid proof-of-possession to prevent rogue-key attacks.
    let pubkey_from_pop =
        &bls12381::public_key_from_bytes_with_pop(
            new_consensus_pubkey,
            &proof_of_possession_from_bytes(proof_of_possession)
        );
    assert!(
        pubkey_from_pop.is_some(), error::invalid_argument(EINVALID_PUBLIC_KEY)
    );
    validator_info.consensus_pubkey = new_consensus_pubkey;

    event::emit(
        RotateConsensusKey { pool_address, old_consensus_pubkey, new_consensus_pubkey }
    );
}

public entry fun update_network_and_fullnode_addresses(
    operator: &signer,
    pool_address: address,
    new_network_addresses: vector<u8>,
    new_fullnode_addresses: vector<u8>
) acquires StakePool, ValidatorConfig {
    check_stake_permission(operator);
    assert_reconfig_not_in_progress();
    assert_stake_pool_exists(pool_address);
    let stake_pool = borrow_global_mut<StakePool>(pool_address);
    assert!(
        signer::address_of(operator) == stake_pool.operator_address,
        error::unauthenticated(ENOT_OPERATOR)
    );
    assert!(
        exists<ValidatorConfig>(pool_address),
        error::not_found(EVALIDATOR_CONFIG)
    );
    let validator_info = borrow_global_mut<ValidatorConfig>(pool_address);
    let old_network_addresses = validator_info.network_addresses;
    validator_info.network_addresses = new_network_addresses;
    let old_fullnode_addresses = validator_info.fullnode_addresses;
    validator_info.fullnode_addresses = new_fullnode_addresses;

    event::emit(
        UpdateNetworkAndFullnodeAddresses {
            pool_address,
            old_network_addresses,
            new_network_addresses,
            old_fullnode_addresses,
            new_fullnode_addresses
        }
    );
}

public entry fun increase_lockup(owner: &signer) acquires OwnerCapability, StakePool {
    check_stake_permission(owner);
    let owner_address = signer::address_of(owner);
    assert_owner_cap_exists(owner_address);
    let ownership_cap = borrow_global<OwnerCapability>(owner_address);
    increase_lockup_with_cap(ownership_cap);
}

public fun increase_lockup_with_cap(owner_cap: &OwnerCapability) acquires StakePool {
    let pool_address = owner_cap.pool_address;
    assert_stake_pool_exists(pool_address);
    let config = staking_config::get();

    let stake_pool = borrow_global_mut<StakePool>(pool_address);
    let old_locked_until_secs = stake_pool.locked_until_secs;
    let new_locked_until_secs =
        timestamp::now_seconds()
            + staking_config::get_recurring_lockup_duration(&config);
    assert!(
        old_locked_until_secs < new_locked_until_secs,
        error::invalid_argument(EINVALID_LOCKUP)
    );
    stake_pool.locked_until_secs = new_locked_until_secs;

    event::emit(
        IncreaseLockup { pool_address, old_locked_until_secs, new_locked_until_secs }
    );
}

public entry fun join_validator_set(
    operator: &signer, pool_address: address
) acquires StakePool, ValidatorConfig, ValidatorSet {
    check_stake_permission(operator);
    assert!(
        staking_config::get_allow_validator_set_change(&staking_config::get()),
        error::invalid_argument(ENO_POST_GENESIS_VALIDATOR_SET_CHANGE_ALLOWED)
    );

    join_validator_set_internal(operator, pool_address);
}

public(friend) fun join_validator_set_internal(
    operator: &signer, pool_address: address
) acquires StakePool, ValidatorConfig, ValidatorSet {
    assert_reconfig_not_in_progress();
    assert_stake_pool_exists(pool_address);
    let stake_pool = borrow_global_mut<StakePool>(pool_address);
    assert!(
        signer::address_of(operator) == stake_pool.operator_address,
        error::unauthenticated(ENOT_OPERATOR)
    );
    assert!(
        get_validator_state(pool_address) == VALIDATOR_STATUS_INACTIVE,
        error::invalid_state(EALREADY_ACTIVE_VALIDATOR)
    );

    let config = staking_config::get();
    let (minimum_stake, maximum_stake) = staking_config::get_required_stake(&config);
    // Settle any pending_inactive whose lockup has already expired so it is not counted
    // as voting power. An inactive validator's pending_inactive is never processed by
    // update_stake_pool, so we must do it here before evaluating the minimum stake.
    // Only settle when locked_until_secs > 0 (i.e., a lockup was ever explicitly set);
    // a value of 0 means the pool was just created and the lockup has not been initialised yet.
    if (stake_pool.locked_until_secs > 0
        && timestamp::now_seconds() >= stake_pool.locked_until_secs) {
        coin::merge(
            &mut stake_pool.inactive,
            coin::extract_all(&mut stake_pool.pending_inactive)
        );
    };
    let voting_power = get_voting_power(stake_pool);
    assert!(voting_power >= minimum_stake, error::invalid_argument(ESTAKE_TOO_LOW));
    assert!(voting_power <= maximum_stake, error::invalid_argument(ESTAKE_TOO_HIGH));

    // Track and validate voting power increase.
    update_voting_power_increase(voting_power);

    // Add validator to pending_active, to be activated in the next epoch.
    let validator_config = borrow_global<ValidatorConfig>(pool_address);
    assert!(
        !validator_config.consensus_pubkey.is_empty(),
        error::invalid_argument(EINVALID_PUBLIC_KEY)
    );

    // Validate the current validator set size has not exceeded the limit.
    let validator_set = borrow_global_mut<ValidatorSet>(@aptos_framework);
    validator_set.pending_active.push_back(
        generate_validator_info(pool_address, stake_pool, *validator_config)
    );
    let validator_set_size =
        validator_set.active_validators.length()
            + validator_set.pending_active.length();
    assert!(
        validator_set_size <= MAX_VALIDATOR_SET_SIZE,
        error::invalid_argument(EVALIDATOR_SET_TOO_LARGE)
    );

    event::emit(JoinValidatorSet { pool_address });
}

public entry fun unlock(owner: &signer, amount: u64) acquires OwnerCapability, StakePool {
    check_stake_permission(owner);
    assert_reconfig_not_in_progress();
    let owner_address = signer::address_of(owner);
    assert_owner_cap_exists(owner_address);
    let ownership_cap = borrow_global<OwnerCapability>(owner_address);
    unlock_with_cap(amount, ownership_cap);
}

public fun unlock_with_cap(amount: u64, owner_cap: &OwnerCapability) acquires StakePool {
    assert_reconfig_not_in_progress();
    // Short-circuit if amount to unlock is 0 so we don't emit events.
    if (amount == 0) { return };

    // Unlocked coins are moved to pending_inactive. When the current lockup cycle expires, they will be moved into
    // inactive in the earliest possible epoch transition.
    let pool_address = owner_cap.pool_address;
    assert_stake_pool_exists(pool_address);
    let stake_pool = borrow_global_mut<StakePool>(pool_address);
    // Cap amount to unlock by maximum active stake.
    let amount = min(amount, coin::value(&stake_pool.active));
    let unlocked_stake = coin::extract(&mut stake_pool.active, amount);
    coin::merge<AptosCoin>(&mut stake_pool.pending_inactive, unlocked_stake);

    event::emit(UnlockStake { pool_address, amount_unlocked: amount });
}

public entry fun withdraw(
    owner: &signer, withdraw_amount: u64
) acquires OwnerCapability, StakePool, ValidatorSet {
    check_stake_permission(owner);
    let owner_address = signer::address_of(owner);
    assert_owner_cap_exists(owner_address);
    let ownership_cap = borrow_global<OwnerCapability>(owner_address);
    let coins = withdraw_with_cap(ownership_cap, withdraw_amount);
    coin::deposit<AptosCoin>(owner_address, coins);
}

public fun withdraw_with_cap(
    owner_cap: &OwnerCapability, withdraw_amount: u64
): Coin<AptosCoin> acquires StakePool, ValidatorSet {
    assert_reconfig_not_in_progress();
    let pool_address = owner_cap.pool_address;
    assert_stake_pool_exists(pool_address);
    let stake_pool = borrow_global_mut<StakePool>(pool_address);
    // There's an edge case where a validator unlocks their stake and leaves the validator set before
    // the stake is fully unlocked (the current lockup cycle has not expired yet).
    // This can leave their stake stuck in pending_inactive even after the current lockup cycle expires.
    if (get_validator_state(pool_address) == VALIDATOR_STATUS_INACTIVE
        && timestamp::now_seconds() >= stake_pool.locked_until_secs) {
        let pending_inactive_stake =
            coin::extract_all(&mut stake_pool.pending_inactive);
        coin::merge(&mut stake_pool.inactive, pending_inactive_stake);
    };

    // Cap withdraw amount by total inactive coins.
    withdraw_amount = min(withdraw_amount, coin::value(&stake_pool.inactive));
    if (withdraw_amount == 0) return coin::zero<AptosCoin>();

    event::emit(WithdrawStake { pool_address, amount_withdrawn: withdraw_amount });

    coin::extract(&mut stake_pool.inactive, withdraw_amount)
}

public entry fun leave_validator_set(
    operator: &signer, pool_address: address
) acquires StakePool, ValidatorSet {
    check_stake_permission(operator);
    assert_reconfig_not_in_progress();
    let config = staking_config::get();
    assert!(
        staking_config::get_allow_validator_set_change(&config),
        error::invalid_argument(ENO_POST_GENESIS_VALIDATOR_SET_CHANGE_ALLOWED)
    );

    assert_stake_pool_exists(pool_address);
    let stake_pool = borrow_global_mut<StakePool>(pool_address);
    // Account has to be the operator.
    assert!(
        signer::address_of(operator) == stake_pool.operator_address,
        error::unauthenticated(ENOT_OPERATOR)
    );

    let validator_set = borrow_global_mut<ValidatorSet>(@aptos_framework);
    // If the validator is still pending_active, directly kick the validator out.
    let maybe_pending_active_index =
        find_validator(&validator_set.pending_active, pool_address);
    if (maybe_pending_active_index.is_some()) {
        validator_set.pending_active.swap_remove(maybe_pending_active_index.extract());

        // Decrease the voting power increase as the pending validator's voting power was added when they requested
        // to join. Now that they changed their mind, their voting power should not affect the joining limit of this
        // epoch.
        let validator_stake = (get_voting_power(stake_pool) as u128);
        // total_joining_power should be larger than validator_stake but just in case there has been a small
        // rounding error somewhere that can lead to an underflow, we still want to allow this transaction to
        // succeed.
        if (validator_set.total_joining_power > validator_stake) {
            validator_set.total_joining_power -= validator_stake;
        } else {
            validator_set.total_joining_power = 0;
        };
    } else {
        // Validate that the validator is already part of the validator set.
        let maybe_active_index =
            find_validator(&validator_set.active_validators, pool_address);
        assert!(maybe_active_index.is_some(), error::invalid_state(ENOT_VALIDATOR));
        let validator_info =
            validator_set.active_validators.swap_remove(maybe_active_index.extract());
        assert!(
            validator_set.active_validators.length() > 0,
            error::invalid_state(ELAST_VALIDATOR)
        );
        validator_set.pending_inactive.push_back(validator_info);

        event::emit(LeaveValidatorSet { pool_address });
    };
}

public fun is_current_epoch_validator(pool_address: address): bool acquires ValidatorSet {
    assert_stake_pool_exists(pool_address);
    let validator_state = get_validator_state(pool_address);
    validator_state == VALIDATOR_STATUS_ACTIVE
        || validator_state == VALIDATOR_STATUS_PENDING_INACTIVE
}

public(friend) fun update_performance_statistics(
    proposer_index: Option<u64>, failed_proposer_indices: vector<u64>
) acquires ValidatorPerformance {
    // Validator set cannot change until the end of the epoch, so the validator index in arguments should
    // match with those of the validators in ValidatorPerformance resource.
    let validator_perf = borrow_global_mut<ValidatorPerformance>(@aptos_framework);
    let validator_len = validator_perf.validators.length();

    spec {
        update ghost_valid_perf = validator_perf;
        update ghost_proposer_idx = proposer_index;
    };
    // proposer_index is an option because it can be missing (for NilBlocks)
    if (proposer_index.is_some()) {
        let cur_proposer_index = proposer_index.extract();
        // Here, and in all other vector::borrow, skip any validator indices that are out of bounds,
        // this ensures that this function doesn't abort if there are out of bounds errors.
        if (cur_proposer_index < validator_len) {
            let validator = validator_perf.validators.borrow_mut(cur_proposer_index);
            spec {
                assume validator.successful_proposals + 1 <= MAX_U64;
            };
            validator.successful_proposals += 1;
        };
    };

    let f = 0;
    let f_len = failed_proposer_indices.length();
    while ({
        spec {
            invariant len(validator_perf.validators) == validator_len;
            invariant (
                option::is_some(ghost_proposer_idx)
                    && option::borrow(ghost_proposer_idx) < validator_len
            ) ==>
                (
                    validator_perf.validators[option::borrow(ghost_proposer_idx)].successful_proposals ==
                    ghost_valid_perf.validators[option::borrow(ghost_proposer_idx)].successful_proposals
                    + 1
                );
        };
        f < f_len
    }) {
        let validator_index = failed_proposer_indices[f];
        if (validator_index < validator_len) {
            let validator = validator_perf.validators.borrow_mut(validator_index);
            spec {
                assume validator.failed_proposals + 1 <= MAX_U64;
            };
            validator.failed_proposals += 1;
        };
        f += 1;
    };
}

public(friend) fun on_new_epoch() acquires AptosCoinCapabilities, PendingTransactionFee, PrecomputedValidatorSet, StakePool, TransactionFeeConfig, ValidatorConfig, ValidatorPerformance, ValidatorSet {
    let validator_set = borrow_global_mut<ValidatorSet>(@aptos_framework);
    let config = staking_config::get();
    let validator_perf = borrow_global_mut<ValidatorPerformance>(@aptos_framework);

    // Process pending stake and distribute transaction fees and rewards for each currently active validator.
    validator_set.active_validators.for_each_ref(|validator| {
        let validator: &ValidatorInfo = validator;
        update_stake_pool(validator_perf, validator.addr, &config);
    });

    // Process pending stake and distribute transaction fees and rewards for each currently pending_inactive validator
    // (requested to leave but not removed yet).
    validator_set.pending_inactive.for_each_ref(|validator| {
        let validator: &ValidatorInfo = validator;
        update_stake_pool(validator_perf, validator.addr, &config);
    });

    // Settle expired pending_inactive for pending_active validators before activating them.
    // update_stake_pool is not called for pending_active validators, so without this step
    // their expired pending_inactive would be incorrectly counted as voting power, causing
    // a mismatch with the DKG validator set (which excludes expired pending_inactive) and
    // an out-of-bounds panic in the epoch manager.
    validator_set.pending_active.for_each_ref(|validator| {
        let validator: &ValidatorInfo = validator;
        let stake_pool = borrow_global_mut<StakePool>(validator.addr);
        if (stake_pool.locked_until_secs > 0
            && get_reconfig_start_time_secs() >= stake_pool.locked_until_secs) {
            coin::merge(
                &mut stake_pool.inactive,
                coin::extract_all(&mut stake_pool.pending_inactive)
            );
        };
    });

    // Activate currently pending_active validators.
    append(&mut validator_set.active_validators, &mut validator_set.pending_active);

    // Officially deactivate all pending_inactive validators. They will now no longer receive rewards.
    validator_set.pending_inactive = vector::empty();

    // Determine the next-epoch active set: either consume the cached value
    // produced when reconfig started (async/DKG path), or compute it now from
    // live state (sync/governance path). The two paths are mutually exclusive,
    // so we avoid the O(n) per-validator recomputation when the cache exists.
    let liveness_fallback_event = if (exists<PrecomputedValidatorSet>(@aptos_framework)) {
        let PrecomputedValidatorSet { validator_set: precomputed, is_liveness_fallback } =
            move_from<PrecomputedValidatorSet>(@aptos_framework);
        *validator_set = precomputed;
        if (is_liveness_fallback) {
            let (minimum_stake, _) = staking_config::get_required_stake(&config);
            option::some(ValidatorSetLivenessFallback {
                minimum_stake,
                emergency_validator_count: validator_set.active_validators.length(),
                total_emergency_voting_power: validator_set.total_voting_power,
            })
        } else {
            option::none()
        }
    } else {
        refresh_validator_set_in_place(validator_set, &config)
    };
    validator_set.total_joining_power = 0;

    if (liveness_fallback_event.is_some()) {
        event::emit(liveness_fallback_event.extract());
    };

    // Update validator indices, reset performance scores, and renew lockups.
    validator_perf.validators = vector::empty();
    let recurring_lockup_duration_secs =
        staking_config::get_recurring_lockup_duration(&config);
    let vlen = validator_set.active_validators.length();
    let validator_index = 0;
    while ({
        spec {
            invariant spec_validators_are_initialized(validator_set.active_validators);
            invariant len(validator_set.pending_active) == 0;
            invariant len(validator_set.pending_inactive) == 0;
            invariant 0 <= validator_index && validator_index <= vlen;
            invariant vlen == len(validator_set.active_validators);
            invariant forall i in 0..validator_index:
                global<ValidatorConfig>(validator_set.active_validators[i].addr).validator_index
                    < validator_index;
            invariant forall i in 0..validator_index:
                validator_set.active_validators[i].config.validator_index
                    < validator_index;
            invariant len(validator_perf.validators) == validator_index;
        };
        validator_index < vlen
    }) {
        let validator_info =
            validator_set.active_validators.borrow_mut(validator_index);
        validator_info.config.validator_index = validator_index;
        let validator_config =
            borrow_global_mut<ValidatorConfig>(validator_info.addr);
        validator_config.validator_index = validator_index;

        validator_perf.validators.push_back(
            IndividualValidatorPerformance {
                successful_proposals: 0,
                failed_proposals: 0
            }
        );

        // Automatically renew a validator's lockup for validators that will still be in the validator set in the
        // next epoch.
        let stake_pool = borrow_global_mut<StakePool>(validator_info.addr);
        let now_secs = timestamp::now_seconds();
        let reconfig_start_secs =
            if (chain_status::is_operating()) {
                get_reconfig_start_time_secs()
            } else {
                now_secs
            };
        if (stake_pool.locked_until_secs <= reconfig_start_secs) {
            spec {
                assume now_secs + recurring_lockup_duration_secs <= MAX_U64;
            };
            stake_pool.locked_until_secs = now_secs
                + recurring_lockup_duration_secs;
        };

        validator_index += 1;
    };

    if (exists<PendingTransactionFee>(@aptos_framework)) {
        let pending_fee_by_validator =
            &mut borrow_global_mut<PendingTransactionFee>(@aptos_framework).pending_fee_by_validator;
        assert!(
            pending_fee_by_validator.is_empty(),
            error::internal(ETRANSACTION_FEE_NOT_FULLY_DISTRIBUTED)
        );
        validator_set.active_validators.for_each_ref(|v| pending_fee_by_validator.add(
            v.config.validator_index, aggregator_v2::create_unbounded_aggregator<u64>()
        ));
    };

    if (features::periodical_reward_rate_decrease_enabled()) {
        // Update rewards rate after reward distribution.
        staking_config::calculate_and_save_latest_epoch_rewards_rate();
    };
}

fun refresh_validator_set_in_place(
    validator_set: &mut ValidatorSet,
    config: &staking_config::StakingConfig,
): Option<ValidatorSetLivenessFallback> acquires StakePool, ValidatorConfig {
    // Update active validator set so that network address/public key change takes effect.
    // Moreover, recalculate the total voting power, and deactivate the validator whose
    // voting power is less than the minimum required stake.
    let next_epoch_validators = vector::empty();
    let (minimum_stake, _) = staking_config::get_required_stake(config);
    let vlen = validator_set.active_validators.length();
    let total_voting_power = 0;
    let i = 0;
    while ({
        spec {
            invariant spec_validators_are_initialized(next_epoch_validators);
            invariant i <= vlen;
        };
        i < vlen
    }) {
        let old_validator_info = validator_set.active_validators.borrow_mut(i);
        let pool_address = old_validator_info.addr;
        let validator_config = borrow_global<ValidatorConfig>(pool_address);
        let stake_pool = borrow_global<StakePool>(pool_address);
        let new_validator_info =
            generate_validator_info(pool_address, stake_pool, *validator_config);

        // A validator needs at least the min stake required to join the validator set.
        if (new_validator_info.voting_power >= minimum_stake) {
            spec {
                assume total_voting_power + new_validator_info.voting_power
                    <= MAX_U128;
            };
            total_voting_power +=(new_validator_info.voting_power as u128);
            next_epoch_validators.push_back(new_validator_info);
        };
        i += 1;
    };

    // In the extreme case where the next epoch validator election produces an empty set (i.e., no staker satisfies the minimum stake or participation requirements), the system enters an emergency liveness preservation mode.
    // Instead of transitioning to an empty validator set—which would render the network inoperable—the protocol retains the previous active validator set and recomputes the total voting power from it.
    // A ValidatorSetLivenessFallback event is emitted to signal this critical governance and economic security failure.
    if (!next_epoch_validators.is_empty()) {
        validator_set.active_validators = next_epoch_validators;
        validator_set.total_voting_power = total_voting_power;
        option::none()
    } else {
        // We derive the next validator set from the previous epoch's active and pending-active stakers.
        // If the resulting set is empty, it indicates that no staker is willing or qualified to participate
        // in consensus anymore. In this case, the chain is considered effectively dead, and we must retain
        // the previous active validator set as a last-resort liveness fallback.
        // Recompute each validator's info from current stake (after update_stake_pool) so that
        // voting_power and total_voting_power reflect rewards, fees, and merged stake—not stale values.
        let refreshed_validators = vector::empty();
        let emergency_total_voting_power = 0u128;
        let fallback_vlen = validator_set.active_validators.length();
        let fallback_i = 0;
        while (fallback_i < fallback_vlen) {
            let old_validator_info =
                validator_set.active_validators.borrow(fallback_i);
            let pool_address = old_validator_info.addr;
            let validator_config = &ValidatorConfig[pool_address];
            let stake_pool = &StakePool[pool_address];
            let new_validator_info =
                generate_validator_info(pool_address, stake_pool, *validator_config);
            refreshed_validators.push_back(new_validator_info);
            emergency_total_voting_power +=(new_validator_info.voting_power as u128);
            fallback_i += 1;
        };
        validator_set.active_validators = refreshed_validators;
        validator_set.total_voting_power = emergency_total_voting_power;
        option::some(ValidatorSetLivenessFallback {
            minimum_stake,
            emergency_validator_count: validator_set.active_validators.length(),
            total_emergency_voting_power: validator_set.total_voting_power
        })
    }
}

public fun cur_validator_consensus_infos(): vector<ValidatorConsensusInfo> acquires ValidatorSet {
    let validator_set = borrow_global<ValidatorSet>(@aptos_framework);
    validator_consensus_infos_from_validator_set(validator_set)
}

fun compute_simulated_validator_info(
    candidate: &ValidatorInfo,
    validator_perf: &ValidatorPerformance,
    rewards_rate: u64,
    rewards_rate_denominator: u64,
    validator_index: u64,
    include_rewards: bool
): (u64, ValidatorInfo) acquires StakePool, ValidatorConfig {
    let stake_pool = borrow_global<StakePool>(candidate.addr);
    let cur_active = coin::value(&stake_pool.active);
    let cur_pending_active = coin::value(&stake_pool.pending_active);
    let cur_pending_inactive = coin::value(&stake_pool.pending_inactive);
    let cur_reward =
        if (include_rewards && cur_active > 0) {
            spec {
                assert candidate.config.validator_index
                    < len(validator_perf.validators);
            };
            let cur_perf =
                validator_perf.validators.borrow(candidate.config.validator_index);
            spec {
                assume cur_perf.successful_proposals + cur_perf.failed_proposals
                    <= MAX_U64;
            };
            calculate_rewards_amount(
                cur_active,
                cur_perf.successful_proposals,
                cur_perf.successful_proposals + cur_perf.failed_proposals,
                rewards_rate,
                rewards_rate_denominator
            )
        } else { 0 };
    let lockup_expired = get_reconfig_start_time_secs()
        >= stake_pool.locked_until_secs;
    spec {
        assume cur_active + cur_pending_active + cur_reward <= MAX_U64;
        assume cur_active + cur_pending_inactive + cur_pending_active + cur_reward
            <= MAX_U64;
    };
    let new_voting_power =
        cur_active
            + if (lockup_expired) { 0 }
            else {
                cur_pending_inactive
            } + cur_pending_active + cur_reward;
    let config = *borrow_global<ValidatorConfig>(candidate.addr);
    config.validator_index = validator_index;
    (
        new_voting_power,
        ValidatorInfo { addr: candidate.addr, voting_power: new_voting_power, config }
    )
}

public fun next_validator_consensus_infos(): vector<ValidatorConsensusInfo>  {
    abort(error::unavailable(EDEPRECATED))
}

public(friend) fun next_validator_consensus_infos_v2(): ValidatorSet acquires PrecomputedValidatorSet, ValidatorSet, ValidatorPerformance, StakePool, ValidatorConfig {
    if (exists<PrecomputedValidatorSet>(@aptos_framework)) {
        // Cache hit: already computed for this reconfig, return stored result.
        return borrow_global<PrecomputedValidatorSet>(@aptos_framework).validator_set;
    };

    let cur_validator_set = borrow_global<ValidatorSet>(@aptos_framework);
    let staking_config = staking_config::get();
    let validator_perf = borrow_global<ValidatorPerformance>(@aptos_framework);
    let (minimum_stake, _) = staking_config::get_required_stake(&staking_config);
    let (rewards_rate, rewards_rate_denominator) =
        staking_config::get_reward_rate(&staking_config);

    let new_active_validators = vector[];
    let num_new_actives = 0;
    let candidate_idx = 0;
    let new_total_power = 0;
    let num_cur_actives = cur_validator_set.active_validators.length();
    let num_cur_pending_actives = cur_validator_set.pending_active.length();
    spec {
        assume num_cur_actives + num_cur_pending_actives <= MAX_U64;
    };
    let num_candidates = num_cur_actives + num_cur_pending_actives;
    while ({
        spec {
            invariant candidate_idx <= num_candidates;
            invariant spec_validators_are_initialized(new_active_validators);
            invariant len(new_active_validators) == num_new_actives;
            invariant forall i in 0..len(new_active_validators):
                new_active_validators[i].config.validator_index == i;
            invariant num_new_actives <= candidate_idx;
            invariant spec_validators_are_initialized(new_active_validators);
        };
        candidate_idx < num_candidates
    }) {
        let candidate_in_current = candidate_idx < num_cur_actives;
        // Order matches on_new_epoch's append(): active then pending_active (append uses pop_back → reverse).
        let candidate =
            if (candidate_in_current) {
                cur_validator_set.active_validators.borrow(candidate_idx)
            } else {
                cur_validator_set.pending_active.borrow(
                    num_candidates - 1 - candidate_idx
                )
            };
        let (new_voting_power, new_validator_info) =
            compute_simulated_validator_info(
                candidate,
                validator_perf,
                rewards_rate,
                rewards_rate_denominator,
                num_new_actives,
                candidate_in_current
            );
        if (new_voting_power >= minimum_stake) {
            spec {
                assume new_total_power + new_voting_power <= MAX_U128;
            };
            new_total_power +=(new_voting_power as u128);
            new_active_validators.push_back(new_validator_info);
            num_new_actives += 1;
        };
        candidate_idx += 1;
    };

    // Mirror on_new_epoch's empty-validator-set fallback: active then pending_active.
    // append() uses pop_back so pending_active ends up in reverse order; match that here.
    let is_liveness_fallback = false;
    if (new_active_validators.is_empty()
        && (num_cur_actives > 0 || num_cur_pending_actives > 0)) {
        let num_fallback = num_cur_actives + num_cur_pending_actives;
        for (fallback_idx in 0..num_fallback) {
            let in_active = fallback_idx < num_cur_actives;
            let candidate =
                if (in_active) {
                    cur_validator_set.active_validators.borrow(fallback_idx)
                } else {
                    cur_validator_set.pending_active.borrow(
                        num_fallback - 1 - fallback_idx
                    )
                };
            let (new_voting_power, new_validator_info) =
                compute_simulated_validator_info(
                    candidate,
                    validator_perf,
                    rewards_rate,
                    rewards_rate_denominator,
                    new_active_validators.length(),
                    in_active
                );
            new_active_validators.push_back(new_validator_info);
            new_total_power +=(new_voting_power as u128);
            is_liveness_fallback = true;
        };
    };

    let new_validator_set = ValidatorSet {
        consensus_scheme: cur_validator_set.consensus_scheme,
        active_validators: new_active_validators,
        pending_inactive: vector[],
        pending_active: vector[],
        total_voting_power: new_total_power,
        total_joining_power: 0
    };

    // Save the result by creating the resource.
    move_to(
        &create_signer::create_signer(@aptos_framework),
        PrecomputedValidatorSet { validator_set: new_validator_set, is_liveness_fallback },
    );

    new_validator_set
}

friend fun validator_consensus_infos_from_validator_set(
    validator_set: &ValidatorSet
): vector<ValidatorConsensusInfo> {
    let validator_consensus_infos = vector[];

    let num_active = validator_set.active_validators.length();
    let num_pending_inactive = validator_set.pending_inactive.length();
    spec {
        assume num_active + num_pending_inactive <= MAX_U64;
    };
    let total = num_active + num_pending_inactive;

    // Pre-fill the return value with dummy values.
    let idx = 0;
    while ({
        spec {
            invariant idx
                <= len(validator_set.active_validators)
                    + len(validator_set.pending_inactive);
            invariant len(validator_consensus_infos) == idx;
            invariant len(validator_consensus_infos)
                <= len(validator_set.active_validators)
                    + len(validator_set.pending_inactive);
        };
        idx < total
    }) {
        validator_consensus_infos.push_back(validator_consensus_info::default());
        idx += 1;
    };
    spec {
        assert len(validator_consensus_infos)
            == len(validator_set.active_validators)
                + len(validator_set.pending_inactive);
        assert spec_validator_indices_are_valid_config(
            validator_set.active_validators,
            len(validator_set.active_validators)
                + len(validator_set.pending_inactive)
        );
    };

    validator_set.active_validators.for_each_ref(
        |obj| {
            let vi: &ValidatorInfo = obj;
            spec {
                assume len(validator_consensus_infos)
                    == len(validator_set.active_validators)
                        + len(validator_set.pending_inactive);
                assert vi.config.validator_index < len(validator_consensus_infos);
            };
            let vci = vector::borrow_mut(
                &mut validator_consensus_infos, vi.config.validator_index
            );
            *vci = validator_consensus_info::new(
                vi.addr, vi.config.consensus_pubkey, vi.voting_power
            );
            spec {
                assert len(validator_consensus_infos)
                    == len(validator_set.active_validators)
                        + len(validator_set.pending_inactive);
            };
        }
    );

    validator_set.pending_inactive.for_each_ref(
        |obj| {
            let vi: &ValidatorInfo = obj;
            spec {
                assume len(validator_consensus_infos)
                    == len(validator_set.active_validators)
                        + len(validator_set.pending_inactive);
                assert vi.config.validator_index < len(validator_consensus_infos);
            };
            let vci = vector::borrow_mut(
                &mut validator_consensus_infos, vi.config.validator_index
            );
            *vci = validator_consensus_info::new(
                vi.addr, vi.config.consensus_pubkey, vi.voting_power
            );
            spec {
                assert len(validator_consensus_infos)
                    == len(validator_set.active_validators)
                        + len(validator_set.pending_inactive);
            };
        }
    );

    validator_consensus_infos
}

fun addresses_from_validator_infos(infos: &vector<ValidatorInfo>): vector<address> {
    infos.map_ref(|obj| {
        let info: &ValidatorInfo = obj;
        info.addr
    })
}

fun update_stake_pool(
    validator_perf: &ValidatorPerformance,
    pool_address: address,
    staking_config: &StakingConfig
) acquires AptosCoinCapabilities, PendingTransactionFee, StakePool, TransactionFeeConfig, ValidatorConfig {
    let stake_pool = borrow_global_mut<StakePool>(pool_address);
    let validator_config = borrow_global<ValidatorConfig>(pool_address);
    let validator_index = validator_config.validator_index;
    let cur_validator_perf = validator_perf.validators.borrow(validator_index);
    let num_successful_proposals = cur_validator_perf.successful_proposals;

    let fee_pending_inactive = 0;
    let fee_active = 0;
    let fee_limit =
        if (exists<TransactionFeeConfig>(@aptos_framework)) {
            let TransactionFeeConfig::V0 { max_fee_octa_allowed_per_epoch_per_pool } =
                borrow_global<TransactionFeeConfig>(@aptos_framework);
            *max_fee_octa_allowed_per_epoch_per_pool
        } else {
            MAX_U64 as u64
        };

    if (exists<PendingTransactionFee>(@aptos_framework)) {
        let pending_fee_by_validator =
            &mut borrow_global_mut<PendingTransactionFee>(@aptos_framework).pending_fee_by_validator;
        if (pending_fee_by_validator.contains(&validator_index)) {
            let fee_octa = pending_fee_by_validator.remove(&validator_index).read();
            if (fee_octa > fee_limit) {
                fee_octa = fee_limit;
            };
            let stake_active = (coin::value(&stake_pool.active) as u128);
            let stake_pending_inactive =
                (coin::value(&stake_pool.pending_inactive) as u128);
            fee_pending_inactive =
                (
                    ((fee_octa as u128) * stake_pending_inactive
                        / (stake_active + stake_pending_inactive)) as u64
                );
            fee_active = fee_octa - fee_pending_inactive;
        }
    };

    spec {
        // The following addition should not overflow because `num_total_proposals` cannot be larger than 86400,
        // the maximum number of proposals in a day (1 proposal per second).
        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) =
        staking_config::get_reward_rate(staking_config);
    let rewards_active =
        distribute_rewards(
            &mut stake_pool.active,
            num_successful_proposals,
            num_total_proposals,
            rewards_rate,
            rewards_rate_denominator
        );
    let rewards_pending_inactive =
        distribute_rewards(
            &mut stake_pool.pending_inactive,
            num_successful_proposals,
            num_total_proposals,
            rewards_rate,
            rewards_rate_denominator
        );
    spec {
        assume rewards_active + rewards_pending_inactive <= MAX_U64;
    };

    if (std::features::is_distribute_transaction_fee_enabled()) {
        let mint_cap =
            &borrow_global<AptosCoinCapabilities>(@aptos_framework).mint_cap;
        if (fee_active > 0) {
            coin::merge(&mut stake_pool.active, coin::mint(fee_active, mint_cap));
        };
        if (fee_pending_inactive > 0) {
            coin::merge(
                &mut stake_pool.pending_inactive,
                coin::mint(fee_pending_inactive, mint_cap)
            );
        };
        let fee_amount = fee_active + fee_pending_inactive;
        if (fee_amount > 0) {
            event::emit(DistributeTransactionFee { pool_address, fee_amount });
        };
    };

    let rewards_amount = rewards_active + rewards_pending_inactive;
    // Pending active stake can now be active.
    coin::merge(
        &mut stake_pool.active, coin::extract_all(&mut stake_pool.pending_active)
    );

    // Pending inactive stake is only fully unlocked and moved into inactive if the current lockup cycle has expired
    let current_lockup_expiration = stake_pool.locked_until_secs;
    if (get_reconfig_start_time_secs() >= current_lockup_expiration) {
        coin::merge(
            &mut stake_pool.inactive,
            coin::extract_all(&mut stake_pool.pending_inactive)
        );
    };

    event::emit(DistributeRewards { pool_address, rewards_amount });
}

fun get_reconfig_start_time_secs(): u64 {
    if (reconfiguration_state::is_in_progress()) {
        reconfiguration_state::start_time_secs()
    } else {
        timestamp::now_seconds()
    }
}

fun calculate_rewards_amount(
    stake_amount: u64,
    num_successful_proposals: u64,
    num_total_proposals: u64,
    rewards_rate: u64,
    rewards_rate_denominator: u64
): u64 {
    spec {
        // The following condition must hold because
        // (1) num_successful_proposals <= num_total_proposals, and
        // (2) `num_total_proposals` cannot be larger than 86400, the maximum number of proposals
        //     in a day (1 proposal per second), and `num_total_proposals` is reset to 0 every epoch.
        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);
    let rewards_denominator =
        (rewards_rate_denominator as u128) * (num_total_proposals as u128);
    if (rewards_denominator > 0) {
        ((rewards_numerator / rewards_denominator) as u64)
    } else { 0 }
}

fun distribute_rewards(
    stake: &mut Coin<AptosCoin>,
    num_successful_proposals: u64,
    num_total_proposals: u64,
    rewards_rate: u64,
    rewards_rate_denominator: u64
): u64 acquires AptosCoinCapabilities {
    let stake_amount = coin::value(stake);
    let rewards_amount =
        if (stake_amount > 0) {
            calculate_rewards_amount(
                stake_amount,
                num_successful_proposals,
                num_total_proposals,
                rewards_rate,
                rewards_rate_denominator
            )
        } else { 0 };
    if (rewards_amount > 0) {
        let mint_cap =
            &borrow_global<AptosCoinCapabilities>(@aptos_framework).mint_cap;
        let rewards = coin::mint(rewards_amount, mint_cap);
        coin::merge(stake, rewards);
    };
    rewards_amount
}

fun append<T>(v1: &mut vector<T>, v2: &mut vector<T>) {
    while (!v2.is_empty()) {
        v1.push_back(v2.pop_back());
    }
}

fun find_validator(v: &vector<ValidatorInfo>, addr: address): Option<u64> {
    let i = 0;
    let len = v.length();
    while ({
        spec {
            invariant !(exists j in 0..i: v[j].addr == addr);
        };
        i < len
    }) {
        if (v.borrow(i).addr == addr) {
            return option::some(i)
        };
        i += 1;
    };
    option::none()
}

fun generate_validator_info(
    addr: address, stake_pool: &StakePool, config: ValidatorConfig
): ValidatorInfo {
    let voting_power = get_voting_power(stake_pool);
    ValidatorInfo { addr, voting_power, config }
}

fun get_voting_power(stake_pool: &StakePool): u64 {
    let value_pending_active = coin::value(&stake_pool.pending_active);
    let value_active = coin::value(&stake_pool.active);
    let value_pending_inactive = coin::value(&stake_pool.pending_inactive);
    spec {
        assume value_pending_active + value_active + value_pending_inactive
            <= MAX_U64;
    };
    value_pending_active + value_active + value_pending_inactive
}

fun update_voting_power_increase(increase_amount: u64) acquires ValidatorSet {
    let validator_set = borrow_global_mut<ValidatorSet>(@aptos_framework);
    let voting_power_increase_limit =
        (
            staking_config::get_voting_power_increase_limit(&staking_config::get()) as u128
        );
    validator_set.total_joining_power +=(increase_amount as u128);

    // Only validator voting power increase if the current validator set's voting power > 0.
    if (validator_set.total_voting_power > 0) {
        assert!(
            validator_set.total_joining_power
                <= validator_set.total_voting_power * voting_power_increase_limit
                    / 100,
            error::invalid_argument(EVOTING_POWER_INCREASE_EXCEEDS_LIMIT)
        );
    }
}

fun assert_stake_pool_exists(pool_address: address) {
    assert!(
        stake_pool_exists(pool_address),
        error::invalid_argument(ESTAKE_POOL_DOES_NOT_EXIST)
    );
}

public fun configure_allowed_validators(
    aptos_framework: &signer, accounts: vector<address>
) acquires AllowedValidators {
    let aptos_framework_address = signer::address_of(aptos_framework);
    system_addresses::assert_aptos_framework(aptos_framework);
    if (!exists<AllowedValidators>(aptos_framework_address)) {
        move_to(aptos_framework, AllowedValidators { accounts });
    } else {
        let allowed = borrow_global_mut<AllowedValidators>(aptos_framework_address);
        allowed.accounts = accounts;
    }
}

fun is_allowed(account: address): bool acquires AllowedValidators {
    if (!exists<AllowedValidators>(@aptos_framework)) { true }
    else {
        let allowed = borrow_global<AllowedValidators>(@aptos_framework);
        allowed.accounts.contains(&account)
    }
}

fun assert_owner_cap_exists(owner: address) {
    assert!(
        exists<OwnerCapability>(owner),
        error::not_found(EOWNER_CAP_NOT_FOUND)
    );
}

fun assert_reconfig_not_in_progress() {
    assert!(
        !reconfiguration_state::is_in_progress(),
        error::invalid_state(ERECONFIGURATION_IN_PROGRESS)
    );
}