Fuzz with Echidna

[PaulRBerg]

Echidna can't currently be used in this repo because solc v0.8 is not supported by crytic-compile. Once there is support for v0.8, we should write invariant contracts for Echidna to be able to fuzz test the math library.

Assumptions to validate:

• [ ] The signed result in PRBMathSD59x18.exp2 can never overflow type(int256).max.
• [ ] The result can never be type(uint256).max in mulDivFixedPoint when (1) x * y = type(uint256).max * SCALE and (2) (x * y) % SCALE >= SCALE / 2

[PaulRBerg]

Update: as per this comment, it looks like Solidity v0.8 is supported by Echidna.

[sandybradley]

$ ./echidna-test contracts/test/PRBMathUD60x18.t.sol --contract TestPRBMathUD60x18
Analyzing contract: /.../contracts/test/PRBMathUD60x18.t.sol:TestPRBMathUD60x18
echidna_mulUint:  failed!💥
  Call sequence:
    setX(115916773041390072873637598212453390567932363729484377996870)


echidna_Uint_convertion:  failed!💥
  Call sequence:
    setX(115962837499224411198969207499961588040517688084412876519766)


echidna_divUint:  failed!💥
  Call sequence:
    setX(115989750869986627937072895547572258287879165164826483095329)
    setX1(1)

PRBMathUD60x18.t.sol

pragma solidity ^0.8.0;

import "../libraries/PRBMathUD60x18.sol";
import "../libraries/SafeMath.sol";
// We import this library to be able to use console.log
import "./hardhat-console.sol";

contract TestPRBMathUD60x18 {
    uint256 internal x;
    uint256 internal x1;

    int256 internal y;

    function setX(uint256 _x) public {
        x = _x;
    }

    function setX1(uint256 _x1) public {
        x1 = _x1;
    }

    function setY(int256 _y) public {
        y = _y;
    }

    function echidna_Uint_convertion() public view returns (bool) {
        uint256 z = PRBMathUD60x18.fromUint(x);
        return PRBMathUD60x18.toUint(z) == x;
    }

    function echidna_mulUint() public view returns (bool) {
        uint256 mul = SafeMath.mul(x, x1);

        uint256 z = PRBMathUD60x18.fromUint(x);
        uint256 z1 = PRBMathUD60x18.fromUint(x1);
        uint256 t = PRBMathUD60x18.mul(z, z1);
        return PRBMathUD60x18.toUint(t) == mul;
    }

    function echidna_divUint() public view returns (bool) {
        if (x1 == 0 || x == 0 || x < x1) return true;
        uint256 div = SafeMath.div(x, x1);

        uint256 z = PRBMathUD60x18.fromUint(x);
        uint256 z1 = PRBMathUD60x18.fromUint(x1);
        uint256 t = PRBMathUD60x18.div(z, z1);
        return PRBMathUD60x18.toUint(t) == div;
    }
}

[sandybradley]

By comparison ... ABDKMath

$ ./echidna-test contracts/test/ABDKQuad.t.sol --contract TestABDKMathQuad
Analyzing contract: /.../contracts/test/ABDKQuad.t.sol:TestABDKMathQuad
echidna_mulUint:  failed!💥
  Call sequence:
    setX1(1106235220955)
    setX(9390953368914254812617)


echidna_Uint_convertion:  failed!💥
  Call sequence:
    setX(10518526264810785485368401065708505)


echidna_divUint:  failed!💥
  Call sequence:
    setX(10417774989007224423389698535018119)
    setX1(1)

[PaulRBerg]

Hi @sandybradley, thanks so much for creating these scripts.

Can you provide a brief explanation for what you did here, and why do you think the execution failed?

[sandybradley]

Thanks Paul. I think the generic echidna fuzz test finds maximum points of failure up to unit max. In this libraries case, I think 115962837499224411198969207499961588040517688084412876519766 is the designed maximum input. I'm sure there's a way to pass this in as the designed max, so the test passes. In any case, your library performs much better than ABDKMath.

I'm actually looking for a way to handle uints > 256 bit ...

[PaulRBerg]

I think 115962837499224411198969207499961588040517688084412876519766 is the designed maximum input

This is correct.

I'm sure there's a way to pass this in as the designed max, so the test passes

There should be, but I don't know how to do it either.

In any case, your library performs much better than ABDKMath.

Lovely to hear!

I'm actually looking for a way to handle uints > 256 bit ...

Depending on what you want to achieve, you may already be able to do it using PRBMath's mulDiv implementation. Actually, the PRBMath functions mul and div use mulDiv under the hood, to allow intermediary calculations up to 2^512 but revert when the result ends up being bigger than 2^256.

[sandybradley]

Thanks Paul. I used this in the end. https://github.com/SimonSuckut/Solidity_Uint512

[PaulRBerg]

Very interesting stuff, thanks for sharing.

[PaulRBerg]

Closing this since I have switched to Foundry in the meantime, and Forge has support for fuzzing by default.