feat(invariant): support fuzz with random msg.value

[QiuhaoLi]

Motivation

Currently, the foundry's invariant fuzz testing doesn't support txs with value > 0, which makes it unable to find sequences in some situations. For example, the Pay contract below will only set the hacked variable if the calls are C() --> B() --> A() with 2, msg.value>0.11 ether, 0, but foundry can't generate such calls.

contract Pay {
    uint256 private counter;
    bool public hacked; // CBA with 2,msg.value>0.11,0

    function A(uint8 x) external {
        if (counter == 2 && x == 0) hacked = true; else counter = 0;
    }
    function B() external payable {
        if (counter == 1 && msg.value > 0.11 ether) counter++; else counter = 0;
    }
    function C(uint8 x) external {
        if (counter == 0 && x == 2) counter++;
    }
}

contract PayTest is Test {
    Pay public pay;

    function setUp() public {
        pay = new Pay();
    }
    /// forge-config: default.invariant.runs = 10000
    function invariant_Pay() view external {
        assertEq(pay.hacked(), false);
    }
}

Solution

When generating a tx, we set the msg.value as a random number (uint96) if the target function is payable. After applying this strategy, foundry can find the sequence quickly:

qiuhao@pc:~/tmp$ ./forge test
[⠊] Compiling...
[⠑] Compiling 1 files with Solc 0.8.26
[⠘] Solc 0.8.26 finished in 564.77ms
Compiler run successful!

Ran 1 test for test/Counter.t.sol:PayTest
[FAIL. Reason: invariant_Pay replay failure]
        [Sequence]
                sender=0x0000000000000000000000000000000000000190 addr=[test/Counter.t.sol:Pay]0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f calldata=C(uint8) args=[2]
                sender=0x0000000000000000000000000000000000000851 addr=[test/Counter.t.sol:Pay]0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f calldata=B() args=[] value=[79228162514264337593543950333]
                sender=0x0000000000000000000000000000000000000103 addr=[test/Counter.t.sol:Pay]0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f calldata=A(uint8) args=[0]
 invariant_Pay() (runs: 1, calls: 1, reverts: 1)
Suite result: FAILED. 0 passed; 1 failed; 0 skipped; finished in 3.95ms (1.31ms CPU time)