language/diem-framework/modules/doc/DiemAccount.md
<a name="0x1_DiemAccount"></a>
0x1::DiemAccountThe <code><a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a></code> module manages accounts. It defines the <code><a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a></code> resource and numerous auxiliary data structures. It also defines the prolog and epilog that run before and after every transaction.
DiemAccountBalanceWithdrawCapabilityKeyRotationCapabilityAccountOperationsCapabilityDiemWriteSetManagerSentPaymentEventReceivedPaymentEventAdminTransactionEventCreateAccountEventinitializehas_published_account_limitsshould_track_limits_for_accountdeposittiered_mintcancel_burnwithdraw_from_balancewithdraw_from
preburnextract_withdraw_capabilityrestore_withdraw_capabilitypay_frompay_by_signersrotate_authentication_key
extract_key_rotation_capabilityrestore_key_rotation_capabilityadd_currencies_for_accountmake_accountcreate_authentication_keycreate_diem_root_accountcreate_treasury_compliance_accountcreate_designated_dealercreate_parent_vasp_accountcreate_child_vasp_accountcreate_signerpublish_crsnbalance_forbalanceadd_currencyadd_currency_for_test
accepts_currencysequence_number_for_accountsequence_numberauthentication_keydelegated_key_rotation_capabilitydelegated_withdraw_capabilitywithdraw_capability_addresskey_rotation_capability_addressexists_atmodule_prologuescript_prologuewriteset_prologuemulti_agent_script_prologueprologue_commonepilogueepilogue_commonwriteset_epiloguecreate_validator_accountcreate_validator_operator_account<a name="0x1_DiemAccount_DiemAccount"></a>
DiemAccountAn <code>address</code> is a Diem Account iff it has a published DiemAccount resource.
<pre><code><b>struct</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a> has key </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>authentication_key: vector<u8></code> </dt> <dd> The current authentication key. This can be different from the key used to create the account </dd> <dt> <code>withdraw_capability: <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_Option">Option::Option</a><<a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">DiemAccount::WithdrawCapability</a>></code> </dt> <dd> A <code>withdraw_capability</code> allows whoever holds this capability to withdraw from the account. At the time of account creation this capability is stored in this option. It can later be removed by <code>extract_withdraw_capability</code> and also restored via <code>restore_withdraw_capability</code>. </dd> <dt> <code>key_rotation_capability: <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_Option">Option::Option</a><<a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">DiemAccount::KeyRotationCapability</a>></code> </dt> <dd> A <code>key_rotation_capability</code> allows whoever holds this capability the ability to rotate the authentication key for the account. At the time of account creation this capability is stored in this option. It can later be "extracted" from this field via <code>extract_key_rotation_capability</code>, and can also be restored via <code>restore_key_rotation_capability</code>. </dd> <dt> <code>received_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_EventHandle">Event::EventHandle</a><<a href="DiemAccount.md#0x1_DiemAccount_ReceivedPaymentEvent">DiemAccount::ReceivedPaymentEvent</a>></code> </dt> <dd> Event handle to which ReceivePaymentEvents are emitted when payments are received. </dd> <dt> <code>sent_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_EventHandle">Event::EventHandle</a><<a href="DiemAccount.md#0x1_DiemAccount_SentPaymentEvent">DiemAccount::SentPaymentEvent</a>></code> </dt> <dd> Event handle to which SentPaymentEvents are emitted when payments are sent. </dd> <dt> <code>sequence_number: u64</code> </dt> <dd> The current sequence number of the account. Incremented by one each time a transaction is submitted by this account. </dd> </dl> </details><a name="0x1_DiemAccount_Balance"></a>
BalanceA resource that holds the total value of currency of type <code>Token</code> currently held by the account.
<pre><code><b>struct</b> <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token> has key </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>coin: <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><Token></code> </dt> <dd> Stores the value of the balance in its balance field. A coin has a <code>value</code> field. The amount of money in the balance is changed by modifying this field. </dd> </dl> </details><a name="0x1_DiemAccount_WithdrawCapability"></a>
WithdrawCapabilityThe holder of WithdrawCapability for account_address can withdraw Diem from account_address/DiemAccount/balance. There is at most one WithdrawCapability in existence for a given address.
<pre><code><b>struct</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a> has store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>account_address: address</code> </dt> <dd> Address that WithdrawCapability was associated with when it was created. This field does not change. </dd> </dl> </details><a name="0x1_DiemAccount_KeyRotationCapability"></a>
KeyRotationCapabilityThe holder of KeyRotationCapability for account_address can rotate the authentication key for account_address (i.e., write to account_address/DiemAccount/authentication_key). There is at most one KeyRotationCapability in existence for a given address.
<pre><code><b>struct</b> <a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">KeyRotationCapability</a> has store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>account_address: address</code> </dt> <dd> Address that KeyRotationCapability was associated with when it was created. This field does not change. </dd> </dl> </details><a name="0x1_DiemAccount_AccountOperationsCapability"></a>
AccountOperationsCapabilityA wrapper around an <code>AccountLimitMutationCapability</code> which is used to check for account limits and to record freeze/unfreeze events.
<pre><code><b>struct</b> <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> has key </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>limits_cap: <a href="AccountLimits.md#0x1_AccountLimits_AccountLimitMutationCapability">AccountLimits::AccountLimitMutationCapability</a></code> </dt> <dd> </dd> <dt> <code>creation_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_EventHandle">Event::EventHandle</a><<a href="DiemAccount.md#0x1_DiemAccount_CreateAccountEvent">DiemAccount::CreateAccountEvent</a>></code> </dt> <dd> </dd> </dl> </details><a name="0x1_DiemAccount_DiemWriteSetManager"></a>
DiemWriteSetManagerA resource that holds the event handle for all the past WriteSet transactions that have been committed on chain.
<pre><code><b>struct</b> <a href="DiemAccount.md#0x1_DiemAccount_DiemWriteSetManager">DiemWriteSetManager</a> has key </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>upgrade_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_EventHandle">Event::EventHandle</a><<a href="DiemAccount.md#0x1_DiemAccount_AdminTransactionEvent">DiemAccount::AdminTransactionEvent</a>></code> </dt> <dd> </dd> </dl> </details><a name="0x1_DiemAccount_SentPaymentEvent"></a>
SentPaymentEventMessage for sent events
<pre><code><b>struct</b> <a href="DiemAccount.md#0x1_DiemAccount_SentPaymentEvent">SentPaymentEvent</a> has drop, store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>amount: u64</code> </dt> <dd> The amount of Diem<Token> sent </dd> <dt> <code>currency_code: vector<u8></code> </dt> <dd> The code symbol for the currency that was sent </dd> <dt> <code>payee: address</code> </dt> <dd> The address that was paid </dd> <dt> <code>metadata: vector<u8></code> </dt> <dd> Metadata associated with the payment </dd> </dl> </details><a name="0x1_DiemAccount_ReceivedPaymentEvent"></a>
ReceivedPaymentEventMessage for received events
<pre><code><b>struct</b> <a href="DiemAccount.md#0x1_DiemAccount_ReceivedPaymentEvent">ReceivedPaymentEvent</a> has drop, store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>amount: u64</code> </dt> <dd> The amount of Diem<Token> received </dd> <dt> <code>currency_code: vector<u8></code> </dt> <dd> The code symbol for the currency that was received </dd> <dt> <code>payer: address</code> </dt> <dd> The address that sent the coin </dd> <dt> <code>metadata: vector<u8></code> </dt> <dd> Metadata associated with the payment </dd> </dl> </details><a name="0x1_DiemAccount_AdminTransactionEvent"></a>
AdminTransactionEventMessage for committed WriteSet transaction.
<pre><code><b>struct</b> <a href="DiemAccount.md#0x1_DiemAccount_AdminTransactionEvent">AdminTransactionEvent</a> has drop, store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>committed_timestamp_secs: u64</code> </dt> <dd> </dd> </dl> </details><a name="0x1_DiemAccount_CreateAccountEvent"></a>
CreateAccountEventMessage for creation of a new account
<pre><code><b>struct</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateAccountEvent">CreateAccountEvent</a> has drop, store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>created: address</code> </dt> <dd> Address of the created account </dd> <dt> <code>role_id: u64</code> </dt> <dd> Role of the created account </dd> </dl> </details><a name="@Constants_0"></a>
<a name="0x1_DiemAccount_MAX_U64"></a>
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_MAX_U64">MAX_U64</a>: u128 = 18446744073709551615; </code></pre><a name="0x1_DiemAccount_EACCOUNT"></a>
The <code><a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a></code> resource is not in the required state
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_EACCOUNT">EACCOUNT</a>: u64 = 0; </code></pre><a name="0x1_DiemAccount_EACCOUNT_OPERATIONS_CAPABILITY"></a>
The <code><a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a></code> was not in the required state
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_EACCOUNT_OPERATIONS_CAPABILITY">EACCOUNT_OPERATIONS_CAPABILITY</a>: u64 = 22; </code></pre><a name="0x1_DiemAccount_EADD_EXISTING_CURRENCY"></a>
Tried to add a balance in a currency that this account already has
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_EADD_EXISTING_CURRENCY">EADD_EXISTING_CURRENCY</a>: u64 = 15; </code></pre><a name="0x1_DiemAccount_ECANNOT_CREATE_AT_CORE_CODE"></a>
An account cannot be created at the reserved core code address of 0x1
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_ECANNOT_CREATE_AT_CORE_CODE">ECANNOT_CREATE_AT_CORE_CODE</a>: u64 = 24; </code></pre><a name="0x1_DiemAccount_ECANNOT_CREATE_AT_VM_RESERVED"></a>
An account cannot be created at the reserved VM address of 0x0
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_ECANNOT_CREATE_AT_VM_RESERVED">ECANNOT_CREATE_AT_VM_RESERVED</a>: u64 = 10; </code></pre><a name="0x1_DiemAccount_ECOIN_DEPOSIT_IS_ZERO"></a>
Tried to deposit a coin whose value was zero
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_ECOIN_DEPOSIT_IS_ZERO">ECOIN_DEPOSIT_IS_ZERO</a>: u64 = 2; </code></pre><a name="0x1_DiemAccount_EDEPOSIT_EXCEEDS_LIMITS"></a>
Tried to deposit funds that would have surpassed the account's limits
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_EDEPOSIT_EXCEEDS_LIMITS">EDEPOSIT_EXCEEDS_LIMITS</a>: u64 = 3; </code></pre><a name="0x1_DiemAccount_EGAS"></a>
An invalid amount of gas units was provided for execution of the transaction
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_EGAS">EGAS</a>: u64 = 20; </code></pre><a name="0x1_DiemAccount_EINSUFFICIENT_BALANCE"></a>
The account does not hold a large enough balance in the specified currency
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_EINSUFFICIENT_BALANCE">EINSUFFICIENT_BALANCE</a>: u64 = 5; </code></pre><a name="0x1_DiemAccount_EKEY_ROTATION_CAPABILITY_ALREADY_EXTRACTED"></a>
The <code><a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">KeyRotationCapability</a></code> for this account has already been extracted
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_EKEY_ROTATION_CAPABILITY_ALREADY_EXTRACTED">EKEY_ROTATION_CAPABILITY_ALREADY_EXTRACTED</a>: u64 = 9; </code></pre><a name="0x1_DiemAccount_EMALFORMED_AUTHENTICATION_KEY"></a>
The provided authentication had an invalid length
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_EMALFORMED_AUTHENTICATION_KEY">EMALFORMED_AUTHENTICATION_KEY</a>: u64 = 8; </code></pre><a name="0x1_DiemAccount_EPAYEE_CANT_ACCEPT_CURRENCY_TYPE"></a>
Attempted to send funds in a currency that the receiving account does not hold. e.g., <code><a href="Diem.md#0x1_Diem">Diem</a><<a href="XDX.md#0x1_XDX">XDX</a>></code> to an account that exists, but does not have a <code><a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><<a href="XDX.md#0x1_XDX">XDX</a>></code> resource
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_EPAYEE_CANT_ACCEPT_CURRENCY_TYPE">EPAYEE_CANT_ACCEPT_CURRENCY_TYPE</a>: u64 = 18; </code></pre><a name="0x1_DiemAccount_EPAYEE_DOES_NOT_EXIST"></a>
Attempted to send funds to an account that does not exist
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_EPAYEE_DOES_NOT_EXIST">EPAYEE_DOES_NOT_EXIST</a>: u64 = 17; </code></pre><a name="0x1_DiemAccount_EPAYER_DOESNT_HOLD_CURRENCY"></a>
Tried to withdraw funds in a currency that the account does hold
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_EPAYER_DOESNT_HOLD_CURRENCY">EPAYER_DOESNT_HOLD_CURRENCY</a>: u64 = 19; </code></pre><a name="0x1_DiemAccount_EROLE_CANT_STORE_BALANCE"></a>
Tried to create a balance for an account whose role does not allow holding balances
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_EROLE_CANT_STORE_BALANCE">EROLE_CANT_STORE_BALANCE</a>: u64 = 4; </code></pre><a name="0x1_DiemAccount_EWITHDRAWAL_EXCEEDS_LIMITS"></a>
The withdrawal of funds would have exceeded the the account's limits
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_EWITHDRAWAL_EXCEEDS_LIMITS">EWITHDRAWAL_EXCEEDS_LIMITS</a>: u64 = 6; </code></pre><a name="0x1_DiemAccount_EWITHDRAW_CAPABILITY_ALREADY_EXTRACTED"></a>
The <code><a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a></code> for this account has already been extracted
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_EWITHDRAW_CAPABILITY_ALREADY_EXTRACTED">EWITHDRAW_CAPABILITY_ALREADY_EXTRACTED</a>: u64 = 7; </code></pre><a name="0x1_DiemAccount_EWITHDRAW_CAPABILITY_NOT_EXTRACTED"></a>
The <code><a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a></code> for this account is not extracted
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_EWITHDRAW_CAPABILITY_NOT_EXTRACTED">EWITHDRAW_CAPABILITY_NOT_EXTRACTED</a>: u64 = 11; </code></pre><a name="0x1_DiemAccount_EWRITESET_MANAGER"></a>
The <code><a href="DiemAccount.md#0x1_DiemAccount_DiemWriteSetManager">DiemWriteSetManager</a></code> was not in the required state
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_EWRITESET_MANAGER">EWRITESET_MANAGER</a>: u64 = 23; </code></pre><a name="0x1_DiemAccount_PROLOGUE_EACCOUNT_DNE"></a>
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_EACCOUNT_DNE">PROLOGUE_EACCOUNT_DNE</a>: u64 = 1004; </code></pre><a name="0x1_DiemAccount_PROLOGUE_EACCOUNT_FROZEN"></a>
Prologue errors. These are separated out from the other errors in this module since they are mapped separately to major VM statuses, and are important to the semantics of the system.
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_EACCOUNT_FROZEN">PROLOGUE_EACCOUNT_FROZEN</a>: u64 = 1000; </code></pre><a name="0x1_DiemAccount_PROLOGUE_EBAD_CHAIN_ID"></a>
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_EBAD_CHAIN_ID">PROLOGUE_EBAD_CHAIN_ID</a>: u64 = 1007; </code></pre><a name="0x1_DiemAccount_PROLOGUE_EBAD_TRANSACTION_FEE_CURRENCY"></a>
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_EBAD_TRANSACTION_FEE_CURRENCY">PROLOGUE_EBAD_TRANSACTION_FEE_CURRENCY</a>: u64 = 1012; </code></pre><a name="0x1_DiemAccount_PROLOGUE_ECANT_PAY_GAS_DEPOSIT"></a>
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_ECANT_PAY_GAS_DEPOSIT">PROLOGUE_ECANT_PAY_GAS_DEPOSIT</a>: u64 = 1005; </code></pre><a name="0x1_DiemAccount_PROLOGUE_EINVALID_ACCOUNT_AUTH_KEY"></a>
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_EINVALID_ACCOUNT_AUTH_KEY">PROLOGUE_EINVALID_ACCOUNT_AUTH_KEY</a>: u64 = 1001; </code></pre><a name="0x1_DiemAccount_PROLOGUE_EINVALID_WRITESET_SENDER"></a>
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_EINVALID_WRITESET_SENDER">PROLOGUE_EINVALID_WRITESET_SENDER</a>: u64 = 1010; </code></pre><a name="0x1_DiemAccount_PROLOGUE_EMODULE_NOT_ALLOWED"></a>
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_EMODULE_NOT_ALLOWED">PROLOGUE_EMODULE_NOT_ALLOWED</a>: u64 = 1009; </code></pre><a name="0x1_DiemAccount_PROLOGUE_ESCRIPT_NOT_ALLOWED"></a>
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_ESCRIPT_NOT_ALLOWED">PROLOGUE_ESCRIPT_NOT_ALLOWED</a>: u64 = 1008; </code></pre><a name="0x1_DiemAccount_PROLOGUE_ESECONDARY_KEYS_ADDRESSES_COUNT_MISMATCH"></a>
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_ESECONDARY_KEYS_ADDRESSES_COUNT_MISMATCH">PROLOGUE_ESECONDARY_KEYS_ADDRESSES_COUNT_MISMATCH</a>: u64 = 1013; </code></pre><a name="0x1_DiemAccount_PROLOGUE_ESEQUENCE_NUMBER_TOO_BIG"></a>
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_ESEQUENCE_NUMBER_TOO_BIG">PROLOGUE_ESEQUENCE_NUMBER_TOO_BIG</a>: u64 = 1011; </code></pre><a name="0x1_DiemAccount_PROLOGUE_ESEQUENCE_NUMBER_TOO_NEW"></a>
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_ESEQUENCE_NUMBER_TOO_NEW">PROLOGUE_ESEQUENCE_NUMBER_TOO_NEW</a>: u64 = 1003; </code></pre><a name="0x1_DiemAccount_PROLOGUE_ESEQUENCE_NUMBER_TOO_OLD"></a>
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_ESEQUENCE_NUMBER_TOO_OLD">PROLOGUE_ESEQUENCE_NUMBER_TOO_OLD</a>: u64 = 1002; </code></pre><a name="0x1_DiemAccount_PROLOGUE_ESEQ_NONCE_INVALID"></a>
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_ESEQ_NONCE_INVALID">PROLOGUE_ESEQ_NONCE_INVALID</a>: u64 = 1014; </code></pre><a name="0x1_DiemAccount_PROLOGUE_ETRANSACTION_EXPIRED"></a>
<pre><code><b>const</b> <a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_ETRANSACTION_EXPIRED">PROLOGUE_ETRANSACTION_EXPIRED</a>: u64 = 1006; </code></pre><a name="0x1_DiemAccount_initialize"></a>
initializeInitialize this module. This is only callable from genesis.
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_initialize">initialize</a>(dr_account: &signer, dummy_auth_key_prefix: vector<u8>) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_initialize">initialize</a>( dr_account: &signer, dummy_auth_key_prefix: vector<u8>, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_genesis">DiemTimestamp::assert_genesis</a>(); // Operational constraint, not a privilege constraint. <a href="CoreAddresses.md#0x1_CoreAddresses_assert_diem_root">CoreAddresses::assert_diem_root</a>(dr_account); <a href="DiemAccount.md#0x1_DiemAccount_create_diem_root_account">create_diem_root_account</a>( <b>copy</b> dummy_auth_key_prefix, ); <a href="DiemAccount.md#0x1_DiemAccount_create_treasury_compliance_account">create_treasury_compliance_account</a>( dr_account, <b>copy</b> dummy_auth_key_prefix, ); } </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>{account: dr_account}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateDiemRootAccountAbortsIf">CreateDiemRootAccountAbortsIf</a>{auth_key_prefix: dummy_auth_key_prefix}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateTreasuryComplianceAccountAbortsIf">CreateTreasuryComplianceAccountAbortsIf</a>{auth_key_prefix: dummy_auth_key_prefix}; <b>aborts_if</b> <b>exists</b><<a href="AccountFreezing.md#0x1_AccountFreezing_FreezingBit">AccountFreezing::FreezingBit</a>>(@TreasuryCompliance) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateDiemRootAccountModifies">CreateDiemRootAccountModifies</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateDiemRootAccountEnsures">CreateDiemRootAccountEnsures</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateTreasuryComplianceAccountModifies">CreateTreasuryComplianceAccountModifies</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateTreasuryComplianceAccountEnsures">CreateTreasuryComplianceAccountEnsures</a>; </code></pre> </details><a name="0x1_DiemAccount_has_published_account_limits"></a>
has_published_account_limitsReturn <code><b>true</b></code> if <code>addr</code> has already published account limits for <code>Token</code>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_has_published_account_limits">has_published_account_limits</a><Token>(addr: address): bool </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_has_published_account_limits">has_published_account_limits</a><Token>(addr: address): bool { <b>if</b> (<a href="VASP.md#0x1_VASP_is_vasp">VASP::is_vasp</a>(addr)) { <a href="VASP.md#0x1_VASP_has_account_limits">VASP::has_account_limits</a><Token>(addr) } <b>else</b> { <a href="AccountLimits.md#0x1_AccountLimits_has_window_published">AccountLimits::has_window_published</a><Token>(addr) } } </code></pre> </details><a name="0x1_DiemAccount_should_track_limits_for_account"></a>
should_track_limits_for_accountReturns whether we should track and record limits for the <code>payer</code> or <code>payee</code> account. Depending on the <code>is_withdrawal</code> flag passed in we determine whether the <code>payer</code> or <code>payee</code> account is being queried. <code><a href="VASP.md#0x1_VASP">VASP</a>->any</code> and <code>any-><a href="VASP.md#0x1_VASP">VASP</a></code> transfers are tracked in the VASP.
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_should_track_limits_for_account">should_track_limits_for_account</a><Token>(payer: address, payee: address, is_withdrawal: bool): bool </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_should_track_limits_for_account">should_track_limits_for_account</a><Token>( payer: address, payee: address, is_withdrawal: bool ): bool { <b>if</b> (is_withdrawal) { <a href="DiemAccount.md#0x1_DiemAccount_has_published_account_limits">has_published_account_limits</a><Token>(payer) && <a href="VASP.md#0x1_VASP_is_vasp">VASP::is_vasp</a>(payer) && !<a href="VASP.md#0x1_VASP_is_same_vasp">VASP::is_same_vasp</a>(payer, payee) } <b>else</b> { <a href="DiemAccount.md#0x1_DiemAccount_has_published_account_limits">has_published_account_limits</a><Token>(payee) && <a href="VASP.md#0x1_VASP_is_vasp">VASP::is_vasp</a>(payee) && !<a href="VASP.md#0x1_VASP_is_same_vasp">VASP::is_same_vasp</a>(payee, payer) } } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>aborts_if</b> <b>false</b>; <b>ensures</b> result == <a href="DiemAccount.md#0x1_DiemAccount_spec_should_track_limits_for_account">spec_should_track_limits_for_account</a><Token>(payer, payee, is_withdrawal); </code></pre><a name="0x1_DiemAccount_spec_should_track_limits_for_account"></a>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_should_track_limits_for_account">spec_should_track_limits_for_account</a><Token>( payer: address, payee: address, is_withdrawal: bool ): bool { <b>if</b> (is_withdrawal) { <a href="DiemAccount.md#0x1_DiemAccount_spec_has_published_account_limits">spec_has_published_account_limits</a><Token>(payer) && <a href="VASP.md#0x1_VASP_is_vasp">VASP::is_vasp</a>(payer) && !<a href="VASP.md#0x1_VASP_spec_is_same_vasp">VASP::spec_is_same_vasp</a>(payer, payee) } <b>else</b> { <a href="DiemAccount.md#0x1_DiemAccount_spec_has_published_account_limits">spec_has_published_account_limits</a><Token>(payee) && <a href="VASP.md#0x1_VASP_is_vasp">VASP::is_vasp</a>(payee) && !<a href="VASP.md#0x1_VASP_spec_is_same_vasp">VASP::spec_is_same_vasp</a>(payee, payer) } } </code></pre> </details><a name="0x1_DiemAccount_deposit"></a>
depositRecord a payment of <code>to_deposit</code> from <code>payer</code> to <code>payee</code> with the attached <code>metadata</code>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_deposit">deposit</a><Token>(payer: address, payee: address, to_deposit: <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><Token>, metadata: vector<u8>, metadata_signature: vector<u8>, dual_attestation: bool) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_deposit">deposit</a><Token>( payer: address, payee: address, to_deposit: <a href="Diem.md#0x1_Diem">Diem</a><Token>, metadata: vector<u8>, metadata_signature: vector<u8>, dual_attestation: bool, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>, <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a>, <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_operating">DiemTimestamp::assert_operating</a>(); <a href="AccountFreezing.md#0x1_AccountFreezing_assert_not_frozen">AccountFreezing::assert_not_frozen</a>(payee); // Check that the `to_deposit` coin is non-zero <b>let</b> deposit_value = <a href="Diem.md#0x1_Diem_value">Diem::value</a>(&to_deposit); <b>assert</b>(deposit_value > 0, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemAccount.md#0x1_DiemAccount_ECOIN_DEPOSIT_IS_ZERO">ECOIN_DEPOSIT_IS_ZERO</a>)); // Check that an account <b>exists</b> at `payee` <b>assert</b>(<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(payee), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EPAYEE_DOES_NOT_EXIST">EPAYEE_DOES_NOT_EXIST</a>)); // Check that `payee` can accept payments in `Token` <b>assert</b>( <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payee), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemAccount.md#0x1_DiemAccount_EPAYEE_CANT_ACCEPT_CURRENCY_TYPE">EPAYEE_CANT_ACCEPT_CURRENCY_TYPE</a>) ); <b>if</b> (dual_attestation) { // Check that the payment complies <b>with</b> dual attestation rules <a href="DualAttestation.md#0x1_DualAttestation_assert_payment_ok">DualAttestation::assert_payment_ok</a><Token>( payer, payee, deposit_value, <b>copy</b> metadata, metadata_signature ); }; // Ensure that this deposit is compliant <b>with</b> the account limits on // this account. <b>if</b> (<a href="DiemAccount.md#0x1_DiemAccount_should_track_limits_for_account">should_track_limits_for_account</a><Token>(payer, payee, <b>false</b>)) { <b>assert</b>( <a href="AccountLimits.md#0x1_AccountLimits_update_deposit_limits">AccountLimits::update_deposit_limits</a><Token>( deposit_value, <a href="VASP.md#0x1_VASP_parent_address">VASP::parent_address</a>(payee), &borrow_global<<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot).limits_cap ), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="DiemAccount.md#0x1_DiemAccount_EDEPOSIT_EXCEEDS_LIMITS">EDEPOSIT_EXCEEDS_LIMITS</a>) ) }; // Deposit the `to_deposit` coin <a href="Diem.md#0x1_Diem_deposit">Diem::deposit</a>(&<b>mut</b> borrow_global_mut<<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payee).coin, to_deposit); // Log a received event <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_emit_event">Event::emit_event</a><<a href="DiemAccount.md#0x1_DiemAccount_ReceivedPaymentEvent">ReceivedPaymentEvent</a>>( &<b>mut</b> borrow_global_mut<<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee).received_events, <a href="DiemAccount.md#0x1_DiemAccount_ReceivedPaymentEvent">ReceivedPaymentEvent</a> { amount: deposit_value, currency_code: <a href="Diem.md#0x1_Diem_currency_code">Diem::currency_code</a><Token>(), payer, metadata } ); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payee); <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee); <b>modifies</b> <b>global</b><<a href="AccountLimits.md#0x1_AccountLimits_Window">AccountLimits::Window</a><Token>>(<a href="VASP.md#0x1_VASP_spec_parent_address">VASP::spec_parent_address</a>(payee)); <b>let</b> amount = to_deposit.value; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositAbortsIf">DepositAbortsIf</a><Token>{amount: amount}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositOverflowAbortsIf">DepositOverflowAbortsIf</a><Token>{amount: amount}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositEnsures">DepositEnsures</a><Token>{amount: amount}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositEmits">DepositEmits</a><Token>{amount: amount}; <b>include</b> dual_attestation ==> <a href="DualAttestation.md#0x1_DualAttestation_AssertPaymentOkAbortsIf">DualAttestation::AssertPaymentOkAbortsIf</a><Token>{value: amount}; </code></pre><a name="0x1_DiemAccount_DepositAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositAbortsIf">DepositAbortsIf</a><Token> { payer: address; payee: address; amount: u64; metadata: vector<u8>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositAbortsIfRestricted">DepositAbortsIfRestricted</a><Token>; <b>include</b> <a href="AccountFreezing.md#0x1_AccountFreezing_AbortsIfFrozen">AccountFreezing::AbortsIfFrozen</a>{account: payee}; <b>aborts_if</b> !<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payee) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; <b>aborts_if</b> !<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(payee) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; } </code></pre><a name="0x1_DiemAccount_DepositOverflowAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositOverflowAbortsIf">DepositOverflowAbortsIf</a><Token> { payee: address; amount: u64; <b>aborts_if</b> <a href="DiemAccount.md#0x1_DiemAccount_balance">balance</a><Token>(payee) + amount > max_u64() <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre><a name="0x1_DiemAccount_DepositAbortsIfRestricted"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositAbortsIfRestricted">DepositAbortsIfRestricted</a><Token> { payer: address; payee: address; amount: u64; metadata: vector<u8>; <b>include</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>; <b>aborts_if</b> amount == 0 <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_should_track_limits_for_account">spec_should_track_limits_for_account</a><Token>(payer, payee, <b>false</b>) ==> <a href="AccountLimits.md#0x1_AccountLimits_UpdateDepositLimitsAbortsIf">AccountLimits::UpdateDepositLimitsAbortsIf</a><Token> { addr: <a href="VASP.md#0x1_VASP_spec_parent_address">VASP::spec_parent_address</a>(payee), }; <b>aborts_if</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_should_track_limits_for_account">spec_should_track_limits_for_account</a><Token>(payer, payee, <b>false</b>) && !<a href="AccountLimits.md#0x1_AccountLimits_spec_update_deposit_limits">AccountLimits::spec_update_deposit_limits</a><Token>(amount, <a href="VASP.md#0x1_VASP_spec_parent_address">VASP::spec_parent_address</a>(payee)) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; <b>include</b> <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">Diem::AbortsIfNoCurrency</a><Token>; } </code></pre><a name="0x1_DiemAccount_DepositEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositEnsures">DepositEnsures</a><Token> { payee: address; amount: u64; <b>ensures</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payee); <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_balance">balance</a><Token>(payee) == <b>old</b>(<a href="DiemAccount.md#0x1_DiemAccount_balance">balance</a><Token>(payee)) + amount; <b>ensures</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee); <b>ensures</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee).withdraw_capability == <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee).withdraw_capability); <b>ensures</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee).authentication_key == <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee).authentication_key); <b>ensures</b> <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_spec_guid_eq">Event::spec_guid_eq</a>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee).sent_events, <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee).sent_events)); <b>ensures</b> <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_spec_guid_eq">Event::spec_guid_eq</a>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee).received_events, <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee).received_events)); } </code></pre><a name="0x1_DiemAccount_DepositEmits"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositEmits">DepositEmits</a><Token> { payer: address; payee: address; amount: u64; metadata: vector<u8>; <b>let</b> handle = <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee).received_events; <b>let</b> msg = <a href="DiemAccount.md#0x1_DiemAccount_ReceivedPaymentEvent">ReceivedPaymentEvent</a> { amount, currency_code: <a href="Diem.md#0x1_Diem_spec_currency_code">Diem::spec_currency_code</a><Token>(), payer, metadata }; emits msg <b>to</b> handle; } </code></pre> </details><a name="0x1_DiemAccount_tiered_mint"></a>
tiered_mintMint 'mint_amount' to 'designated_dealer_address' for 'tier_index' tier. Max valid tier index is 3 since there are max 4 tiers per DD. Sender should be treasury compliance account and receiver authorized DD.
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_tiered_mint">tiered_mint</a><Token>(tc_account: &signer, designated_dealer_address: address, mint_amount: u64, tier_index: u64) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_tiered_mint">tiered_mint</a><Token>( tc_account: &signer, designated_dealer_address: address, mint_amount: u64, tier_index: u64, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>, <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a>, <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> { <a href="Roles.md#0x1_Roles_assert_treasury_compliance">Roles::assert_treasury_compliance</a>(tc_account); <b>let</b> coin = <a href="DesignatedDealer.md#0x1_DesignatedDealer_tiered_mint">DesignatedDealer::tiered_mint</a><Token>( tc_account, mint_amount, designated_dealer_address, tier_index ); // Use the reserved address <b>as</b> the payer because the funds did not come from an existing // balance <a href="DiemAccount.md#0x1_DiemAccount_deposit">deposit</a>(@VMReserved, designated_dealer_address, coin, x"", x"", <b>false</b>) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(designated_dealer_address); <b>modifies</b> <b>global</b><<a href="DesignatedDealer.md#0x1_DesignatedDealer_Dealer">DesignatedDealer::Dealer</a>>(designated_dealer_address); <b>modifies</b> <b>global</b><<a href="DesignatedDealer.md#0x1_DesignatedDealer_TierInfo">DesignatedDealer::TierInfo</a><Token>>(designated_dealer_address); <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(designated_dealer_address); <b>modifies</b> <b>global</b><<a href="AccountLimits.md#0x1_AccountLimits_Window">AccountLimits::Window</a><Token>>(<a href="VASP.md#0x1_VASP_spec_parent_address">VASP::spec_parent_address</a>(designated_dealer_address)); <b>modifies</b> <b>global</b><<a href="Diem.md#0x1_Diem_CurrencyInfo">Diem::CurrencyInfo</a><Token>>(@CurrencyInfo); <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_TieredMintAbortsIf">TieredMintAbortsIf</a><Token>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_TieredMintEnsures">TieredMintEnsures</a><Token>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_TieredMintEmits">TieredMintEmits</a><Token>; </code></pre><a name="0x1_DiemAccount_TieredMintAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_TieredMintAbortsIf">TieredMintAbortsIf</a><Token> { tc_account: signer; designated_dealer_address: address; mint_amount: u64; tier_index: u64; <b>include</b> <a href="DesignatedDealer.md#0x1_DesignatedDealer_TieredMintAbortsIf">DesignatedDealer::TieredMintAbortsIf</a><Token>{dd_addr: designated_dealer_address, amount: mint_amount}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositAbortsIf">DepositAbortsIf</a><Token>{payer: @VMReserved, payee: designated_dealer_address, amount: mint_amount, metadata: x""}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositOverflowAbortsIf">DepositOverflowAbortsIf</a><Token>{payee: designated_dealer_address, amount: mint_amount}; } </code></pre><a name="0x1_DiemAccount_TieredMintEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_TieredMintEnsures">TieredMintEnsures</a><Token> { designated_dealer_address: address; mint_amount: u64; <b>let</b> dealer_balance = <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(designated_dealer_address).coin.value; <b>let</b> post post_dealer_balance = <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(designated_dealer_address).coin.value; <b>let</b> currency_info = <b>global</b><<a href="Diem.md#0x1_Diem_CurrencyInfo">Diem::CurrencyInfo</a><Token>>(@CurrencyInfo); <b>let</b> post post_currency_info = <b>global</b><<a href="Diem.md#0x1_Diem_CurrencyInfo">Diem::CurrencyInfo</a><Token>>(@CurrencyInfo); } </code></pre>Total value of the currency increases by <code>amount</code>.
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_TieredMintEnsures">TieredMintEnsures</a><Token> { <b>ensures</b> post_currency_info == update_field(currency_info, total_value, currency_info.total_value + mint_amount); } </code></pre>The balance of designated dealer increases by <code>amount</code>.
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_TieredMintEnsures">TieredMintEnsures</a><Token> { <b>ensures</b> post_dealer_balance == dealer_balance + mint_amount; } </code></pre><a name="0x1_DiemAccount_TieredMintEmits"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_TieredMintEmits">TieredMintEmits</a><Token> { tc_account: signer; designated_dealer_address: address; mint_amount: u64; tier_index: u64; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositEmits">DepositEmits</a><Token>{ payer: @VMReserved, payee: designated_dealer_address, amount: mint_amount, metadata: x"" }; <b>include</b> <a href="DesignatedDealer.md#0x1_DesignatedDealer_TieredMintEmits">DesignatedDealer::TieredMintEmits</a><Token>{dd_addr: designated_dealer_address, amount: mint_amount}; } </code></pre> </details><a name="0x1_DiemAccount_cancel_burn"></a>
cancel_burn<a name="0x1_DiemAccount_CancelBurnAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CancelBurnAbortsIf">CancelBurnAbortsIf</a><Token> { account: signer; preburn_address: address; amount: u64; <b>include</b> <a href="Diem.md#0x1_Diem_CancelBurnAbortsIf">Diem::CancelBurnAbortsIf</a><Token>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositAbortsIf">DepositAbortsIf</a><Token>{ payer: preburn_address, payee: preburn_address, amount: amount, metadata: x"", }; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositOverflowAbortsIf">DepositOverflowAbortsIf</a><Token>{payee: preburn_address, amount: amount}; } </code></pre> </details><a name="0x1_DiemAccount_withdraw_from_balance"></a>
withdraw_from_balanceHelper to withdraw <code>amount</code> from the given account balance and return the withdrawn Diem<Token>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_withdraw_from_balance">withdraw_from_balance</a><Token>(payer: address, payee: address, balance: &<b>mut</b> <a href="DiemAccount.md#0x1_DiemAccount_Balance">DiemAccount::Balance</a><Token>, amount: u64): <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><Token> </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_withdraw_from_balance">withdraw_from_balance</a><Token>( payer: address, payee: address, balance: &<b>mut</b> <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>, amount: u64 ): <a href="Diem.md#0x1_Diem">Diem</a><Token> <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_operating">DiemTimestamp::assert_operating</a>(); <a href="AccountFreezing.md#0x1_AccountFreezing_assert_not_frozen">AccountFreezing::assert_not_frozen</a>(payer); // Make sure that this withdrawal is compliant <b>with</b> the limits on // the account <b>if</b> it's a inter-<a href="VASP.md#0x1_VASP">VASP</a> transfer, <b>if</b> (<a href="DiemAccount.md#0x1_DiemAccount_should_track_limits_for_account">should_track_limits_for_account</a><Token>(payer, payee, <b>true</b>)) { <b>let</b> can_withdraw = <a href="AccountLimits.md#0x1_AccountLimits_update_withdrawal_limits">AccountLimits::update_withdrawal_limits</a><Token>( amount, <a href="VASP.md#0x1_VASP_parent_address">VASP::parent_address</a>(payer), &borrow_global<<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot).limits_cap ); <b>assert</b>(can_withdraw, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="DiemAccount.md#0x1_DiemAccount_EWITHDRAWAL_EXCEEDS_LIMITS">EWITHDRAWAL_EXCEEDS_LIMITS</a>)); }; <b>let</b> coin = &<b>mut</b> balance.coin; // Abort <b>if</b> this withdrawal would make the `payer`'s balance go negative <b>assert</b>(<a href="Diem.md#0x1_Diem_value">Diem::value</a>(coin) >= amount, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="DiemAccount.md#0x1_DiemAccount_EINSUFFICIENT_BALANCE">EINSUFFICIENT_BALANCE</a>)); <a href="Diem.md#0x1_Diem_withdraw">Diem::withdraw</a>(coin, amount) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>modifies</b> <b>global</b><<a href="AccountLimits.md#0x1_AccountLimits_Window">AccountLimits::Window</a><Token>>(<a href="VASP.md#0x1_VASP_spec_parent_address">VASP::spec_parent_address</a>(payer)); <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromBalanceAbortsIf">WithdrawFromBalanceAbortsIf</a><Token>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromBalanceEnsures">WithdrawFromBalanceEnsures</a><Token>; </code></pre><a name="0x1_DiemAccount_WithdrawFromBalanceAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromBalanceAbortsIf">WithdrawFromBalanceAbortsIf</a><Token> { payer: address; payee: address; balance: <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>; amount: u64; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromBalanceNoLimitsAbortsIf">WithdrawFromBalanceNoLimitsAbortsIf</a><Token>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_should_track_limits_for_account">spec_should_track_limits_for_account</a><Token>(payer, payee, <b>true</b>) ==> <a href="AccountLimits.md#0x1_AccountLimits_UpdateWithdrawalLimitsAbortsIf">AccountLimits::UpdateWithdrawalLimitsAbortsIf</a><Token> { addr: <a href="VASP.md#0x1_VASP_spec_parent_address">VASP::spec_parent_address</a>(payer), }; <b>aborts_if</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_should_track_limits_for_account">spec_should_track_limits_for_account</a><Token>(payer, payee, <b>true</b>) && ( !<a href="DiemAccount.md#0x1_DiemAccount_spec_has_account_operations_cap">spec_has_account_operations_cap</a>() || !<a href="AccountLimits.md#0x1_AccountLimits_spec_update_withdrawal_limits">AccountLimits::spec_update_withdrawal_limits</a><Token>(amount, <a href="VASP.md#0x1_VASP_spec_parent_address">VASP::spec_parent_address</a>(payer)) ) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre><a name="0x1_DiemAccount_WithdrawFromBalanceNoLimitsAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromBalanceNoLimitsAbortsIf">WithdrawFromBalanceNoLimitsAbortsIf</a><Token> { payer: address; payee: address; balance: <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>; amount: u64; <b>include</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>; <b>include</b> <a href="AccountFreezing.md#0x1_AccountFreezing_AbortsIfFrozen">AccountFreezing::AbortsIfFrozen</a>{account: payer}; <b>aborts_if</b> balance.coin.value < amount <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre><a name="0x1_DiemAccount_WithdrawFromBalanceEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromBalanceEnsures">WithdrawFromBalanceEnsures</a><Token> { balance: <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>; amount: u64; result: <a href="Diem.md#0x1_Diem">Diem</a><Token>; <b>ensures</b> balance.coin.value == <b>old</b>(balance.coin.value) - amount; <b>ensures</b> result.value == amount; } </code></pre> </details><a name="0x1_DiemAccount_withdraw_from"></a>
withdraw_fromWithdraw <code>amount</code> <code><a href="Diem.md#0x1_Diem">Diem</a><Token></code>'s from the account balance under <code>cap.account_address</code>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_withdraw_from">withdraw_from</a><Token>(cap: &<a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">DiemAccount::WithdrawCapability</a>, payee: address, amount: u64, metadata: vector<u8>): <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><Token> </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_withdraw_from">withdraw_from</a><Token>( cap: &<a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a>, payee: address, amount: u64, metadata: vector<u8>, ): <a href="Diem.md#0x1_Diem">Diem</a><Token> <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a>, <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>, <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a> { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_operating">DiemTimestamp::assert_operating</a>(); <b>let</b> payer = cap.account_address; <b>assert</b>(<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(payer), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EACCOUNT">EACCOUNT</a>)); <b>assert</b>(<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payer), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EPAYER_DOESNT_HOLD_CURRENCY">EPAYER_DOESNT_HOLD_CURRENCY</a>)); <b>let</b> account_balance = borrow_global_mut<<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payer); // Load the payer's account and emit an event <b>to</b> record the withdrawal <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_emit_event">Event::emit_event</a><<a href="DiemAccount.md#0x1_DiemAccount_SentPaymentEvent">SentPaymentEvent</a>>( &<b>mut</b> borrow_global_mut<<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).sent_events, <a href="DiemAccount.md#0x1_DiemAccount_SentPaymentEvent">SentPaymentEvent</a> { amount, currency_code: <a href="Diem.md#0x1_Diem_currency_code">Diem::currency_code</a><Token>(), payee, metadata }, ); <a href="DiemAccount.md#0x1_DiemAccount_withdraw_from_balance">withdraw_from_balance</a><Token>(payer, payee, account_balance, amount) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>let</b> payer = cap.account_address; <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payer); <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer); <b>modifies</b> <b>global</b><<a href="AccountLimits.md#0x1_AccountLimits_Window">AccountLimits::Window</a><Token>>(<a href="VASP.md#0x1_VASP_spec_parent_address">VASP::spec_parent_address</a>(payer)); <b>ensures</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer); <b>ensures</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).withdraw_capability == <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).withdraw_capability); <b>ensures</b> <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_spec_guid_eq">Event::spec_guid_eq</a>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).sent_events, <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).sent_events)); <b>ensures</b> <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_spec_guid_eq">Event::spec_guid_eq</a>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).received_events, <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).received_events)); <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromAbortsIf">WithdrawFromAbortsIf</a><Token>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromBalanceEnsures">WithdrawFromBalanceEnsures</a><Token>{balance: <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payer)}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawOnlyFromCapAddress">WithdrawOnlyFromCapAddress</a><Token>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromEmits">WithdrawFromEmits</a><Token>; </code></pre><a name="0x1_DiemAccount_WithdrawFromAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromAbortsIf">WithdrawFromAbortsIf</a><Token> { cap: <a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a>; payee: address; amount: u64; <b>let</b> payer = cap.account_address; <b>include</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>; <b>include</b> <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">Diem::AbortsIfNoCurrency</a><Token>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromBalanceAbortsIf">WithdrawFromBalanceAbortsIf</a><Token>{payer, balance: <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payer)}; <b>aborts_if</b> !<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(payer) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <b>aborts_if</b> !<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payer) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; } </code></pre><a name="@Access_Control_1"></a>
<a name="0x1_DiemAccount_WithdrawOnlyFromCapAddress"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawOnlyFromCapAddress">WithdrawOnlyFromCapAddress</a><Token> { cap: <a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a>; } </code></pre>Can only withdraw from the balances of cap.account_address [H19].
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawOnlyFromCapAddress">WithdrawOnlyFromCapAddress</a><Token> { <b>ensures</b> <b>forall</b> addr: address <b>where</b> <b>old</b>(<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(addr)) && addr != cap.account_address: <a href="DiemAccount.md#0x1_DiemAccount_balance">balance</a><Token>(addr) == <b>old</b>(<a href="DiemAccount.md#0x1_DiemAccount_balance">balance</a><Token>(addr)); } </code></pre><a name="0x1_DiemAccount_WithdrawFromEmits"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromEmits">WithdrawFromEmits</a><Token> { cap: <a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a>; payee: address; amount: u64; metadata: vector<u8>; <b>let</b> payer = cap.account_address; <b>let</b> handle = <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).sent_events; <b>let</b> msg = <a href="DiemAccount.md#0x1_DiemAccount_SentPaymentEvent">SentPaymentEvent</a> { amount, currency_code: <a href="Diem.md#0x1_Diem_spec_currency_code">Diem::spec_currency_code</a><Token>(), payee, metadata }; emits msg <b>to</b> handle; } </code></pre> </details><a name="0x1_DiemAccount_preburn"></a>
preburnWithdraw <code>amount</code> <code><a href="Diem.md#0x1_Diem">Diem</a><Token></code>'s from <code>cap.address</code> and send them to the <code>Preburn</code> resource under <code>dd</code>.
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_preburn">preburn</a><Token>(dd: &signer, cap: &<a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">DiemAccount::WithdrawCapability</a>, amount: u64) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_preburn">preburn</a><Token>( dd: &signer, cap: &<a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a>, amount: u64 ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a>, <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>, <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a> { <a href="Roles.md#0x1_Roles_assert_designated_dealer">Roles::assert_designated_dealer</a>(dd); <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_operating">DiemTimestamp::assert_operating</a>(); <a href="Diem.md#0x1_Diem_preburn_to">Diem::preburn_to</a><Token>(dd, <a href="DiemAccount.md#0x1_DiemAccount_withdraw_from">withdraw_from</a>(cap, <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(dd), amount, x"")) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>let</b> dd_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(dd); <b>let</b> payer = cap.account_address; <b>modifies</b> <b>global</b><<a href="AccountLimits.md#0x1_AccountLimits_Window">AccountLimits::Window</a><Token>>(<a href="VASP.md#0x1_VASP_spec_parent_address">VASP::spec_parent_address</a>(payer)); <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer); <b>ensures</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer); <b>ensures</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).withdraw_capability == <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).withdraw_capability); <b>ensures</b> <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_spec_guid_eq">Event::spec_guid_eq</a>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).sent_events, <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).sent_events)); <b>ensures</b> <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_spec_guid_eq">Event::spec_guid_eq</a>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).received_events, <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).received_events)); <b>ensures</b> <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_spec_guid_eq">Event::spec_guid_eq</a>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(dd_addr).sent_events, <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(dd_addr).sent_events)); <b>ensures</b> <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_spec_guid_eq">Event::spec_guid_eq</a>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(dd_addr).received_events, <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(dd_addr).received_events)); <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_PreburnAbortsIf">PreburnAbortsIf</a><Token>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_PreburnEnsures">PreburnEnsures</a><Token>{dd, payer}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_PreburnEmits">PreburnEmits</a><Token>; </code></pre><a name="0x1_DiemAccount_PreburnAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PreburnAbortsIf">PreburnAbortsIf</a><Token> { dd: signer; cap: <a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a>; amount: u64; <b>include</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>{}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromAbortsIf">WithdrawFromAbortsIf</a><Token>{payee: <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(dd)}; <b>include</b> <a href="Diem.md#0x1_Diem_PreburnToAbortsIf">Diem::PreburnToAbortsIf</a><Token>{account: dd}; } </code></pre><a name="0x1_DiemAccount_PreburnEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PreburnEnsures">PreburnEnsures</a><Token> { dd: signer; payer: address; amount: u64; <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payer); <b>let</b> payer_balance = <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payer).coin.value; <b>let</b> post post_payer_balance = <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payer).coin.value; } </code></pre>The balance of payer decreases by <code>amount</code>.
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PreburnEnsures">PreburnEnsures</a><Token> { <b>ensures</b> post_payer_balance == payer_balance - amount; } </code></pre>The value of preburn at <code>dd_addr</code> increases by <code>amount</code>;
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PreburnEnsures">PreburnEnsures</a><Token> { <b>include</b> <a href="Diem.md#0x1_Diem_PreburnToEnsures">Diem::PreburnToEnsures</a><Token>{amount, account: dd}; } </code></pre><a name="0x1_DiemAccount_PreburnEmits"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PreburnEmits">PreburnEmits</a><Token> { dd: signer; cap: <a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a>; amount: u64; <b>let</b> dd_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(dd); <b>include</b> <a href="Diem.md#0x1_Diem_PreburnWithResourceEmits">Diem::PreburnWithResourceEmits</a><Token>{preburn_address: dd_addr}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromEmits">WithdrawFromEmits</a><Token>{payee: dd_addr, metadata: x""}; } </code></pre> </details><a name="0x1_DiemAccount_extract_withdraw_capability"></a>
extract_withdraw_capabilityReturn a unique capability granting permission to withdraw from the sender's account balance.
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_extract_withdraw_capability">extract_withdraw_capability</a>(sender: &signer): <a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">DiemAccount::WithdrawCapability</a> </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_extract_withdraw_capability">extract_withdraw_capability</a>( sender: &signer ): <a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a> <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a> { <b>let</b> sender_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(sender); // Abort <b>if</b> we already extracted the unique withdraw capability for this account. <b>assert</b>( !<a href="DiemAccount.md#0x1_DiemAccount_delegated_withdraw_capability">delegated_withdraw_capability</a>(sender_addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(<a href="DiemAccount.md#0x1_DiemAccount_EWITHDRAW_CAPABILITY_ALREADY_EXTRACTED">EWITHDRAW_CAPABILITY_ALREADY_EXTRACTED</a>) ); <b>assert</b>(<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(sender_addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EACCOUNT">EACCOUNT</a>)); <b>let</b> account = borrow_global_mut<<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(sender_addr); <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_extract">Option::extract</a>(&<b>mut</b> account.withdraw_capability) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>let</b> sender_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(sender); <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(sender_addr); <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_ExtractWithdrawCapAbortsIf">ExtractWithdrawCapAbortsIf</a>{sender_addr}; <b>ensures</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(sender_addr); <b>ensures</b> result == <b>old</b>(<a href="DiemAccount.md#0x1_DiemAccount_spec_get_withdraw_cap">spec_get_withdraw_cap</a>(sender_addr)); <b>ensures</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(sender_addr) == update_field(<b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(sender_addr)), withdraw_capability, <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_spec_none">Option::spec_none</a>()); <b>ensures</b> result.account_address == sender_addr; </code></pre><a name="0x1_DiemAccount_ExtractWithdrawCapAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_ExtractWithdrawCapAbortsIf">ExtractWithdrawCapAbortsIf</a> { sender_addr: address; <b>aborts_if</b> !<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(sender_addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <b>aborts_if</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_delegated_withdraw_capability">spec_holds_delegated_withdraw_capability</a>(sender_addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_STATE">Errors::INVALID_STATE</a>; } </code></pre> </details><a name="0x1_DiemAccount_restore_withdraw_capability"></a>
restore_withdraw_capabilityReturn the withdraw capability to the account it originally came from
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_restore_withdraw_capability">restore_withdraw_capability</a>(cap: <a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">DiemAccount::WithdrawCapability</a>) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_restore_withdraw_capability">restore_withdraw_capability</a>(cap: <a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a>) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a> { <b>assert</b>(<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(cap.account_address), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EACCOUNT">EACCOUNT</a>)); // Abort <b>if</b> the withdraw capability for this account is not extracted, // indicating that the withdraw capability is not unique. <b>assert</b>( <a href="DiemAccount.md#0x1_DiemAccount_delegated_withdraw_capability">delegated_withdraw_capability</a>(cap.account_address), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(<a href="DiemAccount.md#0x1_DiemAccount_EWITHDRAW_CAPABILITY_NOT_EXTRACTED">EWITHDRAW_CAPABILITY_NOT_EXTRACTED</a>) ); <b>let</b> account = borrow_global_mut<<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(cap.account_address); <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_fill">Option::fill</a>(&<b>mut</b> account.withdraw_capability, cap) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>let</b> cap_addr = cap.account_address; <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(cap_addr); <b>ensures</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(cap_addr) == update_field(<b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(cap_addr)), withdraw_capability, <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_spec_some">Option::spec_some</a>(cap)); <b>aborts_if</b> !<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(cap_addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <b>aborts_if</b> !<a href="DiemAccount.md#0x1_DiemAccount_delegated_withdraw_capability">delegated_withdraw_capability</a>(cap_addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_STATE">Errors::INVALID_STATE</a>; <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_own_withdraw_cap">spec_holds_own_withdraw_cap</a>(cap_addr); </code></pre> </details><a name="0x1_DiemAccount_pay_from"></a>
pay_fromWithdraw <code>amount</code> Diem<Token> from the address embedded in <code><a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a></code> and deposits it into the <code>payee</code>'s account balance. The included <code>metadata</code> will appear in the <code><a href="DiemAccount.md#0x1_DiemAccount_SentPaymentEvent">SentPaymentEvent</a></code> and <code><a href="DiemAccount.md#0x1_DiemAccount_ReceivedPaymentEvent">ReceivedPaymentEvent</a></code>. The <code>metadata_signature</code> will only be checked if this payment is subject to the dual attestation protocol
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_pay_from">pay_from</a><Token>(cap: &<a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">DiemAccount::WithdrawCapability</a>, payee: address, amount: u64, metadata: vector<u8>, metadata_signature: vector<u8>) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_pay_from">pay_from</a><Token>( cap: &<a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a>, payee: address, amount: u64, metadata: vector<u8>, metadata_signature: vector<u8> ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>, <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a>, <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> { <a href="DiemAccount.md#0x1_DiemAccount_deposit">deposit</a><Token>( *&cap.account_address, payee, <a href="DiemAccount.md#0x1_DiemAccount_withdraw_from">withdraw_from</a>(cap, payee, amount, <b>copy</b> metadata), metadata, metadata_signature, <b>true</b> ); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>let</b> payer = cap.account_address; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_PayFromWithoutDualAttestation">PayFromWithoutDualAttestation</a><Token>; <b>include</b> <a href="DualAttestation.md#0x1_DualAttestation_AssertPaymentOkAbortsIf">DualAttestation::AssertPaymentOkAbortsIf</a><Token>{value: amount}; </code></pre> </details><a name="0x1_DiemAccount_pay_by_signers"></a>
pay_by_signersWithdraw <code>amount</code> Diem<Token> from the address embedded in <code><a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a></code> and deposits it into the <code>payee</code>'s account balance. The included <code>metadata</code> will appear in the <code><a href="DiemAccount.md#0x1_DiemAccount_SentPaymentEvent">SentPaymentEvent</a></code> and <code><a href="DiemAccount.md#0x1_DiemAccount_ReceivedPaymentEvent">ReceivedPaymentEvent</a></code>. As <code>payee</code> is also signer of the transaction, no metadata signature is required for dual attestation.
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_pay_by_signers">pay_by_signers</a><Token>(cap: &<a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">DiemAccount::WithdrawCapability</a>, payee: &signer, amount: u64, metadata: vector<u8>) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_pay_by_signers">pay_by_signers</a><Token>( cap: &<a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a>, payee: &signer, amount: u64, metadata: vector<u8>, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>, <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a>, <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> { <b>let</b> payee_address = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(payee); <a href="DiemAccount.md#0x1_DiemAccount_deposit">deposit</a><Token>( *&cap.account_address, payee_address, <a href="DiemAccount.md#0x1_DiemAccount_withdraw_from">withdraw_from</a>(cap, payee_address, amount, <b>copy</b> metadata), metadata, x"", <b>false</b> ); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_PayFromWithoutDualAttestation">PayFromWithoutDualAttestation</a><Token>{ payer: cap.account_address, payee: <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(payee) }; </code></pre><a name="0x1_DiemAccount_PayFromWithoutDualAttestation"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PayFromWithoutDualAttestation">PayFromWithoutDualAttestation</a><Token> { payer: address; payee: address; amount: u64; metadata: vector<u8>; <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer); <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee); <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payer); <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payee); <b>modifies</b> <b>global</b><<a href="AccountLimits.md#0x1_AccountLimits_Window">AccountLimits::Window</a><Token>>(<a href="VASP.md#0x1_VASP_spec_parent_address">VASP::spec_parent_address</a>(payer)); <b>modifies</b> <b>global</b><<a href="AccountLimits.md#0x1_AccountLimits_Window">AccountLimits::Window</a><Token>>(<a href="VASP.md#0x1_VASP_spec_parent_address">VASP::spec_parent_address</a>(payee)); <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(payer); <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(payee); <b>ensures</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payer); <b>ensures</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payee); <b>ensures</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).withdraw_capability == <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).withdraw_capability); <b>ensures</b> <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_spec_guid_eq">Event::spec_guid_eq</a>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).sent_events, <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).sent_events)); <b>ensures</b> <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_spec_guid_eq">Event::spec_guid_eq</a>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).received_events, <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payer).received_events)); <b>ensures</b> <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_spec_guid_eq">Event::spec_guid_eq</a>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee).sent_events, <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee).sent_events)); <b>ensures</b> <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_spec_guid_eq">Event::spec_guid_eq</a>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee).received_events, <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(payee).received_events)); <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_PayFromAbortsIf">PayFromAbortsIf</a><Token>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_PayFromEnsures">PayFromEnsures</a><Token>{payer}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_PayFromEmits">PayFromEmits</a><Token>; } </code></pre><a name="0x1_DiemAccount_PayFromAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PayFromAbortsIf">PayFromAbortsIf</a><Token> { cap: <a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a>; payee: address; amount: u64; metadata: vector<u8>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositAbortsIf">DepositAbortsIf</a><Token>{payer: cap.account_address}; <b>include</b> cap.account_address != payee ==> <a href="DiemAccount.md#0x1_DiemAccount_DepositOverflowAbortsIf">DepositOverflowAbortsIf</a><Token>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromAbortsIf">WithdrawFromAbortsIf</a><Token>; } </code></pre><a name="0x1_DiemAccount_PayFromAbortsIfRestricted"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PayFromAbortsIfRestricted">PayFromAbortsIfRestricted</a><Token> { cap: <a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a>; payee: address; amount: u64; metadata: vector<u8>; <b>let</b> payer = cap.account_address; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositAbortsIfRestricted">DepositAbortsIfRestricted</a><Token>{payer: cap.account_address}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromBalanceNoLimitsAbortsIf">WithdrawFromBalanceNoLimitsAbortsIf</a><Token>{payer, balance: <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payer)}; <b>aborts_if</b> !<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(payer) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; } </code></pre><a name="0x1_DiemAccount_PayFromEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PayFromEnsures">PayFromEnsures</a><Token> { payer: address; payee: address; amount: u64; <b>ensures</b> payer == payee ==> <a href="DiemAccount.md#0x1_DiemAccount_balance">balance</a><Token>(payer) == <b>old</b>(<a href="DiemAccount.md#0x1_DiemAccount_balance">balance</a><Token>(payer)); <b>ensures</b> payer != payee ==> <a href="DiemAccount.md#0x1_DiemAccount_balance">balance</a><Token>(payer) == <b>old</b>(<a href="DiemAccount.md#0x1_DiemAccount_balance">balance</a><Token>(payer)) - amount; <b>ensures</b> payer != payee ==> <a href="DiemAccount.md#0x1_DiemAccount_balance">balance</a><Token>(payee) == <b>old</b>(<a href="DiemAccount.md#0x1_DiemAccount_balance">balance</a><Token>(payee)) + amount; } </code></pre><a name="0x1_DiemAccount_PayFromEmits"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PayFromEmits">PayFromEmits</a><Token> { cap: <a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a>; payee: address; amount: u64; metadata: vector<u8>; <b>let</b> payer = cap.account_address; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_DepositEmits">DepositEmits</a><Token>{payer: payer}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_WithdrawFromEmits">WithdrawFromEmits</a><Token>; } </code></pre> </details><a name="0x1_DiemAccount_rotate_authentication_key"></a>
rotate_authentication_keyRotate the authentication key for the account under cap.account_address
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_rotate_authentication_key">rotate_authentication_key</a>(cap: &<a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">DiemAccount::KeyRotationCapability</a>, new_authentication_key: vector<u8>) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_rotate_authentication_key">rotate_authentication_key</a>( cap: &<a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">KeyRotationCapability</a>, new_authentication_key: vector<u8>, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a> { <b>assert</b>(<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(cap.account_address), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EACCOUNT">EACCOUNT</a>)); <b>let</b> sender_account_resource = borrow_global_mut<<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(cap.account_address); // Don't allow rotating <b>to</b> clearly invalid key <b>assert</b>( <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(&new_authentication_key) == 32, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemAccount.md#0x1_DiemAccount_EMALFORMED_AUTHENTICATION_KEY">EMALFORMED_AUTHENTICATION_KEY</a>) ); sender_account_resource.authentication_key = new_authentication_key; } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_RotateAuthenticationKeyAbortsIf">RotateAuthenticationKeyAbortsIf</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_RotateAuthenticationKeyEnsures">RotateAuthenticationKeyEnsures</a>{addr: cap.account_address}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_RotateOnlyKeyOfCapAddress">RotateOnlyKeyOfCapAddress</a>; </code></pre><a name="0x1_DiemAccount_RotateAuthenticationKeyAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_RotateAuthenticationKeyAbortsIf">RotateAuthenticationKeyAbortsIf</a> { cap: &<a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">KeyRotationCapability</a>; new_authentication_key: vector<u8>; <b>aborts_if</b> !<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(cap.account_address) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <b>aborts_if</b> len(new_authentication_key) != 32 <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre><a name="0x1_DiemAccount_RotateAuthenticationKeyEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_RotateAuthenticationKeyEnsures">RotateAuthenticationKeyEnsures</a> { addr: address; new_authentication_key: vector<u8>; <b>ensures</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr).authentication_key == new_authentication_key; } </code></pre><a name="@Access_Control_2"></a>
<a name="0x1_DiemAccount_RotateOnlyKeyOfCapAddress"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_RotateOnlyKeyOfCapAddress">RotateOnlyKeyOfCapAddress</a> { cap: <a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">KeyRotationCapability</a>; } </code></pre>Can only rotate the authentication_key of cap.account_address [H18].
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_RotateOnlyKeyOfCapAddress">RotateOnlyKeyOfCapAddress</a> { <b>ensures</b> <b>forall</b> addr: address <b>where</b> addr != cap.account_address && <b>old</b>(<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr)): <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr).authentication_key == <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr).authentication_key); } </code></pre> </details><a name="0x1_DiemAccount_extract_key_rotation_capability"></a>
extract_key_rotation_capabilityReturn a unique capability granting permission to rotate the sender's authentication key
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_extract_key_rotation_capability">extract_key_rotation_capability</a>(account: &signer): <a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">DiemAccount::KeyRotationCapability</a> </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_extract_key_rotation_capability">extract_key_rotation_capability</a>(account: &signer): <a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">KeyRotationCapability</a> <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a> { <b>let</b> account_address = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); // Abort <b>if</b> we already extracted the unique key rotation capability for this account. <b>assert</b>( !<a href="DiemAccount.md#0x1_DiemAccount_delegated_key_rotation_capability">delegated_key_rotation_capability</a>(account_address), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(<a href="DiemAccount.md#0x1_DiemAccount_EKEY_ROTATION_CAPABILITY_ALREADY_EXTRACTED">EKEY_ROTATION_CAPABILITY_ALREADY_EXTRACTED</a>) ); <b>assert</b>(<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(account_address), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EACCOUNT">EACCOUNT</a>)); <b>let</b> account = borrow_global_mut<<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(account_address); <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_extract">Option::extract</a>(&<b>mut</b> account.key_rotation_capability) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_ExtractKeyRotationCapabilityAbortsIf">ExtractKeyRotationCapabilityAbortsIf</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_ExtractKeyRotationCapabilityEnsures">ExtractKeyRotationCapabilityEnsures</a>; </code></pre><a name="0x1_DiemAccount_ExtractKeyRotationCapabilityAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_ExtractKeyRotationCapabilityAbortsIf">ExtractKeyRotationCapabilityAbortsIf</a> { account: signer; <b>let</b> account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); <b>aborts_if</b> !<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(account_addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_AbortsIfDelegatedKeyRotationCapability">AbortsIfDelegatedKeyRotationCapability</a>; } </code></pre><a name="0x1_DiemAccount_AbortsIfDelegatedKeyRotationCapability"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_AbortsIfDelegatedKeyRotationCapability">AbortsIfDelegatedKeyRotationCapability</a> { account: signer; <b>aborts_if</b> <a href="DiemAccount.md#0x1_DiemAccount_delegated_key_rotation_capability">delegated_key_rotation_capability</a>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account)) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_STATE">Errors::INVALID_STATE</a>; } </code></pre><a name="0x1_DiemAccount_ExtractKeyRotationCapabilityEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_ExtractKeyRotationCapabilityEnsures">ExtractKeyRotationCapabilityEnsures</a> { account: signer; <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_delegated_key_rotation_capability">delegated_key_rotation_capability</a>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account)); } </code></pre> </details><a name="0x1_DiemAccount_restore_key_rotation_capability"></a>
restore_key_rotation_capabilityReturn the key rotation capability to the account it originally came from
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_restore_key_rotation_capability">restore_key_rotation_capability</a>(cap: <a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">DiemAccount::KeyRotationCapability</a>) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_restore_key_rotation_capability">restore_key_rotation_capability</a>(cap: <a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">KeyRotationCapability</a>) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a> { <b>assert</b>(<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(cap.account_address), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EACCOUNT">EACCOUNT</a>)); <b>let</b> account = borrow_global_mut<<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(cap.account_address); <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_fill">Option::fill</a>(&<b>mut</b> account.key_rotation_capability, cap) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_RestoreKeyRotationCapabilityAbortsIf">RestoreKeyRotationCapabilityAbortsIf</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_RestoreKeyRotationCapabilityEnsures">RestoreKeyRotationCapabilityEnsures</a>; </code></pre><a name="0x1_DiemAccount_RestoreKeyRotationCapabilityAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_RestoreKeyRotationCapabilityAbortsIf">RestoreKeyRotationCapabilityAbortsIf</a> { cap: <a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">KeyRotationCapability</a>; <b>aborts_if</b> !<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(cap.account_address) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <b>aborts_if</b> !<a href="DiemAccount.md#0x1_DiemAccount_delegated_key_rotation_capability">delegated_key_rotation_capability</a>(cap.account_address) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre><a name="0x1_DiemAccount_RestoreKeyRotationCapabilityEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_RestoreKeyRotationCapabilityEnsures">RestoreKeyRotationCapabilityEnsures</a> { cap: <a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">KeyRotationCapability</a>; <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_own_key_rotation_cap">spec_holds_own_key_rotation_cap</a>(cap.account_address); } </code></pre> </details><a name="0x1_DiemAccount_add_currencies_for_account"></a>
add_currencies_for_accountAdd balances for <code>Token</code> to <code>new_account</code>. If <code>add_all_currencies</code> is true, then add for both token types.
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_add_currencies_for_account">add_currencies_for_account</a><Token>(new_account: &signer, add_all_currencies: bool) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_add_currencies_for_account">add_currencies_for_account</a><Token>( new_account: &signer, add_all_currencies: bool, ) { <b>let</b> new_account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(new_account); <a href="DiemAccount.md#0x1_DiemAccount_add_currency">add_currency</a><Token>(new_account); <b>if</b> (add_all_currencies) { <b>if</b> (!<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><<a href="XUS.md#0x1_XUS">XUS</a>>>(new_account_addr)) { <a href="DiemAccount.md#0x1_DiemAccount_add_currency">add_currency</a><<a href="XUS.md#0x1_XUS">XUS</a>>(new_account); }; <b>if</b> (!<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><<a href="XDX.md#0x1_XDX">XDX</a>>>(new_account_addr)) { <a href="DiemAccount.md#0x1_DiemAccount_add_currency">add_currency</a><<a href="XDX.md#0x1_XDX">XDX</a>>(new_account); }; }; } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>let</b> new_account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(new_account); <b>aborts_if</b> !<a href="Roles.md#0x1_Roles_spec_can_hold_balance_addr">Roles::spec_can_hold_balance_addr</a>(new_account_addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; <b>aborts_if</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(new_account_addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; <b>aborts_if</b> !<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(new_account_addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyForAccountAbortsIf">AddCurrencyForAccountAbortsIf</a><Token>{addr: new_account_addr}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyForAccountEnsures">AddCurrencyForAccountEnsures</a><Token>{addr: new_account_addr}; </code></pre><a name="0x1_DiemAccount_AddCurrencyForAccountAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyForAccountAbortsIf">AddCurrencyForAccountAbortsIf</a><Token> { addr: address; add_all_currencies: bool; <b>include</b> <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">Diem::AbortsIfNoCurrency</a><Token>; <b>include</b> add_all_currencies && !<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><<a href="XUS.md#0x1_XUS">XUS</a>>>(addr) ==> <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">Diem::AbortsIfNoCurrency</a><<a href="XUS.md#0x1_XUS">XUS</a>>; <b>include</b> add_all_currencies && !<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><<a href="XDX.md#0x1_XDX">XDX</a>>>(addr) ==> <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">Diem::AbortsIfNoCurrency</a><<a href="XDX.md#0x1_XDX">XDX</a>>; } </code></pre><a name="0x1_DiemAccount_AddCurrencyForAccountEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyForAccountEnsures">AddCurrencyForAccountEnsures</a><Token> { addr: address; add_all_currencies: bool; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyEnsures">AddCurrencyEnsures</a><Token>; <b>include</b> add_all_currencies && !<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><<a href="XUS.md#0x1_XUS">XUS</a>>>(addr) ==> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyEnsures">AddCurrencyEnsures</a><<a href="XUS.md#0x1_XUS">XUS</a>>; <b>include</b> add_all_currencies && !<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><<a href="XDX.md#0x1_XDX">XDX</a>>>(addr) ==> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyEnsures">AddCurrencyEnsures</a><<a href="XDX.md#0x1_XDX">XDX</a>>; } </code></pre> </details><a name="0x1_DiemAccount_make_account"></a>
make_accountCreates a new account with account at <code>new_account_address</code> with authentication key <code>auth_key_prefix</code> | <code>fresh_address</code>. Aborts if there is already an account at <code>new_account_address</code>.
Creating an account at address 0x0 will abort as it is a reserved address for the MoveVM.
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_make_account">make_account</a>(new_account: &signer, auth_key_prefix: vector<u8>) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_make_account">make_account</a>( new_account: &signer, auth_key_prefix: vector<u8>, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> { <b>let</b> new_account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(new_account); // cannot create an account at the reserved address 0x0 <b>assert</b>( new_account_addr != @VMReserved, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemAccount.md#0x1_DiemAccount_ECANNOT_CREATE_AT_VM_RESERVED">ECANNOT_CREATE_AT_VM_RESERVED</a>) ); <b>assert</b>( new_account_addr != @DiemFramework, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemAccount.md#0x1_DiemAccount_ECANNOT_CREATE_AT_CORE_CODE">ECANNOT_CREATE_AT_CORE_CODE</a>) ); // Construct authentication key. <b>let</b> authentication_key = <a href="DiemAccount.md#0x1_DiemAccount_create_authentication_key">create_authentication_key</a>(new_account, auth_key_prefix); // Publish <a href="AccountFreezing.md#0x1_AccountFreezing_FreezingBit">AccountFreezing::FreezingBit</a> (initially not frozen) <a href="AccountFreezing.md#0x1_AccountFreezing_create">AccountFreezing::create</a>(new_account); // The <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> is published during <a href="Genesis.md#0x1_Genesis">Genesis</a>, so it should // always exist. This is a sanity check. <b>assert</b>( <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EACCOUNT_OPERATIONS_CAPABILITY">EACCOUNT_OPERATIONS_CAPABILITY</a>) ); // Emit the <a href="DiemAccount.md#0x1_DiemAccount_CreateAccountEvent">CreateAccountEvent</a> <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_emit_event">Event::emit_event</a>( &<b>mut</b> borrow_global_mut<<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot).creation_events, <a href="DiemAccount.md#0x1_DiemAccount_CreateAccountEvent">CreateAccountEvent</a> { created: new_account_addr, role_id: <a href="Roles.md#0x1_Roles_get_role_id">Roles::get_role_id</a>(new_account_addr) }, ); move_to( new_account, <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a> { authentication_key, withdraw_capability: <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_some">Option::some</a>( <a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a> { account_address: new_account_addr }), key_rotation_capability: <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_some">Option::some</a>( <a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">KeyRotationCapability</a> { account_address: new_account_addr }), received_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_new_event_handle">Event::new_event_handle</a><<a href="DiemAccount.md#0x1_DiemAccount_ReceivedPaymentEvent">ReceivedPaymentEvent</a>>(new_account), sent_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_new_event_handle">Event::new_event_handle</a><<a href="DiemAccount.md#0x1_DiemAccount_SentPaymentEvent">SentPaymentEvent</a>>(new_account), sequence_number: 0, } ); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> opaque; <b>let</b> new_account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(new_account); <b>requires</b> !<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(new_account_addr); <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(new_account_addr); <b>modifies</b> <b>global</b><<a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_EventHandleGenerator">Event::EventHandleGenerator</a>>(new_account_addr); <b>modifies</b> <b>global</b><<a href="AccountFreezing.md#0x1_AccountFreezing_FreezingBit">AccountFreezing::FreezingBit</a>>(new_account_addr); <b>requires</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot); <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot); <b>ensures</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot); <b>requires</b> <b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">Roles::RoleId</a>>(new_account_addr); <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_MakeAccountAbortsIf">MakeAccountAbortsIf</a>{addr: new_account_addr}; <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(new_account_addr); <b>ensures</b> <a href="AccountFreezing.md#0x1_AccountFreezing_spec_account_is_not_frozen">AccountFreezing::spec_account_is_not_frozen</a>(new_account_addr); <b>let</b> account_ops_cap = <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot); <b>let</b> post post_account_ops_cap = <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot); <b>ensures</b> post_account_ops_cap == update_field(account_ops_cap, creation_events, account_ops_cap.creation_events); <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_own_key_rotation_cap">spec_holds_own_key_rotation_cap</a>(new_account_addr); <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_own_withdraw_cap">spec_holds_own_withdraw_cap</a>(new_account_addr); <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_MakeAccountEmits">MakeAccountEmits</a>{new_account_address: <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(new_account)}; </code></pre><a name="0x1_DiemAccount_MakeAccountAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_MakeAccountAbortsIf">MakeAccountAbortsIf</a> { addr: address; auth_key_prefix: vector<u8>; <b>aborts_if</b> addr == @VMReserved <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; <b>aborts_if</b> addr == @DiemFramework <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; <b>aborts_if</b> <b>exists</b><<a href="AccountFreezing.md#0x1_AccountFreezing_FreezingBit">AccountFreezing::FreezingBit</a>>(addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; <b>aborts_if</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_is_genesis">DiemTimestamp::is_genesis</a>() && !<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateAuthenticationKeyAbortsIf">CreateAuthenticationKeyAbortsIf</a>; } </code></pre><a name="0x1_DiemAccount_MakeAccountEmits"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_MakeAccountEmits">MakeAccountEmits</a> { new_account_address: address; <b>let</b> post handle = <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot).creation_events; <b>let</b> post msg = <a href="DiemAccount.md#0x1_DiemAccount_CreateAccountEvent">CreateAccountEvent</a> { created: new_account_address, role_id: <a href="Roles.md#0x1_Roles_spec_get_role_id">Roles::spec_get_role_id</a>(new_account_address) }; emits msg <b>to</b> handle; } </code></pre> </details><a name="0x1_DiemAccount_create_authentication_key"></a>
create_authentication_keyConstruct an authentication key, aborting if the prefix is not valid.
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_create_authentication_key">create_authentication_key</a>(account: &signer, auth_key_prefix: vector<u8>): vector<u8> </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_create_authentication_key">create_authentication_key</a>(account: &signer, auth_key_prefix: vector<u8>): vector<u8> { <b>let</b> authentication_key = auth_key_prefix; <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_append">Vector::append</a>( &<b>mut</b> authentication_key, <a href="../../../../../../move-stdlib/docs/BCS.md#0x1_BCS_to_bytes">BCS::to_bytes</a>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_borrow_address">Signer::borrow_address</a>(account)) ); <b>assert</b>( <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(&authentication_key) == 32, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemAccount.md#0x1_DiemAccount_EMALFORMED_AUTHENTICATION_KEY">EMALFORMED_AUTHENTICATION_KEY</a>) ); authentication_key } </code></pre> </details> <details> <summary>Specification</summary>The specification of this function is abstracted to avoid the complexity of vector concatenation of serialization results. The actual value of the key is assumed to be irrelevant for callers. Instead the uninterpreted function <code>spec_abstract_create_authentication_key</code> is used to represent the key value. The aborts behavior is, however, preserved: the caller must provide a key prefix of a specific length.
<pre><code><b>pragma</b> opaque; <b>include</b> [abstract] <a href="DiemAccount.md#0x1_DiemAccount_CreateAuthenticationKeyAbortsIf">CreateAuthenticationKeyAbortsIf</a>; <b>ensures</b> [abstract] result == <a href="DiemAccount.md#0x1_DiemAccount_spec_abstract_create_authentication_key">spec_abstract_create_authentication_key</a>(auth_key_prefix) && len(result) == 32; </code></pre><a name="0x1_DiemAccount_CreateAuthenticationKeyAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateAuthenticationKeyAbortsIf">CreateAuthenticationKeyAbortsIf</a> { auth_key_prefix: vector<u8>; <b>aborts_if</b> 16 + len(auth_key_prefix) != 32 <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre><a name="0x1_DiemAccount_spec_abstract_create_authentication_key"></a>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_abstract_create_authentication_key">spec_abstract_create_authentication_key</a>(auth_key_prefix: vector<u8>): vector<u8>; </code></pre> </details><a name="0x1_DiemAccount_create_diem_root_account"></a>
create_diem_root_accountCreates the diem root account (during genesis). Publishes the Diem root role, Publishes a SlidingNonce resource, sets up event generator, publishes AccountOperationsCapability, WriteSetManager, and finally makes the account.
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_create_diem_root_account">create_diem_root_account</a>(auth_key_prefix: vector<u8>) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_create_diem_root_account">create_diem_root_account</a>( auth_key_prefix: vector<u8>, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_genesis">DiemTimestamp::assert_genesis</a>(); <b>let</b> dr_account = <a href="DiemAccount.md#0x1_DiemAccount_create_signer">create_signer</a>(@DiemRoot); <a href="CoreAddresses.md#0x1_CoreAddresses_assert_diem_root">CoreAddresses::assert_diem_root</a>(&dr_account); <a href="Roles.md#0x1_Roles_grant_diem_root_role">Roles::grant_diem_root_role</a>(&dr_account); <a href="SlidingNonce.md#0x1_SlidingNonce_publish">SlidingNonce::publish</a>(&dr_account); <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_publish_generator">Event::publish_generator</a>(&dr_account); <b>assert</b>( !<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_already_published">Errors::already_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EACCOUNT_OPERATIONS_CAPABILITY">EACCOUNT_OPERATIONS_CAPABILITY</a>) ); move_to( &dr_account, <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> { limits_cap: <a href="AccountLimits.md#0x1_AccountLimits_grant_mutation_capability">AccountLimits::grant_mutation_capability</a>(&dr_account), creation_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_new_event_handle">Event::new_event_handle</a><<a href="DiemAccount.md#0x1_DiemAccount_CreateAccountEvent">CreateAccountEvent</a>>(&dr_account), } ); <b>assert</b>( !<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_DiemWriteSetManager">DiemWriteSetManager</a>>(@DiemRoot), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_already_published">Errors::already_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EWRITESET_MANAGER">EWRITESET_MANAGER</a>) ); move_to( &dr_account, <a href="DiemAccount.md#0x1_DiemAccount_DiemWriteSetManager">DiemWriteSetManager</a> { upgrade_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_new_event_handle">Event::new_event_handle</a><<a href="DiemAccount.md#0x1_DiemAccount_AdminTransactionEvent">Self::AdminTransactionEvent</a>>(&dr_account), } ); <a href="DiemAccount.md#0x1_DiemAccount_make_account">make_account</a>(&dr_account, auth_key_prefix) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> disable_invariants_in_body; <b>pragma</b> opaque; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateDiemRootAccountModifies">CreateDiemRootAccountModifies</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateDiemRootAccountAbortsIf">CreateDiemRootAccountAbortsIf</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateDiemRootAccountEnsures">CreateDiemRootAccountEnsures</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_MakeAccountEmits">MakeAccountEmits</a>{new_account_address: @DiemRoot}; </code></pre><a name="0x1_DiemAccount_CreateDiemRootAccountModifies"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateDiemRootAccountModifies">CreateDiemRootAccountModifies</a> { <b>let</b> dr_addr = @DiemRoot; <b>modifies</b> <b>global</b><<a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_EventHandleGenerator">Event::EventHandleGenerator</a>>(dr_addr); <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(dr_addr); <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(dr_addr); <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_DiemWriteSetManager">DiemWriteSetManager</a>>(dr_addr); <b>modifies</b> <b>global</b><<a href="SlidingNonce.md#0x1_SlidingNonce_SlidingNonce">SlidingNonce::SlidingNonce</a>>(dr_addr); <b>modifies</b> <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">Roles::RoleId</a>>(dr_addr); <b>modifies</b> <b>global</b><<a href="AccountFreezing.md#0x1_AccountFreezing_FreezingBit">AccountFreezing::FreezingBit</a>>(dr_addr); } </code></pre><a name="0x1_DiemAccount_CreateDiemRootAccountAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateDiemRootAccountAbortsIf">CreateDiemRootAccountAbortsIf</a> { auth_key_prefix: vector<u8>; <b>include</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotGenesis">DiemTimestamp::AbortsIfNotGenesis</a>; <b>include</b> <a href="Roles.md#0x1_Roles_GrantRole">Roles::GrantRole</a>{addr: @DiemRoot, role_id: <a href="Roles.md#0x1_Roles_DIEM_ROOT_ROLE_ID">Roles::DIEM_ROOT_ROLE_ID</a>}; <b>aborts_if</b> <b>exists</b><<a href="SlidingNonce.md#0x1_SlidingNonce_SlidingNonce">SlidingNonce::SlidingNonce</a>>(@DiemRoot) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; <b>aborts_if</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; <b>aborts_if</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_DiemWriteSetManager">DiemWriteSetManager</a>>(@DiemRoot) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; <b>aborts_if</b> <b>exists</b><<a href="AccountFreezing.md#0x1_AccountFreezing_FreezingBit">AccountFreezing::FreezingBit</a>>(@DiemRoot) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateAuthenticationKeyAbortsIf">CreateAuthenticationKeyAbortsIf</a>; } </code></pre><a name="0x1_DiemAccount_CreateDiemRootAccountEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateDiemRootAccountEnsures">CreateDiemRootAccountEnsures</a> { <b>let</b> dr_addr = @DiemRoot; <b>ensures</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(dr_addr); <b>ensures</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_DiemWriteSetManager">DiemWriteSetManager</a>>(dr_addr); <b>ensures</b> <b>exists</b><<a href="SlidingNonce.md#0x1_SlidingNonce_SlidingNonce">SlidingNonce::SlidingNonce</a>>(dr_addr); <b>ensures</b> <a href="Roles.md#0x1_Roles_spec_has_diem_root_role_addr">Roles::spec_has_diem_root_role_addr</a>(dr_addr); <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(dr_addr); <b>ensures</b> <a href="AccountFreezing.md#0x1_AccountFreezing_spec_account_is_not_frozen">AccountFreezing::spec_account_is_not_frozen</a>(dr_addr); <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_own_key_rotation_cap">spec_holds_own_key_rotation_cap</a>(dr_addr); <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_own_withdraw_cap">spec_holds_own_withdraw_cap</a>(dr_addr); } </code></pre> </details><a name="0x1_DiemAccount_create_treasury_compliance_account"></a>
create_treasury_compliance_accountCreate a treasury/compliance account at <code>new_account_address</code> with authentication key <code>auth_key_prefix</code> | <code>new_account_address</code>. Can only be called during genesis. Also, publishes the treasury compliance role, the SlidingNonce resource, and event handle generator, then makes the account.
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_create_treasury_compliance_account">create_treasury_compliance_account</a>(dr_account: &signer, auth_key_prefix: vector<u8>) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_create_treasury_compliance_account">create_treasury_compliance_account</a>( dr_account: &signer, auth_key_prefix: vector<u8>, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_genesis">DiemTimestamp::assert_genesis</a>(); <a href="Roles.md#0x1_Roles_assert_diem_root">Roles::assert_diem_root</a>(dr_account); <b>let</b> new_account_address = @TreasuryCompliance; <b>let</b> new_account = <a href="DiemAccount.md#0x1_DiemAccount_create_signer">create_signer</a>(new_account_address); <a href="Roles.md#0x1_Roles_grant_treasury_compliance_role">Roles::grant_treasury_compliance_role</a>(&new_account, dr_account); <a href="SlidingNonce.md#0x1_SlidingNonce_publish">SlidingNonce::publish</a>(&new_account); <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_publish_generator">Event::publish_generator</a>(&new_account); <a href="VASPDomain.md#0x1_VASPDomain_publish_vasp_domain_manager">VASPDomain::publish_vasp_domain_manager</a>(&new_account); <a href="DiemAccount.md#0x1_DiemAccount_make_account">make_account</a>(&new_account, auth_key_prefix) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> disable_invariants_in_body; <b>pragma</b> opaque; <b>let</b> tc_addr = @TreasuryCompliance; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateTreasuryComplianceAccountModifies">CreateTreasuryComplianceAccountModifies</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateTreasuryComplianceAccountAbortsIf">CreateTreasuryComplianceAccountAbortsIf</a>; <b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">Roles::AbortsIfNotDiemRoot</a>{account: dr_account}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_MakeAccountAbortsIf">MakeAccountAbortsIf</a>{addr: @TreasuryCompliance}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateTreasuryComplianceAccountEnsures">CreateTreasuryComplianceAccountEnsures</a>; <b>let</b> account_ops_cap = <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot); <b>let</b> post post_account_ops_cap = <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot); <b>ensures</b> post_account_ops_cap == update_field(account_ops_cap, creation_events, account_ops_cap.creation_events); <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_MakeAccountEmits">MakeAccountEmits</a>{new_account_address: @TreasuryCompliance}; <b>aborts_if</b> <a href="VASPDomain.md#0x1_VASPDomain_tc_domain_manager_exists">VASPDomain::tc_domain_manager_exists</a>() <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; </code></pre><a name="0x1_DiemAccount_CreateTreasuryComplianceAccountModifies"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateTreasuryComplianceAccountModifies">CreateTreasuryComplianceAccountModifies</a> { <b>let</b> tc_addr = @TreasuryCompliance; <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(tc_addr); <b>modifies</b> <b>global</b><<a href="SlidingNonce.md#0x1_SlidingNonce_SlidingNonce">SlidingNonce::SlidingNonce</a>>(tc_addr); <b>modifies</b> <b>global</b><<a href="Roles.md#0x1_Roles_RoleId">Roles::RoleId</a>>(tc_addr); <b>modifies</b> <b>global</b><<a href="AccountFreezing.md#0x1_AccountFreezing_FreezingBit">AccountFreezing::FreezingBit</a>>(tc_addr); <b>modifies</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot); <b>ensures</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot); <b>modifies</b> <b>global</b><<a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_EventHandleGenerator">Event::EventHandleGenerator</a>>(@TreasuryCompliance); <b>modifies</b> <b>global</b><<a href="VASPDomain.md#0x1_VASPDomain_VASPDomainManager">VASPDomain::VASPDomainManager</a>>(tc_addr); } </code></pre><a name="0x1_DiemAccount_CreateTreasuryComplianceAccountAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateTreasuryComplianceAccountAbortsIf">CreateTreasuryComplianceAccountAbortsIf</a> { dr_account: signer; auth_key_prefix: vector<u8>; <b>include</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotGenesis">DiemTimestamp::AbortsIfNotGenesis</a>; <b>include</b> <a href="Roles.md#0x1_Roles_GrantRole">Roles::GrantRole</a>{addr: @TreasuryCompliance, role_id: <a href="Roles.md#0x1_Roles_TREASURY_COMPLIANCE_ROLE_ID">Roles::TREASURY_COMPLIANCE_ROLE_ID</a>}; <b>aborts_if</b> <b>exists</b><<a href="SlidingNonce.md#0x1_SlidingNonce_SlidingNonce">SlidingNonce::SlidingNonce</a>>(@TreasuryCompliance) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; <b>aborts_if</b> <a href="VASPDomain.md#0x1_VASPDomain_tc_domain_manager_exists">VASPDomain::tc_domain_manager_exists</a>() <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; } </code></pre><a name="0x1_DiemAccount_CreateTreasuryComplianceAccountEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateTreasuryComplianceAccountEnsures">CreateTreasuryComplianceAccountEnsures</a> { <b>let</b> tc_addr = @TreasuryCompliance; <b>ensures</b> <a href="Roles.md#0x1_Roles_spec_has_treasury_compliance_role_addr">Roles::spec_has_treasury_compliance_role_addr</a>(tc_addr); <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(tc_addr); <b>ensures</b> <b>exists</b><<a href="SlidingNonce.md#0x1_SlidingNonce_SlidingNonce">SlidingNonce::SlidingNonce</a>>(tc_addr); <b>ensures</b> <a href="AccountFreezing.md#0x1_AccountFreezing_spec_account_is_not_frozen">AccountFreezing::spec_account_is_not_frozen</a>(tc_addr); <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_own_key_rotation_cap">spec_holds_own_key_rotation_cap</a>(tc_addr); <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_own_withdraw_cap">spec_holds_own_withdraw_cap</a>(tc_addr); <b>ensures</b> <b>exists</b><<a href="VASPDomain.md#0x1_VASPDomain_VASPDomainManager">VASPDomain::VASPDomainManager</a>>(tc_addr); } </code></pre> </details><a name="0x1_DiemAccount_create_designated_dealer"></a>
create_designated_dealerCreate a designated dealer account at <code>new_account_address</code> with authentication key <code>auth_key_prefix</code> | <code>new_account_address</code>, for non synthetic CoinType. Creates Preburn resource under account 'new_account_address'
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_create_designated_dealer">create_designated_dealer</a><CoinType>(creator_account: &signer, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>, add_all_currencies: bool) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_create_designated_dealer">create_designated_dealer</a><CoinType>( creator_account: &signer, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>, add_all_currencies: bool, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_operating">DiemTimestamp::assert_operating</a>(); <a href="Roles.md#0x1_Roles_assert_treasury_compliance">Roles::assert_treasury_compliance</a>(creator_account); <b>let</b> new_dd_account = <a href="DiemAccount.md#0x1_DiemAccount_create_signer">create_signer</a>(new_account_address); <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_publish_generator">Event::publish_generator</a>(&new_dd_account); <a href="Roles.md#0x1_Roles_new_designated_dealer_role">Roles::new_designated_dealer_role</a>(creator_account, &new_dd_account); <a href="DesignatedDealer.md#0x1_DesignatedDealer_publish_designated_dealer_credential">DesignatedDealer::publish_designated_dealer_credential</a><CoinType>(&new_dd_account, creator_account, add_all_currencies); <a href="DualAttestation.md#0x1_DualAttestation_publish_credential">DualAttestation::publish_credential</a>(&new_dd_account, creator_account, human_name); <a href="DiemAccount.md#0x1_DiemAccount_make_account">make_account</a>(&new_dd_account, auth_key_prefix); <a href="DiemAccount.md#0x1_DiemAccount_add_currencies_for_account">add_currencies_for_account</a><CoinType>(&new_dd_account, add_all_currencies) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> disable_invariants_in_body; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateDesignatedDealerAbortsIf">CreateDesignatedDealerAbortsIf</a><CoinType>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateDesignatedDealerEnsures">CreateDesignatedDealerEnsures</a><CoinType>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_MakeAccountEmits">MakeAccountEmits</a>; </code></pre><a name="0x1_DiemAccount_CreateDesignatedDealerAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateDesignatedDealerAbortsIf">CreateDesignatedDealerAbortsIf</a><CoinType> { creator_account: signer; new_account_address: address; auth_key_prefix: vector<u8>; add_all_currencies: bool; <b>include</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>; <b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">Roles::AbortsIfNotTreasuryCompliance</a>{account: creator_account}; <b>aborts_if</b> <b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">Roles::RoleId</a>>(new_account_address) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; <b>aborts_if</b> <b>exists</b><<a href="DesignatedDealer.md#0x1_DesignatedDealer_Dealer">DesignatedDealer::Dealer</a>>(new_account_address) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; <b>include</b> <b>if</b> (add_all_currencies) <a href="DesignatedDealer.md#0x1_DesignatedDealer_AddCurrencyAbortsIf">DesignatedDealer::AddCurrencyAbortsIf</a><<a href="XUS.md#0x1_XUS">XUS</a>>{dd_addr: new_account_address} <b>else</b> <a href="DesignatedDealer.md#0x1_DesignatedDealer_AddCurrencyAbortsIf">DesignatedDealer::AddCurrencyAbortsIf</a><CoinType>{dd_addr: new_account_address}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyForAccountAbortsIf">AddCurrencyForAccountAbortsIf</a><CoinType>{addr: new_account_address}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_MakeAccountAbortsIf">MakeAccountAbortsIf</a>{addr: new_account_address}; } </code></pre><a name="0x1_DiemAccount_CreateDesignatedDealerEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateDesignatedDealerEnsures">CreateDesignatedDealerEnsures</a><CoinType> { new_account_address: address; <b>ensures</b> <b>exists</b><<a href="DesignatedDealer.md#0x1_DesignatedDealer_Dealer">DesignatedDealer::Dealer</a>>(new_account_address); <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(new_account_address); <b>ensures</b> <a href="Roles.md#0x1_Roles_spec_has_designated_dealer_role_addr">Roles::spec_has_designated_dealer_role_addr</a>(new_account_address); <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyForAccountEnsures">AddCurrencyForAccountEnsures</a><CoinType>{addr: new_account_address}; } </code></pre> </details><a name="0x1_DiemAccount_create_parent_vasp_account"></a>
create_parent_vasp_accountCreate an account with the ParentVASP role at <code>new_account_address</code> with authentication key <code>auth_key_prefix</code> | <code>new_account_address</code>. If <code>add_all_currencies</code> is true, 0 balances for all available currencies in the system will also be added.
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_create_parent_vasp_account">create_parent_vasp_account</a><Token>(creator_account: &signer, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>, add_all_currencies: bool) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_create_parent_vasp_account">create_parent_vasp_account</a><Token>( creator_account: &signer, // TreasuryCompliance new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>, add_all_currencies: bool ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> { <a href="Roles.md#0x1_Roles_assert_treasury_compliance">Roles::assert_treasury_compliance</a>(creator_account); <b>let</b> new_account = <a href="DiemAccount.md#0x1_DiemAccount_create_signer">create_signer</a>(new_account_address); <a href="Roles.md#0x1_Roles_new_parent_vasp_role">Roles::new_parent_vasp_role</a>(creator_account, &new_account); <a href="VASP.md#0x1_VASP_publish_parent_vasp_credential">VASP::publish_parent_vasp_credential</a>(&new_account, creator_account); <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_publish_generator">Event::publish_generator</a>(&new_account); <a href="DualAttestation.md#0x1_DualAttestation_publish_credential">DualAttestation::publish_credential</a>(&new_account, creator_account, human_name); <a href="VASPDomain.md#0x1_VASPDomain_publish_vasp_domains">VASPDomain::publish_vasp_domains</a>(&new_account); <a href="DiemAccount.md#0x1_DiemAccount_make_account">make_account</a>(&new_account, auth_key_prefix); <a href="DiemAccount.md#0x1_DiemAccount_add_currencies_for_account">add_currencies_for_account</a><Token>(&new_account, add_all_currencies); <b>spec</b> { <b>assert</b> <b>exists</b><<a href="VASPDomain.md#0x1_VASPDomain_VASPDomains">VASPDomain::VASPDomains</a>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(new_account)); <b>assert</b> <a href="Roles.md#0x1_Roles_spec_has_treasury_compliance_role_addr">Roles::spec_has_treasury_compliance_role_addr</a>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(creator_account)); } } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> disable_invariants_in_body; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateParentVASPAccountAbortsIf">CreateParentVASPAccountAbortsIf</a><Token>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateParentVASPAccountEnsures">CreateParentVASPAccountEnsures</a><Token>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_MakeAccountEmits">MakeAccountEmits</a>; </code></pre><a name="0x1_DiemAccount_CreateParentVASPAccountAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateParentVASPAccountAbortsIf">CreateParentVASPAccountAbortsIf</a><Token> { creator_account: signer; new_account_address: address; auth_key_prefix: vector<u8>; add_all_currencies: bool; <b>include</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>; <b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">Roles::AbortsIfNotTreasuryCompliance</a>{account: creator_account}; <b>include</b> <a href="VASPDomain.md#0x1_VASPDomain_PublishVASPDomainsAbortsIf">VASPDomain::PublishVASPDomainsAbortsIf</a>{vasp_addr: new_account_address}; <b>aborts_if</b> <b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">Roles::RoleId</a>>(new_account_address) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; <b>aborts_if</b> <a href="VASP.md#0x1_VASP_is_vasp">VASP::is_vasp</a>(new_account_address) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyForAccountAbortsIf">AddCurrencyForAccountAbortsIf</a><Token>{addr: new_account_address}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_MakeAccountAbortsIf">MakeAccountAbortsIf</a>{addr: new_account_address}; } </code></pre><a name="0x1_DiemAccount_CreateParentVASPAccountEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateParentVASPAccountEnsures">CreateParentVASPAccountEnsures</a><Token> { new_account_address: address; <b>include</b> <a href="VASP.md#0x1_VASP_PublishParentVASPEnsures">VASP::PublishParentVASPEnsures</a>{vasp_addr: new_account_address}; <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(new_account_address); <b>ensures</b> <a href="Roles.md#0x1_Roles_spec_has_parent_VASP_role_addr">Roles::spec_has_parent_VASP_role_addr</a>(new_account_address); <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyForAccountEnsures">AddCurrencyForAccountEnsures</a><Token>{addr: new_account_address}; <b>include</b> <a href="VASPDomain.md#0x1_VASPDomain_PublishVASPDomainsEnsures">VASPDomain::PublishVASPDomainsEnsures</a>{ vasp_addr: new_account_address }; } </code></pre> </details><a name="0x1_DiemAccount_create_child_vasp_account"></a>
create_child_vasp_accountCreate an account with the ChildVASP role at <code>new_account_address</code> with authentication key <code>auth_key_prefix</code> | <code>new_account_address</code> and a 0 balance of type <code>Token</code>. If <code>add_all_currencies</code> is true, 0 balances for all avaialable currencies in the system will also be added. This account will be a child of <code>creator</code>, which must be a ParentVASP.
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_create_child_vasp_account">create_child_vasp_account</a><Token>(parent: &signer, new_account_address: address, auth_key_prefix: vector<u8>, add_all_currencies: bool) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_create_child_vasp_account">create_child_vasp_account</a><Token>( parent: &signer, new_account_address: address, auth_key_prefix: vector<u8>, add_all_currencies: bool, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_operating">DiemTimestamp::assert_operating</a>(); <a href="Roles.md#0x1_Roles_assert_parent_vasp_role">Roles::assert_parent_vasp_role</a>(parent); <b>let</b> new_account = <a href="DiemAccount.md#0x1_DiemAccount_create_signer">create_signer</a>(new_account_address); <a href="Roles.md#0x1_Roles_new_child_vasp_role">Roles::new_child_vasp_role</a>(parent, &new_account); <a href="VASP.md#0x1_VASP_publish_child_vasp_credential">VASP::publish_child_vasp_credential</a>( parent, &new_account, ); <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_publish_generator">Event::publish_generator</a>(&new_account); <a href="DiemAccount.md#0x1_DiemAccount_make_account">make_account</a>(&new_account, auth_key_prefix); <a href="DiemAccount.md#0x1_DiemAccount_add_currencies_for_account">add_currencies_for_account</a><Token>(&new_account, add_all_currencies); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> disable_invariants_in_body; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateChildVASPAccountAbortsIf">CreateChildVASPAccountAbortsIf</a><Token>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateChildVASPAccountEnsures">CreateChildVASPAccountEnsures</a><Token>{ parent_addr: <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(parent), child_addr: new_account_address, }; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyForAccountEnsures">AddCurrencyForAccountEnsures</a><Token>{addr: new_account_address}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_MakeAccountEmits">MakeAccountEmits</a>; </code></pre><a name="0x1_DiemAccount_CreateChildVASPAccountAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateChildVASPAccountAbortsIf">CreateChildVASPAccountAbortsIf</a><Token> { parent: signer; new_account_address: address; auth_key_prefix: vector<u8>; add_all_currencies: bool; <b>include</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>; <b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotParentVasp">Roles::AbortsIfNotParentVasp</a>{account: parent}; <b>aborts_if</b> <b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">Roles::RoleId</a>>(new_account_address) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; <b>include</b> <a href="VASP.md#0x1_VASP_PublishChildVASPAbortsIf">VASP::PublishChildVASPAbortsIf</a>{child_addr: new_account_address}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyForAccountAbortsIf">AddCurrencyForAccountAbortsIf</a><Token>{addr: new_account_address}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_MakeAccountAbortsIf">MakeAccountAbortsIf</a>{addr: new_account_address}; } </code></pre><a name="0x1_DiemAccount_CreateChildVASPAccountEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateChildVASPAccountEnsures">CreateChildVASPAccountEnsures</a><Token> { parent_addr: address; child_addr: address; add_all_currencies: bool; <b>include</b> <a href="VASP.md#0x1_VASP_PublishChildVASPEnsures">VASP::PublishChildVASPEnsures</a>; <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(child_addr); <b>ensures</b> <a href="Roles.md#0x1_Roles_spec_has_child_VASP_role_addr">Roles::spec_has_child_VASP_role_addr</a>(child_addr); } </code></pre> </details><a name="0x1_DiemAccount_create_signer"></a>
create_signer<a name="0x1_DiemAccount_publish_crsn"></a>
publish_crsn<a name="0x1_DiemAccount_balance_for"></a>
balance_forHelper to return the u64 value of the <code>balance</code> for <code>account</code>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_balance_for">balance_for</a><Token>(balance: &<a href="DiemAccount.md#0x1_DiemAccount_Balance">DiemAccount::Balance</a><Token>): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_balance_for">balance_for</a><Token>(balance: &<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>): u64 { <a href="Diem.md#0x1_Diem_value">Diem::value</a><Token>(&balance.coin) } </code></pre> </details><a name="0x1_DiemAccount_balance"></a>
balanceReturn the current balance of the account at <code>addr</code>.
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_balance">balance</a><Token>(addr: address): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_balance">balance</a><Token>(addr: address): u64 <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a> { <b>assert</b>(<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EPAYER_DOESNT_HOLD_CURRENCY">EPAYER_DOESNT_HOLD_CURRENCY</a>)); <a href="DiemAccount.md#0x1_DiemAccount_balance_for">balance_for</a>(borrow_global<<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(addr)) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>aborts_if</b> !<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; </code></pre> </details><a name="0x1_DiemAccount_add_currency"></a>
add_currencyAdd a balance of <code>Token</code> type to the sending account
<pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_add_currency">add_currency</a><Token>(account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b>(<b>friend</b>) <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_add_currency">add_currency</a><Token>(account: &signer) { <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); // aborts <b>if</b> `Token` is not a currency type in the system <a href="Diem.md#0x1_Diem_assert_is_currency">Diem::assert_is_currency</a><Token>(); <b>assert</b>(<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EACCOUNT">EACCOUNT</a>)); // Check that an account <b>with</b> this role is allowed <b>to</b> hold funds <b>assert</b>( <a href="Roles.md#0x1_Roles_can_hold_balance">Roles::can_hold_balance</a>(account), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemAccount.md#0x1_DiemAccount_EROLE_CANT_STORE_BALANCE">EROLE_CANT_STORE_BALANCE</a>) ); // aborts <b>if</b> this account already has a balance in `Token` <b>assert</b>( !<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_already_published">Errors::already_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EADD_EXISTING_CURRENCY">EADD_EXISTING_CURRENCY</a>) ); move_to(account, <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>{ coin: <a href="Diem.md#0x1_Diem_zero">Diem::zero</a><Token>() }) } </code></pre> </details> <details> <summary>Specification</summary>An account must exist at the address
<pre><code><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> !<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyAbortsIf">AddCurrencyAbortsIf</a><Token>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyEnsures">AddCurrencyEnsures</a><Token>; </code></pre><a name="0x1_DiemAccount_AddCurrencyAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyAbortsIf">AddCurrencyAbortsIf</a><Token> { account: signer; } </code></pre><code>Currency</code> must be valid
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyAbortsIf">AddCurrencyAbortsIf</a><Token> { <b>include</b> <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">Diem::AbortsIfNoCurrency</a><Token>; } </code></pre><code>account</code> cannot have an existing balance in <code>Currency</code>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyAbortsIf">AddCurrencyAbortsIf</a><Token> { <b>aborts_if</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account)) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; } </code></pre><code>account</code> must be allowed to hold balances.
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyAbortsIf">AddCurrencyAbortsIf</a><Token> { <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_AbortsIfAccountCantHoldBalance">AbortsIfAccountCantHoldBalance</a>; } </code></pre><a name="0x1_DiemAccount_AddCurrencyEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyEnsures">AddCurrencyEnsures</a><Token> { addr: address; } </code></pre>This publishes a <code><a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Currency></code> to the caller's account
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_AddCurrencyEnsures">AddCurrencyEnsures</a><Token> { <b>ensures</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(addr); <b>ensures</b> <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(addr) == <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>{ coin: <a href="Diem.md#0x1_Diem">Diem</a><Token> { value: 0 } }; } </code></pre> </details><a name="0x1_DiemAccount_add_currency_for_test"></a>
add_currency_for_test<a name="@Access_Control_3"></a>
<a name="0x1_DiemAccount_AbortsIfAccountCantHoldBalance"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_AbortsIfAccountCantHoldBalance">AbortsIfAccountCantHoldBalance</a> { account: signer; } </code></pre>This function must abort if the predicate <code>can_hold_balance</code> for <code>account</code> returns false [D1][D2][D3][D4][D5][D6][D7].
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_AbortsIfAccountCantHoldBalance">AbortsIfAccountCantHoldBalance</a> { <b>aborts_if</b> !<a href="Roles.md#0x1_Roles_can_hold_balance">Roles::can_hold_balance</a>(account) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre> </details><a name="0x1_DiemAccount_accepts_currency"></a>
accepts_currencyReturn whether the account at <code>addr</code> accepts <code>Token</code> type coins
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_accepts_currency">accepts_currency</a><Token>(addr: address): bool </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_accepts_currency">accepts_currency</a><Token>(addr: address): bool { <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(addr) } </code></pre> </details><a name="0x1_DiemAccount_sequence_number_for_account"></a>
sequence_number_for_accountHelper to return the sequence number field for given <code>account</code>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_sequence_number_for_account">sequence_number_for_account</a>(account: &<a href="DiemAccount.md#0x1_DiemAccount_DiemAccount">DiemAccount::DiemAccount</a>): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_sequence_number_for_account">sequence_number_for_account</a>(account: &<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>): u64 { account.sequence_number } </code></pre> </details><a name="0x1_DiemAccount_sequence_number"></a>
sequence_numberReturn the current sequence number at <code>addr</code>
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_sequence_number">sequence_number</a>(addr: address): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_sequence_number">sequence_number</a>(addr: address): u64 <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a> { <b>assert</b>(<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EACCOUNT">EACCOUNT</a>)); <a href="DiemAccount.md#0x1_DiemAccount_sequence_number_for_account">sequence_number_for_account</a>(borrow_global<<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr)) } </code></pre> </details><a name="0x1_DiemAccount_authentication_key"></a>
authentication_keyReturn the authentication key for this account
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_authentication_key">authentication_key</a>(addr: address): vector<u8> </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_authentication_key">authentication_key</a>(addr: address): vector<u8> <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a> { <b>assert</b>(<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EACCOUNT">EACCOUNT</a>)); *&borrow_global<<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr).authentication_key } </code></pre> </details><a name="0x1_DiemAccount_delegated_key_rotation_capability"></a>
delegated_key_rotation_capabilityReturn true if the account at <code>addr</code> has delegated its key rotation capability
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_delegated_key_rotation_capability">delegated_key_rotation_capability</a>(addr: address): bool </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_delegated_key_rotation_capability">delegated_key_rotation_capability</a>(addr: address): bool <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a> { <b>assert</b>(<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EACCOUNT">EACCOUNT</a>)); <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_is_none">Option::is_none</a>(&borrow_global<<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr).key_rotation_capability) } </code></pre> </details><a name="0x1_DiemAccount_delegated_withdraw_capability"></a>
delegated_withdraw_capabilityReturn true if the account at <code>addr</code> has delegated its withdraw capability
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_delegated_withdraw_capability">delegated_withdraw_capability</a>(addr: address): bool </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_delegated_withdraw_capability">delegated_withdraw_capability</a>(addr: address): bool <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a> { <b>assert</b>(<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="DiemAccount.md#0x1_DiemAccount_EACCOUNT">EACCOUNT</a>)); <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_is_none">Option::is_none</a>(&borrow_global<<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr).withdraw_capability) } </code></pre> </details><a name="0x1_DiemAccount_withdraw_capability_address"></a>
withdraw_capability_addressReturn a reference to the address associated with the given withdraw capability
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_withdraw_capability_address">withdraw_capability_address</a>(cap: &<a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">DiemAccount::WithdrawCapability</a>): &address </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_withdraw_capability_address">withdraw_capability_address</a>(cap: &<a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a>): &address { &cap.account_address } </code></pre> </details><a name="0x1_DiemAccount_key_rotation_capability_address"></a>
key_rotation_capability_addressReturn a reference to the address associated with the given key rotation capability
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_key_rotation_capability_address">key_rotation_capability_address</a>(cap: &<a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">DiemAccount::KeyRotationCapability</a>): &address </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_key_rotation_capability_address">key_rotation_capability_address</a>(cap: &<a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">KeyRotationCapability</a>): &address { &cap.account_address } </code></pre> </details><a name="0x1_DiemAccount_exists_at"></a>
exists_atChecks if an account exists at <code>check_addr</code>
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(check_addr: address): bool </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(check_addr: address): bool { <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(check_addr) } </code></pre> </details><a name="0x1_DiemAccount_module_prologue"></a>
module_prologueThe prologue for module transaction
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_module_prologue">module_prologue</a><Token>(sender: signer, txn_sequence_number: u64, txn_public_key: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_module_prologue">module_prologue</a><Token>( sender: signer, txn_sequence_number: u64, txn_public_key: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>, <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a> { <b>assert</b>( <a href="DiemTransactionPublishingOption.md#0x1_DiemTransactionPublishingOption_is_module_allowed">DiemTransactionPublishingOption::is_module_allowed</a>(&sender), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(<a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_EMODULE_NOT_ALLOWED">PROLOGUE_EMODULE_NOT_ALLOWED</a>), ); <a href="DiemAccount.md#0x1_DiemAccount_prologue_common">prologue_common</a><Token>( &sender, txn_sequence_number, txn_public_key, txn_gas_price, txn_max_gas_units, txn_expiration_time, chain_id, ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>let</b> transaction_sender = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(sender); <b>let</b> max_transaction_fee = txn_gas_price * txn_max_gas_units; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_ModulePrologueAbortsIf">ModulePrologueAbortsIf</a><Token> { max_transaction_fee, txn_expiration_time_seconds: txn_expiration_time, }; <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_prologue_guarantees">prologue_guarantees</a>(sender); </code></pre><a name="0x1_DiemAccount_ModulePrologueAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_ModulePrologueAbortsIf">ModulePrologueAbortsIf</a><Token> { sender: signer; txn_sequence_number: u64; txn_public_key: vector<u8>; chain_id: u8; max_transaction_fee: u128; txn_expiration_time_seconds: u64; <b>let</b> transaction_sender = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(sender); <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> { transaction_sender, txn_sequence_number, txn_public_key, chain_id, max_transaction_fee, txn_expiration_time_seconds, }; } </code></pre>Aborts only in genesis. Does not need to be handled.
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_ModulePrologueAbortsIf">ModulePrologueAbortsIf</a><Token> { <b>include</b> <a href="DiemTransactionPublishingOption.md#0x1_DiemTransactionPublishingOption_AbortsIfNoTransactionPublishingOption">DiemTransactionPublishingOption::AbortsIfNoTransactionPublishingOption</a>; } </code></pre>Covered: L75 (Match 9)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_ModulePrologueAbortsIf">ModulePrologueAbortsIf</a><Token> { <b>aborts_if</b> !<a href="DiemTransactionPublishingOption.md#0x1_DiemTransactionPublishingOption_spec_is_module_allowed">DiemTransactionPublishingOption::spec_is_module_allowed</a>(sender) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_STATE">Errors::INVALID_STATE</a>; } </code></pre> </details><a name="0x1_DiemAccount_script_prologue"></a>
script_prologueThe prologue for script transaction
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_script_prologue">script_prologue</a><Token>(sender: signer, txn_sequence_number: u64, txn_public_key: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, script_hash: vector<u8>) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_script_prologue">script_prologue</a><Token>( sender: signer, txn_sequence_number: u64, txn_public_key: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, script_hash: vector<u8>, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>, <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a> { <b>assert</b>( <a href="DiemTransactionPublishingOption.md#0x1_DiemTransactionPublishingOption_is_script_allowed">DiemTransactionPublishingOption::is_script_allowed</a>(&sender, &script_hash), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(<a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_ESCRIPT_NOT_ALLOWED">PROLOGUE_ESCRIPT_NOT_ALLOWED</a>), ); <a href="DiemAccount.md#0x1_DiemAccount_prologue_common">prologue_common</a><Token>( &sender, txn_sequence_number, txn_public_key, txn_gas_price, txn_max_gas_units, txn_expiration_time, chain_id, ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>let</b> transaction_sender = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(sender); <b>let</b> max_transaction_fee = txn_gas_price * txn_max_gas_units; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_ScriptPrologueAbortsIf">ScriptPrologueAbortsIf</a><Token>{ max_transaction_fee, txn_expiration_time_seconds: txn_expiration_time, }; <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_prologue_guarantees">prologue_guarantees</a>(sender); </code></pre><a name="0x1_DiemAccount_ScriptPrologueAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_ScriptPrologueAbortsIf">ScriptPrologueAbortsIf</a><Token> { sender: signer; txn_sequence_number: u64; txn_public_key: vector<u8>; chain_id: u8; max_transaction_fee: u128; txn_expiration_time_seconds: u64; script_hash: vector<u8>; <b>let</b> transaction_sender = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(sender); <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> {transaction_sender}; } </code></pre>Aborts only in Genesis. Does not need to be handled.
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_ScriptPrologueAbortsIf">ScriptPrologueAbortsIf</a><Token> { <b>include</b> <a href="DiemTransactionPublishingOption.md#0x1_DiemTransactionPublishingOption_AbortsIfNoTransactionPublishingOption">DiemTransactionPublishingOption::AbortsIfNoTransactionPublishingOption</a>; } </code></pre>Covered: L74 (Match 8)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_ScriptPrologueAbortsIf">ScriptPrologueAbortsIf</a><Token> { <b>aborts_if</b> !<a href="DiemTransactionPublishingOption.md#0x1_DiemTransactionPublishingOption_spec_is_script_allowed">DiemTransactionPublishingOption::spec_is_script_allowed</a>(sender, script_hash) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_STATE">Errors::INVALID_STATE</a>; } </code></pre> </details><a name="0x1_DiemAccount_writeset_prologue"></a>
writeset_prologueThe prologue for WriteSet transaction
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_writeset_prologue">writeset_prologue</a>(sender: signer, txn_sequence_number: u64, txn_public_key: vector<u8>, txn_expiration_time: u64, chain_id: u8) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_writeset_prologue">writeset_prologue</a>( sender: signer, txn_sequence_number: u64, txn_public_key: vector<u8>, txn_expiration_time: u64, chain_id: u8, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>, <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a> { <b>assert</b>( <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(&sender) == @DiemRoot, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_EINVALID_WRITESET_SENDER">PROLOGUE_EINVALID_WRITESET_SENDER</a>) ); <b>assert</b>(<a href="Roles.md#0x1_Roles_has_diem_root_role">Roles::has_diem_root_role</a>(&sender), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_EINVALID_WRITESET_SENDER">PROLOGUE_EINVALID_WRITESET_SENDER</a>)); // Currency code don't matter here <b>as</b> it won't be charged anyway. Gas constants are ommitted. <a href="DiemAccount.md#0x1_DiemAccount_prologue_common">prologue_common</a><<a href="XUS.md#0x1_XUS">XUS</a>>( &sender, txn_sequence_number, txn_public_key, 0, 0, txn_expiration_time, chain_id, ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_WritesetPrologueAbortsIf">WritesetPrologueAbortsIf</a> {txn_expiration_time_seconds: txn_expiration_time}; <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_prologue_guarantees">prologue_guarantees</a>(sender); <b>ensures</b> <a href="Roles.md#0x1_Roles_has_diem_root_role">Roles::has_diem_root_role</a>(sender); </code></pre><a name="0x1_DiemAccount_WritesetPrologueAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_WritesetPrologueAbortsIf">WritesetPrologueAbortsIf</a> { sender: signer; txn_sequence_number: u64; txn_public_key: vector<u8>; txn_expiration_time_seconds: u64; chain_id: u8; <b>let</b> transaction_sender = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(sender); } </code></pre>Covered: L146 (Match 0)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_WritesetPrologueAbortsIf">WritesetPrologueAbortsIf</a> { <b>aborts_if</b> transaction_sender != @DiemRoot <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>Must abort if the signer does not have the DiemRoot role [H9]. Covered: L146 (Match 0)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_WritesetPrologueAbortsIf">WritesetPrologueAbortsIf</a> { <b>aborts_if</b> !<a href="Roles.md#0x1_Roles_spec_has_diem_root_role_addr">Roles::spec_has_diem_root_role_addr</a>(transaction_sender) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><<a href="XUS.md#0x1_XUS">XUS</a>>{ transaction_sender, max_transaction_fee: 0, }; } </code></pre> </details><a name="0x1_DiemAccount_multi_agent_script_prologue"></a>
multi_agent_script_prologueThe prologue for multi-agent user transactions
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_multi_agent_script_prologue">multi_agent_script_prologue</a><Token>(sender: signer, txn_sequence_number: u64, txn_sender_public_key: vector<u8>, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<vector<u8>>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_multi_agent_script_prologue">multi_agent_script_prologue</a><Token>( sender: signer, txn_sequence_number: u64, txn_sender_public_key: vector<u8>, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<vector<u8>>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>, <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a> { <b>let</b> num_secondary_signers = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(&secondary_signer_addresses); // Number of <b>public</b> key hashes must match the number of secondary signers. <b>assert</b>( <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(&secondary_signer_public_key_hashes) == num_secondary_signers, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_ESECONDARY_KEYS_ADDRESSES_COUNT_MISMATCH">PROLOGUE_ESECONDARY_KEYS_ADDRESSES_COUNT_MISMATCH</a>), ); <b>let</b> i = 0; <b>while</b> ({ <b>spec</b> { <b>invariant</b> <b>forall</b> j in 0..i: <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(secondary_signer_addresses[j]); <b>invariant</b> <b>forall</b> j in 0..i: secondary_signer_public_key_hashes[j] == <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(secondary_signer_addresses[j]).authentication_key; }; (i < num_secondary_signers) }) { // Check that all secondary signers have accounts. <b>let</b> secondary_address = *<a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_borrow">Vector::borrow</a>(&secondary_signer_addresses, i); <b>assert</b>(<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(secondary_address), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_EACCOUNT_DNE">PROLOGUE_EACCOUNT_DNE</a>)); // Check that for each secondary signer, the provided <b>public</b> key hash // is equal <b>to</b> the authentication key stored on-chain. <b>let</b> signer_account = borrow_global<<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(secondary_address); <b>let</b> signer_public_key_hash = *<a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_borrow">Vector::borrow</a>(&secondary_signer_public_key_hashes, i); <b>assert</b>( signer_public_key_hash == *&signer_account.authentication_key, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_EINVALID_ACCOUNT_AUTH_KEY">PROLOGUE_EINVALID_ACCOUNT_AUTH_KEY</a>), ); i = i + 1; }; <b>spec</b> { <b>assert</b> <b>forall</b> j in 0..num_secondary_signers: <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(secondary_signer_addresses[j]); <b>assert</b> <b>forall</b> j in 0..num_secondary_signers: secondary_signer_public_key_hashes[j] == <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(secondary_signer_addresses[j]).authentication_key; }; <a href="DiemAccount.md#0x1_DiemAccount_prologue_common">prologue_common</a><Token>( &sender, txn_sequence_number, txn_sender_public_key, txn_gas_price, txn_max_gas_units, txn_expiration_time, chain_id, ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>let</b> transaction_sender = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(sender); <b>let</b> max_transaction_fee = txn_gas_price * txn_max_gas_units; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_MultiAgentScriptPrologueAbortsIf">MultiAgentScriptPrologueAbortsIf</a><Token>{ max_transaction_fee, txn_expiration_time_seconds: txn_expiration_time, }; <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_prologue_guarantees">prologue_guarantees</a>(sender); </code></pre><a name="0x1_DiemAccount_MultiAgentScriptPrologueAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_MultiAgentScriptPrologueAbortsIf">MultiAgentScriptPrologueAbortsIf</a><Token> { sender: signer; txn_sequence_number: u64; txn_sender_public_key: vector<u8>; secondary_signer_addresses: vector<address>; secondary_signer_public_key_hashes: vector<vector<u8>>; chain_id: u8; max_transaction_fee: u128; txn_expiration_time_seconds: u64; <b>let</b> transaction_sender = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(sender); <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> {transaction_sender, txn_public_key: txn_sender_public_key}; <b>aborts_if</b> len(secondary_signer_addresses) != len(secondary_signer_public_key_hashes) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; <b>let</b> num_secondary_signers = len(secondary_signer_addresses); <b>aborts_if</b> <b>exists</b> i in 0..num_secondary_signers: !<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(secondary_signer_addresses[i]) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; <b>aborts_if</b> <b>exists</b> i in 0..num_secondary_signers: secondary_signer_public_key_hashes[i] != <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(secondary_signer_addresses[i]).authentication_key <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre> </details><a name="0x1_DiemAccount_prologue_common"></a>
prologue_commonThe common prologue is invoked at the beginning of every transaction The main properties that it verifies:
<a name="0x1_DiemAccount_PrologueCommonAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> { transaction_sender: address; txn_sequence_number: u64; txn_public_key: vector<u8>; chain_id: u8; max_transaction_fee: u128; txn_expiration_time_seconds: u64; } </code></pre>Only happens if this is called in Genesis. Doesn't need to be handled.
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> { <b>include</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>; } </code></pre>[PCA1] Covered: L73 (Match 7)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> { <b>aborts_if</b> chain_id != <a href="ChainId.md#0x1_ChainId_spec_get_chain_id">ChainId::spec_get_chain_id</a>() <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>[PCA2] Covered: L65 (Match 4)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> { <b>aborts_if</b> !<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(transaction_sender) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>[PCA3] Covered: L57 (Match 0)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> { <b>aborts_if</b> <a href="AccountFreezing.md#0x1_AccountFreezing_spec_account_is_frozen">AccountFreezing::spec_account_is_frozen</a>(transaction_sender) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_STATE">Errors::INVALID_STATE</a>; } </code></pre>[PCA4] Covered: L59 (Match 1)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> { <b>aborts_if</b> <a href="../../../../../../move-stdlib/docs/Hash.md#0x1_Hash_sha3_256">Hash::sha3_256</a>(txn_public_key) != <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(transaction_sender).authentication_key <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>[PCA5] Covered: L69 (Match 5)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> { <b>aborts_if</b> max_transaction_fee > <a href="DiemAccount.md#0x1_DiemAccount_MAX_U64">MAX_U64</a> <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>[PCA6] Covered: L69 (Match 5)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> { <b>aborts_if</b> max_transaction_fee > 0 && !<a href="TransactionFee.md#0x1_TransactionFee_is_coin_initialized">TransactionFee::is_coin_initialized</a><Token>() <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>[PCA7] Covered: L69 (Match 5)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> { <b>aborts_if</b> max_transaction_fee > 0 && !<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(transaction_sender) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>[PCA8] Covered: L69 (Match 5)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> { <b>aborts_if</b> max_transaction_fee > 0 && <a href="DiemAccount.md#0x1_DiemAccount_balance">balance</a><Token>(transaction_sender) < max_transaction_fee <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>[PCA9] Covered: L72 (Match 6)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> { <b>aborts_if</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_spec_now_seconds">DiemTimestamp::spec_now_seconds</a>() >= txn_expiration_time_seconds <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>[PCA10] Covered: L81 (match 11)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> { <b>aborts_if</b> txn_sequence_number >= <a href="DiemAccount.md#0x1_DiemAccount_MAX_U64">MAX_U64</a> <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre>[PCA11] Covered: L61 (Match 2)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> { <b>aborts_if</b> !<a href="CRSN.md#0x1_CRSN_has_crsn">CRSN::has_crsn</a>(transaction_sender) && txn_sequence_number < <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(transaction_sender).sequence_number <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>[PCA12] Covered: L63 (match 3)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> { <b>aborts_if</b> !<a href="CRSN.md#0x1_CRSN_has_crsn">CRSN::has_crsn</a>(transaction_sender) && txn_sequence_number > <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(transaction_sender).sequence_number <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>[PCA13] Covered: L93 (match 14)
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PrologueCommonAbortsIf">PrologueCommonAbortsIf</a><Token> { <b>aborts_if</b> <a href="CRSN.md#0x1_CRSN_has_crsn">CRSN::has_crsn</a>(transaction_sender) && !<a href="CRSN.md#0x1_CRSN_spec_check">CRSN::spec_check</a>(transaction_sender, txn_sequence_number) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre> </details><a name="0x1_DiemAccount_epilogue"></a>
epilogueCollects gas and bumps the sequence number for executing a transaction. The epilogue is invoked at the end of the transaction. If the exection of the epilogue fails, it is re-invoked with different arguments, and based on the conditions checked in the prologue, should never fail.
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_epilogue">epilogue</a><Token>(account: signer, txn_sequence_number: u64, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_epilogue">epilogue</a><Token>( account: signer, txn_sequence_number: u64, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64 ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>, <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a> { <a href="DiemAccount.md#0x1_DiemAccount_epilogue_common">epilogue_common</a><Token>( &account, txn_sequence_number, txn_gas_price, txn_max_gas_units, gas_units_remaining, ) } </code></pre> </details><a name="0x1_DiemAccount_epilogue_common"></a>
epilogue_common<a name="0x1_DiemAccount_writeset_epilogue"></a>
writeset_epilogueEpilogue for WriteSet trasnaction
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_writeset_epilogue">writeset_epilogue</a>(dr_account: signer, txn_sequence_number: u64, should_trigger_reconfiguration: bool) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_writeset_epilogue">writeset_epilogue</a>( dr_account: signer, txn_sequence_number: u64, should_trigger_reconfiguration: bool, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount_DiemWriteSetManager">DiemWriteSetManager</a>, <a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>, <a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a> { <b>let</b> dr_account = &dr_account; <b>let</b> writeset_events_ref = borrow_global_mut<<a href="DiemAccount.md#0x1_DiemAccount_DiemWriteSetManager">DiemWriteSetManager</a>>(@DiemRoot); <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_emit_event">Event::emit_event</a><<a href="DiemAccount.md#0x1_DiemAccount_AdminTransactionEvent">AdminTransactionEvent</a>>( &<b>mut</b> writeset_events_ref.upgrade_events, <a href="DiemAccount.md#0x1_DiemAccount_AdminTransactionEvent">AdminTransactionEvent</a> { committed_timestamp_secs: <a href="DiemTimestamp.md#0x1_DiemTimestamp_now_seconds">DiemTimestamp::now_seconds</a>() }, ); // Double check that the sender is the DiemRoot account at the `@DiemRoot` <b>assert</b>( <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(dr_account) == @DiemRoot, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_EINVALID_WRITESET_SENDER">PROLOGUE_EINVALID_WRITESET_SENDER</a>) ); <b>assert</b>( <a href="Roles.md#0x1_Roles_has_diem_root_role">Roles::has_diem_root_role</a>(dr_account), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="DiemAccount.md#0x1_DiemAccount_PROLOGUE_EINVALID_WRITESET_SENDER">PROLOGUE_EINVALID_WRITESET_SENDER</a>) ); // Currency code don't matter here <b>as</b> it won't be charged anyway. <a href="DiemAccount.md#0x1_DiemAccount_epilogue_common">epilogue_common</a><<a href="XUS.md#0x1_XUS">XUS</a>>(dr_account, txn_sequence_number, 0, 0, 0); <b>if</b> (should_trigger_reconfiguration) <a href="DiemConfig.md#0x1_DiemConfig_reconfigure">DiemConfig::reconfigure</a>(dr_account) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_WritesetEpilogueEmits">WritesetEpilogueEmits</a>; </code></pre><a name="0x1_DiemAccount_WritesetEpilogueEmits"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_WritesetEpilogueEmits">WritesetEpilogueEmits</a> { should_trigger_reconfiguration: bool; <b>let</b> handle = <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_DiemWriteSetManager">DiemWriteSetManager</a>>(@DiemRoot).upgrade_events; <b>let</b> msg = <a href="DiemAccount.md#0x1_DiemAccount_AdminTransactionEvent">AdminTransactionEvent</a> { committed_timestamp_secs: <a href="DiemTimestamp.md#0x1_DiemTimestamp_spec_now_seconds">DiemTimestamp::spec_now_seconds</a>() }; emits msg <b>to</b> handle; <b>include</b> should_trigger_reconfiguration ==> <a href="DiemConfig.md#0x1_DiemConfig_ReconfigureEmits">DiemConfig::ReconfigureEmits</a>; } </code></pre> </details><a name="0x1_DiemAccount_create_validator_account"></a>
create_validator_accountCreate a Validator account
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_create_validator_account">create_validator_account</a>(dr_account: &signer, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_create_validator_account">create_validator_account</a>( dr_account: &signer, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> { <a href="Roles.md#0x1_Roles_assert_diem_root">Roles::assert_diem_root</a>(dr_account); <b>let</b> new_account = <a href="DiemAccount.md#0x1_DiemAccount_create_signer">create_signer</a>(new_account_address); // The dr_account account is verified <b>to</b> have the diem root role in `<a href="Roles.md#0x1_Roles_new_validator_role">Roles::new_validator_role</a>` <a href="Roles.md#0x1_Roles_new_validator_role">Roles::new_validator_role</a>(dr_account, &new_account); <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_publish_generator">Event::publish_generator</a>(&new_account); <a href="ValidatorConfig.md#0x1_ValidatorConfig_publish">ValidatorConfig::publish</a>(&new_account, dr_account, human_name); <a href="DiemAccount.md#0x1_DiemAccount_make_account">make_account</a>(&new_account, auth_key_prefix) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> disable_invariants_in_body; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateValidatorAccountAbortsIf">CreateValidatorAccountAbortsIf</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateValidatorAccountEnsures">CreateValidatorAccountEnsures</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_MakeAccountEmits">MakeAccountEmits</a>; </code></pre><a name="0x1_DiemAccount_CreateValidatorAccountAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateValidatorAccountAbortsIf">CreateValidatorAccountAbortsIf</a> { dr_account: signer; new_account_address: address; <b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">Roles::AbortsIfNotDiemRoot</a>{account: dr_account}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_MakeAccountAbortsIf">MakeAccountAbortsIf</a>{addr: new_account_address}; <b>include</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>; <b>aborts_if</b> <a href="ValidatorConfig.md#0x1_ValidatorConfig_exists_config">ValidatorConfig::exists_config</a>(new_account_address) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; } </code></pre><a name="0x1_DiemAccount_CreateValidatorAccountEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateValidatorAccountEnsures">CreateValidatorAccountEnsures</a> { new_account_address: address; <b>include</b> <a href="Roles.md#0x1_Roles_GrantRole">Roles::GrantRole</a>{addr: new_account_address, role_id: <a href="Roles.md#0x1_Roles_VALIDATOR_ROLE_ID">Roles::VALIDATOR_ROLE_ID</a>}; <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(new_account_address); <b>ensures</b> <a href="ValidatorConfig.md#0x1_ValidatorConfig_exists_config">ValidatorConfig::exists_config</a>(new_account_address); } </code></pre> </details><a name="0x1_DiemAccount_create_validator_operator_account"></a>
create_validator_operator_accountCreate a Validator Operator account
<pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_create_validator_operator_account">create_validator_operator_account</a>(dr_account: &signer, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>) </code></pre> <details> <summary>Implementation</summary> <pre><code><b>public</b> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_create_validator_operator_account">create_validator_operator_account</a>( dr_account: &signer, new_account_address: address, auth_key_prefix: vector<u8>, human_name: vector<u8>, ) <b>acquires</b> <a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a> { <a href="Roles.md#0x1_Roles_assert_diem_root">Roles::assert_diem_root</a>(dr_account); <b>let</b> new_account = <a href="DiemAccount.md#0x1_DiemAccount_create_signer">create_signer</a>(new_account_address); // The dr_account is verified <b>to</b> have the diem root role in `<a href="Roles.md#0x1_Roles_new_validator_operator_role">Roles::new_validator_operator_role</a>` <a href="Roles.md#0x1_Roles_new_validator_operator_role">Roles::new_validator_operator_role</a>(dr_account, &new_account); <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_publish_generator">Event::publish_generator</a>(&new_account); <a href="ValidatorOperatorConfig.md#0x1_ValidatorOperatorConfig_publish">ValidatorOperatorConfig::publish</a>(&new_account, dr_account, human_name); <a href="DiemAccount.md#0x1_DiemAccount_make_account">make_account</a>(&new_account, auth_key_prefix) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code><b>pragma</b> disable_invariants_in_body; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateValidatorOperatorAccountAbortsIf">CreateValidatorOperatorAccountAbortsIf</a>; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateValidatorOperatorAccountEnsures">CreateValidatorOperatorAccountEnsures</a>; </code></pre><a name="0x1_DiemAccount_CreateValidatorOperatorAccountAbortsIf"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateValidatorOperatorAccountAbortsIf">CreateValidatorOperatorAccountAbortsIf</a> { dr_account: signer; new_account_address: address; <b>include</b> <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">Roles::AbortsIfNotDiemRoot</a>{account: dr_account}; <b>include</b> <a href="DiemAccount.md#0x1_DiemAccount_MakeAccountAbortsIf">MakeAccountAbortsIf</a>{addr: new_account_address}; <b>include</b> <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>; <b>aborts_if</b> <a href="ValidatorOperatorConfig.md#0x1_ValidatorOperatorConfig_has_validator_operator_config">ValidatorOperatorConfig::has_validator_operator_config</a>(new_account_address) <b>with</b> <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; } </code></pre><a name="0x1_DiemAccount_CreateValidatorOperatorAccountEnsures"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_CreateValidatorOperatorAccountEnsures">CreateValidatorOperatorAccountEnsures</a> { new_account_address: address; <b>include</b> <a href="Roles.md#0x1_Roles_GrantRole">Roles::GrantRole</a>{addr: new_account_address, role_id: <a href="Roles.md#0x1_Roles_VALIDATOR_OPERATOR_ROLE_ID">Roles::VALIDATOR_OPERATOR_ROLE_ID</a>}; <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(new_account_address); <b>ensures</b> <a href="ValidatorOperatorConfig.md#0x1_ValidatorOperatorConfig_has_validator_operator_config">ValidatorOperatorConfig::has_validator_operator_config</a>(new_account_address); } </code></pre> </details><a name="@Module_Specification_4"></a>
<a name="0x1_DiemAccount_spec_has_published_account_limits"></a>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_has_published_account_limits">spec_has_published_account_limits</a><Token>(addr: address): bool { <b>if</b> (<a href="VASP.md#0x1_VASP_is_vasp">VASP::is_vasp</a>(addr)) <a href="VASP.md#0x1_VASP_spec_has_account_limits">VASP::spec_has_account_limits</a><Token>(addr) <b>else</b> <a href="AccountLimits.md#0x1_AccountLimits_has_window_published">AccountLimits::has_window_published</a><Token>(addr) } </code></pre><a name="@Access_Control_5"></a>
<a name="@Key_Rotation_Capability_6"></a>
the permission "RotateAuthenticationKey(addr)" is granted to the account at addr [H18]. When an account is created, its KeyRotationCapability is granted to the account.
<pre><code><b>apply</b> <a href="DiemAccount.md#0x1_DiemAccount_EnsuresHasKeyRotationCap">EnsuresHasKeyRotationCap</a>{account: new_account} <b>to</b> make_account; </code></pre>Only <code>make_account</code> creates KeyRotationCap [H18][I18]. <code>create_*_account</code> only calls <code>make_account</code>, and does not pack KeyRotationCap by itself. <code>restore_key_rotation_capability</code> restores KeyRotationCap, and does not create new one.
<pre><code><b>apply</b> <a href="DiemAccount.md#0x1_DiemAccount_PreserveKeyRotationCapAbsence">PreserveKeyRotationCapAbsence</a> <b>to</b> * <b>except</b> make_account, create_*_account, restore_key_rotation_capability, initialize; </code></pre>Every account holds either no key rotation capability (because KeyRotationCapability has been delegated) or the key rotation capability for addr itself [H18].
<pre><code><b>invariant</b> <b>forall</b> addr: address <b>where</b> <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr): <a href="DiemAccount.md#0x1_DiemAccount_delegated_key_rotation_capability">delegated_key_rotation_capability</a>(addr) || <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_own_key_rotation_cap">spec_holds_own_key_rotation_cap</a>(addr); </code></pre><a name="0x1_DiemAccount_EnsuresHasKeyRotationCap"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_EnsuresHasKeyRotationCap">EnsuresHasKeyRotationCap</a> { account: signer; <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_own_key_rotation_cap">spec_holds_own_key_rotation_cap</a>(addr); } </code></pre><a name="0x1_DiemAccount_PreserveKeyRotationCapAbsence"></a>
The absence of KeyRotationCap is preserved.
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PreserveKeyRotationCapAbsence">PreserveKeyRotationCapAbsence</a> { <b>ensures</b> <b>forall</b> addr: address: <b>old</b>(!<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr) || !<a href="DiemAccount.md#0x1_DiemAccount_spec_has_key_rotation_cap">spec_has_key_rotation_cap</a>(addr)) ==> (!<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr) || !<a href="DiemAccount.md#0x1_DiemAccount_spec_has_key_rotation_cap">spec_has_key_rotation_cap</a>(addr)); } </code></pre><a name="@Withdraw_Capability_7"></a>
the permission "WithdrawCapability(addr)" is granted to the account at addr [H19]. When an account is created, its WithdrawCapability is granted to the account.
<pre><code><b>apply</b> <a href="DiemAccount.md#0x1_DiemAccount_EnsuresWithdrawCap">EnsuresWithdrawCap</a>{account: new_account} <b>to</b> make_account; </code></pre>Only <code>make_account</code> creates WithdrawCap [H19][I19]. <code>create_*_account</code> only calls <code>make_account</code>, and does not pack KeyRotationCap by itself. <code>restore_withdraw_capability</code> restores WithdrawCap, and does not create new one.
<pre><code><b>apply</b> <a href="DiemAccount.md#0x1_DiemAccount_PreserveWithdrawCapAbsence">PreserveWithdrawCapAbsence</a> <b>to</b> * <b>except</b> make_account, create_*_account, restore_withdraw_capability, initialize; </code></pre>Every account holds either no withdraw capability (because withdraw cap has been delegated) or the withdraw capability for addr itself [H19].
<pre><code><b>invariant</b> <b>forall</b> addr: address <b>where</b> <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr): <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_delegated_withdraw_capability">spec_holds_delegated_withdraw_capability</a>(addr) || <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_own_withdraw_cap">spec_holds_own_withdraw_cap</a>(addr); </code></pre><a name="0x1_DiemAccount_EnsuresWithdrawCap"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_EnsuresWithdrawCap">EnsuresWithdrawCap</a> { account: signer; <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); <b>ensures</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_own_withdraw_cap">spec_holds_own_withdraw_cap</a>(addr); } </code></pre><a name="0x1_DiemAccount_PreserveWithdrawCapAbsence"></a>
The absence of WithdrawCap is preserved.
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_PreserveWithdrawCapAbsence">PreserveWithdrawCapAbsence</a> { <b>ensures</b> <b>forall</b> addr: address: <b>old</b>(!<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr) || <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_is_none">Option::is_none</a>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr).withdraw_capability)) ==> (!<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr) || <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_is_none">Option::is_none</a>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr).withdraw_capability)); } </code></pre><a name="@Authentication_Key_8"></a>
only <code><a href="DiemAccount.md#0x1_DiemAccount_rotate_authentication_key">Self::rotate_authentication_key</a></code> can rotate authentication_key [H18].
<pre><code><b>apply</b> <a href="DiemAccount.md#0x1_DiemAccount_AuthenticationKeyRemainsSame">AuthenticationKeyRemainsSame</a> <b>to</b> *, *<T> <b>except</b> rotate_authentication_key; </code></pre><a name="0x1_DiemAccount_AuthenticationKeyRemainsSame"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_AuthenticationKeyRemainsSame">AuthenticationKeyRemainsSame</a> { <b>ensures</b> <b>forall</b> addr: address <b>where</b> <b>old</b>(<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr)): <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr).authentication_key == <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr).authentication_key); } </code></pre><a name="@Balance_9"></a>
only <code><a href="DiemAccount.md#0x1_DiemAccount_withdraw_from">Self::withdraw_from</a></code> and its helper and clients can withdraw [H19].
<pre><code><b>apply</b> <a href="DiemAccount.md#0x1_DiemAccount_BalanceNotDecrease">BalanceNotDecrease</a><Token> <b>to</b> *<Token> <b>except</b> withdraw_from, withdraw_from_balance, staple_xdx, unstaple_xdx, preburn, pay_from, pay_by_signers, epilogue_common, epilogue, failure_epilogue, success_epilogue; </code></pre><a name="0x1_DiemAccount_BalanceNotDecrease"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_BalanceNotDecrease">BalanceNotDecrease</a><Token> { <b>ensures</b> <b>forall</b> addr: address <b>where</b> <b>old</b>(<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(addr)): <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(addr).coin.value >= <b>old</b>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><Token>>(addr).coin.value); } </code></pre><a name="@Persistence_of_Resources_10"></a>
Accounts are never deleted.
<pre><code><b>invariant</b> <b>update</b> <b>forall</b> addr: address <b>where</b> <b>old</b>(<a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr)): <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr); </code></pre>After genesis, the <code><a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a></code> exists.
<pre><code><b>invariant</b> [suspendable] <a href="DiemTimestamp.md#0x1_DiemTimestamp_is_operating">DiemTimestamp::is_operating</a>() ==> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot); </code></pre>After genesis, the <code><a href="DiemAccount.md#0x1_DiemAccount_DiemWriteSetManager">DiemWriteSetManager</a></code> exists.
<pre><code><b>invariant</b> [suspendable] <a href="DiemTimestamp.md#0x1_DiemTimestamp_is_operating">DiemTimestamp::is_operating</a>() ==> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_DiemWriteSetManager">DiemWriteSetManager</a>>(@DiemRoot); </code></pre>resource struct <code><a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><CoinType></code> is persistent
<pre><code><b>invariant</b><CoinType> <b>update</b> <b>forall</b> addr: address <b>where</b> <b>old</b>(<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><CoinType>>(addr)): <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><CoinType>>(addr); </code></pre>resource struct <code><a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a></code> is persistent
<pre><code><b>invariant</b> <b>update</b> <b>old</b>(<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot)) ==> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot); </code></pre>resource struct <code><a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a></code> is persistent
<pre><code><b>invariant</b> <b>update</b> <b>old</b>(<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_DiemWriteSetManager">DiemWriteSetManager</a>>(@DiemRoot)) ==> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_DiemWriteSetManager">DiemWriteSetManager</a>>(@DiemRoot); </code></pre><a name="@Other_invariants_11"></a>
An address has a published account iff it has a published RoleId
<pre><code><b>invariant</b> [suspendable] <b>forall</b> addr: address: <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr) <==> <b>exists</b><<a href="Roles.md#0x1_Roles_RoleId">Roles::RoleId</a>>(addr); </code></pre>There is a published AccountOperationsCapability iff there is an account and it's at Diem root address
<pre><code><b>invariant</b> [suspendable] <b>forall</b> addr: address: <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(addr) <==> (addr == @DiemRoot && <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr)); </code></pre>An account has a WriteSetManager iff if it is Diem root
<pre><code><b>invariant</b> [suspendable] <b>forall</b> addr: address: <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_DiemWriteSetManager">DiemWriteSetManager</a>>(addr) <==> (addr == @DiemRoot && <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr)); </code></pre>There is a VASPDomainManager at an address iff the address is a diem treasury compliance account
<pre><code><b>invariant</b> [suspendable] <b>forall</b> addr: address: <b>exists</b><<a href="VASPDomain.md#0x1_VASPDomain_VASPDomainManager">VASPDomain::VASPDomainManager</a>>(addr) <==> <a href="Roles.md#0x1_Roles_spec_has_treasury_compliance_role_addr">Roles::spec_has_treasury_compliance_role_addr</a>(addr); </code></pre>There is a VASPDomains at an address iff the address is a Diem treasury compliance account
<pre><code><b>invariant</b> [suspendable] <b>forall</b> addr: address: <b>exists</b><<a href="VASPDomain.md#0x1_VASPDomain_VASPDomains">VASPDomain::VASPDomains</a>>(addr) <==> <a href="Roles.md#0x1_Roles_spec_has_parent_VASP_role_addr">Roles::spec_has_parent_VASP_role_addr</a>(addr); </code></pre>Account has a balance only iff it is parent or child VASP or a designated dealer
<pre><code><b>invariant</b> <b>forall</b> addr: address: (<b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><<a href="XUS.md#0x1_XUS">XUS</a>>>(addr) || <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><<a href="XDX.md#0x1_XDX">XDX</a>>>(addr)) ==> <a href="Roles.md#0x1_Roles_spec_can_hold_balance_addr">Roles::spec_can_hold_balance_addr</a>(addr); </code></pre>Note: It would be better to make this generic over all existing and future coins, but that would require existential quantification over types, and I'm not sure if that works with monomorphization.
There is a <code><a href="DesignatedDealer.md#0x1_DesignatedDealer_Dealer">DesignatedDealer::Dealer</a></code> published at <code>addr</code> iff the <code>addr</code> has a <code>Roles::DesignatedDealer</code> role.
<pre><code><b>invariant</b> [suspendable] <b>forall</b> addr: address: <b>exists</b><<a href="DesignatedDealer.md#0x1_DesignatedDealer_Dealer">DesignatedDealer::Dealer</a>>(addr) <==> <a href="Roles.md#0x1_Roles_spec_has_designated_dealer_role_addr">Roles::spec_has_designated_dealer_role_addr</a>(addr); </code></pre>There is a DualAttestation credential iff account has designated dealer or parent VASP role
<pre><code><b>invariant</b> [suspendable] <b>forall</b> addr: address: <b>exists</b><<a href="DualAttestation.md#0x1_DualAttestation_Credential">DualAttestation::Credential</a>>(addr) <==> (<a href="Roles.md#0x1_Roles_spec_has_designated_dealer_role_addr">Roles::spec_has_designated_dealer_role_addr</a>(addr) || <a href="Roles.md#0x1_Roles_spec_has_parent_VASP_role_addr">Roles::spec_has_parent_VASP_role_addr</a>(addr)); </code></pre>An address has an account iff there is a published FreezingBit struct
<pre><code><b>invariant</b> [suspendable] <b>forall</b> addr: address: <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr) <==> <b>exists</b><<a href="AccountFreezing.md#0x1_AccountFreezing_FreezingBit">AccountFreezing::FreezingBit</a>>(addr); <b>invariant</b> [suspendable] <b>forall</b> addr: address: <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr) ==> <b>exists</b><<a href="AccountFreezing.md#0x1_AccountFreezing_FreezingBit">AccountFreezing::FreezingBit</a>>(addr); </code></pre>Balances can only be published at addresses where an account exists
<pre><code><b>invariant</b><CoinType> [suspendable] <b>forall</b> addr: address <b>where</b> <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_Balance">Balance</a><CoinType>>(addr): <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr); </code></pre>TODO: I think this is redundant with previous invariants. exists_at <==> Role, and Balance <==> can_hold_balance
Account has SlidingNonce only if it's Diem Root or Treasury Compliance
<pre><code><b>invariant</b> [suspendable] <b>forall</b> addr: address: <b>exists</b><<a href="SlidingNonce.md#0x1_SlidingNonce_SlidingNonce">SlidingNonce::SlidingNonce</a>>(addr) <==> (<a href="Roles.md#0x1_Roles_spec_has_diem_root_role_addr">Roles::spec_has_diem_root_role_addr</a>(addr) || <a href="Roles.md#0x1_Roles_spec_has_treasury_compliance_role_addr">Roles::spec_has_treasury_compliance_role_addr</a>(addr)); </code></pre>Address has a ValidatorConfig iff it is a Validator address
<pre><code><b>invariant</b> [suspendable] <b>forall</b> addr: address: <a href="ValidatorConfig.md#0x1_ValidatorConfig_exists_config">ValidatorConfig::exists_config</a>(addr) <==> <a href="Roles.md#0x1_Roles_spec_has_validator_role_addr">Roles::spec_has_validator_role_addr</a>(addr); </code></pre>Address has a ValidatorOperatorConfig iff it is a ValidatorOperator address
<pre><code><b>invariant</b> [suspendable] <b>forall</b> addr: address: <a href="ValidatorOperatorConfig.md#0x1_ValidatorOperatorConfig_has_validator_operator_config">ValidatorOperatorConfig::has_validator_operator_config</a>(addr) <==> <a href="Roles.md#0x1_Roles_spec_has_validator_operator_role_addr">Roles::spec_has_validator_operator_role_addr</a>(addr); </code></pre>Address has a parent VASP credential iff it has a parent VASP role
<pre><code><b>invariant</b> [suspendable] <b>forall</b> addr: address: <a href="VASP.md#0x1_VASP_is_parent">VASP::is_parent</a>(addr) <==> <a href="Roles.md#0x1_Roles_spec_has_parent_VASP_role_addr">Roles::spec_has_parent_VASP_role_addr</a>(addr); </code></pre>Address has a child VASP credential iff it has a child VASP role
<pre><code><b>invariant</b> [suspendable] <b>forall</b> addr: address: <a href="VASP.md#0x1_VASP_is_child">VASP::is_child</a>(addr) <==> <a href="Roles.md#0x1_Roles_spec_has_child_VASP_role_addr">Roles::spec_has_child_VASP_role_addr</a>(addr); </code></pre><a name="@Helper_Functions_and_Schemas_12"></a>
<a name="@Capabilities_13"></a>
Returns field <code>key_rotation_capability</code> of the DiemAccount under <code>addr</code>.
<a name="0x1_DiemAccount_spec_get_key_rotation_cap_field"></a>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_get_key_rotation_cap_field">spec_get_key_rotation_cap_field</a>(addr: address): <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option">Option</a><<a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">KeyRotationCapability</a>> { <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr).key_rotation_capability } </code></pre>Returns the KeyRotationCapability of the field <code>key_rotation_capability</code>.
<a name="0x1_DiemAccount_spec_get_key_rotation_cap"></a>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_get_key_rotation_cap">spec_get_key_rotation_cap</a>(addr: address): <a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">KeyRotationCapability</a> { <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_borrow">Option::borrow</a>(<a href="DiemAccount.md#0x1_DiemAccount_spec_get_key_rotation_cap_field">spec_get_key_rotation_cap_field</a>(addr)) } <a name="0x1_DiemAccount_spec_has_key_rotation_cap"></a> <b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_has_key_rotation_cap">spec_has_key_rotation_cap</a>(addr: address): bool { <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_is_some">Option::is_some</a>(<a href="DiemAccount.md#0x1_DiemAccount_spec_get_key_rotation_cap_field">spec_get_key_rotation_cap_field</a>(addr)) } </code></pre>Returns true if the DiemAccount at <code>addr</code> holds <code><a href="DiemAccount.md#0x1_DiemAccount_KeyRotationCapability">KeyRotationCapability</a></code> for itself.
<a name="0x1_DiemAccount_spec_holds_own_key_rotation_cap"></a>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_own_key_rotation_cap">spec_holds_own_key_rotation_cap</a>(addr: address): bool { <a href="DiemAccount.md#0x1_DiemAccount_spec_has_key_rotation_cap">spec_has_key_rotation_cap</a>(addr) && addr == <a href="DiemAccount.md#0x1_DiemAccount_spec_get_key_rotation_cap">spec_get_key_rotation_cap</a>(addr).account_address } </code></pre>Returns true if <code><a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a></code> is published.
<a name="0x1_DiemAccount_spec_has_account_operations_cap"></a>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_has_account_operations_cap">spec_has_account_operations_cap</a>(): bool { <b>exists</b><<a href="DiemAccount.md#0x1_DiemAccount_AccountOperationsCapability">AccountOperationsCapability</a>>(@DiemRoot) } </code></pre>Returns field <code>withdraw_capability</code> of DiemAccount under <code>addr</code>.
<a name="0x1_DiemAccount_spec_get_withdraw_cap_field"></a>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_get_withdraw_cap_field">spec_get_withdraw_cap_field</a>(addr: address): <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option">Option</a><<a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a>> { <b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr).withdraw_capability } </code></pre>Returns the WithdrawCapability of the field <code>withdraw_capability</code>.
<a name="0x1_DiemAccount_spec_get_withdraw_cap"></a>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_get_withdraw_cap">spec_get_withdraw_cap</a>(addr: address): <a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a> { <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_borrow">Option::borrow</a>(<a href="DiemAccount.md#0x1_DiemAccount_spec_get_withdraw_cap_field">spec_get_withdraw_cap_field</a>(addr)) } </code></pre>Returns true if the DiemAccount at <code>addr</code> holds a <code><a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a></code>.
<a name="0x1_DiemAccount_spec_has_withdraw_cap"></a>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_has_withdraw_cap">spec_has_withdraw_cap</a>(addr: address): bool { <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_is_some">Option::is_some</a>(<a href="DiemAccount.md#0x1_DiemAccount_spec_get_withdraw_cap_field">spec_get_withdraw_cap_field</a>(addr)) } </code></pre>Returns true if the DiemAccount at <code>addr</code> holds <code><a href="DiemAccount.md#0x1_DiemAccount_WithdrawCapability">WithdrawCapability</a></code> for itself.
<a name="0x1_DiemAccount_spec_holds_own_withdraw_cap"></a>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_own_withdraw_cap">spec_holds_own_withdraw_cap</a>(addr: address): bool { <a href="DiemAccount.md#0x1_DiemAccount_spec_has_withdraw_cap">spec_has_withdraw_cap</a>(addr) && addr == <a href="DiemAccount.md#0x1_DiemAccount_spec_get_withdraw_cap">spec_get_withdraw_cap</a>(addr).account_address } </code></pre>Returns true of the account holds a delegated withdraw capability.
<a name="0x1_DiemAccount_spec_holds_delegated_withdraw_capability"></a>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_spec_holds_delegated_withdraw_capability">spec_holds_delegated_withdraw_capability</a>(addr: address): bool { <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr) && <a href="../../../../../../move-stdlib/docs/Option.md#0x1_Option_is_none">Option::is_none</a>(<b>global</b><<a href="DiemAccount.md#0x1_DiemAccount">DiemAccount</a>>(addr).withdraw_capability) } </code></pre><a name="@Prologue_14"></a>
<a name="0x1_DiemAccount_prologue_guarantees"></a>
<pre><code><b>fun</b> <a href="DiemAccount.md#0x1_DiemAccount_prologue_guarantees">prologue_guarantees</a>(sender: signer) : bool { <b>let</b> addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(sender); <a href="DiemTimestamp.md#0x1_DiemTimestamp_is_operating">DiemTimestamp::is_operating</a>() && <a href="DiemAccount.md#0x1_DiemAccount_exists_at">exists_at</a>(addr) && !<a href="AccountFreezing.md#0x1_AccountFreezing_account_is_frozen">AccountFreezing::account_is_frozen</a>(addr) } </code></pre>Used in transaction script to specify properties checked by the prologue.
<a name="0x1_DiemAccount_TransactionChecks"></a>
<pre><code><b>schema</b> <a href="DiemAccount.md#0x1_DiemAccount_TransactionChecks">TransactionChecks</a> { sender: signer; <b>requires</b> <a href="DiemAccount.md#0x1_DiemAccount_prologue_guarantees">prologue_guarantees</a>(sender); } </code></pre>