starcoin-framework

Module 0x1::Treasury

The module for the Treasury of DAO, which can hold the token of DAO.

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

Resource Treasury

struct Treasury<TokenT> has store, key
Fields
balance: Token::Token<TokenT>
withdraw_events: Event::EventHandle<Treasury::WithdrawEvent>
event handle for treasury withdraw event
deposit_events: Event::EventHandle<Treasury::DepositEvent>
event handle for treasury deposit event
Specification

Resource WithdrawCapability

A withdraw capability allows tokens of type TokenT to be withdraw from Treasury.

struct WithdrawCapability<TokenT> has store, key
Fields
dummy_field: bool

Resource LinearWithdrawCapability

A linear time withdraw capability which can withdraw token from Treasury in a period by time-based linear release.

struct LinearWithdrawCapability<TokenT> has store, key
Fields
total: u128
The total amount of tokens that can be withdrawn by this capability
withdraw: u128
The amount of tokens that have been withdrawn by this capability
start_time: u64
The time-based linear release start time, timestamp in seconds.
period: u64
The time-based linear release period in seconds

Struct WithdrawEvent

Message for treasury withdraw event.

struct WithdrawEvent has drop, store
Fields
amount: u128

Struct DepositEvent

Message for treasury deposit event.

struct DepositEvent has drop, store
Fields
amount: u128

Constants

const ERR_INVALID_PERIOD: u64 = 101;


const ERR_NOT_AUTHORIZED: u64 = 104;


const ERR_TOO_BIG_AMOUNT: u64 = 103;


const ERR_TREASURY_NOT_EXIST: u64 = 105;


const ERR_ZERO_AMOUNT: u64 = 102;

Function initialize

Init a Treasury for TokenT. Can only be called by token issuer.

public fun initialize<TokenT: store>(signer: &signer, init_token: Token::Token<TokenT>): Treasury::WithdrawCapability<TokenT>
Implementation 
public fun initialize<TokenT: store>(signer: &signer, init_token: Token<TokenT>): WithdrawCapability<TokenT> {
    let token_issuer = Token::token_address<TokenT>();
    assert!(Signer::address_of(signer) == token_issuer, Errors::requires_address(ERR_NOT_AUTHORIZED));
    let treasure = Treasury {
        balance: init_token,
        withdraw_events: Event::new_event_handle<WithdrawEvent>(signer),
        deposit_events: Event::new_event_handle<DepositEvent>(signer),
    };
    move_to(signer, treasure);
    WithdrawCapability<TokenT>{}
}
Specification 
aborts_if Signer::address_of(signer) != Token::SPEC_TOKEN_TEST_ADDRESS();
aborts_if exists<Treasury<TokenT>>(Token::SPEC_TOKEN_TEST_ADDRESS());
ensures exists<Treasury<TokenT>>(Token::SPEC_TOKEN_TEST_ADDRESS());
ensures result == WithdrawCapability<TokenT>{};

Function exists_at

Check the Treasury of TokenT is exists.

public fun exists_at<TokenT: store>(): bool
Implementation 
public fun exists_at<TokenT: store>(): bool {
    let token_issuer = Token::token_address<TokenT>();
    exists<Treasury<TokenT>>(token_issuer)
}
Specification 
aborts_if false;
ensures result == exists<Treasury<TokenT>>(Token::SPEC_TOKEN_TEST_ADDRESS());

Function balance

Get the balance of TokenT’s Treasury if the Treasury do not exists, return 0.

public fun balance<TokenT: store>(): u128
Implementation 
public fun balance<TokenT:store>(): u128 acquires Treasury {
    let token_issuer = Token::token_address<TokenT>();
    if (!exists<Treasury<TokenT>>(token_issuer)) {
        return 0
    };
    let treasury = borrow_global<Treasury<TokenT>>(token_issuer);
    Token::value(&treasury.balance)
}
Specification 
aborts_if false;
ensures if (exists<Treasury<TokenT>>(Token::SPEC_TOKEN_TEST_ADDRESS()))
            result == spec_balance<TokenT>()
        else
            result == 0;

Function deposit

public fun deposit<TokenT: store>(token: Token::Token<TokenT>)
Implementation 
public fun deposit<TokenT: store>(token: Token<TokenT>) acquires Treasury {
    assert!(exists_at<TokenT>(), Errors::not_published(ERR_TREASURY_NOT_EXIST));
    let token_address = Token::token_address<TokenT>();
    let treasury = borrow_global_mut<Treasury<TokenT>>(token_address);
    let amount = Token::value(&token);
    Event::emit_event(
        &mut treasury.deposit_events,
        DepositEvent { amount },
    );
    Token::deposit(&mut treasury.balance, token);
}
Specification 
aborts_if !exists<Treasury<TokenT>>(Token::SPEC_TOKEN_TEST_ADDRESS());
aborts_if spec_balance<TokenT>() + token.value > MAX_U128;
ensures spec_balance<TokenT>() == old(spec_balance<TokenT>()) + token.value;

