franck44/yul-dafny

Yul semantics and verification in Dafny

yul-dafny's Issues

Create a library for the common low-level Yul functions

What is it about?

When we generate Yul code from Solidity code (solc --ir), a lot of low-level functions are generated.
Examples are:

function revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b() {
     revert(0, 0)
}

function abi_decode_tuple_(headStart, dataEnd)   {
     if slt(sub(dataEnd, headStart), 0) { revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b() }
}

function shift_right_unsigned_dynamic(bits, value) -> newValue {
     newValue := shr(bits, value)
}

function cleanup_from_storage_t_uint256(value) -> cleaned {
    cleaned := value
}

As these functions are common to a lot of Yul code, we may add them to a library in Dafny.
This will enable us to re-use some functions (and their EVM byte code) as well as declutter the code.

To do

Create a library with the functions commonly generated by the Solidity compiler.
Re-factor current examples to use the library.

Implement missing builtin operators

The problem

A limited number builtin operators is supported in the semantics of Yul in Dafny (CommonSem.dfy).
The following builtins are supported:

• arithmetic operators,
• comparison operators,
• bitwise operators,
• memory and storage operators,
• return, revert
• sone context operators (e.g. calldatasize, calldataload).

To do

Implement the remaining builtin operators.

How to do it

The Dafny-EVM has an implementation for all the opcodes of the EVM.
The state of the Yul machine is a trimmed version (Yul has bio stack) of the state of the EVM.
As a result we can generally re-use the Dafny-EVM semantics to implement the Yul semantics.

Example

The semantics of MemSize is provided by the following Dafny function MemSize.

   /**
     * Get the size of active memory in bytes.
     */
    function MSize(st: ExecutingState): (st': State)
    ensures st'.EXECUTING? || st' == ERROR(STACK_OVERFLOW) || st' == ERROR(MEMORY_OVERFLOW)
    ensures st'.EXECUTING? <==> st.Capacity() >= 1 && Memory.Size(st.evm.memory) <= MAX_U256
    ensures st'.EXECUTING? ==> st'.Operands() == st.Operands() + 1
    {
        if st.Capacity() >= 1
        then
            var s := Memory.Size(st.evm.memory);
            if s <= MAX_U256
            then
                st.Push(s as u256).Next()
            else
                ERROR(MEMORY_OVERFLOW)
        else
            ERROR(STACK_OVERFLOW)
    }

The corresponding function in the Yul semantics can be:

   /**
     * Get the size of active memory in bytes.
     */
    function MSize(s: Executing): (r: u256)
    {
      Memory.Size(s.yul.memory);
    }

As the Yul machine does not have a stack nor gas, the semantics of a builtin is usually much easier to write than its counterpart in the EVM.
And because there is no stack, instead of pushing a result on the stack, we can simply return the value.