aptos_account - [mainnet]

use 0x1::account;
use 0x1::aptos_coin;
use 0x1::coin;
use 0x1::create_signer;
use 0x1::error;
use 0x1::event;
use 0x1::features;
use 0x1::fungible_asset;
use 0x1::object;
use 0x1::primary_fungible_store;
use 0x1::signer;

Constants

Account opted out of receiving coins that they did not register to receive.

const EACCOUNT_DOES_NOT_ACCEPT_DIRECT_COIN_TRANSFERS: u64 = 3;

Account opted out of directly receiving NFT tokens.

const EACCOUNT_DOES_NOT_ACCEPT_DIRECT_TOKEN_TRANSFERS: u64 = 4;

Account does not exist.

const EACCOUNT_NOT_FOUND: u64 = 1;

Account is not registered to receive APT.

const EACCOUNT_NOT_REGISTERED_FOR_APT: u64 = 2;

The lengths of the recipients and amounts lists don’t match.

const EMISMATCHING_RECIPIENTS_AND_AMOUNTS_LENGTH: u64 = 5;

Structs

`DirectCoinTransferConfigUpdatedEvent`

Event emitted when an account’s direct coins transfer config is updated.

struct DirectCoinTransferConfigUpdatedEvent has drop, store

Fields

new_allow_direct_transfers: bool

`DirectCoinTransferConfigUpdated`

#[event]
struct DirectCoinTransferConfigUpdated has drop, store

Fields

account: address
new_allow_direct_transfers: bool

Resources

`DirectTransferConfig`

Configuration for whether an account can receive direct transfers of coins that they have not registered.

By default, this is enabled. Users can opt-out by disabling at any time.

struct DirectTransferConfig has key

Fields

allow_arbitrary_coin_transfers: bool
update_coin_transfer_events: event::EventHandle<aptos_account::DirectCoinTransferConfigUpdatedEvent>

Functions

`create_account`

Basic account creation methods.

public entry fun create_account(auth_key: address)

Implementation

public entry fun create_account(auth_key: address) {
    let account_signer = account::create_account(auth_key);
    register_apt(&account_signer);
}

`batch_transfer`

Batch version of APT transfer.

public entry fun batch_transfer(source: &signer, recipients: vector<address>, amounts: vector<u64>)

Implementation

public entry fun batch_transfer(source: &signer, recipients: vector<address>, amounts: vector<u64>) {
    let recipients_len = vector::length(&recipients);
    assert!(
        recipients_len == vector::length(&amounts),
        error::invalid_argument(EMISMATCHING_RECIPIENTS_AND_AMOUNTS_LENGTH),
    );

    vector::enumerate_ref(&recipients, |i, to| {
        let amount = *vector::borrow(&amounts, i);
        transfer(source, *to, amount);
    });
}

`transfer`

Convenient function to transfer APT to a recipient account that might not exist. This would create the recipient account first, which also registers it to receive APT, before transferring.

public entry fun transfer(source: &signer, to: address, amount: u64)

Implementation

public entry fun transfer(source: &signer, to: address, amount: u64) {
    if (!account::exists_at(to)) {
        create_account(to)
    };

    if (features::operations_default_to_fa_apt_store_enabled()) {
        fungible_transfer_only(source, to, amount)
    } else {
        // Resource accounts can be created without registering them to receive APT.
        // This conveniently does the registration if necessary.
        if (!coin::is_account_registered<AptosCoin>(to)) {
            coin::register<AptosCoin>(&create_signer(to));
        };
        coin::transfer<AptosCoin>(source, to, amount)
    }
}

`batch_transfer_coins`

Batch version of transfer_coins.

public entry fun batch_transfer_coins<CoinType>(from: &signer, recipients: vector<address>, amounts: vector<u64>)

Implementation

