Feature/uniswap v2 properties

CLAUDE.md

@@ -4,11 +4,12 @@ This file provides guidance to Claude Code (claude.ai/code) when working with co
 
 ## Project Overview
 
-This repository by Trail of Bits provides 168 pre-made Solidity property tests for fuzz testing smart contracts with [Echidna](https://github.com/crytic/echidna) or [Medusa](https://github.com/crytic/medusa). It covers:
+This repository by Trail of Bits provides 200+ pre-made Solidity property tests for fuzz testing smart contracts with [Echidna](https://github.com/crytic/echidna) or [Medusa](https://github.com/crytic/medusa). It covers:
 - ERC20 tokens (25 properties)
 - ERC721 tokens (19 properties)
 - ERC4626 vaults (37 properties)
 - ABDKMath64x64 fixed-point library (106 properties)
+- Uniswap V2 AMM pairs (30+ properties)
 
 ## Build Commands
 
@@ -56,6 +57,7 @@ medusa fuzz --target-contracts CryticERC20InternalHarness --config medusa-config
 ### Directory Structure
 - `contracts/` - Property contracts by standard
   - `ERC20/`, `ERC721/`, `ERC4626/` - Each split into `internal/` and `external/` testing
+  - `UniswapV2/` - Automated Market Maker (AMM) properties for constant product pools
   - `Math/ABDKMath64x64/` - Fixed-point math properties
   - `util/` - Helper functions (PropertiesHelper.sol, Hevm.sol, PropertiesConstants.sol)
 - `tests/` - Example test harnesses for Foundry and Hardhat

contracts/UniswapV2/internal/properties/UniswapV2BasicProperties.sol

@@ -0,0 +1,160 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+pragma solidity ^0.8.0;
+
+import "../util/UniswapV2TestBase.sol";
+
+/**
+ * @title Uniswap V2 Basic Properties (Liquidity Addition)
+ * @author Trail of Bits
+ * @notice Properties for testing liquidity addition (mint) in Uniswap V2 pairs
+ */
+abstract contract CryticUniswapV2BasicProperties is CryticUniswapV2Base {
+    constructor() {}
+
+    ////////////////////////////////////////
+    // Properties
+
+    // Adding liquidity should increase K
+    function test_V2_addLiquidityIncreasesK() public {
+        uint256 kBefore = _getK();
+        (uint112 reserve0Before, uint112 reserve1Before,) = getReserves();
+        require(reserve0Before > 0 && reserve1Before > 0);
+
+        uint256 liquidityMinted = mint(msg.sender);
+        require(liquidityMinted > 0);
+
+        uint256 kAfter = _getK();
+        assertGt(kAfter, kBefore, "K did not increase after adding liquidity");
+    }
+
+    // Adding liquidity should increase total supply of LP tokens
+    function test_V2_addLiquidityIncreasesTotalSupply() public {
+        uint256 supplyBefore = totalSupply();
+        (uint112 reserve0Before, uint112 reserve1Before,) = getReserves();
+        require(reserve0Before > 0 && reserve1Before > 0);
+
+        uint256 liquidityMinted = mint(msg.sender);
+        require(liquidityMinted > 0);
+
+        uint256 supplyAfter = totalSupply();
+        assertGt(
+            supplyAfter,
+            supplyBefore,
+            "Total supply did not increase after adding liquidity"
+        );
+    }
+
+    // Adding liquidity should increase reserves of both tokens
+    function test_V2_addLiquidityIncreasesReserves() public {
+        (uint112 reserve0Before, uint112 reserve1Before,) = getReserves();
+        require(reserve0Before > 0 && reserve1Before > 0);
+
+        uint256 liquidityMinted = mint(msg.sender);
+        require(liquidityMinted > 0);
+
+        (uint112 reserve0After, uint112 reserve1After,) = getReserves();
+        assertGt(
+            reserve0After,
+            reserve0Before,
+            "Reserve0 did not increase after adding liquidity"
+        );
+        assertGt(
+            reserve1After,
+            reserve1Before,
+            "Reserve1 did not increase after adding liquidity"
+        );
+    }
+
+    // Adding liquidity should increase the user's LP balance
+    function test_V2_addLiquidityIncreasesUserBalance() public {
+        uint256 balanceBefore = balanceOf(msg.sender);
+        (uint112 reserve0Before, uint112 reserve1Before,) = getReserves();
+        require(reserve0Before > 0 && reserve1Before > 0);
+
+        uint256 liquidityMinted = mint(msg.sender);
+        require(liquidityMinted > 0);
+
+        uint256 balanceAfter = balanceOf(msg.sender);
+        assertGt(
+            balanceAfter,
+            balanceBefore,
+            "User LP balance did not increase after adding liquidity"
+        );
+        assertEq(
+            balanceAfter - balanceBefore,
+            liquidityMinted,
+            "User LP balance increase does not equal minted liquidity"
+        );
+    }
+
+    // First mint should lock MINIMUM_LIQUIDITY (1000 tokens)
+    function test_V2_firstMintLocksMinimumLiquidity() public {
+        uint256 supply = totalSupply();
+
+        if (supply == 0) {
+            // This is the first mint
+            uint256 liquidityMinted = mint(msg.sender);
+            require(liquidityMinted > 0);
+
+            uint256 supplyAfter = totalSupply();
+            assertGte(
+                supplyAfter,
+                MINIMUM_LIQUIDITY,
+                "Total supply after first mint is less than MINIMUM_LIQUIDITY"
+            );
+
+            // The locked liquidity should be sent to address(0) or burned
+            // User receives: minted - MINIMUM_LIQUIDITY
+            uint256 userBalance = balanceOf(msg.sender);
+            assertEq(
+                userBalance + MINIMUM_LIQUIDITY,
+                supplyAfter,
+                "First mint did not properly lock MINIMUM_LIQUIDITY"
+            );
+        }
+    }
+
+    // Total supply should never be less than MINIMUM_LIQUIDITY after initialization
+    function test_V2_totalSupplyAboveMinimum() public {
+        uint256 supply = totalSupply();
+
+        if (supply > 0) {
+            assertGte(
+                supply,
+                MINIMUM_LIQUIDITY,
+                "Total supply fell below MINIMUM_LIQUIDITY"
+            );
+        }
+    }
+
+    // LP token balance of zero address should be MINIMUM_LIQUIDITY (burned on first mint)
+    function test_V2_zeroAddressHoldsMinimumLiquidity() public {
+        uint256 supply = totalSupply();
+
+        if (supply > 0) {
+            uint256 zeroBalance = balanceOf(address(0));
+            // On first mint, MINIMUM_LIQUIDITY is sent to address(0)
+            assertGte(
+                zeroBalance,
+                0,
+                "Zero address LP balance check failed"
+            );
+        }
+    }
+
+    // Minting zero liquidity should fail
+    function test_V2_mintZeroLiquidityFails() public {
+        (uint112 reserve0Before, uint112 reserve1Before,) = getReserves();
+
+        // If reserves haven't changed since last mint, should mint 0 liquidity
+        if (reserve0Before > 0 && reserve1Before > 0) {
+            // Don't transfer any new tokens
+            // Attempting to mint should fail or return 0
+            try this.mint(msg.sender) returns (uint256 liquidity) {
+                assertEq(liquidity, 0, "Minted non-zero liquidity without adding tokens");
+            } catch {
+                // Expected to fail
+            }
+        }
+    }
+}

contracts/UniswapV2/internal/properties/UniswapV2InvariantProperties.sol

@@ -0,0 +1,209 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+pragma solidity ^0.8.0;
+
+import "../util/UniswapV2TestBase.sol";
+
+/**
+ * @title Uniswap V2 Invariant Properties
+ * @author Trail of Bits
+ * @notice Core invariant and security properties for Uniswap V2 pairs
+ * @dev These properties test the constant product formula (x*y=k) and critical security invariants
+ */
+abstract contract CryticUniswapV2InvariantProperties is CryticUniswapV2Base {
+    constructor() {}
+
+    ////////////////////////////////////////
+    // Core Invariant Properties
+
+    // K should never decrease except through liquidity removal
+    function test_V2_kNeverDecreasesExceptBurn() public {
+        uint256 kBefore = _getK();
+        uint256 balanceBefore = balanceOf(msg.sender);
+
+        // Perform any operation
+        // (This will be fuzzed by Echidna/Medusa)
+
+        uint256 kAfter = _getK();
+        uint256 balanceAfter = balanceOf(msg.sender);
+
+        // If user didn't burn LP tokens, K should not decrease
+        if (balanceAfter >= balanceBefore) {
+            assertGte(kAfter, kBefore, "K decreased without burning liquidity");
+        }
+    }
+
+    // Reserves should never be zero after initialization
+    function test_V2_reservesNeverZeroAfterInit() public {
+        uint256 supply = totalSupply();
+
+        if (supply > 0) {
+            (uint112 reserve0, uint112 reserve1,) = getReserves();
+            assertGt(reserve0, 0, "Reserve0 is zero after initialization");
+            assertGt(reserve1, 0, "Reserve1 is zero after initialization");
+        }
+    }
+
+    // Total supply should equal sum of all balances
+    function test_V2_totalSupplyEqualsBalances() public {
+        uint256 supply = totalSupply();
+        uint256 balance0 = balanceOf(address(0));
+        uint256 balance1 = balanceOf(USER1);
+        uint256 balance2 = balanceOf(USER2);
+        uint256 balance3 = balanceOf(USER3);
+
+        uint256 sumBalances = balance0 + balance1 + balance2 + balance3;
+
+        // Sum of tracked balances should not exceed total supply
+        assertLte(
+            sumBalances,
+            supply,
+            "Sum of balances exceeds total supply"
+        );
+    }
+
+    ////////////////////////////////////////
+    // Security Properties
+
+    // First depositor attack protection: MINIMUM_LIQUIDITY is locked
+    function test_V2_minimumLiquidityLocked() public {
+        uint256 supply = totalSupply();
+
+        if (supply > 0) {
+            assertGte(
+                supply,
+                MINIMUM_LIQUIDITY,
+                "Total supply below MINIMUM_LIQUIDITY (first depositor protection broken)"
+            );
+        }
+    }
+
+    // Donation attack resistance: Direct transfers should not affect LP value
+    function test_V2_donationDoesNotInflateLPValue() public {
+        uint256 supply = totalSupply();
+        require(supply > MINIMUM_LIQUIDITY);
+
+        uint256 lpValueBefore = _getLPTokenValue();
+
+        // Simulate donation by calling sync() which updates reserves to balances
+        // In a real attack, attacker would transfer tokens directly to the pair
+        sync();
+
+        uint256 lpValueAfter = _getLPTokenValue();
+
+        // LP value per token should not change significantly from sync alone
+        // Allow small deviation for rounding
+        if (lpValueBefore > 0) {
+            uint256 diff = lpValueAfter > lpValueBefore
+                ? lpValueAfter - lpValueBefore
+                : lpValueBefore - lpValueAfter;
+            uint256 percentDiff = (diff * 100) / lpValueBefore;
+
+            assertLte(
+                percentDiff,
+                1, // 1% tolerance
+                "LP value changed significantly from sync (donation attack risk)"
+            );
+        }
+    }
+
+    // No free money: mint then burn should not be profitable
+    function test_V2_mintBurnNotProfitable() public {
+        (uint112 reserve0Before, uint112 reserve1Before,) = getReserves();
+        require(reserve0Before > 1000 && reserve1Before > 1000);
+
+        uint256 supply = totalSupply();
+        require(supply > MINIMUM_LIQUIDITY);
+
+        // Calculate expected amounts for a proportional deposit
+        uint256 amount0 = 1000;
+        uint256 amount1 = (uint256(amount0) * reserve1Before) / reserve0Before;
+
+        // Simulate providing liquidity
+        uint256 liquidity = mint(msg.sender);
+        require(liquidity > 0);
+
+        // Immediately burn
+        (uint256 returned0, uint256 returned1) = burn(msg.sender);
+
+        // User should not receive more than they put in (accounting for rounding)
+        assertLte(returned0, amount0 + 1, "Mint-burn profitable in token0");
+        assertLte(returned1, amount1 + 1, "Mint-burn profitable in token1");
+    }
+
+    // Price accumulator should be monotonically increasing
+    function test_V2_priceAccumulatorMonotonic() public {
+        uint256 accumulator0Before = price0CumulativeLast();
+        uint256 accumulator1Before = price1CumulativeLast();
+
+        // Advance time
+        require(block.timestamp > 0);
+
+        // Trigger price accumulator update
+        sync();
+
+        uint256 accumulator0After = price0CumulativeLast();
+        uint256 accumulator1After = price1CumulativeLast();
+
+        // Price accumulators should never decrease
+        assertGte(
+            accumulator0After,
+            accumulator0Before,
+            "Price0 accumulator decreased"
+        );
+        assertGte(
+            accumulator1After,
+            accumulator1Before,
+            "Price1 accumulator decreased"
+        );
+    }
+
+    // LP tokens should represent proportional ownership
+    function test_V2_lpTokensProportional() public {
+        uint256 supply = totalSupply();
+        require(supply > MINIMUM_LIQUIDITY);
+
+        uint256 userBalance = balanceOf(msg.sender);
+        require(userBalance > 0);
+
+        (uint112 reserve0, uint112 reserve1,) = getReserves();
+
+        // User's share of reserves should equal their LP token share
+        uint256 expectedShare0 = (uint256(reserve0) * userBalance) / supply;
+        uint256 expectedShare1 = (uint256(reserve1) * userBalance) / supply;
+
+        // These represent the user's claimable amounts
+        assertGt(expectedShare0, 0, "User has zero share of reserve0");
+        assertGt(expectedShare1, 0, "User has zero share of reserve1");
+
+        // Shares should be proportional
+        uint256 ratio0 = (userBalance * 1000) / supply;
+        uint256 expectedRatio0 = (expectedShare0 * 1000) / reserve0;
+
+        // Allow small rounding difference
+        uint256 diff = ratio0 > expectedRatio0
+            ? ratio0 - expectedRatio0
+            : expectedRatio0 - ratio0;
+
+        assertLte(diff, 1, "LP tokens not proportional to ownership");
+    }
+
+    // Flash swap must restore K (plus fees)
+    function test_V2_flashSwapRestoresK() public {
+        uint256 kBefore = _getK();
+        (uint112 reserve0, uint112 reserve1,) = getReserves();
+        require(reserve0 > 1000 && reserve1 > 1000);
+
+        // Perform a flash swap (borrow tokens, repay in callback)
+        uint256 amount0Out = uint256(reserve0) / 100;
+
+        try this.swap(amount0Out, 0, address(this), hex"01") {
+            // Flash swap callback executed
+            uint256 kAfter = _getK();
+
+            // K should be restored (plus fees)
+            assertGte(kAfter, kBefore, "K not restored after flash swap");
+        } catch {
+            // Flash swap might not be implemented or callback failed
+        }
+    }
+}