Required context to read this: [FFMul RFC](https://o1-labs.github.io/proof-systems/rfcs/foreign_field_mul.html)

Given witnesses $a$, $b$, $q$, $r$ each represented as 3 limbs $(x_0, x_1, x_2)$ by

$$x = x_0 + 2^\ell x_1 + 2^{2\ell} x_2,$$

we want to prove that, assuming a certain list of constraints,

\begin{equation}
a b = q f + r \qquad (1)
\end{equation}

holds as an equation over the integers.

## FFMul without range checks

Our derivation in this section will use the constraints of the FFMul gate, except for any assumptions about the sizes of $a$, $b$, $q$ and $r$. The goal is to work out exactly what range checks we need on these values.

The first constraint we use is checking $(1)$ modulo the native modulus $n$ (where we expand each term into its limbs). This single constraint proves that there is an $\varepsilon \in\mathbb{Z}$ such that

$$
a b - q f - r = \varepsilon n \qquad\text{(2: native)}
$$

Our strategy now is to also constrain the LHS modulo $2^{3\ell}$ and then use CRT-type arguments. So, let's expand $a b - q f - r$ into limbs, but collect all terms higher than $2^{3\ell}$ into a single term $w$.

\begin{aligned}
& a b - q f - r = \\
& (a_0 b_0 + q_0 f'_0 - r_0) \\
&+ 2^{\ell} (a_0 b_1 + a_1 b_0 + q_0 f'_1 + q_1 f'_0 - r_1) \\
&+ 2^{2\ell} (a_0 b_2 + a_2 b_0 + q_0 f'_2 + q_2 f'_0 + a_1 b_1 + q_1 f'_1 - r_2) \\
&+ 2^{3\ell} w
\end{aligned}

This equation holds over the integers. Like in the RFC, to abbreviate formulas we define $p_i$ such that the equation becomes

$$
a b - q f - r = (p_0 - r_0) + 2^{\ell} (p_1 - r_1) + 2^{2\ell} (p_2 - r_2) + 2^{3\ell} w \qquad (2')
$$

Next, we split $p_1 = p_{01} + 2^\ell p_{11}$ where we add range checks to prove that $p_{01}$ has at most $\ell$ bits and $p_{11}$ has at most $\ell + 2$ bits. The split itself is a constraint modulo $n$, showing that

$$
p_1 = p_{01} + 2^\ell p_{11} + \beta n \qquad \text{(3: split)}
$$

for some $\beta \in\mathbb{Z}$.

Expanding $p_1$ using the last equation in $(2')$, we get
$$
a b - q f - r = (p_0 + 2^\ell p_{01} - r_0 - 2^\ell r_1) + 2^{2\ell} (p_2 + p_{11} - r_2) + 2^{3\ell} w + 2^\ell \beta n \qquad(2'')
$$

Now we will start constraining this equation limb-wise. We add a constraint for the bottom 2 limbs, namely

$$
p_0 + 2^\ell p_{01} - r_0 - 2^\ell r_1 = 2^{2\ell} v_0 + \alpha n \qquad\text{(4: bottom limbs)}
$$

for some $\alpha \in\mathbb{Z}$, where $v_0$ is some carry value and we prove that $v_0$ has at most 2 bits. Plugging this into $(2'')$, we eliminate the first bracketed term and get

$$
a b - q f - r = 2^{2\ell} (p_2 + p_{11} - r_2 + v_0) + 2^{3\ell} w + (\alpha + 2^\ell \beta) n \qquad(2''')
$$

Next, we add a constraint for the high limb. For this we introduce a carry value $v_{1}$ which is range-checked to have at most $\ell + 3$ bits. We add the following constraint:

$$
p_2 + p_{11} - r_2 + v_0 = 2^{\ell} v_{1} + \gamma n \qquad\text{(5: high limb)}
$$

for some $\gamma \in\mathbb{Z}$. Plugging this into $(2''')$, the $2^\ell$ term is eliminated and we have proved that

$$
a b - q f - r = 2^{3\ell} (w + v_{1}) + (\alpha + 2^\ell \beta + 2^{2\ell} \gamma) n \qquad(2'''')
$$

Now, for a brief moment let's look at this equation modulo $n$. Since the LHS is equal to $\varepsilon n$ by $\text{(2: native)}$, we have

$$
2^{3\ell} (w + v_{1}) = 0 \mod{n}
$$

Because $2^{3\ell}$ and $n$ are co-prime, we can multiply with $2^{-3\ell}$ to see that

$$
w + v_{1} = 0 \mod{n}
$$

So let's write

$$
w + v_{1} = \delta n
$$

(This was the CRT-type argument.)

In summary, by $(2'''')$ and **without any assumptions on the sizes of $a$, $b$, $q$, $r$, our constraints prove that**

$$
a b - q f - r = (\alpha + 2^\ell \beta + 2^{2\ell} \gamma + 2^{3\ell}\delta) n \qquad(6)
$$

It only remains to introduce range checks sufficient to imply that $\alpha = \beta = \gamma = \delta = 0$. Or, looked at it differently, it suffices to make one of those values non-zero to find a counter-example to the soundness of the FFMul gate.

## Conditions to make $\alpha = \beta = \gamma = \delta = 0$

Let's recall where possible non-zero values on the RHS may come from:

* **$\alpha$ can be non-zero if $\text{(4: bottom limbs)}$ overflows $n$.**
* **$\beta$ can be non-zero if $\text{(3: split)}$ overflows $n$.**
* **$\gamma$ can be non-zero if $\text{(5: high limb)}$ overflows $n$.**

To prove $\alpha = 0$ it's enough to show
$$-n < p_0 + 2^\ell p_{01} - r_0 - 2^\ell r_1 - 2^{2\ell} v_0 < n \qquad(7a)$$

To prove $\beta = 0$ it's enough to show
$$-n < p_1 - p_{01} + 2^\ell p_{11} < n \qquad(7b)$$

To prove $\gamma = 0$ it's enough to show
$$-n < p_2 + p_{11} - r_2 + v_0 - 2^{\ell} v_{1} < n \qquad(7c)$$

If $\alpha = \beta = \gamma = 0$, then by $(6)$ we know that

$$
a b - q f - r = \delta 2^{3\ell} n \qquad \text{(8: final)}
$$

* **$\delta$ can be non-zero if $\text{(8: final)}$ overflows $2^{3\ell} n$.**

To prove $\delta = 0$ it's enough to show $\alpha = \beta = \gamma = 0$ and

$$-2^{3\ell} n < a b - q f - r < 2^{3\ell} n\qquad(9)$$

## Range-checking $a$, $b$, $q$, $r$

Recall the following range checks which we already had to assume so far:

* $v_0$ $\in [0,2^2)$
* $p_{01}$ $\in [0,2^\ell)$
* $p_{11}$ $\in [0,2^{\ell + 2})$
* $v_{1}$ $\in [0,2^{\ell + 3})$

Now, let's assume in addition that all of the following limb values are ranged-checked to be at most $\ell$ bits:

* $a_0$, $a_1$, $a_2$ $\in [0,2^\ell)$
* $b_0$, $b_1$, $b_2$ $\in [0,2^\ell)$
* $q_0$, $q_1$, $r_2$ $\in [0,2^\ell)$
* $r_0 + 2^\ell r_1 \in [0,2^{2\ell})$
* $r_2$ $\in [0,2^\ell)$

Note that $r$ is treated a bit differently than the other values: We don't require a range-check of the individual limbs $r_0$ and $r_1$, but only of the combined "compact limb" $r_0 + 2^\ell r_1$. This works because our constraints use only the combined form.

This is enough to prove $(7a)$, $(7b)$ and $(7c)$.

### (7a)

First, we put estimates on $p_0 = a_0 b_0 + q_0 f'_0$:

$$0 \le a_0 b_0 + q_0 f'_0 < 2^{2\ell} + 2^{2\ell} = 2^{2\ell + 1} $$

Using that we get $(7a)$, upper bound:

\begin{align}
& p_0 + 2^\ell p_{01} - (r_0 + 2^\ell r_1) - 2^{2\ell} v_0 < \\
& 2^{2\ell + 1} + 2^{2\ell} - 0 - 0 < \\
& 2^{2\ell + 2} < n
\end{align}

$(7a)$, lower bound:

\begin{align}
& -p_0 - 2^\ell p_{01} + (r_0 + 2^\ell r_1) + 2^{2\ell} v_0 < \\
& -0 - 0 + 2^{2\ell} + 3 \cdot 2^{2\ell} = \\
& 2^{2\ell + 2} < n
\end{align}

### (7b)

Estimate $p_1 = a_0 b_1 + a_1 b_0 + q_0 f'_1 + q_1 f'_0$:

$$0 \le a_0 b_1 + a_1 b_0 + q_0 f'_1 + q_1 f'_0 < 4 \cdot 2^{2\ell} = 2^{2\ell + 2} $$

$(7b)$, upper bound:

\begin{align}
& p_1 - p_{01} + 2^\ell p_{11} < \\
& 2^{2\ell + 2} - 0 + 2^{2\ell + 2} = \\
& 2^{2\ell + 3} < n
\end{align}

$(7b)$, lower bound:

\begin{align}
& -p_1 + p_{01} - 2^\ell p_{11} < \\
& -0 + 2^\ell - 0 = \\
& 2^\ell < n
\end{align}

### (7c)

Estimate $p_2 = a_0 b_2 + a_1 b_1 + a_2 b_0 + q_0 f'_2 + q_1 f'_1 + q_2 f'_0$:

$$0 \le p_2 < 6 \cdot 2^{2\ell} $$

$(7c)$, upper bound:

\begin{align}
& p_2 + p_{11} - r_2 + v_0 - 2^{\ell} v_{1} < \\
& 6 \cdot 2^{2\ell} + 2^{\ell + 2} - 0 + 2^2 - 0 < \\
& 2^{2\ell + 3} < n
\end{align}

$(7c)$, lower bound:

\begin{align}
& -p_2 - p_{11} + r_2 - v_0 + 2^{\ell} v_{1} < \\
& -0 - 0 + 2^\ell - 0 + 2^{2\ell + 3} = \\
& 2^{2\ell + 4} < n
\end{align}

### Final bound

We will now discuss how to prove the final bound

$$-2^{3\ell} n < a b - q f - r < 2^{3\ell} n\qquad(9)$$

To prove $(9)$, it's not enough to have $\ell$-bit range checks on all the limbs, because for example $ab = (2^{3\ell} - 1)^2 > 2^{3\ell} n$. The RFC chose $\ell$ and $3$ specifically such that
$$f^2 < 2^{3\ell} n$$
for all $f$ that we care about, so that the estimate $(9)$ works if $a$, $b$, $q$, $r$ < $f$ (i.e., if they are foreign field elements in canonical representation).

However, for efficiency we want to relax the $< f$ requirement a bit, because it would require a foreign field addition plus 3 range checks per variable. We can get an almost equivalent estimate by only range-checking the highest limb of each variable and a native addition.

Concretely, for a variable $x = (x_0, x_1, x_2)$ we define the _high-limb bounds check_ as the following two constraints:

* $x_2 + (2^\ell - f_2) = z \mod n$
* $z \in [0,2^\ell)$

We might write this succinctly as "$x_2 + (2^\ell - f_2) \in [0,2^\ell)$" but in that case we must not forget that "$+$" is finite field addition.

For a field element $x_2 \in [0, n)$ the high-limb bounds check implies that

$$x_2 \in [0, f_2) \cup [n - 2^\ell + f_2, n).$$

So this allows $x_2$ to be a large number close to $n$. If, in addition, $x_2$ is range-checked to be at most $\ell$ bits, the high interval is excluded:

$$x_2 \in [0, 2^\ell) \quad\text{and}\quad x_2 + (2^\ell - f_2) \in [0,2^\ell) \quad\Longrightarrow\quad x_2 \in [0, f_2)$$

For $x = (x_0, x_1, x_2)$, the 3-limb range check plus high-limb bounds check imply $x < f + 2^{2\ell}$, as follows:

$$
x = 2^{2\ell} x_2 + 2^\ell x_1 + x_0 < 2^{2\ell} f_2 + 2^{2\ell} \le f + 2^{2\ell}
$$

This is only slightly weaker than $x < f$ and is enough for us to prove $(9)$.

We add the high-limb bounds check to the 3-limb range-checks for $a$, $b$ and $q$:

* $a_2 + (2^\ell - f_2) \in [0,2^\ell)$
* $b_2 + (2^\ell - f_2) \in [0,2^\ell)$
* $q_2 + (2^\ell - f_2) \in [0,2^\ell)$

This implies that $a,b,q \in[0, f + 2^\ell)$. For $r$, we already know that $r \in [0, 2^{3\ell})$ and don't need additional assumptions.

We now get the following upper bound:

$$
ab - qr - f < ab < (f + 2^\ell)^2
$$

And lower bound:

$$
-ab + qr + f < qr + f < (f + 2^\ell)^2 + 2^{3\ell}
$$

Thus, we can prove $(9)$ if the foreign field modulus satisfies

$$
(f + 2^\ell)^2 + 2^{3\ell} < 2^{3\ell} n
$$

$$
f < \sqrt{ 2^{3\ell} (n - 1) } - 2^\ell
$$

For both Pasta moduli $n$, this still means that $f$ can be any prime up to 259 bits.

## Necessity of range checks

In the last section we identified range conditions sufficient to make the FFmul gate sound. Ideally, we also want to be sure that they are _necessary_, and that we can't optimize our design further by removing some of them.

We'll analyze two different ideas to optimize the gate by removing conditions on $q$:

* **First idea**: Skip the check $q_2 \in [0, 2^\ell)$, so that $q_2$ is only constrained by $q_2 + (2^\ell - f_2) \in [0, 2^\ell)$
* **Second idea**: Do not range-check $q_0$ and $q_1$ individually, but only their combination into a compact limb: $q_0 + 2^\ell q_1 \in [0, 2^\ell)$ (where "$+$" is field addition)

The second idea allows us to borrow or carry values between $q_0$ and $q_1$. For example, we could represent $q = n$ by the limbs $(q_0, q_1, q_2) = (2^\ell, n-1, 0)$, because

$$(q_0 + 2^\ell q_1) \bmod{n} = 0 \in [0, 2^\ell)$$

In equations $\bmod{n}$, these limbs will be indistinguishable from $(2^\ell, -1, 0)$ which is a mathematically valid representation of $q = 0$. Indeed, it is easy to show that we satisfy all our constraints with $a = b = r = 0$ and $q = (2^\ell, n-1, 0)$, for typical values of $f$. In other words, the prover fools the verifer into believing that $q = n$ is a valid witness for

$$
0 \cdot 0 = qf + 0
$$

This breaks soundness if we consider $q$ one of the outputs of the FFmul gate.

However, in most applications, we don't care about the value of $q$, and only care about $r$ as an output. With that in mind, we could interpret the FFmul gate as a way to prove

$$
\exists q' \colon \quad ab = q' f + r \qquad (10)
$$

given witnesses $a$, $b$ and $r$.

The example we just gave does **not** break soundness in this interpretation, because we only made $q$ have an invalid value, but $a$, $b$, $r$ are correct and the statement $(10)$ remains true.

In the remaining section, we aim for stronger counter-examples which provide an invalid $r$, and thus break soundness for $(10)$ as well.

### Counter-example 1: Skipping $q_2 \in [0, 2^\ell)$

If we skip the check $q_2 \in [0, 2^\ell)$ and only use the bounds check $q_2 + (2^\ell - f_2) \in [0, 2^\ell)$, we potentially allow $q_2 \in [n - 2^\ell + f_2, n)$. The idea for exploiting this is that $q_2$ can be used to represent negative values of $q$ (modulo $n$).

#### Representing negative $q$

In general, if $q = -|q|$ is negative, we can first split the abolute value $|q|$ into positive limbs $(|q|_0, |q|_1, |q|_2) \in [0, 2^\ell)^3$ as usual, and then represent $q$ as

$$
q \cong (q_0, q_1, q_2) = (2^\ell - |q|_0, 2^\ell - 1 - |q|_1, -|q|_2 - 1)
$$

(Detail: If $|q|_0 = 0$ this doesn't work but then we just don't do the borrowing.)

In words, by borrowing from higher limbs we only need the highest limb $q_2 = -|q|_2 - 1$ to be negative. Now, $-|q|_2 - 1$ is indistinguishable in our constraints from $n-|q|_2 - 1$, and $q_2 = n-|q|_2 - 1$ is an allowed value for all $|q|_2 \in [0, 2^\ell - f_2)$. This means we can "represent" most negative $q \in (-2^{3\ell}, 0)$ by

$$
q_\text{fake} \cong (2^\ell - |q|_0, 2^\ell - |q|_1 + 1, n-|q|_2 - 1).
$$

Note that

$$
q_\text{fake} = q + 2^{2\ell} n
$$

#### Attack on FFMul

If we are able to use large negative $q$, the estimates for the final bound $(9)$ are no longer valid, which we can exploit. Given any $a$, $b$, we can find $q$, $r$ such that

$$
ab = qf + r + 2^{3\ell} n \qquad (9_\text{fake})
$$

This is always possible: we pick $q$ and $r$ to be the quotient and remainder of the modified divsion $(ab - 2^{3\ell} n) / f$. Concretely, $q = \lfloor\frac{ab - 2^{3\ell} n}{f}\rfloor$, which is a negative number (but big enough that we can always represent it by $q_\text{fake}$, if e.g. $2n < f$).

If we replace $q$ by $q_\text{fake} = q + 2^{2\ell}n$, we get a modified equation which still features the same $a$, $b$, $r$:

$$
ab = (q_\text{fake} - 2^{2\ell} n)f + r + 2^{3\ell} n \qquad (9'_\text{fake})
$$

So, we want to fool the verifier into accepting $a$, $b$ and $r$ satisfying $(9'_\text{fake})$. $r$ is not the correct remainder of $ab / f$, because $2^{3\ell} n$ is not a multiple of $f$.

Since $q_\text{fake} = q \bmod n$, equation $\text{(2: native)}$ is satisfied, and since we use the correct, $\ell$-bit values for $q_0$ and $q_1$, equations $\text{(3: split)}$ and $\text{(4: bottom limbs)}$ are as well (added multiples of $n$ like $2^{3\ell} n$ affect none of our constraints).

The only way our attack can sometimes fail is because $q_2$ is now "negative", the expression $p_2$ is no longer guaranteed to be positive and we might underflow 0 in $\text{(5: high limb)}$, which the range-check on the RHS doesn't allow:

$$
(ab)_2 + q_0f'_2 + q_1f'_1 + (- |q|_2 - 1)f'_0 + p_{11} - r_2 + v_0 = 2^{\ell} v_{1} \mod n \quad\text{(5: high limb)}
$$

However, underflow caused by one negative value $(- |q|_2 - 1)f'_0$ against 5 positive values of similar size is the exception. Furthermore, there are important primes where $f'_0$ is an unusually small number:
* For Curve25519 we have $f'_0 = 19$
* For seqp256k1 we have $f'_0 = 2^{32} + 2^9 + 2^8 + 2^7 + 2^6 + 2^4 + 1$

In these cases, the negative $-|q|_2f'_0$ is small and should never cause underflow for "random" input values. In other words, the prover can use an incorrect output $r$ in almost every foreign field multiplication.

**Conclusion**: The full range check $q_2 \in [0,2^\ell)$ is necessary.

### Counter-example 2: Compact range-check on $q_0 + 2^\ell q_1$

TBC