Function do_withdraw

fun do_withdraw<TokenT: store>(amount: u128): Token::Token<TokenT>
Implementation 
fun do_withdraw<TokenT: store>(amount: u128): Token<TokenT> acquires Treasury {
    assert!(amount > 0, Errors::invalid_argument(ERR_ZERO_AMOUNT));
    assert!(exists_at<TokenT>(), Errors::not_published(ERR_TREASURY_NOT_EXIST));
    let token_address = Token::token_address<TokenT>();
    let treasury = borrow_global_mut<Treasury<TokenT>>(token_address);
    assert!(amount <= Token::value(&treasury.balance) , Errors::invalid_argument(ERR_TOO_BIG_AMOUNT));
    Event::emit_event(
        &mut treasury.withdraw_events,
        WithdrawEvent { amount },
    );
    Token::withdraw(&mut treasury.balance, amount)
}
Specification 
include WithdrawSchema<TokenT>;

schema WithdrawSchema<TokenT> {
    amount: u64;
    aborts_if amount <= 0;
    aborts_if !exists<Treasury<TokenT>>(Token::SPEC_TOKEN_TEST_ADDRESS());
    aborts_if spec_balance<TokenT>() < amount;
    ensures spec_balance<TokenT>() ==
        old(spec_balance<TokenT>()) - amount;
}

Function withdraw_with_capability

Withdraw tokens with given LinearWithdrawCapability.

public fun withdraw_with_capability<TokenT: store>(_cap: &mut Treasury::WithdrawCapability<TokenT>, amount: u128): Token::Token<TokenT>
Implementation 
public fun withdraw_with_capability<TokenT: store>(
    _cap: &mut WithdrawCapability<TokenT>,
    amount: u128,
): Token<TokenT> acquires Treasury {
    do_withdraw(amount)
}
Specification 
include WithdrawSchema<TokenT>;

Function withdraw

Withdraw from TokenT’s treasury, the signer must have WithdrawCapability

public fun withdraw<TokenT: store>(signer: &signer, amount: u128): Token::Token<TokenT>
Implementation 
public fun withdraw<TokenT: store>(
    signer: &signer,
    amount: u128
): Token<TokenT> acquires Treasury, WithdrawCapability {
    let cap = borrow_global_mut<WithdrawCapability<TokenT>>(Signer::address_of(signer));
    Self::withdraw_with_capability(cap, amount)
}
Specification 
aborts_if !exists<WithdrawCapability<TokenT>>(Signer::address_of(signer));
include WithdrawSchema<TokenT>;

Function issue_linear_withdraw_capability

Issue a LinearWithdrawCapability with given WithdrawCapability.

public fun issue_linear_withdraw_capability<TokenT: store>(_capability: &mut Treasury::WithdrawCapability<TokenT>, amount: u128, period: u64): Treasury::LinearWithdrawCapability<TokenT>
Implementation 
public fun issue_linear_withdraw_capability<TokenT: store>(
    _capability: &mut WithdrawCapability<TokenT>,
    amount: u128,
    period: u64
): LinearWithdrawCapability<TokenT> {
    assert!(period > 0, Errors::invalid_argument(ERR_INVALID_PERIOD));
    assert!(amount > 0, Errors::invalid_argument(ERR_ZERO_AMOUNT));
    let start_time = Timestamp::now_seconds();
    LinearWithdrawCapability<TokenT> {
        total: amount,
        withdraw: 0,
        start_time,
        period,
    }
}
Specification 
aborts_if period == 0;
aborts_if amount == 0;
aborts_if !exists<Timestamp::CurrentTimeMilliseconds>(StarcoinFramework::CoreAddresses::GENESIS_ADDRESS());

Function withdraw_with_linear_capability

Withdraw tokens with given LinearWithdrawCapability.

public fun withdraw_with_linear_capability<TokenT: store>(cap: &mut Treasury::LinearWithdrawCapability<TokenT>): Token::Token<TokenT>
Implementation 
public fun withdraw_with_linear_capability<TokenT: store>(
    cap: &mut LinearWithdrawCapability<TokenT>,
): Token<TokenT> acquires Treasury {
    let amount = withdraw_amount_of_linear_cap(cap);
    let token = do_withdraw(amount);
    cap.withdraw = cap.withdraw + amount;
    token
}
Specification 
pragma aborts_if_is_partial;

Function withdraw_by_linear

Withdraw from TokenT’s treasury, the signer must have LinearWithdrawCapability

