section 5: My invariant test doesn't catch the invariant break

[Jaunepr]

In the video ,Patrick catched the fee transfer break the invariant, but when I test it. why doesn't it catch the invariant break.
At first I thought it was because the number of runs was not enough, but when I increased the number to 10,000, it still didn’t work.
Has anyone encountered the same problem? please help me !!
Here is Handler.t.sol

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

import {Test, console} from "forge-std/Test.sol";
import {TSwapPool} from "../../src/TSwapPool.sol";
import {ERC20Mock} from "@openzeppelin/contracts/mocks/token/ERC20Mock.sol";

contract Handler is Test {
    TSwapPool pool;
    ERC20Mock mockWeth;
    ERC20Mock poolToken;

    int256 startingX;
    int256 startingY;

    int256 public expectDeltaX;
    int256 public expectDeltaY;

    int256 endingX;
    int256 endingY;

    int256 public actualDeltaX;
    int256 public actualDeltaY;

    address lp = makeAddr("liquidityProvider");
    address swapper = makeAddr("swapper");

    constructor(TSwapPool _pool) {
        pool = _pool;
        mockWeth = ERC20Mock(pool.getWeth());
        poolToken = ERC20Mock(pool.getPoolToken());
    }

    // we need pooltoken input and get weth output!
    // we want wethAmout output : deltaY pool.getInputAmountBasedOnOutput()
    // ∆x  = (x*outputAmount)/(y - outputAmount)
    function poolTokenSwapForWethBasedOnOutputAmount(
        uint256 wethAmountOutput
    ) public {
        // determine the wethamount not more than in pools
        wethAmountOutput = bound(
            wethAmountOutput,
            pool.getMinimumWethDepositAmount(),
            type(uint64).max
        );

        if (wethAmountOutput >= mockWeth.balanceOf(address(pool))) {
            return;
        }

        // determine how many pooltoken amount we needed
        //getInputAmountBasedOnOutput(outputAmount, inputReserves, outputReserves)
        uint256 poolTokenAmount = pool.getInputAmountBasedOnOutput(
            wethAmountOutput,
            poolToken.balanceOf(address(pool)),
            mockWeth.balanceOf(address(pool))
        ); 
        if (poolTokenAmount >= type(uint64).max) {
            return;
        }

        startingY = int256(mockWeth.balanceOf(address(pool)));
        startingX = int256(poolToken.balanceOf(address(pool)));

        expectDeltaY = int256(-1) * int256(wethAmountOutput);
        expectDeltaX = int256(poolTokenAmount);

        // then we need a swapper to swap!
        // swapper must have enough balance！
        if (poolToken.balanceOf(swapper) < uint256(expectDeltaX)) {
            poolToken.mint(
                swapper,
                uint256(expectDeltaX) - poolToken.balanceOf(swapper) + 1
            );
        }
        // Start Swap
        vm.startPrank(swapper);
        poolToken.approve(address(pool), type(uint256).max);
        pool.swapExactOutput(
            poolToken,
            mockWeth,
            wethAmountOutput,
            uint64(block.timestamp)
        );
        vm.stopPrank();

        // check 2 assets in pool
        endingX = int256(poolToken.balanceOf(address(pool)));
        endingY = int256(mockWeth.balanceOf(address(pool)));

        actualDeltaX = endingX - startingX;
        actualDeltaY = endingY - startingY;

    }

    //q Handler should do what functions to do?
    // deposit, swap, withdraw,

    function deposit(uint256 wethAmount) public {
        wethAmount = bound(
            wethAmount,
            pool.getMinimumWethDepositAmount(),
            type(uint64).max
        );

        startingX = int256(poolToken.balanceOf(address(pool)));
        startingY = int256(mockWeth.balanceOf(address(pool)));

        expectDeltaX = int256(
            pool.getPoolTokensToDepositBasedOnWeth(wethAmount)
        );
        expectDeltaY = int256(wethAmount);

        // Prank a liquidityProvider to mint
        vm.startPrank(lp);
        mockWeth.mint(lp, wethAmount);
        poolToken.mint(lp, uint256(expectDeltaX));

        mockWeth.approve(address(pool), type(uint256).max);
        poolToken.approve(address(pool), type(uint256).max);

        pool.deposit(
            wethAmount,
            pool.getMinimumWethDepositAmount(),
            uint256(expectDeltaX),
            uint64(block.timestamp)
        );
        vm.stopPrank();

        // check the actual deltaX & deltaY
        endingX = int256(poolToken.balanceOf(address(pool)));
        endingY = int256(mockWeth.balanceOf(address(pool)));

        actualDeltaX = endingX - startingX;
        actualDeltaY = endingY - startingY;
    }
}

Here is my invariant.t.sol

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

import {Test} from "forge-std/Test.sol";
import {StdInvariant} from "forge-std/StdInvariant.sol";
import {ERC20Mock} from "@openzeppelin/contracts/mocks/token/ERC20Mock.sol";
import {PoolFactory} from "../../src/PoolFactory.sol";
import {TSwapPool} from "../../src/TSwapPool.sol";
import {Handler} from "./Handler.t.sol";

