reconfiguration - [mainnet]

Publishes configuration information for validators, and issues reconfiguration events to synchronize configuration changes for the validators.

use 0x1::account;
use 0x1::chain_status;
use 0x1::error;
use 0x1::event;
use 0x1::features;
use 0x1::reconfiguration_state;
use 0x1::signer;
use 0x1::stake;
use 0x1::storage_gas;
use 0x1::system_addresses;
use 0x1::timestamp;

Constants

A Reconfiguration resource is in an invalid state

const ECONFIG: u64 = 2;

The Configuration resource is in an invalid state

const ECONFIGURATION: u64 = 1;

An invalid block time was encountered.

const EINVALID_BLOCK_TIME: u64 = 4;

An invalid block time was encountered.

const EINVALID_GUID_FOR_EVENT: u64 = 5;

A ModifyConfigCapability is in a different state than was expected

const EMODIFY_CAPABILITY: u64 = 3;

Structs

`NewEpochEvent`

Event that signals consensus to start a new epoch, with new configuration information. This is also called a “reconfiguration event”

#[event]
struct NewEpochEvent has drop, store

Fields

epoch: u64

`NewEpoch`

Event that signals consensus to start a new epoch, with new configuration information. This is also called a “reconfiguration event”

#[event]
struct NewEpoch has drop, store

Fields

epoch: u64

Resources

`Configuration`

Holds information about state of reconfiguration

struct Configuration has key

Fields

epoch: u64: Epoch number
last_reconfiguration_time: u64: Time of last reconfiguration. Only changes on reconfiguration events.
events: event::EventHandle<reconfiguration::NewEpochEvent>: Event handle for reconfiguration events

`DisableReconfiguration`

Reconfiguration will be disabled if this resource is published under the aptos_framework system address

struct DisableReconfiguration has key

Fields

dummy_field: bool

Functions

`initialize`

Only called during genesis. Publishes Configuration resource. Can only be invoked by aptos framework account, and only a single time in Genesis.

public(friend) fun initialize(aptos_framework: &signer)

Implementation

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

    // assert it matches `new_epoch_event_key()`, otherwise the event can't be recognized
    assert!(account::get_guid_next_creation_num(signer::address_of(aptos_framework)) == 2, error::invalid_state(EINVALID_GUID_FOR_EVENT));
    move_to<Configuration>(
        aptos_framework,
        Configuration {
            epoch: 0,
            last_reconfiguration_time: 0,
            events: account::new_event_handle<NewEpochEvent>(aptos_framework),
        }
    );
}

`disable_reconfiguration`

Private function to temporarily halt reconfiguration. This function should only be used for offline WriteSet generation purpose and should never be invoked on chain.

fun disable_reconfiguration(aptos_framework: &signer)

Implementation

fun disable_reconfiguration(aptos_framework: &signer) {
    system_addresses::assert_aptos_framework(aptos_framework);
    assert!(reconfiguration_enabled(), error::invalid_state(ECONFIGURATION));
    move_to(aptos_framework, DisableReconfiguration {})
}

`enable_reconfiguration`

Private function to resume reconfiguration. This function should only be used for offline WriteSet generation purpose and should never be invoked on chain.

fun enable_reconfiguration(aptos_framework: &signer)

Implementation

fun enable_reconfiguration(aptos_framework: &signer) acquires DisableReconfiguration {
    system_addresses::assert_aptos_framework(aptos_framework);

    assert!(!reconfiguration_enabled(), error::invalid_state(ECONFIGURATION));
    DisableReconfiguration {} = move_from<DisableReconfiguration>(signer::address_of(aptos_framework));
}

`reconfiguration_enabled`

fun reconfiguration_enabled(): bool

Implementation

fun reconfiguration_enabled(): bool {
    !exists<DisableReconfiguration>(@aptos_framework)
}

`reconfigure`

Signal validators to start using new configuration. Must be called from friend config modules.

public(friend) fun reconfigure()

Implementation

