statefulFuzz_constantProductFormulaStaysTheSame X & Y pass

[z0Ld3v]

I've followed along from lessons 21 - 26 in the TSwap course twice and both invariant tests are passing. I don't understand how is that possible. The Handler code in the repo is not remotely close to what's shown in the tutorial. How can I get one of the tests to fail?

Here's my Handler contract

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

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

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

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

    // Ghost variables
    int256 startingX;
    int256 startingY;
    int256 public expectedDeltaX; // Represents the expected change in poolToken balance
    int256 public expectedDeltaY; // Represents the expected change in weth balance
    int256 public actualDeltaX; // Represents the actual change in poolToken balance
    int256 public actualDeltaY; // Represents the actual change in weth balance

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

    function swapPoolTokenForWethBasedOnOutputWeth(uint256 outputWeth) public {
        outputWeth = bound(
            outputWeth,
            pool.getMinimumWethDepositAmount(),
            weth.balanceOf(address(pool))
        );
        // To prevent from swapping all the money in the pool, we need to set a condition
        if (outputWeth >= weth.balanceOf(address(pool))) {
            return;
        }
        // The expected ∆x = (β/(1-β)) * x
        uint256 poolTokenAmount = pool.getInputAmountBasedOnOutput(
            outputWeth,
            poolToken.balanceOf(address(pool)), // inputReserves
            weth.balanceOf(address(pool)) // outputReserves
        );
        // Check if the pool token amount is reasonable
        if (poolTokenAmount > type(uint64).max) {
            return;
        }
        startingX = int256(poolToken.balanceOf(address(pool)));
        startingY = int256(weth.balanceOf(address(pool)));
        expectedDeltaX = int256(poolTokenAmount);
        expectedDeltaY = int256(-1) * int256(outputWeth);

        if (poolToken.balanceOf(swapper) < poolTokenAmount) {
            poolToken.mint(
                swapper,
                poolTokenAmount - poolToken.balanceOf(swapper) + 1
            );
        }

        // Swap
        vm.startPrank(swapper);
        poolToken.approve(address(pool), type(uint256).max);
        pool.swapExactOutput(
            poolToken,
            weth,
            outputWeth,
            uint64(block.timestamp)
        );
        vm.stopPrank();

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

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

    // deposit, swapExactOutput
    function deposit(uint256 wethAmount) public {
        // Needs to be a reasonable amount, to avoid overflow issues
        uint256 minWeth = pool.getMinimumWethDepositAmount();
        wethAmount = bound(wethAmount, minWeth, type(uint64).max);
        startingX = int256(poolToken.balanceOf(address(pool)));
        startingY = int256(weth.balanceOf(address(pool)));
        expectedDeltaX = int256(
            pool.getPoolTokensToDepositBasedOnWeth(wethAmount)
        );
        expectedDeltaY = int256(wethAmount);

        // Deposit
        vm.startPrank(liqidityProvider);
        weth.mint(liqidityProvider, wethAmount);
        poolToken.mint(liqidityProvider, 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();
        // Actual
        uint256 endingX = poolToken.balanceOf(address(pool));
        uint256 endingY = weth.balanceOf(address(pool));

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

Here's my Invariant contract

//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 { PoolFactory } from "../../src/PoolFactory.sol";
import { TSwapPool } from "../../src/TSwapPool.sol";
import { Handler } from "./Handler.t.sol";

contract Invariant is StdInvariant, Test {
    // These pools have 2 assets
    ERC20Mock poolToken;
    ERC20Mock weth;

    // We need the contracts
    PoolFactory factory;
    TSwapPool pool; // poolToken / weth
    Handler handler;

    int256 constant STARTING_X = 100e18; // Starting poolToken balance
    int256 constant STARTING_Y = 50e18; // Starting weth balance

    function setUp() public {
        weth = new ERC20Mock();
        poolToken = new ERC20Mock();
        factory = new PoolFactory(address(weth));
        pool = TSwapPool(factory.createPool(address(poolToken)));

        // Create the pools with the initial balances of x & y
        poolToken.mint(address(this), uint256(STARTING_X));
        weth.mint(address(this), uint256(STARTING_Y));

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

        // Deposit x & y into the pool, create starting ratio
        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 view {
        // We need to assert the change in pool size of WETH should follow this formula:
        // ∆x = (β/(1-β)) * x
        // In a handler, we can create a variable for the actual change in x
        // compare it to the expected change in x and assert that they are equal
        // actualDeltaX == ∆x = (β/(1-β)) * x
        assertEq(handler.actualDeltaX(), handler.expectedDeltaX());
    }

    function statefulFuzz_constantProductFormulaStaysTheSameY() public view {
        // We need to assert the change in pool size of WETH should follow this formula:
        // ∆x = (β/(1-β)) * x
        // In a handler, we can create a variable for the actual change in x
        // compare it to the expected change in x and assert that they are equal
        // actualDeltaX == ∆x = (β/(1-β)) * x
        assertEq(handler.actualDeltaY(), handler.expectedDeltaY());
    }
}

Please let me know where am I going wrong at

[EngrPips]

Hello, @z0Ldev. Which of the tests is supposed to fail?

[EngrPips]

Why is it that the test for X has to pass and the test for Y has to fail?

[z0Ld3v]

According to the tutorial, the invariant is supposed to break when testing Y. But it's not, they're both passing, it doesn't really matter which one breaks. I just need to know if I'm doing something wrong, or is the tutorial omitting steps?

[EngrPips]

I will watch the tutorial again and see what you are saying. I can't remember every detail of the tutorial.

[z0Ld3v]

Thank you, please let me know what you find.

[EngrPips]

Yeah, sure, Friend. I will be back soon.

[Chinwuba22]

Also, do well do configure your toml well. Like the Invariant section. Goodluck.

[SyedAsadKazmi]

Alright, sir, I will look into it as soon as I can and get in touch here to inform you of my observation.

@EngrPips, Did you get a chance to look at it yet?

[EngrPips]

I know I promised to check and circle back, but my hands are tied to a lot of stuff. If you have some time, I will say you should check the swap functions in the TWAP codebase and see what their implementation is. I will surely circle back here any time I get the chance to check

[EngrPips]

I know I promised to check and circle back, but my hands are tied to a lot of stuff. If you have some time, I will say you should check the swap functions in the TWAP codebase and see what their implementation is. I will surely circle back here any time I get the chance to check

@SyedAsadKazmi did you check what I suggested already and did you find anything interesting?

[SyedAsadKazmi]

@EngrPips, aren't we supposed to compare the product of X & Y instead of checking them individually? 🤔

That means the invariant test should be:

function statefulFuzz_constantProductFormulaStaysTheSame() public {
    int256 actualK = handler.actualDeltaX() * handler.actualDeltaY();
    int256 expectedK = handler.expectedDeltaX() * handler.expectedDeltaY();
    assertEq(actualK, expectedK);
}

This test is actually verifying the invariant K, and it's failing (as expected) because Y is changing.

[EngrPips]

@SyedAsadKazmi, Yeah, you are correct, as we would compare k with your approach, which is what makes more sense for us to check, but Patrick chose to check the affected token, which isn't entirely wrong.

I think it is supposed to make sense to you now why Patrick's check was failing for only one side. essentially that is how it is supposed to be. If you are still unable to make sense of why Patrick's check only fails for one side let me know and I will try to explain it.

[0xharrywang]

Hello, I’ve noticed something.

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:

    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:

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

[EngrPips]

Interesting heads-up.

[SyedAsadKazmi]

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

@0xharrywang, thanks a lot for the response!

After changing this line in the swapPoolTokenForWethBasedOnOutputWeth function of the Handler.t.sol, the invariant still breaks only for a one-sided swap, but not for both-sided swaps, means it's failing for statefulFuzz_constantProductFormulaStaysTheSameY, but not for statefulFuzz_constantProductFormulaStaysTheSameX as shown in the screenshot I shared in the thread above.

function swapPoolTokenForWethBasedOnOutputWeth(uint256 outputWeth) public {
-        outputWeth = bound(outputWeth, pool.getMinimumWethDepositAmount(), weth.balanceOf(address(pool)));
+        outputWeth = bound(outputWeth, pool.getMinimumWethDepositAmount(), 1e18);

[0xharrywang]

@SyedAsadKazmi Yes, that may be correct, sir. As shown in the tutorial, the invariant only breaks on statefulFuzz_constantProductFormulaStaysTheSameY.

[EngrPips]

Interesting.

[s3bc40]

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

@0xharrywang, thanks a lot for the response!

After changing this line in the swapPoolTokenForWethBasedOnOutputWeth function of the Handler.t.sol, the invariant still breaks only for a one-sided swap, but not for both-sided swaps, means it's failing for statefulFuzz_constantProductFormulaStaysTheSameY, but not for statefulFuzz_constantProductFormulaStaysTheSameX as shown in the screenshot I shared in the thread above.

function swapPoolTokenForWethBasedOnOutputWeth(uint256 outputWeth) public {
-        outputWeth = bound(outputWeth, pool.getMinimumWethDepositAmount(), weth.balanceOf(address(pool)));
+        outputWeth = bound(outputWeth, pool.getMinimumWethDepositAmount(), 1e18);

I confirm that now I get the result of the course. Great finding frens!