|
| 1 | +## Implementation of `f` |
| 2 | + |
| 3 | +`f` (aka the "EulerSwap Function") is a parameterisable curve that defines the boundary of permissible points for EulerSwap AMMs. Points on the curve or above and to-the right are allowed, others are not. |
| 4 | + |
| 5 | +Only formula 3 from the whitepaper is implemented in the EulerSwap core, since this can be used for both domains of the curve by mirroring the parameters. The more complicated formula 4 is a closed-form method for quoting swaps so it can be implemented in a periphery (if desired). |
| 6 | + |
| 7 | +### Derivation |
| 8 | + |
| 9 | +Formula 3 from the whitepaper: |
| 10 | + |
| 11 | + y0 + (px / py) * (x0 - x) * (c + (1 - c) * (x0 / x)) |
| 12 | + |
| 13 | +Multiply second term by `x/x`: |
| 14 | + |
| 15 | + y0 + (px / py) * (x0 - x) * ((c * x) + (1 - c) * x0) / x |
| 16 | + |
| 17 | +`c` is scaled by `1e18`: |
| 18 | + |
| 19 | + y0 + (px / py) * (x0 - x) * ((c * x) + (1e18 - c) * x0) / (x * 1e18) |
| 20 | + |
| 21 | +Re-order division by `py`: |
| 22 | + |
| 23 | + y0 + px * (x0 - x) * ((c * x) + (1e18 - c) * x0) / (x * 1e18) / py |
| 24 | + |
| 25 | +Use `mulDiv` to avoid intermediate overflow: |
| 26 | + |
| 27 | + y0 + Math.mulDiv(px * (x0 - x), c * x + (1e18 - c) * x0, x * 1e18) / py |
| 28 | + |
| 29 | +Round up for both divisions (operation is distributive): |
| 30 | + |
| 31 | + y0 + (Math.mulDiv(px * (x0 - x), c * x + (1e18 - c) * x0, x * 1e18, Math.Rounding.Ceil) + (py-1)) / py |
| 32 | + |
| 33 | +### Boundary Analysis |
| 34 | + |
| 35 | +Pre-conditions: x <= x0, 1 <= {px,py} <= 1e36, {x0,y0} <= type(uint112).max, c <= 1e18 |
| 36 | + |
| 37 | +None of the computations for the arguments to `mulDiv` can overflow: |
| 38 | + |
| 39 | +* Arg 1: `px * (x0 - x)` |
| 40 | + * Upper-bound: `1e36*(2**112 - 1) =~ 232 bits` |
| 41 | +* Arg 2: `c * x + (1e18 - c) * x0` |
| 42 | + * Upper-bound: `1e18*(2**112 - 1)*2 =~ 173 bits` |
| 43 | +* Arg 3: `x * 1e18` |
| 44 | + * Upper-bound: `1e18*(2**112 - 1) =~ 172 bits` |
| 45 | + |
| 46 | +If amounts/prices are large, and we travel too far down the curve, then `mulDiv` (or the subsequent `y0` addition) could overflow because its output value cannot be represented as a `uint256`. However, these output values would never be valid anyway, because they exceed `type(uint112).max`. |
| 47 | + |
| 48 | +To see this, consider the case where `mulDiv` fails due to overflow. This means that its result would've been greater than `2**256 - 1`. Dividing this value by the largest allowed value for `py` (`1e36`) gives approximately `2**136`, which is greater than the maximum allowed amount value of `2**112 - 1`. Both the rounding up operation and the final addition of `y0` can only further *increase* this value. This means that all cases where `mulDiv` or the subsequent additions overflow would involve `f()` returning values that are impossible for a swapper to satisfy, so they would revert anyways. |
| 49 | + |
| 50 | +### Unchecked Math |
| 51 | + |
| 52 | +As-per the previous section, none of the computations of the arguments to `mulDiv` can overflow. To prevent overflows in the remaining operations, the `mulDiv` output is further restricted to `2**248 - 1`: |
| 53 | + |
| 54 | + unchecked { |
| 55 | + uint256 v = Math.mulDiv(px * (x0 - x), c * x + (1e18 - c) * x0, x * 1e18, Math.Rounding.Ceil); |
| 56 | + require(v <= type(uint248).max, Overflow()); |
| 57 | + return y0 + (v + (py - 1)) / py; |
| 58 | + } |
| 59 | + |
| 60 | +Note that this does not change the analysis of the previous section: Values between `2**248 - 1` and `2**256 - 1` will also never reduce down to the required `2**112 - 1`, so this does not cause any additional failure cases. |
0 commit comments