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
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 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.
In the above, the columns have the following meanings:
- Periodic columns
and . These columns contain values needed to switch various constraint on or off. contains a repeating sequence of a single one, followed by 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:
a | b | x0 | x1 | x2 | x3 | y0 | y1 | y2 | y3 | zp | z |
---|---|---|---|---|---|---|---|---|---|---|---|
10 | 9 | 0 | 1 | 0 | 1 | 1 | 0 | 0 | 1 | 0 | 8 |
163 | 157 | 1 | 1 | 0 | 0 | 1 | 0 | 1 | 1 | 8 | 129 |
2615 | 2526 | 1 | 1 | 1 | 0 | 0 | 1 | 1 | 1 | 129 | 2070 |
41851 | 40426 | 1 | 1 | 0 | 1 | 0 | 1 | 0 | 1 | 2070 | 33130 |
Here, in the first row, we set each of the b1010
and b1001
). Column b1000
), while column
With every subsequent row, we inject the next-most-significant 4 bits of each value into the bit columns, increase the
Constraints¶
AIR constraints needed to ensure the correctness of the above table are described below. We also add one more column 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
Then, we need to make sure that on the first row of every 8-row cycle, the values in the columns
The above constraints enforce that when
Lastly, we need to make sure that for all rows in an 8-row cycle except for the last one, the values in
The above constraints enforce that when
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
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
Where,
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
First, we’ll define another intermediate variable
Then, setting
The above ensures that when
The response side of the bus communication can be enforced with the following constraint: