kimchi/circuits/polynomials/range_check/
circuitgates.rs

1//~ The multi range check gadget is comprised of three circuit gates (`RangeCheck0`,
2//~ `RangeCheck1` and `Zero`) and can perform range checks on three values ($v_0,
3//~ v_1$ and $v_2$) of up to 88 bits each.
4//~
5//~ Values can be copied as inputs to the multi range check gadget in two ways:
6//~
7//~ * (Standard mode) With 3 copies, by copying $v_0, v_1$ and $v_2$ to the first
8//~     cells of the first 3 rows of the gadget.  In this mode the first gate
9//~     coefficient is set to `0`.
10//~ * (Compact mode) With 2 copies, by copying $v_2$ to the first cell of the first
11//~     row and copying $v_{10} = v_0 + 2^{\ell} \cdot v_1$ to the 2nd cell of row 2.
12//~     In this mode the first gate coefficient is set to `1`.
13//~
14//~ The `RangeCheck0` gate can also be used on its own to perform 64-bit range checks by
15//~ constraining witness cells 1-2 to zero.
16//~
17//~ **Byte-order:**
18//~
19//~ * Each cell value is in little-endian byte order
20//~ * Limbs are mapped to columns in big-endian order (i.e. the lowest columns
21//~   contain the highest bits)
22//~ * We also have the highest bits covered by copy constraints and plookups, so that
23//~   we can copy the highest two constraints to zero and get a 64-bit lookup, which
24//~   are envisioned to be a common case
25//~
26//~ The values are decomposed into limbs as follows:
27//~
28//~ * `L` is a 12-bit lookup (or copy) limb,
29//~ * `C` is a 2-bit "crumb" limb (we call half a nybble a crumb).
30//~
31//~ ```text
32//~         <----6----> <------8------>
33//~    v0 = L L L L L L C C C C C C C C
34//~    v1 = L L L L L L C C C C C C C C
35//~         <2> <--4--> <---------------18---------------->
36//~    v2 = C C L L L L C C C C C C C C C C C C C C C C C C
37//~ ```
38//~
39//~ **Witness structure:**
40//~
41//~ | Row | Contents        |
42//~ | --- | --------------- |
43//~ |  0  | $v_0$           |
44//~ |  1  | $v_1$           |
45//~ |  2  | $v_2$           |
46//~ |  3  | $v_0, v_1, v_2$ |
47//~
48//~ * The first 2 rows contain $v_0$ and $v_1$ and their respective decompositions
49//~   into 12-bit and 2-bit limbs
50//~ * The 3rd row contains $v_2$ and part of its decomposition: four 12-bit limbs and
51//~   the 1st 10 crumbs
52//~ * The final row contains $v_0$'s and $v_1$'s 5th and 6th 12-bit limbs as well as the
53//~   remaining 10 crumbs of $v_2$
54//~
55//~ ```admonish
56//~ Because we are constrained to 4 lookups per row, we are forced to postpone
57//~ some lookups of v0 and v1 to the final row.
58//~ ```
59//~
60//~ **Constraints:**
61//~
62//~ For efficiency, the limbs are constrained differently according to their type:
63//~
64//~ * 12-bit limbs are constrained with plookups
65//~ * 2-bit crumbs are constrained with degree-4 constraints $x(x-1)(x-2)(x-3)$
66//~
67//~ **Layout:**
68//~
69//~ This is how the three 88-bit inputs $v_0, v_1$ and $v_2$ are laid out and constrained.
70//~
71//~ * `vipj` is the jth 12-bit limb of value $v_i$
72//~ * `vicj` is the jth 2-bit crumb limb of value $v_i$
73//~
74//~ | Gates | `RangeCheck0`  | `RangeCheck0`  | `RangeCheck1`   | `Zero`          |
75//~ | ----- | -------------- | -------------- | --------------- | --------------- |
76//~ | Rows  |          0     |          1     |          2      |          3      |
77//~ | Cols  |                |                |                 |                 |
78//~ |     0 |         `v0`   |         `v1`   |          `v2`   | crumb   `v2c9`  |
79//~ |  MS:1 | copy    `v0p0` | copy    `v1p0` | optional `v12`  | crumb   `v2c10` |
80//~ |     2 | copy    `v0p1` | copy    `v1p1` | crumb    `v2c0` | crumb   `v2c11` |
81//~ |     3 | plookup `v0p2` | plookup `v1p2` | plookup  `v2p0` | plookup `v0p0`  |
82//~ |     4 | plookup `v0p3` | plookup `v1p3` | plookup  `v2p1` | plookup `v0p1`  |
83//~ |     5 | plookup `v0p4` | plookup `v1p4` | plookup  `v2p2` | plookup `v1p0`  |
84//~ |     6 | plookup `v0p5` | plookup `v1p5` | plookup  `v2p3` | plookup `v1p1`  |
85//~ |     7 | crumb   `v0c0` | crumb   `v1c0` | crumb    `v2c1` | crumb   `v2c12` |
86//~ |     8 | crumb   `v0c1` | crumb   `v1c1` | crumb    `v2c2` | crumb   `v2c13` |
87//~ |     9 | crumb   `v0c2` | crumb   `v1c2` | crumb    `v2c3` | crumb   `v2c14` |
88//~ |    10 | crumb   `v0c3` | crumb   `v1c3` | crumb    `v2c4` | crumb   `v2c15` |
89//~ |    11 | crumb   `v0c4` | crumb   `v1c4` | crumb    `v2c5` | crumb   `v2c16` |
90//~ |    12 | crumb   `v0c5` | crumb   `v1c5` | crumb    `v2c6` | crumb   `v2c17` |
91//~ |    13 | crumb   `v0c6` | crumb   `v1c6` | crumb    `v2c7` | crumb   `v2c18` |
92//~ | LS:14 | crumb   `v0c7` | crumb   `v1c7` | crumb    `v2c8` | crumb   `v2c19` |
93//~
94//~ The 12-bit chunks are constrained with plookups and the 2-bit crumbs are
95//~ constrained with degree-4 constraints of the form $x (x - 1) (x - 2) (x - 3)$.
96//~
97//~ Note that copy denotes a plookup that is deferred to the 4th gate (i.e. `Zero`).
98//~ This is because of the limitation that we have at most 4 lookups per row.
99//~ The copies are constrained using the permutation argument.
100//~
101//~ **Gate types:**
102//~
103//~ Different rows are constrained using different `CircuitGate` types
104//~
105//~ | Row | `CircuitGate` | Purpose                                                            |
106//~ | --- | ------------- | ------------------------------------------------------------------ |
107//~ |   0 | `RangeCheck0` | Partially constrain $v_0$                                          |
108//~ |   1 | `RangeCheck0` | Partially constrain $v_1$                                          |
109//~ |   2 | `RangeCheck1` | Fully constrain $v_2$ (and trigger plookups constraints on row 3)  |
110//~ |   3 | `Zero`        | Complete the constraining of $v_0$ and $v_1$ using lookups         |
111//~
112//~ ```admonish
113//~  Each CircuitGate type corresponds to a unique polynomial and thus is assigned
114//~  its own unique powers of alpha
115//~ ```
116
117use core::marker::PhantomData;
118
119use crate::circuits::{
120    argument::{Argument, ArgumentEnv, ArgumentType},
121    berkeley_columns::BerkeleyChallengeTerm,
122    expr::{
123        constraints::{crumb, ExprOps},
124        Cache,
125    },
126    gate::GateType,
127    polynomial::COLUMNS,
128};
129use ark_ff::PrimeField;
130
131//~
132//~ **`RangeCheck0` - Range check constraints**
133//~
134//~ * This circuit gate is used to partially constrain values $v_0$ and $v_1$
135//~ * Optionally, it can be used on its own as a single 64-bit range check by
136//~   constraining columns 1 and 2 to zero
137//~ * The rest of $v_0$ and $v_1$ are constrained by the lookups in the `Zero` gate row
138//~ * This gate operates on the `Curr` row
139//~
140//~ It uses three different types of constraints:
141//~
142//~ * copy    - copy to another cell (12-bits)
143//~ * plookup - plookup (12-bits)
144//~ * crumb   - degree-4 constraint (2-bits)
145//~
146//~ Given value `v` the layout looks like this
147//~
148//~ | Column | `Curr`        |
149//~ | ------ | ------------- |
150//~ |      0 |         `v`   |
151//~ |      1 | copy    `vp0` |
152//~ |      2 | copy    `vp1` |
153//~ |      3 | plookup `vp2` |
154//~ |      4 | plookup `vp3` |
155//~ |      5 | plookup `vp4` |
156//~ |      6 | plookup `vp5` |
157//~ |      7 | crumb   `vc0` |
158//~ |      8 | crumb   `vc1` |
159//~ |      9 | crumb   `vc2` |
160//~ |     10 | crumb   `vc3` |
161//~ |     11 | crumb   `vc4` |
162//~ |     12 | crumb   `vc5` |
163//~ |     13 | crumb   `vc6` |
164//~ |     14 | crumb   `vc7` |
165//~
166//~ where the notation `vpi` and `vci` defined in the "Layout" section above.
167
168#[derive(Default)]
169pub struct RangeCheck0<F>(PhantomData<F>);
170
171impl<F> Argument<F> for RangeCheck0<F>
172where
173    F: PrimeField,
174{
175    const ARGUMENT_TYPE: ArgumentType = ArgumentType::Gate(GateType::RangeCheck0);
176    const CONSTRAINTS: u32 = 10;
177
178    // Constraints for RangeCheck0
179    //   * Operates on Curr row
180    //   * Range constrain all limbs except vp0 and vp1 (barring plookup constraints, which are done elsewhere)
181    //   * Constrain that combining all limbs equals the limb stored in column 0
182    fn constraint_checks<T: ExprOps<F, BerkeleyChallengeTerm>>(
183        env: &ArgumentEnv<F, T>,
184        _cache: &mut Cache,
185    ) -> Vec<T> {
186        // 1) Apply range constraints on the limbs
187        //    * Columns 1-2 are 12-bit copy constraints
188        //        * They are copied 3 rows ahead (to the final row) and are constrained by lookups
189        //          triggered by RangeCheck1 on the Next row
190        //        * Optionally, they can be constrained to zero to convert the RangeCheck0 gate into
191        //          a single 64-bit range check
192        //    * Columns 3-6 are 12-bit plookup range constraints (these are specified in the lookup gate)
193        //    * Columns 7-14 are 2-bit crumb range constraints
194        let mut constraints = (7..COLUMNS)
195            .map(|i| crumb(&env.witness_curr(i)))
196            .collect::<Vec<T>>();
197
198        // 2) Constrain that the combined limbs equals the value v stored in w(0):
199        //
200        //        w(0) = v = vp0 vp1 vp2 vp3 vp4 vp5 vc0 vc1 vc2 vc3 vc4 vc5 vc6 vc7
201        //
202        //    where the value and limbs are stored in little-endian byte order, but mapped
203        //    to cells in big-endian order.
204        //
205        //    Cols: 0  1   2   3   4   5   6   7   8   9   10  11  12  13  14
206        //    Curr: v  vp0 vp1 vp2 vp3 vp4 vp5 vc0 vc1 vc2 vc3 vc4 vc5 vc6 vc7  <- LSB
207
208        let mut power_of_2 = T::one();
209        let mut sum_of_limbs = T::zero();
210
211        // Sum 2-bit limbs
212        for i in (7..COLUMNS).rev() {
213            sum_of_limbs += power_of_2.clone() * env.witness_curr(i);
214            power_of_2 *= T::from(4u64); // 2 bits
215        }
216
217        // Sum 12-bit limbs
218        for i in (1..=6).rev() {
219            sum_of_limbs += power_of_2.clone() * env.witness_curr(i);
220            power_of_2 *= 4096u64.into(); // 12 bits
221        }
222
223        // Check value v against the sum of limbs
224        constraints.push(sum_of_limbs - env.witness_curr(0));
225
226        // Optional compact limbs format (enabled when coeff[0] == 1, disabled when coeff[1] = 0)
227        //   Constrain decomposition of compact limb next(1)
228        //   next(1) = curr(0) + 2^L * next(0)
229        constraints.push(
230            env.coeff(0)
231                * (env.witness_next(1)
232                    - (env.witness_curr(0) + T::two_to_limb() * env.witness_next(0))),
233        );
234
235        constraints
236    }
237}
238
239//~
240//~ **`RangeCheck1` - Range check constraints**
241//~
242//~ * This circuit gate is used to fully constrain $v_2$
243//~ * It operates on the `Curr` and `Next` rows
244//~
245//~ It uses two different types of constraints:
246//~
247//~ * plookup - plookup (12-bits)
248//~ * crumb   - degree-4 constraint (2-bits)
249//~
250//~ Given value `v2` the layout looks like this
251//~
252//~ | Column | `Curr`          | `Next`        |
253//~ | ------ | --------------- | ------------- |
254//~ |      0 |          `v2`   | crumb `v2c9`  |
255//~ |      1 | optional `v12`  | crumb `v2c10` |
256//~ |      2 | crumb    `v2c0` | crumb `v2c11` |
257//~ |      3 | plookup  `v2p0` | (ignored)     |
258//~ |      4 | plookup  `v2p1` | (ignored)     |
259//~ |      5 | plookup  `v2p2` | (ignored)     |
260//~ |      6 | plookup  `v2p3` | (ignored)     |
261//~ |      7 | crumb    `v2c1` | crumb `v2c12` |
262//~ |      8 | crumb    `v2c2` | crumb `v2c13` |
263//~ |      9 | crumb    `v2c3` | crumb `v2c14` |
264//~ |     10 | crumb    `v2c4` | crumb `v2c15` |
265//~ |     11 | crumb    `v2c5` | crumb `v2c16` |
266//~ |     12 | crumb    `v2c6` | crumb `v2c17` |
267//~ |     13 | crumb    `v2c7` | crumb `v2c18` |
268//~ |     14 | crumb    `v2c8` | crumb `v2c19` |
269//~
270//~ where the notation `v2ci` and `v2pi` defined in the "Layout" section above.
271
272#[derive(Default)]
273pub struct RangeCheck1<F>(PhantomData<F>);
274
275impl<F> Argument<F> for RangeCheck1<F>
276where
277    F: PrimeField,
278{
279    const ARGUMENT_TYPE: ArgumentType = ArgumentType::Gate(GateType::RangeCheck1);
280    const CONSTRAINTS: u32 = 21;
281
282    // Constraints for RangeCheck1
283    //   * Operates on Curr and Next row
284    //   * Range constrain all limbs (barring plookup constraints, which are done elsewhere)
285    //   * Constrain that combining all limbs equals the value v2 stored in row Curr, column 0
286    fn constraint_checks<T: ExprOps<F, BerkeleyChallengeTerm>>(
287        env: &ArgumentEnv<F, T>,
288        _cache: &mut Cache,
289    ) -> Vec<T> {
290        // 1) Apply range constraints on limbs for Curr row
291        //    * Column 2 is a 2-bit crumb
292        let mut constraints = vec![crumb(&env.witness_curr(2))];
293
294        //    * Columns 3-6 are 12-bit plookup range constraints (these are specified
295        //      in the lookup gate)
296        //    * Columns 7-14 are 2-bit crumb range constraints
297        constraints.append(
298            &mut (7..COLUMNS)
299                .map(|i| crumb(&env.witness_curr(i)))
300                .collect::<Vec<T>>(),
301        );
302
303        // 2) Apply range constraints on limbs for Next row
304        //    * Columns 0-2 are 2-bit crumbs
305        constraints.append(
306            &mut (0..=2)
307                .map(|i| crumb(&env.witness_next(i)))
308                .collect::<Vec<T>>(),
309        );
310        //    * Columns 3-6 are 12-bit plookup range constraints for v0 and v1 (these
311        //      are specified in the lookup gate)
312        //    * Columns 7-14 are more 2-bit crumbs
313        constraints.append(
314            &mut (7..COLUMNS)
315                .map(|i| crumb(&env.witness_next(i)))
316                .collect::<Vec<T>>(),
317        );
318
319        // 2) Constrain that the combined limbs equals the value v2 stored in w(0) where
320        //
321        //    w(0) = v2 = vc0 vc1 vp0 vp1 vp2 vp3 vc2 vc3 vc4 vc5 vc6 vc7 vc8 vc9 vc10 vc11 vc12
322        //                vc13 vc14 vc15 vc16 vc17 vc18 vc19
323        //
324        //    where the value and limbs are stored in little-endian byte order, but mapped
325        //    to cells in big-endian order.
326        //
327        //          0  1   2   3   4   5    6    7    8    9    10   11   12   13   14
328        //    Curr  v2 vc0 vc1 vp0 vp1 vp2  vp3  vc2  vc3  vc4  vc5  vc6  vc7  vc8  vc9
329        //    Next                     vc10 vc11 vc12 vc13 vc14 vc15 vc16 vc17 vc18 vc19 <- LSB
330
331        let mut power_of_2 = T::one();
332        let mut sum_of_limbs = T::zero();
333
334        // Next row: Sum 2-bit limbs
335        for i in (7..COLUMNS).rev() {
336            sum_of_limbs += power_of_2.clone() * env.witness_next(i);
337            power_of_2 *= 4u64.into(); // 2 bits
338        }
339
340        // Next row:  Sum remaining 2-bit limbs v2c9, v2c10, and v2c11 (reverse order)
341        for i in (0..=2).rev() {
342            sum_of_limbs += power_of_2.clone() * env.witness_next(i);
343            power_of_2 *= 4u64.into(); // 2 bits
344        }
345
346        // Curr row:  Sum 2-bit limbs
347        for i in (7..COLUMNS).rev() {
348            sum_of_limbs += power_of_2.clone() * env.witness_curr(i);
349            power_of_2 *= 4u64.into(); // 2 bits
350        }
351
352        // Curr row: Sum 12-bit limbs
353        for i in (3..=6).rev() {
354            sum_of_limbs += power_of_2.clone() * env.witness_curr(i);
355            power_of_2 *= 4096u64.into(); // 12 bits
356        }
357
358        // Curr row:  Add remaining 2-bit limb v2c0 to sum
359        sum_of_limbs += power_of_2.clone() * env.witness_curr(2);
360
361        // Check value v2 against the sum of limbs
362        constraints.push(sum_of_limbs - env.witness_curr(0));
363
364        constraints
365    }
366}