language/diem-framework/releases/artifacts/release-1.2.0-rc0/docs/modules/Roles.md
<a name="0x1_Roles"></a>
0x1::RolesThis module defines role-based access control for the Diem framework.
Roles are associated with accounts and govern what operations are permitted by those accounts. A role is typically asserted on function entry using a statement like <code><a href="Roles.md#0x1_Roles_assert_diem_root">Self::assert_diem_root</a>(account)</code>. This module provides multiple assertion functions like this one, as well as the functions to setup roles.
For a conceptual discussion of roles, see the DIP-2 document.
RoleIdgrant_diem_root_rolegrant_treasury_compliance_rolenew_designated_dealer_rolenew_validator_rolenew_validator_operator_rolenew_parent_vasp_rolenew_child_vasp_rolegrant_rolehas_rolehas_diem_root_rolehas_treasury_compliance_rolehas_designated_dealer_rolehas_validator_rolehas_validator_operator_rolehas_parent_VASP_rolehas_child_VASP_roleget_role_idcan_hold_balanceassert_diem_rootassert_treasury_complianceassert_parent_vasp_roleassert_child_vasp_roleassert_designated_dealerassert_validatorassert_validator_operatorassert_parent_vasp_or_designated_dealerassert_parent_vasp_or_child_vasp<a name="0x1_Roles_RoleId"></a>
RoleIdThe roleId contains the role id for the account. This is only moved to an account as a top-level resource, and is otherwise immovable.
<pre><code><b>resource</b> <b>struct</b> <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>role_id: u64</code> </dt> <dd> </dd> </dl> </details><a name="@Constants_0"></a>
<a name="0x1_Roles_EDIEM_ROOT"></a>
The signer didn't have the required Diem Root role
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_EDIEM_ROOT">EDIEM_ROOT</a>: u64 = 1; </code></pre><a name="0x1_Roles_ETREASURY_COMPLIANCE"></a>
The signer didn't have the required Treasury & Compliance role
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_ETREASURY_COMPLIANCE">ETREASURY_COMPLIANCE</a>: u64 = 2; </code></pre><a name="0x1_Roles_CHILD_VASP_ROLE_ID"></a>
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_CHILD_VASP_ROLE_ID">CHILD_VASP_ROLE_ID</a>: u64 = 6; </code></pre><a name="0x1_Roles_DESIGNATED_DEALER_ROLE_ID"></a>
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_DESIGNATED_DEALER_ROLE_ID">DESIGNATED_DEALER_ROLE_ID</a>: u64 = 2; </code></pre><a name="0x1_Roles_DIEM_ROOT_ROLE_ID"></a>
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_DIEM_ROOT_ROLE_ID">DIEM_ROOT_ROLE_ID</a>: u64 = 0; </code></pre><a name="0x1_Roles_ECHILD_VASP"></a>
The signer didn't have the required Child VASP role
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_ECHILD_VASP">ECHILD_VASP</a>: u64 = 9; </code></pre><a name="0x1_Roles_EDESIGNATED_DEALER"></a>
The signer didn't have the required Designated Dealer role
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_EDESIGNATED_DEALER">EDESIGNATED_DEALER</a>: u64 = 6; </code></pre><a name="0x1_Roles_EPARENT_VASP"></a>
The signer didn't have the required Parent VASP role
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_EPARENT_VASP">EPARENT_VASP</a>: u64 = 3; </code></pre><a name="0x1_Roles_EPARENT_VASP_OR_CHILD_VASP"></a>
The signer didn't have the required ParentVASP or ChildVASP role
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_EPARENT_VASP_OR_CHILD_VASP">EPARENT_VASP_OR_CHILD_VASP</a>: u64 = 4; </code></pre><a name="0x1_Roles_EPARENT_VASP_OR_DESIGNATED_DEALER"></a>
The signer didn't have the required Parent VASP or Designated Dealer role
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_EPARENT_VASP_OR_DESIGNATED_DEALER">EPARENT_VASP_OR_DESIGNATED_DEALER</a>: u64 = 5; </code></pre><a name="0x1_Roles_EROLE_ID"></a>
A <code><a href="Roles.md#0x1_Roles_RoleId">RoleId</a></code> resource was in an unexpected state
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_EROLE_ID">EROLE_ID</a>: u64 = 0; </code></pre><a name="0x1_Roles_EVALIDATOR"></a>
The signer didn't have the required Validator role
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_EVALIDATOR">EVALIDATOR</a>: u64 = 7; </code></pre><a name="0x1_Roles_EVALIDATOR_OPERATOR"></a>
The signer didn't have the required Validator Operator role
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_EVALIDATOR_OPERATOR">EVALIDATOR_OPERATOR</a>: u64 = 8; </code></pre><a name="0x1_Roles_PARENT_VASP_ROLE_ID"></a>
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_PARENT_VASP_ROLE_ID">PARENT_VASP_ROLE_ID</a>: u64 = 5; </code></pre><a name="0x1_Roles_TREASURY_COMPLIANCE_ROLE_ID"></a>
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_TREASURY_COMPLIANCE_ROLE_ID">TREASURY_COMPLIANCE_ROLE_ID</a>: u64 = 1; </code></pre><a name="0x1_Roles_VALIDATOR_OPERATOR_ROLE_ID"></a>
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_VALIDATOR_OPERATOR_ROLE_ID">VALIDATOR_OPERATOR_ROLE_ID</a>: u64 = 4; </code></pre><a name="0x1_Roles_VALIDATOR_ROLE_ID"></a>
<pre><code><b>const</b> <a href="Roles.md#0x1_Roles_VALIDATOR_ROLE_ID">VALIDATOR_ROLE_ID</a>: u64 = 3; </code></pre><a name="0x1_Roles_grant_diem_root_role"></a>
grant_diem_root_rolePublishes diem root role. Granted only in genesis.
<pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_grant_diem_root_role">grant_diem_root_role</a>(dr_account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_grant_diem_root_role">grant_diem_root_role</a>( dr_account: &signer, ) { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_genesis">DiemTimestamp::assert_genesis</a>(); // Checks actual <a href="Diem.md#0x1_Diem">Diem</a> root because <a href="Diem.md#0x1_Diem">Diem</a> root role is not set // until next line of code. <a href="CoreAddresses.md#0x1_CoreAddresses_assert_diem_root">CoreAddresses::assert_diem_root</a>(dr_account); // Grant the role <b>to</b> the diem root account <a href="Roles.md#0x1_Roles_grant_role">grant_role</a>(dr_account, <a href="Roles.md#0x1_Roles_DIEM_ROOT_ROLE_ID">DIEM_ROOT_ROLE_ID</a>); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>include</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotGenesis">DiemTimestamp::AbortsIfNotGenesis</a>; <b>include</b> <a href="CoreAddresses.md#0x1_CoreAddresses_AbortsIfNotDiemRoot">CoreAddresses::AbortsIfNotDiemRoot</a>{account: dr_account}; <b>include</b> <a href="Roles.md#0x1_Roles_GrantRole">GrantRole</a>{addr: <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(dr_account), role_id: <a href="Roles.md#0x1_Roles_DIEM_ROOT_ROLE_ID">DIEM_ROOT_ROLE_ID</a>}; </code></pre> </details><a name="0x1_Roles_grant_treasury_compliance_role"></a>
grant_treasury_compliance_rolePublishes treasury compliance role. Granted only in genesis.
<pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_grant_treasury_compliance_role">grant_treasury_compliance_role</a>(treasury_compliance_account: &signer, dr_account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_grant_treasury_compliance_role">grant_treasury_compliance_role</a>( treasury_compliance_account: &signer, dr_account: &signer, ) <b>acquires</b> <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_genesis">DiemTimestamp::assert_genesis</a>(); <a href="CoreAddresses.md#0x1_CoreAddresses_assert_treasury_compliance">CoreAddresses::assert_treasury_compliance</a>(treasury_compliance_account); <a href="Roles.md#0x1_Roles_assert_diem_root">assert_diem_root</a>(dr_account); // Grant the TC role <b>to</b> the treasury_compliance_account <a href="Roles.md#0x1_Roles_grant_role">grant_role</a>(treasury_compliance_account, <a href="Roles.md#0x1_Roles_TREASURY_COMPLIANCE_ROLE_ID">TREASURY_COMPLIANCE_ROLE_ID</a>); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>include</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotGenesis">DiemTimestamp::AbortsIfNotGenesis</a>; <b>include</b> <a href="CoreAddresses.md#0x1_CoreAddresses_AbortsIfNotTreasuryCompliance">CoreAddresses::AbortsIfNotTreasuryCompliance</a>{account: treasury_compliance_account}; <b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">AbortsIfNotDiemRoot</a>{account: dr_account}; <b>include</b> <a href="Roles.md#0x1_Roles_GrantRole">GrantRole</a>{addr: <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(treasury_compliance_account), role_id: <a href="Roles.md#0x1_Roles_TREASURY_COMPLIANCE_ROLE_ID">TREASURY_COMPLIANCE_ROLE_ID</a>}; </code></pre> </details><a name="0x1_Roles_new_designated_dealer_role"></a>
new_designated_dealer_rolePublishes a DesignatedDealer <code><a href="Roles.md#0x1_Roles_RoleId">RoleId</a></code> under <code>new_account</code>. The <code>creating_account</code> must be treasury compliance.
<pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_new_designated_dealer_role">new_designated_dealer_role</a>(creating_account: &signer, new_account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_new_designated_dealer_role">new_designated_dealer_role</a>( creating_account: &signer, new_account: &signer, ) <b>acquires</b> <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> { <a href="Roles.md#0x1_Roles_assert_treasury_compliance">assert_treasury_compliance</a>(creating_account); <a href="Roles.md#0x1_Roles_grant_role">grant_role</a>(new_account, <a href="Roles.md#0x1_Roles_DESIGNATED_DEALER_ROLE_ID">DESIGNATED_DEALER_ROLE_ID</a>); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">AbortsIfNotTreasuryCompliance</a>{account: creating_account}; <b>include</b> <a href="Roles.md#0x1_Roles_GrantRole">GrantRole</a>{addr: <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(new_account), role_id: <a href="Roles.md#0x1_Roles_DESIGNATED_DEALER_ROLE_ID">DESIGNATED_DEALER_ROLE_ID</a>}; </code></pre> </details><a name="0x1_Roles_new_validator_role"></a>
new_validator_rolePublish a Validator <code><a href="Roles.md#0x1_Roles_RoleId">RoleId</a></code> under <code>new_account</code>. The <code>creating_account</code> must be diem root.
<pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_new_validator_role">new_validator_role</a>(creating_account: &signer, new_account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_new_validator_role">new_validator_role</a>( creating_account: &signer, new_account: &signer ) <b>acquires</b> <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> { <a href="Roles.md#0x1_Roles_assert_diem_root">assert_diem_root</a>(creating_account); <a href="Roles.md#0x1_Roles_grant_role">grant_role</a>(new_account, <a href="Roles.md#0x1_Roles_VALIDATOR_ROLE_ID">VALIDATOR_ROLE_ID</a>); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">AbortsIfNotDiemRoot</a>{account: creating_account}; <b>include</b> <a href="Roles.md#0x1_Roles_GrantRole">GrantRole</a>{addr: <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(new_account), role_id: <a href="Roles.md#0x1_Roles_VALIDATOR_ROLE_ID">VALIDATOR_ROLE_ID</a>}; </code></pre> </details><a name="0x1_Roles_new_validator_operator_role"></a>
new_validator_operator_rolePublish a ValidatorOperator <code><a href="Roles.md#0x1_Roles_RoleId">RoleId</a></code> under <code>new_account</code>. The <code>creating_account</code> must be DiemRoot
<pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_new_validator_operator_role">new_validator_operator_role</a>(creating_account: &signer, new_account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_new_validator_operator_role">new_validator_operator_role</a>( creating_account: &signer, new_account: &signer, ) <b>acquires</b> <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> { <a href="Roles.md#0x1_Roles_assert_diem_root">assert_diem_root</a>(creating_account); <a href="Roles.md#0x1_Roles_grant_role">grant_role</a>(new_account, <a href="Roles.md#0x1_Roles_VALIDATOR_OPERATOR_ROLE_ID">VALIDATOR_OPERATOR_ROLE_ID</a>); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">AbortsIfNotDiemRoot</a>{account: creating_account}; <b>include</b> <a href="Roles.md#0x1_Roles_GrantRole">GrantRole</a>{addr: <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(new_account), role_id: <a href="Roles.md#0x1_Roles_VALIDATOR_OPERATOR_ROLE_ID">VALIDATOR_OPERATOR_ROLE_ID</a>}; </code></pre> </details><a name="0x1_Roles_new_parent_vasp_role"></a>
new_parent_vasp_rolePublish a ParentVASP <code><a href="Roles.md#0x1_Roles_RoleId">RoleId</a></code> under <code>new_account</code>. The <code>creating_account</code> must be TreasuryCompliance
<pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_new_parent_vasp_role">new_parent_vasp_role</a>(creating_account: &signer, new_account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_new_parent_vasp_role">new_parent_vasp_role</a>( creating_account: &signer, new_account: &signer, ) <b>acquires</b> <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> { <a href="Roles.md#0x1_Roles_assert_treasury_compliance">assert_treasury_compliance</a>(creating_account); <a href="Roles.md#0x1_Roles_grant_role">grant_role</a>(new_account, <a href="Roles.md#0x1_Roles_PARENT_VASP_ROLE_ID">PARENT_VASP_ROLE_ID</a>); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">AbortsIfNotTreasuryCompliance</a>{account: creating_account}; <b>include</b> <a href="Roles.md#0x1_Roles_GrantRole">GrantRole</a>{addr: <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(new_account), role_id: <a href="Roles.md#0x1_Roles_PARENT_VASP_ROLE_ID">PARENT_VASP_ROLE_ID</a>}; </code></pre> </details><a name="0x1_Roles_new_child_vasp_role"></a>
new_child_vasp_rolePublish a ChildVASP <code><a href="Roles.md#0x1_Roles_RoleId">RoleId</a></code> under <code>new_account</code>. The <code>creating_account</code> must be a ParentVASP
<pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_new_child_vasp_role">new_child_vasp_role</a>(creating_account: &signer, new_account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_new_child_vasp_role">new_child_vasp_role</a>( creating_account: &signer, new_account: &signer, ) <b>acquires</b> <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> { <a href="Roles.md#0x1_Roles_assert_parent_vasp_role">assert_parent_vasp_role</a>(creating_account); <a href="Roles.md#0x1_Roles_grant_role">grant_role</a>(new_account, <a href="Roles.md#0x1_Roles_CHILD_VASP_ROLE_ID">CHILD_VASP_ROLE_ID</a>); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotParentVasp">AbortsIfNotParentVasp</a>{account: creating_account}; <b>include</b> <a href="Roles.md#0x1_Roles_GrantRole">GrantRole</a>{addr: <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(new_account), role_id: <a href="Roles.md#0x1_Roles_CHILD_VASP_ROLE_ID">CHILD_VASP_ROLE_ID</a>}; </code></pre> </details><a name="0x1_Roles_grant_role"></a>
grant_roleHelper function to grant a role.
<pre><code><b>fun</b> <a href="Roles.md#0x1_Roles_grant_role">grant_role</a>(account: &signer, role_id: u64) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="Roles.md#0x1_Roles_grant_role">grant_role</a>(account: &signer, role_id: u64) { <b>assert</b>(!<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account)), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_already_published">Errors::already_published</a>(<a href="Roles.md#0x1_Roles_EROLE_ID">EROLE_ID</a>)); move_to(account, <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> { role_id }); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>include</b> <a href="Roles.md#0x1_Roles_GrantRole">GrantRole</a>{addr: <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account)}; <a name="0x1_Roles_addr$45"></a> <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); <b>requires</b> role_id == <a href="Roles.md#0x1_Roles_DIEM_ROOT_ROLE_ID">DIEM_ROOT_ROLE_ID</a> ==> addr == <a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>(); <b>requires</b> role_id == <a href="Roles.md#0x1_Roles_TREASURY_COMPLIANCE_ROLE_ID">TREASURY_COMPLIANCE_ROLE_ID</a> ==> addr == <a href="CoreAddresses.md#0x1_CoreAddresses_TREASURY_COMPLIANCE_ADDRESS">CoreAddresses::TREASURY_COMPLIANCE_ADDRESS</a>(); </code></pre><a name="0x1_Roles_GrantRole"></a>
<pre><code><b>schema</b> <a href="Roles.md#0x1_Roles_GrantRole">GrantRole</a> { addr: address; role_id: num; <b>aborts_if</b> <b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; <b>ensures</b> <b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr); <b>ensures</b> <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id == role_id; <b>modifies</b> <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr); } </code></pre> </details><a name="0x1_Roles_has_role"></a>
has_role<a name="0x1_Roles_has_diem_root_role"></a>
has_diem_root_role<a name="0x1_Roles_has_treasury_compliance_role"></a>
has_treasury_compliance_role<a name="0x1_Roles_has_designated_dealer_role"></a>
has_designated_dealer_role<a name="0x1_Roles_has_validator_role"></a>
has_validator_role<a name="0x1_Roles_has_validator_operator_role"></a>
has_validator_operator_role<a name="0x1_Roles_has_parent_VASP_role"></a>
has_parent_VASP_role<a name="0x1_Roles_has_child_VASP_role"></a>
has_child_VASP_role<a name="0x1_Roles_get_role_id"></a>
get_role_id<a name="0x1_Roles_can_hold_balance"></a>
can_hold_balanceReturn true if <code>addr</code> is allowed to receive and send <code><a href="Diem.md#0x1_Diem">Diem</a><T></code> for any T
<pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_can_hold_balance">can_hold_balance</a>(account: &signer): bool </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_can_hold_balance">can_hold_balance</a>(account: &signer): bool <b>acquires</b> <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> { // <a href="VASP.md#0x1_VASP">VASP</a> accounts and designated_dealers can hold balances. // Administrative accounts (`Validator`, `ValidatorOperator`, `TreasuryCompliance`, and // `DiemRoot`) cannot. <a href="Roles.md#0x1_Roles_has_parent_VASP_role">has_parent_VASP_role</a>(account) || <a href="Roles.md#0x1_Roles_has_child_VASP_role">has_child_VASP_role</a>(account) || <a href="Roles.md#0x1_Roles_has_designated_dealer_role">has_designated_dealer_role</a>(account) } </code></pre> </details><a name="0x1_Roles_assert_diem_root"></a>
assert_diem_rootAssert that the account is diem root.
<pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_assert_diem_root">assert_diem_root</a>(account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_assert_diem_root">assert_diem_root</a>(account: &signer) <b>acquires</b> <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> { <a href="CoreAddresses.md#0x1_CoreAddresses_assert_diem_root">CoreAddresses::assert_diem_root</a>(account); <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); <b>assert</b>(<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="Roles.md#0x1_Roles_EROLE_ID">EROLE_ID</a>)); <b>assert</b>(borrow_global<<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id == <a href="Roles.md#0x1_Roles_DIEM_ROOT_ROLE_ID">DIEM_ROOT_ROLE_ID</a>, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_requires_role">Errors::requires_role</a>(<a href="Roles.md#0x1_Roles_EDIEM_ROOT">EDIEM_ROOT</a>)); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>include</b> <a href="CoreAddresses.md#0x1_CoreAddresses_AbortsIfNotDiemRoot">CoreAddresses::AbortsIfNotDiemRoot</a>; <b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">AbortsIfNotDiemRoot</a>; </code></pre> </details><a name="0x1_Roles_assert_treasury_compliance"></a>
assert_treasury_complianceAssert that the account is treasury compliance.
<pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_assert_treasury_compliance">assert_treasury_compliance</a>(account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_assert_treasury_compliance">assert_treasury_compliance</a>(account: &signer) <b>acquires</b> <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> { <a href="CoreAddresses.md#0x1_CoreAddresses_assert_treasury_compliance">CoreAddresses::assert_treasury_compliance</a>(account); <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); <b>assert</b>(<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="Roles.md#0x1_Roles_EROLE_ID">EROLE_ID</a>)); <b>assert</b>( borrow_global<<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id == <a href="Roles.md#0x1_Roles_TREASURY_COMPLIANCE_ROLE_ID">TREASURY_COMPLIANCE_ROLE_ID</a>, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_requires_role">Errors::requires_role</a>(<a href="Roles.md#0x1_Roles_ETREASURY_COMPLIANCE">ETREASURY_COMPLIANCE</a>) ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">AbortsIfNotTreasuryCompliance</a>; </code></pre> </details><a name="0x1_Roles_assert_parent_vasp_role"></a>
assert_parent_vasp_roleAssert that the account has the parent vasp role.
<pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_assert_parent_vasp_role">assert_parent_vasp_role</a>(account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_assert_parent_vasp_role">assert_parent_vasp_role</a>(account: &signer) <b>acquires</b> <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> { <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); <b>assert</b>(<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="Roles.md#0x1_Roles_EROLE_ID">EROLE_ID</a>)); <b>assert</b>( borrow_global<<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id == <a href="Roles.md#0x1_Roles_PARENT_VASP_ROLE_ID">PARENT_VASP_ROLE_ID</a>, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_requires_role">Errors::requires_role</a>(<a href="Roles.md#0x1_Roles_EPARENT_VASP">EPARENT_VASP</a>) ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotParentVasp">AbortsIfNotParentVasp</a>; </code></pre> </details><a name="0x1_Roles_assert_child_vasp_role"></a>
assert_child_vasp_roleAssert that the account has the child vasp role.
<pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_assert_child_vasp_role">assert_child_vasp_role</a>(account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_assert_child_vasp_role">assert_child_vasp_role</a>(account: &signer) <b>acquires</b> <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> { <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); <b>assert</b>(<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="Roles.md#0x1_Roles_EROLE_ID">EROLE_ID</a>)); <b>assert</b>( borrow_global<<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id == <a href="Roles.md#0x1_Roles_CHILD_VASP_ROLE_ID">CHILD_VASP_ROLE_ID</a>, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_requires_role">Errors::requires_role</a>(<a href="Roles.md#0x1_Roles_ECHILD_VASP">ECHILD_VASP</a>) ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotChildVasp">AbortsIfNotChildVasp</a>{account: <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account)}; </code></pre> </details><a name="0x1_Roles_assert_designated_dealer"></a>
assert_designated_dealerAssert that the account has the designated dealer role.
<pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_assert_designated_dealer">assert_designated_dealer</a>(account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_assert_designated_dealer">assert_designated_dealer</a>(account: &signer) <b>acquires</b> <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> { <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); <b>assert</b>(<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="Roles.md#0x1_Roles_EROLE_ID">EROLE_ID</a>)); <b>assert</b>( borrow_global<<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id == <a href="Roles.md#0x1_Roles_DESIGNATED_DEALER_ROLE_ID">DESIGNATED_DEALER_ROLE_ID</a>, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_requires_role">Errors::requires_role</a>(<a href="Roles.md#0x1_Roles_EDESIGNATED_DEALER">EDESIGNATED_DEALER</a>) ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotDesignatedDealer">AbortsIfNotDesignatedDealer</a>; </code></pre> </details><a name="0x1_Roles_assert_validator"></a>
assert_validatorAssert that the account has the validator role.
<pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_assert_validator">assert_validator</a>(validator_account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_assert_validator">assert_validator</a>(validator_account: &signer) <b>acquires</b> <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> { <b>let</b> validator_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(validator_account); <b>assert</b>(<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(validator_addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="Roles.md#0x1_Roles_EROLE_ID">EROLE_ID</a>)); <b>assert</b>( borrow_global<<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(validator_addr).role_id == <a href="Roles.md#0x1_Roles_VALIDATOR_ROLE_ID">VALIDATOR_ROLE_ID</a>, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_requires_role">Errors::requires_role</a>(<a href="Roles.md#0x1_Roles_EVALIDATOR">EVALIDATOR</a>) ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotValidator">AbortsIfNotValidator</a>{validator_addr: <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(validator_account)}; </code></pre> </details><a name="0x1_Roles_assert_validator_operator"></a>
assert_validator_operatorAssert that the account has the validator operator role.
<pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_assert_validator_operator">assert_validator_operator</a>(validator_operator_account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_assert_validator_operator">assert_validator_operator</a>(validator_operator_account: &signer) <b>acquires</b> <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> { <b>let</b> validator_operator_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(validator_operator_account); <b>assert</b>(<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(validator_operator_addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="Roles.md#0x1_Roles_EROLE_ID">EROLE_ID</a>)); <b>assert</b>( borrow_global<<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(validator_operator_addr).role_id == <a href="Roles.md#0x1_Roles_VALIDATOR_OPERATOR_ROLE_ID">VALIDATOR_OPERATOR_ROLE_ID</a>, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_requires_role">Errors::requires_role</a>(<a href="Roles.md#0x1_Roles_EVALIDATOR_OPERATOR">EVALIDATOR_OPERATOR</a>) ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotValidatorOperator">AbortsIfNotValidatorOperator</a>{validator_operator_addr: <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(validator_operator_account)}; </code></pre> </details><a name="0x1_Roles_assert_parent_vasp_or_designated_dealer"></a>
assert_parent_vasp_or_designated_dealerAssert that the account has either the parent vasp or designated dealer role.
<pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_assert_parent_vasp_or_designated_dealer">assert_parent_vasp_or_designated_dealer</a>(account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="Roles.md#0x1_Roles_assert_parent_vasp_or_designated_dealer">assert_parent_vasp_or_designated_dealer</a>(account: &signer) <b>acquires</b> <a href="Roles.md#0x1_Roles_RoleId">RoleId</a> { <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); <b>assert</b>(<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="Roles.md#0x1_Roles_EROLE_ID">EROLE_ID</a>)); <b>let</b> role_id = borrow_global<<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id; <b>assert</b>( role_id == <a href="Roles.md#0x1_Roles_PARENT_VASP_ROLE_ID">PARENT_VASP_ROLE_ID</a> || role_id == <a href="Roles.md#0x1_Roles_DESIGNATED_DEALER_ROLE_ID">DESIGNATED_DEALER_ROLE_ID</a>, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_requires_role">Errors::requires_role</a>(<a href="Roles.md#0x1_Roles_EPARENT_VASP_OR_DESIGNATED_DEALER">EPARENT_VASP_OR_DESIGNATED_DEALER</a>) ); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotParentVaspOrDesignatedDealer">AbortsIfNotParentVaspOrDesignatedDealer</a>; </code></pre> </details><a name="0x1_Roles_assert_parent_vasp_or_child_vasp"></a>
assert_parent_vasp_or_child_vasp<a name="@Module_Specification_1"></a>
<a name="@Persistence_of_Roles_2"></a>
Once an account at an address is granted a role it will remain an account role for all time.
<pre><code><b>invariant</b> <b>update</b> [<b>global</b>] <b>forall</b> addr: address <b>where</b> <b>old</b>(<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr)): <b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr) && <b>old</b>(<b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id) == <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id; </code></pre><a name="@Access_Control_3"></a>
In this section, the conditions from the requirements for access control are systematically applied to the functions in this module. While some of those conditions have already been included in individual function specifications, listing them here again gives additional assurance that that all requirements are covered.
The DiemRoot role is only granted in genesis [A1]. A new <code><a href="Roles.md#0x1_Roles_RoleId">RoleId</a></code> with <code><a href="Roles.md#0x1_Roles_DIEM_ROOT_ROLE_ID">DIEM_ROOT_ROLE_ID</a></code> is only published through <code>grant_diem_root_role</code> which aborts if it is not invoked in genesis.
<pre><code><b>apply</b> <a href="Roles.md#0x1_Roles_ThisRoleIsNotNewlyPublished">ThisRoleIsNotNewlyPublished</a>{this: <a href="Roles.md#0x1_Roles_DIEM_ROOT_ROLE_ID">DIEM_ROOT_ROLE_ID</a>} <b>to</b> * <b>except</b> grant_diem_root_role, grant_role; <b>apply</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotGenesis">DiemTimestamp::AbortsIfNotGenesis</a> <b>to</b> grant_diem_root_role; </code></pre>TreasuryCompliance role is only granted in genesis [A2]. A new <code><a href="Roles.md#0x1_Roles_RoleId">RoleId</a></code> with <code><a href="Roles.md#0x1_Roles_TREASURY_COMPLIANCE_ROLE_ID">TREASURY_COMPLIANCE_ROLE_ID</a></code> is only published through <code>grant_treasury_compliance_role</code> which aborts if it is not invoked in genesis.
<pre><code><b>apply</b> <a href="Roles.md#0x1_Roles_ThisRoleIsNotNewlyPublished">ThisRoleIsNotNewlyPublished</a>{this: <a href="Roles.md#0x1_Roles_TREASURY_COMPLIANCE_ROLE_ID">TREASURY_COMPLIANCE_ROLE_ID</a>} <b>to</b> * <b>except</b> grant_treasury_compliance_role, grant_role; <b>apply</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotGenesis">DiemTimestamp::AbortsIfNotGenesis</a> <b>to</b> grant_treasury_compliance_role; </code></pre>Validator roles are only granted by DiemRoot [A3]. A new <code><a href="Roles.md#0x1_Roles_RoleId">RoleId</a></code> with <code><a href="Roles.md#0x1_Roles_VALIDATOR_ROLE_ID">VALIDATOR_ROLE_ID</a></code> is only published through <code>new_validator_role</code> which aborts if <code>creating_account</code> does not have the DiemRoot role.
<pre><code><b>apply</b> <a href="Roles.md#0x1_Roles_ThisRoleIsNotNewlyPublished">ThisRoleIsNotNewlyPublished</a>{this: <a href="Roles.md#0x1_Roles_VALIDATOR_ROLE_ID">VALIDATOR_ROLE_ID</a>} <b>to</b> * <b>except</b> new_validator_role, grant_role; <b>apply</b> <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">AbortsIfNotDiemRoot</a>{account: creating_account} <b>to</b> new_validator_role; </code></pre>ValidatorOperator roles are only granted by DiemRoot [A4]. A new <code><a href="Roles.md#0x1_Roles_RoleId">RoleId</a></code> with <code><a href="Roles.md#0x1_Roles_VALIDATOR_OPERATOR_ROLE_ID">VALIDATOR_OPERATOR_ROLE_ID</a></code> is only published through <code>new_validator_operator_role</code> which aborts if <code>creating_account</code> does not have the DiemRoot role.
<pre><code><b>apply</b> <a href="Roles.md#0x1_Roles_ThisRoleIsNotNewlyPublished">ThisRoleIsNotNewlyPublished</a>{this: <a href="Roles.md#0x1_Roles_VALIDATOR_OPERATOR_ROLE_ID">VALIDATOR_OPERATOR_ROLE_ID</a>} <b>to</b> * <b>except</b> new_validator_operator_role, grant_role; <b>apply</b> <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">AbortsIfNotDiemRoot</a>{account: creating_account} <b>to</b> new_validator_operator_role; </code></pre>DesignatedDealer roles are only granted by TreasuryCompliance [A5]. A new <code><a href="Roles.md#0x1_Roles_RoleId">RoleId</a></code> with <code><a href="Roles.md#0x1_Roles_DESIGNATED_DEALER_ROLE_ID">DESIGNATED_DEALER_ROLE_ID</a>()</code> is only published through <code>new_designated_dealer_role</code> which aborts if <code>creating_account</code> does not have the TreasuryCompliance role.
<pre><code><b>apply</b> <a href="Roles.md#0x1_Roles_ThisRoleIsNotNewlyPublished">ThisRoleIsNotNewlyPublished</a>{this: <a href="Roles.md#0x1_Roles_DESIGNATED_DEALER_ROLE_ID">DESIGNATED_DEALER_ROLE_ID</a>} <b>to</b> * <b>except</b> new_designated_dealer_role, grant_role; <b>apply</b> <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">AbortsIfNotTreasuryCompliance</a>{account: creating_account} <b>to</b> new_designated_dealer_role; </code></pre>ParentVASP roles are only granted by TreasuryCompliance [A6]. A new <code><a href="Roles.md#0x1_Roles_RoleId">RoleId</a></code> with <code><a href="Roles.md#0x1_Roles_PARENT_VASP_ROLE_ID">PARENT_VASP_ROLE_ID</a>()</code> is only published through <code>new_parent_vasp_role</code> which aborts if <code>creating_account</code> does not have the TreasuryCompliance role.
<pre><code><b>apply</b> <a href="Roles.md#0x1_Roles_ThisRoleIsNotNewlyPublished">ThisRoleIsNotNewlyPublished</a>{this: <a href="Roles.md#0x1_Roles_PARENT_VASP_ROLE_ID">PARENT_VASP_ROLE_ID</a>} <b>to</b> * <b>except</b> new_parent_vasp_role, grant_role; <b>apply</b> <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">AbortsIfNotTreasuryCompliance</a>{account: creating_account} <b>to</b> new_parent_vasp_role; </code></pre>ChildVASP roles are only granted by ParentVASP [A7]. A new <code><a href="Roles.md#0x1_Roles_RoleId">RoleId</a></code> with <code><a href="Roles.md#0x1_Roles_CHILD_VASP_ROLE_ID">CHILD_VASP_ROLE_ID</a></code> is only published through <code>new_child_vasp_role</code> which aborts if <code>creating_account</code> does not have the ParentVASP role.
<pre><code><b>apply</b> <a href="Roles.md#0x1_Roles_ThisRoleIsNotNewlyPublished">ThisRoleIsNotNewlyPublished</a>{this: <a href="Roles.md#0x1_Roles_CHILD_VASP_ROLE_ID">CHILD_VASP_ROLE_ID</a>} <b>to</b> * <b>except</b> new_child_vasp_role, grant_role; <b>apply</b> <a href="Roles.md#0x1_Roles_AbortsIfNotParentVasp">AbortsIfNotParentVasp</a>{account: creating_account} <b>to</b> new_child_vasp_role; </code></pre>The DiemRoot role is globally unique [B1], and is published at DIEM_ROOT_ADDRESS [C1]. In other words, a <code><a href="Roles.md#0x1_Roles_RoleId">RoleId</a></code> with <code><a href="Roles.md#0x1_Roles_DIEM_ROOT_ROLE_ID">DIEM_ROOT_ROLE_ID</a></code> uniquely exists at <code>DIEM_ROOT_ADDRESS</code>.
<pre><code><b>invariant</b> [<b>global</b>, isolated] <b>forall</b> addr: address <b>where</b> <a href="Roles.md#0x1_Roles_spec_has_diem_root_role_addr">spec_has_diem_root_role_addr</a>(addr): addr == <a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>(); <b>invariant</b> [<b>global</b>, isolated] <a href="DiemTimestamp.md#0x1_DiemTimestamp_is_operating">DiemTimestamp::is_operating</a>() ==> <a href="Roles.md#0x1_Roles_spec_has_diem_root_role_addr">spec_has_diem_root_role_addr</a>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()); </code></pre>The TreasuryCompliance role is globally unique [B2], and is published at TREASURY_COMPLIANCE_ADDRESS [C2]. In other words, a <code><a href="Roles.md#0x1_Roles_RoleId">RoleId</a></code> with <code><a href="Roles.md#0x1_Roles_TREASURY_COMPLIANCE_ROLE_ID">TREASURY_COMPLIANCE_ROLE_ID</a></code> uniquely exists at <code>TREASURY_COMPLIANCE_ADDRESS</code>.
<pre><code><b>invariant</b> [<b>global</b>, isolated] <b>forall</b> addr: address <b>where</b> <a href="Roles.md#0x1_Roles_spec_has_treasury_compliance_role_addr">spec_has_treasury_compliance_role_addr</a>(addr): addr == <a href="CoreAddresses.md#0x1_CoreAddresses_TREASURY_COMPLIANCE_ADDRESS">CoreAddresses::TREASURY_COMPLIANCE_ADDRESS</a>(); <b>invariant</b> [<b>global</b>, isolated] <a href="DiemTimestamp.md#0x1_DiemTimestamp_is_operating">DiemTimestamp::is_operating</a>() ==> <a href="Roles.md#0x1_Roles_spec_has_treasury_compliance_role_addr">spec_has_treasury_compliance_role_addr</a>(<a href="CoreAddresses.md#0x1_CoreAddresses_TREASURY_COMPLIANCE_ADDRESS">CoreAddresses::TREASURY_COMPLIANCE_ADDRESS</a>()); </code></pre>DiemRoot cannot have balances [D1].
<pre><code><b>invariant</b> [<b>global</b>, isolated] <b>forall</b> addr: address <b>where</b> <a href="Roles.md#0x1_Roles_spec_has_diem_root_role_addr">spec_has_diem_root_role_addr</a>(addr): !<a href="Roles.md#0x1_Roles_spec_can_hold_balance_addr">spec_can_hold_balance_addr</a>(addr); </code></pre>TreasuryCompliance cannot have balances [D2].
<pre><code><b>invariant</b> [<b>global</b>, isolated] <b>forall</b> addr: address <b>where</b> <a href="Roles.md#0x1_Roles_spec_has_treasury_compliance_role_addr">spec_has_treasury_compliance_role_addr</a>(addr): !<a href="Roles.md#0x1_Roles_spec_can_hold_balance_addr">spec_can_hold_balance_addr</a>(addr); </code></pre>Validator cannot have balances [D3].
<pre><code><b>invariant</b> [<b>global</b>, isolated] <b>forall</b> addr: address <b>where</b> <a href="Roles.md#0x1_Roles_spec_has_validator_role_addr">spec_has_validator_role_addr</a>(addr): !<a href="Roles.md#0x1_Roles_spec_can_hold_balance_addr">spec_can_hold_balance_addr</a>(addr); </code></pre>ValidatorOperator cannot have balances [D4].
<pre><code><b>invariant</b> [<b>global</b>, isolated] <b>forall</b> addr: address <b>where</b> <a href="Roles.md#0x1_Roles_spec_has_validator_operator_role_addr">spec_has_validator_operator_role_addr</a>(addr): !<a href="Roles.md#0x1_Roles_spec_can_hold_balance_addr">spec_can_hold_balance_addr</a>(addr); </code></pre>DesignatedDealer have balances [D5].
<pre><code><b>invariant</b> [<b>global</b>, isolated] <b>forall</b> addr: address <b>where</b> <a href="Roles.md#0x1_Roles_spec_has_designated_dealer_role_addr">spec_has_designated_dealer_role_addr</a>(addr): <a href="Roles.md#0x1_Roles_spec_can_hold_balance_addr">spec_can_hold_balance_addr</a>(addr); </code></pre>ParentVASP have balances [D6].
<pre><code><b>invariant</b> [<b>global</b>, isolated] <b>forall</b> addr: address <b>where</b> <a href="Roles.md#0x1_Roles_spec_has_parent_VASP_role_addr">spec_has_parent_VASP_role_addr</a>(addr): <a href="Roles.md#0x1_Roles_spec_can_hold_balance_addr">spec_can_hold_balance_addr</a>(addr); </code></pre>ChildVASP have balances [D7].
<pre><code><b>invariant</b> [<b>global</b>, isolated] <b>forall</b> addr: address <b>where</b> <a href="Roles.md#0x1_Roles_spec_has_child_VASP_role_addr">spec_has_child_VASP_role_addr</a>(addr): <a href="Roles.md#0x1_Roles_spec_can_hold_balance_addr">spec_can_hold_balance_addr</a>(addr); </code></pre><a name="@Helper_Functions_and_Schemas_4"></a>
<a name="0x1_Roles_spec_get_role_id"></a>
<pre><code><b>define</b> <a href="Roles.md#0x1_Roles_spec_get_role_id">spec_get_role_id</a>(addr: address): u64 { <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id } <a name="0x1_Roles_spec_has_role_id_addr"></a> <b>define</b> <a href="Roles.md#0x1_Roles_spec_has_role_id_addr">spec_has_role_id_addr</a>(addr: address, role_id: u64): bool { <b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr) && <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id == role_id } <a name="0x1_Roles_spec_has_diem_root_role_addr"></a> <b>define</b> <a href="Roles.md#0x1_Roles_spec_has_diem_root_role_addr">spec_has_diem_root_role_addr</a>(addr: address): bool { <a href="Roles.md#0x1_Roles_spec_has_role_id_addr">spec_has_role_id_addr</a>(addr, <a href="Roles.md#0x1_Roles_DIEM_ROOT_ROLE_ID">DIEM_ROOT_ROLE_ID</a>) } <a name="0x1_Roles_spec_has_treasury_compliance_role_addr"></a> <b>define</b> <a href="Roles.md#0x1_Roles_spec_has_treasury_compliance_role_addr">spec_has_treasury_compliance_role_addr</a>(addr: address): bool { <a href="Roles.md#0x1_Roles_spec_has_role_id_addr">spec_has_role_id_addr</a>(addr, <a href="Roles.md#0x1_Roles_TREASURY_COMPLIANCE_ROLE_ID">TREASURY_COMPLIANCE_ROLE_ID</a>) } <a name="0x1_Roles_spec_has_designated_dealer_role_addr"></a> <b>define</b> <a href="Roles.md#0x1_Roles_spec_has_designated_dealer_role_addr">spec_has_designated_dealer_role_addr</a>(addr: address): bool { <a href="Roles.md#0x1_Roles_spec_has_role_id_addr">spec_has_role_id_addr</a>(addr, <a href="Roles.md#0x1_Roles_DESIGNATED_DEALER_ROLE_ID">DESIGNATED_DEALER_ROLE_ID</a>) } <a name="0x1_Roles_spec_has_validator_role_addr"></a> <b>define</b> <a href="Roles.md#0x1_Roles_spec_has_validator_role_addr">spec_has_validator_role_addr</a>(addr: address): bool { <a href="Roles.md#0x1_Roles_spec_has_role_id_addr">spec_has_role_id_addr</a>(addr, <a href="Roles.md#0x1_Roles_VALIDATOR_ROLE_ID">VALIDATOR_ROLE_ID</a>) } <a name="0x1_Roles_spec_has_validator_operator_role_addr"></a> <b>define</b> <a href="Roles.md#0x1_Roles_spec_has_validator_operator_role_addr">spec_has_validator_operator_role_addr</a>(addr: address): bool { <a href="Roles.md#0x1_Roles_spec_has_role_id_addr">spec_has_role_id_addr</a>(addr, <a href="Roles.md#0x1_Roles_VALIDATOR_OPERATOR_ROLE_ID">VALIDATOR_OPERATOR_ROLE_ID</a>) } <a name="0x1_Roles_spec_has_parent_VASP_role_addr"></a> <b>define</b> <a href="Roles.md#0x1_Roles_spec_has_parent_VASP_role_addr">spec_has_parent_VASP_role_addr</a>(addr: address): bool { <a href="Roles.md#0x1_Roles_spec_has_role_id_addr">spec_has_role_id_addr</a>(addr, <a href="Roles.md#0x1_Roles_PARENT_VASP_ROLE_ID">PARENT_VASP_ROLE_ID</a>) } <a name="0x1_Roles_spec_has_child_VASP_role_addr"></a> <b>define</b> <a href="Roles.md#0x1_Roles_spec_has_child_VASP_role_addr">spec_has_child_VASP_role_addr</a>(addr: address): bool { <a href="Roles.md#0x1_Roles_spec_has_role_id_addr">spec_has_role_id_addr</a>(addr, <a href="Roles.md#0x1_Roles_CHILD_VASP_ROLE_ID">CHILD_VASP_ROLE_ID</a>) } <a name="0x1_Roles_spec_can_hold_balance_addr"></a> <b>define</b> <a href="Roles.md#0x1_Roles_spec_can_hold_balance_addr">spec_can_hold_balance_addr</a>(addr: address): bool { <a href="Roles.md#0x1_Roles_spec_has_parent_VASP_role_addr">spec_has_parent_VASP_role_addr</a>(addr) || <a href="Roles.md#0x1_Roles_spec_has_child_VASP_role_addr">spec_has_child_VASP_role_addr</a>(addr) || <a href="Roles.md#0x1_Roles_spec_has_designated_dealer_role_addr">spec_has_designated_dealer_role_addr</a>(addr) } </code></pre><a name="0x1_Roles_ThisRoleIsNotNewlyPublished"></a>
<pre><code><b>schema</b> <a href="Roles.md#0x1_Roles_ThisRoleIsNotNewlyPublished">ThisRoleIsNotNewlyPublished</a> { this: u64; <b>ensures</b> <b>forall</b> addr: address <b>where</b> <b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr) && <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id == this: <b>old</b>(<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr)) && <b>old</b>(<b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id) == this; } </code></pre><a name="0x1_Roles_AbortsIfNotDiemRoot"></a>
<pre><code><b>schema</b> <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">AbortsIfNotDiemRoot</a> { account: signer; <b>include</b> <a href="CoreAddresses.md#0x1_CoreAddresses_AbortsIfNotDiemRoot">CoreAddresses::AbortsIfNotDiemRoot</a>; <a name="0x1_Roles_addr$37"></a> <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); <b>aborts_if</b> !<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <b>aborts_if</b> <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id != <a href="Roles.md#0x1_Roles_DIEM_ROOT_ROLE_ID">DIEM_ROOT_ROLE_ID</a> <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_REQUIRES_ROLE">Errors::REQUIRES_ROLE</a>; } </code></pre><a name="0x1_Roles_AbortsIfNotTreasuryCompliance"></a>
<pre><code><b>schema</b> <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">AbortsIfNotTreasuryCompliance</a> { account: signer; <b>include</b> <a href="CoreAddresses.md#0x1_CoreAddresses_AbortsIfNotTreasuryCompliance">CoreAddresses::AbortsIfNotTreasuryCompliance</a>; <a name="0x1_Roles_addr$38"></a> <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); <b>aborts_if</b> !<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <b>aborts_if</b> <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id != <a href="Roles.md#0x1_Roles_TREASURY_COMPLIANCE_ROLE_ID">TREASURY_COMPLIANCE_ROLE_ID</a> <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_REQUIRES_ROLE">Errors::REQUIRES_ROLE</a>; } </code></pre><a name="0x1_Roles_AbortsIfNotParentVasp"></a>
<pre><code><b>schema</b> <a href="Roles.md#0x1_Roles_AbortsIfNotParentVasp">AbortsIfNotParentVasp</a> { account: signer; <a name="0x1_Roles_addr$39"></a> <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); <b>aborts_if</b> !<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <b>aborts_if</b> <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id != <a href="Roles.md#0x1_Roles_PARENT_VASP_ROLE_ID">PARENT_VASP_ROLE_ID</a> <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_REQUIRES_ROLE">Errors::REQUIRES_ROLE</a>; } </code></pre><a name="0x1_Roles_AbortsIfNotChildVasp"></a>
<pre><code><b>schema</b> <a href="Roles.md#0x1_Roles_AbortsIfNotChildVasp">AbortsIfNotChildVasp</a> { account: address; <b>aborts_if</b> !<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(account) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <b>aborts_if</b> <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(account).role_id != <a href="Roles.md#0x1_Roles_CHILD_VASP_ROLE_ID">CHILD_VASP_ROLE_ID</a> <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_REQUIRES_ROLE">Errors::REQUIRES_ROLE</a>; } </code></pre><a name="0x1_Roles_AbortsIfNotDesignatedDealer"></a>
<pre><code><b>schema</b> <a href="Roles.md#0x1_Roles_AbortsIfNotDesignatedDealer">AbortsIfNotDesignatedDealer</a> { account: signer; <a name="0x1_Roles_addr$40"></a> <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); <b>aborts_if</b> !<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <b>aborts_if</b> <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id != <a href="Roles.md#0x1_Roles_DESIGNATED_DEALER_ROLE_ID">DESIGNATED_DEALER_ROLE_ID</a> <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_REQUIRES_ROLE">Errors::REQUIRES_ROLE</a>; } </code></pre><a name="0x1_Roles_AbortsIfNotParentVaspOrDesignatedDealer"></a>
<pre><code><b>schema</b> <a href="Roles.md#0x1_Roles_AbortsIfNotParentVaspOrDesignatedDealer">AbortsIfNotParentVaspOrDesignatedDealer</a> { account: signer; <a name="0x1_Roles_addr$41"></a> <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); <b>aborts_if</b> !<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <a name="0x1_Roles_role_id$42"></a> <b>let</b> role_id = <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id; <b>aborts_if</b> role_id != <a href="Roles.md#0x1_Roles_PARENT_VASP_ROLE_ID">PARENT_VASP_ROLE_ID</a> && role_id != <a href="Roles.md#0x1_Roles_DESIGNATED_DEALER_ROLE_ID">DESIGNATED_DEALER_ROLE_ID</a> <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_REQUIRES_ROLE">Errors::REQUIRES_ROLE</a>; } </code></pre><a name="0x1_Roles_AbortsIfNotParentVaspOrChildVasp"></a>
<pre><code><b>schema</b> <a href="Roles.md#0x1_Roles_AbortsIfNotParentVaspOrChildVasp">AbortsIfNotParentVaspOrChildVasp</a> { account: signer; <a name="0x1_Roles_addr$43"></a> <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); <b>aborts_if</b> !<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <a name="0x1_Roles_role_id$44"></a> <b>let</b> role_id = <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(addr).role_id; <b>aborts_if</b> role_id != <a href="Roles.md#0x1_Roles_PARENT_VASP_ROLE_ID">PARENT_VASP_ROLE_ID</a> && role_id != <a href="Roles.md#0x1_Roles_CHILD_VASP_ROLE_ID">CHILD_VASP_ROLE_ID</a> <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_REQUIRES_ROLE">Errors::REQUIRES_ROLE</a>; } </code></pre><a name="0x1_Roles_AbortsIfNotValidator"></a>
<pre><code><b>schema</b> <a href="Roles.md#0x1_Roles_AbortsIfNotValidator">AbortsIfNotValidator</a> { validator_addr: address; <b>aborts_if</b> !<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(validator_addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <b>aborts_if</b> <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(validator_addr).role_id != <a href="Roles.md#0x1_Roles_VALIDATOR_ROLE_ID">VALIDATOR_ROLE_ID</a> <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_REQUIRES_ROLE">Errors::REQUIRES_ROLE</a>; } </code></pre><a name="0x1_Roles_AbortsIfNotValidatorOperator"></a>
<pre><code><b>schema</b> <a href="Roles.md#0x1_Roles_AbortsIfNotValidatorOperator">AbortsIfNotValidatorOperator</a> { validator_operator_addr: address; <b>aborts_if</b> !<b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(validator_operator_addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <b>aborts_if</b> <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">RoleId</a>>(validator_operator_addr).role_id != <a href="Roles.md#0x1_Roles_VALIDATOR_OPERATOR_ROLE_ID">VALIDATOR_OPERATOR_ROLE_ID</a> <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_REQUIRES_ROLE">Errors::REQUIRES_ROLE</a>; } </code></pre>