From 82d209a1d5b1ac2d79ed4bcfd96fa21295793ea1 Mon Sep 17 00:00:00 2001 From: Omar Inuwa Date: Fri, 28 Nov 2025 08:19:06 +0100 Subject: [PATCH 1/2] Add Uniswap V2 AMM properties Implements 30+ property tests for Uniswap V2 constant product (x*y=k) automated market makers. These properties cover liquidity provision, removal, swaps, and critical security invariants. Properties Implemented: Basic Properties (8 properties): - Adding liquidity increases K, total supply, reserves, and user LP balance - First mint locks MINIMUM_LIQUIDITY (1000 tokens) to prevent first depositor attack - Total supply maintained above MINIMUM_LIQUIDITY after initialization Remove Liquidity Properties (7 properties): - Removing liquidity decreases K, total supply, reserves, and user LP balance - Burn returns proportional amounts of both tokens - Total supply never falls below MINIMUM_LIQUIDITY Swap Properties (8 properties): - Swapping does not decrease K (increases due to 0.3% fees) - Price moves in correct direction based on swap - LP token balances unaffected by swaps - Zero amount swaps have no effect - Insufficient liquidity and invalid swaps fail Invariant Properties (10 properties): - K never decreases except through liquidity removal (core invariant) - Reserves never zero after initialization - Total supply equals sum of balances - MINIMUM_LIQUIDITY locked prevents first depositor attacks - Donation attack resistance: direct transfers don't inflate LP value - No free money: mint then immediate burn not profitable - Price accumulator monotonically increasing (TWAP oracle) - LP tokens represent proportional ownership - Flash swaps must restore K (plus fees) Files Added: Property Contracts: - contracts/UniswapV2/internal/properties/UniswapV2BasicProperties.sol - contracts/UniswapV2/internal/properties/UniswapV2RemoveLiquidityProperties.sol - contracts/UniswapV2/internal/properties/UniswapV2SwapProperties.sol - contracts/UniswapV2/internal/properties/UniswapV2InvariantProperties.sol Utilities: - contracts/UniswapV2/util/IUniswapV2Pair.sol (minimal interface) - contracts/UniswapV2/internal/util/UniswapV2TestBase.sol (base contract) Test Harness: - tests/UniswapV2/foundry/src/SimplePair.sol (example implementation) - tests/UniswapV2/foundry/src/MockERC20.sol (test token) - tests/UniswapV2/foundry/test/CryticUniswapV2Test.sol (complete harness) Updated: - CLAUDE.md (added UniswapV2 to project overview) Security Properties Coverage: First Depositor Attack Protection: The MINIMUM_LIQUIDITY mechanism prevents share price manipulation on first deposit by burning 1000 LP tokens. Properties verify this protection is maintained throughout the pool lifecycle. Donation Attack Resistance: Properties verify that direct token transfers (donations) to the pair do not inflate LP token value. Similar to ERC4626 inflation attacks and Euler donation attack pattern. Constant Product Invariant (x*y=k): Core properties ensure K never decreases except through liquidity removal. Swaps must increase K due to 0.3% fees. Violations indicate value leakage or fee bypass. No Free Money: Properties verify mint-burn cycles cannot be profitable, catching rounding errors and integer overflow/underflow issues. Flash Swap Safety: Properties ensure flash swaps (borrow-repay in single transaction) restore K plus fees, preventing free token extraction. Testing Approach: These properties support internal testing mode (test contract inherits from pair implementation). External testing mode can be added following the same pattern as ERC20/ERC721 properties. Example Usage: contract MyPairTest is MyUniswapV2Pair, CryticUniswapV2BasicProperties, CryticUniswapV2InvariantProperties { // Run with: echidna . --contract MyPairTest --config echidna-config.yaml } Resolves #4 --- CLAUDE.md | 4 +- .../properties/UniswapV2BasicProperties.sol | 160 ++++++++++++++ .../UniswapV2InvariantProperties.sol | 209 ++++++++++++++++++ .../UniswapV2RemoveLiquidityProperties.sol | 141 ++++++++++++ .../properties/UniswapV2SwapProperties.sol | 158 +++++++++++++ .../internal/util/UniswapV2TestBase.sol | 63 ++++++ contracts/UniswapV2/util/IUniswapV2Pair.sol | 17 ++ tests/UniswapV2/foundry/src/MockERC20.sol | 39 ++++ tests/UniswapV2/foundry/src/SimplePair.sol | 153 +++++++++++++ .../foundry/test/CryticUniswapV2Test.sol | 44 ++++ 10 files changed, 987 insertions(+), 1 deletion(-) create mode 100644 contracts/UniswapV2/internal/properties/UniswapV2BasicProperties.sol create mode 100644 contracts/UniswapV2/internal/properties/UniswapV2InvariantProperties.sol create mode 100644 contracts/UniswapV2/internal/properties/UniswapV2RemoveLiquidityProperties.sol create mode 100644 contracts/UniswapV2/internal/properties/UniswapV2SwapProperties.sol create mode 100644 contracts/UniswapV2/internal/util/UniswapV2TestBase.sol create mode 100644 contracts/UniswapV2/util/IUniswapV2Pair.sol create mode 100644 tests/UniswapV2/foundry/src/MockERC20.sol create mode 100644 tests/UniswapV2/foundry/src/SimplePair.sol create mode 100644 tests/UniswapV2/foundry/test/CryticUniswapV2Test.sol diff --git a/CLAUDE.md b/CLAUDE.md index 62dc1e8..f763655 100644 --- a/CLAUDE.md +++ b/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 diff --git a/contracts/UniswapV2/internal/properties/UniswapV2BasicProperties.sol b/contracts/UniswapV2/internal/properties/UniswapV2BasicProperties.sol new file mode 100644 index 0000000..7f8c82b --- /dev/null +++ b/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 + } + } + } +} diff --git a/contracts/UniswapV2/internal/properties/UniswapV2InvariantProperties.sol b/contracts/UniswapV2/internal/properties/UniswapV2InvariantProperties.sol new file mode 100644 index 0000000..413e0ed --- /dev/null +++ b/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 + } + } +} diff --git a/contracts/UniswapV2/internal/properties/UniswapV2RemoveLiquidityProperties.sol b/contracts/UniswapV2/internal/properties/UniswapV2RemoveLiquidityProperties.sol new file mode 100644 index 0000000..af29831 --- /dev/null +++ b/contracts/UniswapV2/internal/properties/UniswapV2RemoveLiquidityProperties.sol @@ -0,0 +1,141 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "../util/UniswapV2TestBase.sol"; + +/** + * @title Uniswap V2 Remove Liquidity Properties + * @author Trail of Bits + * @notice Properties for testing liquidity removal (burn) in Uniswap V2 pairs + */ +abstract contract CryticUniswapV2RemoveLiquidityProperties is CryticUniswapV2Base { + constructor() {} + + //////////////////////////////////////// + // Properties + + // Removing liquidity should decrease K + function test_V2_removeLiquidityDecreasesK() public { + uint256 kBefore = _getK(); + uint256 userBalance = balanceOf(msg.sender); + require(userBalance > 0); + require(kBefore > 0); + + (uint256 amount0, uint256 amount1) = burn(msg.sender); + require(amount0 > 0 || amount1 > 0); + + uint256 kAfter = _getK(); + assertLt(kAfter, kBefore, "K did not decrease after removing liquidity"); + } + + // Removing liquidity should decrease total supply of LP tokens + function test_V2_removeLiquidityDecreasesTotalSupply() public { + uint256 supplyBefore = totalSupply(); + uint256 userBalance = balanceOf(msg.sender); + require(userBalance > 0); + + (uint256 amount0, uint256 amount1) = burn(msg.sender); + require(amount0 > 0 || amount1 > 0); + + uint256 supplyAfter = totalSupply(); + assertLt( + supplyAfter, + supplyBefore, + "Total supply did not decrease after removing liquidity" + ); + } + + // Removing liquidity should decrease reserves of both tokens + function test_V2_removeLiquidityDecreasesReserves() public { + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + uint256 userBalance = balanceOf(msg.sender); + require(userBalance > 0); + require(reserve0Before > 0 && reserve1Before > 0); + + (uint256 amount0, uint256 amount1) = burn(msg.sender); + require(amount0 > 0 && amount1 > 0); + + (uint112 reserve0After, uint112 reserve1After,) = getReserves(); + assertLt( + reserve0After, + reserve0Before, + "Reserve0 did not decrease after removing liquidity" + ); + assertLt( + reserve1After, + reserve1Before, + "Reserve1 did not decrease after removing liquidity" + ); + } + + // Removing liquidity should decrease the user's LP balance + function test_V2_removeLiquidityDecreasesUserBalance() public { + uint256 balanceBefore = balanceOf(msg.sender); + require(balanceBefore > 0); + + (uint256 amount0, uint256 amount1) = burn(msg.sender); + require(amount0 > 0 || amount1 > 0); + + uint256 balanceAfter = balanceOf(msg.sender); + assertLt( + balanceAfter, + balanceBefore, + "User LP balance did not decrease after removing liquidity" + ); + } + + // Burning zero liquidity should return zero amounts + function test_V2_burnZeroLiquidity() public { + uint256 userBalance = balanceOf(msg.sender); + + if (userBalance == 0) { + (uint256 amount0, uint256 amount1) = burn(msg.sender); + assertEq(amount0, 0, "Burning zero liquidity returned non-zero amount0"); + assertEq(amount1, 0, "Burning zero liquidity returned non-zero amount1"); + } + } + + // Burning should return proportional amounts + function test_V2_burnReturnsProportionalAmounts() public { + (uint112 reserve0, uint112 reserve1,) = getReserves(); + uint256 supply = totalSupply(); + uint256 userBalance = balanceOf(msg.sender); + + require(userBalance > 0); + require(supply > 0); + require(reserve0 > 0 && reserve1 > 0); + + (uint256 amount0, uint256 amount1) = burn(msg.sender); + + if (amount0 > 0 && amount1 > 0) { + // Check proportionality: amount0/reserve0 ≈ amount1/reserve1 + // Allow 1% deviation for rounding + uint256 ratio0 = (amount0 * 1000) / reserve0; + uint256 ratio1 = (amount1 * 1000) / reserve1; + + uint256 diff = ratio0 > ratio1 ? ratio0 - ratio1 : ratio1 - ratio0; + assertLte( + diff, + 10, // 1% tolerance + "Burn did not return proportional amounts" + ); + } + } + + // Total supply should never fall below MINIMUM_LIQUIDITY + function test_V2_totalSupplyNeverBelowMinimum() public { + uint256 supply = totalSupply(); + uint256 userBalance = balanceOf(msg.sender); + + if (userBalance > 0 && supply > MINIMUM_LIQUIDITY) { + burn(msg.sender); + + uint256 supplyAfter = totalSupply(); + assertGte( + supplyAfter, + MINIMUM_LIQUIDITY, + "Total supply fell below MINIMUM_LIQUIDITY after burn" + ); + } + } +} diff --git a/contracts/UniswapV2/internal/properties/UniswapV2SwapProperties.sol b/contracts/UniswapV2/internal/properties/UniswapV2SwapProperties.sol new file mode 100644 index 0000000..e1c3ec6 --- /dev/null +++ b/contracts/UniswapV2/internal/properties/UniswapV2SwapProperties.sol @@ -0,0 +1,158 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "../util/UniswapV2TestBase.sol"; + +/** + * @title Uniswap V2 Swap Properties + * @author Trail of Bits + * @notice Properties for testing token swaps in Uniswap V2 pairs + */ +abstract contract CryticUniswapV2SwapProperties is CryticUniswapV2Base { + constructor() {} + + //////////////////////////////////////// + // Properties + + // Swapping should not decrease K (should increase due to fees) + function test_V2_swapDoesNotDecreaseK() public { + uint256 kBefore = _getK(); + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + require(reserve0Before > 0 && reserve1Before > 0); + + // Perform a swap (amount0Out > 0 means buying token0) + uint256 amount0Out = uint256(reserve0Before) / 100; // 1% of reserves + require(amount0Out > 0); + + swap(amount0Out, 0, msg.sender, ""); + + uint256 kAfter = _getK(); + assertGte(kAfter, kBefore, "K decreased after swap"); + } + + // Swapping should move price in correct direction + function test_V2_swapMovesPriceCorrectly() public { + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + require(reserve0Before > 0 && reserve1Before > 0); + + uint256 price0Before = _getPrice0(); + + // Buy token0 (sell token1) + uint256 amount0Out = uint256(reserve0Before) / 100; + require(amount0Out > 0 && amount0Out < reserve0Before); + + swap(amount0Out, 0, msg.sender, ""); + + uint256 price0After = _getPrice0(); + + // Buying token0 should increase its price (decrease reserve0, increase reserve1) + assertGt( + price0After, + price0Before, + "Price did not move correctly after swap" + ); + } + + // Swapping should not decrease LP token balance (unless fees are on) + function test_V2_swapDoesNotDecreaseLPBalance() public { + uint256 balanceBefore = balanceOf(msg.sender); + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + require(reserve0Before > 0 && reserve1Before > 0); + + uint256 amount0Out = uint256(reserve0Before) / 100; + require(amount0Out > 0 && amount0Out < reserve0Before); + + swap(amount0Out, 0, msg.sender, ""); + + uint256 balanceAfter = balanceOf(msg.sender); + + // LP balance should not decrease from a swap (might increase if protocol fees are on) + assertGte( + balanceAfter, + balanceBefore, + "LP balance decreased after swap" + ); + } + + // Swapping zero amounts should not change reserves + function test_V2_swapZeroAmountNoEffect() public { + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + + // Swap zero amounts + swap(0, 0, msg.sender, ""); + + (uint112 reserve0After, uint112 reserve1After,) = getReserves(); + + assertEq(reserve0After, reserve0Before, "Reserve0 changed after zero swap"); + assertEq(reserve1After, reserve1Before, "Reserve1 changed after zero swap"); + } + + // Swapping with insufficient liquidity should fail + function test_V2_swapInsufficientLiquidityFails() public { + (uint112 reserve0, uint112 reserve1,) = getReserves(); + require(reserve0 > 0 && reserve1 > 0); + + // Try to swap more than available reserves + try this.swap(uint256(reserve0) + 1, 0, msg.sender, "") { + assertWithMsg(false, "Swap with insufficient liquidity did not fail"); + } catch { + // Expected to fail + } + } + + // Swapping both directions simultaneously should fail + function test_V2_swapBothDirectionsFails() public { + (uint112 reserve0, uint112 reserve1,) = getReserves(); + require(reserve0 > 0 && reserve1 > 0); + + uint256 amount0Out = uint256(reserve0) / 100; + uint256 amount1Out = uint256(reserve1) / 100; + require(amount0Out > 0 && amount1Out > 0); + + // Swapping both tokens out should fail + try this.swap(amount0Out, amount1Out, msg.sender, "") { + assertWithMsg(false, "Swap in both directions did not fail"); + } catch { + // Expected to fail + } + } + + // Swap output should be positive if input is provided + function test_V2_swapPositiveOutput() public { + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + require(reserve0Before > 1000 && reserve1Before > 1000); + + uint256 amount1Out = 100; // Request small amount of token1 + + // The swap should succeed if we provide enough token0 + try this.swap(0, amount1Out, msg.sender, "") { + (uint112 reserve0After, uint112 reserve1After,) = getReserves(); + + // Reserve1 should have decreased (we received token1) + assertLt(reserve1After, reserve1Before, "Reserve1 did not decrease"); + + // Reserve0 should have increased (we paid token0) + assertGt(reserve0After, reserve0Before, "Reserve0 did not increase"); + } catch { + // Might fail if we didn't provide enough input tokens + } + } + + // K should increase by at least the fee amount (0.3%) + function test_V2_swapIncreasesKByFee() public { + uint256 kBefore = _getK(); + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + require(reserve0Before > 10000 && reserve1Before > 10000); + + uint256 amount0Out = uint256(reserve0Before) / 100; + require(amount0Out > 0 && amount0Out < reserve0Before); + + swap(amount0Out, 0, msg.sender, ""); + + uint256 kAfter = _getK(); + + // K should increase (fees accumulate in the pool) + // Due to 0.3% fee, K_after > K_before + assertGt(kAfter, kBefore, "K did not increase after swap (fee not collected)"); + } +} diff --git a/contracts/UniswapV2/internal/util/UniswapV2TestBase.sol b/contracts/UniswapV2/internal/util/UniswapV2TestBase.sol new file mode 100644 index 0000000..f8b9981 --- /dev/null +++ b/contracts/UniswapV2/internal/util/UniswapV2TestBase.sol @@ -0,0 +1,63 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "../../../util/PropertiesConstants.sol"; +import "../../../util/PropertiesAsserts.sol"; + +abstract contract CryticUniswapV2Base is + PropertiesAsserts, + PropertiesConstants +{ + // Minimum liquidity locked forever (Uniswap V2 constant) + uint256 internal constant MINIMUM_LIQUIDITY = 1000; + + constructor() {} + + //////////////////////////////////////// + // Abstract functions to be implemented by inheriting contract + + function token0() public view virtual returns (address); + function token1() public view virtual returns (address); + function getReserves() public view virtual returns (uint112 reserve0, uint112 reserve1, uint32 blockTimestampLast); + function price0CumulativeLast() public view virtual returns (uint256); + function price1CumulativeLast() public view virtual returns (uint256); + function kLast() public view virtual returns (uint256); + function totalSupply() public view virtual returns (uint256); + function balanceOf(address account) public view virtual returns (uint256); + + function mint(address to) public virtual returns (uint256 liquidity); + function burn(address to) public virtual returns (uint256 amount0, uint256 amount1); + function swap(uint256 amount0Out, uint256 amount1Out, address to, bytes calldata data) public virtual; + function skim(address to) public virtual; + function sync() public virtual; + + //////////////////////////////////////// + // Helper functions + + function _getK() internal view returns (uint256) { + (uint112 reserve0, uint112 reserve1,) = getReserves(); + return uint256(reserve0) * uint256(reserve1); + } + + function _getLPTokenValue() internal view returns (uint256) { + uint256 supply = totalSupply(); + if (supply == 0) return 0; + + (uint112 reserve0, uint112 reserve1,) = getReserves(); + // Value per LP token = (reserve0 + reserve1) / totalSupply + // Simplified assuming token0 and token1 have same value + return (uint256(reserve0) + uint256(reserve1)) / supply; + } + + function _getPrice0() internal view returns (uint256) { + (uint112 reserve0, uint112 reserve1,) = getReserves(); + if (reserve0 == 0) return 0; + return (uint256(reserve1) * 1e18) / uint256(reserve0); + } + + function _getPrice1() internal view returns (uint256) { + (uint112 reserve0, uint112 reserve1,) = getReserves(); + if (reserve1 == 0) return 0; + return (uint256(reserve0) * 1e18) / uint256(reserve1); + } +} diff --git a/contracts/UniswapV2/util/IUniswapV2Pair.sol b/contracts/UniswapV2/util/IUniswapV2Pair.sol new file mode 100644 index 0000000..e7d8eae --- /dev/null +++ b/contracts/UniswapV2/util/IUniswapV2Pair.sol @@ -0,0 +1,17 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +interface IUniswapV2Pair { + function token0() external view returns (address); + function token1() external view returns (address); + function getReserves() external view returns (uint112 reserve0, uint112 reserve1, uint32 blockTimestampLast); + function price0CumulativeLast() external view returns (uint256); + function price1CumulativeLast() external view returns (uint256); + function kLast() external view returns (uint256); + + function mint(address to) external returns (uint256 liquidity); + function burn(address to) external returns (uint256 amount0, uint256 amount1); + function swap(uint256 amount0Out, uint256 amount1Out, address to, bytes calldata data) external; + function skim(address to) external; + function sync() external; +} diff --git a/tests/UniswapV2/foundry/src/MockERC20.sol b/tests/UniswapV2/foundry/src/MockERC20.sol new file mode 100644 index 0000000..de23369 --- /dev/null +++ b/tests/UniswapV2/foundry/src/MockERC20.sol @@ -0,0 +1,39 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +contract MockERC20 { + string public name; + string public symbol; + uint8 public decimals = 18; + uint256 public totalSupply; + mapping(address => uint256) public balanceOf; + mapping(address => mapping(address => uint256)) public allowance; + + constructor(string memory _name, string memory _symbol) { + name = _name; + symbol = _symbol; + } + + function transfer(address to, uint256 amount) external returns (bool) { + balanceOf[msg.sender] -= amount; + balanceOf[to] += amount; + return true; + } + + function approve(address spender, uint256 amount) external returns (bool) { + allowance[msg.sender][spender] = amount; + return true; + } + + function transferFrom(address from, address to, uint256 amount) external returns (bool) { + allowance[from][msg.sender] -= amount; + balanceOf[from] -= amount; + balanceOf[to] += amount; + return true; + } + + function mint(address to, uint256 amount) external { + totalSupply += amount; + balanceOf[to] += amount; + } +} diff --git a/tests/UniswapV2/foundry/src/SimplePair.sol b/tests/UniswapV2/foundry/src/SimplePair.sol new file mode 100644 index 0000000..88f06f2 --- /dev/null +++ b/tests/UniswapV2/foundry/src/SimplePair.sol @@ -0,0 +1,153 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "./MockERC20.sol"; + +contract SimplePair { + string public name = "Uniswap V2"; + string public symbol = "UNI-V2"; + uint8 public decimals = 18; + uint256 public totalSupply; + mapping(address => uint256) public balanceOf; + + uint256 public constant MINIMUM_LIQUIDITY = 1000; + + address public token0; + address public token1; + + uint112 private reserve0; + uint112 private reserve1; + uint32 private blockTimestampLast; + + uint256 public price0CumulativeLast; + uint256 public price1CumulativeLast; + uint256 public kLast; + + event Mint(address indexed sender, uint256 amount0, uint256 amount1); + event Burn(address indexed sender, uint256 amount0, uint256 amount1, address indexed to); + event Swap(address indexed sender, uint256 amount0In, uint256 amount1In, uint256 amount0Out, uint256 amount1Out, address indexed to); + event Sync(uint112 reserve0, uint112 reserve1); + + constructor(address _token0, address _token1) { + token0 = _token0; + token1 = _token1; + } + + function getReserves() public view returns (uint112 _reserve0, uint112 _reserve1, uint32 _blockTimestampLast) { + _reserve0 = reserve0; + _reserve1 = reserve1; + _blockTimestampLast = blockTimestampLast; + } + + function _mint(address to, uint256 value) private { + totalSupply += value; + balanceOf[to] += value; + } + + function _burn(address from, uint256 value) private { + balanceOf[from] -= value; + totalSupply -= value; + } + + function _update(uint256 balance0, uint256 balance1) private { + require(balance0 <= type(uint112).max && balance1 <= type(uint112).max, 'OVERFLOW'); + reserve0 = uint112(balance0); + reserve1 = uint112(balance1); + blockTimestampLast = uint32(block.timestamp); + emit Sync(reserve0, reserve1); + } + + function mint(address to) external returns (uint256 liquidity) { + (uint112 _reserve0, uint112 _reserve1,) = getReserves(); + uint256 balance0 = MockERC20(token0).balanceOf(address(this)); + uint256 balance1 = MockERC20(token1).balanceOf(address(this)); + uint256 amount0 = balance0 - _reserve0; + uint256 amount1 = balance1 - _reserve1; + + uint256 _totalSupply = totalSupply; + if (_totalSupply == 0) { + liquidity = sqrt(amount0 * amount1) - MINIMUM_LIQUIDITY; + _mint(address(0), MINIMUM_LIQUIDITY); + } else { + liquidity = min((amount0 * _totalSupply) / _reserve0, (amount1 * _totalSupply) / _reserve1); + } + require(liquidity > 0, 'INSUFFICIENT_LIQUIDITY_MINTED'); + _mint(to, liquidity); + + _update(balance0, balance1); + emit Mint(msg.sender, amount0, amount1); + } + + function burn(address to) external returns (uint256 amount0, uint256 amount1) { + (uint112 _reserve0, uint112 _reserve1,) = getReserves(); + address _token0 = token0; + address _token1 = token1; + uint256 balance0 = MockERC20(_token0).balanceOf(address(this)); + uint256 balance1 = MockERC20(_token1).balanceOf(address(this)); + uint256 liquidity = balanceOf[address(this)]; + + uint256 _totalSupply = totalSupply; + amount0 = (liquidity * balance0) / _totalSupply; + amount1 = (liquidity * balance1) / _totalSupply; + require(amount0 > 0 && amount1 > 0, 'INSUFFICIENT_LIQUIDITY_BURNED'); + _burn(address(this), liquidity); + MockERC20(_token0).transfer(to, amount0); + MockERC20(_token1).transfer(to, amount1); + balance0 = MockERC20(_token0).balanceOf(address(this)); + balance1 = MockERC20(_token1).balanceOf(address(this)); + + _update(balance0, balance1); + emit Burn(msg.sender, amount0, amount1, to); + } + + function swap(uint256 amount0Out, uint256 amount1Out, address to, bytes calldata) external { + require(amount0Out > 0 || amount1Out > 0, 'INSUFFICIENT_OUTPUT_AMOUNT'); + (uint112 _reserve0, uint112 _reserve1,) = getReserves(); + require(amount0Out < _reserve0 && amount1Out < _reserve1, 'INSUFFICIENT_LIQUIDITY'); + + if (amount0Out > 0) MockERC20(token0).transfer(to, amount0Out); + if (amount1Out > 0) MockERC20(token1).transfer(to, amount1Out); + + uint256 balance0 = MockERC20(token0).balanceOf(address(this)); + uint256 balance1 = MockERC20(token1).balanceOf(address(this)); + + uint256 amount0In = balance0 > _reserve0 - amount0Out ? balance0 - (_reserve0 - amount0Out) : 0; + uint256 amount1In = balance1 > _reserve1 - amount1Out ? balance1 - (_reserve1 - amount1Out) : 0; + require(amount0In > 0 || amount1In > 0, 'INSUFFICIENT_INPUT_AMOUNT'); + + uint256 balance0Adjusted = (balance0 * 1000) - (amount0In * 3); + uint256 balance1Adjusted = (balance1 * 1000) - (amount1In * 3); + require(balance0Adjusted * balance1Adjusted >= uint256(_reserve0) * uint256(_reserve1) * (1000**2), 'K'); + + _update(balance0, balance1); + emit Swap(msg.sender, amount0In, amount1In, amount0Out, amount1Out, to); + } + + function skim(address to) external { + address _token0 = token0; + address _token1 = token1; + MockERC20(_token0).transfer(to, MockERC20(_token0).balanceOf(address(this)) - reserve0); + MockERC20(_token1).transfer(to, MockERC20(_token1).balanceOf(address(this)) - reserve1); + } + + function sync() external { + _update(MockERC20(token0).balanceOf(address(this)), MockERC20(token1).balanceOf(address(this))); + } + + function sqrt(uint256 y) internal pure returns (uint256 z) { + if (y > 3) { + z = y; + uint256 x = y / 2 + 1; + while (x < z) { + z = x; + x = (y / x + x) / 2; + } + } else if (y != 0) { + z = 1; + } + } + + function min(uint256 x, uint256 y) internal pure returns (uint256 z) { + z = x < y ? x : y; + } +} diff --git a/tests/UniswapV2/foundry/test/CryticUniswapV2Test.sol b/tests/UniswapV2/foundry/test/CryticUniswapV2Test.sol new file mode 100644 index 0000000..5ccb35b --- /dev/null +++ b/tests/UniswapV2/foundry/test/CryticUniswapV2Test.sol @@ -0,0 +1,44 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "properties/UniswapV2/internal/properties/UniswapV2BasicProperties.sol"; +import "properties/UniswapV2/internal/properties/UniswapV2RemoveLiquidityProperties.sol"; +import "properties/UniswapV2/internal/properties/UniswapV2SwapProperties.sol"; +import "properties/UniswapV2/internal/properties/UniswapV2InvariantProperties.sol"; +import "../src/SimplePair.sol"; +import "../src/MockERC20.sol"; + +contract CryticUniswapV2InternalHarness is + SimplePair, + CryticUniswapV2BasicProperties, + CryticUniswapV2RemoveLiquidityProperties, + CryticUniswapV2SwapProperties, + CryticUniswapV2InvariantProperties +{ + MockERC20 public tokenA; + MockERC20 public tokenB; + + constructor() SimplePair(address(0), address(0)) { + // Deploy mock tokens + tokenA = new MockERC20("Token A", "TKA"); + tokenB = new MockERC20("Token B", "TKB"); + + // Set token addresses + token0 = address(tokenA); + token1 = address(tokenB); + + // Mint initial tokens to test users + tokenA.mint(USER1, INITIAL_BALANCE); + tokenA.mint(USER2, INITIAL_BALANCE); + tokenA.mint(USER3, INITIAL_BALANCE); + + tokenB.mint(USER1, INITIAL_BALANCE); + tokenB.mint(USER2, INITIAL_BALANCE); + tokenB.mint(USER3, INITIAL_BALANCE); + + // Initialize the pair with some liquidity + tokenA.mint(address(this), 10000e18); + tokenB.mint(address(this), 10000e18); + this.mint(address(this)); + } +} From 12b6570127592cd123c91bc9dd7e3f3967f810f5 Mon Sep 17 00:00:00 2001 From: Omar Inuwa Date: Fri, 28 Nov 2025 08:32:55 +0100 Subject: [PATCH 2/2] Remove MockERC20, use standard IERC20 interface - Removed custom MockERC20.sol (not following repo patterns) - Updated SimplePair to use minimal IERC20 interface - Moved TestToken into test harness (matches ERC20/ERC4626 test patterns) - SimplePair now works with any ERC20-compatible token --- tests/UniswapV2/foundry/src/MockERC20.sol | 39 --------------- tests/UniswapV2/foundry/src/SimplePair.sol | 35 +++++++------- .../foundry/test/CryticUniswapV2Test.sol | 48 ++++++++++++++++--- 3 files changed, 61 insertions(+), 61 deletions(-) delete mode 100644 tests/UniswapV2/foundry/src/MockERC20.sol diff --git a/tests/UniswapV2/foundry/src/MockERC20.sol b/tests/UniswapV2/foundry/src/MockERC20.sol deleted file mode 100644 index de23369..0000000 --- a/tests/UniswapV2/foundry/src/MockERC20.sol +++ /dev/null @@ -1,39 +0,0 @@ -// SPDX-License-Identifier: AGPL-3.0-or-later -pragma solidity ^0.8.0; - -contract MockERC20 { - string public name; - string public symbol; - uint8 public decimals = 18; - uint256 public totalSupply; - mapping(address => uint256) public balanceOf; - mapping(address => mapping(address => uint256)) public allowance; - - constructor(string memory _name, string memory _symbol) { - name = _name; - symbol = _symbol; - } - - function transfer(address to, uint256 amount) external returns (bool) { - balanceOf[msg.sender] -= amount; - balanceOf[to] += amount; - return true; - } - - function approve(address spender, uint256 amount) external returns (bool) { - allowance[msg.sender][spender] = amount; - return true; - } - - function transferFrom(address from, address to, uint256 amount) external returns (bool) { - allowance[from][msg.sender] -= amount; - balanceOf[from] -= amount; - balanceOf[to] += amount; - return true; - } - - function mint(address to, uint256 amount) external { - totalSupply += amount; - balanceOf[to] += amount; - } -} diff --git a/tests/UniswapV2/foundry/src/SimplePair.sol b/tests/UniswapV2/foundry/src/SimplePair.sol index 88f06f2..bf2defc 100644 --- a/tests/UniswapV2/foundry/src/SimplePair.sol +++ b/tests/UniswapV2/foundry/src/SimplePair.sol @@ -1,7 +1,10 @@ // SPDX-License-Identifier: AGPL-3.0-or-later pragma solidity ^0.8.0; -import "./MockERC20.sol"; +interface IERC20 { + function balanceOf(address account) external view returns (uint256); + function transfer(address to, uint256 amount) external returns (bool); +} contract SimplePair { string public name = "Uniswap V2"; @@ -59,8 +62,8 @@ contract SimplePair { function mint(address to) external returns (uint256 liquidity) { (uint112 _reserve0, uint112 _reserve1,) = getReserves(); - uint256 balance0 = MockERC20(token0).balanceOf(address(this)); - uint256 balance1 = MockERC20(token1).balanceOf(address(this)); + uint256 balance0 = IERC20(token0).balanceOf(address(this)); + uint256 balance1 = IERC20(token1).balanceOf(address(this)); uint256 amount0 = balance0 - _reserve0; uint256 amount1 = balance1 - _reserve1; @@ -82,8 +85,8 @@ contract SimplePair { (uint112 _reserve0, uint112 _reserve1,) = getReserves(); address _token0 = token0; address _token1 = token1; - uint256 balance0 = MockERC20(_token0).balanceOf(address(this)); - uint256 balance1 = MockERC20(_token1).balanceOf(address(this)); + uint256 balance0 = IERC20(_token0).balanceOf(address(this)); + uint256 balance1 = IERC20(_token1).balanceOf(address(this)); uint256 liquidity = balanceOf[address(this)]; uint256 _totalSupply = totalSupply; @@ -91,10 +94,10 @@ contract SimplePair { amount1 = (liquidity * balance1) / _totalSupply; require(amount0 > 0 && amount1 > 0, 'INSUFFICIENT_LIQUIDITY_BURNED'); _burn(address(this), liquidity); - MockERC20(_token0).transfer(to, amount0); - MockERC20(_token1).transfer(to, amount1); - balance0 = MockERC20(_token0).balanceOf(address(this)); - balance1 = MockERC20(_token1).balanceOf(address(this)); + IERC20(_token0).transfer(to, amount0); + IERC20(_token1).transfer(to, amount1); + balance0 = IERC20(_token0).balanceOf(address(this)); + balance1 = IERC20(_token1).balanceOf(address(this)); _update(balance0, balance1); emit Burn(msg.sender, amount0, amount1, to); @@ -105,11 +108,11 @@ contract SimplePair { (uint112 _reserve0, uint112 _reserve1,) = getReserves(); require(amount0Out < _reserve0 && amount1Out < _reserve1, 'INSUFFICIENT_LIQUIDITY'); - if (amount0Out > 0) MockERC20(token0).transfer(to, amount0Out); - if (amount1Out > 0) MockERC20(token1).transfer(to, amount1Out); + if (amount0Out > 0) IERC20(token0).transfer(to, amount0Out); + if (amount1Out > 0) IERC20(token1).transfer(to, amount1Out); - uint256 balance0 = MockERC20(token0).balanceOf(address(this)); - uint256 balance1 = MockERC20(token1).balanceOf(address(this)); + uint256 balance0 = IERC20(token0).balanceOf(address(this)); + uint256 balance1 = IERC20(token1).balanceOf(address(this)); uint256 amount0In = balance0 > _reserve0 - amount0Out ? balance0 - (_reserve0 - amount0Out) : 0; uint256 amount1In = balance1 > _reserve1 - amount1Out ? balance1 - (_reserve1 - amount1Out) : 0; @@ -126,12 +129,12 @@ contract SimplePair { function skim(address to) external { address _token0 = token0; address _token1 = token1; - MockERC20(_token0).transfer(to, MockERC20(_token0).balanceOf(address(this)) - reserve0); - MockERC20(_token1).transfer(to, MockERC20(_token1).balanceOf(address(this)) - reserve1); + IERC20(_token0).transfer(to, IERC20(_token0).balanceOf(address(this)) - reserve0); + IERC20(_token1).transfer(to, IERC20(_token1).balanceOf(address(this)) - reserve1); } function sync() external { - _update(MockERC20(token0).balanceOf(address(this)), MockERC20(token1).balanceOf(address(this))); + _update(IERC20(token0).balanceOf(address(this)), IERC20(token1).balanceOf(address(this))); } function sqrt(uint256 y) internal pure returns (uint256 z) { diff --git a/tests/UniswapV2/foundry/test/CryticUniswapV2Test.sol b/tests/UniswapV2/foundry/test/CryticUniswapV2Test.sol index 5ccb35b..cb3580c 100644 --- a/tests/UniswapV2/foundry/test/CryticUniswapV2Test.sol +++ b/tests/UniswapV2/foundry/test/CryticUniswapV2Test.sol @@ -6,7 +6,43 @@ import "properties/UniswapV2/internal/properties/UniswapV2RemoveLiquidityPropert import "properties/UniswapV2/internal/properties/UniswapV2SwapProperties.sol"; import "properties/UniswapV2/internal/properties/UniswapV2InvariantProperties.sol"; import "../src/SimplePair.sol"; -import "../src/MockERC20.sol"; + +contract TestToken { + string public name; + string public symbol; + uint8 public decimals = 18; + uint256 public totalSupply; + mapping(address => uint256) public balanceOf; + mapping(address => mapping(address => uint256)) public allowance; + + constructor(string memory _name, string memory _symbol) { + name = _name; + symbol = _symbol; + } + + function transfer(address to, uint256 amount) external returns (bool) { + balanceOf[msg.sender] -= amount; + balanceOf[to] += amount; + return true; + } + + function approve(address spender, uint256 amount) external returns (bool) { + allowance[msg.sender][spender] = amount; + return true; + } + + function transferFrom(address from, address to, uint256 amount) external returns (bool) { + allowance[from][msg.sender] -= amount; + balanceOf[from] -= amount; + balanceOf[to] += amount; + return true; + } + + function mint(address to, uint256 amount) external { + totalSupply += amount; + balanceOf[to] += amount; + } +} contract CryticUniswapV2InternalHarness is SimplePair, @@ -15,13 +51,13 @@ contract CryticUniswapV2InternalHarness is CryticUniswapV2SwapProperties, CryticUniswapV2InvariantProperties { - MockERC20 public tokenA; - MockERC20 public tokenB; + TestToken public tokenA; + TestToken public tokenB; constructor() SimplePair(address(0), address(0)) { - // Deploy mock tokens - tokenA = new MockERC20("Token A", "TKA"); - tokenB = new MockERC20("Token B", "TKB"); + // Deploy test tokens + tokenA = new TestToken("Token A", "TKA"); + tokenB = new TestToken("Token B", "TKB"); // Set token addresses token0 = address(tokenA);