One paid call

In this section, we model reservation, settlement, and refund for a single payment. We implement the state transitions in Lean and prove that every accepted action and sequence preserves total funds. We then extend the model with a saved receipt and prove that retries after a lost reply do not repeat the payment.

Follow the money #

A buyer requests a service from a provider for 30 units. Initially, the buyer has 100 units and the provider has 20. Reserving 30 units sets them aside for this call, so neither party can spend them while payment is pending.

Settlement transfers the reservation to the provider. Refund returns it to the buyer. These are alternative endings to the same reservation.

The total stays at 120, but the available balances alone fall to 90 while the call is pending. We therefore need to count reserved funds separately. Here a reservation is an entry in our model; no real wallet or custody service is involved. Amounts are natural numbers in one common unit, and we assume no fees.

Represent the state #

The four phases record where we are in the call. The reserved phase also holds the price: the amount to transfer on settlement or return on refund:

inductive Phase where
  | ready
  | reserved (price : Nat)
  | settled
  | refunded
  deriving DecidableEq, Repr

A state combines this phase with the two available balances:

structure State where
  buyer : Nat
  provider : Nat
  phase : Phase
  deriving DecidableEq, Repr

Keeping the price inside reserved means a settled or refunded state cannot retain a reservation. The representation expresses this choice directly. The function escrow reads the reserved amount, returning zero in every other phase:

def escrow (s : State) : Nat :=
  match s.phase with
  | .reserved price => price
  | _ => 0

The sum of the three balances is:

def totalFunds (s : State) : Nat :=
  s.buyer + s.provider + escrow s

State the rule, then implement it #

Our specification says that a successful transition must leave this total unchanged. It compares two states without saying how to compute the second:

def PreservesFunds (before after : State) : Prop :=
  totalFunds after = totalFunds before

The implementation supplies that computation. There are three actions: reserve price, settle, and refund. Reservation is allowed only when the call is ready and the buyer can afford the price. Settlement and refund each require a reservation. Everything else is rejected.

def execute (s : State) (action : Action) : Option State :=
  match s.phase, action with
  | .ready, .reserve price =>
      if price ≤ s.buyer then
        some ⟨s.buyer - price, s.provider, .reserved price⟩
      else
        none
  | .reserved price, .settle =>
      some ⟨s.buyer, s.provider + price, .settled⟩
  | .reserved price, .refund =>
      some ⟨s.buyer + price, s.provider, .refunded⟩
  | _, _ => none

Read each successful branch against the diagram. Reservation subtracts from the buyer, settlement adds to the provider, and refund adds back to the buyer. some next returns the resulting state; none rejects the action without returning a new state. After either ending, the final catch-all branch also rejects any attempt to settle the same call again.

The balance check matters: subtraction on Nat stops at zero. Reserving 130 from a buyer with 100 without this check would leave buyer 0 and reservation 130, creating 30 units in the accounting.

Run the paths #

run feeds each successful state into the next action. An empty action list returns the current state, and a rejected action makes the whole result none:

def run (s : State) : List Action → Option State
  | [] => some s
  | action :: rest => (execute s action).bind fun next => run next rest

From the repository root, run:

lake exe demo

The demo starts at balances 100 and 20. Reserving 30 and settling gives 70 and 50; reserving 30 and refunding gives 100 and 20. Trying to settle twice returns none. This is a pure calculation: rejecting a sequence does not undo payments already made in some external system.

Before trying another example, predict what happens when the buyer reserves 101 units, or reserves zero. Which branch of execute explains each result?

Why the total is preserved #

The example checks particular numbers. To cover every accepted action, consider each of the three successful branches. Write the balances as $b$ and $v$, and the price as $p$:

• Reservation changes the total from $b+v$ to $(b-p)+v+p$. The check $p\le b$ ensures subtraction loses exactly $p$, so adding it back restores the total.
• Settlement changes $b+v+p$ to $b+(v+p)$.
• Refund changes $b+v+p$ to $(b+p)+v$.

All three preserve the sum. The theorem states this for any before, action, and after, provided execution actually returns some after:

theorem execute_preservesFunds (before after : State) (action : Action)
    (accepted : execute before action = some after) :
    PreservesFunds before after := by
  rcases before with ⟨buyer, provider, phase⟩
  cases phase <;> cases action <;>
    simp_all [execute, PreservesFunds, totalFunds, escrow]
  · rcases accepted with ⟨funded, rfl⟩
    simp_all <;> omega
  · cases accepted
    simp_all <;> omega
  · cases accepted
    simp_all <;> omega

The proof follows the same case split. Simplification removes rejected cases, which contradict the accepted hypothesis. In the remaining cases, omega discharges the arithmetic equalities using the balance check where needed.

For a successful sequence, apply this argument at every step: the first step preserves the total, and so does the remaining sequence. This induction is the proof of run_preservesFunds in Verification.lean. That file also checks rejection after a finished call and restoration of the initial balances by reserve followed by refund.

Recover a lost reply #

