Appendix: Coq proof of reserve-balance safety

This file accompanies the blog post and serves as a literate walkthrough of the final model. The guiding idea is simple:

• *Consensus* computes a **worst-case, fee-only budget** (the “effective reserve”) for the yet-to-be-executed suffix and only proposes blocks when that budget stays non-negative for every **sender** that appears later.
• *Execution* runs the actual EVM step and enforces that **no account dips below its protected reserve slice** (with a carefully fenced “emptying” exception). If a transaction would violate that, it is reverted in place.

The definitions below encode those two algorithms and the invariants we prove about them. The consensus check is defined in consensusAcceptableTxs, the execution check is in execTx. The main soundness theorem is fullBlockStep. References to any Coq item are hyperlinked to its definition if the definition is in this file or in the Coq standard library.

Preliminaries

This is the full EVM state that EVM execution takes as input and returns as output.

Many of the EVM semantics definitions we use come from Yoichi's EVM semantics, developed several years ago. The definition of Transaction there lacks fields to support newer features like delegation. Also, the last field is to support user-configurable reserve balances in Monad. There is a new transaction type which can update the configured reserve balance of the sender. Such transactions do nothing else.

The fields above should ultimately come from EVM semantics and not here. The fields below are monad-specific.

^ updates the reserve balance of the sender if Some. In that case, the transaction does nothing else, e.g., smart contract invocation or transfer.

Our **fee upper bound** is intentionally pessimistic: the consensus rule reasons about gas_limit × gas_price, never about *actual* gas used. This mismatch is the source of slack that makes safety proofs simple while remaining implementable.

The proofs in this file never unfold the definition of maxTxFee, so nothing will break if this definition is changed.

Parameterization by the lookahead window K: consensus can be ahead of execution by at most K. n+Kth block must have the state root hash after execution block n. the next 2 variables are parameters for the rest of the proofs. All “emptying” checks therefore only look at activity within a K-sized window. We also fix a default reserve cap used when an account has never reconfigured its reserve.

To implement reserve balance checks, execution needs to maintain some extra state (beyond the core EVM state) for each account:

^ last block index where this account sent a transaction. In the implementation, we can just track the last 2K range, e.g. this can be None if the last tx was more than 2K block before. we do not need to store this information in the db as it can be easily computed

^ last block index where this address was delegated or undelegated. In the implementation, we can just track the last 2K range.

^ the current configured reserve balance of the account. will either be DefaultReserveBal or something else if the account sent a transaction where reserveBalUpdate is not None

Our modified execution function which does reserve balance checks will use the following type as input/output. Consensus checks also take this as input, where the AugmentedState is the state after N-K block when proposing a new block. However, when the next pending (already proposed) block is executed, it can be a later state.

returns true if sender tx sent a transaction within the last K blocks of txBlockNum tx

returns true if the account sender tx was delegated/undelegated within the last K blocks of txBlockNum tx

Consensus Check (algo 1)

Below, we build up the definition of the consensus check consensusAcceptableTxs The “emptying” gate: A sender may “empty” (i.e., allow value to eat into reserve for this one tx) iff all three are true:

• it is *not* currently delegated,
• it had no delegation change within the last K blocks (including the in-flight suffix),
• it did not send a transaction in the last K blocks (including the in-flight suffix).

This gate is what lets consensus handle fee-only budgets and still tolerate occasional value drains safely.

The effective reserve map: Consensus reasons about *how much of the protected (reserve) slice of the balance can be consumed* by the yet-to-run suffix. This is the “effective reserve” map:

• It is initialized with min(balance, configuredReserve).
• Every transaction removes *at most* its fee from the sender’s entry, except for the “emptying” hole, where the pessimistic removal accounts for value + fee in one shot.

Notice the type is Z: negative entries encode an *over-consumption* that should make the proposal unacceptable.

Consensus’ decrement step: remainingEffReserveBals is the algebraic heart of consensus check algorithm: fold this function left-to-right over the suffix, and you get the remaining worst-case protected reserve for every sender. Formally, this function conservatively estimates the remaining effective reserve balance after executing candidateTx, assuming preCandidateTxResBalances is the estimate before candidateTx. This is done in a setting where the latest available state is preIntermediatesState and intermediates are all the transactions between preIntermediatesState and candidateTx. Only the current sender’s entry changes; all other entries are unchanged. In the definition of newBal (let binding), the subtraction is capped below at 0: the result is a natural number (N). So, if if sbal < maxTxFee next + value next but maxTxFee next ≤ sbal, this transaction (next) will be accepted but all subsequent ones from the same sender will be rejected as the remaining effective reserve balance becomes 0.

regular tx, not one that sets reserve balance

Algorithm 1 (consensus): acceptability of a suffix

