transaction_fee - [mainnet]

use 0x1::aptos_account;
use 0x1::aptos_coin;
use 0x1::coin;
use 0x1::error;
use 0x1::event;
use 0x1::features;
use 0x1::fungible_asset;
use 0x1::option;
use 0x1::signer;
use 0x1::system_addresses;

Constants

Gas fees are already being collected and the struct holding information about collected amounts is already published.

const EALREADY_COLLECTING_FEES: u64 = 1;

const EFA_GAS_CHARGING_NOT_ENABLED: u64 = 5;

The burn percentage is out of range [0, 100].

const EINVALID_BURN_PERCENTAGE: u64 = 3;

No longer supported.

const ENO_LONGER_SUPPORTED: u64 = 4;

Structs

`FeeStatement`

Breakdown of fee charge and refund for a transaction. The structure is:

Net charge or refund (not in the statement)
total charge: total_charge_gas_units, matches gas_used in the on-chain TransactionInfo. This is the sum of the sub-items below. Notice that there’s potential precision loss when the conversion between internal and external gas units and between native token and gas units, so it’s possible that the numbers don’t add up exactly. — This number is the final charge, while the break down is merely informational.
gas charge for execution (CPU time): execution_gas_units
gas charge for IO (storage random access): io_gas_units
storage fee charge (storage space): storage_fee_octas, to be included in total_charge_gas_unit, this number is converted to gas units according to the user specified gas_unit_price on the transaction.
storage deletion refund: storage_fee_refund_octas, this is not included in gas_used or total_charge_gas_units, the net charge / refund is calculated by total_charge_gas_units * gas_unit_price - storage_fee_refund_octas.

This is meant to emitted as a module event.

#[event]
struct FeeStatement has drop, store

Fields

total_charge_gas_units: u64: Total gas charge.
execution_gas_units: u64: Execution gas charge.
io_gas_units: u64: IO gas charge.
storage_fee_octas: u64: Storage fee charge.
storage_fee_refund_octas: u64: Storage fee refund.

Resources

`AptosCoinCapabilities`

Stores burn capability to burn the gas fees.

struct AptosCoinCapabilities has key

Fields

burn_cap: coin::BurnCapability<aptos_coin::AptosCoin>

`AptosFABurnCapabilities`

Stores burn capability to burn the gas fees.

struct AptosFABurnCapabilities has key

Fields

burn_ref: fungible_asset::BurnRef

`AptosCoinMintCapability`

Stores mint capability to mint the refunds.

struct AptosCoinMintCapability has key

Fields

mint_cap: coin::MintCapability<aptos_coin::AptosCoin>

`CollectedFeesPerBlock`

DEPRECATED: Stores information about the block proposer and the amount of fees collected when executing the block.

#[deprecated]
struct CollectedFeesPerBlock has key

Fields

amount: coin::AggregatableCoin<aptos_coin::AptosCoin>
proposer: option::Option<address>
burn_percentage: u8

Functions

`burn_fee`

Burn transaction fees in epilogue.

public(friend) fun burn_fee(account: address, fee: u64)

Implementation

public(friend) fun burn_fee(account: address, fee: u64) acquires AptosFABurnCapabilities, AptosCoinCapabilities {
    if (exists<AptosFABurnCapabilities>(@aptos_framework)) {
        let burn_ref = &borrow_global<AptosFABurnCapabilities>(@aptos_framework).burn_ref;
        aptos_account::burn_from_fungible_store_for_gas(burn_ref, account, fee);
    } else {
        let burn_cap = &borrow_global<AptosCoinCapabilities>(@aptos_framework).burn_cap;
        if (features::operations_default_to_fa_apt_store_enabled()) {
            let (burn_ref, burn_receipt) = coin::get_paired_burn_ref(burn_cap);
            aptos_account::burn_from_fungible_store_for_gas(&burn_ref, account, fee);
            coin::return_paired_burn_ref(burn_ref, burn_receipt);
        } else {
            coin::burn_from_for_gas<AptosCoin>(
                account,
                fee,
                burn_cap,
            );
        };
    };
}

`mint_and_refund`

Mint refund in epilogue.

public(friend) fun mint_and_refund(account: address, refund: u64)

Implementation

public(friend) fun mint_and_refund(account: address, refund: u64) acquires AptosCoinMintCapability {
    let mint_cap = &borrow_global<AptosCoinMintCapability>(@aptos_framework).mint_cap;
    let refund_coin = coin::mint(refund, mint_cap);
    coin::deposit_for_gas_fee(account, refund_coin);
}

`store_aptos_coin_burn_cap`

Only called during genesis.

public(friend) fun store_aptos_coin_burn_cap(aptos_framework: &signer, burn_cap: coin::BurnCapability<aptos_coin::AptosCoin>)

