starcoin-framework

Module 0x1::Token

Token implementation of Starcoin.

use 0x1::Errors;
use 0x1::Event;
use 0x1::Math;
use 0x1::Signer;

Struct Token

The token has a TokenType color that tells us what token the value inside represents.

struct Token<TokenType> has store
Fields
value: u128

Struct TokenCode

Token Code which identify a unique Token.

struct TokenCode has copy, drop, store
Fields
addr: address
address who define the module contains the Token Type.
module_name: vector<u8>
module which contains the Token Type.
name: vector<u8>
name of the token. may nested if the token is an instantiated generic token type.

Resource MintCapability

A minting capability allows tokens of type TokenType to be minted

struct MintCapability<TokenType> has store, key
Fields
dummy_field: bool

Resource FixedTimeMintKey

A fixed time mint key which can mint token until global time > end_time

struct FixedTimeMintKey<TokenType> has store, key
Fields
total: u128
end_time: u64

Resource LinearTimeMintKey

A linear time mint key which can mint token in a period by time-based linear release.

struct LinearTimeMintKey<TokenType> has store, key
Fields
total: u128
minted: u128
start_time: u64
period: u64

Resource BurnCapability

A burn capability allows tokens of type TokenType to be burned.

struct BurnCapability<TokenType> has store, key
Fields
dummy_field: bool

Struct MintEvent

Event emitted when token minted.

struct MintEvent has drop, store
Fields
amount: u128
funds added to the system
token_code: Token::TokenCode
full info of Token.

Struct BurnEvent

Event emitted when token burned.

struct BurnEvent has drop, store
Fields
amount: u128
funds removed from the system
token_code: Token::TokenCode
full info of Token

Resource TokenInfo

Token information.

struct TokenInfo<TokenType> has key
Fields
total_value: u128
The total value for the token represented by TokenType. Mutable.
scaling_factor: u128
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 Coin1
mint_events: Event::EventHandle<Token::MintEvent>
event stream for minting
burn_events: Event::EventHandle<Token::BurnEvent>
event stream for burning

Constants

const EAMOUNT_EXCEEDS_COIN_VALUE: u64 = 102;


const EDEPRECATED_FUNCTION: u64 = 19;


const EDESTROY_KEY_NOT_EMPTY: u64 = 104;


const EDESTROY_TOKEN_NON_ZERO: u64 = 16;


const EEMPTY_KEY: u64 = 106;


const EINVALID_ARGUMENT: u64 = 18;


const EMINT_AMOUNT_EQUAL_ZERO: u64 = 109;


const EMINT_KEY_TIME_LIMIT: u64 = 103;


const EPERIOD_NEW: u64 = 108;


const EPRECISION_TOO_LARGE: u64 = 105;


const ESPLIT: u64 = 107;

Token register’s address should same as TokenType’s address.

const ETOKEN_REGISTER: u64 = 101;

2^128 < 10**39

const MAX_PRECISION: u8 = 38;

Function register_token

Register the type TokenType as a Token and got MintCapability and BurnCapability.

public fun register_token<TokenType: store>(account: &signer, precision: u8)
Implementation 
public fun register_token<TokenType: store>(
    account: &signer,
    precision: u8,
) {
    assert!(precision <= MAX_PRECISION, Errors::invalid_argument(EPRECISION_TOO_LARGE));
    let scaling_factor = Math::pow(10, (precision as u64));
    let token_address = token_address<TokenType>();
    assert!(Signer::address_of(account) == token_address, Errors::requires_address(ETOKEN_REGISTER));
    move_to(account, MintCapability<TokenType> {});
    move_to(account, BurnCapability<TokenType> {});
    move_to(
        account,
        TokenInfo<TokenType> {
            total_value: 0,
            scaling_factor,
            mint_events: Event::new_event_handle<MintEvent>(account),
            burn_events: Event::new_event_handle<BurnEvent>(account),
        },
    );
}
Specification 
include RegisterTokenAbortsIf<TokenType>;
include RegisterTokenEnsures<TokenType>;

schema RegisterTokenAbortsIf<TokenType> {
    precision: u8;
    account: signer;
    aborts_if precision > MAX_PRECISION;
    aborts_if Signer::address_of(account) != SPEC_TOKEN_TEST_ADDRESS();
    aborts_if exists<MintCapability<TokenType>>(Signer::address_of(account));
    aborts_if exists<BurnCapability<TokenType>>(Signer::address_of(account));
    aborts_if exists<TokenInfo<TokenType>>(Signer::address_of(account));
}

