reconfiguration_state - [mainnet]

Reconfiguration meta-state resources and util functions.

WARNING: reconfiguration_state::initialize() is required before RECONFIGURE_WITH_DKG can be enabled.

use 0x1::copyable_any;
use 0x1::error;
use 0x1::string;
use 0x1::system_addresses;
use 0x1::timestamp;

Constants

const ERECONFIG_NOT_IN_PROGRESS: u64 = 1;

Structs

`StateInactive`

A state variant indicating no reconfiguration is in progress.

struct StateInactive has copy, drop, store

Fields

dummy_field: bool

`StateActive`

A state variant indicating a reconfiguration is in progress.

struct StateActive has copy, drop, store

Fields

start_time_secs: u64

Resources

`State`

Reconfiguration drivers update this resources to notify other modules of some reconfiguration state.

struct State has key

Fields

variant: copyable_any::Any: The state variant packed as an Any. Currently the variant type is one of the following. - ReconfigStateInactive - ReconfigStateActive

Functions

`is_initialized`

public fun is_initialized(): bool

Implementation

public fun is_initialized(): bool {
    exists<State>(@aptos_framework)
}

`initialize`

public fun initialize(fx: &signer)

Implementation

public fun initialize(fx: &signer) {
    system_addresses::assert_aptos_framework(fx);
    if (!exists<State>(@aptos_framework)) {
        move_to(fx, State {
            variant: copyable_any::pack(StateInactive {})
        })
    }
}

`initialize_for_testing`

public fun initialize_for_testing(fx: &signer)

Implementation

public fun initialize_for_testing(fx: &signer) {
    initialize(fx)
}

`is_in_progress`

Return whether the reconfiguration state is marked “in progress”.

public(friend) fun is_in_progress(): bool

Implementation

public(friend) fun is_in_progress(): bool acquires State {
    if (!exists<State>(@aptos_framework)) {
        return false
    };

    let state = borrow_global<State>(@aptos_framework);
    let variant_type_name = *string::bytes(copyable_any::type_name(&state.variant));
    variant_type_name == b"0x1::reconfiguration_state::StateActive"
}

`on_reconfig_start`

Called at the beginning of a reconfiguration (either immediate or async) to mark the reconfiguration state “in progress” if it is currently “stopped”.

Also record the current time as the reconfiguration start time. (Some module, e.g., stake.move, needs this info).

public(friend) fun on_reconfig_start()

Implementation

public(friend) fun on_reconfig_start() acquires State {
    if (exists<State>(@aptos_framework)) {
        let state = borrow_global_mut<State>(@aptos_framework);
        let variant_type_name = *string::bytes(copyable_any::type_name(&state.variant));
        if (variant_type_name == b"0x1::reconfiguration_state::StateInactive") {
            state.variant = copyable_any::pack(StateActive {
                start_time_secs: timestamp::now_seconds()
            });
        }
    };
}

`start_time_secs`

Get the unix time when the currently in-progress reconfiguration started. Abort if the reconfiguration state is not “in progress”.

public(friend) fun start_time_secs(): u64

Implementation

public(friend) fun start_time_secs(): u64 acquires State {
    let state = borrow_global<State>(@aptos_framework);
    let variant_type_name = *string::bytes(copyable_any::type_name(&state.variant));
    if (variant_type_name == b"0x1::reconfiguration_state::StateActive") {
        let active = copyable_any::unpack<StateActive>(state.variant);
        active.start_time_secs
    } else {
        abort(error::invalid_state(ERECONFIG_NOT_IN_PROGRESS))
    }
}

`on_reconfig_finish`

Called at the end of every reconfiguration to mark the state as “stopped”. Abort if the current state is not “in progress”.

public(friend) fun on_reconfig_finish()

Implementation

public(friend) fun on_reconfig_finish() acquires State {
    if (exists<State>(@aptos_framework)) {
        let state = borrow_global_mut<State>(@aptos_framework);
        let variant_type_name = *string::bytes(copyable_any::type_name(&state.variant));
        if (variant_type_name == b"0x1::reconfiguration_state::StateActive") {
            state.variant = copyable_any::pack(StateInactive {});
        } else {
            abort(error::invalid_state(ERECONFIG_NOT_IN_PROGRESS))
        }
    }
}

Specification

invariant [suspendable] chain_status::is_operating() ==> exists<State>(@aptos_framework);