public entry fun batch_transfer_coins<CoinType>(
    from: &signer, recipients: vector<address>, amounts: vector<u64>) acquires DirectTransferConfig {
    let recipients_len = vector::length(&recipients);
    assert!(
        recipients_len == vector::length(&amounts),
        error::invalid_argument(EMISMATCHING_RECIPIENTS_AND_AMOUNTS_LENGTH),
    );

    vector::enumerate_ref(&recipients, |i, to| {
        let amount = *vector::borrow(&amounts, i);
        transfer_coins<CoinType>(from, *to, amount);
    });
}

`transfer_coins`

Convenient function to transfer a custom CoinType to a recipient account that might not exist. This would create the recipient account first and register it to receive the CoinType, before transferring.

public entry fun transfer_coins<CoinType>(from: &signer, to: address, amount: u64)

Implementation

public entry fun transfer_coins<CoinType>(from: &signer, to: address, amount: u64) acquires DirectTransferConfig {
    deposit_coins(to, coin::withdraw<CoinType>(from, amount));
}

`deposit_coins`

Convenient function to deposit a custom CoinType into a recipient account that might not exist. This would create the recipient account first and register it to receive the CoinType, before transferring.

public fun deposit_coins<CoinType>(to: address, coins: coin::Coin<CoinType>)

Implementation

public fun deposit_coins<CoinType>(to: address, coins: Coin<CoinType>) acquires DirectTransferConfig {
    if (!account::exists_at(to)) {
        create_account(to);
        spec {
            // TODO(fa_migration)
            // assert coin::spec_is_account_registered<AptosCoin>(to);
            // assume aptos_std::type_info::type_of<CoinType>() == aptos_std::type_info::type_of<AptosCoin>() ==>
            //     coin::spec_is_account_registered<CoinType>(to);
        };
    };
    if (!coin::is_account_registered<CoinType>(to)) {
        assert!(
            can_receive_direct_coin_transfers(to),
            error::permission_denied(EACCOUNT_DOES_NOT_ACCEPT_DIRECT_COIN_TRANSFERS),
        );
        coin::register<CoinType>(&create_signer(to));
    };
    coin::deposit<CoinType>(to, coins)
}

`batch_transfer_fungible_assets`

Batch version of transfer_fungible_assets.

public entry fun batch_transfer_fungible_assets(from: &signer, metadata: object::Object<fungible_asset::Metadata>, recipients: vector<address>, amounts: vector<u64>)

Implementation

public entry fun batch_transfer_fungible_assets(
    from: &signer,
    metadata: Object<Metadata>,
    recipients: vector<address>,
    amounts: vector<u64>
) {
    let recipients_len = vector::length(&recipients);
    assert!(
        recipients_len == vector::length(&amounts),
        error::invalid_argument(EMISMATCHING_RECIPIENTS_AND_AMOUNTS_LENGTH),
    );

    vector::enumerate_ref(&recipients, |i, to| {
        let amount = *vector::borrow(&amounts, i);
        transfer_fungible_assets(from, metadata, *to, amount);
    });
}

`transfer_fungible_assets`

Convenient function to deposit fungible asset into a recipient account that might not exist. This would create the recipient account first to receive the fungible assets.

public entry fun transfer_fungible_assets(from: &signer, metadata: object::Object<fungible_asset::Metadata>, to: address, amount: u64)

Implementation

public entry fun transfer_fungible_assets(from: &signer, metadata: Object<Metadata>, to: address, amount: u64) {
    deposit_fungible_assets(to, primary_fungible_store::withdraw(from, metadata, amount));
}

`deposit_fungible_assets`

Convenient function to deposit fungible asset into a recipient account that might not exist. This would create the recipient account first to receive the fungible assets.

public fun deposit_fungible_assets(to: address, fa: fungible_asset::FungibleAsset)

Implementation

public fun deposit_fungible_assets(to: address, fa: FungibleAsset) {
    if (!account::exists_at(to)) {
        create_account(to);
    };
    primary_fungible_store::deposit(to, fa)
}

`assert_account_exists`

public fun assert_account_exists(addr: address)

Implementation

public fun assert_account_exists(addr: address) {
    assert!(account::exists_at(addr), error::not_found(EACCOUNT_NOT_FOUND));
}

