Skip to content

Latest commit

 

History

History
3676 lines (2054 loc) · 128 KB

Account.md

File metadata and controls

3676 lines (2054 loc) · 128 KB
Raw

Module 0x1::Account

The module for the account resource that governs every account

use 0x1::Authenticator;
use 0x1::BCS;
use 0x1::CoreAddresses;
use 0x1::Errors;
use 0x1::Event;
use 0x1::Hash;
use 0x1::Math;
use 0x1::Option;
use 0x1::STC;
use 0x1::Signer;
use 0x1::Timestamp;
use 0x1::Token;
use 0x1::TransactionFee;
use 0x1::Vector;

Resource Account

Every account has a Account::Account resource

struct Account has key
Fields
authentication_key: vector<u8>
The current authentication key. This can be different than the key used to create the account
withdrawal_capability: Option::Option<Account::WithdrawCapability>
A withdrawal_capability allows whoever holds this capability to withdraw from the account. At the time of account creation this capability is stored in this option. It can later be "extracted" from this field via extract_withdraw_capability, and can also be restored via restore_withdraw_capability.
key_rotation_capability: Option::Option<Account::KeyRotationCapability>
A key_rotation_capability allows whoever holds this capability the ability to rotate the authentication key for the account. At the time of account creation this capability is stored in this option. It can later be "extracted" from this field via extract_key_rotation_capability, and can also be restored via restore_key_rotation_capability.
withdraw_events: Event::EventHandle<Account::WithdrawEvent>
event handle for account balance withdraw event
deposit_events: Event::EventHandle<Account::DepositEvent>
event handle for account balance deposit event
accept_token_events: Event::EventHandle<Account::AcceptTokenEvent>
Event handle for accept_token event
sequence_number: u64
The current sequence number. Incremented by one each time a transaction is submitted

Resource Balance

A resource that holds the tokens stored in this account

struct Balance<TokenType> has key
Fields
token: Token::Token<TokenType>

Struct WithdrawCapability

The holder of WithdrawCapability for account_address can withdraw Token from account_address/Account::Account/balance. There is at most one WithdrawCapability in existence for a given address.

struct WithdrawCapability has store
Fields
account_address: address

Struct KeyRotationCapability

The holder of KeyRotationCapability for account_address can rotate the authentication key for account_address (i.e., write to account_address/Account::Account/authentication_key). There is at most one KeyRotationCapability in existence for a given address.

struct KeyRotationCapability has store
Fields
account_address: address

Struct WithdrawEvent

Message for balance withdraw event.

struct WithdrawEvent has drop, store
Fields
amount: u128
The amount of Token sent
token_code: Token::TokenCode
The code symbol for the token that was sent
metadata: vector<u8>
Metadata associated with the withdraw

Struct DepositEvent

Message for balance deposit event.

struct DepositEvent has drop, store
Fields
amount: u128
The amount of Token sent
token_code: Token::TokenCode
The code symbol for the token that was sent
metadata: vector<u8>
Metadata associated with the deposit

Struct AcceptTokenEvent

Message for accept token events

struct AcceptTokenEvent has drop, store
Fields
token_code: Token::TokenCode

Resource SignerDelegated

struct SignerDelegated has key
Fields
dummy_field: bool

Struct SignerCapability

struct SignerCapability has store
Fields
addr: address

Resource AutoAcceptToken

struct AutoAcceptToken has key
Fields
enable: bool

Struct RotateAuthKeyEvent

Message for rotate_authentication_key events

struct RotateAuthKeyEvent has drop, store
Fields
account_address: address
new_auth_key: vector<u8>

Struct ExtractWithdrawCapEvent

Message for extract_withdraw_capability events

struct ExtractWithdrawCapEvent has drop, store
Fields
account_address: address

Struct SignerDelegateEvent

Message for SignerDelegate events

struct SignerDelegateEvent has drop, store
Fields
account_address: address

Resource EventStore

struct EventStore has key
Fields
rotate_auth_key_events: Event::EventHandle<Account::RotateAuthKeyEvent>
Event handle for rotate_authentication_key event
extract_withdraw_cap_events: Event::EventHandle<Account::ExtractWithdrawCapEvent>
Event handle for extract_withdraw_capability event
signer_delegate_events: Event::EventHandle<Account::SignerDelegateEvent>
Event handle for signer delegated event

Constants

const MAX_U64: u128 = 18446744073709551615;


const EDEPRECATED_FUNCTION: u64 = 19;


const EPROLOGUE_ACCOUNT_DOES_NOT_EXIST: u64 = 0;

The address bytes length

const ADDRESS_LENGTH: u64 = 16;


const CONTRACT_ACCOUNT_AUTH_KEY_PLACEHOLDER: vector<u8> = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1];


const DUMMY_AUTH_KEY: vector<u8> = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0];


const EADDRESS_AND_AUTH_KEY_MISMATCH: u64 = 105;


const EADDRESS_PUBLIC_KEY_INCONSISTENT: u64 = 104;


const EBAD_TRANSACTION_FEE_TOKEN: u64 = 18;


const ECOIN_DEPOSIT_IS_ZERO: u64 = 15;


const EINSUFFICIENT_BALANCE: u64 = 10;


const EKEY_ROTATION_CAPABILITY_ALREADY_EXTRACTED: u64 = 103;


const EMALFORMED_AUTHENTICATION_KEY: u64 = 102;


const EPROLOGUE_CANT_PAY_GAS_DEPOSIT: u64 = 4;


const EPROLOGUE_INVALID_ACCOUNT_AUTH_KEY: u64 = 1;


const EPROLOGUE_SEQUENCE_NUMBER_TOO_BIG: u64 = 9;


const EPROLOGUE_SEQUENCE_NUMBER_TOO_NEW: u64 = 3;


const EPROLOGUE_SEQUENCE_NUMBER_TOO_OLD: u64 = 2;


const EPROLOGUE_SIGNER_ALREADY_DELEGATED: u64 = 200;


const ERR_SIGNER_ALREADY_DELEGATED: u64 = 107;


const ERR_TOKEN_NOT_ACCEPT: u64 = 106;


const EWITHDRAWAL_CAPABILITY_ALREADY_EXTRACTED: u64 = 101;

Function remove_signer_capability

A one-way action, once SignerCapability is removed from signer, the address cannot send txns anymore. This function can only called once by signer.

public fun remove_signer_capability(signer: &signer): Account::SignerCapability
Implementation 
public fun remove_signer_capability(signer: &signer): SignerCapability
acquires Account, EventStore {
    let signer_addr = Signer::address_of(signer);
    assert!(!is_signer_delegated(signer_addr), Errors::invalid_state(ERR_SIGNER_ALREADY_DELEGATED));

    // set to account auth key to noop.
    {
        let key_rotation_capability = extract_key_rotation_capability(signer);
        rotate_authentication_key_with_capability(&key_rotation_capability, CONTRACT_ACCOUNT_AUTH_KEY_PLACEHOLDER);
        destroy_key_rotation_capability(key_rotation_capability);
        move_to(signer, SignerDelegated {});

        make_event_store_if_not_exist(signer);
        let event_store = borrow_global_mut<EventStore>(signer_addr);
        Event::emit_event<SignerDelegateEvent>(
            &mut event_store.signer_delegate_events,
            SignerDelegateEvent {
                account_address: signer_addr
            }
        );
    };

    let signer_cap = SignerCapability {addr: signer_addr };
    signer_cap
}

