Skip to content

Latest commit

 

History

History
1088 lines (643 loc) · 43.6 KB

DiemConfig.md

File metadata and controls

1088 lines (643 loc) · 43.6 KB

Module 0x1::DiemConfig

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

use 0x1::CoreAddresses;
use 0x1::DiemTimestamp;
use 0x1::Errors;
use 0x1::Event;
use 0x1::Roles;
use 0x1::Signer;

Resource DiemConfig

A generic singleton resource that holds a value of a specific type.

resource struct DiemConfig<Config: copyable>
Fields
payload: Config
Holds specific info for instance of Config type.

Struct NewEpochEvent

Event that signals DiemBFT algorithm to start a new epoch, with new configuration information. This is also called a "reconfiguration event"

struct NewEpochEvent
Fields
epoch: u64

Resource Configuration

Holds information about state of reconfiguration

resource struct Configuration
Fields
epoch: u64
Epoch number
last_reconfiguration_time: u64
Time of last reconfiguration. Only changes on reconfiguration events.
events: Event::EventHandle<DiemConfig::NewEpochEvent>
Event handle for reconfiguration events

Resource ModifyConfigCapability

Accounts with this privilege can modify DiemConfig under Diem root address.

resource struct ModifyConfigCapability<TypeName>
Fields
dummy_field: bool

Resource DisableReconfiguration

Reconfiguration disabled if this resource occurs under LibraRoot.

resource struct DisableReconfiguration
Fields
dummy_field: bool

Constants

The largest possible u64 value

const MAX_U64: u64 = 18446744073709551615;

The Configuration resource is in an invalid state

const ECONFIGURATION: u64 = 0;

A DiemConfig resource is in an invalid state

const EDIEM_CONFIG: u64 = 1;

An invalid block time was encountered.

const EINVALID_BLOCK_TIME: u64 = 3;

A ModifyConfigCapability is in a different state than was expected

const EMODIFY_CAPABILITY: u64 = 2;

Function initialize

Publishes Configuration resource. Can only be invoked by Diem root, and only a single time in Genesis.

public fun initialize(dr_account: &signer)
Implementation 
public fun initialize(
    dr_account: &signer,
) {
    DiemTimestamp::assert_genesis();
    CoreAddresses::assert_diem_root(dr_account);
    assert(!exists<Configuration>(CoreAddresses::DIEM_ROOT_ADDRESS()), Errors::already_published(ECONFIGURATION));
    move_to<Configuration>(
        dr_account,
        Configuration {
            epoch: 0,
            last_reconfiguration_time: 0,
            events: Event::new_event_handle<NewEpochEvent>(dr_account),
        }
    );
}
Specification 
pragma opaque;
include InitializeAbortsIf;
include InitializeEnsures;
modifies global<Configuration>(CoreAddresses::DIEM_ROOT_ADDRESS());


schema InitializeAbortsIf {
    dr_account: signer;
    include DiemTimestamp::AbortsIfNotGenesis;
    include CoreAddresses::AbortsIfNotDiemRoot{account: dr_account};
    aborts_if spec_has_config() with Errors::ALREADY_PUBLISHED;
}


schema InitializeEnsures {
    ensures spec_has_config();
    
    let new_config = global<Configuration>(CoreAddresses::DIEM_ROOT_ADDRESS());
    ensures new_config.epoch == 0;
    ensures new_config.last_reconfiguration_time == 0;
}

Function get

Returns a copy of Config value stored under addr.

public fun get<Config: copyable>(): Config
Implementation 
public fun get<Config: copyable>(): Config
acquires DiemConfig {
    let addr = CoreAddresses::DIEM_ROOT_ADDRESS();
    assert(exists<DiemConfig<Config>>(addr), Errors::not_published(EDIEM_CONFIG));
    *&borrow_global<DiemConfig<Config>>(addr).payload
}
Specification 
pragma opaque;
include AbortsIfNotPublished<Config>;
ensures result == get<Config>();


schema AbortsIfNotPublished<Config> {
    aborts_if !exists<DiemConfig<Config>>(CoreAddresses::DIEM_ROOT_ADDRESS()) with Errors::NOT_PUBLISHED;
}

Function set

Set a config item to a new value with the default capability stored under config address and trigger a reconfiguration. This function requires that the signer have a ModifyConfigCapability<Config> resource published under it.

