Coq model of reserve balance and proof of safety

This is a new proposal for reserve balance checks. It is drastically simpler and much easier to implement/maintain than the one currently implemented in Monad, and yet has the same safety theorems proved in Coq. This document does not assume that you understand the old one, except mentioning the differences at some places, which you can safely ignore. This document uses the same names for analogous definitions, so that you can compare and judge the simplifications in this new proposal. Whenever we say “old design” below, we mean the reserve-balance mechanism currently implemented in Monad. Main advantages of this proposal:

• No need to maintain history of previous 2K transactions. Any *currently* undelegated sender is allowed to empty, even if it sent many other transactions in the same block or was delegated earlier in the same block. There can be many emptying transactions.
• The execution check is *strictly* more liberal, so transactions are less likely to revert. The only execution change is the new (more permissive) definition of isAllowedToEmpty.
• The definitions and proofs are much shorter (< 1/2 the size in Coq).
• Consensus checks are more liberal in some ways and less liberal in others. They are more liberal because several emptying transactions in the same block are allowed, as long as the balance lower-bound estimates allow it. They are less liberal in the sense that they may reject some sequences that the previous design allowed, but those transactions would have reverted during execution anyway unless there was an intervening credit. A concrete example:

Alice: balance = 100, reserve = 5, undelegated
tx1: sent by Alice, fee 6, value 1 (balance ≈ 93 after tx1)
tx2: some tx from Bob that does not change any account's delegation status
tx3: sent by Alice, fee 2, value 91 (needs ≈93 total, fully consuming the budget)
tx4: sent by Alice, fee 1, value 0

This sequence would be allowed by the old consensus check algorithm: tx1 is allowed to empty, so Alice's effective reserve balance after tx1 becomes 5, which the old logic treats as enough to pay the fees of the remaining transactions from Alice (because they are deemed not allowed to empty). During execution, tx3 would revert unless tx2 credited Alice's account. In the new proposal, tx4 will not be accepted and tx3 will not revert during execution. Consensus lowers the balance estimate for Alice to 0 after tx3, so tx4 is rejected. Tx3 is also allowed to empty because it is not delegated. If tx2 indeed credited Alice, tx4 can be accepted by the new consensus check in the Kth block after the credit, because by that time the full execution result of the block containing the credit is available. It can be argued that minimizing tx reverts is more important for a good user experience because reverts cost the user, and delaying transaction inclusion to a later block when there is revert risk may be a fair price to pay for it. The simplicity and ease of implementation are other pros for this new proposal. Next, we give a very brief overview of the design in the new proposal and then look at several examples illustrating the difference in consensus/execution behavior. Only then do we present the Coq definitions of the new design.

Design Overview:

The model has two cooperating pieces:

• **Consensus** does a very shallow execution of transactions to only compute 3 pieces of info for each account (the implementation can be sparse):
  • whether the account is delegated after the tx
  • the current configured reserve balance
  • a lower bound on the balance of the account. a tx is accepted if its sender's pre-tx lowerbound is enough to cover the max fee.
• **Execution**: exactly the same as before, except for the simpler (and more liberal) definition of isAllowedToEmpty: execute the core EVM step and then check each changed delegated/non-code account to ensure it did not dip too far into the reserve; otherwise revert.

Examples illustrating the difference

Below are more examples contrasting the consensus and execution behavior difference between the old design and the new proposal:

Example 2:

Alice: bal 100, reserve 5, undelegated
tx1: alice, fee 6, value 10
tx2: alice, fee 6, value 10

• consensus: the new design accepts this sequence of 2 txs but the old one rejects tx2 because the estimate of remaining reserve balance after tx1 is less than the fee of 6. Because Alice remains undelegated throughout, its balance lower bound can be more precisely computed by tracking the value transfers, so the new design of consensus checks knows that tx2 has enough balance to cover the fee.
• execution: the new design will not revert tx2 because it is allowed to empty because it is undelegated.

Example 3:

Alice 100, undelegated, reservebal =5
tx1: sender Alice, delegates Alice, value 10, fee 1
tx2: Bob sends to Alice, and a delegated smart-contract execution debits her by 20
tx3: sender Alice, undelegates Alice, value 0, fee 1
tx4: sender Alice, value 10, fee 1

• consensus: both new and old designs will accept. In the new proposal, consensus maintains a lower bound on every account's balance and ensures that the lower bound is enough to cover the fees. Once an account is delegated, its lower bound drops to the min of the previous lower bound and configured reserve balance. After tx4, in the new design, the balance lower bound estimate becomes negative for Alice and thus no more transactions from Alice will be accepted for the next K blocks.
• execution: only the old design will unnecessarily revert tx4. In the new proposal, tx4 will be considered emptying because it is not delegated and will NOT revert.

Main artifacts:

• Consensus check: consensusAcceptableTxs.
• Execution step (with its check): execValidatedTx (called by execTx).
• Main “safety” theorem: fullBlockStep, says that if a sequence of txs is accepted by consensus, the execution of that sequence cannot run into an error due to inability to pay the fee.

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). If this proposal is adopted, we can write a U256 (finite-width arithmetic) version and prove it equivalent, ideally under no additional assumptions.

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.

A transaction that reconfigures a user's reserve balance cannot also change any delegation status. In the implementation, the data-structure design probably will not allow both. Here, we simply ignore the reserve-balance update of a transaction if the transaction delegates or undelegates.

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.

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

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

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

Does tx delegate/undelegate addr?

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.

