Module `0x1::AccountLimits`

Module which manages account limits, like the amount of currency which can flow in or out over a given time period.

Struct AccountLimitMutationCapability
Resource LimitsDefinition
Resource Window
Constants
Function grant_mutation_capability
Function update_deposit_limits
Function update_withdrawal_limits
Function publish_window
Function publish_unrestricted_limits
Function update_limits_definition
Function update_window_info
Function reset_window
Function can_receive_and_update_window
Function can_withdraw_and_update_window
Function is_unrestricted
Function limits_definition_address
Function has_limits_published
Function has_window_published
Function current_time
Module Specification
- Access Control

<pre><code>use <a href="DiemTimestamp.md#0x1_DiemTimestamp">0x1::DiemTimestamp</a>; use <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors">0x1::Errors</a>; use <a href="Roles.md#0x1_Roles">0x1::Roles</a>; use <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer">0x1::Signer</a>; </code></pre>

Struct `AccountLimitMutationCapability`

An operations capability that restricts callers of this module since the operations can mutate account states.

<pre><code>struct <a href="AccountLimits.md#0x1_AccountLimits_AccountLimitMutationCapability">AccountLimitMutationCapability</a> </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>dummy_field: bool</code> </dt> <dd> </dd> </dl> </details>

Resource `LimitsDefinition`

A resource specifying the account limits per-currency. There is a default "unlimited" <code><a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a></code> resource for accounts published at <code><a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()</code>, but other accounts may have different account limit definitons. In such cases, they will have a <code><a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a></code> published under their (root) account.

<pre><code>resource struct <a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType> </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>max_inflow: u64</code> </dt> <dd> The maximum inflow allowed during the specified time period. </dd> <dt> <code>max_outflow: u64</code> </dt> <dd> The maximum outflow allowed during the specified time period. </dd> <dt> <code>time_period: u64</code> </dt> <dd> Time period, specified in microseconds </dd> <dt> <code>max_holding: u64</code> </dt> <dd> The maximum amount that can be held </dd> </dl> </details> <details> <summary>Specification</summary> <pre><code>invariant max_inflow > 0; invariant max_outflow > 0; invariant time_period > 0; invariant max_holding > 0; </code></pre> </details>

Resource `Window`

A struct holding account transaction information for the time window starting at <code>window_start</code> and lasting for the <code>time_period</code> specified in the limits definition at <code>limit_address</code>.

<pre><code>resource struct <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType> </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>window_start: u64</code> </dt> <dd> Time window start in microseconds </dd> <dt> <code>window_inflow: u64</code> </dt> <dd> The inflow during this time window </dd> <dt> <code>window_outflow: u64</code> </dt> <dd> The inflow during this time window </dd> <dt> <code>tracked_balance: u64</code> </dt> <dd> The balance that this account has held during this time period. </dd> <dt> <code>limit_address: address</code> </dt> <dd> address storing the LimitsDefinition resource that governs this window </dd> </dl> </details>

Constants

<pre><code>const <a href="AccountLimits.md#0x1_AccountLimits_MAX_U64">MAX_U64</a>: u64 = 18446744073709551615; </code></pre>

The <code><a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a></code> resource is in an invalid state

<pre><code>const <a href="AccountLimits.md#0x1_AccountLimits_ELIMITS_DEFINITION">ELIMITS_DEFINITION</a>: u64 = 0; </code></pre>

The <code><a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a></code> resource is in an invalid state

<pre><code>const <a href="AccountLimits.md#0x1_AccountLimits_EWINDOW">EWINDOW</a>: u64 = 1; </code></pre>

24 hours in microseconds

<pre><code>const <a href="AccountLimits.md#0x1_AccountLimits_ONE_DAY">ONE_DAY</a>: u64 = 86400000000; </code></pre>

Function `grant_mutation_capability`

Grant a capability to call this module. This does not necessarily need to be a unique capability.

<pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_grant_mutation_capability">grant_mutation_capability</a>(dr_account: &signer): <a href="AccountLimits.md#0x1_AccountLimits_AccountLimitMutationCapability">AccountLimits::AccountLimitMutationCapability</a> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_grant_mutation_capability">grant_mutation_capability</a>(dr_account: &signer): <a href="AccountLimits.md#0x1_AccountLimits_AccountLimitMutationCapability">AccountLimitMutationCapability</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); <a href="AccountLimits.md#0x1_AccountLimits_AccountLimitMutationCapability">AccountLimitMutationCapability</a>{} } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotGenesis">DiemTimestamp::AbortsIfNotGenesis</a>; include <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">Roles::AbortsIfNotDiemRoot</a>{account: dr_account}; </code></pre> </details>

Function `update_deposit_limits`

Determines if depositing <code>amount</code> of <code>CoinType</code> coins into the account at <code>addr</code> is amenable with their account limits. Returns false if this deposit violates the account limits.

<pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_update_deposit_limits">update_deposit_limits</a><CoinType>(amount: u64, addr: address, _cap: &<a href="AccountLimits.md#0x1_AccountLimits_AccountLimitMutationCapability">AccountLimits::AccountLimitMutationCapability</a>): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_update_deposit_limits">update_deposit_limits</a><CoinType: store>( amount: u64, addr: address, _cap: &<a href="AccountLimits.md#0x1_AccountLimits_AccountLimitMutationCapability">AccountLimitMutationCapability</a>, ): bool acquires <a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a>, <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a> { assert(exists<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="AccountLimits.md#0x1_AccountLimits_EWINDOW">EWINDOW</a>)); <a href="AccountLimits.md#0x1_AccountLimits_can_receive_and_update_window">can_receive_and_update_window</a><CoinType>( amount, borrow_global_mut<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(addr), ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; modifies global<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(addr); include <a href="AccountLimits.md#0x1_AccountLimits_UpdateDepositLimitsAbortsIf">UpdateDepositLimitsAbortsIf</a><CoinType>; include <a href="AccountLimits.md#0x1_AccountLimits_CanReceiveEnsures">CanReceiveEnsures</a><CoinType>{receiving: global<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(addr)}; </code></pre>

<pre><code>schema <a href="AccountLimits.md#0x1_AccountLimits_UpdateDepositLimitsAbortsIf">UpdateDepositLimitsAbortsIf</a><CoinType> { amount: u64; addr: address; include <a href="AccountLimits.md#0x1_AccountLimits_AbortsIfNoWindow">AbortsIfNoWindow</a><CoinType>; include <a href="AccountLimits.md#0x1_AccountLimits_CanReceiveAbortsIf">CanReceiveAbortsIf</a><CoinType>{receiving: global<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(addr)}; } </code></pre>

<pre><code>schema <a href="AccountLimits.md#0x1_AccountLimits_AbortsIfNoWindow">AbortsIfNoWindow</a><CoinType> { addr: address; aborts_if !exists<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(addr) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; } </code></pre>

<pre><code>define <a href="AccountLimits.md#0x1_AccountLimits_spec_update_deposit_limits">spec_update_deposit_limits</a><CoinType>(amount: u64, addr: address): bool { <a href="AccountLimits.md#0x1_AccountLimits_spec_receiving_limits_ok">spec_receiving_limits_ok</a>(global<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(addr), amount) } </code></pre> </details>

Function `update_withdrawal_limits`

Determine if withdrawing <code>amount</code> of <code>CoinType</code> coins from the account at <code>addr</code> would violate the account limits for that account. Returns <code>false</code> if this withdrawal violates account limits.

<pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_update_withdrawal_limits">update_withdrawal_limits</a><CoinType>(amount: u64, addr: address, _cap: &<a href="AccountLimits.md#0x1_AccountLimits_AccountLimitMutationCapability">AccountLimits::AccountLimitMutationCapability</a>): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_update_withdrawal_limits">update_withdrawal_limits</a><CoinType: store>( amount: u64, addr: address, _cap: &<a href="AccountLimits.md#0x1_AccountLimits_AccountLimitMutationCapability">AccountLimitMutationCapability</a>, ): bool acquires <a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a>, <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a> { assert(exists<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="AccountLimits.md#0x1_AccountLimits_EWINDOW">EWINDOW</a>)); <a href="AccountLimits.md#0x1_AccountLimits_can_withdraw_and_update_window">can_withdraw_and_update_window</a><CoinType>( amount, borrow_global_mut<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(addr), ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; modifies global<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(addr); include <a href="AccountLimits.md#0x1_AccountLimits_UpdateWithdrawalLimitsAbortsIf">UpdateWithdrawalLimitsAbortsIf</a><CoinType>; include <a href="AccountLimits.md#0x1_AccountLimits_CanWithdrawEnsures">CanWithdrawEnsures</a><CoinType>{sending: global<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(addr)}; </code></pre>

<pre><code>schema <a href="AccountLimits.md#0x1_AccountLimits_UpdateWithdrawalLimitsAbortsIf">UpdateWithdrawalLimitsAbortsIf</a><CoinType> { amount: u64; addr: address; include <a href="AccountLimits.md#0x1_AccountLimits_AbortsIfNoWindow">AbortsIfNoWindow</a><CoinType>; include <a href="AccountLimits.md#0x1_AccountLimits_CanWithdrawAbortsIf">CanWithdrawAbortsIf</a><CoinType>{sending: global<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(addr)}; } </code></pre>

<pre><code>define <a href="AccountLimits.md#0x1_AccountLimits_spec_update_withdrawal_limits">spec_update_withdrawal_limits</a><CoinType>(amount: u64, addr: address): bool { <a href="AccountLimits.md#0x1_AccountLimits_spec_withdrawal_limits_ok">spec_withdrawal_limits_ok</a>(global<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(addr), amount) } </code></pre> </details>

Function `publish_window`

All accounts that could be subject to account limits will have a <code><a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a></code> for each currency they can hold published at the top level. Root accounts for multi-account entities will hold this resource at their root/parent account.

<pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_publish_window">publish_window</a><CoinType>(dr_account: &signer, to_limit: &signer, limit_address: address) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_publish_window">publish_window</a><CoinType: store>( dr_account: &signer, to_limit: &signer, limit_address: address, ) { <a href="Roles.md#0x1_Roles_assert_diem_root">Roles::assert_diem_root</a>(dr_account); assert(exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>>(limit_address), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="AccountLimits.md#0x1_AccountLimits_ELIMITS_DEFINITION">ELIMITS_DEFINITION</a>)); <a href="Roles.md#0x1_Roles_assert_parent_vasp_or_child_vasp">Roles::assert_parent_vasp_or_child_vasp</a>(to_limit); assert( !exists<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(to_limit)), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_already_published">Errors::already_published</a>(<a href="AccountLimits.md#0x1_AccountLimits_EWINDOW">EWINDOW</a>) ); move_to( to_limit, <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType> { window_start: <a href="AccountLimits.md#0x1_AccountLimits_current_time">current_time</a>(), window_inflow: 0, window_outflow: 0, tracked_balance: 0, limit_address, } ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="AccountLimits.md#0x1_AccountLimits_PublishWindowAbortsIf">PublishWindowAbortsIf</a><CoinType>; </code></pre>

<pre><code>schema <a href="AccountLimits.md#0x1_AccountLimits_PublishWindowAbortsIf">PublishWindowAbortsIf</a><CoinType> { dr_account: signer; to_limit: signer; limit_address: address; } </code></pre>

Only ParentVASP and ChildVASP can have the account limits [E1][E2][E3][E4][E5][E6][E7].

<pre><code>schema <a href="AccountLimits.md#0x1_AccountLimits_PublishWindowAbortsIf">PublishWindowAbortsIf</a><CoinType> { include <a href="Roles.md#0x1_Roles_AbortsIfNotParentVaspOrChildVasp">Roles::AbortsIfNotParentVaspOrChildVasp</a>{account: to_limit}; include <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">Roles::AbortsIfNotDiemRoot</a>{account: dr_account}; aborts_if !exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>>(limit_address) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; aborts_if exists<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(to_limit)) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; } </code></pre> </details>

Function `publish_unrestricted_limits`

Unrestricted limits are represented by setting all fields in the limits definition to <code><a href="AccountLimits.md#0x1_AccountLimits_MAX_U64">MAX_U64</a></code>. Anyone can publish an unrestricted limits since no windows will point to this limits definition unless the TC account, or a caller with access to a <code>&<a href="AccountLimits.md#0x1_AccountLimits_AccountLimitMutationCapability">AccountLimitMutationCapability</a></code> points a window to it. Additionally, the TC controls the values held within this resource once it's published.

<pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_publish_unrestricted_limits">publish_unrestricted_limits</a><CoinType>(publish_account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_publish_unrestricted_limits">publish_unrestricted_limits</a><CoinType: store>(publish_account: &signer) { assert( !exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(publish_account)), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_already_published">Errors::already_published</a>(<a href="AccountLimits.md#0x1_AccountLimits_ELIMITS_DEFINITION">ELIMITS_DEFINITION</a>) ); move_to( publish_account, <a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType> { max_inflow: <a href="AccountLimits.md#0x1_AccountLimits_MAX_U64">MAX_U64</a>, max_outflow: <a href="AccountLimits.md#0x1_AccountLimits_MAX_U64">MAX_U64</a>, max_holding: <a href="AccountLimits.md#0x1_AccountLimits_MAX_U64">MAX_U64</a>, time_period: <a href="AccountLimits.md#0x1_AccountLimits_ONE_DAY">ONE_DAY</a>, } ) } </code></pre> </details> <details> <summary>Specification</summary>

TODO: turned off verification until we solve the generic type/specific invariant issue. Similar to in DiemConfig, this function violates an invariant in XUS about LimitsDefinition<XUS>.

<pre><code>pragma verify = false; include <a href="AccountLimits.md#0x1_AccountLimits_PublishUnrestrictedLimitsAbortsIf">PublishUnrestrictedLimitsAbortsIf</a><CoinType>; </code></pre>

<pre><code>schema <a href="AccountLimits.md#0x1_AccountLimits_PublishUnrestrictedLimitsAbortsIf">PublishUnrestrictedLimitsAbortsIf</a><CoinType> { publish_account: signer; aborts_if exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(publish_account)) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; } </code></pre>

<pre><code>schema <a href="AccountLimits.md#0x1_AccountLimits_PublishUnrestrictedLimitsEnsures">PublishUnrestrictedLimitsEnsures</a><CoinType> { publish_account: signer; ensures exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(publish_account)); } </code></pre> </details>

Function `update_limits_definition`

Updates the <code><a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType></code> resource at <code>limit_address</code>. If any of the field arguments is <code>0</code> the corresponding field is not updated.

TODO: This should be specified.

<pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_update_limits_definition">update_limits_definition</a><CoinType>(tc_account: &signer, limit_address: address, new_max_inflow: u64, new_max_outflow: u64, new_max_holding_balance: u64, new_time_period: u64) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_update_limits_definition">update_limits_definition</a><CoinType: store>( tc_account: &signer, limit_address: address, new_max_inflow: u64, new_max_outflow: u64, new_max_holding_balance: u64, new_time_period: u64, ) acquires <a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a> { <a href="Roles.md#0x1_Roles_assert_treasury_compliance">Roles::assert_treasury_compliance</a>(tc_account); // As we don't have Optionals for txn scripts, in update_account_limit_definition.move // we use 0 value to represent a None (ie no update to that variable) assert(exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>>(limit_address), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="AccountLimits.md#0x1_AccountLimits_ELIMITS_DEFINITION">ELIMITS_DEFINITION</a>)); let limits_def = borrow_global_mut<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>>(limit_address); if (new_max_inflow > 0) { limits_def.max_inflow = new_max_inflow }; if (new_max_outflow > 0) { limits_def.max_outflow = new_max_outflow }; if (new_max_holding_balance > 0) { limits_def.max_holding = new_max_holding_balance }; if (new_time_period > 0) { limits_def.time_period = new_time_period }; } </code></pre> </details>

Function `update_window_info`

Update either the <code>tracked_balance</code> or <code>limit_address</code> fields of the <code><a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType></code> stored under <code>window_address</code>.

Since we don't track balances of accounts before they are limited, once they do become limited the approximate balance in <code>CoinType</code> held by the entity across all of its accounts will need to be set by the association. if <code>aggregate_balance</code> is set to zero the field is not updated.
This updates the <code>limit_address</code> in the window resource to a new limits definition at <code>new_limit_address</code>. If the <code>aggregate_balance</code> needs to be updated but the <code>limit_address</code> should remain the same, the current <code>limit_address</code> needs to be passed in for <code>new_limit_address</code>. TODO(wrwg): specify

<pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_update_window_info">update_window_info</a><CoinType>(tc_account: &signer, window_address: address, aggregate_balance: u64, new_limit_address: address) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_update_window_info">update_window_info</a><CoinType: store>( tc_account: &signer, window_address: address, aggregate_balance: u64, new_limit_address: address, ) acquires <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a> { <a href="Roles.md#0x1_Roles_assert_treasury_compliance">Roles::assert_treasury_compliance</a>(tc_account); let window = borrow_global_mut<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(window_address); if (aggregate_balance != 0) { window.tracked_balance = aggregate_balance }; assert(exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>>(new_limit_address), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="AccountLimits.md#0x1_AccountLimits_ELIMITS_DEFINITION">ELIMITS_DEFINITION</a>)); window.limit_address = new_limit_address; } </code></pre> </details>

Function `reset_window`

If the time window starting at <code>window.window_start</code> and lasting for <code>limits_definition.time_period</code> has elapsed, resets the window and the inflow and outflow records.