public fun set<Config: copyable>(account: &signer, payload: Config)
Implementation 
public fun set<Config: copyable>(account: &signer, payload: Config)
acquires DiemConfig, Configuration {
    let signer_address = Signer::address_of(account);
    // Next should always be true if properly initialized.
    assert(exists<ModifyConfigCapability<Config>>(signer_address), Errors::requires_capability(EMODIFY_CAPABILITY));

    let addr = CoreAddresses::DIEM_ROOT_ADDRESS();
    assert(exists<DiemConfig<Config>>(addr), Errors::not_published(EDIEM_CONFIG));
    let config = borrow_global_mut<DiemConfig<Config>>(addr);
    config.payload = payload;

    reconfigure_();
}
Specification

TODO: turned off verification until we solve the generic type/specific invariant issue

pragma opaque, verify = false;
modifies global<Configuration>(CoreAddresses::DIEM_ROOT_ADDRESS());
include SetAbortsIf<Config>;
include SetEnsures<Config>;


schema SetAbortsIf<Config> {
    account: signer;
    include AbortsIfNotModifiable<Config>;
    include AbortsIfNotPublished<Config>;
    include ReconfigureAbortsIf;
}


schema AbortsIfNotModifiable<Config> {
    account: signer;
    aborts_if !exists<ModifyConfigCapability<Config>>(Signer::spec_address_of(account))
        with Errors::REQUIRES_CAPABILITY;
}


schema SetEnsures<Config> {
    payload: Config;
    ensures spec_is_published<Config>();
    ensures get<Config>() == payload;
    ensures old(spec_has_config()) == spec_has_config();
}

Function set_with_capability_and_reconfigure

Set a config item to a new value and trigger a reconfiguration. This function requires a reference to a ModifyConfigCapability, which is returned when the config is published using publish_new_config_and_get_capability. It is called by DiemSystem::update_config_and_reconfigure, which allows validator operators to change the validator set. All other config changes require a Diem root signer.

public fun set_with_capability_and_reconfigure<Config: copyable>(_cap: &DiemConfig::ModifyConfigCapability<Config>, payload: Config)
Implementation 
public fun set_with_capability_and_reconfigure<Config: copyable>(
    _cap: &ModifyConfigCapability<Config>,
    payload: Config
) acquires DiemConfig, Configuration {
    let addr = CoreAddresses::DIEM_ROOT_ADDRESS();
    assert(exists<DiemConfig<Config>>(addr), Errors::not_published(EDIEM_CONFIG));
    let config = borrow_global_mut<DiemConfig<Config>>(addr);
    config.payload = payload;
    reconfigure_();
}
Specification

TODO: turned off verification until we solve the generic type/specific invariant issue

pragma opaque, verify = false;
modifies global<Configuration>(CoreAddresses::DIEM_ROOT_ADDRESS());
include AbortsIfNotPublished<Config>;
include ReconfigureAbortsIf;
modifies global<DiemConfig<Config>>(CoreAddresses::DIEM_ROOT_ADDRESS());
include SetEnsures<Config>;

Function 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(dr_account: &signer)
Implementation 
fun disable_reconfiguration(dr_account: &signer) {
    assert(
        Signer::address_of(dr_account) == CoreAddresses::DIEM_ROOT_ADDRESS(),
        Errors::requires_address(EDIEM_CONFIG)
    );
    Roles::assert_diem_root(dr_account);
    assert(reconfiguration_enabled(), Errors::invalid_state(ECONFIGURATION));
    move_to(dr_account, DisableReconfiguration {} )
}

Function 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(dr_account: &signer)
Implementation 
fun enable_reconfiguration(dr_account: &signer) acquires DisableReconfiguration {
    assert(
        Signer::address_of(dr_account) == CoreAddresses::DIEM_ROOT_ADDRESS(),
        Errors::requires_address(EDIEM_CONFIG)
    );
    Roles::assert_diem_root(dr_account);

    assert(!reconfiguration_enabled(), Errors::invalid_state(ECONFIGURATION));
    DisableReconfiguration {} = move_from<DisableReconfiguration>(Signer::address_of(dr_account));
}

Function reconfiguration_enabled

fun reconfiguration_enabled(): bool
Implementation 
fun reconfiguration_enabled(): bool {
    !exists<DisableReconfiguration>(CoreAddresses::DIEM_ROOT_ADDRESS())
}

Function publish_new_config_and_get_capability

Publishes a new config. The caller will use the returned ModifyConfigCapability to specify the access control policy for who can modify the config. Does not trigger a reconfiguration.

