ark-r1cs-std/r1cs-std/src/fields/fp12.rs
r1cs-std/src/fields/fp12.rsRaw
1use r1cs_core::{ConstraintSystem, SynthesisError};
2
3use algebra::{
4 PrimeField, Field,
5 fields::{
6 fp12_2over3over2::{Fp12, Fp12Parameters},
7 fp6_3over2::{Fp6, Fp6Parameters},
8 Fp2Parameters,
9 },
10 BitIterator,
11};
12use std::{borrow::Borrow, marker::PhantomData};
13
14use crate::prelude::*;
15use crate::Assignment;
16
17type Fp2Gadget<P, ConstraintF> =
18 super::fp2::Fp2Gadget<<<P as Fp12Parameters>::Fp6Params as Fp6Parameters>::Fp2Params, ConstraintF>;
19type Fp6Gadget<P, ConstraintF> = super::fp6_3over2::Fp6Gadget<<P as Fp12Parameters>::Fp6Params, ConstraintF>;
20type Fp6GadgetVariable<P, ConstraintF> =
21 <Fp6Gadget<P, ConstraintF> as FieldGadget<Fp6<<P as Fp12Parameters>::Fp6Params>, ConstraintF>>::Variable;
22
23#[derive(Derivative)]
24#[derivative(Debug(bound = "ConstraintF: PrimeField"))]
25#[must_use]
26pub struct Fp12Gadget<P, ConstraintF: PrimeField>
27where
28 P: Fp12Parameters,
29 <P::Fp6Params as Fp6Parameters>::Fp2Params: Fp2Parameters<Fp = ConstraintF>,
30{
31 pub c0: Fp6Gadget<P, ConstraintF>,
32 pub c1: Fp6Gadget<P, ConstraintF>,
33 #[derivative(Debug = "ignore")]
34 _params: PhantomData<P>,
35}
36
37impl<P, ConstraintF: PrimeField> Fp12Gadget<P, ConstraintF>
38where
39 P: Fp12Parameters,
40 <P::Fp6Params as Fp6Parameters>::Fp2Params: Fp2Parameters<Fp = ConstraintF>,
41{
42 #[inline]
43 pub fn new(c0: Fp6Gadget<P, ConstraintF>, c1: Fp6Gadget<P, ConstraintF>) -> Self {
44 Self {
45 c0,
46 c1,
47 _params: PhantomData,
48 }
49 }
50
51 /// Multiply by quadratic nonresidue v.
52 #[inline]
53 pub(crate) fn mul_fp6_by_nonresidue<CS: ConstraintSystem<ConstraintF>>(
54 cs: CS,
55 fe: &Fp6Gadget<P, ConstraintF>,
56 ) -> Result<Fp6Gadget<P, ConstraintF>, SynthesisError> {
57 let new_c0 = Fp6Gadget::<P, ConstraintF>::mul_fp2_gadget_by_nonresidue(cs, &fe.c2)?;
58 let new_c1 = fe.c0.clone();
59 let new_c2 = fe.c1.clone();
60 Ok(Fp6Gadget::<P, ConstraintF>::new(new_c0, new_c1, new_c2))
61 }
62
63 #[inline]
64 pub fn conjugate_in_place<CS: ConstraintSystem<ConstraintF>>(
65 &mut self,
66 cs: CS,
67 ) -> Result<&mut Self, SynthesisError> {
68 self.c1.negate_in_place(cs)?;
69 Ok(self)
70 }
71
72 /// Multiplies by an element of the form (c0 = (c0, c1, 0), c1 = (0, d1, 0))
73 #[inline]
74 pub fn mul_by_014<CS: ConstraintSystem<ConstraintF>>(
75 &self,
76 mut cs: CS,
77 c0: &Fp2Gadget<P, ConstraintF>,
78 c1: &Fp2Gadget<P, ConstraintF>,
79 d1: &Fp2Gadget<P, ConstraintF>,
80 ) -> Result<Self, SynthesisError> {
81 let v0 = self.c0.mul_by_c0_c1_0(cs.ns(|| "v0"), &c0, &c1)?;
82 let v1 = self.c1.mul_by_0_c1_0(cs.ns(|| "v1"), &d1)?;
83 let new_c0 = Self::mul_fp6_by_nonresidue(cs.ns(|| "first mul_by_nr"), &v1)?
84 .add(cs.ns(|| "v0 + nonresidue * v1"), &v0)?;
85
86 let c1 = {
87 let tmp = c1.add(cs.ns(|| "c1 + d1"), &d1)?;
88 let a0_plus_a1 = self.c0.add(cs.ns(|| "a0 + a1"), &self.c1)?;
89 a0_plus_a1
90 .mul_by_c0_c1_0(cs.ns(|| "(a0 + a1) * (b0 + b1)"), &c0, &tmp)?
91 .sub(cs.ns(|| "sub v0"), &v0)?
92 .sub(cs.ns(|| "sub v1"), &v1)?
93 };
94 Ok(Self::new(new_c0, c1))
95 }
96
97 /// Multiplies by an element of the form (c0 = (c0, 0, 0), c1 = (d0, d1, 0))
98 #[inline]
99 pub fn mul_by_034<CS: ConstraintSystem<ConstraintF>>(
100 &self,
101 mut cs: CS,
102 c0: &Fp2Gadget<P, ConstraintF>,
103 d0: &Fp2Gadget<P, ConstraintF>,
104 d1: &Fp2Gadget<P, ConstraintF>,
105 ) -> Result<Self, SynthesisError> {
106 let a0 = self.c0.c0.mul(cs.ns(|| "a0"), &c0)?;
107 let a1 = self.c0.c1.mul(cs.ns(|| "a1"), &c0)?;
108 let a2 = self.c0.c2.mul(cs.ns(|| "a2"), &c0)?;
109 let a = Fp6Gadget::<P, ConstraintF>::new(a0, a1, a2);
110 let b = self.c1.mul_by_c0_c1_0(cs.ns(|| "b"), &d0, &d1)?;
111
112 let c0 = c0.add(cs.ns(|| "c0 + d0"), &d0)?;
113 let c1 = d1;
114 let e = self
115 .c0
116 .add(cs.ns(|| "self.c0 + self.c1"), &self.c1)?
117 .mul_by_c0_c1_0(cs.ns(|| "compute e"), &c0, &c1)?;
118 let a_plus_b = a.add(cs.ns(|| "a + b"), &b)?;
119 let c1 = e.sub(cs.ns(|| "e - (a + b)"), &a_plus_b)?;
120 let c0 = Self::mul_fp6_by_nonresidue(cs.ns(|| "b *nr"), &b)?.add(cs.ns(|| "plus a"), &a)?;
121
122 Ok(Self::new(c0, c1))
123 }
124
125 pub fn cyclotomic_square<CS: ConstraintSystem<ConstraintF>>(
126 &self,
127 mut cs: CS,
128 ) -> Result<Self, SynthesisError> {
129 let mut result = Self::zero(cs.ns(|| "alloc result"))?;
130 let fp2_nr = <P::Fp6Params as Fp6Parameters>::NONRESIDUE;
131
132 let z0 = &self.c0.c0;
133 let z4 = &self.c0.c1;
134 let z3 = &self.c0.c2;
135 let z2 = &self.c1.c0;
136 let z1 = &self.c1.c1;
137 let z5 = &self.c1.c2;
138
139 // t0 + t1*y = (z0 + z1*y)^2 = a^2
140 let tmp = z0.mul(cs.ns(|| "first mul"), &z1)?;
141 let t0 = {
142 // (z0 + &z1) * &(z0 + &(fp2_nr * &z1)) - &tmp - &(tmp * &fp2_nr);
143 let mut cs = cs.ns(|| "t0");
144 let tmp1 = z0.add(cs.ns(|| "tmp1"), &z1)?;
145 let tmp2 = z1
146 .mul_by_constant(cs.ns(|| "tmp2.1"), &fp2_nr)?
147 .add(cs.ns(|| "tmp2.2"), &z0)?;
148 let tmp4 = tmp
149 .mul_by_constant(cs.ns(|| "tmp4.1"), &fp2_nr)?
150 .add(cs.ns(|| "tmp4.2"), &tmp)?;
151 tmp1.mul(cs.ns(|| "tmp3.1"), &tmp2)?
152 .sub(cs.ns(|| "tmp3.2"), &tmp4)?
153 };
154 let t1 = tmp.double(cs.ns(|| "t1"))?;
155
156 // t2 + t3*y = (z2 + z3*y)^2 = b^2
157 let tmp = z2.mul(cs.ns(|| "second mul"), &z3)?;
158 let t2 = {
159 // (z2 + &z3) * &(z2 + &(fp2_nr * &z3)) - &tmp - &(tmp * &fp2_nr);
160 let mut cs = cs.ns(|| "t2");
161 let tmp1 = z2.add(cs.ns(|| "tmp1"), &z3)?;
162 let tmp2 = z3
163 .mul_by_constant(cs.ns(|| "tmp2.1"), &fp2_nr)?
164 .add(cs.ns(|| "tmp2.2"), &z2)?;
165 let tmp4 = tmp
166 .mul_by_constant(cs.ns(|| "tmp4.1"), &fp2_nr)?
167 .add(cs.ns(|| "tmp4.2"), &tmp)?;
168 tmp1.mul(cs.ns(|| "tmp3.1"), &tmp2)?
169 .sub(cs.ns(|| "tmp3.2"), &tmp4)?
170 };
171 let t3 = tmp.double(cs.ns(|| "t3"))?;
172
173 // t4 + t5*y = (z4 + z5*y)^2 = c^2
174 let tmp = z4.mul(cs.ns(|| "third mul"), &z5)?;
175 let t4 = {
176 // (z4 + &z5) * &(z4 + &(fp2_nr * &z5)) - &tmp - &(tmp * &fp2_nr);
177 let mut cs = cs.ns(|| "t4");
178 let tmp1 = z4.add(cs.ns(|| "tmp1"), &z5)?;
179 let tmp2 = z5
180 .mul_by_constant(cs.ns(|| "tmp2.1"), &fp2_nr)?
181 .add(cs.ns(|| "tmp2.2"), &z4)?;
182 let tmp4 = tmp
183 .mul_by_constant(cs.ns(|| "tmp4.1"), &fp2_nr)?
184 .add(cs.ns(|| "tmp4.2"), &tmp)?;
185 tmp1.mul(cs.ns(|| "tmp3.1"), &tmp2)?
186 .sub(cs.ns(|| "tmp3.2"), &tmp4)?
187 };
188 let t5 = tmp.double(cs.ns(|| "t5"))?;
189
190 // for A
191
192 // z0 = 3 * t0 - 2 * z0
193 result.c0.c0 = {
194 let mut cs = cs.ns(|| "result.c0.c0");
195 t0.sub(cs.ns(|| "1"), &z0)?
196 .double(cs.ns(|| "2"))?
197 .add(cs.ns(|| "3"), &t0)?
198 };
199
200 // z1 = 3 * t1 + 2 * z1
201 result.c1.c1 = {
202 let mut cs = cs.ns(|| "result.c1.c1");
203 t1.add(cs.ns(|| "1"), &z1)?
204 .double(cs.ns(|| "2"))?
205 .add(cs.ns(|| "3"), &t1)?
206 };
207
208 // for B
209
210 // z2 = 3 * (xi * t5) + 2 * z2
211 result.c1.c0 = {
212 let mut cs = cs.ns(|| "result.c1.c0");
213 let tmp = t5.mul_by_constant(cs.ns(|| "1"), &fp2_nr)?;
214 z2.add(cs.ns(|| "2"), &tmp)?
215 .double(cs.ns(|| "3"))?
216 .add(cs.ns(|| "4"), &tmp)?
217 };
218
219 // z3 = 3 * t4 - 2 * z3
220 result.c0.c2 = {
221 let mut cs = cs.ns(|| "result.c0.c2");
222 t4.sub(cs.ns(|| "1"), &z3)?
223 .double(cs.ns(|| "2"))?
224 .add(cs.ns(|| "3"), &t4)?
225 };
226
227 // for C
228
229 // z4 = 3 * t2 - 2 * z4
230 result.c0.c1 = {
231 let mut cs = cs.ns(|| "result.c0.c1");
232 t2.sub(cs.ns(|| "1"), &z4)?
233 .double(cs.ns(|| "2"))?
234 .add(cs.ns(|| "3"), &t2)?
235 };
236
237 // z5 = 3 * t3 + 2 * z5
238 result.c1.c2 = {
239 let mut cs = cs.ns(|| "result.c1.c2");
240 t3.add(cs.ns(|| "1"), &z5)?
241 .double(cs.ns(|| "2"))?
242 .add(cs.ns(|| "3"), &t3)?
243 };
244
245 Ok(result)
246 }
247
248 #[inline]
249 pub fn cyclotomic_exp<CS: ConstraintSystem<ConstraintF>, S: AsRef<[u64]>>(
250 &self,
251 mut cs: CS,
252 exp: S,
253 ) -> Result<Self, SynthesisError> {
254 let mut res = Self::one(cs.ns(|| "one"))?;
255 let mut found_one = false;
256 for (j, i) in BitIterator::new(exp).enumerate() {
257 if found_one {
258 res = res.cyclotomic_square(cs.ns(|| format!("res_square_{:?}", j)))?;
259 } else {
260 found_one = i;
261 }
262 if i {
263 res.mul_in_place(cs.ns(|| format!("res_mul2_{:?}", j)), self)?;
264 }
265 }
266 Ok(res)
267 }
268}
269
270impl<P, ConstraintF: PrimeField> FieldGadget<Fp12<P>, ConstraintF> for Fp12Gadget<P, ConstraintF>
271where
272 P: Fp12Parameters,
273 <P::Fp6Params as Fp6Parameters>::Fp2Params: Fp2Parameters<Fp = ConstraintF>,
274{
275 type Variable = (Fp6GadgetVariable<P, ConstraintF>, Fp6GadgetVariable<P, ConstraintF>);
276
277 #[inline]
278 fn get_value(&self) -> Option<Fp12<P>> {
279 Some(Fp12::new(self.c0.get_value()?, self.c1.get_value()?))
280 }
281
282 #[inline]
283 fn get_variable(&self) -> Self::Variable {
284 (self.c0.get_variable(), self.c1.get_variable())
285 }
286
287 #[inline]
288 fn zero<CS: ConstraintSystem<ConstraintF>>(mut cs: CS) -> Result<Self, SynthesisError> {
289 let c0 = Fp6Gadget::<P, ConstraintF>::zero(cs.ns(|| "c0"))?;
290 let c1 = Fp6Gadget::<P, ConstraintF>::zero(cs.ns(|| "c1"))?;
291 Ok(Self::new(c0, c1))
292 }
293
294 #[inline]
295 fn one<CS: ConstraintSystem<ConstraintF>>(mut cs: CS) -> Result<Self, SynthesisError> {
296 let c0 = Fp6Gadget::<P, ConstraintF>::one(cs.ns(|| "c0"))?;
297 let c1 = Fp6Gadget::<P, ConstraintF>::zero(cs.ns(|| "c1"))?;
298 Ok(Self::new(c0, c1))
299 }
300
301 #[inline]
302 fn add<CS: ConstraintSystem<ConstraintF>>(
303 &self,
304 mut cs: CS,
305 other: &Self,
306 ) -> Result<Self, SynthesisError> {
307 let c0 = self.c0.add(cs.ns(|| "c0"), &other.c0)?;
308 let c1 = self.c1.add(cs.ns(|| "c1"), &other.c1)?;
309 Ok(Self::new(c0, c1))
310 }
311
312 #[inline]
313 fn add_in_place<CS: ConstraintSystem<ConstraintF>>(
314 &mut self,
315 mut cs: CS,
316 other: &Self,
317 ) -> Result<&mut Self, SynthesisError> {
318 self.c0.add_in_place(cs.ns(|| "c0"), &other.c0)?;
319 self.c1.add_in_place(cs.ns(|| "c1"), &other.c1)?;
320 Ok(self)
321 }
322
323 #[inline]
324 fn sub<CS: ConstraintSystem<ConstraintF>>(
325 &self,
326 mut cs: CS,
327 other: &Self,
328 ) -> Result<Self, SynthesisError> {
329 let c0 = self.c0.sub(cs.ns(|| "c0"), &other.c0)?;
330 let c1 = self.c1.sub(cs.ns(|| "c1"), &other.c1)?;
331 Ok(Self::new(c0, c1))
332 }
333
334 #[inline]
335 fn sub_in_place<CS: ConstraintSystem<ConstraintF>>(
336 &mut self,
337 mut cs: CS,
338 other: &Self,
339 ) -> Result<&mut Self, SynthesisError> {
340 self.c0.sub_in_place(cs.ns(|| "c0"), &other.c0)?;
341 self.c1.sub_in_place(cs.ns(|| "c1"), &other.c1)?;
342 Ok(self)
343 }
344
345 #[inline]
346 fn negate<CS: ConstraintSystem<ConstraintF>>(&self, mut cs: CS) -> Result<Self, SynthesisError> {
347 let c0 = self.c0.negate(cs.ns(|| "c0"))?;
348 let c1 = self.c1.negate(cs.ns(|| "c1"))?;
349 Ok(Self::new(c0, c1))
350 }
351
352 #[inline]
353 fn negate_in_place<CS: ConstraintSystem<ConstraintF>>(
354 &mut self,
355 mut cs: CS,
356 ) -> Result<&mut Self, SynthesisError> {
357 self.c0.negate_in_place(cs.ns(|| "c0"))?;
358 self.c1.negate_in_place(cs.ns(|| "c1"))?;
359 Ok(self)
360 }
361
362 #[inline]
363 fn mul<CS: ConstraintSystem<ConstraintF>>(
364 &self,
365 mut cs: CS,
366 other: &Self,
367 ) -> Result<Self, SynthesisError> {
368 // Karatsuba multiplication:
369 // v0 = A.c0 * B.c0
370 // v1 = A.c1 * B.c1
371 // result.c0 = v0 + non_residue * v1
372 // result.c1 = (A.c0 + A.c1) * (B.c0 + B.c1) - v0 - v1
373 //
374 // Enforced with 3 Fp3_mul_gadget's that ensure that:
375 // A.c1 * B.c1 = v1
376 // A.c0 * B.c0 = v0
377 // (A.c0+A.c1)*(B.c0+B.c1) = result.c1 + v0 + v1
378
379 let v0 = self.c0.mul(cs.ns(|| "v0"), &other.c0)?;
380 let v1 = self.c1.mul(cs.ns(|| "v1"), &other.c1)?;
381 let c0 = {
382 let non_residue_times_v1 =
383 Self::mul_fp6_by_nonresidue(cs.ns(|| "first mul_by_nr"), &v1)?;
384 v0.add(cs.ns(|| "v0 + beta * v1"), &non_residue_times_v1)?
385 };
386 let c1 = {
387 let a0_plus_a1 = self.c0.add(cs.ns(|| "a0 + a1"), &self.c1)?;
388 let b0_plus_b1 = other.c0.add(cs.ns(|| "b0 + b1"), &other.c1)?;
389 let a0_plus_a1_times_b0_plus_b1 =
390 a0_plus_a1.mul(&mut cs.ns(|| "(a0 + a1) * (b0 + b1)"), &b0_plus_b1)?;
391 a0_plus_a1_times_b0_plus_b1
392 .sub(cs.ns(|| "res - v0"), &v0)?
393 .sub(cs.ns(|| "res - v0 - v1"), &v1)?
394 };
395
396 Ok(Self::new(c0, c1))
397 }
398
399 fn square<CS: ConstraintSystem<ConstraintF>>(&self, mut cs: CS) -> Result<Self, SynthesisError> {
400 // From Libsnark/fp2_gadget.tcc
401 // Complex multiplication for Fp2:
402 // v0 = A.c0 * A.c1
403 // result.c0 = (A.c0 + A.c1) * (A.c0 + non_residue * A.c1) - (1 +
404 // non_residue) * v0 result.c1 = 2 * v0
405 // Enforced with 2 constraints:
406 // (2*A.c0) * A.c1 = result.c1
407 // (A.c0 + A.c1) * (A.c0 + non_residue * A.c1) = result.c0 + result.c1 * (1
408 // + non_residue)/2 Reference:
409 // "Multiplication and Squaring on Pairing-Friendly Fields"
410 // Devegili, OhEigeartaigh, Scott, Dahab
411
412 let mut v0 = self.c0.mul(cs.ns(|| "v0"), &self.c1)?;
413 let a0_plus_a1 = self.c0.add(cs.ns(|| "a0 + a1"), &self.c1)?;
414
415 let non_residue_a1 = Self::mul_fp6_by_nonresidue(cs.ns(|| "non_residue * a1"), &self.c1)?;
416 let a0_plus_non_residue_a1 = self
417 .c0
418 .add(cs.ns(|| "a0 + non_residue * a1"), &non_residue_a1)?;
419 let one_plus_non_residue_v0 =
420 Self::mul_fp6_by_nonresidue(cs.ns(|| "non_residue * v0"), &v0)?
421 .add(cs.ns(|| "plus v0"), &v0)?;
422
423 let c0 = a0_plus_a1
424 .mul(
425 cs.ns(|| "(a0 + a1) * (a0 + non_residue * a1)"),
426 &a0_plus_non_residue_a1,
427 )?
428 .sub(cs.ns(|| "- (1 + non_residue) v0"), &one_plus_non_residue_v0)?;
429
430 v0.double_in_place(cs.ns(|| "2v0"))?;
431 let c1 = v0;
432
433 Ok(Self {
434 c0,
435 c1,
436 _params: PhantomData,
437 })
438 }
439
440 #[inline]
441 fn add_constant<CS: ConstraintSystem<ConstraintF>>(
442 &self,
443 mut cs: CS,
444 other: &Fp12<P>,
445 ) -> Result<Self, SynthesisError> {
446 let c0 = self.c0.add_constant(cs.ns(|| "c0"), &other.c0)?;
447 let c1 = self.c1.add_constant(cs.ns(|| "c1"), &other.c1)?;
448
449 Ok(Self::new(c0, c1))
450 }
451
452 #[inline]
453 fn add_constant_in_place<CS: ConstraintSystem<ConstraintF>>(
454 &mut self,
455 mut cs: CS,
456 other: &Fp12<P>,
457 ) -> Result<&mut Self, SynthesisError> {
458 self.c0.add_constant_in_place(cs.ns(|| "c0"), &other.c0)?;
459 self.c1.add_constant_in_place(cs.ns(|| "c1"), &other.c1)?;
460 Ok(self)
461 }
462
463 fn mul_by_constant<CS: ConstraintSystem<ConstraintF>>(
464 &self,
465 mut cs: CS,
466 other: &Fp12<P>,
467 ) -> Result<Self, SynthesisError> {
468 // Karatsuba multiplication (see mul above).
469 // Doesn't need any constraints; returns linear combinations of
470 // `self`'s variables.
471 //
472 // (The operations below are guaranteed to return linear combinations)
473 let (a0, a1) = (&self.c0, &self.c1);
474 let (b0, b1) = (other.c0, other.c1);
475 let mut v0 = a0.mul_by_constant(&mut cs.ns(|| "v0"), &b0)?;
476 let mut v1 = Self::mul_fp6_by_nonresidue(&mut cs.ns(|| "v1"), a1)?;
477 let beta_v1 = v1.mul_by_constant_in_place(&mut cs.ns(|| "beta * v1"), &b1)?;
478
479 v0.add_in_place(&mut cs.ns(|| "c0"), beta_v1)?;
480 let c0 = v0;
481
482 let mut a0b1 = a0.mul_by_constant(&mut cs.ns(|| "a0b1"), &b1)?;
483 let a1b0 = a1.mul_by_constant(&mut cs.ns(|| "a1b0"), &b0)?;
484 a0b1.add_in_place(&mut cs.ns(|| "c1"), &a1b0)?;
485 let c1 = a0b1;
486 Ok(Self::new(c0, c1))
487 }
488
489 fn frobenius_map<CS: ConstraintSystem<ConstraintF>>(
490 &self,
491 cs: CS,
492 power: usize,
493 ) -> Result<Self, SynthesisError> {
494 let mut res = self.clone();
495 res.frobenius_map_in_place(cs, power)?;
496 Ok(res)
497 }
498
499 fn frobenius_map_in_place<CS: ConstraintSystem<ConstraintF>>(
500 &mut self,
501 mut cs: CS,
502 power: usize,
503 ) -> Result<&mut Self, SynthesisError> {
504 self.c0
505 .frobenius_map_in_place(cs.ns(|| "frob_map1"), power)?;
506 self.c1
507 .frobenius_map_in_place(cs.ns(|| "frob_map2"), power)?;
508
509 self.c1
510 .c0
511 .mul_by_constant_in_place(cs.ns(|| "mul1"), &P::FROBENIUS_COEFF_FP12_C1[power % 12])?;
512 self.c1
513 .c1
514 .mul_by_constant_in_place(cs.ns(|| "mul2"), &P::FROBENIUS_COEFF_FP12_C1[power % 12])?;
515 self.c1
516 .c2
517 .mul_by_constant_in_place(cs.ns(|| "mul3"), &P::FROBENIUS_COEFF_FP12_C1[power % 12])?;
518 Ok(self)
519 }
520
521 fn inverse<CS: ConstraintSystem<ConstraintF>>(&self, mut cs: CS) -> Result<Self, SynthesisError> {
522 let inverse = Self::alloc(&mut cs.ns(|| "alloc inverse"), || {
523 self.get_value().and_then(|val| val.inverse()).get()
524 })?;
525
526 // Karatsuba multiplication for Fp2 with the inverse:
527 // v0 = A.c0 * B.c0
528 // v1 = A.c1 * B.c1
529 //
530 // 1 = v0 + non_residue * v1
531 // => v0 = 1 - non_residue * v1
532 //
533 // 0 = result.c1 = (A.c0 + A.c1) * (B.c0 + B.c1) - v0 - v1
534 // => v0 + v1 = (A.c0 + A.c1) * (B.c0 + B.c1)
535 // => 1 + (1 - non_residue) * v1 = (A.c0 + A.c1) * (B.c0 + B.c1)
536 // Enforced with 2 constraints:
537 // A.c1 * B.c1 = v1
538 // => 1 + (1 - non_residue) * v1 = (A.c0 + A.c1) * (B.c0 + B.c1)
539 // Reference:
540 // "Multiplication and Squaring on Pairing-Friendly Fields"
541 // Devegili, OhEigeartaigh, Scott, Dahab
542
543 // Constraint 1
544 let v1 = self.c1.mul(cs.ns(|| "inv_constraint_1"), &inverse.c1)?;
545
546 // Constraint 2
547 let a0_plus_a1 = self.c0.add(cs.ns(|| "a0 + a1"), &self.c1)?;
548 let b0_plus_b1 = inverse.c0.add(cs.ns(|| "b0 + b1"), &inverse.c1)?;
549
550 let one = Fp6::<P::Fp6Params>::one();
551 let rhs = Self::mul_fp6_by_nonresidue(cs.ns(|| "nr * v1"), &v1)?
552 .sub(cs.ns(|| "sub v1"), &v1)?
553 .negate(cs.ns(|| "negate it"))?
554 .add_constant(cs.ns(|| "add one"), &one)?;
555 a0_plus_a1.mul_equals(cs.ns(|| "inv_constraint_2"), &b0_plus_b1, &rhs)?;
556 Ok(inverse)
557 }
558
559 fn mul_equals<CS: ConstraintSystem<ConstraintF>>(
560 &self,
561 mut cs: CS,
562 other: &Self,
563 result: &Self,
564 ) -> Result<(), SynthesisError> {
565 // Karatsuba multiplication for Fp2:
566 // v0 = A.c0 * B.c0
567 // v1 = A.c1 * B.c1
568 // result.c0 = v0 + non_residue * v1
569 // result.c1 = (A.c0 + A.c1) * (B.c0 + B.c1) - v0 - v1
570 // Enforced with 3 constraints:
571 // A.c1 * B.c1 = v1
572 // A.c0 * B.c0 = result.c0 - non_residue * v1
573 // (A.c0+A.c1)*(B.c0+B.c1) = result.c1 + result.c0 + (1 - non_residue) * v1
574 // Reference:
575 // "Multiplication and Squaring on Pairing-Friendly Fields"
576 // Devegili, OhEigeartaigh, Scott, Dahab
577 let mul_cs = &mut cs.ns(|| "mul");
578
579 // Compute v1
580 let v1 = self.c1.mul(mul_cs.ns(|| "v1"), &other.c1)?;
581
582 // Perform second check
583 let non_residue_times_v1 = Self::mul_fp6_by_nonresidue(mul_cs.ns(|| "nr * v1"), &v1)?;
584 let rhs = result
585 .c0
586 .sub(mul_cs.ns(|| "sub from result.c0"), &non_residue_times_v1)?;
587 self.c0
588 .mul_equals(mul_cs.ns(|| "second check"), &other.c0, &rhs)?;
589
590 // Last check
591 let a0_plus_a1 = self.c0.add(mul_cs.ns(|| "a0 + a1"), &self.c1)?;
592 let b0_plus_b1 = other.c0.add(mul_cs.ns(|| "b0 + b1"), &other.c1)?;
593 let one_minus_non_residue_v1 =
594 v1.sub(mul_cs.ns(|| "sub from v1"), &non_residue_times_v1)?;
595
596 let result_c1_plus_result_c0_plus_one_minus_non_residue_v1 = result
597 .c1
598 .add(mul_cs.ns(|| "c1 + c0"), &result.c0)?
599 .add(mul_cs.ns(|| "rest of stuff"), &one_minus_non_residue_v1)?;
600
601 a0_plus_a1.mul_equals(
602 mul_cs.ns(|| "third check"),
603 &b0_plus_b1,
604 &result_c1_plus_result_c0_plus_one_minus_non_residue_v1,
605 )?;
606
607 Ok(())
608 }
609
610 fn cost_of_mul() -> usize {
611 unimplemented!()
612 }
613
614 fn cost_of_inv() -> usize {
615 Self::cost_of_mul() + <Self as EqGadget<ConstraintF>>::cost()
616 }
617}
618
619impl<P, ConstraintF: PrimeField> PartialEq for Fp12Gadget<P, ConstraintF>
620where
621 P: Fp12Parameters,
622 <P::Fp6Params as Fp6Parameters>::Fp2Params: Fp2Parameters<Fp = ConstraintF>,
623{
624 fn eq(&self, other: &Self) -> bool {
625 self.c0 == other.c0 && self.c1 == other.c1
626 }
627}
628
629impl<P, ConstraintF: PrimeField> Eq for Fp12Gadget<P, ConstraintF>
630where
631 P: Fp12Parameters,
632 <P::Fp6Params as Fp6Parameters>::Fp2Params: Fp2Parameters<Fp = ConstraintF>,
633{
634}
635
636impl<P, ConstraintF: PrimeField> EqGadget<ConstraintF> for Fp12Gadget<P, ConstraintF>
637where
638 P: Fp12Parameters,
639 <P::Fp6Params as Fp6Parameters>::Fp2Params: Fp2Parameters<Fp = ConstraintF>,
640{
641}
642
643impl<P, ConstraintF: PrimeField> ConditionalEqGadget<ConstraintF> for Fp12Gadget<P, ConstraintF>
644where
645 P: Fp12Parameters,
646 <P::Fp6Params as Fp6Parameters>::Fp2Params: Fp2Parameters<Fp = ConstraintF>,
647{
648 #[inline]
649 fn conditional_enforce_equal<CS: ConstraintSystem<ConstraintF>>(
650 &self,
651 mut cs: CS,
652 other: &Self,
653 condition: &Boolean,
654 ) -> Result<(), SynthesisError> {
655 self.c0
656 .conditional_enforce_equal(&mut cs.ns(|| "c0"), &other.c0, condition)?;
657 self.c1
658 .conditional_enforce_equal(&mut cs.ns(|| "c1"), &other.c1, condition)?;
659 Ok(())
660 }
661
662 fn cost() -> usize {
663 2 * <Fp6Gadget<P, ConstraintF> as ConditionalEqGadget<ConstraintF>>::cost()
664 }
665}
666
667impl<P, ConstraintF: PrimeField> NEqGadget<ConstraintF> for Fp12Gadget<P, ConstraintF>
668where
669 P: Fp12Parameters,
670 <P::Fp6Params as Fp6Parameters>::Fp2Params: Fp2Parameters<Fp = ConstraintF>,
671{
672 #[inline]
673 fn enforce_not_equal<CS: ConstraintSystem<ConstraintF>>(
674 &self,
675 mut cs: CS,
676 other: &Self,
677 ) -> Result<(), SynthesisError> {
678 self.c0.enforce_not_equal(&mut cs.ns(|| "c0"), &other.c0)?;
679 self.c1.enforce_not_equal(&mut cs.ns(|| "c1"), &other.c1)?;
680 Ok(())
681 }
682
683 fn cost() -> usize {
684 2 * <Fp6Gadget<P, ConstraintF> as NEqGadget<ConstraintF>>::cost()
685 }
686}
687
688impl<P, ConstraintF: PrimeField> ToBitsGadget<ConstraintF> for Fp12Gadget<P, ConstraintF>
689where
690 P: Fp12Parameters,
691 <P::Fp6Params as Fp6Parameters>::Fp2Params: Fp2Parameters<Fp = ConstraintF>,
692{
693 fn to_bits<CS: ConstraintSystem<ConstraintF>>(&self, mut cs: CS) -> Result<Vec<Boolean>, SynthesisError> {
694 let mut c0 = self.c0.to_bits(&mut cs)?;
695 let mut c1 = self.c1.to_bits(cs)?;
696 c0.append(&mut c1);
697 Ok(c0)
698 }
699
700 fn to_bits_strict<CS: ConstraintSystem<ConstraintF>>(
701 &self,
702 mut cs: CS,
703 ) -> Result<Vec<Boolean>, SynthesisError> {
704 let mut c0 = self.c0.to_bits_strict(&mut cs)?;
705 let mut c1 = self.c1.to_bits_strict(cs)?;
706 c0.append(&mut c1);
707 Ok(c0)
708 }
709}
710
711impl<P, ConstraintF: PrimeField> ToBytesGadget<ConstraintF> for Fp12Gadget<P, ConstraintF>
712where
713 P: Fp12Parameters,
714 <P::Fp6Params as Fp6Parameters>::Fp2Params: Fp2Parameters<Fp = ConstraintF>,
715{
716 fn to_bytes<CS: ConstraintSystem<ConstraintF>>(&self, mut cs: CS) -> Result<Vec<UInt8>, SynthesisError> {
717 let mut c0 = self.c0.to_bytes(cs.ns(|| "c0"))?;
718 let mut c1 = self.c1.to_bytes(cs.ns(|| "c1"))?;
719 c0.append(&mut c1);
720 Ok(c0)
721 }
722
723 fn to_bytes_strict<CS: ConstraintSystem<ConstraintF>>(
724 &self,
725 mut cs: CS,
726 ) -> Result<Vec<UInt8>, SynthesisError> {
727 let mut c0 = self.c0.to_bytes_strict(cs.ns(|| "c0"))?;
728 let mut c1 = self.c1.to_bytes_strict(cs.ns(|| "c1"))?;
729 c0.append(&mut c1);
730 Ok(c0)
731 }
732}
733
734impl<P, ConstraintF: PrimeField> Clone for Fp12Gadget<P, ConstraintF>
735where
736 P: Fp12Parameters,
737 <P::Fp6Params as Fp6Parameters>::Fp2Params: Fp2Parameters<Fp = ConstraintF>,
738{
739 fn clone(&self) -> Self {
740 Self::new(self.c0.clone(), self.c1.clone())
741 }
742}
743
744impl<P, ConstraintF: PrimeField> CondSelectGadget<ConstraintF> for Fp12Gadget<P, ConstraintF>
745where
746 P: Fp12Parameters,
747 <P::Fp6Params as Fp6Parameters>::Fp2Params: Fp2Parameters<Fp = ConstraintF>,
748{
749 #[inline]
750 fn conditionally_select<CS: ConstraintSystem<ConstraintF>>(
751 mut cs: CS,
752 cond: &Boolean,
753 first: &Self,
754 second: &Self,
755 ) -> Result<Self, SynthesisError> {
756 let c0 = Fp6Gadget::<P, ConstraintF>::conditionally_select(
757 &mut cs.ns(|| "c0"),
758 cond,
759 &first.c0,
760 &second.c0,
761 )?;
762 let c1 = Fp6Gadget::<P, ConstraintF>::conditionally_select(
763 &mut cs.ns(|| "c1"),
764 cond,
765 &first.c1,
766 &second.c1,
767 )?;
768
769 Ok(Self::new(c0, c1))
770 }
771
772 fn cost() -> usize {
773 2 * <Fp6Gadget<P, ConstraintF> as CondSelectGadget<ConstraintF>>::cost()
774 }
775}
776
777impl<P, ConstraintF: PrimeField> TwoBitLookupGadget<ConstraintF> for Fp12Gadget<P, ConstraintF>
778where
779 P: Fp12Parameters,
780 <P::Fp6Params as Fp6Parameters>::Fp2Params: Fp2Parameters<Fp = ConstraintF>,
781{
782 type TableConstant = Fp12<P>;
783 fn two_bit_lookup<CS: ConstraintSystem<ConstraintF>>(
784 mut cs: CS,
785 b: &[Boolean],
786 c: &[Self::TableConstant],
787 ) -> Result<Self, SynthesisError> {
788 let c0s = c.iter().map(|f| f.c0).collect::<Vec<_>>();
789 let c1s = c.iter().map(|f| f.c1).collect::<Vec<_>>();
790 let c0 = Fp6Gadget::<P, ConstraintF>::two_bit_lookup(cs.ns(|| "Lookup c0"), b, &c0s)?;
791 let c1 = Fp6Gadget::<P, ConstraintF>::two_bit_lookup(cs.ns(|| "Lookup c1"), b, &c1s)?;
792 Ok(Self::new(c0, c1))
793 }
794
795 fn cost() -> usize {
796 2 * <Fp6Gadget<P, ConstraintF> as TwoBitLookupGadget<ConstraintF>>::cost()
797 }
798}
799
800impl<P, ConstraintF: PrimeField> AllocGadget<Fp12<P>, ConstraintF> for Fp12Gadget<P, ConstraintF>
801where
802 P: Fp12Parameters,
803 <P::Fp6Params as Fp6Parameters>::Fp2Params: Fp2Parameters<Fp = ConstraintF>,
804{
805 #[inline]
806 fn alloc<F, T, CS: ConstraintSystem<ConstraintF>>(
807 mut cs: CS,
808 value_gen: F,
809 ) -> Result<Self, SynthesisError>
810 where
811 F: FnOnce() -> Result<T, SynthesisError>,
812 T: Borrow<Fp12<P>>,
813 {
814 let (c0, c1) = match value_gen() {
815 Ok(fe) => {
816 let fe = *fe.borrow();
817 (Ok(fe.c0), Ok(fe.c1))
818 },
819 Err(_) => (
820 Err(SynthesisError::AssignmentMissing),
821 Err(SynthesisError::AssignmentMissing),
822 ),
823 };
824
825 let c0 = Fp6Gadget::<P, ConstraintF>::alloc(&mut cs.ns(|| "c0"), || c0)?;
826 let c1 = Fp6Gadget::<P, ConstraintF>::alloc(&mut cs.ns(|| "c1"), || c1)?;
827 Ok(Self::new(c0, c1))
828 }
829
830 #[inline]
831 fn alloc_input<F, T, CS: ConstraintSystem<ConstraintF>>(
832 mut cs: CS,
833 value_gen: F,
834 ) -> Result<Self, SynthesisError>
835 where
836 F: FnOnce() -> Result<T, SynthesisError>,
837 T: Borrow<Fp12<P>>,
838 {
839 let (c0, c1) = match value_gen() {
840 Ok(fe) => {
841 let fe = *fe.borrow();
842 (Ok(fe.c0), Ok(fe.c1))
843 },
844 Err(_) => (
845 Err(SynthesisError::AssignmentMissing),
846 Err(SynthesisError::AssignmentMissing),
847 ),
848 };
849
850 let c0 = Fp6Gadget::<P, ConstraintF>::alloc_input(&mut cs.ns(|| "c0"), || c0)?;
851 let c1 = Fp6Gadget::<P, ConstraintF>::alloc_input(&mut cs.ns(|| "c1"), || c1)?;
852 Ok(Self::new(c0, c1))
853 }
854}