Move overflow checks to int lib

[henry-hz]

Let me suggest to make the overflow checks as

WrappedEther.dfy/src/WrappedEtherBinary_deposit.dfy

Line 114 in dc8a523

assert (st.Peek(0) + st.Peek(1)) <= (MAX_U256 as u256);

to the int lib here https://github.com/Consensys/evm-dafny/blob/ede86d640f25f673e1bb204701b4ecaf104c2344/src/dafny/bytecode.dfy#L54 to something like:

    function Add(x: u256, y: u256) : (z: u256) {
        var lhs := x as int;
        var rhs := y as int;
        var res := (lhs + rhs);
        assert res <= MAX_U256;
        res as u256
    }

or

    function Add(x: u256, y: u256) : (z: u256) {
        var lhs := x as int;
        var rhs := y as int;
        var res := (lhs + rhs) % TWO_256;
        res as u256
    }


    function Add'(x: u256, y: u256) : (z: u256)
    requires Add(x,y) < MAX_U256 as u256
    requires Add(x,y) > x
    ensures z < MAX_U256 as u256 {
        Add(x,y)
    }

So we can have the EVM reverting as expected [as from solc 0.8.1] and avoid adding evm responsability into the contract transpilation. Makes sense ?

[DavePearce]

I understand what you are saying, but there are conflicting goals here:

• The DafnyEVM is trying to accurately recreate the EVM. In particular, we run it against the official EVM test suite to check for compliance. Therefore, e.g. ADD must have "wrap around" semantics.
• So, the first suggestion you have above cannot work because it would break EVM compatibility.
• The second option would be fine, but is not really part of the DafnyEVM. Instead it could be part of some supplementary library for verification.

To be honest, just having the assert statements inline is not that big an overhead. One challenge is that arithmetic overflow does occur inside many contracts in a safe fashion (e.g. in code generated by the Solidity compiler). So, the verification engineer has to manually decide whether an assert should actually pass or not. Also, of course, I want to add assert checks for more aspects of EVM execution (see here for a list of ideas). This is a work-in-progress though!

[henry-hz]

Got it, thanks @DavePearce
Indeed the list seems very good!

I think having a math lib for common things like decimal precision to model and emulate protocols in dafny is a good pick for me now, as I am using Dafny to model and check economics, governance, config range inputs and calculations. So far I did this code below, please, let me know if you find the direction is good. The goal is to have a reusable DSMath in dafny.

include "../../lib/evm-dafny/src/dafny/util/int.dfy"
include "../../lib/evm-dafny/libs/DafnyCrypto/src/dafny/util/math.dfy"

module DSMath {
    import opened Int
    import opened MathUtils

    const WAD   : u256 := MathUtils.Pow(10,18) as u256
    const RAY   : u128 := MathUtils.Pow(10,27) as u128

    function Mul(x: u256, y: u256) : (z: u256)
    requires MulOverflowCheck(x as int, y as int) {
        x * y
    }

    /**
     * Add with protected overflow
     */
    function Add(x: u256, y: u256) : (z: u256)
    requires AddOverflowCheck(x as int, y as int) {
        x + y
    }

    /**
     * Because we use modulus, to avoid div by zero we have to return
     * true if x or y are zero, and overflow on x or y itself
     * is already protected by the type u256
     */
    predicate AddOverflowCheck(x: int, y: int) {
        (x == 0) || (y == 0) || ((x + y) != 0 ==> ((x + y) % TWO_256) > x)
    }

    predicate MulOverflowCheck(x: int, y: int){
        (y != 0 && x != 0) ==> ((x * y) % TWO_256) / y == x
    }
}

[DavePearce]

Yeah, definitely looks interesting!

[henry-hz]

Thanks for the feedback, so I think we can close this issue.