> ## Documentation Index
> Fetch the complete documentation index at: https://docs.phylax.systems/llms.txt
> Use this file to discover all available pages before exploring further.

# Lending Health Factor

> Assert that the health factor of updated positions in a lending protocol is above a certain threshold

## When to Use This Pattern

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.

## What This Pattern Checks

Monitors health factors of positions during specific lending operations using:

* `getCallInputs()`: Track all function calls to specified protocol functions
* `registerFnCallTrigger()`: Trigger on lending operations (supply, borrow, withdraw, repay)
* `_postTx()`: 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](/credible/cheatcodes-reference).

## Assertion Pattern

```solidity theme={null}
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.13;

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

contract LendingHealthFactorAssertion is Assertion {
    bytes32 internal constant HEALTH_FACTOR_SLOT = bytes32(uint256(0));
    uint256 internal constant MIN_HEALTH_FACTOR = 1e18;

    constructor() {
        registerAssertionSpec(AssertionSpec.Reshiram);
    }

    function triggers() external view override {
        registerFnCallTrigger(this.assertionOperationSafety.selector, IMorpho.supply.selector);
        registerFnCallTrigger(this.assertionOperationSafety.selector, IMorpho.borrow.selector);
        registerFnCallTrigger(this.assertionOperationSafety.selector, IMorpho.withdraw.selector);
        registerFnCallTrigger(this.assertionOperationSafety.selector, IMorpho.repay.selector);
    }

    /// @notice Checks that the touched account remains healthy after a lending operation.
    function assertionOperationSafety() external view {
        PhEvm.TriggerContext memory ctx = ph.context();
        PhEvm.ForkId memory postCall = PhEvm.ForkId({forkType: 3, callIndex: ctx.callEnd});
        (uint256 marketId,) = abi.decode(_stripSelector(ph.callinputAt(ctx.callStart)), (uint256, uint256));
        address account = _matchingCaller(ctx.selector);
        bytes32 healthSlot = _healthFactorSlot(marketId, account);
        uint256 healthFactor = uint256(ph.loadStateAt(ph.getAssertionAdopter(), healthSlot, postCall));

        require(healthFactor >= MIN_HEALTH_FACTOR, "Operation resulted in unhealthy position");
    }

    function _matchingCaller(bytes4 selector) internal view returns (address) {
        PhEvm.TriggerCall[] memory calls = ph.matchingCalls(ph.getAssertionAdopter(), selector, _successfulCalls(), 1);
        require(calls.length == 1, "missing triggered call");
        return calls[0].caller;
    }

    function _successfulCalls() internal pure returns (PhEvm.CallFilter memory filter) {
        filter.callType = 1;
        filter.successOnly = true;
    }

    function _healthFactorSlot(uint256 marketId, address account) internal pure returns (bytes32) {
        return keccak256(abi.encode(account, keccak256(abi.encode(marketId, HEALTH_FACTOR_SLOT))));
    }

    function _stripSelector(bytes memory data) internal pure returns (bytes memory) {
        bytes memory stripped = new bytes(data.length - 4);
        for (uint256 i = 4; i < data.length; i++) {
            stripped[i - 4] = data[i];
        }
        return stripped;
    }
}

interface IMorpho {
    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 and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book).</Note>

<Info>
  **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
</Info>

## Related Patterns

* [Full Aave Assertion Suite](/assertions-book/assertions/aave-v3-suite)
* [ERC20 Cumulative Outflow Breaker](/assertions-book/assertions/ass20-erc20-drain)
* [Panic State Validation](/assertions-book/assertions/ass17-panic-state-validation)
* [Owner Change](/assertions-book/assertions/ass05-ownership-change)