A suffix is **consensus-acceptable** if, after pessimistically removing the head-then-tail debits, *every sender that appears later still has a non-negative effective reserve*. This is exactly the safety condition proposers maintain as they build blocks up to K ahead. When evaluating a new tx at block number N to add at the end of postStateSuffix, latestState must be the state after N-K block when proposing a new block. However, when the next pending (already proposed) block is executed, we need to derive that the remaining already proposed transactions are still valid on top of the more recent state: this is what the main soundness lemma fullBlockStep proves, in addition to proving that postStateSuffix will execute without running out of fees to pay.

Execution Check (algo 2)

The execution logic is also tweaked to ensure that a transaction cannot dip too much into reserves so as to not have enough fees for a transaction already included by consensus. First, some helpers for that. isAllowedToEmptyExec is a trivial wrapper used in execution, where there are intermediate transactions between the current transaction and the last known fully executed state.

updateExtraState is the execution-time maintenance of the tiny history we need for emptiness checks and reserve-config changes. It is deliberately side-effect-free except for the fields it touches.

Abstract execution and revert

We postulate a single-step EVM core (evmExecTxCore) that returns the new state and the set of changed accounts; and the revert step for failed checks. This keeps the reserve logic orthogonal to the (much larger) EVM semantics.

Algorithm 2 (execution): execute a transaction

This assumes that t has already been validated to ensure that the sender has enough balance to cover maxTxFee. Execution proceeds as follows:

• Special “reserve update” tx: pay fee; set new configured reserve.
• Otherwise, run the core EVM step to obtain the *actual* post state.
• For *changed* accounts, enforce reserve discipline:
  • Non-sender: their *previous* protected slice must still fit in the *current* balance (unless they have code, deployed in this tx or before). if the account does have code, the address was generated by a keccak, so the proof assumes that nobody has the corresponding private key and thus the address can never send a transaction, thus this step can empty the balance.
  • Sender: either allowed to empty, or must retain at least min(R, balance_before) − maxTxFee.
• If any check fails, revert the tx *and still* update the extra history (so K-window bookkeeping remains accurate).

Note that because the hasCode check is done on si (the result of running the EVM blackbox to execute t), not s (the pre-exec state), the following scenario is allowed.

• Alice sends money to addr2 in some contract. Alice is EOA.
• Alice sends tx foo to a smart contract address addr.
• addr execution deploys code at addr2 and calls it, and the call empties addr2.

Basic pre-validation: proposers guaranteed fee solvency for senders of the head transaction; executors re-check that cheaply before doing real work. The implementation checks nonces as well, but here we are only concerned with tx fees.

Top-level execution wrapper that fails fast when validation fails. None means the execution of the whole block containing t aborts, which is what the consensus/execution checks must guarantee to never happen.

execute a list of transactions one by one. note that the execution of any tx returns None (balance insufficient to cover fees), the entire execution (of the whole list of txs) returns None

Main correctness theorem

our correctness property only holds when the set of proposed transactions are within K. this helps capture that assumption

The lemma below is probably what one would come up first as the main correctness theorem. blocks represents the transactions in the blocks proposed after latestState. It says that consensus checks (consensusAcceptableTxs latestState blocks) implies that the execution of all transactions blocks one by one, starting from the state latestState will succeed and not abort (None) due to preTx balance being less than maxTxFee.

main correctness theorem

We will prove the above correctness theorem below, but the actual correctness theorem we need is slightly different. Suppose we split blocks in the theorem above into firstblock and restblocks such that blocks=firstblocks++blocksrest and suppose these blocks together are all transactions from the K proposed blocks since the last consensed state. Now, consensus will wait for execution to catch up and compute the state after firstblock, say latestState'. After that, consensus should check the next block after blocksrest w.r.t latestState'. At that time, it needs to know that blocksrest is already valid w.r.t latestState', i.e. consensusAcceptableTxs latestState' blocksrest. This is precisely what the main theorem, shown next does:

^ execution cannot abort (indicated by returning None) due to balance being insufficient to even pay fees

in this case, we have enough conditions to guarantee fee-solvency of block2, so that it can be extended and then this lemma reapplied

Proof

core execution assumptions

To prove the theorem fullBlockStep, we need to make some assumptions about how the core EVM execution updates balances and delegated-ness. The names of these axioms are fairly descriptive.

One caveat in the assumption below is that it assumes that the account ac does not receive so much credit that it overflows 2^256. In practice, this should never happen, assuming the ETH supply is well below 2^256. Thus, we can assume that evmExecTxCore caps the balance at 2^256 should it overflow, instead of wrapping around, which may violate this assumption.

lemmas about execution

Unless there is a comment before a lemma, the lemma follows easily from the axioms above about evmExecTxCore and revertTx and by the definition of execTx

This lemma combines many of the execution lemmas above to build a lower bound of the balance of any account after executing a transaction.

isAllowedToEmpty lemmas

Recall isAllowedToEmpty s (txInterfirst :: rest) txnext determines whether the transaction txnext is allowed to empty its balance, in the setting where s is the last available state and (txInterfirst :: rest) are the transactions between s and txnext. This lemma proves that to be equivalent to executing txInterfirst at state s and considering the result as the latest available state and thereby removing txInterfirst from intermediates.

