Foreign Field Multiplication

This document is an original RFC explaining how we constrain foreign field multiplication (i.e. non-native field multiplication) in the Kimchi proof system. For a more recent RFC, see FFmul RFC.

Changelog

Overview

This gate constrains

$$a\cdot b=c\mathrm{mod}f$$

where $a,b,c\in {\mathbb{F}}_f$, a foreign field with modulus $f$, using the native field ${\mathbb{F}}_n$ with prime modulus $n$.

Approach

In foreign field multiplication the foreign field modulus $f$ could be bigger or smaller than the native field modulus $n$. When the foreign field modulus is bigger, then we need to emulate foreign field multiplication by splitting the foreign field elements up into limbs that fit into the native field element size. When the foreign modulus is smaller everything can be constrained either in the native field or split up into limbs.

Since our projected use cases are when the foreign field modulus is bigger (more on this below) we optimize our design around this scenario. For this case, not only must we split foreign field elements up into limbs that fit within the native field, but we must also operate in a space bigger than the foreign field. This is because we check the multiplication of two foreign field elements by constraining its quotient and remainder. That is, renaming $c$ to $r$, we must constrain

$$a\cdot b=q\cdot f+r,$$

where the maximum size of $q$ and $r$ is $f-1$ and so we have

$$\begin{array}{rl}a\cdot b& \le \underset{q}{\underbrace{(f-1)}}\cdot f+\underset{r}{\underbrace{(f-1)}}\\ & \le f^2-1.\end{array}$$

Thus, the maximum size of the multiplication is quadratic in the size of foreign field.

Naïve approach

Naïvely, this implies that we have elements of size $f^2-1$ that must split them up into limbs of size at most $n-1$. For example, if the foreign field modulus is $256$ and the native field modulus is $255$ bits, then we’d need ${\log }_2((2^{256}{)}^2-1)\approx 512$ bits and, thus, require $512/255\approx 3$ native limbs. However, each limb cannot consume all $255$ bits of the native field element because we need space to perform arithmetic on the limbs themselves while constraining the foreign field multiplication. Therefore, we need to choose a limb size that leaves space for performing these computations.

Later in this document (see the section entitled “Choosing the limb configuration”) we determine the optimal number of limbs that reduces the number of rows and gates required to constrain foreign field multiplication. This results in $\ell =88$ bits as our optimal limb size. In the section about intermediate products we place some upperbounds on the number of bits required when constraining foreign field multiplication with limbs of size $\ell$ thereby proving that the computations can fit within the native field size.

Observe that by combining the naïve approach above with a limb size of $88$ bits, we would require $512/88\approx 6$ limbs for representing foreign field elements. Each limb is stored in a witness cell (a native field element). However, since each limb is necessarily smaller than the native field element size, it must be copied to the range-check gate to constrain its value. Since Kimchi only supports 7 copyable witness cells per row, this means that only one foreign field element can be stored per row. This means a single foreign field multiplication would consume at least 4 rows (just for the operands, quotient and remainder). This is not ideal because we want to limit the number of rows for improved performance.

Chinese remainder theorem

Fortunately, we can do much better than this, however, by leveraging the chinese remainder theorem (CRT for short) as we will now show. The idea is to reduce the number of bits required by constraining our multiplication modulo two coprime moduli: $2^t$ and $n$. By constraining the multiplication with both moduli the CRT guarantees that the constraints hold with the bigger modulus $2^t\cdot n$.

The advantage of this approach is that constraining with the native modulus $n$ is very fast, allowing us to speed up our non-native computations. This practically reduces the costs to constraining with limbs over $2^t$, where $t$ is something much smaller than $512$.

For this to work, we must select a value for $t$ that is big enough. That is, we select $t$ such that $2^t\cdot n>f^2-1$. As described later on in this document, by doing so we reduce the number of bits required for our use cases to $264$. With $88$ bit limbs this means that each foreign field element only consumes $3$ witness elements, and that means the foreign field multiplication gate now only consumes $2$ rows. The section entitled “Choosing $t$” describes this in more detail.

Overall approach

Bringing it all together, our approach is to verify that

$$\begin{array}{r}a\cdot b=q\cdot f+r\end{array}$$

over ${\mathbb{Z}}^{+}$. In order to do this efficiently we use the CRT, which means that the equation holds mod $M=2^t\cdot n$. For the equation to hold over the integers we must also check that each side of the equation is less than $2^t\cdot n$.

The overall steps are therefore

1. Apply CRT to equation (1)
   • Check validity with binary modulus $\mathrm{mod}{2}^t$
   • Check validity with native modulus $\mathrm{mod}n$
2. Check each side of equation (1) is less than $M$
   • $a\cdot b<2^t\cdot n$
   • $q\cdot f+r<2^t\cdot n$

This then implies that

$$a\cdot b=c\mathrm{mod}f.$$

where $c=r$. That is, $a$ multiplied with $b$ is equal to $c$ where $a,b,c\in {\mathbb{F}}_f$. There is a lot more to each of these steps. That is the subject of the rest of this document.

Other strategies

Within our overall approach, aside from the CRT, we also use a number of other strategies to reduce the number and degree of constraints.

• Avoiding borrows and carries
• Intermediate product elimination
• Combining multiplications

The rest of this document describes each part in detail.

Parameter selection

This section describes important parameters that we require and how they are computed.

• Native field modulus $n$
• Foreign field modulus $f$
• Binary modulus $2^t$
• CRT modulus $2^t\cdot n$
• Limb size in bits $\ell$

Choosing $t$

Under the hood, we constrain $a\cdot b=q\cdot f+r\mathrm{mod}{2}^t\cdot n$. Since this is a multiplication in the foreign field $f$, the maximum size of $q$ and $r$ are $f-1$, so this means

$$\begin{array}{rl}a\cdot b& \le (f-1)\cdot f+(f-1)\\ & \le f^2-1.\end{array}$$

