EVM Equivalence

Evm Models Equivalence

The project’s goal is to prove the equivalence between two mathematical models of the EVM. The mathematical models are Nethermind’s EvmYul and Runtime Verification’s KEVM.

Notably, these two models are written in very different languages: EvmYul in Lean 4 and KEVM in K. The first step to prove equivalence is to have a framework in which to compare what the models do, and then show the equivalence of it.

To this end, the K framework allows for the generation of Lean 4 code representing compiled K definitions. Hence, the methodology is to show in Lean 4 the equivalence between EvmYul and the generated Lean 4 code from the KEVM definitions.

This blueprint will (for the time being) only concern about the Lean proofs on equivalence. For documentation on the more engineering-related topics please refer to the repository.

Overall Approach

What follows is a summary of what is explained in the blueprint.

This project consists of several parts that lead up to proving equiavlence between the EvmYul model and KEVM.

Code generation

The most fundamental layer from the KEVM side is to extract the compiled KEVM definitions to Lean 4. We do this by means of the klean tool.

There are three things of special importance to the generated code.

  • Function termination: There are some generated functions that Lean can’t automatically deduce its termination argument. Modify the code to provide it.

  • Uninterpreted functions: Some functions require an ad-hoc implementation by the Lean 4 backend. When this implementation is not provided they are declared as axioms.

  • Rewrites type: The Rewrites is formatted for better reading.

Refer to to 1 for details.

Reasoning Interfaces

The second layer is that of reasoning interfaces. Files containing results that make reasoning about both models more amenable.

The results present in these files cover from basic facts about the types we’re dealing with to conversions to more friendly representations of convoluted expressions.

KEVM’s GasInterface.lean is particularly time-intensive to execute. For debugging anything unrelated to it it’s advised to sorry our its proofs.

See 2 for more details.

EvmYul Summaries

There is a series of files containing results that encapsulate the computational behavior of EvmYul’s functions for specific opcodes or classes of opcodes. This allows us to have a precise description of the state updates that each opcode entails.

Note that we also have the equivalent of these summaries for KEVM. However, they’re produced differently: KEVM computes the states updates and then they are exported as the constructors of the Rewrites type.

For a more detailed discussion see 4.

State Mapping

Once we have reasonable reasoning interfaces and the summaries of the computational behavior at the opcode level for each model, we define a function that maps states from one model to the other.

So far, we have a mapping from KEVM states to EvmYul ones. It remains as future work to do the inverse direction.

For a more detailed discussion see 3.

Proving Equivalence

The last step is to prove equivalence for each opcode. For a formal deinition of the equivalence definition and proof strategy see 5.

Axioms and sorries

We employ axioms for different uses, from generated uninterpreted functions to blueprints for future function implementations or theorems that should be proven at some point.

See 6 for a more detailed description.