diff --git a/language/stdlib/compiled/error_descriptions/error_descriptions.errmap b/language/stdlib/compiled/error_descriptions/error_descriptions.errmap index dc88054f888..264ff6caadd 100644 Binary files a/language/stdlib/compiled/error_descriptions/error_descriptions.errmap and b/language/stdlib/compiled/error_descriptions/error_descriptions.errmap differ diff --git a/language/stdlib/compiled/stdlib/005_Roles.mv b/language/stdlib/compiled/stdlib/005_Roles.mv index b254641f2b1..ab232f5ed83 100644 Binary files a/language/stdlib/compiled/stdlib/005_Roles.mv and b/language/stdlib/compiled/stdlib/005_Roles.mv differ diff --git a/language/stdlib/compiled/stdlib/030_SlidingNonce.mv b/language/stdlib/compiled/stdlib/030_SlidingNonce.mv index aa2f1d7a3a1..76454fc8dbe 100644 Binary files a/language/stdlib/compiled/stdlib/030_SlidingNonce.mv and b/language/stdlib/compiled/stdlib/030_SlidingNonce.mv differ diff --git a/language/stdlib/compiled/stdlib/032_LibraAccount.mv b/language/stdlib/compiled/stdlib/032_LibraAccount.mv index 8731dc76927..f1cb1907cfa 100644 Binary files a/language/stdlib/compiled/stdlib/032_LibraAccount.mv and b/language/stdlib/compiled/stdlib/032_LibraAccount.mv differ diff --git a/language/stdlib/compiled/stdlib/038_Genesis.mv b/language/stdlib/compiled/stdlib/038_Genesis.mv index 4d488099f4d..ba63b9bdcc7 100644 Binary files a/language/stdlib/compiled/stdlib/038_Genesis.mv and b/language/stdlib/compiled/stdlib/038_Genesis.mv differ diff --git a/language/stdlib/modules/Genesis.move b/language/stdlib/modules/Genesis.move index dedbd34786c..2f9fdcdb071 100644 --- a/language/stdlib/modules/Genesis.move +++ b/language/stdlib/modules/Genesis.move @@ -20,16 +20,14 @@ 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, - tc_addr: address, + _tc_addr: address, tc_auth_key: vector, initial_script_allow_list: vector>, is_open_module: bool, @@ -37,12 +35,10 @@ module Genesis { native_schedule: vector, 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); @@ -61,11 +57,6 @@ 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( @@ -73,13 +64,6 @@ module Genesis { 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, ); diff --git a/language/stdlib/modules/LibraAccount.move b/language/stdlib/modules/LibraAccount.move index e61601c38e1..478ae4bfc58 100644 --- a/language/stdlib/modules/LibraAccount.move +++ b/language/stdlib/modules/LibraAccount.move @@ -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(CoreAddresses::LIBRA_ROOT_ADDRESS()), Errors::already_published(EACCOUNT_OPERATIONS_CAPABILITY) @@ -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(new_account_addr); + } + /// Creates the libra root account in genesis. public fun create_libra_root_account( - new_account_address: address, auth_key_prefix: vector, ) { 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) } @@ -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, ) { 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) @@ -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, human_name: vector, ) { 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, human_name: vector, ) { 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) } @@ -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(addr1); + } + /// only rotate_authentication_key can rotate authentication_key [B26]. spec schema AuthenticationKeyRemainsSame { ensures forall addr1: address where old(exists_at(addr1)): diff --git a/language/stdlib/modules/LibraSystem.move b/language/stdlib/modules/LibraSystem.move index 0dc9b41c320..c69ee5202f3 100644 --- a/language/stdlib/modules/LibraSystem.move +++ b/language/stdlib/modules/LibraSystem.move @@ -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, } 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() && - exists(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 @@ -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( - config_account, + lr_account, LibraSystem { scheme: 0, validators: Vector::empty(), @@ -79,16 +72,16 @@ module LibraSystem { !exists(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>(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() with Errors::ALREADY_PUBLISHED; - aborts_if exists(config_addr) with Errors::ALREADY_PUBLISHED; - ensures exists(config_addr); + aborts_if exists(lr_addr) with Errors::ALREADY_PUBLISHED; + ensures exists(lr_addr); ensures LibraConfig::spec_is_published(); ensures len(spec_get_validators()) == 0; } @@ -110,15 +103,10 @@ module LibraSystem { pragma opaque; modifies global>(CoreAddresses::LIBRA_ROOT_ADDRESS()); include LibraTimestamp::AbortsIfNotOperating; - include AbortsIfNoCapabilityHolder; include LibraConfig::ReconfigureAbortsIf; ensures global>(CoreAddresses::LIBRA_ROOT_ADDRESS()).payload == value; } - spec schema AbortsIfNoCapabilityHolder { - aborts_if !exists(CoreAddresses::LIBRA_ROOT_ADDRESS()) with Errors::NOT_PUBLISHED; - } - /////////////////////////////////////////////////////////////////////////// // Methods operating the Validator Set config callable by the libra root account /////////////////////////////////////////////////////////////////////////// @@ -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, }); @@ -154,17 +142,17 @@ module LibraSystem { modifies global>(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, } ); @@ -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(); @@ -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 @@ -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() && + exists(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; @@ -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 *, * except add_validator, remove_validator, update_config_and_reconfigure, initialize_validator_set, set_libra_system_config; diff --git a/language/stdlib/modules/Roles.move b/language/stdlib/modules/Roles.move index bfab2f1d995..84b86a28267 100644 --- a/language/stdlib/modules/Roles.move +++ b/language/stdlib/modules/Roles.move @@ -179,14 +179,15 @@ module Roles { spec fun grant_role { pragma opaque; include GrantRole; + let addr = Signer::spec_address_of(account); + // Requires to satisfy global invariants. + requires role_id == LIBRA_ROOT_ROLE_ID ==> addr == CoreAddresses::LIBRA_ROOT_ADDRESS(); + requires role_id == TREASURY_COMPLIANCE_ROLE_ID ==> addr == CoreAddresses::TREASURY_COMPLIANCE_ADDRESS(); } spec schema GrantRole { account: signer; role_id: num; let addr = Signer::spec_address_of(account); - // Requires to satisfy global invariants. - requires role_id == LIBRA_ROOT_ROLE_ID ==> addr == CoreAddresses::LIBRA_ROOT_ADDRESS(); - requires role_id == TREASURY_COMPLIANCE_ROLE_ID ==> addr == CoreAddresses::TREASURY_COMPLIANCE_ADDRESS(); aborts_if exists(addr) with Errors::ALREADY_PUBLISHED; ensures exists(addr); ensures global(addr).role_id == role_id; @@ -312,11 +313,11 @@ module Roles { } /// Assert that the account has the validator role. - public fun assert_validator(account: &signer) acquires RoleId { - let addr = Signer::address_of(account); - assert(exists(addr), Errors::not_published(EROLE_ID)); + public fun assert_validator(validator_account: &signer) acquires RoleId { + let validator_addr = Signer::address_of(validator_account); + assert(exists(validator_addr), Errors::not_published(EROLE_ID)); assert( - borrow_global(addr).role_id == VALIDATOR_ROLE_ID, + borrow_global(validator_addr).role_id == VALIDATOR_ROLE_ID, Errors::requires_role(EVALIDATOR) ) } @@ -326,11 +327,11 @@ module Roles { } /// Assert that the account has the validator operator role. - public fun assert_validator_operator(account: &signer) acquires RoleId { - let addr = Signer::address_of(account); - assert(exists(addr), Errors::not_published(EROLE_ID)); + public fun assert_validator_operator(validator_operator_account: &signer) acquires RoleId { + let validator_operator_addr = Signer::address_of(validator_operator_account); + assert(exists(validator_operator_addr), Errors::not_published(EROLE_ID)); assert( - borrow_global(addr).role_id == VALIDATOR_OPERATOR_ROLE_ID, + borrow_global(validator_operator_addr).role_id == VALIDATOR_OPERATOR_ROLE_ID, Errors::requires_role(EVALIDATOR_OPERATOR) ) } @@ -479,17 +480,18 @@ module Roles { } spec schema AbortsIfNotValidator { - account: signer; - let addr = Signer::spec_address_of(account); - aborts_if !exists(addr) with Errors::NOT_PUBLISHED; - aborts_if global(addr).role_id != VALIDATOR_ROLE_ID with Errors::REQUIRES_ROLE; + validator_account: signer; + let validator_addr = Signer::spec_address_of(validator_account); + aborts_if !exists(validator_addr) with Errors::NOT_PUBLISHED; + aborts_if global(validator_addr).role_id != VALIDATOR_ROLE_ID with Errors::REQUIRES_ROLE; } spec schema AbortsIfNotValidatorOperator { - account: signer; - let addr = Signer::spec_address_of(account); - aborts_if !exists(addr) with Errors::NOT_PUBLISHED; - aborts_if global(addr).role_id != VALIDATOR_OPERATOR_ROLE_ID with Errors::REQUIRES_ROLE; + validator_operator_account: signer; + let validator_operator_addr = Signer::spec_address_of(validator_operator_account); + aborts_if !exists(validator_operator_addr) with Errors::NOT_PUBLISHED; + aborts_if global(validator_operator_addr).role_id != VALIDATOR_OPERATOR_ROLE_ID + with Errors::REQUIRES_ROLE; } diff --git a/language/stdlib/modules/SlidingNonce.move b/language/stdlib/modules/SlidingNonce.move index 17e69b07602..a6e82b241f1 100644 --- a/language/stdlib/modules/SlidingNonce.move +++ b/language/stdlib/modules/SlidingNonce.move @@ -21,6 +21,8 @@ module SlidingNonce { const ENONCE_TOO_NEW: u64 = 2; /// The nonce was already recorded previously const ENONCE_ALREADY_RECORDED: u64 = 3; + /// Nonce + const ENONCE_ALREADY_PUBLISHED: u64 = 4; /// Size of SlidingNonce::nonce_mask in bits. const NONCE_MASK_SIZE: u64 = 128; @@ -68,6 +70,7 @@ module SlidingNonce { /// Publishes nonce resource for `account` /// This is required before other functions in this module can be called for `account public fun publish(account: &signer) { + assert(!exists(Signer::address_of(account)), Errors::invalid_argument(ENONCE_ALREADY_PUBLISHED)); move_to(account, SlidingNonce { min_nonce: 0, nonce_mask: 0 }); } @@ -82,7 +85,9 @@ module SlidingNonce { min_nonce: 0, nonce_mask: 0, }; - move_to(account, new_resource) + assert(!exists(Signer::address_of(account)), + Errors::invalid_argument(ENONCE_ALREADY_PUBLISHED)); + move_to(account, new_resource); } } } diff --git a/language/stdlib/modules/ValidatorConfig.move b/language/stdlib/modules/ValidatorConfig.move index 61b47962fa3..af9ea0cecac 100644 --- a/language/stdlib/modules/ValidatorConfig.move +++ b/language/stdlib/modules/ValidatorConfig.move @@ -42,18 +42,18 @@ module ValidatorConfig { /// will have critical info such as keys, network addresses for validators, /// and the address of the validator operator. public fun publish( - account: &signer, + validator_account: &signer, lr_account: &signer, human_name: vector, ) { LibraTimestamp::assert_operating(); Roles::assert_libra_root(lr_account); - Roles::assert_validator(account); + Roles::assert_validator(validator_account); assert( - !exists(Signer::address_of(account)), + !exists(Signer::address_of(validator_account)), Errors::already_published(EVALIDATOR_CONFIG) ); - move_to(account, ValidatorConfig { + move_to(validator_account, ValidatorConfig { config: Option::none(), operator_account: Option::none(), human_name, @@ -64,8 +64,9 @@ module ValidatorConfig { include LibraTimestamp::AbortsIfNotOperating; include Roles::AbortsIfNotLibraRoot{account: lr_account}; include Roles::AbortsIfNotValidator; - aborts_if exists_config(Signer::spec_address_of(account)) with Errors::ALREADY_PUBLISHED; - ensures exists_config(Signer::spec_address_of(account)); + aborts_if exists_config(Signer::spec_address_of(validator_account)) + with Errors::ALREADY_PUBLISHED; + ensures exists_config(Signer::spec_address_of(validator_account)); } /// Returns true if a ValidatorConfig resource exists under addr. @@ -85,8 +86,8 @@ module ValidatorConfig { /// Sets a new operator account, preserving the old config. /// Note: Access control. No one but the owner of the account may change .operator_account - public fun set_operator(account: &signer, operator_account: address) acquires ValidatorConfig { - Roles::assert_validator(account); + public fun set_operator(validator_account: &signer, operator_account: address) acquires ValidatorConfig { + Roles::assert_validator(validator_account); // Check for validator role is not necessary since the role is checked when the config // resource is published. // TODO (dd): Probably need to prove an invariant about role. @@ -94,7 +95,7 @@ module ValidatorConfig { ValidatorOperatorConfig::has_validator_operator_config(operator_account), Errors::invalid_argument(ENOT_A_VALIDATOR_OPERATOR) ); - let sender = Signer::address_of(account); + let sender = Signer::address_of(validator_account); assert(exists_config(sender), Errors::not_published(EVALIDATOR_CONFIG)); (borrow_global_mut(sender)).operator_account = Option::some(operator_account); } @@ -104,7 +105,7 @@ module ValidatorConfig { aborts_if !ValidatorOperatorConfig::has_validator_operator_config(operator_account) with Errors::INVALID_ARGUMENT; - let sender = Signer::spec_address_of(account); + let sender = Signer::spec_address_of(validator_account); include AbortsIfNoValidatorConfig{addr: sender}; aborts_if !ValidatorOperatorConfig::has_validator_operator_config(operator_account) with Errors::NOT_PUBLISHED; ensures spec_has_operator(sender); @@ -139,9 +140,9 @@ module ValidatorConfig { /// Removes an operator account, setting a corresponding field to Option::none. /// The old config is preserved. - public fun remove_operator(account: &signer) acquires ValidatorConfig { - Roles::assert_validator(account); - let sender = Signer::address_of(account); + public fun remove_operator(validator_account: &signer) acquires ValidatorConfig { + Roles::assert_validator(validator_account); + let sender = Signer::address_of(validator_account); // Config field remains set assert(exists_config(sender), Errors::not_published(EVALIDATOR_CONFIG)); (borrow_global_mut(sender)).operator_account = Option::none(); @@ -151,9 +152,9 @@ module ValidatorConfig { /// Must abort if the signer does not have the Validator role [B24]. include Roles::AbortsIfNotValidator; - let sender = Signer::spec_address_of(account); + let sender = Signer::spec_address_of(validator_account); include AbortsIfNoValidatorConfig{addr: sender}; - ensures !spec_has_operator(Signer::spec_address_of(account)); + ensures !spec_has_operator(Signer::spec_address_of(validator_account)); ensures spec_get_operator(sender) == sender; /// The signer can only change its own operator account [B24]. diff --git a/language/stdlib/modules/ValidatorOperatorConfig.move b/language/stdlib/modules/ValidatorOperatorConfig.move index 3e7dc22c66d..e862cd7a073 100644 --- a/language/stdlib/modules/ValidatorOperatorConfig.move +++ b/language/stdlib/modules/ValidatorOperatorConfig.move @@ -14,45 +14,46 @@ module ValidatorOperatorConfig { const EVALIDATOR_OPERATOR_CONFIG: u64 = 0; public fun publish( - account: &signer, + validator_operator_account: &signer, lr_account: &signer, human_name: vector, ) { Roles::assert_libra_root(lr_account); - Roles::assert_validator_operator(account); + Roles::assert_validator_operator(validator_operator_account); assert( - !has_validator_operator_config(Signer::address_of(account)), + !has_validator_operator_config(Signer::address_of(validator_operator_account)), Errors::already_published(EVALIDATOR_OPERATOR_CONFIG) ); - move_to(account, ValidatorOperatorConfig { + move_to(validator_operator_account, ValidatorOperatorConfig { human_name, }); } spec fun publish { include Roles::AbortsIfNotLibraRoot{account: lr_account}; include Roles::AbortsIfNotValidatorOperator; - aborts_if has_validator_operator_config(Signer::spec_address_of(account)) with Errors::ALREADY_PUBLISHED; - ensures has_validator_operator_config(Signer::spec_address_of(account)); + aborts_if has_validator_operator_config(Signer::spec_address_of(validator_operator_account)) + with Errors::ALREADY_PUBLISHED; + ensures has_validator_operator_config(Signer::spec_address_of(validator_operator_account)); } /// Get validator's account human name /// Aborts if there is no ValidatorOperatorConfig resource - public fun get_human_name(addr: address): vector acquires ValidatorOperatorConfig { - assert(has_validator_operator_config(addr), Errors::not_published(EVALIDATOR_OPERATOR_CONFIG)); - *&borrow_global(addr).human_name + public fun get_human_name(validator_operator_addr: address): vector acquires ValidatorOperatorConfig { + assert(has_validator_operator_config(validator_operator_addr), Errors::not_published(EVALIDATOR_OPERATOR_CONFIG)); + *&borrow_global(validator_operator_addr).human_name } spec fun get_human_name { pragma opaque; - aborts_if !has_validator_operator_config(addr) with Errors::NOT_PUBLISHED; - ensures result == get_human_name(addr); + aborts_if !has_validator_operator_config(validator_operator_addr) with Errors::NOT_PUBLISHED; + ensures result == get_human_name(validator_operator_addr); } - public fun has_validator_operator_config(addr: address): bool { - exists(addr) + public fun has_validator_operator_config(validator_operator_addr: address): bool { + exists(validator_operator_addr) } spec fun has_validator_operator_config { - ensures result == has_validator_operator_config(addr); + ensures result == has_validator_operator_config(validator_operator_addr); } } } diff --git a/language/stdlib/modules/doc/Genesis.md b/language/stdlib/modules/doc/Genesis.md index 380f15239c0..4dfe77e49e5 100644 --- a/language/stdlib/modules/doc/Genesis.md +++ b/language/stdlib/modules/doc/Genesis.md @@ -15,7 +15,7 @@ -
fun initialize(lr_account: &signer, tc_account: &signer, lr_auth_key: vector<u8>, 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)
+
fun initialize(lr_account: &signer, tc_account: &signer, lr_auth_key: vector<u8>, _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)
 

 
 
