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 and are field elements in a 64-bit prime field. Assume also that and are known to contain values smaller than . We want to compute , where is either bitwise AND or XOR, and 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:

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 bitwsie 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 and . These columns contain values needed to switch various constraints on or off. contains a single one, followed by a repeating sequence of seven zeros. contains a repeating sequence of seven ones, followed by a single zero.
  • Input columns and . 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 and will contain the full input values for the bitwise operation.
  • Columns , , , , , , , will contain lower 4 bits of their corresponding values.
  • Output column . This column represents the value of column for the prior row. For the first row, it is set to .
  • Output column . This column will be used to aggregate the results of bitwise operations performed over columns , , , , , , , . 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 (b1010_0011_0111_1011) and (b1001_1101_1110_1010), then (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 and columns to the value of their most-significant 4-bit limb. The bit columns ( and ) in the first row contain the lower 4 bits of their corresponding values (b1010 and b1001). Column contains the result of bitwise AND for the upper 4 bits (b1000), while column 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 and columns accordingly, and aggregate the result of bitwise AND into the column, adding it to times the value of in the previous row. We set column to be the value of in the prior row. By the time we get to the last row, the column contains the result of the bitwise AND, while columns and 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 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:
  • U32XOR:

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

Input decomposition

We need to make sure that inputs and are decomposed correctly into their individual bits. To do this, first, we need to make sure that columns , , , , , , , , can contain only binary values ( or ). This can be accomplished with the following constraints (for ranging between and ):

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

The above constraints enforce that when , and .

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

The above constraints enforce that when , and .

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.

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.

Lastly, we need to ensure that for all rows the value in the column is computed by multiplying the previous output value (from the column in the current row) by 16 and then adding it to the bitwise operation applied to the row's set of bits of and . 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:

For U32XOR, this is enforced with the following constraint:

Chiplets bus constraints

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

Where, 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 , and at the last row of the cycle.

First, we'll define another intermediate variable . It will include into the product when . ( represents the value of for row of the trace.)

Then, setting , we can compute the permutation product from the bitwise chiplet as follows:

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

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