Skip to content
Aptos Docs

transaction_validation - [mainnet]

use 0x1::account;
use 0x1::account_abstraction;
use 0x1::aptos_account;
use 0x1::aptos_coin;
use 0x1::chain_id;
use 0x1::coin;
use 0x1::create_signer;
use 0x1::error;
use 0x1::features;
use 0x1::nonce_validation;
use 0x1::option;
use 0x1::permissioned_signer;
use 0x1::signer;
use 0x1::system_addresses;
use 0x1::timestamp;
use 0x1::transaction_fee;
use 0x1::vector;

Enum ReplayProtector

enum ReplayProtector
Variants
Nonce
Fields
0: u64
SequenceNumber
Fields
0: u64

Constants

MSB is used to indicate a gas payer tx

const MAX_U64: u128 = 18446744073709551615;

Transaction exceeded its allocated max gas

const EOUT_OF_GAS: u64 = 6;
const MAX_EXPIRATION_TIME_SECONDS_FOR_ORDERLESS_TXNS: u64 = 65;
const PROLOGUE_EACCOUNT_DOES_NOT_EXIST: u64 = 1004;
const PROLOGUE_EBAD_CHAIN_ID: u64 = 1007;
const PROLOGUE_ECANT_PAY_GAS_DEPOSIT: u64 = 1005;
const PROLOGUE_EFEE_PAYER_NOT_ENABLED: u64 = 1010;

Prologue errors. These are separated out from the other errors in this module since they are mapped separately to major VM statuses, and are important to the semantics of the system.

const PROLOGUE_EINVALID_ACCOUNT_AUTH_KEY: u64 = 1001;
const PROLOGUE_ENONCE_ALREADY_USED: u64 = 1012;
const PROLOGUE_ESECONDARY_KEYS_ADDRESSES_COUNT_MISMATCH: u64 = 1009;
const PROLOGUE_ESEQUENCE_NUMBER_TOO_BIG: u64 = 1008;
const PROLOGUE_ESEQUENCE_NUMBER_TOO_NEW: u64 = 1003;
const PROLOGUE_ESEQUENCE_NUMBER_TOO_OLD: u64 = 1002;
const PROLOGUE_ETRANSACTION_EXPIRATION_TOO_FAR_IN_FUTURE: u64 = 1013;
const PROLOGUE_ETRANSACTION_EXPIRED: u64 = 1006;
const PROLOGUE_PERMISSIONED_GAS_LIMIT_INSUFFICIENT: u64 = 1011;

Structs

GasPermission

struct GasPermission has copy, drop, store
Fields
dummy_field: bool

Resources

TransactionValidation

This holds information that will be picked up by the VM to call the correct chain-specific prologue and epilogue functions

struct TransactionValidation has key
Fields
module_addr: address
module_name: vector<u8>
script_prologue_name: vector<u8>
module_prologue_name: vector<u8>
multi_agent_prologue_name: vector<u8>
user_epilogue_name: vector<u8>

Functions

grant_gas_permission

Permission management

Master signer grant permissioned signer ability to consume a given amount of gas in octas.

public fun grant_gas_permission(master: &signer, permissioned: &signer, gas_amount: u64)
Implementation 
public fun grant_gas_permission(
    master: &signer,
    permissioned: &signer,
    gas_amount: u64
) {
    permissioned_signer::authorize_increase(
        master,
        permissioned,
        (gas_amount as u256),
        GasPermission {}
    )
}

revoke_gas_permission

Removing permissions from permissioned signer.

public fun revoke_gas_permission(permissioned: &signer)
Implementation 
public fun revoke_gas_permission(permissioned: &signer) {
    permissioned_signer::revoke_permission(permissioned, GasPermission {})
}

initialize

Only called during genesis to initialize system resources for this module.

public(friend) fun initialize(aptos_framework: &signer, script_prologue_name: vector<u8>, module_prologue_name: vector<u8>, multi_agent_prologue_name: vector<u8>, user_epilogue_name: vector<u8>)
Implementation 
public(friend) fun initialize(
    aptos_framework: &signer,
    script_prologue_name: vector<u8>,
    // module_prologue_name is deprecated and not used.
    module_prologue_name: vector<u8>,
    multi_agent_prologue_name: vector<u8>,
    user_epilogue_name: vector<u8>,
) {
    system_addresses::assert_aptos_framework(aptos_framework);


    move_to(aptos_framework, TransactionValidation {
        module_addr: @aptos_framework,
        module_name: b"transaction_validation",
        script_prologue_name,
        // module_prologue_name is deprecated and not used.
        module_prologue_name,
        multi_agent_prologue_name,
        user_epilogue_name,
    });
}

allow_missing_txn_authentication_key

fun allow_missing_txn_authentication_key(transaction_sender: address): bool
Implementation 
inline fun allow_missing_txn_authentication_key(transaction_sender: address): bool {
    // aa verifies authentication itself
    features::is_derivable_account_abstraction_enabled()
        || (features::is_account_abstraction_enabled() && account_abstraction::using_dispatchable_authenticator(transaction_sender))
}

prologue_common

