Module `0x1::Diem`

The <code><a href="Diem.md#0x1_Diem">Diem</a></code> module describes the concept of a coin in the Diem framework. It introduces the resource <code><a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType></code>, representing a coin of given coin type. The module defines functions operating on coins as well as functionality like minting and burning of coins.

Struct Diem
Resource MintCapability
Resource BurnCapability
Struct MintEvent
Struct BurnEvent
Struct PreburnEvent
Struct CancelBurnEvent
Struct ToXDXExchangeRateUpdateEvent
Resource CurrencyInfo
Resource Preburn
Struct PreburnWithMetadata
Resource PreburnQueue
Constants
Function initialize
Function publish_burn_capability
Function mint
Function burn
Function cancel_burn
Function mint_with_capability
Function preburn_with_resource
Function create_preburn
Function publish_preburn_queue
Function publish_preburn_queue_to_account
Function publish_preburn_queue_to_account_for_test
Function upgrade_preburn
Function add_preburn_to_queue
Function preburn_to
Function remove_preburn_from_queue
Function burn_with_capability
Function burn_with_resource_cap
Function cancel_burn_with_capability
Function burn_now
Function remove_burn_capability
Function preburn_value
Function zero
Function value
Function split
Function withdraw
Function withdraw_all
Function join
Function deposit
Function destroy_zero
Function register_currency
Function register_SCS_currency
Function market_cap
Function approx_xdx_for_value
Function approx_xdx_for_coin
Function is_currency
Function is_SCS_currency
Function is_synthetic_currency
Function scaling_factor
Function fractional_part
Function currency_code
Function update_xdx_exchange_rate
Function xdx_exchange_rate
Function update_minting_ability
Function assert_is_currency
Function assert_is_SCS_currency
Module Specification
- Access Control
- Helper Functions

<pre><code>use <a href="CoreAddresses.md#0x1_CoreAddresses">0x1::CoreAddresses</a>; 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="../../../../../../move-stdlib/docs/Event.md#0x1_Event">0x1::Event</a>; use <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32">0x1::FixedPoint32</a>; use <a href="RegisteredCurrencies.md#0x1_RegisteredCurrencies">0x1::RegisteredCurrencies</a>; use <a href="Roles.md#0x1_Roles">0x1::Roles</a>; use <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer">0x1::Signer</a>; use <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector">0x1::Vector</a>; </code></pre>

Struct `Diem`

The <code><a href="Diem.md#0x1_Diem">Diem</a></code> resource defines the Diem coin for each currency in Diem. Each "coin" is coupled with a type <code>CoinType</code> specifying the currency of the coin, and a <code>value</code> field specifying the value of the coin (in the base units of the currency <code>CoinType</code> and specified in the <code><a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a></code> resource for that <code>CoinType</code> published under the <code>@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a></code> account address).

<pre><code>struct <a href="Diem.md#0x1_Diem">Diem</a><CoinType> has store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>value: u64</code> </dt> <dd> The value of this coin in the base units for <code>CoinType</code> </dd> </dl> </details>

Resource `MintCapability`

The <code><a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a></code> resource defines a capability to allow minting of coins of <code>CoinType</code> currency by the holder of this capability. This capability is held only either by the <code>@TreasuryCompliance</code> account or the <code>DiemFramework::XDX</code> module (and <code>@DiemRoot</code> in testnet).

<pre><code>struct <a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType> has store, key </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>dummy_field: bool</code> </dt> <dd> </dd> </dl> </details>

Resource `BurnCapability`

The <code><a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a></code> resource defines a capability to allow coins of <code>CoinType</code> currency to be burned by the holder of it.

<pre><code>struct <a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType> has store, key </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>dummy_field: bool</code> </dt> <dd> </dd> </dl> </details>

Struct `MintEvent`

A <code><a href="Diem.md#0x1_Diem_MintEvent">MintEvent</a></code> is emitted every time a Diem coin is minted. This contains the <code>amount</code> minted (in base units of the currency being minted) along with the <code>currency_code</code> for the coin(s) being minted, and that is defined in the <code>currency_code</code> field of the <code><a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a></code> resource for the currency.

<pre><code>struct <a href="Diem.md#0x1_Diem_MintEvent">MintEvent</a> has drop, store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>amount: u64</code> </dt> <dd> Funds added to the system </dd> <dt> <code>currency_code: vector<u8></code> </dt> <dd> ASCII encoded symbol for the coin type (e.g., "XDX") </dd> </dl> </details>

Struct `BurnEvent`

A <code><a href="Diem.md#0x1_Diem_BurnEvent">BurnEvent</a></code> is emitted every time a non-synthetic Diem coin (i.e., a Diem coin with false <code>is_synthetic</code> field) is burned. It contains the <code>amount</code> burned in base units for the currency, along with the <code>currency_code</code> for the coins being burned (and as defined in the <code><a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a></code> resource for that currency). It also contains the <code>preburn_address</code> from which the coin is extracted for burning.

<pre><code>struct <a href="Diem.md#0x1_Diem_BurnEvent">BurnEvent</a> has drop, store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>amount: u64</code> </dt> <dd> Funds removed from the system </dd> <dt> <code>currency_code: vector<u8></code> </dt> <dd> ASCII encoded symbol for the coin type (e.g., "XDX") </dd> <dt> <code>preburn_address: address</code> </dt> <dd> Address with the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource that stored the now-burned funds </dd> </dl> </details>

Struct `PreburnEvent`

A <code><a href="Diem.md#0x1_Diem_PreburnEvent">PreburnEvent</a></code> is emitted every time an <code>amount</code> of funds with a coin type <code>currency_code</code> is enqueued in the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource under the account at the address <code>preburn_address</code>.

<pre><code>struct <a href="Diem.md#0x1_Diem_PreburnEvent">PreburnEvent</a> has drop, store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>amount: u64</code> </dt> <dd> The amount of funds waiting to be removed (burned) from the system </dd> <dt> <code>currency_code: vector<u8></code> </dt> <dd> ASCII encoded symbol for the coin type (e.g., "XDX") </dd> <dt> <code>preburn_address: address</code> </dt> <dd> Address with the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource that now holds the funds </dd> </dl> </details>

Struct `CancelBurnEvent`

A <code><a href="Diem.md#0x1_Diem_CancelBurnEvent">CancelBurnEvent</a></code> is emitted every time funds of <code>amount</code> in a <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> resource held in a <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> at <code>preburn_address</code> is canceled (removed from the preburn queue, but not burned). The currency of the funds is given by the <code>currency_code</code> as defined in the <code><a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a></code> for that currency.

<pre><code>struct <a href="Diem.md#0x1_Diem_CancelBurnEvent">CancelBurnEvent</a> has drop, store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>amount: u64</code> </dt> <dd> The amount of funds returned </dd> <dt> <code>currency_code: vector<u8></code> </dt> <dd> ASCII encoded symbol for the coin type (e.g., "XDX") </dd> <dt> <code>preburn_address: address</code> </dt> <dd> Address of the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource that held the now-returned funds. </dd> </dl> </details>

Struct `ToXDXExchangeRateUpdateEvent`

An <code><a href="Diem.md#0x1_Diem_ToXDXExchangeRateUpdateEvent">ToXDXExchangeRateUpdateEvent</a></code> is emitted every time the to-XDX exchange rate for the currency given by <code>currency_code</code> is updated.

<pre><code>struct <a href="Diem.md#0x1_Diem_ToXDXExchangeRateUpdateEvent">ToXDXExchangeRateUpdateEvent</a> has drop, store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>currency_code: vector<u8></code> </dt> <dd> The currency code of the currency whose exchange rate was updated. </dd> <dt> <code>new_to_xdx_exchange_rate: u64</code> </dt> <dd> The new on-chain to-XDX exchange rate between the <code>currency_code</code> currency and XDX. Represented in conversion between the (on-chain) base-units for the currency and microdiem. </dd> </dl> </details>

Resource `CurrencyInfo`

The <code><a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType></code> resource stores the various pieces of information needed for a currency (<code>CoinType</code>) that is registered on-chain. This resource must be published under the address given by <code>@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a></code> in order for the registration of <code>CoinType</code> as a recognized currency on-chain to be successful. At the time of registration, the <code><a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType></code> and <code><a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType></code> capabilities are returned to the caller. Unless they are specified otherwise the fields in this resource are immutable.

<pre><code>struct <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType> has key </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>total_value: u128</code> </dt> <dd> The total value for the currency represented by <code>CoinType</code>. Mutable. </dd> <dt> <code>preburn_value: u64</code> </dt> <dd> Value of funds that are in the process of being burned. Mutable. </dd> <dt> <code>to_xdx_exchange_rate: <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32_FixedPoint32">FixedPoint32::FixedPoint32</a></code> </dt> <dd> The (rough) exchange rate from <code>CoinType</code> to <code><a href="XDX.md#0x1_XDX">XDX</a></code>. Mutable. </dd> <dt> <code>is_synthetic: bool</code> </dt> <dd> Holds whether or not this currency is synthetic (contributes to the off-chain reserve) or not. An example of such a synthetic currency would be the XDX. </dd> <dt> <code>scaling_factor: u64</code> </dt> <dd> The scaling factor for the coin (i.e. the amount to divide by to get to the human-readable representation for this currency). e.g. 10^6 for <code><a href="XUS.md#0x1_XUS">XUS</a></code> </dd> <dt> <code>fractional_part: u64</code> </dt> <dd> The smallest fractional part (number of decimal places) to be used in the human-readable representation for the currency (e.g. 10^2 for <code><a href="XUS.md#0x1_XUS">XUS</a></code> cents) </dd> <dt> <code>currency_code: vector<u8></code> </dt> <dd> The code symbol for this <code>CoinType</code>. ASCII encoded. e.g. for "XDX" this is x"584458". No character limit. </dd> <dt> <code>can_mint: bool</code> </dt> <dd> Minting of new currency of CoinType is allowed only if this field is true. We may want to disable the ability to mint further coins of a currency while that currency is still around. This allows us to keep the currency in circulation while disallowing further creation of coins in the <code>CoinType</code> currency. Mutable. </dd> <dt> <code>mint_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_EventHandle">Event::EventHandle</a><<a href="Diem.md#0x1_Diem_MintEvent">Diem::MintEvent</a>></code> </dt> <dd> Event stream for minting and where <code><a href="Diem.md#0x1_Diem_MintEvent">MintEvent</a></code>s will be emitted. </dd> <dt> <code>burn_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_EventHandle">Event::EventHandle</a><<a href="Diem.md#0x1_Diem_BurnEvent">Diem::BurnEvent</a>></code> </dt> <dd> Event stream for burning, and where <code><a href="Diem.md#0x1_Diem_BurnEvent">BurnEvent</a></code>s will be emitted. </dd> <dt> <code>preburn_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_EventHandle">Event::EventHandle</a><<a href="Diem.md#0x1_Diem_PreburnEvent">Diem::PreburnEvent</a>></code> </dt> <dd> Event stream for preburn requests, and where all <code><a href="Diem.md#0x1_Diem_PreburnEvent">PreburnEvent</a></code>s for this <code>CoinType</code> will be emitted. </dd> <dt> <code>cancel_burn_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_EventHandle">Event::EventHandle</a><<a href="Diem.md#0x1_Diem_CancelBurnEvent">Diem::CancelBurnEvent</a>></code> </dt> <dd> Event stream for all cancelled preburn requests for this <code>CoinType</code>. </dd> <dt> <code>exchange_rate_update_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_EventHandle">Event::EventHandle</a><<a href="Diem.md#0x1_Diem_ToXDXExchangeRateUpdateEvent">Diem::ToXDXExchangeRateUpdateEvent</a>></code> </dt> <dd> Event stream for emiting exchange rate change events </dd> </dl> </details> <details> <summary>Specification</summary>

Data structure invariant for CurrencyInfo. Asserts that <code><a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>.scaling_factor</code> is always greater than 0 and not greater than <code><a href="Diem.md#0x1_Diem_MAX_SCALING_FACTOR">MAX_SCALING_FACTOR</a></code>

<pre><code>invariant 0 < scaling_factor && <a href="Diem.md#0x1_Diem_scaling_factor">scaling_factor</a> <= <a href="Diem.md#0x1_Diem_MAX_SCALING_FACTOR">MAX_SCALING_FACTOR</a>; </code></pre> </details>

Resource `Preburn`

A holding area where funds that will subsequently be burned wait while their underlying assets are moved off-chain. This resource can only be created by the holder of a <code><a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a></code> or during an upgrade process to the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> by a designated dealer. An account that contains this address has the authority to initiate a burn request. A burn request can be resolved by the holder of a <code><a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a></code> by either (1) burning the funds, or (2) returning the funds to the account that initiated the burn request.

<pre><code>struct <a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType> has store, key </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>to_burn: <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType></code> </dt> <dd> A single pending burn amount. This is an element in the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource published under each Designated Dealer account. </dd> </dl> </details>

Struct `PreburnWithMetadata`

A preburn request, along with (an opaque to Move) metadata that is associated with the preburn request.

<pre><code>struct <a href="Diem.md#0x1_Diem_PreburnWithMetadata">PreburnWithMetadata</a><CoinType> has store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>preburn: <a href="Diem.md#0x1_Diem_Preburn">Diem::Preburn</a><CoinType></code> </dt> <dd> </dd> <dt> <code>metadata: vector<u8></code> </dt> <dd> </dd> </dl> </details>

Resource `PreburnQueue`

A queue of preburn requests. This is a FIFO queue whose elements are indexed by the value held within each preburn resource in the <code>preburns</code> field. When burning or cancelling a burn of a given <code>amount</code>, the <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> resource with with the smallest index in this queue matching <code>amount</code> in its <code>to_burn</code> coin's <code>value</code> field will be removed and its contents either (1) burned, or (2) returned back to the holding DD's account balance. Every <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> resource in the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> must have a nonzero coin value within it. This resource can be created by either the TreasuryCompliance account, or during the upgrade process, by a designated dealer with an existing <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> resource in <code>CoinType</code>

<pre><code>struct <a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType> has key </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>preburns: vector<<a href="Diem.md#0x1_Diem_PreburnWithMetadata">Diem::PreburnWithMetadata</a><CoinType>></code> </dt> <dd> The queue of preburn requests </dd> </dl> </details> <details> <summary>Specification</summary>

The number of outstanding preburn requests is bounded.

<pre><code>invariant len(preburns) <= <a href="Diem.md#0x1_Diem_MAX_OUTSTANDING_PREBURNS">MAX_OUTSTANDING_PREBURNS</a>; </code></pre>

No preburn request can have a zero value. The <code>value</code> field of any coin in a <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> resource within this field must be nonzero.

<pre><code>invariant forall i in 0..len(preburns): preburns[i].preburn.to_burn.value > 0; </code></pre> </details>

Constants

Maximum u64 value.

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

Maximum u128 value.

<pre><code>const <a href="Diem.md#0x1_Diem_MAX_U128">MAX_U128</a>: u128 = 340282366920938463463374607431768211455; </code></pre>

A property expected of a <code><a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a></code> resource didn't hold

<pre><code>const <a href="Diem.md#0x1_Diem_ECURRENCY_INFO">ECURRENCY_INFO</a>: u64 = 1; </code></pre>