lemmas about remainingEffReserveBals

The next pair of lemma states that the “remaining effective reserve” function is monotone: if you start from a pointwise larger map, you end at a pointwise larger map. rbLe is defined right above.

In the proof of the main correctness theorem, we use a slightly different variant of monotoncity, where in the RHS of ≤, remainingEffReserveBals starts from the final state after executing tx from s and as a result, tx is dropped from the list of intermediate transactions between the state and the candidate transaction txc. The proof follows from the definition of remainingEffReserveBals and the execution lemmas above.

lifts mono from remainingEffReserveBals to remainingEffReserveBalsL: proof follows a straightforward induction on the list extension, using mono to fulfil the obligations of the induction hypothesis

Similarly, lifts mono2 from remainingEffReserveBals to remainingEffReserveBalsL: proof follows a straightforward induction on the list extension, using mono2 to fulfil the obligations of the induction hypothesis.

This lemma captures a key property of remainingEffReserveBals: it underapproximates the resultant effective balance after execution of the transaction

for any account that is a sender of one of the intermediate transactions (between s and the candidate transaction txc), remainingEffReserveBals is a non-increasing function.

lifts the previous lemma from remainingEffReserveBals to remainingEffReserveBals. induction on nextL

Finally, here is one of the key stepping stones to the main theorem, it says that the consensus checks guarantee that execution of the first transaction will pass validation during execution, i.e. the balance would be sufficient to cover maxTxFee. This doesn't say anything about whether the execution of the later transactions (extension) will also pass the check. That is where the next lemma comes in handy.

you can pick the first tx in the proposed extension and the consensus checks would still hold on the resultant state for the remaining transactions in the proposal.

the above 2 lemmas can be combined to yield the following:

Proof of main theorem:

Straightforward induction on firstblock, with inductiveStep used in the inductive step.

All assumptions of the proof:
Section Variables:
K
: N
Axioms:
revertTxDelegationUpdCore :
  ∀ (tx : TxWithHdr) (s : StateOfAccounts),
    reserveBalUpdateOfTx tx = None
    → ∀ (sf := revertTx s tx) (ac : EvmAddr),
        addrDelegated sf ac =
        addrDelegated s ac && bool_decide (ac ∉ undels tx.1.2) || bool_decide (ac ∈ dels tx.1.2)
revertTx : StateOfAccounts → TxWithHdr → StateOfAccounts
execTxSenderBalCore :
  ∀ (tx : TxWithHdr) (s : StateOfAccounts),
    (maxTxFee tx ≤ balanceOfAc s (sender tx))%N
    → reserveBalUpdateOfTx tx = None
      → let sf := (evmExecTxCore s tx).1 in
        addrDelegated s (sender tx) = false
        → balanceOfAc sf (sender tx) = (balanceOfAc s (sender tx) - (maxTxFee tx + value tx))%N
          ∨ balanceOfAc sf (sender tx) = (balanceOfAc s (sender tx) - maxTxFee tx)%N
execTxDelegationUpdCore :
  ∀ (tx : TxWithHdr) (s : StateOfAccounts),
    reserveBalUpdateOfTx tx = None
    → ∀ (sf := (evmExecTxCore s tx).1) (ac : EvmAddr),
        addrDelegated sf ac =
        addrDelegated s ac && bool_decide (ac ∉ undels tx.1.2) || bool_decide (ac ∈ dels tx.1.2)
execTxCannotDebitNonDelegatedNonContractAccountsCore :
  ∀ (tx : TxWithHdr) (s : StateOfAccounts),
    reserveBalUpdateOfTx tx = None
    → ∀ (sf := (evmExecTxCore s tx).1) (ac : EvmAddr),
        ac ≠ sender tx
        → addrDelegated sf ac || hasCode sf ac = false
          → (balanceOfAc s ac ≤ balanceOfAc sf ac)%N
evmExecTxCore : StateOfAccounts → TxWithHdr → StateOfAccounts × list EvmAddr
changedAccountSetSound :
  ∀ (tx : TxWithHdr) (s : StateOfAccounts),
    reserveBalUpdateOfTx tx = None
    → let (sf, changedAccounts) := evmExecTxCore s tx in
      ∀ ac : EvmAddr, ac ∉ changedAccounts → sf ac = s ac
balanceOfRevertSender :
  ∀ (s : StateOfAccounts) (tx : TxWithHdr),
    (maxTxFee tx ≤ balanceOfAc s (sender tx))%N
    → reserveBalUpdateOfTx tx = None
      → balanceOfAc (revertTx s tx) (sender tx) = (balanceOfAc s (sender tx) - maxTxFee tx)%N
balanceOfRevertOther :
  ∀ (s : StateOfAccounts) (tx : TxWithHdr) (ac : EvmAddr),
    reserveBalUpdateOfTx tx = None
    → ac ≠ sender tx → balanceOfAc (revertTx s tx) ac = balanceOfAc s ac