schema RegisterTokenEnsures<TokenType> {
    account: signer;
    ensures exists<MintCapability<TokenType>>(Signer::address_of(account));
    ensures exists<BurnCapability<TokenType>>(Signer::address_of(account));
    ensures exists<TokenInfo<TokenType>>(Signer::address_of(account));
}

Function remove_mint_capability

Remove mint capability from signer.

public fun remove_mint_capability<TokenType: store>(signer: &signer): Token::MintCapability<TokenType>
Implementation 
public fun remove_mint_capability<TokenType: store>(signer: &signer): MintCapability<TokenType>
acquires MintCapability {
    move_from<MintCapability<TokenType>>(Signer::address_of(signer))
}
Specification 
aborts_if !exists<MintCapability<TokenType>>(Signer::address_of(signer));
ensures !exists<MintCapability<TokenType>>(Signer::address_of(signer));

Function add_mint_capability

Add mint capability to signer.

public fun add_mint_capability<TokenType: store>(signer: &signer, cap: Token::MintCapability<TokenType>)
Implementation 
public fun add_mint_capability<TokenType: store>(signer: &signer, cap: MintCapability<TokenType>) {
    move_to(signer, cap)
}
Specification 
aborts_if exists<MintCapability<TokenType>>(Signer::address_of(signer));
ensures exists<MintCapability<TokenType>>(Signer::address_of(signer));

Function destroy_mint_capability

Destroy the given mint capability.

public fun destroy_mint_capability<TokenType: store>(cap: Token::MintCapability<TokenType>)
Implementation 
public fun destroy_mint_capability<TokenType: store>(cap: MintCapability<TokenType>) {
    let MintCapability<TokenType> {} = cap;
}
Specification

Function remove_burn_capability

remove the token burn capability from signer.

public fun remove_burn_capability<TokenType: store>(signer: &signer): Token::BurnCapability<TokenType>
Implementation 
public fun remove_burn_capability<TokenType: store>(signer: &signer): BurnCapability<TokenType>
acquires BurnCapability {
    move_from<BurnCapability<TokenType>>(Signer::address_of(signer))
}
Specification 
aborts_if !exists<BurnCapability<TokenType>>(Signer::address_of(signer));
ensures !exists<BurnCapability<TokenType>>(Signer::address_of(signer));

Function add_burn_capability

Add token burn capability to signer.

public fun add_burn_capability<TokenType: store>(signer: &signer, cap: Token::BurnCapability<TokenType>)
Implementation 
public fun add_burn_capability<TokenType: store>(signer: &signer, cap: BurnCapability<TokenType>) {
    move_to(signer, cap)
}
Specification 
aborts_if exists<BurnCapability<TokenType>>(Signer::address_of(signer));
ensures exists<BurnCapability<TokenType>>(Signer::address_of(signer));

Function destroy_burn_capability

Destroy the given burn capability.

public fun destroy_burn_capability<TokenType: store>(cap: Token::BurnCapability<TokenType>)
Implementation 
public fun destroy_burn_capability<TokenType: store>(cap: BurnCapability<TokenType>) {
    let BurnCapability<TokenType> {} = cap;
}
Specification

Function mint

Return amount tokens. Fails if the sender does not have a published MintCapability.

public fun mint<TokenType: store>(account: &signer, amount: u128): Token::Token<TokenType>
Implementation 
public fun mint<TokenType: store>(account: &signer, amount: u128): Token<TokenType>
acquires TokenInfo, MintCapability {
    mint_with_capability(
        borrow_global<MintCapability<TokenType>>(Signer::address_of(account)),
        amount,
    )
}
Specification 
aborts_if spec_abstract_total_value<TokenType>() + amount > MAX_U128;
aborts_if !exists<MintCapability<TokenType>>(Signer::address_of(account));

Function mint_with_capability

Mint a new Token::Token worth amount. The caller must have a reference to a MintCapability. Only the Association account can acquire such a reference, and it can do so only via borrow_sender_mint_capability