Therefore, we need the modulus $2^t\cdot n$ such that

$$2^t\cdot n>f^2-1,$$

which is the same as saying, given $f$ and $n$, we must select $t$ such that

$$\begin{array}{rl}{2}^t\cdot n& \ge f^2\\ t& \ge 2{\log }_2(f)-{\log }_2(n).\end{array}$$

Thus, we have an lower bound on $t$.

Instead of dynamically selecting $t$ for every $n$ and $f$ combination, we fix a $t$ that will work for the different selections of $n$ and $f$ relevant to our use cases.

To guide us, from above we know that

$$t_{min}=2{\log }_2(f)-{\log }_2(n)$$

and we know the field moduli for our immediate use cases.

vesta     = 2^254 + 45560315531506369815346746415080538113 (255 bits)
pallas    = 2^254 + 45560315531419706090280762371685220353 (255 bits)
secp256k1 = 2^256 - 2^32 - 2^9 - 2^8 - 2^7 - 2^6 - 2^4 - 1 (256 bits)

So we can create a table

and know that to cover our use cases we need $t\ge 258$.

Next, given our native modulus $n$ and $t$, we can compute the maximum foreign field modulus supported. Actually, we compute the maximum supported bit length of the foreign field modulus $f=2^m$.

$$\begin{array}{rl}{2}^t\cdot n& \ge f^2\\ & \ge (2^m{)}^2=2^{2m}\\ t+{\log }_2(n)& >{\log }_2(2^{2m})=2m\end{array}$$

So we get

$$m_{max}=\frac{t+{\log }_2(n)}{2}.$$

With $t=258,n=255$ we have

$$\begin{array}{rl}{m}_{max}& =\frac{258+255}{2}=256.5,\end{array}$$

which is not enough space to handle anything larger than 256 bit moduli. Instead, we will use $t=264$, giving $m_{max}=259$ bits.

The above formula is useful for checking the maximum number of bits supported of the foreign field modulus, but it is not useful for computing the maximum foreign field modulus itself (because $2^{m_{max}}$ is too coarse). For these checks, we can compute our maximum foreign field modulus more precisely with

$$ma{x}_{mod}=\lfloor \sqrt{2^t\cdot n}\rfloor .$$

The max prime foreign field modulus satisfying the above inequality for both Pallas and Vesta is 926336713898529563388567880069503262826888842373627227613104999999999999999607.

Choosing the limb configuration

Choosing the right limb size and the right number of limbs is a careful balance between the number of constraints (i.e. the polynomial degree) and the witness length (i.e. the number of rows). Because one limiting factor that we have in Kimchi is the 12-bit maximum for range check lookups, we could be tempted to introduce 12-bit limbs. However, this would mean having many more limbs, which would consume more witness elements and require significantly more rows. It would also increase the polynomial degree by increasing the number of constraints required for the intermediate products (more on this later).

We need to find a balance between the number of limbs and the size of the limbs. The limb configuration is dependent on the value of $t$ and our maximum foreign modulus (as described in the previous section). The larger the maximum foreign modulus, the more witness rows we will require to constrain the computation. In particular, each limb needs to be constrained by the range check gate and, thus, must be in a copyable (i.e. permuteable) witness cell. We have at most 7 copyable cells per row and gates can operate on at most 2 rows, meaning that we have an upperbound of at most 14 limbs per gate (or 7 limbs per row).

As stated above, we want the foreign field modulus to fit in as few rows as possible and we need to constrain operands $a,b$, the quotient $q$ and remainder $r$. Each of these will require cells for each limb. Thus, the number of cells required for these is

$$cells=4\cdot limbs$$

It is highly advantageous for performance to constrain foreign field multiplication with the minimal number of gates. This not only helps limit the number of rows, but also to keep the gate selector polynomial small. Because of all of this, we aim to constrain foreign field multiplication with a single gate (spanning at most $2$ rows). As mentioned above, we have a maximum of 14 permuteable cells per gate, so we can compute the maximum number of limbs that fit within a single gate like this.

$$\begin{array}{rl}limb{s}_{max}& =\lfloor cells/4\rfloor \\ & =\lfloor 14/4\rfloor \\ & =3\end{array}$$

Thus, the maximum number of limbs possible in a single gate configuration is 3.

Using $limb{s}_{max}=3$ and $t=264$ that covers our use cases (see the previous section), we are finally able to derive our limbs size

$$\begin{array}{rl}\ell & =\frac{t}{limb{s}_{max}}\\ & =264/3\\ & =88\end{array}$$

Therefore, our limb configuration is:

• Limb size $\ell =88$ bits
• Number of limbs is $3$

Avoiding borrows

When we constrain $a\cdot b-q\cdot f=r\mathrm{mod}{2}^t$ we want to be as efficient as possible.

Observe that the expansion of $a\cdot b-q\cdot f$ into limbs would also have subtractions between limbs, requiring our constraints to account for borrowing. Dealing with this would create undesired complexity and increase the degree of our constraints.

In order to avoid the possibility of subtractions we instead use $a\cdot b+q\cdot f^{\prime }$ where

$$\begin{array}{rl}{f}^{\prime }& =-f\mathrm{mod}{2}^t\\ & =2^t-f\end{array}$$

The negated modulus $f^{\prime }$ becomes part of our gate coefficients and is not constrained because it is publicly auditable.

Using the substitution of the negated modulus, we now must constrain $a\cdot b+q\cdot f^{\prime }=r\mathrm{mod}{2}^t$.

Observe that $f^{\prime }<2^t$ since $f<2^t$ and that $f^{\prime }>f$ when $f<2^{t-1}$.

Intermediate products

This section explains how we expand our constraints into limbs and then eliminate a number of extra terms.

We must constrain $a\cdot b+q\cdot f^{\prime }=r\mathrm{mod}{2}^t$ on the limbs, rather than as a whole. As described above, each foreign field element $x$ is split into three 88-bit limbs: $x_0,x_1,x_2$, where $x_0$ contains the least significant bits and $x_2$ contains the most significant bits and so on.

