​
Use Case

Check if the constant product (k = x * y) is maintained in an AMM pool. This is a critical security parameter for Automated Market Maker (AMM) protocols as it ensures:

  • Prevention of unauthorized manipulation of pool reserves
  • Detection of potential flash loan attacks that could drain the pool
  • Verification that trades maintain the expected mathematical relationship between assets
  • Protection against arithmetic overflow/underflow vulnerabilities in reserve calculations

The constant product formula (k = x * y) is fundamental to many AMM designs, particularly those following the Uniswap V2 model. Any deviation from this invariant could indicate a serious security issue or potential exploit.

​
Applicable Protocols

  • Uniswap V2-style AMMs that use the x * y = k formula
  • DEX aggregators that interact with constant product pools
  • Lending protocols that use AMM pools as price oracles
  • Yield farming protocols that provide liquidity to AMM pools

These protocols rely heavily on the constant product invariant for:

  • Price discovery and trading
  • Liquidity provision calculations
  • Fee calculations
  • Oracle price feeds

​
Explanation

The assertion monitors the product of reserves (k) in an AMM pool to ensure it remains constant after transactions:

  1. Pre-state verification: Captures the initial state of pool reserves
  2. Post-state verification: Checks the final state after transactions
  3. Constant product validation: Ensures k = reserve0 * reserve1 remains unchanged

The assertion uses the following cheatcodes:

  • forkPreState(): Creates a fork of the state before the transaction to capture initial reserves
  • forkPostState(): Creates a fork of the state after the transaction to verify final reserves
  • getStateChanges(): Monitors reserve changes throughout the transaction callstack to detect potential manipulations

The implementation performs two checks:

  1. A direct comparison between pre-state and post-state constant product values
  2. Verification that the final product equals the initial product

This approach ensures that:

  • The constant product invariant is maintained throughout the transaction
  • No unauthorized manipulation of reserves occurs
  • The mathematical relationship between assets is preserved

Note that as mentioned in the code comments, an ideal solution would allow for checking the invariant at any point during the transaction’s execution, not just at the beginning and end.

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";
// Aerodrome style pool interface

interface IAmm {
    function getReserves() external view returns (uint256, uint256);
}

contract ConstantProductAssertion is Assertion {
    IAmm public amm;

    constructor(address _amm) {
        amm = IAmm(_amm);
    }

    function triggers() external view override {
        // Register triggers for both reserve slots for each assertion
        // This ensures we catch any modifications to either reserve
        registerStorageChangeTrigger(this.assertionConstantProduct.selector, bytes32(uint256(0)));
        registerStorageChangeTrigger(this.assertionConstantProduct.selector, bytes32(uint256(1)));
    }

    // Assert that the constant product (k = x * y) invariant is maintained
    // This is done by comparing the pre-state and post-state values
    //
    // NOTE: Due to current limitations in getStateChanges, there are no guarantees
    // regarding timing when comparing values from two stateChanges arrays throughout the callstack.
    // An ideal solution in the future would allow for comparing values at any given
    // point in time during the callstack, thus making it possible to prevent
    // potential intra-transaction manipulations of the constant product invariant.
    //
    // For example, a malicious actor could temporarily manipulate the reserves
    // to violate the invariant during the transaction, then restore them before
    // the end of the transaction to avoid detection in a pre/post comparison.
    function assertionConstantProduct() external {
        // Get pre-state reserves and calculate initial k
        ph.forkPreState();
        (uint256 reserve0Pre, uint256 reserve1Pre) = amm.getReserves();
        uint256 kPre = reserve0Pre * reserve1Pre;

        // Get post-state reserves and calculate final k
        ph.forkPostState();
        (uint256 reserve0Post, uint256 reserve1Post) = amm.getReserves();
        uint256 kPost = reserve0Post * reserve1Post;

        // Verify the final state maintains the constant product
        require(kPre == kPost, "Constant product invariant violated");
    }
}

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:

  1. Deploy an AMM pool with the constant product formula
  2. Set up the assertion contract with the pool address
  3. Test various scenarios:
    • Normal trades that maintain the constant product
    • Edge cases with very small/large numbers
    • Attempted manipulations that should be caught
    • Flash loan attacks that try to drain the pool

​
Assertion Best Practices

  • Consider combining this assertion with Fee Calculations for comprehensive AMM security
  • Use precise arithmetic checks to prevent rounding errors from triggering false positives
  • Monitor both reserve slots to catch any unauthorized modifications
  • Add detailed error messages to help with debugging when assertions fail