Allow parametrised invariants

[andreas-blockswap]

Component

Forge

Describe the feature you would like

I would like to be able to parametrise my invariants. For example

function invariantSomePropertyTest(uint256 _x) external {
  uint256 expectedResult = computeExpectedResult();
  uint256 actualResult = computeActualResult(_x);
  assertEq(expectedResult, actualResult);
}

This should work like a normal invariant test with a fuzzing campaign, but every time a non-parametrised invariant would call the function, the parametrised invariant should generate multiple calls with fuzzing.

The invariant fuzzing campaign brings the contract in many different states before testing the property, which is useful because it allows detection of bugs that depend on a particular chain of function calls before showing up.

I have implemented a quick a dirty PoC on my fork https://github.com/andreas-blockswap/foundry/tree/invariant-parameters

Additional context

No response

[mds1]

I'm not sure I understand the feature request here, can you clarify?

The invariant fuzzing campaign brings the contract in many different states before testing the property, which is useful because it allows detection of bugs that depend on a particular chain of function calls before showing up.

This is exactly what the current invariant testing does. If you have an invariant test called invariantSomePropertyTest() what happens is:

1. forge runs the code within that test and verifies the assertions pass. If they fail, the test fails.
2. forge fuzzer executes a random call to your contracts to mutate state.
3. The code within that test is re-run to verify the assertions pass. If they fail, the test fails.
4. Repeat steps 2-3 depth times

Check out the invariant testing docs for more info

[andreas-blockswap]

The feature request is to add support for parameters/input to invariant functions, like the parameter uint256 _x in the example.

What I meant by

The invariant fuzzing campaign brings the contract in many different states before testing the property, which is useful because it allows detection of bugs that depend on a particular chain of function calls before showing up

is that the combination invariant fuzzing + parameters is useful together.

Does that clarify?

[mds1]

Ah, so you want step 3 to basically act like a fuzz test within the invariant test? Do you have a concrete example of where that would be useful? Because my initial reaction is that what should be tested inside your invariant tests are things like "sum of all balance equals total supply", where fuzzing doesn't make sense because your invariant test is already considering the full state of your contracts

[andreas-blockswap]

Ah, so you want step 3 to basically act like a fuzz test within the invariant test?

Yes I want a step like that.

Do you have a concrete example of where that would be useful?

The following is an example where it is useful:

contract MyMath {
  uint256 private oops;
  /// Implementation of addition
  function add(uint256 _x, uint256 _y) external view returns (uint256) {
    return _x + _y + oops; // NOTICE the bug
  }
  function setOops(uint256 _oops) external {
    oops = _oops;
  }
}

The test contract

contract TestMyMath is Test {
  MyMath internal myMath;
  function setUp() {
    myMath = new MyMath();
  }
  function testAdd(uint256 _x, uint256 _y) external {
    assertEq(myMath.add(_x, _y), _x + _y);
  }
  function invariantTestAdd(uint256 _x, uint256 _y) external {
    assertEq(myMath.add(_x, _y), _x + _y);
  }
}

Here testAdd does not catch the bug, but invariantTestAdd will most likely catch the bug.

Because my initial reaction is that what should be tested inside your invariant tests are things like "sum of all balance equals total supply", where fuzzing doesn't make sense because your invariant test is already considering the full state of your contracts

Indeed, if I am just testing an invariant. But invariant functions can be used to test properties, which is more powerful than mere test functions, because invariant functions consider many initial states.

I am currently simulating invariant parameters with input as state. What I do is something like

contract MyMathInput {
  uint256 public x;
  uint256 public y;
  function set(uint256 _x, uint256 _y) external {
    x = _x;
    y = _y;
  }
}
contract TestMyMath is Test {
  MyMath internal myMath;
  MyMathInput internal input;
  function setUp() {
    myMath = new MyMath();
    input = new MyMathInput();
  }
  function invariantTestAdd() external {
    assertEq(myMath.add(input.x(), input.y()), input.x() + input.y());
  }
}

But this is far from optimal, since the invariant fuzzing campaign would blindly call input.set 50% of the time. There are other ways to set input state, but I have not been able to make this work in an intelligent way.

[mds1]

Thanks for the examples, that was helpful! The way I'd currently get your desired behavior is with the handler pattern for invariant tests, shown below. This is a very flexible/popular pattern, which you can read more about here:

• https://mirror.xyz/horsefacts.eth/Jex2YVaO65dda6zEyfM_-DXlXhOWCAoSpOx5PLocYgw
• https://book.getfoundry.sh/forge/invariant-testing

// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.13;

import {Test, console2} from "forge-std/Test.sol";
import {CommonBase} from "forge-std/Base.sol";
import {StdCheats} from "forge-std/StdCheats.sol";
import {StdUtils} from "forge-std/StdUtils.sol";

contract MyMath {
    uint256 private oops;
    /// Implementation of addition
    function add(uint256 x, uint256 y) external view returns (uint256) {
        return x + y + oops; // NOTICE the bug
    }
    function setOops(uint256 _oops) external {
        oops = _oops;
    }
}

