Skip to content

Latest commit

 

History

History
454 lines (260 loc) · 17.2 KB

TransactionFee.md

File metadata and controls

454 lines (260 loc) · 17.2 KB

Module 0x1::TransactionFee

Functions to initialize, accumulated, and burn transaction fees.

use 0x1::CoreAddresses;
use 0x1::Diem;
use 0x1::DiemTimestamp;
use 0x1::Errors;
use 0x1::Roles;
use 0x1::XDX;
use 0x1::XUS;

Resource TransactionFee

The TransactionFee resource holds a preburn resource for each fiat CoinType that can be collected as a transaction fee.

resource struct TransactionFee<CoinType>
Fields
balance: Diem::Diem<CoinType>
preburn: Diem::Preburn<CoinType>

Constants

A TransactionFee resource is not in the required state

const ETRANSACTION_FEE: u64 = 0;

Function initialize

Called in genesis. Sets up the needed resources to collect transaction fees from the TransactionFee resource with the TreasuryCompliance account.

public fun initialize(tc_account: &signer)
Implementation 
public fun initialize(
    tc_account: &signer,
) {
    DiemTimestamp::assert_genesis();
    Roles::assert_treasury_compliance(tc_account);
    // accept fees in all the currencies
    add_txn_fee_currency<XUS>(tc_account);
}
Specification 
include DiemTimestamp::AbortsIfNotGenesis;
include Roles::AbortsIfNotTreasuryCompliance{account: tc_account};
include AddTxnFeeCurrencyAbortsIf<XUS>;
ensures is_initialized();
ensures spec_transaction_fee<XUS>().balance.value == 0;


schema AddTxnFeeCurrencyAbortsIf<CoinType> {
    include Diem::AbortsIfNoCurrency<CoinType>;
    aborts_if exists<TransactionFee<CoinType>>(CoreAddresses::TREASURY_COMPLIANCE_ADDRESS())
        with Errors::ALREADY_PUBLISHED;
}

Function is_coin_initialized

public fun is_coin_initialized<CoinType>(): bool
Implementation 
public fun is_coin_initialized<CoinType>(): bool {
    exists<TransactionFee<CoinType>>(CoreAddresses::TREASURY_COMPLIANCE_ADDRESS())
}

Function is_initialized

fun is_initialized(): bool
Implementation 
fun is_initialized(): bool {
    is_coin_initialized<XUS>()
}

Function add_txn_fee_currency

Sets up the needed transaction fee state for a given CoinType currency by (1) configuring tc_account to accept CoinType (2) publishing a wrapper of the Preburn<CoinType> resource under tc_account

public fun add_txn_fee_currency<CoinType>(tc_account: &signer)
Implementation 
public fun add_txn_fee_currency<CoinType>(tc_account: &signer) {
    Diem::assert_is_currency<CoinType>();
    assert(
        !is_coin_initialized<CoinType>(),
        Errors::already_published(ETRANSACTION_FEE)
    );
    move_to(
        tc_account,
        TransactionFee<CoinType> {
            balance: Diem::zero(),
            preburn: Diem::create_preburn(tc_account)
        }
    )
}

Function pay_fee

Deposit coin into the transaction fees bucket

public fun pay_fee<CoinType>(coin: Diem::Diem<CoinType>)
Implementation 
public fun pay_fee<CoinType>(coin: Diem<CoinType>) acquires TransactionFee {
    DiemTimestamp::assert_operating();
    assert(is_coin_initialized<CoinType>(), Errors::not_published(ETRANSACTION_FEE));
    let fees = borrow_global_mut<TransactionFee<CoinType>>(
        CoreAddresses::TREASURY_COMPLIANCE_ADDRESS(),
    );
    Diem::deposit(&mut fees.balance, coin)
}
Specification 
include DiemTimestamp::AbortsIfNotOperating;
aborts_if !is_coin_initialized<CoinType>() with Errors::NOT_PUBLISHED;

let fees = spec_transaction_fee<CoinType>().balance;
include Diem::DepositAbortsIf<CoinType>{coin: fees, check: coin};
ensures fees.value == old(fees.value) + coin.value;

Function burn_fees

Preburns the transaction fees collected in the CoinType currency. If the CoinType is XDX, it unpacks the coin and preburns the underlying fiat.

public fun burn_fees<CoinType>(tc_account: &signer)
Implementation 
public fun burn_fees<CoinType>(
    tc_account: &signer,
) acquires TransactionFee {
    DiemTimestamp::assert_operating();
    Roles::assert_treasury_compliance(tc_account);
    assert(is_coin_initialized<CoinType>(), Errors::not_published(ETRANSACTION_FEE));
    let tc_address = CoreAddresses::TREASURY_COMPLIANCE_ADDRESS();
    if (XDX::is_xdx<CoinType>()) {
        // TODO: Once the composition of XDX is determined fill this in to
        // unpack and burn the backing coins of the XDX coin.
        abort Errors::invalid_state(ETRANSACTION_FEE)
    } else {
        // extract fees
        let fees = borrow_global_mut<TransactionFee<CoinType>>(tc_address);
        let coin = Diem::withdraw_all(&mut fees.balance);
        let burn_cap = Diem::remove_burn_capability<CoinType>(tc_account);
        // burn
        Diem::burn_now(
            coin,
            &mut fees.preburn,
            tc_address,
            &burn_cap
        );
        Diem::publish_burn_capability(tc_account, burn_cap);
    }
}
Specification

Must abort if the account does not have the TreasuryCompliance role [H3].

include Roles::AbortsIfNotTreasuryCompliance{account: tc_account};
include DiemTimestamp::AbortsIfNotOperating;
aborts_if !is_coin_initialized<CoinType>() with Errors::NOT_PUBLISHED;
include if (XDX::spec_is_xdx<CoinType>()) BurnFeesXDX else BurnFeesNotXDX<CoinType>;

The correct amount of fees is burnt and subtracted from market cap.

ensures Diem::spec_market_cap<CoinType>()
    == old(Diem::spec_market_cap<CoinType>()) - old(spec_transaction_fee<CoinType>().balance.value);

All the fees is burnt so the balance becomes 0.

ensures spec_transaction_fee<CoinType>().balance.value == 0;

STUB: To be filled in at a later date once the makeup of the XDX has been determined.

Specification of the case where burn type is XDX.

schema BurnFeesXDX {
    tc_account: signer;
    aborts_if true with Errors::INVALID_STATE;
}

Specification of the case where burn type is not XDX.

schema BurnFeesNotXDX<CoinType> {
    tc_account: signer;
}

Must abort if the account does not have BurnCapability [H3].

schema BurnFeesNotXDX<CoinType> {
    include Diem::AbortsIfNoBurnCapability<CoinType>{account: tc_account};
    
    let fees = spec_transaction_fee<CoinType>();
    include Diem::BurnNowAbortsIf<CoinType>{coin: fees.balance, preburn: fees.preburn};
}

tc_account retrieves BurnCapability [H3]. BurnCapability is not transferrable [J3].

schema BurnFeesNotXDX<CoinType> {
    ensures exists<Diem::BurnCapability<CoinType>>(Signer::spec_address_of(tc_account));
}

Module Specification

Initialization

If time has started ticking, then TransactionFee resources have been initialized.

invariant [global] DiemTimestamp::is_operating() ==> is_initialized();

Helper Function

define spec_transaction_fee<CoinType>(): TransactionFee<CoinType> {
   borrow_global<TransactionFee<CoinType>>(CoreAddresses::TREASURY_COMPLIANCE_ADDRESS())
}