Lending Health Factor

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

import {Assertion} from "../lib/credible-std/Assertion.sol";

// We use Morpho as an example, but this could be any lending protocol
interface IMorpho {
    struct MarketParams {
        Id id;
    }
    struct Id {
        uint256 marketId;
    }

    function _isHealthy(MarketParams memory marketParams, Id memory id, address borrower) external view returns (bool);
}

contract LendingHealthFactorAssertion is Assertion {
    IMorpho public morpho = IMorpho(address(0xbeef));

    function fnSelectors() external pure override returns (Trigger[] memory) {
        Trigger[] memory triggers = new Trigger[](1); // Define the number of triggers
        triggers[0] = Trigger(TriggerType.STORAGE, this.assertionHealthFactor.selector); // Define the trigger
        return triggers;
    }

    // Check that the position is still healthy after the transaction
    // This check only works for the withdrawCollateral function from Morpho
    // Morpho correctly checks the health factor in the withdrawCollateral function,
    // but if we assume that the check was mistakenly not done, this assertion could
    // be used to check if the health factor is still healthy after the transaction
    // return true indicates a valid state
    // return false indicates an invalid state
    function assertionHealthFactor() external returns (bool) {
        ph.forkPostState();
        (, , , bytes memory data) = ph.getTransaction(); // TODO: Check if this works once we have the cheatcode
        bytes4 functionSelector = bytes4(data[:4]);
        if (functionSelector != morpho.withdrawCollateral.selector) {
            return true; // Skip the assertion if the function is not withdrawCollateral
        }

        // Skip the first 4 bytes (function selector) by passing the full calldata to decode
        (IMorpho.MarketParams memory marketParams, uint256 assets, address onBehalf, address receiver) = abi.decode(
            data[4:],
            (IMorpho.MarketParams, uint256, address, address)
        );

        return morpho._isHealthy(marketParams, marketParams.id, onBehalf);
    }
}