kimchi/circuits/polynomials/foreign_field_mul/circuitgates.rs
1//! Foreign field multiplication
2
3//~ This gadget is used to constrain that
4//~
5//~```text
6//~ left_input * right_input = quotient * foreign_field_modulus + remainder
7//~```
8//~
9//~ ##### Documentation
10//~
11//~ For more details please see the [Foreign Field Multiplication](../kimchi/foreign_field_mul.md)
12//~ chapter or the original [Foreign Field Multiplication RFC](https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md).
13//~
14//~ ##### Notations
15//~
16//~ For clarity, we use more descriptive variable names in the code than in
17//~ the RFC, which uses mathematical notations.
18//~
19//~ In order to relate the two documents, the following mapping between the
20//~ variable names used in the code and those of the RFC can be helpful.
21//~
22//~ ```text
23//~ left_input0 => a0 right_input0 => b0 quotient0 => q0 remainder01 => r01
24//~ left_input1 => a1 right_input1 => b1 quotient1 => q1
25//~ left_input2 => a2 right_input2 => b2 quotient2 => q2 remainder2 => r2
26//~
27//~ product1_lo => p10 product1_hi_0 => p110 product1_hi_1 => p111
28//~ carry0 => v0 carry1_lo => v10 carry1_hi => v11
29//~ quotient_hi_bound => q'2
30//~
31//~ ````
32//~
33//~ ##### Suffixes
34//~
35//~ The variable names in this code uses descriptive suffixes to convey information about the
36//~ positions of the bits referred to. When a word is split into up to `n` parts
37//~ we use: `0`, `1` ... `n` (where `n` is the most significant). For example, if we split
38//~ word `x` into three limbs, we'd name them `x0`, `x1` and `x2` or `x[0]`, `x[1]` and `x[2]`.
39//~
40//~ Continuing in this fashion, when one of those words is subsequently split in half, then we
41//~ add the suffixes `_lo` and `_hi`, where `hi` corresponds to the most significant bits.
42//~ For our running example, `x1` would become `x1_lo` and `x1_hi`. If we are splitting into
43//~ more than two things, then we pick meaningful names for each.
44//~
45//~ So far we've explained our conventions for a splitting depth of up to 2. For splitting
46//~ deeper than two, we simply cycle back to our depth 1 suffixes again. So for example, `x1_lo`
47//~ would be split into `x1_lo_0` and `x1_lo_1`.
48//~
49//~ ##### Parameters
50//~
51//~ * `hi_foreign_field_modulus` := high limb of foreign field modulus $f$ (stored in gate coefficient 0)
52//~ * `neg_foreign_field_modulus` := negated foreign field modulus $f'$ (stored in gate coefficients 1-3)
53//~ * `n` := the native field modulus is obtainable from `F`, the native field's trait bound
54//~
55//~ ##### Witness
56//~
57//~ * `left_input` := left foreign field element multiplicand $ ~\in F_f$
58//~ * `right_input` := right foreign field element multiplicand $ ~\in F_f$
59//~ * `quotient` := foreign field quotient $ ~\in F_f$
60//~ * `remainder` := foreign field remainder $ ~\in F_f$
61//~ * `carry0` := 2 bit carry
62//~ * `carry1_lo` := low 88 bits of `carry1`
63//~ * `carry1_hi` := high 3 bits of `carry1`
64//~ * `product1_lo` := lowest 88 bits of middle intermediate product
65//~ * `product1_hi_0` := lowest 88 bits of middle intermediate product's highest 88 + 2 bits
66//~ * `product1_hi_1` := highest 2 bits of middle intermediate product
67//~ * `quotient_hi_bound` := quotient high bound for checking `q2 ≤ f2`
68//~
69//~ ##### Layout
70//~
71//~ The foreign field multiplication gate's rows are laid out like this
72//~
73//~ | col | `ForeignFieldMul` | `Zero` |
74//~ | --- | ----------------------- | -------------------------- |
75//~ | 0 | `left_input0` (copy) | `remainder01` (copy) |
76//~ | 1 | `left_input1` (copy) | `remainder2` (copy) |
77//~ | 2 | `left_input2` (copy) | `quotient0` (copy) |
78//~ | 3 | `right_input0` (copy) | `quotient1` (copy) |
79//~ | 4 | `right_input1` (copy) | `quotient2` (copy) |
80//~ | 5 | `right_input2` (copy) | `quotient_hi_bound` (copy) |
81//~ | 6 | `product1_lo` (copy) | `product1_hi_0` (copy) |
82//~ | 7 | `carry1_0` (plookup) | `product1_hi_1` (dummy) |
83//~ | 8 | `carry1_12 (plookup) | `carry1_48` (plookup) |
84//~ | 9 | `carry1_24` (plookup) | `carry1_60` (plookup) |
85//~ | 10 | `carry1_36` (plookup) | `carry1_72` (plookup) |
86//~ | 11 | `carry1_84` | `carry0` |
87//~ | 12 | `carry1_86` | |
88//~ | 13 | `carry1_88` | |
89//~ | 14 | `carry1_90` | |
90//~
91
92use crate::{
93 auto_clone_array,
94 circuits::{
95 argument::{Argument, ArgumentEnv, ArgumentType},
96 berkeley_columns::BerkeleyChallengeTerm,
97 expr::{constraints::ExprOps, Cache},
98 gate::GateType,
99 },
100};
101use ark_ff::PrimeField;
102use core::{array, marker::PhantomData};
103
104/// Compute non-zero intermediate products
105///
106/// For more details see the "Intermediate products" Section of
107/// the [Foreign Field Multiplication RFC](https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md)
108///
109pub fn compute_intermediate_products<F: PrimeField, T: ExprOps<F, BerkeleyChallengeTerm>>(
110 left_input: &[T; 3],
111 right_input: &[T; 3],
112 quotient: &[T; 3],
113 neg_foreign_field_modulus: &[T; 3],
114) -> [T; 3] {
115 auto_clone_array!(left_input);
116 auto_clone_array!(right_input);
117 auto_clone_array!(quotient);
118 auto_clone_array!(neg_foreign_field_modulus);
119
120 [
121 // p0 = a0 * b0 + q0 * f'0
122 left_input(0) * right_input(0) + quotient(0) * neg_foreign_field_modulus(0),
123 // p1 = a0 * b1 + a1 * b0 + q0 * f'1 + q1 * f'0
124 left_input(0) * right_input(1)
125 + left_input(1) * right_input(0)
126 + quotient(0) * neg_foreign_field_modulus(1)
127 + quotient(1) * neg_foreign_field_modulus(0),
128 // p2 = a0 * b2 + a2 * b0 + a1 * b1 + q0 * f'2 + q2 * f'0 + q1 * f'1
129 left_input(0) * right_input(2)
130 + left_input(2) * right_input(0)
131 + left_input(1) * right_input(1)
132 + quotient(0) * neg_foreign_field_modulus(2)
133 + quotient(2) * neg_foreign_field_modulus(0)
134 + quotient(1) * neg_foreign_field_modulus(1),
135 ]
136}
137
138// Compute native modulus values
139pub fn compute_native_modulus_values<F: PrimeField, T: ExprOps<F, BerkeleyChallengeTerm>>(
140 left_input: &[T; 3],
141 right_input: &[T; 3],
142 quotient: &[T; 3],
143 remainder: &[T; 2],
144 neg_foreign_field_modulus: &[T; 3],
145) -> [T; 5] {
146 auto_clone_array!(left_input);
147 auto_clone_array!(right_input);
148 auto_clone_array!(quotient);
149 auto_clone_array!(remainder);
150 auto_clone_array!(neg_foreign_field_modulus);
151
152 [
153 // an = 2^2L * a2 + 2^L * a1 + a0
154 T::two_to_2limb() * left_input(2) + T::two_to_limb() * left_input(1) + left_input(0),
155 // bn = 2^2L * b2 + 2^L * b1 + b0
156 T::two_to_2limb() * right_input(2) + T::two_to_limb() * right_input(1) + right_input(0),
157 // qn = 2^2L * q2 + 2^L * q1 + b0
158 T::two_to_2limb() * quotient(2) + T::two_to_limb() * quotient(1) + quotient(0),
159 // rn = 2^2L * r2 + 2^L * r1 + r0 = 2^2L * r2 + r01
160 T::two_to_2limb() * remainder(1) + remainder(0),
161 // f'n = 2^2L * f'2 + 2^L * f'1 + f'0
162 T::two_to_2limb() * neg_foreign_field_modulus(2)
163 + T::two_to_limb() * neg_foreign_field_modulus(1)
164 + neg_foreign_field_modulus(0),
165 ]
166}
167
168/// Composes the 91-bit carry1 value from its parts
169pub fn compose_carry<F: PrimeField, T: ExprOps<F, BerkeleyChallengeTerm>>(carry: &[T; 11]) -> T {
170 auto_clone_array!(carry);
171 carry(0)
172 + T::two_pow(12) * carry(1)
173 + T::two_pow(2 * 12) * carry(2)
174 + T::two_pow(3 * 12) * carry(3)
175 + T::two_pow(4 * 12) * carry(4)
176 + T::two_pow(5 * 12) * carry(5)
177 + T::two_pow(6 * 12) * carry(6)
178 + T::two_pow(7 * 12) * carry(7)
179 + T::two_pow(86) * carry(8)
180 + T::two_pow(88) * carry(9)
181 + T::two_pow(90) * carry(10)
182}
183
184// ForeignFieldMul - foreign field multiplication gate
185/// * This gate operates on the Curr and Next rows
186/// * It uses copy, plookup, crumb and custom constraints
187#[derive(Default)]
188pub struct ForeignFieldMul<F>(PhantomData<F>);
189
190impl<F> Argument<F> for ForeignFieldMul<F>
191where
192 F: PrimeField,
193{
194 const ARGUMENT_TYPE: ArgumentType = ArgumentType::Gate(GateType::ForeignFieldMul);
195 const CONSTRAINTS: u32 = 11;
196 // DEGREE is 4
197
198 fn constraint_checks<T: ExprOps<F, BerkeleyChallengeTerm>>(
199 env: &ArgumentEnv<F, T>,
200 _cache: &mut Cache,
201 ) -> Vec<T> {
202 let mut constraints = vec![];
203
204 //
205 // Define some helper variables to refer to the witness elements
206 // described in the layout. Note that the limbs below are
207 // defined with least significant bits in lower limbs indexes.
208 //
209
210 // Left multiplicand a
211 let left_input = [
212 // Copied for multi-range-check
213 env.witness_curr(0),
214 env.witness_curr(1),
215 env.witness_curr(2),
216 ];
217
218 // Right multiplicand b
219 let right_input = [
220 // Copied for multi-range-check
221 env.witness_curr(3),
222 env.witness_curr(4),
223 env.witness_curr(5),
224 ];
225
226 // Carry bits v1 decomposed into 7 sublimbs of 12 bits, 3 crumbs of 2 bits, and 1 bit
227 // Total is 91 bits (v11 3 bits + v10 88 bits)
228 let carry1_crumb0 = env.witness_curr(11);
229 let carry1_crumb1 = env.witness_curr(12);
230 let carry1_crumb2 = env.witness_curr(13);
231 let carry1_bit = env.witness_curr(14);
232 let carry1 = compose_carry(&[
233 env.witness_curr(7), // 12-bit lookup
234 env.witness_curr(8), // 12-bit lookup
235 env.witness_curr(9), // 12-bit lookup
236 env.witness_curr(10), // 12-bit lookup
237 env.witness_next(8), // 12-bit lookup
238 env.witness_next(9), // 12-bit lookup
239 env.witness_next(10), // 12-bit lookup
240 carry1_crumb0.clone(), // 2-bit crumb
241 carry1_crumb1.clone(), // 2-bit crumb
242 carry1_crumb2.clone(), // 2-bit crumb
243 carry1_bit.clone(), // 1-bit
244 ]);
245
246 // Carry bits v0
247 let carry0 = env.witness_next(11);
248
249 // Quotient q
250 let quotient = [
251 env.witness_next(2),
252 env.witness_next(3),
253 env.witness_next(4),
254 ];
255
256 // Quotient high bound: q2 + 2^88 - f2
257 // Copied for multi-range-check
258 let quotient_hi_bound = env.witness_next(5);
259
260 // Remainder r (a.k.a. result) in compact format
261 // remainder01 := remainder0 + remainder1 * 2^88
262 // Actual limbs of the result will be obtained from the multi-range-check
263 // Copiable for multi-range-check
264 let remainder = [env.witness_next(0), env.witness_next(1)];
265
266 // Decomposition of the middle intermediate product
267 let product1_lo = env.witness_curr(6); // Copied for multi-range-check
268 let product1_hi_0 = env.witness_next(6); // Copied for multi-range-check
269 let product1_hi_1 = env.witness_next(7); // dummy
270
271 // Foreign field modulus high limb
272 let hi_foreign_field_modulus = env.coeff(0);
273
274 // Negated foreign field modulus limbs
275 let neg_foreign_field_modulus = array::from_fn(|i| env.coeff(1 + i));
276
277 // Compute intermediate products
278 auto_clone_array!(
279 products,
280 compute_intermediate_products(
281 &left_input,
282 &right_input,
283 "ient,
284 &neg_foreign_field_modulus,
285 )
286 );
287
288 // Compute native modulus values
289 let [left_input_n, right_input_n, quotient_n, remainder_n, neg_foreign_field_modulus_n] =
290 compute_native_modulus_values(
291 &left_input,
292 &right_input,
293 "ient,
294 &remainder,
295 &neg_foreign_field_modulus,
296 );
297
298 // bound = x2 + 2^88 - f2 - 1
299 let bound = quotient[2].clone() + T::two_to_limb() - hi_foreign_field_modulus - T::one();
300
301 // Define the constraints
302 // For more the details on each constraint please see the
303 // Foreign Field Multiplication RFC where each of the constraints
304 // numbered below are described in full detail.
305
306 // External checks
307 // multi-range-check: q'2, p10, p110
308 // That is, check bound, product1_lo, product1_hi_0 each in [0, 2^L)
309 // Must be done externally with a multi-range-check gadget
310
311 // C1: Constrain intermediate product fragment product1_hi_1 \in [0, 2^2)
312 // RFC: Corresponds to C3
313 constraints.push(product1_hi_1.crumb());
314
315 // C2: Constrain first carry witness value v0 \in [0, 2^2)
316 // RFC: Corresponds to C5
317 constraints.push(carry0.crumb());
318
319 // C3: Constrain decomposition of middle intermediate product p1
320 // p1 = 2^L*p11 + p10
321 // where p11 = 2^L * p111 + p110
322 // RFC: corresponds to C2
323 let product1_hi = T::two_to_limb() * product1_hi_1 + product1_hi_0;
324 let product1 = T::two_to_limb() * product1_hi.clone() + product1_lo.clone();
325 constraints.push(products(1) - product1);
326
327 // C4: Constrain that 2^2L * v0 = p0 + 2^L * p10 - r01. That is, that
328 // 2^2L * carry0 = rhs
329 // RFC: Corresponds to C4
330 constraints.push(
331 T::two_to_2limb() * carry0.clone()
332 - (products(0) + T::two_to_limb() * product1_lo - remainder[0].clone()),
333 );
334
335 // C5: Native modulus constraint a_n * b_n + q_n * f'_n - q_n * 2^264 = r_n
336 // RFC: Corresponds to C1
337 constraints.push(
338 left_input_n * right_input_n + quotient_n.clone() * neg_foreign_field_modulus_n
339 - remainder_n
340 - quotient_n * T::two_to_3limb(),
341 );
342
343 // Constrain v1 is 91-bits (done with 7 plookups, 3 crumbs, and 1 bit)
344 // C6: 2-bit c1_84
345 // RFC: Corresponds to C7
346 constraints.push(carry1_crumb0.crumb());
347 // C7: 2-bit c1_86
348 // RFC: Corresponds to C8
349 constraints.push(carry1_crumb1.crumb());
350 // C8: 2-bit c1_88
351 // RFC: Corresponds to C9
352 constraints.push(carry1_crumb2.crumb());
353 // C9: 1-bit c1_90
354 // RFC: Corresponds to C10
355 constraints.push(carry1_bit.boolean());
356
357 // C10: Top part:
358 // Constrain that 2^L * v1 = p2 + p11 + v0 - r2. That is,
359 // 2^L * (2^L * carry1_hi + carry1_lo) = rhs
360 // RFC: Corresponds to C6
361 constraints.push(
362 T::two_to_limb() * carry1 - (products(2) + product1_hi + carry0 - remainder[1].clone()),
363 );
364
365 // C11: Constrain that q'2 is correct
366 // RFC: Corresponds to C11
367 constraints.push(quotient_hi_bound - bound);
368
369 constraints
370 }
371}