`State`

struct State has key

variant: copyable_any::Any: The state variant packed as an Any. Currently the variant type is one of the following. - ReconfigStateInactive - ReconfigStateActive

invariant copyable_any::type_name(variant).bytes == b"0x1::reconfiguration_state::StateActive" ||
    copyable_any::type_name(variant).bytes == b"0x1::reconfiguration_state::StateInactive";
invariant copyable_any::type_name(variant).bytes == b"0x1::reconfiguration_state::StateActive"
    ==> from_bcs::deserializable<StateActive>(variant.data);
invariant copyable_any::type_name(variant).bytes == b"0x1::reconfiguration_state::StateInactive"
    ==> from_bcs::deserializable<StateInactive>(variant.data);
invariant copyable_any::type_name(variant).bytes == b"0x1::reconfiguration_state::StateActive" ==>
    type_info::type_name<StateActive>() == variant.type_name;
invariant copyable_any::type_name(variant).bytes == b"0x1::reconfiguration_state::StateInactive" ==>
    type_info::type_name<StateInactive>() == variant.type_name;

`initialize`

public fun initialize(fx: &signer)

aborts_if signer::address_of(fx) != @aptos_framework;
let post post_state = global<State>(@aptos_framework);
ensures exists<State>(@aptos_framework);
ensures !exists<State>(@aptos_framework) ==> from_bcs::deserializable<StateInactive>(post_state.variant.data);

`initialize_for_testing`

public fun initialize_for_testing(fx: &signer)

aborts_if signer::address_of(fx) != @aptos_framework;

`is_in_progress`

public(friend) fun is_in_progress(): bool

aborts_if false;

fun spec_is_in_progress(): bool {
   if (!exists<State>(@aptos_framework)) {
       false
   } else {
       copyable_any::type_name(global<State>(@aptos_framework).variant).bytes == b"0x1::reconfiguration_state::StateActive"
   }
}

`on_reconfig_start`

public(friend) fun on_reconfig_start()

aborts_if false;
requires exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework);
let state = Any {
    type_name: type_info::type_name<StateActive>(),
    data: bcs::serialize(StateActive {
        start_time_secs: timestamp::spec_now_seconds()
    })
};
let pre_state = global<State>(@aptos_framework);
let post post_state = global<State>(@aptos_framework);
ensures (exists<State>(@aptos_framework) && copyable_any::type_name(pre_state.variant).bytes
    == b"0x1::reconfiguration_state::StateInactive") ==> copyable_any::type_name(post_state.variant).bytes
    == b"0x1::reconfiguration_state::StateActive";
ensures (exists<State>(@aptos_framework) && copyable_any::type_name(pre_state.variant).bytes
    == b"0x1::reconfiguration_state::StateInactive") ==> post_state.variant == state;
ensures (exists<State>(@aptos_framework) && copyable_any::type_name(pre_state.variant).bytes
    == b"0x1::reconfiguration_state::StateInactive") ==> from_bcs::deserializable<StateActive>(post_state.variant.data);

`start_time_secs`

public(friend) fun start_time_secs(): u64

include StartTimeSecsAbortsIf;

fun spec_start_time_secs(): u64 {
   use aptos_std::from_bcs;
   let state = global<State>(@aptos_framework);
   from_bcs::deserialize<StateActive>(state.variant.data).start_time_secs
}

schema StartTimeSecsRequirement {
    requires exists<State>(@aptos_framework);
    requires copyable_any::type_name(global<State>(@aptos_framework).variant).bytes
        == b"0x1::reconfiguration_state::StateActive";
    include UnpackRequiresStateActive {
        x:  global<State>(@aptos_framework).variant
    };
}

schema UnpackRequiresStateActive {
    x: Any;
    requires type_info::type_name<StateActive>() == x.type_name && from_bcs::deserializable<StateActive>(x.data);
}

schema StartTimeSecsAbortsIf {
    aborts_if !exists<State>(@aptos_framework);
    include  copyable_any::type_name(global<State>(@aptos_framework).variant).bytes
        == b"0x1::reconfiguration_state::StateActive" ==>
    copyable_any::UnpackAbortsIf<StateActive> {
        self: global<State>(@aptos_framework).variant
    };
    aborts_if copyable_any::type_name(global<State>(@aptos_framework).variant).bytes
        != b"0x1::reconfiguration_state::StateActive";
}