Skip to main content

​
Use Case & Applications

Ensures the health factor of updated positions in lending protocols remains above a threshold, preventing unauthorized liquidations and protocol insolvency. Critical for lending protocols (Aave, Compound, Morpho), margin trading platforms, and any DeFi protocol using health factors for position management. Focuses on core lending operations (supply, borrow, withdraw, repay) while allowing other functions like liquidations to operate as designed.

​
Explanation

Monitors health factors of positions during specific lending operations using:
  • getCallInputs(): Track all function calls to specified protocol functions
  • registerCallTrigger(): Trigger on lending operations (supply, borrow, withdraw, repay)
  • forkPostState(): Verify health factor after each operation (used by default if no pre-state specified)
The assertion checks each lending operation individually to ensure positions affected by these operations remain healthy. For more information about cheatcodes, see the Cheatcodes Documentation.

​
Code Example

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.13;

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

contract LendingHealthFactorAssertion is Assertion {
    function triggers() external view override {
        // Register triggers for each function that should maintain healthy positions
        registerCallTrigger(this.assertionSupply.selector, IMorpho.supply.selector);
        registerCallTrigger(this.assertionBorrow.selector, IMorpho.borrow.selector);
        registerCallTrigger(this.assertionWithdraw.selector, IMorpho.withdraw.selector);
        registerCallTrigger(this.assertionRepay.selector, IMorpho.repay.selector);
    }

    // Check that supply operation maintains healthy positions
    function assertionSupply() external {
        // Get the assertion adopter address
        IMorpho adopter = IMorpho(ph.getAssertionAdopter());

        PhEvm.CallInputs[] memory callInputs = ph.getCallInputs(address(adopter), adopter.supply.selector);
        for (uint256 i = 0; i < callInputs.length; i++) {
            (uint256 marketId,) = abi.decode(callInputs[i].input, (uint256, uint256));
            address user = callInputs[i].caller;

            IMorpho.MarketParams memory marketParams = adopter.idToMarketParams(marketId);

            require(adopter._isHealthy(marketParams, marketId, user), "Supply operation resulted in unhealthy position");
        }
    }

    // Check that borrow operation maintains healthy positions
    function assertionBorrow() external {
        // Get the assertion adopter address
        IMorpho adopter = IMorpho(ph.getAssertionAdopter());

        PhEvm.CallInputs[] memory callInputs = ph.getCallInputs(address(adopter), adopter.borrow.selector);
        for (uint256 i = 0; i < callInputs.length; i++) {
            (uint256 marketId,) = abi.decode(callInputs[i].input, (uint256, uint256));
            address user = callInputs[i].caller;

            IMorpho.MarketParams memory marketParams = adopter.idToMarketParams(marketId);

            require(adopter._isHealthy(marketParams, marketId, user), "Borrow operation resulted in unhealthy position");
        }
    }

    // Check that withdraw operation maintains healthy positions
    function assertionWithdraw() external {
        // Get the assertion adopter address
        IMorpho adopter = IMorpho(ph.getAssertionAdopter());

        PhEvm.CallInputs[] memory callInputs = ph.getCallInputs(address(adopter), adopter.withdraw.selector);
        for (uint256 i = 0; i < callInputs.length; i++) {
            (uint256 marketId,) = abi.decode(callInputs[i].input, (uint256, uint256));
            address user = callInputs[i].caller;

            IMorpho.MarketParams memory marketParams = adopter.idToMarketParams(marketId);

            require(
                adopter._isHealthy(marketParams, marketId, user), "Withdraw operation resulted in unhealthy position"
            );
        }
    }

    // Check that repay operation maintains healthy positions
    function assertionRepay() external {
        // Get the assertion adopter address
        IMorpho adopter = IMorpho(ph.getAssertionAdopter());

        PhEvm.CallInputs[] memory callInputs = ph.getCallInputs(address(adopter), adopter.repay.selector);
        for (uint256 i = 0; i < callInputs.length; i++) {
            (uint256 marketId,) = abi.decode(callInputs[i].input, (uint256, uint256));
            address user = callInputs[i].caller;

            IMorpho.MarketParams memory marketParams = adopter.idToMarketParams(marketId);

            require(adopter._isHealthy(marketParams, marketId, user), "Repay operation resulted in unhealthy position");
        }
    }
}

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

    struct Position {
        uint256 supplyShares;
        uint128 borrowShares;
        uint128 collateral;
    }

    function idToMarketParams(uint256) external view returns (MarketParams memory);
    function position(uint256, address) external view returns (Position memory);
    function _isHealthy(MarketParams memory marketParams, uint256 marketId, address borrower)
        external
        view
        returns (bool);

    // Functions used in triggers
    function supply(uint256 marketId, uint256 amount) external;
    function borrow(uint256 marketId, uint256 amount) external;
    function withdraw(uint256 marketId, uint256 amount) external;
    function repay(uint256 marketId, uint256 amount) external;
}
Note: Full examples with tests available in the Phylax Assertion Examples Repository.
Extending Assertions: When new functions are added to the protocol that should maintain healthy positions, you can create a new assertion file (e.g., LendingHealthFactorExtendedAssertion.sol) that follows the same pattern. This allows you to:
  • Keep the original assertions active for existing functions
  • Add new assertions for new functions without modifying existing code
  • Maintain clear separation of concerns between different protocol features
⌘I