public fun publish_new_config_and_get_capability<Config: copyable>(dr_account: &signer, payload: Config): DiemConfig::ModifyConfigCapability<Config>
Implementation 
public fun publish_new_config_and_get_capability<Config: copyable>(
    dr_account: &signer,
    payload: Config,
): ModifyConfigCapability<Config> {
    DiemTimestamp::assert_genesis();
    Roles::assert_diem_root(dr_account);
    assert(
        !exists<DiemConfig<Config>>(Signer::address_of(dr_account)),
        Errors::already_published(EDIEM_CONFIG)
    );
    move_to(dr_account, DiemConfig { payload });
    ModifyConfigCapability<Config> {}
}
Specification

TODO: turned off verification until we solve the generic type/specific invariant issue

pragma opaque, verify = false;
modifies global<DiemConfig<Config>>(CoreAddresses::DIEM_ROOT_ADDRESS());
include DiemTimestamp::AbortsIfNotGenesis;
include Roles::AbortsIfNotDiemRoot{account: dr_account};
include AbortsIfPublished<Config>;
include SetEnsures<Config>;


schema AbortsIfPublished<Config> {
    aborts_if exists<DiemConfig<Config>>(CoreAddresses::DIEM_ROOT_ADDRESS()) with Errors::ALREADY_PUBLISHED;
}

Function publish_new_config

Publish a new config item. Only Diem root can modify such config. Publishes the capability to modify this config under the Diem root account. Does not trigger a reconfiguration.

public fun publish_new_config<Config: copyable>(dr_account: &signer, payload: Config)
Implementation 
public fun publish_new_config<Config: copyable>(
    dr_account: &signer,
    payload: Config
) {
    let capability = publish_new_config_and_get_capability<Config>(dr_account, payload);
    assert(
        !exists<ModifyConfigCapability<Config>>(Signer::address_of(dr_account)),
        Errors::already_published(EMODIFY_CAPABILITY)
    );
    move_to(dr_account, capability);
}
Specification 
pragma opaque;
modifies global<DiemConfig<Config>>(CoreAddresses::DIEM_ROOT_ADDRESS());
modifies global<ModifyConfigCapability<Config>>(CoreAddresses::DIEM_ROOT_ADDRESS());
include PublishNewConfigAbortsIf<Config>;
include PublishNewConfigEnsures<Config>;


schema PublishNewConfigAbortsIf<Config> {
    dr_account: signer;
    include DiemTimestamp::AbortsIfNotGenesis;
    include Roles::AbortsIfNotDiemRoot{account: dr_account};
    aborts_if spec_is_published<Config>();
    aborts_if exists<ModifyConfigCapability<Config>>(Signer::spec_address_of(dr_account));
}


schema PublishNewConfigEnsures<Config> {
    dr_account: signer;
    payload: Config;
    include SetEnsures<Config>;
    ensures exists<ModifyConfigCapability<Config>>(Signer::spec_address_of(dr_account));
}

Function reconfigure

Signal validators to start using new configuration. Must be called by Diem root.

public fun reconfigure(dr_account: &signer)
Implementation 
public fun reconfigure(
    dr_account: &signer,
) acquires Configuration {
    Roles::assert_diem_root(dr_account);
    reconfigure_();
}
Specification 
pragma opaque;
modifies global<Configuration>(CoreAddresses::DIEM_ROOT_ADDRESS());
include Roles::AbortsIfNotDiemRoot{account: dr_account};
include ReconfigureAbortsIf;

Function reconfigure_

Private function to do reconfiguration. Updates reconfiguration status resource Configuration and emits a NewEpochEvent

fun reconfigure_()
Implementation 
fun reconfigure_() acquires Configuration {
    // Do not do anything if genesis has not finished.
    if (DiemTimestamp::is_genesis() || DiemTimestamp::now_microseconds() == 0 || !reconfiguration_enabled()) {
        return ()
    };

    let config_ref = borrow_global_mut<Configuration>(CoreAddresses::DIEM_ROOT_ADDRESS());
    let current_time = DiemTimestamp::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
    //   DiemVM 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
    };

    assert(current_time > config_ref.last_reconfiguration_time, Errors::invalid_state(EINVALID_BLOCK_TIME));
    config_ref.last_reconfiguration_time = current_time;
    config_ref.epoch = config_ref.epoch + 1;

    Event::emit_event<NewEpochEvent>(
        &mut config_ref.events,
        NewEpochEvent {
            epoch: config_ref.epoch,
        },
    );
}
Specification 
pragma opaque;
modifies global<Configuration>(CoreAddresses::DIEM_ROOT_ADDRESS());
ensures old(spec_has_config()) == spec_has_config();

