Module `0x1::XDX`

NB: This module is a stub of the <code><a href="XDX.md#0x1_XDX">XDX</a></code> at the moment.

Once the component makeup of the XDX has been chosen the <code><a href="XDX.md#0x1_XDX_Reserve">Reserve</a></code> will be updated to hold the backing coins in the correct ratios.

Struct XDX
Resource Reserve
Constants
Function initialize
Function is_xdx
Function reserve_address
Module Specification
- Persistence of Resources
- Helper Functions

<pre><code>use <a href="AccountLimits.md#0x1_AccountLimits">0x1::AccountLimits</a>; use <a href="CoreAddresses.md#0x1_CoreAddresses">0x1::CoreAddresses</a>; use <a href="Diem.md#0x1_Diem">0x1::Diem</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/FixedPoint32.md#0x1_FixedPoint32">0x1::FixedPoint32</a>; </code></pre>

Struct `XDX`

The type tag representing the <code><a href="XDX.md#0x1_XDX">XDX</a></code> currency on-chain.

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

Resource `Reserve`

Note: Currently only holds the mint, burn, and preburn capabilities for XDX. Once the makeup of the XDX has been determined this resource will be updated to hold the backing XDX reserve compnents on-chain.

The on-chain reserve for the <code><a href="XDX.md#0x1_XDX">XDX</a></code> holds both the capability for minting <code><a href="XDX.md#0x1_XDX">XDX</a></code> coins, and also each reserve component that holds the backing for these coins on-chain. Currently this holds no coins since XDX is not able to be minted/created.

<pre><code>resource struct <a href="XDX.md#0x1_XDX_Reserve">Reserve</a> </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>mint_cap: <a href="Diem.md#0x1_Diem_MintCapability">Diem::MintCapability</a><<a href="XDX.md#0x1_XDX_XDX">XDX::XDX</a>></code> </dt> <dd> The mint capability allowing minting of <code><a href="XDX.md#0x1_XDX">XDX</a></code> coins. </dd> <dt> <code>burn_cap: <a href="Diem.md#0x1_Diem_BurnCapability">Diem::BurnCapability</a><<a href="XDX.md#0x1_XDX_XDX">XDX::XDX</a>></code> </dt> <dd> The burn capability for <code><a href="XDX.md#0x1_XDX">XDX</a></code> coins. This is used for the unpacking of <code><a href="XDX.md#0x1_XDX">XDX</a></code> coins into the underlying backing currencies. </dd> <dt> <code>preburn_cap: <a href="Diem.md#0x1_Diem_Preburn">Diem::Preburn</a><<a href="XDX.md#0x1_XDX_XDX">XDX::XDX</a>></code> </dt> <dd> The preburn for <code><a href="XDX.md#0x1_XDX">XDX</a></code>. This is an administrative field since we need to alway preburn before we burn. </dd> </dl> </details>

Constants

The <code><a href="XDX.md#0x1_XDX_Reserve">Reserve</a></code> resource is in an invalid state

<pre><code>const <a href="XDX.md#0x1_XDX_ERESERVE">ERESERVE</a>: u64 = 0; </code></pre>

Function `initialize`

Initializes the <code><a href="XDX.md#0x1_XDX">XDX</a></code> module. This sets up the initial <code><a href="XDX.md#0x1_XDX">XDX</a></code> ratios and reserve components, and creates the mint, preburn, and burn capabilities for <code><a href="XDX.md#0x1_XDX">XDX</a></code> coins. The <code><a href="XDX.md#0x1_XDX">XDX</a></code> currency must not already be registered in order for this to succeed. The sender must both be the correct address (<code><a href="CoreAddresses.md#0x1_CoreAddresses_CURRENCY_INFO_ADDRESS">CoreAddresses::CURRENCY_INFO_ADDRESS</a></code>) and have the correct permissions (<code>&Capability<RegisterNewCurrency></code>). Both of these restrictions are enforced in the <code><a href="Diem.md#0x1_Diem_register_currency">Diem::register_currency</a></code> function, but also enforced here.

