# FORVES 2.0: FORmally VErified EVM optimizationS -- leveraging FORVES to inter-block optimizations

## Project Abstract
The FORVES 2.0 project aims at developing a fully automated context-sensitive verification tool in Coq to check semantic equivalence of two EVM sequences given an initial context. This will enable the verification of cross-block optimizations.

## Objectives
### What are you hoping to accomplish with this grant? How do you define and measure success for this project?

The FORVES 2.0 project aims at developing a fully automated context-sensitive verification tool, in Coq, that is able to check the semantic equivalence of two sequences of EVM code given some initial context information. The context information --given by means of constraints involving both stack variables and memory/storage contents-- provides information statically known when reaching the pair of sequences being verified. The direct application of our tool is to verify (and certify) the correctness of inter-block optimizations carried out by the _solc_ compiler, or by any other EVM optimizer, by using as initial context to verify one block the (disjunction of the) output states of its caller blocks. As examples, we can easily capture constant propagation across blocks by instantiating in the initial context the stack or memory contents to the constant values obtained from the output state of the caller block. This in turn enables proving optimizations made in the memory/storage, such as elimination of redundant LOAD/STORE instructions. We will provide an interface to easily integrate our context-sensitive verifier within any tool that requires proving that two fragments of EVM sequences are semantically equivalent given some initial context information.

The FORVES 2.0 project is thus leveraging the results and tool developed in FORVES to enable the verification of inter-block EVM optimizations.

Our starting point is a formally verified equivalence checker (in Coq) that we have developed in the FORVES project. The tool takes as input two jump-free EVM blocks B1 and B2 and a size k of the initial stack, and checks if their executions, when starting from any initial state with a stack of size k, always lead to the same state. This tool has the following main components:

1. a concrete interpreter for a loop-free fragment of EVM, that we use as the EVM semantics in the soundness proofs.

1. a symbolic version of the interpreter that, instead of concrete values, works over symbolic state for the stack, memory and storage

3. optimization rules that are based on predefined patterns, that simplify symbolic states, .e.g, simplifies X*0 to X.

4. a comparator that checks if two (possibly simplified) symbolic states are equivalent.

The work flow of the checker is: it symbolically executes B1 and B2 (using 2), from an initial symbolic state with a stack of size k, to generate two output symbolic states S1 and S2; it simplifies S1 and S2 to S1' and S2' (using the simplification rules in 3); and finally it checks (using 4) that S1' and S2' are equivalent. Note that concrete interpreter is only used in the soundness theorems.

Our challenge is to leverage this checker to incorporate context information and this way enable proofs on inter-block optimizations. The context is given by means of constraints on the initial states from which B1 and B2 can be executed. This overall objective is detailed into the following sub-objectives:

[__O1__] Extend the symbolic states to allow symbolic initial memory/storage (currently this can be done only for the stack, memory/storage are assumed to be "any"). This requires generalizing the notion of variable, from stack variable (as in the current tool) to a general one that can be used anywhere.

[__O2__] Develop a language for context information, i.e., the kind of constraints supported, and all the required machinery in Coq to reason about such constraints.

[__O3__] Integrate context information into the new symbolic states, to allow adding constraints on variables, and thus on the initial values stored on the stack/memory/storage

[__O4__] Develop a comparator similar to the one of point 4 above, but that takes context information into account.

[__O5__] Modify the simplification rules to use the new comparator, this way we can easily migrate them from the existing to the new tool

[__O6__] Modify the overall checker to include context information, and have the following workflow

1. it takes as input two sequences of EVM bytecode B1 and B2 with a specification S of the initial symbolic state (including the context information).

1. it symbolically executes B1 and B2 from S to generate two corresponding symbolic states S1 and S2.

1. it simplifies S1 and S2 into S1' and S2' by applying a sequence of optimization rules.

1. it checks if S1' and S2' are equivalent states taking into account the context information, and the properties such as commutativity of operations.

