Coq model of reserve balance and proof of safety

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.

Below we define the two algorithms, followed by proofs. The consensus check is defined in consensusAcceptableTxs, the execution check is in execValidatedTx (called by execTx after validation). **Delayed reserve-balance configuration.** Accounts can update their reserve balance by calling a stateful precompile; updates become effective only after K blocks. We model this via delayedReserveBalOfAddr, which returns the latest update at or before block n-K when processing block n. Consensus therefore does not need to inspect transactions to track reserve-balance updates, and execution records pending updates in extra state. Reverted transactions discard reserve-balance updates. The main soundness theorem is fullBlockStep. Intuitively, it says that if any sequence of txs is accepted by consensus, execution of those txs cannot run into an error because of inability to pay gas fees. References to any Coq item are hyperlinked to its definition if the definition is in this file or in the Coq standard library. consensusAcceptableTxs is defined using idealized arithmetic (Z, which is Coq's type of unbounded integers with no over/underflow in operations). To be sure that it can be implemented without over/underflow issues, at the end of this file, we define a variant that only uses U256 operations and prove that variant equivalent to the one using Z. The proof essentially boils down to showing that it can be implemented in a way that avoids any over/underflows during the U256 operations involved in the computation.

Preliminaries

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

Whether an address is currently delegated in the core state.

^ None means the signature was invalid

^ address 0 means undelegate

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. We extend the extra fields with a summary of reserve-balance configuration updates (if any) that occurred during execution; these updates are applied with a delayed effect after K blocks, so consensus does not need to inspect transactions to determine current reserve balances.

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

^ index of this transaction in the block. monaddb stores when (blockindex, txindex) an account was born Reserve-balance updates are no longer summarized in TxExtra; they are emitted by the EVM core during execution and applied with a delayed effect.

for any decidable assertion/proposition P, asbool P is a boolean such that (asbool P = true) ↔ P, where ↔ means iff (if and only if)

list of accounts requested to be delegated in transaction txe

list of accounts requested to be undelegated in transaction txe

The type A × B in Coq can be thought of as std::pair<A,B>. The projections .1 and .2 can be used to obtain the first and second components of the pair, respectively.

Our **fee upper bound** is intentionally pessimistic: the consensus rule reasons about gas_limit × gas_price, not about *actual* gas used, which can be hard to efficiently estimate. This excludes storage fees, which are are separately handled below because storage fees are only accounted by consensus for transactions that are allowed to empty. The proofs in this file never unfold the definition of maxTxFee, so nothing will break if this definition is changed.

max storage fee. the exact definition does not matter for our proofs, so we keep it undefined, so our proofs would have to work for all possible definitions. one can choose the body as 0 to effectively disable storage fees

Parameterization by the lookahead window K: Consensus can be ahead of execution by at most K. The n+Kth block must have the state root hash after executing block n. The next two variables are parameters for the rest of the proofs.

Next, we have some simple wrappers for brevity. sender of a transaction:

balance of an account in a given state:

update the value of the key updKey in oldMap to f (oldMap updKey) (f applied to the old value of the key updKey in the map)

update balance of the account addr such that the new value is upd applied to the old value

value transfer field of a of a transaction

addresses delegated or undelegated by tx

block number of a transaction

A transaction may emit multiple reserve-balance updates (e.g., via repeated precompile calls). Each entry targets a specific address.

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.

^ last *settled* reserve balance value for this account (defaults to DefaultReserveBal).

^ pending reserve balance update (if any), as (value, block).

The settled (non-delayed) configured reserve balance value.

Our modified execution function which does reserve balance checks will use the following type as input/output.

balance of an account in a given augmented state

just an abstract helper used in the next two definitions, which choose different instantiations for the proj argument

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

is an account a smart contract?

in state s, is the account at address addr a smart contract?

Consensus Check (algo 1)

Below, we build up the definition of the consensus check consensusAcceptableTxs The “emptying” gate: candidateTx may “empty” the sender's balance iff all three are true about its sender:

• it is *not* currently delegated,
• it had no delegation change within the last K blocks (last K-1 blocks and the prev transactions in the current block),
• it did not send a transaction in the last K blocks.

This gate is what lets consensus handle fee-only budgets and still allows an EOA to empty their account under certain conditions. preIntermediatesState is the latest fully-executed state and intermediates is a list of all the transactions between preIntermediatesState and candidateTx.

Whether this is the first transaction from the sender within the last K blocks and without delegation/undelegation activity in that window. This is a slightly *weaker* condition than isAllowedToEmpty because it ignores delegation/undelegation activity that may appear in candidateTx itself. Hence isAllowedToEmpty implies senderNoRecentActivity, but not conversely (e.g., a tx that contains a self-authorization can make isAllowedToEmpty false while senderNoRecentActivity remains true). A precise characterization of this gap is given later in Lemma isAllowedToEmpty_false_senderNoRecentActivity.

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, userConfiguredReserve).
• 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. Z is the type of mathematical numbers in Coq: unbounded, exact arithmetic (no over/under flows). At the end of this file, we implement in Coq the algorithm using just U256, while still avoiding over/underflows and thus prove equivalence

