Statefull Fuzz Passed Instead Of failed.

[lintianyuan666]

I wrote the invariant test suite of TSwap according to the course, but when testing the assert of weth, the course showed failed, but my test passed. I thought my code was wrong, but when I copied the test suite of TSwap from github and ran it locally, it still returned pass.

Here is my code below.
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 "../mocks/ERC20Mock.sol";
import {TSwapPool} from "../../src/TSwapPool.sol";
import {PoolFactory} from "../../src/PoolFactory.sol";
import {Handler} from "./Handler.t.sol";

contract Invariant is StdInvariant,Test {
    ERC20Mock poolToken;
    ERC20Mock weth;
    //初始的x和y值
    int256 constant STARTING_X=100e18;//poolToken
    int256 constant STARTING_Y=50e18;//weth

    PoolFactory factory;
    TSwapPool pool; //这个池子对应poolToken和weth
    Handler handler;

    function setUp() public {
        weth = new ERC20Mock();
        poolToken = new ERC20Mock();
        factory = new PoolFactory(address(weth));
        pool = TSwapPool(factory.createPool(address(poolToken)));//用PoolFactory创建一个池子，前面的TSswapPool是为了把原来的地址转换成TSwapPool类型的地址

        poolToken.mint(address(this), uint256(STARTING_X));//铸币到当前地址
        weth.mint(address(this),uint256(STARTING_Y));

        poolToken.approve(address(pool),type(uint256).max);//允许pool合约调用当前地址的poolToken
        weth.approve(address(pool),type(uint256).max);

        pool.deposit(uint256(STARTING_Y), uint256(STARTING_Y), uint256(STARTING_X), uint64(block.timestamp));
 
        handler = new Handler(pool);
        bytes4[] memory selectors = new bytes4[](2);
        selectors[0] = Handler.deposit.selector;
        selectors[1] = Handler.swapPoolTokenForWethBasedOnOutputWeth.selector;
        targetSelector(FuzzSelector({addr:address(handler),selectors:selectors}));
        targetContract(address(handler));
    }

    function statefulFuzz_constantProductFormulaStaysTheSameX() public {
        assertEq(handler.actualDeltaX(),handler.expectedDeltaX());
    }

    function statefulFuzz_constantProductFormulaStaysTheSameY() public {
        assertEq(handler.actualDeltaY(),handler.expectedDeltaY());
    }
}

And Handler.t.sol

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

import {Test,console2} from "forge-std/Test.sol";
// import {StdInvariant} from "forge-std/StdInvariant.sol";
import {ERC20Mock} from "../mocks/ERC20Mock.sol";
import {TSwapPool} from "../../src/TSwapPool.sol";
// import {PoolFactory} from "../../src/PoolFactory.sol";

contract Handler is Test {
    TSwapPool pool;
    ERC20Mock weth;
    ERC20Mock poolToken;
    address liquidityProvider = makeAddr("lp");
    address swapper=makeAddr("swapper");

    int256 startingY;
    int256 startingX; 
    int256 public expectedDeltaY;
    int256 public expectedDeltaX;
    int256 public actualDeltaX;
    int256 public actualDeltaY;

    constructor(TSwapPool _pool) {
        pool = _pool;
        weth = ERC20Mock(_pool.getWeth());//给weth赋值为传入的池子的weth的地址
        poolToken = ERC20Mock(_pool.getPoolToken());
    }

    function swapPoolTokenForWethBasedOnOutputWeth(uint256 outputWeth) public {
        outputWeth = bound(outputWeth, pool.getMinimumWethDepositAmount(), weth.balanceOf(address(pool)));
        if(outputWeth > weth.balanceOf(address(this))){
            return;
        }

        uint256 poolTokenAmount = pool.getInputAmountBasedOnOutput(outputWeth,poolToken.balanceOf(address(this)),weth.balanceOf(address(this)));//这就是我们要的三角形x的值，因为取出来的y是固定的
        if(poolTokenAmount > type(uint64).max){
            return;
        }

        startingX=int256(poolToken.balanceOf(address(pool)));
        startingY=int256(weth.balanceOf(address(pool)));
        expectedDeltaY = int256(-1)*int256(outputWeth);//预期取出的weth
        expectedDeltaX = int256(poolTokenAmount);

        if(poolToken.balanceOf(swapper) < poolTokenAmount){
            poolToken.mint(swapper, poolTokenAmount-poolToken.balanceOf(swapper)+1);//确保每次转完钱以后都能有剩的
        }

        vm.startPrank(swapper);//开始模拟一个地址的取钱操作
        poolToken.approve(address(pool), type(uint256).max);
        pool.swapExactOutput(poolToken, weth, outputWeth, uint64(block.timestamp));
        vm.stopPrank();

        uint256 endingX = poolToken.balanceOf(address(pool));
        uint256 endingY = weth.balanceOf(address(pool));

        actualDeltaY = int256(endingY) - int256(startingY);
        actualDeltaX = int256(endingX) - int256(startingX);
    }

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

        startingX=int256(poolToken.balanceOf(address(pool)));
        startingY=int256(weth.balanceOf(address(pool)));
        expectedDeltaY = int256(wethAmount);//预期充入的weth
        expectedDeltaX = int256(pool.getPoolTokensToDepositBasedOnWeth(wethAmount));//计算存入这多weth对应多少pooltoken

        vm.startPrank(liquidityProvider);//开始模拟一个地址的存钱操作
        weth.mint(liquidityProvider, wethAmount);
        poolToken.mint(liquidityProvider, uint256(expectedDeltaX));
        weth.approve(address(pool), type(uint256).max);
        poolToken.approve(address(pool), type(uint256).max);
        pool.deposit(wethAmount, 0, uint256(expectedDeltaX), uint64(block.timestamp));
        vm.stopPrank();

        uint256 endingX = poolToken.balanceOf(address(pool));
        uint256 endingY = weth.balanceOf(address(pool));

        actualDeltaY = int256(endingY) - int256(startingY);
        actualDeltaX = int256(endingX) - int256(startingX);


    }
}

Here are the results of my forge test:

Suite result: ok. 1 passed; 0 failed; 0 skipped; finished in 225.17s (225.17s CPU time)

[EngrPips]

I think you need to do 10 swaps in a swap direction for the protocol invariant to break. Check your test process stack trace to see if the process did up to 10 swaps in a swap direction.

[lintianyuan666]

I found the cause of the problem. Depth=32 is too small. Therefore, although swap is called more than 10 times, many of them are reverted due to the incoming parameters, so the effective calls are less than 10 times.

[EngrPips]

I found the cause of the problem. Depth=32 is too small. Therefore, although swap is called more than 10 times, many of them are reverted due to the incoming parameters, so the effective calls are less than 10 times.

Awesome, I am glad you figured it out. Do you get it to work now?

[lintianyuan666]

Yes.It works.Thank you bro.

[EngrPips]

Yes.It works.Thank you bro.

I am glad it works now, keep crushing it, bro!

[Preciousbas]

Yes.It works.Thank you bro.

I am glad it works now, keep crushing it, bro!

Thanks for this. I ran into the same issue and increased my depth to 256 and it worked

[AwnishSingh]

In your Handler.t.sol try replacing

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

with

if (poolTokenAmount > poolToken.balanceOf(address(pool))) { return; }

[lintianyuan666]

I tried it but no use.