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). 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.

Many of the EVM semantics definitions we use come from Yoichi's EVM semantics, developed several years ago. The definition of block.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., no smart contract invocation or transfer. It must be None for regular transactions (which do not reconfigure the reserve balance). option N in Coq can be thought of as std::optional<N> in C++. None in Coq corresponds to std::nullopt in C++. Transactions to uodate reserve balance will be implemented as a call to a special precompile: A stateful precompile at address 0xRESERVES maintains a mapping from account addresses to their configured reserve balance values. The precompile exposes an update(uint256) function that allows accounts to set their reserve balance. Any internal call (from a smart contract) to the update function of 0xRESERVES causes the transaction to revert. Only EOA accounts may call the precompile’s update function directly. A transaction t is a reconfiguring transaction if it calls the update(uint256) function of the 0xRESERVES precompile (inspectable by the to and calldata field). A reconfiguring transaction is required to have value field set as 0. Behavior of the precompile: When a reconfiguring transaction is executed, the precompile only updates the reserve balance mapping for t.sender to the specified value. The precompile performs no other operations: no balance transfers, no state changes beyond updating the single mapping entry. As a result, a reconfiguring transaction never reverts. This simplicity is assumed for proving the correctness of the reserve balance mechanism.

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

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

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:

value transfer field of a of a transaction

addresses delegated or undelegated by tx

block number of a transaction

returns None if this tx is not a reserve-balance-reconfig tx. Else it returns Some newRb, where newRb will become the new reserve balance threshold of the sender if/when t is executed.

NEW: We assume there is some mechanism by which a user can specify that they intend a transaction to be emptying. We leave it undefined, so our proofs work for any possible way to define it. But note that the definition can only inspect the transaction, e.g. it has no access to history or the current state of accounts. An ideal way to define it would be to have a boolean field in the transaction header. The user needs to understand that if they chose to set this field (thus request to be allowed to empty), consensus will exclude their transactions for the next K blocks. A suboptimal way may be to define it as whether the sender has requested themself to be undelegated in this transaction, but this may have unintended effects if the user did not really mean this tx to be emptying, as consensus will exclude transactions from this sender for the next K blocks

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

NEW: ^ record the last block index where a transaction with an explicit emptying request was sent

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

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 the account a smart contract: must have code that is not a delegation marker

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)

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.

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

some more wrappers:

balance of an account in a given state:

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

balance of an account in a given augmented state

initial effective reserve balances, before any proposed tx

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 only used for the isAllowedToEmpty and senderinForbiddenWindow checks: so the Rust implementation can optimize it by instead just maintaining the 3 pieces of info isAllowedToEmpty needs from intermediates: the set of senders, the set of addrs that are delegated or undelegated, and the set of emptying requestors in those intermediates. NEW:

• in the None case, the top-level branching on senderinForbiddenWindow is new. this is to exclude transactions from senders that recently explicitly requested emptying transactions
• at the end, the branching on reqAllowToEmpty is new. the else case returns the value as before. in the then case we set the effective reserve balance as 0 or negative: transactions from this sender will be excluded anyway for the the next K blocks. Because a user can request a transaction to be emptying even if the account is delegated or sent transactions in the same block, we do not have a good way to estimate its previous balance. We do know its previous effective reserve balance, which we use to determine whether that is enough to pay fees: if not, we return a negative number. If the previous effective reserve balance is sufficient, we return 0: transactions from this sender will be excluded anyway for the the next K blocks.

compare with the old version

regular tx, not one that sets reserve balance:

At the end of this file, we have defined remainingEffReserveBalOfSenderF which is analogous to remainingEffReserveBalOfSender but instead of Z arithmetic (idealized, unbounded), only uses U256 aritmetic. Instead of returning Z, it returns an option U256, where negative numbers are represented by None. In that version, candidateTx is accepted iff the result is not None. We proved that remainingEffReserveBalOfSenderF and remainingEffReserveBalOfSender are equivalent. 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, the intermediates list is only used for the isAllowedToEmpty and senderinForbiddenWindow checks: the Rust implementation can instead maintain aggregate stats, as described above.

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 reserve-config changes.

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. 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:

• 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, 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).

NEW:

• the only change is that isAllowedToEmptyExec s t was replaced with isAllowedToEmptyExec s t || reqAllowToEmpty t

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

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. 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 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 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

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.

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.

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 && asbool (ac ∉ undels tx.1.2) || asbool (ac ∈ dels tx.1.2)
revertTx : StateOfAccounts → TxWithHdr → StateOfAccounts
maxStorageFee : TxWithHdr → N
execTxSenderBalCore :
  ∀ (tx : TxWithHdr) (s : StateOfAccounts),
    (maxTxFee tx ≤ balanceOfAc s (sender tx))%N
    → reserveBalUpdateOfTx tx = None
      → let sf := (evmExecTxCore s tx).1 in
        addrDelegated sf (sender tx) = false
        → (balanceOfAc s (sender tx) - (maxTxFee tx + value tx + maxStorageFee tx) ≤ balanceOfAc sf (sender 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 && asbool (ac ∉ undels tx.1.2) || asbool (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 || isSC 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

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

Subtraction is tricky. if a and b are negative numbers, the result may be negative or positive. But as we represent both a and b by None, we do not have enough information to determine that. Fortunately, in remainingEffReserveBalOfSender, the RHS of subtraction was always known to be non-negative. So it suffices to just define for that case:

^ subtracting a non-negative number from a negative number is always negative

We define some notations to make our definition of remainingEffReserveBalOfSenderF look similar

the line below tells Coq to parse x ⊖ y as u256_opt_sub x y

Finally, below is the U256 version of remainingEffReserveBalOfSender

^ pay attention to the bracketing. If we instead first add up maxTxFeeF candidateTx, valueF candidateTx, and maxStorageFeeF candidateTx, and only then subtract from senderBal, the result of addition may overflow, although only a malicious person would probably send such a transaction

Next we prove equivalence: for that, we need to assume that the balances, configured reserve balance thresholds of all accounts, value, maxTxFee, etc. are within bounds of U256. These are trivial invariants because the EVM datatypes already enforce that

we can now use the above 2 definitions to state the equivalence theorem. The proof is mainly just unfolding definitions and using an arithmetic solver that understands Z.modulo