fun prologue_common(sender: &signer, gas_payer: &signer, replay_protector: transaction_validation::ReplayProtector, txn_authentication_key: option::Option<vector<u8>>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, is_simulation: bool)
Implementation 
fun prologue_common(
    sender: &signer,
    gas_payer: &signer,
    replay_protector: ReplayProtector,
    txn_authentication_key: Option<vector<u8>>,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    txn_expiration_time: u64,
    chain_id: u8,
    is_simulation: bool,
) {
    let sender_address = signer::address_of(sender);
    let gas_payer_address = signer::address_of(gas_payer);
    assert!(
        timestamp::now_seconds() < txn_expiration_time,
        error::invalid_argument(PROLOGUE_ETRANSACTION_EXPIRED),
    );
    assert!(chain_id::get() == chain_id, error::invalid_argument(PROLOGUE_EBAD_CHAIN_ID));


    // TODO[Orderless]: Here, we are maintaining the same order of validation steps as before orderless txns were introduced.
    // Ideally, do the replay protection check in the end after the authentication key check and gas payment checks.


    // Check if the authentication key is valid
    if (!skip_auth_key_check(is_simulation, &txn_authentication_key)) {
        if (option::is_some(&txn_authentication_key)) {
            if (
                sender_address == gas_payer_address ||
                account::exists_at(sender_address) ||
                !features::sponsored_automatic_account_creation_enabled()
            ) {
                assert!(
                    txn_authentication_key == option::some(account::get_authentication_key(sender_address)),
                    error::invalid_argument(PROLOGUE_EINVALID_ACCOUNT_AUTH_KEY),
                );
            };
        } else {
            assert!(
                allow_missing_txn_authentication_key(sender_address),
                error::invalid_argument(PROLOGUE_EINVALID_ACCOUNT_AUTH_KEY)
            );
        };
    };


    // Check for replay protection
    match (replay_protector) {
        SequenceNumber(txn_sequence_number) => {
            check_for_replay_protection_regular_txn(
                sender_address,
                gas_payer_address,
                txn_sequence_number,
            );
        },
        Nonce(nonce) => {
            check_for_replay_protection_orderless_txn(
                sender_address,
                nonce,
                txn_expiration_time,
            );
        }
    };


    // Check if the gas payer has enough balance to pay for the transaction
    let max_transaction_fee = txn_gas_price * txn_max_gas_units;
    if (!skip_gas_payment(
        is_simulation,
        gas_payer_address
    )) {
        assert!(
            permissioned_signer::check_permission_capacity_above(
                gas_payer,
                (max_transaction_fee as u256),
                GasPermission {}
            ),
            error::permission_denied(PROLOGUE_PERMISSIONED_GAS_LIMIT_INSUFFICIENT)
        );
        if (features::operations_default_to_fa_apt_store_enabled()) {
            assert!(
                aptos_account::is_fungible_balance_at_least(gas_payer_address, max_transaction_fee),
                error::invalid_argument(PROLOGUE_ECANT_PAY_GAS_DEPOSIT)
            );
        } else {
            assert!(
                coin::is_balance_at_least<AptosCoin>(gas_payer_address, max_transaction_fee),
                error::invalid_argument(PROLOGUE_ECANT_PAY_GAS_DEPOSIT)
            );
        }
    };
}

check_for_replay_protection_regular_txn

fun check_for_replay_protection_regular_txn(sender_address: address, gas_payer_address: address, txn_sequence_number: u64)
Implementation 
fun check_for_replay_protection_regular_txn(
    sender_address: address,
    gas_payer_address: address,
    txn_sequence_number: u64,
) {
    if (
        sender_address == gas_payer_address
            || account::exists_at(sender_address)
            || !features::sponsored_automatic_account_creation_enabled()
            || txn_sequence_number > 0
    ) {
        assert!(account::exists_at(sender_address), error::invalid_argument(PROLOGUE_EACCOUNT_DOES_NOT_EXIST));
        let account_sequence_number = account::get_sequence_number(sender_address);
        assert!(
            txn_sequence_number < (1u64 << 63),
            error::out_of_range(PROLOGUE_ESEQUENCE_NUMBER_TOO_BIG)
        );


        assert!(
            txn_sequence_number >= account_sequence_number,
            error::invalid_argument(PROLOGUE_ESEQUENCE_NUMBER_TOO_OLD)
        );


        assert!(
            txn_sequence_number == account_sequence_number,
            error::invalid_argument(PROLOGUE_ESEQUENCE_NUMBER_TOO_NEW)
        );
    } else {
        // In this case, the transaction is sponsored and the account does not exist, so ensure
        // the default values match.
        assert!(
            txn_sequence_number == 0,
            error::invalid_argument(PROLOGUE_ESEQUENCE_NUMBER_TOO_NEW)
        );
    };
}

check_for_replay_protection_orderless_txn

fun check_for_replay_protection_orderless_txn(sender: address, nonce: u64, txn_expiration_time: u64)
Implementation 
fun check_for_replay_protection_orderless_txn(
    sender: address,
    nonce: u64,
    txn_expiration_time: u64,
) {
    // prologue_common already checks that the current_time > txn_expiration_time
    assert!(
        txn_expiration_time <= timestamp::now_seconds() + MAX_EXPIRATION_TIME_SECONDS_FOR_ORDERLESS_TXNS,
        error::invalid_argument(PROLOGUE_ETRANSACTION_EXPIRATION_TOO_FAR_IN_FUTURE),
    );
    assert!(nonce_validation::check_and_insert_nonce(sender, nonce, txn_expiration_time), error::invalid_argument(PROLOGUE_ENONCE_ALREADY_USED));
}

script_prologue

fun script_prologue(sender: signer, txn_sequence_number: u64, txn_public_key: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, _script_hash: vector<u8>)
Implementation 
fun script_prologue(
    sender: signer,
    txn_sequence_number: u64,
    txn_public_key: vector<u8>,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    txn_expiration_time: u64,
    chain_id: u8,
    _script_hash: vector<u8>,
) {
    // prologue_common with is_simulation set to false behaves identically to the original script_prologue function.
    prologue_common(
        &sender,
        &sender,
        ReplayProtector::SequenceNumber(txn_sequence_number),
        option::some(txn_public_key),
        txn_gas_price,
        txn_max_gas_units,
        txn_expiration_time,
        chain_id,
        false,
    )
}

script_prologue_extended

