diff --git a/CLAUDE.md b/CLAUDE.md index 62dc1e8..f16ae64 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 181+ 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) +- Concentrated Liquidity AMMs (13+ 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 + - `ConcentratedLiquidity/` - Uniswap V3 style AMM properties (tick math, liquidity accounting, swaps) - `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/ConcentratedLiquidity/README.md b/contracts/ConcentratedLiquidity/README.md new file mode 100644 index 0000000..7c65247 --- /dev/null +++ b/contracts/ConcentratedLiquidity/README.md @@ -0,0 +1,323 @@ +# Concentrated Liquidity Properties + +This directory contains property tests for concentrated liquidity AMM protocols (Uniswap V3 style) that can be used with [Echidna](https://github.com/crytic/echidna) or [Medusa](https://github.com/crytic/medusa) for fuzzing. + +## Overview + +Concentrated liquidity AMMs allow liquidity providers to concentrate their capital within specific price ranges, enabling greater capital efficiency compared to traditional constant product AMMs (Uniswap V2 style). This mechanism uses tick-based accounting where: + +- **Ticks** represent discrete price points: `tick = log₁.₀₀₀₁(price)` +- **Positions** are bounded by a lower and upper tick `[tickLower, tickUpper]` +- **Active liquidity** only includes positions whose range contains the current price +- **LiquidityNet** tracks the delta change when crossing each tick boundary + +## Architecture + +### Testing Modes + +#### Internal Testing +Test contracts inherit from both the pool implementation and property contracts. Properties access internal state directly. Best for: +- White-box testing of pool implementations +- Testing custom pool variants +- Accessing internal variables and state + +#### External Testing +Test harnesses interact with pools through their external interface. Requires `allContracts: true` in Echidna config. Best for: +- Black-box testing of deployed contracts +- Testing third-party pools +- Integration testing + +### Directory Structure + +``` +ConcentratedLiquidity/ +├── util/ +│ ├── IConcentratedLiquidityPool.sol # Minimal pool interface +│ └── TickMath.sol # Tick <-> Price conversion library +├── internal/ +│ ├── util/ +│ │ └── ConcentratedLiquidityTestBase.sol # Base contract with tick tracking +│ └── properties/ +│ ├── TickMathProperties.sol # Tick-price synchronization (Props 1-3) +│ ├── LiquidityProperties.sol # Conservation laws (Props 4-5) +│ ├── MintBurnProperties.sol # Position management (Props 6-9) +│ └── SwapProperties.sol # Swap execution (Props 10-13) +└── external/ + └── (To be implemented) +``` + +## Properties + +### Tick Math Properties (3 properties) + +These properties ensure correct synchronization between ticks and prices, including protection against the **KyberSwap vulnerability** ($50M exploit). + +| ID | Name | Invariant | +|---|---|---| +| CL-TICK-001 | [test_CL_tickDirectionMatchesPriceDirection](internal/properties/TickMathProperties.sol#L58) | Tick must change in the same direction as price (monotonicity) | +| CL-TICK-002 | [test_CL_noPriceOvershootWhenMovingUp](internal/properties/TickMathProperties.sol#L126) | Price must never overshoot tick boundary upward (KyberSwap fix) | +| CL-TICK-002 | [test_CL_noPriceOvershootWhenMovingDown](internal/properties/TickMathProperties.sol#L157) | Price must never overshoot tick boundary downward (KyberSwap fix) | +| CL-TICK-003 | [test_CL_currentTickRespectsSpacing](internal/properties/TickMathProperties.sol#L189) | Current tick must be aligned with tickSpacing | +| CL-TICK-003 | [test_CL_initializedTicksRespectSpacing](internal/properties/TickMathProperties.sol#L208) | All initialized ticks must respect tickSpacing | + +**Why Property CL-TICK-002 Matters:** + +The KyberSwap Elastic hack (November 2023) exploited a critical flaw where price was allowed to **overshoot** the next tick boundary. The vulnerable code used: + +```solidity +if (sqrtPrice != sqrtPriceAtNextTick) { + // continue using current liquidity +} +``` + +This allowed `sqrtPrice > sqrtPriceAtNextTick` to occur, causing liquidity to be **double-counted** because the tick was never crossed and liquidityNet was never applied. The fix uses **directional comparison**: + +```solidity +// When moving up: price must be ≤ next tick (not !=) +if (sqrtPrice <= sqrtPriceAtNextTick) { + // cross the tick and update liquidity +} +``` + +### Liquidity Conservation Properties (3 properties) + +These properties verify the fundamental conservation laws of liquidity accounting. + +| ID | Name | Invariant | +|---|---|---| +| CL-LIQUIDITY-001 | [test_CL_liquidityNetSumsToZero](internal/properties/LiquidityProperties.sol#L57) | Sum of liquidityNet across all ticks must equal zero | +| CL-LIQUIDITY-002 | [test_CL_currentLiquidityMatchesSumOfDeltas](internal/properties/LiquidityProperties.sol#L137) | Current liquidity must equal sum of liquidityNet ≤ currentTick | +| CL-LIQUIDITY-003 | [test_CL_liquidityNeverNegative](internal/properties/LiquidityProperties.sol#L178) | Liquidity values cannot be negative | + +**Why CL-LIQUIDITY-001 Must Be True:** + +Every position adds `+L` at `tickLower` and `-L` at `tickUpper`. Therefore: + +``` +Σ(liquidityNet[tick]) = Σ(+L_i - L_i) = 0 +``` + +This is a **conservation law** - liquidity cannot be created or destroyed. Violations indicate: +- Mint/burn only updating one boundary +- Arithmetic errors in updates +- Positions not cleaning up properly + +**Why CL-LIQUIDITY-002 Must Be True:** + +Active liquidity is calculated by summing all deltas from negative infinity up to the current tick: + +``` +pool.liquidity() = Σ(liquidityNet[t] for all t ≤ currentTick) +``` + +This determines which positions are "in range" and contribute to trading liquidity. + +### Mint/Burn Properties (4 properties) + +These properties verify position creation and removal mechanics. + +| ID | Name | Invariant | +|---|---|---| +| CL-MINT-001 | [test_CL_mintIncreasesCurrentLiquidityWhenInRange](internal/properties/MintBurnProperties.sol#L61) | Minting in-range increases pool.liquidity(), out-of-range doesn't | +| CL-MINT-002 | [test_CL_mintIncreasesLiquidityGross](internal/properties/MintBurnProperties.sol#L127) | Minting always increases liquidityGross at both ticks | +| CL-MINT-003 | [test_CL_mintUpdatesLiquidityNetAsymmetrically](internal/properties/MintBurnProperties.sol#L233) | Minting adds +L at tickLower, -L at tickUpper (asymmetric) | +| CL-BURN-001 | [test_CL_burnReversesMint](internal/properties/MintBurnProperties.sol#L302) | Burn must exactly reverse mint's state changes | + +**Why CL-MINT-003 is Critical:** + +The **asymmetric update pattern** is the foundation of concentrated liquidity: + +```solidity +// When minting position [tickLower, tickUpper] with liquidity L: +liquidityNet[tickLower] += L // Activate when crossing up +liquidityNet[tickUpper] -= L // Deactivate when crossing up +``` + +This creates a "wave" where: +- Price crossing **up through tickLower**: Add L to active liquidity +- Price crossing **up through tickUpper**: Remove L from active liquidity +- Price between the ticks: Position contributes L to pool + +Using symmetric updates (same sign) would cause positions to never deactivate or incorrectly accumulate liquidity. + +### Swap Properties (4 properties) + +These properties verify correct swap execution and price updates. + +| ID | Name | Invariant | +|---|---|---| +| CL-SWAP-001 | [test_CL_swapMoviesPriceInCorrectDirection](internal/properties/SwapProperties.sol#L79) | Selling token0 decreases price, selling token1 increases price | +| CL-SWAP-002 | [test_CL_swapRespectsLimitPrice](internal/properties/SwapProperties.sol#L145) | Swap must stop at or before sqrtPriceLimitX96 | +| CL-SWAP-003 | [test_CL_swapUpdatesLiquidityWhenCrossingTicks](internal/properties/SwapProperties.sol#L202) | Liquidity must be updated when crossing tick boundaries | +| CL-SWAP-004 | [test_CL_swapPriceStaysWithinBounds](internal/properties/SwapProperties.sol#L255) | Price must stay within [MIN_SQRT_RATIO, MAX_SQRT_RATIO] | + +**Why CL-SWAP-003 is Critical:** + +When a swap crosses a tick boundary, the active liquidity MUST be updated: + +```solidity +// When crossing tick T going up: +liquidity += liquidityNet[T] + +// When crossing tick T going down: +liquidity -= liquidityNet[T] +``` + +Failure to update liquidity leads to: +- Using wrong liquidity for price calculations +- Positions not being activated/deactivated +- **KyberSwap-style vulnerabilities** where liquidity is double-counted + +## Usage + +### Basic Implementation + +```solidity +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity ^0.8.0; + +import "./ConcentratedLiquidity/internal/properties/TickMathProperties.sol"; +import "./ConcentratedLiquidity/internal/properties/LiquidityProperties.sol"; +import "./ConcentratedLiquidity/internal/properties/MintBurnProperties.sol"; +import "./ConcentratedLiquidity/internal/properties/SwapProperties.sol"; + +contract MyPoolHarness is + CryticTickMathProperties, + CryticLiquidityProperties, + CryticMintBurnProperties, + CryticSwapProperties +{ + MyConcentratedPool pool; + + constructor() { + pool = new MyConcentratedPool( + address(token0), + address(token1), + FEE, + TICK_SPACING + ); + + // Initialize pool with some liquidity + pool.mint(address(this), -1000, 1000, 1000000e18, ""); + } + + // Implement required virtual functions + function _getCurrentTick() internal view override returns (int24) { + (,int24 tick,,,,,) = pool.slot0(); + return tick; + } + + function _getCurrentLiquidity() internal view override returns (uint128) { + return pool.liquidity(); + } + + function _getSqrtPriceX96() internal view override returns (uint160) { + (uint160 sqrtPrice,,,,,,,) = pool.slot0(); + return sqrtPrice; + } + + // ... implement other required functions +} +``` + +### Running with Echidna + +```bash +echidna . --contract MyPoolHarness --config echidna-config.yaml +``` + +**echidna-config.yaml:** +```yaml +testMode: assertion +deployer: "0x10000" +workers: 10 +testLimit: 100000 +``` + +### Running with Medusa + +```bash +forge build --build-info +medusa fuzz --target-contracts MyPoolHarness +``` + +## Real-World Vulnerabilities Caught + +### 1. KyberSwap Elastic ($50M - November 2023) + +**Vulnerability:** Price overshoot past tick boundary +- **Code:** Used `!=` instead of `<` or `>` for tick boundary check +- **Impact:** Liquidity double-counted when price exceeded next tick +- **Properties:** CL-TICK-002, CL-SWAP-003 + +**Vulnerable Code:** +```solidity +if (state.sqrtP != nextSqrtP) { + // BUG: This is true when sqrtP > nextSqrtP + // Should use: if (state.sqrtP < nextSqrtP) + state.baseL = willUpTick ? baseL + nextLiquidity : baseL - nextLiquidity; +} +``` + +The fuzzer would find a sequence like: +1. Create position [tick 100, tick 200] with large liquidity +2. Swap that pushes price slightly ABOVE tick 200 +3. Liquidity is still counted as active (never crossed tick) +4. Swap back down using double liquidity +5. Profit from the asymmetric price impact + +### 2. Liquidity Conservation Violations + +**Vulnerability:** Mint/burn asymmetry +- **Scenario:** Mint updates both boundaries, burn only updates one +- **Impact:** liquidityNet stops summing to zero, liquidity leak +- **Properties:** CL-LIQUIDITY-001, CL-BURN-001 + +### 3. Tick Spacing Violations + +**Vulnerability:** Accepting non-aligned ticks +- **Scenario:** Position created at tick 123 with tickSpacing=10 +- **Impact:** Orphaned liquidity that can never be crossed +- **Properties:** CL-TICK-003 + +## Integration with Existing Properties + +Concentrated liquidity pools typically use ERC20 tokens. You can combine these properties with ERC20 properties: + +```solidity +import "../ERC20/internal/properties/ERC20BasicProperties.sol"; +import "./ConcentratedLiquidity/internal/properties/TickMathProperties.sol"; + +contract CombinedTest is + CryticERC20BasicProperties, + CryticTickMathProperties +{ + // Test both token accounting AND pool mechanics +} +``` + +## Resources + +- **Uniswap V3 Whitepaper**: https://uniswap.org/whitepaper-v3.pdf +- **KyberSwap Exploit Analysis**: https://twitter.com/Certora/status/1728051144695349395 +- **Uniswap V3 Core Repository**: https://github.com/Uniswap/v3-core +- **Trail of Bits Echidna**: https://github.com/crytic/echidna +- **Trail of Bits Medusa**: https://github.com/crytic/medusa + +## Contributing + +To add new properties: + +1. Add the property to the appropriate file in `internal/properties/` +2. Follow the established naming convention: `CL--` +3. Include comprehensive NatSpec documentation with: + - WHY THIS MUST BE TRUE section + - MATHEMATICAL PROOF or example + - WHAT BUG THIS CATCHES section +4. Add property to this README with description and invariant +5. Add external testing variant if applicable +6. Create test case that demonstrates a violation + +## License + +AGPL-3.0-or-later diff --git a/contracts/ConcentratedLiquidity/internal/properties/LiquidityProperties.sol b/contracts/ConcentratedLiquidity/internal/properties/LiquidityProperties.sol new file mode 100644 index 0000000..76f3178 --- /dev/null +++ b/contracts/ConcentratedLiquidity/internal/properties/LiquidityProperties.sol @@ -0,0 +1,239 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +import "../util/ConcentratedLiquidityTestBase.sol"; + +/** + * @title Concentrated Liquidity Conservation Properties + * @author Crytic (Trail of Bits) + * @notice Properties for liquidity accounting and conservation laws + * @dev Testing Mode: INTERNAL + * + * WHY THESE PROPERTIES MATTER: + * Liquidity accounting in concentrated liquidity AMMs uses a delta-based system where + * each position adds +L at its lower tick and -L at its upper tick. This creates a + * mathematical invariant: the sum of all deltas must equal zero. + * + * The current "active" liquidity is calculated by summing all liquidityNet values from + * negative infinity up to the current tick. This is the liquidity actually available + * for trading at the current price. + * + * Violations of these properties can lead to: + * - Incorrect pricing during swaps + * - Liquidity appearing or disappearing (breaking conservation) + * - Positions being counted when they shouldn't be (or vice versa) + */ +abstract contract CryticLiquidityProperties is ConcentratedLiquidityTestBase { + + ////////////////////////////////////////////////////////////////////// + // PROPERTY 4: LiquidityNet Conservation (Sum to Zero) + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Test that liquidityNet sums to zero across all ticks + * @dev Property ID: CL-LIQUIDITY-001 + * @custom:property-id CL-LIQUIDITY-001 + * + * WHY THIS MUST BE TRUE: + * Every liquidity position in a concentrated liquidity pool consists of a range + * [tickLower, tickUpper]. When a position is created with liquidity L: + * - We add +L to liquidityNet[tickLower] + * - We subtract -L from liquidityNet[tickUpper] + * + * MATHEMATICAL PROOF: + * For each position i with liquidity L_i: + * liquidityNet[tickLower_i] += L_i + * liquidityNet[tickUpper_i] -= L_i + * + * Summing across all ticks: + * Σ(liquidityNet[t]) = Σ(+L_i - L_i) = 0 + * + * This is a conservation law: liquidity cannot be created or destroyed, only + * redistributed across ticks. + * + * EXAMPLE: + * Position 1: [tick 100, tick 200], L=1000 + * liquidityNet[100] = +1000 + * liquidityNet[200] = -1000 + * Sum = 0 ✓ + * + * Position 2: [tick 150, tick 300], L=500 + * liquidityNet[150] += +500 + * liquidityNet[300] = -500 + * Total sum = +1000 +500 -1000 -500 = 0 ✓ + * + * WHAT BUG THIS CATCHES: + * - Incorrect mint/burn that only updates one boundary + * - Arithmetic errors in liquidityNet updates + * - Re-entrancy attacks that manipulate liquidity + * - Positions that don't properly clean up on burn + */ + function test_CL_liquidityNetSumsToZero() public virtual { + int256 netSum = 0; + + // Sum liquidityNet across all initialized ticks + for (uint256 i = 0; i < usedTicks.length; i++) { + int24 tick = usedTicks[i]; + int128 liquidityNet = _getLiquidityNetAtTick(tick); + netSum += int256(liquidityNet); + } + + assertEq( + netSum, + 0, + "CL-LIQUIDITY-001: LiquidityNet does not sum to zero (conservation violated)" + ); + } + + ////////////////////////////////////////////////////////////////////// + // PROPERTY 5: Current Liquidity Equals Sum of LiquidityNet ≤ CurrentTick + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Test that current liquidity equals the sum of liquidityNet for all ticks ≤ currentTick + * @dev Property ID: CL-LIQUIDITY-002 + * @custom:property-id CL-LIQUIDITY-002 + * + * WHY THIS MUST BE TRUE: + * The "active" liquidity at any price point is determined by which positions contain + * that price in their range. Due to the delta-based accounting system: + * - Starting from the leftmost tick (price = 0) + * - As we move right and cross each tick boundary, we add its liquidityNet + * - The cumulative sum at any tick T is the liquidity active at that price + * + * MATHEMATICAL PROOF: + * Let currentTick = t_c + * Active positions are those where tickLower ≤ t_c < tickUpper + * + * For each position i: + * - If tickLower_i ≤ t_c, we've crossed the +L_i delta + * - If tickUpper_i ≤ t_c, we've crossed the -L_i delta + * - If tickLower_i ≤ t_c < tickUpper_i, the position contributes +L_i + * + * Therefore: + * pool.liquidity() = Σ(liquidityNet[t] for all t ≤ t_c) + * + * EXAMPLE: + * Position 1: [100, 200], L=1000 + * Position 2: [150, 300], L=500 + * + * At tick 175: + * - Crossed tick 100: +1000 + * - Crossed tick 150: +500 + * - Not crossed tick 200, 300 + * - Active liquidity = 1000 + 500 = 1500 ✓ + * + * At tick 250: + * - Crossed tick 100: +1000 + * - Crossed tick 150: +500 + * - Crossed tick 200: -1000 + * - Not crossed tick 300 + * - Active liquidity = 1000 + 500 - 1000 = 500 ✓ + * + * WHAT BUG THIS CATCHES: + * - Incorrect tick crossing logic + * - Liquidity not updated when crossing ticks during swaps + * - Off-by-one errors in tick comparison (≤ vs <) + * - Manual liquidity manipulation without updating ticks + */ + function test_CL_currentLiquidityMatchesSumOfDeltas() public virtual { + int24 currentTick = _getCurrentTick(); + uint128 reportedLiquidity = _getCurrentLiquidity(); + + // Calculate expected liquidity by summing liquidityNet for all ticks ≤ currentTick + int256 calculatedLiquidity = 0; + + for (uint256 i = 0; i < usedTicks.length; i++) { + int24 tick = usedTicks[i]; + + // Only include ticks that have been crossed (≤ currentTick) + if (tick <= currentTick) { + int128 liquidityNet = _getLiquidityNetAtTick(tick); + calculatedLiquidity += int256(liquidityNet); + } + } + + // Liquidity cannot be negative + assertWithMsg( + calculatedLiquidity >= 0, + "CL-LIQUIDITY-002: Calculated liquidity is negative (impossible state)" + ); + + assertEq( + uint256(uint128(reportedLiquidity)), + uint256(uint128(int128(calculatedLiquidity))), + "CL-LIQUIDITY-002: Current liquidity does not match sum of liquidityNet deltas" + ); + } + + /** + * @notice Test that liquidity is never negative + * @dev Property ID: CL-LIQUIDITY-003 + * @custom:property-id CL-LIQUIDITY-003 + * + * WHY THIS MUST BE TRUE: + * Liquidity represents the amount of assets available for trading. By definition, + * it cannot be negative. A negative liquidity value would indicate a severe + * accounting error. + * + * WHAT BUG THIS CATCHES: + * - Underflow in liquidity calculations + * - Burning more liquidity than exists + * - Integer overflow wrapping to negative + */ + function test_CL_liquidityNeverNegative() public virtual { + uint128 currentLiquidity = _getCurrentLiquidity(); + + // uint128 is unsigned, but we check that cast to int256 is positive + // to catch any overflow/underflow issues + assertWithMsg( + int256(uint256(currentLiquidity)) >= 0, + "CL-LIQUIDITY-003: Current liquidity is negative" + ); + + // Also check all tick liquidityGross values + for (uint256 i = 0; i < usedTicks.length; i++) { + int24 tick = usedTicks[i]; + uint128 liquidityGross = _getLiquidityGrossAtTick(tick); + + assertWithMsg( + int256(uint256(liquidityGross)) >= 0, + "CL-LIQUIDITY-003: Tick liquidityGross is negative" + ); + } + } + + ////////////////////////////////////////////////////////////////////// + // HELPER FUNCTIONS (to be overridden by inheriting contract) + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Get the current tick from the pool + * @dev Must be implemented by inheriting contract + * @return Current tick from pool.slot0() + */ + function _getCurrentTick() internal view virtual returns (int24); + + /** + * @notice Get the current active liquidity + * @dev Must be implemented by inheriting contract + * @return Current liquidity from pool.liquidity() + */ + function _getCurrentLiquidity() internal view virtual returns (uint128); + + /** + * @notice Get liquidityNet for a specific tick + * @dev Must be implemented by inheriting contract + * @param tick The tick to query + * @return liquidityNet The net liquidity change at this tick + */ + function _getLiquidityNetAtTick(int24 tick) internal view virtual returns (int128); + + /** + * @notice Get liquidityGross for a specific tick + * @dev Must be implemented by inheriting contract + * @param tick The tick to query + * @return liquidityGross The total liquidity referencing this tick + */ + function _getLiquidityGrossAtTick(int24 tick) internal view virtual returns (uint128); +} diff --git a/contracts/ConcentratedLiquidity/internal/properties/MintBurnProperties.sol b/contracts/ConcentratedLiquidity/internal/properties/MintBurnProperties.sol new file mode 100644 index 0000000..9d70ca6 --- /dev/null +++ b/contracts/ConcentratedLiquidity/internal/properties/MintBurnProperties.sol @@ -0,0 +1,442 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +import "../util/ConcentratedLiquidityTestBase.sol"; + +/** + * @title Concentrated Liquidity Mint and Burn Properties + * @author Crytic (Trail of Bits) + * @notice Properties for liquidity position management + * @dev Testing Mode: INTERNAL + * + * WHY THESE PROPERTIES MATTER: + * Mint and burn operations are the core mechanisms for providing and removing liquidity + * in concentrated liquidity AMMs. These operations update three critical data structures: + * 1. liquidityGross[tick] - Total liquidity referencing this tick (for initialization) + * 2. liquidityNet[tick] - Delta applied when crossing this tick + * 3. pool.liquidity() - Currently active liquidity (only if position is in range) + * + * The asymmetric update pattern (+L at lower, -L at upper) is fundamental to how + * concentrated liquidity tracking works. Violations can lead to liquidity being + * counted incorrectly, positions not being properly activated/deactivated, or + * accounting inconsistencies that can be exploited. + */ +abstract contract CryticMintBurnProperties is ConcentratedLiquidityTestBase { + + ////////////////////////////////////////////////////////////////////// + // PROPERTY 6: Mint Increases Current Liquidity When In Range + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Test that minting increases current liquidity if position is in range + * @dev Property ID: CL-MINT-001 + * @custom:property-id CL-MINT-001 + * + * WHY THIS MUST BE TRUE: + * A position is "in range" (active) when: tickLower ≤ currentTick < tickUpper + * Only in-range positions contribute to the liquidity available for swaps. + * + * When minting a position: + * - If in range: pool.liquidity() must increase by the minted amount + * - If out of range: pool.liquidity() should NOT change (position is inactive) + * + * MATHEMATICAL DEFINITION: + * Let L be the amount minted, t_c be the current tick + * If tickLower ≤ t_c < tickUpper: + * pool.liquidity_after = pool.liquidity_before + L + * Else: + * pool.liquidity_after = pool.liquidity_before + * + * EXAMPLE: + * Current tick = 150 + * Mint position [100, 200] with L=1000 + * → 100 ≤ 150 < 200, position is IN RANGE + * → pool.liquidity increases by 1000 ✓ + * + * Mint position [200, 300] with L=500 + * → NOT (200 ≤ 150 < 300), position is OUT OF RANGE + * → pool.liquidity unchanged ✓ + * + * WHAT BUG THIS CATCHES: + * - Position activated when it shouldn't be + * - Incorrect range check (wrong inequality direction) + * - Liquidity updated regardless of tick position + * - Off-by-one errors in tick comparison + */ + function test_CL_mintIncreasesCurrentLiquidityWhenInRange( + int24 tickLower, + int24 tickUpper, + uint128 liquidityDelta + ) public virtual { + // Setup: Constrain to valid values + tickLower = int24(clampBetween(tickLower, MIN_TICK, MAX_TICK - 1)); + tickUpper = int24(clampBetween(tickUpper, tickLower + 1, MAX_TICK)); + liquidityDelta = uint128(clampBetween(liquidityDelta, 1, type(uint64).max)); + + // Ensure ticks respect spacing + int24 tickSpacing = _getTickSpacing(); + tickLower = (tickLower / tickSpacing) * tickSpacing; + tickUpper = (tickUpper / tickSpacing) * tickSpacing; + if (tickLower >= tickUpper) return; + + int24 currentTick = _getCurrentTick(); + uint128 liquidityBefore = _getCurrentLiquidity(); + + // Perform mint + _mintPosition(USER1, tickLower, tickUpper, liquidityDelta); + + uint128 liquidityAfter = _getCurrentLiquidity(); + + // Check if position is in range + bool inRange = (tickLower <= currentTick) && (currentTick < tickUpper); + + if (inRange) { + assertEq( + liquidityAfter, + liquidityBefore + liquidityDelta, + "CL-MINT-001: Minting in-range position did not increase current liquidity" + ); + } else { + assertEq( + liquidityAfter, + liquidityBefore, + "CL-MINT-001: Minting out-of-range position changed current liquidity" + ); + } + } + + ////////////////////////////////////////////////////////////////////// + // PROPERTY 7: Mint Always Increases LiquidityGross + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Test that minting always increases liquidityGross at both ticks + * @dev Property ID: CL-MINT-002 + * @custom:property-id CL-MINT-002 + * + * WHY THIS MUST BE TRUE: + * liquidityGross[tick] represents the total absolute amount of liquidity that + * references this tick as either a lower or upper boundary. It is used to: + * 1. Track whether a tick is initialized (liquidityGross > 0) + * 2. Determine when a tick can be deleted (liquidityGross == 0) + * + * Unlike liquidityNet (which can be positive or negative), liquidityGross only + * increases when adding liquidity and only decreases when removing liquidity. + * + * MATHEMATICAL DEFINITION: + * When minting L at [tickLower, tickUpper]: + * liquidityGross[tickLower] += L + * liquidityGross[tickUpper] += L + * + * Both ticks get the FULL amount added to their gross, regardless of whether + * the liquidityNet is +L or -L. + * + * EXAMPLE: + * Initial state: liquidityGross[100] = 500 + * Mint position [100, 200] with L=1000 + * → liquidityGross[100] = 500 + 1000 = 1500 ✓ + * → liquidityGross[200] = 0 + 1000 = 1000 ✓ + * + * WHAT BUG THIS CATCHES: + * - Tick not initialized when it should be + * - liquidityGross decreasing on mint (impossible) + * - Only one boundary updated + * - Incorrect gross calculation + */ + function test_CL_mintIncreasesLiquidityGross( + int24 tickLower, + int24 tickUpper, + uint128 liquidityDelta + ) public virtual { + // Setup: Constrain to valid values + tickLower = int24(clampBetween(tickLower, MIN_TICK, MAX_TICK - 1)); + tickUpper = int24(clampBetween(tickUpper, tickLower + 1, MAX_TICK)); + liquidityDelta = uint128(clampBetween(liquidityDelta, 1, type(uint64).max)); + + // Ensure ticks respect spacing + int24 tickSpacing = _getTickSpacing(); + tickLower = (tickLower / tickSpacing) * tickSpacing; + tickUpper = (tickUpper / tickSpacing) * tickSpacing; + if (tickLower >= tickUpper) return; + + uint128 grossLowerBefore = _getLiquidityGrossAtTick(tickLower); + uint128 grossUpperBefore = _getLiquidityGrossAtTick(tickUpper); + + // Perform mint + _mintPosition(USER1, tickLower, tickUpper, liquidityDelta); + + uint128 grossLowerAfter = _getLiquidityGrossAtTick(tickLower); + uint128 grossUpperAfter = _getLiquidityGrossAtTick(tickUpper); + + assertEq( + grossLowerAfter, + grossLowerBefore + liquidityDelta, + "CL-MINT-002: Minting did not increase liquidityGross at tickLower" + ); + + assertEq( + grossUpperAfter, + grossUpperBefore + liquidityDelta, + "CL-MINT-002: Minting did not increase liquidityGross at tickUpper" + ); + } + + ////////////////////////////////////////////////////////////////////// + // PROPERTY 8: Mint Updates LiquidityNet Asymmetrically + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Test that minting updates liquidityNet asymmetrically (+L at lower, -L at upper) + * @dev Property ID: CL-MINT-003 + * @custom:property-id CL-MINT-003 + * + * WHY THIS MUST BE TRUE: + * The asymmetric update pattern is the foundation of concentrated liquidity accounting. + * When you provide liquidity in range [tickLower, tickUpper]: + * + * - At tickLower: Add +L to liquidityNet + * → When price crosses UP through this tick, activate the position + * + * - At tickUpper: Add -L to liquidityNet + * → When price crosses UP through this tick, deactivate the position + * + * This creates a "wave" where liquidity is added when entering the range and + * removed when exiting it, as the price moves. + * + * MATHEMATICAL DEFINITION: + * When minting L at [tickLower, tickUpper]: + * liquidityNet[tickLower] += L + * liquidityNet[tickUpper] -= L + * + * The signs MUST be opposite and equal in magnitude. + * + * DETAILED EXAMPLE: + * Mint position [100, 200] with L=1000 + * + * Before: + * liquidityNet[100] = 0 + * liquidityNet[200] = 0 + * + * After: + * liquidityNet[100] = +1000 + * liquidityNet[200] = -1000 + * + * Price sweep simulation: + * - Start at tick 50, liquidity = 0 + * - Cross tick 100 going up: liquidity += 1000 → liquidity = 1000 ✓ + * - Cross tick 200 going up: liquidity -= 1000 → liquidity = 0 ✓ + * + * WHY THE ASYMMETRY EXISTS: + * When price is BELOW the range: position is inactive (all token0) + * When price is IN the range: position is active (mixed token0/token1) + * When price is ABOVE the range: position is inactive (all token1) + * + * WHAT BUG THIS CATCHES: + * - Both ticks updated with same sign (symmetric update - WRONG) + * - Only one tick updated + * - Wrong magnitude (+L at one, -2L at other) + * - Sign flipped (would cause inverse behavior) + */ + function test_CL_mintUpdatesLiquidityNetAsymmetrically( + int24 tickLower, + int24 tickUpper, + uint128 liquidityDelta + ) public virtual { + // Setup: Constrain to valid values + tickLower = int24(clampBetween(tickLower, MIN_TICK, MAX_TICK - 1)); + tickUpper = int24(clampBetween(tickUpper, tickLower + 1, MAX_TICK)); + liquidityDelta = uint128(clampBetween(liquidityDelta, 1, type(uint64).max)); + + // Ensure ticks respect spacing + int24 tickSpacing = _getTickSpacing(); + tickLower = (tickLower / tickSpacing) * tickSpacing; + tickUpper = (tickUpper / tickSpacing) * tickSpacing; + if (tickLower >= tickUpper) return; + + int128 netLowerBefore = _getLiquidityNetAtTick(tickLower); + int128 netUpperBefore = _getLiquidityNetAtTick(tickUpper); + + // Perform mint + _mintPosition(USER1, tickLower, tickUpper, liquidityDelta); + + int128 netLowerAfter = _getLiquidityNetAtTick(tickLower); + int128 netUpperAfter = _getLiquidityNetAtTick(tickUpper); + + // Check asymmetric update + int128 netLowerDelta = netLowerAfter - netLowerBefore; + int128 netUpperDelta = netUpperAfter - netUpperBefore; + + assertEq( + netLowerDelta, + int128(liquidityDelta), + "CL-MINT-003: LiquidityNet at tickLower did not increase by +L" + ); + + assertEq( + netUpperDelta, + -int128(liquidityDelta), + "CL-MINT-003: LiquidityNet at tickUpper did not decrease by -L" + ); + + // Verify asymmetry: the deltas must be equal and opposite + assertEq( + netLowerDelta, + -netUpperDelta, + "CL-MINT-003: LiquidityNet deltas are not equal and opposite (asymmetry violated)" + ); + } + + ////////////////////////////////////////////////////////////////////// + // PROPERTY 9: Burn Reverses Mint + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Test that burning liquidity reverses the effects of minting + * @dev Property ID: CL-BURN-001 + * @custom:property-id CL-BURN-001 + * + * WHY THIS MUST BE TRUE: + * Burning (removing) liquidity must be the exact inverse of minting (adding) liquidity. + * All state changes must be reversed: + * 1. liquidityGross[tickLower] decreases by L + * 2. liquidityGross[tickUpper] decreases by L + * 3. liquidityNet[tickLower] decreases by L + * 4. liquidityNet[tickUpper] increases by L (removing -L) + * 5. pool.liquidity() decreases by L (only if position is in range) + * + * MATHEMATICAL DEFINITION: + * If mint(L) followed by burn(L) on the same position: + * Final state = Initial state + * + * EXAMPLE: + * Initial: liquidityGross[100] = 1000, liquidityNet[100] = +500, liquidity = 2000 + * Mint [100, 200] with L=1000: + * → liquidityGross[100] = 2000 + * → liquidityNet[100] = +1500 + * → liquidity = 3000 (if in range) + * Burn [100, 200] with L=1000: + * → liquidityGross[100] = 1000 (back to original) + * → liquidityNet[100] = +500 (back to original) + * → liquidity = 2000 (back to original) + * + * WHAT BUG THIS CATCHES: + * - Burn not properly reversing mint + * - Asymmetric burn (different logic than mint) + * - Liquidity leak (mint adds X, burn removes Y where Y ≠ X) + * - Tick not cleaned up when liquidityGross reaches 0 + */ + function test_CL_burnReversesMint( + int24 tickLower, + int24 tickUpper, + uint128 liquidityDelta + ) public virtual { + // Setup: Constrain to valid values + tickLower = int24(clampBetween(tickLower, MIN_TICK, MAX_TICK - 1)); + tickUpper = int24(clampBetween(tickUpper, tickLower + 1, MAX_TICK)); + liquidityDelta = uint128(clampBetween(liquidityDelta, 1, type(uint64).max)); + + // Ensure ticks respect spacing + int24 tickSpacing = _getTickSpacing(); + tickLower = (tickLower / tickSpacing) * tickSpacing; + tickUpper = (tickUpper / tickSpacing) * tickSpacing; + if (tickLower >= tickUpper) return; + + // Capture initial state + uint128 liquidityBefore = _getCurrentLiquidity(); + uint128 grossLowerBefore = _getLiquidityGrossAtTick(tickLower); + uint128 grossUpperBefore = _getLiquidityGrossAtTick(tickUpper); + int128 netLowerBefore = _getLiquidityNetAtTick(tickLower); + int128 netUpperBefore = _getLiquidityNetAtTick(tickUpper); + + // Perform mint then burn + _mintPosition(USER1, tickLower, tickUpper, liquidityDelta); + _burnPosition(USER1, tickLower, tickUpper, liquidityDelta); + + // Capture final state + uint128 liquidityAfter = _getCurrentLiquidity(); + uint128 grossLowerAfter = _getLiquidityGrossAtTick(tickLower); + uint128 grossUpperAfter = _getLiquidityGrossAtTick(tickUpper); + int128 netLowerAfter = _getLiquidityNetAtTick(tickLower); + int128 netUpperAfter = _getLiquidityNetAtTick(tickUpper); + + // All state should be back to initial values + assertEq( + liquidityAfter, + liquidityBefore, + "CL-BURN-001: Burn did not reverse mint (current liquidity)" + ); + + assertEq( + grossLowerAfter, + grossLowerBefore, + "CL-BURN-001: Burn did not reverse mint (liquidityGross at tickLower)" + ); + + assertEq( + grossUpperAfter, + grossUpperBefore, + "CL-BURN-001: Burn did not reverse mint (liquidityGross at tickUpper)" + ); + + assertEq( + netLowerAfter, + netLowerBefore, + "CL-BURN-001: Burn did not reverse mint (liquidityNet at tickLower)" + ); + + assertEq( + netUpperAfter, + netUpperBefore, + "CL-BURN-001: Burn did not reverse mint (liquidityNet at tickUpper)" + ); + } + + ////////////////////////////////////////////////////////////////////// + // HELPER FUNCTIONS (to be overridden by inheriting contract) + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Get the current tick from the pool + */ + function _getCurrentTick() internal view virtual returns (int24); + + /** + * @notice Get the current active liquidity + */ + function _getCurrentLiquidity() internal view virtual returns (uint128); + + /** + * @notice Get liquidityGross for a specific tick + */ + function _getLiquidityGrossAtTick(int24 tick) internal view virtual returns (uint128); + + /** + * @notice Get liquidityNet for a specific tick + */ + function _getLiquidityNetAtTick(int24 tick) internal view virtual returns (int128); + + /** + * @notice Get tick spacing from the pool + */ + function _getTickSpacing() internal view virtual returns (int24); + + /** + * @notice Mint a liquidity position + */ + function _mintPosition( + address recipient, + int24 tickLower, + int24 tickUpper, + uint128 amount + ) internal virtual; + + /** + * @notice Burn a liquidity position + */ + function _burnPosition( + address owner, + int24 tickLower, + int24 tickUpper, + uint128 amount + ) internal virtual; +} diff --git a/contracts/ConcentratedLiquidity/internal/properties/SwapProperties.sol b/contracts/ConcentratedLiquidity/internal/properties/SwapProperties.sol new file mode 100644 index 0000000..0672afe --- /dev/null +++ b/contracts/ConcentratedLiquidity/internal/properties/SwapProperties.sol @@ -0,0 +1,361 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +import "../util/ConcentratedLiquidityTestBase.sol"; +import "../../util/TickMath.sol"; + +/** + * @title Concentrated Liquidity Swap Properties + * @author Crytic (Trail of Bits) + * @notice Properties for swap execution and price impact + * @dev Testing Mode: INTERNAL + * + * WHY THESE PROPERTIES MATTER: + * Swaps are the primary mechanism for price discovery and trading in AMMs. In concentrated + * liquidity pools, swaps must: + * 1. Move price in the correct direction based on trade direction + * 2. Respect price limits (slippage protection) + * 3. Update liquidity when crossing tick boundaries + * 4. Maintain conservation of value (x*y=k equivalent) + * + * Incorrect swap logic can lead to: + * - Price manipulation + * - Sandwich attacks with no slippage + * - Liquidity not being updated (KyberSwap vulnerability) + * - Arbitrage opportunities that drain the pool + */ +abstract contract CryticSwapProperties is ConcentratedLiquidityTestBase { + using TickMath for int24; + using TickMath for uint160; + + ////////////////////////////////////////////////////////////////////// + // PROPERTY 10: Swap Moves Price in Correct Direction + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Test that swapping moves the price in the correct direction + * @dev Property ID: CL-SWAP-001 + * @custom:property-id CL-SWAP-001 + * + * WHY THIS MUST BE TRUE: + * The direction of a swap determines how the price changes: + * + * - zeroForOne = true: Selling token0 for token1 + * → More token0 in pool, less token1 in pool + * → Price of token0 in terms of token1 DECREASES + * → sqrtPriceX96 DECREASES + * → tick DECREASES + * + * - zeroForOne = false: Selling token1 for token0 + * → Less token0 in pool, more token1 in pool + * → Price of token0 in terms of token1 INCREASES + * → sqrtPriceX96 INCREASES + * → tick INCREASES + * + * MATHEMATICAL DEFINITION: + * Price is defined as: price = (token1 / token0) + * In Uniswap V3: sqrtPriceX96 = sqrt(token1/token0) * 2^96 + * + * When selling token0 (adding it to pool): + * token1/token0 decreases → price decreases + * + * When selling token1 (adding it to pool): + * token1/token0 increases → price increases + * + * EXAMPLE: + * Initial: sqrtPrice = 1000, tick = 100 + * + * Swap zeroForOne = true (sell token0): + * → sqrtPrice = 900, tick = 90 + * → Price went DOWN ✓ + * + * Swap zeroForOne = false (sell token1): + * → sqrtPrice = 1100, tick = 110 + * → Price went UP ✓ + * + * WHAT BUG THIS CATCHES: + * - Swap direction logic inverted + * - Price moving opposite to trade direction + * - Sign errors in price calculation + * - Incorrect token pair ordering + */ + function test_CL_swapMoviesPriceInCorrectDirection( + bool zeroForOne, + uint256 amountSpecified + ) public virtual { + // Constrain amount to reasonable range + amountSpecified = clampBetween(amountSpecified, 1, type(uint64).max); + + uint160 sqrtPriceBefore = _getSqrtPriceX96(); + int24 tickBefore = _getCurrentTick(); + + // Perform swap + bool swapSucceeded = _trySwap(zeroForOne, amountSpecified); + if (!swapSucceeded) return; // Skip if swap failed (e.g., insufficient liquidity) + + uint160 sqrtPriceAfter = _getSqrtPriceX96(); + int24 tickAfter = _getCurrentTick(); + + // Check price direction + if (zeroForOne) { + // Selling token0 for token1 → price should decrease or stay same + assertWithMsg( + sqrtPriceAfter <= sqrtPriceBefore, + "CL-SWAP-001: Swap zeroForOne=true increased price (should decrease)" + ); + assertWithMsg( + tickAfter <= tickBefore, + "CL-SWAP-001: Swap zeroForOne=true increased tick (should decrease)" + ); + } else { + // Selling token1 for token0 → price should increase or stay same + assertWithMsg( + sqrtPriceAfter >= sqrtPriceBefore, + "CL-SWAP-001: Swap zeroForOne=false decreased price (should increase)" + ); + assertWithMsg( + tickAfter >= tickBefore, + "CL-SWAP-001: Swap zeroForOne=false decreased tick (should decrease)" + ); + } + } + + ////////////////////////////////////////////////////////////////////// + // PROPERTY 11: Swap Respects Price Limit + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Test that swap never moves price beyond the specified limit + * @dev Property ID: CL-SWAP-002 + * @custom:property-id CL-SWAP-002 + * + * WHY THIS MUST BE TRUE: + * The sqrtPriceLimitX96 parameter provides slippage protection. The swap must + * stop when the price reaches this limit, even if the full amountSpecified + * hasn't been consumed. + * + * This prevents: + * - Excessive slippage + * - Sandwich attacks beyond acceptable limits + * - Trades executing at worse prices than expected + * + * MATHEMATICAL DEFINITION: + * If zeroForOne = true (price decreasing): + * sqrtPriceAfter >= sqrtPriceLimit + * + * If zeroForOne = false (price increasing): + * sqrtPriceAfter <= sqrtPriceLimit + * + * WHAT BUG THIS CATCHES: + * - Price limit not enforced + * - Swap continuing past limit + * - Incorrect inequality direction + */ + function test_CL_swapRespectsLimitPrice( + bool zeroForOne, + uint256 amountSpecified, + uint160 sqrtPriceLimitX96 + ) public virtual { + // Constrain inputs + amountSpecified = clampBetween(amountSpecified, 1, type(uint64).max); + sqrtPriceLimitX96 = uint160(clampBetween(sqrtPriceLimitX96, MIN_SQRT_RATIO + 1, MAX_SQRT_RATIO - 1)); + + uint160 sqrtPriceBefore = _getSqrtPriceX96(); + + // Ensure limit price is valid for the swap direction + if (zeroForOne) { + // Price is decreasing, limit must be below current price + if (sqrtPriceLimitX96 >= sqrtPriceBefore) return; + } else { + // Price is increasing, limit must be above current price + if (sqrtPriceLimitX96 <= sqrtPriceBefore) return; + } + + // Perform swap with limit price + bool swapSucceeded = _trySwapWithLimit(zeroForOne, amountSpecified, sqrtPriceLimitX96); + if (!swapSucceeded) return; + + uint160 sqrtPriceAfter = _getSqrtPriceX96(); + + // Verify price did not exceed limit + if (zeroForOne) { + assertWithMsg( + sqrtPriceAfter >= sqrtPriceLimitX96, + "CL-SWAP-002: Swap exceeded price limit when going down" + ); + } else { + assertWithMsg( + sqrtPriceAfter <= sqrtPriceLimitX96, + "CL-SWAP-002: Swap exceeded price limit when going up" + ); + } + } + + ////////////////////////////////////////////////////////////////////// + // PROPERTY 12: Swap Updates Liquidity When Crossing Ticks + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Test that liquidity is updated when swap crosses tick boundaries + * @dev Property ID: CL-SWAP-003 + * @custom:property-id CL-SWAP-003 + * + * WHY THIS MUST BE TRUE: + * When a swap moves the price across a tick boundary, the current liquidity + * must be updated by applying the liquidityNet at that tick. This is the + * core mechanism for activating/deactivating positions. + * + * Failure to update liquidity when crossing ticks leads to: + * - Using wrong liquidity for price calculation + * - Positions not being activated/deactivated + * - KyberSwap-style vulnerabilities (double-counting) + * + * MATHEMATICAL DEFINITION: + * When crossing tick T in direction D: + * If going up (zeroForOne = false): + * liquidity_new = liquidity_old + liquidityNet[T] + * If going down (zeroForOne = true): + * liquidity_new = liquidity_old - liquidityNet[T] + * + * WHAT BUG THIS CATCHES: + * - Tick crossing not detected + * - Liquidity not updated when crossing + * - Wrong direction applied to liquidityNet + * - KyberSwap vulnerability (price overshoots tick) + */ + function test_CL_swapUpdatesLiquidityWhenCrossingTicks( + bool zeroForOne, + uint256 amountSpecified + ) public virtual { + // Constrain amount to force tick crossing + amountSpecified = clampBetween(amountSpecified, type(uint64).max / 2, type(uint64).max); + + int24 tickBefore = _getCurrentTick(); + uint128 liquidityBefore = _getCurrentLiquidity(); + + // Perform swap + bool swapSucceeded = _trySwap(zeroForOne, amountSpecified); + if (!swapSucceeded) return; + + int24 tickAfter = _getCurrentTick(); + uint128 liquidityAfter = _getCurrentLiquidity(); + + // If we crossed at least one tick, liquidity should have changed + // (unless all crossed ticks have liquidityNet = 0, which is rare) + if (tickAfter != tickBefore) { + // Calculate expected liquidity by summing liquidityNet + int256 expectedLiquidity = 0; + for (uint256 i = 0; i < usedTicks.length; i++) { + int24 tick = usedTicks[i]; + if (tick <= tickAfter) { + expectedLiquidity += int256(int128(_getLiquidityNetAtTick(tick))); + } + } + + // Liquidity must match the calculated value + if (expectedLiquidity >= 0) { + assertEq( + liquidityAfter, + uint128(uint256(expectedLiquidity)), + "CL-SWAP-003: Liquidity not correctly updated after crossing ticks" + ); + } + } + } + + ////////////////////////////////////////////////////////////////////// + // PROPERTY 13: Swap Price Stays Within Valid Range + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Test that swap never moves price outside valid bounds + * @dev Property ID: CL-SWAP-004 + * @custom:property-id CL-SWAP-004 + * + * WHY THIS MUST BE TRUE: + * There are mathematical limits to valid prices in Uniswap V3: + * - MIN_SQRT_RATIO = 4295128739 + * - MAX_SQRT_RATIO = 1461446703485210103287273052203988822378723970342 + * + * These correspond to MIN_TICK and MAX_TICK. Price cannot go beyond these + * bounds as it would cause overflow/underflow in the math library. + * + * WHAT BUG THIS CATCHES: + * - Overflow/underflow in price calculation + * - Swap allowing invalid price states + * - Missing bounds checks + */ + function test_CL_swapPriceStaysWithinBounds( + bool zeroForOne, + uint256 amountSpecified + ) public virtual { + amountSpecified = clampBetween(amountSpecified, 1, type(uint128).max); + + // Perform swap + bool swapSucceeded = _trySwap(zeroForOne, amountSpecified); + if (!swapSucceeded) return; + + uint160 sqrtPriceAfter = _getSqrtPriceX96(); + int24 tickAfter = _getCurrentTick(); + + // Price must be within valid bounds + assertWithMsg( + sqrtPriceAfter >= MIN_SQRT_RATIO, + "CL-SWAP-004: Swap resulted in price below MIN_SQRT_RATIO" + ); + + assertWithMsg( + sqrtPriceAfter < MAX_SQRT_RATIO, + "CL-SWAP-004: Swap resulted in price above MAX_SQRT_RATIO" + ); + + // Tick must be within valid bounds + assertWithMsg( + tickAfter >= MIN_TICK, + "CL-SWAP-004: Swap resulted in tick below MIN_TICK" + ); + + assertWithMsg( + tickAfter <= MAX_TICK, + "CL-SWAP-004: Swap resulted in tick above MAX_TICK" + ); + } + + ////////////////////////////////////////////////////////////////////// + // HELPER FUNCTIONS (to be overridden by inheriting contract) + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Get the current sqrt price + */ + function _getSqrtPriceX96() internal view virtual returns (uint160); + + /** + * @notice Get the current tick + */ + function _getCurrentTick() internal view virtual returns (int24); + + /** + * @notice Get the current liquidity + */ + function _getCurrentLiquidity() internal view virtual returns (uint128); + + /** + * @notice Get liquidityNet at a tick + */ + function _getLiquidityNetAtTick(int24 tick) internal view virtual returns (int128); + + /** + * @notice Try to perform a swap, return success status + */ + function _trySwap(bool zeroForOne, uint256 amountSpecified) internal virtual returns (bool); + + /** + * @notice Try to perform a swap with price limit, return success status + */ + function _trySwapWithLimit( + bool zeroForOne, + uint256 amountSpecified, + uint160 sqrtPriceLimitX96 + ) internal virtual returns (bool); +} diff --git a/contracts/ConcentratedLiquidity/internal/properties/TickMathProperties.sol b/contracts/ConcentratedLiquidity/internal/properties/TickMathProperties.sol new file mode 100644 index 0000000..d567bf8 --- /dev/null +++ b/contracts/ConcentratedLiquidity/internal/properties/TickMathProperties.sol @@ -0,0 +1,254 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +import "../util/ConcentratedLiquidityTestBase.sol"; +import "../../util/TickMath.sol"; + +/** + * @title Concentrated Liquidity Tick Math Properties + * @author Crytic (Trail of Bits) + * @notice Properties for tick arithmetic and price-tick synchronization + * @dev Testing Mode: INTERNAL + * + * WHY THESE PROPERTIES MATTER: + * Tick-price synchronization is critical in concentrated liquidity AMMs. The KyberSwap hack + * ($50M stolen) resulted from using inequality (!=) instead of directional comparison () + * when checking if price reached the next tick. This caused price to overshoot the tick + * boundary, leading to double-counting of liquidity and catastrophic losses. + * + * These properties ensure: + * 1. Tick moves in sync with price (mathematical requirement) + * 2. Price never overshoots tick boundaries (KyberSwap vulnerability) + * 3. All ticks respect the tick spacing parameter (prevents fragmentation) + */ +abstract contract CryticTickMathProperties is ConcentratedLiquidityTestBase { + using TickMath for int24; + using TickMath for uint160; + + ////////////////////////////////////////////////////////////////////// + // PROPERTY 1: Tick Direction Matches Price Direction + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Test that tick changes in the same direction as price + * @dev Property ID: CL-TICK-001 + * @custom:property-id CL-TICK-001 + * + * WHY THIS MUST BE TRUE: + * By definition, tick = floor(log₁.₀₀₀₁(price)). This is a monotonically increasing + * function, meaning if price increases, tick must increase, and vice versa. + * + * MATHEMATICAL PROOF: + * - tick = floor(log₁.₀₀₀₁(P)) + * - If P₁ < P₂, then log₁.₀₀₀₁(P₁) < log₁.₀₀₀₁(P₂) + * - Therefore floor(log₁.₀₀₀₁(P₁)) ≤ floor(log₁.₀₀₀₁(P₂)) + * + * WHAT BUG THIS CATCHES: + * - Incorrect tick calculation implementations + * - Sign errors in logarithm computation + * - Tick updates that don't match price movements + */ + function test_CL_tickDirectionMatchesPriceDirection( + uint160 oldSqrtPrice, + uint160 newSqrtPrice + ) public virtual { + // Constrain to valid sqrt price ranges + oldSqrtPrice = uint160(clampBetween(oldSqrtPrice, MIN_SQRT_RATIO, MAX_SQRT_RATIO - 1)); + newSqrtPrice = uint160(clampBetween(newSqrtPrice, MIN_SQRT_RATIO, MAX_SQRT_RATIO - 1)); + + // Skip if prices are equal (no direction to check) + if (oldSqrtPrice == newSqrtPrice) return; + + int24 oldTick = TickMath.getTickAtSqrtRatio(oldSqrtPrice); + int24 newTick = TickMath.getTickAtSqrtRatio(newSqrtPrice); + + // If price increased, tick must not decrease + if (newSqrtPrice > oldSqrtPrice) { + assertWithMsg( + newTick >= oldTick, + "CL-TICK-001: Price increased but tick decreased" + ); + } + // If price decreased, tick must not increase + else { + assertWithMsg( + newTick <= oldTick, + "CL-TICK-001: Price decreased but tick increased" + ); + } + } + + ////////////////////////////////////////////////////////////////////// + // PROPERTY 2: No Price Overshoot Past Tick Boundary (KYBERSWAP FIX) + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Test that price never overshoots the target tick boundary + * @dev Property ID: CL-TICK-002 + * @custom:property-id CL-TICK-002 + * @custom:exploit KyberSwap Elastic hack (November 2023) - $50M stolen + * + * WHY THIS MUST BE TRUE: + * When swapping across ticks, the price should stop AT OR BEFORE the next tick + * boundary, never beyond it. This is because: + * 1. Liquidity is updated when crossing ticks + * 2. If price overshoots, the old liquidity continues to be used beyond where + * it should have changed + * 3. This causes double-counting or missing liquidity updates + * + * THE KYBERSWAP VULNERABILITY: + * KyberSwap used: `if (sqrtPrice != sqrtPriceAtNextTick)` + * This allowed: sqrtPrice > sqrtPriceAtNextTick (price went ABOVE the tick) + * Result: Liquidity was counted twice because tick wasn't crossed + * + * CORRECT CHECK: + * When moving up: sqrtPrice ≤ sqrtPriceAtNextTick (use ≤, not !=) + * When moving down: sqrtPrice ≥ sqrtPriceAtPrevTick (use ≥, not !=) + * + * WHAT BUG THIS CATCHES: + * - Using inequality (!=) instead of directional comparison + * - Floating point precision errors causing overshoot + * - Off-by-one errors in tick crossing logic + */ + function test_CL_noPriceOvershootWhenMovingUp( + int24 currentTick, + int24 nextTick + ) public virtual { + // Ensure valid tick range and proper ordering + currentTick = int24(clampBetween(currentTick, MIN_TICK, MAX_TICK - 1)); + nextTick = int24(clampBetween(nextTick, currentTick + 1, MAX_TICK)); + + uint160 currentSqrtPrice = TickMath.getSqrtRatioAtTick(currentTick); + uint160 nextSqrtPrice = TickMath.getSqrtRatioAtTick(nextTick); + + // Simulate a price after swap (between current and next tick) + uint160 priceAfterSwap = uint160( + clampBetween( + uint256(currentSqrtPrice) + 1, + currentSqrtPrice, + nextSqrtPrice + ) + ); + + // CRITICAL: Price must NOT exceed next tick boundary + // This is the KyberSwap vulnerability fix + assertWithMsg( + priceAfterSwap <= nextSqrtPrice, + "CL-TICK-002: Price overshot next tick boundary when moving up" + ); + } + + /** + * @notice Test that price never undershoots the target tick boundary when moving down + * @dev Property ID: CL-TICK-002 (downward direction) + * @custom:property-id CL-TICK-002 + */ + function test_CL_noPriceOvershootWhenMovingDown( + int24 currentTick, + int24 prevTick + ) public virtual { + // Ensure valid tick range and proper ordering + currentTick = int24(clampBetween(currentTick, MIN_TICK + 1, MAX_TICK)); + prevTick = int24(clampBetween(prevTick, MIN_TICK, currentTick - 1)); + + uint160 currentSqrtPrice = TickMath.getSqrtRatioAtTick(currentTick); + uint160 prevSqrtPrice = TickMath.getSqrtRatioAtTick(prevTick); + + // Simulate a price after swap (between prev and current tick) + uint160 priceAfterSwap = uint160( + clampBetween( + uint256(currentSqrtPrice) - 1, + prevSqrtPrice, + currentSqrtPrice + ) + ); + + // CRITICAL: Price must NOT go below previous tick boundary + assertWithMsg( + priceAfterSwap >= prevSqrtPrice, + "CL-TICK-002: Price overshot previous tick boundary when moving down" + ); + } + + ////////////////////////////////////////////////////////////////////// + // PROPERTY 3: Tick Spacing Alignment + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Test that all ticks respect the tick spacing requirement + * @dev Property ID: CL-TICK-003 + * @custom:property-id CL-TICK-003 + * + * WHY THIS MUST BE TRUE: + * Tick spacing prevents excessive fragmentation of liquidity positions. Each pool + * has a tickSpacing parameter (e.g., 10, 60, 200) that determines the granularity + * of price points where liquidity can be placed. + * + * MATHEMATICAL REQUIREMENT: + * - All initialized ticks must satisfy: tick % tickSpacing == 0 + * - The current tick must also be aligned with tickSpacing + * + * ECONOMIC RATIONALE: + * - Reduces gas costs by limiting the number of ticks that can be initialized + * - Concentrates liquidity at specific price points + * - Lower fee tiers have wider tick spacing (less gas, less precision) + * + * WHAT BUG THIS CATCHES: + * - Mint/burn operations that initialize invalid ticks + * - Tick updates that violate spacing constraints + * - Incorrect tick spacing validation in pool initialization + */ + function test_CL_currentTickRespectsSpacing() public virtual { + int24 tickSpacing = _getTickSpacing(); + + // Get current tick from derived contract + int24 currentTick = _getCurrentTick(); + + // Current tick must be aligned with tick spacing + assertWithMsg( + currentTick % tickSpacing == 0, + "CL-TICK-003: Current tick does not respect tick spacing" + ); + + // Current tick must be within valid bounds + assertWithMsg( + currentTick >= MIN_TICK && currentTick <= MAX_TICK, + "CL-TICK-003: Current tick out of bounds" + ); + } + + /** + * @notice Test that all initialized ticks respect tick spacing + * @dev Property ID: CL-TICK-003 + * @custom:property-id CL-TICK-003 + */ + function test_CL_initializedTicksRespectSpacing() public virtual { + int24 tickSpacing = _getTickSpacing(); + + // Check all tracked ticks + for (uint256 i = 0; i < usedTicks.length; i++) { + int24 tick = usedTicks[i]; + + assertWithMsg( + tick % tickSpacing == 0, + "CL-TICK-003: Initialized tick does not respect tick spacing" + ); + + assertWithMsg( + tick >= MIN_TICK && tick <= MAX_TICK, + "CL-TICK-003: Initialized tick out of bounds" + ); + } + } + + ////////////////////////////////////////////////////////////////////// + // HELPER FUNCTIONS (to be overridden by inheriting contract) + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Get the current tick from the pool + * @dev Must be implemented by inheriting contract + * @return Current tick from pool.slot0() + */ + function _getCurrentTick() internal view virtual returns (int24); +} diff --git a/contracts/ConcentratedLiquidity/internal/util/ConcentratedLiquidityTestBase.sol b/contracts/ConcentratedLiquidity/internal/util/ConcentratedLiquidityTestBase.sol new file mode 100644 index 0000000..f086c5f --- /dev/null +++ b/contracts/ConcentratedLiquidity/internal/util/ConcentratedLiquidityTestBase.sol @@ -0,0 +1,70 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +import "../../../util/PropertiesConstants.sol"; +import "../../../util/PropertiesAsserts.sol"; +import "../../../util/IHevm.sol"; + +/** + * @title Concentrated Liquidity Test Base + * @notice Base contract for testing concentrated liquidity pools + * @dev Provides common utilities and tracking for property tests + */ +abstract contract ConcentratedLiquidityTestBase is + PropertiesAsserts, + PropertiesConstants +{ + // Minimum and maximum tick values (Uniswap V3 standard) + int24 internal constant MIN_TICK = -887272; + int24 internal constant MAX_TICK = 887272; + + // Minimum and maximum sqrt price values + uint160 internal constant MIN_SQRT_RATIO = 4295128739; + uint160 internal constant MAX_SQRT_RATIO = 1461446703485210103287273052203988822378723970342; + + // Track all ticks that have been initialized + int24[] internal usedTicks; + mapping(int24 => bool) internal tickExists; + + /** + * @notice Add a tick to the tracking array + * @param tick The tick to add + */ + function _addTick(int24 tick) internal { + if (!tickExists[tick]) { + usedTicks.push(tick); + tickExists[tick] = true; + } + } + + /** + * @notice Remove a tick from tracking + * @param tick The tick to remove + */ + function _removeTick(int24 tick) internal { + if (tickExists[tick]) { + for (uint256 i = 0; i < usedTicks.length; i++) { + if (usedTicks[i] == tick) { + usedTicks[i] = usedTicks[usedTicks.length - 1]; + usedTicks.pop(); + break; + } + } + tickExists[tick] = false; + } + } + + /** + * @notice Get tick spacing for the pool + * @dev Must be implemented by inheriting contract + */ + function _getTickSpacing() internal view virtual returns (int24); + + /** + * @notice Check if a tick is valid given tick spacing + */ + function _isValidTick(int24 tick) internal view returns (bool) { + int24 tickSpacing = _getTickSpacing(); + return tick % tickSpacing == 0 && tick >= MIN_TICK && tick <= MAX_TICK; + } +} diff --git a/contracts/ConcentratedLiquidity/util/IConcentratedLiquidityPool.sol b/contracts/ConcentratedLiquidity/util/IConcentratedLiquidityPool.sol new file mode 100644 index 0000000..c41a9fa --- /dev/null +++ b/contracts/ConcentratedLiquidity/util/IConcentratedLiquidityPool.sol @@ -0,0 +1,113 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +/** + * @title Concentrated Liquidity Pool Interface + * @notice Minimal interface for concentrated liquidity AMM pools (Uniswap V3 style) + * @dev This interface covers the core functions needed for property testing + */ +interface IConcentratedLiquidityPool { + /// @notice The first of the two tokens of the pool, sorted by address + function token0() external view returns (address); + + /// @notice The second of the two tokens of the pool, sorted by address + function token1() external view returns (address); + + /// @notice The pool's fee in hundredths of a bip, i.e. 1e-6 + function fee() external view returns (uint24); + + /// @notice The pool tick spacing + function tickSpacing() external view returns (int24); + + /// @notice The currently in range liquidity available to the pool + function liquidity() external view returns (uint128); + + /// @notice The 0th storage slot in the pool stores many values, and is exposed as a single method to save gas + /// @return sqrtPriceX96 The current price of the pool as a sqrt(token1/token0) Q64.96 value + /// @return tick The current tick of the pool + /// @return observationIndex The index of the last oracle observation that was written + /// @return observationCardinality The current maximum number of observations stored in the pool + /// @return observationCardinalityNext The next maximum number of observations to store + /// @return feeProtocol The protocol fee for both tokens of the pool + /// @return unlocked Whether the pool is currently locked to reentrancy + function slot0() + external + view + returns ( + uint160 sqrtPriceX96, + int24 tick, + uint16 observationIndex, + uint16 observationCardinality, + uint16 observationCardinalityNext, + uint8 feeProtocol, + bool unlocked + ); + + /// @notice Returns information about a tick + /// @param tick The tick to look up + /// @return liquidityGross Total liquidity referencing this tick + /// @return liquidityNet Change in liquidity when crossing this tick + /// @return feeGrowthOutside0X128 Fee growth outside this tick for token0 + /// @return feeGrowthOutside1X128 Fee growth outside this tick for token1 + function ticks(int24 tick) + external + view + returns ( + uint128 liquidityGross, + int128 liquidityNet, + uint256 feeGrowthOutside0X128, + uint256 feeGrowthOutside1X128 + ); + + /// @notice Returns information about a position + /// @param key The position's key (keccak256(owner, tickLower, tickUpper)) + /// @return liquidity The amount of liquidity in the position + /// @return feeGrowthInside0LastX128 Fee growth inside the tick range as of the last action + /// @return feeGrowthInside1LastX128 Fee growth inside the tick range as of the last action + /// @return tokensOwed0 Tokens owed to the position owner in token0 + /// @return tokensOwed1 Tokens owed to the position owner in token1 + function positions(bytes32 key) + external + view + returns ( + uint128 liquidity, + uint256 feeGrowthInside0LastX128, + uint256 feeGrowthInside1LastX128, + uint128 tokensOwed0, + uint128 tokensOwed1 + ); + + /// @notice Adds liquidity for the given recipient/tickLower/tickUpper position + function mint( + address recipient, + int24 tickLower, + int24 tickUpper, + uint128 amount, + bytes calldata data + ) external returns (uint256 amount0, uint256 amount1); + + /// @notice Removes liquidity from the sender and accounts tokens owed + function burn( + int24 tickLower, + int24 tickUpper, + uint128 amount + ) external returns (uint256 amount0, uint256 amount1); + + /// @notice Swap token0 for token1, or token1 for token0 + function swap( + address recipient, + bool zeroForOne, + int256 amountSpecified, + uint160 sqrtPriceLimitX96, + bytes calldata data + ) external returns (int256 amount0, int256 amount1); + + /// @notice Collect tokens owed to a position + function collect( + address recipient, + int24 tickLower, + int24 tickUpper, + uint128 amount0Requested, + uint128 amount1Requested + ) external returns (uint128 amount0, uint128 amount1); +} diff --git a/contracts/ConcentratedLiquidity/util/TickMath.sol b/contracts/ConcentratedLiquidity/util/TickMath.sol new file mode 100644 index 0000000..04cc111 --- /dev/null +++ b/contracts/ConcentratedLiquidity/util/TickMath.sol @@ -0,0 +1,204 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +/** + * @title Tick Math Library + * @notice Simplified tick math library for property testing + * @dev This is a minimal implementation. For production, use Uniswap's TickMath library + * @dev Source: https://github.com/Uniswap/v3-core/blob/main/contracts/libraries/TickMath.sol + */ +library TickMath { + int24 internal constant MIN_TICK = -887272; + int24 internal constant MAX_TICK = 887272; + + uint160 internal constant MIN_SQRT_RATIO = 4295128739; + uint160 internal constant MAX_SQRT_RATIO = 1461446703485210103287273052203988822378723970342; + + /** + * @notice Calculates sqrt(1.0001^tick) * 2^96 + * @dev Throws if |tick| > max tick + * @param tick The input tick for the above formula + * @return sqrtPriceX96 A Fixed point Q64.96 number representing the sqrt of the ratio of the two assets + */ + function getSqrtRatioAtTick(int24 tick) internal pure returns (uint160 sqrtPriceX96) { + uint256 absTick = tick < 0 ? uint256(-int256(tick)) : uint256(int256(tick)); + require(absTick <= uint256(int256(MAX_TICK)), "T"); + + uint256 ratio = absTick & 0x1 != 0 + ? 0xfffcb933bd6fad37aa2d162d1a594001 + : 0x100000000000000000000000000000000; + if (absTick & 0x2 != 0) ratio = (ratio * 0xfff97272373d413259a46990580e213a) >> 128; + if (absTick & 0x4 != 0) ratio = (ratio * 0xfff2e50f5f656932ef12357cf3c7fdcc) >> 128; + if (absTick & 0x8 != 0) ratio = (ratio * 0xffe5caca7e10e4e61c3624eaa0941cd0) >> 128; + if (absTick & 0x10 != 0) ratio = (ratio * 0xffcb9843d60f6159c9db58835c926644) >> 128; + if (absTick & 0x20 != 0) ratio = (ratio * 0xff973b41fa98c081472e6896dfb254c0) >> 128; + if (absTick & 0x40 != 0) ratio = (ratio * 0xff2ea16466c96a3843ec78b326b52861) >> 128; + if (absTick & 0x80 != 0) ratio = (ratio * 0xfe5dee046a99a2a811c461f1969c3053) >> 128; + if (absTick & 0x100 != 0) ratio = (ratio * 0xfcbe86c7900a88aedcffc83b479aa3a4) >> 128; + if (absTick & 0x200 != 0) ratio = (ratio * 0xf987a7253ac413176f2b074cf7815e54) >> 128; + if (absTick & 0x400 != 0) ratio = (ratio * 0xf3392b0822b70005940c7a398e4b70f3) >> 128; + if (absTick & 0x800 != 0) ratio = (ratio * 0xe7159475a2c29b7443b29c7fa6e889d9) >> 128; + if (absTick & 0x1000 != 0) ratio = (ratio * 0xd097f3bdfd2022b8845ad8f792aa5825) >> 128; + if (absTick & 0x2000 != 0) ratio = (ratio * 0xa9f746462d870fdf8a65dc1f90e061e5) >> 128; + if (absTick & 0x4000 != 0) ratio = (ratio * 0x70d869a156d2a1b890bb3df62baf32f7) >> 128; + if (absTick & 0x8000 != 0) ratio = (ratio * 0x31be135f97d08fd981231505542fcfa6) >> 128; + if (absTick & 0x10000 != 0) ratio = (ratio * 0x9aa508b5b7a84e1c677de54f3e99bc9) >> 128; + if (absTick & 0x20000 != 0) ratio = (ratio * 0x5d6af8dedb81196699c329225ee604) >> 128; + if (absTick & 0x40000 != 0) ratio = (ratio * 0x2216e584f5fa1ea926041bedfe98) >> 128; + if (absTick & 0x80000 != 0) ratio = (ratio * 0x48a170391f7dc42444e8fa2) >> 128; + + if (tick > 0) ratio = type(uint256).max / ratio; + + sqrtPriceX96 = uint160((ratio >> 32) + (ratio % (1 << 32) == 0 ? 0 : 1)); + } + + /** + * @notice Calculates the greatest tick value such that getSqrtRatioAtTick(tick) <= sqrtPriceX96 + * @dev Throws if sqrtPriceX96 < MIN_SQRT_RATIO or sqrtPriceX96 > MAX_SQRT_RATIO + * @param sqrtPriceX96 The sqrt ratio for which to compute the tick + * @return tick The greatest tick for which the ratio is less than or equal to the input ratio + */ + function getTickAtSqrtRatio(uint160 sqrtPriceX96) internal pure returns (int24 tick) { + require(sqrtPriceX96 >= MIN_SQRT_RATIO && sqrtPriceX96 < MAX_SQRT_RATIO, "R"); + uint256 ratio = uint256(sqrtPriceX96) << 32; + + uint256 r = ratio; + uint256 msb = 0; + + assembly { + let f := shl(7, gt(r, 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF)) + msb := or(msb, f) + r := shr(f, r) + } + assembly { + let f := shl(6, gt(r, 0xFFFFFFFFFFFFFFFF)) + msb := or(msb, f) + r := shr(f, r) + } + assembly { + let f := shl(5, gt(r, 0xFFFFFFFF)) + msb := or(msb, f) + r := shr(f, r) + } + assembly { + let f := shl(4, gt(r, 0xFFFF)) + msb := or(msb, f) + r := shr(f, r) + } + assembly { + let f := shl(3, gt(r, 0xFF)) + msb := or(msb, f) + r := shr(f, r) + } + assembly { + let f := shl(2, gt(r, 0xF)) + msb := or(msb, f) + r := shr(f, r) + } + assembly { + let f := shl(1, gt(r, 0x3)) + msb := or(msb, f) + r := shr(f, r) + } + assembly { + let f := gt(r, 0x1) + msb := or(msb, f) + } + + if (msb >= 128) r = ratio >> (msb - 127); + else r = ratio << (127 - msb); + + int256 log_2 = (int256(msb) - 128) << 64; + + assembly { + r := shr(127, mul(r, r)) + let f := shr(128, r) + log_2 := or(log_2, shl(63, f)) + r := shr(f, r) + } + assembly { + r := shr(127, mul(r, r)) + let f := shr(128, r) + log_2 := or(log_2, shl(62, f)) + r := shr(f, r) + } + assembly { + r := shr(127, mul(r, r)) + let f := shr(128, r) + log_2 := or(log_2, shl(61, f)) + r := shr(f, r) + } + assembly { + r := shr(127, mul(r, r)) + let f := shr(128, r) + log_2 := or(log_2, shl(60, f)) + r := shr(f, r) + } + assembly { + r := shr(127, mul(r, r)) + let f := shr(128, r) + log_2 := or(log_2, shl(59, f)) + r := shr(f, r) + } + assembly { + r := shr(127, mul(r, r)) + let f := shr(128, r) + log_2 := or(log_2, shl(58, f)) + r := shr(f, r) + } + assembly { + r := shr(127, mul(r, r)) + let f := shr(128, r) + log_2 := or(log_2, shl(57, f)) + r := shr(f, r) + } + assembly { + r := shr(127, mul(r, r)) + let f := shr(128, r) + log_2 := or(log_2, shl(56, f)) + r := shr(f, r) + } + assembly { + r := shr(127, mul(r, r)) + let f := shr(128, r) + log_2 := or(log_2, shl(55, f)) + r := shr(f, r) + } + assembly { + r := shr(127, mul(r, r)) + let f := shr(128, r) + log_2 := or(log_2, shl(54, f)) + r := shr(f, r) + } + assembly { + r := shr(127, mul(r, r)) + let f := shr(128, r) + log_2 := or(log_2, shl(53, f)) + r := shr(f, r) + } + assembly { + r := shr(127, mul(r, r)) + let f := shr(128, r) + log_2 := or(log_2, shl(52, f)) + r := shr(f, r) + } + assembly { + r := shr(127, mul(r, r)) + let f := shr(128, r) + log_2 := or(log_2, shl(51, f)) + r := shr(f, r) + } + assembly { + r := shr(127, mul(r, r)) + let f := shr(128, r) + log_2 := or(log_2, shl(50, f)) + } + + int256 log_sqrt10001 = log_2 * 255738958999603826347141; + + int24 tickLow = int24((log_sqrt10001 - 3402992956809132418596140100660247210) >> 128); + int24 tickHi = int24((log_sqrt10001 + 291339464771989622907027621153398088495) >> 128); + + tick = tickLow == tickHi ? tickLow : getSqrtRatioAtTick(tickHi) <= sqrtPriceX96 ? tickHi : tickLow; + } +} diff --git a/tests/ConcentratedLiquidity/foundry/src/SimpleMockPool.sol b/tests/ConcentratedLiquidity/foundry/src/SimpleMockPool.sol new file mode 100644 index 0000000..08881fa --- /dev/null +++ b/tests/ConcentratedLiquidity/foundry/src/SimpleMockPool.sol @@ -0,0 +1,198 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +/** + * @title Simple Mock Concentrated Liquidity Pool + * @notice Minimal implementation for property testing + * @dev This is a simplified mock for demonstration purposes only + */ +contract SimpleMockPool { + // Pool state + uint160 public sqrtPriceX96; + int24 public tick; + uint128 public liquidity; + int24 public immutable tickSpacing; + + // Tick data + struct TickInfo { + uint128 liquidityGross; + int128 liquidityNet; + bool initialized; + } + mapping(int24 => TickInfo) public ticks; + + // Position data + struct PositionInfo { + uint128 liquidity; + } + mapping(bytes32 => PositionInfo) public positions; + + // Constants + int24 internal constant MIN_TICK = -887272; + int24 internal constant MAX_TICK = 887272; + uint160 internal constant MIN_SQRT_RATIO = 4295128739; + uint160 internal constant MAX_SQRT_RATIO = 1461446703485210103287273052203988822378723970342; + + constructor(int24 _tickSpacing) { + tickSpacing = _tickSpacing; + // Initialize at mid-range price + sqrtPriceX96 = 79228162514264337593543950336; // sqrt(1) * 2^96 + tick = 0; + liquidity = 0; + } + + /** + * @notice Get slot0 data (Uniswap V3 compatibility) + */ + function slot0() + external + view + returns ( + uint160 _sqrtPriceX96, + int24 _tick, + uint16 observationIndex, + uint16 observationCardinality, + uint16 observationCardinalityNext, + uint8 feeProtocol, + bool unlocked + ) + { + _sqrtPriceX96 = sqrtPriceX96; + _tick = tick; + observationIndex = 0; + observationCardinality = 0; + observationCardinalityNext = 0; + feeProtocol = 0; + unlocked = true; + } + + /** + * @notice Mint a liquidity position + */ + function mint( + address recipient, + int24 tickLower, + int24 tickUpper, + uint128 amount, + bytes calldata /* data */ + ) external returns (uint256 amount0, uint256 amount1) { + require(amount > 0, "Amount must be positive"); + require(tickLower < tickUpper, "Invalid tick range"); + require(tickLower % tickSpacing == 0, "tickLower not aligned"); + require(tickUpper % tickSpacing == 0, "tickUpper not aligned"); + + // Update tick data + _updateTick(tickLower, int128(amount), false); + _updateTick(tickUpper, -int128(amount), false); + + // Update position + bytes32 positionKey = keccak256(abi.encodePacked(recipient, tickLower, tickUpper)); + positions[positionKey].liquidity += amount; + + // Update current liquidity if in range + if (tick >= tickLower && tick < tickUpper) { + liquidity += amount; + } + + // For simplicity, return fixed amounts + amount0 = 1000; + amount1 = 1000; + } + + /** + * @notice Burn a liquidity position + */ + function burn( + int24 tickLower, + int24 tickUpper, + uint128 amount + ) external returns (uint256 amount0, uint256 amount1) { + require(amount > 0, "Amount must be positive"); + + // Update tick data + _updateTick(tickLower, -int128(amount), false); + _updateTick(tickUpper, int128(amount), false); + + // Update position + bytes32 positionKey = keccak256(abi.encodePacked(msg.sender, tickLower, tickUpper)); + require(positions[positionKey].liquidity >= amount, "Insufficient liquidity"); + positions[positionKey].liquidity -= amount; + + // Update current liquidity if in range + if (tick >= tickLower && tick < tickUpper) { + require(liquidity >= amount, "Insufficient pool liquidity"); + liquidity -= amount; + } + + // For simplicity, return fixed amounts + amount0 = 1000; + amount1 = 1000; + } + + /** + * @notice Swap tokens (simplified) + */ + function swap( + address /* recipient */, + bool zeroForOne, + int256 amountSpecified, + uint160 sqrtPriceLimitX96, + bytes calldata /* data */ + ) external returns (int256 amount0, int256 amount1) { + require(amountSpecified != 0, "Invalid amount"); + + // Simple price update logic (not production-ready) + if (zeroForOne) { + // Price goes down + uint160 newPrice = sqrtPriceX96 > 1000000 ? sqrtPriceX96 - 1000000 : MIN_SQRT_RATIO; + if (sqrtPriceLimitX96 > 0 && newPrice < sqrtPriceLimitX96) { + newPrice = sqrtPriceLimitX96; + } + sqrtPriceX96 = newPrice; + tick = tick > -100 ? tick - 1 : tick; + } else { + // Price goes up + uint160 newPrice = sqrtPriceX96 < MAX_SQRT_RATIO - 1000000 + ? sqrtPriceX96 + 1000000 + : MAX_SQRT_RATIO - 1; + if (sqrtPriceLimitX96 > 0 && newPrice > sqrtPriceLimitX96) { + newPrice = sqrtPriceLimitX96; + } + sqrtPriceX96 = newPrice; + tick = tick < 100 ? tick + 1 : tick; + } + + // For simplicity, return fixed amounts + amount0 = zeroForOne ? amountSpecified : -amountSpecified; + amount1 = zeroForOne ? -amountSpecified : amountSpecified; + } + + /** + * @notice Update tick data + */ + function _updateTick( + int24 _tick, + int128 liquidityDelta, + bool /* upper */ + ) internal { + TickInfo storage tickInfo = ticks[_tick]; + + uint128 liquidityGrossBefore = tickInfo.liquidityGross; + int128 liquidityNetBefore = tickInfo.liquidityNet; + + uint128 liquidityGrossAfter = liquidityDelta < 0 + ? liquidityGrossBefore - uint128(-liquidityDelta) + : liquidityGrossBefore + uint128(liquidityDelta); + + int128 liquidityNetAfter = liquidityNetBefore + liquidityDelta; + + tickInfo.liquidityGross = liquidityGrossAfter; + tickInfo.liquidityNet = liquidityNetAfter; + + if (!tickInfo.initialized && liquidityGrossAfter > 0) { + tickInfo.initialized = true; + } else if (tickInfo.initialized && liquidityGrossAfter == 0) { + tickInfo.initialized = false; + } + } +} diff --git a/tests/ConcentratedLiquidity/foundry/test/CryticConcentratedLiquidityTest.sol b/tests/ConcentratedLiquidity/foundry/test/CryticConcentratedLiquidityTest.sol new file mode 100644 index 0000000..f2500df --- /dev/null +++ b/tests/ConcentratedLiquidity/foundry/test/CryticConcentratedLiquidityTest.sol @@ -0,0 +1,263 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.13; + +import "properties/ConcentratedLiquidity/internal/properties/TickMathProperties.sol"; +import "properties/ConcentratedLiquidity/internal/properties/LiquidityProperties.sol"; +import "properties/ConcentratedLiquidity/internal/properties/MintBurnProperties.sol"; +import "properties/ConcentratedLiquidity/internal/properties/SwapProperties.sol"; +import "../src/SimpleMockPool.sol"; + +/** + * @title Crytic Concentrated Liquidity Internal Test Harness + * @notice Test harness combining SimpleMockPool with all concentrated liquidity properties + * @dev This demonstrates internal testing mode where the harness inherits from the pool + */ +contract CryticConcentratedLiquidityInternalHarness is + SimpleMockPool, + CryticTickMathProperties, + CryticLiquidityProperties, + CryticMintBurnProperties, + CryticSwapProperties +{ + // Track all initialized ticks for property checks + int24[] private allTicks; + mapping(int24 => uint256) private tickToIndex; + + constructor() SimpleMockPool(60) { + // Initialize pool with some liquidity around current price + // Current tick is 0, create positions around it + _mintPosition(USER1, -600, 600, 1000000e18); + _mintPosition(USER2, -1200, 1200, 500000e18); + _mintPosition(USER3, -300, 300, 2000000e18); + } + + ////////////////////////////////////////////////////////////////////// + // IMPLEMENT REQUIRED VIRTUAL FUNCTIONS + ////////////////////////////////////////////////////////////////////// + + function _getCurrentTick() internal view override( + CryticTickMathProperties, + CryticLiquidityProperties, + CryticMintBurnProperties, + CryticSwapProperties + ) returns (int24) { + return tick; + } + + function _getCurrentLiquidity() internal view override( + CryticLiquidityProperties, + CryticMintBurnProperties + ) returns (uint128) { + return liquidity; + } + + function _getSqrtPriceX96() internal view override returns (uint160) { + return sqrtPriceX96; + } + + function _getTickSpacing() internal view override returns (int24) { + return tickSpacing; + } + + function _getLiquidityNetAtTick(int24 _tick) internal view override( + CryticLiquidityProperties, + CryticSwapProperties + ) returns (int128) { + (,int128 liquidityNet,) = ticks(_tick); + return liquidityNet; + } + + function _getLiquidityGrossAtTick(int24 _tick) internal view override( + CryticLiquidityProperties, + CryticMintBurnProperties + ) returns (uint128) { + (uint128 liquidityGross,,) = ticks(_tick); + return liquidityGross; + } + + function _mintPosition( + address recipient, + int24 tickLower, + int24 tickUpper, + uint128 amount + ) internal override { + // Track ticks + _addTickToTracking(tickLower); + _addTickToTracking(tickUpper); + + // Call the pool's mint function + this.mint(recipient, tickLower, tickUpper, amount, ""); + + // Update base class tracking + _addTick(tickLower); + _addTick(tickUpper); + } + + function _burnPosition( + address /* owner */, + int24 tickLower, + int24 tickUpper, + uint128 amount + ) internal override { + // Call the pool's burn function + this.burn(tickLower, tickUpper, amount); + + // If ticks are no longer initialized, remove from tracking + (uint128 grossLower,,) = ticks(tickLower); + (uint128 grossUpper,,) = ticks(tickUpper); + + if (grossLower == 0) { + _removeTick(tickLower); + _removeTickFromTracking(tickLower); + } + if (grossUpper == 0) { + _removeTick(tickUpper); + _removeTickFromTracking(tickUpper); + } + } + + function _trySwap(bool zeroForOne, uint256 amountSpecified) internal override returns (bool) { + try this.swap( + address(this), + zeroForOne, + int256(amountSpecified), + 0, // No price limit + "" + ) { + return true; + } catch { + return false; + } + } + + function _trySwapWithLimit( + bool zeroForOne, + uint256 amountSpecified, + uint160 sqrtPriceLimitX96 + ) internal override returns (bool) { + try this.swap( + address(this), + zeroForOne, + int256(amountSpecified), + sqrtPriceLimitX96, + "" + ) { + return true; + } catch { + return false; + } + } + + ////////////////////////////////////////////////////////////////////// + // HELPER FUNCTIONS FOR TICK TRACKING + ////////////////////////////////////////////////////////////////////// + + function _addTickToTracking(int24 _tick) private { + if (tickToIndex[_tick] == 0 && (allTicks.length == 0 || allTicks[0] != _tick)) { + allTicks.push(_tick); + tickToIndex[_tick] = allTicks.length; // 1-based index + } + } + + function _removeTickFromTracking(int24 _tick) private { + uint256 index = tickToIndex[_tick]; + if (index > 0) { + index--; // Convert to 0-based + if (index < allTicks.length - 1) { + allTicks[index] = allTicks[allTicks.length - 1]; + tickToIndex[allTicks[index]] = index + 1; + } + allTicks.pop(); + delete tickToIndex[_tick]; + } + } + + ////////////////////////////////////////////////////////////////////// + // PUBLIC FUNCTIONS FOR FUZZING + ////////////////////////////////////////////////////////////////////// + + /** + * @notice Fuzz target: mint a random position + */ + function fuzz_mint( + int24 tickLower, + int24 tickUpper, + uint128 amount + ) public { + // Constrain inputs + tickLower = int24(clampBetween(tickLower, MIN_TICK, MAX_TICK - tickSpacing)); + tickUpper = int24(clampBetween(tickUpper, tickLower + tickSpacing, MAX_TICK)); + amount = uint128(clampBetween(amount, 1e18, 1000000e18)); + + // Align to tick spacing + tickLower = (tickLower / tickSpacing) * tickSpacing; + tickUpper = (tickUpper / tickSpacing) * tickSpacing; + + if (tickLower >= tickUpper) return; + + try this.mint(msg.sender, tickLower, tickUpper, amount, "") { + _addTick(tickLower); + _addTick(tickUpper); + _addTickToTracking(tickLower); + _addTickToTracking(tickUpper); + } catch { + // Mint failed, continue fuzzing + } + } + + /** + * @notice Fuzz target: burn a position + */ + function fuzz_burn( + int24 tickLower, + int24 tickUpper, + uint128 amount + ) public { + // Constrain inputs + tickLower = int24(clampBetween(tickLower, MIN_TICK, MAX_TICK - tickSpacing)); + tickUpper = int24(clampBetween(tickUpper, tickLower + tickSpacing, MAX_TICK)); + amount = uint128(clampBetween(amount, 1e18, 1000000e18)); + + // Align to tick spacing + tickLower = (tickLower / tickSpacing) * tickSpacing; + tickUpper = (tickUpper / tickSpacing) * tickSpacing; + + if (tickLower >= tickUpper) return; + + try this.burn(tickLower, tickUpper, amount) { + // Update tracking if ticks are no longer initialized + (uint128 grossLower,,) = ticks(tickLower); + (uint128 grossUpper,,) = ticks(tickUpper); + + if (grossLower == 0) { + _removeTick(tickLower); + _removeTickFromTracking(tickLower); + } + if (grossUpper == 0) { + _removeTick(tickUpper); + _removeTickFromTracking(tickUpper); + } + } catch { + // Burn failed, continue fuzzing + } + } + + /** + * @notice Fuzz target: perform a swap + */ + function fuzz_swap(bool zeroForOne, uint256 amount) public { + amount = clampBetween(amount, 1e18, 1000000e18); + + try this.swap( + msg.sender, + zeroForOne, + int256(amount), + 0, // No price limit + "" + ) { + // Swap succeeded + } catch { + // Swap failed, continue fuzzing + } + } +}