We are continuing to specify the Ethereum Virtual Machine (EVM) in the formal verification language Coq. We are working from the automatic translation in Coq of the reference implementation of the EVM, which is written in the language Python.

In this article, we will see how we specify the EVM in Coq by writing an interpreter that closely mimics the behavior of the Python code. We call that implementation a *simulation* as it aims to reproduce the behavior of the Python code, the reference.

In contrast to the automatic translation from Python, the simulation is a manual translation written in idiomatic Coq. We expect it to be ten times smaller in lines compared to the automatic translation, and of about the same size as the Python code. This is because the automatic translation needs to encode all the Python specific features in Coq, like variable mutations and the class system.

In the following article, we will show how we can prove that the simulation is correct, meaning that it behaves exactly as the automatic translation.

The code of this project is open-source and available on GitHub: formal-land/coq-of-python. This work follows a call from Vitalik Buterin for more formal verification of the Ethereum's code.

## The `add`

function 🧮

We focus on a simulation for the `add`

function in vm/instructions/arithmetic.py that implements the addition primitive of the EVM. The Python code is:

`def add(evm: Evm) -> None:`

"""

Adds the top two elements of the stack together, and pushes the result back

on the stack.

Parameters

----------

evm :

The current EVM frame.

"""

# STACK

x = pop(evm.stack)

y = pop(evm.stack)

# GAS

charge_gas(evm, GAS_VERY_LOW)

# OPERATION

result = x.wrapping_add(y)

push(evm.stack, result)

# PROGRAM COUNTER

evm.pc += 1

Most of the functions of the interpreter are written in this style. They take the global state of the interpreter, called `Evm`

as input, and mutate it with the effect of the current instruction.

The `Evm`

structure is defined as:

`@dataclass`

class Evm:

"""The internal state of the virtual machine."""

pc: Uint

stack: List[U256]

memory: bytearray

code: Bytes

gas_left: Uint

env: Environment

valid_jump_destinations: Set[Uint]

logs: Tuple[Log, ...]

refund_counter: int

running: bool

message: Message

output: Bytes

accounts_to_delete: Set[Address]

touched_accounts: Set[Address]

return_data: Bytes

error: Optional[Exception]

accessed_addresses: Set[Address]

accessed_storage_keys: Set[Tuple[Address, Bytes32]]

It contains the current instruction pointer `pc`

, the stack of the EVM, the memory, the code, the gas left, ...

As the EVM is a stack-based machine, the addition function does the following:

- It pops the two top elements of the stack
`x`

and`y`

, - It charges a very low amount of gas,
- It computes the result of the addition
`result = x + y`

, - It pushes the result back on the stack,
- It increments the program counter
`pc`

.

Note that all these operations might fail and raise an exception, for example,if the stack is empty when we pop `x`

and `y`

at the beginning.

## Monad for the simulations 🧪

The main side-effects that we want to integrate into the Coq simulations are:

- the mutation of the global state
`Evm`

, - the raising of exceptions.

For that, we use a state and error monad `MS?`

:

`Module StateError.`

Definition t (State Error A : Set) : Set :=

State -> (A + Error) * State.

Definition return_ {State Error A : Set}

(value : A) :

t State Error A :=

fun state => (inl value, state).

Definition bind {State Error A B : Set}

(value : t State Error A)

(f : A -> t State Error B) :

t State Error B :=

fun state =>

let (value, state) := value state in

match value with

| inl value => f value state

| inr error => (inr error, state)

end.

End StateError.

Notation "MS?" := StateError.t.

We parametrize it by an equivalent definition in Coq of the type `Evm`

and the type of exceptions that we might raise.

In Python the exceptions are a class that is extended as needed to add new kinds of exceptions. We use a closed sum type in Coq to represent the all possible exceptions that might happen in the EVM interpreter.

For the `Evm`

state, some functions might actually only modify a part of it. For example, the `pop`

function only modifies the `stack`

field. We use a mechanism of lens to specialize the state monad to only modify a part of the state. For example, the `pop`

function has the type:

`pop : MS? (list U256.t) Exception.t U256.t`

where `list U256.t`

is the type of the stack, while the `add`

function has type:

`add : MS? Evm.t Exception.t unit`

We define a lens for the stack in the `Evm`

type with:

`Module Lens.`

Record t (Big_A A : Set) : Set := {

read : Big_A -> A;

write : Big_A -> A -> Big_A

}.

End Lens.

Module Evm.

Module Lens.

Definition stack : Lens.t Evm.t (list U256.t) := {|

Lens.read := (* ... *);

Lens.write := (* ... *);

|}.

We can then lift the `pop`

function to be used in a context where the `Evm`

state is modified with:

`letS? x := StateError.lift_lens Evm.Lens.stack pop in`

## Typing discipline 👮

We keep in Coq all the type names from the Python source code. When a new class is created we create a new Coq type. When the class inherits from another one, we add a field in the Coq type to represent the parent class. Thus we work by composition rather than inheritance.

Here is an example of the primitive types defined in base_types.py:

`class FixedUint(int):`

MAX_VALUE: ClassVar["FixedUint"]

# ...

def __add__(self: T, right: int) -> T:

# ...

class U256(FixedUint):

MAX_VALUE = 2**256 - 1

# ...

We simulate it by:

`Module FixedUint.`

Record t : Set := {

MAX_VALUE : Z;

value : Z;

}.

Definition __add__ (self right_ : t) : M? Exception.t t :=

(* ... *).

End FixedUint.

Module U256.

Inductive t : Set :=

| Make (value : FixedUint.t).

Definition of_Z (value : Z) : t :=

Make {|

FixedUint.MAX_VALUE := 2^256 - 1;

FixedUint.value := value;

|}.

(* ... *)

End U256.

For the imports, that are generally written with an explicit list of names:

`from ethereum.base_types import U255_CEIL_VALUE, U256, U256_CEIL_VALUE, Uint`

we follow the same pattern in Coq:

`Require ethereum.simulations.base_types.`

Definition U255_CEIL_VALUE := base_types.U255_CEIL_VALUE.

Module U256 := base_types.U256.

Definition U256_CEIL_VALUE := base_types.U256_CEIL_VALUE.

Module Uint := base_types.Uint.

This is a bit more verbose than the usual way in Coq to import a module, but it makes the translation more straightforward.

## Final simulation 🪶

Finally, our Coq simulation of the `add`

function is the following:

`Definition add : MS? Evm.t Exception.t unit :=`

(* STACK *)

letS? x := StateError.lift_lens Evm.Lens.stack pop in

letS? y := StateError.lift_lens Evm.Lens.stack pop in

(* GAS *)

letS? _ := charge_gas GAS_VERY_LOW in

(* OPERATION *)

let result := U256.wrapping_add x y in

letS? _ := StateError.lift_lens Evm.Lens.stack (push result) in

(* PROGRAM COUNTER *)

letS? _ := StateError.lift_lens Evm.Lens.pc (fun pc =>

(inl tt, Uint.__add__ pc (Uint.Make 1))) in

returnS? tt.

We believe that it has a size and readability close to the original Python code. You can look at this definition in vm/instructions/simulations/arithmetic.v. As a reference, the automatic translation is 65 lines long and in vm/instructions/arithmetic.v.

## Conclusion

We have seen how to write a simulation for one example of a Python function. We now need to do it for the rest of the code of the interpreter. We will also see in a following article how to prove that the simulation behaves as the automatic translation of the Python code in Coq.

For our formal verification services, reach us at contact@formal.land 🏇! To know more about what we have done, see our previous project on the verification of the L1 of Tezos.