public fun mint_with_capability<TokenType: store>(_capability: &Token::MintCapability<TokenType>, amount: u128): Token::Token<TokenType>
Implementation 
public fun mint_with_capability<TokenType: store>(
    _capability: &MintCapability<TokenType>,
    amount: u128,
): Token<TokenType> acquires TokenInfo {
    do_mint(amount)
}
Specification 
aborts_if spec_abstract_total_value<TokenType>() + amount > MAX_U128;
ensures spec_abstract_total_value<TokenType>() ==
        old(global<TokenInfo<TokenType>>(SPEC_TOKEN_TEST_ADDRESS()).total_value) + amount;

Function do_mint

fun do_mint<TokenType: store>(amount: u128): Token::Token<TokenType>
Implementation 
fun do_mint<TokenType: store>(amount: u128): Token<TokenType> acquires TokenInfo {
    // update market cap resource to reflect minting
    let (token_address, module_name, token_name) = name_of_token<TokenType>();
    let info = borrow_global_mut<TokenInfo<TokenType>>(token_address);
    info.total_value = info.total_value + amount;
    Event::emit_event(
        &mut info.mint_events,
        MintEvent {
            amount,
            token_code: TokenCode { addr: token_address, module_name, name: token_name },
        },
    );
    Token<TokenType> { value: amount }
}
Specification 
aborts_if !exists<TokenInfo<TokenType>>(SPEC_TOKEN_TEST_ADDRESS());
aborts_if spec_abstract_total_value<TokenType>() + amount > MAX_U128;

Function issue_fixed_mint_key

Deprecated since @v3 Issue a FixedTimeMintKey with given MintCapability.

public fun issue_fixed_mint_key<TokenType: store>(_capability: &Token::MintCapability<TokenType>, _amount: u128, _period: u64): Token::FixedTimeMintKey<TokenType>
Implementation 
public fun issue_fixed_mint_key<TokenType: store>(
    _capability: &MintCapability<TokenType>,
    _amount: u128,
    _period: u64,
): FixedTimeMintKey<TokenType> {
    abort Errors::deprecated(EDEPRECATED_FUNCTION)
}
Specification 
aborts_if true;

Function issue_linear_mint_key

Deprecated since @v3 Issue a LinearTimeMintKey with given MintCapability.

public fun issue_linear_mint_key<TokenType: store>(_capability: &Token::MintCapability<TokenType>, _amount: u128, _period: u64): Token::LinearTimeMintKey<TokenType>
Implementation 
public fun issue_linear_mint_key<TokenType: store>(
    _capability: &MintCapability<TokenType>,
    _amount: u128,
    _period: u64,
): LinearTimeMintKey<TokenType> {
    abort Errors::deprecated(EDEPRECATED_FUNCTION)
}
Specification 
aborts_if true;

Function destroy_linear_time_key

Destroy LinearTimeMintKey, for deprecated

public fun destroy_linear_time_key<TokenType: store>(key: Token::LinearTimeMintKey<TokenType>): (u128, u128, u64, u64)
Implementation 
public fun destroy_linear_time_key<TokenType: store>(key: LinearTimeMintKey<TokenType>): (u128, u128, u64, u64) {
    let LinearTimeMintKey<TokenType> { total, minted, start_time, period } = key;
    (total, minted, start_time, period)
}

Function read_linear_time_key

public fun read_linear_time_key<TokenType: store>(key: &Token::LinearTimeMintKey<TokenType>): (u128, u128, u64, u64)
Implementation 
public fun read_linear_time_key<TokenType: store>(key: &LinearTimeMintKey<TokenType>): (u128, u128, u64, u64) {
    (key.total, key.minted, key.start_time, key.period)
}

Function burn

Burn some tokens of signer.

public fun burn<TokenType: store>(account: &signer, tokens: Token::Token<TokenType>)
Implementation 
public fun burn<TokenType: store>(account: &signer, tokens: Token<TokenType>)
acquires TokenInfo, BurnCapability {
    burn_with_capability(
        borrow_global<BurnCapability<TokenType>>(Signer::address_of(account)),
        tokens,
    )
}
Specification 
aborts_if spec_abstract_total_value<TokenType>() - tokens.value < 0;
aborts_if !exists<BurnCapability<TokenType>>(Signer::address_of(account));

Function burn_with_capability

Burn tokens with the given BurnCapability.