Expanding the right-hand side into limbs we have

$$\begin{array}{rl}& (a_0+a_1\cdot 2^{\ell }+a_2\cdot 2^{2\ell })\cdot (b_0+b_1\cdot 2^{\ell }+b_2\cdot 2^{2\ell })+(q_0+q_1\cdot 2^{\ell }+q_2\cdot 2^{2\ell })\cdot (f_0^{\prime }+f_1^{\prime }\cdot 2^{\ell }+f_2^{\prime }\cdot 2^{2\ell })\\ & =\\ & a_0\cdot b_0+a_0\cdot b_1\cdot 2^{\ell }+a_0\cdot b_2\cdot 2^{2\ell }\\ & +a_1\cdot b_0\cdot 2^{\ell }+a_1\cdot b_1\cdot 2^{2\ell }+a_1\cdot b_2\cdot 2^{3\ell }\\ & +a_2\cdot b_0\cdot 2^{2\ell }+a_2\cdot b_1\cdot 2^{3\ell }+a_2\cdot b_2\cdot 2^{4\ell }\\ & +\\ & q_0\cdot f_0^{\prime }+q_0\cdot f_1^{\prime }\cdot 2^{\ell }+q_0\cdot f_2^{\prime }\cdot 2^{2\ell }\\ & +q_1\cdot f_0^{\prime }\cdot 2^{\ell }+q_1\cdot f_1^{\prime }\cdot 2^{2\ell }+q_1\cdot f_2^{\prime }\cdot 2^{3\ell }\\ & +q_2\cdot f_0^{\prime }\cdot 2^{2\ell }+q_2\cdot f_1^{\prime }\cdot 2^{3\ell }+q_2\cdot f_2^{\prime }\cdot 2^{4\ell }\\ & =\\ & a_0\cdot b_0+q_0\cdot f_0^{\prime }\\ & +2^{\ell }\cdot (a_0\cdot b_1+a_1\cdot b_0+q_0\cdot f_1^{\prime }+q_1\cdot f_0^{\prime })\\ & +2^{2\ell }\cdot (a_0\cdot b_2+a_2\cdot b_0+q_0\cdot f_2^{\prime }+q_2\cdot f_0^{\prime }+a_1\cdot b_1+q_1\cdot f_1^{\prime })\\ & +2^{3\ell }\cdot (a_1\cdot b_2+a_2\cdot b_1+q_1\cdot f_2^{\prime }+q_2\cdot f_1^{\prime })\\ & +2^{4\ell }\cdot (a_2\cdot b_2+q_2\cdot f_2^{\prime })\end{array}$$

Since $t=3\ell$, the terms scaled by $2^{3\ell }$ and $2^{4\ell }$ are a multiple of the binary modulus and, thus, congruent to zero $\mathrm{mod}{2}^t$. They can be eliminated and we don’t need to compute them. So we are left with 3 intermediate products that we call $p_0,p_1,p_2$:

So far, we have introduced these checked computations to our constraints

1. Computation of $p_0,p_1,p_2$

Constraining $\mathrm{mod}{2}^t$

Let’s call $p:=ab+q{f}^{\prime }\mathrm{mod}{2}^t$. Remember that our goal is to constrain that $p-r=0\mathrm{mod}{2}^t$ (recall that any more significant bits than the 264th are ignored in $\mathrm{mod}{2}^t$). Decomposing that claim into limbs, that means

$$\begin{array}{r}{2}^{2\ell }(p_2-r_2)+2^{\ell }(p_1-r_1)+p_0-r_0=0\mathrm{mod}{2}^t.\end{array}$$

We face two challenges

• Since $p_0,p_1,p_2$ are at least $2^{\ell }$ bits each, the right side of the equation above does not fit in ${\mathbb{F}}_n$
• The subtraction of the remainder’s limbs $r_0$ and $r_1$ could require borrowing

For the moment, let’s not worry about the possibility of borrows and instead focus on the first problem.

Combining multiplications

The first problem is that our native field is too small to constrain $2^{2\ell }(p_2-r_2)+2^{\ell }(p_1-r_1)+p_0-r_0=0\mathrm{mod}{2}^t$. We could split this up by multiplying $a\cdot b$ and $q\cdot f^{\prime }$ separately and create constraints that carefully track borrows and carries between limbs. However, a more efficient approach is combined the whole computation together and accumulate all the carries and borrows in order to reduce their number.

The trick is to assume a space large enough to hold the computation, view the outcome in binary and then split it up into chunks that fit in the native modulus.

To this end, it helps to know how many bits these intermediate products require. On the left side of the equation, $p_0$ is at most $2\ell +1$ bits. We can compute this by substituting the maximum possible binary values (all bits set to 1) into $p_0=a_0{b}_0+q_0{f}_0^{\prime }$ like this

$$\begin{array}{rl}\mathsf{maxbits}(p_0)& ={\log }_2(\underset{a_0}{\underbrace{(2^{\ell }-1)}}\underset{b_0}{\underbrace{(2^{\ell }-1)}}+\underset{q_0}{\underbrace{(2^{\ell }-1)}}\underset{f_0^{\prime }}{\underbrace{(2^{\ell }-1)}})\\ & ={\log }_2(2(2^{2\ell }-2^{\ell +1}+1))\\ & ={\log }_2(2^{2\ell +1}-2^{\ell +2}+2).\end{array}$$

So $p_0$ fits in $2\ell +1$ bits. Similarly, $p_1$ needs at most $2\ell +2$ bits and $p_2$ is at most $2\ell +3$ bits.

The diagram below shows the right hand side of the zero-sum equality from equation (2). That is, the value $p-r$. Let’s look at how the different bits of $p_0,p_1,p_2,r_0,r_1$ and $r_2$ impact it.

0             L             2L            3L            4L
|-------------|-------------|-------------|-------------|-------------|
                            :