Suppose the buyer pays 30 units, but the reply is lost before reaching the client. The provider now has 50 units, while the client has no receipt. Rejecting a second settlement prevents another transfer, but does not tell the client what happened to the first one.

We give the purchase an identifier and save its receipt with the payment. The client retries the same purchase, and the server sends the saved receipt. The example uses purchase 7 and a pure echo service: input "report" produces result "report". Amounts remain integer base units of one fixed asset, with no fees.

This distinguishes a purchase identifier from a transfer nonce. EIP-3009 prevents reuse of a transfer authorization through its nonce. If a client creates a fresh authorization for the same purchase after a timeout, the application must still recognize that purchase. Our example studies this application-level accounting rule. It does not execute EIP-3009 or the x402 protocol.

Bind the receipt to the purchase #

The approved call fixes the identifier, price, and service input:

structure Call where
  id : Nat
  price : Nat
  input : String
  deriving DecidableEq, Repr

The buyer, provider, asset, and authenticated client are fixed for the entire case. Approval is an input to the model. A request must match the complete approved call; changing its price or input while retaining the identifier is rejected without a state change. A different purchase identifier is also rejected by this single-purchase instance.

saved holds the committed receipt. pending holds a reply in transit, and received records the client's last delivered reply:

structure State where
  funds : PaidCall.State
  saved : Option Receipt := none
  pending : Option Receipt := none
  received : Option Receipt := none
  commits : Nat := 0
  deriving DecidableEq, Repr

Dropping a reply clears pending, leaving the payment and saved unchanged. Delivery moves a pending receipt to the client. Delivery with no pending reply leaves the state unchanged.

The first accepted request uses the existing reservation and settlement functions. The resulting balances and echo receipt are saved together in one atomic transition. A retry enqueues the saved receipt without calling the payment interpreter again:

def request (approved : Call) (s : State) (supplied : Call) : State :=
  if supplied = approved then
    match s.saved with
    | some receipt => { s with pending := some receipt }
    | none =>
        match PaidCall.run s.funds [.reserve approved.price, .settle] with
        | none => s
        | some funds =>
            let receipt := receiptFor approved
            { s with funds, saved := some receipt, pending := some receipt,
                     commits := s.commits + 1 }
  else s

The commits field counts these atomic model payments. In the trace above, two requests cause one payment commit. This is an operation count for this model; it does not measure network latency or gas savings.

Prove the retry behavior #

The accounting specification permits two states: the initial balances with no saved receipt, or exactly one transfer of the approved price with its receipt. It also requires sufficient initial funds for the latter state:

def Accounting (call : Call) (buyer provider : Nat) (s : State) : Prop :=
  (s.funds = PaidCall.initial buyer provider ∧ s.saved = none ∧ s.commits = 0) ∨
  (call.price ≤ buyer ∧
    s.funds = ⟨buyer - call.price, provider + call.price, .settled⟩ ∧
    s.saved = some (receiptFor call) ∧ s.commits = 1)

RepliesMatch requires every pending or delivered receipt to match the saved receipt. execute_preservesInvariant proves these conditions are preserved by each request, loss, or delivery; induction extends the result to any finite sequence. In particular, any such sequence commits at most once:

theorem run_atMostOnce (call : Call) (buyer provider : Nat) (actions : List Action) :
    (run call (initial buyer provider) actions).commits ≤ 1 := by
  have valid := run_preservesInvariant call buyer provider _ actions
    (initial_invariant call buyer provider)
  rcases valid.1 with h | h <;> omega

run_preservesFunds proves the balances and any reservation still sum to the initial total. run_receivedReceipt proves that a delivered receipt identifies the approved purchase and a committed model payment. The recovery theorem states the complete result when the first reply is lost and the retry's reply is delivered:

theorem lostReply_recovers (call : Call) (buyer provider : Nat) (funded : call.price ≤ buyer) :
    run call (initial buyer provider)
      [.request call, .dropReply, .request call, .deliverReply] =
    { funds := ⟨buyer - call.price, provider + call.price, .settled⟩,
      saved := some (receiptFor call), pending := none,
      received := some (receiptFor call), commits := 1 } := by
  simp [run, execute, request, initial, PaidCall.run, PaidCall.execute,
    PaidCall.initial, funded]

Run lake exe demo to see these states. The executable checks also cover insufficient funds, changed terms, repeated retries, exact funding, and a zero-price call.

Atomicity and delivery assumptions #

The proofs assume a serialized transition that commits the local balance changes and saved receipt together. The record is retained for all retries; deleting it or reusing this instance for a different purchase is outside the model. The service is a pure echo computation with no external effects.

A chain transaction and a database write do not automatically form such an atomic transition. A crash after chain settlement but before saving the receipt requires a recovery mechanism that reconciles the external payment with the purchase record. The current proof does not cover that failure, cryptographic verification, multiple purchases sharing a budget, or chain finality.

Reply loss can continue indefinitely. Recovery is proved for a retry whose reply is delivered; eventual delivery is an environmental condition. A payment receipt establishes the modeled payment and echo result, without establishing the quality of an external service.