Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Module 0x1::transaction_validation 

use 0x1::account;
use 0x1::account_abstraction;
use 0x1::aptos_account;
use 0x1::chain_id;
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::transaction_limits;
use 0x1::vector;

Enum ReplayProtector 

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

Resource 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>

Struct GasPermission 

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

Enum PrologueArgs

Versioned enum-based prologue and epilogue Arguments for versioned_prologue. A new field becomes a new enum variant.

  • Old variants are kept for compatibility; their on-chain layout must remain stable.
  • Only the most recent variant needs real handling here — old variants were executed against the framework version that shipped them and are not reached from this code.
enum PrologueArgs
Variants
V1
Fields
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
txn_limits_request: option::Option<transaction_limits::UserTxnLimitsRequest>

Enum EpilogueArgs

Arguments for versioned_epilogue. A new field becomes a new enum variant.

  • Old variants are kept for compatibility; their on-chain layout must remain stable.
  • Only the most recent variant needs real handling here — old variants were executed against the framework version that shipped them and are not reached from this code.
enum EpilogueArgs
Variants
V1
Fields
fee_statement: transaction_fee::FeeStatement
txn_gas_price: u64
txn_max_gas_units: u64
gas_units_remaining: u64
is_simulation: bool
is_orderless_txn: bool

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_EXP_TIME_SECONDS_FOR_ORDERLESS_TXNS: u64 = 100;


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;

Function 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 {}
    )
}

Function 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 {})
}

Function 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,
    });
}

Function 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))
}

Function 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, txn_limits_request: option::Option<transaction_limits::UserTxnLimitsRequest>)
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,
    txn_limits_request: Option<UserTxnLimitsRequest>,
) {
    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 (txn_authentication_key.is_some()) {
            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,
            );
        }
    };

    if (txn_limits_request.is_some()) {
        transaction_limits::validate_high_txn_limits(
            gas_payer_address,
            txn_limits_request.destroy_some(),
        );
    };

    // 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)
        );
        assert!(
            aptos_account::is_fungible_balance_at_least(gas_payer_address, max_transaction_fee),
            error::invalid_argument(PROLOGUE_ECANT_PAY_GAS_DEPOSIT)
        );
    };
}

Function 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)
        );
    };
}

Function 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_EXP_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));
}

Function 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,
        option::none(),
    )
}

Function 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,
        option::none(),
    )
}

Function 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,
        option::none(),
    );
    multi_agent_common_prologue(
        secondary_signer_addresses,
        secondary_signer_public_key_hashes.map(|x| option::some(x)),
        false
    );
}

Function 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,
        option::none(),
    );
    multi_agent_common_prologue(
        secondary_signer_addresses,
        secondary_signer_public_key_hashes.map(|x| option::some(x)),
        is_simulation
    );
}

Function 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 = secondary_signer_addresses.length();
    assert!(
        secondary_signer_public_key_hashes.length() == 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 = secondary_signer_addresses[i];
        assert!(account::exists_at(secondary_address), error::invalid_argument(PROLOGUE_EACCOUNT_DOES_NOT_EXIST));
        let signer_public_key_hash = secondary_signer_public_key_hashes[i];
        if (!skip_auth_key_check(is_simulation, &signer_public_key_hash)) {
            if (signer_public_key_hash.is_some()) {
                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 += 1;
    }
}

Function 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,
) {
    // 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,
        option::none(),
    );
    multi_agent_common_prologue(
        secondary_signer_addresses,
        secondary_signer_public_key_hashes.map(|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),
    );
}

Function 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,
) {
    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,
        option::none(),
    );
    multi_agent_common_prologue(
        secondary_signer_addresses,
        secondary_signer_public_key_hashes.map(|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),
            )
    }
}

Function 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
    );
}

Function 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
    );
}

Function 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,
    );
}

Function 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)) {
        assert!(
            aptos_account::is_fungible_balance_at_least(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);
}

Function 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 && (auth_key.is_none() || auth_key.borrow().is_empty())
}

