del ASSERT that relied on suboptimality of reserve balance accounting

[aa755]

The 2 occurrences of MONAD_ASSERT_THROW that are being deleted are basically the same: one for the uncached and one for the cached implementation of reserve balance.

There is a history of problems with this assert. In November2025, it was changed from MONAD_ASSERT to MONAD_ASSERT_THROW when it was discovered that this assert can fire when balance overrides are used in the RPC path. At that time, it was believed, including by me, that the assert can only fire in the RPC path but not when running as a live mainnet node where the transactions are coming from consensus which checks reserve balance conditions.

While doing the Coq proof of this C++ code, I found that although it would not fire in live mainnet context, the reasoning is much more tricky than I thought initially thought. Perhaps the authors/reviewers had the same misunderstanding. Also, the reasoning may actually not hold if we further optimize the reserve balance design to be more permissive to users (e.g. allow multiple emptying transactions, track statically known credits to non-delegated accounts): if we do that, this deleted assert may crash the node under some interleavings of optimistic execution.

The issue is that even though consensus has ensured this assert condition, it estimates that by considering transactions sequentially (debiting fees (and value for emptying txs) one by one). But at this point in code, we may be doing speculative execution so the accound balances and account codes (which determines the delegation status) may be wrong/different from what will happen in the actual sequential execution, so the consensus guarantee of reserve balance being sufficient to pay at least the fee do not apply directly. Fortunately, there is no problem currently because the reserve-balance design is not very aggressive: it allows only 1 emptying transaction and disregards even statically known credits, even to non-delegated accounts:

We do validate the transactions before reaching this point and only reach here when validation succeeds. The validation success implies that the original balance (speculatively assumed pre-tx balance) is at least as large as the max fee (+tx.value). For non-emptying transactions, this is sufficient because consensus also checks that for non-emptying transactions max_fee is <= 10 MON, and these 2 assumptions imply the asserted condition:

Lemma foo (original_bal value gas_fee: N) :
  value + gas_fee <= original_bal (* condition checked by transaction validation in execution. original_bal may be a speculated value *)
  -> gas_fee <= 10 (* condition checked by consensus for non-emptying txs. gas_fee is fixed for a tx and not affected by speculation *)
  -> gas_fee <= original_bal `min` 10 (* this assert *).
Proof. lia. Qed.

But for emptying transactions, consensus does not check that gas_fee <= 10. Fortunately, the assert occurs only inside the non-emptying case, when can_sender_dip_into_reserve returns false. But one problem is that because of speculation, the Account::code read in dipped_into_reserve to computed the delegation status for can_sender_dip_into_reserve may not be what consensus used its calculations. But that turns out to not be a problem. This assert only pertains to the sender and we know the sender's address cannot be an SC (cryptographic hardness).So the sender's code is either empty or has a delegaton marker. But there can be a delegation mismatch: consensus considered the sender's account delegated as it would be in a sequential execution but this account is not delegated in speculative execution, or vice versa.
But if consensus determined that the tx was allowed to empty, then execution would also make the same determination: even if it speculatively reads Account::code even before the previous transaction has finished or even started. The reason is as follows:
If consensus determined that the tx was allowed to empty, there must be no delegation/undelegation requests (EIP7702 authorities) for the sender in this block, at least till this transaction. Also, the account must be undelegated at the beginning of the block. Also, any sender's account cannot be a smart contract, so Account::code must be empty. Thus Account::code must be empty in the pre-block state and remains empty during the execution of all the previous transactions. So even if speculative execution reads an state that is not that from the just previous transaction, it will read the correct delegation status (not delegated): the same as what consensus used in its calculations.

[Copilot]

Pull request overview

Removes two MONAD_ASSERT_THROW checks in reserve-balance enforcement that could fire under speculative execution / RPC balance overrides, avoiding node crashes from assertions that rely on subtle reserve-balance accounting assumptions.

Changes:

• Deleted an assertion in the uncached dipped_into_reserve(...) path that assumed violation_threshold must be present for non-dipping senders.
• Deleted an assertion in the cached ReserveBalance::update_violation_status(...) path that assumed sender_gas_fees_ <= reserve.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Pull request overview

Copilot reviewed 3 out of 3 changed files in this pull request and generated no new comments.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[dhil]

Looks reasonable to me.

[aa755]

I have kept commits separate to aid re-reviews. After reviews, I will squash all commits to one.

[aa755]

Just FYI: this changes the externally visible behaviour of RPC. previously, the execution used to throw when fee < min (10, pretx balance). now it doesnt and the tx reverts