A withdrawal greater than the value of the coin was attempted.

<pre><code>const <a href="Diem.md#0x1_Diem_EAMOUNT_EXCEEDS_COIN_VALUE">EAMOUNT_EXCEEDS_COIN_VALUE</a>: u64 = 10; </code></pre>

A <code><a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a></code> resource is in an unexpected state.

<pre><code>const <a href="Diem.md#0x1_Diem_EBURN_CAPABILITY">EBURN_CAPABILITY</a>: u64 = 0; </code></pre>

A property expected of the coin provided didn't hold

<pre><code>const <a href="Diem.md#0x1_Diem_ECOIN">ECOIN</a>: u64 = 7; </code></pre>

The destruction of a non-zero coin was attempted. Non-zero coins must be burned.

<pre><code>const <a href="Diem.md#0x1_Diem_EDESTRUCTION_OF_NONZERO_COIN">EDESTRUCTION_OF_NONZERO_COIN</a>: u64 = 8; </code></pre>

The currency specified is a synthetic (non-fiat) currency

<pre><code>const <a href="Diem.md#0x1_Diem_EIS_SYNTHETIC_CURRENCY">EIS_SYNTHETIC_CURRENCY</a>: u64 = 6; </code></pre>

Minting is not allowed for the specified currency

<pre><code>const <a href="Diem.md#0x1_Diem_EMINTING_NOT_ALLOWED">EMINTING_NOT_ALLOWED</a>: u64 = 5; </code></pre>

A property expected of <code><a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a></code> didn't hold

<pre><code>const <a href="Diem.md#0x1_Diem_EMINT_CAPABILITY">EMINT_CAPABILITY</a>: u64 = 9; </code></pre>

A property expected of a <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> resource didn't hold

<pre><code>const <a href="Diem.md#0x1_Diem_EPREBURN">EPREBURN</a>: u64 = 2; </code></pre>

A burn was attempted on <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> resource that cointained no coins

<pre><code>const <a href="Diem.md#0x1_Diem_EPREBURN_EMPTY">EPREBURN_EMPTY</a>: u64 = 4; </code></pre>

A preburn with a matching amount in the preburn queue was not found.

<pre><code>const <a href="Diem.md#0x1_Diem_EPREBURN_NOT_FOUND">EPREBURN_NOT_FOUND</a>: u64 = 12; </code></pre>

The preburn slot is already occupied with coins to be burned.

<pre><code>const <a href="Diem.md#0x1_Diem_EPREBURN_OCCUPIED">EPREBURN_OCCUPIED</a>: u64 = 3; </code></pre>

A property expected of the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource didn't hold.

<pre><code>const <a href="Diem.md#0x1_Diem_EPREBURN_QUEUE">EPREBURN_QUEUE</a>: u64 = 11; </code></pre>

The maximum number of preburn requests that can be outstanding for a given designated dealer/currency.

<pre><code>const <a href="Diem.md#0x1_Diem_MAX_OUTSTANDING_PREBURNS">MAX_OUTSTANDING_PREBURNS</a>: u64 = 256; </code></pre>

The maximum value for <code><a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>.scaling_factor</code>

<pre><code>const <a href="Diem.md#0x1_Diem_MAX_SCALING_FACTOR">MAX_SCALING_FACTOR</a>: u64 = 10000000000; </code></pre>

Function `initialize`

Initialization of the <code><a href="Diem.md#0x1_Diem">Diem</a></code> module. Initializes the set of registered currencies in the <code>DiemFramework::RegisteredCurrencies</code> on-chain config, and publishes the <code>CurrencyRegistrationCapability</code> under the <code>@DiemRoot</code>. This can only be called from genesis.

<pre><code>public fun <a href="Diem.md#0x1_Diem_initialize">initialize</a>(dr_account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_initialize">initialize</a>( dr_account: &signer, ) { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_genesis">DiemTimestamp::assert_genesis</a>(); // Operational constraint <a href="CoreAddresses.md#0x1_CoreAddresses_assert_diem_root">CoreAddresses::assert_diem_root</a>(dr_account); <a href="RegisteredCurrencies.md#0x1_RegisteredCurrencies_initialize">RegisteredCurrencies::initialize</a>(dr_account); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotGenesis">DiemTimestamp::AbortsIfNotGenesis</a>; include <a href="CoreAddresses.md#0x1_CoreAddresses_AbortsIfNotDiemRoot">CoreAddresses::AbortsIfNotDiemRoot</a>{account: dr_account}; include <a href="RegisteredCurrencies.md#0x1_RegisteredCurrencies_InitializeAbortsIf">RegisteredCurrencies::InitializeAbortsIf</a>; include <a href="RegisteredCurrencies.md#0x1_RegisteredCurrencies_InitializeEnsures">RegisteredCurrencies::InitializeEnsures</a>; </code></pre> </details>

Function `publish_burn_capability`

Publishes the <code><a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a></code> <code>cap</code> for the <code>CoinType</code> currency under <code>account</code>. <code>CoinType</code> must be a registered currency type. The caller must pass a treasury compliance account.

<pre><code>public fun <a href="Diem.md#0x1_Diem_publish_burn_capability">publish_burn_capability</a><CoinType>(tc_account: &signer, cap: <a href="Diem.md#0x1_Diem_BurnCapability">Diem::BurnCapability</a><CoinType>) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_publish_burn_capability">publish_burn_capability</a><CoinType>( tc_account: &signer, cap: <a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>, ) { <a href="Roles.md#0x1_Roles_assert_treasury_compliance">Roles::assert_treasury_compliance</a>(tc_account); <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>(); assert( !exists<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(tc_account)), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_already_published">Errors::already_published</a>(<a href="Diem.md#0x1_Diem_EBURN_CAPABILITY">EBURN_CAPABILITY</a>) ); move_to(tc_account, cap) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>aborts_if !<a href="Diem.md#0x1_Diem_spec_is_currency">spec_is_currency</a><CoinType>(); include <a href="Diem.md#0x1_Diem_PublishBurnCapAbortsIfs">PublishBurnCapAbortsIfs</a><CoinType>; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_PublishBurnCapAbortsIfs">PublishBurnCapAbortsIfs</a><CoinType> { tc_account: &signer; } </code></pre>

Must abort if tc_account does not have the TreasuryCompliance role. Only a TreasuryCompliance account can have the BurnCapability [H3].

<pre><code>schema <a href="Diem.md#0x1_Diem_PublishBurnCapAbortsIfs">PublishBurnCapAbortsIfs</a><CoinType> { include <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">Roles::AbortsIfNotTreasuryCompliance</a>{account: tc_account}; aborts_if exists<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(tc_account)) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_PublishBurnCapEnsures">PublishBurnCapEnsures</a><CoinType> { tc_account: &signer; ensures exists<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(tc_account)); } </code></pre> </details>

Function `mint`

Mints <code>amount</code> of currency. The <code>account</code> must hold a <code><a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType></code> at the top-level in order for this call to be successful.

<pre><code>public fun <a href="Diem.md#0x1_Diem_mint">mint</a><CoinType>(account: &signer, value: u64): <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_mint">mint</a><CoinType>(account: &signer, value: u64): <a href="Diem.md#0x1_Diem">Diem</a><CoinType> acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>, <a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a> { let addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); assert(exists<<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_requires_capability">Errors::requires_capability</a>(<a href="Diem.md#0x1_Diem_EMINT_CAPABILITY">EMINT_CAPABILITY</a>)); <a href="Diem.md#0x1_Diem_mint_with_capability">mint_with_capability</a>( value, borrow_global<<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>>(addr) ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>modifies global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); ensures exists<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); </code></pre>

Must abort if the account does not have the MintCapability [H1].

<pre><code>aborts_if !exists<<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account)) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_REQUIRES_CAPABILITY">Errors::REQUIRES_CAPABILITY</a>; include <a href="Diem.md#0x1_Diem_MintAbortsIf">MintAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_MintEnsures">MintEnsures</a><CoinType>; </code></pre> </details>

Function `burn`

Burns the coins held in the first <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> request in the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource held under <code>preburn_address</code> that is equal to <code>amount</code>. Calls to this functions will fail if the <code>account</code> does not have a published <code><a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a></code> for the <code>CoinType</code> published under it, or if there is not a <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> request in the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> that does not equal <code>amount</code>.

<pre><code>public fun <a href="Diem.md#0x1_Diem_burn">burn</a><CoinType>(account: &signer, preburn_address: address, amount: u64) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_burn">burn</a><CoinType>( account: &signer, preburn_address: address, amount: u64, ) acquires <a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a>, <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>, <a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a> { let addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); assert(exists<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_requires_capability">Errors::requires_capability</a>(<a href="Diem.md#0x1_Diem_EBURN_CAPABILITY">EBURN_CAPABILITY</a>)); <a href="Diem.md#0x1_Diem_burn_with_capability">burn_with_capability</a>( preburn_address, borrow_global<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(addr), amount ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="Diem.md#0x1_Diem_BurnAbortsIf">BurnAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_BurnEnsures">BurnEnsures</a><CoinType>; include <a href="Diem.md#0x1_Diem_BurnWithResourceCapEmits">BurnWithResourceCapEmits</a><CoinType>{preburn: <a href="Diem.md#0x1_Diem_spec_make_preburn">spec_make_preburn</a>(amount)}; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_BurnAbortsIf">BurnAbortsIf</a><CoinType> { account: signer; preburn_address: address; } </code></pre>

Must abort if the account does not have the BurnCapability [H3].

<pre><code>schema <a href="Diem.md#0x1_Diem_BurnAbortsIf">BurnAbortsIf</a><CoinType> { aborts_if !exists<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account)) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_REQUIRES_CAPABILITY">Errors::REQUIRES_CAPABILITY</a>; include <a href="Diem.md#0x1_Diem_BurnWithCapabilityAbortsIf">BurnWithCapabilityAbortsIf</a><CoinType>; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_BurnEnsures">BurnEnsures</a><CoinType> { account: signer; preburn_address: address; include <a href="Diem.md#0x1_Diem_BurnWithCapabilityEnsures">BurnWithCapabilityEnsures</a><CoinType>; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_AbortsIfNoPreburnQueue">AbortsIfNoPreburnQueue</a><CoinType> { preburn_address: address; aborts_if !exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(preburn_address) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; } </code></pre> </details>

Function `cancel_burn`

Cancels the <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> request in the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource held under the <code>preburn_address</code> with a value equal to <code>amount</code>, and returns the coins. Calls to this will fail if the sender does not have a published <code><a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType></code>, or if there is no preburn request outstanding in the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource under <code>preburn_address</code> with a value equal to <code>amount</code>.

<pre><code>public fun <a href="Diem.md#0x1_Diem_cancel_burn">cancel_burn</a><CoinType>(account: &signer, preburn_address: address, amount: u64): <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_cancel_burn">cancel_burn</a><CoinType>( account: &signer, preburn_address: address, amount: u64, ): <a href="Diem.md#0x1_Diem">Diem</a><CoinType> acquires <a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a>, <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>, <a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a> { <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>(); let addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); assert(exists<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_requires_capability">Errors::requires_capability</a>(<a href="Diem.md#0x1_Diem_EBURN_CAPABILITY">EBURN_CAPABILITY</a>)); <a href="Diem.md#0x1_Diem_cancel_burn_with_capability">cancel_burn_with_capability</a>( preburn_address, borrow_global<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(addr), amount, ) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>let currency_info = global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); let post post_currency_info = global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); modifies global<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(preburn_address); modifies global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); include <a href="Diem.md#0x1_Diem_CancelBurnAbortsIf">CancelBurnAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_CancelBurnWithCapEnsures">CancelBurnWithCapEnsures</a><CoinType>; include <a href="Diem.md#0x1_Diem_CancelBurnWithCapEmits">CancelBurnWithCapEmits</a><CoinType>; ensures exists<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); ensures exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(preburn_address); ensures post_currency_info == update_field( currency_info, preburn_value, post_currency_info.preburn_value ); ensures result.value == amount; ensures result.value > 0; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_CancelBurnAbortsIf">CancelBurnAbortsIf</a><CoinType> { account: signer; preburn_address: address; amount: u64; } </code></pre>

Must abort if the account does not have the BurnCapability [H3].

<pre><code>schema <a href="Diem.md#0x1_Diem_CancelBurnAbortsIf">CancelBurnAbortsIf</a><CoinType> { aborts_if !exists<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account)) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_REQUIRES_CAPABILITY">Errors::REQUIRES_CAPABILITY</a>; include <a href="Diem.md#0x1_Diem_CancelBurnWithCapAbortsIf">CancelBurnWithCapAbortsIf</a><CoinType>; } </code></pre> </details>

Function `mint_with_capability`

Mint a new <code><a href="Diem.md#0x1_Diem">Diem</a></code> coin of <code>CoinType</code> currency worth <code>value</code>. The caller must have a reference to a <code><a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType></code>. Only the treasury compliance account or the <code>DiemFramework::XDX</code> module can acquire such a reference.

<pre><code>public fun <a href="Diem.md#0x1_Diem_mint_with_capability">mint_with_capability</a><CoinType>(value: u64, _capability: &<a href="Diem.md#0x1_Diem_MintCapability">Diem::MintCapability</a><CoinType>): <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_mint_with_capability">mint_with_capability</a><CoinType>( value: u64, _capability: &<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType> ): <a href="Diem.md#0x1_Diem">Diem</a><CoinType> acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>(); let currency_code = <a href="Diem.md#0x1_Diem_currency_code">currency_code</a><CoinType>(); // update market cap resource to reflect minting let info = borrow_global_mut<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); assert(info.can_mint, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(<a href="Diem.md#0x1_Diem_EMINTING_NOT_ALLOWED">EMINTING_NOT_ALLOWED</a>)); assert(<a href="Diem.md#0x1_Diem_MAX_U128">MAX_U128</a> - info.total_value >= (value as u128), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="Diem.md#0x1_Diem_ECURRENCY_INFO">ECURRENCY_INFO</a>)); info.total_value = info.total_value + (value as u128); // don't emit mint events for synthetic currenices as this does not // change the total value of fiat currencies held on-chain. if (!info.is_synthetic) { <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_emit_event">Event::emit_event</a>( &mut info.mint_events, <a href="Diem.md#0x1_Diem_MintEvent">MintEvent</a>{ amount: value, currency_code, } ); }; <a href="Diem.md#0x1_Diem">Diem</a><CoinType> { value } } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; modifies global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); ensures exists<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); include <a href="Diem.md#0x1_Diem_MintAbortsIf">MintAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_MintEnsures">MintEnsures</a><CoinType>; include <a href="Diem.md#0x1_Diem_MintEmits">MintEmits</a><CoinType>; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_MintAbortsIf">MintAbortsIf</a><CoinType> { value: u64; include <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">AbortsIfNoCurrency</a><CoinType>; aborts_if !<a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().can_mint with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_STATE">Errors::INVALID_STATE</a>; aborts_if <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().total_value + value > max_u128() with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_MintEnsures">MintEnsures</a><CoinType> { value: u64; result: <a href="Diem.md#0x1_Diem">Diem</a><CoinType>; let currency_info = global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); let post post_currency_info = global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); ensures exists<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); ensures post_currency_info == update_field(currency_info, total_value, currency_info.total_value + value); ensures result.value == value; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_MintEmits">MintEmits</a><CoinType> { value: u64; let currency_info = global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); let handle = currency_info.mint_events; let msg = <a href="Diem.md#0x1_Diem_MintEvent">MintEvent</a>{ amount: value, currency_code: currency_info.currency_code, }; emits msg to handle if !currency_info.is_synthetic; } </code></pre> </details>

