Enforce reserve amounts amounts strictly positive #290
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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
andreserve_b = 0
(or vice-versa). See the test in commit1338a7c
for a scenario that leads to this viadeposit
. 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 commit3b1da32
.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