[amm] Prove construction safety for "hTokenOutForUnderlyingIn" and "underlyingOutForHTokenIn"

[PaulRBerg]

Problem Statement

In the hTokenOutForUnderlyingIn and the underlyingOutForHTokenIn functions, the last operation is a subtraction:

hTokenOut = hTokenReserves - newHTokenReserves;

And:

normalizedUnderlyingOut = normalizedUnderlyingReserves - newNormalizedUnderlyingReserves;

The task is to derive a mathematical proof that it is not possible for this subtraction to revert.

Suggestions

• Hack around with Mathematica. Build on top of my set of inequalities.
• Use Echidna to fuzz the inputs and see if the fuzzer can find anything. Add an "assert" statement to let Echidna know that "hTokenReserves" must be greater than or equal to "newHTokenReserves", ditto for the other two vars.

[PaulRBerg]

Note that since this hasn't been proved mathematically yet, I added a require statement right before the last operation of both "hTokenOutForUnderlyingIn" and "underlyingOutForHTokenIn". But I didn't write tests that cover this require branch because I don't know any inputs which can trigger it.

[PaulRBerg]

Benson worked on this and came up with a beautiful explanation for why this construction is safe in the realm of pure mathematics. Now the question is to prove whether Solidity’s inevitable rounding errors don’t break the purely mathematical logic.

Construction_Safety_for_OutForIn_Functions.pdf