spec: echidna tests for bigint precision

Author: sambacha

src/main.tex

@@ -1,6 +1,7 @@
 \documentclass[runningheads]{llncs}
 %
 \usepackage{graphicx}
+\usepackage{minted}
 %
 % If you use the hyperref package, please uncomment the following line
 % to display URLs in blue roman font according to Springer's eBook style:
@@ -239,6 +240,192 @@ \section{Liquidity Execution}
 
 \section{Equivalence Checking}
 
+Backrun placement
+
+By definition, backruns must occur after user to user swap. From a design point of view the simplest place to insert the backrun function would be in the internal `_swap` function which is called by the other swaps. However, some of the swap variants eg `swapTokensForExactETH` perform user actions after `_swap` is called. This is not ideal, as we do not want to interfere with the user swap. Moreover, other swap variants such as `swapExactTokensForTokensSupportingFeeOnTransferTokens` do not use `_swap`. Backrun functions were therefore placed at the end of each external swap variant. E.g.
+
+Original
+\begin{minted}{javascript}{javascript}
+\label{Before swapExactTokensforTokens:1}
+    function swapExactTokensForTokens(
+        uint amountIn,
+        uint amountOutMin,
+        address[] calldata path,
+        address to,
+        uint deadline
+    ) external virtual override ensure(deadline) returns (uint[] memory amounts) {
+        amounts = UniswapV2Library.getAmountsOut(factory, amountIn, path);
+        require(amounts[amounts.length - 1] >= amountOutMin, 'UniswapV2Router: INSUFFICIENT_OUTPUT_AMOUNT');
+        TransferHelper.safeTransferFrom(
+            path[0], msg.sender, UniswapV2Library.pairFor(factory, path[0], path[1]), amounts[0]
+        );
+        _swap(amounts, path, to);
+    }
+\end{minted}
+
+Design change:
+
+\begin{minted}{javascript}
+\label{After swapExactTokensforTokens:2}
+function swapExactTokensForTokens(
+    uint amountIn,
+    uint amountOutMin,
+    address[] calldata path,
+    address to,
+    uint deadline
+) external virtual override ensure(deadline) returns (uint[] memory amounts) {
+    amounts = UniswapV2Library.getAmountsOut(factory, amountIn, path);
+    require(amounts[amounts.length - 1] >= amountOutMin, 'UniswapV2Router: INSUFFICIENT_OUTPUT_AMOUNT');
+    TransferHelper.safeTransferFrom(
+        path[0], msg.sender, UniswapV2Library.pairFor(factory, path[0], path[1]), amounts[0]
+    );
+    _swap(amounts, path, to);
+    _backrunSwaps(path);
+}
+\end{minted}
+
+Multiple factories
+Multiple factories (at least 2) are required for the backrun arbitrage. The adoption of multiple factories within the router, lead to some internal function changes. In particular `pairFor`.
+
+\begin{minted}{javascript}
+\label{CREATE2 Factory:3}
+// calculates the CREATE2 address for a pair without making any external calls
+function pairFor(address factory, address tokenA, address tokenB) internal pure returns (address pair) {
+(address token0, address token1) = sortTokens(tokenA, tokenB);
+pair = address(uint160(uint(keccak256(abi.encodePacked(
+        hex'ff',
+        factory,
+        keccak256(abi.encodePacked(token0, token1)),
+        hex'96e8ac4277198ff8b6f785478aa9a39f403cb768dd02cbee326c3e7da348845f' // hard coded factory init code hash
+    )))));
+}
+\end{minted}
+
+Changes to 
+\begin{minted}{javascript}
+
+function pairFor(address factory, address tokenA, address tokenB) internal view returns (address pair) {
+    bytes memory factoryHash = factory == SUSHI_FACTORY ? SUSHI_FACTORY_HASH : BACKUP_FACTORY_HASH;
+
+(address token0, address token1) = _sortTokens(tokenA, tokenB);
+pair = address(uint160(uint(keccak256(abi.encodePacked(
+        hex'ff',
+        factory,
+        keccak256(abi.encodePacked(token0, token1)),
+        factoryHash // init code hash
+    )))));
+}
+\end{minted}
+
+Fallback factory
+Since the extra factory is required for the arbitrage, we can use it, for the user, to check for an available swap on the alternate factory if it would otherwise fail on the default factory through slippage.
+
+
+\begin{minted}{javascript}
+\label{Fallback Factory:4}
+amounts = UniswapV2Library.getAmountsOut(factory, amountIn, path);
+require(amounts[amounts.length - 1] >= amountOutMin, 'UniswapV2Router: INSUFFICIENT_OUTPUT_AMOUNT');
+\end{minted}
+Changes to
+\begin{minted}{javascript}
+address factory = SUSHI_FACTORY;
+amounts = _getAmountsOut(factory, amountIn, path);
+if(amounts[amounts.length - 1] < amountOutMin){
+    // Change 1 -> fallback for insufficient output amount, check backup router
+    amounts = _getAmountsOut(BACKUP_FACTORY, amountIn, path);
+    require(amounts[amounts.length - 1] >= amountOutMin, 'UniswapV2Router: INSUFFICIENT_OUTPUT_AMOUNT');
+    factory = BACKUP_FACTORY;
+}
+\end{minted}
+
+
+Uint256 overflow
+Optimal arbitrage calculations were overflowing uint256. e.g.
+\begin{minted}{javascript}
+\label{Uint256 overflow:5}
+uint Cd = reserve0Token1.mul(997).mul(997);
+uint Cc = reserve1Token1.mul(997000);
+uint Cb = reserve1Token1.mul(reserve0Token0).mul(1000).mul(1000);
+uint Ca = reserve1Token0.mul(reserve0Token1).mul(997).mul(997);
+uint Cf = Ca - Cb;
+uint Cg = Cc + Cd;
+uint a = Cg * Cg;
+uint b = 2 * Cb * Cg;
+uint c = Cb * Cf;
+uint d = (b*b) + ( 4 * a * c ); 
+\end{minted}
+
+would consistently overflow by `uint b`. Found out through individual checks:
+\begin{minted}{javascript}
+unchecked {
+    uint a = Cg * Cg;
+    require(a/Cg == Cg,"a overflow");
+    uint b = 2 * Cb * Cg;
+    require(b/Cb == 2*Cg ,"b overflow");
+    uint c = Cb * Cf;
+    require(c/Cb == Cf,"c overflow");
+    uint d = (b*b) + ( 4 * a * c );
+    require(d/(b*b) == 4*a*c,"d overflow");
+}
+\end{minted}
+
+ABDKMath \footnote{https://github.com/abdk-consulting/abdk-libraries-solidity} libs were used for a time, as it avoided overflow by dropping to floats. E.g.
+
+\begin{minted}{javascript}
+bytes16 _Cg = ABDKMathQuad.fromUInt(Cg);
+bytes16 _a = ABDKMathQuad.mul(_Cg, _Cg);
+\end{minted}
+
+However we found this lost precision and failed echidna tests.
+\begin{minted}{javascript}
+\label{Uint256 overflow:5}
+\caption{{\em echidna} test}
+echidna_mulUint:  failed!
+  Call sequence:
+    setX1(1106235220955)
+    setX(9390953368914254812617)
+
+
+echidna_Uint_convertion:  failed!
+  Call sequence:
+    setX(10518526264810785485368401065708505)
+
+
+echidna_divUint:  failed!
+  Call sequence:
+    setX(10417774989007224423389698535018119)
+    setX1(1)
+\end{minted}
+
+We also tried PRBMath\footnote{https://github.com/paulrberg/prb-math/} libs. These faired better in echidna tests but still suffered overflow issues. 
+
+\begin{minted}{javascript}
+echidna_mulUint:  failed!
+  Call sequence:
+    setX(115916773041390072873637598212453390567932363729484377996870)
+
+
+echidna_Uint_convertion:  failed!
+  Call sequence:
+    setX(115962837499224411198969207499961588040517688084412876519766)
+
+
+echidna_divUint:  failed!
+  Call sequence:
+    setX(115989750869986627937072895547572258287879165164826483095329)
+    setX1(1)
+\end{minted}
+
+Eventually we found Uint512\footnote{https://github.com/SimonSuckut/Solidity_Uint512/blob/main/contracts/Uint512.sol} which both passed echidna and overflow issue.
+\begin{minted}{javascript}
+echidna_mulUint:  passed! 
+echidna_divUint:  passed!
+\end{minted}
+
+
+
+https://github.com/SimonSuckut/Solidity_Uint512/blob/main/contracts/Uint512.sol
+
 \section{Benchmarking}
 
 \section{Use Cases and Experiments}