WETH9.

Liveness, with exact gas

The exit theorem.

A wrapper’s one job is to give the ether back. Safety theorems cannot say that it will — a contract that always reverts satisfies every invariant of its storage — so this theorem constructs the withdrawal. Its conclusion is a fact about processTransaction, Jaune’s function for executing one transaction inside a block, which block processing calls for every transaction and the conformance fixtures therefore exercise.

theorem weth9_history_tx_withdraw
    {ca : Adr} {cfg : ChainConfig} {checkpoint future : BlockChain} {K₀ : Key → Prop}
    (trace : ConfiguredHistoryTrace cfg checkpoint future)
    (installed : some (checkpoint.state.getCode ca).toList = weth9Sem.image)
    (sumNof : SumNof checkpoint.state.bal)
    (initial : FootInv K₀ (checkpoint.state.getStor ca) (checkpoint.state.bal ca))
    (fresh : KeysFresh K₀ (historyTouchedKeys ca trace))
    {benv : Benv} {bout : BlockOutput} {tx : Tx} {index : Nat} {E : Adr} {wad : B256}
    {chainId : UInt64} {maxPriorityFee maxFee : Nat}
    (hstate : benv.state = future.state)
    (hfork : CoveredFork benv.stat.fork)
    (htype : tx.type = .two chainId maxPriorityFee maxFee (some ca) [])
    (hvalue : tx.value = 0) (hdata : tx.data = withdrawCalldata wad)
    (hchain : chainId = benv.stat.chainId)
    (hprio : maxPriorityFee ≤ maxFee) (hbase : benv.stat.baseFeePerGas ≤ maxFee)
    (hgas : withdrawIntrinsicGas wad + withdrawFrameGas wad + 811 ≤ tx.gas)
    (hcap : tx.gas ≤ 16777216)
    (hroom : tx.gas ≤ benv.stat.blockGasLimit - bout.blockGasUsed)
    (hrecover : recoverSender benv.stat.chainId tx = .ok E)
    (hnonce : (benv.state.get E).nonce = tx.nonce) (hnonceMax : tx.nonce ≠ UInt64.max)
    (hnocode : (benv.state.getCode E).size = 0)
    (hfunds : tx.gas * maxFee ≤ (benv.state.get E).bal.toNat)
    (hprecE : benv.stat.rules.isPrecomp E = false) (hprecCa : benv.stat.rules.isPrecomp ca = false)
    (hholder : historyKeyUniverse ca trace K₀ (.bal E))
    (hbal : wad ≤ (future.state.getStor ca).get (balSlot E))
    (hcbE : benv.stat.coinbase ≠ E) (hcbCa : benv.stat.coinbase ≠ ca) :
    ∃ (st : Jaune.State) (bout' : BlockOutput), processTransaction benv bout tx index = .ok (st, bout') ∧
      bout'.cumulativeGasUsed = bout.cumulativeGasUsed +
        withdrawGasUsed ((future.state.getStor ca).get (balSlot E)) wad ∧
      bout'.blockGasUsed = bout.blockGasUsed +
        withdrawGasUsed ((future.state.getStor ca).get (balSlot E)) wad ∧
      st.getStor ca = (future.state.getStor ca).set (balSlot E)
        ((future.state.getStor ca).get (balSlot E) - wad) ∧
      (∀ a, a ≠ ca → st.getStor a = future.state.getStor a) ∧
      (st.get E).nonce = tx.nonce + 1 ∧
      (st.get E).bal = future.state.bal E -
          (tx.gas * (min maxPriorityFee (maxFee - benv.stat.baseFeePerGas) +
            benv.stat.baseFeePerGas)).toB256 + wad +
        ((tx.gas - withdrawGasUsed ((future.state.getStor ca).get (balSlot E)) wad) *
          (min maxPriorityFee (maxFee - benv.stat.baseFeePerGas) +
            benv.stat.baseFeePerGas)).toB256 ∧
      (st.get ca).bal = future.state.bal ca - wad ∧
      ((future.state.bal E).toNat + wad.toNat < 2 ^ 256 →
        (st.get E).bal.toNat + withdrawGasUsed ((future.state.getStor ca).get (balSlot E)) wad *
          (min maxPriorityFee (maxFee - benv.stat.baseFeePerGas) + benv.stat.baseFeePerGas) =
          (future.state.bal E).toNat + wad.toNat)

Twenty-seven explicit hypotheses, nine conclusions. The hypotheses fall into five groups.