public fun withdraw_by_linear<TokenT: store>(signer: &signer): Token::Token<TokenT>
Implementation 
public fun withdraw_by_linear<TokenT:store>(
    signer: &signer,
): Token<TokenT> acquires Treasury, LinearWithdrawCapability {
    let cap = borrow_global_mut<LinearWithdrawCapability<TokenT>>(Signer::address_of(signer));
    Self::withdraw_with_linear_capability(cap)
}
Specification 
pragma aborts_if_is_partial;
aborts_if !exists<LinearWithdrawCapability<TokenT>>(Signer::address_of(signer));

Function split_linear_withdraw_cap

Split the given LinearWithdrawCapability.

public fun split_linear_withdraw_cap<TokenT: store>(cap: &mut Treasury::LinearWithdrawCapability<TokenT>, amount: u128): (Token::Token<TokenT>, Treasury::LinearWithdrawCapability<TokenT>)
Implementation 
public fun split_linear_withdraw_cap<TokenT: store>(
    cap: &mut LinearWithdrawCapability<TokenT>,
    amount: u128,
): (Token<TokenT>, LinearWithdrawCapability<TokenT>) acquires Treasury {
    assert!(amount > 0, Errors::invalid_argument(ERR_ZERO_AMOUNT));
    let token = Self::withdraw_with_linear_capability(cap);
    assert!((cap.withdraw + amount) <= cap.total, Errors::invalid_argument(ERR_TOO_BIG_AMOUNT));
    cap.total = cap.total - amount;
    let start_time = Timestamp::now_seconds();
    let new_period = cap.start_time + cap.period - start_time;
    let new_key = LinearWithdrawCapability<TokenT> {
        total: amount,
        withdraw: 0,
        start_time,
        period: new_period
    };
    (token, new_key)
}
Specification 
pragma aborts_if_is_partial;
ensures old(cap.total - cap.withdraw) ==
    result_1.value + (result_2.total - result_2.withdraw) + (cap.total - cap.withdraw);

Function withdraw_amount_of_linear_cap

Returns the amount of the LinearWithdrawCapability can mint now.

public fun withdraw_amount_of_linear_cap<TokenT: store>(cap: &Treasury::LinearWithdrawCapability<TokenT>): u128
Implementation 
public fun withdraw_amount_of_linear_cap<TokenT: store>(cap: &LinearWithdrawCapability<TokenT>): u128 {
    let now = Timestamp::now_seconds();
    let elapsed_time = now - cap.start_time;
    if (elapsed_time >= cap.period) {
        cap.total - cap.withdraw
    } else {
        Math::mul_div(cap.total, (elapsed_time as u128), (cap.period as u128)) - cap.withdraw
    }
}
Specification 
pragma aborts_if_is_partial;
aborts_if !exists<Timestamp::CurrentTimeMilliseconds>(StarcoinFramework::CoreAddresses::GENESIS_ADDRESS());
aborts_if Timestamp::spec_now_seconds() < cap.start_time;
aborts_if Timestamp::spec_now_seconds() - cap.start_time >= cap.period && cap.total < cap.withdraw;
aborts_if [abstract]
    Timestamp::spec_now_seconds() - cap.start_time < cap.period && Math::spec_mul_div() < cap.withdraw;
ensures [abstract] result <= cap.total - cap.withdraw;

Function is_empty_linear_withdraw_cap

Check if the given LinearWithdrawCapability is empty.

public fun is_empty_linear_withdraw_cap<TokenT: store>(key: &Treasury::LinearWithdrawCapability<TokenT>): bool
Implementation 
public fun is_empty_linear_withdraw_cap<TokenT:store>(key: &LinearWithdrawCapability<TokenT>) : bool {
    key.total == key.withdraw
}
Specification 
aborts_if false;
ensures result == (key.total == key.withdraw);

Function remove_withdraw_capability

Remove mint capability from signer.

public fun remove_withdraw_capability<TokenT: store>(signer: &signer): Treasury::WithdrawCapability<TokenT>
Implementation 
public fun remove_withdraw_capability<TokenT: store>(signer: &signer): WithdrawCapability<TokenT>
acquires WithdrawCapability {
    move_from<WithdrawCapability<TokenT>>(Signer::address_of(signer))
}
Specification 
aborts_if !exists<WithdrawCapability<TokenT>>(Signer::address_of(signer));
ensures !exists<WithdrawCapability<TokenT>>(Signer::address_of(signer));

Function add_withdraw_capability

Save mint capability to signer.

public fun add_withdraw_capability<TokenT: store>(signer: &signer, cap: Treasury::WithdrawCapability<TokenT>)
Implementation 
public fun add_withdraw_capability<TokenT: store>(signer: &signer, cap: WithdrawCapability<TokenT>) {
    move_to(signer, cap)
}
Specification 
aborts_if exists<WithdrawCapability<TokenT>>(Signer::address_of(signer));
ensures exists<WithdrawCapability<TokenT>>(Signer::address_of(signer));

