Why Are Explicit Health Factor Checks Needed in Fuzz Handlers While Parick's Code Runs Without Them?

[mosesmrima]

I am implementing a fuzz handler for the redeemCollateral function in my project to test its behavior under various scenarios. To avoid unnecessary reverts, I added explicit checks in the handler to ensure the health factor remains above 1. Without these checks, my fuzz tests frequently cause the health factor to drop below the threshold, leading to reverts.

However, in Patrick's code, there are no explicit checks in the fuzz handler, and yet his runs do not seem to violate the health factor. The redeemCollateral function implementations in both my handler and Patrick's code are effectively the same.

Here’s my fuzz handler implementation:

function redeemCollateral(uint256 _collateralSeed, uint256 _amount) public {
    ERC20Mock collateral = _getCollateralFromSeed(_collateralSeed);

    uint256 maxCollateralToRedeem = engine.getCollateralBalanceOfUser(msg.sender, address(collateral));
    uint256 mintedDsc = engine.getMintedDsc();
    uint256 collateralDeposited = engine.getCollateralBalanceOfUser(msg.sender, address(collateral));

    if (_amount > collateralDeposited) {
        return;
    }
    _amount = bound(_amount, 0, maxCollateralToRedeem);

    uint256 collateralAfterRedeem = collateralDeposited - _amount;
    uint256 healthFactor = engine.calculateHealthFactor(mintedDsc, collateralAfterRedeem);

    // Explicit check I have to add
    if (healthFactor < 1e18) {
        return;
    }

    if (_amount == 0) {
        return;
    }

    vm.startPrank(msg.sender);
    engine.redeemCollateral(address(collateral), _amount);
    vm.stopPrank();
    timesRedeemCollateralCalled++;
}

Here’s the redeemCollateral implementation in my DSCEngine contract:

function redeemCollateral(address _token, uint256 _amount) public moreThanZero(_amount) {
    _redeemCollateral(_token, _amount, msg.sender, msg.sender);
    _revertIfHealthFactorIsBroken(msg.sender);
}

function _redeemCollateral(address _token, uint256 _amount, address _from, address _to) private {
    s_collateralDeposited[_from][_token] -= _amount;
    emit CollateralRedemed(_from, _to, _token, _amount);

    bool success = IERC20(_token).transfer(_to, _amount);
    if (!success) {
        revert DSCEngine__TransferFailed();
    }
}

function _healthFactor(address user) internal view returns (uint256) {
    (uint256 totalDscMinted, uint256 collateralValueInUsd) = _getAccountInfo(user);

    if (totalDscMinted == 0) {
        return type(uint256).max; // Handles no debt case
    }
    uint256 collateralAdjustedForThreshold =
        (collateralValueInUsd * LIQUIDATATION_THRESHOLD) / LIQUIDATATION_PRECISION;

    return (collateralAdjustedForThreshold * PRECISION) / totalDscMinted;
}

function _revertIfHealthFactorIsBroken(address _user) internal view {
    uint256 userHealthFactor = _healthFactor(_user);
    if (userHealthFactor < MIN_HEALTH_FACTOR) {
        revert DSCEngine__BreaksHealthFactor(userHealthFactor);
    }
}

Here’s Patrick’s fuzz handler:

function redeemCollateral(uint256 collateralSeed, uint256 amountCollateral) public {
    ERC20Mock collateral = _getCollateralFromSeed(collateralSeed);
    uint256 maxCollateral = dscEngine.getCollateralBalanceOfUser(msg.sender, address(collateral));

    amountCollateral = bound(amountCollateral, 0, maxCollateral);
    if (amountCollateral == 0) {
        return;
    }
    vm.prank(msg.sender);
    dscEngine.redeemCollateral(address(collateral), amountCollateral);
}

Observations:

1. My fuzz handler includes explicit health factor checks to avoid reverts, but Patrick's code does not.
2. Patrick's runs pass without health factor violations, even without the explicit checks.
3. The redeemCollateral implementation in both my handler and DSCEngine is the same as in Patrick's code.

[EngrPips]

Hello @mosesmrima, Programming is tough, and sometimes you need to make it work for you. I have the same redeemCollateral in my Handler contract as Patrick, and I didn't run into an issue when I ran my Invariant test. This could be happening probably because of the difference in the variables that control our invariant testing process, such as the seed and the no_of_runs, but regardless if you have to make one or more adjustments to make it work as you expect, then that is totally fine.

[mosesmrima]

Thank you!

[EngrPips]

You are welcome, Friend. Keep crushing it.