1use crate::{
2 convert::{ToBitsGadget, ToBytesGadget, ToConstraintFieldGadget},
3 fields::{fp::FpVar, FieldOpsBounds, FieldVar},
4 prelude::*,
5 Vec,
6};
7use ark_ff::{
8 fields::{Field, QuadExtConfig, QuadExtField},
9 Zero,
10};
11use ark_relations::r1cs::{ConstraintSystemRef, Namespace, SynthesisError};
12use core::{borrow::Borrow, marker::PhantomData};
13use educe::Educe;
14
15#[derive(Educe)]
18#[educe(Debug, Clone)]
19#[must_use]
20pub struct QuadExtVar<BF: FieldVar<P::BaseField, P::BasePrimeField>, P: QuadExtVarConfig<BF>>
21where
22 for<'a> &'a BF: FieldOpsBounds<'a, P::BaseField, BF>,
23{
24 pub c0: BF,
26 pub c1: BF,
28 #[educe(Debug(ignore))]
29 _params: PhantomData<P>,
30}
31
32pub trait QuadExtVarConfig<BF: FieldVar<Self::BaseField, Self::BasePrimeField>>:
35 QuadExtConfig
36where
37 for<'a> &'a BF: FieldOpsBounds<'a, Self::BaseField, BF>,
38{
39 fn mul_base_field_var_by_frob_coeff(fe: &mut BF, power: usize);
43}
44
45impl<BF: FieldVar<P::BaseField, P::BasePrimeField>, P: QuadExtVarConfig<BF>> QuadExtVar<BF, P>
46where
47 for<'a> &'a BF: FieldOpsBounds<'a, P::BaseField, BF>,
48{
49 pub fn new(c0: BF, c1: BF) -> Self {
51 Self {
52 c0,
53 c1,
54 _params: PhantomData,
55 }
56 }
57
58 #[inline]
61 pub fn mul_base_field_by_nonresidue(fe: &BF) -> Result<BF, SynthesisError> {
62 Ok(fe * P::NONRESIDUE)
63 }
64
65 #[inline]
67 pub fn mul_by_base_field_constant(&self, fe: P::BaseField) -> Self {
68 let c0 = self.c0.clone() * fe;
69 let c1 = self.c1.clone() * fe;
70 QuadExtVar::new(c0, c1)
71 }
72
73 #[inline]
75 pub fn mul_assign_by_base_field_constant(&mut self, fe: P::BaseField) {
76 *self = (&*self).mul_by_base_field_constant(fe);
77 }
78
79 #[inline]
82 pub fn unitary_inverse(&self) -> Result<Self, SynthesisError> {
83 Ok(Self::new(self.c0.clone(), self.c1.negate()?))
84 }
85
86 #[inline]
89 #[tracing::instrument(target = "r1cs", skip(exponent))]
90 pub fn cyclotomic_exp(&self, exponent: impl AsRef<[u64]>) -> Result<Self, SynthesisError>
91 where
92 Self: FieldVar<QuadExtField<P>, P::BasePrimeField>,
93 {
94 let mut res = Self::one();
95 let self_inverse = self.unitary_inverse()?;
96
97 let mut found_nonzero = false;
98 let naf = ark_ff::biginteger::arithmetic::find_naf(exponent.as_ref());
99
100 for &value in naf.iter().rev() {
101 if found_nonzero {
102 res.square_in_place()?;
103 }
104
105 if value != 0 {
106 found_nonzero = true;
107
108 if value > 0 {
109 res *= self;
110 } else {
111 res *= &self_inverse;
112 }
113 }
114 }
115
116 Ok(res)
117 }
118}
119
120impl<BF, P> R1CSVar<P::BasePrimeField> for QuadExtVar<BF, P>
121where
122 BF: FieldVar<P::BaseField, P::BasePrimeField>,
123 for<'a> &'a BF: FieldOpsBounds<'a, P::BaseField, BF>,
124 P: QuadExtVarConfig<BF>,
125{
126 type Value = QuadExtField<P>;
127
128 fn cs(&self) -> ConstraintSystemRef<P::BasePrimeField> {
129 [&self.c0, &self.c1].cs()
130 }
131
132 #[inline]
133 fn value(&self) -> Result<Self::Value, SynthesisError> {
134 match (self.c0.value(), self.c1.value()) {
135 (Ok(c0), Ok(c1)) => Ok(QuadExtField::new(c0, c1)),
136 (..) => Err(SynthesisError::AssignmentMissing),
137 }
138 }
139}
140
141impl<BF, P> From<Boolean<P::BasePrimeField>> for QuadExtVar<BF, P>
142where
143 BF: FieldVar<P::BaseField, P::BasePrimeField>,
144 for<'a> &'a BF: FieldOpsBounds<'a, P::BaseField, BF>,
145 P: QuadExtVarConfig<BF>,
146{
147 fn from(other: Boolean<P::BasePrimeField>) -> Self {
148 let c0 = BF::from(other);
149 let c1 = BF::zero();
150 Self::new(c0, c1)
151 }
152}
153
154impl<'a, BF, P> FieldOpsBounds<'a, QuadExtField<P>, QuadExtVar<BF, P>> for QuadExtVar<BF, P>
155where
156 BF: FieldVar<P::BaseField, P::BasePrimeField>,
157 for<'b> &'b BF: FieldOpsBounds<'b, P::BaseField, BF>,
158 P: QuadExtVarConfig<BF>,
159{
160}
161impl<'a, BF, P> FieldOpsBounds<'a, QuadExtField<P>, QuadExtVar<BF, P>> for &'a QuadExtVar<BF, P>
162where
163 BF: FieldVar<P::BaseField, P::BasePrimeField>,
164 for<'b> &'b BF: FieldOpsBounds<'b, P::BaseField, BF>,
165 P: QuadExtVarConfig<BF>,
166{
167}
168
169impl<BF, P> FieldVar<QuadExtField<P>, P::BasePrimeField> for QuadExtVar<BF, P>
170where
171 BF: FieldVar<P::BaseField, P::BasePrimeField>,
172 for<'a> &'a BF: FieldOpsBounds<'a, P::BaseField, BF>,
173 P: QuadExtVarConfig<BF>,
174{
175 fn constant(other: QuadExtField<P>) -> Self {
176 let c0 = BF::constant(other.c0);
177 let c1 = BF::constant(other.c1);
178 Self::new(c0, c1)
179 }
180
181 fn zero() -> Self {
182 let c0 = BF::zero();
183 let c1 = BF::zero();
184 Self::new(c0, c1)
185 }
186
187 fn one() -> Self {
188 let c0 = BF::one();
189 let c1 = BF::zero();
190 Self::new(c0, c1)
191 }
192
193 #[inline]
194 #[tracing::instrument(target = "r1cs")]
195 fn double(&self) -> Result<Self, SynthesisError> {
196 let c0 = self.c0.double()?;
197 let c1 = self.c1.double()?;
198 Ok(Self::new(c0, c1))
199 }
200
201 #[inline]
202 #[tracing::instrument(target = "r1cs")]
203 fn negate(&self) -> Result<Self, SynthesisError> {
204 let mut result = self.clone();
205 result.c0.negate_in_place()?;
206 result.c1.negate_in_place()?;
207 Ok(result)
208 }
209
210 #[inline]
211 #[tracing::instrument(target = "r1cs")]
212 fn square(&self) -> Result<Self, SynthesisError> {
213 let mut v0 = &self.c0 - &self.c1;
220 let v3 = &self.c0 - &Self::mul_base_field_by_nonresidue(&self.c1)?;
222 let v2 = &self.c0 * &self.c1;
224
225 v0 *= &v3;
227 v0 += &v2;
228
229 let c0 = &v0 + &Self::mul_base_field_by_nonresidue(&v2)?;
230 let c1 = v2.double()?;
231
232 Ok(Self::new(c0, c1))
233 }
234
235 #[tracing::instrument(target = "r1cs")]
236 fn mul_equals(&self, other: &Self, result: &Self) -> Result<(), SynthesisError> {
237 let v1 = &self.c1 * &other.c1;
251
252 let non_residue_times_v1 = Self::mul_base_field_by_nonresidue(&v1)?;
254 let rhs = &result.c0 - &non_residue_times_v1;
255 self.c0.mul_equals(&other.c0, &rhs)?;
256
257 let a0_plus_a1 = &self.c0 + &self.c1;
259 let b0_plus_b1 = &other.c0 + &other.c1;
260 let one_minus_non_residue_v1 = &v1 - &non_residue_times_v1;
261
262 let tmp = &(&result.c1 + &result.c0) + &one_minus_non_residue_v1;
263 a0_plus_a1.mul_equals(&b0_plus_b1, &tmp)?;
264
265 Ok(())
266 }
267
268 #[tracing::instrument(target = "r1cs")]
269 fn frobenius_map(&self, power: usize) -> Result<Self, SynthesisError> {
270 let mut result = self.clone();
271 result.c0.frobenius_map_in_place(power)?;
272 result.c1.frobenius_map_in_place(power)?;
273 P::mul_base_field_var_by_frob_coeff(&mut result.c1, power);
274 Ok(result)
275 }
276
277 #[tracing::instrument(target = "r1cs")]
278 fn inverse(&self) -> Result<Self, SynthesisError> {
279 let mode = if self.is_constant() {
280 AllocationMode::Constant
281 } else {
282 AllocationMode::Witness
283 };
284 let inverse = Self::new_variable(
285 self.cs(),
286 || {
287 self.value()
288 .map(|f| f.inverse().unwrap_or_else(QuadExtField::zero))
289 },
290 mode,
291 )?;
292 self.mul_equals(&inverse, &Self::one())?;
293 Ok(inverse)
294 }
295}
296
297impl_bounded_ops!(
298 QuadExtVar<BF, P>,
299 QuadExtField<P>,
300 Add,
301 add,
302 AddAssign,
303 add_assign,
304 |this: &'a QuadExtVar<BF, P>, other: &'a QuadExtVar<BF, P>| {
305 let c0 = &this.c0 + &other.c0;
306 let c1 = &this.c1 + &other.c1;
307 QuadExtVar::new(c0, c1)
308 },
309 |this: &'a QuadExtVar<BF, P>, other: QuadExtField<P>| {
310 this + QuadExtVar::constant(other)
311 },
312 (BF: FieldVar<P::BaseField, P::BasePrimeField>, P: QuadExtVarConfig<BF>),
313 for <'b> &'b BF: FieldOpsBounds<'b, P::BaseField, BF>
314);
315impl_bounded_ops!(
316 QuadExtVar<BF, P>,
317 QuadExtField<P>,
318 Sub,
319 sub,
320 SubAssign,
321 sub_assign,
322 |this: &'a QuadExtVar<BF, P>, other: &'a QuadExtVar<BF, P>| {
323 let c0 = &this.c0 - &other.c0;
324 let c1 = &this.c1 - &other.c1;
325 QuadExtVar::new(c0, c1)
326 },
327 |this: &'a QuadExtVar<BF, P>, other: QuadExtField<P>| {
328 this - QuadExtVar::constant(other)
329 },
330 (BF: FieldVar<P::BaseField, P::BasePrimeField>, P: QuadExtVarConfig<BF>),
331 for <'b> &'b BF: FieldOpsBounds<'b, P::BaseField, BF>
332);
333impl_bounded_ops!(
334 QuadExtVar<BF, P>,
335 QuadExtField<P>,
336 Mul,
337 mul,
338 MulAssign,
339 mul_assign,
340 |this: &'a QuadExtVar<BF, P>, other: &'a QuadExtVar<BF, P>| {
341 let mut result = this.clone();
354 let v0 = &this.c0 * &other.c0;
355 let v1 = &this.c1 * &other.c1;
356
357 result.c1 += &this.c0;
358 result.c1 *= &other.c0 + &other.c1;
359 result.c1 -= &v0;
360 result.c1 -= &v1;
361 result.c0 = v0 + &QuadExtVar::<BF, P>::mul_base_field_by_nonresidue(&v1).unwrap();
362 result
363 },
364 |this: &'a QuadExtVar<BF, P>, other: QuadExtField<P>| {
365 this * QuadExtVar::constant(other)
366 },
367 (BF: FieldVar<P::BaseField, P::BasePrimeField>, P: QuadExtVarConfig<BF>),
368 for <'b> &'b BF: FieldOpsBounds<'b, P::BaseField, BF>
369);
370
371impl<BF, P> EqGadget<P::BasePrimeField> for QuadExtVar<BF, P>
372where
373 BF: FieldVar<P::BaseField, P::BasePrimeField>,
374 for<'b> &'b BF: FieldOpsBounds<'b, P::BaseField, BF>,
375 P: QuadExtVarConfig<BF>,
376{
377 #[tracing::instrument(target = "r1cs")]
378 fn is_eq(&self, other: &Self) -> Result<Boolean<P::BasePrimeField>, SynthesisError> {
379 let b0 = self.c0.is_eq(&other.c0)?;
380 let b1 = self.c1.is_eq(&other.c1)?;
381 Ok(b0 & b1)
382 }
383
384 #[inline]
385 #[tracing::instrument(target = "r1cs")]
386 fn conditional_enforce_equal(
387 &self,
388 other: &Self,
389 condition: &Boolean<P::BasePrimeField>,
390 ) -> Result<(), SynthesisError> {
391 self.c0.conditional_enforce_equal(&other.c0, condition)?;
392 self.c1.conditional_enforce_equal(&other.c1, condition)?;
393 Ok(())
394 }
395
396 #[inline]
397 #[tracing::instrument(target = "r1cs")]
398 fn conditional_enforce_not_equal(
399 &self,
400 other: &Self,
401 condition: &Boolean<P::BasePrimeField>,
402 ) -> Result<(), SynthesisError> {
403 let is_equal = self.is_eq(other)?;
404 (is_equal & condition).enforce_equal(&Boolean::FALSE)
405 }
406}
407
408impl<BF, P> ToBitsGadget<P::BasePrimeField> for QuadExtVar<BF, P>
409where
410 BF: FieldVar<P::BaseField, P::BasePrimeField>,
411 for<'b> &'b BF: FieldOpsBounds<'b, P::BaseField, BF>,
412 P: QuadExtVarConfig<BF>,
413{
414 #[tracing::instrument(target = "r1cs")]
415 fn to_bits_le(&self) -> Result<Vec<Boolean<P::BasePrimeField>>, SynthesisError> {
416 let mut c0 = self.c0.to_bits_le()?;
417 let mut c1 = self.c1.to_bits_le()?;
418 c0.append(&mut c1);
419 Ok(c0)
420 }
421
422 #[tracing::instrument(target = "r1cs")]
423 fn to_non_unique_bits_le(&self) -> Result<Vec<Boolean<P::BasePrimeField>>, SynthesisError> {
424 let mut c0 = self.c0.to_non_unique_bits_le()?;
425 let mut c1 = self.c1.to_non_unique_bits_le()?;
426 c0.append(&mut c1);
427 Ok(c0)
428 }
429}
430
431impl<BF, P> ToBytesGadget<P::BasePrimeField> for QuadExtVar<BF, P>
432where
433 BF: FieldVar<P::BaseField, P::BasePrimeField>,
434 for<'b> &'b BF: FieldOpsBounds<'b, P::BaseField, BF>,
435 P: QuadExtVarConfig<BF>,
436{
437 #[tracing::instrument(target = "r1cs")]
438 fn to_bytes_le(&self) -> Result<Vec<UInt8<P::BasePrimeField>>, SynthesisError> {
439 let mut c0 = self.c0.to_bytes_le()?;
440 let mut c1 = self.c1.to_bytes_le()?;
441 c0.append(&mut c1);
442 Ok(c0)
443 }
444
445 #[tracing::instrument(target = "r1cs")]
446 fn to_non_unique_bytes_le(&self) -> Result<Vec<UInt8<P::BasePrimeField>>, SynthesisError> {
447 let mut c0 = self.c0.to_non_unique_bytes_le()?;
448 let mut c1 = self.c1.to_non_unique_bytes_le()?;
449 c0.append(&mut c1);
450 Ok(c0)
451 }
452}
453
454impl<BF, P> ToConstraintFieldGadget<P::BasePrimeField> for QuadExtVar<BF, P>
455where
456 BF: FieldVar<P::BaseField, P::BasePrimeField>,
457 for<'a> &'a BF: FieldOpsBounds<'a, P::BaseField, BF>,
458 P: QuadExtVarConfig<BF>,
459 BF: ToConstraintFieldGadget<P::BasePrimeField>,
460{
461 #[tracing::instrument(target = "r1cs")]
462 fn to_constraint_field(&self) -> Result<Vec<FpVar<P::BasePrimeField>>, SynthesisError> {
463 let mut res = Vec::new();
464
465 res.extend_from_slice(&self.c0.to_constraint_field()?);
466 res.extend_from_slice(&self.c1.to_constraint_field()?);
467
468 Ok(res)
469 }
470}
471
472impl<BF, P> CondSelectGadget<P::BasePrimeField> for QuadExtVar<BF, P>
473where
474 BF: FieldVar<P::BaseField, P::BasePrimeField>,
475 for<'b> &'b BF: FieldOpsBounds<'b, P::BaseField, BF>,
476 P: QuadExtVarConfig<BF>,
477{
478 #[inline]
479 fn conditionally_select(
480 cond: &Boolean<P::BasePrimeField>,
481 true_value: &Self,
482 false_value: &Self,
483 ) -> Result<Self, SynthesisError> {
484 let c0 = BF::conditionally_select(cond, &true_value.c0, &false_value.c0)?;
485 let c1 = BF::conditionally_select(cond, &true_value.c1, &false_value.c1)?;
486 Ok(Self::new(c0, c1))
487 }
488}
489
490impl<BF, P> TwoBitLookupGadget<P::BasePrimeField> for QuadExtVar<BF, P>
491where
492 BF: FieldVar<P::BaseField, P::BasePrimeField>
493 + TwoBitLookupGadget<P::BasePrimeField, TableConstant = P::BaseField>,
494 for<'b> &'b BF: FieldOpsBounds<'b, P::BaseField, BF>,
495 P: QuadExtVarConfig<BF>,
496{
497 type TableConstant = QuadExtField<P>;
498
499 #[tracing::instrument(target = "r1cs")]
500 fn two_bit_lookup(
501 b: &[Boolean<P::BasePrimeField>],
502 c: &[Self::TableConstant],
503 ) -> Result<Self, SynthesisError> {
504 let c0s = c.iter().map(|f| f.c0).collect::<Vec<_>>();
505 let c1s = c.iter().map(|f| f.c1).collect::<Vec<_>>();
506 let c0 = BF::two_bit_lookup(b, &c0s)?;
507 let c1 = BF::two_bit_lookup(b, &c1s)?;
508 Ok(Self::new(c0, c1))
509 }
510}
511
512impl<BF, P> ThreeBitCondNegLookupGadget<P::BasePrimeField> for QuadExtVar<BF, P>
513where
514 BF: FieldVar<P::BaseField, P::BasePrimeField>
515 + ThreeBitCondNegLookupGadget<P::BasePrimeField, TableConstant = P::BaseField>,
516 for<'b> &'b BF: FieldOpsBounds<'b, P::BaseField, BF>,
517 P: QuadExtVarConfig<BF>,
518{
519 type TableConstant = QuadExtField<P>;
520
521 #[tracing::instrument(target = "r1cs")]
522 fn three_bit_cond_neg_lookup(
523 b: &[Boolean<P::BasePrimeField>],
524 b0b1: &Boolean<P::BasePrimeField>,
525 c: &[Self::TableConstant],
526 ) -> Result<Self, SynthesisError> {
527 let c0s = c.iter().map(|f| f.c0).collect::<Vec<_>>();
528 let c1s = c.iter().map(|f| f.c1).collect::<Vec<_>>();
529 let c0 = BF::three_bit_cond_neg_lookup(b, b0b1, &c0s)?;
530 let c1 = BF::three_bit_cond_neg_lookup(b, b0b1, &c1s)?;
531 Ok(Self::new(c0, c1))
532 }
533}
534
535impl<BF, P> AllocVar<QuadExtField<P>, P::BasePrimeField> for QuadExtVar<BF, P>
536where
537 BF: FieldVar<P::BaseField, P::BasePrimeField>,
538 for<'b> &'b BF: FieldOpsBounds<'b, P::BaseField, BF>,
539 P: QuadExtVarConfig<BF>,
540{
541 fn new_variable<T: Borrow<QuadExtField<P>>>(
542 cs: impl Into<Namespace<P::BasePrimeField>>,
543 f: impl FnOnce() -> Result<T, SynthesisError>,
544 mode: AllocationMode,
545 ) -> Result<Self, SynthesisError> {
546 let ns = cs.into();
547 let cs = ns.cs();
548 let (c0, c1) = match f() {
549 Ok(fe) => (Ok(fe.borrow().c0), Ok(fe.borrow().c1)),
550 Err(_) => (
551 Err(SynthesisError::AssignmentMissing),
552 Err(SynthesisError::AssignmentMissing),
553 ),
554 };
555
556 let c0 = BF::new_variable(ark_relations::ns!(cs, "c0"), || c0, mode)?;
557 let c1 = BF::new_variable(ark_relations::ns!(cs, "c1"), || c1, mode)?;
558 Ok(Self::new(c0, c1))
559 }
560}