Skip to main content

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.

​
When to Use This Pattern

Enforces a critical ERC4626 vault invariant: total shares must never exceed total assets converted to shares, preventing share price manipulation and fund loss. Critical for yield aggregators, lending protocols implementing ERC4626, liquidity pools using ERC4626 for LP tokens, and staking protocols with ERC4626 vaults. Any violation could allow unauthorized share minting that dilutes existing holders or enables withdrawal of more assets than deposited, potentially leading to protocol insolvency.

​
What This Pattern Checks

Verifies the fundamental ERC4626 share-to-asset relationship using a basic approach:
  • registerTxEndTrigger(): Trigger when total supply storage slot changes
  • Verify total assets are sufficient to back all outstanding shares
  • Ensure share value is preserved and users can withdraw their assets
This ensures there are always enough assets to back all shares, maintaining accurate share values and preventing value extraction from the vault. For more information about cheatcodes, see the Cheatcodes Documentation.

​
Assertion Pattern

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

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

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

    /// @notice Checks that stored total assets are sufficient to back stored total shares.
    function assertionAssetsShares() external view {
        address vault = ph.getAssertionAdopter();
        PhEvm.ForkId memory postFork = _postTx();

        uint256 totalAssets = uint256(ph.loadStateAt(vault, TOTAL_ASSETS_SLOT, postFork));
        uint256 totalSupply = uint256(ph.loadStateAt(vault, TOTAL_SUPPLY_SLOT, postFork));

        require(totalAssets >= totalSupply, "Not enough assets to back all shares");
    }
}
Full examples and mock protocol code are available in credible-std.