fun script_prologue_extended(sender: signer, txn_sequence_number: u64, txn_public_key: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, _script_hash: vector<u8>, is_simulation: bool)
Implementation 
fun script_prologue_extended(
    sender: signer,
    txn_sequence_number: u64,
    txn_public_key: vector<u8>,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    txn_expiration_time: u64,
    chain_id: u8,
    _script_hash: vector<u8>,
    is_simulation: bool,
) {
    prologue_common(
        &sender,
        &sender,
        ReplayProtector::SequenceNumber(txn_sequence_number),
        option::some(txn_public_key),
        txn_gas_price,
        txn_max_gas_units,
        txn_expiration_time,
        chain_id,
        is_simulation,
    )
}

multi_agent_script_prologue

fun multi_agent_script_prologue(sender: signer, txn_sequence_number: u64, txn_sender_public_key: vector<u8>, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<vector<u8>>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8)
Implementation 
fun multi_agent_script_prologue(
    sender: signer,
    txn_sequence_number: u64,
    txn_sender_public_key: vector<u8>,
    secondary_signer_addresses: vector<address>,
    secondary_signer_public_key_hashes: vector<vector<u8>>,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    txn_expiration_time: u64,
    chain_id: u8,
) {
    // prologue_common and multi_agent_common_prologue with is_simulation set to false behaves identically to the
    // original multi_agent_script_prologue function.
    prologue_common(
        &sender,
        &sender,
        ReplayProtector::SequenceNumber(txn_sequence_number),
        option::some(txn_sender_public_key),
        txn_gas_price,
        txn_max_gas_units,
        txn_expiration_time,
        chain_id,
        false,
    );
    multi_agent_common_prologue(
        secondary_signer_addresses,
        vector::map(secondary_signer_public_key_hashes, |x| option::some(x)),
        false
    );
}

multi_agent_script_prologue_extended

fun multi_agent_script_prologue_extended(sender: signer, txn_sequence_number: u64, txn_sender_public_key: vector<u8>, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<vector<u8>>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, is_simulation: bool)
Implementation 
fun multi_agent_script_prologue_extended(
    sender: signer,
    txn_sequence_number: u64,
    txn_sender_public_key: vector<u8>,
    secondary_signer_addresses: vector<address>,
    secondary_signer_public_key_hashes: vector<vector<u8>>,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    txn_expiration_time: u64,
    chain_id: u8,
    is_simulation: bool,
) {
    prologue_common(
        &sender,
        &sender,
        ReplayProtector::SequenceNumber(txn_sequence_number),
        option::some(txn_sender_public_key),
        txn_gas_price,
        txn_max_gas_units,
        txn_expiration_time,
        chain_id,
        is_simulation,
    );
    multi_agent_common_prologue(
        secondary_signer_addresses,
        vector::map(secondary_signer_public_key_hashes, |x| option::some(x)),
        is_simulation
    );
}

multi_agent_common_prologue

fun multi_agent_common_prologue(secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<option::Option<vector<u8>>>, is_simulation: bool)
Implementation 
fun multi_agent_common_prologue(
    secondary_signer_addresses: vector<address>,
    secondary_signer_public_key_hashes: vector<Option<vector<u8>>>,
    is_simulation: bool,
) {
    let num_secondary_signers = vector::length(&secondary_signer_addresses);
    assert!(
        vector::length(&secondary_signer_public_key_hashes) == num_secondary_signers,
        error::invalid_argument(PROLOGUE_ESECONDARY_KEYS_ADDRESSES_COUNT_MISMATCH),
    );


    let i = 0;
    while ({
        // spec {
        //     invariant i <= num_secondary_signers;
        //     invariant forall j in 0..i:
        //         account::exists_at(secondary_signer_addresses[j]);
        //     invariant forall j in 0..i:
        //         secondary_signer_public_key_hashes[j] == account::get_authentication_key(secondary_signer_addresses[j]) ||
        //             (features::spec_simulation_enhancement_enabled() && is_simulation && vector::is_empty(secondary_signer_public_key_hashes[j]));
        //         account::account_resource_exists_at(secondary_signer_addresses[j])
        //         && secondary_signer_public_key_hashes[j]
        //             == account::get_authentication_key(secondary_signer_addresses[j])
        //             || features::account_abstraction_enabled() && account_abstraction::using_native_authenticator(
        //             secondary_signer_addresses[j]
        //         ) && option::spec_some(secondary_signer_public_key_hashes[j]) == account_abstraction::native_authenticator(
        //         account::exists_at(secondary_signer_addresses[j])
        //         && secondary_signer_public_key_hashes[j]
        //             == account::spec_get_authentication_key(secondary_signer_addresses[j])
        //             || features::spec_account_abstraction_enabled() && account_abstraction::using_native_authenticator(
        //             secondary_signer_addresses[j]
        //         ) && option::spec_some(
        //             secondary_signer_public_key_hashes[j]
        //         ) == account_abstraction::spec_native_authenticator(
        //             secondary_signer_addresses[j]
        //         );
        // };
        (i < num_secondary_signers)
    }) {
        let secondary_address = *vector::borrow(&secondary_signer_addresses, i);
        assert!(account::exists_at(secondary_address), error::invalid_argument(PROLOGUE_EACCOUNT_DOES_NOT_EXIST));
        let signer_public_key_hash = *vector::borrow(&secondary_signer_public_key_hashes, i);
        if (!skip_auth_key_check(is_simulation, &signer_public_key_hash)) {
            if (option::is_some(&signer_public_key_hash)) {
                assert!(
                    signer_public_key_hash == option::some(account::get_authentication_key(secondary_address)),
                    error::invalid_argument(PROLOGUE_EINVALID_ACCOUNT_AUTH_KEY)
                );
            } else {
                assert!(
                    allow_missing_txn_authentication_key(secondary_address),
                    error::invalid_argument(PROLOGUE_EINVALID_ACCOUNT_AUTH_KEY)
                )
            };
        };


        i = i + 1;
    }
}

fee_payer_script_prologue