<pre><code>fun <a href="AccountLimits.md#0x1_AccountLimits_reset_window">reset_window</a><CoinType>(window: &mut <a href="AccountLimits.md#0x1_AccountLimits_Window">AccountLimits::Window</a><CoinType>, limits_definition: &<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">AccountLimits::LimitsDefinition</a><CoinType>) </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="AccountLimits.md#0x1_AccountLimits_reset_window">reset_window</a><CoinType: store>(window: &mut <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>, limits_definition: &<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>) { let current_time = <a href="DiemTimestamp.md#0x1_DiemTimestamp_now_microseconds">DiemTimestamp::now_microseconds</a>(); assert(window.window_start <= <a href="AccountLimits.md#0x1_AccountLimits_MAX_U64">MAX_U64</a> - limits_definition.time_period, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="AccountLimits.md#0x1_AccountLimits_EWINDOW">EWINDOW</a>)); if (current_time > window.window_start + limits_definition.time_period) { window.window_start = current_time; window.window_inflow = 0; window.window_outflow = 0; } } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="AccountLimits.md#0x1_AccountLimits_ResetWindowAbortsIf">ResetWindowAbortsIf</a><CoinType>; include <a href="AccountLimits.md#0x1_AccountLimits_ResetWindowEnsures">ResetWindowEnsures</a><CoinType>; </code></pre>

<pre><code>schema <a href="AccountLimits.md#0x1_AccountLimits_ResetWindowAbortsIf">ResetWindowAbortsIf</a><CoinType> { window: <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>; limits_definition: <a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>; include <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotOperating">DiemTimestamp::AbortsIfNotOperating</a>; aborts_if window.window_start + limits_definition.time_period > max_u64() with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre>

<pre><code>schema <a href="AccountLimits.md#0x1_AccountLimits_ResetWindowEnsures">ResetWindowEnsures</a><CoinType> { window: <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>; limits_definition: <a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>; ensures window == old(<a href="AccountLimits.md#0x1_AccountLimits_spec_window_reset_with_limits">spec_window_reset_with_limits</a>(window, limits_definition)); } </code></pre>

<pre><code>define <a href="AccountLimits.md#0x1_AccountLimits_spec_window_expired">spec_window_expired</a><CoinType>( window: <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>, limits_definition: <a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType> ): bool { <a href="DiemTimestamp.md#0x1_DiemTimestamp_spec_now_microseconds">DiemTimestamp::spec_now_microseconds</a>() > window.window_start + limits_definition.time_period } <a name="0x1_AccountLimits_spec_window_reset_with_limits"></a> define <a href="AccountLimits.md#0x1_AccountLimits_spec_window_reset_with_limits">spec_window_reset_with_limits</a><CoinType>( window: <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>, limits_definition: <a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType> ): <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType> { if (<a href="AccountLimits.md#0x1_AccountLimits_spec_window_expired">spec_window_expired</a><CoinType>(window, limits_definition)) { <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>{ limit_address: window.limit_address, tracked_balance: window.tracked_balance, window_start: <a href="DiemTimestamp.md#0x1_DiemTimestamp_spec_now_microseconds">DiemTimestamp::spec_now_microseconds</a>(), window_inflow: 0, window_outflow: 0 } } else { window } } </code></pre> </details>

Function `can_receive_and_update_window`

Verify that the receiving account tracked by the <code>receiving</code> window can receive <code>amount</code> funds without violating requirements specified the <code>limits_definition</code> passed in. If the receipt of <code>amount</code> doesn't violate the limits <code>amount</code> of <code>CoinType</code> is recorded as received in the given <code>receiving</code> window.

<pre><code>fun <a href="AccountLimits.md#0x1_AccountLimits_can_receive_and_update_window">can_receive_and_update_window</a><CoinType>(amount: u64, receiving: &mut <a href="AccountLimits.md#0x1_AccountLimits_Window">AccountLimits::Window</a><CoinType>): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="AccountLimits.md#0x1_AccountLimits_can_receive_and_update_window">can_receive_and_update_window</a><CoinType: store>( amount: u64, receiving: &mut <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>, ): bool acquires <a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a> { assert(exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>>(receiving.limit_address), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="AccountLimits.md#0x1_AccountLimits_ELIMITS_DEFINITION">ELIMITS_DEFINITION</a>)); let limits_definition = borrow_global<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>>(receiving.limit_address); // If the limits are unrestricted then don't do any more work. if (<a href="AccountLimits.md#0x1_AccountLimits_is_unrestricted">is_unrestricted</a>(limits_definition)) return true; <a href="AccountLimits.md#0x1_AccountLimits_reset_window">reset_window</a>(receiving, limits_definition); // Check that the inflow is OK // TODO(wrwg): instead of aborting if the below additions overflow, we should perhaps just have ok false. assert(receiving.window_inflow <= <a href="AccountLimits.md#0x1_AccountLimits_MAX_U64">MAX_U64</a> - amount, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="AccountLimits.md#0x1_AccountLimits_EWINDOW">EWINDOW</a>)); let inflow_ok = (receiving.window_inflow + amount) <= limits_definition.max_inflow; // Check that the holding after the deposit is OK assert(receiving.tracked_balance <= <a href="AccountLimits.md#0x1_AccountLimits_MAX_U64">MAX_U64</a> - amount, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="AccountLimits.md#0x1_AccountLimits_EWINDOW">EWINDOW</a>)); let holding_ok = (receiving.tracked_balance + amount) <= limits_definition.max_holding; // The account with `receiving` window can receive the payment so record it. if (inflow_ok && holding_ok) { receiving.window_inflow = receiving.window_inflow + amount; receiving.tracked_balance = receiving.tracked_balance + amount; }; inflow_ok && holding_ok } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="AccountLimits.md#0x1_AccountLimits_CanReceiveAbortsIf">CanReceiveAbortsIf</a><CoinType>; include <a href="AccountLimits.md#0x1_AccountLimits_CanReceiveEnsures">CanReceiveEnsures</a><CoinType>; </code></pre>

<pre><code>schema <a href="AccountLimits.md#0x1_AccountLimits_CanReceiveAbortsIf">CanReceiveAbortsIf</a><CoinType> { amount: num; receiving: <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>; aborts_if !exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>>(receiving.limit_address) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; include !<a href="AccountLimits.md#0x1_AccountLimits_spec_window_unrestricted">spec_window_unrestricted</a><CoinType>(receiving) ==> <a href="AccountLimits.md#0x1_AccountLimits_CanReceiveRestrictedAbortsIf">CanReceiveRestrictedAbortsIf</a><CoinType>; } </code></pre>

<pre><code>schema <a href="AccountLimits.md#0x1_AccountLimits_CanReceiveRestrictedAbortsIf">CanReceiveRestrictedAbortsIf</a><CoinType> { amount: num; receiving: <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>; include <a href="AccountLimits.md#0x1_AccountLimits_ResetWindowAbortsIf">ResetWindowAbortsIf</a><CoinType>{ window: receiving, limits_definition: <a href="AccountLimits.md#0x1_AccountLimits_spec_window_limits">spec_window_limits</a><CoinType>(receiving) }; aborts_if <a href="AccountLimits.md#0x1_AccountLimits_spec_window_reset">spec_window_reset</a>(receiving).window_inflow + amount > max_u64() with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; aborts_if <a href="AccountLimits.md#0x1_AccountLimits_spec_window_reset">spec_window_reset</a>(receiving).tracked_balance + amount > max_u64() with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre>

<pre><code>schema <a href="AccountLimits.md#0x1_AccountLimits_CanReceiveEnsures">CanReceiveEnsures</a><CoinType> { amount: num; receiving: <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>; result: bool; ensures result == <a href="AccountLimits.md#0x1_AccountLimits_spec_receiving_limits_ok">spec_receiving_limits_ok</a>(old(receiving), amount); ensures if (result && !<a href="AccountLimits.md#0x1_AccountLimits_spec_window_unrestricted">spec_window_unrestricted</a>(old(receiving))) receiving == <a href="AccountLimits.md#0x1_AccountLimits_spec_update_inflow">spec_update_inflow</a>(<a href="AccountLimits.md#0x1_AccountLimits_spec_window_reset">spec_window_reset</a>(old(receiving)), amount) else receiving == <a href="AccountLimits.md#0x1_AccountLimits_spec_window_reset">spec_window_reset</a>(old(receiving)) || receiving == old(receiving); } </code></pre>

Returns the limits associated with this window.

<pre><code>define <a href="AccountLimits.md#0x1_AccountLimits_spec_window_limits">spec_window_limits</a><CoinType>(window: <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>): <a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType> { global<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>>(window.limit_address) } </code></pre>

Returns true of the window has unrestricted limits.

<pre><code>define <a href="AccountLimits.md#0x1_AccountLimits_spec_window_unrestricted">spec_window_unrestricted</a><CoinType>(window: <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>): bool { <a href="AccountLimits.md#0x1_AccountLimits_spec_is_unrestricted">spec_is_unrestricted</a>(<a href="AccountLimits.md#0x1_AccountLimits_spec_window_limits">spec_window_limits</a><CoinType>(window)) } </code></pre>

Resets wrapping variables of the given window.

<pre><code>define <a href="AccountLimits.md#0x1_AccountLimits_spec_window_reset">spec_window_reset</a><CoinType>(window: <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>): <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType> { <a href="AccountLimits.md#0x1_AccountLimits_spec_window_reset_with_limits">spec_window_reset_with_limits</a>(window, <a href="AccountLimits.md#0x1_AccountLimits_spec_window_limits">spec_window_limits</a><CoinType>(window)) } </code></pre>

Checks whether receiving limits are satisfied.

<pre><code>define <a href="AccountLimits.md#0x1_AccountLimits_spec_receiving_limits_ok">spec_receiving_limits_ok</a><CoinType>(receiving: <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>, amount: u64): bool { <a href="AccountLimits.md#0x1_AccountLimits_spec_window_unrestricted">spec_window_unrestricted</a>(receiving) || <a href="AccountLimits.md#0x1_AccountLimits_spec_window_reset">spec_window_reset</a>(receiving).window_inflow + amount <= <a href="AccountLimits.md#0x1_AccountLimits_spec_window_limits">spec_window_limits</a>(receiving).max_inflow && <a href="AccountLimits.md#0x1_AccountLimits_spec_window_reset">spec_window_reset</a>(receiving).tracked_balance + amount <= <a href="AccountLimits.md#0x1_AccountLimits_spec_window_limits">spec_window_limits</a>(receiving).max_holding } </code></pre>

<pre><code>define <a href="AccountLimits.md#0x1_AccountLimits_spec_update_inflow">spec_update_inflow</a><CoinType>(receiving: <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>, amount: u64): <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType> { update_field(update_field(receiving, window_inflow, receiving.window_inflow + amount), tracked_balance, receiving.tracked_balance + amount) } </code></pre> </details>

Function `can_withdraw_and_update_window`

Verify that <code>amount</code> can be withdrawn from the account tracked by the <code>sending</code> window without violating any limits specified in its <code>limits_definition</code>. If the withdrawal of <code>amount</code> doesn't violate the limits <code>amount</code> of <code>CoinType</code> is recorded as withdrawn in the given <code>sending</code> window.

<pre><code>fun <a href="AccountLimits.md#0x1_AccountLimits_can_withdraw_and_update_window">can_withdraw_and_update_window</a><CoinType>(amount: u64, sending: &mut <a href="AccountLimits.md#0x1_AccountLimits_Window">AccountLimits::Window</a><CoinType>): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="AccountLimits.md#0x1_AccountLimits_can_withdraw_and_update_window">can_withdraw_and_update_window</a><CoinType: store>( amount: u64, sending: &mut <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>, ): bool acquires <a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a> { assert(exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>>(sending.limit_address), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="AccountLimits.md#0x1_AccountLimits_ELIMITS_DEFINITION">ELIMITS_DEFINITION</a>)); let limits_definition = borrow_global<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>>(sending.limit_address); // If the limits are unrestricted then don't do any more work. if (<a href="AccountLimits.md#0x1_AccountLimits_is_unrestricted">is_unrestricted</a>(limits_definition)) return true; <a href="AccountLimits.md#0x1_AccountLimits_reset_window">reset_window</a>(sending, limits_definition); // Check outflow is OK assert(sending.window_outflow <= <a href="AccountLimits.md#0x1_AccountLimits_MAX_U64">MAX_U64</a> - amount, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="AccountLimits.md#0x1_AccountLimits_EWINDOW">EWINDOW</a>)); let outflow_ok = sending.window_outflow + amount <= limits_definition.max_outflow; // Flow is OK, so record it. if (outflow_ok) { sending.window_outflow = sending.window_outflow + amount; sending.tracked_balance = if (amount >= sending.tracked_balance) 0 else sending.tracked_balance - amount; }; outflow_ok } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="AccountLimits.md#0x1_AccountLimits_CanWithdrawAbortsIf">CanWithdrawAbortsIf</a><CoinType>; include <a href="AccountLimits.md#0x1_AccountLimits_CanWithdrawEnsures">CanWithdrawEnsures</a><CoinType>; </code></pre>

<pre><code>schema <a href="AccountLimits.md#0x1_AccountLimits_CanWithdrawAbortsIf">CanWithdrawAbortsIf</a><CoinType> { amount: u64; sending: &mut <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>; aborts_if !exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>>(sending.limit_address) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; include !<a href="AccountLimits.md#0x1_AccountLimits_spec_window_unrestricted">spec_window_unrestricted</a>(sending) ==> <a href="AccountLimits.md#0x1_AccountLimits_CanWithdrawRestrictedAbortsIf">CanWithdrawRestrictedAbortsIf</a><CoinType>; } </code></pre>

<pre><code>schema <a href="AccountLimits.md#0x1_AccountLimits_CanWithdrawRestrictedAbortsIf">CanWithdrawRestrictedAbortsIf</a><CoinType> { amount: u64; sending: &mut <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>; include <a href="AccountLimits.md#0x1_AccountLimits_ResetWindowAbortsIf">ResetWindowAbortsIf</a><CoinType>{ window: sending, limits_definition: <a href="AccountLimits.md#0x1_AccountLimits_spec_window_limits">spec_window_limits</a><CoinType>(sending) }; aborts_if <a href="AccountLimits.md#0x1_AccountLimits_spec_window_reset">spec_window_reset</a>(sending).window_outflow + amount > <a href="AccountLimits.md#0x1_AccountLimits_MAX_U64">MAX_U64</a> with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre>

<pre><code>schema <a href="AccountLimits.md#0x1_AccountLimits_CanWithdrawEnsures">CanWithdrawEnsures</a><CoinType> { result: bool; amount: u64; sending: &mut <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>; ensures result == <a href="AccountLimits.md#0x1_AccountLimits_spec_withdrawal_limits_ok">spec_withdrawal_limits_ok</a>(old(sending), amount); ensures if (result && !<a href="AccountLimits.md#0x1_AccountLimits_spec_window_unrestricted">spec_window_unrestricted</a>(old(sending))) sending == <a href="AccountLimits.md#0x1_AccountLimits_spec_update_outflow">spec_update_outflow</a>(<a href="AccountLimits.md#0x1_AccountLimits_spec_window_reset">spec_window_reset</a>(old(sending)), amount) else sending == <a href="AccountLimits.md#0x1_AccountLimits_spec_window_reset">spec_window_reset</a>(old(sending)) || sending == old(sending); } </code></pre>

Check whether withdrawal limits are satisfied.

<pre><code>define <a href="AccountLimits.md#0x1_AccountLimits_spec_withdrawal_limits_ok">spec_withdrawal_limits_ok</a><CoinType>(sending: <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>, amount: u64): bool { <a href="AccountLimits.md#0x1_AccountLimits_spec_window_unrestricted">spec_window_unrestricted</a>(sending) || <a href="AccountLimits.md#0x1_AccountLimits_spec_window_reset">spec_window_reset</a>(sending).window_outflow + amount <= <a href="AccountLimits.md#0x1_AccountLimits_spec_window_limits">spec_window_limits</a>(sending).max_outflow } </code></pre>

Update outflow.

<pre><code>define <a href="AccountLimits.md#0x1_AccountLimits_spec_update_outflow">spec_update_outflow</a><CoinType>(sending: <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>, amount: u64): <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType> { update_field(update_field(sending, window_outflow, sending.window_outflow + amount), tracked_balance, if (amount >= sending.tracked_balance) 0 else sending.tracked_balance - amount) } </code></pre> </details>

Function `is_unrestricted`

Determine whether the <code><a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a></code> resource has no restrictions.

<pre><code>fun <a href="AccountLimits.md#0x1_AccountLimits_is_unrestricted">is_unrestricted</a><CoinType>(limits_def: &<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">AccountLimits::LimitsDefinition</a><CoinType>): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="AccountLimits.md#0x1_AccountLimits_is_unrestricted">is_unrestricted</a><CoinType: store>(limits_def: &<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>): bool { limits_def.max_inflow == <a href="AccountLimits.md#0x1_AccountLimits_MAX_U64">MAX_U64</a> && limits_def.max_outflow == <a href="AccountLimits.md#0x1_AccountLimits_MAX_U64">MAX_U64</a> && limits_def.max_holding == <a href="AccountLimits.md#0x1_AccountLimits_MAX_U64">MAX_U64</a> && limits_def.time_period == <a href="AccountLimits.md#0x1_AccountLimits_ONE_DAY">ONE_DAY</a> } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if false; ensures result == <a href="AccountLimits.md#0x1_AccountLimits_spec_is_unrestricted">spec_is_unrestricted</a>(limits_def); </code></pre>

Checks whether the limits definition is unrestricted.

<pre><code>define <a href="AccountLimits.md#0x1_AccountLimits_spec_is_unrestricted">spec_is_unrestricted</a><CoinType>(limits_def: <a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>): bool { limits_def.max_inflow == max_u64() && limits_def.max_outflow == max_u64() && limits_def.max_holding == max_u64() && limits_def.time_period == 86400000000 } </code></pre> </details>

Function `limits_definition_address`

<pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_limits_definition_address">limits_definition_address</a><CoinType>(addr: address): address </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_limits_definition_address">limits_definition_address</a><CoinType: store>(addr: address): address acquires <a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a> { borrow_global<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(addr).limit_address } </code></pre> </details>

Function `has_limits_published`

<pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_has_limits_published">has_limits_published</a><CoinType>(addr: address): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_has_limits_published">has_limits_published</a><CoinType: store>(addr: address): bool { exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType>>(addr) } </code></pre> </details>

Function `has_window_published`

<pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_has_window_published">has_window_published</a><CoinType>(addr: address): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="AccountLimits.md#0x1_AccountLimits_has_window_published">has_window_published</a><CoinType: store>(addr: address): bool { exists<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(addr) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>ensures result == <a href="AccountLimits.md#0x1_AccountLimits_spec_has_window_published">spec_has_window_published</a><CoinType>(addr); </code></pre>

<pre><code>define <a href="AccountLimits.md#0x1_AccountLimits_spec_has_window_published">spec_has_window_published</a><CoinType>(addr: address): bool { exists<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType>>(addr) } </code></pre> </details>

Function `current_time`

<pre><code>fun <a href="AccountLimits.md#0x1_AccountLimits_current_time">current_time</a>(): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="AccountLimits.md#0x1_AccountLimits_current_time">current_time</a>(): u64 { if (<a href="DiemTimestamp.md#0x1_DiemTimestamp_is_genesis">DiemTimestamp::is_genesis</a>()) 0 else <a href="DiemTimestamp.md#0x1_DiemTimestamp_now_microseconds">DiemTimestamp::now_microseconds</a>() } </code></pre> </details>

Module Specification

<code><a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><CoinType></code> persists after publication.

<pre><code>invariant update [global] forall addr: address, coin_type: type where old(exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><coin_type>>(addr)): exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><coin_type>>(addr); </code></pre>

<code><a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><CoinType></code> persists after publication

<pre><code>invariant update [global] forall window_addr: address, coin_type: type where old(exists<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><coin_type>>(window_addr)): exists<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><coin_type>>(window_addr); </code></pre>

Invariant that <code><a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a></code> exists if a <code><a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a></code> exists.

<pre><code>invariant [global] forall window_addr: address, coin_type: type where exists<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><coin_type>>(window_addr): exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">LimitsDefinition</a><coin_type>>(global<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><coin_type>>(window_addr).limit_address); </code></pre>

Access Control

Only ParentVASP and ChildVASP can have the account limits [E1][E2][E3][E4][E5][E6][E7].

<pre><code>invariant [global] forall addr: address, coin_type: type where exists<<a href="AccountLimits.md#0x1_AccountLimits_Window">Window</a><coin_type>>(addr): exists<<a href="Roles.md#0x1_Roles_RoleId">Roles::RoleId</a>>(addr) && (global<<a href="Roles.md#0x1_Roles_RoleId">Roles::RoleId</a>>(addr).role_id == <a href="Roles.md#0x1_Roles_PARENT_VASP_ROLE_ID">Roles::PARENT_VASP_ROLE_ID</a> || global<<a href="Roles.md#0x1_Roles_RoleId">Roles::RoleId</a>>(addr).role_id == <a href="Roles.md#0x1_Roles_CHILD_VASP_ROLE_ID">Roles::CHILD_VASP_ROLE_ID</a>); </code></pre>

Module `0x1::AccountLimits`

Module 0x1::AccountLimits

Struct AccountLimitMutationCapability

Resource LimitsDefinition

Resource Window

Constants

Function grant_mutation_capability

Function update_deposit_limits

Function update_withdrawal_limits

Function publish_window

Function publish_unrestricted_limits

Function update_limits_definition

Function update_window_info

Function reset_window

Function can_receive_and_update_window

Function can_withdraw_and_update_window

Function is_unrestricted

Function limits_definition_address

Function has_limits_published

Function has_window_published

Function current_time

Module Specification

Access Control

Module `0x1::AccountLimits`

Struct `AccountLimitMutationCapability`

Resource `LimitsDefinition`

Resource `Window`

Function `grant_mutation_capability`

Function `update_deposit_limits`

Function `update_withdrawal_limits`

Function `publish_window`

Function `publish_unrestricted_limits`

Function `update_limits_definition`

Function `update_window_info`

Function `reset_window`

Function `can_receive_and_update_window`

Function `can_withdraw_and_update_window`

Function `is_unrestricted`

Function `limits_definition_address`

Function `has_limits_published`

Function `has_window_published`

Function `current_time`