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