let config = global<Configuration>(CoreAddresses::DIEM_ROOT_ADDRESS());

let now = DiemTimestamp::spec_now_microseconds();

let epoch = config.epoch;
include !spec_reconfigure_omitted() || (config.last_reconfiguration_time == now)
    ==> InternalReconfigureAbortsIf && ReconfigureAbortsIf;
ensures spec_reconfigure_omitted() || (old(config).last_reconfiguration_time == now)
    ==> config == old(config);
ensures !(spec_reconfigure_omitted() || (config.last_reconfiguration_time == now))
    ==> config ==
        update_field(
        update_field(old(config),
            epoch, old(config.epoch) + 1),
            last_reconfiguration_time, now);

The following schema describes aborts conditions which we do not want to be propagated to the verification of callers, and which are therefore marked as concrete to be only verified against the implementation. These conditions are unlikely to happen in reality, and excluding them avoids formal noise.

schema InternalReconfigureAbortsIf {
    let config = global<Configuration>(CoreAddresses::DIEM_ROOT_ADDRESS());
    
    let current_time = DiemTimestamp::spec_now_microseconds();
    aborts_if [concrete] current_time < config.last_reconfiguration_time with Errors::INVALID_STATE;
    aborts_if [concrete] config.epoch == MAX_U64
        && current_time != config.last_reconfiguration_time with EXECUTION_FAILURE;
}

This schema is to be used by callers of reconfigure

schema ReconfigureAbortsIf {
    let config = global<Configuration>(CoreAddresses::DIEM_ROOT_ADDRESS());
    
    let current_time = DiemTimestamp::spec_now_microseconds();
    aborts_if DiemTimestamp::is_operating()
        && reconfiguration_enabled()
        && DiemTimestamp::spec_now_microseconds() > 0
        && config.epoch < MAX_U64
        && current_time < config.last_reconfiguration_time
            with Errors::INVALID_STATE;
}

Function 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 {
    assert(exists<Configuration>(CoreAddresses::DIEM_ROOT_ADDRESS()), Errors::not_published(ECONFIGURATION));
    let config_ref = borrow_global_mut<Configuration>(CoreAddresses::DIEM_ROOT_ADDRESS());
    assert(config_ref.epoch == 0 && config_ref.last_reconfiguration_time == 0, Errors::invalid_state(ECONFIGURATION));
    config_ref.epoch = 1;

    Event::emit_event<NewEpochEvent>(
        &mut config_ref.events,
        NewEpochEvent {
            epoch: config_ref.epoch,
        },
    );
}

Module Specification

define spec_reconfigure_omitted(): bool {
  DiemTimestamp::is_genesis() || DiemTimestamp::spec_now_microseconds() == 0 || !reconfiguration_enabled()
}

Initialization

After genesis, the Configuration is published.

invariant [global] DiemTimestamp::is_operating() ==> spec_has_config();

Invariants

Configurations are only stored at the diem root address.

invariant [global]
    forall config_address: address, config_type: type where exists<DiemConfig<config_type>>(config_address):
        config_address == CoreAddresses::DIEM_ROOT_ADDRESS();

After genesis, no new configurations are added.

invariant update [global]
    DiemTimestamp::is_operating() ==>
        (forall config_type: type where spec_is_published<config_type>(): old(spec_is_published<config_type>()));

Published configurations are persistent.

invariant update [global]
    (forall config_type: type where old(spec_is_published<config_type>()): spec_is_published<config_type>());

If ModifyConfigCapability<Config> is published, it is persistent.

invariant update [global] forall config_type: type
    where old(exists<ModifyConfigCapability<config_type>>(CoreAddresses::DIEM_ROOT_ADDRESS())):
        exists<ModifyConfigCapability<config_type>>(CoreAddresses::DIEM_ROOT_ADDRESS());

Helper Functions

define spec_has_config(): bool {
    exists<Configuration>(CoreAddresses::DIEM_ROOT_ADDRESS())
}

define spec_is_published<Config>(): bool {
    exists<DiemConfig<Config>>(CoreAddresses::DIEM_ROOT_ADDRESS())
}

define spec_get_config<Config>(): Config {
    global<DiemConfig<Config>>(CoreAddresses::DIEM_ROOT_ADDRESS()).payload
}