Skip to content

Commit

Permalink
[move-prover][move framework] Cleanup of comments in LibraConfig
Browse files Browse the repository at this point in the history 
Improved comments and formatting, no changes to code or specs.

Closes: aptos-labs#6379
  • Loading branch information
@DavidLDill @bors-libra
DavidLDill authored and bors-libra committed Oct 6, 2020
1 parent 987dc6d commit 57fae95
Show file tree
Hide file tree
Showing 4 changed files with 175 additions and 68 deletions.
112 changes: 74 additions & 38 deletions language/stdlib/modules/LibraConfig.move
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,8 @@
address 0x1 {

/// Publishes configuration information for validators, and issues reconfiguration events
/// to synchronize configuration changes for the validators.
module LibraConfig {
use 0x1::CoreAddresses;
use 0x1::Errors;
Expand All @@ -7,21 +11,30 @@ module LibraConfig {
use 0x1::Signer;
use 0x1::Roles;

// A generic singleton resource that holds a value of a specific type.
resource struct LibraConfig<Config: copyable> { payload: Config }
/// A generic singleton resource that holds a value of a specific type.
resource struct LibraConfig<Config: copyable> {
/// Holds specific info for instance of `Config` type.
payload: Config
}

/// Event that signals LibraBFT algorithm to start a new epoch,
/// with new configuration information. This is also called a
/// "reconfiguration event"
struct NewEpochEvent {
epoch: u64,
}

/// Holds information about state of reconfiguration
resource struct Configuration {
/// Epoch number
epoch: u64,
/// Time of last reconfiguration. Only changes on reconfiguration events.
last_reconfiguration_time: u64,
/// Event handle for reconfiguration events
events: Event::EventHandle<NewEpochEvent>,
}

// Accounts with this privilege can modify config of type TypeName under default_address
// Currently, the capability is only published on Libra root.
/// Accounts with this privilege can modify LibraConfig<TypeName> under Libra root address.
resource struct ModifyConfigCapability<TypeName> {}

/// The `Configuration` resource is in an invalid state
Expand All @@ -32,11 +45,10 @@ module LibraConfig {
const EMODIFY_CAPABILITY: u64 = 2;
/// An invalid block time was encountered.
const EINVALID_BLOCK_TIME: u64 = 4;

/// The largest possible u64 value
const MAX_U64: u64 = 18446744073709551615;

// This can only be invoked by the config address, and only a single time.
// Currently, it is invoked in the genesis transaction
/// Publishes `Configuration` resource. Can only be invoked by Libra root, and only a single time in Genesis.
public fun initialize(
lr_account: &signer,
) {
Expand All @@ -55,20 +67,24 @@ module LibraConfig {
spec fun initialize {
pragma opaque;
include InitializeAbortsIf;
include InitializeEnsures;
modifies global<Configuration>(CoreAddresses::LIBRA_ROOT_ADDRESS());
ensures spec_has_config();
let new_config = global<Configuration>(CoreAddresses::LIBRA_ROOT_ADDRESS());
ensures new_config.epoch == 0;
ensures new_config.last_reconfiguration_time == 0;
}
spec schema InitializeAbortsIf {
lr_account: signer;
include LibraTimestamp::AbortsIfNotGenesis;
include CoreAddresses::AbortsIfNotLibraRoot{account: lr_account};
aborts_if spec_has_config() with Errors::ALREADY_PUBLISHED;
}
spec schema InitializeEnsures {
ensures spec_has_config();
let new_config = global<Configuration>(CoreAddresses::LIBRA_ROOT_ADDRESS());
ensures new_config.epoch == 0;
ensures new_config.last_reconfiguration_time == 0;
}

// Get a copy of `Config` value stored under `addr`.

/// Returns a copy of `Config` value stored under `addr`.
public fun get<Config: copyable>(): Config
acquires LibraConfig {
let addr = CoreAddresses::LIBRA_ROOT_ADDRESS();
Expand All @@ -84,11 +100,12 @@ module LibraConfig {
aborts_if !exists<LibraConfig<Config>>(CoreAddresses::LIBRA_ROOT_ADDRESS()) with Errors::NOT_PUBLISHED;
}

// Set a config item to a new value with the default capability stored under config address and trigger a
// reconfiguration.
/// 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 be Libra root.
public fun set<Config: copyable>(account: &signer, payload: Config)
acquires LibraConfig, 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::LIBRA_ROOT_ADDRESS();
Expand Down Expand Up @@ -120,7 +137,12 @@ module LibraConfig {
ensures get<Config>() == payload;
}

// Set a config item to a new value and trigger a reconfiguration.
/// 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 `LibraSystem::update_config_and_reconfigure`, which allows
/// validator operators to change the validator set. All other config changes require
/// a Libra root signer.
public fun set_with_capability_and_reconfigure<Config: copyable>(
_cap: &ModifyConfigCapability<Config>,
payload: Config
Expand All @@ -140,10 +162,10 @@ module LibraConfig {
include SetEnsures<Config>;
}

// Publish a new config item.
// The caller will use the returned ModifyConfigCapability to specify the access control
// policy for who can modify the config.
// Does not trigger a reconfiguration.
/// 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>(
lr_account: &signer,
payload: Config,
Expand All @@ -169,9 +191,9 @@ module LibraConfig {
aborts_if exists<LibraConfig<Config>>(CoreAddresses::LIBRA_ROOT_ADDRESS()) with Errors::ALREADY_PUBLISHED;
}

// Publish a new config item. Only the config address can modify such config.
// Does not trigger a reconfiguration. Will also publish the capability to
// modify this config under the given account.
/// Publish a new config item. Only Libra root can modify such config.
/// Publishes the capability to modify this config under the Libra root account.
/// Does not trigger a reconfiguration.
public fun publish_new_config<Config: copyable>(
lr_account: &signer,
payload: Config
Expand Down Expand Up @@ -204,7 +226,7 @@ module LibraConfig {
ensures exists<ModifyConfigCapability<Config>>(Signer::spec_address_of(lr_account));
}

// Publish a new config item. Only the delegated address can modify such config after redeeming the capability.
/// Signal validators to start using new configuration. Must be called by Libra root.
public fun reconfigure(
lr_account: &signer,
) acquires Configuration {
Expand All @@ -218,6 +240,8 @@ module LibraConfig {
include ReconfigureAbortsIf;
}

/// Private function to do reconfiguration. Updates reconfiguration status resource
/// `Configuration` and emits a `NewEpochEvent`
fun reconfigure_() acquires Configuration {
// Do not do anything if genesis has not finished.
if (LibraTimestamp::is_genesis() || LibraTimestamp::now_microseconds() == 0) {
Expand Down Expand Up @@ -266,6 +290,7 @@ module LibraConfig {
aborts_if [concrete] current_time <= config.last_reconfiguration_time with Errors::INVALID_STATE;
aborts_if [concrete] config.epoch == MAX_U64 with EXECUTION_FAILURE;
}
/// This schema is to be used by callers of `reconfigure`
spec schema ReconfigureAbortsIf {
let config = global<Configuration>(CoreAddresses::LIBRA_ROOT_ADDRESS());
let current_time = LibraTimestamp::spec_now_microseconds();
Expand All @@ -276,8 +301,8 @@ module LibraConfig {
with Errors::INVALID_STATE;
}

// Emit a reconfiguration event. This function will be invoked by genesis directly to generate the very first
// 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() acquires Configuration {
assert(exists<Configuration>(CoreAddresses::LIBRA_ROOT_ADDRESS()), Errors::not_published(ECONFIGURATION));
let config_ref = borrow_global_mut<Configuration>(CoreAddresses::LIBRA_ROOT_ADDRESS());
Expand All @@ -292,24 +317,19 @@ module LibraConfig {
);
}

// **************** Specifications ****************

spec module {
define spec_has_config(): bool {
exists<Configuration>(CoreAddresses::LIBRA_ROOT_ADDRESS())
}

define spec_is_published<Config>(): bool {
exists<LibraConfig<Config>>(CoreAddresses::LIBRA_ROOT_ADDRESS())
}
// =================================================================
// Module Specification

define spec_get_config<Config>(): Config {
global<LibraConfig<Config>>(CoreAddresses::LIBRA_ROOT_ADDRESS()).payload
}
spec module {} // Switch to module documentation context

/// # Initialization
spec module {
/// After genesis, the `Configuration` is published.
invariant [global] LibraTimestamp::is_operating() ==> spec_has_config();
}

/// # Invariants
spec module {
/// Configurations are only stored at the libra root address.
invariant [global]
forall config_address: address, config_type: type where exists<LibraConfig<config_type>>(config_address):
Expand All @@ -320,9 +340,25 @@ module LibraConfig {
LibraTimestamp::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>());
}

/// # Helper Functions
spec module {
define spec_has_config(): bool {
exists<Configuration>(CoreAddresses::LIBRA_ROOT_ADDRESS())
}

define spec_is_published<Config>(): bool {
exists<LibraConfig<Config>>(CoreAddresses::LIBRA_ROOT_ADDRESS())
}

define spec_get_config<Config>(): Config {
global<LibraConfig<Config>>(CoreAddresses::LIBRA_ROOT_ADDRESS()).payload
}
}

}
}
2 changes: 1 addition & 1 deletion language/stdlib/modules/LibraSystem.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ module LibraSystem {


/// Publishes the LibraConfig for the LibraSystem struct, which contains the current
/// validator set. Also publishes the CapabilityHolder with the
/// validator set. Also publishes the `CapabilityHolder` with the
/// ModifyConfigCapability<LibraSystem> returned by the publish function, which allows
/// code in this module to change LibraSystem config (including the validator set).
/// Must be invoked by the Libra root a single time in Genesis.
Expand Down
Loading

0 comments on commit 57fae95

Please sign in to comment.