contract Invariant_test is StdInvariant, Test {
    // one pool has two asset
    ERC20Mock mockWeth;
    ERC20Mock poolToken;
    // needed contract
    PoolFactory poolFactory;
    TSwapPool tswapPool; // pooltoken / mockWeth

    Handler handler;

    int256 public constant STARTING_X = 100 ether;
    int256 public constant STARTING_Y = 50 ether;

    function setUp() public {
        mockWeth = new ERC20Mock();
        poolToken = new ERC20Mock();
        poolFactory = new PoolFactory(address(mockWeth));
        tswapPool = TSwapPool(poolFactory.createPool(address(poolToken)));

        // now needs some x & y balance
        mockWeth.mint(address(this), uint256(STARTING_Y));
        poolToken.mint(address(this), uint256(STARTING_X));

        mockWeth.approve(address(tswapPool), type(uint256).max);
        poolToken.approve(address(tswapPool), type(uint256).max);

        // now needes deposit into pool
        tswapPool.deposit(
            uint256(STARTING_Y),
            uint256(STARTING_Y),
            uint256(STARTING_X),
            uint64(block.timestamp)
        );

        handler = new Handler(tswapPool);
        bytes4[] memory selectors = new bytes4[](2);
        selectors[0] = Handler.deposit.selector;
        selectors[1] = Handler.poolTokenSwapForWethBasedOnOutputAmount.selector;
        targetSelector(
            FuzzSelector({addr: address(handler), selectors: selectors})
        );
        targetContract(address(handler));
    }

    function statefulFuzz_constantProductFormulaStayTheSameX() public view {
        assertEq(handler.expectDeltaX(), handler.actualDeltaX());
    }

    function statefulFuzz_constantProductFormulaStayTheSameY() public view {
        assertEq(handler.expectDeltaY(), handler.actualDeltaY());
    }
}

The foundry.toml is

[fuzz]
seed = "0x1"

[invariant]
runs = 256
depth = 32
fail_on_revert = true

And the message I got always be

Ran 1 test for test/invariantBreak/Invariant.t.sol:Invariant_test
[PASS] statefulFuzz_constantProductFormulaStayTheSameX() (runs: 256, calls: 8192, reverts: 0)
Suite result: ok. 1 passed; 0 failed; 0 skipped; finished in 780.10ms (778.56ms CPU time)

Ran 1 test suite in 781.35ms (780.10ms CPU time): 1 tests passed, 0 failed, 0 skipped (1 total tests)

[vascofcd]

Isn't Patrick catching the invariant break while running statefulFuzz_constantProductFormulaStayTheSameY? I can't quite recall, but I believe statefulFuzz_constantProductFormulaStayTheSameX does not catch it.

[Jaunepr]

sry, I test them all ,and the statefulFuzz_constantProductFormulaStayTheSameY get the same result.

jaunepr@Crocea-Mors:5-t-swap-audit$ forge test --mt statefulFuzz_constantProductFormulaStayTheSameY 
[⠊] Compiling...
No files changed, compilation skipped

Ran 1 test for test/invariantBreak/Invariant.t.sol:Invariant_test
[PASS] statefulFuzz_constantProductFormulaStayTheSameY() (runs: 256, calls: 8192, reverts: 0)
Suite result: ok. 1 passed; 0 failed; 0 skipped; finished in 772.05ms (765.30ms CPU time)

Ran 1 test suite in 779.64ms (772.05ms CPU time): 1 tests passed, 0 failed, 0 skipped (1 total tests)

[EngrPips]

Hello @Jaunepr, test for statefulFuzz_constantProductFormulaStayTheSameY like @vascofcd suggested, and let's see if you catch it.

[Jaunepr]

It still didn't catch the invariant break

[EngrPips]

weird. Please run your test with the -vvvv flag and check how often your fuzzer called poolTokenSwapForWethBasedOnOutputAmount on the handler contract. Is it up to 10 times?

[Jaunepr]

Yes，it called more than 10 times. here is the output
output.txt

[EngrPips]

Yes，it called more than 10 times. here is the output output.txt

Most of the calls to poolTokenSwapForWethBasedOnOutputAmount on the handler didn't actually execute but instead, they were returning. Consider checking what @Chinwuba22 pointed out.

[Jaunepr]

Oh,I see, the depth is not enough to call the poolTokenSwapForWethBasedOnOutputAmount executed up to 10 times, so it passed.

[EngrPips]

Awesome, That was a little bit tough to catch lol.

[Chinwuba22]

He did use wethAmountOutput = bound(wethAmountOutput, pool.getMinimumWethDepositAmount(), wethToken.balanceOf(address(pool))); in Handler:: poolTokenSwapForWethBasedOnOutputAmount, as type(uint64).max was resulting into an issue...

[Chinwuba22]

Not sure if this is the issues with yours Just pointing it out

[Jaunepr]

thanks, but I didn't trigger the exception when I used type(uint64).max

[0xharrywang]

Here’s what I’ve noticed.

Possible Reason:

The upper bound for the invariant test is set too high. Initially, the pool contains 50e18 WETH. If the random number ends up being really close to that value, it essentially empties the WETH from the pool. According to the AMM mechanism, the price of WETH increases significantly (which means more pool tokens are required). As a result, when the test runs again, the poolTokenAmount becomes much larger, triggering the following logic in Handler.t.sol::poolTokenSwapForWethBasedOnOutputAmount:

    if (poolTokenAmount > type(uint64).max) {
        return;
    }

This causes the test to exit early, and swapExactOutput doesn’t get executed. That’s why, under the default [invariant] settings in foundry.toml, the swap doesn’t actually run 10 times.

Solution:

The simplest solution is to set a smaller bound on Handler.t.sol, like in the following code, or adjust the fuzz testing configuration:

    wethAmountOutput = bound(wethAmountOutput, pool.getMinimumWethDepositAmount(), 1e18);

[EngrPips]

Interesting heads-up.