Uniswap v3: Liquidity and Invariants 101

Uniswap v3 is the largest cornerstone in the DeFi space on Ethereum. While Uniswap v3 is efficient, the v3 update has made the mathematical relationship between the liquidity of a position, the amount of assets in that position, and its price range more complex. In this article we will discuss how do we understand liquidity and how does uniswap v3 come up with its interval liquidity formula? We will also cover a few liquidity invariants written by echidna which should never be violated for security reasons. Without further ado, let's talk UniswapV3 math.

Uniswap v3: Liquidity Math

To understand liquidity in uniswap v3 we will take a single position liquidity for simplicity. Uniswap uses product fixed model (x.y = k). It is defined as a trading function between two assets X and Y where the multiplication of these reserves corresponds to a fixed value of total supply of tokens.

Asset Price

We will use P to represent the price of asset X in terms of asset Y and is equivalent to P= y_p/x_p. This price P is also equivalent to -d_y/d_x. How? Let's follow the reason provided in the YieldSpace paper.

Imagine we require a liquidity provision formula similar to the constant product formula but with a desire to satisfy the property of a 50-50 portfolio of two assets. The task is to design a formula in a way that it never violates the invariant relationship between asset x and y. Now let's understand the most important fact about all these curves representing our liquidity for AMM. 

If Bob sells some quantity of asset x in exchange of y then the pool reserves of x will get increase represent as d_x and pool reserves of y will get decrease -d_y. So the ratio represents the price at which the bob has sold asset x.

P = \frac{\mathrm{d}_{y}^{}}{\mathrm{d}_{x}^{}}

Single Liquidity Position and Uniswap v2: what’s similar?

Now, the whole innovation of Uniswap v3 starts from Ticks. In Uniswap v3, anyone can create a custom position to provide some amount of liquidity L within a price range [P_a^, P_b ] between two ticks and earn fees. This is called providing concentrated liquidity for efficient usage of capital, unlike v2 where liquidity is in the range of [0,∞]. If the position exceeds the limit the liquidity will convert entirely into one asset and the position will be liquidated, meaning no more swaps possible within that range hence no more fee collection.

x.y = k = \mathrm{L}_{}^{2} \to 2.1

The liquidity was distributed uniformly along the price curve between 0 and infinity in Uniswap v1 and v2. In v3 the liquidity is allocated within a custom price range. We called it “real reserves”. Real reserves is only some part of the virtual reserves

\Rightarrow \mathrm{x}_{virtual}^{} - \mathrm{x}_{pb}^{} = \mathrm{x}_{real}^{}

\Rightarrow \mathrm{y}_{virtual}^{} - \mathrm{y}_{pa}^{} = \mathrm{y}_{real}^{}

\Rightarrow \mathrm{x}_{pb}^{} = \frac{L}{\sqrt{\mathrm{P}_{b}^{}}}

\Rightarrow \mathrm{y}_{pa}^{} = \frac{L}{\sqrt{\mathrm{P}_{a}^{}}}

Hence, the formula for the v3 curve can be represented as:

(x+\frac{L}{\sqrt{\mathrm{P}_{}^{b}}})(y+ L\sqrt{\mathrm{P}_{a}^{}})=L^{2}\to 2.2

The uniswap v3 doesn’t track the virtual reserves x and y because it keeps changing on every trade; however, it does record the values of L and √P. This is convenient because only one of them changes at a time. √P changes when swapping within a tick, while liquidity changes when crossing a tick, or when minting or burning. This helps us to avoid some rounding errors that could be encountered if tracking virtual reserves x and y.

L = \sqrt{\mathrm{x.y}}

\sqrt{P} = \sqrt{\frac{y}{x}}

So whenever a trade happens the change of value of one asset with respect to the change of price of its value can help us to determine the interval liquidity of a position.

L = \frac{\Delta y}{\Delta \sqrt{P}}

Suppose there is a small y, and we need to swap it with x. When swapping one token for the other, the pool contract can first compute the new √P using 

{\Delta \sqrt{P}} = \frac{\Delta y}{L}

And then we can compute the amount of token0 to be sent in pool using formula:

{\Delta {x}} = \frac{L}{\Delta\sqrt{P}}

Liquidity Value of a Single Position

Lets calculate how we can derive the L from the token x and token y, price interval [p_a, p_b] and current price P.

We already know that the curve reserves between the price range [P_a, P_b] is defined as:

