sonobe/folding-schemes/src/folding/circuits/nonnative/uint.rs
folding-schemes/src/folding/circuits/nonnative/uint.rsRaw
1use std::{
2 borrow::Borrow,
3 cmp::{max, min},
4};
5
6use ark_ff::{BigInteger, Field, One, PrimeField, Zero};
7use ark_r1cs_std::{
8 alloc::{AllocVar, AllocationMode},
9 boolean::Boolean,
10 fields::{fp::FpVar, FieldVar},
11 prelude::EqGadget,
12 select::CondSelectGadget,
13 R1CSVar, ToBitsGadget, ToConstraintFieldGadget,
14};
15use ark_relations::r1cs::{ConstraintSystemRef, Namespace, SynthesisError};
16use num_bigint::BigUint;
17use num_integer::Integer;
18
19use crate::{
20 transcript::{AbsorbNonNative, AbsorbNonNativeGadget},
21 utils::gadgets::{MatrixGadget, SparseMatrixVar, VectorGadget},
22};
23
24/// `LimbVar` represents a single limb of a non-native unsigned integer in the
25/// circuit.
26/// The limb value `v` should be small enough to fit into `FpVar`, and we also
27/// store an upper bound `ub` for the limb value, which is treated as a constant
28/// in the circuit and is used for efficient equality checks and some arithmetic
29/// operations.
30#[derive(Debug, Clone)]
31pub struct LimbVar<F: PrimeField> {
32 pub v: FpVar<F>,
33 pub ub: BigUint,
34}
35
36impl<F: PrimeField, B: AsRef<[Boolean<F>]>> From<B> for LimbVar<F> {
37 fn from(bits: B) -> Self {
38 Self {
39 v: Boolean::le_bits_to_fp_var(bits.as_ref()).unwrap(),
40 ub: (BigUint::one() << bits.as_ref().len()) - BigUint::one(),
41 }
42 }
43}
44
45impl<F: PrimeField> Default for LimbVar<F> {
46 fn default() -> Self {
47 Self {
48 v: FpVar::zero(),
49 ub: BigUint::zero(),
50 }
51 }
52}
53
54impl<F: PrimeField> R1CSVar<F> for LimbVar<F> {
55 type Value = F;
56
57 fn cs(&self) -> ConstraintSystemRef<F> {
58 self.v.cs()
59 }
60
61 fn value(&self) -> Result<Self::Value, SynthesisError> {
62 self.v.value()
63 }
64}
65
66impl<F: PrimeField> CondSelectGadget<F> for LimbVar<F> {
67 fn conditionally_select(
68 cond: &Boolean<F>,
69 true_value: &Self,
70 false_value: &Self,
71 ) -> Result<Self, SynthesisError> {
72 // We only allow selecting between two values with the same upper bound
73 assert_eq!(true_value.ub, false_value.ub);
74 Ok(Self {
75 v: cond.select(&true_value.v, &false_value.v)?,
76 ub: true_value.ub.clone(),
77 })
78 }
79}
80
81impl<F: PrimeField> LimbVar<F> {
82 /// Add two `LimbVar`s.
83 /// Returns `None` if the upper bound of the sum is too large, i.e.,
84 /// greater than `F::MODULUS_MINUS_ONE_DIV_TWO`.
85 /// Otherwise, returns the sum as a `LimbVar`.
86 pub fn add(&self, other: &Self) -> Option<Self> {
87 let ubound = &self.ub + &other.ub;
88 if ubound < F::MODULUS_MINUS_ONE_DIV_TWO.into() {
89 Some(Self {
90 v: &self.v + &other.v,
91 ub: ubound,
92 })
93 } else {
94 None
95 }
96 }
97
98 /// Add multiple `LimbVar`s.
99 /// Returns `None` if the upper bound of the sum is too large, i.e.,
100 /// greater than `F::MODULUS_MINUS_ONE_DIV_TWO`.
101 /// Otherwise, returns the sum as a `LimbVar`.
102 pub fn add_many(limbs: &[Self]) -> Option<Self> {
103 let ubound = limbs.iter().map(|l| &l.ub).sum();
104 if ubound < F::MODULUS_MINUS_ONE_DIV_TWO.into() {
105 Some(Self {
106 v: if limbs.is_constant() {
107 FpVar::constant(limbs.value().unwrap_or_default().into_iter().sum())
108 } else {
109 limbs.iter().map(|l| &l.v).sum()
110 },
111 ub: ubound,
112 })
113 } else {
114 None
115 }
116 }
117
118 /// Multiply two `LimbVar`s.
119 /// Returns `None` if the upper bound of the product is too large, i.e.,
120 /// greater than `F::MODULUS_MINUS_ONE_DIV_TWO`.
121 /// Otherwise, returns the product as a `LimbVar`.
122 pub fn mul(&self, other: &Self) -> Option<Self> {
123 let ubound = &self.ub * &other.ub;
124 if ubound < F::MODULUS_MINUS_ONE_DIV_TWO.into() {
125 Some(Self {
126 v: &self.v * &other.v,
127 ub: ubound,
128 })
129 } else {
130 None
131 }
132 }
133
134 pub fn zero() -> Self {
135 Self::default()
136 }
137
138 pub fn constant(v: F) -> Self {
139 Self {
140 v: FpVar::constant(v),
141 ub: v.into(),
142 }
143 }
144}
145
146impl<F: PrimeField> ToBitsGadget<F> for LimbVar<F> {
147 fn to_bits_le(&self) -> Result<Vec<Boolean<F>>, SynthesisError> {
148 let cs = self.cs();
149
150 let bits = &self
151 .v
152 .value()
153 .unwrap_or_default()
154 .into_bigint()
155 .to_bits_le()[..self.ub.bits() as usize];
156 let bits = if cs.is_none() {
157 Vec::new_constant(cs, bits)?
158 } else {
159 Vec::new_witness(cs, || Ok(bits))?
160 };
161
162 Boolean::le_bits_to_fp_var(&bits)?.enforce_equal(&self.v)?;
163
164 Ok(bits)
165 }
166}
167
168/// `NonNativeUintVar` represents a non-native unsigned integer (BigUint) in the
169/// circuit.
170/// We apply [xJsnark](https://akosba.github.io/papers/xjsnark.pdf)'s techniques
171/// for efficient operations on `NonNativeUintVar`.
172/// Note that `NonNativeUintVar` is different from arkworks' `NonNativeFieldVar`
173/// in that the latter runs the expensive `reduce` (`align` + `modulo` in our
174/// terminology) after each arithmetic operation, while the former only reduces
175/// the integer when explicitly called.
176#[derive(Debug, Clone)]
177pub struct NonNativeUintVar<F: PrimeField>(pub Vec<LimbVar<F>>);
178
179impl<F: PrimeField> NonNativeUintVar<F> {
180 pub const fn bits_per_limb() -> usize {
181 assert!(F::MODULUS_BIT_SIZE > 250);
182 // For a `F` with order > 250 bits, 55 is chosen for optimizing the most
183 // expensive part `Az∘Bz` when checking the R1CS relation for CycleFold.
184 // Consider using `NonNativeUintVar` to represent the base field `Fq`.
185 // Since 250 / 55 = 4.46, the `NonNativeUintVar` has 5 limbs.
186 // Now, the multiplication of two `NonNativeUintVar`s has 9 limbs, and
187 // each limb has at most 2^{55 * 2} * 5 = 112.3 bits.
188 // For a 1400x1400 matrix `A`, the multiplication of `A`'s row and `z`
189 // is the sum of 1400 `NonNativeUintVar`s, each with 9 limbs.
190 // Thus, the maximum bit length of limbs of each element in `Az` is
191 // 2^{55 * 2} * 5 * 1400 = 122.7 bits.
192 // Finally, in the hadamard product of `Az` and `Bz`, every element has
193 // 17 limbs, whose maximum bit length is (2^{55 * 2} * 5 * 1400)^2 * 9
194 // = 248.7 bits and is less than the native field `Fr`.
195 // Thus, 55 allows us to compute `Az∘Bz` without the expensive alignment
196 // operation.
197 //
198 // TODO (@winderica): either make it a global const, or compute an
199 // optimal value based on the modulus size
200 55
201 }
202}
203
204struct BoundedBigUint(BigUint, usize);
205
206impl<F: PrimeField> AllocVar<BoundedBigUint, F> for NonNativeUintVar<F> {
207 fn new_variable<T: Borrow<BoundedBigUint>>(
208 cs: impl Into<Namespace<F>>,
209 f: impl FnOnce() -> Result<T, SynthesisError>,
210 mode: AllocationMode,
211 ) -> Result<Self, SynthesisError> {
212 let cs = cs.into().cs();
213 let v = f()?;
214 let BoundedBigUint(x, l) = v.borrow();
215
216 let mut limbs = vec![];
217 for chunk in (0..*l)
218 .map(|i| x.bit(i as u64))
219 .collect::<Vec<_>>()
220 .chunks(Self::bits_per_limb())
221 {
222 let limb = F::from_bigint(F::BigInt::from_bits_le(chunk)).unwrap();
223 let limb = FpVar::new_variable(cs.clone(), || Ok(limb), mode)?;
224 Self::enforce_bit_length(&limb, chunk.len())?;
225 limbs.push(LimbVar {
226 v: limb,
227 ub: (BigUint::one() << chunk.len()) - BigUint::one(),
228 });
229 }
230
231 Ok(Self(limbs))
232 }
233}
234
235impl<F: PrimeField, G: Field> AllocVar<G, F> for NonNativeUintVar<F> {
236 fn new_variable<T: Borrow<G>>(
237 cs: impl Into<Namespace<F>>,
238 f: impl FnOnce() -> Result<T, SynthesisError>,
239 mode: AllocationMode,
240 ) -> Result<Self, SynthesisError> {
241 let cs = cs.into().cs();
242 let v = f()?;
243 assert_eq!(G::extension_degree(), 1);
244 let v = v.borrow().to_base_prime_field_elements().next().unwrap();
245
246 let mut limbs = vec![];
247
248 for chunk in v.into_bigint().to_bits_le().chunks(Self::bits_per_limb()) {
249 let limb = F::from_bigint(F::BigInt::from_bits_le(chunk)).unwrap();
250 let limb = FpVar::new_variable(cs.clone(), || Ok(limb), mode)?;
251 Self::enforce_bit_length(&limb, chunk.len())?;
252 limbs.push(LimbVar {
253 v: limb,
254 ub: (BigUint::one() << chunk.len()) - BigUint::one(),
255 });
256 }
257
258 Ok(Self(limbs))
259 }
260}
261
262impl<F: PrimeField> NonNativeUintVar<F> {
263 pub fn inputize<T: Field>(x: T) -> Vec<F> {
264 assert_eq!(T::extension_degree(), 1);
265 x.to_base_prime_field_elements()
266 .next()
267 .unwrap()
268 .into_bigint()
269 .to_bits_le()
270 .chunks(Self::bits_per_limb())
271 .map(|chunk| F::from_bigint(F::BigInt::from_bits_le(chunk)).unwrap())
272 .collect()
273 }
274}
275
276impl<F: PrimeField> R1CSVar<F> for NonNativeUintVar<F> {
277 type Value = BigUint;
278
279 fn cs(&self) -> ConstraintSystemRef<F> {
280 self.0.cs()
281 }
282
283 fn value(&self) -> Result<Self::Value, SynthesisError> {
284 let mut r = BigUint::zero();
285
286 for limb in self.0.value()?.into_iter().rev() {
287 r <<= Self::bits_per_limb();
288 r += Into::<BigUint>::into(limb);
289 }
290
291 Ok(r)
292 }
293}
294
295impl<F: PrimeField> NonNativeUintVar<F> {
296 /// Enforce `self` to be less than `other`, where `self` and `other` should
297 /// be aligned.
298 /// Adapted from https://github.com/akosba/jsnark/blob/0955389d0aae986ceb25affc72edf37a59109250/JsnarkCircuitBuilder/src/circuit/auxiliary/LongElement.java#L801-L872
299 pub fn enforce_lt(&self, other: &Self) -> Result<(), SynthesisError> {
300 let len = max(self.0.len(), other.0.len());
301 let zero = LimbVar::zero();
302
303 // Compute the difference between limbs of `other` and `self`.
304 // Denote a positive limb by `+`, a negative limb by `-`, a zero limb by
305 // `0`, and an unknown limb by `?`.
306 // Then, for `self < other`, `delta` should look like:
307 // ? ? ... ? ? + 0 0 ... 0 0
308 let delta = (0..len)
309 .map(|i| {
310 let x = &self.0.get(i).unwrap_or(&zero).v;
311 let y = &other.0.get(i).unwrap_or(&zero).v;
312 y - x
313 })
314 .collect::<Vec<_>>();
315
316 // `helper` is a vector of booleans that indicates if the corresponding
317 // limb of `delta` is the first (searching from MSB) positive limb.
318 // For example, if `delta` is:
319 // - + ... + - + 0 0 ... 0 0
320 // <---- search in this direction --------
321 // Then `helper` should be:
322 // F F ... F F T F F ... F F
323 let helper = {
324 let cs = self.cs().or(other.cs());
325 let mut helper = vec![false; len];
326 for i in (0..len).rev() {
327 let delta = delta[i].value().unwrap_or_default().into_bigint();
328 if !delta.is_zero() && delta < F::MODULUS_MINUS_ONE_DIV_TWO {
329 helper[i] = true;
330 break;
331 }
332 }
333 if cs.is_none() {
334 Vec::<Boolean<F>>::new_constant(cs, helper)?
335 } else {
336 Vec::new_witness(cs, || Ok(helper))?
337 }
338 };
339
340 // `p` is the first positive limb in `delta`.
341 let mut p = FpVar::<F>::zero();
342 // `r` is the sum of all bits in `helper`, which should be 1 when `self`
343 // is less than `other`, as there should be more than one positive limb
344 // in `delta`, and thus exactly one true bit in `helper`.
345 let mut r = FpVar::zero();
346 for (b, d) in helper.into_iter().zip(delta) {
347 // Choose the limb `d` only if `b` is true.
348 p += b.select(&d, &FpVar::zero())?;
349 // Either `r` or `d` should be zero.
350 // Consider the same example as above:
351 // - + ... + - + 0 0 ... 0 0
352 // F F ... F F T F F ... F F
353 // |-----------|
354 // `r = 0` in this range (before/when we meet the first positive limb)
355 // |---------|
356 // `d = 0` in this range (after we meet the first positive limb)
357 // This guarantees that for every bit after the true bit in `helper`,
358 // the corresponding limb in `delta` is zero.
359 (&r * &d).enforce_equal(&FpVar::zero())?;
360 // Add the current bit to `r`.
361 r += FpVar::from(b);
362 }
363
364 // Ensure that `r` is exactly 1. This guarantees that there is exactly
365 // one true value in `helper`.
366 r.enforce_equal(&FpVar::one())?;
367 // Ensure that `p` is positive, i.e.,
368 // `0 <= p - 1 < 2^bits_per_limb < F::MODULUS_MINUS_ONE_DIV_TWO`.
369 // This guarantees that the true value in `helper` corresponds to a
370 // positive limb in `delta`.
371 Self::enforce_bit_length(&(p - FpVar::one()), Self::bits_per_limb())?;
372
373 Ok(())
374 }
375
376 /// Enforce `self` to be equal to `other`, where `self` and `other` are not
377 /// necessarily aligned.
378 ///
379 /// Adapted from https://github.com/akosba/jsnark/blob/0955389d0aae986ceb25affc72edf37a59109250/JsnarkCircuitBuilder/src/circuit/auxiliary/LongElement.java#L562-L798
380 /// Similar implementations can also be found in https://github.com/alex-ozdemir/bellman-bignat/blob/0585b9d90154603a244cba0ac80b9aafe1d57470/src/mp/bignat.rs#L566-L661
381 /// and https://github.com/arkworks-rs/r1cs-std/blob/4020fbc22625621baa8125ede87abaeac3c1ca26/src/fields/emulated_fp/reduce.rs#L201-L323
382 pub fn enforce_equal_unaligned(&self, other: &Self) -> Result<(), SynthesisError> {
383 let len = min(self.0.len(), other.0.len());
384
385 // Group the limbs of `self` and `other` so that each group nearly
386 // reaches the capacity `F::MODULUS_MINUS_ONE_DIV_TWO`.
387 // By saying group, we mean the operation `Σ x_i 2^{i * W}`, where `W`
388 // is the initial number of bits in a limb, just as what we do in grade
389 // school arithmetic, e.g.,
390 // 5 9
391 // x 7 3
392 // -------------
393 // 15 27
394 // 35 63
395 // ------------- <- When grouping 35, 15 + 63, and 27, we are computing
396 // 4 3 0 7 35 * 100 + (15 + 63) * 10 + 27 = 4307
397 // Note that this is different from the concatenation `x_0 || x_1 ...`,
398 // since the bit-length of each limb is not necessarily the initial size
399 // `W`.
400 let (steps, x, y, rest) = {
401 // `steps` stores the size of each grouped limb.
402 let mut steps = vec![];
403 // `x_grouped` stores the grouped limbs of `self`.
404 let mut x_grouped = vec![];
405 // `y_grouped` stores the grouped limbs of `other`.
406 let mut y_grouped = vec![];
407 let mut i = 0;
408 while i < len {
409 let mut j = i;
410 // The current grouped limbs of `self` and `other`.
411 let mut xx = LimbVar::zero();
412 let mut yy = LimbVar::zero();
413 while j < len {
414 let shift = BigUint::one() << (Self::bits_per_limb() * (j - i));
415 assert!(shift < F::MODULUS_MINUS_ONE_DIV_TWO.into());
416 let shift = LimbVar::constant(shift.into());
417 match (
418 // Try to group `x` and `y` into `xx` and `yy`.
419 self.0[j].mul(&shift).and_then(|x| xx.add(&x)),
420 other.0[j].mul(&shift).and_then(|y| yy.add(&y)),
421 ) {
422 // Update the result if successful.
423 (Some(x), Some(y)) => (xx, yy) = (x, y),
424 // Break the loop if the upper bound of the result exceeds
425 // the maximum capacity.
426 _ => break,
427 }
428 j += 1;
429 }
430 // Store the grouped limbs and their size.
431 steps.push((j - i) * Self::bits_per_limb());
432 x_grouped.push(xx);
433 y_grouped.push(yy);
434 // Start the next group
435 i = j;
436 }
437 let remaining_limbs = &(if i < self.0.len() { self } else { other }).0[i..];
438 let rest = if remaining_limbs.is_empty() {
439 FpVar::zero()
440 } else {
441 // If there is any remaining limb, the first one should be the
442 // final carry (which will be checked later), and the following
443 // ones should be zero.
444
445 // Enforce the remaining limbs to be zero.
446 // Instead of doing that one by one, we check if their sum is
447 // zero using a single constraint.
448 // This is sound, as the upper bounds of the limbs and their sum
449 // are guaranteed to be less than `F::MODULUS_MINUS_ONE_DIV_TWO`
450 // (i.e., all of them are "non-negative"), implying that all
451 // limbs should be zero to make the sum zero.
452 LimbVar::add_many(&remaining_limbs[1..])
453 .unwrap()
454 .v
455 .enforce_equal(&FpVar::zero())?;
456 remaining_limbs[0].v.clone()
457 };
458 (steps, x_grouped, y_grouped, rest)
459 };
460 let n = steps.len();
461 // `c` stores the current carry of `x_i - y_i`
462 let mut c = FpVar::<F>::zero();
463 // For each group, check the last `step_i` bits of `x_i` and `y_i` are
464 // equal.
465 // The intuition is to check `diff = x_i - y_i = 0 (mod 2^step_i)`.
466 // However, this is only true for `i = 0`, and we need to consider carry
467 // values `diff >> step_i` for `i > 0`.
468 // Therefore, we actually check `diff = x_i - y_i + c = 0 (mod 2^step_i)`
469 // and derive the next `c` by computing `diff >> step_i`.
470 // To enforce `diff = 0 (mod 2^step_i)`, we compute `diff / 2^step_i`
471 // and enforce it to be small (soundness holds because for `a` that does
472 // not divide `b`, `b / a` in the field will be very large.
473 for i in 0..n {
474 let step = steps[i];
475 c = (&x[i].v - &y[i].v + &c)
476 .mul_by_inverse_unchecked(&FpVar::constant(F::from(BigUint::one() << step)))?;
477 if i != n - 1 {
478 // Unlike the code mentioned above which add some offset to the
479 // diff `x_i - y_i + c` to make it always positive, we directly
480 // check if the absolute value of the diff is small.
481 Self::enforce_abs_bit_length(
482 &c,
483 (max(&x[i].ub, &y[i].ub).bits() as usize)
484 .checked_sub(step)
485 .unwrap_or_default(),
486 )?;
487 } else {
488 // For the final carry, we need to ensure that it equals the
489 // remaining limb `rest`.
490 c.enforce_equal(&rest)?;
491 }
492 }
493
494 Ok(())
495 }
496}
497
498impl<F: PrimeField> ToBitsGadget<F> for NonNativeUintVar<F> {
499 fn to_bits_le(&self) -> Result<Vec<Boolean<F>>, SynthesisError> {
500 Ok(self
501 .0
502 .iter()
503 .map(|limb| limb.to_bits_le())
504 .collect::<Result<Vec<_>, _>>()?
505 .concat())
506 }
507}
508
509impl<F: PrimeField> ToConstraintFieldGadget<F> for NonNativeUintVar<F> {
510 fn to_constraint_field(&self) -> Result<Vec<FpVar<F>>, SynthesisError> {
511 let bits_per_limb = F::MODULUS_BIT_SIZE as usize - 1;
512
513 let limbs = self
514 .to_bits_le()?
515 .chunks(bits_per_limb)
516 .map(Boolean::le_bits_to_fp_var)
517 .collect::<Result<Vec<_>, _>>()?;
518
519 Ok(limbs)
520 }
521}
522
523impl<F: PrimeField> CondSelectGadget<F> for NonNativeUintVar<F> {
524 fn conditionally_select(
525 cond: &Boolean<F>,
526 true_value: &Self,
527 false_value: &Self,
528 ) -> Result<Self, SynthesisError> {
529 assert_eq!(true_value.0.len(), false_value.0.len());
530 let mut v = vec![];
531 for i in 0..true_value.0.len() {
532 v.push(cond.select(&true_value.0[i], &false_value.0[i])?);
533 }
534 Ok(Self(v))
535 }
536}
537
538impl<F: PrimeField> NonNativeUintVar<F> {
539 pub fn ubound(&self) -> BigUint {
540 let mut r = BigUint::zero();
541
542 for i in self.0.iter().rev() {
543 r <<= Self::bits_per_limb();
544 r += &i.ub;
545 }
546
547 r
548 }
549
550 fn enforce_bit_length(x: &FpVar<F>, length: usize) -> Result<Vec<Boolean<F>>, SynthesisError> {
551 let cs = x.cs();
552
553 let bits = &x.value().unwrap_or_default().into_bigint().to_bits_le()[..length];
554 let bits = if cs.is_none() {
555 Vec::new_constant(cs, bits)?
556 } else {
557 Vec::new_witness(cs, || Ok(bits))?
558 };
559
560 Boolean::le_bits_to_fp_var(&bits)?.enforce_equal(x)?;
561
562 Ok(bits)
563 }
564
565 fn enforce_abs_bit_length(
566 x: &FpVar<F>,
567 length: usize,
568 ) -> Result<Vec<Boolean<F>>, SynthesisError> {
569 let cs = x.cs();
570 let mode = if cs.is_none() {
571 AllocationMode::Constant
572 } else {
573 AllocationMode::Witness
574 };
575
576 let is_neg = Boolean::new_variable(
577 cs.clone(),
578 || Ok(x.value().unwrap_or_default().into_bigint() > F::MODULUS_MINUS_ONE_DIV_TWO),
579 mode,
580 )?;
581 let bits = Vec::new_variable(
582 cs.clone(),
583 || {
584 Ok({
585 let x = x.value().unwrap_or_default();
586 let mut bits = if is_neg.value().unwrap_or_default() {
587 -x
588 } else {
589 x
590 }
591 .into_bigint()
592 .to_bits_le();
593 bits.resize(length, false);
594 bits
595 })
596 },
597 mode,
598 )?;
599
600 // Below is equivalent to but more efficient than
601 // `Boolean::le_bits_to_fp_var(&bits)?.enforce_equal(&is_neg.select(&x.negate()?, &x)?)?`
602 // Note that this enforces:
603 // 1. The claimed absolute value `is_neg.select(&x.negate()?, &x)?` has
604 // exactly `length` bits.
605 // 2. `is_neg` is indeed the sign of `x`, i.e., `is_neg = false` when
606 // `0 <= x < (|F| - 1) / 2`, and `is_neg = true` when
607 // `(|F| - 1) / 2 <= x < F`, thus the claimed absolute value is
608 // correct.
609 // If `is_neg` is incorrect, then:
610 // a. `0 <= x < (|F| - 1) / 2`, but `is_neg = true`, then
611 // `is_neg.select(&x.negate()?, &x)?` returns `|F| - x`,
612 // which is greater than `(|F| - 1) / 2` and cannot fit in
613 // `length` bits (given that `length` is small).
614 // b. `(|F| - 1) / 2 <= x < F`, but `is_neg = false`, then
615 // `is_neg.select(&x.negate()?, &x)?` returns `x`, which is
616 // greater than `(|F| - 1) / 2` and cannot fit in `length`
617 // bits.
618 FpVar::from(is_neg).mul_equals(&x.double()?, &(x - Boolean::le_bits_to_fp_var(&bits)?))?;
619
620 Ok(bits)
621 }
622
623 /// Compute `self + other`, without aligning the limbs.
624 pub fn add_no_align(&self, other: &Self) -> Self {
625 let mut z = vec![LimbVar::zero(); max(self.0.len(), other.0.len())];
626 for (i, v) in self.0.iter().enumerate() {
627 z[i] = z[i].add(v).unwrap();
628 }
629 for (i, v) in other.0.iter().enumerate() {
630 z[i] = z[i].add(v).unwrap();
631 }
632 Self(z)
633 }
634
635 /// Compute `self * other`, without aligning the limbs.
636 /// Implements the O(n) approach described in xJsnark, Section IV.B.1)
637 pub fn mul_no_align(&self, other: &Self) -> Result<Self, SynthesisError> {
638 let len = self.0.len() + other.0.len() - 1;
639 if self.is_constant() || other.is_constant() {
640 // Use the naive approach for constant operands, which costs no
641 // constraints.
642 let z = (0..len)
643 .map(|i| {
644 let start = max(i + 1, other.0.len()) - other.0.len();
645 let end = min(i + 1, self.0.len());
646 LimbVar::add_many(
647 &(start..end)
648 .map(|j| self.0[j].mul(&other.0[i - j]))
649 .collect::<Option<Vec<_>>>()?,
650 )
651 })
652 .collect::<Option<Vec<_>>>()
653 .unwrap();
654 return Ok(Self(z));
655 }
656 let cs = self.cs().or(other.cs());
657 let mode = if cs.is_none() {
658 AllocationMode::Constant
659 } else {
660 AllocationMode::Witness
661 };
662
663 // Compute the result `z` outside the circuit and provide it as hints.
664 let z = {
665 let mut z = vec![(F::zero(), BigUint::zero()); len];
666 for i in 0..self.0.len() {
667 for j in 0..other.0.len() {
668 z[i + j].0 += self.0[i].value().unwrap_or_default()
669 * other.0[j].value().unwrap_or_default();
670 z[i + j].1 += &self.0[i].ub * &other.0[j].ub;
671 }
672 }
673 z.into_iter()
674 .map(|(v, ub)| {
675 assert!(ub < F::MODULUS_MINUS_ONE_DIV_TWO.into());
676 Ok(LimbVar {
677 v: FpVar::new_variable(cs.clone(), || Ok(v), mode)?,
678 ub,
679 })
680 })
681 .collect::<Result<Vec<_>, _>>()?
682 };
683 for c in 1..=len {
684 let c = F::from(c as u64);
685 let mut t = F::one();
686 let mut c_powers = vec![];
687 for _ in 0..len {
688 c_powers.push(t);
689 t *= c;
690 }
691 // `l = Σ self[i] c^i`
692 let l = self
693 .0
694 .iter()
695 .zip(&c_powers)
696 .map(|(v, t)| (&v.v * *t))
697 .collect::<Vec<_>>()
698 .iter()
699 .sum::<FpVar<_>>();
700 // `r = Σ other[i] c^i`
701 let r = other
702 .0
703 .iter()
704 .zip(&c_powers)
705 .map(|(v, t)| (&v.v * *t))
706 .collect::<Vec<_>>()
707 .iter()
708 .sum::<FpVar<_>>();
709 // `o = Σ z[i] c^i`
710 let o = z
711 .iter()
712 .zip(&c_powers)
713 .map(|(v, t)| &v.v * *t)
714 .collect::<Vec<_>>()
715 .iter()
716 .sum::<FpVar<_>>();
717 // Enforce `o = l * r`
718 l.mul_equals(&r, &o)?;
719 }
720
721 Ok(Self(z))
722 }
723
724 /// Convert `Self` to an element in `M`, i.e., compute `Self % M::MODULUS`.
725 pub fn modulo<M: PrimeField>(&self) -> Result<Self, SynthesisError> {
726 let cs = self.cs();
727 let mode = if cs.is_none() {
728 AllocationMode::Constant
729 } else {
730 AllocationMode::Witness
731 };
732 let m: BigUint = M::MODULUS.into();
733 // Provide the quotient and remainder as hints
734 let (q, r) = {
735 let v = self.value().unwrap_or_default();
736 let (q, r) = v.div_rem(&m);
737 let q_ubound = self.ubound().div_ceil(&m);
738 let r_ubound = &m;
739 (
740 Self::new_variable(
741 cs.clone(),
742 || Ok(BoundedBigUint(q, q_ubound.bits() as usize)),
743 mode,
744 )?,
745 Self::new_variable(
746 cs.clone(),
747 || Ok(BoundedBigUint(r, r_ubound.bits() as usize)),
748 mode,
749 )?,
750 )
751 };
752
753 let m = Self::new_constant(cs.clone(), BoundedBigUint(m, M::MODULUS_BIT_SIZE as usize))?;
754 // Enforce `self = q * m + r`
755 q.mul_no_align(&m)?
756 .add_no_align(&r)
757 .enforce_equal_unaligned(self)?;
758 // Enforce `r < m` (and `r >= 0` already holds)
759 r.enforce_lt(&m)?;
760
761 Ok(r)
762 }
763
764 /// Enforce that `self` is congruent to `other` modulo `M::MODULUS`.
765 pub fn enforce_congruent<M: PrimeField>(&self, other: &Self) -> Result<(), SynthesisError> {
766 let cs = self.cs();
767 let mode = if cs.is_none() {
768 AllocationMode::Constant
769 } else {
770 AllocationMode::Witness
771 };
772 let m: BigUint = M::MODULUS.into();
773 let bits = (max(self.ubound(), other.ubound()) / &m).bits() as usize;
774 // Provide the quotient `|x - y| / m` and a boolean indicating if `x > y`
775 // as hints.
776 let (q, is_ge) = {
777 let x = self.value().unwrap_or_default();
778 let y = other.value().unwrap_or_default();
779 let (d, b) = if x > y {
780 ((x - y) / &m, true)
781 } else {
782 ((y - x) / &m, false)
783 };
784 (
785 Self::new_variable(cs.clone(), || Ok(BoundedBigUint(d, bits)), mode)?,
786 Boolean::new_variable(cs.clone(), || Ok(b), mode)?,
787 )
788 };
789
790 let zero = Self::new_constant(cs.clone(), BoundedBigUint(BigUint::zero(), bits))?;
791 let m = Self::new_constant(cs.clone(), BoundedBigUint(m, M::MODULUS_BIT_SIZE as usize))?;
792 let l = self.add_no_align(&is_ge.select(&zero, &q)?.mul_no_align(&m)?);
793 let r = other.add_no_align(&is_ge.select(&q, &zero)?.mul_no_align(&m)?);
794 // If `self >= other`, enforce `self = other + q * m`
795 // Otherwise, enforce `self + q * m = other`
796 // Soundness holds because if `self` and `other` are not congruent, then
797 // one can never find a `q` satisfying either equation above.
798 l.enforce_equal_unaligned(&r)
799 }
800}
801
802impl<F: PrimeField, B: AsRef<[Boolean<F>]>> From<B> for NonNativeUintVar<F> {
803 fn from(bits: B) -> Self {
804 Self(
805 bits.as_ref()
806 .chunks(Self::bits_per_limb())
807 .map(LimbVar::from)
808 .collect::<Vec<_>>(),
809 )
810 }
811}
812
813// If we impl `AbsorbNonNative` directly for `PrimeField`, rustc will complain
814// that this impl conflicts with the impl for `CurveGroup`.
815// Therefore, we instead impl `AbsorbNonNative` for a slice of `PrimeField` as a
816// workaround.
817impl<TargetField: PrimeField, BaseField: PrimeField> AbsorbNonNative<BaseField>
818 for [TargetField]
819{
820 fn to_native_sponge_field_elements(&self, dest: &mut Vec<BaseField>) {
821 self.iter()
822 .for_each(|x| dest.extend(&nonnative_field_to_field_elements(x)));
823 }
824}
825
826impl<F: PrimeField> AbsorbNonNativeGadget<F> for NonNativeUintVar<F> {
827 fn to_native_sponge_field_elements(&self) -> Result<Vec<FpVar<F>>, SynthesisError> {
828 self.to_constraint_field()
829 }
830}
831
832/// The out-circuit counterpart of `NonNativeUintVar::to_constraint_field`
833pub(super) fn nonnative_field_to_field_elements<TargetField: Field, BaseField: PrimeField>(
834 f: &TargetField,
835) -> Vec<BaseField> {
836 assert_eq!(TargetField::extension_degree(), 1);
837 let bits = f
838 .to_base_prime_field_elements()
839 .next()
840 .unwrap()
841 .into_bigint()
842 .to_bits_le();
843
844 let bits_per_limb = BaseField::MODULUS_BIT_SIZE as usize - 1;
845 let num_limbs =
846 (TargetField::BasePrimeField::MODULUS_BIT_SIZE as usize).div_ceil(bits_per_limb);
847
848 let mut limbs = bits
849 .chunks(bits_per_limb)
850 .map(|chunk| {
851 let mut limb = BaseField::zero();
852 let mut w = BaseField::one();
853 for &b in chunk.iter() {
854 limb += BaseField::from(b) * w;
855 w.double_in_place();
856 }
857 limb
858 })
859 .collect::<Vec<BaseField>>();
860 limbs.resize(num_limbs, BaseField::zero());
861
862 limbs
863}
864
865impl<F: PrimeField> VectorGadget<NonNativeUintVar<F>> for [NonNativeUintVar<F>] {
866 fn add(&self, other: &Self) -> Result<Vec<NonNativeUintVar<F>>, SynthesisError> {
867 Ok(self
868 .iter()
869 .zip(other.iter())
870 .map(|(x, y)| x.add_no_align(y))
871 .collect())
872 }
873
874 fn hadamard(&self, other: &Self) -> Result<Vec<NonNativeUintVar<F>>, SynthesisError> {
875 self.iter()
876 .zip(other.iter())
877 .map(|(x, y)| x.mul_no_align(y))
878 .collect()
879 }
880
881 fn mul_scalar(
882 &self,
883 other: &NonNativeUintVar<F>,
884 ) -> Result<Vec<NonNativeUintVar<F>>, SynthesisError> {
885 self.iter().map(|x| x.mul_no_align(other)).collect()
886 }
887}
888
889impl<F: PrimeField, CF: PrimeField> MatrixGadget<NonNativeUintVar<CF>>
890 for SparseMatrixVar<F, CF, NonNativeUintVar<CF>>
891{
892 fn mul_vector(
893 &self,
894 v: &[NonNativeUintVar<CF>],
895 ) -> Result<Vec<NonNativeUintVar<CF>>, SynthesisError> {
896 Ok(self
897 .coeffs
898 .iter()
899 .map(|row| {
900 let len = row
901 .iter()
902 .map(|(value, col_i)| value.0.len() + v[*col_i].0.len() - 1)
903 .max()
904 .unwrap_or(0);
905 // This is a combination of `mul_no_align` and `add_no_align`
906 // that results in more flattened `LinearCombination`s.
907 // Consequently, `ConstraintSystem::inline_all_lcs` costs less
908 // time, thus making trusted setup and proof generation faster.
909 let limbs = (0..len)
910 .map(|i| {
911 LimbVar::add_many(
912 &row.iter()
913 .flat_map(|(value, col_i)| {
914 let start = max(i + 1, v[*col_i].0.len()) - v[*col_i].0.len();
915 let end = min(i + 1, value.0.len());
916 (start..end).map(|j| value.0[j].mul(&v[*col_i].0[i - j]))
917 })
918 .collect::<Option<Vec<_>>>()?,
919 )
920 })
921 .collect::<Option<Vec<_>>>()
922 .unwrap();
923 NonNativeUintVar(limbs)
924 })
925 .collect())
926 }
927}
928
929#[cfg(test)]
930mod tests {
931 use std::error::Error;
932
933 use super::*;
934 use ark_pallas::{Fq, Fr};
935 use ark_relations::r1cs::ConstraintSystem;
936 use ark_std::{test_rng, UniformRand};
937 use num_bigint::RandBigInt;
938
939 #[test]
940 fn test_mul_biguint() -> Result<(), Box<dyn Error>> {
941 let cs = ConstraintSystem::<Fr>::new_ref();
942
943 let size = 256;
944
945 let rng = &mut test_rng();
946 let a = rng.gen_biguint(size as u64);
947 let b = rng.gen_biguint(size as u64);
948 let ab = &a * &b;
949 let aab = &a * &ab;
950 let abb = &ab * &b;
951
952 let a_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(BoundedBigUint(a, size)))?;
953 let b_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(BoundedBigUint(b, size)))?;
954 let ab_var =
955 NonNativeUintVar::new_witness(cs.clone(), || Ok(BoundedBigUint(ab, size * 2)))?;
956 let aab_var =
957 NonNativeUintVar::new_witness(cs.clone(), || Ok(BoundedBigUint(aab, size * 3)))?;
958 let abb_var =
959 NonNativeUintVar::new_witness(cs.clone(), || Ok(BoundedBigUint(abb, size * 3)))?;
960
961 a_var
962 .mul_no_align(&b_var)?
963 .enforce_equal_unaligned(&ab_var)?;
964 a_var
965 .mul_no_align(&ab_var)?
966 .enforce_equal_unaligned(&aab_var)?;
967 ab_var
968 .mul_no_align(&b_var)?
969 .enforce_equal_unaligned(&abb_var)?;
970
971 assert!(cs.is_satisfied()?);
972 Ok(())
973 }
974
975 #[test]
976 fn test_mul_fq() -> Result<(), Box<dyn Error>> {
977 let cs = ConstraintSystem::<Fr>::new_ref();
978
979 let rng = &mut test_rng();
980 let a = Fq::rand(rng);
981 let b = Fq::rand(rng);
982 let ab = a * b;
983 let aab = a * ab;
984 let abb = ab * b;
985
986 let a_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(a))?;
987 let b_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(b))?;
988 let ab_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(ab))?;
989 let aab_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(aab))?;
990 let abb_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(abb))?;
991
992 a_var
993 .mul_no_align(&b_var)?
994 .enforce_congruent::<Fq>(&ab_var)?;
995 a_var
996 .mul_no_align(&ab_var)?
997 .enforce_congruent::<Fq>(&aab_var)?;
998 ab_var
999 .mul_no_align(&b_var)?
1000 .enforce_congruent::<Fq>(&abb_var)?;
1001
1002 assert!(cs.is_satisfied()?);
1003 Ok(())
1004 }
1005
1006 #[test]
1007 fn test_pow() -> Result<(), Box<dyn Error>> {
1008 let cs = ConstraintSystem::<Fr>::new_ref();
1009
1010 let rng = &mut test_rng();
1011
1012 let a = Fq::rand(rng);
1013
1014 let a_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(a))?;
1015
1016 let mut r_var = a_var.clone();
1017 for _ in 0..16 {
1018 r_var = r_var.mul_no_align(&r_var)?.modulo::<Fq>()?;
1019 }
1020 r_var = r_var.mul_no_align(&a_var)?.modulo::<Fq>()?;
1021 assert_eq!(a.pow([65537u64]), Fq::from(r_var.value()?));
1022 assert!(cs.is_satisfied()?);
1023 Ok(())
1024 }
1025
1026 #[test]
1027 fn test_vec_vec_mul() -> Result<(), Box<dyn Error>> {
1028 let cs = ConstraintSystem::<Fr>::new_ref();
1029
1030 let len = 1000;
1031
1032 let rng = &mut test_rng();
1033 let a = (0..len).map(|_| Fq::rand(rng)).collect::<Vec<Fq>>();
1034 let b = (0..len).map(|_| Fq::rand(rng)).collect::<Vec<Fq>>();
1035 let c = a.iter().zip(b.iter()).map(|(a, b)| a * b).sum::<Fq>();
1036
1037 let a_var = Vec::<NonNativeUintVar<Fr>>::new_witness(cs.clone(), || Ok(a))?;
1038 let b_var = Vec::<NonNativeUintVar<Fr>>::new_witness(cs.clone(), || Ok(b))?;
1039 let c_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(c))?;
1040
1041 let mut r_var =
1042 NonNativeUintVar::new_constant(cs.clone(), BoundedBigUint(BigUint::zero(), 0))?;
1043 for (a, b) in a_var.into_iter().zip(b_var.into_iter()) {
1044 r_var = r_var.add_no_align(&a.mul_no_align(&b)?);
1045 }
1046 r_var.enforce_congruent::<Fq>(&c_var)?;
1047
1048 assert!(cs.is_satisfied()?);
1049 Ok(())
1050 }
1051}