​
Use Case

This assertion verifies that the sum of all individual positions in a protocol exactly matches the total supply reported by the protocol. This is a critical security check that prevents several potential vulnerabilities:

  • Supply Manipulation: Ensures that positions cannot be minted or burned without being properly accounted for in the total supply
  • Double Counting: Prevents the same assets from being counted multiple times in different positions
  • Missing Deductions: Catches cases where assets are removed from positions but not subtracted from the total supply
  • Accounting Discrepancies: Identifies any discrepancies between the protocol’s internal accounting and the reported total supply

This assertion is particularly critical for protocols that manage user deposits and withdrawals, as any discrepancy between individual positions and total supply could lead to:

  • Incorrect interest calculations
  • Inability to withdraw funds
  • Protocol insolvency
  • Potential for economic attacks

​
Applicable Protocols

This assertion is essential for:

  • Lending Protocols: Where users deposit assets and receive interest, and the protocol must maintain accurate accounting of all deposits
  • Liquidity Pools: Such as AMMs or yield farms where users provide liquidity and the protocol tracks their share of the pool
  • Staking Mechanisms: Where users stake tokens and the protocol must accurately track all staked positions
  • Synthetic Asset Protocols: Where the protocol creates synthetic representations of assets and must maintain a 1:1 relationship between the underlying and synthetic assets
  • Fractionalized NFT Protocols: Where NFTs are split into multiple shares that must sum to the total value of the NFT

For these protocols, maintaining the integrity of the relationship between individual positions and total supply is fundamental to their security and economic model.

​
Explanation

This assertion works by comparing two key metrics:

  1. The sum of all individual positions in the protocol
  2. The total supply reported by the protocol

In a correctly functioning protocol, these two values should always be equal. Any discrepancy indicates a potential vulnerability in the protocol’s accounting system.

​
Implementation Approach

Since direct iteration over all non-zero entries in a mapping is not currently supported, we use a workaround based on function call inputs:

  1. Capture the pre-state total supply before the transaction
  2. Execute the transaction
  3. Identify all function calls that modify positions (e.g., deposit, withdraw)
  4. Calculate the sum of changes to these positions
  5. Verify that the new total supply equals the pre-state total supply plus the sum of position changes

This approach avoids the need to iterate over all positions while still effectively detecting accounting discrepancies.

Check the Modified Keys use case for a detailed breakdown of what the iteration over all positions would look like.

​
Cheatcodes Used

The assertion uses the following cheatcodes and functions:

  • ph.forkPreState(): Captures the state before the transaction
  • ph.forkPostState(): Creates a fork of the state after the transaction
  • ph.getCallInputs(): Gets the inputs to function calls for tracking position changes
  • registerCallTrigger(): Registers a trigger for deposit function calls

You can find more information about the cheatcodes in 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 a simple lending contract as an example
// Adjust accordingly to the interface of your protocol
interface ILending {
    function totalSupply() external view returns (uint256);
    function balanceOf(address account) external view returns (uint256);
    function deposit(address user, uint256 amount) external;
}

// Assert that the sum of all positions is the same as the total supply reported by the protocol
contract PositionSumAssertion is Assertion {
    ILending public lending;

    constructor(address _lending) {
        lending = ILending(_lending);
    }

    function triggers() external view override {
        // Register trigger for changes to the total supply
        registerCallTrigger(this.assertionPositionsSum.selector, lending.deposit.selector);
    }

    // Compare the sum of all updated positions to the total supply reported by the protocol
    function assertionPositionsSum() external {
        // Capture the pre-state total supply
        ph.forkPreState();
        uint256 preStateTotalSupply = lending.totalSupply();

        // Execute the transaction
        ph.forkPostState();

        // Get the new total supply
        uint256 newTotalSupply = lending.totalSupply();

        // Calculate the expected change in total supply
        uint256 expectedTotalSupplyChange = newTotalSupply - preStateTotalSupply;

        // Track the actual sum of position changes
        uint256 positionChangesSum = 0;

        // Get deposit function call inputs
        PhEvm.CallInputs[] memory callInputs = ph.getCallInputs(address(lending), lending.deposit.selector);

        // Process deposit function calls
        for (uint256 i = 0; i < callInputs.length; i++) {
            // Decode the function call input
            (address user, uint256 amount) = abi.decode(callInputs[i].input, (address, uint256));

            // Add the deposit amount to the position changes sum
            positionChangesSum += amount;
        }

        // Note: In a complete implementation, you would also check for withdraw calls
        // and other functions that modify positions. Ideally, you would have separate
        // assertion functions for each type of call to make the code more maintainable
        // and easier to understand.

        // Verify that the sum of position changes equals the change in total supply
        require(positionChangesSum == expectedTotalSupplyChange, "Positions sum does not match total supply");
    }
}

Note: This code example is maintained in the Phylax Assertion Examples Repository. For a full examples with mock protocol code and tests please refer to the repository.

​
Testing

To test this assertion effectively:

  1. Setup a test environment with a mock lending protocol that has:

    • A total supply function
    • A balance mapping for user positions
    • Functions to deposit and withdraw assets

  2. Create test scenarios that:

    • Make normal deposits and withdrawals
    • Attempt to manipulate the total supply without updating positions
    • Create edge cases with very large or very small position changes

  3. Verify the assertion catches:

    • Discrepancies between position changes and total supply changes
    • Cases where the total supply is updated incorrectly

​
Assertion Best Practices

When implementing this assertion:

  1. Function Call Tracking: Ensure you’re tracking all relevant function calls that modify positions. For complex protocols, this may include deposit, withdraw, transfer, and other custom functions.

  2. Precision Handling: Be careful with integer precision when summing changes, especially for protocols with very large numbers or when dealing with multiple function calls.

  3. Separate Assertions: Consider creating separate assertion functions for different types of position-modifying functions (deposits, withdrawals, transfers) to make the code more maintainable and easier to debug.

  4. Debugging Tips:

    • Log the pre-state total supply, position changes, and new total supply
    • Compare the expected vs. actual values when failures occur