Invariants

​

Pool initialization

• Calls to initializePool can only be done successfully once in the lifetime of a pool.

​

Liquidity Invariants

• Removing liquidity doesn’t impact the price.
• Adding liquidity doesn’t impact the price.
• Liquidity can only be added in the proportions dictated by the pool.
• After the pool initialization , deposits of liquidity on an inactive position will revert.

​

Fees and Revenue

• Revenue accrued by the pool can only increase over time.
• Calls to withdrawRevenue never lead to a decrease of liquidity.
• Calls to collectProtocolFees can never lead to a decrease of liquidity.

​

Authorization Invariants

• Calls to enableSwaps by any address that is not the contract owner will revert.
• Calls to setLPFee by any address that is not the contract owner will revert.
• Calls to initializePool by any address that is not the contract owner will revert.
• Calls to depositLiquidity on a position NFT by any address that is not the owner of that position NFT will revert.
• Calls to withdrawPartialLiquidity or withdrawAllLiquidity by any address that is not the owner of the position NFT will revert.
• Calls to depositLiquidity while the contract is paused will revert.
• Calls to swap while the contract is paused will revert.

​

Swap Invariants

• A swap resulting in an amount out of Token X higher than the AMM’s current xMAx will revert.
• After initialization of the AMM all swaps selling Token X to the pool will fail until the first swap selling Token Y to the pool takes place.
• After a swap selling X to the AMM, the AMM’s tracked X value will decrease by the amount sold.
• After a swap buying X from the AMM, the AMM’s tracked X value will increase by the amount bought.
• After a swap selling Y to the AMM, the AMM’s tracked X value will increase by the amount out.
• After a swap buying Y from the AMM, the AMM’s tracked X value will decrease by the amount out.
• The price (f(x)) will never drop below the Minimum Price set during the AMM’s initialization.
• The price (f(x)) will never go above the Maximum Price set during the AMM’s inialization.
• The price (f(x)) at a position on the x axis $x_{p}$ at a given time will never be lower in future Occasions where x happens to be $x_{p}$ again.
• The price (f(x)) can never decrease when x increases.