public(friend) fun reconfigure() acquires Configuration {
    // Do not do anything if genesis has not finished.
    if (chain_status::is_genesis() || timestamp::now_microseconds() == 0 || !reconfiguration_enabled()) {
        return
    };

    let config_ref = borrow_global_mut<Configuration>(@aptos_framework);
    let current_time = timestamp::now_microseconds();

    // Do not do anything if a reconfiguration event is already emitted within this transaction.
    //
    // This is OK because:
    // - The time changes in every non-empty block
    // - A block automatically ends after a transaction that emits a reconfiguration event, which is guaranteed by
    //   VM spec that all transactions comming after a reconfiguration transaction will be returned as Retry
    //   status.
    // - Each transaction must emit at most one reconfiguration event
    //
    // Thus, this check ensures that a transaction that does multiple "reconfiguration required" actions emits only
    // one reconfiguration event.
    //
    if (current_time == config_ref.last_reconfiguration_time) {
        return
    };

    reconfiguration_state::on_reconfig_start();

    // Call stake to compute the new validator set and distribute rewards and transaction fees.
    stake::on_new_epoch();
    storage_gas::on_reconfig();

    assert!(current_time > config_ref.last_reconfiguration_time, error::invalid_state(EINVALID_BLOCK_TIME));
    config_ref.last_reconfiguration_time = current_time;
    spec {
        assume config_ref.epoch + 1 <= MAX_U64;
    };
    config_ref.epoch = config_ref.epoch + 1;

    if (std::features::module_event_migration_enabled()) {
        event::emit(
            NewEpoch {
                epoch: config_ref.epoch,
            },
        );
    };
    event::emit_event<NewEpochEvent>(
        &mut config_ref.events,
        NewEpochEvent {
            epoch: config_ref.epoch,
        },
    );

    reconfiguration_state::on_reconfig_finish();
}

`last_reconfiguration_time`

public fun last_reconfiguration_time(): u64

Implementation

public fun last_reconfiguration_time(): u64 acquires Configuration {
    borrow_global<Configuration>(@aptos_framework).last_reconfiguration_time
}

`current_epoch`

public fun current_epoch(): u64

Implementation

public fun current_epoch(): u64 acquires Configuration {
    borrow_global<Configuration>(@aptos_framework).epoch
}

`emit_genesis_reconfiguration_event`

Emit a NewEpochEvent event. This function will be invoked by genesis directly to generate the very first reconfiguration event.

fun emit_genesis_reconfiguration_event()

Implementation

fun emit_genesis_reconfiguration_event() acquires Configuration {
    let config_ref = borrow_global_mut<Configuration>(@aptos_framework);
    assert!(config_ref.epoch == 0 && config_ref.last_reconfiguration_time == 0, error::invalid_state(ECONFIGURATION));
    config_ref.epoch = 1;

    if (std::features::module_event_migration_enabled()) {
        event::emit(
            NewEpoch {
                epoch: config_ref.epoch,
            },
        );
    };
    event::emit_event<NewEpochEvent>(
        &mut config_ref.events,
        NewEpochEvent {
            epoch: config_ref.epoch,
        },
    );
}

Specification

High-level Requirements

No.	Requirement	Criticality	Implementation	Enforcement
1	The Configuration resource is stored under the Aptos framework account with initial values upon module's initialization.	Medium	The Configuration resource may only be initialized with specific values and published under the aptos_framework account.	Formally verified via initialize.
2	The reconfiguration status may be determined at any time without causing an abort, indicating whether or not the system allows reconfiguration.	Low	The reconfiguration_enabled function will never abort and always returns a boolean value that accurately represents whether the system allows reconfiguration.	Formally verified via reconfiguration_enabled.
3	For each reconfiguration, the epoch value (config_ref.epoch) increases by 1, and one 'NewEpochEvent' is emitted.	Critical	After reconfiguration, the reconfigure() function increases the epoch value of the configuration by one and increments the counter of the NewEpochEvent's EventHandle by one.	Audited that these two values remain in sync.
4	Reconfiguration is possible only if genesis has started and reconfiguration is enabled. Also, the last reconfiguration must not be the current time, returning early without further actions otherwise.	High	The reconfigure() function may only execute to perform successful reconfiguration when genesis has started and when reconfiguration is enabled. Without satisfying both conditions, the function returns early without executing any further actions.	Formally verified via reconfigure.
5	Consecutive reconfigurations without the passage of time are not permitted.	High	The reconfigure() function enforces the restriction that reconfiguration may only be performed when the current time is not equal to the last_reconfiguration_time.	Formally verified via reconfigure.

