Blockchain infrastructure

In this section, we review Bitcoin, Ethereum, and Solana, focusing on their ledger structures, transaction execution mechanisms, and fee systems. We use Lean to develop mathematical models, formal specifications, and executable programs for selected mechanisms.

Our main references are the Bitcoin whitepaper, the Ethereum whitepaper and execution specifications, and the Solana documentation.

Bitcoin #

In a bank transfer, the bank keeps the ledger and updates balances when money moves. This lets it check that funds are available before approving a payment. Bitcoin's motivation was to make electronic payments possible without relying on such a trusted intermediary.

This is the double-spending problem. On 31 October 2008, Satoshi Nakamoto announced Bitcoin. The whitepaper proposed a solution: participants share a transaction history and use proof of work to agree on which history to accept.

For example, Alice signs a payment to Bob, then signs another payment to Carol using the same funds. Bob can verify that Alice authorized his payment. That signature does not tell him whether she has also paid Carol with those funds.

The problem of course is the payee can't verify that one of the owners did not double-spend the coin.

— Satoshi Nakamoto, Section 2: Transactions

Here, u is one unspent transaction output controlled by Alice. Either payment can spend it, but a valid chain cannot include both. The blocks in this example have equal difficulty, so the branch with more blocks also has more work.

From a payment to a block #

1. Broadcast. Alice sends her signed transaction to peers, which relay it through the network.
2. Mine. Miners choose valid transactions and summarize them in a Merkle root, a hash stored in the block header alongside the previous block's hash. They vary the nonce and other header data until hashing the header twice with SHA-256 gives a value at or below the target. The network's difficulty rules set this target; a lower target requires more attempts on average.
3. Verify. Full nodes check the proof of work and every transaction. They follow the valid chain with the greatest accumulated work.

Changing an earlier payment changes its block's Merkle root and hash. Every later header in that branch must then change, and its proof of work must be redone. The replacement branch must also overtake the honest chain as it continues to grow. The whitepaper's security argument assumes that honest participants control most of the computing power. Bitcoin's block and proof-of-work rules.

Ethereum #

State transitions #

The Ethereum whitepaper describes a ledger as a state transition system: a transaction changes the current state, or is rejected. For Bitcoin, that state is the set of unspent transaction outputs.

abbrev Transition
    (State Transaction : Type) :=
  State → Transaction → Option State

State represents $\Sigma$, and Transaction represents $\mathcal{T}$. The function takes a state, then a transaction. Its result is some next for $S'$ or none for $\bot$. For Ethereum, the network rules and block context must also be fixed.

Ethereum's shared state #

Ethereum's account model associates each address with a nonce, an ETH balance, and, where applicable, code and storage. The nonce is the counter used to check outgoing transactions. A transaction can transfer ETH or execute contract code. The account definitions below reuse Nonce and Amount from Quantities and units; Wei specializes the amount type to native ETH.

To describe an ETH transfer, keep only balances and nonces. Amounts are integer numbers of wei, where $1\ \mathrm{ETH}=10^{18}\ \mathrm{wei}$. Authentication, fees, and contract execution are outside this transfer model.

structure Account where
  /-- Next outgoing nonce. -/
  nonce : Nonce
  /-- Native ETH, in wei. -/
  balance : Wei
  deriving DecidableEq, Repr

abbrev State := String → Account

state address is $S(a)$; its .nonce.value and .balance.units fields give $n(a)$ and $b(a)$. Wei attaches the amount to native ETH. Strings stand for already validated addresses.

structure Transfer where
  sender : String
  recipient : String
  /-- Amount to move, in wei. -/
  value : Wei
  /-- Must match the sender nonce. -/
  nonce : Nonce
  deriving DecidableEq, Repr

def ValidTransfer
    (state : State) (tx : Transfer) : Prop :=
  tx.nonce = (state tx.sender).nonce ∧
  tx.value.units ≤ (state tx.sender).balance.units

The four fields correspond to $(s,r,v,k)$. ValidTransfer is a proposition about the current state and transfer; it changes no account. Both checks compare natural numbers, so the proposition is decidable. The sender field names an account but does not establish control of it—authentication must happen before calling this rule.

def applyTransfer : Transition State Transfer :=
  fun state tx =>
    if ValidTransfer state tx then
      some fun address =>
        let account := state address
        let debit :=
          if address = tx.sender then tx.value.units else 0
        let credit :=
          if address = tx.recipient then tx.value.units else 0
        let nextNonce :=
          if address = tx.sender then account.nonce.next
          else account.nonce
        { balance :=
            ⟨account.balance.units - debit + credit⟩
          nonce := nextNonce }
    else none

debit and credit are the balance terms in the formula. Nonce.next implements the increment for the sender; other nonces stay unchanged. Every account is computed from the same input state. If sender and recipient coincide, debit and credit cancel, while the nonce still increases. The balance check ensures subtraction cannot underflow; none returns no updated state. The definitions use unbounded natural numbers.