Function 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
}

Function 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,
    )
}

Function 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,
    )
}

Function 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,
    )
}

Function 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,
        option::none(),
    );
    multi_agent_common_prologue(secondary_signer_addresses, secondary_signer_public_key_hashes, is_simulation);
}

Function 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,
        option::none(),
    );
    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 (fee_payer_public_key_hash.is_some()) {
            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)
            )
        };
    }
}

Function 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
    )) {
        assert!(
            aptos_account::is_fungible_balance_at_least(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);
    }
}

Function versioned_prologue 

fun versioned_prologue(sender: signer, fee_payer: signer, args: transaction_validation::PrologueArgs)
Implementation 
fun versioned_prologue(sender: signer, fee_payer: signer, args: PrologueArgs) {
    match (args) {
        V1 {
            txn_sender_public_key,
            fee_payer_public_key_hash,
            replay_protector,
            secondary_signer_addresses,
            secondary_signer_public_key_hashes,
            txn_gas_price,
            txn_max_gas_units,
            txn_expiration_time,
            chain_id,
            is_simulation,
            txn_limits_request,
        } => {
            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,
                txn_limits_request,
            );
            multi_agent_common_prologue(
                secondary_signer_addresses,
                secondary_signer_public_key_hashes,
                is_simulation,
            );

            let fee_payer_address = signer::address_of(&fee_payer);
            if (fee_payer_address != signer::address_of(&sender)) {
                if (!skip_auth_key_check(is_simulation, &fee_payer_public_key_hash)) {
                    if (fee_payer_public_key_hash.is_some()) {
                        let fee_payer_public_key_hash = fee_payer_public_key_hash.destroy_some();
                        assert!(
                            fee_payer_public_key_hash == 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),
                        );
                    };
                };
            };
        },
    }
}

Function versioned_epilogue 

fun versioned_epilogue(account: signer, fee_payer: signer, args: transaction_validation::EpilogueArgs)
Implementation 
fun versioned_epilogue(account: signer, fee_payer: signer, args: EpilogueArgs) {
    match (args) {
        V1 {
            fee_statement,
            txn_gas_price,
            txn_max_gas_units,
            gas_units_remaining,
            is_simulation,
            is_orderless_txn,
        } => {
            unified_epilogue_v2(
                account,
                fee_payer,
                fee_statement.storage_fee_refund_octas(),
                txn_gas_price,
                txn_max_gas_units,
                gas_units_remaining,
                is_simulation,
                is_orderless_txn,
            );
            transaction_fee::emit_fee_statement(fee_statement);
        },
    }
}

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;

Function grant_gas_permission 

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

pragma aborts_if_is_partial;

Function revoke_gas_permission 

public fun revoke_gas_permission(permissioned: &signer)

pragma aborts_if_is_partial;

Function 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);
}

Function 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, txn_limits_request: option::Option<transaction_limits::UserTxnLimitsRequest>)

pragma verify = false;
include PrologueCommonAbortsIf;

Function 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;

Function check_for_replay_protection_orderless_txn 

fun check_for_replay_protection_orderless_txn(sender: address, nonce: u64, txn_expiration_time: u64)

pragma verify = false;

Function 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::is_some(secondary_signer_public_key_hashes[i]) && option::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::is_none(secondary_signer_public_key_hashes[i]) || option::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::is_none(auth_key)
}

Function 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),
};

Function 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;

Function 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;

Function 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;

Function 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;

Function 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::spec_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();

Function 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;

Function 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) };

Function 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;

Function 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;

Function 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;

Function 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;

Function 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;

Function 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;

Function 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;

Function 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;

Function versioned_prologue 

fun versioned_prologue(sender: signer, fee_payer: signer, args: transaction_validation::PrologueArgs)

pragma verify = false;

Function versioned_epilogue 

fun versioned_epilogue(account: signer, fee_payer: signer, args: transaction_validation::EpilogueArgs)

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::is_some(maybe_apt_supply);
    let apt_supply = option::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::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 };
}