Skip to main content

kimchi/circuits/polynomials/
xor.rs

1//! This module includes the definition of the XOR gadget for 64, 32, and 16 bits,
2//! the definition of the constraints of the `Xor16` circuit gate,
3//! and the code for witness generation for the XOR gadget.
4use crate::{
5    circuits::{
6        argument::{Argument, ArgumentEnv, ArgumentType},
7        berkeley_columns::BerkeleyChallengeTerm,
8        expr::{constraints::ExprOps, Cache},
9        gate::{CircuitGate, Connect, GateType},
10        lookup::{
11            self,
12            tables::{GateLookupTable, LookupTable},
13        },
14        polynomial::COLUMNS,
15        wires::Wire,
16        witness::{self, ConstantCell, CopyBitsCell, VariableBitsCell, Variables, WitnessCell},
17    },
18    variable_map,
19};
20use alloc::{boxed::Box, vec, vec::Vec};
21use ark_ff::PrimeField;
22use core::{array, marker::PhantomData};
23use num_bigint::BigUint;
24use o1_utils::{BigUintFieldHelpers, BigUintHelpers, BitwiseOps, FieldHelpers};
25
26use super::generic::GenericGateSpec;
27
28impl<F: PrimeField> CircuitGate<F> {
29    /// Extends a XOR gadget for `bits` length to a circuit
30    ///
31    /// Includes:
32    /// - num_xors Xor16 gates
33    /// - 1 Generic gate to constrain the final row to be zero with itself
34    ///
35    /// Input:
36    /// - gates     : vector of circuit gates
37    /// - bits      : length of the XOR gadget
38    ///
39    /// Output:
40    /// - new row index
41    pub fn extend_xor_gadget(gates: &mut Vec<Self>, bits: usize) -> usize {
42        let new_row = gates.len();
43        let (_, mut xor_gates) = Self::create_xor_gadget(new_row, bits);
44        // extend the whole circuit with the xor gadget
45        gates.append(&mut xor_gates);
46
47        // check fin_in1, fin_in2, fin_out are zero
48        let zero_row = gates.len() - 1;
49        gates.connect_cell_pair((zero_row, 0), (zero_row, 1));
50        gates.connect_cell_pair((zero_row, 0), (zero_row, 2));
51
52        gates.len()
53    }
54
55    /// Creates a XOR gadget for `bits` length
56    ///
57    /// Includes:
58    /// - num_xors Xor16 gates
59    /// - 1 Generic gate to constrain the final row to be zero with itself
60    ///
61    /// Input:
62    /// - new_row   : row to start the XOR gadget
63    /// - bits      : number of bits in the XOR
64    ///   Outputs tuple (next_row, circuit_gates) where
65    /// - next_row  : next row after this gate
66    /// - gates     : vector of circuit gates comprising this gate
67    ///
68    /// Warning:
69    /// - don't forget to check that the final row is all zeros as in
70    ///   `extend_xor_gadget`
71    pub fn create_xor_gadget(new_row: usize, bits: usize) -> (usize, Vec<Self>) {
72        let num_xors = num_xors(bits);
73        let mut xor_gates = (0..num_xors)
74            .map(|i| CircuitGate {
75                typ: GateType::Xor16,
76                wires: Wire::for_row(new_row + i),
77                coeffs: vec![],
78            })
79            .collect::<Vec<_>>();
80        let zero_row = new_row + num_xors;
81        xor_gates.push(CircuitGate::create_generic_gadget(
82            Wire::for_row(zero_row),
83            GenericGateSpec::Const(F::zero()),
84            None,
85        ));
86
87        (new_row + xor_gates.len(), xor_gates)
88    }
89}
90
91/// Get the xor lookup table
92pub fn lookup_table<F: PrimeField>() -> LookupTable<F> {
93    lookup::tables::get_table::<F>(GateLookupTable::Xor)
94}
95
96//~ `Xor16` - Chainable XOR constraints for words of multiples of 16 bits.
97//~
98//~ * This circuit gate is used to constrain that `in1` xored with `in2` equals `out`
99//~ * The length of `in1`, `in2` and `out` must be the same and a multiple of 16bits.
100//~ * This gate operates on the `Curr` and `Next` rows.
101//~
102//~ It uses three different types of constraints:
103//~
104//~ * copy          - copy to another cell (32-bits)
105//~ * plookup       - xor-table plookup (4-bits)
106//~ * decomposition - the constraints inside the gate
107//~
108//~ The 4-bit nybbles are assumed to be laid out with `0` column being the least significant nybble.
109//~ Given values `in1`, `in2` and `out`, the layout looks like this:
110//~
111//~ | Column |          `Curr`  |          `Next`  |
112//~ | ------ | ---------------- | ---------------- |
113//~ |      0 | copy     `in1`   | copy     `in1'`  |
114//~ |      1 | copy     `in2`   | copy     `in2'`  |
115//~ |      2 | copy     `out`   | copy     `out'`  |
116//~ |      3 | plookup0 `in1_0` |                  |
117//~ |      4 | plookup1 `in1_1` |                  |
118//~ |      5 | plookup2 `in1_2` |                  |
119//~ |      6 | plookup3 `in1_3` |                  |
120//~ |      7 | plookup0 `in2_0` |                  |
121//~ |      8 | plookup1 `in2_1` |                  |
122//~ |      9 | plookup2 `in2_2` |                  |
123//~ |     10 | plookup3 `in2_3` |                  |
124//~ |     11 | plookup0 `out_0` |                  |
125//~ |     12 | plookup1 `out_1` |                  |
126//~ |     13 | plookup2 `out_2` |                  |
127//~ |     14 | plookup3 `out_3` |                  |
128//~
129//~ One single gate with next values of `in1'`, `in2'` and `out'` being zero can be used to check
130//~ that the original `in1`, `in2` and `out` had 16-bits. We can chain this gate 4 times as follows
131//~ to obtain a gadget for 64-bit words XOR:
132//~
133//~ | Row | `CircuitGate` | Purpose                                    |
134//~ | --- | ------------- | ------------------------------------------ |
135//~ |   0 | `Xor16`       | Xor 2 least significant bytes of the words |
136//~ |   1 | `Xor16`       | Xor next 2 bytes of the words              |
137//~ |   2 | `Xor16`       | Xor next 2 bytes of the words              |
138//~ |   3 | `Xor16`       | Xor 2 most significant bytes of the words  |
139//~ |   4 | `Generic`     | Zero values, can be reused as generic gate |
140//~
141//~ ```admonish info
142//~ We could halve the number of rows of the 64-bit XOR gadget by having lookups
143//~ for 8 bits at a time, but for now we will use the 4-bit XOR table that we have.
144//~ Rough computations show that if we run 8 or more Keccaks in one circuit we should
145//~ use the 8-bit XOR table.
146//~ ```
147
148#[derive(Default)]
149pub struct Xor16<F>(PhantomData<F>);
150
151impl<F> Argument<F> for Xor16<F>
152where
153    F: PrimeField,
154{
155    const ARGUMENT_TYPE: ArgumentType = ArgumentType::Gate(GateType::Xor16);
156    const CONSTRAINTS: u32 = 3;
157
158    // Constraints for Xor16
159    //   * Operates on Curr and Next rows
160    //   * Constrain the decomposition of `in1`, `in2` and `out` of multiples of 16 bits
161    //   * The actual XOR is performed thanks to the plookups of 4-bit XORs.
162    fn constraint_checks<T: ExprOps<F, BerkeleyChallengeTerm>>(
163        env: &ArgumentEnv<F, T>,
164        _cache: &mut Cache,
165    ) -> Vec<T> {
166        let two = T::from(2u64);
167        // in1 = in1_0 + in1_1 * 2^4 + in1_2 * 2^8 + in1_3 * 2^12 + next_in1 * 2^16
168        // in2 = in2_0 + in2_1 * 2^4 + in2_2 * 2^8 + in2_3 * 2^12 + next_in2 * 2^16
169        // out = out_0 + out_1 * 2^4 + out_2 * 2^8 + out_3 * 2^12 + next_out * 2^16
170        (0..3)
171            .map(|i| {
172                env.witness_curr(3 + 4 * i)
173                    + env.witness_curr(4 + 4 * i) * two.clone().pow(4)
174                    + env.witness_curr(5 + 4 * i) * two.clone().pow(8)
175                    + env.witness_curr(6 + 4 * i) * two.clone().pow(12)
176                    + two.clone().pow(16) * env.witness_next(i)
177                    - env.witness_curr(i)
178            })
179            .collect::<Vec<T>>()
180    }
181}
182
183// Witness layout
184fn layout<F: PrimeField>(curr_row: usize, bits: usize) -> Vec<Vec<Box<dyn WitnessCell<F>>>> {
185    let num_xor = num_xors(bits);
186    let mut layout = (0..num_xor)
187        .map(|i| xor_row(i, curr_row + i))
188        .collect::<Vec<_>>();
189    layout.push(zero_row());
190    layout
191}
192
193fn xor_row<F: PrimeField>(nybble: usize, curr_row: usize) -> Vec<Box<dyn WitnessCell<F>>> {
194    let start = nybble * 16;
195    vec![
196        VariableBitsCell::create("in1", start, None),
197        VariableBitsCell::create("in2", start, None),
198        VariableBitsCell::create("out", start, None),
199        CopyBitsCell::create(curr_row, 0, 0, 4), // First 4-bit nybble of in1
200        CopyBitsCell::create(curr_row, 0, 4, 8), // Second 4-bit nybble of in1
201        CopyBitsCell::create(curr_row, 0, 8, 12), // Third 4-bit nybble of in1
202        CopyBitsCell::create(curr_row, 0, 12, 16), // Fourth 4-bit nybble of in1
203        CopyBitsCell::create(curr_row, 1, 0, 4), // First 4-bit nybble of in2
204        CopyBitsCell::create(curr_row, 1, 4, 8), // Second 4-bit nybble of in2
205        CopyBitsCell::create(curr_row, 1, 8, 12), // Third 4-bit nybble of in2
206        CopyBitsCell::create(curr_row, 1, 12, 16), // Fourth 4-bit nybble of in2
207        CopyBitsCell::create(curr_row, 2, 0, 4), // First 4-bit nybble of out
208        CopyBitsCell::create(curr_row, 2, 4, 8), // Second 4-bit nybble of out
209        CopyBitsCell::create(curr_row, 2, 8, 12), // Third 4-bit nybble of out
210        CopyBitsCell::create(curr_row, 2, 12, 16), // Fourth 4-bit nybble of out
211    ]
212}
213
214fn zero_row<F: PrimeField>() -> Vec<Box<dyn WitnessCell<F>>> {
215    vec![
216        ConstantCell::create(F::zero()),
217        ConstantCell::create(F::zero()),
218        ConstantCell::create(F::zero()),
219        ConstantCell::create(F::zero()),
220        ConstantCell::create(F::zero()),
221        ConstantCell::create(F::zero()),
222        ConstantCell::create(F::zero()),
223        ConstantCell::create(F::zero()),
224        ConstantCell::create(F::zero()),
225        ConstantCell::create(F::zero()),
226        ConstantCell::create(F::zero()),
227        ConstantCell::create(F::zero()),
228        ConstantCell::create(F::zero()),
229        ConstantCell::create(F::zero()),
230        ConstantCell::create(F::zero()),
231    ]
232}
233
234pub(crate) fn init_xor<F: PrimeField>(
235    witness: &mut [Vec<F>; COLUMNS],
236    curr_row: usize,
237    bits: usize,
238    words: (F, F, F),
239) {
240    let xor_rows = layout(curr_row, bits);
241
242    witness::init(
243        witness,
244        curr_row,
245        &xor_rows,
246        &variable_map!["in1" => words.0, "in2" => words.1, "out" => words.2],
247    )
248}
249
250/// Extends the Xor rows to the full witness
251/// Panics if the words are larger than the desired bits
252pub fn extend_xor_witness<F: PrimeField>(
253    witness: &mut [Vec<F>; COLUMNS],
254    input1: F,
255    input2: F,
256    bits: usize,
257) {
258    let xor_witness = create_xor_witness(input1, input2, bits);
259    for col in 0..COLUMNS {
260        witness[col].extend(xor_witness[col].iter());
261    }
262}
263
264/// Create a Xor for up to the native length starting at row 0
265/// Input: first input and second input, bits length, current row
266/// Panics if the desired bits is smaller than the inputs length
267pub fn create_xor_witness<F: PrimeField>(input1: F, input2: F, bits: usize) -> [Vec<F>; COLUMNS] {
268    let input1_big = input1.to_biguint();
269    let input2_big = input2.to_biguint();
270    if bits < input1_big.bitlen() || bits < input2_big.bitlen() {
271        panic!("Bits must be greater or equal than the inputs length");
272    }
273    let output = BigUint::bitwise_xor(&input1_big, &input2_big);
274
275    let mut xor_witness: [Vec<F>; COLUMNS] =
276        array::from_fn(|_| vec![F::zero(); 1 + num_xors(bits)]);
277
278    init_xor(
279        &mut xor_witness,
280        0,
281        bits,
282        (input1, input2, output.to_field().unwrap()),
283    );
284
285    xor_witness
286}
287
288/// Returns the number of XOR rows needed for inputs of usize bits
289pub fn num_xors(bits: usize) -> usize {
290    bits.div_ceil(16)
291}