We will measure the success for the project by applying it on real contracts using the cross-block optimizations performed by the _solc_ compiler.

## Outcomes
### How does this project benefit the greater Ethereum ecosystem?

Ethereum smart contracts developers and owners can be reluctant to use non-verified optimization tools, as they could introduce bugs in the optimized code and cause tremendous damage and economical losses. However, the use of optimization tools can be greatly beneficial for the Ethereum ecosystem both in terms of storage savings (since the size of the EVM bytecode can be reduced) and of gas costs of the transactions (since the gas consumption of the code is reduced).

The FORVES project was a major step to increase the trustworthiness of EVM optimizers. However, due to its limitation to intra-block optimizations, its applicability is not as wide as the Ethereum ecosystem needs, e.g., some of the optimizations performed by the _solc_ compiler cannot be verified. The Ethereum ecosystem will greatly benefit from a verification tool that overcomes the intra-block boundary and can be applied both to prove optimizations performed by the _solc_ compiler as well as other standalone inter-block optimization tools.

## Grant Scope

The problem we want to research is:

Given two jump-free sequences of EVM bytecode instructions B1 and B2, and constraints C on the initial state from which the execution of B1 and B2 starts, we want to formally verify that the executions B1 and B2, when starting from any concrete initial state that satisfies the constraints C, result in equivalent output states. The constraints are mainly numerical, e.g., stating that two stack/memory/storage elements are equal, that a stack/memory/storage element is positive, or stating a linear relation between stack/memory/storage elements.

This problem is key to leverage the work done in FORVES for cross-block optimizations, where B1 is assumed to be the original EVM sequence we want to optimize, C is a set of constraints, inferred by means of a global static analysis, that always hold when reaching B1, and B2 is the result of optimizing B1 under the assumption that C holds.

## Challenges

FORVES 2.0 is based on the FORVES project, where we have developed a certified verifier for context-insensitive jump-free blocks of EVM code in Coq. The way in which we have approached the development of the FORVES 2.0 project would reuse many parts of the original FORVES project, so we do not anticipate unreachable problems. Moreover, we start from a codebase we completely understand and we have gained experience when working with the Coq system.

However, the extension is far from trivial and we may be facing some technical challenges:

1. common problems/challenges that arise when writing programs using a proof assistant such as Coq, usually related to the limitations of the underlying programming language that require writing programs in a particular way to ease the proofs.

1. reasoning with linear constraints involving 256-bit numbers instead of unbounded natural numbers. We plan to rely heavily on the "Bedrock Bit Vectors" Coq library and its proven results to perform this reasoning as simple and efficient as possible, but we may need to extend it with further results and their proofs.

1. when applying the verification tool on optimizations performed by the _solc_ compiler, we will need to obtain that context information from the solc intermediate output and adapt it to our language for context information. This process may face some technical challenges regarding the availability of that information and the transformation between formats.

## Project Team

We are all members of the research team COSTA https://costa.fdi.ucm.es/web, which devises formal techniques and models for optimizing, verifying and understanding programs, and develops related implementation technology. Detailed information on team members, publications, projects, research activities, etc. is accessible from the previous URL.

__Samir Genaim__ is a professor at the Universidad Complutense de Madrid since December 2008. He received a Ph.D in Computer Science from Ben-Gurion University in Israel in 2003, and then was a postdoc researcher at the University of Verona (2003-2005) and the Technical University of Madrid (2006-2008). Samir's research expertise is in the area of formal approaches to program analysis, which includes developing program analysis tools and their underlying theory in order to statically (i.e. without execution) infer run-time properties of a given program. In particular, Samir made fundamental contributions to the fields of cost and termination analysis, with publications in conference like POPL and CAV, and the journal of the ACM. Samir has participated in 15 research national and European research projects. More info at: https://costa.fdi.ucm.es/~genaim/