Function `preburn_with_resource`

Add the <code>coin</code> to the <code>preburn.to_burn</code> field in the <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> resource held in the preburn queue at the address <code>preburn_address</code> if it is empty, otherwise raise a <code><a href="Diem.md#0x1_Diem_EPREBURN_OCCUPIED">EPREBURN_OCCUPIED</a></code> Error. Emits a <code><a href="Diem.md#0x1_Diem_PreburnEvent">PreburnEvent</a></code> to the <code>preburn_events</code> event stream in the <code><a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a></code> for the <code>CoinType</code> passed in. However, if the currency being preburned is a synthetic currency (<code>is_synthetic = true</code>) then no <code><a href="Diem.md#0x1_Diem_PreburnEvent">PreburnEvent</a></code> will be emitted.

<pre><code>fun <a href="Diem.md#0x1_Diem_preburn_with_resource">preburn_with_resource</a><CoinType>(coin: <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType>, preburn: &mut <a href="Diem.md#0x1_Diem_Preburn">Diem::Preburn</a><CoinType>, preburn_address: address) </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="Diem.md#0x1_Diem_preburn_with_resource">preburn_with_resource</a><CoinType>( coin: <a href="Diem.md#0x1_Diem">Diem</a><CoinType>, preburn: &mut <a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>, preburn_address: address, ) acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { let coin_value = <a href="Diem.md#0x1_Diem_value">value</a>(&coin); // Throw if already occupied assert(<a href="Diem.md#0x1_Diem_value">value</a>(&preburn.to_burn) == 0, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(<a href="Diem.md#0x1_Diem_EPREBURN_OCCUPIED">EPREBURN_OCCUPIED</a>)); <a href="Diem.md#0x1_Diem_deposit">deposit</a>(&mut preburn.to_burn, coin); let currency_code = <a href="Diem.md#0x1_Diem_currency_code">currency_code</a><CoinType>(); let info = borrow_global_mut<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); assert(<a href="Diem.md#0x1_Diem_MAX_U64">MAX_U64</a> - info.preburn_value >= coin_value, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="Diem.md#0x1_Diem_ECOIN">ECOIN</a>)); info.preburn_value = info.preburn_value + coin_value; // don't emit preburn events for synthetic currenices as this does not // change the total value of fiat currencies held on-chain, and // therefore no off-chain movement of the backing coins needs to be // performed. if (!info.is_synthetic) { <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_emit_event">Event::emit_event</a>( &mut info.preburn_events, <a href="Diem.md#0x1_Diem_PreburnEvent">PreburnEvent</a>{ amount: coin_value, currency_code, preburn_address, } ); }; } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>modifies global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); ensures exists<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); include <a href="Diem.md#0x1_Diem_PreburnWithResourceAbortsIf">PreburnWithResourceAbortsIf</a><CoinType>{amount: coin.value}; include <a href="Diem.md#0x1_Diem_PreburnEnsures">PreburnEnsures</a><CoinType>{amount: coin.value}; include <a href="Diem.md#0x1_Diem_PreburnWithResourceEmits">PreburnWithResourceEmits</a><CoinType>{amount: coin.value}; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_PreburnWithResourceAbortsIf">PreburnWithResourceAbortsIf</a><CoinType> { amount: u64; preburn: <a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>; aborts_if preburn.to_burn.value > 0 with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_STATE">Errors::INVALID_STATE</a>; include <a href="Diem.md#0x1_Diem_PreburnAbortsIf">PreburnAbortsIf</a><CoinType>; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_PreburnAbortsIf">PreburnAbortsIf</a><CoinType> { amount: u64; include <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">AbortsIfNoCurrency</a><CoinType>; aborts_if <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().preburn_value + amount > <a href="Diem.md#0x1_Diem_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="Diem.md#0x1_Diem_PreburnEnsures">PreburnEnsures</a><CoinType> { amount: u64; preburn: <a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>; let info = <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>(); let post post_info = <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>(); ensures post_info == update_field(info, preburn_value, info.preburn_value + amount); } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_PreburnWithResourceEmits">PreburnWithResourceEmits</a><CoinType> { amount: u64; preburn_address: address; let info = <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>(); let currency_code = <a href="Diem.md#0x1_Diem_spec_currency_code">spec_currency_code</a><CoinType>(); let handle = info.preburn_events; let msg = <a href="Diem.md#0x1_Diem_PreburnEvent">PreburnEvent</a> { amount, currency_code, preburn_address, }; emits msg to handle if !info.is_synthetic; } </code></pre> </details>

Function `create_preburn`

Create a <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType></code> resource. This is useful for places where a module needs to be able to burn coins outside of a Designated Dealer, e.g., for transaction fees, or for the XDX reserve.

<pre><code>public fun <a href="Diem.md#0x1_Diem_create_preburn">create_preburn</a><CoinType>(tc_account: &signer): <a href="Diem.md#0x1_Diem_Preburn">Diem::Preburn</a><CoinType> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_create_preburn">create_preburn</a><CoinType>( tc_account: &signer ): <a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType> { <a href="Roles.md#0x1_Roles_assert_treasury_compliance">Roles::assert_treasury_compliance</a>(tc_account); <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>(); <a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType> { to_burn: <a href="Diem.md#0x1_Diem_zero">zero</a><CoinType>() } } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="Diem.md#0x1_Diem_CreatePreburnAbortsIf">CreatePreburnAbortsIf</a><CoinType>; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_CreatePreburnAbortsIf">CreatePreburnAbortsIf</a><CoinType> { tc_account: signer; include <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">Roles::AbortsIfNotTreasuryCompliance</a>{account: tc_account}; include <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">AbortsIfNoCurrency</a><CoinType>; } </code></pre> </details>

Function `publish_preburn_queue`

Publish an empty <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource under the Designated Dealer dealer account <code>account</code>.

<pre><code>fun <a href="Diem.md#0x1_Diem_publish_preburn_queue">publish_preburn_queue</a><CoinType>(account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="Diem.md#0x1_Diem_publish_preburn_queue">publish_preburn_queue</a><CoinType>( account: &signer ) { let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); <a href="Roles.md#0x1_Roles_assert_designated_dealer">Roles::assert_designated_dealer</a>(account); <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>(); assert( !exists<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(account_addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(<a href="Diem.md#0x1_Diem_EPREBURN">EPREBURN</a>) ); assert( !exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_already_published">Errors::already_published</a>(<a href="Diem.md#0x1_Diem_EPREBURN_QUEUE">EPREBURN_QUEUE</a>) ); move_to(account, <a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType> { preburns: <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_empty">Vector::empty</a>() }) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); modifies global<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr); aborts_if exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; aborts_if exists<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(account_addr) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_STATE">Errors::INVALID_STATE</a>; include <a href="Diem.md#0x1_Diem_PublishPreburnQueueAbortsIf">PublishPreburnQueueAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_PublishPreburnQueueEnsures">PublishPreburnQueueEnsures</a><CoinType>; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_PublishPreburnQueueAbortsIf">PublishPreburnQueueAbortsIf</a><CoinType> { account: signer; include <a href="Roles.md#0x1_Roles_AbortsIfNotDesignatedDealer">Roles::AbortsIfNotDesignatedDealer</a>; include <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">AbortsIfNoCurrency</a><CoinType>; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_PublishPreburnQueueEnsures">PublishPreburnQueueEnsures</a><CoinType> { account: signer; let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); ensures exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr); ensures !exists<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(account_addr); ensures <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(global<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr).preburns) == 0; } </code></pre> </details>

Function `publish_preburn_queue_to_account`

Publish a <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> resource under <code>account</code>. This function is used for bootstrapping the designated dealer at account-creation time, and the association TC account <code>tc_account</code> (at <code>@TreasuryCompliance</code>) is creating this resource for the designated dealer <code>account</code>.

<pre><code>public(friend) fun <a href="Diem.md#0x1_Diem_publish_preburn_queue_to_account">publish_preburn_queue_to_account</a><CoinType>(account: &signer, tc_account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code>public(friend) fun <a href="Diem.md#0x1_Diem_publish_preburn_queue_to_account">publish_preburn_queue_to_account</a><CoinType>( account: &signer, tc_account: &signer ) acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { <a href="Roles.md#0x1_Roles_assert_designated_dealer">Roles::assert_designated_dealer</a>(account); <a href="Roles.md#0x1_Roles_assert_treasury_compliance">Roles::assert_treasury_compliance</a>(tc_account); assert(!<a href="Diem.md#0x1_Diem_is_synthetic_currency">is_synthetic_currency</a><CoinType>(), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="Diem.md#0x1_Diem_EIS_SYNTHETIC_CURRENCY">EIS_SYNTHETIC_CURRENCY</a>)); <a href="Diem.md#0x1_Diem_publish_preburn_queue">publish_preburn_queue</a><CoinType>(account) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); modifies global<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr); </code></pre>

The premission "PreburnCurrency" is granted to DesignatedDealer [H4]. Must abort if the account does not have the DesignatedDealer role.

<pre><code>include <a href="Roles.md#0x1_Roles_AbortsIfNotDesignatedDealer">Roles::AbortsIfNotDesignatedDealer</a>; </code></pre>

PreburnQueue is published under the DesignatedDealer account.

<pre><code>include <a href="Diem.md#0x1_Diem_PublishPreburnQueueAbortsIf">PublishPreburnQueueAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_PublishPreburnQueueEnsures">PublishPreburnQueueEnsures</a><CoinType>; ensures exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr); include <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">Roles::AbortsIfNotTreasuryCompliance</a>{account: tc_account}; include <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">AbortsIfNoCurrency</a><CoinType>; aborts_if <a href="Diem.md#0x1_Diem_is_synthetic_currency">is_synthetic_currency</a><CoinType>() with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; aborts_if exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; aborts_if exists<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(account_addr) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_STATE">Errors::INVALID_STATE</a>; </code></pre> </details>

Function `publish_preburn_queue_to_account_for_test`

<pre><code>public fun <a href="Diem.md#0x1_Diem_publish_preburn_queue_to_account_for_test">publish_preburn_queue_to_account_for_test</a><CoinType>(account: &signer, tc_account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_publish_preburn_queue_to_account_for_test">publish_preburn_queue_to_account_for_test</a><CoinType>( account: &signer, tc_account: &signer ) acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { <a href="Diem.md#0x1_Diem_publish_preburn_queue_to_account">publish_preburn_queue_to_account</a><CoinType>(account, tc_account) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma verify = false; </code></pre> </details>

Function `upgrade_preburn`

Upgrade a designated dealer account from using a single <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> resource to using a <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource so that multiple preburn requests can be outstanding in the same currency for a designated dealer.

<pre><code>fun <a href="Diem.md#0x1_Diem_upgrade_preburn">upgrade_preburn</a><CoinType>(account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="Diem.md#0x1_Diem_upgrade_preburn">upgrade_preburn</a><CoinType>(account: &signer) acquires <a href="Diem.md#0x1_Diem_Preburn">Preburn</a>, <a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a> { <a href="Roles.md#0x1_Roles_assert_designated_dealer">Roles::assert_designated_dealer</a>(account); let sender = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); let preburn_exists = exists<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(sender); let preburn_queue_exists = exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(sender); // The DD must already have an existing `<a href="Diem.md#0x1_Diem_Preburn">Preburn</a>` resource, and not a // `<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a>` resource already, in order to be upgraded. if (preburn_exists && !preburn_queue_exists) { let <a href="Diem.md#0x1_Diem_Preburn">Preburn</a> { to_burn } = move_from<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(sender); <a href="Diem.md#0x1_Diem_publish_preburn_queue">publish_preburn_queue</a><CoinType>(account); // If the DD has an old preburn balance, this is converted over // into the new preburn queue when it's upgraded. if (to_burn.value > 0) { <a href="Diem.md#0x1_Diem_add_preburn_to_queue">add_preburn_to_queue</a>(account, <a href="Diem.md#0x1_Diem_PreburnWithMetadata">PreburnWithMetadata</a> { preburn: <a href="Diem.md#0x1_Diem_Preburn">Preburn</a> { to_burn }, metadata: x"", }) } else { <a href="Diem.md#0x1_Diem_destroy_zero">destroy_zero</a>(to_burn) }; } } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); modifies global<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(account_addr); modifies global<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr); include <a href="Diem.md#0x1_Diem_UpgradePreburnAbortsIf">UpgradePreburnAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_UpgradePreburnEnsures">UpgradePreburnEnsures</a><CoinType>; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_UpgradePreburnAbortsIf">UpgradePreburnAbortsIf</a><CoinType> { account: signer; let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); let upgrade = exists<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(account_addr) && !exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr); } </code></pre>

Must abort if the account doesn't have the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> or <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> resource to satisfy [H4] of <code>preburn_to</code>.

<pre><code>schema <a href="Diem.md#0x1_Diem_UpgradePreburnAbortsIf">UpgradePreburnAbortsIf</a><CoinType> { include upgrade ==> <a href="Diem.md#0x1_Diem_PublishPreburnQueueAbortsIf">PublishPreburnQueueAbortsIf</a><CoinType>; include <a href="Roles.md#0x1_Roles_AbortsIfNotDesignatedDealer">Roles::AbortsIfNotDesignatedDealer</a>; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_UpgradePreburnEnsures">UpgradePreburnEnsures</a><CoinType> { account: signer; let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); let upgrade = exists<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(account_addr) && !exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr); let preburn = global<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(account_addr); ensures upgrade ==> !exists<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(account_addr) && exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr); ensures upgrade && preburn.to_burn.value > 0 ==> global<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr).preburns == vec(<a href="Diem.md#0x1_Diem_PreburnWithMetadata">PreburnWithMetadata</a> { preburn, metadata: x"" }); ensures upgrade && preburn.to_burn.value == 0 ==> global<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr).preburns == vec(); } </code></pre> </details>

Function `add_preburn_to_queue`

Add the <code>preburn</code> request to the preburn queue of <code>account</code>, and check that the number of preburn requests does not exceed <code><a href="Diem.md#0x1_Diem_MAX_OUTSTANDING_PREBURNS">MAX_OUTSTANDING_PREBURNS</a></code>.

<pre><code>fun <a href="Diem.md#0x1_Diem_add_preburn_to_queue">add_preburn_to_queue</a><CoinType>(account: &signer, preburn: <a href="Diem.md#0x1_Diem_PreburnWithMetadata">Diem::PreburnWithMetadata</a><CoinType>) </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="Diem.md#0x1_Diem_add_preburn_to_queue">add_preburn_to_queue</a><CoinType>(account: &signer, preburn: <a href="Diem.md#0x1_Diem_PreburnWithMetadata">PreburnWithMetadata</a><CoinType>) acquires <a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a> { let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); assert(exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(<a href="Diem.md#0x1_Diem_EPREBURN_QUEUE">EPREBURN_QUEUE</a>)); assert(<a href="Diem.md#0x1_Diem_value">value</a>(&preburn.preburn.to_burn) > 0, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="Diem.md#0x1_Diem_EPREBURN">EPREBURN</a>)); let preburns = &mut borrow_global_mut<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr).preburns; assert( <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(preburns) < <a href="Diem.md#0x1_Diem_MAX_OUTSTANDING_PREBURNS">MAX_OUTSTANDING_PREBURNS</a>, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="Diem.md#0x1_Diem_EPREBURN_QUEUE">EPREBURN_QUEUE</a>) ); <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_push_back">Vector::push_back</a>(preburns, preburn); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); let preburns = global<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr).preburns; let post post_preburns = global<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr).preburns; modifies global<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr); aborts_if !exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_STATE">Errors::INVALID_STATE</a>; include <a href="Diem.md#0x1_Diem_AddPreburnToQueueAbortsIf">AddPreburnToQueueAbortsIf</a><CoinType>; ensures exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr); ensures <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_eq_push_back">Vector::eq_push_back</a>(post_preburns, preburns, preburn); </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_AddPreburnToQueueAbortsIf">AddPreburnToQueueAbortsIf</a><CoinType> { account: signer; preburn: <a href="Diem.md#0x1_Diem_PreburnWithMetadata">PreburnWithMetadata</a><CoinType>; let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); aborts_if preburn.preburn.to_burn.value == 0 with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; aborts_if exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr) && <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(global<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr).preburns) >= <a href="Diem.md#0x1_Diem_MAX_OUTSTANDING_PREBURNS">MAX_OUTSTANDING_PREBURNS</a> with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre> </details>