Alice pays Bob #

Alice has 0.010 ETH and nonce 7. Bob has 0.002 ETH and nonce 0:

def initialState : State := fun address =>
  if address = "Alice" then
    { nonce := ⟨7⟩, balance := milliEther 10 }
  else if address = "Bob" then
    { nonce := ⟨0⟩, balance := milliEther 2 }
  else
    { nonce := ⟨0⟩, balance := ⟨0⟩ }

Alice submits a transfer of 0.003 ETH to Bob with nonce 7:

def payment : Transfer :=
  { sender := "Alice"
    recipient := "Bob"
    value := milliEther 3
    nonce := ⟨7⟩ }

The example observes the balances and sender nonce with named fields:

structure TransferSnapshot where
  senderBalance : Wei
  recipientBalance : Wei
  senderNonce : Nonce
  deriving DecidableEq, Repr

def transferExample : Option TransferSnapshot := do
  let next ← applyTransfer initialState payment
  let sender := next payment.sender
  let recipient := next payment.recipient
  pure {
    senderBalance := sender.balance
    recipientBalance := recipient.balance
    senderNonce := sender.nonce
  }

transferExample returns some with senderBalance = milliEther 7, recipientBalance = milliEther 5, and senderNonce.value = 8:

Submitting the same transfer again returns none, because nonce 7 no longer matches 8. A competing payment from Alice to Carol with nonce 7 is rejected for the same reason.

Ethereum's full transition also accounts for gas and contract execution. A contract may update storage or call another contract. A reverted execution still consumes gas and the sender's nonce; it is different from the rejected transfer represented by none here.

From a transaction to a block #

The diagram shows the transaction path in present-day Ethereum and how executing a transaction changes the state.

1. Submit. The wallet signs a transaction specifying the recipient, value, nonce, fee parameters, and optional call data, then sends it to the network. It is pending until included in a block. Transaction lifecycle.
2. Execute and check. A proposed block contains an ordered list of transactions. Execution clients apply them to the parent state, including any contract execution in the EVM. Other nodes repeat the computation and check the result against the block's state root, a hash commitment to that state. The same starting state and valid block must produce the same result. Blocks, EVM.
3. Agree on the history. Validators attest to blocks. Fork choice selects the chain head; votes representing at least two-thirds of the active stake can justify and finalize checkpoints under the protocol's rules. Inclusion in a block and finality are different stages. Proof of stake.

The original Ethereum whitepaper describes proof-of-work mining. Ethereum switched to proof of stake in 2022. Its account and execution concepts remain useful here; the diagram uses the current consensus mechanism.

Hashes and blocks #

A hash is a fixed-length digest computed from data. The same input always gives the same digest; finding different inputs with the same digest should be computationally infeasible.

The bottom of the diagram shows the structure of execution blocks. Each contains a header and a body with an ordered transaction list. The header's transactions_root commits to that list, and state_root commits to the state after execution. Its parent_hash identifies the preceding execution block. Block structure.

The block hash is computed from the encoded header: block hash = Keccak-256(RLP(header)). The diagram abbreviates this as hash(header) and labels the results h0, h1, and h2. Block n stores h0 as its parent hash; Block n + 1 stores h1. Header hashing in Geth.

Changing a transaction changes its root commitment and therefore the block hash, assuming the hash function resists collisions. The next block's existing parent reference then no longer matches. Hash links make such changes detectable; the consensus rules determine which history the network accepts.

ETH, wei, and gas #

Ethereum is the network. ETH is its native asset, and wei is its smallest unit: 1 ETH = $10^{18}$ wei. A payment of 0.003 ETH therefore carries 3,000,000,000,000,000 wei. Ethereum's unit reference.

Gas measures the resources used by a transaction. The fee definition multiplies supplied gas usage by its effective price, with explicit units. This accounting function is separate from the transfer rule above. The sender pays a fee in ETH in addition to the amount transferred. Including this fee in Alice's example leaves her with 0.007 ETH minus the transaction fee. Bob still receives 0.003 ETH; Alice's nonce still increases from 7 to 8.

Contract execution can fail even after a transaction is included. A reverted call rolls back its contract changes, but the sender still pays for gas used. An invalid transaction, such as one with the wrong nonce, cannot be included as a valid transaction. Transactions and gas.

Execution specifications #

ethereum/execution-specs gives executable Python rules organized by network fork. It is the reference for account fields and transaction processing; the transfer model above keeps only balances and nonces.

At revision dc6d1a5, Account in state.py contains a nonce, balance, and code hash. Contract storage is tracked separately. The Prague LegacyTransaction definition separates value, gas, and gas_price. This is one transaction format; it is not the fee format of every current Ethereum transaction.

Accounts and amounts #

Our network identifier uses CAIP-2: eip155:1 denotes Ethereum mainnet. Native ETH uses the CAIP-19 asset reference eip155:1/slip44:60.