fun fee_payer_script_prologue(sender: signer, txn_sequence_number: u64, txn_sender_public_key: vector<u8>, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<vector<u8>>, fee_payer_address: address, fee_payer_public_key_hash: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8)
Implementation 
fun fee_payer_script_prologue(
    sender: signer,
    txn_sequence_number: u64,
    txn_sender_public_key: vector<u8>,
    secondary_signer_addresses: vector<address>,
    secondary_signer_public_key_hashes: vector<vector<u8>>,
    fee_payer_address: address,
    fee_payer_public_key_hash: vector<u8>,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    txn_expiration_time: u64,
    chain_id: u8,
) {
    assert!(features::fee_payer_enabled(), error::invalid_state(PROLOGUE_EFEE_PAYER_NOT_ENABLED));
    // prologue_common and multi_agent_common_prologue with is_simulation set to false behaves identically to the
    // original fee_payer_script_prologue function.
    prologue_common(
        &sender,
        &create_signer::create_signer(fee_payer_address),
        ReplayProtector::SequenceNumber(txn_sequence_number),
        option::some(txn_sender_public_key),
        txn_gas_price,
        txn_max_gas_units,
        txn_expiration_time,
        chain_id,
        false,
    );
    multi_agent_common_prologue(
        secondary_signer_addresses,
        vector::map(secondary_signer_public_key_hashes, |x| option::some(x)),
        false
    );
    assert!(
        fee_payer_public_key_hash == account::get_authentication_key(fee_payer_address),
        error::invalid_argument(PROLOGUE_EINVALID_ACCOUNT_AUTH_KEY),
    );
}

fee_payer_script_prologue_extended

fun fee_payer_script_prologue_extended(sender: signer, txn_sequence_number: u64, txn_sender_public_key: vector<u8>, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<vector<u8>>, fee_payer_address: address, fee_payer_public_key_hash: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, is_simulation: bool)
Implementation 
fun fee_payer_script_prologue_extended(
    sender: signer,
    txn_sequence_number: u64,
    txn_sender_public_key: vector<u8>,
    secondary_signer_addresses: vector<address>,
    secondary_signer_public_key_hashes: vector<vector<u8>>,
    fee_payer_address: address,
    fee_payer_public_key_hash: vector<u8>,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    txn_expiration_time: u64,
    chain_id: u8,
    is_simulation: bool,
) {
    assert!(features::fee_payer_enabled(), error::invalid_state(PROLOGUE_EFEE_PAYER_NOT_ENABLED));
    prologue_common(
        &sender,
        &create_signer::create_signer(fee_payer_address),
        ReplayProtector::SequenceNumber(txn_sequence_number),
        option::some(txn_sender_public_key),
        txn_gas_price,
        txn_max_gas_units,
        txn_expiration_time,
        chain_id,
        is_simulation,
    );
    multi_agent_common_prologue(
        secondary_signer_addresses,
        vector::map(secondary_signer_public_key_hashes, |x| option::some(x)),
        is_simulation
    );
    if (!skip_auth_key_check(is_simulation, &option::some(fee_payer_public_key_hash))) {
            assert!(
                fee_payer_public_key_hash == account::get_authentication_key(fee_payer_address),
                error::invalid_argument(PROLOGUE_EINVALID_ACCOUNT_AUTH_KEY),
            )
    }
}

epilogue

Epilogue function is run after a transaction is successfully executed. Called by the Adapter

fun epilogue(account: signer, storage_fee_refunded: u64, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64)
Implementation 
fun epilogue(
    account: signer,
    storage_fee_refunded: u64,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    gas_units_remaining: u64,
) {
    let addr = signer::address_of(&account);
    epilogue_gas_payer(
        account,
        addr,
        storage_fee_refunded,
        txn_gas_price,
        txn_max_gas_units,
        gas_units_remaining
    );
}

epilogue_extended

fun epilogue_extended(account: signer, storage_fee_refunded: u64, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64, is_simulation: bool)
Implementation 
fun epilogue_extended(
    account: signer,
    storage_fee_refunded: u64,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    gas_units_remaining: u64,
    is_simulation: bool,
) {
    let addr = signer::address_of(&account);
    epilogue_gas_payer_extended(
        account,
        addr,
        storage_fee_refunded,
        txn_gas_price,
        txn_max_gas_units,
        gas_units_remaining,
        is_simulation
    );
}

epilogue_gas_payer

Epilogue function with explicit gas payer specified, is run after a transaction is successfully executed. Called by the Adapter

fun epilogue_gas_payer(account: signer, gas_payer: address, storage_fee_refunded: u64, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64)
Implementation 
fun epilogue_gas_payer(
    account: signer,
    gas_payer: address,
    storage_fee_refunded: u64,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    gas_units_remaining: u64
) {
    // epilogue_gas_payer_extended with is_simulation set to false behaves identically to the original
    // epilogue_gas_payer function.
    epilogue_gas_payer_extended(
        account,
        gas_payer,
        storage_fee_refunded,
        txn_gas_price,
        txn_max_gas_units,
        gas_units_remaining,
        false,
    );
}

epilogue_gas_payer_extended

