MUL Constraints

Enforcing unsigned-integer-multiplication relations

Multiplication constraints let us capture the unsigned integer multiplication of 64-bit words. We now fix a total number of MUL constraints, $n_\text{mul}$ . For each $x \in \{0, \ldots , n_\text{mul} - 1\}$ , the $x$ ^th MUL constraint is a tuple $(L^p_x, L^q_x, L^\text{hi}_x, L^\text{lo}_x)$ of four lists of shifted value indices.

The Constraint Arrays

Immediately adopting the constraint array formalism, we now obtain length- $n_\text{mul}$ arrays $p$ , $q$ , $\text{lo}$ , and $\text{hi}$ of 64-bit words, defined, for each $x \in \{0, \ldots , n_\text{mul} - 1\}$ , by:

\begin{align*} p[x] \coloneqq \bigoplus_{(y, \text{op}, s) \in L^p_x} \text{op}(w[y], s), \\ q[x] \coloneqq \bigoplus_{(y, \text{op}, s) \in L^q_x} \text{op}(w[y], s), \\ \text{lo}[x] \coloneqq \bigoplus_{(y, \text{op}, s) \in L^\text{lo}_x} \text{op}(w[y], s), \\ \text{hi}[x] \coloneqq \bigoplus_{(y, \text{op}, s) \in L^\text{hi}_x} \text{op}(w[y], s). \\ \end{align*}

The prover data $w$ fulfills the constraint system's MUL constraints if, for each $x \in \{0, \ldots , n_\text{mul} - 1\}$ ,

\begin{equation*}p[x] \cdot q[x] \stackrel{?}= 2^{64} \cdot \text{hi}[x] + \text{lo}[x]\end{equation*}

holds over the integers. We interpret all of the words $p[x]$ , $q[x]$ , $\text{hi}[x]$ and $\text{lo}[x]$ as as elements of $\{0, \ldots , 2^{64} - 1\}$ , and interpret the $\cdot$ symbol as integer multiplication. That is, the product $p[x] \cdot q[x]$ is double-width; its high and low halves are given by $\text{hi}[x]$ and $\text{lo}[x]$ .