Function create_signer_with_cap

public fun create_signer_with_cap(cap: &Account::SignerCapability): signer
Implementation 
public fun create_signer_with_cap(cap: &SignerCapability): signer {
    create_signer(cap.addr)
}

Function destroy_signer_cap

public fun destroy_signer_cap(cap: Account::SignerCapability)
Implementation 
public fun destroy_signer_cap(cap: SignerCapability) {
    let SignerCapability {addr: _} = cap;
}

Function signer_address

public fun signer_address(cap: &Account::SignerCapability): address
Implementation 
public fun signer_address(cap: &SignerCapability): address {
    cap.addr
}

Function is_signer_delegated

public fun is_signer_delegated(addr: address): bool
Implementation 
public fun is_signer_delegated(addr: address): bool {
    exists<SignerDelegated>(addr)
}

Function create_genesis_account

Create an genesis account at new_account_address and return signer. Genesis authentication_key is zero bytes.

public fun create_genesis_account(new_account_address: address): signer
Implementation 
public fun create_genesis_account(
    new_account_address: address,
) :signer {
    Timestamp::assert_genesis();
    let new_account = create_signer(new_account_address);
    make_account(&new_account, DUMMY_AUTH_KEY);
    new_account
}
Specification 
aborts_if !Timestamp::is_genesis();
aborts_if len(DUMMY_AUTH_KEY) != 32;
aborts_if exists<Account>(new_account_address);

Function release_genesis_signer

Release genesis account signer

public fun release_genesis_signer(_genesis_account: signer)
Implementation 
public fun release_genesis_signer(_genesis_account: signer){
}
Specification 
aborts_if false;

Function create_account

Deprecated since @v5

public fun create_account<TokenType: store>(_authentication_key: vector<u8>): address
Implementation 
public fun create_account<TokenType: store>(_authentication_key: vector<u8>): address {
    abort Errors::deprecated(EDEPRECATED_FUNCTION)
}
Specification 
aborts_if true;

Function create_account_with_address

Creates a new account at fresh_address with a balance of zero and empty auth key, the address as init auth key for check transaction. Creating an account at address StarcoinFramework will cause runtime failure as it is a reserved address for the MoveVM.

public fun create_account_with_address<TokenType: store>(fresh_address: address)
Implementation 
public fun create_account_with_address<TokenType: store>(fresh_address: address) acquires Account {
    let new_account = create_signer(fresh_address);
    make_account(&new_account, DUMMY_AUTH_KEY);
    // Make sure all account accept STC.
    if (!STC::is_stc<TokenType>()){
        do_accept_token<STC>(&new_account);
    };
    do_accept_token<TokenType>(&new_account);
}
Specification 
aborts_if exists<Account>(fresh_address);
aborts_if Token::spec_token_code<TokenType>() != Token::spec_token_code<STC>() && exists<Balance<STC>>(fresh_address);
aborts_if exists<Balance<TokenType>>(fresh_address);
ensures exists_at(fresh_address);
ensures exists<Balance<TokenType>>(fresh_address);

Function make_account

fun make_account(new_account: &signer, authentication_key: vector<u8>)
Implementation 
fun make_account(
    new_account: &signer,
    authentication_key: vector<u8>,
) {
    assert!(Vector::length(&authentication_key) == 32, Errors::invalid_argument(EMALFORMED_AUTHENTICATION_KEY));
    let new_account_addr = Signer::address_of(new_account);
    Event::publish_generator(new_account);
    move_to(new_account, Account {
          authentication_key,
          withdrawal_capability: Option::some(
              WithdrawCapability {
                  account_address: new_account_addr
          }),
          key_rotation_capability: Option::some(
              KeyRotationCapability {
                  account_address: new_account_addr
          }),
          withdraw_events: Event::new_event_handle<WithdrawEvent>(new_account),
          deposit_events: Event::new_event_handle<DepositEvent>(new_account),
          accept_token_events: Event::new_event_handle<AcceptTokenEvent>(new_account),
          sequence_number: 0,
    });
    move_to(new_account, AutoAcceptToken{enable: true});
    move_to(new_account, EventStore {
          rotate_auth_key_events: Event::new_event_handle<RotateAuthKeyEvent>(new_account),
          extract_withdraw_cap_events: Event::new_event_handle<ExtractWithdrawCapEvent>(new_account),
          signer_delegate_events: Event::new_event_handle<SignerDelegateEvent>(new_account),
    });
}
Specification 
aborts_if len(authentication_key) != 32;
aborts_if exists<Account>(Signer::address_of(new_account));
aborts_if exists<AutoAcceptToken>(Signer::address_of(new_account));
ensures exists_at(Signer::address_of(new_account));

Function create_signer

fun create_signer(addr: address): signer
Implementation 
native fun create_signer(addr: address): signer;

Function create_account_with_initial_amount

public entry fun create_account_with_initial_amount<TokenType: store>(account: signer, fresh_address: address, _auth_key: vector<u8>, initial_amount: u128)
Implementation 
public entry fun create_account_with_initial_amount<TokenType: store>(account: signer, fresh_address: address, _auth_key: vector<u8>, initial_amount: u128)
acquires Account, Balance, AutoAcceptToken {
    create_account_with_initial_amount_entry<TokenType>(account, fresh_address, initial_amount);
}
Specification 
pragma verify = false;

Function create_account_with_initial_amount_v2

public entry fun create_account_with_initial_amount_v2<TokenType: store>(account: signer, fresh_address: address, initial_amount: u128)
Implementation 
public entry fun create_account_with_initial_amount_v2<TokenType: store>(account: signer, fresh_address: address, initial_amount: u128)
acquires Account, Balance, AutoAcceptToken {
    create_account_with_initial_amount_entry<TokenType>(account, fresh_address, initial_amount);
}
Specification 
pragma verify = false;

Function create_account_with_initial_amount_entry

public entry fun create_account_with_initial_amount_entry<TokenType: store>(account: signer, fresh_address: address, initial_amount: u128)
Implementation 
public entry fun create_account_with_initial_amount_entry<TokenType: store>(account: signer, fresh_address: address, initial_amount: u128)
acquires Account, Balance, AutoAcceptToken {
    create_account_with_address<TokenType>(fresh_address);
    if (initial_amount > 0) {
        pay_from<TokenType>(&account, fresh_address, initial_amount);
    };
}

Function create_delegate_account

Generate an new address and create a new account, then delegate the account and return the new account address and SignerCapability