public fun burn_with_capability<TokenType: store>(_capability: &Token::BurnCapability<TokenType>, tokens: Token::Token<TokenType>)
Implementation 
public fun burn_with_capability<TokenType: store>(
    _capability: &BurnCapability<TokenType>,
    tokens: Token<TokenType>,
) acquires TokenInfo {
    let (token_address, module_name, token_name) = name_of_token<TokenType>();
    let info = borrow_global_mut<TokenInfo<TokenType>>(token_address);
    let Token { value } = tokens;
    info.total_value = info.total_value - value;
    Event::emit_event(
        &mut info.burn_events,
        BurnEvent {
            amount: value,
            token_code: TokenCode { addr: token_address, module_name, name: token_name },
        },
    );
}
Specification 
aborts_if spec_abstract_total_value<TokenType>() - tokens.value < 0;
ensures spec_abstract_total_value<TokenType>() ==
        old(global<TokenInfo<TokenType>>(SPEC_TOKEN_TEST_ADDRESS()).total_value) - tokens.value;

Function zero

Create a new Token::Token with a value of 0

public fun zero<TokenType: store>(): Token::Token<TokenType>
Implementation 
public fun zero<TokenType: store>(): Token<TokenType> {
    Token<TokenType> { value: 0 }
}
Specification 
ensures result.value == 0;

Function value

Public accessor for the value of a token

public fun value<TokenType: store>(token: &Token::Token<TokenType>): u128
Implementation 
public fun value<TokenType: store>(token: &Token<TokenType>): u128 {
    token.value
}
Specification 
aborts_if false;
ensures result == token.value;

Function split

Splits the given token into two and returns them both

public fun split<TokenType: store>(token: Token::Token<TokenType>, value: u128): (Token::Token<TokenType>, Token::Token<TokenType>)
Implementation 
public fun split<TokenType: store>(
    token: Token<TokenType>,
    value: u128,
): (Token<TokenType>, Token<TokenType>) {
    let rest = withdraw(&mut token, value);
    (token, rest)
}
Specification 
aborts_if token.value < value;
ensures token.value == result_1.value + result_2.value;

Function withdraw

“Divides” the given token into two, where the original token is modified in place. The original token will have value = original value - value The new token will have a value = value Fails if the tokens value is less than value

public fun withdraw<TokenType: store>(token: &mut Token::Token<TokenType>, value: u128): Token::Token<TokenType>
Implementation 
public fun withdraw<TokenType: store>(
    token: &mut Token<TokenType>,
    value: u128,
): Token<TokenType> {
    // Check that `value` is less than the token's value
    assert!(token.value >= value, Errors::limit_exceeded(EAMOUNT_EXCEEDS_COIN_VALUE));
    token.value = token.value - value;
    Token { value: value }
}
Specification 
aborts_if token.value < value;
ensures result.value == value;
ensures token.value == old(token).value - value;

Function join

Merges two tokens of the same token and returns a new token whose value is equal to the sum of the two inputs

public fun join<TokenType: store>(token1: Token::Token<TokenType>, token2: Token::Token<TokenType>): Token::Token<TokenType>
Implementation 
public fun join<TokenType: store>(
    token1: Token<TokenType>,
    token2: Token<TokenType>,
): Token<TokenType> {
    deposit(&mut token1, token2);
    token1
}
Specification 
aborts_if token1.value + token2.value > max_u128();
ensures token1.value + token2.value == result.value;

Function deposit

“Merges” the two tokens The token passed in by reference will have a value equal to the sum of the two tokens The check token is consumed in the process

public fun deposit<TokenType: store>(token: &mut Token::Token<TokenType>, check: Token::Token<TokenType>)
Implementation 
public fun deposit<TokenType: store>(token: &mut Token<TokenType>, check: Token<TokenType>) {
    let Token { value } = check;
    token.value = token.value + value;
}
Specification 
aborts_if token.value + check.value > max_u128();
ensures old(token).value + check.value == token.value;

Function destroy_zero

Destroy a token Fails if the value is non-zero The amount of Token in the system is a tightly controlled property, so you cannot “burn” any non-zero amount of Token

public fun destroy_zero<TokenType: store>(token: Token::Token<TokenType>)
Implementation 
public fun destroy_zero<TokenType: store>(token: Token<TokenType>) {
    let Token { value } = token;
    assert!(value == 0, Errors::invalid_state(EDESTROY_TOKEN_NON_ZERO))
}
Specification 
aborts_if token.value > 0;