Implementation

public(friend) fun store_aptos_coin_burn_cap(aptos_framework: &signer, burn_cap: BurnCapability<AptosCoin>) {
    system_addresses::assert_aptos_framework(aptos_framework);

    if (features::operations_default_to_fa_apt_store_enabled()) {
        let burn_ref = coin::convert_and_take_paired_burn_ref(burn_cap);
        move_to(aptos_framework, AptosFABurnCapabilities { burn_ref });
    } else {
        move_to(aptos_framework, AptosCoinCapabilities { burn_cap })
    }
}

`convert_to_aptos_fa_burn_ref`

public entry fun convert_to_aptos_fa_burn_ref(aptos_framework: &signer)

Implementation

public entry fun convert_to_aptos_fa_burn_ref(aptos_framework: &signer) acquires AptosCoinCapabilities {
    assert!(features::operations_default_to_fa_apt_store_enabled(), EFA_GAS_CHARGING_NOT_ENABLED);
    system_addresses::assert_aptos_framework(aptos_framework);
    let AptosCoinCapabilities {
        burn_cap,
    } = move_from<AptosCoinCapabilities>(signer::address_of(aptos_framework));
    let burn_ref = coin::convert_and_take_paired_burn_ref(burn_cap);
    move_to(aptos_framework, AptosFABurnCapabilities { burn_ref });
}

`store_aptos_coin_mint_cap`

Only called during genesis.

public(friend) fun store_aptos_coin_mint_cap(aptos_framework: &signer, mint_cap: coin::MintCapability<aptos_coin::AptosCoin>)

Implementation

public(friend) fun store_aptos_coin_mint_cap(aptos_framework: &signer, mint_cap: MintCapability<AptosCoin>) {
    system_addresses::assert_aptos_framework(aptos_framework);
    move_to(aptos_framework, AptosCoinMintCapability { mint_cap })
}

`emit_fee_statement`

fun emit_fee_statement(fee_statement: transaction_fee::FeeStatement)

Implementation

fun emit_fee_statement(fee_statement: FeeStatement) {
    event::emit(fee_statement)
}

`initialize_fee_collection_and_distribution`

DEPRECATED

#[deprecated]
public fun initialize_fee_collection_and_distribution(_aptos_framework: &signer, _burn_percentage: u8)

Implementation

public fun initialize_fee_collection_and_distribution(_aptos_framework: &signer, _burn_percentage: u8) {
    abort error::not_implemented(ENO_LONGER_SUPPORTED)
}

`upgrade_burn_percentage`

DEPRECATED

#[deprecated]
public fun upgrade_burn_percentage(_aptos_framework: &signer, _new_burn_percentage: u8)

Implementation

public fun upgrade_burn_percentage(
    _aptos_framework: &signer,
    _new_burn_percentage: u8
) {
    abort error::not_implemented(ENO_LONGER_SUPPORTED)
}

`initialize_storage_refund`

#[deprecated]
public fun initialize_storage_refund(_: &signer)

Implementation

public fun initialize_storage_refund(_: &signer) {
    abort error::not_implemented(ENO_LONGER_SUPPORTED)
}

Specification

High-level Requirements

No.	Requirement	Criticality	Implementation	Enforcement
1	Given the blockchain is in an operating state, it guarantees that the Aptos framework signer may burn Aptos coins.	Critical	The AptosCoinCapabilities structure is defined in this module and it stores burn capability to burn the gas fees.	Formally Verified via module.
2	The initialization function may only be called once.	Medium	The initialize_fee_collection_and_distribution function ensures CollectedFeesPerBlock does not already exist.	Formally verified via initialize_fee_collection_and_distribution.
3	Only the admin address is authorized to call the initialization function.	Critical	The initialize_fee_collection_and_distribution function ensures only the Aptos framework address calls it.	Formally verified via initialize_fee_collection_and_distribution.
4	The percentage of the burnt collected fee is always a value from 0 to 100.	Medium	During the initialization of CollectedFeesPerBlock in Initialize_fee_collection_and_distribution, and while upgrading burn percentage, it asserts that burn_percentage is within the specified limits.	Formally verified via CollectedFeesPerBlock.
5	Prior to upgrading the burn percentage, it must process all the fees collected up to that point.	Critical	The upgrade_burn_percentage function ensures process_collected_fees function is called before updating the burn percentage.	Formally verified in ProcessCollectedFeesRequiresAndEnsures.
6	The presence of the resource, indicating collected fees per block under the Aptos framework account, is a prerequisite for the successful execution of the following functionalities: Upgrading burn percentage. Registering a block proposer. Processing collected fees.	Low	The functions: upgrade_burn_percentage, register_proposer_for_fee_collection, and process_collected_fees all ensure that the CollectedFeesPerBlock resource exists under aptos_framework by calling the is_fees_collection_enabled method, which returns a boolean value confirming if the resource exists or not.	Formally verified via register_proposer_for_fee_collection, process_collected_fees, and upgrade_burn_percentage.