Module-level Specification

pragma verify = true;
pragma aborts_if_is_strict;
invariant [suspendable] chain_status::is_operating() ==> exists<Configuration>(@aptos_framework);
invariant [suspendable] chain_status::is_operating() ==>
    (timestamp::spec_now_microseconds() >= last_reconfiguration_time());

Make sure the signer address is @aptos_framework.

schema AbortsIfNotAptosFramework {
    aptos_framework: &signer;
    let addr = signer::address_of(aptos_framework);
    aborts_if !system_addresses::is_aptos_framework_address(addr);
}

`initialize`

public(friend) fun initialize(aptos_framework: &signer)

Address @aptos_framework must exist resource Account and Configuration. Already exists in framework account. Guid_creation_num should be 2 according to logic.

include AbortsIfNotAptosFramework;
let addr = signer::address_of(aptos_framework);
let post config = global<Configuration>(@aptos_framework);
requires exists<Account>(addr);
aborts_if !(global<Account>(addr).guid_creation_num == 2);
aborts_if exists<Configuration>(@aptos_framework);
// This enforces high-level requirement 1:
ensures exists<Configuration>(@aptos_framework);
ensures config.epoch == 0 && config.last_reconfiguration_time == 0;
ensures config.events == event::EventHandle<NewEpochEvent> {
    counter: 0,
    guid: guid::GUID {
        id: guid::ID {
            creation_num: 2,
            addr: @aptos_framework
        }
    }
};

`disable_reconfiguration`

fun disable_reconfiguration(aptos_framework: &signer)

include AbortsIfNotAptosFramework;
aborts_if exists<DisableReconfiguration>(@aptos_framework);
ensures exists<DisableReconfiguration>(@aptos_framework);

`enable_reconfiguration`

fun enable_reconfiguration(aptos_framework: &signer)

Make sure the caller is admin and check the resource DisableReconfiguration.

include AbortsIfNotAptosFramework;
aborts_if !exists<DisableReconfiguration>(@aptos_framework);
ensures !exists<DisableReconfiguration>(@aptos_framework);

`reconfiguration_enabled`

fun reconfiguration_enabled(): bool

// This enforces high-level requirement 2:
aborts_if false;
ensures result == !exists<DisableReconfiguration>(@aptos_framework);

`reconfigure`

public(friend) fun reconfigure()

pragma verify = true;
pragma verify_duration_estimate = 600;
let success = !(chain_status::is_genesis() || timestamp::spec_now_microseconds() == 0 || !reconfiguration_enabled())
    && timestamp::spec_now_microseconds() != global<Configuration>(@aptos_framework).last_reconfiguration_time;
include features::spec_periodical_reward_rate_decrease_enabled() ==> staking_config::StakingRewardsConfigEnabledRequirement;
include success ==> aptos_coin::ExistsAptosCoin;
aborts_if false;
ensures success ==> global<Configuration>(@aptos_framework).epoch == old(global<Configuration>(@aptos_framework).epoch) + 1;
ensures success ==> global<Configuration>(@aptos_framework).last_reconfiguration_time == timestamp::spec_now_microseconds();
// This enforces high-level requirement 4 and high-level requirement 5:
ensures !success ==> global<Configuration>(@aptos_framework).epoch == old(global<Configuration>(@aptos_framework).epoch);

`last_reconfiguration_time`

public fun last_reconfiguration_time(): u64

aborts_if !exists<Configuration>(@aptos_framework);
ensures result == global<Configuration>(@aptos_framework).last_reconfiguration_time;

`current_epoch`

public fun current_epoch(): u64

aborts_if !exists<Configuration>(@aptos_framework);
ensures result == global<Configuration>(@aptos_framework).epoch;

`emit_genesis_reconfiguration_event`

fun emit_genesis_reconfiguration_event()

When genesis_event emit the epoch and the last_reconfiguration_time . Should equal to 0

aborts_if !exists<Configuration>(@aptos_framework);
let config_ref = global<Configuration>(@aptos_framework);
aborts_if !(config_ref.epoch == 0 && config_ref.last_reconfiguration_time == 0);
ensures global<Configuration>(@aptos_framework).epoch == 1;