Adding UniswapV2 properties

[tuturu-tech]

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 crytic/echidna#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

[aviggiano]

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.

[aviggiano]

This may revert with an underflow, as the high parameter of the _between function inToken.balanceOf(address(user)) can be 0, while low is 1.

I believe it is necessary to add a require(inToken.balanceOf(user) >= 1); before this