-
Notifications
You must be signed in to change notification settings - Fork 1.1k
EVM with abstract interpretation and backtracking
Describe what abstract interpretation and backtracking means, and how to implement it efficiently
By resources here we understand things that programmer of EVM may use to store and manipulate data, and to perform computations. Some of the resources EVM are accessible directly via opcodes, whereas others - indirectly via side-effects of certain operations.
When EVM is activated (which is usually) by sending a transaction to a deployed smart contract, with some input, the first execution frame is created. It gets its program counter, gas counter, "read only" flag (whether any mutating operations are allowed), input data in memory, and output data region in memory. Execution frame is mostly segregated from other execution frames, but there are few ways they can communicate:
- Via input data
- Via gas counter
- Via storage writes (only for execution frames of the same contract)
Each execution frame has its own stack, and it is only accessible from that one execution frame.
Each execution frame has its own memory. Memory expands in chunks of 32 bytes, when used, but is accessible with the granularity of a single byte.
Whenever an item is read from the state, it potentially modifies state cache, which has an impact on the gas cost of subsequent operations with the same state item. Whenever a state item is created or updated, it also modifies state cache in a different way, which affects the cost of subsequent update operations for the same state item. State caches can be explicitly modelled as EVM resources for better specification and less error-prone implementation, but also for the purpose of implementing the backtracking.
Access lists are related to the state caches in a way that they pre-initialise read caches in a certain way.
Which accounts will be self-destructed and removed from the state at the end of a transaction. Self-destruct lists needs to be explicitly modelled for better specification and less error-prone implementation, but also for the purpose of implementing the backtracking.
Timestamp, block hash, gas limit, base fee
Recent block hashes