|--------------p0-----------:-| 2L + 1
                            :
              |-------------:-p1------------| 2L + 2
                    p10➚    :        p11➚
                            |----------------p2-------------| 2L + 3
                            :
|-----r0------|             :
                            :
              |-----r1------|
                            :
                            |-----r2------|
\__________________________/ \______________________________/
             ≈ h0                           ≈ h1

Within our native field modulus we can fit up to $2\ell +\delta <{\log }_2(n)$ bits, for small values of $\delta$ (but sufficient for our case). Thus, we can only constrain approximately half of $p-r$ at a time. In the diagram above the vertical line at 2L bisects $p-r$ into two $\approx 2\ell$ bit values: $h_0$ and $h_1$ (the exact definition of these values follow). Our goal is to constrain $h_0$ and $h_1$.

Computing the zero-sum halves: $h_0$ and $h_1$

Now we can derive how to compute $h_0$ and $h_1$ from $p$ and $r$.

The direct approach would be to bisect both $p_0$ and $p_1$ and then define $h_0$ as just the sum of the $2\ell$ lower bits of $p_0$ and $p_1$ minus $r_0$ and $r_1$. Similarly $h_1$ would be just the sum of upper bits of $p_0,p_1$ and $p_2$ minus $r_2$. However, each bisection requires constraints for the decomposition and range checks for the two halves. Thus, we would like to avoid bisections as they are expensive.

Ideally, if our $p$’s lined up on the $2\ell$ boundary, we would not need to bisect at all. However, we are unlucky and it seems like we must bisect both $p_0$ and $p_1$. Fortunately, we can at least avoid bisecting $p_0$ by allowing it to be summed into $h_0$ like this

$$h_0=p_0+2^{\ell }\cdot p_{10}-r_0-2^{\ell }\cdot r_1$$

Note that $h_0$ is actually greater than $2\ell$ bits in length. This may not only be because it contains $p_0$ whose length is $2\ell +1$, but also because adding $p_{10}$ may cause an overflow. The maximum length of $h_0$ is computed by substituting in the maximum possible binary value of $2^{\ell }-1$ for the added terms and $0$ for the subtracted terms of the above equation.

$$\begin{array}{rl}\mathsf{maxbits}(h_0)& ={\log }_2(\underset{p_0}{\underbrace{(2^{\ell }-1)(2^{\ell }-1)+(2^{\ell }-1)(2^{\ell }-1)}}+2^{\ell }\cdot \underset{p_{10}}{\underbrace{(2^{\ell }-1)}})\\ & ={\log }_2(2^{2\ell +1}-2^{\ell +2}+2+2^{2\ell }-2^{\ell })\\ & ={\log }_2(3\cdot 2^{2\ell }-5\cdot 2^{\ell }+2)\end{array}$$

which is $2\ell +2$ bits.

N.b. This computation assumes correct sizes values for $r_0$ and $r_1$, which we assure by range checks on the limbs.

Next, we compute $h_1$ as

$$h_1=p_{11}+p_2-r_2$$

The maximum size of $h_1$ is computed as

$$\begin{array}{rl}\mathsf{maxbits}(h_1)& =\mathsf{maxbits}(p_{11}+p_2)\end{array}$$

In order to obtain the maximum value of $p_{11}$, we define $p_{11}:=\frac{p_1}{2^{\ell }}$. Since the maximum value of $p_1$ was $2^{2\ell +2}-2^{\ell +3}+4$, then the maximum value of $p_{11}$ is $2^{\ell +2}-8$. For $p_2$, the maximum value was $6\cdot 2^{2\ell }-12\cdot 2^{\ell }+6$, and thus:

$$\begin{array}{rl}\mathsf{maxbits}(h_1)& =lo{g}_2(\underset{p_{11}}{\underbrace{2^{\ell +2}-8}}+\underset{p_2}{\underbrace{6\cdot 2^{2\ell }-12\cdot 2^{\ell }+6}})\\ & ={\log }_2(6\cdot 2^{2\ell }-8\cdot 2^{\ell }-2)\end{array}$$

which is $2\ell +3$ bits.

Thus far we have the following constraints

2. Composition of $p_{10}$ and $p_{11}$ result in $p_1$
3. Range check $p_{11}\in [0,2^{\ell +2})$
4. Range check $p_{10}\in [0,2^{\ell })$

For the next step we would like to constrain $h_0$ and $h_1$ to zero. Unfortunately, we are not able to do this!

• Firstly, as defined $h_0$ may not be zero because we have not bisected it precisely at $2\ell$ bits, but have allowed it to contain the full $2\ell +2$ bits. Recall that these two additional bits are because $p_0$ is at most $2\ell +1$ bits long, but also because adding $p_{10}$ increases it to $2\ell +2$. These two additional bits are not part of the first $2\ell$ bits of $p-r$ and, thus, are not necessarily zero. That is, they are added from the second $2\ell$ bits (i.e. $h_1$).

• Secondly, whilst the highest $\ell +3$ bits of $p-r$ would wrap to zero $\mathrm{mod}{2}^t$, when placed into the smaller $2\ell +3$ bit $h_1$ in the native field, this wrapping does not happen. Thus, $h_1$’s $\ell +3$ highest bits may be nonzero.

We can deal with this non-zero issue by computing carry witness values.

Computing carry witnesses values $v_0$ and $v_1$

Instead of constraining $h_0$ and $h_1$ to zero, there must be satisfying witness $v_0$ and $v_1$ such that the following constraints hold.

5. There exists $v_0$ such that $h_0=v_0\cdot 2^{2\ell }$
6. There exists $v_1$ such that $h_1=v_1\cdot 2^{\ell }-v_0$

Here $v_0$ is the last two bits of $h_0$’s $2\ell +2$ bits, i.e., the result of adding the highest bit of $p_0$ and any possible carry bit from the operation of $h_0$. Similarly, $v_1$ corresponds to the highest $\ell +3$ bits of $h_1$. It looks like this