• The history. trace is any configured history from checkpoint to future: a retained run of Jaune’s block transition over valid blocks, each under Prague, Osaka, BPO1 or BPO2. Apart from the hash premise, nothing restricts which transactions it contains or how other contracts call WETH9.
• The checkpoint. The bytes are installed at ca, the total ether is below 2²⁵⁶, and the footprint invariant FootInv K₀ holds: every nonzero storage word lies at one of the three metadata slots or at a tracked key’s slot, tracked keys occupy distinct slots off the metadata slots, and the tracked balances sum to at most the contract’s ether. Executing WETH9’s recorded creation input establishes it, with nothing tracked and no hash premise (below).
• The hashes. fresh says that each key the history may touch is tracked already or lands on a slot in no use, and that distinct keys land on distinct slots (below).
• The holder. E’s balance key is tracked, its WETH balance covers wad, and E has no code — so it is neither a contract, whose withdrawal needs a premise about the callee, nor an account with an EIP-7702 delegation — and is not a precompile.
• The transaction. Everything else: a type-2 transaction to the contract with zero value and no access list, calldata withdraw(wad), consistent chain id and fee fields, a gas limit between the needed amount plus 811 and EIP-7825’s cap of 2²⁴, room in the block, a signature that recovers to E, E’s nonce and funds, and a fee recipient other than E and the contract, whose fee would otherwise mix into the balances the theorem computes. Signature recovery is a premise because the theorem ranges over every signed transaction; for a concrete transaction the kernel computes it.

The conclusion is the holder’s guarantee. The transaction is admitted; the holder’s balance slot is debited by exactly wad and nothing else in the contract’s storage changes; no other account’s storage changes; the contract’s ether falls by wad; and, net of fees, the holder receives exactly wad: provided their ether plus wad stays below 2²⁵⁶, their new balance plus gasUsed times the effective gas price equals their old balance plus wad.

The companion weth9_prefix_tx_withdraw puts the withdrawal where real transactions run: after a block’s two opening system calls and any number of its transactions. Given a history up to the start of a block and the block’s retained execution, it derives the installed code and the footprint invariant at the cut, and if the block’s next transaction is such a withdrawal, it is admitted with the same conclusions — and its result is the one the block actually produced.

Read off the bytes and the fork rules

The gas, term by term.

def withdrawIntrinsicGas (wad : B256) : Nat := 21000 + 4 * calldataTokens (withdrawCalldata wad)
def withdrawFrameGas (wad : B256) : Nat := if wad = 0 then 4440 else 13940
def withdrawRefund (bal wad : B256) : Nat := if wad ≠ 0 ∧ wad = bal then 4800 else 0
def withdrawGasUsed (bal wad : B256) : Nat :=
  withdrawIntrinsicGas wad + withdrawFrameGas wad - withdrawRefund bal wad

The intrinsic cost is the 21,000 every transaction pays plus four gas per calldata token, a zero byte counting as one token and a nonzero byte as four. The frame cost for a nonzero withdrawal is the sum below.

When wad = 0 the write and the transfer cost 100 each and the frame costs 4,440. When a nonzero withdrawal empties the balance, clearing the slot earns EIP-3529’s 4,800-gas refund. The refund cap of one fifth of the gas used and EIP-7623’s calldata floor never bind for this call, which the proof establishes rather than assumes.

The 811 gas of margin in the gas-limit premise is gas the transaction must hold but does not use. The CALL that sends the ether is charged 9,100 before the 2,300-gas stipend it hands the recipient comes back unused, so the frame must momentarily hold 2,300 more than the transfer’s net 6,800; and 1,489 gas of the frame’s cost, mostly the Withdrawal event’s LOG2, falls after the call. 2,300 − 1,489 = 811.

A gas limit equal to the receipt’s 30,344 does not meet the theorem’s premise; 35,955 is sufficient, not shown to be minimal.

An empirical test, outside the proof

Against the chain.

A gas formula proved against a model is only as good as the model’s gas schedule. The conformance fixtures test that schedule; the formula can also be compared with mainnet directly. In the 30,000 blocks from 26,111,230 to 26,141,229 (3 to 7 October 2026), WETH9’s Withdrawal events locate every successful direct call to withdraw:

The matches span twelve combinations of calldata tokens, from 60 to 75, and emptying; none withdraws zero. Two excluded groups still admit a prediction, and their 98 admissible calls of type 0 and 1,590 calls with 37 to 76 bytes of calldata match too; they are counted apart. Calls from accounts with code cannot be predicted, since the ether transfer runs the sender’s code.

What the comparison does and does not show. The prediction needs one bit of state, whether the withdrawal empties the sender’s balance, so it needs the balance the withdrawal starts from. WETH9 logs an event for every change to a balance; when no other event of the block names the sender, that balance is the sender’s balance at the end of the previous block, and a withdrawal is called emptying when its amount equals that balance. This holds for 3,748 of the 3,780; the other 32 share their block with another WETH9 event naming the sender, and are set aside. Every one of the 3,748 receipts equals the prediction. The comparison exercises nonzero withdrawals under one fork, BPO2, and establishes none of the theorem’s other hypotheses for these transactions.

Safety, after any history

Backing and exact replay.

Beneath the exit theorem, the safety results hold after any configured history from a checkpoint satisfying the footprint invariant, under the same hash and total-ether premises.