Function `preburn_to`

Sends <code>coin</code> to the preburn queue for <code>account</code>, where it will wait to either be burned or returned to the balance of <code>account</code>. Calls to this function will fail if:

<code>account</code> does not have a <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType></code> resource published under it; or
the preburn queue is already at capacity (i.e., at <code><a href="Diem.md#0x1_Diem_MAX_OUTSTANDING_PREBURNS">MAX_OUTSTANDING_PREBURNS</a></code>); or
<code>coin</code> has a <code>value</code> field of zero.

<pre><code>public fun <a href="Diem.md#0x1_Diem_preburn_to">preburn_to</a><CoinType>(account: &signer, coin: <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType>) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_preburn_to">preburn_to</a><CoinType>( account: &signer, coin: <a href="Diem.md#0x1_Diem">Diem</a><CoinType> ) acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>, <a href="Diem.md#0x1_Diem_Preburn">Preburn</a>, <a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a> { <a href="Roles.md#0x1_Roles_assert_designated_dealer">Roles::assert_designated_dealer</a>(account); // any coin that is preburned needs to have a nonzero value assert(<a href="Diem.md#0x1_Diem_value">value</a>(&coin) > 0, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="Diem.md#0x1_Diem_ECOIN">ECOIN</a>)); let sender = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); // After an upgrade a `<a href="Diem.md#0x1_Diem_Preburn">Preburn</a>` resource no longer exists in this // currency, and it is replaced with a `<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a>` resource // for the same currency. <a href="Diem.md#0x1_Diem_upgrade_preburn">upgrade_preburn</a><CoinType>(account); let preburn = <a href="Diem.md#0x1_Diem_PreburnWithMetadata">PreburnWithMetadata</a> { preburn: <a href="Diem.md#0x1_Diem_Preburn">Preburn</a> { to_burn: <a href="Diem.md#0x1_Diem_zero">zero</a><CoinType>() }, metadata: x"", }; <a href="Diem.md#0x1_Diem_preburn_with_resource">preburn_with_resource</a>(coin, &mut preburn.preburn, sender); <a href="Diem.md#0x1_Diem_add_preburn_to_queue">add_preburn_to_queue</a>(account, preburn); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="Diem.md#0x1_Diem_PreburnToAbortsIf">PreburnToAbortsIf</a><CoinType>{amount: coin.value}; include <a href="Diem.md#0x1_Diem_PreburnToEnsures">PreburnToEnsures</a><CoinType>{amount: coin.value}; let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); include <a href="Diem.md#0x1_Diem_PreburnWithResourceEmits">PreburnWithResourceEmits</a><CoinType>{amount: coin.value, preburn_address: account_addr}; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_PreburnToAbortsIf">PreburnToAbortsIf</a><CoinType> { account: signer; amount: u64; let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); } </code></pre>

Must abort if the account doesn't have the PreburnQueue or Preburn resource, or has not the correct role [H4].

<pre><code>schema <a href="Diem.md#0x1_Diem_PreburnToAbortsIf">PreburnToAbortsIf</a><CoinType> { aborts_if !(exists<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(account_addr) || exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr)); include <a href="Roles.md#0x1_Roles_AbortsIfNotDesignatedDealer">Roles::AbortsIfNotDesignatedDealer</a>; include <a href="Diem.md#0x1_Diem_PreburnAbortsIf">PreburnAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_UpgradePreburnAbortsIf">UpgradePreburnAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_AddPreburnToQueueAbortsIf">AddPreburnToQueueAbortsIf</a><CoinType>{preburn: <a href="Diem.md#0x1_Diem_PreburnWithMetadata">PreburnWithMetadata</a>{ preburn: <a href="Diem.md#0x1_Diem_spec_make_preburn">spec_make_preburn</a>(amount), metadata: x"" } }; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_PreburnToEnsures">PreburnToEnsures</a><CoinType> { account: signer; amount: u64; let account_addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account); } </code></pre>

Removes the preburn resource if it exists

Publishes if it doesn't exists. Updates its state either way.

<pre><code>schema <a href="Diem.md#0x1_Diem_PreburnToEnsures">PreburnToEnsures</a><CoinType> { modifies global<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr); ensures exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(account_addr); modifies global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); include <a href="Diem.md#0x1_Diem_PreburnEnsures">PreburnEnsures</a><CoinType>{preburn: <a href="Diem.md#0x1_Diem_spec_make_preburn">spec_make_preburn</a>(amount)}; } </code></pre> </details>

Function `remove_preburn_from_queue`

Remove the oldest preburn request in the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType></code> resource published under <code>preburn_address</code> whose value is equal to <code>amount</code>. Calls to this function will fail if:

<code>preburn_address</code> doesn't have a <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType></code> resource published under it; or
a preburn request with the correct value for <code>amount</code> cannot be found in the preburn queue for <code>preburn_address</code>;

<pre><code>fun <a href="Diem.md#0x1_Diem_remove_preburn_from_queue">remove_preburn_from_queue</a><CoinType>(preburn_address: address, amount: u64): <a href="Diem.md#0x1_Diem_PreburnWithMetadata">Diem::PreburnWithMetadata</a><CoinType> </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="Diem.md#0x1_Diem_remove_preburn_from_queue">remove_preburn_from_queue</a><CoinType>(preburn_address: address, amount: u64): <a href="Diem.md#0x1_Diem_PreburnWithMetadata">PreburnWithMetadata</a><CoinType> acquires <a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a> { assert(exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(preburn_address), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="Diem.md#0x1_Diem_EPREBURN_QUEUE">EPREBURN_QUEUE</a>)); // We search from the head of the queue let index = 0; let preburn_queue = &mut borrow_global_mut<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(preburn_address).preburns; let queue_length = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(preburn_queue); while ({ spec { invariant index <= queue_length; invariant forall j in 0..index: preburn_queue[j].preburn.to_burn.value != amount; }; (index < queue_length) }) { let elem = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_borrow">Vector::borrow</a>(preburn_queue, index); if (<a href="Diem.md#0x1_Diem_value">value</a>(&elem.preburn.to_burn) == amount) { let preburn = <a href="../../../../../../move-stdlib/docs/Vector.md#0x1_Vector_remove">Vector::remove</a>(preburn_queue, index); // Make sure that the value is correct return preburn }; index = index + 1; }; spec { assert index == queue_length; assert forall j in 0..queue_length: preburn_queue[j].preburn.to_burn.value != amount; }; // If we didn't return already, we couldn't find a preburn with a matching value. abort <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(<a href="Diem.md#0x1_Diem_EPREBURN_NOT_FOUND">EPREBURN_NOT_FOUND</a>) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; modifies global<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(preburn_address); include <a href="Diem.md#0x1_Diem_RemovePreburnFromQueueAbortsIf">RemovePreburnFromQueueAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_RemovePreburnFromQueueEnsures">RemovePreburnFromQueueEnsures</a><CoinType>; ensures result.preburn.to_burn.value == amount; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_RemovePreburnFromQueueAbortsIf">RemovePreburnFromQueueAbortsIf</a><CoinType> { preburn_address: address; amount: u64; let preburn_queue = global<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(preburn_address).preburns; aborts_if !exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(preburn_address) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; aborts_if forall i in 0..len(preburn_queue): preburn_queue[i].preburn.to_burn.value != amount with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_STATE">Errors::INVALID_STATE</a>; } </code></pre>

TODO: See this cannot currently be expressed in the MSL. See https://github.com/diem/diem/issues/7615 for more information.

<pre><code>schema <a href="Diem.md#0x1_Diem_RemovePreburnFromQueueEnsures">RemovePreburnFromQueueEnsures</a><CoinType> { preburn_address: address; amount: u64; ensures old(exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(preburn_address)) ==> exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(preburn_address); } </code></pre> </details>

Function `burn_with_capability`

Permanently removes the coins in the oldest preburn request in the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource under <code>preburn_address</code> that has a <code>to_burn</code> value of <code>amount</code> and updates the market cap accordingly. This function can only be called by the holder of a <code><a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType></code>. Calls to this function will fail if the there is no <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType></code> resource under <code>preburn_address</code>, or, if there is no preburn request in the preburn queue with a <code>to_burn</code> amount equal to <code>amount</code>.

<pre><code>public fun <a href="Diem.md#0x1_Diem_burn_with_capability">burn_with_capability</a><CoinType>(preburn_address: address, capability: &<a href="Diem.md#0x1_Diem_BurnCapability">Diem::BurnCapability</a><CoinType>, amount: u64) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_burn_with_capability">burn_with_capability</a><CoinType>( preburn_address: address, capability: &<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>, amount: u64, ) acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>, <a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a> { // Remove the preburn request let <a href="Diem.md#0x1_Diem_PreburnWithMetadata">PreburnWithMetadata</a>{ preburn, metadata: _ } = <a href="Diem.md#0x1_Diem_remove_preburn_from_queue">remove_preburn_from_queue</a><CoinType>(preburn_address, amount); // Burn the contained coins <a href="Diem.md#0x1_Diem_burn_with_resource_cap">burn_with_resource_cap</a>(&mut preburn, preburn_address, capability); let <a href="Diem.md#0x1_Diem_Preburn">Preburn</a> { to_burn } = preburn; <a href="Diem.md#0x1_Diem_destroy_zero">destroy_zero</a>(to_burn); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="Diem.md#0x1_Diem_BurnWithResourceCapEmits">BurnWithResourceCapEmits</a><CoinType>{preburn: <a href="Diem.md#0x1_Diem_spec_make_preburn">spec_make_preburn</a>(amount)}; include <a href="Diem.md#0x1_Diem_BurnWithCapabilityAbortsIf">BurnWithCapabilityAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_BurnWithCapabilityEnsures">BurnWithCapabilityEnsures</a><CoinType>; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_BurnWithCapabilityAbortsIf">BurnWithCapabilityAbortsIf</a><CoinType> { preburn_address: address; amount: u64; let preburn = <a href="Diem.md#0x1_Diem_spec_make_preburn">spec_make_preburn</a><CoinType>(amount); include <a href="Diem.md#0x1_Diem_AbortsIfNoPreburnQueue">AbortsIfNoPreburnQueue</a><CoinType>; include <a href="Diem.md#0x1_Diem_RemovePreburnFromQueueAbortsIf">RemovePreburnFromQueueAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_BurnWithResourceCapAbortsIf">BurnWithResourceCapAbortsIf</a><CoinType>{preburn: preburn}; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_BurnWithCapabilityEnsures">BurnWithCapabilityEnsures</a><CoinType> { preburn_address: address; amount: u64; let preburn = <a href="Diem.md#0x1_Diem_spec_make_preburn">spec_make_preburn</a><CoinType>(amount); include <a href="Diem.md#0x1_Diem_BurnWithResourceCapEnsures">BurnWithResourceCapEnsures</a><CoinType>{preburn: preburn}; include <a href="Diem.md#0x1_Diem_RemovePreburnFromQueueEnsures">RemovePreburnFromQueueEnsures</a><CoinType>; } </code></pre> </details>

Function `burn_with_resource_cap`

Permanently removes the coins held in the <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> resource (in <code>to_burn</code> field) that was stored in a <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> at <code>preburn_address</code> and updates the market cap accordingly. This function can only be called by the holder of a <code><a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType></code>. Calls to this function will fail if the preburn <code>to_burn</code> area for <code>CoinType</code> is empty.