0             L             2L            3L            4L
|-------------|-------------|-------------|-------------|-------------|
                            :
|--------------h0-----------:--| 2L + 2
                            : ↖v0
                            :-------------h1-------------| 2L + 3
                            :              \____________/
                            :                  v1➚

Remember we only need to prove the first $3\ell$ bits of $p-r$ are zero, since everything is $\mathrm{mod}{2}^t$ and $t=3\ell$. It may not be clear how this approach proves the $3\ell$ bits are indeed zero because within $h_0$ and $h_1$ there are bits that are nonzero. The key observation is that these bits are too high for $\mathrm{mod}{2}^t$.

By making the argument with $v_0$ and $v_1$ we are proving that $h_0$ is something where the $2\ell$ least significant bits are all zeros and that $h_1+v_0$ is something where the $\ell$ are also zeros. Any nonzero bits after $3\ell$ do not matter, since everything is $\mathrm{mod}{2}^t$.

All that remains is to range check $v_0$ and $v_1$

7. Range check $v_0\in [0,2^2)$
8. Range check $v_1=\in [0,2^{\ell +3})$

Subtractions

When unconstrained, computing $u_0=p_0+2^{\ell }\cdot p_{10}-(r_0+2^{\ell }\cdot r_1)$ could require borrowing. Fortunately, we have the constraint that the $2\ell$ least significant bits of $u_0$ are 0 (i.e. $u_0=2^{2\ell }\cdot v_0$), which means borrowing cannot happen.

Borrowing is prevented because when the $2\ell$ least significant bits of the result are 0 it is not possible for the minuend to be less than the subtrahend. We can prove this by contradiction.

Let

• $x=p_0+2^{\ell }\cdot p_{10}$
• $y=r_0+2^{\ell }\cdot r_1$
• the $2\ell$ least significant bits of $x-y$ be 0

Suppose that borrowing occurs, that is, that $x<y$. Recall that the length of $x$ is at most $2\ell +2$ bits. Therefore, since $x<y$ the top two bits of $x$ must be zero and so we have

$$x-y=x_{2\ell }-y,$$

where $x_{2\ell }$ denotes the $2\ell$ least significant bits of $x$.

Recall also that the length of $y$ is $2\ell$ bits. We know this because limbs of the result are each constrained to be in $[0,2^{\ell })$. So the result of this subtraction is $2\ell$ bits. Since the $2\ell$ least significant bits of the subtraction are 0 this means that

$$\begin{array}{rl}x-y& =0\\ x& =y,\end{array}$$

which is a contradiction with $x<y$.

Costs

Range checks should be the dominant cost, let’s see how many we have.

Range check (3) requires two range checks for $p_{11}=p_{111}\cdot 2^{\ell }+p_{110}$

• a) $p_{110}\in [0,2^{\ell })$
• b) $p_{111}\in [0,2^2)$

Range check (8) requires two range checks and a decomposition check that is merged in (6).

• a) $v_{10}\in [0,2^{\ell })$
• b) $v_{11}\in [0,2^3)$

The range checks on $p_0,p_1$ and $p_2$ follow from the range checks on $a,b$ and $q$.

So we have 3.a, 3.b, 4, 7, 8.a, 8.b.

So we have 1 multi-range-check, 1 single-range-check and 2 low-degree range checks. This consumes just over 5 rows.

Use CRT to constrain $a\cdot b-q\cdot f-r\equiv 0\mathrm{mod}n$

Until now we have constrained the equation $\mathrm{mod}{2}^t$, but remember that our application of the CRT means that we must also constrain the equation $\mathrm{mod}n$. We are leveraging the fact that if the identity holds for all moduli in $\mathcal{M}=\{n,2^t\}$, then it holds for $\mathtt{lcm}(\mathcal{M})=2^t\cdot n=M$.

Thus, we must check $a\cdot b-q\cdot f-r\equiv 0\mathrm{mod}n$, which is over ${\mathbb{F}}_n$.

This gives us equality $\mathrm{mod}{2}^t\cdot n$ as long as the divisors are coprime. That is, as long as $\mathsf{gcd}(2^t,n)=1$. Since the native modulus $n$ is prime, this is true.

Thus, to perform this check is simple. We compute

$$\begin{array}{rl}{a}_n& =a\mathrm{mod}n\\ b_n& =b\mathrm{mod}n\\ q_n& =q\mathrm{mod}n\\ r_n& =r\mathrm{mod}n\\ f_n& =f\mathrm{mod}n\end{array}$$

using our native field modulus with constraints like this

$$\begin{array}{rl}{a}_n& =2^{2\ell }\cdot a_2+2^{\ell }\cdot a_1+a_0\\ b_n& =2^{2\ell }\cdot b_2+2^{\ell }\cdot b_1+b_0\\ q_n& =2^{2\ell }\cdot q_2+2^{\ell }\cdot q_1+q_0\\ r_n& =2^{2\ell }\cdot r_2+2^{\ell }\cdot r_1+r_0\\ f_n& =2^{2\ell }\cdot f_2+2^{\ell }\cdot f_1+f_0\end{array}$$

and then constrain

$$a_n\cdot b_n-q_n\cdot f_n-r_n=0\mathrm{mod}n.$$

Note that we do not use the negated foreign field modulus here.

This requires a single constraint of the form

9. $a_n\cdot b_n-q_n\cdot f_n=r_n$

with all of the terms expanded into the limbs according the above equations. The values $a_n,b_n,q_n,f_n$ and $r_n$ do not need to be in the witness.

Range check both sides of $a\cdot b=q\cdot f+r$

Until now we have constrained that equation $a\cdot b=q\cdot f+r$ holds modulo $2^t$ and modulo $n$, so by the CRT it holds modulo $M=2^t\cdot n$. Remember that, as outlined in the “Overview” section, we must prove our equation over the positive integers, rather than $\mathrm{mod}M$. By doing so, we assure that our solution is not equal to some $q^{\prime }\cdot M+r^{\prime }$ where $q^{\prime },r^{\prime }\in F_M$, in which case $q$ or $r$ would be invalid.