def ether : AssetId :=
  ⟨mainnet, "slip44", "60"⟩

Amount asset stores units : Nat, attaching an integer quantity to a particular asset. For Wei, every unit belongs to native ETH on this network:

abbrev Wei := Amount ether

The conversion uses integer arithmetic, so a small payment does not require floating-point numbers.

def milliEther (n : Nat) : Wei :=
  ⟨n * 10 ^ 15⟩

milliEther 3 evaluates to 3,000,000,000,000,000 wei; milliEther 1000 to one ETH. The build checks both conversions. Nat gives mathematical nonnegative amounts; the model omits the upstream U256 bound. Its transfer rule does not verify signatures, charge gas, or execute contracts. Network and address strings are treated as already validated inputs.

EVMYulLean models EVM and Yul machine execution, including machine state and operations.

Solana #

Accounts and programs #

For a SOL payment, Alice sends a System Program transfer instruction naming her account, Bob's account, and the amount. Both accounts must be writable; Alice authorizes the debit by signing. The transaction also identifies its fee payer, which can be a different signer. Transfer instruction and account permissions.

An account holds a lamport balance, data, an owning program, and an executable flag. Here, owner means the program allowed to modify the account's data and debit its lamports. It does not mean the person whose key controls a wallet. Programs store their application state in separate data accounts, which are passed into instructions. This differs from Ethereum's association of a contract address with its code and storage. Account structure, modification rules.

Transaction lifetime and failure #

An ordinary transaction includes a recent blockhash. The runtime checks that it is still valid and that the message has not already been processed. A durable nonce account supports transactions signed ahead of time; its stored nonce is not Ethereum's per-sender transaction counter. Transaction checks, durable nonces.

Instructions within one transaction execute in order. If an instruction fails, the instruction changes are rolled back together. The fee remains charged, and a durable nonce already advanced during validation remains advanced. Execution and rollback.

Account access and parallel execution #

Suppose Alice pays Bob while Carol pays Dave. Both transactions use the System Program, but they update different balances. Sharing a read-only program does not create a write conflict. Sharing Alice's account, Bob's account, or a common fee payer does.

Solana transactions declare the accounts they access and their permissions. Agave's account-lock checks allow concurrent readers; a writer excludes both readers and other writers of that account. The reference here is AccountLocks at revision 39f386a.

structure AccountAccess where
  readOnly : List String
  writable : List String
  deriving DecidableEq, Repr

The lists name resolved accounts with their effective permissions. NoOverlap xs ys means that no address in xs occurs in ys:

def Compatible (left right : AccountAccess) : Prop :=
  NoOverlap left.writable
    (right.readOnly ++ right.writable) ∧
  NoOverlap right.writable
    (left.readOnly ++ left.writable)

def canRunTogether (left right : AccountAccess) : Bool :=
  decide (Compatible left right)

true means these account accesses do not conflict. It does not establish that either transaction is valid or that a scheduler will execute them simultaneously. Address resolution, message validation, program execution, and resource limits are outside this check.

Two payments, one shared wallet #

Each sender initially pays its own transaction fee:

def aliceToBob : AccountAccess :=
  { readOnly := ["SystemProgram"]
    writable := ["Alice", "Bob"] }

def carolToDave : AccountAccess :=
  { readOnly := ["SystemProgram"]
    writable := ["Carol", "Dave"] }

A sponsor adds the same writable fee-payer account to both transactions:

def withSponsor (access : AccountAccess) : AccountAccess :=
  { access with writable := "Sponsor" :: access.writable }

def paymentAccessExample : Bool × Bool :=
  (canRunTogether aliceToBob carolToDave,
   canRunTogether
     (withSponsor aliceToBob) (withSponsor carolToDave))

The result is (true, false): the first pair can acquire compatible account locks; the sponsored pair shares a write target. The build also checks a competing debit, a read/write overlap, and two readers with different fee payers. The compatibility relation is symmetric, as proved by compatible_symm.

For an agent service market, this means separate tasks can still contend on one shared payment account. Wallet layout affects concurrency even when the tasks and their recipients are independent.

SOL, lamports, and compute units #

One SOL is $10^9$ lamports. A compute unit (CU) measures execution according to the runtime's cost rules. For legacy and v0 transactions, the fee is a signature-based base fee plus a prioritization fee:

Here $p_{\mathrm{CU}}$ is in micro-lamports per CU, $L_{\mathrm{CU}}$ is the requested CU limit, and fees are in lamports. The priority fee uses the requested limit, even if execution consumes less. This differs from Ethereum's gas-used accounting. The documented v1 format instead specifies the priority fee directly in lamports. Solana fee structure, Ethereum gas accounting.

Gas and CU are protocol accounting units. Neither supplies a conversion to joules: the energy model needs separate power and duration inputs.

The Solana documentation cited here was checked on 8 October 2026; the account-lock source is pinned above.