<pre><code>fun <a href="Diem.md#0x1_Diem_burn_with_resource_cap">burn_with_resource_cap</a><CoinType>(preburn: &mut <a href="Diem.md#0x1_Diem_Preburn">Diem::Preburn</a><CoinType>, preburn_address: address, _capability: &<a href="Diem.md#0x1_Diem_BurnCapability">Diem::BurnCapability</a><CoinType>) </code></pre> <details> <summary>Implementation</summary> <pre><code>fun <a href="Diem.md#0x1_Diem_burn_with_resource_cap">burn_with_resource_cap</a><CoinType>( preburn: &mut <a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>, preburn_address: address, _capability: &<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType> ) acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { let currency_code = <a href="Diem.md#0x1_Diem_currency_code">currency_code</a><CoinType>(); // Abort if no coin present in preburn area assert(preburn.to_burn.value > 0, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(<a href="Diem.md#0x1_Diem_EPREBURN_EMPTY">EPREBURN_EMPTY</a>)); // destroy the coin in <a href="Diem.md#0x1_Diem_Preburn">Preburn</a> area let <a href="Diem.md#0x1_Diem">Diem</a> { value } = <a href="Diem.md#0x1_Diem_withdraw_all">withdraw_all</a><CoinType>(&mut preburn.to_burn); // update the market cap <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>(); let info = borrow_global_mut<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); assert(info.total_value >= (value as u128), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="Diem.md#0x1_Diem_ECURRENCY_INFO">ECURRENCY_INFO</a>)); info.total_value = info.total_value - (value as u128); assert(info.preburn_value >= value, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="Diem.md#0x1_Diem_EPREBURN">EPREBURN</a>)); info.preburn_value = info.preburn_value - value; // don't emit burn events for synthetic currenices as this does not // change the total value of fiat currencies held on-chain. if (!info.is_synthetic) { <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_emit_event">Event::emit_event</a>( &mut info.burn_events, <a href="Diem.md#0x1_Diem_BurnEvent">BurnEvent</a> { amount: value, currency_code, preburn_address, } ); }; } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>let pre_preburn = preburn; include <a href="Diem.md#0x1_Diem_BurnWithResourceCapAbortsIf">BurnWithResourceCapAbortsIf</a><CoinType>{preburn: pre_preburn}; include <a href="Diem.md#0x1_Diem_BurnWithResourceCapEnsures">BurnWithResourceCapEnsures</a><CoinType>{preburn: pre_preburn}; include <a href="Diem.md#0x1_Diem_BurnWithResourceCapEmits">BurnWithResourceCapEmits</a><CoinType>{preburn: pre_preburn}; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_BurnWithResourceCapAbortsIf">BurnWithResourceCapAbortsIf</a><CoinType> { preburn: <a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>; include <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">AbortsIfNoCurrency</a><CoinType>; let to_burn = preburn.to_burn.value; let info = <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>(); aborts_if to_burn == 0 with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_STATE">Errors::INVALID_STATE</a>; aborts_if info.total_value < to_burn with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; aborts_if info.<a href="Diem.md#0x1_Diem_preburn_value">preburn_value</a> < to_burn with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_BurnWithResourceCapEnsures">BurnWithResourceCapEnsures</a><CoinType> { preburn: <a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>; ensures <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().total_value == old(<a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().total_value) - preburn.to_burn.value; ensures <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().preburn_value == old(<a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().preburn_value) - preburn.to_burn.value; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_BurnWithResourceCapEmits">BurnWithResourceCapEmits</a><CoinType> { preburn: <a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>; preburn_address: address; let info = <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>(); let currency_code = <a href="Diem.md#0x1_Diem_spec_currency_code">spec_currency_code</a><CoinType>(); let handle = info.burn_events; emits <a href="Diem.md#0x1_Diem_BurnEvent">BurnEvent</a> { amount: preburn.to_burn.value, currency_code, preburn_address, } to handle if !info.is_synthetic; } </code></pre> </details>

Function `cancel_burn_with_capability`

Cancels the oldest preburn request held in the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource under <code>preburn_address</code> with a <code>to_burn</code> amount matching <code>amount</code>. It then returns these coins to the caller. This function can only be called by the holder of a <code><a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType></code>, and will fail if the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType></code> resource at <code>preburn_address</code> does not contain a preburn request of the right amount.

<pre><code>public fun <a href="Diem.md#0x1_Diem_cancel_burn_with_capability">cancel_burn_with_capability</a><CoinType>(preburn_address: address, _capability: &<a href="Diem.md#0x1_Diem_BurnCapability">Diem::BurnCapability</a><CoinType>, amount: u64): <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_cancel_burn_with_capability">cancel_burn_with_capability</a><CoinType>( preburn_address: address, _capability: &<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>, amount: u64, ): <a href="Diem.md#0x1_Diem">Diem</a><CoinType> acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>, <a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a> { // destroy the coin in the preburn area let <a href="Diem.md#0x1_Diem_PreburnWithMetadata">PreburnWithMetadata</a>{ preburn: <a href="Diem.md#0x1_Diem_Preburn">Preburn</a> { to_burn }, metadata: _ } = <a href="Diem.md#0x1_Diem_remove_preburn_from_queue">remove_preburn_from_queue</a><CoinType>(preburn_address, amount); // update the market cap let currency_code = <a href="Diem.md#0x1_Diem_currency_code">currency_code</a><CoinType>(); let info = borrow_global_mut<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); assert(info.preburn_value >= amount, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="Diem.md#0x1_Diem_EPREBURN">EPREBURN</a>)); info.preburn_value = info.preburn_value - amount; // Don't emit cancel burn events for synthetic currencies. cancel_burn // shouldn't be be used for synthetic coins in the first place. if (!info.is_synthetic) { <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_emit_event">Event::emit_event</a>( &mut info.cancel_burn_events, <a href="Diem.md#0x1_Diem_CancelBurnEvent">CancelBurnEvent</a> { amount, currency_code, preburn_address, } ); }; to_burn } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>modifies global<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(preburn_address); modifies global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); include <a href="Diem.md#0x1_Diem_CancelBurnWithCapAbortsIf">CancelBurnWithCapAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_CancelBurnWithCapEnsures">CancelBurnWithCapEnsures</a><CoinType>; include <a href="Diem.md#0x1_Diem_CancelBurnWithCapEmits">CancelBurnWithCapEmits</a><CoinType>; ensures exists<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); ensures result.value == amount; ensures result.value > 0; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_CancelBurnWithCapAbortsIf">CancelBurnWithCapAbortsIf</a><CoinType> { preburn_address: address; amount: u64; let info = global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); include <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">AbortsIfNoCurrency</a><CoinType>; include <a href="Diem.md#0x1_Diem_RemovePreburnFromQueueAbortsIf">RemovePreburnFromQueueAbortsIf</a><CoinType>; aborts_if info.<a href="Diem.md#0x1_Diem_preburn_value">preburn_value</a> < amount with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_CancelBurnWithCapEnsures">CancelBurnWithCapEnsures</a><CoinType> { preburn_address: address; amount: u64; include <a href="Diem.md#0x1_Diem_RemovePreburnFromQueueEnsures">RemovePreburnFromQueueEnsures</a><CoinType>; let info = global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); let post post_info = global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); ensures post_info == update_field(info, preburn_value, info.preburn_value - amount); } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_CancelBurnWithCapEmits">CancelBurnWithCapEmits</a><CoinType> { preburn_address: address; amount: u64; let info = <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>(); let currency_code = <a href="Diem.md#0x1_Diem_spec_currency_code">spec_currency_code</a><CoinType>(); let handle = info.cancel_burn_events; emits <a href="Diem.md#0x1_Diem_CancelBurnEvent">CancelBurnEvent</a> { amount, currency_code, preburn_address, } to handle if !info.is_synthetic; } </code></pre> </details>

Function `burn_now`

A shortcut for immediately burning a coin. This calls preburn followed by a subsequent burn, and is used for administrative burns, like unpacking an XDX coin or charging fees.

<pre><code>public fun <a href="Diem.md#0x1_Diem_burn_now">burn_now</a><CoinType>(coin: <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType>, preburn: &mut <a href="Diem.md#0x1_Diem_Preburn">Diem::Preburn</a><CoinType>, preburn_address: address, capability: &<a href="Diem.md#0x1_Diem_BurnCapability">Diem::BurnCapability</a><CoinType>) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_burn_now">burn_now</a><CoinType>( coin: <a href="Diem.md#0x1_Diem">Diem</a><CoinType>, preburn: &mut <a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>, preburn_address: address, capability: &<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType> ) acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { assert(coin.value > 0, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="Diem.md#0x1_Diem_ECOIN">ECOIN</a>)); <a href="Diem.md#0x1_Diem_preburn_with_resource">preburn_with_resource</a>(coin, preburn, preburn_address); <a href="Diem.md#0x1_Diem_burn_with_resource_cap">burn_with_resource_cap</a>(preburn, preburn_address, capability); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="Diem.md#0x1_Diem_BurnNowAbortsIf">BurnNowAbortsIf</a><CoinType>; let info = <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>(); let post post_info = <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>(); include <a href="Diem.md#0x1_Diem_PreburnWithResourceEmits">PreburnWithResourceEmits</a><CoinType>{amount: coin.value, preburn_address: preburn_address}; include <a href="Diem.md#0x1_Diem_BurnWithResourceCapEmits">BurnWithResourceCapEmits</a><CoinType>{preburn: <a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>{to_burn: coin}}; ensures preburn.to_burn.value == 0; ensures post_info == update_field(info, total_value, info.total_value - coin.value); </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_BurnNowAbortsIf">BurnNowAbortsIf</a><CoinType> { coin: <a href="Diem.md#0x1_Diem">Diem</a><CoinType>; preburn: <a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>; aborts_if coin.value == 0 with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; include <a href="Diem.md#0x1_Diem_PreburnWithResourceAbortsIf">PreburnWithResourceAbortsIf</a><CoinType>{amount: coin.value}; let info = <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>(); aborts_if info.total_value < coin.value with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre> </details>

Function `remove_burn_capability`

Removes and returns the <code><a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType></code> from <code>account</code>. Calls to this function will fail if <code>account</code> does not have a published <code><a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType></code> resource at the top-level.

<pre><code>public fun <a href="Diem.md#0x1_Diem_remove_burn_capability">remove_burn_capability</a><CoinType>(account: &signer): <a href="Diem.md#0x1_Diem_BurnCapability">Diem::BurnCapability</a><CoinType> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_remove_burn_capability">remove_burn_capability</a><CoinType>(account: &signer): <a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType> acquires <a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a> { let addr = <a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account); assert(exists<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(addr), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_requires_capability">Errors::requires_capability</a>(<a href="Diem.md#0x1_Diem_EBURN_CAPABILITY">EBURN_CAPABILITY</a>)); move_from<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(addr) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="Diem.md#0x1_Diem_AbortsIfNoBurnCapability">AbortsIfNoBurnCapability</a><CoinType>; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_AbortsIfNoBurnCapability">AbortsIfNoBurnCapability</a><CoinType> { account: signer; aborts_if !exists<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(account)) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_REQUIRES_CAPABILITY">Errors::REQUIRES_CAPABILITY</a>; } </code></pre> </details>

Function `preburn_value`

Returns the total value of <code><a href="Diem.md#0x1_Diem">Diem</a><CoinType></code> that is waiting to be burned throughout the system (i.e. the sum of all outstanding preburn requests across all preburn resources for the <code>CoinType</code> currency).

<pre><code>public fun <a href="Diem.md#0x1_Diem_preburn_value">preburn_value</a><CoinType>(): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_preburn_value">preburn_value</a><CoinType>(): u64 acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>(); borrow_global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>).preburn_value } </code></pre> </details>

Function `zero`

Create a new <code><a href="Diem.md#0x1_Diem">Diem</a><CoinType></code> with a value of <code>0</code>. Anyone can call this and it will be successful as long as <code>CoinType</code> is a registered currency.

<pre><code>public fun <a href="Diem.md#0x1_Diem_zero">zero</a><CoinType>(): <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_zero">zero</a><CoinType>(): <a href="Diem.md#0x1_Diem">Diem</a><CoinType> { <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>(); <a href="Diem.md#0x1_Diem">Diem</a><CoinType> { value: 0 } } </code></pre> </details>

Function `value`

Returns the <code>value</code> of the passed in <code>coin</code>. The value is represented in the base units for the currency represented by <code>CoinType</code>.

<pre><code>public fun <a href="Diem.md#0x1_Diem_value">value</a><CoinType>(coin: &<a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType>): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_value">value</a><CoinType>(coin: &<a href="Diem.md#0x1_Diem">Diem</a><CoinType>): u64 { coin.value } </code></pre> </details>

Function `split`

Removes <code>amount</code> of value from the passed in <code>coin</code>. Returns the remaining balance of the passed in <code>coin</code>, along with another coin with value equal to <code>amount</code>. Calls will fail if <code>amount > <a href="Diem.md#0x1_Diem_value">Diem::value</a>(&coin)</code>.

<pre><code>public fun <a href="Diem.md#0x1_Diem_split">split</a><CoinType>(coin: <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType>, amount: u64): (<a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType>, <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType>) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_split">split</a><CoinType>(coin: <a href="Diem.md#0x1_Diem">Diem</a><CoinType>, amount: u64): (<a href="Diem.md#0x1_Diem">Diem</a><CoinType>, <a href="Diem.md#0x1_Diem">Diem</a><CoinType>) { let other = <a href="Diem.md#0x1_Diem_withdraw">withdraw</a>(&mut coin, amount); (coin, other) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>aborts_if coin.<a href="Diem.md#0x1_Diem_value">value</a> < amount with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; ensures result_1.value == coin.value - amount; ensures result_2.value == amount; </code></pre> </details>

Function `withdraw`

Withdraw <code>amount</code> from the passed-in <code>coin</code>, where the original coin is modified in place. After this function is executed, the original <code>coin</code> will have <code>value = original_value - amount</code>, and the new coin will have a <code>value = amount</code>. Calls will abort if the passed-in <code>amount</code> is greater than the value of the passed-in <code>coin</code>.

<pre><code>public fun <a href="Diem.md#0x1_Diem_withdraw">withdraw</a><CoinType>(coin: &mut <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType>, amount: u64): <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_withdraw">withdraw</a><CoinType>(coin: &mut <a href="Diem.md#0x1_Diem">Diem</a><CoinType>, amount: u64): <a href="Diem.md#0x1_Diem">Diem</a><CoinType> { // Check that `amount` is less than the coin's value assert(coin.value >= amount, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="Diem.md#0x1_Diem_EAMOUNT_EXCEEDS_COIN_VALUE">EAMOUNT_EXCEEDS_COIN_VALUE</a>)); coin.value = coin.value - amount; <a href="Diem.md#0x1_Diem">Diem</a> { value: amount } } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="Diem.md#0x1_Diem_WithdrawAbortsIf">WithdrawAbortsIf</a><CoinType>; ensures coin.value == old(coin.value) - amount; ensures result.value == amount; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_WithdrawAbortsIf">WithdrawAbortsIf</a><CoinType> { coin: <a href="Diem.md#0x1_Diem">Diem</a><CoinType>; amount: u64; aborts_if coin.<a href="Diem.md#0x1_Diem_value">value</a> < amount with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre> </details>

Function `withdraw_all`

Return a <code><a href="Diem.md#0x1_Diem">Diem</a><CoinType></code> worth <code>coin.value</code> and reduces the <code>value</code> of the input <code>coin</code> to zero. Does not abort.

<pre><code>public fun <a href="Diem.md#0x1_Diem_withdraw_all">withdraw_all</a><CoinType>(coin: &mut <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType>): <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_withdraw_all">withdraw_all</a><CoinType>(coin: &mut <a href="Diem.md#0x1_Diem">Diem</a><CoinType>): <a href="Diem.md#0x1_Diem">Diem</a><CoinType> { let val = coin.value; <a href="Diem.md#0x1_Diem_withdraw">withdraw</a>(coin, val) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if false; ensures result.value == old(coin.value); ensures coin.value == 0; </code></pre> </details>

Function `join`

Takes two coins as input, returns a single coin with the total value of both coins. Destroys on of the input coins.

<pre><code>public fun <a href="Diem.md#0x1_Diem_join">join</a><CoinType>(coin1: <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType>, coin2: <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType>): <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_join">join</a><CoinType>(coin1: <a href="Diem.md#0x1_Diem">Diem</a><CoinType>, coin2: <a href="Diem.md#0x1_Diem">Diem</a><CoinType>): <a href="Diem.md#0x1_Diem">Diem</a><CoinType> { <a href="Diem.md#0x1_Diem_deposit">deposit</a>(&mut coin1, coin2); coin1 } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if coin1.value + coin2.value > max_u64() with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; ensures result.value == coin1.value + coin2.value; </code></pre> </details>

Function `deposit`

"Merges" the two coins. The coin passed in by reference will have a value equal to the sum of the two coins The <code>check</code> coin is consumed in the process