__Elvira Albert__ is a professor at the Universidad Complutense de Madrid (Spain). Since 2018, she has been building foundations and tools for optimizing and verifying security and safety of Ethereum smart contracts and has published the main results at prestigious international conferences such as CAV, OOPSLA, ISSTA, TACAS and ATVA and given keynote talks at IJCAR'22, VPT'22 and SOAP'22. Elvira has led the GASOL and FORVES projects funded by the Ethereum Foundation and will closely collaborate with Samir on the project management tasks. More info at: https://costa.fdi.ucm.es/~elvira/

__Enrique Martin-Martin__ is a professor at the Universidad Complutense de Madrid (Spain) with 15 years of research experience. He has participated as a researcher in 10+ research projects devoted to the use of formal methods for program analysis. His experience in the semantics of programming languages and formal methods has been essential in the FORVES project and will be very also key for the FORVES 2.0 extension.

We want to employ an advanced programmer with deep knowledge on formal verification to work full-time on the project. We have already been talking to several outstanding candidates who are finishing (or just finished) a double degree on Mathematics and Computer Science and who are very interested in the project.

## Background

The work done in the first stage of the FORVES project has been submitted for its evaluation at the prestigious CAV'23 conference. The paper can be accessed at: https://costa.fdi.ucm.es/papers/costa/forves.pdf

## Methodology and Timeline

### Stage 1: Leveraging the Coq data structures used in FORVES

In this stage we will leverage the symbolic states defined in the former FORVES project to include symbolic memory and storage, as well as including context information using simplified constraints (e.g. only equalities between variables and constants)

- Expected roadmap

- __Month 1 - Month 2__

Extend the symbolic states to allow symbolic initial memory/storage (O1)

Develop a language for simplified context information (O2)

Integrate context information into the new symbolic states (O3)

- Expected result

Definition of the extended Coq data structures required to handle symbolic memory/storage and context information.

- Ballpark Grant ask

10.000 USD

- Use of resources

- 180 hours of the 3 team members

### Stage 2: Proof of concept of the context-sensitive verification tool

In this stage we leverage two key elements of the FORVES checker to manage context information: the symbolic states comparator and some of the simplification rules.

- Expected roadmap

- __Month 3 - Month 4 - Month 5__

Develop a symbolic state comparator that checks if two symbolic states are equivalent by taking the context information into account (O4)

Modify a subset of the simplification rules to use the new comparator (O5)

- __Month 6__

Modify the overall checker to include context information (O6). It takes two sequences B1 and B2 together with a specification of the initial symbolic state, including the context information, and determines if they are equivalent.

Extraction to an OCaml version to generate a Linux binary.

- Expected result

Release of FORVES 1.1, a verifier for optimizations that takes into account basic context information and applies a subset of the optimization rules, and a corresponding deliverable

- Ballpark Grant ask

20.000 USD

- Use of resources

- 300 hours of the 3 team members
- 4 months contract of a full-time developer

### Stage 3: Release of verification tool

In this stage we extend the proof-of-concept developed in the previous stage to enhance the language of context constraints with more complex linear constraints and also extend the available optimization rules used to simplify symbolic states.

- Expected roadmap

- __Month 7 - Month 8 - Month 9 - Month 10__

Extend the proof of concept with more complex constraints: equalities and inequalities involving linear expressions (O4)

Extend the set of optimization rules used in the former FORVES project to use context information (O5)

- __Month 11 - Month 12__

Extraction to an OCaml version to generate a Linux binary of the complete verification tool.

Applying it on real contracts using some of the cross-block optimizations performed by the _solc_ compiler or other EVM optimizers.

- Expected result

Release of FORVES 2.0, a verifier for EVM optimizations taking into account
context information and a final project deliverable

- Ballpark Grant ask

30.000 USD

- Use of resources

- 450 hours of the 3 team members
- 6 months contract of a full-time developer

## Budget

60.000 USD (see details in the different stages in the timeline)