• The footprint survives. The code is intact, and there is a footprint of tracked keys — the checkpoint’s, extended by keys the history touched — such that every nonzero storage word sits at a metadata slot or a tracked key’s slot, tracked slots are distinct and apart from the metadata slots, and the tracked balances sum to at most the contract’s ether. Blanc.Lift.Weth9.weth9_history_footprint
• Every tracked balance is backed, in total and one by one, and an address whose balance slot is neither a metadata slot nor a tracked slot is owed nothing. Blanc.Lift.Weth9.weth9_history_backed
• The ledger is exactly the committed calls. The ledger read from the final storage is the model’s ledger run over exactly the settlement-committed calls to the contract’s writers, in order: rolled-back frames are absent, view calls contribute nothing, and a call re-entered from inside a withdrawal’s ether transfer is placed after the withdrawal that made it. Blanc.Lift.Weth9.weth9_history_committed

Constructed executions

Every writer, live.

Every writer runs from a fresh frame at a cost that is a closed sum of fixed charges and the actual storage charges of the slots it touches, and so do balanceOf and decimals. A selection:

Liveness climbs four rungs. From a fresh frame, every writer succeeds at its exact cost. At the model level, any writer call the model accepts is realized by an execution ending in the model’s next ledger. At a reachable state — after any configured history — a tracked holder can withdraw to an account without code, deposit, or transfer what its stored balance covers (weth9_history_withdraw_live, …_deposit_live, …_transfer_live). And as a signed transaction, the withdrawal is admitted, as above. approve and transferFrom are proved live at the frame and model levels only.

Where a history can start

Deployment, and a closed instance.

An invariant stated at a checkpoint is worth something only if a real state satisfies it. Under every covered fork, Blanc executes the recorded creation input of WETH9’s deployment transaction as a CREATE message from the recorded deployer at nonce 446, and proves that it succeeds, installs exactly the certified runtime at the CREATE address, and leaves exactly the constructor’s name, symbol and decimals storage — which satisfies the footprint invariant with nothing tracked, for every ether balance, with no hash premise (weth9_deploy_covered, weth9_deploy_init_covered). This is a modeled deployment: it runs the historical input under current rules and does not prove that the 2017 transaction was included in the chain.

The premises of the exit theorem can all hold at once. weth9_closed_exit_instance discharges every one of them, with no hypotheses left, on one connected execution in a synthetic BPO2 world: the recorded creation input deploys the runtime; a valid configured block commits a signed deposit of one wei by a funded holder; and at the history’s end a concrete signed withdraw(1) by that holder is admitted, using 30,344 gas. Both signatures are recovered by the kernel. The world is synthetic — finite funding, and a STOP program at each system-contract address in place of the canonical code — so the instance shows the premises are satisfiable together, not that anything happened on mainnet.

Hashes without axioms

The hash premise, and why it is there.

WETH9 keeps balances and allowances at hashed storage slots, keccak(a ‖ 3) for balanceOf[a]. A proof about such storage must know the slots it reasons about are distinct. Blanc adds no axiom about Keccak-256 — the injectivity axiom some systems adopt is false, since the hash maps an unbounded domain into 2²⁵⁶ values. Instead the theorem states, as the premise fresh, exactly the separation it uses: each key the history may touch — five per call to the contract, computed from its caller and the first two words of its arguments, whatever the function or outcome — is tracked already or lands on a slot in no use, and distinct keys land on distinct slots.

This is a statement about finitely many concrete hash values, which anyone holding the history can compute: five keys and seven Keccak evaluations per call. It is not implied by computational collision resistance, and no reduction is proved. It is also necessary: a written allowance slot that coincides with a tracked balance slot breaks backing (trackedSum_collision_breaks_backing).

Stated, so it is not inferred

Not claimed.

• That today’s WETH9 satisfies the footprint invariant. The theorems start from a modeled fresh deployment; reaching the live contract means rebuilding every address that has held a balance or an allowance from its logs and calldata, and showing from a complete enumeration of its storage that nothing else is stored — a finite check over public data that has not been run.
• Anything about balances outside the tracked keys, or about accounts holding code, which need the SendOk callee premise to withdraw.
• approve and transferFrom liveness after a history.
• The effects of static frames, which the committed list leaves out by the form of the statement rather than by proof, and of rolled-back frames.
• Inclusion: the transaction theorems execute a transaction at a given state or position; whether any block includes it is outside them.
• Amsterdam, or any fork other than Prague, Osaka, BPO1 and BPO2.

The claim map’s WETH9 section lists every theorem with its premises and its file and line, checked by a gate.

Context

Earlier work, and Blanc’s own WETH.

Verifereum, in HOL4, includes among its experimental developments a WETH9 example on the bytes at the mainnet address. EquiVM proves refinement for a local build of WETH9’s source — 1,763 bytes of solc 0.5.16 output — rather than the deployed 3,124 bytes of solc 0.4.19 output.

Blanc also contains a WETH written in its own language — a different artifact with a different subject — whose 988-byte runtime keys balances by raw address words, so its solvency theorem needs no hash premise at all. Two theorems in Blanc’s composition stratum compare it with the deployed WETH9 exactly: balanceOf costs 2,260 gas cold against WETH9’s 2,534, and decimals 158 against 2,444 (balanceOf_weth9_vs_weth, decimals_weth9_vs_weth). More on Blanc’s WETH.