public fun create_delegate_account(sender: &signer): (address, Account::SignerCapability)
Implementation 
public fun create_delegate_account(sender: &signer) : (address, SignerCapability) acquires Balance, Account, EventStore {
    let sender_address = Signer::address_of(sender);
    let sequence_number = Self::sequence_number(sender_address);
    // use stc balance as part of seed, just for new address more random.
    let stc_balance = Self::balance<STC>(sender_address);

    let seed_bytes = BCS::to_bytes(&sender_address);
    Vector::append(&mut seed_bytes, BCS::to_bytes(&sequence_number));
    Vector::append(&mut seed_bytes, BCS::to_bytes(&stc_balance));

    let seed_hash = Hash::sha3_256(seed_bytes);
    let i = 0;
    let address_bytes = Vector::empty();
    while (i < ADDRESS_LENGTH) {
        Vector::push_back(&mut address_bytes, *Vector::borrow(&seed_hash,i));
        i = i + 1;
    };
    let new_address = BCS::to_address(address_bytes);
    Self::create_account_with_address<STC>(new_address);
    let new_signer = Self::create_signer(new_address);
    (new_address, Self::remove_signer_capability(&new_signer))
}
Specification 
pragma verify = false;

Function deposit_to_self

Deposits the to_deposit token into the self's account balance

public fun deposit_to_self<TokenType: store>(account: &signer, to_deposit: Token::Token<TokenType>)
Implementation 
public fun deposit_to_self<TokenType: store>(account: &signer, to_deposit: Token<TokenType>)
acquires Account, Balance, AutoAcceptToken {
    let account_address = Signer::address_of(account);
    if (!is_accepts_token<TokenType>(account_address)){
        do_accept_token<TokenType>(account);
    };
    deposit(account_address, to_deposit);
}
Specification 
aborts_if to_deposit.value == 0;
let is_accepts_token = exists<Balance<TokenType>>(Signer::address_of(account));
aborts_if is_accepts_token && global<Balance<TokenType>>(Signer::address_of(account)).token.value + to_deposit.value > max_u128();
aborts_if !exists<Account>(Signer::address_of(account));
ensures exists<Balance<TokenType>>(Signer::address_of(account));

Function deposit

Deposits the to_deposit token into the receiver's account balance with the no metadata It's a reverse operation of withdraw.

public fun deposit<TokenType: store>(receiver: address, to_deposit: Token::Token<TokenType>)
Implementation 
public fun deposit<TokenType: store>(
    receiver: address,
    to_deposit: Token<TokenType>,
) acquires Account, Balance, AutoAcceptToken {
    deposit_with_metadata<TokenType>(receiver, to_deposit, x"")
}
Specification 
include DepositWithMetadataAbortsIf<TokenType>;

Function deposit_with_metadata

Deposits the to_deposit token into the receiver's account balance with the attached metadata It's a reverse operation of withdraw_with_metadata.

public fun deposit_with_metadata<TokenType: store>(receiver: address, to_deposit: Token::Token<TokenType>, metadata: vector<u8>)
Implementation 
public fun deposit_with_metadata<TokenType: store>(
    receiver: address,
    to_deposit: Token<TokenType>,
    metadata: vector<u8>,
) acquires Account, Balance, AutoAcceptToken {

    if (!exists_at(receiver)) {
        create_account_with_address<TokenType>(receiver);
    };

    try_accept_token<TokenType>(receiver);

    let deposit_value = Token::value(&to_deposit);
    if (deposit_value > 0u128) {
        // Deposit the `to_deposit` token
        deposit_to_balance<TokenType>(borrow_global_mut<Balance<TokenType>>(receiver), to_deposit);

        // emit deposit event
        emit_account_deposit_event<TokenType>(receiver, deposit_value, metadata);
    } else {
        Token::destroy_zero(to_deposit);
    };
}
Specification 
include DepositWithMetadataAbortsIf<TokenType>;
ensures exists<Balance<TokenType>>(receiver);
ensures old(global<Balance<TokenType>>(receiver)).token.value + to_deposit.value == global<Balance<TokenType>>(receiver).token.value;


schema DepositWithMetadataAbortsIf<TokenType> {
    receiver: address;
    to_deposit: Token<TokenType>;
    aborts_if to_deposit.value == 0;
    aborts_if !exists<Account>(receiver);
    aborts_if !exists<Balance<TokenType>>(receiver);
    aborts_if global<Balance<TokenType>>(receiver).token.value + to_deposit.value > max_u128();
}

Function deposit_to_balance

Helper to deposit amount to the given account balance

fun deposit_to_balance<TokenType: store>(balance: &mut Account::Balance<TokenType>, token: Token::Token<TokenType>)
Implementation 
fun deposit_to_balance<TokenType: store>(balance: &mut Balance<TokenType>, token: Token::Token<TokenType>) {
    Token::deposit(&mut balance.token, token)
}
Specification 
aborts_if balance.token.value + token.value > MAX_U128;

Function withdraw_from_balance_v2

public(friend) fun withdraw_from_balance_v2<TokenType: store>(sender: address, amount: u128): Token::Token<TokenType>
Implementation 
public(friend) fun withdraw_from_balance_v2<TokenType: store>(sender:address, amount: u128): Token<TokenType> acquires Balance {
    let balance = borrow_global_mut<Balance<TokenType>>(sender);
    Token::withdraw(&mut balance.token, amount)
}

Function set_sequence_number

public(friend) fun set_sequence_number(sender: address, sequence_number: u64)
Implementation 
public (friend) fun set_sequence_number(sender: address, sequence_number: u64) acquires Account {
    let account = borrow_global_mut<Account>(sender);
    account.sequence_number = sequence_number;
}

Function set_authentication_key

public(friend) fun set_authentication_key(sender: address, auth_key: vector<u8>)
Implementation 
public (friend) fun set_authentication_key(sender:address,auth_key:vector<u8>) acquires Account{
    let account = borrow_global_mut<Account>(sender);
    account.authentication_key = auth_key;
}

Function withdraw_from_balance

Helper to withdraw amount from the given account balance and return the withdrawn Token

public fun withdraw_from_balance<TokenType: store>(balance: &mut Account::Balance<TokenType>, amount: u128): Token::Token<TokenType>
Implementation 
public fun withdraw_from_balance<TokenType: store>(balance: &mut Balance<TokenType>, amount: u128): Token<TokenType>{
    Token::withdraw(&mut balance.token, amount)
}
Specification 
aborts_if balance.token.value < amount;

Function withdraw

Withdraw amount Token from the account balance

public fun withdraw<TokenType: store>(account: &signer, amount: u128): Token::Token<TokenType>
Implementation 
public fun withdraw<TokenType: store>(account: &signer, amount: u128): Token<TokenType>
acquires Account, Balance {
    withdraw_with_metadata<TokenType>(account, amount, x"")
}
Specification 
aborts_if !exists<Balance<TokenType>>(Signer::address_of(account));
aborts_if !exists<Account>(Signer::address_of(account));
aborts_if global<Balance<TokenType>>(Signer::address_of(account)).token.value < amount;
aborts_if Option::is_none(global<Account>(Signer::address_of(account)).withdrawal_capability);