@@ -28,7 +28,7 @@
     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,
@@ -36,12 +36,10 @@
     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);
@@ -60,11 +58,6 @@
     );
 
     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(
@@ -72,13 +65,6 @@
         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,
     );
diff --git a/language/stdlib/modules/doc/LibraAccount.md b/language/stdlib/modules/doc/LibraAccount.md
index d2bb3858fc1..861038de1c4 100644
--- a/language/stdlib/modules/doc/LibraAccount.md
+++ b/language/stdlib/modules/doc/LibraAccount.md
@@ -103,6 +103,7 @@
     -  [Function `rotate_authentication_key`](#0x1_LibraAccount_Specification_rotate_authentication_key)
     -  [Function `extract_key_rotation_capability`](#0x1_LibraAccount_Specification_extract_key_rotation_capability)
     -  [Function `restore_key_rotation_capability`](#0x1_LibraAccount_Specification_restore_key_rotation_capability)
+    -  [Function `make_account`](#0x1_LibraAccount_Specification_make_account)
     -  [Function `add_currency`](#0x1_LibraAccount_Specification_add_currency)
     -  [Function `epilogue`](#0x1_LibraAccount_Specification_epilogue)
 
@@ -811,6 +812,16 @@ Initialize this module. This is only callable from genesis.
     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)
@@ -1582,7 +1593,7 @@ Creating an account at address 0x0 will abort as it is a reserved address for th
 Creates the libra root account in genesis.
 
 
-
public fun create_libra_root_account(new_account_address: address, auth_key_prefix: vector<u8>)
+
public fun create_libra_root_account(auth_key_prefix: vector<u8>)
 

 
 
@@ -1592,12 +1603,12 @@ 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)
 }
@@ -1617,7 +1628,7 @@ Create a treasury/compliance account at
 new_account_address
 
 
-
public fun create_treasury_compliance_account(lr_account: &signer, new_account_address: address, auth_key_prefix: vector<u8>)
+
public fun create_treasury_compliance_account(lr_account: &signer, auth_key_prefix: vector<u8>)
 

 
 
@@ -1628,12 +1639,13 @@ Create a treasury/compliance account at
 
 
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)
@@ -2483,7 +2495,7 @@ a writeset transaction is committed.
 
 
 
-
public fun create_validator_account(creator_account: &signer, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>)
+
public fun create_validator_account(lr_account: &signer, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>)
 

 
 
@@ -2493,16 +2505,16 @@ a writeset transaction is committed.
 
 
 
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)
 }
 

