​
Use Case & Applications

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.

​
Explanation

Implements straightforward verification that total tokens borrowed never exceed total tokens deposited:
  • ph.forkPostState(): Capture protocol state after transaction to verify invariant holds
  • registerStorageChangeTrigger(): 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.

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

interface IMorpho {
    function totalSupplyAsset() external view returns (uint256);
    function totalBorrowedAsset() external view returns (uint256);
}

// Assert that the total supply of assets is always greater than or equal to the total borrowed assets
contract TokensBorrowedInvariant is Assertion {
    IMorpho public immutable morpho;

    // Use specific storage slots for the protocol
    bytes32 private constant TOTAL_SUPPLY_SLOT = bytes32(uint256(0)); // Slot 0
    bytes32 private constant TOTAL_BORROW_SLOT = bytes32(uint256(1)); // Slot 1

    // Initialize the contract with the Morpho protocol address
    constructor(address morphoAddress) {
        morpho = IMorpho(morphoAddress);
    }

    function triggers() external view override {
        // Register triggers for changes to either storage slot with the main assertion function
        registerStorageChangeTrigger(this.assertBorrowedInvariant.selector, TOTAL_SUPPLY_SLOT);
        registerStorageChangeTrigger(this.assertBorrowedInvariant.selector, TOTAL_BORROW_SLOT);
    }

    // Check the invariant whenever supply or borrow values change
    function assertBorrowedInvariant() external {
        // Check the state after the transaction to ensure the invariant holds
        ph.forkPostState();

        // Get the current protocol state
        uint256 totalSupplyAsset = morpho.totalSupplyAsset();
        uint256 totalBorrowedAsset = morpho.totalBorrowedAsset();

        // Ensure the core invariant is maintained
        require(
            totalSupplyAsset >= totalBorrowedAsset,
            "INVARIANT VIOLATION: Total supply of assets is less than total borrowed assets"
        );
    }
}
Note: Full examples with tests available in the Phylax Assertion Examples Repository.