Function withdraw_with_metadata

Withdraw amount tokens from signer with given metadata.

public fun withdraw_with_metadata<TokenType: store>(account: &signer, amount: u128, metadata: vector<u8>): Token::Token<TokenType>
Implementation 
public fun withdraw_with_metadata<TokenType: store>(account: &signer, amount: u128, metadata: vector<u8>): Token<TokenType>
acquires Account, Balance {
    let sender_addr = Signer::address_of(account);
    let sender_balance = borrow_global_mut<Balance<TokenType>>(sender_addr);
    // The sender_addr has delegated the privilege to withdraw from her account elsewhere--abort.
    assert!(!delegated_withdraw_capability(sender_addr), Errors::invalid_state(EWITHDRAWAL_CAPABILITY_ALREADY_EXTRACTED));
    if (amount == 0){
        return Token::zero()
    };
    emit_account_withdraw_event<TokenType>(sender_addr, amount, metadata);
    // The sender_addr has retained her withdrawal privileges--proceed.
    withdraw_from_balance<TokenType>(sender_balance, amount)
}
Specification 
aborts_if !exists<Balance<TokenType>>(Signer::address_of(account));
aborts_if !exists<Account>(Signer::address_of(account));
aborts_if global<Balance<TokenType>>(Signer::address_of(account)).token.value < amount;
aborts_if Option::is_none(global<Account>(Signer::address_of(account)).withdrawal_capability);


fun spec_withdraw<TokenType>(account: signer, amount: u128): Token<TokenType> {
   Token<TokenType> { value: amount }
}

Function withdraw_with_capability

Withdraw amount Token from the account under cap.account_address with no metadata

public fun withdraw_with_capability<TokenType: store>(cap: &Account::WithdrawCapability, amount: u128): Token::Token<TokenType>
Implementation 
public fun withdraw_with_capability<TokenType: store>(
    cap: &WithdrawCapability, amount: u128
): Token<TokenType> acquires Balance, Account {
    withdraw_with_capability_and_metadata<TokenType>(cap, amount, x"")
}
Specification 
aborts_if !exists<Balance<TokenType>>(cap.account_address);
aborts_if !exists<Account>(cap.account_address);
aborts_if global<Balance<TokenType>>(cap.account_address).token.value < amount;

Function withdraw_with_capability_and_metadata

Withdraw amount Token from the account under cap.account_address with metadata

public fun withdraw_with_capability_and_metadata<TokenType: store>(cap: &Account::WithdrawCapability, amount: u128, metadata: vector<u8>): Token::Token<TokenType>
Implementation 
public fun withdraw_with_capability_and_metadata<TokenType: store>(
    cap: &WithdrawCapability, amount: u128, metadata: vector<u8>
): Token<TokenType> acquires Balance, Account {
    let balance = borrow_global_mut<Balance<TokenType>>(cap.account_address);
    emit_account_withdraw_event<TokenType>(cap.account_address, amount, metadata);
    withdraw_from_balance<TokenType>(balance , amount)
}
Specification 
aborts_if !exists<Balance<TokenType>>(cap.account_address);
aborts_if !exists<Account>(cap.account_address);
aborts_if global<Balance<TokenType>>(cap.account_address).token.value < amount;

Function extract_withdraw_capability

Return a unique capability granting permission to withdraw from the sender's account balance.

public fun extract_withdraw_capability(sender: &signer): Account::WithdrawCapability
Implementation 
public fun extract_withdraw_capability(
    sender: &signer
): WithdrawCapability acquires Account, EventStore {
    let sender_addr = Signer::address_of(sender);
    // Abort if we already extracted the unique withdraw capability for this account.
    assert!(!delegated_withdraw_capability(sender_addr), Errors::invalid_state(EWITHDRAWAL_CAPABILITY_ALREADY_EXTRACTED));

    make_event_store_if_not_exist(sender);
    let event_store = borrow_global_mut<EventStore>(sender_addr);
    Event::emit_event<ExtractWithdrawCapEvent>(
        &mut event_store.extract_withdraw_cap_events,
        ExtractWithdrawCapEvent {
            account_address: sender_addr,
        }
    );
    let account = borrow_global_mut<Account>(sender_addr);
    Option::extract(&mut account.withdrawal_capability)
}
Specification 
aborts_if !exists<Account>(Signer::address_of(sender));
aborts_if Option::is_none(global<Account>( Signer::address_of(sender)).withdrawal_capability);

Function restore_withdraw_capability

Return the withdraw capability to the account it originally came from

public fun restore_withdraw_capability(cap: Account::WithdrawCapability)
Implementation 
public fun restore_withdraw_capability(cap: WithdrawCapability)
   acquires Account {
       let account = borrow_global_mut<Account>(cap.account_address);
       Option::fill(&mut account.withdrawal_capability, cap)
}
Specification 
aborts_if Option::is_some(global<Account>(cap.account_address).withdrawal_capability);
aborts_if !exists<Account>(cap.account_address);

Function emit_account_withdraw_event

fun emit_account_withdraw_event<TokenType: store>(account: address, amount: u128, metadata: vector<u8>)
Implementation 
fun emit_account_withdraw_event<TokenType: store>(account: address, amount: u128, metadata: vector<u8>)
acquires Account {
    // emit withdraw event
    let account = borrow_global_mut<Account>(account);

    Event::emit_event<WithdrawEvent>(&mut account.withdraw_events, WithdrawEvent {
        amount,
        token_code: Token::token_code<TokenType>(),
        metadata,
    });
}
Specification 
aborts_if !exists<Account>(account);

Function emit_account_deposit_event

fun emit_account_deposit_event<TokenType: store>(account: address, amount: u128, metadata: vector<u8>)
Implementation 
fun emit_account_deposit_event<TokenType: store>(account: address, amount: u128, metadata: vector<u8>)
acquires Account {
    // emit withdraw event
    let account = borrow_global_mut<Account>(account);

    Event::emit_event<DepositEvent>(&mut account.deposit_events, DepositEvent {
        amount,
        token_code: Token::token_code<TokenType>(),
        metadata,
    });
}
Specification 
aborts_if !exists<Account>(account);

Function pay_from_capability

Withdraws amount Token using the passed in WithdrawCapability, and deposits it into the payee's account balance. Creates the payee account if it doesn't exist.

public fun pay_from_capability<TokenType: store>(cap: &Account::WithdrawCapability, payee: address, amount: u128, metadata: vector<u8>)
Implementation 
public fun pay_from_capability<TokenType: store>(
    cap: &WithdrawCapability,
    payee: address,
    amount: u128,
    metadata: vector<u8>,
) acquires Account, Balance, AutoAcceptToken {
    let tokens = withdraw_with_capability_and_metadata<TokenType>(cap, amount, *&metadata);
    deposit_with_metadata<TokenType>(
        payee,
        tokens,
        metadata,
    );
}
Specification 
aborts_if !exists<Balance<TokenType>>(cap.account_address);
aborts_if !exists<Account>(cap.account_address);
aborts_if global<Balance<TokenType>>(cap.account_address).token.value < amount;
aborts_if amount == 0;
aborts_if !exists<Account>(payee);
aborts_if !exists<Balance<TokenType>>(payee);
aborts_if cap.account_address != payee && global<Balance<TokenType>>(payee).token.value + amount > MAX_U128;