First, let’s consider the right hand side $q\cdot f+r$. We have

$$q\cdot f+r<2^t\cdot n$$

Recall that we have parameterized $2^t\cdot n\ge f^2$, so if we can bound $q$ and $r$ such that

$$q\cdot f+r<f^2$$

then we have achieved our goal. We know that $q$ must be less than $f$, so that is our first check, leaving us with

$$\begin{array}{rl}(f-1)\cdot f+r& <f^2\\ r& <f^2-(f-1)\cdot f=f\end{array}$$

Therefore, to check $q\cdot f+r<2^t\cdot n$, we need to check

• $q<f$
• $r<f$

This should come at no surprise, since that is how we parameterized $2^t\cdot n$ earlier on. Note that by checking $q<f$ we assure correctness, while checking $r<f$ assures our solution is unique (sometimes referred to as canonical).

Next, we must perform the same checks for the left hand side (i.e., $a\cdot b<2^t\cdot n$). Since $a$ and $b$ must be less than the foreign field modulus $f$, this means checking

• $a<f$
• $b<f$

So we have

$$\begin{array}{rl}a\cdot b& \le (f-1)\cdot (f-1)=f^2-2f+1\end{array}$$

Since $2^t\cdot n\ge f^2$ we have

$$\begin{array}{rl}& f^2-2f+1<f^2\le 2^t\cdot n\\ & ⟹a\cdot b<2^t\cdot n\end{array}$$

Bound checks

To perform the above range checks we use the upper bound check method described in the upper bound check section in Foreign Field Addition.

The upper bound check is as follows. We must constrain $0\le q<f$ over the positive integers, so

$$\begin{array}{rl}{2}^t\le q& +2^t<f+2^t\\ 2^t-f\le q& +2^t-f<2^t\end{array}$$

Remember $f^{\prime }=2^t-f$ is our negated foreign field modulus. Thus, we have

$$\begin{array}{rl}{f}^{\prime }\le q& +f^{\prime }<2^t\end{array}$$

So to check $q<t$ we just need to compute $q^{\prime }=q+f^{\prime }$ and check $f^{\prime }\le q^{\prime }<2^t$

Observe that

$$0\le q⟹f^{\prime }\le q^{\prime }$$

and that

$$q^{\prime }<2^t⟹q<f$$

So we only need to check

• $0\le q$
• $q^{\prime }<2^t$

The first check is always true since we are operating over the positive integers and $q\in {\mathbb{Z}}^{+}$. Observe that the second check also constrains that $q<2^t$, since $f\le 2^{259}<2^t$ and thus

$$\begin{array}{rl}{q}^{\prime }& \le 2^t\\ q+f^{\prime }& \le 2^t\\ q& \le 2^t-(2^t-f)=f\\ q& <2^t\end{array}$$

Therefore, to constrain $q<f$ we only need constraints for

• $q^{\prime }=q+f^{\prime }$
• $q^{\prime }<2^t$

and we don’t require an additional multi-range-check for $q<2^t$.

Cost of bound checks

This section analyzes the structure and costs of bounds checks for foreign field addition and foreign field multiplication.

Addition

In our foreign field addition design the operands $a$ and $b$ do not need to be less than $f$. The field overflow bit $o$ for foreign field addition is at most 1. That is, $a+b=o\cdot f+r$, where $r$ is allowed to be greater than $f$. Therefore,

$$(f+a)+(f+b)=1\cdot f+(f+a+b)$$

These can be chained along $k$ times as desired. The final result

$$r=(\underset{k}{\underbrace{f+\cdots +f}}+a_1+b_1+\cdots a_k+b_k)$$

Since the bit length of $r$ increases logarithmically with the number of additions, in Kimchi we must only check that the final $r$ in the chain is less than $f$ to constrain the entire chain.

Security note: In order to defer the $r<f$ check to the end of any chain of additions, it is extremely important to consider the potential impact of wraparound in ${\mathbb{F}}_n$. That is, we need to consider whether the addition of a large chain of elements greater than the foreign field modulus could wrap around. If this could happen then the $r<f$ check could fail to detect an invalid witness. Below we will show that this is not possible in Kimchi.

Recall that our foreign field elements are comprised of 3 limbs of 88-bits each that are each represented as native field elements in our proof system. In order to wrap around and circumvent the $r<f$ check, the highest limb would need to wrap around. This means that an attacker would need to perform about $k\approx n/2^{\ell }$ additions of elements greater than then foreign field modulus. Since Kimchi’s native moduli (Pallas and Vesta) are 255-bits, the attacker would need to provide a witness for about $k\approx 2^{167}$ additions. This length of witness is greater than Kimchi’s maximum circuit (resp. witness) length. Thus, it is not possible for the attacker to generate a false proof by causing wraparound with a large chain of additions.

In summary, for foreign field addition in Kimchi it is sufficient to only bound check the last result $r^{\prime }$ in a chain of additions (and subtractions)

• Compute bound $r^{\prime }=r+f^{\prime }$ with addition gate (2 rows)
• Range check $r^{\prime }<2^t$ (4 rows)

Multiplication

In foreign field multiplication, the situation is unfortunately different, and we must check that each of $a,b,q$ and $r$ are less than $f$. We cannot adopt the strategy from foreign field addition where the operands are allowed to be greater than $f$ because the bit length of $r$ would increases linearly with the number of multiplications. That is,

$$(a_1+f)\cdot (a_2+f)=1\cdot f+\underset{r}{\underbrace{f^2+(a_1+a_2-1)\cdot f+a_1\cdot a_2}}$$

and after a chain of $k$ multiplication we have

$$r=f^k+\dots +a_1\cdots a_k$$

