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}