This post provides a rough explanation for the reserve balance specification in Category Labs’ Monad Initial Specification Proposal.
Special thanks to Abhishek Anand for writing the coq proofs that are linked towards the end.
Why is reserve balance needed?
Monad has asynchronous execution: consensus is allowed to progress with building and validating blocks without waiting for execution to catch up. Specifically, proposing and validating consensus block n only requires knowledge of the state obtained after applying block n-k, where k is a protocol parameter (for synchronous execution, k=1). While asynchronous execution has performance benefits, it introduces a novel challenge: how is consensus supposed to know the validity of a block if it does not have the latest state?
Let’s illustrate this challenge with an example (for our examples, we will use k = 3):
Consensus is validating block 4, which contains a transaction t from Alice with the relevant fields as:
sender=Alice, to=Bob, value=10, gas=1
Consensus only has the state that was obtained by executing block 1:
block=1, balances={Alice: 11}
If consensus simply accepts block 4 as valid because Alice appears to have enough balance, it risks a safety failure. For instance, Alice may have already spent her balance in transaction t’ in block 2. This creates a denial-of-service (DoS) vector, as Alice could cause consensus to include many transactions for free.
First attempt at a solution
One idea is for the consensus client to statically inspect transactions in blocks 2 and later, checking if Alice has spent any value in her transactions. This would let consensus reject block 4 as invalid if any transaction before t (such as t') in blocks 2, 3, or 4 originates from Alice and spends some value or gas.
While this is a fine solution on the face of it, it suffers from two shortcomings:
-
Suppose, as part of smart contract execution in blocks 2 or 3, Alice received a lot of currency. She would have had enough balance to pay for transaction
tdespitet'existing, if only we had the latest state. So, rejecting transactions based solely on static checks is overly restrictive. -
It is not only restrictive, it is also not safe with EIP-7702 (account abstraction). With EIP-7702, Alice could have her account delegated to a smart contract, which can transfer out currency from Alice’s account in a way that is not statically inspectable by consensus. Concretely in our example, Alice does not need to send a transaction like
t'from her account in order to spend currency from her account, if her account is delegated. So our static check would not succeed and it may be unsafe to accept block 4 as valid even if we don’t see any other transaction from Alice in blocks 2,3 and 4.
Reserve balance as the solution
Intuitively, the core idea of reserve balance is as follows: if execution prevents user account balances from dipping below a certain threshold known to consensus, then consensus can safely include user transactions without knowing the latest state and without being vulnerable to the DoS vector described above.
In our example, if execution ensures that Alice’s account cannot be drawn below 1 MON (otherwise, the withdrawing transactions are reverted), then consensus can safely include transaction t, as by definition Alice’s account will have at least 1 MON to pay for transaction t.
This concept can be generalized as follows:
Consensus accepts transactions from user u after the delayed state s as long as the sum of the gas fees for these transactions is below a parameter called user_reserve_balance and, of course, the user’s balance in s. Execution reverts any transaction that causes an account’s balance to dip below user_reserve_balance, except due to transaction fees.
Algorithms 1 and 2 in the reserve balance spec implement this check for consensus and execution, respectively. Algorithm 3 implements the mechanism to detect the dipping into the reserve balance (Algorithm 2 uses Algorithm 3 to revert transactions that dip).
Now we enrich our description by incorporating cases in which transaction senders are allowed to dip into their reserve balance outside of the gas fees. This is useful for users to be able empty out their account, for example.
First notice that if a user account is undelegated, then consensus can simply inspect transactions statically in order to estimate the lowest a user’s balance can possible go (thanks to the way EVM works, an undelegated user’s account can only be debited due to value transfers and gas fees specified in the transaction data, and not due to any smart contract execution).
Therefore, for an undelegated account, execution can just let the transaction dip arbitrarily and consensus can account for it by adjusting its estimate of the balance accordingly. These cases of emptying transactions are handled in Algorithms 1 and 2 for consensus and exeuction respectively.
One “emptying transaction” is allowed in k blocks. This implies that for a transaction to be considered emptying, there should not be another transaction from the sender in the prior k blocks.
It is important to note that for an undelegated account, the first transaction in a k block window is NOT subject to reserve balance checks in consensus and execution.
Algorithm 4 specifies the criteria for emptying transactions:
-
The sender account must be undelegated in the prior
kblocks. This is checked statically by verifying the account was undelegated in a known state in the pastkblocks, and there has been no change in its delegation status in the lastkblocks (this can be inspected statically). -
There must not be another transaction from the same sender in the prior
kblocks.
Consensus validity checks (Algorithm 1) do not perform reserve balance checks on emptying transactions. Consensus just adjusts the balance estimate due to any prior emptying transaction before checking the reserve balance criteria on subsequent (non-emptying) transactions. Similarly, Algorithm 3 (used for checking whether execution can dip into the reserve balance) allows sender accounts to dip below the threshold if the transaction is an emptying transaction.
Coq proofs
We proved the safety of the reserve balance specification in Coq. The full proofs documentation is available https://category-labs.github.io/category-research/reserve-balance-coq-proofs.
The consensus check is formalized in Coq as consensusAcceptableTxs. The predicate, consensusAcceptableTxs s ltx, defines the criteria for the consensus module to accept the list of transactions ltx on top of state s.
We proved that consensusAcceptableTxs s ltx implies that when the execution module executes all the transactions in ltx one by one on top of s, none of them will fail due to having insufficient balance to cover gas fees. The proof is by induction on the list ltx: one can think of this as doing natural induction on the length of ltx. The proof in the inductive step involves unfolding the definitions of the consensus and execution checks and considering all the cases. In each case, the estimates of effective reserve balance in consensus checks is shown to be conservative w.r.t. what happens in execution.
Setting the reserve balance parameter
We now discuss briefly what are the tradeoffs with respect to the reserve balance parameter:
-
If the parameter is set too low, not many transactions (or, more precisely, not much gas across multiple transactions) can be pending execution (i.e., sequenced by consensus but not executed).
-
If it is set too high, user accounts that are delegated or that send more than one transaction in
k(=3) blocks cannot have their balances dip below this threshold; any transaction that would dip below will revert.
More Examples
Finally, we end this post with some examples along with the expected outcome, for the reader’s exercise. Each example is independent.
In the following examples, we use start_block = 2, meaning the initial balances and reserves are after block 1. We also specify the reserve balance parameter for each example, although it is a constant system wide parameter.
For each transaction, the expected result is:
-
2: Successfully executed
-
1: Included but reverted during execution (due to reserve balance dip)
-
0: Excluded by consensus
Example 1: Basic Transaction Inclusion
Initial state:
-
Alice: balance = 100, reserve = 10
-
Bob: balance = 5, reserve = 10
Transactions:
Block 2: [
Alice: send 1 MON, fee 0.05 — Expected: 2
Bob: send 2 MON, fee 0.05 — Expected: 2
]
Final balances:
-
Alice: 98.95
-
Bob: 2.95
Example 2: Low Reserve Balance but High Balance
Initial state:
- Alice: balance = 100, reserve = 1
Transactions:
Block 2: [
Alice: send 3 MON, fee 2 — Expected: 2 (emptying transaction)
Alice: send 3 MON, fee 2 — Expected: 0 (excluded)
]
Final balance:
- Alice: 95.0
Example 3: Multi-Block, Low Reserve but High Balance
Initial state:
- Alice: balance = 100, reserve = 1
Transactions:
Block 2: [
Alice: send 3 MON, fee 2 — Expected: 2
]
Block 5: [
Alice: send 3 MON, fee 2 — Expected: 2
]
Final balance:
- Alice: 90.0
Example 4: Comprehensive
Initial state:
- Alice: balance = 100, reserve = 1
Transactions:
Block 2: [
Alice: send 99 MON, fee 0.1 — Expected: 2 (large emptying transaction)
]
Block 3: [
Alice: send 0.5 MON, fee 0.99 — Expected: 0 (excluded)
]
Block 4: [
Alice: send 0.8 MON, fee 0.1 — Expected: 1 (included but reverted)
]
Block 5: [
Alice: send 0 MON, fee 0.9 — Expected: 0 (excluded)
Alice: send 5 MON, fee 0.1 — Expected: 1 (included but reverted)
Alice: send 5 MON, fee 0.8 — Expected: 0 (excluded)
]
Final balance:
- Alice: 0.70
Example 5: Edge Case — Zero Value Transactions
Initial state:
- Alice: balance = 2, reserve = 1
Transactions:
Block 2: [
Alice: send 0 MON, fee 0.5 — Expected: 2
Alice: send 0 MON, fee 0.6 — Expected: 2
Alice: send 0 MON, fee 0.5 — Expected: 0 (exceeds reserve)
]
Final balance:
- Alice: 0.9
Example 6: Reserve Balance Boundary
Initial state:
- Alice: balance = 10, reserve = 2
Transactions:
Block 2: [
Alice: send 1 MON, fee 2 — Expected: 2 (matches reserve)
Alice: send 0 MON, fee 0.01 — Expected: 2
]
Final balance:
- Alice: 6.99