Implement missing builtin operators

[franck44]

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.