RegisteredCurrencies.md

Module 0x1::RegisteredCurrencies

Module for registering currencies in Diem. Basically, this means adding a string (vector) for the currency name to vector of names in DiemConfig.

• Struct RegisteredCurrencies
• Constants
• Function initialize
• Function add_currency_code
• Module Specification
  • Initialization
  • Helper Functions

use 0x1::DiemConfig;
use 0x1::DiemTimestamp;
use 0x1::Errors;
use 0x1::Roles;
use 0x1::Vector;

Struct RegisteredCurrencies

A DiemConfig config holding all of the currency codes for registered currencies. The inner vector's are string representations of currency names.

struct RegisteredCurrencies

Fields

currency_codes: vector<vector<u8>>

Constants

Attempted to add a currency code that is already in use

const ECURRENCY_CODE_ALREADY_TAKEN: u64 = 0;

Function initialize

Initializes this module. Can only be called from genesis, with a Diem root signer.

public fun initialize(dr_account: &signer)

Implementation

public fun initialize(dr_account: &signer) {
    DiemTimestamp::assert_genesis();
    Roles::assert_diem_root(dr_account);
    DiemConfig::publish_new_config(
        dr_account,
        RegisteredCurrencies { currency_codes: Vector::empty() }
    );
}

Specification

include InitializeAbortsIf;
include InitializeEnsures;

schema InitializeAbortsIf {
    dr_account: signer;
    include DiemTimestamp::AbortsIfNotGenesis;
    include Roles::AbortsIfNotDiemRoot{account: dr_account};
    include DiemConfig::PublishNewConfigAbortsIf<RegisteredCurrencies>;
}

schema InitializeEnsures {
    include DiemConfig::PublishNewConfigEnsures<RegisteredCurrencies>{
        payload: RegisteredCurrencies { currency_codes: Vector::empty() }
    };
    ensures len(get_currency_codes()) == 0;
}

Function add_currency_code

Adds a new currency code. The currency code must not yet exist.

public fun add_currency_code(dr_account: &signer, currency_code: vector<u8>)

Implementation

public fun add_currency_code(
    dr_account: &signer,
    currency_code: vector<u8>,
) {
    let config = DiemConfig::get<RegisteredCurrencies>();
    assert(
        !Vector::contains(&config.currency_codes, ¤cy_code),
        Errors::invalid_argument(ECURRENCY_CODE_ALREADY_TAKEN)
    );
    Vector::push_back(&mut config.currency_codes, currency_code);
    DiemConfig::set(dr_account, config);
}

Specification

include AddCurrencyCodeAbortsIf;
include AddCurrencyCodeEnsures;

schema AddCurrencyCodeAbortsIf {
    dr_account: &signer;
    currency_code: vector<u8>;
    include DiemConfig::SetAbortsIf<RegisteredCurrencies>{ account: dr_account };
}

The same currency code can be only added once.

schema AddCurrencyCodeAbortsIf {
    aborts_if Vector::spec_contains(
        DiemConfig::get<RegisteredCurrencies>().currency_codes,
        currency_code
    ) with Errors::INVALID_ARGUMENT;
}

schema AddCurrencyCodeEnsures {
    currency_code: vector<u8>;
    ensures Vector::eq_push_back(get_currency_codes(), old(get_currency_codes()), currency_code);
    include DiemConfig::SetEnsures<RegisteredCurrencies> {payload: DiemConfig::get<RegisteredCurrencies>()};
}

Module Specification

Initialization

Global invariant that currency config is always available after genesis.

invariant [global] DiemTimestamp::is_operating() ==> DiemConfig::spec_is_published<RegisteredCurrencies>();

Helper Functions

Helper to get the currency code vector.

define get_currency_codes(): vector<vector<u8>> {
    DiemConfig::get<RegisteredCurrencies>().currency_codes
}