Function pay_from_with_metadata

Withdraw amount Token from the transaction sender's account balance and send the token to the payee address with the attached metadata Creates the payee account if it does not exist

public fun pay_from_with_metadata<TokenType: store>(account: &signer, payee: address, amount: u128, metadata: vector<u8>)
Implementation 
public fun pay_from_with_metadata<TokenType: store>(
    account: &signer,
    payee: address,
    amount: u128,
    metadata: vector<u8>,
) acquires Account, Balance, AutoAcceptToken {
    let tokens = withdraw_with_metadata<TokenType>(account, amount, *&metadata);
    deposit_with_metadata<TokenType>(
        payee,
        tokens,
        metadata,
    );
}
Specification 
aborts_if !exists<Balance<TokenType>>(Signer::address_of(account));
aborts_if !exists<Account>(Signer::address_of(account));
aborts_if global<Balance<TokenType>>(Signer::address_of(account)).token.value < amount;
aborts_if Option::is_none(global<Account>(Signer::address_of(account)).withdrawal_capability);
aborts_if amount == 0;
aborts_if !exists<Account>(payee);
aborts_if !exists<Balance<TokenType>>(payee);
aborts_if Signer::address_of(account) != payee && global<Balance<TokenType>>(payee).token.value + amount > max_u128();


schema DepositWithPayerAndMetadataAbortsIf<TokenType> {
    payer: address;
    payee: address;
    to_deposit: Token<TokenType>;
    aborts_if to_deposit.value == 0;
    aborts_if !exists<Account>(payer);
    aborts_if !exists<Account>(payee);
    aborts_if !exists<Balance<TokenType>>(payee);
    aborts_if global<Balance<TokenType>>(payee).token.value + to_deposit.value > max_u128();
}

Function pay_from

Withdraw amount Token from the transaction sender's account balance and send the token to the payee address Creates the payee account if it does not exist

public fun pay_from<TokenType: store>(account: &signer, payee: address, amount: u128)
Implementation 
public fun pay_from<TokenType: store>(
    account: &signer,
    payee: address,
    amount: u128
) acquires Account, Balance, AutoAcceptToken {
    pay_from_with_metadata<TokenType>(account, payee, amount, x"");
}
Specification 
aborts_if !exists<Balance<TokenType>>(Signer::address_of(account));
aborts_if !exists<Account>(Signer::address_of(account));
aborts_if global<Balance<TokenType>>(Signer::address_of(account)).token.value < amount;
aborts_if Option::is_none(global<Account>(Signer::address_of(account)).withdrawal_capability);
aborts_if amount == 0;
aborts_if !exists<Account>(payee);
aborts_if !exists<Balance<TokenType>>(payee);
aborts_if Signer::address_of(account) != payee && global<Balance<TokenType>>(payee).token.value + amount > max_u128();

Function rotate_authentication_key_with_capability

Rotate the authentication key for the account under cap.account_address

public fun rotate_authentication_key_with_capability(cap: &Account::KeyRotationCapability, new_authentication_key: vector<u8>)
Implementation 
public fun rotate_authentication_key_with_capability(
    cap: &KeyRotationCapability,
    new_authentication_key: vector<u8>,
) acquires Account  {
    let sender_account_resource = borrow_global_mut<Account>(cap.account_address);
    // Don't allow rotating to clearly invalid key
    assert!(Vector::length(&new_authentication_key) == 32, Errors::invalid_argument(EMALFORMED_AUTHENTICATION_KEY));
    sender_account_resource.authentication_key = new_authentication_key;
}
Specification 
aborts_if !exists<Account>(cap.account_address);
aborts_if len(new_authentication_key) != 32;
ensures global<Account>(cap.account_address).authentication_key == new_authentication_key;


fun spec_rotate_authentication_key_with_capability(addr: address, new_authentication_key: vector<u8>): bool {
   global<Account>(addr).authentication_key == new_authentication_key
}

Function extract_key_rotation_capability

Return a unique capability granting permission to rotate the sender's authentication key

public fun extract_key_rotation_capability(account: &signer): Account::KeyRotationCapability
Implementation 
public fun extract_key_rotation_capability(account: &signer): KeyRotationCapability
acquires Account {
    let account_address = Signer::address_of(account);
    // Abort if we already extracted the unique key rotation capability for this account.
    assert!(!delegated_key_rotation_capability(account_address), Errors::invalid_state(EKEY_ROTATION_CAPABILITY_ALREADY_EXTRACTED));
    let account = borrow_global_mut<Account>(account_address);
    Option::extract(&mut account.key_rotation_capability)
}
Specification 
aborts_if !exists<Account>(Signer::address_of(account));
aborts_if Option::is_none(global<Account>(Signer::address_of(account)).key_rotation_capability);

Function restore_key_rotation_capability

Return the key rotation capability to the account it originally came from

public fun restore_key_rotation_capability(cap: Account::KeyRotationCapability)
Implementation 
public fun restore_key_rotation_capability(cap: KeyRotationCapability)
acquires Account {
    let account = borrow_global_mut<Account>(cap.account_address);
    Option::fill(&mut account.key_rotation_capability, cap)
}
Specification 
aborts_if Option::is_some(global<Account>(cap.account_address).key_rotation_capability);
aborts_if !exists<Account>(cap.account_address);

Function destroy_key_rotation_capability

public fun destroy_key_rotation_capability(cap: Account::KeyRotationCapability)
Implementation 
public fun destroy_key_rotation_capability(cap: KeyRotationCapability) {
    let KeyRotationCapability {account_address: _} = cap;
}

Function rotate_authentication_key

public entry fun rotate_authentication_key(account: signer, new_key: vector<u8>)
Implementation 
public entry fun rotate_authentication_key(account: signer, new_key: vector<u8>) acquires Account, EventStore {
    rotate_authentication_key_entry(account, new_key);
}
Specification 
pragma verify = false;

Function rotate_authentication_key_entry

public entry fun rotate_authentication_key_entry(account: signer, new_key: vector<u8>)
Implementation 
public entry fun rotate_authentication_key_entry(account: signer, new_key: vector<u8>) acquires Account, EventStore {
    do_rotate_authentication_key(&account, new_key);
}

Function do_rotate_authentication_key

public fun do_rotate_authentication_key(account: &signer, new_key: vector<u8>)
Implementation 
public fun do_rotate_authentication_key(account: &signer, new_key: vector<u8>) acquires Account, EventStore {
    let key_rotation_capability = extract_key_rotation_capability(account);
    rotate_authentication_key_with_capability(&key_rotation_capability, copy new_key);
    restore_key_rotation_capability(key_rotation_capability);

    make_event_store_if_not_exist(account);
    let signer_addr = Signer::address_of(account);
    let event_store = borrow_global_mut<EventStore>(signer_addr);
    Event::emit_event<RotateAuthKeyEvent>(
        &mut event_store.rotate_auth_key_events,
        RotateAuthKeyEvent {
            account_address: signer_addr,
            new_auth_key: new_key,
        }
    );
}