Function destroy_withdraw_capability

Destroy the given mint capability.

public fun destroy_withdraw_capability<TokenT: store>(cap: Treasury::WithdrawCapability<TokenT>)
Implementation 
public fun destroy_withdraw_capability<TokenT: store>(cap: WithdrawCapability<TokenT>) {
    let WithdrawCapability<TokenT> {} = cap;
}
Specification

Function add_linear_withdraw_capability

Add LinearWithdrawCapability to signer, a address only can have one LinearWithdrawCapability

public fun add_linear_withdraw_capability<TokenT: store>(signer: &signer, cap: Treasury::LinearWithdrawCapability<TokenT>)
Implementation 
public fun add_linear_withdraw_capability<TokenT: store>(signer: &signer, cap: LinearWithdrawCapability<TokenT>) {
    move_to(signer, cap)
}
Specification 
aborts_if exists<LinearWithdrawCapability<TokenT>>(Signer::address_of(signer));
ensures exists<LinearWithdrawCapability<TokenT>>(Signer::address_of(signer));

Function remove_linear_withdraw_capability

Remove LinearWithdrawCapability from signer.

public fun remove_linear_withdraw_capability<TokenT: store>(signer: &signer): Treasury::LinearWithdrawCapability<TokenT>
Implementation 
public fun remove_linear_withdraw_capability<TokenT: store>(signer: &signer): LinearWithdrawCapability<TokenT>
acquires LinearWithdrawCapability {
    move_from<LinearWithdrawCapability<TokenT>>(Signer::address_of(signer))
}
Specification 
aborts_if !exists<LinearWithdrawCapability<TokenT>>(Signer::address_of(signer));
ensures !exists<LinearWithdrawCapability<TokenT>>(Signer::address_of(signer));

Function destroy_linear_withdraw_capability

Destroy LinearWithdrawCapability.

public fun destroy_linear_withdraw_capability<TokenT: store>(cap: Treasury::LinearWithdrawCapability<TokenT>)
Implementation 
public fun destroy_linear_withdraw_capability<TokenT: store>(cap: LinearWithdrawCapability<TokenT>) {
    let LinearWithdrawCapability{ total: _, withdraw: _, start_time: _, period: _ } = cap;
}

Function is_empty_linear_withdraw_capability

public fun is_empty_linear_withdraw_capability<TokenT: store>(cap: &Treasury::LinearWithdrawCapability<TokenT>): bool
Implementation 
public fun is_empty_linear_withdraw_capability<TokenT: store>(cap: &LinearWithdrawCapability<TokenT>): bool {
    cap.total == cap.withdraw
}

Function get_linear_withdraw_capability_total

Get LinearWithdrawCapability total amount

public fun get_linear_withdraw_capability_total<TokenT: store>(cap: &Treasury::LinearWithdrawCapability<TokenT>): u128
Implementation 
public fun get_linear_withdraw_capability_total<TokenT: store>(cap: &LinearWithdrawCapability<TokenT>): u128 {
    cap.total
}

Function get_linear_withdraw_capability_withdraw

Get LinearWithdrawCapability withdraw amount

public fun get_linear_withdraw_capability_withdraw<TokenT: store>(cap: &Treasury::LinearWithdrawCapability<TokenT>): u128
Implementation 
public fun get_linear_withdraw_capability_withdraw<TokenT: store>(cap: &LinearWithdrawCapability<TokenT>): u128 {
    cap.withdraw
}

Function get_linear_withdraw_capability_period

Get LinearWithdrawCapability period in seconds

public fun get_linear_withdraw_capability_period<TokenT: store>(cap: &Treasury::LinearWithdrawCapability<TokenT>): u64
Implementation 
public fun get_linear_withdraw_capability_period<TokenT: store>(cap: &LinearWithdrawCapability<TokenT>): u64 {
    cap.period
}

Function get_linear_withdraw_capability_start_time

Get LinearWithdrawCapability start_time in seconds

public fun get_linear_withdraw_capability_start_time<TokenT: store>(cap: &Treasury::LinearWithdrawCapability<TokenT>): u64
Implementation 
public fun get_linear_withdraw_capability_start_time<TokenT: store>(cap: &LinearWithdrawCapability<TokenT>): u64 {
    cap.start_time
}

Module Specification

pragma verify;
pragma aborts_if_is_strict;


fun spec_balance<TokenType>(): num {
   global<Treasury<TokenType>>(Token::SPEC_TOKEN_TEST_ADDRESS()).balance.value
}
This site is open source. Improve this page.