Multiplying in the Exponent

Here, we explain a fairly simple mathematical idea that underpins our multiplication technique. We fix a number $n_\text{mul}$ of MUL constraints; we recall the constraint arrays $p$, $q$, $\text{lo}$ and $\text{hi}$. Each of these arrays is of length $n_\text{mul}$ and contains 64-bit words.

For each $x \in \{0, \ldots , n_\text{mul} - 1\}$, $p[x]$ and $q[x]$ are in $\{0, \ldots , 2^{64} - 1\}$. We're interested in $p[x] \cdot q[x]$. Recall that we work throughout with binary fields. This means that we can't use typical prime-field ideas (like breaking our numbers into limbs so small that their products don't overflow the characteristic, using range checks, and so on).

The Exponentiation Identity

The idea is to use the basic identity $(g^{p[x]})^{q[x]} = g^{p[x] \cdot q[x]}$. This is true in all rings, but we have to be careful about reduction in the exponent.

We recall that the multiplicative group of units $\mathbb{F}_{2^{128}}^*$ is cyclic; we fix a generator $g \in \mathbb{F}_{2^{128}}^*$. Thus, the multiplicative order of $g$ in $\mathbb{F}_{2^{128}}$ is $2^{128} - 1$.

For each $x \in \{0, \ldots , n_\text{mul} - 1\}$, the array elements $p[x]$, $q[x]$, $\text{lo}[x]$ and $\text{hi}[x]$ are all elements of $\{0, \ldots , 2^{64} - 1\}$. Our goal is to check whether

holds as integers. By the basic properties of rings, we know that

holds if and only if $r \equiv s \pmod{\text{ord}(g)}$; in our case, we conclude that

holds in in $\mathbb{F}_{2^{128}}$ if and only if

Controlling Wraparound

If $p[x] \cdot q[x] \stackrel{?}= 2^{64} \cdot \text{hi}[x] + \text{lo}[x]$ holds as integers, then it definitely also holds modulo $2^{128} - 1$. The converse is not quite true, as we now explain. Since

$p[x] \cdot q[x]$ can't wrap around modulo $2^{128} - 1$. On the other hand, since

$2^{64} \cdot \text{hi}[x] + \text{lo}[x]$ can wrap around only in the case of a direct equality $2^{64} \cdot \text{hi}[x] + \text{lo}[x] = 2^{128} - 1$. This equality happens if and only if $\text{lo}[x]$ and $\text{hi}[x]$ are both $2^{64} - 1$; and indeed, by choosing at least one of $p[x]$ and $q[x]$ to be zero, the prover could get a case in which $p[x] \cdot q[x] \stackrel{?}= 2^{64} \cdot \text{hi}[x] + \text{lo}[x]$ holds modulo $2^{128} - 1$ but not over the integers.

In this latter case, $p[x] \cdot q[x]$ is even, while $2^{64} \cdot \text{hi}[x] + \text{lo}[x]$ is odd. To eliminate it, it thus suffices to ensure to boot that

This latter equality is easy to check, since it only depends on the least-significant bits of $p$, $q$ and $\text{lo}$. One simple way to do this is to use AND constraints. It's enough to add 3 new witness words, say $p'$, $q'$, and $\text{lo}'$, and to constrain that

as well as that $p = p'$, $q = q'$, and $\text{lo} = \text{lo}'$. The total cost for this is 3 new witness components and 4 new AND constraints (we note that MUL is already much costlier than AND, on a per-constraint basis).

Putting it Together

Assuming that the above issue has been separately resolved, we see that the MUL constraint

holds over the integers if and only if

holds in $\mathbb{F}_{2^{128}}$. We spend the rest of this site section explaining how to check the exponent condition above.