4 EvmYul Summaries
A prior step to proving any notion of equivalence is to encapsulate or summarize the computational content of both models. In the KEVM case, the computational content is summarized by a rewrite rule on the KEVM side, and then extracted to Lean as shown in the Rewrite.lean file.
The way summarizing the computational content for the EvmYul model will come in the form of theorems. To know which theorems we need to take a step back and look at which parts of the two models we want to equate. On the KEVM side, it’s the summaries in form of constructors of the Rewrites type. On the EvmYul side, we don’t have as fine-grained semantic steps as KEVM’s rewrite rules for opcode execution, so we will produce theorems that state the specific semantic steps we’re interested in. With this in mind, we will focus on two of the core EvmYul functions: EVM.step and EVM.X.
EVM.step orchestrates opcode execution, taking the following arguments.
Amount of gas left: fuel
Cost of executing the opcode: gasCost
Opcode to be executed: instr
Given these arguments and an EVM.state, the step function will perform the correspondent updates on the provided state according to the semantics of instr.
From this definition there are a couple of things to be noted.
The instr parameter is of type Option and as such can be none, in which case the opcode is fetched from the execution environment’s bytecode.
gasCost is always given by functions calling step.
If fuel is not strictly positive, step will immediately fail.
This means that while the step function captures a big portion of the executed opcode’s semantics, it is not the full picture.
To incorporate a most complete picture of opcode semantics execution we turn to the EVM.X function. This function iterates the above EVM.step and performs several important actions.
Formalization of the yellow paper’s \(X\) function as defined in section 9.4.
Given the following arguments:
Amount of gas left: fuel.
Valid jumpdests: validJumps.
An EVM.State: evmState.
The function X performs the following tasks:
Decode the opcodes present in evmState’s execution environment.
Perform sanity checks and halt execution if these are not met.
Assign gas costs depending on the decoded opcode.
Execute EVM.step with the current decoded opcode.
Iterate if the conditions are right.
Since the X function operates on the evmState’s bytecode, in order to exercise its semantic content we will execute it but restricting evmState’s bytecode to be a one-opcode program.
4.1 EVM.step and EVM.X summary
We can now state summarization theorems for step and X. Given a fully symbolic EVM.State \(S\), summarization theorems clearly state which are the precise state updates that occur to \(S\) after executing the step or X functions with the following:
A set of concrete opcodes.
Enough gas to perform execution.
Well-formedness of other inputs to the functions such as a symbolic stack.
The sets of concrete opcodes are created by grouping opcodes that have similar effects to \(S\). For instance, we can group all opcodes that perform operations on the stack such as ADD, SHL and so on, and have a general enough theorem that captures the effects of these opcodes on \(S\) without having to do a separate summary for each of them.