5 Equivalences

With what we have defined so far we are in a position to start proving equivalence between KEVM and the EvmYul model. However, first, we need to pinpoint exactly what do we mean by equivalence.

5.1 Defining Equivalence

We define now the notion of equivalence we’re dealing with, and to what extent is it formalized and proven.

The overarching goal is to prove that there exists a bisimulation relation between KEVM and the EvmYul model.

We start by refreshing the definition of a bisimulation.

In our context,

• \(S\) is the union of both KEVM and EvmYul states (\(S_{\text{KEVM}}\) and \(S_{\text{EvmYul}}\) respectively). So we have \(S_{\text{KEVM}}\, \bigcup \, S_{\text{EvmYul}} = S\) and \(S_{\text{KEVM}}\, \bigcap \, S_{\text{EvmYul}} = \emptyset \).

• The transition relation \(\rightarrow \) is execution in any of the models. In particular, we have that \(\rightarrow \, \subset S_{\text{KEVM}} \times S_{\text{KEVM}} \, \bigcup \, S_{\text{EvmYul}} \times S_{\text{EvmYul}}\).

• \(R = \bigl\{ \bigl( p, \text{stateMap}(p) \bigr)\, |\, p\in S_{\text{KEVM}}\bigr\} \, \bigcup \, \bigl\{ \bigl(\text{stateMap}'(q), q\bigr)\, |\, q\in S_{\text{EvmYul}}\bigr\} \) where \(\text{stateMap}\) is defined in 37 and \(\text{stateMap}'\, :\, S_{\text{EvmYul}}\rightarrow S_{\text{KEVM}}\) has not yet been defined.

Note that \(R \subsetneq S_{\text{KEVM}}\times S_{\text{EvmYul}}\). With this in mind, we currently have machinnery to prove the first implication of the bisimulation definition.

Given KEVM states \(p, p'\) with \(p \rightarrow p'\), we know that \(\bigl( p, \text{stateMap}(p) \bigr)\) and \(\bigl( p', \text{stateMap}(p') \bigr)\) belong to \(R\). Hence, to prove the first item we only need to show that \(\text{stateMap}(p) \rightarrow \text{stateMap}(p')\).

Clarifications on \(\rightarrow \)

Saying “the transition relation \(\rightarrow \) is execution in any of the models” is admittedly quite loose. So we can make its definition more precise as follows.

Now we can start describing the proof process more clearly.

5.2 Proof Outline

Given all the above and \(f\in \{ \texttt{step}, \texttt{X}\} \), the first implication translates to

While the second translates to

The above statement is still not fully precise, since we’re only feeding elements of \(S_{\text{EvmYul}}\) to \(f\), but both step and X take more arguments. However, the only argument that we’ll fix is the opcode being executed.

This means that we will be reproducing the above argument on a per-opcode basis. The reasoning being that showing equivalence at the opcode-execution level is fundamental enough to argue that both models share the same understanding of the semantics.

The following example should shine enough light on the specificities that we have left out so far.

5.3 Case Study: Stack Operations

In this example we will be covering proofs for 1 for “stack operation opcodes”, meaning opcodes that perform operations on the stack such as ADD or SHL. Since we’re reproducing the same argument for each opcode, the proof process is architecturally similar across the files.

In fact, for some opcodes, we can bundle them together and reproduce the above argument at once per opcode class.

5.3.1 Opcode Bundling

The main criteria for creating these opcode classes is based on their KEVM summaries. To understand how KEVM summaries condition which opcodes go to each class (which is still a somewhat arbitrary taxonomy) we assume understanding of the anatomy of rewrite rules.

There are two main frictions when bundling opcodes together: how fine-grained we need the state representation to be and how many “steps” does it take for KEVM to encode the state changes.

The fine-grainedness of the state refers to how abstracted the satate is. For instance, instead of specifying symbolic values for all the components of the network cell, we just have a symbolic network cell variable. This is not troublesome in general.

What is more defining for opcode bundling is the amount of steps or conditions needed to encode the state changes performed per opcode. For example, for the ADD opcode we need two conditions (one per operation) to define the value that will be put on the top of the stack. The first condition adds the first two items of the stack, and the second one takes the corresponding modulus:

(defn_Val3 : «_+Int_» W0 W1 = some _Val3)
(defn_Val4 : chop _Val3 = some _Val4)

In this case, _Val4 is going to be the value introduced at the top of the stack.

We can contrast this to the DIV opcode, which only takes one condition to encode the value of the newly added stack item:

(defn_Val3 : «_/Word__EVM-TYPES_Int_Int_Int» W0 W1 = some _Val3)

With this in mind, we first define an inductive type representing all opcodes in this class. The class being “opcodes that perform stack operations and take one condition to summarize the new value added to the stack.”

This definition will allow us to generalize the rest of the description to the whole class of opcodes.

In the remaining of this chapter we’re going to be lying down the formalization process for 1 for the opcode class stackOps_op.

5.3.2 \(\forall p, p'\in S_{\text{KEVM}}\, \, \texttt{Rewrites}\, \, p \, \, p'\)

The first stop is to, given the class of opcodes stackOps_op, identify all \(p, p'\in S_{\text{KEVM}}\) such that \(\texttt{Rewrites}\, \, p \, \, p'\) holds by means of executing any of the opcodes in that equivalence class (written as \(\texttt{Rewrites}_{\texttt{stackOps_op}}\, \, p \, \, p'\)). To achieve this we rely on the following two definitions.

The next step is, given \(p\in \mathcal{Im}(\texttt{oneOpLHS})\) and \(p'\in \mathcal{Im}(\texttt{oneOpRHS})\), to find which are the necessary conditions such that \(\texttt{Rewrites}_{\texttt{stackOps_op}}\, \, p \, \, p'\) holds. For this we turn to the constructors of the \(\texttt{Rewrites}\) type.

Each constructor represents an opcode, encoding the KEVM summary of executing such opcode on a symbolic state. The constructors of the rewrite type in turn contain all the conditions (such as defn_Val3 above) to satisfy the rewrite summary. That is, the necessary conditions that ensure \(\texttt{Rewrites}_{\texttt{stackOps_op}}\, \, p \, \, p'\). The following theorem proves that for any two such \(p, p'\), under the restrictions posed by the constructors associated to the stackOps_op class, \(p\rightarrow p'\).

Note that, oneOpLHS and oneOpRHS being symbolic states, it is also correct to state Rewrites oneOpLHS oneOpRHS. However, this means that oneOpLHS rewrites to oneOpRHS for all possible value of its symbolic parameters. This is generally a false statement without restricting their symbolic values.

5.3.3 \(f\bigl(\text{stateMap}(p)\bigr) = \text{stateMap}(p')\)

Now that we know the conditions under which \(\texttt{Rewrites}_{\texttt{stackOps_op}}\) oneOpLHS oneOpRHS holds, we have to show \(f\bigl(\text{stateMap}(\texttt{oneOpLHS})\bigr) = \text{stateMap}(\texttt{oneOpRHS})\) for \(f\in \{ \texttt{step}, \texttt{X}\} \).

But in order to compute \(f\), first we need to know the values of \(\text{stateMap}(\texttt{oneOpLHS})\) and \(\text{stateMap}(\texttt{oneOpRHS})\). Similarly as with the EvmYul summaries [4], we do this with theorems.

Equipped with these theorems, we can now state and prove the main theorems for the functions step and X. Since X iteratively applies step, we start with the step function.

intMap W0 / intMap W1 = intMap (divWord W0 W1)

With these two theorems proven we can conclude that under the conditions of satisfaction of the summaries for the stackOps_op opcodes, together with some well-formedness constraints, there is a similarity relationship (equation 1) between executing the stackOps_op opcodes in KEVM and executing them in the EvmYul model.

5.4 Future Work

There are a number of items that remain as future work. For one, formalizing and proving equation 2 in a similar fashion to what we’ve shown with equation 1. But within the formalization efforts of equation 1, it remains to close a number of proof obligations and formalizing other classes of opcodes.