3 State Map
One of the key components of this project is the notion of state mapping. Since we want to show that KEVM and the EvmYul models agree on opcode execution, we need a notion of state equivalence to evaluate the agreement.
So far we are only doing one side of the equiavlence. Namely, from KEVM to EvmYul. This shows that what KEVM does is agreed on by the EvmYul model. Hence, the state mapping we present here will map a KEVM state into an EvmYul one.
3.1 Type Mapping
The first thing for mapping KEVM states to EvmYul states is to convert KEVM types to their corresponding EvmYul ones. Because KEVM operates on integers and then imposes restrictions on their value when applying rules, such restrictions don’t exist at the type level. This is important to keep in mind since when mapping integers representing EVM values, we don’t have to translate the full generality of the KEVM types. But we need to be mindful on how the integers are used in each instance in order to provide an accurate mapping.
The first step is to choose a default on how to map integers themselves to EvmYul’s UInt256.
Given \(n\) of type SortInt, \(\text{intMap}\, n =\, \)UInt256.toSigned\(\, n\).
Once we have the mapping of one of the fundamental KEVM underlying types, we have to map KEVM’s cells. K cells are extracted to Lean as structs that act as a wrapper for an integer value or for another wrapper.
As an example, take SortGasCell, Lean’s extraction of KEVM’s gas cell which is used to track the amount of gas left:
structure SortGasCell : Type where val : SortGas
We see that it’s a wrapper for a SortGas value, and that SortGas follows the same structure:
inductive SortGas : Type where | inj_SortInt (x : SortInt) : SortGas
The fact that SortGasCell has a SortGas value and not a plain SortInt is to avoid the mixing of integer values at the cell level.
Given this, the mapping of SortGasCell will come down to unwrapping it to its SortGas value and in turn map its SortInt contents through the intMap function to EvmYul’s UInt256.
3.2 State Mapping
Once we have mapped a subset of KEVM generated types to their corresponding EvmYul’s images, we can map KEVM states to EvmYul ones.
KEVM states are represented by the type SortGeneratedTopCell. Hence, we will be taking as input a SortGeneratedTopCell and converting it to an EVM.State.
The state mapping function will take an extra EVM.State argument to perform the identity mapping on the parts of the state that are not yet mapped.
3.3 Axiomatic Mapping
Some of the state mapping is done in an axiomatic manner. This is because of two different reasons. First, we have not yet committed to a definitive map structure for the Lean extracted code. Second, since the EvmYul model is more geared towards execution than reasoning, we’ve decided to not commit to their underlying map structure based on Red-Black trees.
To this effect, we postulate as axioms the existence of the following functions:
SortAccountsCellMap: maps SortAccoutsCell to AccountMap.
SortAccessedStorageCellMap: maps SortAccessedStorageCell to the type of accessedStorageKeys.
SortStorageCellMap: maps SortStorageCell to Storage.
SortTransientStorageCellMap: maps SortTransientStorageCell to Storage.
3.3.1 Axioms as pre-theorems
Since these are uninterpreted functions, we also assert behavioral axioms on how these functions have to behave. These axioms serve as a blueprint for any future implementation of these functions, since whatever implementation is chosen should render the behavioral axioms as theorems.