delayed user reserve balance: latest update whose block index plus K is ≤ n.

delayed user reserve balance at address addr in the state map.

initial effective reserve balances, before any proposed tx. For delayed URB, the initial value is a placeholder; the first time a sender appears, we recompute using the block number of that tx (via the senderNoRecentActivity and advanceEffReserveBals steps). For senders that never appear in the suffix, this placeholder is irrelevant.

Advance the effective-reserve map to a block b by clamping each entry to the delayed reserve balance effective at b.

Consensus’ decrement step: The next defn is the algebraic heart of consensus check algorithm: fold this function left-to-right over the entire sequence of proposed txs, and you get the remaining worst-case protected reserve for every sender. Formally, this function conservatively estimates the remaining effective reserve balance of the sender of candidateTx after executing candidateTx, assuming prevErb is the estimate of the reserve balance of the sender of candidateTx just before executing candidateTx. preIntermediatesState is the latest fully-executed state and intermediates is a list of all the transactions between preIntermediatesState and candidateTx. In the definition of newBal (let binding), the subtraction is capped below at 0: the result is non-negative. So, if sbal < maxTxFee candidateTx + value candidateTx but maxTxFee next ≤ sbal, this transaction (candidateTx) will be accepted but all subsequent ones (with maxTxFee > 0) from the same sender will be rejected as the remaining effective reserve balance becomes 0. This function represents the check that consensus needs to do when adding candidateTx at the end of the already built/proposed valid sequence of txs intermediates. candidateTx will be accepted iff the returned value is non-negative. The intermediates list is used only for the isAllowedToEmpty check and to detect whether the sender already appeared in the last K blocks. So the Rust implementation can optimize it by instead just maintaining the necessary summaries (the set of senders and the set of addrs that are delegated or undelegated in those txs).

The file also contains a finite-width (U256) variant of the consensus checks; see Section U256Consensus near the end. Next, we just "fold" the above function over the entire sequence of proposed transactions, starting from the first one after the fully executed state. Note how in the recursive call, we add the processed head to the list of intermediate transactions. As with the function above, postStateAccountedSuffix is only used to track whether the sender already appeared in the suffix and for the isAllowedToEmpty check. An optimized implementation can maintain just the necessary summaries instead of the full list.

Algorithm 1 (consensus): acceptability of a suffix

postStateProposedTxs 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 postStateProposedTxs, 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 postStateProposedTxs 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. The main complication is that some EOAs may be delegated and thus transactions sent to them can make arbitrary debits that are hard to statically estimate without actually executing the transaction. Thus, we have a dynamic check at the end of execution, to check if some EOA account (possibly other than the sender) was debited too much. First, some helpers for that. isAllowedToEmptyExec is a trivial wrapper used in execution, where there are NO 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 delayed reserve-config changes. It applies all reserve updates emitted during execution (possibly for multiple addresses) only on successful execution; updateExtraStateNoReserve is used on revert, and only promotes already-pending updates (it discards any new reserve updates from the reverted tx).

if multiple updates are applied in a single block, the latest wins

Abstract execution and revert

We postulate a single-step EVM core (evmExecTxCore) that returns the new state, a transaction result (receipt), 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. The list (list EvmAddr) returned by evmExecTxCore contains all the changed accounts.