<pre><code>public fun <a href="Diem.md#0x1_Diem_deposit">deposit</a><CoinType>(coin: &mut <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType>, check: <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType>) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_deposit">deposit</a><CoinType>(coin: &mut <a href="Diem.md#0x1_Diem">Diem</a><CoinType>, check: <a href="Diem.md#0x1_Diem">Diem</a><CoinType>) { let <a href="Diem.md#0x1_Diem">Diem</a> { value } = check; assert(<a href="Diem.md#0x1_Diem_MAX_U64">MAX_U64</a> - coin.value >= value, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_limit_exceeded">Errors::limit_exceeded</a>(<a href="Diem.md#0x1_Diem_ECOIN">ECOIN</a>)); coin.value = coin.value + value; } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="Diem.md#0x1_Diem_DepositAbortsIf">DepositAbortsIf</a><CoinType>; ensures coin.value == old(coin.value) + check.value; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_DepositAbortsIf">DepositAbortsIf</a><CoinType> { coin: <a href="Diem.md#0x1_Diem">Diem</a><CoinType>; check: <a href="Diem.md#0x1_Diem">Diem</a><CoinType>; aborts_if coin.value + check.value > <a href="Diem.md#0x1_Diem_MAX_U64">MAX_U64</a> with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_LIMIT_EXCEEDED">Errors::LIMIT_EXCEEDED</a>; } </code></pre> </details>

Function `destroy_zero`

Destroy a zero-value coin. Calls will fail if the <code>value</code> in the passed-in <code>coin</code> is non-zero so it is impossible to "burn" any non-zero amount of <code><a href="Diem.md#0x1_Diem">Diem</a></code> without having a <code><a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a></code> for the specific <code>CoinType</code>.

<pre><code>public fun <a href="Diem.md#0x1_Diem_destroy_zero">destroy_zero</a><CoinType>(coin: <a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><CoinType>) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_destroy_zero">destroy_zero</a><CoinType>(coin: <a href="Diem.md#0x1_Diem">Diem</a><CoinType>) { let <a href="Diem.md#0x1_Diem">Diem</a> { value } = coin; assert(value == 0, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="Diem.md#0x1_Diem_EDESTRUCTION_OF_NONZERO_COIN">EDESTRUCTION_OF_NONZERO_COIN</a>)) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if coin.value > 0 with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; </code></pre> </details>

Function `register_currency`

Register the type <code>CoinType</code> as a currency. Until the type is registered as a currency it cannot be used as a coin/currency unit in Diem. The passed-in <code>dr_account</code> must be a specific address (<code>@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a></code>) and <code>dr_account</code> must also have the correct <code>DiemRoot</code> account role. After the first registration of <code>CoinType</code> as a currency, additional attempts to register <code>CoinType</code> as a currency will abort. When the <code>CoinType</code> is registered it publishes the <code><a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType></code> resource under the <code>@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a></code> and adds the currency to the set of <code><a href="RegisteredCurrencies.md#0x1_RegisteredCurrencies">RegisteredCurrencies</a></code>. It returns <code><a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType></code> and <code><a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType></code> resources.