where $r>f^k$ quickly overflows our CRT modulus $2^t\cdot n$. For example, assuming our maximum foreign modulus of $f=2^{259}$ and either of Kimchi’s native moduli (i.e. Pallas or Vesta), $f^k>2^t\cdot n$ for $k>2$. That is, an overflow is possible for a chain of greater than 1 foreign field multiplication. Thus, we must check $a,b,q$ and $r$ are less than $f$ for each multiplication.

Fortunately, in many situations the input operands may already be checked either as inputs or as outputs of previous operations, so they may not be required for each multiplication operation.

Thus, the $q^{\prime }$ and $r^{\prime }$ checks (or equivalently $q$ and $r$) are our main focus because they must be done for every multiplication.

• Compute bound $q^{\prime }=q+f^{\prime }$ with addition gate (2 rows)
• Compute bound $r^{\prime }=r+f^{\prime }$ with addition gate (2 rows)
• Range check $q^{\prime }<2^t$ (4 rows)
• Range check $r^{\prime }<2^t$ (4 rows)

This costs 12 rows per multiplication. In a subsequent section, we will reduce it to 8 rows.

2-limb decomposition

Due to the limited number of permutable cells per gate, we do not have enough cells for copy constraining $q^{\prime }$ and $r^{\prime }$ (or $q$ and $r$) to their respective range check gadgets. To address this issue, we must decompose $q^{\prime }$ into 2 limbs instead of 3, like so

$$q^{\prime }=q_{01}^{\prime }+2^{2\ell }\cdot q_2^{\prime }$$

and

$$q_{01}^{\prime }=q_0^{\prime }+2^{\ell }\cdot q_1^{\prime }$$

Thus, $q^{\prime }$ is decomposed into two limbs $q_{01}^{\prime }$ (at most $2\ell$ bits) and $q_2^{\prime }$ (at most $\ell$ bits).

Note that $q^{\prime }$ must be range checked by a multi-range-check gadget. To do this the multi-range-check gadget must

• Store a copy of the limbs $q_0^{\prime },q_1^{\prime }$ and $q_2^{\prime }$ in its witness
• Range check that they are $\ell$ bit each
• Constrain that $q_{01}^{\prime }=q_0^{\prime }+2^{\ell }\cdot q_1^{\prime }$ (this is done with a special mode of the multi-range-check gadget)
• Have copy constraints for $q_{01}^{\prime }$ and $q_2^{\prime }$ as outputs of the ForeignFieldMul gate and inputs to the multi-range-check gadget

Note that since the foreign field multiplication gate computes $q^{\prime }$ from $q$ which is already in the witness and $q_{01}^{\prime }$ and $q_2^{\prime }$ have copy constraints to a multi-range-check gadget that fully constrains their decomposition from $q^{\prime }$, then the ForeignFieldMul gate does not need to store an additional copy of $q_0^{\prime }$ and $q_1^{\prime }$.

An optimization

Since the $q<f$ and $r<f$ checks must be done for each multiplication it makes sense to integrate them into the foreign field multiplication gate. By doing this we can save 4 rows per multiplication.

Doing this doesn’t require adding a lot more witness data because the operands for the bound computations $q^{\prime }=q+f^{\prime }$ and $r^{\prime }=r+f^{\prime }$ are already present in the witness of the multiplication gate. We only need to store the bounds $q^{\prime }$ and $r^{\prime }$ in permutable witness cells so that they may be copied to multi-range-check gates to check they are each less than $2^t$.

To constrain $x+f^{\prime }=x^{\prime }$, the equation we use is

$$x+2^t=o\cdot f+x^{\prime },$$

where $x$ is the original value, $o=1$ is the field overflow bit and $x^{\prime }$ is the remainder and our desired addition result (e.g. the bound). Rearranging things we get

$$x+2^t-f=x^{\prime },$$

which is just

$$x+f^{\prime }=x^{\prime },$$

Recall from the section “Avoiding borrows” that $f^{\prime }$ is often larger than $f$. At first this seems like it could be a problem because in multiplication each operation must be less than $f$. However, this is because the maximum size of the multiplication was quadratic in the size of $f$ (we use the CRT, which requires the bound that $a\cdot b<2^t\cdot n$). However, for addition the result is much smaller and we do not require the CRT nor the assumption that the operands are smaller than $f$. Thus, we have plenty of space in $\ell$-bit limbs to perform our addition.

So, the equation we need to constrain is

$$x+f^{\prime }=x^{\prime }.$$

We can expand the left hand side into the 2 limb format in order to obtain 2 intermediate sums

$$\begin{array}{r}{s}_{01}=x_{01}+f_{01}^{\prime }\\ s_2=x_2+f_2^{\prime }\end{array}$$

where $x_{01}$ and $f_{01}^{\prime }$ are defined like this

$$\begin{array}{r}{x}_{01}=x_0+2^{\ell }\cdot x_1\\ f_{01}^{\prime }=f_0^{\prime }+2^{\ell }\cdot f_1^{\prime }\end{array}$$

and $x$ and $f^{\prime }$ are defined like this

$$\begin{array}{r}x=x_{01}+2^{2\ell }\cdot x_2\\ f^{\prime }=f_{01}^{\prime }+2^{2\ell }\cdot f_2^{\prime }\end{array}$$

Going back to our intermediate sums, the maximum bit length of sum $s_{01}$ is computed from the maximum bit lengths of $x_{01}$ and $f_{01}^{\prime }$

$$\underset{x_{01}}{\underbrace{(2^{\ell }-1)+2^{\ell }\cdot (2^{\ell }-1)}}+\underset{f_{01}^{\prime }}{\underbrace{(2^{\ell }-1)+2^{\ell }\cdot (2^{\ell }-1)}}=2^{2\ell +1}-2,$$

which means $s_{01}$ is at most $2\ell +1$ bits long.

Similarly, since $x_2$ and $f_2^{\prime }$ are less than $2^{\ell }$, the max value of $s_2$ is

