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