Function balance_for

Helper to return the u128 value of the balance for account

fun balance_for<TokenType: store>(balance: &Account::Balance<TokenType>): u128
Implementation 
fun balance_for<TokenType: store>(balance: &Balance<TokenType>): u128 {
    Token::value<TokenType>(&balance.token)
}
Specification 
aborts_if false;

Function balance

Return the current TokenType balance of the account at addr.

public fun balance<TokenType: store>(addr: address): u128
Implementation 
public fun balance<TokenType: store>(addr: address): u128 acquires Balance {
    if (exists<Balance<TokenType>>(addr)) {
        balance_for(borrow_global<Balance<TokenType>>(addr))
    } else {
        0u128
    }
}

Function do_accept_token

Add a balance of Token type to the sending account.

public fun do_accept_token<TokenType: store>(account: &signer)
Implementation 
public fun do_accept_token<TokenType: store>(account: &signer) acquires Account {
    move_to(account, Balance<TokenType>{ token: Token::zero<TokenType>() });
    let token_code = Token::token_code<TokenType>();
    // Load the sender's account
    let sender_account_ref = borrow_global_mut<Account>(Signer::address_of(account));
    // Log a sent event
    Event::emit_event<AcceptTokenEvent>(
        &mut sender_account_ref.accept_token_events,
        AcceptTokenEvent {
            token_code:  token_code,
        },
    );
}
Specification 
aborts_if exists<Balance<TokenType>>(Signer::address_of(account));
aborts_if !exists<Account>(Signer::address_of(account));

Function accept_token

public entry fun accept_token<TokenType: store>(account: signer)
Implementation 
public entry fun accept_token<TokenType: store>(account: signer) acquires Account {
    accept_token_entry<TokenType>(account);
}
Specification 
pragma verify = false;

Function accept_token_entry

public entry fun accept_token_entry<TokenType: store>(account: signer)
Implementation 
public entry fun accept_token_entry<TokenType: store>(account: signer) acquires Account {
    do_accept_token<TokenType>(&account);
}

Function is_accepts_token

This is a alias of is_accept_token

public fun is_accepts_token<TokenType: store>(addr: address): bool
Implementation 
public fun is_accepts_token<TokenType: store>(addr: address): bool acquires AutoAcceptToken {
    Self::is_accept_token<TokenType>(addr)
}
Specification 
aborts_if false;

aborts_if false;

Function is_accept_token

Return whether the account at addr accept Token type tokens

public fun is_accept_token<TokenType: store>(addr: address): bool
Implementation 
public fun is_accept_token<TokenType: store>(addr: address): bool acquires AutoAcceptToken {
    if (can_auto_accept_token(addr)) {
        true
    } else {
        exists<Balance<TokenType>>(addr)
    }
}
Specification 
aborts_if false;

Function can_auto_accept_token

Check whether the address can auto accept token.

public fun can_auto_accept_token(addr: address): bool
Implementation 
public fun can_auto_accept_token(addr: address): bool acquires AutoAcceptToken {
    if (exists<AutoAcceptToken>(addr)) {
        borrow_global<AutoAcceptToken>(addr).enable
    } else {
        false
    }
}

Function set_auto_accept_token_entry

public entry fun set_auto_accept_token_entry(account: signer, enable: bool)
Implementation 
public entry fun set_auto_accept_token_entry(account: signer, enable: bool) acquires AutoAcceptToken {
    set_auto_accept_token(&account, enable);
}

Function set_auto_accept_token

Configure whether auto-accept tokens.

public fun set_auto_accept_token(account: &signer, enable: bool)
Implementation 
public fun set_auto_accept_token(account: &signer, enable: bool) acquires AutoAcceptToken {
    let addr = Signer::address_of(account);
    if (exists<AutoAcceptToken>(addr)) {
        let config = borrow_global_mut<AutoAcceptToken>(addr);
        config.enable = enable;
    } else {
        move_to(account, AutoAcceptToken{enable});
    };
}
Specification 
aborts_if false;

Function try_accept_token

try to accept token for addr.

fun try_accept_token<TokenType: store>(addr: address)
Implementation 
fun try_accept_token<TokenType: store>(addr: address) acquires AutoAcceptToken, Account {
    if (!exists<Balance<TokenType>>(addr)) {
        if (can_auto_accept_token(addr)) {
            let signer = create_signer(addr);
            do_accept_token<TokenType>(&signer);
        }else{
            abort Errors::not_published(ERR_TOKEN_NOT_ACCEPT)
        }
    };
}
Specification 
aborts_if false;

Function sequence_number_for_account

Helper to return the sequence number field for given account

fun sequence_number_for_account(account: &Account::Account): u64
Implementation 
fun sequence_number_for_account(account: &Account): u64 {
    account.sequence_number
}

Function sequence_number

Return the current sequence number at addr

public fun sequence_number(addr: address): u64
Implementation 
public fun sequence_number(addr: address): u64 acquires Account {
    sequence_number_for_account(borrow_global<Account>(addr))
}
Specification 
aborts_if !exists<Account>(addr);

Function authentication_key

Return the authentication key for this account

public fun authentication_key(addr: address): vector<u8>
Implementation 
public fun authentication_key(addr: address): vector<u8> acquires Account {
    *&borrow_global<Account>(addr).authentication_key
}
Specification 
aborts_if !exists<Account>(addr);

Function delegated_key_rotation_capability

Return true if the account at addr has delegated its key rotation capability

public fun delegated_key_rotation_capability(addr: address): bool
Implementation 
public fun delegated_key_rotation_capability(addr: address): bool
acquires Account {
    Option::is_none(&borrow_global<Account>(addr).key_rotation_capability)
}
Specification 
aborts_if !exists<Account>(addr);

Function delegated_withdraw_capability

Return true if the account at addr has delegated its withdraw capability

public fun delegated_withdraw_capability(addr: address): bool
Implementation 
public fun delegated_withdraw_capability(addr: address): bool
acquires Account {
    Option::is_none(&borrow_global<Account>(addr).withdrawal_capability)
}
Specification 
aborts_if !exists<Account>(addr);

Function withdraw_capability_address

Return a reference to the address associated with the given withdraw capability

public fun withdraw_capability_address(cap: &Account::WithdrawCapability): &address
Implementation 
public fun withdraw_capability_address(cap: &WithdrawCapability): &address {
    &cap.account_address
}
Specification 
aborts_if false;

Function key_rotation_capability_address

Return a reference to the address associated with the given key rotation capability

public fun key_rotation_capability_address(cap: &Account::KeyRotationCapability): &address
Implementation 
public fun key_rotation_capability_address(cap: &KeyRotationCapability): &address {
    &cap.account_address
}
Specification 
aborts_if false;

