From cff02bad86e7139e8bf4bcb033c4b12a1a8ac088 Mon Sep 17 00:00:00 2001 From: David Dill Date: Fri, 11 Sep 2020 11:10:01 -0700 Subject: [PATCH] [move framework][move-prover] DRAFT: Move role creation from Genesis 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. --- .../error_descriptions.errmap | Bin 12898 -> 12953 bytes language/stdlib/compiled/stdlib/005_Roles.mv | Bin 1946 -> 1952 bytes .../compiled/stdlib/030_SlidingNonce.mv | Bin 783 -> 848 bytes .../compiled/stdlib/032_LibraAccount.mv | Bin 6902 -> 7052 bytes .../stdlib/compiled/stdlib/038_Genesis.mv | Bin 1077 -> 841 bytes language/stdlib/modules/Genesis.move | 22 +--- language/stdlib/modules/LibraAccount.move | 47 +++++-- language/stdlib/modules/LibraSystem.move | 86 ++++++------ language/stdlib/modules/Roles.move | 40 +++--- language/stdlib/modules/SlidingNonce.move | 7 +- language/stdlib/modules/ValidatorConfig.move | 31 ++--- .../modules/ValidatorOperatorConfig.move | 29 +++-- language/stdlib/modules/doc/Genesis.md | 22 +--- language/stdlib/modules/doc/LibraAccount.md | 72 +++++++--- language/stdlib/modules/doc/LibraSystem.md | 123 +++++++++--------- language/stdlib/modules/doc/Roles.md | 51 ++++---- language/stdlib/modules/doc/SlidingNonce.md | 18 ++- .../stdlib/modules/doc/ValidatorConfig.md | 43 +++--- .../modules/doc/ValidatorOperatorConfig.md | 41 +++--- .../create_validator_account.move | 6 +- .../create_validator_operator_account.move | 6 +- .../doc/create_validator_account.md | 8 +- .../doc/create_validator_operator_account.md | 8 +- .../transaction_scripts/doc/freeze_account.md | 8 +- .../transaction_scripts/freeze_account.move | 6 +- 25 files changed, 371 insertions(+), 303 deletions(-) diff --git a/language/stdlib/compiled/error_descriptions/error_descriptions.errmap b/language/stdlib/compiled/error_descriptions/error_descriptions.errmap index dc88054f888ac0fd3950791f8e3989744888a4ba..264ff6caadd0ccd43ffc1a0dd669b1aa28e5c72d 100644 GIT binary patch delta 82 zcmaEqGBb69ov?tfg0g~ZQBi)8LUMjeYBASld*N-|j4YeK$*D4GurNS?gsY#wpR;Sc hqfd~lqf2CbK&X?CXRwE>3!8#peqM6wW@!a?Apqr57Q6re delta 26 icmbQ4`Y2_CoiL-_WFedS>;t3HwP)W3jqLqQ3u%o diff --git a/language/stdlib/compiled/stdlib/005_Roles.mv b/language/stdlib/compiled/stdlib/005_Roles.mv index b254641f2b14a9f13389cf2c4ad9599e39b9c929..ab232f5ed83aaa06da728b6b1c213dda7f811784 100644 GIT binary patch delta 190 zcma*eF%AJi6adiw=g*%%W*QKJ}XFKCMU8g3o|RS zvkNlwu=22QvoK3@v#K-kO^#z#6K7Fm=Rg(bXJlmHob1Ksz{oYZo2`hEd-6ZFMF0#B B6*K?< diff --git a/language/stdlib/compiled/stdlib/030_SlidingNonce.mv b/language/stdlib/compiled/stdlib/030_SlidingNonce.mv index aa2f1d7a3a1ed5031f6219aee1228efaec5242da..76454fc8dbea7039ee755d30ca190df9944f5977 100644 GIT binary patch delta 236 zcmYL@F-k*06h+^CZ~mLfyovq~-vs$28j!>Yf}{{z7h#ds!YTw@heZriX9HP-jh%Kj z*@D~9F9~?7Q=9{LrC<75pN{>*7U2h_u6P#T*{2WQNq3{`>-)eE2?SX`e+EbUk_X&e yaoa^-Qr%A+*}Jja6!SmmD-IueNuzp~ANdk4zwpx#+$N}F(U?ERi5^7a7C^r|NE(g+ delta 171 zcmXYou@1pd7)Jl^zwLjo+lop`BTa|_C6RQp8*NsL(Ia>W3(b9mZbq9&kQi(t@gx$7 z3THaQIXBtMA@20`@(A-nBsU@c0{YPo#fnz0^VC#dv<5NyY~7LAKOVB-($zIPvZEpaU9!;Z?SW6;u;-B)a{A224;r(1cFZdrd=Tg6I{sXFCv~1}2 zT7C1p^(TeQFNX@juZNzFt)xyNGB)w_*>qJPq&h)Bwo4FnJLnM{^3Im;1qt~+H#?pp z=yx#S;Dm!g2PX;2L!Lk^5BnT36QvcRI;{mVH3Ek43<=;UO29Fs**Gm(1v0?SqO6i5 zlYt~W=TJ{61^m3oLNF~zGnmO)!dXF@!G*lDT&!_8SD?Fs`J&rh5QN@hiR|7|EzL`p zkhDt6brMP|bZ_Z0B9yL>r=_a|<{B@98Lw{uv+CkE*BctaztKeJ{k1~^iZ?Ay>t3L# zeX%)2wCgQourIZes=XDqA=bLh!Ul=uUZx!7ZXcEacigRT_Xu&}9yq*@3g7{ftMJNE zhYu-sn8~@l&31>?tz&L@q{zOVOdn$hz^k3K-svLPb+AW4z~>xX=yvqacaZT5J#PA% zvwjhJ0lox%0AD`tjISr2yx}hUNb-%U*4!!vZ*_i>bJ0Po@$4Kv}) z_{_vi7*2CTL-HFvoU$|RY9bcWOpKlAh<0t&D5)Dh4_$~2M z&Wwy(WVhgo;fHhb87nkgUY@F~Tv@)pKDju*G&fsWn4F4#?>%fR-rKqLXm5SNJ_9-ZOKt)Cxa@pjhbmB{mZ1E`&2BY{U{RUvj=fp`7ciKQ=HKQ z&eeaX)dQO{%%DcDG;3GT#dAC|?Am`ANB##zL>aaUoU(p?(HipTQ2emwFs{Y#){Nna z_%}6!+3O5$B#fDXq<;Cr?dsZoxjQ(!N&2(RNx>NP;MLIctuVrH&3T|jJK5F}-%>_u z$?J5AOr6|0n&nZ6z3|!d*FrD*|IeEP0TI=*7h^15s;&db47oSJh4d9fWrLDx5!Jhk z*h>f(o08fnuaq>_k^%~L#d;kOdT5#9hH1uYHK68{JqjqyLl3Z9E>aCSk8J?VO$4qp zU2)T`9=F^`BedW_{86!=lJ>V^WL++M9WK)v({`md6riB5Ml6`5D(kVV5&$@FVAC{+mPFzfHD3G@ka1 zFVCfouYHO%%^oE=TyAqY%=rZ)Y-D`8Vkj2nw%TFi*|ZYc^NN(%F1DR??n*pXey#F2 zIcYPRvQF|m>ZZf=?|>EwIn7>82$v5zX}3WNJ+8j?lxq(g#s4U`Ht!rXgwJ*p?JHf@ oP=AmoQc22cR6o_U2MAXO5}89TUO&q6v}{!L4QWrr&+Bjg3shbY{{R30 delta 2269 zcmaJ>S#wm!6+Wkzxp%sI?o5wnMl;%IEg-bcNJ!{{79=4d0RjO+Alukr1lVAKMOG(q zGS1?}Yhrx8l^l!ZRxTn! zNBq?||@XCmj!)TU`RmPgq)4pQNRI>VQME*Sg7IpY9=5 z`;6;FZ1v94brLJwpvn}U?UMjEeN@;!NL;uD9&e)pxPx?6c0s4WyJHpIY`EDjr!%cz4bd#2ly^D0A3pN z#_y#!`MwYKgK-A%@)277aKgKOH0iN<)Z;6dntqIRa{mMy0-EqsoTAOoF!qF35jnum z@fhJR@VHO!HJm2@>zKwlH{)4vq^376YA(o2}0_rrbSuz#Vc2UF*t2cg#)KryEz@krCJBDp<;w^K*^4dUd6`w(WLZzguxL z^_j*sw>!VPu(>$wb{9A2Hy2vhoEu0!;a@8z6+^=_MkeowPm(b?{P|7!0ZU5Z_UFF| z>tPcZ{u09w8U6}&7PG(@zJrpp%x%RUq0V8Lc{hEr1a*L+crSg)SCI=Q-ba2)u@6vw zh!pGb{-eEpCY3^m^SFSEClLf!Fb!-80Q(eJFf4gsXY?|{$(~q{B}#s4<1?qIyi0l7 zZUta7h8fhzm1g}4hIj!=Yy}Yo@n<2xT3qVe{JK7(KN}C>|>1}EaWC1Fb9|q( z@qb&uW5X{0lac(Pr5bI5FY>8%t0{bY^4FF=+)ApYIcy|XOB4Ak46de()p6g~1B{yXuq3-bR>+$ne9Q_1V) zi?^-;$Q;G1b0I?oam}FA^ltML#hyl3s-)%2+F$@&fR^nKTR{Vj2+bSasj~+dL7x;~DpJ@56X<|vNh=8Z{q$+3xDraL zOx(ksO~+Eu{R&};eB@W;k9(i;}o&zuLPf^HrQ|-$`{_Mr z3qo1JD4Rse8Y6J?R}Lk9A7|IAy6x(le)-T|HBHeqebq1To9eFas;;kBeRDfJiu2(| zyskZfzBJ$_28?zQCuCwqa)VBdPDZEPiZK~ZbH*{6DVUtG)?|i+o04&v0g^^J;+atD SW`umFj40+ixs1Sp5bzHk-zU!i delta 613 zcmZvZF>ll`7=}N8Nu0!X({nG^_ChJp3Q-jaF|e{SAh7^@l;+GeQkqn;Z(zES`P3OC zenfvnJ9X{IjF|WV@cHNf5|-X4uiy8Rt;kpWGCBIX_gyjoNEjUBaTq-N#G*^~I{wA3 z!{myO_$|-X5B_C!_+$xV$kTfa#uH$$u?+}YJ080M0-us&1p$i?L3)>X1O>IBN9+;# zEcY%eB7}606Yj@^eMlhnZTcV~JWLU^-;O*s3xUr;Jt8X(2vA76jw==ca>W$^1FnQX zhLP}=xVkySK&*a#TSjmD)>!_onRjN$-Var0tJ*bv_sSSi&1QqKw(LLT*0|C&XQn)@ zY-wFJI5V5fY21}T0vD_4(qYZR}||H+16# z$Hy~7@ZDSloG)FXPTe^vpY-o!wE4kFcDfJVWH0VyQK zq=Y)A(>47Z(~{DNv_%3T^yWIQMyaoCMnXCG!gJZYb7%&QRhctft~2_^ UGSNGdQLi#3L+X_tOVAAAH}g$u3jhEB 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);
 }
 }