​
Use Case

Check that the health factor of updated positions in a lending protocol is above a certain threshold. The health factor is a critical security parameter that determines whether a position is at risk of liquidation. An unhealthy position could lead to:

  • Unauthorized liquidations of user positions
  • Protocol insolvency if positions become undercollateralized
  • Cascading liquidations that could destabilize the entire protocol
  • Loss of user funds through forced liquidations at unfavorable prices

This assertion is particularly important for:

  • Preventing positions from becoming undercollateralized
  • Ensuring protocol solvency is maintained
  • Detecting potential manipulation of health factor calculations
  • Maintaining protocol security by enforcing health factor invariants

​
Expected vs Unexpected Health Factor Violations

It’s important to distinguish between expected and unexpected health factor violations:

Expected Violations:

  • Market price movements causing positions to become undercollateralized
  • Protocol-initiated liquidations as part of normal risk management
  • Scheduled parameter updates that may temporarily affect health factors
  • Protocol upgrades that include health factor adjustments

Unexpected Violations:

  • Bugs in health factor calculations
  • Unauthorized modifications to position parameters
  • Exploits that manipulate collateral or debt values
  • Missing health factor checks in new protocol functions

The assertion focuses on ensuring that core lending operations (supply, borrow, withdraw, repay) maintain healthy positions, while allowing other protocol functions (like liquidations) to operate as designed.

​
Applicable Protocols

  • Lending protocols (e.g., Aave, Compound, Morpho) that need to enforce strict health factor requirements
  • Margin trading protocols that rely on health factors for position management
  • Cross-collateral lending systems where health factors are critical for risk management
  • Protocols using health factors as a key risk parameter for position management

​
Explanation

The assertion monitors the health factors of positions in lending protocols during specific lending operations. The health factor is calculated as the ratio of the total value of collateral to the total value of debt, and it determines whether a position is at risk of liquidation.

The assertion uses the following cheatcodes:

  • getCallInputs(): Retrieves information about all function calls to the specified protocol functions
  • registerCallTrigger(): Triggers the assertion when specific lending operations are called
  • If no forkPreState() or forkPostState() is provided, the assertion will use the forkPostState() cheatcode by default

This approach ensures that:

  1. Each lending operation (supply, borrow, withdraw, repay) is monitored individually
  2. The assertion directly checks the health factor after each operation
  3. Positions affected by these operations remain healthy
  4. All protocol users’ positions are verified after relevant operations

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";

// 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;
}

contract LendingHealthFactorAssertion is Assertion {
    IMorpho public morpho;

    constructor(address _morpho) {
        morpho = IMorpho(_morpho);
    }

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

    // Check that supply operation maintains healthy positions
    function assertionSupply() external {
        PhEvm.CallInputs[] memory callInputs = ph.getCallInputs(address(morpho), morpho.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 = morpho.idToMarketParams(marketId);

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

    // Check that borrow operation maintains healthy positions
    function assertionBorrow() external {
        PhEvm.CallInputs[] memory callInputs = ph.getCallInputs(address(morpho), morpho.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 = morpho.idToMarketParams(marketId);

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

    // Check that withdraw operation maintains healthy positions
    function assertionWithdraw() external {
        PhEvm.CallInputs[] memory callInputs = ph.getCallInputs(address(morpho), morpho.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 = morpho.idToMarketParams(marketId);

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

    // Check that repay operation maintains healthy positions
    function assertionRepay() external {
        PhEvm.CallInputs[] memory callInputs = ph.getCallInputs(address(morpho), morpho.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 = morpho.idToMarketParams(marketId);

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

Note: This code example is maintained in the Phylax Assertion Examples Repository where you can also find test examples.

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

​
Testing

To test this assertion:

  1. Deploy a test instance of the lending protocol
  2. Create positions with varying health factors
  3. Test operations that should maintain healthy positions:
    • Supply collateral
    • Borrow assets
    • Withdraw collateral
    • Repay borrowed assets
  4. Verify the assertion ensures positions remain healthy after these operations
  5. Test edge cases:
    • Multiple positions affected by a single transaction
    • Positions near the health factor threshold
    • Concurrent operations on the same position

For test examples, see the Phylax Assertion Examples Repository.

​
Assertion Best Practices

  • Combine this assertion with other lending-related assertions like ERC20 Drain for comprehensive security
  • Use appropriate health factor thresholds based on protocol risk parameters
  • Consider the impact of market conditions on position health when designing the assertion