Proposing new tx execution output and reserve update modeling
I'm proposing to change evmExecTxCore to return a tuple including reserve balance updates as a list of (EvmAddr * N) rather than storing them inside TxExtra. This allows reserve updates produced during smart contract execution to live in the execution state, not the transaction metadata. The updated output would be (postTxState, txr, changed, reserveUpdates). Then execValidatedTx can consume this and updateExtraState will be redefined to accept and merge these reserve updates directly, removing reliance on reserveBalUpdateOfTx. Reserve updates apply only to affected accounts, reflecting that contract calls can update diverse accounts, not only the sender. Reverts should discard these updates. I'll keep existing handling of lastTxInBlockIndex and lastDelUndelInBlockIndex in updateExtraStateBase unchanged. An applyReserveBalUpdates function will perform merging of these updates into ExtraAcStates per block. This design keeps reserve updates aligned with execution outcomes and separates them cleanly from TxExtra.
Proposing clear updated definitions removing reserveBalUpdateOfTx
I'm proposing to remove reserveBalUpdate from TxExtra and the reserveBalUpdateOfTx accessor, replacing them with a new type alias:
Definition ReserveBalUpdate := (EvmAddr * N).
Definition ReserveBalUpdates := list ReserveBalUpdate.
Then, update evmExecTxCore to return the reserve balance updates alongside execution state and changed accounts:
Variable evmExecTxCore : StateOfAccounts -> TxWithHdr -> ((StateOfAccounts * TxResult) * list EvmAddr) * ReserveBalUpdates.
Accessors for the execution results adjust accordingly:
Definition evmExecTxCoreState s t := (evmExecTxCore s t).1.1.
Definition evmExecTxCoreUpdates s t := (evmExecTxCore s t).2.
Also, define applyReserveBalUpdates to fold these updates into ExtraAcStates at a given block number, and modify updateExtraState to accept the updates list instead of relying on reserveBalUpdateOfTx. Reverts discard these updates as before.
This cleansly separates reserve updates from TxExtra, models them as an explicit output of evmExecTxCore, and better reflects that SC execution can affect multiple accounts, not just the sender. Proofs depending on reserveBalUpdateOfTx will need later adjustment.
No proofs are updated yet; these are only the new type and function definitions showing the intended modeling change.
Proposing record type for clearer execution result and updated output handling
To simplify handling multiple return values from evmExecTxCore, I propose defining a record:
Record ExecCoreResult := {
exec_post_state : StateOfAccounts;
exec_tx_result : TxResult;
exec_changed_accounts : list EvmAddr;
exec_reserve_updates : ReserveBalUpdates;
}.
Then, evmExecTxCore returns ExecCoreResult instead of nested pairs, clarifying pattern matching and accessor usage.
We remove reserveBalUpdate from TxExtra and delete reserveBalUpdateOfTx. In place, exec_reserve_updates holds arbitrary reserve balance updates produced during execution, accounting for updates to any relevant addresses, including contracts called by SC execution.
updateExtraState now takes a ReserveBalUpdates argument and applies them to ExtraAcStates by folding applyReserveBalUpdate over the updates list, promoting pending balances as needed per address.
Promotion of pending balances still occurs for the sender explicitly in updateExtraState.
This modeling decouples reserve updates from transaction metadata and clarifies the execution result structure, aiding maintainability and reducing pattern-matching confusion. Proofs depending on the old structure will require corresponding updates.
Starting patch to remove reserveBalUpdate from TxExtra and related definitions
I'm preparing to remove the reserveBalUpdate field from TxExtra and the reserveBalUpdateOfTx definition, as well as update the evmExecTxCore type and related functions accordingly. This will set the foundation for integrating reserve balance updates as explicit outputs from evmExecTxCore, enabling further changes to updateExtraState and proofs later.
Proposing new tx execution output and reserve update modeling
I'm proposing to change evmExecTxCore to return a tuple including reserve balance updates as a list of (EvmAddr * N) rather than storing them inside TxExtra. This allows reserve updates produced during smart contract execution to live in the execution state, not the transaction metadata. The updated output would be (postTxState, txr, changed, reserveUpdates). Then execValidatedTx can consume this and updateExtraState will be redefined to accept and merge these reserve updates directly, removing reliance on reserveBalUpdateOfTx. Reserve updates apply only to affected accounts, reflecting that contract calls can update diverse accounts, not only the sender. Reverts should discard these updates. I'll keep existing handling of lastTxInBlockIndex and lastDelUndelInBlockIndex in updateExtraStateBase unchanged. An applyReserveBalUpdates function will perform merging of these updates into ExtraAcStates per block. This design keeps reserve updates aligned with execution outcomes and separates them cleanly from TxExtra.
Proposing clear updated definitions removing reserveBalUpdateOfTx
I'm proposing to remove reserveBalUpdate from TxExtra and the reserveBalUpdateOfTx accessor, replacing them with a new type alias:
Definition ReserveBalUpdate := (EvmAddr * N).
Definition ReserveBalUpdates := list ReserveBalUpdate.
Then, update evmExecTxCore to return the reserve balance updates alongside execution state and changed accounts:
Variable evmExecTxCore : StateOfAccounts -> TxWithHdr -> ((StateOfAccounts * TxResult) * list EvmAddr) * ReserveBalUpdates.
Accessors for the execution results adjust accordingly:
Definition evmExecTxCoreState s t := (evmExecTxCore s t).1.1.
Definition evmExecTxCoreUpdates s t := (evmExecTxCore s t).2.
Also, define applyReserveBalUpdates to fold these updates into ExtraAcStates at a given block number, and modify updateExtraState to accept the updates list instead of relying on reserveBalUpdateOfTx. Reverts discard these updates as before.
This cleansly separates reserve updates from TxExtra, models them as an explicit output of evmExecTxCore, and better reflects that SC execution can affect multiple accounts, not just the sender. Proofs depending on reserveBalUpdateOfTx will need later adjustment.
No proofs are updated yet; these are only the new type and function definitions showing the intended modeling change.
Proposing record type for clearer execution result and updated output handling
To simplify handling multiple return values from evmExecTxCore, I propose defining a record:
Record ExecCoreResult := {
exec_post_state : StateOfAccounts;
exec_tx_result : TxResult;
exec_changed_accounts : list EvmAddr;
exec_reserve_updates : ReserveBalUpdates;
}.
Then, evmExecTxCore returns ExecCoreResult instead of nested pairs, clarifying pattern matching and accessor usage.
We remove reserveBalUpdate from TxExtra and delete reserveBalUpdateOfTx. In place, exec_reserve_updates holds arbitrary reserve balance updates produced during execution, accounting for updates to any relevant addresses, including contracts called by SC execution.
updateExtraState now takes a ReserveBalUpdates argument and applies them to ExtraAcStates by folding applyReserveBalUpdate over the updates list, promoting pending balances as needed per address.
Promotion of pending balances still occurs for the sender explicitly in updateExtraState.
This modeling decouples reserve updates from transaction metadata and clarifies the execution result structure, aiding maintainability and reducing pattern-matching confusion. Proofs depending on the old structure will require corresponding updates.
Starting patch to remove reserveBalUpdate from TxExtra and related definitions
I'm preparing to remove the reserveBalUpdate field from TxExtra and the reserveBalUpdateOfTx definition, as well as update the evmExecTxCore type and related functions accordingly. This will set the foundation for integrating reserve balance updates as explicit outputs from evmExecTxCore, enabling further changes to updateExtraState and proofs later.
Reviewing comment updates
Noted the presence of reserveBalUpdate comments near the top; updating them can be deferred for now while focusing next on updating updateExtraState definitions.
Updating core execution signature
I'm modifying the core execution variable to match the new output format that includes updates, aligning it with the updated extra state handling.
Updating validated transaction execution
I'm adding rbUpdates from evmExecTxCore to the destructured output and passing it to updateExtraState to ensure it uses the new updates.
Preparing to update execution pattern destructuring
I'm identifying all instances of evmExecTxCore s.1 destructuring patterns to update them consistently with the new execS2 and related lemma changes. Next, I'll locate these via search and plan batch or manual updates.
Updating pattern matches for transaction results
I'm adjusting pattern matches around line 810 to include the new nested structure for transaction results, changing bindings to account for additional components introduced in the updated type.
Removing reserveBalUpdateOfTx premises in EVMAssumptions
I'm verifying that the class definitions in EVMAssumptions around execTxSenderBalCore and related methods no longer include reserveBalUpdateOfTx conditions, and planning to patch the class and assumptions by removing these premises accordingly.
Planning precondition checks update
I'll review the start of the class to confirm if old preconditions around execTxSenderBalCore and related methods have already been removed or need updating.
Preparing to update proofs
I'm searching for all occurrences of the removed definition to adjust related proofs to use the new updates list properly.
Planning lemma updates and comment cleanup
Noticing reserved balance updates are now passed differently in proofs, so lemmas referencing them need adjusting to reflect the new update list and simplified proof structure; comments about U256Consensus and Print Assumptions blocks are outdated and can be cleaned later to avoid confusion.
Detailing lemmas for reserve balance updates
Identified key lemmas to formalize how applying reserve balance updates preserves lastTxInBlockIndex and lastDelUndelInBlockIndex, and proves delayedReserveBal remains unchanged within the K-block window despite updates; also recognizing the need to adjust proofs where prior assumptions about updates affecting only sender no longer hold due to possible updates on arbitrary addresses.
Preparing new definitions and code adjustments
I'm formalizing definitions for reserve balance updates and changing evmExecTxCore to return the update list as requested, then planning to adjust proofs and code to handle updated signature and incorporate reserve balance updates accordingly.
Planning lemma updates and comment cleanup
Noticing reserved balance updates are now passed differently in proofs, so lemmas referencing them need adjusting to reflect the new update list and simplified proof structure; comments about U256Consensus and Print Assumptions blocks are outdated and can be cleaned later to avoid confusion.
Detailing lemmas for reserve balance updates
Identified key lemmas to formalize how applying reserve balance updates preserves lastTxInBlockIndex and lastDelUndelInBlockIndex, and proves delayedReserveBal remains unchanged within the K-block window despite updates; also recognizing the need to adjust proofs where prior assumptions about updates affecting only sender no longer hold due to possible updates on arbitrary addresses.
Preparing new definitions and code adjustments
I'm formalizing definitions for reserve balance updates and changing evmExecTxCore to return the update list as requested, then planning to adjust proofs and code to handle updated signature and incorporate reserve balance updates accordingly.
Adjusting destructuring syntax in code
51 additional activitys hidden.