<pre><code>public fun <a href="Diem.md#0x1_Diem_register_currency">register_currency</a><CoinType>(dr_account: &signer, to_xdx_exchange_rate: <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32_FixedPoint32">FixedPoint32::FixedPoint32</a>, is_synthetic: bool, scaling_factor: u64, fractional_part: u64, currency_code: vector<u8>): (<a href="Diem.md#0x1_Diem_MintCapability">Diem::MintCapability</a><CoinType>, <a href="Diem.md#0x1_Diem_BurnCapability">Diem::BurnCapability</a><CoinType>) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_register_currency">register_currency</a><CoinType>( dr_account: &signer, to_xdx_exchange_rate: <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>, is_synthetic: bool, scaling_factor: u64, fractional_part: u64, currency_code: vector<u8>, ): (<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>, <a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>) { <a href="Roles.md#0x1_Roles_assert_diem_root">Roles::assert_diem_root</a>(dr_account); // Operational constraint that it must be stored under a specific address. <a href="CoreAddresses.md#0x1_CoreAddresses_assert_currency_info">CoreAddresses::assert_currency_info</a>(dr_account); assert( !exists<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(dr_account)), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_already_published">Errors::already_published</a>(<a href="Diem.md#0x1_Diem_ECURRENCY_INFO">ECURRENCY_INFO</a>) ); assert(0 < scaling_factor && <a href="Diem.md#0x1_Diem_scaling_factor">scaling_factor</a> <= <a href="Diem.md#0x1_Diem_MAX_SCALING_FACTOR">MAX_SCALING_FACTOR</a>, <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="Diem.md#0x1_Diem_ECURRENCY_INFO">ECURRENCY_INFO</a>)); move_to(dr_account, <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType> { total_value: 0, preburn_value: 0, to_xdx_exchange_rate, is_synthetic, scaling_factor, fractional_part, currency_code: copy currency_code, can_mint: true, mint_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_new_event_handle">Event::new_event_handle</a><<a href="Diem.md#0x1_Diem_MintEvent">MintEvent</a>>(dr_account), burn_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_new_event_handle">Event::new_event_handle</a><<a href="Diem.md#0x1_Diem_BurnEvent">BurnEvent</a>>(dr_account), preburn_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_new_event_handle">Event::new_event_handle</a><<a href="Diem.md#0x1_Diem_PreburnEvent">PreburnEvent</a>>(dr_account), cancel_burn_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_new_event_handle">Event::new_event_handle</a><<a href="Diem.md#0x1_Diem_CancelBurnEvent">CancelBurnEvent</a>>(dr_account), exchange_rate_update_events: <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_new_event_handle">Event::new_event_handle</a><<a href="Diem.md#0x1_Diem_ToXDXExchangeRateUpdateEvent">ToXDXExchangeRateUpdateEvent</a>>(dr_account) }); <a href="RegisteredCurrencies.md#0x1_RegisteredCurrencies_add_currency_code">RegisteredCurrencies::add_currency_code</a>( dr_account, currency_code, ); (<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>{}, <a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>{}) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="Diem.md#0x1_Diem_RegisterCurrencyAbortsIf">RegisterCurrencyAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_RegisterCurrencyEnsures">RegisterCurrencyEnsures</a><CoinType>; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_RegisterCurrencyAbortsIf">RegisterCurrencyAbortsIf</a><CoinType> { dr_account: signer; currency_code: vector<u8>; scaling_factor: u64; } </code></pre>

Must abort if the signer does not have the DiemRoot role [H8].

<pre><code>schema <a href="Diem.md#0x1_Diem_RegisterCurrencyAbortsIf">RegisterCurrencyAbortsIf</a><CoinType> { include <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">Roles::AbortsIfNotDiemRoot</a>{account: dr_account}; aborts_if scaling_factor == 0 || scaling_factor > <a href="Diem.md#0x1_Diem_MAX_SCALING_FACTOR">MAX_SCALING_FACTOR</a> with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; include <a href="CoreAddresses.md#0x1_CoreAddresses_AbortsIfNotCurrencyInfo">CoreAddresses::AbortsIfNotCurrencyInfo</a>{account: dr_account}; aborts_if exists<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(dr_account)) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; include <a href="RegisteredCurrencies.md#0x1_RegisteredCurrencies_AddCurrencyCodeAbortsIf">RegisteredCurrencies::AddCurrencyCodeAbortsIf</a>; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_RegisterCurrencyEnsures">RegisterCurrencyEnsures</a><CoinType> { ensures <a href="Diem.md#0x1_Diem_spec_is_currency">spec_is_currency</a><CoinType>(); ensures <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().total_value == 0; } </code></pre> </details>

Function `register_SCS_currency`

Registers a stable currency (SCS) coin -- i.e., a non-synthetic currency. Resources are published on two distinct accounts: The <code>CoinInfo</code> is published on the Diem root account, and the mint and burn capabilities are published on a treasury compliance account. This code allows different currencies to have different treasury compliance accounts.

<pre><code>public fun <a href="Diem.md#0x1_Diem_register_SCS_currency">register_SCS_currency</a><CoinType>(dr_account: &signer, tc_account: &signer, to_xdx_exchange_rate: <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32_FixedPoint32">FixedPoint32::FixedPoint32</a>, scaling_factor: u64, fractional_part: u64, currency_code: vector<u8>) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_register_SCS_currency">register_SCS_currency</a><CoinType>( dr_account: &signer, tc_account: &signer, to_xdx_exchange_rate: <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>, scaling_factor: u64, fractional_part: u64, currency_code: vector<u8>, ) { <a href="Roles.md#0x1_Roles_assert_treasury_compliance">Roles::assert_treasury_compliance</a>(tc_account); <a href="Roles.md#0x1_Roles_assert_diem_root">Roles::assert_diem_root</a>(dr_account); let (mint_cap, burn_cap) = <a href="Diem.md#0x1_Diem_register_currency">register_currency</a><CoinType>( dr_account, to_xdx_exchange_rate, false, // is_synthetic scaling_factor, fractional_part, currency_code, ); assert( !exists<<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(tc_account)), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_already_published">Errors::already_published</a>(<a href="Diem.md#0x1_Diem_EMINT_CAPABILITY">EMINT_CAPABILITY</a>) ); move_to(tc_account, mint_cap); <a href="Diem.md#0x1_Diem_publish_burn_capability">publish_burn_capability</a><CoinType>(tc_account, burn_cap); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="Diem.md#0x1_Diem_RegisterSCSCurrencyAbortsIf">RegisterSCSCurrencyAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_RegisterSCSCurrencyEnsures">RegisterSCSCurrencyEnsures</a><CoinType>; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_RegisterSCSCurrencyAbortsIf">RegisterSCSCurrencyAbortsIf</a><CoinType> { tc_account: signer; dr_account: signer; currency_code: vector<u8>; scaling_factor: u64; } </code></pre>

Must abort if tc_account does not have the TreasuryCompliance role. Only a TreasuryCompliance account can have the MintCapability [H1]. Only a TreasuryCompliance account can have the BurnCapability [H3].

<pre><code>schema <a href="Diem.md#0x1_Diem_RegisterSCSCurrencyAbortsIf">RegisterSCSCurrencyAbortsIf</a><CoinType> { include <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">Roles::AbortsIfNotTreasuryCompliance</a>{account: tc_account}; aborts_if exists<<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(tc_account)) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; include <a href="Diem.md#0x1_Diem_RegisterCurrencyAbortsIf">RegisterCurrencyAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_PublishBurnCapAbortsIfs">PublishBurnCapAbortsIfs</a><CoinType>; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_RegisterSCSCurrencyEnsures">RegisterSCSCurrencyEnsures</a><CoinType> { tc_account: signer; ensures <a href="Diem.md#0x1_Diem_spec_has_mint_capability">spec_has_mint_capability</a><CoinType>(<a href="../../../../../../move-stdlib/docs/Signer.md#0x1_Signer_spec_address_of">Signer::spec_address_of</a>(tc_account)); } </code></pre> </details>

Function `market_cap`

Returns the total amount of currency minted of type <code>CoinType</code>.

<pre><code>public fun <a href="Diem.md#0x1_Diem_market_cap">market_cap</a><CoinType>(): u128 </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_market_cap">market_cap</a><CoinType>(): u128 acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>(); borrow_global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>).total_value } </code></pre> </details>

Function `approx_xdx_for_value`

Returns the value of the coin in the <code>FromCoinType</code> currency in XDX. This should only be used where a rough approximation of the exchange rate is needed.

<pre><code>public fun <a href="Diem.md#0x1_Diem_approx_xdx_for_value">approx_xdx_for_value</a><FromCoinType>(from_value: u64): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_approx_xdx_for_value">approx_xdx_for_value</a><FromCoinType>(from_value: u64): u64 acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { let xdx_exchange_rate = <a href="Diem.md#0x1_Diem_xdx_exchange_rate">xdx_exchange_rate</a><FromCoinType>(); <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32_multiply_u64">FixedPoint32::multiply_u64</a>(from_value, xdx_exchange_rate) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="Diem.md#0x1_Diem_ApproxXdmForValueAbortsIf">ApproxXdmForValueAbortsIf</a><FromCoinType>; ensures result == <a href="Diem.md#0x1_Diem_spec_approx_xdx_for_value">spec_approx_xdx_for_value</a><FromCoinType>(from_value); </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_ApproxXdmForValueAbortsIf">ApproxXdmForValueAbortsIf</a><CoinType> { from_value: num; include <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">AbortsIfNoCurrency</a><CoinType>; let xdx_exchange_rate = <a href="Diem.md#0x1_Diem_spec_xdx_exchange_rate">spec_xdx_exchange_rate</a><CoinType>(); include <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32_MultiplyAbortsIf">FixedPoint32::MultiplyAbortsIf</a>{val: from_value, multiplier: xdx_exchange_rate}; } </code></pre> </details>

Function `approx_xdx_for_coin`

Returns the value of the coin in the <code>FromCoinType</code> currency in XDX. This should only be used where a rough approximation of the exchange rate is needed.

<pre><code>public fun <a href="Diem.md#0x1_Diem_approx_xdx_for_coin">approx_xdx_for_coin</a><FromCoinType>(coin: &<a href="Diem.md#0x1_Diem_Diem">Diem::Diem</a><FromCoinType>): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_approx_xdx_for_coin">approx_xdx_for_coin</a><FromCoinType>(coin: &<a href="Diem.md#0x1_Diem">Diem</a><FromCoinType>): u64 acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { let from_value = <a href="Diem.md#0x1_Diem_value">value</a>(coin); <a href="Diem.md#0x1_Diem_approx_xdx_for_value">approx_xdx_for_value</a><FromCoinType>(from_value) } </code></pre> </details>

Function `is_currency`

Returns <code>true</code> if the type <code>CoinType</code> is a registered currency. Returns <code>false</code> otherwise.

<pre><code>public fun <a href="Diem.md#0x1_Diem_is_currency">is_currency</a><CoinType>(): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_is_currency">is_currency</a><CoinType>(): bool { exists<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>) } </code></pre> </details>

Function `is_SCS_currency`

<pre><code>public fun <a href="Diem.md#0x1_Diem_is_SCS_currency">is_SCS_currency</a><CoinType>(): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_is_SCS_currency">is_SCS_currency</a><CoinType>(): bool acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { <a href="Diem.md#0x1_Diem_is_currency">is_currency</a><CoinType>() && !borrow_global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>).is_synthetic } </code></pre> </details>

Function `is_synthetic_currency`

Returns <code>true</code> if <code>CoinType</code> is a synthetic currency as defined in its <code><a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a></code>. Returns <code>false</code> otherwise.

<pre><code>public fun <a href="Diem.md#0x1_Diem_is_synthetic_currency">is_synthetic_currency</a><CoinType>(): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_is_synthetic_currency">is_synthetic_currency</a><CoinType>(): bool acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { let addr = @<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>; exists<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(addr) && borrow_global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(addr).is_synthetic } </code></pre> </details>

Function `scaling_factor`

Returns the scaling factor for the <code>CoinType</code> currency as defined in its <code><a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a></code>.

<pre><code>public fun <a href="Diem.md#0x1_Diem_scaling_factor">scaling_factor</a><CoinType>(): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_scaling_factor">scaling_factor</a><CoinType>(): u64 acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>(); borrow_global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>).scaling_factor } </code></pre> </details>

Function `fractional_part`

Returns the representable (i.e. real-world) fractional part for the <code>CoinType</code> currency as defined in its <code><a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a></code>.

<pre><code>public fun <a href="Diem.md#0x1_Diem_fractional_part">fractional_part</a><CoinType>(): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_fractional_part">fractional_part</a><CoinType>(): u64 acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>(); borrow_global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>).fractional_part } </code></pre> </details>

Function `currency_code`

Returns the currency code for the registered currency as defined in its <code><a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a></code> resource.

<pre><code>public fun <a href="Diem.md#0x1_Diem_currency_code">currency_code</a><CoinType>(): vector<u8> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_currency_code">currency_code</a><CoinType>(): vector<u8> acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>(); *&borrow_global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>).currency_code } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">AbortsIfNoCurrency</a><CoinType>; ensures result == <a href="Diem.md#0x1_Diem_spec_currency_code">spec_currency_code</a><CoinType>(); </code></pre>

<pre><code>fun <a href="Diem.md#0x1_Diem_spec_currency_code">spec_currency_code</a><CoinType>(): vector<u8> { <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().currency_code } </code></pre> </details>

Function `update_xdx_exchange_rate`

Updates the <code>to_xdx_exchange_rate</code> held in the <code><a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a></code> for <code>FromCoinType</code> to the new passed-in <code>xdx_exchange_rate</code>.

<pre><code>public fun <a href="Diem.md#0x1_Diem_update_xdx_exchange_rate">update_xdx_exchange_rate</a><FromCoinType>(tc_account: &signer, xdx_exchange_rate: <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32_FixedPoint32">FixedPoint32::FixedPoint32</a>) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_update_xdx_exchange_rate">update_xdx_exchange_rate</a><FromCoinType>( tc_account: &signer, xdx_exchange_rate: <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a> ) acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { <a href="Roles.md#0x1_Roles_assert_treasury_compliance">Roles::assert_treasury_compliance</a>(tc_account); <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><FromCoinType>(); let currency_info = borrow_global_mut<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><FromCoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); currency_info.to_xdx_exchange_rate = xdx_exchange_rate; <a href="../../../../../../move-stdlib/docs/Event.md#0x1_Event_emit_event">Event::emit_event</a>( &mut currency_info.exchange_rate_update_events, <a href="Diem.md#0x1_Diem_ToXDXExchangeRateUpdateEvent">ToXDXExchangeRateUpdateEvent</a> { currency_code: *&currency_info.currency_code, new_to_xdx_exchange_rate: <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32_get_raw_value">FixedPoint32::get_raw_value</a>(*&currency_info.to_xdx_exchange_rate), } ); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="Diem.md#0x1_Diem_UpdateXDXExchangeRateAbortsIf">UpdateXDXExchangeRateAbortsIf</a><FromCoinType>; include <a href="Diem.md#0x1_Diem_UpdateXDXExchangeRateEnsures">UpdateXDXExchangeRateEnsures</a><FromCoinType>; include <a href="Diem.md#0x1_Diem_UpdateXDXExchangeRateEmits">UpdateXDXExchangeRateEmits</a><FromCoinType>; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_UpdateXDXExchangeRateAbortsIf">UpdateXDXExchangeRateAbortsIf</a><FromCoinType> { tc_account: signer; } </code></pre>

Must abort if the account does not have the TreasuryCompliance Role [H5].

<pre><code>schema <a href="Diem.md#0x1_Diem_UpdateXDXExchangeRateAbortsIf">UpdateXDXExchangeRateAbortsIf</a><FromCoinType> { include <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">Roles::AbortsIfNotTreasuryCompliance</a>{account: tc_account}; include <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">AbortsIfNoCurrency</a><FromCoinType>; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_UpdateXDXExchangeRateEnsures">UpdateXDXExchangeRateEnsures</a><FromCoinType> { xdx_exchange_rate: <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>; ensures <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><FromCoinType>().to_xdx_exchange_rate == xdx_exchange_rate; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_UpdateXDXExchangeRateEmits">UpdateXDXExchangeRateEmits</a><FromCoinType> { xdx_exchange_rate: <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a>; let handle = global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><FromCoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>).exchange_rate_update_events; let msg = <a href="Diem.md#0x1_Diem_ToXDXExchangeRateUpdateEvent">ToXDXExchangeRateUpdateEvent</a> { currency_code: global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><FromCoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>).currency_code, new_to_xdx_exchange_rate: <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32_get_raw_value">FixedPoint32::get_raw_value</a>(xdx_exchange_rate) }; emits msg to handle; } </code></pre> </details>

Function `xdx_exchange_rate`

Returns the (rough) exchange rate between <code>CoinType</code> and <code><a href="XDX.md#0x1_XDX">XDX</a></code>

<pre><code>public fun <a href="Diem.md#0x1_Diem_xdx_exchange_rate">xdx_exchange_rate</a><CoinType>(): <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32_FixedPoint32">FixedPoint32::FixedPoint32</a> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_xdx_exchange_rate">xdx_exchange_rate</a><CoinType>(): <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a> acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>(); *&borrow_global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>).to_xdx_exchange_rate } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">AbortsIfNoCurrency</a><CoinType>; let info = global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); ensures result == info.to_xdx_exchange_rate; </code></pre> </details>

Function `update_minting_ability`

There may be situations in which we disallow the further minting of coins in the system without removing the currency. This function allows the association treasury compliance account to control whether or not further coins of <code>CoinType</code> can be minted or not. If this is called with <code>can_mint = true</code>, then minting is allowed, if <code>can_mint = false</code> then minting is disallowed until it is turned back on via this function. All coins start out in the default state of <code>can_mint = true</code>.

<pre><code>public fun <a href="Diem.md#0x1_Diem_update_minting_ability">update_minting_ability</a><CoinType>(tc_account: &signer, can_mint: bool) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_update_minting_ability">update_minting_ability</a><CoinType>( tc_account: &signer, can_mint: bool, ) acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { <a href="Roles.md#0x1_Roles_assert_treasury_compliance">Roles::assert_treasury_compliance</a>(tc_account); <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>(); let currency_info = borrow_global_mut<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>); currency_info.can_mint = can_mint; } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="Diem.md#0x1_Diem_UpdateMintingAbilityAbortsIf">UpdateMintingAbilityAbortsIf</a><CoinType>; include <a href="Diem.md#0x1_Diem_UpdateMintingAbilityEnsures">UpdateMintingAbilityEnsures</a><CoinType>; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_UpdateMintingAbilityAbortsIf">UpdateMintingAbilityAbortsIf</a><CoinType> { tc_account: signer; include <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">AbortsIfNoCurrency</a><CoinType>; } </code></pre>

Only the TreasuryCompliance role can enable/disable minting [H2].

<pre><code>schema <a href="Diem.md#0x1_Diem_UpdateMintingAbilityAbortsIf">UpdateMintingAbilityAbortsIf</a><CoinType> { include <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">Roles::AbortsIfNotTreasuryCompliance</a>{account: tc_account}; } </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_UpdateMintingAbilityEnsures">UpdateMintingAbilityEnsures</a><CoinType> { tc_account: signer; can_mint: bool; ensures <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().can_mint == can_mint; } </code></pre> </details>

Function `assert_is_currency`

Asserts that <code>CoinType</code> is a registered currency.

<pre><code>public fun <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>() </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>() { assert(<a href="Diem.md#0x1_Diem_is_currency">is_currency</a><CoinType>(), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_not_published">Errors::not_published</a>(<a href="Diem.md#0x1_Diem_ECURRENCY_INFO">ECURRENCY_INFO</a>)); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">AbortsIfNoCurrency</a><CoinType>; </code></pre>

<pre><code>schema <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">AbortsIfNoCurrency</a><CoinType> { aborts_if !<a href="Diem.md#0x1_Diem_spec_is_currency">spec_is_currency</a><CoinType>() with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; } </code></pre> </details>

Function `assert_is_SCS_currency`

<pre><code>public fun <a href="Diem.md#0x1_Diem_assert_is_SCS_currency">assert_is_SCS_currency</a><CoinType>() </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Diem.md#0x1_Diem_assert_is_SCS_currency">assert_is_SCS_currency</a><CoinType>() acquires <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a> { <a href="Diem.md#0x1_Diem_assert_is_currency">assert_is_currency</a><CoinType>(); assert(<a href="Diem.md#0x1_Diem_is_SCS_currency">is_SCS_currency</a><CoinType>(), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_invalid_state">Errors::invalid_state</a>(<a href="Diem.md#0x1_Diem_ECURRENCY_INFO">ECURRENCY_INFO</a>)); } </code></pre> </details>

Module Specification

Returns the market cap of CoinType.

<pre><code>fun <a href="Diem.md#0x1_Diem_spec_market_cap">spec_market_cap</a><CoinType>(): u128 { global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>).total_value } </code></pre>

<pre><code>fun <a href="Diem.md#0x1_Diem_spec_scaling_factor">spec_scaling_factor</a><CoinType>(): u64 { global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>).scaling_factor } </code></pre>

Access Control

Only mint functions can increase the total amount of currency [H1].

<pre><code>apply <a href="Diem.md#0x1_Diem_TotalValueNotIncrease">TotalValueNotIncrease</a><CoinType> to *<CoinType> except <a href="Diem.md#0x1_Diem_mint">mint</a><CoinType>, <a href="Diem.md#0x1_Diem_mint_with_capability">mint_with_capability</a><CoinType>; </code></pre>

In order to successfully call <code>mint</code> and <code>mint_with_capability</code>, MintCapability is required. MintCapability must be only granted to a TreasuryCompliance account [H1]. Only <code>register_SCS_currency</code> creates MintCapability, which must abort if the account does not have the TreasuryCompliance role [H1].

<pre><code>apply <a href="Diem.md#0x1_Diem_PreserveMintCapAbsence">PreserveMintCapAbsence</a><CoinType> to *<CoinType> except <a href="Diem.md#0x1_Diem_register_SCS_currency">register_SCS_currency</a><CoinType>; apply <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">Roles::AbortsIfNotTreasuryCompliance</a>{account: tc_account} to <a href="Diem.md#0x1_Diem_register_SCS_currency">register_SCS_currency</a><CoinType>; </code></pre>

Only TreasuryCompliance can have MintCapability [H1]. If an account has MintCapability, it is a TreasuryCompliance account.

<pre><code>invariant<CoinType> forall mint_cap_owner: address where exists<<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>>(mint_cap_owner): <a href="Roles.md#0x1_Roles_spec_has_treasury_compliance_role_addr">Roles::spec_has_treasury_compliance_role_addr</a>(mint_cap_owner); </code></pre>

MintCapability is not transferrable [J1].

<pre><code>apply <a href="Diem.md#0x1_Diem_PreserveMintCapExistence">PreserveMintCapExistence</a><CoinType> to *<CoinType>; </code></pre>

The permission "MintCurrency" is unique per currency [I1]. At most one address has a mint capability for SCS CoinType

<pre><code>invariant<CoinType> <a href="Diem.md#0x1_Diem_is_SCS_currency">is_SCS_currency</a><CoinType>() ==> ( forall mint_cap_owner1: address, mint_cap_owner2: address where ( exists<<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>>(mint_cap_owner1) && exists<<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>>(mint_cap_owner2) ): mint_cap_owner1 == mint_cap_owner2 ); </code></pre>

If an address has a mint capability, it is an SCS currency.

<pre><code>invariant<CoinType> forall addr3: address where <a href="Diem.md#0x1_Diem_spec_has_mint_capability">spec_has_mint_capability</a><CoinType>(addr3): <a href="Diem.md#0x1_Diem_is_SCS_currency">is_SCS_currency</a><CoinType>(); </code></pre>

Minting

The total amount of currency does not increase.

<pre><code>schema <a href="Diem.md#0x1_Diem_TotalValueNotIncrease">TotalValueNotIncrease</a><CoinType> { ensures old(<a href="Diem.md#0x1_Diem_spec_is_currency">spec_is_currency</a><CoinType>()) ==> <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().total_value <= old(<a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().total_value); } </code></pre>

The existence of MintCapability is preserved.

<pre><code>schema <a href="Diem.md#0x1_Diem_PreserveMintCapExistence">PreserveMintCapExistence</a><CoinType> { ensures forall addr: address: old(exists<<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>>(addr)) ==> exists<<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>>(addr); } </code></pre>

The absence of MintCapability is preserved.

<pre><code>schema <a href="Diem.md#0x1_Diem_PreserveMintCapAbsence">PreserveMintCapAbsence</a><CoinType> { ensures forall addr: address: old(!exists<<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>>(addr)) ==> !exists<<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>>(addr); } </code></pre>

Burning

The total amount of currency does not decrease.

<pre><code>schema <a href="Diem.md#0x1_Diem_TotalValueNotDecrease">TotalValueNotDecrease</a><CoinType> { ensures old(<a href="Diem.md#0x1_Diem_spec_is_currency">spec_is_currency</a><CoinType>()) ==> <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().total_value >= old(<a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().total_value); } </code></pre>

The existence of BurnCapability is preserved.

<pre><code>schema <a href="Diem.md#0x1_Diem_PreserveBurnCapExistence">PreserveBurnCapExistence</a><CoinType> { ensures forall addr: address: old(exists<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(addr)) ==> exists<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(addr); } </code></pre>

The absence of BurnCapability is preserved.

<pre><code>schema <a href="Diem.md#0x1_Diem_PreserveBurnCapAbsence">PreserveBurnCapAbsence</a><CoinType> { ensures forall addr: address: old(!exists<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(addr)) ==> !exists<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(addr); } </code></pre>

Only burn functions can decrease the total amount of currency [H3].

<pre><code>apply <a href="Diem.md#0x1_Diem_TotalValueNotDecrease">TotalValueNotDecrease</a><CoinType> to *<CoinType> except <a href="Diem.md#0x1_Diem_burn">burn</a><CoinType>, <a href="Diem.md#0x1_Diem_burn_with_capability">burn_with_capability</a><CoinType>, <a href="Diem.md#0x1_Diem_burn_with_resource_cap">burn_with_resource_cap</a><CoinType>, <a href="Diem.md#0x1_Diem_burn_now">burn_now</a><CoinType>; </code></pre>

In order to successfully call the burn functions, BurnCapability is required. BurnCapability must be only granted to a TreasuryCompliance account [H3]. Only <code>register_SCS_currency</code> and <code>publish_burn_capability</code> publish BurnCapability, which must abort if the account does not have the TreasuryCompliance role [H8].

<pre><code>apply <a href="Diem.md#0x1_Diem_PreserveBurnCapAbsence">PreserveBurnCapAbsence</a><CoinType> to *<CoinType> except <a href="Diem.md#0x1_Diem_register_SCS_currency">register_SCS_currency</a><CoinType>, <a href="Diem.md#0x1_Diem_publish_burn_capability">publish_burn_capability</a><CoinType>; apply <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">Roles::AbortsIfNotTreasuryCompliance</a>{account: tc_account} to <a href="Diem.md#0x1_Diem_register_SCS_currency">register_SCS_currency</a><CoinType>; </code></pre>

Only TreasuryCompliance can have BurnCapability [H3]. If an account has BurnCapability, it is a TreasuryCompliance account.

<pre><code>invariant<CoinType> forall addr1: address: exists<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(addr1) ==> <a href="Roles.md#0x1_Roles_spec_has_treasury_compliance_role_addr">Roles::spec_has_treasury_compliance_role_addr</a>(addr1); </code></pre>

BurnCapability is not transferrable [J3]. BurnCapability can be extracted from an account, but is always moved back to the original account. This is the case in <code><a href="TransactionFee.md#0x1_TransactionFee_burn_fees">TransactionFee::burn_fees</a></code> which is the only user of <code>remove_burn_capability</code> and <code>publish_burn_capability</code>.

<pre><code>apply <a href="Diem.md#0x1_Diem_PreserveBurnCapExistence">PreserveBurnCapExistence</a><CoinType> to *<CoinType> except <a href="Diem.md#0x1_Diem_remove_burn_capability">remove_burn_capability</a><CoinType>; </code></pre>

Preburning

The preburn value of currency does not increase.

<pre><code>schema <a href="Diem.md#0x1_Diem_PreburnValueNotIncrease">PreburnValueNotIncrease</a><CoinType> { ensures old(<a href="Diem.md#0x1_Diem_spec_is_currency">spec_is_currency</a><CoinType>()) ==> <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().<a href="Diem.md#0x1_Diem_preburn_value">preburn_value</a> <= old(<a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().preburn_value); } </code></pre>

The the preburn value of currency does not decrease.

<pre><code>schema <a href="Diem.md#0x1_Diem_PreburnValueNotDecrease">PreburnValueNotDecrease</a><CoinType> { ensures old(<a href="Diem.md#0x1_Diem_spec_is_currency">spec_is_currency</a><CoinType>()) ==> <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().preburn_value >= old(<a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>().preburn_value); } </code></pre>

The existence of the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource is preserved.

<pre><code>schema <a href="Diem.md#0x1_Diem_PreservePreburnQueueExistence">PreservePreburnQueueExistence</a><CoinType> { ensures forall addr: address: old(exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(addr)) ==> exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(addr); } </code></pre>

The absence of a <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> is preserved.

NB: As part of the upgrade process, we also tie this in with the non-existence of a <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> resource as well. Once the upgrade process is complete this additional existence check can be removed.

<pre><code>schema <a href="Diem.md#0x1_Diem_PreservePreburnQueueAbsence">PreservePreburnQueueAbsence</a><CoinType> { ensures forall addr: address: old(!(exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(addr) || exists<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(addr))) ==> !exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(addr); } </code></pre>

Only burn functions can decrease the preburn value of currency [H4].

<pre><code>apply <a href="Diem.md#0x1_Diem_PreburnValueNotDecrease">PreburnValueNotDecrease</a><CoinType> to *<CoinType> except <a href="Diem.md#0x1_Diem_burn">burn</a><CoinType>, <a href="Diem.md#0x1_Diem_burn_with_capability">burn_with_capability</a><CoinType>, <a href="Diem.md#0x1_Diem_burn_with_resource_cap">burn_with_resource_cap</a><CoinType>, <a href="Diem.md#0x1_Diem_burn_now">burn_now</a><CoinType>, <a href="Diem.md#0x1_Diem_cancel_burn">cancel_burn</a><CoinType>, <a href="Diem.md#0x1_Diem_cancel_burn_with_capability">cancel_burn_with_capability</a><CoinType>; </code></pre>

Only preburn functions can increase the preburn value of currency [H4].

<pre><code>apply <a href="Diem.md#0x1_Diem_PreburnValueNotIncrease">PreburnValueNotIncrease</a><CoinType> to *<CoinType> except <a href="Diem.md#0x1_Diem_preburn_to">preburn_to</a><CoinType>, <a href="Diem.md#0x1_Diem_preburn_with_resource">preburn_with_resource</a><CoinType>; </code></pre>

In order to successfully call the preburn functions, Preburn is required. Preburn must be only granted to a DesignatedDealer account [H4]. Only <code>publish_preburn_queue_to_account</code> and <code>publish_preburn_queue</code> publishes <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code>, which must abort if the account does not have the DesignatedDealer role [H4].

<pre><code>apply <a href="Roles.md#0x1_Roles_AbortsIfNotDesignatedDealer">Roles::AbortsIfNotDesignatedDealer</a> to <a href="Diem.md#0x1_Diem_publish_preburn_queue">publish_preburn_queue</a><CoinType>, <a href="Diem.md#0x1_Diem_publish_preburn_queue_to_account">publish_preburn_queue_to_account</a><CoinType>; apply <a href="Diem.md#0x1_Diem_PreservePreburnQueueAbsence">PreservePreburnQueueAbsence</a><CoinType> to *<CoinType> except <a href="Diem.md#0x1_Diem_publish_preburn_queue">publish_preburn_queue</a><CoinType>, <a href="Diem.md#0x1_Diem_publish_preburn_queue_to_account">publish_preburn_queue_to_account</a><CoinType>; </code></pre>

Only DesignatedDealer can have PreburnQueue [H3]. If an account has PreburnQueue, it is a DesignatedDealer account.

NB: during the transition this holds for both <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> and <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resources.

<pre><code>invariant<CoinType> forall addr1: address: exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(addr1) || exists<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(addr1) ==> <a href="Roles.md#0x1_Roles_spec_has_designated_dealer_role_addr">Roles::spec_has_designated_dealer_role_addr</a>(addr1); </code></pre>

If there is a preburn resource published, it must have a value of zero. If there is a preburn resource published, there cannot also be a <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource published under that same account for the same currency.

NB: This invariant is part of the upgrade process, eventually this will be removed once all DD's have been upgraded to using the <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code>.

<pre><code>invariant<CoinType> forall dd_addr: address where exists<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(dd_addr): global<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(dd_addr).to_burn.value == 0 && !exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(dd_addr); </code></pre>

If there is a <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource published, then there cannot also be a <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> resource for that same currency published under the same address.

<pre><code>invariant<CoinType> forall dd_addr: address where exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(dd_addr): !exists<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(dd_addr); </code></pre>

A <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> resource can only be published holding a currency type.

<pre><code>invariant<CoinType> forall addr: address where exists<<a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType>>(addr): <a href="Diem.md#0x1_Diem_spec_is_currency">spec_is_currency</a><CoinType>(); </code></pre>

A <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource can only be published holding a currency type.

TODO: This assertion is causing a violation for unknown reasons, probably a prover bug. Preburn is not transferrable [J4].

<pre><code>apply <a href="Diem.md#0x1_Diem_PreservePreburnQueueExistence">PreservePreburnQueueExistence</a><CoinType> to *<CoinType>; </code></pre>

resource struct <code><a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a></code> is persistent

<pre><code>invariant<CoinType> update forall dr_addr: address where old(exists<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(dr_addr)): exists<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(dr_addr); </code></pre>

resource struct <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType></code> is persistent

<pre><code>invariant<CoinType> update forall tc_addr: address where old(exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(tc_addr)): exists<<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a><CoinType>>(tc_addr); </code></pre>

resource struct <code><a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType></code> is persistent

<pre><code>invariant<CoinType> update forall tc_addr: address where old(exists<<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>>(tc_addr)): exists<<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>>(tc_addr); </code></pre>

Update Exchange Rates

Only TreasuryCompliance can change the exchange rate [H5].

<pre><code>invariant<CoinType> update old(<a href="Diem.md#0x1_Diem_spec_is_currency">spec_is_currency</a><CoinType>()) ==> ((<a href="Diem.md#0x1_Diem_spec_xdx_exchange_rate">spec_xdx_exchange_rate</a><CoinType>() != old(<a href="Diem.md#0x1_Diem_spec_xdx_exchange_rate">spec_xdx_exchange_rate</a><CoinType>())) ==> <a href="Roles.md#0x1_Roles_spec_signed_by_treasury_compliance_role">Roles::spec_signed_by_treasury_compliance_role</a>()); </code></pre>

Enable/disable minting

Only TreasuryCompliance can enable/disable minting [H2].

<pre><code>invariant<CoinType> update old(<a href="Diem.md#0x1_Diem_spec_is_currency">spec_is_currency</a><CoinType>()) ==> ((<a href="Diem.md#0x1_Diem_spec_can_mint">spec_can_mint</a><CoinType>() != old(<a href="Diem.md#0x1_Diem_spec_can_mint">spec_can_mint</a><CoinType>())) ==> <a href="Roles.md#0x1_Roles_spec_signed_by_treasury_compliance_role">Roles::spec_signed_by_treasury_compliance_role</a>()); </code></pre>

Register new currency

Only DiemRoot can register a new currency [H8].

<pre><code>invariant<CoinType> update !old(<a href="Diem.md#0x1_Diem_spec_is_currency">spec_is_currency</a><CoinType>()) && <a href="Diem.md#0x1_Diem_spec_is_currency">spec_is_currency</a><CoinType>() ==> <a href="Roles.md#0x1_Roles_spec_signed_by_diem_root_role">Roles::spec_signed_by_diem_root_role</a>(); </code></pre>

Helper Functions

Checks whether currency is registered. Mirrors <code><a href="Diem.md#0x1_Diem_is_currency">Self::is_currency</a><CoinType></code>.

<pre><code>fun <a href="Diem.md#0x1_Diem_spec_is_currency">spec_is_currency</a><CoinType>(): bool { exists<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>) } </code></pre>

Returns currency information.

<pre><code>fun <a href="Diem.md#0x1_Diem_spec_currency_info">spec_currency_info</a><CoinType>(): <a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType> { global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>) } </code></pre>

Specification version of <code><a href="Diem.md#0x1_Diem_approx_xdx_for_value">Self::approx_xdx_for_value</a></code>.

<pre><code>fun <a href="Diem.md#0x1_Diem_spec_approx_xdx_for_value">spec_approx_xdx_for_value</a><CoinType>(value: num): num { <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32_spec_multiply_u64">FixedPoint32::spec_multiply_u64</a>(value, <a href="Diem.md#0x1_Diem_spec_xdx_exchange_rate">spec_xdx_exchange_rate</a><CoinType>()) } </code></pre>

Returns the <code>to_xdx_exchange_rate</code> of CoinType

<pre><code>fun <a href="Diem.md#0x1_Diem_spec_xdx_exchange_rate">spec_xdx_exchange_rate</a><CoinType>(): <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32">FixedPoint32</a> { global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>).to_xdx_exchange_rate } </code></pre>

Returns the <code>to_xdx_exchange_rate</code> of CoinType

<pre><code>fun <a href="Diem.md#0x1_Diem_spec_can_mint">spec_can_mint</a><CoinType>(): bool { global<<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a><CoinType>>(@<a href="Diem.md#0x1_Diem_CurrencyInfo">CurrencyInfo</a>).can_mint } </code></pre>

Checks whether the currency has a mint capability. This is only relevant for SCS coins

<pre><code>fun <a href="Diem.md#0x1_Diem_spec_has_mint_capability">spec_has_mint_capability</a><CoinType>(addr: address): bool { exists<<a href="Diem.md#0x1_Diem_MintCapability">MintCapability</a><CoinType>>(addr) } </code></pre>

Returns true if a BurnCapability for CoinType exists at addr.

<pre><code>fun <a href="Diem.md#0x1_Diem_spec_has_burn_capability">spec_has_burn_capability</a><CoinType>(addr: address): bool { exists<<a href="Diem.md#0x1_Diem_BurnCapability">BurnCapability</a><CoinType>>(addr) } </code></pre>

Returns the Preburn in the preburn queue.

<pre><code>fun <a href="Diem.md#0x1_Diem_spec_make_preburn">spec_make_preburn</a><CoinType>(amount: u64): <a href="Diem.md#0x1_Diem_Preburn">Preburn</a><CoinType> { <a href="Diem.md#0x1_Diem_Preburn">Preburn</a> { to_burn: <a href="Diem.md#0x1_Diem">Diem</a> { value: amount }} } </code></pre>

Module `0x1::Diem`

Module 0x1::Diem

Struct Diem

Resource MintCapability

Resource BurnCapability

Struct MintEvent

Struct BurnEvent

Struct PreburnEvent

Struct CancelBurnEvent

Struct ToXDXExchangeRateUpdateEvent

Resource CurrencyInfo

Resource Preburn

Struct PreburnWithMetadata

Resource PreburnQueue

Constants

Function initialize

Function publish_burn_capability

Function mint

Function burn

Function cancel_burn

Function mint_with_capability

Function preburn_with_resource

Function create_preburn

Function publish_preburn_queue

Function publish_preburn_queue_to_account

Function publish_preburn_queue_to_account_for_test

Function upgrade_preburn

Function add_preburn_to_queue

Function preburn_to

Function remove_preburn_from_queue

Function burn_with_capability

Function burn_with_resource_cap

Function cancel_burn_with_capability

Function burn_now

Function remove_burn_capability

Function preburn_value

Function zero

Function value

Function split

Function withdraw

Function withdraw_all

Function join

Function deposit

Function destroy_zero

Function register_currency

Function register_SCS_currency

Function market_cap

Function approx_xdx_for_value

Function approx_xdx_for_coin

Function is_currency

Function is_SCS_currency

Function is_synthetic_currency

Function scaling_factor

Function fractional_part

Function currency_code

Function update_xdx_exchange_rate

Function xdx_exchange_rate

Function update_minting_ability

Function assert_is_currency

Function assert_is_SCS_currency

Module Specification

Access Control

Minting

Burning

Preburning

Update Exchange Rates

Enable/disable minting

Register new currency

Helper Functions

Module `0x1::Diem`

Struct `Diem`

Resource `MintCapability`

Resource `BurnCapability`

Struct `MintEvent`

Struct `BurnEvent`

Struct `PreburnEvent`

Struct `CancelBurnEvent`

Struct `ToXDXExchangeRateUpdateEvent`

Resource `CurrencyInfo`

Resource `Preburn`

Struct `PreburnWithMetadata`

Resource `PreburnQueue`

Function `initialize`

Function `publish_burn_capability`

Function `mint`

Function `burn`

Function `cancel_burn`

Function `mint_with_capability`

Function `preburn_with_resource`

Function `create_preburn`

Function `publish_preburn_queue`

Function `publish_preburn_queue_to_account`

Function `publish_preburn_queue_to_account_for_test`

Function `upgrade_preburn`

Function `add_preburn_to_queue`

Function `preburn_to`

Function `remove_preburn_from_queue`

Function `burn_with_capability`

Function `burn_with_resource_cap`

Function `cancel_burn_with_capability`

Function `burn_now`

Function `remove_burn_capability`

Function `preburn_value`

Function `zero`

Function `value`

Function `split`

Function `withdraw`

Function `withdraw_all`

Function `join`

Function `deposit`

Function `destroy_zero`

Function `register_currency`

Function `register_SCS_currency`

Function `market_cap`

Function `approx_xdx_for_value`

Function `approx_xdx_for_coin`

Function `is_currency`

Function `is_SCS_currency`

Function `is_synthetic_currency`

Function `scaling_factor`

Function `fractional_part`

Function `currency_code`

Function `update_xdx_exchange_rate`

Function `xdx_exchange_rate`

Function `update_minting_ability`

Function `assert_is_currency`

Function `assert_is_SCS_currency`