Token implementation of Starcoin.
- Struct
Token
- Struct
TokenCode
- Resource
MintCapability
- Resource
FixedTimeMintKey
- Resource
LinearTimeMintKey
- Resource
BurnCapability
- Struct
MintEvent
- Struct
BurnEvent
- Resource
TokenInfo
- Constants
- Function
register_token
- Function
remove_mint_capability
- Function
add_mint_capability
- Function
destroy_mint_capability
- Function
remove_burn_capability
- Function
add_burn_capability
- Function
destroy_burn_capability
- Function
mint
- Function
mint_with_capability
- Function
do_mint
- Function
issue_fixed_mint_key
- Function
issue_linear_mint_key
- Function
destroy_linear_time_key
- Function
read_linear_time_key
- Function
burn
- Function
burn_with_capability
- Function
zero
- Function
value
- Function
split
- Function
withdraw
- Function
join
- Function
deposit
- Function
destroy_zero
- Function
scaling_factor
- Function
market_cap
- Function
is_registered_in
- Function
is_same_token
- Function
token_address
- Function
token_code
- Function
type_of
- Function
name_of
- Function
name_of_token
- Module Specification
use 0x1::Errors;
use 0x1::Event;
use 0x1::Math;
use 0x1::Signer;
The token has a TokenType
color that tells us what token the
value
inside represents.
struct Token<TokenType> has store
Fields
-
value: u128
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.
A minting capability allows tokens of type TokenType
to be minted
struct MintCapability<TokenType> has store, key
Fields
-
dummy_field: bool
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
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
A burn capability allows tokens of type TokenType
to be burned.
struct BurnCapability<TokenType> has store, key
Fields
-
dummy_field: bool
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.
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
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
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;
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));
}
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));
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));
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
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));
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));
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
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));
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;
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;
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;
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;
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)
}
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)
}
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));
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;
Create a new Token::Token with a value of 0
public fun zero<TokenType: store>(): Token::Token<TokenType>
Implementation
Specification
ensures result.value == 0;
Public accessor for the value of a token
public fun value<TokenType: store>(token: &Token::Token<TokenType>): u128
Specification
aborts_if false;
ensures result == token.value;
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
Specification
aborts_if token.value < value;
ensures token.value == result_1.value + result_2.value;
"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;
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
Specification
aborts_if token1.value + token2.value > max_u128();
ensures token1.value + token2.value == result.value;
"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
Specification
aborts_if token.value + check.value > max_u128();
ensures old(token).value + check.value == token.value;
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;
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;
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;
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);
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;
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;
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;
public(friend) fun type_of<T>(): (address, vector<u8>, vector<u8>)
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;
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
}
pragma verify;
pragma aborts_if_is_strict;