Why does this afterInvariant test revert?

Question

Context

After applying this solution, the invariant test fails, even though I would expect it to pass.

Invariant.t.sol

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.24;

import {StdInvariant} from "forge-std/src/StdInvariant.sol";
import {Handler} from "./Handler.sol";
import { Test, console } from "forge-std/src/Test.sol";

contract InvariantsTest is StdInvariant, Test {
    Handler public handler;

    function setUp() public {
        handler = new Handler();
        targetContract(address(handler));
    }

    function invariant_test() public  {
        // handler.increment();
        // console.log("Is Incremented=");
        // console.log(handler.isIncrementTested());
        // handler.setNumber(66);
    }

    function afterInvariant() public {
        console.log(handler.isIncrementTested(), handler.isSetNumberTested());
        console.log(handler.numberOfTestRunsForIncrement(), handler.numberOfTestRunsForSetNumber());

        assertEq(handler.isIncrementTested(), true);
        assertEq(handler.isSetNumberTested(), true);
        assertGe(handler.numberOfTestRunsForIncrement(), 3);
        // assertEq( + handler.numberOfTestRunsForSetNumber(), 3);
        console.log("AFTER ALL");
    }
}

Handler.t.sol

pragma solidity ^0.8.24;

import { Test, console } from "forge-std/src/Test.sol";
import { Counter } from "./../../src/Counter.sol";

contract Handler is Test {
  Counter public counter;

  bool public isIncrementTested;
  bool public isSetNumberTested;
  uint256 public numberOfTestRunsForIncrement;
  uint256 public numberOfTestRunsForSetNumber;

  constructor() {
    counter = new Counter();
  }

  function increment() public {
    uint256 numberBeforeIncrement = counter.number();
    if (numberBeforeIncrement < type(uint256).max) {
      counter.increment();
      assertEq(counter.number(), numberBeforeIncrement + 1);
    }
    isIncrementTested = true;
    numberOfTestRunsForIncrement++;
  }

  function setNumber(uint256 x) public {
    counter.setNumber(x);
    assertEq(counter.number(), x);
    isSetNumberTested = true;
    numberOfTestRunsForSetNumber++;
  }
}

Counter.sol

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.24;

contract Counter {
  uint256 public number;

  function setNumber(uint256 newNumber) public {
    number = newNumber;
  }

  function increment() public {
    number++;
  }
}

foundry.toml

[invariant]
runs = 2
depth = 3
fail_on_revert = true

Running

I ran these tests with:

clear && forge test -vvvvvvvv --config-path foundry.toml

Output:

Ran 1 test for test/fuzz/Invariants.sol:InvariantsTest
[FAIL: <empty revert data>] invariant_test() (runs: 2, calls: 258, reverts: 0)
Logs:
  false false
  0 0
  Error: a == b not satisfied [bool]
        Left: false
       Right: true
  Error: a == b not satisfied [bool]
        Left: false
       Right: true
  Error: a >= b not satisfied [uint]
    Value a: 0
    Value b: 50
  Error: a >= b not satisfied [uint]
    Value a: 0
    Value b: 50
  Error: a == b not satisfied [uint]
        Left: 0
       Right: 129
  AFTER ALL

