Skip to content

Commit 61bdd1e

Browse files
Merge pull request #41 from euler-xyz/doc-improvements
Doc improvements
2 parents bbfa037 + 3035a51 commit 61bdd1e

File tree

20 files changed

+1325
-66
lines changed

20 files changed

+1325
-66
lines changed

README.md

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,12 @@ forge test
4242
forge coverage
4343
```
4444

45+
## Smart Contracts Documentation
46+
47+
```sh
48+
forge doc --serve --port 4000
49+
```
50+
4551
## Safety
4652

4753
This software is experimental and is provided "as is" and "as available".

docs/boundary-analysis.md

Lines changed: 138 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,138 @@
1+
# Boundary analysis
2+
3+
## Introduction
4+
5+
The EulerSwap automated market maker (AMM) curve is governed by two key functions: f() and fInverse(). These functions are critical to maintaining protocol invariants and ensuring accurate swap calculations within the AMM. This document provides a detailed boundary analysis of both functions, assessing their Solidity implementations against the equations in the white paper. It ensures that appropriate safety measures are in place to avoid overflow, underflow, and precision loss, and that unchecked operations are thoroughly justified.
6+
7+
## Implementation of function `f()`
8+
9+
The `f()` function is part of the EulerSwap core, defined in `EulerSwap.sol`, and corresponds to equation (2) in the EulerSwap white paper. The `f()` function is a parameterisable curve in the `EulerSwap` contract that defines the permissible boundary for points in EulerSwap AMMs. The curve allows points on or above and to the right of the curve while restricting others. Its primary purpose is to act as an invariant validator by checking if a hypothetical state `(x, y)` within the AMM is valid. It also calculates swap output amounts for given inputs, though some swap scenarios require `fInverse()`.
10+
11+
### Derivation
12+
13+
This derivation shows how to implement the `f()` function in Solidity, starting from the theoretical model described in the EulerSwap white paper. The initial equation from the EulerSwap white paper is:
14+
15+
\[
16+
y_0 + \left(\frac{p_x}{p_y}\right) (x_0 - x) \left(c + (1 - c) \frac{x_0}{x}\right)
17+
\]
18+
19+
Multiply the second term by \(\frac{x}{x}\) and scale `c` by \(1e18\):
20+
21+
\[
22+
y_0 + \left(\frac{p_x}{p_y}\right) (x_0 - x) \frac{(c \cdot x) + (1e18 - c) \cdot x_0}{x \cdot 1e18}
23+
\]
24+
25+
Reorder division by \(p_y\) to prepare for Solidity implementation:
26+
27+
\[
28+
y_0 + p_x \cdot (x_0 - x) \cdot \frac{(c \cdot x) + (1e18 - c) \cdot x_0}{x \cdot 1e18} \cdot \frac{1}{p_y}
29+
\]
30+
31+
To avoid intermediate overflow, use `Math.mulDiv` in Solidity, which combines multiplication and division safely:
32+
33+
\[
34+
y_0 + \frac{\text{Math.mulDiv}(p_x \cdot (x_0 - x), c \cdot x + (1e18 - c) \cdot x_0, x \cdot 1e18)}{p_y}
35+
\]
36+
37+
Applying ceiling rounding with `Math.Rounding.Ceil` ensures accuracy:
38+
39+
\[
40+
y_0 + \left(\text{Math.mulDiv}(p_x \cdot (x_0 - x), c \cdot x + (1e18 - c) \cdot x_0, x \cdot 1e18, \text{Math.Rounding.Ceil}) + (p_y - 1)\right) / p_y
41+
\]
42+
43+
Adding `(p_y - 1)` ensures proper ceiling rounding by making sure the result is rounded up when the numerator is not perfectly divisible by `p_y`.
44+
45+
### Boundary analysis
46+
47+
#### Pre-conditions
48+
49+
- \(x \leq x_0\)
50+
- \(1e18 \leq p_x, p_y \leq 1e36\) (60 to 120 bits)
51+
- \(1 \leq x_0, y_0 \leq 2^{112} - 1 \approx 5.19e33\) (0 to 112 bits)
52+
- \(1 < c \leq 1e18\) (0 to 60 bits)
53+
54+
#### Step-by-step
55+
56+
The arguments to `mulDiv` are safe from overflow:
57+
58+
- **Arg 1:** `px * (x0 - x)``1e36 * (2**112 - 1)` ≈ 232 bits
59+
- **Arg 2:** `c * x + (1e18 - c) * x0``1e18 * (2**112 - 1) * 2` ≈ 173 bits
60+
- **Arg 3:** `x * 1e18``1e18 * (2**112 - 1)` ≈ 172 bits
61+
62+
If `mulDiv` or the addition with `y0` overflows, the result would exceed `type(uint112).max`. When `mulDiv` overflows, its result would be > `2**256 - 1`. Dividing by `py` (`1e36` max) gives ~`2**136`, which exceeds the `2**112 - 1` limit, meaning these results are invalid as they cannot be satisfied by any swapper.
63+
64+
#### Unchecked math considerations
65+
66+
The arguments to `mulDiv` are protected from overflow as demonstrated above. The `mulDiv` output is further limited to `2**248 - 1` to prevent overflow in subsequent operations:
67+
68+
```solidity
69+
unchecked {
70+
uint256 v = Math.mulDiv(px * (x0 - x), c * x + (1e18 - c) * x0, x * 1e18, Math.Rounding.Ceil);
71+
require(v <= type(uint248).max, Overflow());
72+
return y0 + (v + (py - 1)) / py;
73+
}
74+
```
75+
76+
This does not introduce additional failure cases. Even values between `2**248 - 1` and `2**256 - 1` would not reduce to `2**112 - 1`, aligning with the boundary analysis.
77+
78+
## Implementation of function `fInverse()`
79+
80+
The `fInverse()` function, defined in `EulerSwapPeriphery.sol`, is part of the periphery because it is not required as an invariant. Instead, its sole purpose is to facilitate specific swap input and output calculations that cannot be managed by `f()`. This function maps to equation (22) in the Appendix of the EulerSwap white paper.
81+
82+
### Boundary analysis
83+
84+
#### Pre-conditions
85+
86+
- \(y > y_0\)
87+
- \(1e18 \leq p_x, p_y \leq 1e36\) (60 to 120 bits)
88+
- \(1 \leq x_0, y_0 \leq 2^{112} - 1 \approx 5.19e33\) (0 to 112 bits)
89+
- \(1 < c \leq 1e18\) (0 to 60 bits)
90+
91+
#### Step-by-step
92+
93+
1. **A component (`A = 2 * c`)**
94+
95+
- Since `c <= 1e18`, `A = 2 * c <= 2e18`, well within `uint256` capacity (max `2**256 - 1`).
96+
97+
2. **B component calculation**
98+
99+
- `B = int256((px * (y - y0) + py - 1) / py) - int256((x0 * (2 * c - 1e18) + 1e18 - 1) / 1e18)`
100+
- The first term is bounded by `(px * (y - y0)) / py`, where `px, py <= 1e36` and `(y - y0) <= 2**112 - 1`.
101+
- The second term scales `x0` with `(2 * c - 1e18)`, keeping the result well within the `int256` bounds due to controlled arithmetic and the limits on `c` and `x0`.
102+
103+
3. **Absolute value and B² computation**
104+
105+
- `absB = B < 0 ? uint256(-B) : uint256(B)`
106+
- `squaredB = Math.mulDiv(absB, absB, 1e18, Math.Rounding.Ceil)`
107+
- As `absB` is derived from `B`, and `B` is bounded, `squaredB` remains within a safe range.
108+
109+
4. **4AC Component (`AC4 = AC4a * AC4b / 1e18`)**
110+
111+
- `AC4a = Math.mulDiv(4 * c, (1e18 - c), 1e18, Math.Rounding.Ceil)`
112+
- `4 * c * (1e18 - c)` has a maximum of `1e18 * 1e18 = 1e36`, divided by `1e18`, the result ≤ `1e18`.
113+
- `AC4b = Math.mulDiv(x0, x0, 1e18, Math.Rounding.Ceil)`
114+
- The maximum value of `x0 * x0` is `(2**112 - 1)² ≈ 2**224`, safely within the `uint256` range.
115+
116+
5. **Discriminant calculation**
117+
118+
- `discriminant = (squaredB + AC4) * 1e18`
119+
- Since both `squaredB` and `AC4` are bounded by `uint256`, multiplying by `1e18` does not cause overflow.
120+
121+
6. **Square root computation and adjustment**
122+
123+
- `uint256 sqrt = Math.sqrt(discriminant)`
124+
- The square root of a `uint256` value is always within `uint128`, making this operation safe.
125+
- Adjustment step `sqrt = (sqrt * sqrt < discriminant) ? sqrt + 1 : sqrt` maintains precision without overflow.
126+
127+
7. **Final computation of `x`**
128+
- `Math.mulDiv(uint256(int256(sqrt) - B), 1e18, A, Math.Rounding.Ceil)`
129+
- The subtraction and multiplication are controlled by previous bounds, ensuring no overflow.
130+
- Division by `A` is safe as `A` is non-zero and small (`≤ 2e18`).
131+
132+
#### Unchecked math considerations
133+
134+
As above, the use of unchecked arithmetic is safe because all inputs are bounded by pre-conditions.
135+
136+
## Conclusion
137+
138+
The `f()` and `fInverse()` functions of EulerSwap are implemented with rigorous safety measures, using `Math.mulDiv` for safe arithmetic and applying ceiling rounding to maintain precision. Boundary analysis shows that all potential overflow scenarios are precluded by pre-condition checks and bounded operations, justifying the use of unchecked math in the Solidity implementation.

docs/f.md

Lines changed: 0 additions & 60 deletions
This file was deleted.

foundry-docs/.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
book/

foundry-docs/book.css

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
table {
2+
margin: 0 auto;
3+
border-collapse: collapse;
4+
width: 100%;
5+
}
6+
7+
table td:first-child {
8+
width: 15%;
9+
}
10+
11+
table td:nth-child(2) {
12+
width: 25%;
13+
}

foundry-docs/book.toml

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
[book]
2+
src = "src"
3+
title = "Euler Swap Contracts Documentation"
4+
5+
[output.html]
6+
no-section-label = true
7+
additional-js = ["solidity.min.js"]
8+
additional-css = ["book.css"]
9+
git-repository-url = "https://github.com/euler-xyz/euler-maglev"
10+
11+
[output.html.fold]
12+
enable = true

foundry-docs/solidity.min.js

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
hljs.registerLanguage("solidity",(()=>{"use strict";function e(){try{return!0
2+
}catch(e){return!1}}
3+
var a=/-?(\b0[xX]([a-fA-F0-9]_?)*[a-fA-F0-9]|(\b[1-9](_?\d)*(\.((\d_?)*\d)?)?|\.\d(_?\d)*)([eE][-+]?\d(_?\d)*)?|\b0)(?!\w|\$)/
4+
;e()&&(a=a.source.replace(/\\b/g,"(?<!\\$)\\b"));var s={className:"number",
5+
begin:a,relevance:0},n={
6+
keyword:"assembly let function if switch case default for leave break continue u256 jump jumpi stop return revert selfdestruct invalid",
7+
built_in:"add sub mul div sdiv mod smod exp not lt gt slt sgt eq iszero and or xor byte shl shr sar addmod mulmod signextend keccak256 pc pop dup1 dup2 dup3 dup4 dup5 dup6 dup7 dup8 dup9 dup10 dup11 dup12 dup13 dup14 dup15 dup16 swap1 swap2 swap3 swap4 swap5 swap6 swap7 swap8 swap9 swap10 swap11 swap12 swap13 swap14 swap15 swap16 mload mstore mstore8 sload sstore msize gas address balance selfbalance caller callvalue calldataload calldatasize calldatacopy codesize codecopy extcodesize extcodecopy returndatasize returndatacopy extcodehash create create2 call callcode delegatecall staticcall log0 log1 log2 log3 log4 chainid origin gasprice basefee blockhash coinbase timestamp number difficulty gaslimit",
8+
literal:"true false"},i={className:"string",
9+
begin:/\bhex'(([0-9a-fA-F]{2}_?)*[0-9a-fA-F]{2})?'/},t={className:"string",
10+
begin:/\bhex"(([0-9a-fA-F]{2}_?)*[0-9a-fA-F]{2})?"/};function r(e){
11+
return e.inherit(e.APOS_STRING_MODE,{begin:/(\bunicode)?'/})}function l(e){
12+
return e.inherit(e.QUOTE_STRING_MODE,{begin:/(\bunicode)?"/})}var o={
13+
SOL_ASSEMBLY_KEYWORDS:n,baseAssembly:e=>{
14+
var a=r(e),o=l(e),c=/[A-Za-z_$][A-Za-z_$0-9.]*/,d=e.inherit(e.TITLE_MODE,{
15+
begin:/[A-Za-z$_][0-9A-Za-z$_]*/,lexemes:c,keywords:n}),u={className:"params",
16+
begin:/\(/,end:/\)/,excludeBegin:!0,excludeEnd:!0,lexemes:c,keywords:n,
17+
contains:[e.C_LINE_COMMENT_MODE,e.C_BLOCK_COMMENT_MODE,a,o,s]},_={
18+
className:"operator",begin:/:=|->/};return{keywords:n,lexemes:c,
19+
contains:[a,o,i,t,e.C_LINE_COMMENT_MODE,e.C_BLOCK_COMMENT_MODE,s,_,{
20+
className:"function",lexemes:c,beginKeywords:"function",end:"{",excludeEnd:!0,
21+
contains:[d,u,e.C_LINE_COMMENT_MODE,e.C_BLOCK_COMMENT_MODE,_]}]}},
22+
solAposStringMode:r,solQuoteStringMode:l,HEX_APOS_STRING_MODE:i,
23+
HEX_QUOTE_STRING_MODE:t,SOL_NUMBER:s,isNegativeLookbehindAvailable:e}
24+
;const{baseAssembly:c,solAposStringMode:d,solQuoteStringMode:u,HEX_APOS_STRING_MODE:_,HEX_QUOTE_STRING_MODE:m,SOL_NUMBER:b,isNegativeLookbehindAvailable:E}=o
25+
;return e=>{for(var a=d(e),s=u(e),n=[],i=0;i<32;i++)n[i]=i+1
26+
;var t=n.map((e=>8*e)),r=[];for(i=0;i<=80;i++)r[i]=i
27+
;var l=n.map((e=>"bytes"+e)).join(" ")+" ",o=t.map((e=>"uint"+e)).join(" ")+" ",g=t.map((e=>"int"+e)).join(" ")+" ",M=[].concat.apply([],t.map((e=>r.map((a=>e+"x"+a))))),p={
28+
keyword:"var bool string int uint "+g+o+"byte bytes "+l+"fixed ufixed "+M.map((e=>"fixed"+e)).join(" ")+" "+M.map((e=>"ufixed"+e)).join(" ")+" enum struct mapping address new delete if else for while continue break return throw emit try catch revert unchecked _ function modifier event constructor fallback receive error virtual override constant immutable anonymous indexed storage memory calldata external public internal payable pure view private returns import from as using pragma contract interface library is abstract type assembly",
29+
literal:"true false wei gwei szabo finney ether seconds minutes hours days weeks years",
30+
built_in:"self this super selfdestruct suicide now msg block tx abi blockhash gasleft assert require Error Panic sha3 sha256 keccak256 ripemd160 ecrecover addmod mulmod log0 log1 log2 log3 log4"
31+
},O={className:"operator",begin:/[+\-!~*\/%<>&^|=]/
32+
},C=/[A-Za-z_$][A-Za-z_$0-9]*/,N={className:"params",begin:/\(/,end:/\)/,
33+
excludeBegin:!0,excludeEnd:!0,lexemes:C,keywords:p,
34+
contains:[e.C_LINE_COMMENT_MODE,e.C_BLOCK_COMMENT_MODE,a,s,b,"self"]},f={
35+
begin:/\.\s*/,end:/[^A-Za-z0-9$_\.]/,excludeBegin:!0,excludeEnd:!0,keywords:{
36+
built_in:"gas value selector address length push pop send transfer call callcode delegatecall staticcall balance code codehash wrap unwrap name creationCode runtimeCode interfaceId min max"
37+
},relevance:2},y=e.inherit(e.TITLE_MODE,{begin:/[A-Za-z$_][0-9A-Za-z$_]*/,
38+
lexemes:C,keywords:p}),w={className:"built_in",
39+
begin:(E()?"(?<!\\$)\\b":"\\b")+"(gas|value|salt)(?=:)"};function x(e,a){return{
40+
begin:(E()?"(?<!\\$)\\b":"\\b")+e+"\\.\\s*",end:/[^A-Za-z0-9$_\.]/,
41+
excludeBegin:!1,excludeEnd:!0,lexemes:C,keywords:{built_in:e+" "+a},
42+
contains:[f],relevance:10}}var h=c(e),v=e.inherit(h,{
43+
contains:h.contains.concat([{begin:/\./,end:/[^A-Za-z0-9$.]/,excludeBegin:!0,
44+
excludeEnd:!0,keywords:{built_in:"slot offset length address selector"},
45+
relevance:2},{begin:/_/,end:/[^A-Za-z0-9$.]/,excludeBegin:!0,excludeEnd:!0,
46+
keywords:{built_in:"slot offset"},relevance:2}])});return{aliases:["sol"],
47+
keywords:p,lexemes:C,
48+
contains:[a,s,_,m,e.C_LINE_COMMENT_MODE,e.C_BLOCK_COMMENT_MODE,b,w,O,{
49+
className:"function",lexemes:C,
50+
beginKeywords:"function modifier event constructor fallback receive error",
51+
end:/[{;]/,excludeEnd:!0,
52+
contains:[y,N,w,e.C_LINE_COMMENT_MODE,e.C_BLOCK_COMMENT_MODE],illegal:/%/
53+
},x("msg","gas value data sender sig"),x("block","blockhash coinbase difficulty gaslimit basefee number timestamp chainid"),x("tx","gasprice origin"),x("abi","decode encode encodePacked encodeWithSelector encodeWithSignature encodeCall"),x("bytes","concat"),f,{
54+
className:"class",lexemes:C,beginKeywords:"contract interface library",end:"{",
55+
excludeEnd:!0,illegal:/[:"\[\]]/,contains:[{beginKeywords:"is",lexemes:C
56+
},y,N,w,e.C_LINE_COMMENT_MODE,e.C_BLOCK_COMMENT_MODE]},{lexemes:C,
57+
beginKeywords:"struct enum",end:"{",excludeEnd:!0,illegal:/[:"\[\]]/,
58+
contains:[y,e.C_LINE_COMMENT_MODE,e.C_BLOCK_COMMENT_MODE]},{
59+
beginKeywords:"import",end:";",lexemes:C,keywords:"import from as",
60+
contains:[y,a,s,_,m,e.C_LINE_COMMENT_MODE,e.C_BLOCK_COMMENT_MODE,O]},{
61+
beginKeywords:"using",end:";",lexemes:C,keywords:"using for",
62+
contains:[y,e.C_LINE_COMMENT_MODE,e.C_BLOCK_COMMENT_MODE,O]},{className:"meta",
63+
beginKeywords:"pragma",end:";",lexemes:C,keywords:{
64+
keyword:"pragma solidity experimental abicoder",
65+
built_in:"ABIEncoderV2 SMTChecker v1 v2"},
66+
contains:[e.C_LINE_COMMENT_MODE,e.C_BLOCK_COMMENT_MODE,e.inherit(a,{
67+
className:"meta-string"}),e.inherit(s,{className:"meta-string"})]},{
68+
beginKeywords:"assembly",end:/\b\B/,
69+
contains:[e.C_LINE_COMMENT_MODE,e.C_BLOCK_COMMENT_MODE,e.inherit(v,{begin:"{",
70+
end:"}",endsParent:!0,contains:v.contains.concat([e.inherit(v,{begin:"{",
71+
end:"}",contains:v.contains.concat(["self"])})])})]}],illegal:/#/}}})());
72+
73+
// Ugly hack to reload HLJS
74+
hljs.initHighlightingOnLoad();

0 commit comments

Comments
 (0)