Accounts and storage

The account tuple and its sentinels, and the per-layer account/storage entry types that cross the host interface (overlay rows, merge enumeration). Pure data — no registers, no externs.

type AccountInfo

Account state (Yellow Paper §4.1, the account tuple σ[a]). storage_root is the account's pre-state storage root — the witness anchor that stateless storage reads walk on a cached-state miss. It is set when the account is materialized from the witness and is not kept live during execution (storage mutates in the overlay maps; the post-state root is computed on demand). Code bytes are not held here — the account carries only code_hash, a content address into the code store; the code hash is itself observable state (EXTCODEHASH, EIP-1052) and the binding a stateless witness checks code against.

struct AccountInfo = {
    /* sigma[a]_n: nonce (EIP-2681 caps it at 2^64-1) */
    nonce : account_nonce,
    /* sigma[a]_b: balance in wei */
    balance : word,
    /* sigma[a]_c: keccak256(code); KECCAK_EMPTY if codeless */
    code_hash : hash,
    /* sigma[a]_s: PRE-STATE storage root, the witness anchor */
    storage_root : hash,
}

type Account

An account plus its lifecycle flags: existence, EIP-161 storage clearing, same-transaction creation (EIP-6780), and selfdestruction.

struct Account = {
    info           : AccountInfo,
    present        : bool,
    storage_cleared: bool,
    created        : bool,
    selfdestructed : bool,
}

type StorageValue

A storage slot's current and original (transaction-start) values — the pair EIP-2200/EIP-3529 gas and refund rules compare.

struct StorageValue = { curr : word, orig : word }

type StorageTxLookup

Result of consulting the transaction storage layer. A clear generation is not a slot-row hit: it resolves the value to zero, but the caller must still record the first EIP-7928 read of that slot.

union StorageTxLookup = {
    /* the slot's transaction-layer current/original value pair */
    StorageTxHit : StorageValue,
    /* a clear generation covers the slot: it reads as zero */
    StorageTxCleared : unit,
    /* the transaction layer holds nothing for the slot */
    StorageTxMiss : unit,
}

type StorageKey

A fully qualified storage key: account address and 256-bit slot.

struct StorageKey = { addr : address, slot : word }

type StorageEntry

An overlay storage row: the form in which storage entries are enumerated at transaction-end merge.

struct StorageEntry = { key : StorageKey, value : StorageValue }

type StorageBlockRow

A block-layer storage lookup. value is meaningful exactly when found is true; the explicit bit keeps a real all-zero row distinct from a miss.

struct StorageBlockRow = { found : bool, value : StorageValue }

type StorageTxPopResult

One transaction-layer storage row, or exhaustion of the destructive transaction-end drain.

union StorageTxPopResult = {
    /* the next drained transaction-layer storage row */
    StorageTxPopRow : StorageEntry,
    /* the drain has yielded every row */
    StorageTxPopExhausted : unit,
}

type AcctValue

An account's current and original (transaction-start) states.

struct AcctValue = { curr : Account, orig : Account }

type AcctEntry

An overlay account row: the form in which account entries are enumerated at transaction-end merge.

struct AcctEntry = { addr : address, value : AcctValue }

type AccountRow

An account-layer lookup. account is meaningful exactly when found is true; EMPTY_ACCOUNT is the payload sentinel for a miss.

struct AccountRow = { found : bool, account : Account }

type AcctTxPopResult

One transaction-layer account row, or exhaustion of the destructive transaction-end drain.

union AcctTxPopResult = {
    /* the next drained transaction-layer account row */
    AcctTxPopRow : AcctEntry,
    /* the drain has yielded every row */
    AcctTxPopExhausted : unit,
}

type StorageTrieEntry

A host storage row prepared for secure-trie traversal. The semantic row remains StorageEntry; these cached digests are derived traversal metadata computed when the witness value is first materialized.

struct StorageTrieEntry = {
    entry : StorageEntry,
    address_hash : hash,
    slot_hash : hash,
}

type StorageBlockIterResult

One block-layer storage iterator row, or iterator exhaustion.

union StorageBlockIterResult = {
    /* the next block-layer storage row, with its cached traversal digests */
    StorageBlockIterRow : StorageTrieEntry,
    /* the iterator has yielded every row */
    StorageBlockIterExhausted : unit,
}

type AcctTrieEntry

A host account row prepared for secure-trie traversal.

struct AcctTrieEntry = {
    entry : AcctEntry,
    address_hash : hash,
}

type AcctBlockIterResult

One block-layer account iterator row, or iterator exhaustion.

union AcctBlockIterResult = {
    /* the next block-layer account row, with its cached address digest */
    AcctBlockIterRow : AcctTrieEntry,
    /* the iterator has yielded every row */
    AcctBlockIterExhausted : unit,
}

let EMPTY_ACCOUNT_INFO

The empty account tuple: zero nonce and balance, KECCAK_EMPTY code hash, empty-trie storage root (YP §4.1).

let EMPTY_ACCOUNT_INFO : AccountInfo = struct {
        nonce = 0,
        balance = ZERO_WORD,
        code_hash = KECCAK_EMPTY,
        storage_root = EMPTY_TRIE_ROOT,
    }

let EMPTY_ACCOUNT

The non-existent account sentinel (EIP-161 "empty").

let EMPTY_ACCOUNT : Account = struct {
        info = EMPTY_ACCOUNT_INFO,
        present = false,
        storage_cleared = true,
        created = false,
        selfdestructed = false,
    }

function account_from_info

Wraps a witnessed account tuple as an existing, unmodified account.

function account_from_info(info : AccountInfo) -> Account =
    struct { info = info, present = true, storage_cleared = false, created = false, selfdestructed = false }