Module-level Specification

pragma verify = false;
pragma aborts_if_is_strict;
// This enforces high-level requirement 1:
invariant [suspendable] chain_status::is_operating() ==> exists<AptosCoinCapabilities>(@aptos_framework) || exists<AptosFABurnCapabilities>(@aptos_framework);

`CollectedFeesPerBlock`

#[deprecated]
struct CollectedFeesPerBlock has key

amount: coin::AggregatableCoin<aptos_coin::AptosCoin>
proposer: option::Option<address>
burn_percentage: u8

// This enforces high-level requirement 4:
invariant burn_percentage <= 100;

`burn_fee`

public(friend) fun burn_fee(account: address, fee: u64)

AptosCoinCapabilities should be exists.

pragma verify = false;
aborts_if !exists<AptosCoinCapabilities>(@aptos_framework);
let account_addr = account;
let amount = fee;
let aptos_addr = type_info::type_of<AptosCoin>().account_address;
let coin_store = global<CoinStore<AptosCoin>>(account_addr);
let post post_coin_store = global<CoinStore<AptosCoin>>(account_addr);
aborts_if amount != 0 && !(exists<CoinInfo<AptosCoin>>(aptos_addr)
    && exists<CoinStore<AptosCoin>>(account_addr));
aborts_if coin_store.coin.value < amount;
let maybe_supply = global<CoinInfo<AptosCoin>>(aptos_addr).supply;
let supply_aggr = option::spec_borrow(maybe_supply);
let value = optional_aggregator::optional_aggregator_value(supply_aggr);
let post post_maybe_supply = global<CoinInfo<AptosCoin>>(aptos_addr).supply;
let post post_supply = option::spec_borrow(post_maybe_supply);
let post post_value = optional_aggregator::optional_aggregator_value(post_supply);
aborts_if option::spec_is_some(maybe_supply) && value < amount;
ensures post_coin_store.coin.value == coin_store.coin.value - amount;
ensures if (option::spec_is_some(maybe_supply)) {
    post_value == value - amount
} else {
    option::spec_is_none(post_maybe_supply)
};
ensures coin::supply<AptosCoin> == old(coin::supply<AptosCoin>) - amount;

`mint_and_refund`

public(friend) fun mint_and_refund(account: address, refund: u64)

pragma verify = false;
let aptos_addr = type_info::type_of<AptosCoin>().account_address;
aborts_if (refund != 0) && !exists<CoinInfo<AptosCoin>>(aptos_addr);
include coin::CoinAddAbortsIf<AptosCoin> { amount: refund };
aborts_if !exists<CoinStore<AptosCoin>>(account);
aborts_if !exists<AptosCoinMintCapability>(@aptos_framework);
let supply = coin::supply<AptosCoin>;
let post post_supply = coin::supply<AptosCoin>;
aborts_if [abstract] supply + refund > MAX_U128;
ensures post_supply == supply + refund;

`store_aptos_coin_burn_cap`

public(friend) fun store_aptos_coin_burn_cap(aptos_framework: &signer, burn_cap: coin::BurnCapability<aptos_coin::AptosCoin>)

Ensure caller is admin. Aborts if AptosCoinCapabilities already exists.

pragma verify = false;
let addr = signer::address_of(aptos_framework);
aborts_if !system_addresses::is_aptos_framework_address(addr);
aborts_if exists<AptosFABurnCapabilities>(addr);
aborts_if exists<AptosCoinCapabilities>(addr);
ensures exists<AptosFABurnCapabilities>(addr) || exists<AptosCoinCapabilities>(addr);

`store_aptos_coin_mint_cap`

public(friend) fun store_aptos_coin_mint_cap(aptos_framework: &signer, mint_cap: coin::MintCapability<aptos_coin::AptosCoin>)

Ensure caller is admin. Aborts if AptosCoinMintCapability already exists.

let addr = signer::address_of(aptos_framework);
aborts_if !system_addresses::is_aptos_framework_address(addr);
aborts_if exists<AptosCoinMintCapability>(addr);
ensures exists<AptosCoinMintCapability>(addr);

`emit_fee_statement`

fun emit_fee_statement(fee_statement: transaction_fee::FeeStatement)

Aborts if module event feature is not enabled.

`initialize_fee_collection_and_distribution`

#[deprecated]
public fun initialize_fee_collection_and_distribution(_aptos_framework: &signer, _burn_percentage: u8)

`initialize_storage_refund`

#[deprecated]
public fun initialize_storage_refund(_: &signer)

Historical. Aborts.

aborts_if true;