fun epilogue_gas_payer_extended(account: signer, gas_payer: address, storage_fee_refunded: u64, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64, is_simulation: bool)
Implementation 
fun epilogue_gas_payer_extended(
    account: signer,
    gas_payer: address,
    storage_fee_refunded: u64,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    gas_units_remaining: u64,
    is_simulation: bool,
) {
    assert!(txn_max_gas_units >= gas_units_remaining, error::invalid_argument(EOUT_OF_GAS));
    let gas_used = txn_max_gas_units - gas_units_remaining;


    assert!(
        (txn_gas_price as u128) * (gas_used as u128) <= MAX_U64,
        error::out_of_range(EOUT_OF_GAS)
    );
    let transaction_fee_amount = txn_gas_price * gas_used;


    // it's important to maintain the error code consistent with vm
    // to do failed transaction cleanup.
    if (!skip_gas_payment(is_simulation, gas_payer)) {
        if (features::operations_default_to_fa_apt_store_enabled()) {
            assert!(
                aptos_account::is_fungible_balance_at_least(gas_payer, transaction_fee_amount),
                error::out_of_range(PROLOGUE_ECANT_PAY_GAS_DEPOSIT),
            );
        } else {
            assert!(
                coin::is_balance_at_least<AptosCoin>(gas_payer, transaction_fee_amount),
                error::out_of_range(PROLOGUE_ECANT_PAY_GAS_DEPOSIT),
            );
        };


        if (transaction_fee_amount > storage_fee_refunded) {
            let burn_amount = transaction_fee_amount - storage_fee_refunded;
            transaction_fee::burn_fee(gas_payer, burn_amount);
        } else if (transaction_fee_amount < storage_fee_refunded) {
            let mint_amount = storage_fee_refunded - transaction_fee_amount;
            transaction_fee::mint_and_refund(gas_payer, mint_amount);
        };
    };


    // Increment sequence number
    let addr = signer::address_of(&account);
    account::increment_sequence_number(addr);
}

skip_auth_key_check

fun skip_auth_key_check(is_simulation: bool, auth_key: &option::Option<vector<u8>>): bool
Implementation 
inline fun skip_auth_key_check(is_simulation: bool, auth_key: &Option<vector<u8>>): bool {
    is_simulation && (option::is_none(auth_key) || vector::is_empty(option::borrow(auth_key)))
}

skip_gas_payment

fun skip_gas_payment(is_simulation: bool, gas_payer: address): bool
Implementation 
inline fun skip_gas_payment(is_simulation: bool, gas_payer: address): bool {
    is_simulation && gas_payer == @0x0
}

unified_prologue

new set of functions

fun unified_prologue(sender: signer, txn_sender_public_key: option::Option<vector<u8>>, txn_sequence_number: u64, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<option::Option<vector<u8>>>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, is_simulation: bool)
Implementation 
fun unified_prologue(
    sender: signer,
    // None means no need to check, i.e. either AA (where it is already checked) or simulation
    txn_sender_public_key: Option<vector<u8>>,
    txn_sequence_number: u64,
    secondary_signer_addresses: vector<address>,
    secondary_signer_public_key_hashes: vector<Option<vector<u8>>>,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    txn_expiration_time: u64,
    chain_id: u8,
    is_simulation: bool,
) {
    unified_prologue_v2(
        sender,
        txn_sender_public_key,
        ReplayProtector::SequenceNumber(txn_sequence_number),
        secondary_signer_addresses,
        secondary_signer_public_key_hashes,
        txn_gas_price,
        txn_max_gas_units,
        txn_expiration_time,
        chain_id,
        is_simulation,


    )
}

unified_prologue_fee_payer

If there is no fee_payer, fee_payer = sender

fun unified_prologue_fee_payer(sender: signer, fee_payer: signer, txn_sender_public_key: option::Option<vector<u8>>, fee_payer_public_key_hash: option::Option<vector<u8>>, txn_sequence_number: u64, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<option::Option<vector<u8>>>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, is_simulation: bool)
Implementation 
fun unified_prologue_fee_payer(
    sender: signer,
    fee_payer: signer,
    // None means no need to check, i.e. either AA (where it is already checked) or simulation
    txn_sender_public_key: Option<vector<u8>>,
    // None means no need to check, i.e. either AA (where it is already checked) or simulation
    fee_payer_public_key_hash: Option<vector<u8>>,
    txn_sequence_number: u64,
    secondary_signer_addresses: vector<address>,
    secondary_signer_public_key_hashes: vector<Option<vector<u8>>>,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    txn_expiration_time: u64,
    chain_id: u8,
    is_simulation: bool,
) {
    unified_prologue_fee_payer_v2(
        sender,
        fee_payer,
        txn_sender_public_key,
        fee_payer_public_key_hash,
        ReplayProtector::SequenceNumber(txn_sequence_number),
        secondary_signer_addresses,
        secondary_signer_public_key_hashes,
        txn_gas_price,
        txn_max_gas_units,
        txn_expiration_time,
        chain_id,
        is_simulation,
    )
}

unified_epilogue

fun unified_epilogue(account: signer, gas_payer: signer, storage_fee_refunded: u64, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64, is_simulation: bool)
Implementation 
fun unified_epilogue(
    account: signer,
    gas_payer: signer,
    storage_fee_refunded: u64,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    gas_units_remaining: u64,
    is_simulation: bool,
) {
    unified_epilogue_v2(
        account,
        gas_payer,
        storage_fee_refunded,
        txn_gas_price,
        txn_max_gas_units,
        gas_units_remaining,
        is_simulation,
        false,
    )
}

unified_prologue_v2

new set of functions to support txn payload v2 format and orderless transactions

fun unified_prologue_v2(sender: signer, txn_sender_public_key: option::Option<vector<u8>>, replay_protector: transaction_validation::ReplayProtector, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<option::Option<vector<u8>>>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, is_simulation: bool)
Implementation 
fun unified_prologue_v2(
    sender: signer,
    txn_sender_public_key: Option<vector<u8>>,
    replay_protector: ReplayProtector,
    secondary_signer_addresses: vector<address>,
    secondary_signer_public_key_hashes: vector<Option<vector<u8>>>,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    txn_expiration_time: u64,
    chain_id: u8,
    is_simulation: bool,
) {
    prologue_common(
        &sender,
        &sender,
        replay_protector,
        txn_sender_public_key,
        txn_gas_price,
        txn_max_gas_units,
        txn_expiration_time,
        chain_id,
        is_simulation,
    );
    multi_agent_common_prologue(secondary_signer_addresses, secondary_signer_public_key_hashes, is_simulation);
}