`assert_account_is_registered_for_apt`

public fun assert_account_is_registered_for_apt(addr: address)

Implementation

public fun assert_account_is_registered_for_apt(addr: address) {
    assert_account_exists(addr);
    assert!(coin::is_account_registered<AptosCoin>(addr), error::not_found(EACCOUNT_NOT_REGISTERED_FOR_APT));
}

`set_allow_direct_coin_transfers`

Set whether account can receive direct transfers of coins that they have not explicitly registered to receive.

public entry fun set_allow_direct_coin_transfers(account: &signer, allow: bool)

Implementation

public entry fun set_allow_direct_coin_transfers(account: &signer, allow: bool) acquires DirectTransferConfig {
    let addr = signer::address_of(account);
    if (exists<DirectTransferConfig>(addr)) {
        let direct_transfer_config = borrow_global_mut<DirectTransferConfig>(addr);
        // Short-circuit to avoid emitting an event if direct transfer config is not changing.
        if (direct_transfer_config.allow_arbitrary_coin_transfers == allow) {
            return
        };

        direct_transfer_config.allow_arbitrary_coin_transfers = allow;

        if (std::features::module_event_migration_enabled()) {
            emit(DirectCoinTransferConfigUpdated { account: addr, new_allow_direct_transfers: allow });
        } else {
            emit_event(
                &mut direct_transfer_config.update_coin_transfer_events,
                DirectCoinTransferConfigUpdatedEvent { new_allow_direct_transfers: allow });
        };
    } else {
        let direct_transfer_config = DirectTransferConfig {
            allow_arbitrary_coin_transfers: allow,
            update_coin_transfer_events: new_event_handle<DirectCoinTransferConfigUpdatedEvent>(account),
        };
        if (std::features::module_event_migration_enabled()) {
            emit(DirectCoinTransferConfigUpdated { account: addr, new_allow_direct_transfers: allow });
        } else {
            emit_event(
                &mut direct_transfer_config.update_coin_transfer_events,
                DirectCoinTransferConfigUpdatedEvent { new_allow_direct_transfers: allow });
        };
        move_to(account, direct_transfer_config);
    };
}

`can_receive_direct_coin_transfers`

Return true if account can receive direct transfers of coins that they have not explicitly registered to receive.

By default, this returns true if an account has not explicitly set whether the can receive direct transfers.

#[view]
public fun can_receive_direct_coin_transfers(account: address): bool

Implementation

public fun can_receive_direct_coin_transfers(account: address): bool acquires DirectTransferConfig {
    !exists<DirectTransferConfig>(account) ||
        borrow_global<DirectTransferConfig>(account).allow_arbitrary_coin_transfers
}

`register_apt`

public(friend) fun register_apt(account_signer: &signer)

Implementation

public(friend) fun register_apt(account_signer: &signer) {
    if (features::new_accounts_default_to_fa_apt_store_enabled()) {
        ensure_primary_fungible_store_exists(signer::address_of(account_signer));
    } else {
        coin::register<AptosCoin>(account_signer);
    }
}

`fungible_transfer_only`

APT Primary Fungible Store specific specialized functions, Utilized internally once migration of APT to FungibleAsset is complete. Convenient function to transfer APT to a recipient account that might not exist. This would create the recipient APT PFS first, which also registers it to receive APT, before transferring. TODO: once migration is complete, rename to just “transfer_only” and make it an entry function (for cheapest way to transfer APT) - if we want to allow APT PFS without account itself

public(friend) entry fun fungible_transfer_only(source: &signer, to: address, amount: u64)

Implementation

public(friend) entry fun fungible_transfer_only(
    source: &signer, to: address, amount: u64
) {
    let sender_store = ensure_primary_fungible_store_exists(signer::address_of(source));
    let recipient_store = ensure_primary_fungible_store_exists(to);

    // use internal APIs, as they skip:
    // - owner, frozen and dispatchable checks
    // as APT cannot be frozen or have dispatch, and PFS cannot be transfered
    // (PFS could potentially be burned. regular transfer would permanently unburn the store.
    // Ignoring the check here has the equivalent of unburning, transfers, and then burning again)
    fungible_asset::withdraw_permission_check_by_address(source, sender_store, amount);
    fungible_asset::unchecked_deposit(recipient_store, fungible_asset::unchecked_withdraw(sender_store, amount));
}