// All inputs in the handler and test contracts are uint128 to avoid overflows
// in this example (we could also have kept uint256 and used `bound`).
contract MyMathHandler is CommonBase, StdCheats, StdUtils{
    MyMath myMath;

    constructor(MyMath _myMath) {
        myMath = _myMath;
    }

    function myMath_add(uint128 x, uint128 y) external view {
        uint256 z = myMath.add(x, y);
        require(z == x + y, "invariant broken");
    }

    function myMath_setOops(uint128 _oops) external {
        myMath.setOops(_oops);
    }
}

contract TestMyMath is Test {
    MyMath internal myMath;
    MyMathHandler internal myMathHandler;

    function setUp() public {
        myMath = new MyMath();
        myMathHandler = new MyMathHandler(myMath);

        // Only call methods on the handler contract.
        targetContract(address(myMathHandler));
    }

    function testAdd(uint128 x, uint128 y) external {
        assertEq(myMath.add(x, y), uint256(x) + y);
    }

    function invariantTestAdd() external {
        // We hardcode a few test vectors here, and add additional `require`
        // statements on the fuzzed handler method above. (Regular assertions
        // are not yet supported in handlers, see https://github.com/foundry-rs/foundry/issues/4718)
        assertEq(myMath.add(1, 2), 3);
        assertEq(myMath.add(4, 9), 13);
    }
}

[andreas-blockswap]

I want parametrisation of the invariant function in order to avoid hard coded inputs. Your invariant function fails to find this bug:

    function add(uint256 x, uint256 y) external view returns (uint256) {
        if (x == 1 || y == 9) return x + y;
        return x + y + oops; // NOTICE the bug
    }

[mds1]

You don't actually need those hardcoded inputs, they were just examples. You can leave them in or comment them out, but if you set the invariant fail_on_revert = true setting in your config, you will see my invariant test does find that bug. It's able to find it because of the require statement, which serves the same purpose as your suggestion, i.e. that method in the handler is effectively fuzzed.

Here's the fixed version that finds your bug (my above version had a view modifier which IIRC prevents forge from calling it)

// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.13;

import {Test, console2} from "forge-std/Test.sol";
import {CommonBase} from "forge-std/Base.sol";
import {StdCheats} from "forge-std/StdCheats.sol";
import {StdUtils} from "forge-std/StdUtils.sol";

contract MyMath {
    uint256 private oops;
    /// Implementation of addition
    function add(uint256 x, uint256 y) external view returns (uint256) {
        if (x == 1 || y == 9) return x + y;
        return x + y + oops; // NOTICE the bug
    }

    function setOops(uint256 _oops) external {
        oops = _oops;
    }
}

// All inputs in the handler and test contracts are uint128 to avoid overflows
// in this example (we could also have kept uint256 and used `bound`).
contract MyMathHandler is CommonBase, StdCheats, StdUtils {
    MyMath myMath;

    constructor(MyMath _myMath) {
        myMath = _myMath;
    }

    function myMath_add(uint128 x, uint128 y) external {
        uint256 z = myMath.add(x, y);
        require(z == x + y, "invariant broken");
    }

    function myMath_setOops(uint128 _oops) external {
        myMath.setOops(_oops);
    }
}

contract TestMyMath is Test {
    MyMath internal myMath;
    MyMathHandler internal myMathHandler;

    function setUp() public {
        myMath = new MyMath();
        myMathHandler = new MyMathHandler(myMath);

        // Only call methods on the handler contract.
        targetContract(address(myMathHandler));
    }

    function testAdd(uint128 x, uint128 y) external {
        assertEq(myMath.add(x, y), uint256(x) + y);
    }

    function invariantTestAdd() external {
        // We hardcode a few test vectors here, and add additional `require`
        // statements on the fuzzed handler method above. (Regular assertions
        // are not yet supported in handlers, see https://github.com/foundry-rs/foundry/issues/4718)
        assertEq(myMath.add(1, 2), 3);
        assertEq(myMath.add(4, 9), 13);
    }
}

The point of these examples is to show how you can achieve what you are looking to do, even if this feature is not implemented

[andreas-blockswap]

Looks like it makes all invariant functions fail if require(z == x + y) reverts. Is that the intention?

[mds1]

Right, because the check is in the handler contract, which in this example would be used for all invariant tests. A common pattern (which is also great for performance) is to have a single (or a few), and group multiple invaraint assertions within a single test. For example: https://github.com/maple-labs/maple-core-v2/blob/00f01ae7175885f8d49ac201a1c72465e320b2f6/tests/invariants/BasicInvariants.t.sol#L65-L86

[andreas-blockswap]

It is not convenient to implement property tests in this way and the feedback from forge on failing tests is bad like this.

I think it is straight forward to add support for parametrised invariant functions. I have literally just added the missing fuzz step in my fork and seems to work. One can consider more feedback to the user in the end, but not strictly necessary.