Function exists_at

Checks if an account exists at check_addr

public fun exists_at(check_addr: address): bool
Implementation 
public fun exists_at(check_addr: address): bool {
    exists<Account>(check_addr)
}
Specification 
aborts_if false;

Function is_dummy_auth_key

fun is_dummy_auth_key(account: &Account::Account): bool
Implementation 
fun is_dummy_auth_key(account: &Account): bool {
    *&account.authentication_key == DUMMY_AUTH_KEY
}

Function is_dummy_auth_key_v2

public fun is_dummy_auth_key_v2(account: address): bool
Implementation 
public fun is_dummy_auth_key_v2(account: address): bool acquires Account {
    let account = borrow_global_mut<Account>(account);
    account.authentication_key == DUMMY_AUTH_KEY
}

Function txn_prologue

The prologue is invoked at the beginning of every transaction It verifies:

  • The account's auth key matches the transaction's public key
  • That the account has enough balance to pay for all of the gas
  • That the sequence number matches the transaction's sequence key
public fun txn_prologue<TokenType: store>(account: &signer, txn_sender: address, txn_sequence_number: u64, txn_authentication_key_preimage: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64)
Implementation 
public fun txn_prologue<TokenType: store>(
    account: &signer,
    txn_sender: address,
    txn_sequence_number: u64,
    txn_authentication_key_preimage: vector<u8>,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
) acquires Account, Balance {
    txn_prologue_v2<TokenType>(
        account,
        txn_sender,
        txn_sequence_number,
        txn_authentication_key_preimage,
        txn_gas_price,
        txn_max_gas_units,
        1,
        1,
    )
}
Specification 
aborts_if Signer::address_of(account) != CoreAddresses::GENESIS_ADDRESS();
aborts_if !exists<Account>(txn_sender);
aborts_if global<Account>(txn_sender).authentication_key == DUMMY_AUTH_KEY && Authenticator::spec_derived_address(Hash::sha3_256(txn_authentication_key_preimage)) != txn_sender;
aborts_if global<Account>(txn_sender).authentication_key != DUMMY_AUTH_KEY && Hash::sha3_256(txn_authentication_key_preimage) != global<Account>(txn_sender).authentication_key;
aborts_if txn_sequence_number < global<Account>(txn_sender).sequence_number;

Function txn_prologue_v2

public fun txn_prologue_v2<TokenType: store>(account: &signer, txn_sender: address, txn_sequence_number: u64, txn_authentication_key_preimage: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, stc_price: u128, stc_price_scaling: u128)
Implementation 
public fun txn_prologue_v2<TokenType: store>(
    account: &signer,
    txn_sender: address,
    txn_sequence_number: u64,
    txn_authentication_key_preimage: vector<u8>,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    stc_price: u128,
    stc_price_scaling: u128
) acquires Account, Balance {
    CoreAddresses::assert_genesis_address(account);

    // Verify that the transaction sender's account exists
    assert!(exists_at(txn_sender), Errors::requires_address(EPROLOGUE_ACCOUNT_DOES_NOT_EXIST));
    // Verify the account has not delegate its signer cap.
    assert!(!is_signer_delegated(txn_sender), Errors::invalid_state(EPROLOGUE_SIGNER_ALREADY_DELEGATED));

    // Load the transaction sender's account
    let sender_account = borrow_global_mut<Account>(txn_sender);

    if (is_dummy_auth_key(sender_account)){
        // if sender's auth key is empty, use address as auth key for check transaction.
        assert!(
            Authenticator::derived_address(Hash::sha3_256(txn_authentication_key_preimage)) == txn_sender,
            Errors::invalid_argument(EPROLOGUE_INVALID_ACCOUNT_AUTH_KEY)
        );
    }else{
        // Check that the hash of the transaction's public key matches the account's auth key
        assert!(
            Hash::sha3_256(txn_authentication_key_preimage) == *&sender_account.authentication_key,
            Errors::invalid_argument(EPROLOGUE_INVALID_ACCOUNT_AUTH_KEY)
        );
    };
    // Check that the account has enough balance for all of the gas
    let (max_transaction_fee_stc,max_transaction_fee_token) = transaction_fee_simulate(txn_gas_price,txn_max_gas_units,0, stc_price, stc_price_scaling);
    assert!(
        max_transaction_fee_stc <= MAX_U64,
        Errors::invalid_argument(EPROLOGUE_CANT_PAY_GAS_DEPOSIT),
    );
    if (max_transaction_fee_stc > 0) {
        assert!(
            (txn_sequence_number as u128) < MAX_U64,
            Errors::limit_exceeded(EPROLOGUE_SEQUENCE_NUMBER_TOO_BIG)
        );
        let balance_amount_token = balance<TokenType>(txn_sender);
        assert!(balance_amount_token >= max_transaction_fee_token, Errors::invalid_argument(EPROLOGUE_CANT_PAY_GAS_DEPOSIT));
        if (!is_stc<TokenType>()){
            let balance_amount_stc= balance<STC>(CoreAddresses::GENESIS_ADDRESS());
            assert!(balance_amount_stc >= max_transaction_fee_stc, Errors::invalid_argument(EPROLOGUE_CANT_PAY_GAS_DEPOSIT));
        }
    };
    // Check that the transaction sequence number matches the sequence number of the account
    assert!(txn_sequence_number >= sender_account.sequence_number, Errors::invalid_argument(EPROLOGUE_SEQUENCE_NUMBER_TOO_OLD));
    assert!(txn_sequence_number == sender_account.sequence_number, Errors::invalid_argument(EPROLOGUE_SEQUENCE_NUMBER_TOO_NEW));

}

Function txn_epilogue

The epilogue is invoked at the end of transactions. It collects gas and bumps the sequence number

public fun txn_epilogue<TokenType: store>(account: &signer, txn_sender: address, txn_sequence_number: u64, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64)
Implementation 
public fun txn_epilogue<TokenType: store>(
    account: &signer,
    txn_sender: address,
    txn_sequence_number: u64,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    gas_units_remaining: u64,
) acquires Account, Balance {
    txn_epilogue_v3<TokenType>(account, txn_sender, txn_sequence_number, Vector::empty(), txn_gas_price, txn_max_gas_units, gas_units_remaining,1,1)
}
Specification 
pragma verify = false;

Function transaction_fee_simulate

public fun transaction_fee_simulate(txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64, stc_price: u128, stc_price_scaling: u128): (u128, u128)
Implementation 
public fun transaction_fee_simulate(
    txn_gas_price:u64,
    txn_max_gas_units: u64,
    gas_units_remaining:u64,
    stc_price: u128,
    stc_price_scaling: u128,
): (u128, u128){
    let transaction_fee_stc =(txn_gas_price * (txn_max_gas_units - gas_units_remaining) as u128);
    let transaction_fee_token= Math::mul_div((transaction_fee_stc as u128), stc_price, stc_price_scaling);
    transaction_fee_token = if (transaction_fee_token == 0 && transaction_fee_stc > 0 ) { 1 } else { transaction_fee_token};
    (transaction_fee_stc, transaction_fee_token)
}