`is_fungible_balance_at_least`

Is balance from APT Primary FungibleStore at least the given amount

public(friend) fun is_fungible_balance_at_least(account: address, amount: u64): bool

Implementation

public(friend) fun is_fungible_balance_at_least(account: address, amount: u64): bool {
    let store_addr = primary_fungible_store_address(account);
    fungible_asset::is_address_balance_at_least(store_addr, amount)
}

`burn_from_fungible_store_for_gas`

Burn from APT Primary FungibleStore for gas charge

public(friend) fun burn_from_fungible_store_for_gas(ref: &fungible_asset::BurnRef, account: address, amount: u64)

Implementation

public(friend) fun burn_from_fungible_store_for_gas(
    ref: &BurnRef,
    account: address,
    amount: u64,
) {
    // Skip burning if amount is zero. This shouldn't error out as it's called as part of transaction fee burning.
    if (amount != 0) {
        let store_addr = primary_fungible_store_address(account);
        fungible_asset::address_burn_from_for_gas(ref, store_addr, amount);
    };
}

`ensure_primary_fungible_store_exists`

Ensure that APT Primary FungibleStore exists (and create if it doesn’t)

fun ensure_primary_fungible_store_exists(owner: address): address

Implementation

inline fun ensure_primary_fungible_store_exists(owner: address): address {
    let store_addr = primary_fungible_store_address(owner);
    if (fungible_asset::store_exists(store_addr)) {
        store_addr
    } else {
        object::object_address(&primary_fungible_store::create_primary_store(owner, object::address_to_object<Metadata>(@aptos_fungible_asset)))
    }
}

`primary_fungible_store_address`

Address of APT Primary Fungible Store

fun primary_fungible_store_address(account: address): address

Implementation

inline fun primary_fungible_store_address(account: address): address {
    object::create_user_derived_object_address(account, @aptos_fungible_asset)
}

Specification

High-level Requirements

No.	Requirement	Criticality	Implementation	Enforcement
1	During the creation of an Aptos account the following rules should hold: (1) the authentication key should be 32 bytes in length, (2) an Aptos account should not already exist for that authentication key, and (3) the address of the authentication key should not be equal to a reserved address (0x0, 0x1, or 0x3).	Critical	The authentication key which is passed in as an argument to create_account should satisfy all necessary conditions.	Formally verified via CreateAccountAbortsIf.
2	After creating an Aptos account, the account should become registered to receive AptosCoin.	Critical	The create_account function creates a new account for the particular address and registers AptosCoin.	Formally verified via create_account.
3	An account may receive a direct transfer of coins they have not registered for if and only if the transfer of arbitrary coins is enabled. By default the option should always set to be enabled for an account.	Low	Transfers of a coin to an account that has not yet registered for that coin should abort if and only if the allow_arbitrary_coin_transfers flag is explicitly set to false.	Formally verified via can_receive_direct_coin_transfers.
4	Setting direct coin transfers may only occur if and only if a direct transfer config is associated with the provided account address.	Low	The set_allow_direct_coin_transfers function ensures the DirectTransferConfig structure exists for the signer.	Formally verified via set_allow_direct_coin_transfers.
5	The transfer function should ensure an account is created for the provided destination if one does not exist; then, register AptosCoin for that account if a particular is unregistered before transferring the amount.	Critical	The transfer function checks if the recipient account exists. If the account does not exist, the function creates one and registers the account to AptosCoin if not registered.	Formally verified via transfer.
6	Creating an account for the provided destination and registering it for that particular CoinType should be the only way to enable depositing coins, provided the account does not already exist.	Critical	The deposit_coins function verifies if the recipient account exists. If the account does not exist, the function creates one and ensures that the account becomes registered for the specified CointType.	Formally verified via deposit_coins.
7	When performing a batch transfer of Aptos Coin and/or a batch transfer of a custom coin type, it should ensure that the vector containing destination addresses and the vector containing the corresponding amounts are equal in length.	Low	The batch_transfer and batch_transfer_coins functions verify that the length of the recipient addresses vector matches the length of the amount vector through an assertion.	Formally verified via batch_transfer_coins.

