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

Ensures the constant product (k = x * y) is maintained in AMM pools, preventing unauthorized manipulation of pool reserves and potential flash loan attacks. Critical for Uniswap V2-style AMMs, DEX aggregators, lending protocols using AMM price oracles, and yield farming protocols providing liquidity. The constant product formula is fundamental to many AMM designs - any deviation could indicate a serious security issue or potential exploit.

​
What This Pattern Checks

Monitors the product of reserves (k) in AMM pools to ensure it remains constant after transactions using:
  • _preTx() / _postTx() with Reshiram snapshot reads: Compare reserve product before and after transaction
  • ph.loadStateAt(): Load reserve slots before and after the transaction
  • Direct validation that k = reserve0 * reserve1 remains unchanged
The assertion verifies both initial/final states and detects potential manipulations during transaction execution. 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 ConstantProductAssertion is Assertion {
    bytes32 internal constant RESERVE0_SLOT = bytes32(uint256(0));
    bytes32 internal constant RESERVE1_SLOT = bytes32(uint256(1));

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

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

    /// @notice Checks that the pool's stored reserve product is not reduced by the transaction.
    function assertionConstantProduct() external view {
        address pool = ph.getAssertionAdopter();
        PhEvm.ForkId memory preFork = _preTx();
        PhEvm.ForkId memory postFork = _postTx();

        uint256 reserve0Pre = uint256(ph.loadStateAt(pool, RESERVE0_SLOT, preFork));
        uint256 reserve1Pre = uint256(ph.loadStateAt(pool, RESERVE1_SLOT, preFork));
        uint256 reserve0Post = uint256(ph.loadStateAt(pool, RESERVE0_SLOT, postFork));
        uint256 reserve1Post = uint256(ph.loadStateAt(pool, RESERVE1_SLOT, postFork));

        require(reserve0Post * reserve1Post >= reserve0Pre * reserve1Pre, "Constant product invariant reduced");
    }
}
Full examples and mock protocol code are available in credible-std.