Skip to main content
Version: 0.11 (stable)

Bitwise chiplet

In this note we describe how to compute bitwise AND and XOR operations on 32-bit values and the constraints required for proving correct execution.

Assume that aa and bb are field elements in a 64-bit prime field. Assume also that aa and bb are known to contain values smaller than 2322^{32}. We want to compute abza \oplus b \rightarrow z, where \oplus is either bitwise AND or XOR, and zz is a field element containing the result of the corresponding bitwise operation.

First, observe that we can compute AND and XOR relations for single bit values as follows:

and(a,b)=aband(a, b) = a \cdot b xor(a,b)=a+b2abxor(a, b) = a + b - 2 \cdot a \cdot b

To compute bitwise operations for multi-bit values, we will decompose the values into individual bits, apply the operations to single bits, and then aggregate the bitwise results into the final result.

To perform this operation we will use a table with 12 columns, and computing a single AND or XOR operation will require 8 table rows. We will also rely on two periodic columns as shown below.

bitwise_execution_trace

In the above, the columns have the following meanings:

  • Periodic columns k0k_0 and k1k_1. These columns contain values needed to switch various constraints on or off. k0k_0 contains a single one, followed by a repeating sequence of seven zeros. k1k_1 contains a repeating sequence of seven ones, followed by a single zero.
  • Input columns aa and bb. On the first row of each 8-row cycle, the prover will set values in these columns to the upper 4 bits of the values to which a bitwise operation is to be applied. For all subsequent rows, we will append the next-most-significant 4-bit limb to each value. Thus, by the final row columns aa and bb will contain the full input values for the bitwise operation.
  • Columns a0a_0, a1a_1, a2a_2, a3a_3, b0b_0, b1b_1, b2b_2, b3b_3 will contain lower 4 bits of their corresponding values.
  • Output column zpz_p. This column represents the value of column zz for the prior row. For the first row, it is set to 00.
  • Output column zz. This column will be used to aggregate the results of bitwise operations performed over columns a0a_0, a1a_1, a2a_2, a3a_3, b0b_0, b1b_1, b2b_2, b3b_3. By the time we get to the last row in each 8-row cycle, this column will contain the final result.

Example

Let's illustrate the above table on a concrete example. For simplicity, we'll use 16-bit values, and thus, we'll only need 4 rows to complete the operation (rather than 8 for 32-bit values). Let's say a=41851a = 41851 (b1010_0011_0111_1011) and b=40426b = 40426 (b1001_1101_1110_1010), then and(a,b)=33130and(a, b) = 33130 (b1000_0001_0110_1010). The table for this computation looks like so:

aba0a1a2a3b0b1b2b3zpz
1090101100108
163157110010118129
26152526111001111292070
418514042611010101207033130

Here, in the first row, we set each of the aa and bb columns to the value of their most-significant 4-bit limb. The bit columns (a0..a3a_0 .. a_3 and b0..b3b_0 .. b_3) in the first row contain the lower 4 bits of their corresponding values (b1010 and b1001). Column zz contains the result of bitwise AND for the upper 4 bits (b1000), while column zpz_p contains that result for the prior row.

With every subsequent row, we inject the next-most-significant 4 bits of each value into the bit columns, increase the aa and bb columns accordingly, and aggregate the result of bitwise AND into the zz column, adding it to 242^4 times the value of zz in the previous row. We set column zpz_p to be the value of zz in the prior row. By the time we get to the last row, the zz column contains the result of the bitwise AND, while columns aa and bb contain their original values.

Constraints

AIR constraints needed to ensure the correctness of the above table are described below. We also add one more column ss to the execution trace, to allow us to select between two bitwise operations (U32AND and U32XOR).

Selectors

The Bitwise chiplet supports two operations with the following operation selectors:

  • U32AND: s=0s = 0
  • U32XOR: s=1s = 1

The constraints must require that the selectors be binary and stay the same throughout the cycle:

s2s=0 | degree=2s^2 - s = 0 \text{ | degree} = 2
k1(ss)=0 | degree=2k_1 \cdot (s' - s) = 0 \text{ | degree} = 2

Input decomposition

We need to make sure that inputs aa and bb are decomposed correctly into their individual bits. To do this, first, we need to make sure that columns a0a_0, a1a_1, a2a_2, a3a_3, b0b_0, b1b_1, b2b_2, b3b_3, can contain only binary values (00 or 11). This can be accomplished with the following constraints (for ii ranging between 00 and 33):

ai2ai=0 | degree=2a_i^2 - a_i = 0 \text{ | degree} = 2
bi2bi=0 | degree=2b_i^2 - b_i = 0 \text{ | degree} = 2

Then, we need to make sure that on the first row of every 8-row cycle, the values in the columns aa and bb are exactly equal to the aggregation of binary values contained in the individual bit columns aia_i, and bib_i. This can be enforced with the following constraints:

k0(ai=03(2iai))=0 | degree=2k_0 \cdot \left(a - \sum_{i=0}^3(2^i \cdot a_i)\right) = 0 \text{ | degree} = 2
k0(bi=03(2ibi))=0 | degree=2k_0 \cdot \left(b - \sum_{i=0}^3(2^i \cdot b_i)\right) = 0 \text{ | degree} = 2

The above constraints enforce that when k0=1k_0 = 1, a=i=03(2iai)a = \sum_{i=0}^3(2^i \cdot a_i) and b=i=03(2ibi)b = \sum_{i=0}^3(2^i \cdot b_i).

Lastly, we need to make sure that for all rows in an 8-row cycle except for the last one, the values in aa and bb columns are increased by the values contained in the individual bit columns aia_i and bib_i. Denoting aa as the value of column aa in the current row, and aa' as the value of column aa in the next row, we can enforce these conditions as follows:

k1(a(a16+i=03(2iai)))=0 | degree=2k_1 \cdot \left(a' - \left(a \cdot 16 + \sum_{i=0}^3(2^i \cdot a'_i)\right)\right) = 0 \text{ | degree} = 2
k1(b(b16+i=03(2ibi)))=0 | degree=2k_1 \cdot \left(b' - \left(b \cdot 16 + \sum_{i=0}^3(2^i \cdot b'_i)\right)\right) = 0 \text{ | degree} = 2

The above constraints enforce that when k1=1k_1 = 1 , a=16a+i=03(2iai)a' = 16 \cdot a + \sum_{i=0}^3(2^i \cdot a'_i) and b=16b+i=03(2ibi)b' = 16 \cdot b + \sum_{i=0}^3(2^i \cdot b'_i).

Output aggregation

To ensure correct aggregation of operations over individual bits, first we need to ensure that in the first row, the aggregated output value of the previous row should be 0.

k0zp=0 | degree=2k_0 \cdot z_p = 0 \text{ | degree} = 2

Next, we need to ensure that for each row except the last, the aggregated output value must equal the previous aggregated output value in the next row.

k1(zzp)=0 | degree=2k_1 \cdot \left(z - z'_p\right) = 0 \text{ | degree} = 2

Lastly, we need to ensure that for all rows the value in the zz column is computed by multiplying the previous output value (from the zpz_p column in the current row) by 16 and then adding it to the bitwise operation applied to the row's set of bits of aa and bb. The entire constraint must also be multiplied by the operation selector flag to ensure it is only applied for the appropriate operation.

For U32AND, this is enforced with the following constraint:

(1s)(z(zp16+i=03(2iaibi)))=0 | degree=3(1 - s) \cdot \left(z -(z_p \cdot 16 + \sum_{i=0}^3(2^i \cdot a_i \cdot b_i))\right) = 0 \text{ | degree} = 3

For U32XOR, this is enforced with the following constraint:

s(z(zp16+i=03(2i(ai+bi2aibi))))=0 | degree=3s \cdot \left(z -(z_p \cdot 16 + \sum_{i=0}^3(2^i \cdot (a_i + b_i - 2 \cdot a_i \cdot b_i)))\right) = 0 \text{ | degree} = 3

Chiplets bus constraints

To simplify the notation for describing bitwise constraints on the chiplets bus, we'll first define variable uu, which represents how aa, bb, and zz in the execution trace are reduced to a single value. Denoting the random values received from the verifier as α0,α1\alpha_0, \alpha_1, etc., this can be achieved as follows.

u=α0+α1opbit+α2a+α3b+α4zu = \alpha_0 + \alpha_1 \cdot op_{bit} + \alpha_2 \cdot a + \alpha_3 \cdot b + \alpha_4 \cdot z

Where, opbitop_{bit} is the unique operation label of the bitwise operation.

The request side of the constraint for the bitwise operation is described in the stack bitwise operation section.

To provide the results of bitwise operations to the chiplets bus, we want to include values of aa, bb and zz at the last row of the cycle.

First, we'll define another intermediate variable viv_i. It will include uu into the product when k1=0k_1 = 0. (uiu_i represents the value of uu for row ii of the trace.)

vi=(1k1)uiv_i = (1-k_1) \cdot u_i

Then, setting m=1k1m = 1 - k_1, we can compute the permutation product from the bitwise chiplet as follows:

i=0n(vimi+1mi)\prod_{i=0}^n (v_i \cdot m_i + 1 - m_i)

The above ensures that when 1k1=01 - k_1 = 0 (which is true for all rows in the 8-row cycle except for the last one), the product does not change. Otherwise, viv_i gets included into the product.

The response side of the bus communication can be enforced with the following constraint:

bchip=bchip(vimi+1mi) | degree=4b'_{chip} = b_{chip} \cdot (v_i \cdot m_i + 1 - m_i) \text{ | degree} = 4