Module-level Specification

pragma aborts_if_is_strict;

`create_account`

public entry fun create_account(auth_key: address)

Check if the bytes of the auth_key is 32. The Account does not exist under the auth_key before creating the account. Limit the address of auth_key is not @vm_reserved / @aptos_framework / @aptos_toke.

// This enforces high-level requirement 1:
pragma aborts_if_is_partial;
include CreateAccountAbortsIf;

schema CreateAccountAbortsIf {
    auth_key: address;
    aborts_if exists<account::Account>(auth_key);
    aborts_if auth_key == @vm_reserved || auth_key == @aptos_framework || auth_key == @aptos_token;
}

fun length_judgment(auth_key: address): bool {
   use std::bcs;

   let authentication_key = bcs::to_bytes(auth_key);
   len(authentication_key) != 32
}

`batch_transfer`

public entry fun batch_transfer(source: &signer, recipients: vector<address>, amounts: vector<u64>)

pragma verify = false;
let account_addr_source = signer::address_of(source);
let coin_store_source = global<coin::CoinStore<AptosCoin>>(account_addr_source);
let balance_source = coin_store_source.coin.value;
aborts_if len(recipients) != len(amounts);
aborts_if exists i in 0..len(recipients):
        !account::spec_exists_at(recipients[i]) && length_judgment(recipients[i]);
aborts_if exists i in 0..len(recipients):
        !account::spec_exists_at(recipients[i]) && (recipients[i] == @vm_reserved || recipients[i] == @aptos_framework || recipients[i] == @aptos_token);
ensures forall i in 0..len(recipients):
        (!account::spec_exists_at(recipients[i]) ==> !length_judgment(recipients[i])) &&
            (!account::spec_exists_at(recipients[i]) ==> (recipients[i] != @vm_reserved && recipients[i] != @aptos_framework && recipients[i] != @aptos_token));
aborts_if exists i in 0..len(recipients):
    !exists<coin::CoinStore<AptosCoin>>(account_addr_source);
aborts_if exists i in 0..len(recipients):
    coin_store_source.frozen;
aborts_if exists i in 0..len(recipients):
    global<coin::CoinStore<AptosCoin>>(account_addr_source).coin.value < amounts[i];
aborts_if exists i in 0..len(recipients):
    exists<coin::CoinStore<AptosCoin>>(recipients[i]) && global<coin::CoinStore<AptosCoin>>(recipients[i]).frozen;
aborts_if exists i in 0..len(recipients):
    account::spec_exists_at(recipients[i]) && !exists<coin::CoinStore<AptosCoin>>(recipients[i]) && global<account::Account>(recipients[i]).guid_creation_num + 2 >= account::MAX_GUID_CREATION_NUM;
aborts_if exists i in 0..len(recipients):
    account::spec_exists_at(recipients[i]) && !exists<coin::CoinStore<AptosCoin>>(recipients[i]) && global<account::Account>(recipients[i]).guid_creation_num + 2 > MAX_U64;

`transfer`

public entry fun transfer(source: &signer, to: address, amount: u64)

pragma verify = false;
let account_addr_source = signer::address_of(source);
include CreateAccountTransferAbortsIf;
include GuidAbortsIf<AptosCoin>;
include WithdrawAbortsIf<AptosCoin>{from: source};
include TransferEnsures<AptosCoin>;
aborts_if exists<coin::CoinStore<AptosCoin>>(to) && global<coin::CoinStore<AptosCoin>>(to).frozen;
// This enforces high-level requirement 5:
ensures exists<aptos_framework::account::Account>(to);
ensures exists<coin::CoinStore<AptosCoin>>(to);

