ark-r1cs-std/src/fields/fp/mod.rs
src/fields/fp/mod.rsRaw
1use ark_ff::{BigInteger, PrimeField};
2use ark_relations::r1cs::{
3 ConstraintSystemRef, LinearCombination, Namespace, SynthesisError, Variable,
4};
5
6use core::borrow::Borrow;
7
8use crate::{
9 boolean::AllocatedBool,
10 convert::{ToBitsGadget, ToBytesGadget, ToConstraintFieldGadget},
11 fields::{FieldOpsBounds, FieldVar},
12 prelude::*,
13 Assignment, Vec,
14};
15use ark_std::iter::Sum;
16
17mod cmp;
18
19/// Represents a variable in the constraint system whose
20/// value can be an arbitrary field element.
21#[derive(Debug, Clone)]
22#[must_use]
23pub struct AllocatedFp<F: PrimeField> {
24 pub(crate) value: Option<F>,
25 /// The allocated variable corresponding to `self` in `self.cs`.
26 pub variable: Variable,
27 /// The constraint system that `self` was allocated in.
28 pub cs: ConstraintSystemRef<F>,
29 enable_lc: bool,
30}
31
32impl<F: PrimeField> AllocatedFp<F> {
33 /// Constructs a new `AllocatedFp` from a (optional) value, a low-level
34 /// Variable, and a `ConstraintSystemRef`.
35 pub fn new(value: Option<F>, variable: Variable, cs: ConstraintSystemRef<F>) -> Self {
36 Self {
37 value,
38 variable,
39 enable_lc: cs.should_construct_matrices(),
40 cs,
41 }
42 }
43}
44
45/// Represent variables corresponding to a field element in `F`.
46#[derive(Clone, Debug)]
47#[must_use]
48pub enum FpVar<F: PrimeField> {
49 /// Represents a constant in the constraint system, which means that
50 /// it does not have a corresponding variable.
51 Constant(F),
52 /// Represents an allocated variable constant in the constraint system.
53 Var(AllocatedFp<F>),
54}
55
56impl<F: PrimeField> FpVar<F> {
57 /// Decomposes `self` into a vector of `bits` and a remainder `rest` such
58 /// that
59 /// * `bits.len() == size`, and
60 /// * `rest == 0`.
61 pub fn to_bits_le_with_top_bits_zero(
62 &self,
63 size: usize,
64 ) -> Result<(Vec<Boolean<F>>, Self), SynthesisError> {
65 assert!(size <= F::MODULUS_BIT_SIZE as usize - 1);
66 let cs = self.cs();
67 let mode = if self.is_constant() {
68 AllocationMode::Constant
69 } else {
70 AllocationMode::Witness
71 };
72
73 let value = self.value().map(|f| f.into_bigint());
74 let lower_bits = (0..size)
75 .map(|i| {
76 Boolean::new_variable(cs.clone(), || value.map(|v| v.get_bit(i as usize)), mode)
77 })
78 .collect::<Result<Vec<_>, _>>()?;
79 let lower_bits_fp = Boolean::le_bits_to_fp(&lower_bits)?;
80 let rest = self - &lower_bits_fp;
81 rest.enforce_equal(&Self::zero())?;
82 Ok((lower_bits, rest))
83 }
84}
85
86impl<F: PrimeField> R1CSVar<F> for FpVar<F> {
87 type Value = F;
88
89 fn cs(&self) -> ConstraintSystemRef<F> {
90 match self {
91 Self::Constant(_) => ConstraintSystemRef::None,
92 Self::Var(a) => a.cs.clone(),
93 }
94 }
95
96 fn value(&self) -> Result<Self::Value, SynthesisError> {
97 match self {
98 Self::Constant(v) => Ok(*v),
99 Self::Var(v) => v.value(),
100 }
101 }
102}
103
104impl<F: PrimeField> From<Boolean<F>> for FpVar<F> {
105 fn from(other: Boolean<F>) -> Self {
106 if let Boolean::Constant(b) = other {
107 Self::Constant(F::from(b as u8))
108 } else {
109 // `other` is a variable
110 let cs = other.cs();
111 let variable = cs.new_lc(if cs.should_construct_matrices() {
112 other.lc()
113 } else {
114 lc!()
115 }).unwrap();
116 Self::Var(AllocatedFp::new(
117 other.value().ok().map(|b| F::from(b as u8)),
118 variable,
119 cs,
120 ))
121 }
122 }
123}
124
125impl<F: PrimeField> From<AllocatedFp<F>> for FpVar<F> {
126 fn from(other: AllocatedFp<F>) -> Self {
127 Self::Var(other)
128 }
129}
130
131impl<'a, F: PrimeField> FieldOpsBounds<'a, F, Self> for FpVar<F> {}
132impl<'a, F: PrimeField> FieldOpsBounds<'a, F, FpVar<F>> for &'a FpVar<F> {}
133
134impl<F: PrimeField> AllocatedFp<F> {
135 /// Constructs `Self` from a `Boolean`: if `other` is false, this outputs
136 /// `zero`, else it outputs `one`.
137 pub fn from(other: Boolean<F>) -> Self {
138 let cs = other.cs();
139 let variable = cs.new_lc(if cs.should_construct_matrices() {
140 other.lc()
141 } else {
142 lc!()
143 }).unwrap();
144 Self::new(other.value().ok().map(|b| F::from(b as u8)), variable, cs)
145 }
146
147 /// Returns the value assigned to `self` in the underlying constraint system
148 /// (if a value was assigned).
149 pub fn value(&self) -> Result<F, SynthesisError> {
150 self.value.ok_or(SynthesisError::AssignmentMissing)
151 }
152
153 /// Outputs `self + other`.
154 ///
155 /// This does not create any constraints.
156 #[tracing::instrument(target = "r1cs")]
157 pub fn add(&self, other: &Self) -> Self {
158 let value = match (self.value, other.value) {
159 (Some(val1), Some(val2)) => Some(val1 + &val2),
160 (..) => None,
161 };
162
163 let variable = self
164 .cs
165 .new_lc(if self.enable_lc {
166 lc!() + self.variable + other.variable
167 } else {
168 lc!()
169 })
170 .unwrap();
171 AllocatedFp::new(value, variable, self.cs.clone())
172 }
173
174 /// Add many allocated Fp elements together.
175 ///
176 /// This does not create any constraints and only creates one linear
177 /// combination.
178 pub fn add_many<B: Borrow<Self>, I: Iterator<Item = B>>(iter: I) -> Self {
179 let mut cs = ConstraintSystemRef::None;
180 let mut has_value = true;
181 let mut value = F::zero();
182 let mut new_lc = lc!();
183
184 let mut num_iters = 0;
185 for variable in iter {
186 let variable = variable.borrow();
187 if !variable.cs.is_none() {
188 cs = cs.or(variable.cs.clone());
189 }
190 if variable.value.is_none() {
191 has_value = false;
192 } else {
193 value += variable.value.unwrap();
194 }
195 if variable.enable_lc {
196 new_lc = new_lc + variable.variable;
197 }
198 num_iters += 1;
199 }
200 assert_ne!(num_iters, 0);
201
202 let variable = cs.new_lc(new_lc).unwrap();
203
204 if has_value {
205 AllocatedFp::new(Some(value), variable, cs)
206 } else {
207 AllocatedFp::new(None, variable, cs)
208 }
209 }
210
211 /// Outputs `self - other`.
212 ///
213 /// This does not create any constraints.
214 #[tracing::instrument(target = "r1cs")]
215 pub fn sub(&self, other: &Self) -> Self {
216 let value = match (self.value, other.value) {
217 (Some(val1), Some(val2)) => Some(val1 - &val2),
218 (..) => None,
219 };
220
221 let variable = self
222 .cs
223 .new_lc(if self.enable_lc {
224 lc!() + self.variable - other.variable
225 } else {
226 lc!()
227 })
228 .unwrap();
229 AllocatedFp::new(value, variable, self.cs.clone())
230 }
231
232 /// Outputs `self * other`.
233 ///
234 /// This requires *one* constraint.
235 #[tracing::instrument(target = "r1cs")]
236 pub fn mul(&self, other: &Self) -> Self {
237 let product = AllocatedFp::new_witness(self.cs.clone(), || {
238 Ok(self.value.get()? * &other.value.get()?)
239 })
240 .unwrap();
241 if self.enable_lc {
242 self.cs
243 .enforce_constraint(
244 lc!() + self.variable,
245 lc!() + other.variable,
246 lc!() + product.variable,
247 )
248 .unwrap();
249 } else {
250 self.cs.borrow_mut().unwrap().num_constraints += 1;
251 }
252
253 product
254 }
255
256 /// Output `self + other`
257 ///
258 /// This does not create any constraints.
259 #[tracing::instrument(target = "r1cs")]
260 pub fn add_constant(&self, other: F) -> Self {
261 if other.is_zero() {
262 self.clone()
263 } else {
264 let value = self.value.map(|val| val + other);
265 let variable = self
266 .cs
267 .new_lc(if self.enable_lc {
268 lc!() + self.variable + (other, Variable::One)
269 } else {
270 lc!()
271 })
272 .unwrap();
273 AllocatedFp::new(value, variable, self.cs.clone())
274 }
275 }
276
277 /// Output `self - other`
278 ///
279 /// This does not create any constraints.
280 #[tracing::instrument(target = "r1cs")]
281 pub fn sub_constant(&self, other: F) -> Self {
282 self.add_constant(-other)
283 }
284
285 /// Output `self * other`
286 ///
287 /// This does not create any constraints.
288 #[tracing::instrument(target = "r1cs")]
289 pub fn mul_constant(&self, other: F) -> Self {
290 if other.is_one() {
291 self.clone()
292 } else {
293 let value = self.value.map(|val| val * other);
294 let variable = self
295 .cs
296 .new_lc(if self.enable_lc {
297 lc!() + (other, self.variable)
298 } else {
299 lc!()
300 })
301 .unwrap();
302 AllocatedFp::new(value, variable, self.cs.clone())
303 }
304 }
305
306 /// Output `self + self`
307 ///
308 /// This does not create any constraints.
309 #[tracing::instrument(target = "r1cs")]
310 pub fn double(&self) -> Result<Self, SynthesisError> {
311 let value = self.value.map(|val| val.double());
312 let variable = self.cs.new_lc(if self.enable_lc {
313 lc!() + self.variable + self.variable
314 } else {
315 lc!()
316 })?;
317 Ok(Self::new(value, variable, self.cs.clone()))
318 }
319
320 /// Output `-self`
321 ///
322 /// This does not create any constraints.
323 #[tracing::instrument(target = "r1cs")]
324 pub fn negate(&self) -> Self {
325 let mut result = self.clone();
326 result.negate_in_place();
327 result
328 }
329
330 /// Sets `self = -self`
331 ///
332 /// This does not create any constraints.
333 #[tracing::instrument(target = "r1cs")]
334 pub fn negate_in_place(&mut self) -> &mut Self {
335 if let Some(val) = self.value.as_mut() {
336 *val = -(*val);
337 }
338 self.variable = self
339 .cs
340 .new_lc(if self.enable_lc {
341 lc!() - self.variable
342 } else {
343 lc!()
344 })
345 .unwrap();
346 self
347 }
348
349 /// Outputs `self * self`
350 ///
351 /// This requires *one* constraint.
352 #[tracing::instrument(target = "r1cs")]
353 pub fn square(&self) -> Result<Self, SynthesisError> {
354 Ok(self.mul(self))
355 }
356
357 /// Outputs `result` such that `result * self = 1`.
358 ///
359 /// This requires *one* constraint.
360 #[tracing::instrument(target = "r1cs")]
361 pub fn inverse(&self) -> Result<Self, SynthesisError> {
362 let inverse = Self::new_witness(self.cs.clone(), || {
363 Ok(self.value.get()?.inverse().unwrap_or_else(F::zero))
364 })?;
365
366 if self.enable_lc {
367 self.cs.enforce_constraint(
368 lc!() + self.variable,
369 lc!() + inverse.variable,
370 lc!() + Variable::One,
371 )?;
372 } else {
373 self.cs.borrow_mut().unwrap().num_constraints += 1;
374 }
375
376 Ok(inverse)
377 }
378
379 /// This is a no-op for prime fields.
380 #[tracing::instrument(target = "r1cs")]
381 pub fn frobenius_map(&self, _: usize) -> Result<Self, SynthesisError> {
382 Ok(self.clone())
383 }
384
385 /// Enforces that `self * other = result`.
386 ///
387 /// This requires *one* constraint.
388 #[tracing::instrument(target = "r1cs")]
389 pub fn mul_equals(&self, other: &Self, result: &Self) -> Result<(), SynthesisError> {
390 if self.enable_lc {
391 self.cs.enforce_constraint(
392 lc!() + self.variable,
393 lc!() + other.variable,
394 lc!() + result.variable,
395 )?;
396 } else {
397 self.cs.borrow_mut().unwrap().num_constraints += 1;
398 }
399 Ok(())
400 }
401
402 /// Enforces that `self * self = result`.
403 ///
404 /// This requires *one* constraint.
405 #[tracing::instrument(target = "r1cs")]
406 pub fn square_equals(&self, result: &Self) -> Result<(), SynthesisError> {
407 if self.enable_lc {
408 self.cs.enforce_constraint(
409 lc!() + self.variable,
410 lc!() + self.variable,
411 lc!() + result.variable,
412 )?;
413 } else {
414 self.cs.borrow_mut().unwrap().num_constraints += 1;
415 }
416 Ok(())
417 }
418
419 /// Outputs the bit `self == other`.
420 ///
421 /// This requires two constraints.
422 #[tracing::instrument(target = "r1cs")]
423 pub fn is_eq(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
424 Ok(!self.is_neq(other)?)
425 }
426
427 /// Outputs the bit `self != other`.
428 ///
429 /// This requires two constraints.
430 #[tracing::instrument(target = "r1cs")]
431 pub fn is_neq(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
432 // We don't need to enforce `is_not_equal` to be boolean here;
433 // see the comments above the constraints below for why.
434 let is_not_equal = Boolean::from(AllocatedBool::new_witness_without_booleanity_check(
435 self.cs.clone(),
436 || Ok(self.value.get()? != other.value.get()?),
437 )?);
438 let multiplier = self.cs.new_witness_variable(|| {
439 if is_not_equal.value()? {
440 (self.value.get()? - other.value.get()?).inverse().get()
441 } else {
442 Ok(F::one())
443 }
444 })?;
445
446 // Completeness:
447 // Case 1: self != other:
448 // ----------------------
449 // constraint 1:
450 // (self - other) * multiplier = is_not_equal
451 // => (non_zero) * multiplier = 1 (satisfied, because multiplier = 1/(self -
452 // other)
453 //
454 // constraint 2:
455 // (self - other) * not(is_not_equal) = 0
456 // => (non_zero) * not(1) = 0
457 // => (non_zero) * 0 = 0
458 //
459 // Case 2: self == other:
460 // ----------------------
461 // constraint 1:
462 // (self - other) * multiplier = is_not_equal
463 // => 0 * multiplier = 0 (satisfied, because multiplier = 1
464 //
465 // constraint 2:
466 // (self - other) * not(is_not_equal) = 0
467 // => 0 * not(0) = 0
468 // => 0 * 1 = 0
469 //
470 // --------------------------------------------------------------------
471 //
472 // Soundness:
473 // Case 1: self != other, but is_not_equal != 1.
474 // --------------------------------------------
475 // constraint 2:
476 // (self - other) * not(is_not_equal) = 0
477 // => (non_zero) * (1 - is_not_equal) = 0
478 // => non_zero = 0 (contradiction) || 1 - is_not_equal = 0 (contradiction)
479 //
480 // Case 2: self == other, but is_not_equal != 0.
481 // --------------------------------------------
482 // constraint 1:
483 // (self - other) * multiplier = is_not_equal
484 // 0 * multiplier = is_not_equal != 0 (unsatisfiable)
485 //
486 // That is, constraint 1 enforces that if self == other, then `is_not_equal = 0`
487 // and constraint 2 enforces that if self != other, then `is_not_equal = 1`.
488 // Since these are the only possible two cases, `is_not_equal` is always
489 // constrained to 0 or 1.
490 if self.enable_lc {
491 self.cs.enforce_constraint(
492 lc!() + self.variable - other.variable,
493 lc!() + multiplier,
494 is_not_equal.lc(),
495 )?;
496 self.cs.enforce_constraint(
497 lc!() + self.variable - other.variable,
498 (!&is_not_equal).lc(),
499 lc!(),
500 )?;
501 } else {
502 self.cs.borrow_mut().unwrap().num_constraints += 2;
503 }
504 Ok(is_not_equal)
505 }
506
507 /// Enforces that self == other if `should_enforce.is_eq(&Boolean::TRUE)`.
508 ///
509 /// This requires one constraint.
510 #[tracing::instrument(target = "r1cs")]
511 pub fn conditional_enforce_equal(
512 &self,
513 other: &Self,
514 should_enforce: &Boolean<F>,
515 ) -> Result<(), SynthesisError> {
516 if self.enable_lc {
517 self.cs.enforce_constraint(
518 lc!() + self.variable - other.variable,
519 lc!() + should_enforce.lc(),
520 lc!(),
521 )?;
522 } else {
523 self.cs.borrow_mut().unwrap().num_constraints += 1;
524 }
525 Ok(())
526 }
527
528 /// Enforces that self != other if `should_enforce.is_eq(&Boolean::TRUE)`.
529 ///
530 /// This requires one constraint.
531 #[tracing::instrument(target = "r1cs")]
532 pub fn conditional_enforce_not_equal(
533 &self,
534 other: &Self,
535 should_enforce: &Boolean<F>,
536 ) -> Result<(), SynthesisError> {
537 // The high level logic is as follows:
538 // We want to check that self - other != 0. We do this by checking that
539 // (self - other).inverse() exists. In more detail, we check the following:
540 // If `should_enforce == true`, then we set `multiplier = (self -
541 // other).inverse()`, and check that (self - other) * multiplier == 1.
542 // (i.e., that the inverse exists)
543 //
544 // If `should_enforce == false`, then we set `multiplier == 0`, and check that
545 // (self - other) * 0 == 0, which is always satisfied.
546 let multiplier = Self::new_witness(self.cs.clone(), || {
547 if should_enforce.value()? {
548 (self.value.get()? - other.value.get()?).inverse().get()
549 } else {
550 Ok(F::zero())
551 }
552 })?;
553
554 if self.enable_lc {
555 self.cs.enforce_constraint(
556 lc!() + self.variable - other.variable,
557 lc!() + multiplier.variable,
558 should_enforce.lc(),
559 )?;
560 } else {
561 self.cs.borrow_mut().unwrap().num_constraints += 1;
562 }
563
564 Ok(())
565 }
566}
567
568/// *************************************************************************
569/// *************************************************************************
570
571impl<F: PrimeField> ToBitsGadget<F> for AllocatedFp<F> {
572 /// Outputs the unique bit-wise decomposition of `self` in *little-endian*
573 /// form.
574 ///
575 /// This method enforces that the output is in the field, i.e.
576 /// it invokes `Boolean::enforce_in_field_le` on the bit decomposition.
577 #[tracing::instrument(target = "r1cs")]
578 fn to_bits_le(&self) -> Result<Vec<Boolean<F>>, SynthesisError> {
579 let bits = self.to_non_unique_bits_le()?;
580 Boolean::enforce_in_field_le(&bits)?;
581 Ok(bits)
582 }
583
584 #[tracing::instrument(target = "r1cs")]
585 fn to_non_unique_bits_le(&self) -> Result<Vec<Boolean<F>>, SynthesisError> {
586 let cs = self.cs.clone();
587 use ark_ff::BitIteratorBE;
588 let mut bits = if let Some(value) = self.value {
589 let field_char = BitIteratorBE::new(F::characteristic());
590 let bits: Vec<_> = BitIteratorBE::new(value.into_bigint())
591 .zip(field_char)
592 .skip_while(|(_, c)| !c)
593 .map(|(b, _)| Some(b))
594 .collect();
595 assert_eq!(bits.len(), F::MODULUS_BIT_SIZE as usize);
596 bits
597 } else {
598 vec![None; F::MODULUS_BIT_SIZE as usize]
599 };
600
601 // Convert to little-endian
602 bits.reverse();
603
604 let bits: Vec<_> = bits
605 .into_iter()
606 .map(|b| Boolean::new_witness(cs.clone(), || b.get()))
607 .collect::<Result<_, _>>()?;
608
609 let mut lc = LinearCombination::zero();
610 let mut coeff = F::one();
611
612 for bit in bits.iter() {
613 if self.enable_lc {
614 lc = &lc + bit.lc() * coeff;
615 }
616
617 coeff.double_in_place();
618 }
619
620 if self.enable_lc {
621 lc = lc - &self.variable;
622
623 cs.enforce_constraint(lc!(), lc!(), lc)?;
624 } else {
625 self.cs.borrow_mut().unwrap().num_constraints += 1;
626 }
627
628 Ok(bits)
629 }
630}
631
632impl<F: PrimeField> ToBytesGadget<F> for AllocatedFp<F> {
633 /// Outputs the unique byte decomposition of `self` in *little-endian*
634 /// form.
635 ///
636 /// This method enforces that the decomposition represents
637 /// an integer that is less than `F::MODULUS`.
638 #[tracing::instrument(target = "r1cs")]
639 fn to_bytes_le(&self) -> Result<Vec<UInt8<F>>, SynthesisError> {
640 let num_bits = F::BigInt::NUM_LIMBS * 64;
641 let mut bits = self.to_bits_le()?;
642 let remainder = core::iter::repeat(Boolean::FALSE).take(num_bits - bits.len());
643 bits.extend(remainder);
644 let bytes = bits
645 .chunks(8)
646 .map(|chunk| UInt8::from_bits_le(chunk))
647 .collect();
648 Ok(bytes)
649 }
650
651 #[tracing::instrument(target = "r1cs")]
652 fn to_non_unique_bytes_le(&self) -> Result<Vec<UInt8<F>>, SynthesisError> {
653 let num_bits = F::BigInt::NUM_LIMBS * 64;
654 let mut bits = self.to_non_unique_bits_le()?;
655 let remainder = core::iter::repeat(Boolean::FALSE).take(num_bits - bits.len());
656 bits.extend(remainder);
657 let bytes = bits
658 .chunks(8)
659 .map(|chunk| UInt8::from_bits_le(chunk))
660 .collect();
661 Ok(bytes)
662 }
663}
664
665impl<F: PrimeField> ToConstraintFieldGadget<F> for AllocatedFp<F> {
666 #[tracing::instrument(target = "r1cs")]
667 fn to_constraint_field(&self) -> Result<Vec<FpVar<F>>, SynthesisError> {
668 Ok(vec![self.clone().into()])
669 }
670}
671
672impl<F: PrimeField> CondSelectGadget<F> for AllocatedFp<F> {
673 #[inline]
674 #[tracing::instrument(target = "r1cs")]
675 fn conditionally_select(
676 cond: &Boolean<F>,
677 true_val: &Self,
678 false_val: &Self,
679 ) -> Result<Self, SynthesisError> {
680 match cond {
681 Boolean::Constant(true) => Ok(true_val.clone()),
682 Boolean::Constant(false) => Ok(false_val.clone()),
683 _ => {
684 let cs = cond.cs();
685 let result = Self::new_witness(cs.clone(), || {
686 cond.value()
687 .and_then(|c| if c { true_val } else { false_val }.value.get())
688 })?;
689 // a = self; b = other; c = cond;
690 //
691 // r = c * a + (1 - c) * b
692 // r = b + c * (a - b)
693 // c * (a - b) = r - b
694 if cs.should_construct_matrices() {
695 cs.enforce_constraint(
696 cond.lc(),
697 lc!() + true_val.variable - false_val.variable,
698 lc!() + result.variable - false_val.variable,
699 )?;
700 } else {
701 cs.borrow_mut().unwrap().num_constraints += 1;
702 }
703
704 Ok(result)
705 },
706 }
707 }
708}
709
710/// Uses two bits to perform a lookup into a table
711/// `b` is little-endian: `b[0]` is LSB.
712impl<F: PrimeField> TwoBitLookupGadget<F> for AllocatedFp<F> {
713 type TableConstant = F;
714 #[tracing::instrument(target = "r1cs")]
715 fn two_bit_lookup(b: &[Boolean<F>], c: &[Self::TableConstant]) -> Result<Self, SynthesisError> {
716 debug_assert_eq!(b.len(), 2);
717 debug_assert_eq!(c.len(), 4);
718 let cs = b.cs();
719 let result = Self::new_witness(cs.clone(), || {
720 let lsb = usize::from(b[0].value()?);
721 let msb = usize::from(b[1].value()?);
722 let index = lsb + (msb << 1);
723 Ok(c[index])
724 })?;
725 let one = Variable::One;
726 if cs.should_construct_matrices() {
727 cs.enforce_constraint(
728 lc!() + b[1].lc() * (c[3] - &c[2] - &c[1] + &c[0]) + (c[1] - &c[0], one),
729 lc!() + b[0].lc(),
730 lc!() + result.variable - (c[0], one) + b[1].lc() * (c[0] - &c[2]),
731 )?;
732 } else {
733 cs.borrow_mut().unwrap().num_constraints += 1;
734 }
735
736 Ok(result)
737 }
738}
739
740impl<F: PrimeField> ThreeBitCondNegLookupGadget<F> for AllocatedFp<F> {
741 type TableConstant = F;
742
743 #[tracing::instrument(target = "r1cs")]
744 fn three_bit_cond_neg_lookup(
745 b: &[Boolean<F>],
746 b0b1: &Boolean<F>,
747 c: &[Self::TableConstant],
748 ) -> Result<Self, SynthesisError> {
749 debug_assert_eq!(b.len(), 3);
750 debug_assert_eq!(c.len(), 4);
751 let cs = b.cs();
752 let result = Self::new_witness(cs.clone(), || {
753 let lsb = usize::from(b[0].value()?);
754 let msb = usize::from(b[1].value()?);
755 let index = lsb + (msb << 1);
756 let intermediate = c[index];
757
758 let is_negative = b[2].value()?;
759 let y = if is_negative {
760 -intermediate
761 } else {
762 intermediate
763 };
764 Ok(y)
765 })?;
766
767 if cs.should_construct_matrices() {
768 let y_lc = b0b1.lc() * (c[3] - &c[2] - &c[1] + &c[0])
769 + b[0].lc() * (c[1] - &c[0])
770 + b[1].lc() * (c[2] - &c[0])
771 + (c[0], Variable::One);
772 // enforce y * (1 - 2 * b_2) == res
773 cs.enforce_constraint(
774 y_lc.clone(),
775 b[2].lc() * F::from(2u64).neg() + (F::one(), Variable::One),
776 lc!() + result.variable,
777 )?;
778 } else {
779 cs.borrow_mut().unwrap().num_constraints += 1;
780 }
781
782 Ok(result)
783 }
784}
785
786impl<F: PrimeField> AllocVar<F, F> for AllocatedFp<F> {
787 fn new_variable<T: Borrow<F>>(
788 cs: impl Into<Namespace<F>>,
789 f: impl FnOnce() -> Result<T, SynthesisError>,
790 mode: AllocationMode,
791 ) -> Result<Self, SynthesisError> {
792 let ns = cs.into();
793 let cs = ns.cs();
794 if mode == AllocationMode::Constant {
795 let v = *f()?.borrow();
796 let lc = cs.new_lc(if cs.should_construct_matrices() {
797 lc!() + (v, Variable::One)
798 } else {
799 lc!()
800 })?;
801 Ok(Self::new(Some(v), lc, cs))
802 } else {
803 let mut value = None;
804 let value_generator = || {
805 value = Some(*f()?.borrow());
806 value.ok_or(SynthesisError::AssignmentMissing)
807 };
808 let variable = match mode {
809 AllocationMode::Input => cs.new_input_variable(value_generator)?,
810 AllocationMode::Witness => cs.new_witness_variable(value_generator)?,
811 AllocationMode::Committed => cs.new_committed_variable(value_generator)?,
812 _ => unreachable!(),
813 };
814 Ok(Self::new(value, variable, cs))
815 }
816 }
817}
818
819impl<F: PrimeField> FieldVar<F, F> for FpVar<F> {
820 fn constant(f: F) -> Self {
821 Self::Constant(f)
822 }
823
824 fn zero() -> Self {
825 Self::Constant(F::zero())
826 }
827
828 fn one() -> Self {
829 Self::Constant(F::one())
830 }
831
832 #[tracing::instrument(target = "r1cs")]
833 fn double(&self) -> Result<Self, SynthesisError> {
834 match self {
835 Self::Constant(c) => Ok(Self::Constant(c.double())),
836 Self::Var(v) => Ok(Self::Var(v.double()?)),
837 }
838 }
839
840 #[tracing::instrument(target = "r1cs")]
841 fn negate(&self) -> Result<Self, SynthesisError> {
842 match self {
843 Self::Constant(c) => Ok(Self::Constant(-*c)),
844 Self::Var(v) => Ok(Self::Var(v.negate())),
845 }
846 }
847
848 #[tracing::instrument(target = "r1cs")]
849 fn square(&self) -> Result<Self, SynthesisError> {
850 match self {
851 Self::Constant(c) => Ok(Self::Constant(c.square())),
852 Self::Var(v) => Ok(Self::Var(v.square()?)),
853 }
854 }
855
856 /// Enforce that `self * other == result`.
857 #[tracing::instrument(target = "r1cs")]
858 fn mul_equals(&self, other: &Self, result: &Self) -> Result<(), SynthesisError> {
859 use FpVar::*;
860 match (self, other, result) {
861 (Constant(_), Constant(_), Constant(_)) => Ok(()),
862 (Constant(_), Constant(_), _) | (Constant(_), Var(_), _) | (Var(_), Constant(_), _) => {
863 result.enforce_equal(&(self * other))
864 }, // this multiplication should be free
865 (Var(v1), Var(v2), Var(v3)) => v1.mul_equals(v2, v3),
866 (Var(v1), Var(v2), Constant(f)) => {
867 let cs = v1.cs.clone();
868 let v3 = AllocatedFp::new_constant(cs, f).unwrap();
869 v1.mul_equals(v2, &v3)
870 },
871 }
872 }
873
874 /// Enforce that `self * self == result`.
875 #[tracing::instrument(target = "r1cs")]
876 fn square_equals(&self, result: &Self) -> Result<(), SynthesisError> {
877 use FpVar::*;
878 match (self, result) {
879 (Constant(_), Constant(_)) => Ok(()),
880 (Constant(f), Var(r)) => {
881 let cs = r.cs.clone();
882 let v = AllocatedFp::new_witness(cs, || Ok(f))?;
883 v.square_equals(&r)
884 },
885 (Var(v), Constant(f)) => {
886 let cs = v.cs.clone();
887 let r = AllocatedFp::new_witness(cs, || Ok(f))?;
888 v.square_equals(&r)
889 },
890 (Var(v1), Var(v2)) => v1.square_equals(v2),
891 }
892 }
893
894 #[tracing::instrument(target = "r1cs")]
895 fn inverse(&self) -> Result<Self, SynthesisError> {
896 match self {
897 FpVar::Var(v) => v.inverse().map(FpVar::Var),
898 FpVar::Constant(f) => f.inverse().get().map(FpVar::Constant),
899 }
900 }
901
902 #[tracing::instrument(target = "r1cs")]
903 fn frobenius_map(&self, power: usize) -> Result<Self, SynthesisError> {
904 match self {
905 FpVar::Var(v) => v.frobenius_map(power).map(FpVar::Var),
906 FpVar::Constant(f) => {
907 let mut f = *f;
908 f.frobenius_map_in_place(power);
909 Ok(FpVar::Constant(f))
910 },
911 }
912 }
913
914 #[tracing::instrument(target = "r1cs")]
915 fn frobenius_map_in_place(&mut self, power: usize) -> Result<&mut Self, SynthesisError> {
916 *self = self.frobenius_map(power)?;
917 Ok(self)
918 }
919}
920
921impl_ops!(
922 FpVar<F>,
923 F,
924 Add,
925 add,
926 AddAssign,
927 add_assign,
928 |this: &'a FpVar<F>, other: &'a FpVar<F>| {
929 use FpVar::*;
930 match (this, other) {
931 (Constant(c1), Constant(c2)) => Constant(*c1 + *c2),
932 (Constant(c), Var(v)) | (Var(v), Constant(c)) => Var(v.add_constant(*c)),
933 (Var(v1), Var(v2)) => Var(v1.add(v2)),
934 }
935 },
936 |this: &'a FpVar<F>, other: F| { this + &FpVar::Constant(other) },
937 F: PrimeField,
938);
939
940impl_ops!(
941 FpVar<F>,
942 F,
943 Sub,
944 sub,
945 SubAssign,
946 sub_assign,
947 |this: &'a FpVar<F>, other: &'a FpVar<F>| {
948 use FpVar::*;
949 match (this, other) {
950 (Constant(c1), Constant(c2)) => Constant(*c1 - *c2),
951 (Var(v), Constant(c)) => Var(v.sub_constant(*c)),
952 (Constant(c), Var(v)) => Var(v.sub_constant(*c).negate()),
953 (Var(v1), Var(v2)) => Var(v1.sub(v2)),
954 }
955 },
956 |this: &'a FpVar<F>, other: F| { this - &FpVar::Constant(other) },
957 F: PrimeField
958);
959
960impl_ops!(
961 FpVar<F>,
962 F,
963 Mul,
964 mul,
965 MulAssign,
966 mul_assign,
967 |this: &'a FpVar<F>, other: &'a FpVar<F>| {
968 use FpVar::*;
969 match (this, other) {
970 (Constant(c1), Constant(c2)) => Constant(*c1 * *c2),
971 (Constant(c), Var(v)) | (Var(v), Constant(c)) => Var(v.mul_constant(*c)),
972 (Var(v1), Var(v2)) => Var(v1.mul(v2)),
973 }
974 },
975 |this: &'a FpVar<F>, other: F| {
976 if other.is_zero() {
977 FpVar::zero()
978 } else {
979 this * &FpVar::Constant(other)
980 }
981 },
982 F: PrimeField
983);
984
985/// *************************************************************************
986/// *************************************************************************
987
988impl<F: PrimeField> EqGadget<F> for FpVar<F> {
989 #[tracing::instrument(target = "r1cs")]
990 fn is_eq(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
991 match (self, other) {
992 (Self::Constant(c1), Self::Constant(c2)) => Ok(Boolean::Constant(c1 == c2)),
993 (Self::Constant(c), Self::Var(v)) | (Self::Var(v), Self::Constant(c)) => {
994 let cs = v.cs.clone();
995 let c = AllocatedFp::new_constant(cs, c)?;
996 c.is_eq(v)
997 },
998 (Self::Var(v1), Self::Var(v2)) => v1.is_eq(v2),
999 }
1000 }
1001
1002 #[tracing::instrument(target = "r1cs")]
1003 fn conditional_enforce_equal(
1004 &self,
1005 other: &Self,
1006 should_enforce: &Boolean<F>,
1007 ) -> Result<(), SynthesisError> {
1008 match (self, other) {
1009 (Self::Constant(_), Self::Constant(_)) => Ok(()),
1010 (Self::Constant(c), Self::Var(v)) | (Self::Var(v), Self::Constant(c)) => {
1011 let cs = v.cs.clone();
1012 let c = AllocatedFp::new_constant(cs, c)?;
1013 c.conditional_enforce_equal(v, should_enforce)
1014 },
1015 (Self::Var(v1), Self::Var(v2)) => v1.conditional_enforce_equal(v2, should_enforce),
1016 }
1017 }
1018
1019 #[tracing::instrument(target = "r1cs")]
1020 fn conditional_enforce_not_equal(
1021 &self,
1022 other: &Self,
1023 should_enforce: &Boolean<F>,
1024 ) -> Result<(), SynthesisError> {
1025 match (self, other) {
1026 (Self::Constant(_), Self::Constant(_)) => Ok(()),
1027 (Self::Constant(c), Self::Var(v)) | (Self::Var(v), Self::Constant(c)) => {
1028 let cs = v.cs.clone();
1029 let c = AllocatedFp::new_constant(cs, c)?;
1030 c.conditional_enforce_not_equal(v, should_enforce)
1031 },
1032 (Self::Var(v1), Self::Var(v2)) => v1.conditional_enforce_not_equal(v2, should_enforce),
1033 }
1034 }
1035}
1036
1037impl<F: PrimeField> ToBitsGadget<F> for FpVar<F> {
1038 #[tracing::instrument(target = "r1cs")]
1039 fn to_bits_le(&self) -> Result<Vec<Boolean<F>>, SynthesisError> {
1040 match self {
1041 Self::Constant(_) => self.to_non_unique_bits_le(),
1042 Self::Var(v) => v.to_bits_le(),
1043 }
1044 }
1045
1046 #[tracing::instrument(target = "r1cs")]
1047 fn to_non_unique_bits_le(&self) -> Result<Vec<Boolean<F>>, SynthesisError> {
1048 use ark_ff::BitIteratorLE;
1049 match self {
1050 Self::Constant(c) => Ok(BitIteratorLE::new(&c.into_bigint())
1051 .take((F::MODULUS_BIT_SIZE) as usize)
1052 .map(Boolean::constant)
1053 .collect::<Vec<_>>()),
1054 Self::Var(v) => v.to_non_unique_bits_le(),
1055 }
1056 }
1057}
1058
1059impl<F: PrimeField> ToBytesGadget<F> for FpVar<F> {
1060 /// Outputs the unique byte decomposition of `self` in *little-endian*
1061 /// form.
1062 #[tracing::instrument(target = "r1cs")]
1063 fn to_bytes_le(&self) -> Result<Vec<UInt8<F>>, SynthesisError> {
1064 match self {
1065 Self::Constant(c) => Ok(UInt8::constant_vec(
1066 c.into_bigint().to_bytes_le().as_slice(),
1067 )),
1068 Self::Var(v) => v.to_bytes_le(),
1069 }
1070 }
1071
1072 #[tracing::instrument(target = "r1cs")]
1073 fn to_non_unique_bytes_le(&self) -> Result<Vec<UInt8<F>>, SynthesisError> {
1074 match self {
1075 Self::Constant(c) => Ok(UInt8::constant_vec(
1076 c.into_bigint().to_bytes_le().as_slice(),
1077 )),
1078 Self::Var(v) => v.to_non_unique_bytes_le(),
1079 }
1080 }
1081}
1082
1083impl<F: PrimeField> ToConstraintFieldGadget<F> for FpVar<F> {
1084 #[tracing::instrument(target = "r1cs")]
1085 fn to_constraint_field(&self) -> Result<Vec<FpVar<F>>, SynthesisError> {
1086 Ok(vec![self.clone()])
1087 }
1088}
1089
1090impl<F: PrimeField> CondSelectGadget<F> for FpVar<F> {
1091 #[tracing::instrument(target = "r1cs")]
1092 fn conditionally_select(
1093 cond: &Boolean<F>,
1094 true_value: &Self,
1095 false_value: &Self,
1096 ) -> Result<Self, SynthesisError> {
1097 match cond {
1098 &Boolean::Constant(true) => Ok(true_value.clone()),
1099 &Boolean::Constant(false) => Ok(false_value.clone()),
1100 _ => {
1101 match (true_value, false_value) {
1102 (Self::Constant(t), Self::Constant(f)) => {
1103 let is = AllocatedFp::from(cond.clone());
1104 let not = AllocatedFp::from(!cond);
1105 // cond * t + (1 - cond) * f
1106 Ok(is.mul_constant(*t).add(¬.mul_constant(*f)).into())
1107 },
1108 (..) => {
1109 let cs = cond.cs();
1110 let true_value = match true_value {
1111 Self::Constant(f) => AllocatedFp::new_constant(cs.clone(), f)?,
1112 Self::Var(v) => v.clone(),
1113 };
1114 let false_value = match false_value {
1115 Self::Constant(f) => AllocatedFp::new_constant(cs, f)?,
1116 Self::Var(v) => v.clone(),
1117 };
1118 cond.select(&true_value, &false_value).map(Self::Var)
1119 },
1120 }
1121 },
1122 }
1123 }
1124}
1125
1126/// Uses two bits to perform a lookup into a table
1127/// `b` is little-endian: `b[0]` is LSB.
1128impl<F: PrimeField> TwoBitLookupGadget<F> for FpVar<F> {
1129 type TableConstant = F;
1130
1131 #[tracing::instrument(target = "r1cs")]
1132 fn two_bit_lookup(b: &[Boolean<F>], c: &[Self::TableConstant]) -> Result<Self, SynthesisError> {
1133 debug_assert_eq!(b.len(), 2);
1134 debug_assert_eq!(c.len(), 4);
1135 if b.is_constant() {
1136 let lsb = usize::from(b[0].value()?);
1137 let msb = usize::from(b[1].value()?);
1138 let index = lsb + (msb << 1);
1139 Ok(Self::Constant(c[index]))
1140 } else {
1141 AllocatedFp::two_bit_lookup(b, c).map(Self::Var)
1142 }
1143 }
1144}
1145
1146impl<F: PrimeField> ThreeBitCondNegLookupGadget<F> for FpVar<F> {
1147 type TableConstant = F;
1148
1149 #[tracing::instrument(target = "r1cs")]
1150 fn three_bit_cond_neg_lookup(
1151 b: &[Boolean<F>],
1152 b0b1: &Boolean<F>,
1153 c: &[Self::TableConstant],
1154 ) -> Result<Self, SynthesisError> {
1155 debug_assert_eq!(b.len(), 3);
1156 debug_assert_eq!(c.len(), 4);
1157
1158 if b.cs().or(b0b1.cs()).is_none() {
1159 // We only have constants
1160
1161 let lsb = usize::from(b[0].value()?);
1162 let msb = usize::from(b[1].value()?);
1163 let index = lsb + (msb << 1);
1164 let intermediate = c[index];
1165
1166 let is_negative = b[2].value()?;
1167 let y = if is_negative {
1168 -intermediate
1169 } else {
1170 intermediate
1171 };
1172 Ok(Self::Constant(y))
1173 } else {
1174 AllocatedFp::three_bit_cond_neg_lookup(b, b0b1, c).map(Self::Var)
1175 }
1176 }
1177}
1178
1179impl<F: PrimeField> AllocVar<F, F> for FpVar<F> {
1180 fn new_variable<T: Borrow<F>>(
1181 cs: impl Into<Namespace<F>>,
1182 f: impl FnOnce() -> Result<T, SynthesisError>,
1183 mode: AllocationMode,
1184 ) -> Result<Self, SynthesisError> {
1185 if mode == AllocationMode::Constant {
1186 Ok(Self::Constant(*f()?.borrow()))
1187 } else {
1188 AllocatedFp::new_variable(cs, f, mode).map(Self::Var)
1189 }
1190 }
1191}
1192
1193impl<'a, F: PrimeField> Sum<&'a FpVar<F>> for FpVar<F> {
1194 fn sum<I: Iterator<Item = &'a FpVar<F>>>(iter: I) -> FpVar<F> {
1195 let mut sum_constants = F::zero();
1196 let sum_variables = FpVar::Var(AllocatedFp::<F>::add_many(iter.filter_map(|x| match x {
1197 FpVar::Constant(c) => {
1198 sum_constants += c;
1199 None
1200 },
1201 FpVar::Var(v) => Some(v),
1202 })));
1203
1204 let sum = sum_variables + sum_constants;
1205 sum
1206 }
1207}
1208
1209impl<'a, F: PrimeField> Sum<FpVar<F>> for FpVar<F> {
1210 fn sum<I: Iterator<Item = FpVar<F>>>(iter: I) -> FpVar<F> {
1211 let mut sum_constants = F::zero();
1212 let sum_variables = FpVar::Var(AllocatedFp::<F>::add_many(iter.filter_map(|x| match x {
1213 FpVar::Constant(c) => {
1214 sum_constants += c;
1215 None
1216 },
1217 FpVar::Var(v) => Some(v),
1218 })));
1219
1220 let sum = sum_variables + sum_constants;
1221 sum
1222 }
1223}
1224
1225#[cfg(test)]
1226mod test {
1227 use crate::{
1228 alloc::{AllocVar, AllocationMode},
1229 eq::EqGadget,
1230 fields::fp::FpVar,
1231 R1CSVar,
1232 };
1233 use ark_relations::r1cs::ConstraintSystem;
1234 use ark_std::{UniformRand, Zero};
1235 use ark_test_curves::bls12_381::Fr;
1236
1237 #[test]
1238 fn test_sum_fpvar() {
1239 let mut rng = ark_std::test_rng();
1240 let cs = ConstraintSystem::new_ref();
1241
1242 let mut sum_expected = Fr::zero();
1243
1244 let mut v = Vec::new();
1245 for _ in 0..10 {
1246 let a = Fr::rand(&mut rng);
1247 sum_expected += &a;
1248 v.push(
1249 FpVar::<Fr>::new_variable(cs.clone(), || Ok(a), AllocationMode::Constant).unwrap(),
1250 );
1251 }
1252 for _ in 0..10 {
1253 let a = Fr::rand(&mut rng);
1254 sum_expected += &a;
1255 v.push(
1256 FpVar::<Fr>::new_variable(cs.clone(), || Ok(a), AllocationMode::Witness).unwrap(),
1257 );
1258 }
1259
1260 let sum: FpVar<Fr> = v.iter().sum();
1261
1262 sum.enforce_equal(&FpVar::Constant(sum_expected)).unwrap();
1263
1264 assert!(cs.is_satisfied().unwrap());
1265 assert_eq!(sum.value().unwrap(), sum_expected);
1266 }
1267}