The extra (non-EVM) state needed to be maintained by execution to implement reserve balance checks. Note that this had many more (history) fields in the old design

^ current configured reserve balance of the account (defaults to the global reserve if it never reconfigured).

We thread the EVM state with this metadata. This “augmented state” is the substrate both consensus and execution read from and update.

Whether an address currently has code. excludes cases where the code is just 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 (Algorithm 1)

Consensus maintains **shallow execution summary** per account that is deliberately lossy but safe: it pessimistically lowers a “balance lower bound” and threads the configured reserve cap and delegation flag. This is sufficient to enforce fee‑solvency for any yet‑to‑run suffix. Shallow summary for a single account after shallow execution of a sequence of transactions from a fully executed state:

Pessimistic **lower bound** on the account’s balance:

the account's configured reserve balance:

is the account delegated? :

Shallow execution results of all accounts. It is a pair containing:

• a bool indicating whether the sequence of proposed txs is fee-solvent so far, and
• each account's shallow state after shallow execution.

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 shallow execution result, before executing any proposed transactions. s will typically be the last fully executed/finalized state. If an account is not delegated, its balance lower bound is the entire balance in s. Otherwise, we take the minimum of its balance and the configured reserve balance of the account. The fee-solvency bool (first element of the pair) is true because we are starting with an empty proposal.

the new delegation status of an account after executing tx

Shallow execution of a transaction

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 final result of shallow execution. The first component of the result indicates fee solvency. Formally, this function conservatively estimates the ShallowExecResults after executing candTx (cand is just short for candidate), assuming prevRes is the shallow execution result just before candTx. A few things to note:

• it is monotone (proven in the lemma mono below)
• if the account is delegated, the balance lower bound drops to the min of the previous lower bound and the configured reserve balance
• updates the shallow account state (ShallowExecRes) of not just the sender but also every account that got delegated in candTx
• the fee-solvency bool is true iff the previous result itself was solvent and the previous lower bound on balance was greater than or equal to maxTxFee candTx

We can fold the function above over the entire list of proposed transactions, chaining the results.

Consensus acceptability.

A suffix proposedTxs is **acceptable** if the fee-solvency bool is true in the final result.

Execution Check (algo 2)

The execution logic is also tweaked to ensure that a transaction cannot dip too much into reserves and thereby fail to cover the 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 see if some delegated EOA account (possibly other than the sender) was debited too much. Consensus carries a more precise balance lower-bounding for non-delegated accounts, so execution can let non-delegated accounts empty. Trivial wrapper defining whether the sender is delegated after executing tx in state s.

Notice that we did not need any “isAllowedToEmpty” concept in defining consensus checks. The execution check is the same as in the old design, except that the definition of “is allowed to empty” is radically simplified: it does not need any history of previous transactions and is equivalent to the sender being not delegated *after* executing the transaction.

Helper to update the extra metadata (just the configured reserve balance of each account).

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. Note that the checks are trivial for accounts that have code or are not delegated after executing t.
• If any check fails, revert the tx.

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

Cryptographic difficulty 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 because a head tx lacks enough fee balance.

^ Moreover, the tail remains fee‑solvent (and keeps the hygiene side conditions), enabling induction over blocks.

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 many of the execution lemmas above to build a lower bound of the balance of any account after executing a transaction.

Order and monotonicity for shallowExecTx

We define a “≤” ordering relation on ShallowExecRes values of an account: balances must be ≤ and the other fields must be equal.

this tells Coq to parse l ≼ r as (sresLe l r)

Now we lift the above pointwise order to all accounts to define a “≤” relation on full results (of all accounts). Recall that the results are a pair where the first component is the fee-solvency boolean and the second component is the ShallowExecRes of each account. We only enforce the ≼ relation for the accounts that are in a given set of EOAs. eoas will later be instantiated to the list of all senders in the proposed sequence of transactions.

Reasoning principles for the shallow execution

Two generic themes appear repeatedly:

• **Monotonicity.** If you start from a pointwise larger shallow map, one shallow step (and therefore the whole fold) keeps you pointwise larger. This is the heart of the “execute head, refine the budget, and the tail still passes” argument.
• **Under‑approximation.** A single shallow step *under‑approximates* the effect of the real execution step on the quantities we guard in the execution check. This bridges Algorithm 1 (consensus) and 2 (execution).

The helper relations above (e.g., resLe/sresLe) capture the pointwise orderings the monotonicity results use.

One‑step monotonicity for the shallow execution of a transaction. Proof by unfolding definitions, case analysis, and arithmetic reasoning

monotonicity of shallow executing a list of transactions. proof by induction on extension, using mono.

Under‑approximation for one head step.**

exec1 formalizes the intuition that one shallow step from the initial summary **under‑approximates** (w.r.t. balance) the effect of the real execution step on the quantities Algorithm 2 guards (protected slice for non‑senders and fee budget for the sender). This is the key bridge from consensus to execution.

From one step to many

Two small lemmas express that fee‑solvency of a *tail* implies fee‑solvency of a *prefix* (decreasingness), and lift that from one step to lists.

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 monoL

The two lemmas above combine 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
execTxSenderBalCore :
  ∀ (tx : TxWithHdr) (s : StateOfAccounts),
    (maxTxFee tx ≤ balanceOfAc s (sender tx))%N
    → reserveBalUpdateOfTx tx = None
      → let sf := (evmExecTxCore s tx).1 in
        senderDelegatedAfterTx s 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 && 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