`batch_transfer_coins`

public entry fun batch_transfer_coins<CoinType>(from: &signer, recipients: vector<address>, amounts: vector<u64>)

pragma verify = false;
let account_addr_source = signer::address_of(from);
let coin_store_source = global<coin::CoinStore<CoinType>>(account_addr_source);
let balance_source = coin_store_source.coin.value;
// This enforces high-level requirement 7:
aborts_if len(recipients) != len(amounts);
aborts_if exists i in 0..len(recipients):
        !account::spec_exists_at(recipients[i]) && length_judgment(recipients[i]);
aborts_if exists i in 0..len(recipients):
        !account::spec_exists_at(recipients[i]) && (recipients[i] == @vm_reserved || recipients[i] == @aptos_framework || recipients[i] == @aptos_token);
ensures forall i in 0..len(recipients):
        (!account::spec_exists_at(recipients[i]) ==> !length_judgment(recipients[i])) &&
            (!account::spec_exists_at(recipients[i]) ==> (recipients[i] != @vm_reserved && recipients[i] != @aptos_framework && recipients[i] != @aptos_token));
aborts_if exists i in 0..len(recipients):
    !exists<coin::CoinStore<CoinType>>(account_addr_source);
aborts_if exists i in 0..len(recipients):
    coin_store_source.frozen;
aborts_if exists i in 0..len(recipients):
    global<coin::CoinStore<CoinType>>(account_addr_source).coin.value < amounts[i];
aborts_if exists i in 0..len(recipients):
    exists<coin::CoinStore<CoinType>>(recipients[i]) && global<coin::CoinStore<CoinType>>(recipients[i]).frozen;
aborts_if exists i in 0..len(recipients):
    account::spec_exists_at(recipients[i]) && !exists<coin::CoinStore<CoinType>>(recipients[i]) && global<account::Account>(recipients[i]).guid_creation_num + 2 >= account::MAX_GUID_CREATION_NUM;
aborts_if exists i in 0..len(recipients):
    account::spec_exists_at(recipients[i]) && !exists<coin::CoinStore<CoinType>>(recipients[i]) && global<account::Account>(recipients[i]).guid_creation_num + 2 > MAX_U64;

`transfer_coins`

public entry fun transfer_coins<CoinType>(from: &signer, to: address, amount: u64)

pragma verify = false;
let account_addr_source = signer::address_of(from);
include CreateAccountTransferAbortsIf;
include WithdrawAbortsIf<CoinType>;
include GuidAbortsIf<CoinType>;
include RegistCoinAbortsIf<CoinType>;
include TransferEnsures<CoinType>;
aborts_if exists<coin::CoinStore<CoinType>>(to) && global<coin::CoinStore<CoinType>>(to).frozen;
ensures exists<aptos_framework::account::Account>(to);
ensures exists<aptos_framework::coin::CoinStore<CoinType>>(to);

`deposit_coins`

public fun deposit_coins<CoinType>(to: address, coins: coin::Coin<CoinType>)

pragma verify = false;
include CreateAccountTransferAbortsIf;
include GuidAbortsIf<CoinType>;
include RegistCoinAbortsIf<CoinType>;
let if_exist_coin = exists<coin::CoinStore<CoinType>>(to);
aborts_if if_exist_coin && global<coin::CoinStore<CoinType>>(to).frozen;
// This enforces high-level requirement 6:
ensures exists<aptos_framework::account::Account>(to);
ensures exists<aptos_framework::coin::CoinStore<CoinType>>(to);
let coin_store_to = global<coin::CoinStore<CoinType>>(to).coin.value;
let post post_coin_store_to = global<coin::CoinStore<CoinType>>(to).coin.value;
ensures if_exist_coin ==> post_coin_store_to == coin_store_to + coins.value;

`batch_transfer_fungible_assets`

public entry fun batch_transfer_fungible_assets(from: &signer, metadata: object::Object<fungible_asset::Metadata>, recipients: vector<address>, amounts: vector<u64>)