@@ -2517,7 +2529,7 @@ a writeset transaction is committed.
 
 
 
-
public fun create_validator_operator_account(creator_account: &signer, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>)
+
public fun create_validator_operator_account(lr_account: &signer, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>)
 

 
 
@@ -2527,16 +2539,16 @@ a writeset transaction is committed.
 
 
 
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)
 }
 

@@ -3059,6 +3071,28 @@ Can only rotate the authentication_key of cap.account_address [B26].
 
 
 
+
+
+### Function `make_account`
+
+
+
fun make_account(new_account: signer, auth_key_prefix: vector<u8>)
+

+
+
+
+Needed to prove invariant
+
+
+
+
+
+
let new_account_addr = Signer::address_of(new_account);
+requires exists<Roles::RoleId>(new_account_addr);
+

+
+
+
 
 
 ### Function `add_currency`
@@ -3251,6 +3285,14 @@ The LibraAccount under addr holds either no key rotation capability
 

 
 
+
+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].
 
 
diff --git a/language/stdlib/modules/doc/LibraSystem.md b/language/stdlib/modules/doc/LibraSystem.md
index 8dafdfa959d..fb2a5715683 100644
--- a/language/stdlib/modules/doc/LibraSystem.md
+++ b/language/stdlib/modules/doc/LibraSystem.md
@@ -9,6 +9,7 @@
 -  [Resource `CapabilityHolder`](#0x1_LibraSystem_CapabilityHolder)
 -  [Struct `LibraSystem`](#0x1_LibraSystem_LibraSystem)
 -  [Const `ECAPABILITY_HOLDER`](#0x1_LibraSystem_ECAPABILITY_HOLDER)
+    -  [Error codes](#0x1_LibraSystem_@Error_codes)
 -  [Const `EINVALID_PROSPECTIVE_VALIDATOR`](#0x1_LibraSystem_EINVALID_PROSPECTIVE_VALIDATOR)
 -  [Const `EALREADY_A_VALIDATOR`](#0x1_LibraSystem_EALREADY_A_VALIDATOR)
 -  [Const `ENOT_AN_ACTIVE_VALIDATOR`](#0x1_LibraSystem_ENOT_AN_ACTIVE_VALIDATOR)
@@ -137,14 +138,14 @@
 scheme: u8
 
 

-
+ The current consensus crypto scheme.
 

 

 
 validators: vector<LibraSystem::ValidatorInfo>
 

 

-
+ The current validator set. Updated only at epoch boundaries via reconfiguration.
 

 
 
@@ -155,6 +156,11 @@
 
 ## Const `ECAPABILITY_HOLDER`
 
+
+
+
+### Error codes
+
 The
 CapabilityHolder resource was not in the required state
 
@@ -230,7 +236,7 @@ An out of bounds index for the validator set was encountered
 
 
 
-
public fun initialize_validator_set(config_account: &signer)
+
public fun initialize_validator_set(lr_account: &signer)
 

 
 
@@ -240,13 +246,13 @@ An out of bounds index for the validator set was encountered
 
 
 
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(),
@@ -256,7 +262,7 @@ An out of bounds index for the validator set was encountered
         !exists<CapabilityHolder>(CoreAddresses::LIBRA_ROOT_ADDRESS()),
         Errors::already_published(ECAPABILITY_HOLDER)
     );
-    move_to(config_account, CapabilityHolder { cap })
+    move_to(lr_account, CapabilityHolder { cap })
 }
 

 
@@ -302,7 +308,7 @@ An out of bounds index for the validator set was encountered
 
 
 
-
public fun add_validator(lr_account: &signer, account_address: address)
+
public fun add_validator(lr_account: &signer, validator_address: address)
 

 
 
@@ -313,23 +319,23 @@ An out of bounds index for the validator set was encountered
 
 
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,
     });
@@ -385,7 +391,7 @@ An out of bounds index for the validator set was encountered
 
 
 
-
public fun update_config_and_reconfigure(operator_account: &signer, validator_address: address)
+
public fun update_config_and_reconfigure(validator_operator_account: &signer, validator_address: address)
 

 
 
@@ -395,13 +401,13 @@ An out of bounds index for the validator set was encountered
 
 
 
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();
@@ -674,19 +680,20 @@ An out of bounds index for the validator set was encountered
 scheme: u8
 
 

-
+ The current consensus crypto scheme.
 

 

 
 validators: vector<LibraSystem::ValidatorInfo>
 

 

-
+ The current validator set. Updated only at epoch boundaries via reconfiguration.
 

 
 
 
-Validators have unique addresses.
+Members of
+validators vector (the validator set) have unique addresses.
 
 
 
invariant
@@ -696,24 +703,12 @@ Validators have unique addresses.
 
 
 
-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());
-

-
-
-
 
 
 ### Function `initialize_validator_set`
 
 
-
public fun initialize_validator_set(config_account: &signer)
+
public fun initialize_validator_set(lr_account: &signer)
 

 
 
@@ -721,12 +716,12 @@ to modify it.
 
 
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;
 

@@ -747,30 +742,18 @@ to modify it.
 
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;
 

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

-
-
-
 
 
 ### Function `add_validator`
 
 
-
public fun add_validator(lr_account: &signer, account_address: address)
+
public fun add_validator(lr_account: &signer, validator_address: address)
 

 
 
@@ -779,9 +762,9 @@ to modify it.
 
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);
 

 
 
@@ -794,8 +777,8 @@ to modify it.
 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,
                               }
                            );
