crytic
Adding UniswapV2 properties
Initial draft of UniswapV2 basic properties.
Providing liquidity
- always increases K
- always increases LP token supply
- always increases user LP token supply
- never impacts token prices
- always increases token reserves
Withdrawing liquidity
- always decreases K
- always decreases LP token supply
- always decreases user LP token supply
- never impacts token prices
- always decreases token reserves
Swapping
- never decreases K
- swapping in both directions does not result in tokens gained
- always increases user token out balance
- price of tokenIn always decreases
- price of tokenOut always increases
Blockers: Properties fail with ErrorUnrecognizedOpcode https://github.com/crytic/echidna/issues/984, so far haven't been able to figure out why
Cons: Only tests UniswapV2 pair and router. Next step will be to generalize this so the properties can be easily used in a harness for testing UniV2-based AMMs
Hi, This is a great feature, I'm excited to try this out.
By the way, while working on a fuzzer comparison, I noticed that "Withdrawing liquidity always decreases LP token supply" is not always true:
When the feeTo address is on, withdrawing liquidity can increase the total supply of LP tokens. This is because UniswapV2Pair.burn can trigger a UniswapV2Pair._mint, so depending on the amount minted/burned the net effect can be either positive or negative.
