Assets and tokens

In this section, we review stablecoins and the ERC-20 token standard. We use Lean to model asset identity and token balances, and implement an ordinary token transfer.

Our main references are Circle's USDC documentation, the ERC-20 specification, and OpenZeppelin Contracts.

Stablecoin payments #

A stablecoin targets the value of a reference asset, often a currency such as the US dollar. This gives a service market a way to quote work, set budgets, and compare costs in a shared unit. The peg depends on the coin's design: reserve-backed coins rely on an issuer and redemption arrangements; crypto-collateralized designs use collateral and protocol rules. Ethereum's stablecoin overview.

USDC is Circle's dollar-backed example. Its EVM representation implements ERC-20; the standard specifies balance, transfer, and allowance interfaces. Price stability requires additional economic arrangements beyond that interface. ERC-20 specification.

Price, amount, and fees #

Alice gives an agent a budget of 10 USDC. A provider charges 0.01 USDC per request, so the budget covers 1,000 requests before fees. After one payment, Alice has 9.99 USDC and the provider has received 0.01 USDC.

USDC uses six decimal places in the Circle contract example. The service payment therefore carries an integer amount:

On Ethereum, transaction gas is paid in ETH; on Solana, transaction fees are paid in SOL. The fee payer may differ from the customer. The payment protocol example uses a facilitator to submit a token transfer and pay its gas. The chain notes describe the two fee systems.

A quote fixed at 0.01 USDC stays fixed in USDC if its dollar price moves. A quote fixed at 0.01 USD instead needs an exchange-rate source, a rounding rule, and a validity period to determine the token amount. The same distinction applies when comparing service revenue with electricity or hardware costs.

Reserves and redemption #

Circle describes USDC as backed by cash and cash-equivalent reserves and publishes reserve disclosures and attestations. Direct conversion through Circle Mint is available to eligible businesses. Token transfers update the on-chain ledger; redemption also depends on the issuer and its banking process. USDC overview, reserve disclosures.

Circle's EVM contract assigns roles for minting, burning, pausing transfers, and blocking addresses. An ordinary transfer preserves total supply, while minting and burning change it. Sufficient balance alone does not establish that a transfer is permitted by this contract. FiatToken design at fc85788.

A proof about balance updates cannot establish the value or availability of external reserves, redemption access, or a market price of exactly one dollar. These are separate assumptions when using a stablecoin in an economic model.

Asset identity across chains #

The name USDC does not identify a unique on-chain balance. Payment terms must select the network and token contract or mint. Circle lists separate USDC addresses for each supported network. Bridged representations also depend on the bridge and the assets it holds; they must be distinguished from issuer-native USDC. Native and bridged USDC.

The sources in this section were checked on 8 October 2026. The x402 reference example represents payment terms for Base Sepolia testnet USDC, whose tokens have no dollar redemption value.

ERC-20 transfers #

To isolate the balance update, take a token with 100 base units held by Alice. She transfers 30 to Bob. The token contract records 70 for Alice and 30 for Bob. This small arithmetic example uses a local token fixture, not deployed USDC.

In OpenZeppelin Contracts #

OpenZeppelin Contracts provides Solidity implementations of common contract standards. Its ERC20.sol at cd3284f stores balances in _balances and reads them through balanceOf.

transfer obtains the sender from _msgSender(), then calls _transfer. _transfer rejects zero addresses and delegates the balance changes to _update. For an ordinary transfer, _update checks the sender's balance, debits it, then credits the recipient and emits a Transfer event. Minting and burning take other branches.

decimals() defaults to 18 in this implementation. It affects display only: 30 base units with 18 decimals display as $30 / 10^{18}$ tokens. Other contracts can override the value. The ERC-20 standard also defines approve, allowance, and transferFrom for delegated spending.

Token balances and transfers #

A token is identified by its network and contract address. Decimal metadata does not change that identity.

structure Token where
  contract : AccountId
  decimals : Nat
  deriving DecidableEq, Repr

The ledger belongs to one token contract. A holder address selects a balance inside that ledger:

structure State (token : Token) where
  balanceOf : String → Nat
  totalSupply : Nat

Amount token.asset keeps the transfer quantity tied to the token. The selected ordinary-transfer model checks addresses and available funds before subtraction:

def transfer {token : Token} (state : State token) (sender recipient : String)
    (amount : Amount token.asset) : Option (State token) :=
  if sender = zeroAddress ∨ recipient = zeroAddress then none
  else if amount.units > state.balanceOf sender then none
  else if sender = recipient then some state
  else
    let balances := fun address =>
      if address = sender then state.balanceOf address - amount.units
      else if address = recipient then state.balanceOf address + amount.units
      else state.balanceOf address
    some { state with balanceOf := balances }

A self-transfer returns the original state. In the Solidity implementation, the debit and subsequent credit reach the same result. totalSupply stays unchanged during an ordinary transfer.

def transferReport : Option (Nat × Nat × Nat) := do
  let next ← transfer initial alice bob ⟨30⟩
  pure (next.balanceOf alice, next.balanceOf bob, next.totalSupply)

The example returns some (70, 30, 100): Alice's balance, Bob's balance, and total supply. The build also checks insufficient funds, zero addresses, zero amount, and self-transfer. The example contract address is a local fixture.

This model uses unbounded Nat balances and assumes valid, normalized address strings. It selects balance updates from the contract; it does not implement uint256 bounds, event logs, allowances, minting, or burning. ETH gas accounting is separate from this token ledger. Issuer controls, reserves, and redemption are also outside this ordinary-transfer model.