Help me understand why we use 2 different invariants when adding liquidity & swapping tokens ?

[TilakMaddy]

Purely by looking at the source code for TSwapPool.sol I infer the following:

For swapping tokens we maintain x * y = k

but when it comes to adding liquidity, we try to maintain x / y = C

why do we do that ? and how does the whole math workout?

[PatrickAlphaC]

Where do we do that?

And a few times we do some advanced algebra to derive equations from the y * x = k equation.

[TilakMaddy]

I got my question answered after going through the formal verification paper here

x * y = k is not true throughout the lifetime of the contract. Otherwise, you could never add extra money (for either token - x or y) without removing some from the other (how else would you have a product of two non-negative numbers be constant, right?). Therefore when it comes to adding liquidity, the value of x * y is expected to strictly increase.

The invariant in this situation is the ratio e:t:l (e -> ether, t -> exchange token, l -> total liquidity amount). Say you want to provide Δe to liquidity pool, in order to preserve the e:t:l ratio they also expect you to provide alpha * t to t and, in turn you will be minted alpha * l.

where alpha = e / Δe

This is enforced in TSwap.sol here

However, when it comes to swapping, the invariant is x * y = k

[shobhit-gupta]

@TilakMaddy Thank you for the explanation & the link to the verification paper.