@@ -845,7 +828,7 @@ Removed validator should no longer be valid.
 ### Function `update_config_and_reconfigure`
 
 
-
public fun update_config_and_reconfigure(operator_account: &signer, validator_address: address)
+
public fun update_config_and_reconfigure(validator_operator_account: &signer, validator_address: address)
 

 
 
@@ -858,16 +841,19 @@ Removed validator should no longer be valid.
 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;
 

 
 
@@ -1109,6 +1095,18 @@ exists v in spec_get_validators

 
 
+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.
+
+
+
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].
 
 
@@ -1128,7 +1126,8 @@ The permission "{Add, Remove} Validator" is granted to LibraRoot [B22].
 
 
 
-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>
diff --git a/language/stdlib/modules/doc/Roles.md b/language/stdlib/modules/doc/Roles.md
index da82eb95ef7..54c4b73edfc 100644
--- a/language/stdlib/modules/doc/Roles.md
+++ b/language/stdlib/modules/doc/Roles.md
@@ -927,7 +927,7 @@ Assert that the account has the designated dealer role.
 Assert that the account has the validator role.
 
 
-
public fun assert_validator(account: &signer)
+
public fun assert_validator(validator_account: &signer)
 

 
 
@@ -936,11 +936,11 @@ Assert that the account has the validator role.
 Implementation
 
 