Function txn_epilogue_v2

The epilogue is invoked at the end of transactions. It collects gas and bumps the sequence number

public fun txn_epilogue_v2<TokenType: store>(account: &signer, txn_sender: address, txn_sequence_number: u64, txn_authentication_key_preimage: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64)
Implementation 
public fun txn_epilogue_v2<TokenType: store>(
    account: &signer,
    txn_sender: address,
    txn_sequence_number: u64,
    txn_authentication_key_preimage: vector<u8>,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    gas_units_remaining: u64,
) acquires Account, Balance {
    txn_epilogue_v3<TokenType>(
        account,
        txn_sender,
        txn_sequence_number,
        txn_authentication_key_preimage,
        txn_gas_price,
        txn_max_gas_units,
        gas_units_remaining,1,1)
}
Specification 
pragma verify = false;
aborts_if Signer::address_of(account) != CoreAddresses::GENESIS_ADDRESS();
aborts_if !exists<Account>(txn_sender);
aborts_if !exists<Balance<TokenType>>(txn_sender);
aborts_if txn_max_gas_units < gas_units_remaining;
let transaction_fee_amount = txn_gas_price * (txn_max_gas_units - gas_units_remaining);
aborts_if transaction_fee_amount > max_u128();
aborts_if global<Balance<TokenType>>(txn_sender).token.value < transaction_fee_amount;
aborts_if txn_sequence_number + 1 > max_u64();
aborts_if txn_gas_price * (txn_max_gas_units - gas_units_remaining) > 0 &&
          global<Balance<TokenType>>(txn_sender).token.value  < txn_gas_price * (txn_max_gas_units - gas_units_remaining);
aborts_if txn_gas_price * (txn_max_gas_units - gas_units_remaining) > 0 &&
          !exists<TransactionFee::TransactionFee<TokenType>>(CoreAddresses::GENESIS_ADDRESS());
aborts_if txn_gas_price * (txn_max_gas_units - gas_units_remaining) > 0 &&
          global<TransactionFee::TransactionFee<TokenType>>(CoreAddresses::GENESIS_ADDRESS()).fee.value + txn_gas_price * (txn_max_gas_units - gas_units_remaining) > max_u128();

pragma verify = false;
aborts_if Signer::address_of(account) != CoreAddresses::GENESIS_ADDRESS();
aborts_if !exists<Account>(txn_sender);
aborts_if !exists<Balance<TokenType>>(txn_sender);
aborts_if txn_sequence_number + 1 > max_u64();
aborts_if !exists<Balance<TokenType>>(txn_sender);
aborts_if txn_max_gas_units < gas_units_remaining;

Function txn_epilogue_v3

The epilogue is invoked at the end of transactions. It collects gas and bumps the sequence number

public fun txn_epilogue_v3<TokenType: store>(account: &signer, txn_sender: address, txn_sequence_number: u64, txn_authentication_key_preimage: vector<u8>, txn_gas_price: u64, txn_max_gas_units: u64, gas_units_remaining: u64, stc_price: u128, stc_price_scaling: u128)
Implementation 
public fun txn_epilogue_v3<TokenType: store>(
    account: &signer,
    txn_sender: address,
    txn_sequence_number: u64,
    txn_authentication_key_preimage: vector<u8>,
    txn_gas_price: u64,
    txn_max_gas_units: u64,
    gas_units_remaining: u64,
    stc_price: u128,
    stc_price_scaling: u128,
) acquires Account, Balance {
    CoreAddresses::assert_genesis_address(account);
    // Charge for gas
    let (transaction_fee_amount_stc,transaction_fee_amount_token) = transaction_fee_simulate(
        txn_gas_price,
        txn_max_gas_units,
        gas_units_remaining,
        stc_price,
        stc_price_scaling);
    assert!(
        balance<TokenType>(txn_sender) >= transaction_fee_amount_token,
        Errors::limit_exceeded(EINSUFFICIENT_BALANCE)
    );
    if (!is_stc<TokenType>()){
        let genesis_balance_amount_stc=balance<STC>(CoreAddresses::GENESIS_ADDRESS());
        assert!(genesis_balance_amount_stc >= transaction_fee_amount_stc,
            Errors::invalid_argument(EPROLOGUE_CANT_PAY_GAS_DEPOSIT)
        );
    };
    // Load the transaction sender's account and balance resources
    let sender_account = borrow_global_mut<Account>(txn_sender);
    // Bump the sequence number
    sender_account.sequence_number = txn_sequence_number + 1;
    // Set auth key when user send transaction first.
    if (is_dummy_auth_key(sender_account) && !Vector::is_empty(&txn_authentication_key_preimage)){
        sender_account.authentication_key = Hash::sha3_256(txn_authentication_key_preimage);
    };
    if (transaction_fee_amount_stc > 0) {
        let transaction_fee_token = withdraw_from_balance(
        borrow_global_mut<Balance<TokenType>>(txn_sender),
            transaction_fee_amount_token
        );
        deposit_to_balance(borrow_global_mut<Balance<TokenType>>(CoreAddresses::GENESIS_ADDRESS()), transaction_fee_token);
        let stc_fee_token = withdraw_from_balance(borrow_global_mut<Balance<STC>>(CoreAddresses::GENESIS_ADDRESS()), transaction_fee_amount_stc);
        TransactionFee::pay_fee(stc_fee_token);
    };
}

Function remove_zero_balance_entry

public entry fun remove_zero_balance_entry<TokenType: store>(account: signer)
Implementation 
public entry fun remove_zero_balance_entry<TokenType: store>(account: signer) acquires Balance {
    remove_zero_balance<TokenType>(&account);
}

Function remove_zero_balance

Remove zero Balance

public fun remove_zero_balance<TokenType: store>(account: &signer)
Implementation 
public fun remove_zero_balance<TokenType: store>(account: &signer) acquires Balance {
    let addr: address = Signer::address_of(account);
    let Balance<TokenType> { token } = move_from<Balance<TokenType>>(addr);
    Token::destroy_zero<TokenType>(token);
}
Specification 
let addr = Signer::address_of(account);
aborts_if !exists<Balance<TokenType>>(addr);
ensures !exists<Balance<TokenType>>(addr);

Function make_event_store_if_not_exist

Make a event store if it's not exist.

fun make_event_store_if_not_exist(account: &signer)
Implementation 
fun make_event_store_if_not_exist(account: &signer) {
    if (!exists<EventStore>(Signer::address_of(account))) {
        move_to(account, EventStore {
          rotate_auth_key_events: Event::new_event_handle<RotateAuthKeyEvent>(account),
          extract_withdraw_cap_events: Event::new_event_handle<ExtractWithdrawCapEvent>(account),
          signer_delegate_events: Event::new_event_handle<SignerDelegateEvent>(account),
        })
    };
}

Module Specification

pragma verify = false;
pragma aborts_if_is_strict = true;