<pre><code>public fun <a href="XDX.md#0x1_XDX_initialize">initialize</a>(dr_account: &signer, tc_account: &signer) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="XDX.md#0x1_XDX_initialize">initialize</a>( dr_account: &signer, tc_account: &signer, ) { <a href="DiemTimestamp.md#0x1_DiemTimestamp_assert_genesis">DiemTimestamp::assert_genesis</a>(); // Operational constraint <a href="CoreAddresses.md#0x1_CoreAddresses_assert_currency_info">CoreAddresses::assert_currency_info</a>(dr_account); // <a href="XDX.md#0x1_XDX_Reserve">Reserve</a> must not exist. assert(!exists<<a href="XDX.md#0x1_XDX_Reserve">Reserve</a>>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()), <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_already_published">Errors::already_published</a>(<a href="XDX.md#0x1_XDX_ERESERVE">ERESERVE</a>)); let (mint_cap, burn_cap) = <a href="Diem.md#0x1_Diem_register_currency">Diem::register_currency</a><<a href="XDX.md#0x1_XDX">XDX</a>>( dr_account, <a href="../../../../../../move-stdlib/docs/FixedPoint32.md#0x1_FixedPoint32_create_from_rational">FixedPoint32::create_from_rational</a>(1, 1), // exchange rate to <a href="XDX.md#0x1_XDX">XDX</a> true, // is_synthetic 1000000, // scaling_factor = 10^6 1000, // fractional_part = 10^3 b"<a href="XDX.md#0x1_XDX">XDX</a>" ); // <a href="XDX.md#0x1_XDX">XDX</a> cannot be minted. <a href="Diem.md#0x1_Diem_update_minting_ability">Diem::update_minting_ability</a><<a href="XDX.md#0x1_XDX">XDX</a>>(tc_account, false); <a href="AccountLimits.md#0x1_AccountLimits_publish_unrestricted_limits">AccountLimits::publish_unrestricted_limits</a><<a href="XDX.md#0x1_XDX">XDX</a>>(dr_account); let preburn_cap = <a href="Diem.md#0x1_Diem_create_preburn">Diem::create_preburn</a><<a href="XDX.md#0x1_XDX">XDX</a>>(tc_account); move_to(dr_account, <a href="XDX.md#0x1_XDX_Reserve">Reserve</a> { mint_cap, burn_cap, preburn_cap }); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="CoreAddresses.md#0x1_CoreAddresses_AbortsIfNotCurrencyInfo">CoreAddresses::AbortsIfNotCurrencyInfo</a>{account: dr_account}; aborts_if exists<<a href="XDX.md#0x1_XDX_Reserve">Reserve</a>>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()) with <a href="../../../../../../move-stdlib/docs/Errors.md#0x1_Errors_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; include <a href="Diem.md#0x1_Diem_RegisterCurrencyAbortsIf">Diem::RegisterCurrencyAbortsIf</a><<a href="XDX.md#0x1_XDX">XDX</a>>{ currency_code: b"<a href="XDX.md#0x1_XDX">XDX</a>", scaling_factor: 1000000 }; include <a href="AccountLimits.md#0x1_AccountLimits_PublishUnrestrictedLimitsAbortsIf">AccountLimits::PublishUnrestrictedLimitsAbortsIf</a><<a href="XDX.md#0x1_XDX">XDX</a>>{publish_account: dr_account}; include <a href="Diem.md#0x1_Diem_RegisterCurrencyEnsures">Diem::RegisterCurrencyEnsures</a><<a href="XDX.md#0x1_XDX">XDX</a>>; include <a href="Diem.md#0x1_Diem_UpdateMintingAbilityEnsures">Diem::UpdateMintingAbilityEnsures</a><<a href="XDX.md#0x1_XDX">XDX</a>>{can_mint: false}; include <a href="AccountLimits.md#0x1_AccountLimits_PublishUnrestrictedLimitsEnsures">AccountLimits::PublishUnrestrictedLimitsEnsures</a><<a href="XDX.md#0x1_XDX">XDX</a>>{publish_account: dr_account}; ensures exists<<a href="XDX.md#0x1_XDX_Reserve">Reserve</a>>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()); </code></pre>

Registering XDX can only be done in genesis.

<pre><code>include <a href="DiemTimestamp.md#0x1_DiemTimestamp_AbortsIfNotGenesis">DiemTimestamp::AbortsIfNotGenesis</a>; </code></pre>

Only the DiemRoot account can register a new currency [H8].

<pre><code>include <a href="Roles.md#0x1_Roles_AbortsIfNotDiemRoot">Roles::AbortsIfNotDiemRoot</a>{account: dr_account}; </code></pre>

Only the TreasuryCompliance role can update the <code>can_mint</code> field of CurrencyInfo [H2]. Moreover, only the TreasuryCompliance role can create Preburn.

<pre><code>include <a href="Roles.md#0x1_Roles_AbortsIfNotTreasuryCompliance">Roles::AbortsIfNotTreasuryCompliance</a>{account: tc_account}; </code></pre> </details>

Function `is_xdx`

Returns true if <code>CoinType</code> is <code><a href="XDX.md#0x1_XDX_XDX">XDX::XDX</a></code>

<pre><code>public fun <a href="XDX.md#0x1_XDX_is_xdx">is_xdx</a><CoinType>(): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="XDX.md#0x1_XDX_is_xdx">is_xdx</a><CoinType: store>(): bool { <a href="Diem.md#0x1_Diem_is_currency">Diem::is_currency</a><CoinType>() && <a href="Diem.md#0x1_Diem_currency_code">Diem::currency_code</a><CoinType>() == <a href="Diem.md#0x1_Diem_currency_code">Diem::currency_code</a><<a href="XDX.md#0x1_XDX">XDX</a>>() } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="Diem.md#0x1_Diem_spec_is_currency">Diem::spec_is_currency</a><CoinType>() ==> <a href="Diem.md#0x1_Diem_AbortsIfNoCurrency">Diem::AbortsIfNoCurrency</a><<a href="XDX.md#0x1_XDX">XDX</a>>; ensures result == <a href="XDX.md#0x1_XDX_spec_is_xdx">spec_is_xdx</a><CoinType>(); </code></pre>

<pre><code>define <a href="XDX.md#0x1_XDX_spec_is_xdx">spec_is_xdx</a><CoinType>(): bool { <a href="Diem.md#0x1_Diem_spec_is_currency">Diem::spec_is_currency</a><CoinType>() && <a href="Diem.md#0x1_Diem_spec_is_currency">Diem::spec_is_currency</a><<a href="XDX.md#0x1_XDX">XDX</a>>() && (<a href="Diem.md#0x1_Diem_spec_currency_code">Diem::spec_currency_code</a><CoinType>() == <a href="Diem.md#0x1_Diem_spec_currency_code">Diem::spec_currency_code</a><<a href="XDX.md#0x1_XDX">XDX</a>>()) } </code></pre> </details>

Function `reserve_address`

Return the account address where the globally unique XDX::Reserve resource is stored

<pre><code>public fun <a href="XDX.md#0x1_XDX_reserve_address">reserve_address</a>(): address </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="XDX.md#0x1_XDX_reserve_address">reserve_address</a>(): address { <a href="CoreAddresses.md#0x1_CoreAddresses_CURRENCY_INFO_ADDRESS">CoreAddresses::CURRENCY_INFO_ADDRESS</a>() } </code></pre> </details>

Module Specification

Persistence of Resources

After genesis, the Reserve resource exists.

<pre><code>invariant [global] <a href="DiemTimestamp.md#0x1_DiemTimestamp_is_operating">DiemTimestamp::is_operating</a>() ==> <a href="XDX.md#0x1_XDX_reserve_exists">reserve_exists</a>(); </code></pre>

After genesis, XDX is registered.

<pre><code>invariant [global] <a href="DiemTimestamp.md#0x1_DiemTimestamp_is_operating">DiemTimestamp::is_operating</a>() ==> <a href="Diem.md#0x1_Diem_is_currency">Diem::is_currency</a><<a href="XDX.md#0x1_XDX">XDX</a>>(); </code></pre>

Helper Functions

Checks whether the Reserve resource exists.

<pre><code>define <a href="XDX.md#0x1_XDX_reserve_exists">reserve_exists</a>(): bool { exists<<a href="XDX.md#0x1_XDX_Reserve">Reserve</a>>(<a href="CoreAddresses.md#0x1_CoreAddresses_CURRENCY_INFO_ADDRESS">CoreAddresses::CURRENCY_INFO_ADDRESS</a>()) } </code></pre>

After genesis, <code>LimitsDefinition<<a href="XDX.md#0x1_XDX">XDX</a>></code> is published at Diem root. It's published by AccountLimits::publish_unrestricted_limits, but we can't prove the condition there because it does not hold for all types (but does hold for XDX).

<pre><code>invariant [global] <a href="DiemTimestamp.md#0x1_DiemTimestamp_is_operating">DiemTimestamp::is_operating</a>() ==> exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">AccountLimits::LimitsDefinition</a><<a href="XDX.md#0x1_XDX">XDX</a>>>(<a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>()); </code></pre>

<code>LimitsDefinition<<a href="XDX.md#0x1_XDX">XDX</a>></code> is not published at any other address

<pre><code>invariant [global] forall addr: address where exists<<a href="AccountLimits.md#0x1_AccountLimits_LimitsDefinition">AccountLimits::LimitsDefinition</a><<a href="XDX.md#0x1_XDX">XDX</a>>>(addr): addr == <a href="CoreAddresses.md#0x1_CoreAddresses_DIEM_ROOT_ADDRESS">CoreAddresses::DIEM_ROOT_ADDRESS</a>(); </code></pre>

<code><a href="XDX.md#0x1_XDX_Reserve">Reserve</a></code> is persistent

<pre><code>invariant update [global] old(exists<<a href="XDX.md#0x1_XDX_Reserve">Reserve</a>>(<a href="XDX.md#0x1_XDX_reserve_address">reserve_address</a>())) ==> exists<<a href="XDX.md#0x1_XDX_Reserve">Reserve</a>>(<a href="XDX.md#0x1_XDX_reserve_address">reserve_address</a>()); </code></pre>

Module `0x1::XDX`

Module 0x1::XDX

Struct XDX

Resource Reserve

Constants

Function initialize

Function is_xdx

Function reserve_address

Module Specification

Persistence of Resources

Helper Functions

Module `0x1::XDX`

Struct `XDX`

Resource `Reserve`

Function `initialize`

Function `is_xdx`

Function `reserve_address`