###### tags:`Technical Notes`
# `muldiv` and Fixedpoint arithmetic in Solidity
Some notes on [https://eips.ethereum.org/EIPS/eip-5000](EIP-5000).$\newcommand{\muldiv}{\operatorname{muldiv}}$ $\newcommand{\mod}{\operatorname{mod}}$ $\newcommand{mulmod}{\operatorname{mulmod}}$ $\newcommand{mul}{\operatorname{mul}}$ $\newcommand{add}{\operatorname{add}}$ $\newcommand{sub}{\operatorname{sub}}$
Assume that the operations $\times, +, -, \cdots$ represents arbitrary precision arithmetic.
## `muldiv` in EVM
Let us define
$$\muldiv(a, b, c) = \left\{ \begin{array}{cc}?? & \text{ if } c = 0 \\ \left\lfloor \frac{a \times b}{c} \right\rfloor \pmod{2^{256}} & \text{ otherwise}
\end{array} \right.$$
It is important to know if $\frac{a \times b}{c} \ge 2^{256}$, since for "checked" implementations, this would be the revert condition.
Note that
$$\frac{a \times b}{c} \ge 2^{256} \iff \frac{a \times b}{2^{256}} \ge c$$
The number $\frac{a \times b}{2^{256}}$ is the higher 256-bits of the number $a \times b$ and can be computed by [`muldiv256`](Function-that-returns-higher-order-bits).
```solidity
function checked_muldiv(uint a, uint b, uint c) pure returns (uint d) {
// see Appendix for muldiv256 implementation
if (muldiv256(a, b) >= c) {
revert("overflow");
}
assembly {
d := muldiv(a, b, c)
}
}
```
Alternatively, if we can treat the $r = 0$ case as $r = 2^{256}$, then the checked arithmetic on $\muldiv$ would be checking if $\muldiv(a, b, 0) \ge c$.
```solidity
function checked_muldiv(uint a, uint b, uint c) pure returns (uint d) {
assembly {
if iszero(lt(muldiv(a, b, 0), c) {
revert(0, 0)
}
d := muldiv(a, b, c)
}
}
```
However, if we want the $r = 0$ case to have parity with $\operatorname{div}$, then we have to treat $\muldiv(a, b, 0)$ as $0$.
<!--
## Doing checked `muldiv` without the `c = 0` hack
### If `c` and `type(uint256).max` are coprime
We can use the same trick as in [Doing 512 bit multiplication in EVM](#Doing-512-bit-multiplication-in-EVM).
In particular, for binary fixed point implementations, this is the case as $2^n$ and $2^{256} - 1$ are coprime for $1 \le n \le 255$.
**TODO** Proof of why this works
-->
## Fixed point implementation and `muldiv`
A fixed point number represented in EVM as $a$ with base $B$ corresponds to the number $\frac{a}{B}$ in "real" context. We'll represent the "real" value as with the $'$ notation. Typically the values can be $B = 10^{18}$ (18 decimal fixed point implementation). Uniswap-v3 uses $B = 2^{96}$ (96 bit binary decimals).
For two fixed point numbers $a$ and $b$, the following is the product:
$$a' \times b' = \frac{a}{B} \times \frac{b}{B} = \frac{\frac{a\times b}{B}}{B} = \left(\frac{a \times b}{B}\right)'$$
This is the number $\muldiv(a, b, B)$.
Similarly, $\frac{a}{b}$ as a fixed point number is given by $\mulmod(a, B, b)$.
Addition and subtraction of $a$ and $b$ are exactly the same as $\add(a, b)$ and $\sub(a, b)$ in the EVM.
<!--
Optimization: it's common to do `a * b / c` where `a, b, c` are all fixed point numbers. This value is effectively `checked_muldiv(a, b, c)`, but if you split the expressions, there are some unnecessary intermediate operations.
-->
# Appendix
## Doing 512 bit multiplication in EVM
For 256-bit numbers $a$ and $b$, we want to compute $a \times b$. Decompose this into $a \times b = q \cdot 2^{256} + r$ where $0 \le r < 2^{256}$. Since $\mul(a, b)$ is defined as $a \times b \mod 2^{256}$. We see that $r = \mul(a, b).$ Also note that since $0 \le a,b \le 2^{256} - 1$ we can claim that $q$ is strictly less than $2^{256} - 1$, i.e., $0 \le q \le 2^{256} - 2$.
Notice that $\mulmod(a, b, 2^{256} - 1) = a \times b \pmod {2^{256} - 1} \equiv q \cdot (1) + \mul(a, b) \pmod{2^{256} - 1}.$
This implies that $q \equiv \mulmod(a, b, 2^{256} - 1) - \mul(a, b) \pmod{2^{256} - 1}.$
<!--
> *Chinese reminder theorem*: Let $m_1$ and $m_2$ are coprime. Then the system of simultaneous congruences $x \equiv a_1 \pmod{m_1}$ and $y \equiv a_2 \pmod{m_2}$ has a solution $x = c$ that is unique upto $\mod {m_1 \cdot m_2}$.
-->
## As solidity code
```solidity
/// Returns higher order bits and lower order bits of
/// the 512 bit multiplication of a and b.
function mul512(uint a, uint b) pure returns (uint hi, uint lo) {
uint uint_max = type(uint).max;
assembly {
lo := mul(a, b)
let mm := mulmod(a, b, uint_max);
switch lt(mm, lo)
case 0 {
hi := sub(mm, lo)
}
default {
hi := sub(uint_max, sub(lo, mm))
}
}
}
```
## Branchless implementation of `hi` calculation
```solidity
switch lt(mm, lo)
case 0 {
hi := sub(mm, lo)
}
default {
hi := sub(uint_max, sub(lo, mm))
}
```
is the same as `hi := sub(sub(mm, lo), lt(mm, lo))`. This is implement in [Uniswap FullMath](https://github.com/Uniswap/v3-core/blob/ed88be38ab2032d82bf10ac6f8d03aa631889d48/contracts/libraries/FullMath.sol#L19-L30).
## Function that returns higher order bits
```solidity
/// Returns `hi` such that `a × b = hi × 2**256 + mul(a, b)`
/// A highly optimized stack arrangement would compute this in roughly 25 gas.
function muldiv256(uint a, uint b) returns (uint hi) {
uint uint_max = type(uint).max;
assembly {
let lo := mul(a, b)
let mm := mulmod(a, b, uint_max)
hi := sub(sub(mm, lo), lt(mm, lo))
}
}
```