2

I have the following smart contract that I'm looking to apply formal verification to.

// SPDX-License-Identifier: MIT
pragma solidity 0.8.20;

contract FuzzCanCatch {
    uint256 public total;

    constructor() {
        total = 100;
    }

    // Invariant: this should never revert
    function hellFunc(uint128 randomNumber) public view returns (uint256) {
        uint256 response = total / randomNumber;
        return response;
    }
}

The above function has an invariant that hellFunc should never return 0, however, it obviously returns 0 when 0 is passed as input.

The following test case attempts to apply FV to it. Fuzzing easily solves it.

// SPDX-License-Identifier: MIT
pragma solidity 0.8.20;

import {Test} from "forge-std/Test.sol";
import {StdInvariant} from "forge-std/StdInvariant.sol";
import {FuzzCanCatch} from "../../src/invariant-break/fuzz-cant-catch/FuzzCanCatch.sol";

contract FuzzCantCatchTest is StdInvariant, Test {
    FuzzCanCatch fuzzCanCatch;

    function setUp() public {
        fuzzCanCatch = new FuzzCanCatch();
    }

    function testCatchEasyBugWithFuzz(uint128 randomNumber) public view {
        uint256 response = fuzzCanCatch.hellFunc(randomNumber);
        assert(response >= 0);
    }
}

$ forge test --mt testCatchEasyBugWithFuzz
[⠰] Compiling...
[⠒] Compiling 56 files with 0.8.20
[⠢] Solc 0.8.20 finished in 11.37s
Compiler run successful!

Running 1 test for test/invariant/FuzzCantCatchTest.t.sol:FuzzCantCatchTest
[FAIL. Reason: Division or modulo by 0 Counterexample: calldata=0x0xb7cfac490000000000000000000000000000000000000000000000000000000000000000, args=[0]] testCatchEasyBugWithFuzz(uint128) (runs: 47, μ: 7791, ~: 7791)
Test result: FAILED. 0 passed; 1 failed; 0 skipped; finished in 2.83ms

But halmos does not.

 $ halmos --function testCatchEasyBugWithFuzz
[⠰] Compiling...
[⠒] Compiling 56 files with 0.8.20
[⠢] Solc 0.8.20 finished in 11.39s
Compiler run successful!

Running 1 tests for test/invariant/FuzzCantCatchTest.t.sol:FuzzCantCatchTest
[PASS] testCatchEasyBugWithFuzz(uint128) (paths: 1/3, time: 0.04s, bounds: [])
Symbolic test result: 1 passed; 0 failed; time: 0.07s

(Passing is a bad thing)

Why is this happening?

1 Answer 1

2

Halmos ignores normal reverts and only catches assertion failures -- so we need to assert that the function did not revert.

To fix, you can do a low level call and check the return value on the test instead.

function testCatchEasyBugWithFuzz(uint128 number) public view {
        // uint256 response = fuzzCanCatch.hellFunc(randomNumber);
        // assert(response >= 0);
        // perform low level call
        (bool success,) =
            address(fuzzCanCatch).staticcall(abi.encodeWithSelector(fuzzCanCatch.hellFunc.selector, number));
        assert(success);
    }

And get the following output:

halmos --function testCatchEasyBugWithFuzz

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.