(\mathrm{x}_{r}^{} + \frac{L}{\sqrt{\mathrm{P}_{b}^{}}}) (\mathrm{y}_{r}^{} + {L}{\sqrt{\mathrm{P}_{a}^{}}}) = \mathrm{L}_{}^{2} \to  Eq 1

Now when the current price P is less than P_b , the y_r becomes 0

Case 1

So now replacing y_r = 0 in equations: P <= P_a

(\mathrm{x}_{r}^{} + \frac{L}{\sqrt{\mathrm{P}_{b}^{}}}) (\mathrm{0}_{}^{} + {L}{\sqrt{\mathrm{P}_{a}^{}}}) = \mathrm{L}_{}^{2}

(\mathrm{x}_{r}^{} \sqrt{\mathrm{P}_{a}^{}}+ \frac{L}{\sqrt{\mathrm{P}_{b}^{}}}\sqrt{\mathrm{P}_{a}^{}})= L

(\mathrm{x}_{r}^{} \sqrt{\mathrm{P}_{a}^{}} = L -  \frac{L}{\sqrt{\mathrm{P}_{b}^{}}}\sqrt{\mathrm{P}_{a}^{}})

(\mathrm{x}_{r}^{} \sqrt{\mathrm{P}_{a}^{}} = L (\frac{\sqrt{\mathrm{P}_{b}^{}}-\sqrt{\mathrm{P}_{a}^{}}}{\sqrt{\mathrm{P}_{b}^{}}} )

x_{r}\frac{\sqrt{P_{a}}\sqrt{P_{b}}}{\sqrt{P_{b}}-\sqrt{P_{a}}} = L 

Case 2

Similarly when P_b <= P, x_r = 0:

(0 + \frac{L}{\sqrt{P_{a}}})(y_r + L \sqrt{P_a}) = L^2

\frac{y_r}{\sqrt{P_b}} + \frac{L\sqrt{P_a}}{\sqrt{P_b}} = L

\frac{y_r}{\sqrt{P_b}} = L (1 - \frac{\sqrt{P_a}}{P_b})

L = \frac{y_r}{\sqrt{P_b}-\sqrt{P_a}}

Case 3

When Pb < P < P_a

Here we are assuming that the liquidity L_x is placed in between the range of P to P_b and Liquidity of L_y is in the range of P to P_a as illustrated in the above diagram. Ideally the L_x = L_y.

From the price range formula case 1 we can deduce that when the price is moving from P to P_b the formula will become:

x_r \frac{\sqrt{P}\sqrt{P_b}}{\sqrt{P_b}-\sqrt{P}} = L_x

Similarly for L_y from case2:

L_y = \frac{y_r}{\sqrt{P_b}-\sqrt{P_a}}

Multiple Positions in v3

Uniswap has introduced a unique feature where multiple positions can be initialized with different tick ranges. We can see that in the below graph when both intervals cover the price range, the reserves of both intervals will be used and the virtual reserves equal to the sum of liquidities. Furthermore, if only one interval covers the price then only the reserves of this range will be used. And if prices go beyond these two intervals the pool liquidity will get zero and no provider in that range will earn fees. As the price moves along the virtual curve, the liquidity value changes by some ΔL at certain price points. 

Also, There could be multiple Positions on one Tick. Uniswap v3 has a global state variable of liquidity L. It saves the sum of the corresponding Tick of current price. When the price fluctuates and passes one certain Tick, the liquidity will increase or decrease depending on which way the price fluctuates. 

Now let's discuss some of the invariants written around liquidity by echidna and why do we really care about them?

Liquidity Invariants

What's invariant?

Invariants are the global properties of the program that are expected to be always true. They are helpful to ensure that the smart contracts follow the intended logic.They can also be used as functions that can represent any invalid state that a contract can achieve. To name a few:

Invalid Arithmetic: For example, when the user’s balance can overflow, resulting in a limitless supply of free tokens.

Invalid access control: For example, when the attacker becomes the contract’s owner.

Invalid state machine: For example, when the tokens can be transferred even when the contract is paused.

One other interesting property of invariants checking is that they are very useful on the bytecode level as they allow us to detect low level issues such as compiler optimisation. Now that we know what invariants are, we can apply this methodology to any protocol to verify that indeed the code is behaving as per the specification. Here we will only discuss the few liquidity net invariants for uniswap v3. Nevertheless, it will certainly give us a head start to understand properties and to write a few properties on our own for UniswapV3.

Add Liquidity 

This invariant is about minting liquidity. Minting in Uniswap v3 refers to providing liquidity to the pool by a liquidity provider. This invariant checks multiple properties such as:

    function check_mint_invariants(
        int24 _tickLower,
        int24 _tickUpper,
        UniswapMinter.MinterStats memory bfre,
        UniswapMinter.MinterStats memory aftr
    ) internal {
        (, int24 currentTick, , , , , ) = pool.slot0();

        // prop #1
        if (currentTick >= _tickLower && currentTick < _tickUpper) {
            assert(aftr.liq > bfre.liq);
        } else {
            assert(aftr.liq == bfre.liq);
        }

        // prop #2
        assert(aftr.tL_liqGross > bfre.tL_liqGross);

        // prop #3
        assert(aftr.tU_liqGross > bfre.tU_liqGross);

        // prop #4
        assert(aftr.tL_liqNet > bfre.tL_liqNet);

        // prop #5
        assert(aftr.tU_liqNet < bfre.tU_liqNet);
    }

Prop#1 Calling mint never leads to a decrease in liquidity

The first property checks that whenever the mint function is called, the liquidity will always increase. Else it remains the same.

Prop#2,3 Calling mint always leads to an increase in the LiquidityGross of tickLower and TickUpper

The l_g is the gross liquidity of protocol which should always increase at tickLower and tickUpper. This value ensures that even if net liquidity at a tick is 0, we can still know if a tick is referenced by at least one underlying position or not. So even if our current tick i_c is not in range and the total liquidity has been converted into one of our assets either X or Y. Calling mint at that tick will still increase the total asset liquidity. 

Prop#4 Calling mint always leads to an increase in LiquidityNet of tickLower

The LiquidityNet or ΔL is the delta change of a liquidity at a specific position. This value does not get updated when the tick is crossed rather when a position is updated. This means when adding and removing liquidity such as ΔL can be defined as:

\Delta L = LiquidityAfter - Liquidity Before

We can understand this concept with an example. Suppose an LP provider wants to add liquidity. This liquidity will get spread over all the ticks in the range. When the current tick is crossed we can only add liquidity in one token and we can calculate that liquidity by using these formulas:

\Delta L_x = \frac{\Delta x}{\frac{1}{\sqrt{P}-\sqrt{P_b}}}

\Delta L_y = \frac{\Delta y}{\sqrt{P}-\sqrt{P_a}}

Now to prove that liquidity has been added with an equal amount, the pool adds the liquidity at its tickLower with a positive value and on the other hand it adds the liquidity with a negative value to the tickUpper to make sure that the overall sum of liquidity should remain unchanged.

When liquidity is added to a specific tick range in Uniswap V3, the liquidityNet at tickLower increases (delta L is positive) because the LP is providing additional liquidity at that price level. However, the liquidityNet at tickUpper decreases (delta L is negative) because the added liquidity causes the tickUpper price level to shift closer to the current market price, leading to reduced liquidity within that tick range. This phenomenon allows Uniswap V3 to concentrate liquidity around the current market price and provides more targeted exposure to price movements for LPs.

Prop#5 Calling mint always leads to a decrease in LiquidityNet of tickUpper

Calling the mint function in Uniswap V3 increases the overall liquidity in the pool but decreases the liquidityNet of the tickUpper corresponding to the tick range where the liquidity is added. This is because the added liquidity shifts the tickUpper price level closer to the current market price, reducing the amount of liquidity within that tick range.

The reason for the decrease in liquidityNet at the tickUpper position is related to the way Uniswap V3's price curve works. The price curve in Uniswap V3 is constructed using a logarithmic function, which means that the price change between each tick is not linear. Instead, it becomes more significant as you move farther away from the center of the curve.

Remove Liquidity 

A liquidity burn operation occurs when a liquidity provider (LP) removes liquidity from the pool and closes its position. 

    function check_burn_invariants(
        uint128 _burnAmount,
        int24 _tickLower,
        int24 _tickUpper,
        uint128 _newPosAmount,
        UniswapMinter.MinterStats memory bfre,
        UniswapMinter.MinterStats memory aftr
    ) internal {
        (, int24 currentTick, , , , , ) = pool.slot0();

        if (_burnAmount > 0) {
            // prop #6
            if (currentTick >= _tickLower && currentTick < _tickUpper) {
                assert(aftr.liq < bfre.liq);
            } else {
                assert(aftr.liq == bfre.liq);
            }
        } else {
            assert(aftr.liq == bfre.liq);
        }

        // prop #7
        assert(aftr.tL_liqGross <= bfre.tL_liqGross);

        // prop #8
        assert(aftr.tU_liqGross <= bfre.tU_liqGross);

        // prop #9
        assert(aftr.tL_liqNet <= bfre.tL_liqNet);

        // prop #10
        assert(aftr.tU_liqNet >= bfre.tU_liqNet);

        bytes32 positionKey = keccak256(abi.encodePacked(address(minter), _tickLower, _tickUpper));
        (uint128 positionLiquidity, , , , ) = pool.positions(positionKey);

        // prop #11
        assert(positionLiquidity == _newPosAmount);
    }

Prop#6  Calling burn never leads to an increase in liquidity

This is a simple property which ensures that whenever the current tick is in range, then calling the burn function will result in lower liquidity than the liquidity before. Otherwise, it will remain the same or we could say that Calling burn with amount zero does not change the liquidity of the pool.

Prop#7,8 Calling burn never leads to an increase in LiquidityGross of tickLower and tickUpper

These properties ensure that whenever a burn function is called on a tick the overall gross liquidity for that tick will always decrease. For instance we have two positions: one in the range of 1 to 100 and the other from 1 to 50 with a tick spacing of 10. When we add liquidity in a defined range the pool spreads it on all the ticks in between the range. Now at tick 50 if we call a burn function for the position 1 that does not make the liquidity at tick 50 equals to 0. This is because another position exists at that tick which may not be equal to 0. Hence the gross liquidity should always decrease whenever we call a burn function. 

Prop#9, 10 Calling burn always leads to a decrease in LiquidityNet of tickLower while increase in tickUpper

When the burn function is called, liquidity is removed from the pool by burning the corresponding pool tokens. The burn will force the price to move towards the end of tick Upper and hence the liquidity must be concentrated at the end of tickUpper to compensate for the market demand. 

Prop#11 Burning x amount of a position always decreases position liquidity by x amount

This property first creates the position key for a LP provider using minter address and tick bounds. The total liquidity in the pool after the burn operation and the new position liquidity (_newPosAmount) should add up to the initial liquidity before the burn operation.

Liquidity Net

Prop#12 liquidityNet over all ticks should sum to zero

In Uniswap v3, LPs can supply liquidity within specific price ranges, represented by tick ranges. As a result, the net change in liquidity for each tick is a crucial factor in calculating the pool's overall liquidity. When we provide liquidity between a range of upper and lower tick say for this very example in between the range of 1 to 100 with a tick spacing of 10. The liquidity gets spread logarithmically on all the ticks in between these ranges. 

    function check_liquidityNet_invariant() internal {
        int128 liquidityNet = 0;
        for (uint256 i = 0; i < usedTicks.length; i++) {
            (, int128 tickLiquidityNet, , ) = pool.ticks(usedTicks[i]);
            int128 result = liquidityNet + tickLiquidityNet;
            assert(
                (tickLiquidityNet >= 0 && result >= liquidityNet) || (tickLiquidityNet < 0 && result < liquidityNet)
            );
            liquidityNet = result;
        }

        // prop #12
        assert(liquidityNet == 0);
    }

Now for the sake of explanation lets see the example of Eth/Usdt pool:

tl=10, tu=100, X=1200 Usdt, Y=1Eth

The liquidity can be calculate as l=x.y=34.6410161514

P(50)= 1.0025030023

P(90)= 1.0045099142

P(40)= 1.0020019011

Observe that at tick 50 the value is balanced and contains the equal amount of token X and Y. The more the tick moves towards the right its sqrt(P) value gets increased which indicates that the reserves of X are getting depleted and the reserves of Y are getting increased with a similar dollar value. The opposite will happen for the reverse direction of the tick. This means that at tick 60 and tick 40 the liquidity will be exactly similar but with different values of reserves hence canceling each other. 

By requiring that liquidity netting over all ticks sums to zero, Uniswap v3 promotes a stable and efficient market that reflects the true value of the assets being traded. This requirement also helps to prevent market manipulation by ensuring that no one trader or group of traders can influence the price of an asset by creating artificial imbalances in supply and demand.

Prop#13 liquidity is equal to the summation of liquidityNet for all ticks below and including the current tick

This invariant verifies that the sum of the net liquidity for all used ticks less than or equal to the current tick must always remain equal to the pool's total liquidity

   function check_liquidity_invariant() internal {
        (, int24 currentTick, , , , , ) = pool.slot0();

        int128 liquidity = 0;
        for (uint256 i = 0; i < usedTicks.length; i++) {
            int24 tick = usedTicks[i];

            if (tick <= currentTick) {
                (, int128 tickLiquidityNet, , ) = pool.ticks(tick);

                int128 result = liquidity + tickLiquidityNet;
                assert((tickLiquidityNet >= 0 && result >= liquidity) || (tickLiquidityNet < 0 && result < liquidity));
                liquidity = result;
            }
        }

        // prop #13
        assert(uint128(liquidity) == pool.liquidity());
        assert(liquidity >= 0);
    }

When a user adds funds to a pool, they are effectively providing liquidity to the pool. This liquidity is spread across multiple ticks, depending on the price of the token pair at the time of the addition. Therefore, to calculate the total liquidity in a Uniswap V3 pool at a given point in time, you need to sum up the liquidityNet for all ticks that fall below or equal to the current tick. 

The assert statement here first adds all the liquidity available from the used ticks and compares it to the pool liquidity which must always be equal. 

The given invariant certifies that whenever the liquidity is added or removed from the pool, the change should always be equal and justifiable. 

Prop#14 After mint calling inverse mint will always succeed

Since the mint operation generates and assigns liquidity tokens to the user, the inverse burn operation relies on these tokens to determine the user's share of the assets in the pool. As long as the user possesses the necessary liquidity tokens, they can call the burn operation successfully to redeem their assets. Because the user is entitled to the assets represented by those tokens.

    function test_burn_full(uint128 _amount) public {
        require(positions.length > 0);

        uint128 posIdx = _getRandomPositionIdx(_amount, positions.length);
        // console.log('burn posIdx = %s', posIdx);
        PoolPosition storage pos = positions[posIdx];

        UniswapMinter.MinterStats memory bfre;
        UniswapMinter.MinterStats memory aftr;

        try minter.doBurn(pos.tickLower, pos.tickUpper, pos.amount) returns (
            UniswapMinter.MinterStats memory bfre_burn,
            UniswapMinter.MinterStats memory aftr_burn
        ) {
            bfre = bfre_burn;
            aftr = aftr_burn;
        } catch {
            // prop #14
            assert(false);
        }

        check_burn_invariants(pos.amount, pos.tickLower, pos.tickUpper, 0, bfre, aftr);

        check_liquidityNet_invariant();
        check_liquidity_invariant();
        check_tick_feegrowth_invariant();

        removePosition(posIdx);
    }

The try statement executes the doBurn function from setup.sol and burns the position. Then It retrieves the minter stats of net and gross liquidity. If the doBurn for some reasons fails the catch statement will assert the false statement.

Prop#15 Max Liquidity at every tick should be less than the cap value

Ensuring that the maximum liquidity at every tick is less than or equal to the cap value is important for a couple of reasons. First allowing an unlimited amount of liquidity at each tick could lead to excessive capital allocation, which might not be efficient. It is also helpful for responsible liquidity provisioning and prevents overallocation of resources. This property helps Uniswap to better manage and mitigate potential risks associated with extreme price movements or manipulative activities.

    function checkTickSpacingToParametersInvariants(int24 tickSpacing) external pure {
        require(tickSpacing <= TickMath.MAX_TICK);
        require(tickSpacing > 0);

        int24 minTick = (TickMath.MIN_TICK / tickSpacing) * tickSpacing;
        int24 maxTick = (TickMath.MAX_TICK / tickSpacing) * tickSpacing;

        uint128 maxLiquidityPerTick = Tick.tickSpacingToMaxLiquidityPerTick(tickSpacing);

        // symmetry around 0 tick
        assert(maxTick == -minTick);
        // positive max tick
        assert(maxTick > 0);
        // divisibility
        assert((maxTick - minTick) % tickSpacing == 0);

        uint256 numTicks = uint256((maxTick - minTick) / tickSpacing) + 1;
        // max liquidity at every tick is less than the cap
        assert(uint256(maxLiquidityPerTick) * numTicks <= type(uint128).max);
    }

The assert statement at the end first converts the unit128 maxLiquidityPerTick into uint256 to avoid overflow flags. It then multiplies the maxLiquidityPerTick to numTicks to ensure that the function reverts whenever its multiplication result reaches over the max value of uint128. This ensures that the total liquidity allocated across all ticks remains within the acceptable range and prevents potential overflow issues.

Final Thoughts

The above properties enable us to ensure that the net liquidity supplied by LPs is balanced by the liquidity removed as the price moves across different tick ranges. It also checks the change in liquidity at each tick. 

By ensuring the liquidity properties across all used ticks, the invariant guarantees that LPs receive their rightful share of the fees generated by the pool. 

Also read, Dissecting The MEV Attack: How a Validator Exploited The MEV-BOOST-RELAY Bug To Drain Multiple MEV Bots.