unified_prologue_fee_payer_v2

If there is no fee_payer, fee_payer = sender

fun unified_prologue_fee_payer_v2(sender: signer, fee_payer: signer, txn_sender_public_key: option::Option<vector<u8>>, fee_payer_public_key_hash: option::Option<vector<u8>>, replay_protector: transaction_validation::ReplayProtector, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<option::Option<vector<u8>>>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, is_simulation: bool)
Implementation 
fun unified_prologue_fee_payer_v2(
    sender: signer,
    fee_payer: signer,
    txn_sender_public_key: Option<vector<u8>>,
    fee_payer_public_key_hash: Option<vector<u8>>,
    replay_protector: ReplayProtector,
    secondary_signer_addresses: vector<address>,
    secondary_signer_public_key_hashes: vector<Option<vector<u8>>>,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    txn_expiration_time: u64,
    chain_id: u8,
    is_simulation: bool,
) {
    prologue_common(
        &sender,
        &fee_payer,
        replay_protector,
        txn_sender_public_key,
        txn_gas_price,
        txn_max_gas_units,
        txn_expiration_time,
        chain_id,
        is_simulation,
    );
    multi_agent_common_prologue(secondary_signer_addresses, secondary_signer_public_key_hashes, is_simulation);
    if (!skip_auth_key_check(is_simulation, &fee_payer_public_key_hash)) {
        let fee_payer_address = signer::address_of(&fee_payer);
        if (option::is_some(&fee_payer_public_key_hash)) {
            assert!(
                fee_payer_public_key_hash == option::some(account::get_authentication_key(fee_payer_address)),
                error::invalid_argument(PROLOGUE_EINVALID_ACCOUNT_AUTH_KEY)
            );
        } else {
            assert!(
                allow_missing_txn_authentication_key(fee_payer_address),
                error::invalid_argument(PROLOGUE_EINVALID_ACCOUNT_AUTH_KEY)
            )
        };
    }
}

unified_epilogue_v2

fun unified_epilogue_v2(account: signer, gas_payer: signer, storage_fee_refunded: u64, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64, is_simulation: bool, is_orderless_txn: bool)
Implementation 
fun unified_epilogue_v2(
    account: signer,
    gas_payer: signer,
    storage_fee_refunded: u64,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    gas_units_remaining: u64,
    is_simulation: bool,
    is_orderless_txn: bool,
) {
    assert!(txn_max_gas_units >= gas_units_remaining, error::invalid_argument(EOUT_OF_GAS));
    let gas_used = txn_max_gas_units - gas_units_remaining;


    assert!(
        (txn_gas_price as u128) * (gas_used as u128) <= MAX_U64,
        error::out_of_range(EOUT_OF_GAS)
    );
    let transaction_fee_amount = txn_gas_price * gas_used;


    let gas_payer_address = signer::address_of(&gas_payer);
    // it's important to maintain the error code consistent with vm
    // to do failed transaction cleanup.
    if (!skip_gas_payment(
        is_simulation,
        gas_payer_address
    )) {
        if (features::operations_default_to_fa_apt_store_enabled()) {
            assert!(
                aptos_account::is_fungible_balance_at_least(gas_payer_address, transaction_fee_amount),
                error::out_of_range(PROLOGUE_ECANT_PAY_GAS_DEPOSIT),
            );
        } else {
            assert!(
                coin::is_balance_at_least<AptosCoin>(gas_payer_address, transaction_fee_amount),
                error::out_of_range(PROLOGUE_ECANT_PAY_GAS_DEPOSIT),
            );
        };


        if (transaction_fee_amount > storage_fee_refunded) {
            let burn_amount = transaction_fee_amount - storage_fee_refunded;
            transaction_fee::burn_fee(gas_payer_address, burn_amount);
            permissioned_signer::check_permission_consume(
                &gas_payer,
                (burn_amount as u256),
                GasPermission {}
            );
        } else if (transaction_fee_amount < storage_fee_refunded) {
            let mint_amount = storage_fee_refunded - transaction_fee_amount;
            transaction_fee::mint_and_refund(gas_payer_address, mint_amount);
            permissioned_signer::increase_limit(
                &gas_payer,
                (mint_amount as u256),
                GasPermission {}
            );
        };
    };


    if (!is_orderless_txn) {
        // Increment sequence number
        let addr = signer::address_of(&account);
        account::increment_sequence_number(addr);
    }
}

Specification

High-level Requirements

No.RequirementCriticalityImplementationEnforcement
1 The sender of a transaction should have sufficient coin balance to pay the transaction fee. High The prologue_common function asserts that the transaction sender has enough coin balance to be paid as the max_transaction_fee. Formally verified via PrologueCommonAbortsIf. Moreover, the native transaction validation patterns have been manually audited.
2 All secondary signer addresses are verified to be authentic through a validation process. Critical The function multi_agent_script_prologue ensures that each secondary signer address undergoes authentication validation, including verification of account existence and authentication key matching, confirming their authenticity. Formally verified via multi_agent_script_prologue. Moreover, the native transaction validation patterns have been manually audited.
3 After successful execution, base the transaction fee on the configuration set by the features library. High The epilogue function collects the transaction fee for either redistribution or burning based on the feature::collect_and_distribute_gas_fees result. Formally Verified via epilogue. Moreover, the native transaction validation patterns have been manually audited.

Module-level Specification

pragma verify = true;
pragma aborts_if_is_strict;

grant_gas_permission

public fun grant_gas_permission(master: &signer, permissioned: &signer, gas_amount: u64)
pragma aborts_if_is_partial;

revoke_gas_permission

public fun revoke_gas_permission(permissioned: &signer)
pragma aborts_if_is_partial;

initialize

public(friend) fun initialize(aptos_framework: &signer, script_prologue_name: vector<u8>, module_prologue_name: vector<u8>, multi_agent_prologue_name: vector<u8>, user_epilogue_name: vector<u8>)

