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

kimchi/circuits/polynomials/
xor.rs