Function scaling_factor

Returns the scaling_factor for the TokenType token.

public fun scaling_factor<TokenType: store>(): u128
Implementation 
public fun scaling_factor<TokenType: store>(): u128 acquires TokenInfo {
    let token_address = token_address<TokenType>();
    borrow_global<TokenInfo<TokenType>>(token_address).scaling_factor
}
Specification 
aborts_if false;
ensures result == global<TokenInfo<TokenType>>(SPEC_TOKEN_TEST_ADDRESS()).scaling_factor;

Function market_cap

Return the total amount of token of type TokenType.

public fun market_cap<TokenType: store>(): u128
Implementation 
public fun market_cap<TokenType: store>(): u128 acquires TokenInfo {
    let token_address = token_address<TokenType>();
    borrow_global<TokenInfo<TokenType>>(token_address).total_value
}
Specification 
aborts_if false;
ensures result == global<TokenInfo<TokenType>>(SPEC_TOKEN_TEST_ADDRESS()).total_value;

Function is_registered_in

Return true if the type TokenType is a registered in token_address.

public fun is_registered_in<TokenType: store>(token_address: address): bool
Implementation 
public fun is_registered_in<TokenType: store>(token_address: address): bool {
    exists<TokenInfo<TokenType>>(token_address)
}
Specification 
aborts_if false;
ensures result == exists<TokenInfo<TokenType>>(token_address);

Function is_same_token

Return true if the type TokenType1 is same with TokenType2

public fun is_same_token<TokenType1: store, TokenType2: store>(): bool
Implementation 
public fun is_same_token<TokenType1: store, TokenType2: store>(): bool {
    return token_code<TokenType1>() == token_code<TokenType2>()
}
Specification 
aborts_if false;

Function token_address

Return the TokenType’s address

public fun token_address<TokenType: store>(): address
Implementation 
public fun token_address<TokenType: store>(): address {
    let (addr, _, _) = name_of<TokenType>();
    addr
}
Specification 
pragma opaque = true;
aborts_if false;
ensures [abstract] exists<TokenInfo<TokenType>>(result);
ensures [abstract] result == SPEC_TOKEN_TEST_ADDRESS();
ensures [abstract] global<TokenInfo<TokenType>>(result).total_value == 100000000u128;

Function token_code

Return the token code for the registered token.

public fun token_code<TokenType: store>(): Token::TokenCode
Implementation 
public fun token_code<TokenType: store>(): TokenCode {
    let (addr, module_name, name) = name_of<TokenType>();
    TokenCode {
        addr,
        module_name,
        name
    }
}
Specification 
pragma opaque = true;
aborts_if false;
We use an uninterpreted function to represent the result of derived address. The actual value does not matter for the verification of callers. 
fun spec_token_code<TokenType>(): TokenCode;

Function type_of

public(friend) fun type_of<T>(): (address, vector<u8>, vector<u8>)
Implementation 
public (friend) fun type_of<T>(): (address, vector<u8>, vector<u8>){
    name_of<T>()
}

Function name_of

Return Token’s module address, module name, and type name of TokenType.

fun name_of<TokenType>(): (address, vector<u8>, vector<u8>)
Implementation 
native fun name_of<TokenType>(): (address, vector<u8>, vector<u8>);
Specification 
pragma opaque = true;
aborts_if false;

Function name_of_token

fun name_of_token<TokenType: store>(): (address, vector<u8>, vector<u8>)
Implementation 
fun name_of_token<TokenType: store>(): (address, vector<u8>, vector<u8>) {
    name_of<TokenType>()
}
Specification 
pragma opaque = true;
aborts_if false;
ensures [abstract] exists<TokenInfo<TokenType>>(result_1);
ensures [abstract] result_1 == SPEC_TOKEN_TEST_ADDRESS();
ensures [abstract] global<TokenInfo<TokenType>>(result_1).total_value == 100000000u128;

fun SPEC_TOKEN_TEST_ADDRESS(): address {
   @0x2
}

fun spec_abstract_total_value<TokenType>(): num {
   global<TokenInfo<TokenType>>(SPEC_TOKEN_TEST_ADDRESS()).total_value
}

Module Specification

pragma verify;
pragma aborts_if_is_strict;
This site is open source. Improve this page.