Ensure caller is aptos_framework. Aborts if TransactionValidation already exists.

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

Create a schema to reuse some code. Give some constraints that may abort according to the conditions.

schema PrologueCommonAbortsIf {
    sender: &signer;
    gas_payer: &signer;
    replay_protector: ReplayProtector;
    txn_authentication_key: Option<vector<u8>>;
    txn_gas_price: u64;
    txn_max_gas_units: u64;
    txn_expiration_time: u64;
    chain_id: u8;
    aborts_if !exists<CurrentTimeMicroseconds>(@aptos_framework);
    aborts_if !(timestamp::now_seconds() < txn_expiration_time);
    aborts_if !exists<ChainId>(@aptos_framework);
    aborts_if !(chain_id::get() == chain_id);
    let transaction_sender = signer::address_of(sender);
    let gas_payer_addr = signer::address_of(gas_payer);
}

prologue_common

fun prologue_common(sender: &signer, gas_payer: &signer, replay_protector: transaction_validation::ReplayProtector, txn_authentication_key: option::Option<vector<u8>>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, is_simulation: bool)
pragma verify = false;
include PrologueCommonAbortsIf;

check_for_replay_protection_regular_txn

fun check_for_replay_protection_regular_txn(sender_address: address, gas_payer_address: address, txn_sequence_number: u64)
pragma verify = false;

check_for_replay_protection_orderless_txn

fun check_for_replay_protection_orderless_txn(sender: address, nonce: u64, txn_expiration_time: u64)
pragma verify = false;

script_prologue

fun script_prologue(sender: signer, txn_sequence_number: u64, txn_public_key: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, _script_hash: vector<u8>)
pragma verify = false;
schema MultiAgentPrologueCommonAbortsIf {
    secondary_signer_addresses: vector<address>;
    secondary_signer_public_key_hashes: vector<Option<vector<u8>>>;
    is_simulation: bool;
    let num_secondary_signers = len(secondary_signer_addresses);
    aborts_if len(secondary_signer_public_key_hashes) != num_secondary_signers;
    // This enforces high-level requirement 2:
    aborts_if exists i in 0..num_secondary_signers:
        !account::spec_exists_at(secondary_signer_addresses[i]);
    aborts_if exists i in 0..num_secondary_signers:
        !can_skip(features::spec_simulation_enhancement_enabled(), is_simulation, secondary_signer_public_key_hashes[i]) &&
            option::spec_is_some(secondary_signer_public_key_hashes[i]) && option::spec_borrow(
            secondary_signer_public_key_hashes[i]
        ) !=
                account::spec_get_authentication_key(secondary_signer_addresses[i]);
    ensures forall i in 0..num_secondary_signers:
        account::spec_exists_at(secondary_signer_addresses[i]);
    ensures forall i in 0..num_secondary_signers:
        option::spec_is_none(secondary_signer_public_key_hashes[i]) || option::spec_borrow(
            secondary_signer_public_key_hashes[i]
        ) ==
            account::spec_get_authentication_key(secondary_signer_addresses[i])
            || can_skip(features::spec_simulation_enhancement_enabled(), is_simulation, secondary_signer_public_key_hashes[i]);
}
fun can_skip(feature_flag: bool, is_simulation: bool, auth_key: Option<vector<u8>>): bool {
   features::spec_simulation_enhancement_enabled() && is_simulation && option::spec_is_none(auth_key)
}

script_prologue_extended

fun script_prologue_extended(sender: signer, txn_sequence_number: u64, txn_public_key: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, _script_hash: vector<u8>, is_simulation: bool)
pragma verify = false;
include PrologueCommonAbortsIf {
    gas_payer: sender,
    txn_authentication_key: option::spec_some(txn_public_key),
    replay_protector: ReplayProtector::SequenceNumber(txn_sequence_number),
};

multi_agent_script_prologue

fun multi_agent_script_prologue(sender: signer, txn_sequence_number: u64, txn_sender_public_key: vector<u8>, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<vector<u8>>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8)
pragma verify = false;

multi_agent_script_prologue_extended

fun multi_agent_script_prologue_extended(sender: signer, txn_sequence_number: u64, txn_sender_public_key: vector<u8>, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<vector<u8>>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, is_simulation: bool)

Aborts if length of public key hashed vector not equal the number of singers.

pragma verify_duration_estimate = 120;
let gas_payer = sender;
pragma verify = false;

multi_agent_common_prologue

fun multi_agent_common_prologue(secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<option::Option<vector<u8>>>, is_simulation: bool)
pragma aborts_if_is_partial;

fee_payer_script_prologue

fun fee_payer_script_prologue(sender: signer, txn_sequence_number: u64, txn_sender_public_key: vector<u8>, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<vector<u8>>, fee_payer_address: address, fee_payer_public_key_hash: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8)
pragma verify = false;

fee_payer_script_prologue_extended

fun fee_payer_script_prologue_extended(sender: signer, txn_sequence_number: u64, txn_sender_public_key: vector<u8>, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<vector<u8>>, fee_payer_address: address, fee_payer_public_key_hash: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, is_simulation: bool)
pragma aborts_if_is_partial;
pragma verify_duration_estimate = 120;
aborts_if !features::spec_is_enabled(features::FEE_PAYER_ENABLED);
let gas_payer = create_signer::create_signer(fee_payer_address);
include PrologueCommonAbortsIf {
    gas_payer,
    replay_protector: ReplayProtector::SequenceNumber(txn_sequence_number),
    txn_authentication_key: option::spec_some(txn_sender_public_key),
};
aborts_if !account::spec_exists_at(fee_payer_address);
aborts_if !(fee_payer_public_key_hash == account::spec_get_authentication_key(fee_payer_address));
aborts_if !features::spec_fee_payer_enabled();

