Enforce reserve amounts amounts strictly positive

[dranov]

What

This adds a check to the Liquidity Pool deposit method to ensure that both deposited amounts are strictly positive. This ensures the reserves after a (successful) deposit are both strictly positive.

It also adds a check in swap to ensure that the reserves remain strictly positive after a swap.

Why

Without the checks, it is possible to get in a situation where reserve_a > 0 and reserve_b = 0 (or vice-versa). See the test in commit 1338a7c for a scenario that leads to this via deposit. This leads to all further deposits panicking due to a divide-by-zero error on line 241/242. (This only happens if the malfeasant deposit is the first one; if the contract is otherwise properly initialized, things are OK, so this is not very serious.)

A similar thing can happen via swap, as shown by the test in commit 3b1da32.

More generally, though, it seems that the contract is written to assume in several places that reserve_a > 0 && reserve_b > 0 is an appropriate way to check that the contract has been successfully initialised. For instance, this check shows up on L133 and L240. This change actually enforces that assumption.

Known limitations

We came up with these checks whilst formally verifying the Liquidity Pool example contract in this repo.

We have NOT yet established that the property these checks are enforcing (that reserves are both 0 or both strictly positive) is maintained by the withdraw transition. It might be the case that a similar check is necessary there.

@nano-o

[dranov]

I've pushed a new test case that shows the panic issue for all deposits being produced via a swap (rather than via a deposit), and a change to swap that ensures this doesn't happen.

It's not yet clear to me whether a similar check is needed for withdraw.