> ## 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.

# Tokens Borrowed Invariant

> Make sure that the tokens borrowed are not more than the tokens deposited

## When to Use This Pattern

Ensures the fundamental lending protocol invariant that total tokens borrowed never exceed total tokens deposited, preventing protocol insolvency and ensuring withdrawal requests can be honored. Critical for lending and borrowing platforms (Aave, Compound, Morpho), money markets with deposit/borrow pools, yield aggregators implementing lending strategies, and synthetic asset protocols with collateralized debt positions.

Violating this invariant could lead to protocol insolvency, loss of user funds, or destabilization of dependent DeFi ecosystems.

## What This Pattern Checks

Implements straightforward verification that total tokens borrowed never exceed total tokens deposited:

* `_postTx()`: Capture protocol state after transaction to verify invariant holds
* `registerTxEndTrigger()`: Trigger on storage slots tracking supply and borrow totals
* Check total supply of assets (tokens deposited) and total borrowed assets
* Assert total supply ≥ total borrowed assets

The assertion verifies final state after all transaction operations complete, ensuring the invariant holds at transaction boundaries. This is a known limitation - we cannot capture intermediate state changes during execution, only the final result.

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 TokensBorrowedInvariant is Assertion {
    bytes32 internal constant TOTAL_SUPPLY_SLOT = bytes32(uint256(0));
    bytes32 internal constant TOTAL_BORROW_SLOT = bytes32(uint256(1));

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

    function triggers() external view override {
        registerTxEndTrigger(this.assertBorrowedInvariant.selector);
    }

    /// @notice Checks that total supplied assets cover total borrowed assets after the transaction.
    function assertBorrowedInvariant() external view {
        address market = ph.getAssertionAdopter();
        PhEvm.ForkId memory postFork = _postTx();

        uint256 totalSupplyAsset = uint256(ph.loadStateAt(market, TOTAL_SUPPLY_SLOT, postFork));
        uint256 totalBorrowedAsset = uint256(ph.loadStateAt(market, TOTAL_BORROW_SLOT, postFork));

        require(
            totalSupplyAsset >= totalBorrowedAsset,
            "INVARIANT VIOLATION: Total supply of assets is less than total borrowed assets"
        );
    }
}
```

<Note>Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book).</Note>

## Related Patterns

* [Liquidation Health Factor](/assertions-book/assertions/ass16-liquidation-health-factor)
* [ERC20 Cumulative Outflow Breaker](/assertions-book/assertions/ass20-erc20-drain)
* [Lending Health Factor](/assertions-book/assertions/ass07-lending-health-factor)