epilogue

fun epilogue(account: signer, storage_fee_refunded: u64, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64)
pragma verify = false;

epilogue_extended

fun epilogue_extended(account: signer, storage_fee_refunded: u64, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64, is_simulation: bool)

Abort according to the conditions. AptosCoinCapabilities and CoinInfo should exists. Skip transaction_fee::burn_fee verification.

pragma verify = false;
include EpilogueGasPayerAbortsIf { gas_payer: signer::address_of(account) };

epilogue_gas_payer

fun epilogue_gas_payer(account: signer, gas_payer: address, storage_fee_refunded: u64, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64)
pragma verify = false;

epilogue_gas_payer_extended

fun epilogue_gas_payer_extended(account: signer, gas_payer: address, storage_fee_refunded: u64, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64, is_simulation: bool)

Abort according to the conditions. AptosCoinCapabilities and CoinInfo should exist. Skip transaction_fee::burn_fee verification.

pragma verify = false;
include EpilogueGasPayerAbortsIf;

unified_prologue

fun unified_prologue(sender: signer, txn_sender_public_key: option::Option<vector<u8>>, txn_sequence_number: u64, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<option::Option<vector<u8>>>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, is_simulation: bool)
pragma verify = false;

unified_prologue_fee_payer

fun unified_prologue_fee_payer(sender: signer, fee_payer: signer, txn_sender_public_key: option::Option<vector<u8>>, fee_payer_public_key_hash: option::Option<vector<u8>>, txn_sequence_number: u64, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<option::Option<vector<u8>>>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, is_simulation: bool)
pragma verify = false;

unified_epilogue

fun unified_epilogue(account: signer, gas_payer: signer, storage_fee_refunded: u64, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64, is_simulation: bool)
pragma verify = false;

unified_prologue_v2

fun unified_prologue_v2(sender: signer, txn_sender_public_key: option::Option<vector<u8>>, replay_protector: transaction_validation::ReplayProtector, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<option::Option<vector<u8>>>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, is_simulation: bool)
pragma verify = false;

unified_prologue_fee_payer_v2

fun unified_prologue_fee_payer_v2(sender: signer, fee_payer: signer, txn_sender_public_key: option::Option<vector<u8>>, fee_payer_public_key_hash: option::Option<vector<u8>>, replay_protector: transaction_validation::ReplayProtector, secondary_signer_addresses: vector<address>, secondary_signer_public_key_hashes: vector<option::Option<vector<u8>>>, txn_gas_price: u64, txn_max_gas_units: u64, txn_expiration_time: u64, chain_id: u8, is_simulation: bool)
pragma verify = false;

unified_epilogue_v2

fun unified_epilogue_v2(account: signer, gas_payer: signer, storage_fee_refunded: u64, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64, is_simulation: bool, is_orderless_txn: bool)
pragma verify = false;
schema EpilogueGasPayerAbortsIf {
    account: signer;
    gas_payer: address;
    storage_fee_refunded: u64;
    txn_gas_price: u64;
    txn_max_gas_units: u64;
    gas_units_remaining: u64;
    aborts_if !(txn_max_gas_units >= gas_units_remaining);
    let gas_used = txn_max_gas_units - gas_units_remaining;
    aborts_if !(txn_gas_price * gas_used <= MAX_U64);
    let transaction_fee_amount = txn_gas_price * gas_used;
    let addr = signer::address_of(account);
    let pre_account = global<account::Account>(addr);
    let post account = global<account::Account>(addr);
    aborts_if !exists<CoinStore<AptosCoin>>(gas_payer);
    aborts_if !exists<Account>(addr);
    aborts_if !(global<Account>(addr).sequence_number < MAX_U64);
    ensures account.sequence_number == pre_account.sequence_number + 1;
    let amount_to_burn = transaction_fee_amount - storage_fee_refunded;
    let apt_addr = type_info::type_of<AptosCoin>().account_address;
    let maybe_apt_supply = global<CoinInfo<AptosCoin>>(apt_addr).supply;
    let total_supply_enabled = option::spec_is_some(maybe_apt_supply);
    let apt_supply = option::spec_borrow(maybe_apt_supply);
    let apt_supply_value = optional_aggregator::optional_aggregator_value(apt_supply);
    let post post_maybe_apt_supply = global<CoinInfo<AptosCoin>>(apt_addr).supply;
    let post post_apt_supply = option::spec_borrow(post_maybe_apt_supply);
    let post post_apt_supply_value = optional_aggregator::optional_aggregator_value(post_apt_supply);
    aborts_if amount_to_burn > 0 && !exists<AptosCoinCapabilities>(@aptos_framework);
    aborts_if amount_to_burn > 0 && !exists<CoinInfo<AptosCoin>>(apt_addr);
    aborts_if amount_to_burn > 0 && total_supply_enabled && apt_supply_value < amount_to_burn;
    ensures total_supply_enabled ==> apt_supply_value - amount_to_burn == post_apt_supply_value;
    let amount_to_mint = storage_fee_refunded - transaction_fee_amount;
    let total_supply = coin::supply<AptosCoin>;
    let post post_total_supply = coin::supply<AptosCoin>;
    aborts_if amount_to_mint > 0 && !exists<CoinStore<AptosCoin>>(addr);
    aborts_if amount_to_mint > 0 && !exists<AptosCoinMintCapability>(@aptos_framework);
    aborts_if amount_to_mint > 0 && total_supply + amount_to_mint > MAX_U128;
    ensures amount_to_mint > 0 ==> post_total_supply == total_supply + amount_to_mint;
    let aptos_addr = type_info::type_of<AptosCoin>().account_address;
    aborts_if (amount_to_mint != 0) && !exists<coin::CoinInfo<AptosCoin>>(aptos_addr);
    include coin::CoinAddAbortsIf<AptosCoin> { amount: amount_to_mint };
}