Module 0x1::reconfiguration_state

Reconfiguration meta-state resources and util functions.

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

• Resource State
• Struct StateInactive
• Struct StateActive
• Constants
• Function is_initialized
• Function initialize
• Function initialize_for_testing
• Function is_in_progress
• Function on_reconfig_start
• Function start_time_secs
• Function on_reconfig_finish
• Specification
  • Resource State
  • Function initialize
  • Function initialize_for_testing
  • Function is_in_progress
  • Function on_reconfig_start
  • Function start_time_secs

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

Resource State

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

struct State has key

Struct StateInactive

A state variant indicating no reconfiguration is in progress.

struct StateInactive has copy, drop, store

Struct StateActive

A state variant indicating a reconfiguration is in progress.

struct StateActive has copy, drop, store

Constants

const ERECONFIG_NOT_IN_PROGRESS: u64 = 1;

Function is_initialized

public fun is_initialized(): bool

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

Function initialize

public fun initialize(fx: &signer)

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 {})
            }
        )
    }
}

Function initialize_for_testing

public fun initialize_for_testing(fx: &signer)

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

Function is_in_progress

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

public(friend) fun is_in_progress(): bool

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 = *state.variant.type_name().bytes();
    variant_type_name == b"0x1::reconfiguration_state::StateActive"
}

Function 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()

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 = *state.variant.type_name().bytes();
        if (variant_type_name == b"0x1::reconfiguration_state::StateInactive") {
            state.variant = copyable_any::pack(
                StateActive { start_time_secs: timestamp::now_seconds() }
            );
        }
    };
}

Function 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

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

Function 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()

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 = *state.variant.type_name().bytes();
        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);

Resource 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;

Function 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);

Function initialize_for_testing

public fun initialize_for_testing(fx: &signer)

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

Function 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"
   }
}

Function 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);

Function 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";
}