Algorithm 2 (execution): execute a transaction

Next, we define execValidateTx, which assumes that t has already been validated to ensure that the sender has enough balance to cover maxTxFee. It uses a helper allFinalBalSufficient, which we define first. Execution, as defined by execValidateTx, proceeds as follows:

• Run the core EVM step to obtain the *actual* post state.
• For *changed* accounts, allFinalBalSufficient checks that the account was not debited too much, which may endanger the fee solvency of the later transactions already accepted by consensus.
• If any check fails, revert the tx *and still* update the extra history (so K-window bookkeeping remains accurate). Reserve-balance updates are applied only on success.

allFinalBalSufficient captures the per-account reserve-balance postcondition for a transaction.

Execute a validated tx and return the post-state plus the EVM receipt.

Note that because the isSC 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.

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

Execution check of tx validity: 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. On success, it returns the post-state and receipt for t. 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, returning the final state and receipts. Note that if 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 is 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 stronger. Suppose we split blocks in the theorem above into firstblock and restblocks such that blocks=firstblock++blocksrest and suppose these blocks together are all transactions from the K proposed blocks since the last consensus 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 restblocks, so that it can be extended and then this lemma reapplied:

Proof

core execution assumptions

To prove the theorem fullBlockStep, we needed to make the following assumptions about how the core EVM execution updates balances and delegated-ness. The names of these assumptions 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

This lemma combines the axioms 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 remainingEffReserveBalOfSender

remainingEffReserveBalOfSender is monotone. proof is straightforward by analyzing cases and using Coq's arith automation lia. Monotonicity helpers for Z.min and Z.max.

remainingEffReserveBalOfSender never exceeds the sender's balance, assuming prevErb doesn't.

In the proof of the main correctness theorem, we use a slightly different variant of monotonicity, where in the RHS of ≤, remainingEffReserveBalOfSender 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 remainingEffReserveBalOfSender and the execution lemmas above.

lifts mono2 from remainingEffReserveBalOfSender 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 remainingEffReserveBalOfSender: it underapproximates the resultant effective balance after execution of the transaction. This is the heart of the proof of the top-level correctness theorem fullBlockStep. Proof follows by unfolding definitions and case analysis. uses mono2, execBalLb, and many other lemmas above

lifts the previous lemma from remainingEffReserveBalOfSender to remainingEffReserveBalsL. induction on nextL

Here is a component of 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.

This lemma says that you can execute 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. This follows from exec1 and monoL2

The above 2 lemmas are used to yield the following:

Proof of main theorem:

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

If an account's balance did not decrease, the reserve-balance check cannot fail for that account. finalBalSufficient preTxState postTxState t a is the condition that is checked at the end of a transaction t for every changed account a. If the check returns false for any changed account, the transaction is reverted: see execValidatedTx above

Consensus checks using finite-width arithmetic (U256).

Below we define remainingEffReserveBalOfSenderF, which is equivalent to remainingEffReserveBalOfSender, but only uses finite-width arithmetic (U256), instead of the unbounded/exact Z, where one does not need to worry about over/underflows. The main idea is to represent a Z by option U256 where None represents all the negative numbers. All negative values of remaining effective reserve balance are useless anyway. The definition of remainingEffReserveBalOfSenderF will look almost exactly like remainingEffReserveBalOfSender except that it uses variants of arithmetic operations (like -, `min`, `max`) that work on option U256 instead of Z.

below, we define precisely what it means for an o:option U256 is equivalent to a z:Z

Below, we define variants of previous definitions where Z is substituted in by U256. The suffix F stands for finite width numbers.

Helper projections relying on the invariant that balances already fit in 256 bits.

The definition of remainingEffReserveBalOfSenderF will look almost exactly like remainingEffReserveBalOfSender except that it uses variants of arithmetic operations (like -, `min`, `max`) that work on option U256 instead of Z. So, we define those operations on option 256 and prove that they respect the equivalence u256z_equiv. The first one is the min operation:

^ the min of 2 negative numbers is always a negative number

We easily prove that our min operation on option U256 respects the u256z_equiv relation: on inputs that are equivalent, the outputs of u256_opt_min and Z.min are equivalent

max operation on option U256