Traces:
  [1188570] InvariantsTest::setUp()
    ├─ [1088848] → new Handler@0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f
    │   ├─ [49499] → new Counter@0x104fBc016F4bb334D775a19E8A6510109AC63E00
    │   │   └─ ← [Return] 247 bytes of code
    │   └─ ← [Return] 4699 bytes of code
    └─ ← [Stop] 

  [209] InvariantsTest::invariant_test()
    └─ ← [Stop] 

  [70959] InvariantsTest::afterInvariant()
    ├─ [2372] Handler::isIncrementTested() [staticcall]
    │   └─ ← [Return] false
    ├─ [350] Handler::isSetNumberTested() [staticcall]
    │   └─ ← [Return] false
    ├─ [0] console::log(false, false) [staticcall]
    │   └─ ← [Stop] 
    ├─ [2384] Handler::numberOfTestRunsForIncrement() [staticcall]
    │   └─ ← [Return] 0
    ├─ [2363] Handler::numberOfTestRunsForSetNumber() [staticcall]
    │   └─ ← [Return] 0
    ├─ [0] console::log(0, 0) [staticcall]
    │   └─ ← [Stop] 
    ├─ [372] Handler::isIncrementTested() [staticcall]
    │   └─ ← [Return] false
    ├─ emit log(val: "Error: a == b not satisfied [bool]")
    ├─ emit log_named_string(key: "      Left", val: "false")
    ├─ emit log_named_string(key: "     Right", val: "true")
    ├─ [0] VM::store(VM: [0x7109709ECfa91a80626fF3989D68f67F5b1DD12D], 0x6661696c65640000000000000000000000000000000000000000000000000000, 0x0000000000000000000000000000000000000000000000000000000000000001)
    │   └─ ← [Return] 
    ├─ [350] Handler::isSetNumberTested() [staticcall]
    │   └─ ← [Return] false
    ├─ emit log(val: "Error: a == b not satisfied [bool]")
    ├─ emit log_named_string(key: "      Left", val: "false")
    ├─ emit log_named_string(key: "     Right", val: "true")
    ├─ [0] VM::store(VM: [0x7109709ECfa91a80626fF3989D68f67F5b1DD12D], 0x6661696c65640000000000000000000000000000000000000000000000000000, 0x0000000000000000000000000000000000000000000000000000000000000001)
    │   └─ ← [Return] 
    ├─ [384] Handler::numberOfTestRunsForIncrement() [staticcall]
    │   └─ ← [Return] 0
    ├─ emit log(val: "Error: a >= b not satisfied [uint]")
    ├─ emit log_named_uint(key: "  Value a", val: 0)
    ├─ emit log_named_uint(key: "  Value b", val: 50)
    ├─ [0] VM::store(VM: [0x7109709ECfa91a80626fF3989D68f67F5b1DD12D], 0x6661696c65640000000000000000000000000000000000000000000000000000, 0x0000000000000000000000000000000000000000000000000000000000000001)
    │   └─ ← [Return] 
    ├─ [363] Handler::numberOfTestRunsForSetNumber() [staticcall]
    │   └─ ← [Return] 0
    ├─ emit log(val: "Error: a >= b not satisfied [uint]")
    ├─ emit log_named_uint(key: "  Value a", val: 0)
    ├─ emit log_named_uint(key: "  Value b", val: 50)
    ├─ [0] VM::store(VM: [0x7109709ECfa91a80626fF3989D68f67F5b1DD12D], 0x6661696c65640000000000000000000000000000000000000000000000000000, 0x0000000000000000000000000000000000000000000000000000000000000001)
    │   └─ ← [Return] 
    ├─ [363] Handler::numberOfTestRunsForSetNumber() [staticcall]
    │   └─ ← [Return] 0
    ├─ [384] Handler::numberOfTestRunsForIncrement() [staticcall]
    │   └─ ← [Return] 0
    ├─ emit log(val: "Error: a == b not satisfied [uint]")
    ├─ emit log_named_uint(key: "      Left", val: 0)
    ├─ emit log_named_uint(key: "     Right", val: 129)
    ├─ [0] VM::store(VM: [0x7109709ECfa91a80626fF3989D68f67F5b1DD12D], 0x6661696c65640000000000000000000000000000000000000000000000000000, 0x0000000000000000000000000000000000000000000000000000000000000001)
    │   └─ ← [Return] 
    ├─ [0] console::log("AFTER ALL") [staticcall]
    │   └─ ← [Stop] 
    └─ ← [Stop] 

Suite result: FAILED. 0 passed; 1 failed; 0 skipped; finished in 393.46ms (391.25ms CPU time)

Ran 4 test suites in 964.63ms (403.65ms CPU time): 3 tests passed, 1 failed, 0 skipped (4 total tests)

Failing tests:
Encountered 1 failing test in test/fuzz/Invariants.sol:InvariantsTest
[FAIL: <empty revert data>] invariant_test() (runs: 2, calls: 258, reverts: 0)

Encountered a total of 1 failing tests, 3 tests succeeded

Question

• Why does it fail? Specifically:
• What is the reason of failure, I can see the empty revert but I did not yet figure out why it reverts.
• (Why does it do 129 runs, even though I set the foundry.toml to 2 runs of depth 3?)

Additional Observations

When I uncommennt:

// handler.increment();
// console.log("Is Incremented=");
// console.log(handler.isIncrementTested());
// handler.setNumber(66);

it says handler.isIncrementTested() is true and immediately after that, in theafterInvariants() it says handler.isIncrementTested() is false. I do not yet understand why.

Answer 1

1. It’s failing because the assertEq condition(s) inside the afterInvariant() function are not being fulfilled.

2. It would show the reason of failure in the console like:

   [FAIL: assertion failed: false != true]
   

   If you're not seeing such reason, then run forge clean before executing the test.

3. After doing forge clean and then executing test, in the beginning of the console, it would show the exact number of runs and depth that you've defined in your foundry.toml, along with the reason of failure (if it's failing), like:

   Compiler run successful!
   
   Ran 1 test for test/Invariant.t.sol:InvariantsTest
   [FAIL: assertion failed: false != true] invariant_test() (runs: 3, calls: 6, reverts: 0)
   

So, the reason behind the violation of assertEq is particularly the low number of depth, because for each run, it would do the depth number of function calls (summed up for all the functions), means if depth is 128, then there could be:

• 64 calls of setNumber() and 64 calls of increment().
• 60 calls of setNumber() and 68 calls of increment().
• 54 calls of setNumber() and 74 calls of increment().
• 75 calls of setNumber() and 53 calls of increment().

..., etc.

Means, the sum of total function calls in a single run would be equivalent to depth.

But, in your case, the depth is set too low, i.e., 3, so there are high chances of the conditions like:

• 0 calls of setNumber() and 3 calls of increment() -> resulting in the failure of assertEq(handler.isSetNumberTested(), true);

• 3 calls of setNumber() and 0 calls of increment() -> resulting in the failure of assertEq(handler.isIncrementTested(), true);

So, if you increase the value of depth, then everything would work fine.