$$(2^{\ell }-1)+(2^{\ell }-1)=2^{\ell +1}-2,$$

which means $s_2$ is at most $\ell +1$ bits long.

Thus, we must constrain

$$s_{01}+2^{2\ell }\cdot s_2-x_{01}^{\prime }-2^{2\ell }\cdot x_2^{\prime }=0\mathrm{mod}{2}^t.$$

The accumulation of this into parts looks like this.

0             L             2L            3L=t          4L
|-------------|-------------|-------------|-------------|-------------|
                            :
|------------s01------------:-| 2L + 1
                            : ↖w01
                            |------s2-----:-| L + 1
                            :               ↖w2
                            :
|------------x'01-----------|
                            :
                            |------x'2----|
                            :
\____________________________/
             ≈ z01           \_____________/
                                   ≈ z2

The two parts are computed with

$$\begin{array}{rl}{z}_{01}& =s_{01}-x_{01}^{\prime }\\ z_2& =s_2-x_2^{\prime }.\end{array}$$

Therefore, there are two carry bits $w_{01}$ and $w_2$ such that

$$\begin{array}{rl}{z}_{01}& =2^{2\ell }\cdot w_{01}\\ z_2+w_{01}& =2^{\ell }\cdot w_2\end{array}$$

In this scheme $x_{01}^{\prime },x_2^{\prime },w_{01}$ and $w_2$ are witness data, whereas $s_{01}$ and $s_2$ are formed from a constrained computation of witness data $x_{01},x_2$ and constraint system public parameter $f^{\prime }$. Note that due to carrying, witness $x_{01}^{\prime }$ and $x_2^{\prime }$ can be different than the values $s_{01}$ and $s_2$ computed from the limbs.

Thus, each bound addition $x+f^{\prime }$ requires the following witness data

• $x_{01},x_2$
• $x_{01}^{\prime },x_2^{\prime }$
• $w_{01},w_2$

where $f^{\prime }$ is baked into the gate coefficients. The following constraints are needed

• $2^{2\ell }\cdot w_{01}=s_{01}-x_{01}^{\prime }$
• $2^{\ell }\cdot w_2=s_2+w_{01}-x_2^{\prime }$
• $x_{01}^{\prime }\in [0,2^{2\ell })$
• $x_2^{\prime }\in [0,2^{\ell })$
• $w_{01}\in [0,2)$
• $w_2\in [0,2)$

Due to the limited number of copyable witness cells per gate, we are currently only performing this optimization for $q$.

The witness data is

• $q_0,q_1,q_2$
• $q_{01}^{\prime },q_2^{\prime }$
• $q_{carry01}^{\prime },q_{carry2}^{\prime }$

The checks are

1. $q_0\in [0,2^{\ell })$
2. $q_1\in [0,2^{\ell })$
3. $q_0^{\prime }=q_0+f_0^{\prime }$
4. $q_1^{\prime }=q_1+f_1^{\prime }$
5. $s_{01}=q_0^{\prime }+2^{\ell }\cdot q_1^{\prime }$
6. $q_{01}^{\prime }\in [0,2^{2\ell })$
7. $q_{01}^{\prime }=q_0^{\prime }+2^{\ell }\cdot q_1^{\prime }$
8. $q_{carry01}^{\prime }\in [0,2)$
9. $2^{2\ell }\cdot q_{carry01}^{\prime }=s_{01}-q_{01}^{\prime }$
10. $q_2\in [0,2^{\ell })$
11. $s_2=q_2+f_2^{\prime }$
12. $q_{carry2}^{\prime }\in [0,2)$
13. $2^{\ell }\cdot q_{carry2}^{\prime }=s_2+w_{01}-q_2^{\prime }$

Checks (1) - (5) assure that $s_{01}$ is at most $2\ell +1$ bits. Whereas checks (10) - (11) assure that $s_2$ is at most $\ell +1$ bits. Altogether they are comprise a single multi-range-check of $q_0,q_1$ and $q_2$. However, as noted above, we do not have enough copyable cells to output $q_1,q_2$ and $q_3$ to the multi-range-check gadget. Therefore, we adopt a strategy where the 2 limbs $q_{01}^{\prime }$ and $q_2^{\prime }$ are output to the multi-range-check gadget where the decomposition of $q_0^{\prime }$ and $q_2^{\prime }$ into $q_{01}^{\prime }=p_0+2^{\ell }\cdot p_1$ is constrained and then $q_0^{\prime },q_1^{\prime }$ and $q_2^{\prime }$ are range checked.

Although $q_1,q_2$ and $q_3$ are not range checked directly, this is safe because, as shown in the “Bound checks” section, range-checking that $q^{\prime }\in [0,2^t)$ also constrains that $q\in [0,2^t)$. Therefore, the updated checks are

1. $q_0\in [0,2^{\ell })$ multi-range-check
2. $q_1\in [0,2^{\ell })$ multi-range-check
3. $q_0^{\prime }=q_0+f_0^{\prime }$ ForeignFieldMul
4. $q_1^{\prime }=q_1+f_1^{\prime }$ ForeignFieldMul
5. $s_{01}=q_0^{\prime }+2^{\ell }\cdot q_1^{\prime }$ ForeignFieldMul
6. $q_{01}^{\prime }=q_0^{\prime }+2^{\ell }\cdot q_1^{\prime }$ multi-range-check
7. $q_{carry01}^{\prime }\in [0,2)$ ForeignFieldMul
8. $2^{2\ell }\cdot q_{carry01}^{\prime }=s_{01}-q_{01}^{\prime }$ ForeignFieldMul
9. $q_2\in [0,2^{\ell })$ multi-range-check
10. $s_2=q_2+f_2^{\prime }$ ForeignFieldMul
11. $q_{carry2}^{\prime }\in [0,2)$ ForeignFieldMul
12. $2^{\ell }\cdot q_{carry2}^{\prime }=s_2+q_{carry01}^{\prime }-q_2^{\prime }$ ForeignFieldMul