Skip to content

Commit

Permalink
[move framework][move-prover] DRAFT: Move role creation from Genesis …
Browse files Browse the repository at this point in the history 
…to LibraAccount

Changes to a bunch of .move files related to LibraAccount and LibraSystem.

Added specification that every account has a role in LibraAccount.
Refactored Genesis and LibraAccount some to make this easier to prove,
and to clean up initialization.  Specifically, roles for libra root
and treasury compliance were added in Genesis separately from the
account creation functions.  So, I moved role creation into the account creation functions. Genesis was also creating the libra root and treasury compliance accounts directly, so I moved those into LibraAccount::initialize, which simplifies the Genesis code and eliminates some dependencies.

In various places, I renamed accounts to reflect their roles, if
known.  I also added some assertion checks in SlidingNonce, which was
getting errors from unchecked aborts.
  • Loading branch information
@DavidLDill
DavidLDill committed Sep 11, 2020
1 parent 916630a commit cff02ba
Show file tree
Hide file tree
Showing 25 changed files with 371 additions and 303 deletions.
Binary file modified language/stdlib/compiled/error_descriptions/error_descriptions.errmap
View file
Binary file not shown.
Binary file modified language/stdlib/compiled/stdlib/005_Roles.mv
View file
Binary file not shown.
Binary file modified language/stdlib/compiled/stdlib/030_SlidingNonce.mv
View file
Binary file not shown.
Binary file modified language/stdlib/compiled/stdlib/032_LibraAccount.mv
View file
Binary file not shown.
Binary file modified language/stdlib/compiled/stdlib/038_Genesis.mv
View file
Binary file not shown.
22 changes: 3 additions & 19 deletions language/stdlib/modules/Genesis.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,29 +20,25 @@ module Genesis {
use 0x1::LibraTransactionPublishingOption;
use 0x1::LibraVersion;
use 0x1::LibraWriteSetManager;
use 0x1::Signer;
use 0x1::TransactionFee;
use 0x1::Roles;
use 0x1::LibraVMConfig;

fun initialize(
lr_account: &signer,
tc_account: &signer,
lr_auth_key: vector<u8>,
tc_addr: address,
_tc_addr: address,
tc_auth_key: vector<u8>,
initial_script_allow_list: vector<vector<u8>>,
is_open_module: bool,
instruction_schedule: vector<u8>,
native_schedule: vector<u8>,
chain_id: u8,
) {
let dummy_auth_key_prefix = x"00000000000000000000000000000000";

ChainId::initialize(lr_account, chain_id);
LibraAccount::initialize(lr_account);

Roles::grant_libra_root_role(lr_account);
Roles::grant_treasury_compliance_role(tc_account, lr_account);
ChainId::initialize(lr_account, chain_id);

// Event and On-chain config setup
Event::publish_generator(lr_account);
Expand All @@ -61,25 +57,13 @@ module Genesis {
);

AccountFreezing::initialize(lr_account);
LibraAccount::initialize(lr_account);
LibraAccount::create_libra_root_account(
Signer::address_of(lr_account),
copy dummy_auth_key_prefix,
);

// Register transaction fee resource
TransactionFee::initialize(
lr_account,
tc_account,
);

// Create the treasury compliance account
LibraAccount::create_treasury_compliance_account(
lr_account,
tc_addr,
copy dummy_auth_key_prefix,
);

LibraSystem::initialize_validator_set(
lr_account,
);
Expand Down
47 changes: 36 additions & 11 deletions language/stdlib/modules/LibraAccount.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -177,6 +177,16 @@ module LibraAccount {
LibraTimestamp::assert_genesis();
// Operational constraint, not a privilege constraint.
CoreAddresses::assert_libra_root(lr_account);
let dummy_auth_key_prefix = x"00000000000000000000000000000000";
create_libra_root_account(
copy dummy_auth_key_prefix,
);
// Create the treasury compliance account
create_treasury_compliance_account(
lr_account,
copy dummy_auth_key_prefix,
);

assert(
!exists<AccountOperationsCapability>(CoreAddresses::LIBRA_ROOT_ADDRESS()),
Errors::already_published(EACCOUNT_OPERATIONS_CAPABILITY)
Expand Down Expand Up @@ -802,14 +812,20 @@ module LibraAccount {
destroy_signer(new_account);
}

spec fun make_account {
/// Needed to prove invariant
let new_account_addr = Signer::address_of(new_account);
requires exists<Roles::RoleId>(new_account_addr);
}

/// Creates the libra root account in genesis.
public fun create_libra_root_account(
new_account_address: address,
auth_key_prefix: vector<u8>,
) {
LibraTimestamp::assert_genesis();
let new_account = create_signer(new_account_address);
let new_account = create_signer(CoreAddresses::LIBRA_ROOT_ADDRESS());
CoreAddresses::assert_libra_root(&new_account);
Roles::grant_libra_root_role(&new_account);
SlidingNonce::publish_nonce_resource(&new_account, &new_account);
make_account(new_account, auth_key_prefix)
}
Expand All @@ -818,12 +834,13 @@ module LibraAccount {
/// `auth_key_prefix` | `new_account_address`
public fun create_treasury_compliance_account(
lr_account: &signer,
new_account_address: address,
auth_key_prefix: vector<u8>,
) {
LibraTimestamp::assert_genesis();
Roles::assert_libra_root(lr_account);
let new_account_address = CoreAddresses::TREASURY_COMPLIANCE_ADDRESS();
let new_account = create_signer(new_account_address);
Roles::grant_treasury_compliance_role(&new_account, lr_account);
SlidingNonce::publish_nonce_resource(lr_account, &new_account);
Event::publish_generator(&new_account);
make_account(new_account, auth_key_prefix)
Expand Down Expand Up @@ -1187,30 +1204,30 @@ module LibraAccount {
///////////////////////////////////////////////////////////////////////////

public fun create_validator_account(
creator_account: &signer,
lr_account: &signer,
new_account_address: address,
auth_key_prefix: vector<u8>,
human_name: vector<u8>,
) {
let new_account = create_signer(new_account_address);
// The creator account is verified to have the libra root role in `Roles::new_validator_role`
Roles::new_validator_role(creator_account, &new_account);
// The lr_account account is verified to have the libra root role in `Roles::new_validator_role`
Roles::new_validator_role(lr_account, &new_account);
Event::publish_generator(&new_account);
ValidatorConfig::publish(&new_account, creator_account, human_name);
ValidatorConfig::publish(&new_account, lr_account, human_name);
make_account(new_account, auth_key_prefix)
}

public fun create_validator_operator_account(
creator_account: &signer,
lr_account: &signer,
new_account_address: address,
auth_key_prefix: vector<u8>,
human_name: vector<u8>,
) {
let new_account = create_signer(new_account_address);
// The creator account is verified to have the libra root role in `Roles::new_validator_operator_role`
Roles::new_validator_operator_role(creator_account, &new_account);
// The lr_account is verified to have the libra root role in `Roles::new_validator_operator_role`
Roles::new_validator_operator_role(lr_account, &new_account);
Event::publish_generator(&new_account);
ValidatorOperatorConfig::publish(&new_account, creator_account, human_name);
ValidatorOperatorConfig::publish(&new_account, lr_account, human_name);
make_account(new_account, auth_key_prefix)
}

Expand Down Expand Up @@ -1295,6 +1312,14 @@ module LibraAccount {
delegated_key_rotation_capability(addr1) || spec_holds_own_key_rotation_cap(addr1);
}

// TODO (dd): For each account type, specify that it is set up properly, including other
// published resources.

spec module {
/// Every address that has a published RoleId also has a published Account.
invariant [global] forall addr1: address where exists_at(addr1): exists<Roles::RoleId>(addr1);
}

/// only rotate_authentication_key can rotate authentication_key [B26].
spec schema AuthenticationKeyRemainsSame {
ensures forall addr1: address where old(exists_at(addr1)):
Expand Down
86 changes: 44 additions & 42 deletions language/stdlib/modules/LibraSystem.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,26 +22,19 @@ module LibraSystem {
}

struct LibraSystem {
// The current consensus crypto scheme.
/// The current consensus crypto scheme.
scheme: u8,
// The current validator set. Updated only at epoch boundaries via reconfiguration.
/// The current validator set. Updated only at epoch boundaries via reconfiguration.
validators: vector<ValidatorInfo>,
}
spec struct LibraSystem {
/// Validators have unique addresses.
/// Members of `validators` vector (the validator set) have unique addresses.
invariant
forall i in 0..len(validators), j in 0..len(validators):
validators[i].addr == validators[j].addr ==> i == j;
}

spec module {
/// After genesis, the `LibraSystem` configuration is published, as well as the capability
/// to modify it.
invariant [global] LibraTimestamp::is_operating() ==>
LibraConfig::spec_is_published<LibraSystem>() &&
exists<CapabilityHolder>(CoreAddresses::LIBRA_ROOT_ADDRESS());
}

/// # Error codes
/// The `CapabilityHolder` resource was not in the required state
const ECAPABILITY_HOLDER: u64 = 0;
/// Tried to add a validator with an invalid state to the validator set
Expand All @@ -63,13 +56,13 @@ module LibraSystem {
// the resource under that address.
// It can only be called a single time. Currently, it is invoked in the genesis transaction.
public fun initialize_validator_set(
config_account: &signer,
lr_account: &signer,
) {
LibraTimestamp::assert_genesis();
Roles::assert_libra_root(config_account);
Roles::assert_libra_root(lr_account);

let cap = LibraConfig::publish_new_config_and_get_capability<LibraSystem>(
config_account,
lr_account,
LibraSystem {
scheme: 0,
validators: Vector::empty(),
Expand All @@ -79,16 +72,16 @@ module LibraSystem {
!exists<CapabilityHolder>(CoreAddresses::LIBRA_ROOT_ADDRESS()),
Errors::already_published(ECAPABILITY_HOLDER)
);
move_to(config_account, CapabilityHolder { cap })
move_to(lr_account, CapabilityHolder { cap })
}
spec fun initialize_validator_set {
modifies global<LibraConfig::LibraConfig<LibraSystem>>(CoreAddresses::LIBRA_ROOT_ADDRESS());
include LibraTimestamp::AbortsIfNotGenesis;
include Roles::AbortsIfNotLibraRoot{account: config_account};
let config_addr = Signer::spec_address_of(config_account);
include Roles::AbortsIfNotLibraRoot{account: lr_account};
let lr_addr = Signer::spec_address_of(lr_account);
aborts_if LibraConfig::spec_is_published<LibraSystem>() with Errors::ALREADY_PUBLISHED;
aborts_if exists<CapabilityHolder>(config_addr) with Errors::ALREADY_PUBLISHED;
ensures exists<CapabilityHolder>(config_addr);
aborts_if exists<CapabilityHolder>(lr_addr) with Errors::ALREADY_PUBLISHED;
ensures exists<CapabilityHolder>(lr_addr);
ensures LibraConfig::spec_is_published<LibraSystem>();
ensures len(spec_get_validators()) == 0;
}
Expand All @@ -110,15 +103,10 @@ module LibraSystem {
pragma opaque;
modifies global<LibraConfig::LibraConfig<LibraSystem>>(CoreAddresses::LIBRA_ROOT_ADDRESS());
include LibraTimestamp::AbortsIfNotOperating;
include AbortsIfNoCapabilityHolder;
include LibraConfig::ReconfigureAbortsIf;
ensures global<LibraConfig::LibraConfig<LibraSystem>>(CoreAddresses::LIBRA_ROOT_ADDRESS()).payload == value;
}

spec schema AbortsIfNoCapabilityHolder {
aborts_if !exists<CapabilityHolder>(CoreAddresses::LIBRA_ROOT_ADDRESS()) with Errors::NOT_PUBLISHED;
}

///////////////////////////////////////////////////////////////////////////
// Methods operating the Validator Set config callable by the libra root account
///////////////////////////////////////////////////////////////////////////
Expand All @@ -127,23 +115,23 @@ module LibraSystem {
// If successful, a NewEpochEvent is fired
public fun add_validator(
lr_account: &signer,
account_address: address
validator_address: address
) acquires CapabilityHolder {
LibraTimestamp::assert_operating();
Roles::assert_libra_root(lr_account);
// A prospective validator must have a validator config resource
assert(ValidatorConfig::is_valid(account_address), Errors::invalid_argument(EINVALID_PROSPECTIVE_VALIDATOR));
assert(ValidatorConfig::is_valid(validator_address), Errors::invalid_argument(EINVALID_PROSPECTIVE_VALIDATOR));

let libra_system_config = get_libra_system_config();
// Ensure that this address is not already a validator
assert(
!is_validator_(account_address, &libra_system_config.validators),
!is_validator_(validator_address, &libra_system_config.validators),
Errors::invalid_argument(EALREADY_A_VALIDATOR)
);
// it is guaranteed that the config is non-empty
let config = ValidatorConfig::get_config(account_address);
let config = ValidatorConfig::get_config(validator_address);
Vector::push_back(&mut libra_system_config.validators, ValidatorInfo {
addr: account_address,
addr: validator_address,
config, // copy the config over to ValidatorSet
consensus_voting_power: 1,
});
Expand All @@ -154,17 +142,17 @@ module LibraSystem {
modifies global<LibraConfig::LibraConfig<LibraSystem>>(CoreAddresses::LIBRA_ROOT_ADDRESS());
include LibraTimestamp::AbortsIfNotOperating;
include LibraConfig::ReconfigureAbortsIf;
aborts_if !ValidatorConfig::spec_is_valid(account_address) with Errors::INVALID_ARGUMENT;
aborts_if spec_is_validator(account_address) with Errors::INVALID_ARGUMENT;
ensures spec_is_validator(account_address);
aborts_if !ValidatorConfig::spec_is_valid(validator_address) with Errors::INVALID_ARGUMENT;
aborts_if spec_is_validator(validator_address) with Errors::INVALID_ARGUMENT;
ensures spec_is_validator(validator_address);
}
spec fun add_validator {
let vs = spec_get_validators();
ensures Vector::eq_push_back(vs,
old(vs),
ValidatorInfo {
addr: account_address,
config: ValidatorConfig::spec_get_config(account_address),
addr: validator_address,
config: ValidatorConfig::spec_get_config(validator_address),
consensus_voting_power: 1,
}
);
Expand Down Expand Up @@ -207,13 +195,13 @@ module LibraSystem {
// This function makes no changes to the size or the members of the set.
// If the config in the ValidatorSet changes, a NewEpochEvent is fired.
public fun update_config_and_reconfigure(
operator_account: &signer,
validator_operator_account: &signer,
validator_address: address,
) acquires CapabilityHolder {
LibraTimestamp::assert_operating();
Roles::assert_validator_operator(operator_account);
Roles::assert_validator_operator(validator_operator_account);
assert(
ValidatorConfig::get_operator(validator_address) == Signer::address_of(operator_account),
ValidatorConfig::get_operator(validator_address) == Signer::address_of(validator_operator_account),
Errors::invalid_argument(EINVALID_TRANSACTION_SENDER)
);
let libra_system_config = get_libra_system_config();
Expand All @@ -228,15 +216,18 @@ module LibraSystem {
spec fun update_config_and_reconfigure {
include LibraTimestamp::AbortsIfNotOperating;
/// Must abort if the signer does not have the ValidatorOperator role [B23].
include Roles::AbortsIfNotValidatorOperator{account: operator_account};
include Roles::AbortsIfNotValidatorOperator{validator_operator_account: validator_operator_account};
include ValidatorConfig::AbortsIfNoValidatorConfig{addr: validator_address};
aborts_if ValidatorConfig::spec_get_operator(validator_address) != Signer::spec_address_of(operator_account)
aborts_if ValidatorConfig::spec_get_operator(validator_address)
!= Signer::spec_address_of(validator_operator_account)
with Errors::INVALID_ARGUMENT;
aborts_if !spec_is_validator(validator_address) with Errors::INVALID_ARGUMENT;
let is_validator_info_updated =
ValidatorConfig::spec_is_valid(validator_address) &&
(exists v in spec_get_validators(): v.addr == validator_address && v.config != ValidatorConfig::spec_get_config(validator_address));
include is_validator_info_updated ==> AbortsIfNoCapabilityHolder && LibraConfig::ReconfigureAbortsIf;
(exists v in spec_get_validators():
v.addr == validator_address
&& v.config != ValidatorConfig::spec_get_config(validator_address));
include is_validator_info_updated ==> LibraConfig::ReconfigureAbortsIf;
}

/// *Informally:* Does not change the length of the validator set, only
Expand Down Expand Up @@ -440,6 +431,16 @@ module LibraSystem {
}
}

/// After genesis, the `LibraSystem` configuration is published, as well as the capability
/// to modify it. This invariant removes the need to specify aborts_if's for missing
/// CapabilityHolder at Libra root.
spec module {
invariant [global] LibraTimestamp::is_operating() ==>
LibraConfig::spec_is_published<LibraSystem>() &&
exists<CapabilityHolder>(CoreAddresses::LIBRA_ROOT_ADDRESS());
}


/// The permission "{Add, Remove} Validator" is granted to LibraRoot [B22].
spec module {
apply Roles::AbortsIfNotLibraRoot{account: lr_account} to add_validator, remove_validator;
Expand All @@ -461,7 +462,8 @@ module LibraSystem {
ensures spec_get_validators() == old(spec_get_validators());
}
spec module {
/// Only {add, remove} validator [B22] and update_config_and_reconfigure [B23] may change the set of validators in the configuration.
/// Only {add, remove} validator [B22] and update_config_and_reconfigure
/// [B23] may change the set of validators in the configuration.
apply ValidatorSetConfigRemainsSame to *, *<T>
except add_validator, remove_validator, update_config_and_reconfigure,
initialize_validator_set, set_libra_system_config;
Expand Down

0 comments on commit cff02ba

Please sign in to comment.