pragma verify = false;

`transfer_fungible_assets`

public entry fun transfer_fungible_assets(from: &signer, metadata: object::Object<fungible_asset::Metadata>, to: address, amount: u64)

pragma verify = false;

`deposit_fungible_assets`

public fun deposit_fungible_assets(to: address, fa: fungible_asset::FungibleAsset)

pragma verify = false;

`assert_account_exists`

public fun assert_account_exists(addr: address)

aborts_if !account::spec_exists_at(addr);

`assert_account_is_registered_for_apt`

public fun assert_account_is_registered_for_apt(addr: address)

Check if the address existed. Check if the AptosCoin under the address existed.

pragma aborts_if_is_partial;

`set_allow_direct_coin_transfers`

public entry fun set_allow_direct_coin_transfers(account: &signer, allow: bool)

pragma verify = false;

`can_receive_direct_coin_transfers`

#[view]
public fun can_receive_direct_coin_transfers(account: address): bool

aborts_if false;
// This enforces high-level requirement 3:
ensures result == (
    !exists<DirectTransferConfig>(account) ||
        global<DirectTransferConfig>(account).allow_arbitrary_coin_transfers
);

`register_apt`

public(friend) fun register_apt(account_signer: &signer)

pragma verify = false;

`fungible_transfer_only`

public(friend) entry fun fungible_transfer_only(source: &signer, to: address, amount: u64)

pragma verify = false;

`is_fungible_balance_at_least`

public(friend) fun is_fungible_balance_at_least(account: address, amount: u64): bool

pragma verify = false;

`burn_from_fungible_store_for_gas`

public(friend) fun burn_from_fungible_store_for_gas(ref: &fungible_asset::BurnRef, account: address, amount: u64)

pragma verify = false;

schema CreateAccountTransferAbortsIf {
    to: address;
    aborts_if !account::spec_exists_at(to) && length_judgment(to);
    aborts_if !account::spec_exists_at(to) && (to == @vm_reserved || to == @aptos_framework || to == @aptos_token);
}

schema WithdrawAbortsIf<CoinType> {
    from: &signer;
    amount: u64;
    let account_addr_source = signer::address_of(from);
    let coin_store_source = global<coin::CoinStore<CoinType>>(account_addr_source);
    let balance_source = coin_store_source.coin.value;
    aborts_if !exists<coin::CoinStore<CoinType>>(account_addr_source);
    aborts_if coin_store_source.frozen;
    aborts_if balance_source < amount;
}

schema GuidAbortsIf<CoinType> {
    to: address;
    let acc = global<account::Account>(to);
    aborts_if account::spec_exists_at(to) && !exists<coin::CoinStore<CoinType>>(to) && acc.guid_creation_num + 2 >= account::MAX_GUID_CREATION_NUM;
    aborts_if account::spec_exists_at(to) && !exists<coin::CoinStore<CoinType>>(to) && acc.guid_creation_num + 2 > MAX_U64;
}

schema RegistCoinAbortsIf<CoinType> {
    to: address;
    aborts_if exists<aptos_framework::account::Account>(to);
    aborts_if type_info::type_of<CoinType>() != type_info::type_of<AptosCoin>();
}

schema TransferEnsures<CoinType> {
    to: address;
    account_addr_source: address;
    amount: u64;
    let if_exist_account = exists<account::Account>(to);
    let if_exist_coin = exists<coin::CoinStore<CoinType>>(to);
    let coin_store_to = global<coin::CoinStore<CoinType>>(to);
    let coin_store_source = global<coin::CoinStore<CoinType>>(account_addr_source);
    let post p_coin_store_to = global<coin::CoinStore<CoinType>>(to);
    let post p_coin_store_source = global<coin::CoinStore<CoinType>>(account_addr_source);
    ensures coin_store_source.coin.value - amount == p_coin_store_source.coin.value;
    ensures if_exist_account && if_exist_coin ==> coin_store_to.coin.value + amount == p_coin_store_to.coin.value;
}