-
public fun assert_validator(account: &signer) acquires RoleId {
-    let addr = Signer::address_of(account);
-    assert(exists<RoleId>(addr), Errors::not_published(EROLE_ID));
+
public fun assert_validator(validator_account: &signer) acquires RoleId {
+    let validator_addr = Signer::address_of(validator_account);
+    assert(exists<RoleId>(validator_addr), Errors::not_published(EROLE_ID));
     assert(
-        borrow_global<RoleId>(addr).role_id == VALIDATOR_ROLE_ID,
+        borrow_global<RoleId>(validator_addr).role_id == VALIDATOR_ROLE_ID,
         Errors::requires_role(EVALIDATOR)
     )
 }
@@ -957,7 +957,7 @@ Assert that the account has the validator role.
 Assert that the account has the validator operator role.
 
 
-
public fun assert_validator_operator(account: &signer)
+
public fun assert_validator_operator(validator_operator_account: &signer)
 

 
 
@@ -966,11 +966,11 @@ Assert that the account has the validator operator role.
 Implementation
 
 
-
public fun assert_validator_operator(account: &signer) acquires RoleId {
-    let addr = Signer::address_of(account);
-    assert(exists<RoleId>(addr), Errors::not_published(EROLE_ID));
+
public fun assert_validator_operator(validator_operator_account: &signer) acquires RoleId {
+    let validator_operator_addr = Signer::address_of(validator_operator_account);
+    assert(exists<RoleId>(validator_operator_addr), Errors::not_published(EROLE_ID));
     assert(
-        borrow_global<RoleId>(addr).role_id == VALIDATOR_OPERATOR_ROLE_ID,
+        borrow_global<RoleId>(validator_operator_addr).role_id == VALIDATOR_OPERATOR_ROLE_ID,
         Errors::requires_role(EVALIDATOR_OPERATOR)
     )
 }
@@ -1181,6 +1181,10 @@ Assert that the account has either the parent vasp or designated dealer role.
 
 
pragma opaque;
 include GrantRole;
+
+let addr = Signer::spec_address_of(account);
+requires role_id == LIBRA_ROOT_ROLE_ID ==> addr == CoreAddresses::LIBRA_ROOT_ADDRESS();
+requires role_id == TREASURY_COMPLIANCE_ROLE_ID ==> addr == CoreAddresses::TREASURY_COMPLIANCE_ADDRESS();
 

 
 
@@ -1194,8 +1198,6 @@ Assert that the account has either the parent vasp or designated dealer role.
     role_id: num;
     
     let addr = Signer::spec_address_of(account);
-    requires role_id == LIBRA_ROOT_ROLE_ID ==> addr == CoreAddresses::LIBRA_ROOT_ADDRESS();
-    requires role_id == TREASURY_COMPLIANCE_ROLE_ID ==> addr == CoreAddresses::TREASURY_COMPLIANCE_ADDRESS();
     aborts_if exists<RoleId>(addr) with Errors::ALREADY_PUBLISHED;
     ensures exists<RoleId>(addr);
     ensures global<RoleId>(addr).role_id == role_id;
@@ -1279,7 +1281,7 @@ Assert that the account has either the parent vasp or designated dealer role.
 ### Function `assert_validator`
 
 
-
public fun assert_validator(account: &signer)
+
public fun assert_validator(validator_account: &signer)
 

 
 
@@ -1296,7 +1298,7 @@ Assert that the account has either the parent vasp or designated dealer role.
 ### Function `assert_validator_operator`
 
 
-
public fun assert_validator_operator(account: &signer)
+
public fun assert_validator_operator(validator_operator_account: &signer)
 

 
 
@@ -1519,11 +1521,11 @@ Assert that the account has either the parent vasp or designated dealer role.
 
 
 
schema AbortsIfNotValidator {
-    account: signer;
-    
-    let addr = Signer::spec_address_of(account);
-    aborts_if !exists<RoleId>(addr) with Errors::NOT_PUBLISHED;
-    aborts_if global<RoleId>(addr).role_id != VALIDATOR_ROLE_ID with Errors::REQUIRES_ROLE;
+    validator_account: signer;
+    
+    let validator_addr = Signer::spec_address_of(validator_account);
+    aborts_if !exists<RoleId>(validator_addr) with Errors::NOT_PUBLISHED;
+    aborts_if global<RoleId>(validator_addr).role_id != VALIDATOR_ROLE_ID with Errors::REQUIRES_ROLE;
 }
 

 
@@ -1534,11 +1536,12 @@ Assert that the account has either the parent vasp or designated dealer role.
 
 
 
schema AbortsIfNotValidatorOperator {
-    account: signer;
-    
-    let addr = Signer::spec_address_of(account);
-    aborts_if !exists<RoleId>(addr) with Errors::NOT_PUBLISHED;
-    aborts_if global<RoleId>(addr).role_id != VALIDATOR_OPERATOR_ROLE_ID with Errors::REQUIRES_ROLE;
+    validator_operator_account: signer;
+    
+    let validator_operator_addr = Signer::spec_address_of(validator_operator_account);
+    aborts_if !exists<RoleId>(validator_operator_addr) with Errors::NOT_PUBLISHED;
+    aborts_if global<RoleId>(validator_operator_addr).role_id != VALIDATOR_OPERATOR_ROLE_ID
+        with Errors::REQUIRES_ROLE;
 }
 

 
diff --git a/language/stdlib/modules/doc/SlidingNonce.md b/language/stdlib/modules/doc/SlidingNonce.md
index a7b6fe48bf1..b41295b4a89 100644
--- a/language/stdlib/modules/doc/SlidingNonce.md
+++ b/language/stdlib/modules/doc/SlidingNonce.md
@@ -9,6 +9,7 @@
 -  [Const `ENONCE_TOO_OLD`](#0x1_SlidingNonce_ENONCE_TOO_OLD)
 -  [Const `ENONCE_TOO_NEW`](#0x1_SlidingNonce_ENONCE_TOO_NEW)
 -  [Const `ENONCE_ALREADY_RECORDED`](#0x1_SlidingNonce_ENONCE_ALREADY_RECORDED)
+-  [Const `ENONCE_ALREADY_PUBLISHED`](#0x1_SlidingNonce_ENONCE_ALREADY_PUBLISHED)
 -  [Const `NONCE_MASK_SIZE`](#0x1_SlidingNonce_NONCE_MASK_SIZE)
 -  [Function `record_nonce_or_abort`](#0x1_SlidingNonce_record_nonce_or_abort)
 -  [Function `try_record_nonce`](#0x1_SlidingNonce_try_record_nonce)
@@ -94,6 +95,18 @@ The nonce was already recorded previously
 
 
 
+
+
+## Const `ENONCE_ALREADY_PUBLISHED`
+
+Nonce
+
+
+
const ENONCE_ALREADY_PUBLISHED: u64 = 4;
+

+
+
+
 
 
 ## Const `NONCE_MASK_SIZE`
@@ -205,6 +218,7 @@ This is required before other functions in this module can be called for `accoun
 
 
 
public fun publish(account: &signer) {
+    assert(!exists<SlidingNonce>(Signer::address_of(account)), Errors::invalid_argument(ENONCE_ALREADY_PUBLISHED));
     move_to(account, SlidingNonce {  min_nonce: 0, nonce_mask: 0 });
 }
 

@@ -239,7 +253,9 @@ Only the libra root account can create this resource for different accounts
         min_nonce: 0,
         nonce_mask: 0,
     };
-    move_to(account, new_resource)
+    assert(!exists<SlidingNonce>(Signer::address_of(account)),
+            Errors::invalid_argument(ENONCE_ALREADY_PUBLISHED));
+    move_to(account, new_resource);
 }
 

 
diff --git a/language/stdlib/modules/doc/ValidatorConfig.md b/language/stdlib/modules/doc/ValidatorConfig.md
index 12a5365ad63..78a1370d33f 100644
--- a/language/stdlib/modules/doc/ValidatorConfig.md
+++ b/language/stdlib/modules/doc/ValidatorConfig.md
@@ -177,7 +177,7 @@ will have critical info such as keys, network addresses for validators,
 and the address of the validator operator.
 
 
-
public fun publish(account: &signer, lr_account: &signer, human_name: vector<u8>)
+
public fun publish(validator_account: &signer, lr_account: &signer, human_name: vector<u8>)
 

 
 
@@ -187,18 +187,18 @@ and the address of the validator operator.
 
 
 
public fun publish(
-    account: &signer,
+    validator_account: &signer,
     lr_account: &signer,
     human_name: vector<u8>,
 ) {
     LibraTimestamp::assert_operating();
     Roles::assert_libra_root(lr_account);
-    Roles::assert_validator(account);
+    Roles::assert_validator(validator_account);
     assert(
-        !exists<ValidatorConfig>(Signer::address_of(account)),
+        !exists<ValidatorConfig>(Signer::address_of(validator_account)),
         Errors::already_published(EVALIDATOR_CONFIG)
     );
-    move_to(account, ValidatorConfig {
+    move_to(validator_account, ValidatorConfig {
         config: Option::none(),
         operator_account: Option::none(),
         human_name,
@@ -243,7 +243,7 @@ Sets a new operator account, preserving the old config.
 Note: Access control.  No one but the owner of the account may change .operator_account
 
 
-
public fun set_operator(account: &signer, operator_account: address)
+
public fun set_operator(validator_account: &signer, operator_account: address)
 

 
 
@@ -252,8 +252,8 @@ Note: Access control.  No one but the owner of the account may change .operator_
 Implementation
 
 
-
public fun set_operator(account: &signer, operator_account: address) acquires ValidatorConfig {
-    Roles::assert_validator(account);
+
public fun set_operator(validator_account: &signer, operator_account: address) acquires ValidatorConfig {
+    Roles::assert_validator(validator_account);
     // Check for validator role is not necessary since the role is checked when the config
     // resource is published.
     // TODO (dd): Probably need to prove an invariant about role.
@@ -261,7 +261,7 @@ Note: Access control.  No one but the owner of the account may change .operator_
         ValidatorOperatorConfig::has_validator_operator_config(operator_account),
         Errors::invalid_argument(ENOT_A_VALIDATOR_OPERATOR)
     );
-    let sender = Signer::address_of(account);
+    let sender = Signer::address_of(validator_account);
     assert(exists_config(sender), Errors::not_published(EVALIDATOR_CONFIG));
     (borrow_global_mut<ValidatorConfig>(sender)).operator_account = Option::some(operator_account);
 }
@@ -279,7 +279,7 @@ Removes an operator account, setting a corresponding field to Option::none.
 The old config is preserved.
 
 
-
public fun remove_operator(account: &signer)
+
public fun remove_operator(validator_account: &signer)
 

 
 
@@ -288,9 +288,9 @@ The old config is preserved.
 Implementation
 
 
-
public fun remove_operator(account: &signer) acquires ValidatorConfig {
-    Roles::assert_validator(account);
-    let sender = Signer::address_of(account);
+
public fun remove_operator(validator_account: &signer) acquires ValidatorConfig {
+    Roles::assert_validator(validator_account);
+    let sender = Signer::address_of(validator_account);
     // Config field remains set
     assert(exists_config(sender), Errors::not_published(EVALIDATOR_CONFIG));
     (borrow_global_mut<ValidatorConfig>(sender)).operator_account = Option::none();
@@ -525,7 +525,7 @@ Never aborts
 ### Function `publish`
 
 
-
public fun publish(account: &signer, lr_account: &signer, human_name: vector<u8>)
+
public fun publish(validator_account: &signer, lr_account: &signer, human_name: vector<u8>)
 

 
 
@@ -534,8 +534,9 @@ Never aborts
 
include LibraTimestamp::AbortsIfNotOperating;
 include Roles::AbortsIfNotLibraRoot{account: lr_account};
 include Roles::AbortsIfNotValidator;
-aborts_if exists_config(Signer::spec_address_of(account)) with Errors::ALREADY_PUBLISHED;
-ensures exists_config(Signer::spec_address_of(account));
+aborts_if exists_config(Signer::spec_address_of(validator_account))
+    with Errors::ALREADY_PUBLISHED;
+ensures exists_config(Signer::spec_address_of(validator_account));
 

 
 
@@ -558,7 +559,7 @@ Describes abort if ValidatorConfig does not exist.
 ### Function `set_operator`
 
 
-
public fun set_operator(account: &signer, operator_account: address)
+
public fun set_operator(validator_account: &signer, operator_account: address)
 

 
 
@@ -570,7 +571,7 @@ Must abort if the signer does not have the Validator role [B24].
 aborts_if !ValidatorOperatorConfig::has_validator_operator_config(operator_account)
     with Errors::INVALID_ARGUMENT;
 
-let sender = Signer::spec_address_of(account);
+let sender = Signer::spec_address_of(validator_account);
 include AbortsIfNoValidatorConfig{addr: sender};
 aborts_if !ValidatorOperatorConfig::has_validator_operator_config(operator_account) with Errors::NOT_PUBLISHED;
 ensures spec_has_operator(sender);
@@ -634,7 +635,7 @@ Returns the human name of the validator
 ### Function `remove_operator`
 
 
-
public fun remove_operator(account: &signer)
+
public fun remove_operator(validator_account: &signer)
 

 
 
@@ -644,9 +645,9 @@ Must abort if the signer does not have the Validator role [B24].
 
 
include Roles::AbortsIfNotValidator;
 
-let sender = Signer::spec_address_of(account);
+let sender = Signer::spec_address_of(validator_account);
 include AbortsIfNoValidatorConfig{addr: sender};
-ensures !spec_has_operator(Signer::spec_address_of(account));
+ensures !spec_has_operator(Signer::spec_address_of(validator_account));
 ensures spec_get_operator(sender) == sender;
 

 
diff --git a/language/stdlib/modules/doc/ValidatorOperatorConfig.md b/language/stdlib/modules/doc/ValidatorOperatorConfig.md
index 17c445d06c3..e8796acff1a 100644
--- a/language/stdlib/modules/doc/ValidatorOperatorConfig.md
+++ b/language/stdlib/modules/doc/ValidatorOperatorConfig.md
@@ -64,7 +64,7 @@ The
 
 
 
-
public fun publish(account: &signer, lr_account: &signer, human_name: vector<u8>)
+
public fun publish(validator_operator_account: &signer, lr_account: &signer, human_name: vector<u8>)
 

 
 
@@ -74,18 +74,18 @@ The
 
 
 
public fun publish(
-    account: &signer,
+    validator_operator_account: &signer,
     lr_account: &signer,
     human_name: vector<u8>,
 ) {
     Roles::assert_libra_root(lr_account);
-    Roles::assert_validator_operator(account);
+    Roles::assert_validator_operator(validator_operator_account);
     assert(
-        !has_validator_operator_config(Signer::address_of(account)),
+        !has_validator_operator_config(Signer::address_of(validator_operator_account)),
         Errors::already_published(EVALIDATOR_OPERATOR_CONFIG)
     );
 
-    move_to(account, ValidatorOperatorConfig {
+    move_to(validator_operator_account, ValidatorOperatorConfig {
         human_name,
     });
 }
@@ -103,7 +103,7 @@ Get validator's account human name
 Aborts if there is no ValidatorOperatorConfig resource
 
 
-
public fun get_human_name(addr: address): vector<u8>
+
public fun get_human_name(validator_operator_addr: address): vector<u8>
 

 
 
@@ -112,9 +112,9 @@ Aborts if there is no ValidatorOperatorConfig resource
 Implementation
 
 
-
public fun get_human_name(addr: address): vector<u8> acquires ValidatorOperatorConfig {
-    assert(has_validator_operator_config(addr), Errors::not_published(EVALIDATOR_OPERATOR_CONFIG));
-    *&borrow_global<ValidatorOperatorConfig>(addr).human_name
+
public fun get_human_name(validator_operator_addr: address): vector<u8> acquires ValidatorOperatorConfig {
+    assert(has_validator_operator_config(validator_operator_addr), Errors::not_published(EVALIDATOR_OPERATOR_CONFIG));
+    *&borrow_global<ValidatorOperatorConfig>(validator_operator_addr).human_name
 }
 

 
@@ -128,7 +128,7 @@ Aborts if there is no ValidatorOperatorConfig resource
 
 
 
-
public fun has_validator_operator_config(addr: address): bool
+
public fun has_validator_operator_config(validator_operator_addr: address): bool
 

 
 
@@ -137,8 +137,8 @@ Aborts if there is no ValidatorOperatorConfig resource
 Implementation
 
 
-
public fun has_validator_operator_config(addr: address): bool {
-    exists<ValidatorOperatorConfig>(addr)
+
public fun has_validator_operator_config(validator_operator_addr: address): bool {
+    exists<ValidatorOperatorConfig>(validator_operator_addr)
 }
 

 
@@ -156,7 +156,7 @@ Aborts if there is no ValidatorOperatorConfig resource
 ### Function `publish`
 
 
-
public fun publish(account: &signer, lr_account: &signer, human_name: vector<u8>)
+
public fun publish(validator_operator_account: &signer, lr_account: &signer, human_name: vector<u8>)
 

 
 
@@ -164,8 +164,9 @@ Aborts if there is no ValidatorOperatorConfig resource
 
 
include Roles::AbortsIfNotLibraRoot{account: lr_account};
 include Roles::AbortsIfNotValidatorOperator;
-aborts_if has_validator_operator_config(Signer::spec_address_of(account)) with Errors::ALREADY_PUBLISHED;
-ensures has_validator_operator_config(Signer::spec_address_of(account));
+aborts_if has_validator_operator_config(Signer::spec_address_of(validator_operator_account))
+    with Errors::ALREADY_PUBLISHED;
+ensures has_validator_operator_config(Signer::spec_address_of(validator_operator_account));
 

 
 
@@ -175,15 +176,15 @@ Aborts if there is no ValidatorOperatorConfig resource
 ### Function `get_human_name`
 
 
-
public fun get_human_name(addr: address): vector<u8>
+
public fun get_human_name(validator_operator_addr: address): vector<u8>
 

 
 
 
 
 
pragma opaque;
-aborts_if !has_validator_operator_config(addr) with Errors::NOT_PUBLISHED;
-ensures result == get_human_name(addr);
+aborts_if !has_validator_operator_config(validator_operator_addr) with Errors::NOT_PUBLISHED;
+ensures result == get_human_name(validator_operator_addr);
 

 
 
@@ -193,11 +194,11 @@ Aborts if there is no ValidatorOperatorConfig resource
 ### Function `has_validator_operator_config`
 
 
-
public fun has_validator_operator_config(addr: address): bool
+
public fun has_validator_operator_config(validator_operator_addr: address): bool
 

 
 
 
 
-
ensures result == has_validator_operator_config(addr);
+
ensures result == has_validator_operator_config(validator_operator_addr);
 

diff --git a/language/stdlib/transaction_scripts/create_validator_account.move b/language/stdlib/transaction_scripts/create_validator_account.move
index 228235ccd06..2bac20010ad 100644
--- a/language/stdlib/transaction_scripts/create_validator_account.move
+++ b/language/stdlib/transaction_scripts/create_validator_account.move
@@ -3,15 +3,15 @@ script {
     use 0x1::SlidingNonce;
     /// Create a validator account at `new_validator_address` with `auth_key_prefix`and human_name.
     fun create_validator_account(
-        creator: &signer,
+        lr_account: &signer,
         sliding_nonce: u64,
         new_account_address: address,
         auth_key_prefix: vector,
         human_name: vector,
         ) {
-        SlidingNonce::record_nonce_or_abort(creator, sliding_nonce);
+        SlidingNonce::record_nonce_or_abort(lr_account, sliding_nonce);
         LibraAccount::create_validator_account(
-            creator,
+            lr_account,
             new_account_address,
             auth_key_prefix,
             human_name,
diff --git a/language/stdlib/transaction_scripts/create_validator_operator_account.move b/language/stdlib/transaction_scripts/create_validator_operator_account.move
index 82714e5c3cf..e991c487aaa 100644
--- a/language/stdlib/transaction_scripts/create_validator_operator_account.move
+++ b/language/stdlib/transaction_scripts/create_validator_operator_account.move
@@ -3,10 +3,10 @@ script {
     use 0x1::SlidingNonce;
 
     /// Create a validator operator account at `new_validator_address` with `auth_key_prefix`and human_name.
-    fun create_validator_operator_account(creator: &signer, sliding_nonce: u64, new_account_address: address, auth_key_prefix: vector, human_name: vector) {
-        SlidingNonce::record_nonce_or_abort(creator, sliding_nonce);
+    fun create_validator_operator_account(lr_account: &signer, sliding_nonce: u64, new_account_address: address, auth_key_prefix: vector, human_name: vector) {
+        SlidingNonce::record_nonce_or_abort(lr_account, sliding_nonce);
         LibraAccount::create_validator_operator_account(
-            creator,
+            lr_account,
             new_account_address,
             auth_key_prefix,
             human_name,
diff --git a/language/stdlib/transaction_scripts/doc/create_validator_account.md b/language/stdlib/transaction_scripts/doc/create_validator_account.md
index 480e78685be..6ade2153996 100644
--- a/language/stdlib/transaction_scripts/doc/create_validator_account.md
+++ b/language/stdlib/transaction_scripts/doc/create_validator_account.md
@@ -18,7 +18,7 @@ Create a validator account at
 auth_key_prefixand human_name.
 
 
-
public fun create_validator_account(creator: &signer, sliding_nonce: u64, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>)
+
public fun create_validator_account(lr_account: &signer, sliding_nonce: u64, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>)
 

 
 
@@ -28,15 +28,15 @@ Create a validator account at
 
 
 
fun create_validator_account(
-    creator: &signer,
+    lr_account: &signer,
     sliding_nonce: u64,
     new_account_address: address,
     auth_key_prefix: vector<u8>,
     human_name: vector<u8>,
     ) {
-    SlidingNonce::record_nonce_or_abort(creator, sliding_nonce);
+    SlidingNonce::record_nonce_or_abort(lr_account, sliding_nonce);
     LibraAccount::create_validator_account(
-        creator,
+        lr_account,
         new_account_address,
         auth_key_prefix,
         human_name,
diff --git a/language/stdlib/transaction_scripts/doc/create_validator_operator_account.md b/language/stdlib/transaction_scripts/doc/create_validator_operator_account.md
index 567b51ba23c..442fd7c8a0a 100644
--- a/language/stdlib/transaction_scripts/doc/create_validator_operator_account.md
+++ b/language/stdlib/transaction_scripts/doc/create_validator_operator_account.md
@@ -18,7 +18,7 @@ Create a validator operator account at
 auth_key_prefixand human_name.
 
 
-
public fun create_validator_operator_account(creator: &signer, sliding_nonce: u64, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>)
+
public fun create_validator_operator_account(lr_account: &signer, sliding_nonce: u64, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>)
 

 
 
@@ -27,10 +27,10 @@ Create a validator operator account at
 Implementation
 
 
-
fun create_validator_operator_account(creator: &signer, sliding_nonce: u64, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>) {
-    SlidingNonce::record_nonce_or_abort(creator, sliding_nonce);
+
fun create_validator_operator_account(lr_account: &signer, sliding_nonce: u64, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>) {
+    SlidingNonce::record_nonce_or_abort(lr_account, sliding_nonce);
     LibraAccount::create_validator_operator_account(
-        creator,
+        lr_account,
         new_account_address,
         auth_key_prefix,
         human_name,
diff --git a/language/stdlib/transaction_scripts/doc/freeze_account.md b/language/stdlib/transaction_scripts/doc/freeze_account.md
index 65634f15071..03d3d0a6a77 100644
--- a/language/stdlib/transaction_scripts/doc/freeze_account.md
+++ b/language/stdlib/transaction_scripts/doc/freeze_account.md
@@ -18,7 +18,7 @@ Freeze account
 sliding_nonce is a unique nonce for operation, see sliding_nonce.move for details.
 
 
-
public fun freeze_account(account: &signer, sliding_nonce: u64, to_freeze_account: address)
+
public fun freeze_account(tc_account: &signer, sliding_nonce: u64, to_freeze_account: address)
 

 
 
@@ -27,9 +27,9 @@ Freeze account
 Implementation
 
 
-
fun freeze_account(account: &signer, sliding_nonce: u64, to_freeze_account: address) {
-    SlidingNonce::record_nonce_or_abort(account, sliding_nonce);
-    AccountFreezing::freeze_account(account, to_freeze_account);
+
fun freeze_account(tc_account: &signer, sliding_nonce: u64, to_freeze_account: address) {
+    SlidingNonce::record_nonce_or_abort(tc_account, sliding_nonce);
+    AccountFreezing::freeze_account(tc_account, to_freeze_account);
 }
 

 
diff --git a/language/stdlib/transaction_scripts/freeze_account.move b/language/stdlib/transaction_scripts/freeze_account.move
index c25e7bd4ee2..40732440582 100644
--- a/language/stdlib/transaction_scripts/freeze_account.move
+++ b/language/stdlib/transaction_scripts/freeze_account.move
@@ -4,8 +4,8 @@ use 0x1::SlidingNonce;
 
 /// Freeze account `address`. Initiator must be authorized.
 /// `sliding_nonce` is a unique nonce for operation, see sliding_nonce.move for details.
-fun freeze_account(account: &signer, sliding_nonce: u64, to_freeze_account: address) {
-    SlidingNonce::record_nonce_or_abort(account, sliding_nonce);
-    AccountFreezing::freeze_account(account, to_freeze_account);
+fun freeze_account(tc_account: &signer, sliding_nonce: u64, to_freeze_account: address) {
+    SlidingNonce::record_nonce_or_abort(tc_account, sliding_nonce);
+    AccountFreezing::freeze_account(tc_account, to_freeze_account);
 }
 }