This repository contributes a shallow embedding of Yul in Dafny. It defines the semantics of the source language, Yul, using a host language, Dafny, by translating Yul structures into Dafny structures.
The instructions of the Yul EVM-Dialect are implemented in a Dafny module Common Semantics.
Yul can be seen as structured EVM bytecode: it has control flow structures (if, for, block, etc) and functions.
It does not provide a stack as in the EVM, but rather variables and scopes.
As a result, it is easier to read than EVM bytecode.
The following example defines a function max and uses it to store (in memory) the largest of two values.
object "Runtime" {
code {
function max(x, y) -> result
{
result := x
if lt(x, y) {
result := y
}
}
// Main code
let x := 8
let y := 3
let z := max(x, y)
mstore(0x40, z)
}
}The built-in functions lt, mstore are part of the EVM dialect of Yul.
This dialect has a single variable/literal type which is u256 (unsigned integers over 256 bits), so the type of all variables (x, y, result) is u256.
Yul has been designed to be easy to translate into EVM bytecode.
This still requires to translate the local variables into stack cells, and implement function calls with jumps instead of standard control structures.
It is also claimed that Yul is a good target for formal verification and this project endeavours to show that indeed it is.
An informal semantics of Yul is defined in the Yul documentation. There are several formal semantics of Yul (see resources below), all them being deep embeddings in the sense that the formalisation provides:
- the syntax of Yul, and
- an operational or denotational semantics of the language.
In this project we propose a shallow embedding a Yul into the (host) verification-friendly language Dafny. A shallow embedding re-uses the host language features (control structures, variables declaration, scopes) to equip the source language (Yul) with a formal semantics that is inherited from the host (Dafny).
For instance, the Yul max function above can be translated into Dafny as:
method Max(x: u256, y: u256) returns (result: u256)
// Specification of max
ensures result == x || result == y
ensures result >= x && result >= y
{
result := x;
if Lt(x, y) { // The Dafny lt instruction returns a Boolean
result := y;
}
}The semantics of assignment, function declarations, if and variables' scopes is inherited from the Dafny semantics.
The advantage of a shallow embedding is that it is usually easier to implement.
The max function above is a good example where the body of the function in Yul and Dafny is almost the same.
The advantage is that we can leverage use the powerful verification features of Dafny to provide some guarantees about the code (e.g. ensures).
The example above embeds a specification (ensures) that defines properties of the function. The Dafny verification engine verifies at compile time that for all input x, y the properties hold.
In our project we provide the semantics of the Yul instructions as a Dafny library in the Yul folder. This library leverages the data structures (states, etc) defined in the EVM in Dafny (Dafny-EVM) project.
Yul is an intermediate representation (IR) that can be compiled to EVM bytecode. The solidity compiler can generate Yul as an intermediate representation of Solidity code:
> solc --ir file.sol >file.yulThe Yul code in 'file.yul' can be compiled into EVM bytecode:
> solc --yul file.yul >file.txtWith a shallow embedding of Yul, we get the ability to prove some properties of Yul programs. We can leverage this feature to prove properties of EVM bytecode generated from Yul.
An example is provided in this folder. The verification works as follow:
- some properties are verified on the Yul code
- we then compile the Yul code into EVM bytecode
- we prove that the bytecode for each function (e.g.
max) simulates the Yul code.
The examples folder contains examples of Yul to Dafny translation and verification.