AND Constraints

As usual, we write $w$ for the full list of prover data (a concatenation of constant, input–output, and witness data). Each component of $w$ is a 64-bit word. We saw already that shifted value indices are tuple $(y, \text{op}, s) \in W \times \{\mathsf{sll}, \mathsf{srl}, \mathsf{sra}\} \times \{0, \ldots , 63\}$ consisting of an index $y$ into the prover's runtime-dependent data, a shift type $\text{op}$, and a shift amount $s$.

An AND constraint, by definition, is three lists of shifted value indices, say $(L^a, L^b, L^c)$. We say that the AND constraint $(L^a, L^b, L^c)$ holds with respect to candidate prover data $w$ if and only if:

Note that both sides of this equality are 64-bit words; the symbol $\&$ is a bitwise AND of 64-bit words.

Each given constraint system will specify, first, the total number $n_\text{and}$ of AND constraints; it will moreover supply $n_\text{and}$ triples $(L^a_x, L^b_x, L^c_x)$ of the form already given above, for $x \in \{0, \ldots , n_\text{and} - 1\}$. We will say that the prover data $w$ fulfills the constraint system's AND constraints if and only if for each $x \in \{0, \ldots , n_\text{and} - 1\}$, the above equality holds over $w$ with respect to the $x$^th triple $(L^a_x, L^b_x, L^c_x)$.

The Constraint Arrays

We now apply the constraint array formalism to this condition. Applying it, we get arrays $a$, $b$ and $c$, containing $n_\text{and}$ 64-bit words, defined by the equalities:

Having defined these arrays, we can now say that our constraint system's AND constraints are fulfilled if and only if

holds for each $x \in \{0, \ldots , n_\text{and} - 1\}$.

Completeness

We pause here to argue that our constraint system is at least as powerful as a complete system of boolean circuits on 64-bit words (in fact, it's much more powerful, in concrete terms).

Bitwise AND is supported at the native level. Note that, technically, we can only act on values that have been shifted "somehow"; in order to get non-shifts, we can just use $\text{op} = \textsf{sll}$ and $s = 0$.

In order to constrain that a wire $z$ equals the bitwise XOR of wires $x$ and $y$, we can add a constraint to the effect of

x ⊕ y & 0xFFFFFFFFFFFFFFFF = z.

Bitwise NOT is similar; to obtain a wire $y = \overline{x}$, we can constrain

x & 0xFFFFFFFFFFFFFFFF = y ⊕ 0xFFFFFFFFFFFFFFFF.

Since $z = x \vee y$ is equivalent to $\overline{z} = \overline{x} \mathrel{\&} \overline{y}$, we can use

x ⊕ 0xFFFFFFFFFFFFFFFF & y ⊕ 0xFFFFFFFFFFFFFFFF = z ⊕ 0xFFFFFFFFFFFFFFFF

to get bitwise OR. Alternatively, the expression

x & y = x ⊕ y ⊕ z

also works.