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 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(x: &BigUint, l: usize) -> Vec<F> {
260 (0..l)
261 .map(|i| x.bit(i as u64))
262 .collect::<Vec<_>>()
263 .chunks(Self::bits_per_limb())
264 .map(|chunk| F::from_bigint(F::BigInt::from_bits_le(chunk)).unwrap())
265 .collect()
266 }
267}
268
269impl<F: PrimeField> R1CSVar<F> for NonNativeUintVar<F> {
270 type Value = BigUint;
271
272 fn cs(&self) -> ConstraintSystemRef<F> {
273 self.0.cs()
274 }
275
276 fn value(&self) -> Result<Self::Value, SynthesisError> {
277 let mut r = BigUint::zero();
278
279 for limb in self.0.value()?.into_iter().rev() {
280 r <<= Self::bits_per_limb();
281 r += Into::<BigUint>::into(limb);
282 }
283
284 Ok(r)
285 }
286}
287
288impl<F: PrimeField> NonNativeUintVar<F> {
289 /// Enforce `self` to be less than `other`, where `self` and `other` should
290 /// be aligned.
291 /// Adapted from https://github.com/akosba/jsnark/blob/0955389d0aae986ceb25affc72edf37a59109250/JsnarkCircuitBuilder/src/circuit/auxiliary/LongElement.java#L801-L872
292 pub fn enforce_lt(&self, other: &Self) -> Result<(), SynthesisError> {
293 let len = max(self.0.len(), other.0.len());
294 let zero = LimbVar::zero();
295
296 // Compute the difference between limbs of `other` and `self`.
297 // Denote a positive limb by `+`, a negative limb by `-`, a zero limb by
298 // `0`, and an unknown limb by `?`.
299 // Then, for `self < other`, `delta` should look like:
300 // ? ? ... ? ? + 0 0 ... 0 0
301 let delta = (0..len)
302 .map(|i| {
303 let x = &self.0.get(i).unwrap_or(&zero).v;
304 let y = &other.0.get(i).unwrap_or(&zero).v;
305 y - x
306 })
307 .collect::<Vec<_>>();
308
309 // `helper` is a vector of booleans that indicates if the corresponding
310 // limb of `delta` is the first (searching from MSB) positive limb.
311 // For example, if `delta` is:
312 // - + ... + - + 0 0 ... 0 0
313 // <---- search in this direction --------
314 // Then `helper` should be:
315 // F F ... F F T F F ... F F
316 let helper = {
317 let cs = self.cs().or(other.cs());
318 let mut helper = vec![false; len];
319 for i in (0..len).rev() {
320 let delta = delta[i].value().unwrap_or_default().into_bigint();
321 if !delta.is_zero() && delta < F::MODULUS_MINUS_ONE_DIV_TWO {
322 helper[i] = true;
323 break;
324 }
325 }
326 if cs.is_none() {
327 Vec::<Boolean<F>>::new_constant(cs, helper)?
328 } else {
329 Vec::new_witness(cs, || Ok(helper))?
330 }
331 };
332
333 // `p` is the first positive limb in `delta`.
334 let mut p = FpVar::<F>::zero();
335 // `r` is the sum of all bits in `helper`, which should be 1 when `self`
336 // is less than `other`, as there should be more than one positive limb
337 // in `delta`, and thus exactly one true bit in `helper`.
338 let mut r = FpVar::zero();
339 for (b, d) in helper.into_iter().zip(delta) {
340 // Choose the limb `d` only if `b` is true.
341 p += b.select(&d, &FpVar::zero())?;
342 // Either `r` or `d` should be zero.
343 // Consider the same example as above:
344 // - + ... + - + 0 0 ... 0 0
345 // F F ... F F T F F ... F F
346 // |-----------|
347 // `r = 0` in this range (before/when we meet the first positive limb)
348 // |---------|
349 // `d = 0` in this range (after we meet the first positive limb)
350 // This guarantees that for every bit after the true bit in `helper`,
351 // the corresponding limb in `delta` is zero.
352 (&r * &d).enforce_equal(&FpVar::zero())?;
353 // Add the current bit to `r`.
354 r += FpVar::from(b);
355 }
356
357 // Ensure that `r` is exactly 1. This guarantees that there is exactly
358 // one true value in `helper`.
359 r.enforce_equal(&FpVar::one())?;
360 // Ensure that `p` is positive, i.e.,
361 // `0 <= p - 1 < 2^bits_per_limb < F::MODULUS_MINUS_ONE_DIV_TWO`.
362 // This guarantees that the true value in `helper` corresponds to a
363 // positive limb in `delta`.
364 Self::enforce_bit_length(&(p - FpVar::one()), Self::bits_per_limb())?;
365
366 Ok(())
367 }
368
369 /// Enforce `self` to be equal to `other`, where `self` and `other` are not
370 /// necessarily aligned.
371 ///
372 /// Adapted from https://github.com/akosba/jsnark/blob/0955389d0aae986ceb25affc72edf37a59109250/JsnarkCircuitBuilder/src/circuit/auxiliary/LongElement.java#L562-L798
373 /// Similar implementations can also be found in https://github.com/alex-ozdemir/bellman-bignat/blob/0585b9d90154603a244cba0ac80b9aafe1d57470/src/mp/bignat.rs#L566-L661
374 /// and https://github.com/arkworks-rs/r1cs-std/blob/4020fbc22625621baa8125ede87abaeac3c1ca26/src/fields/emulated_fp/reduce.rs#L201-L323
375 pub fn enforce_equal_unaligned(&self, other: &Self) -> Result<(), SynthesisError> {
376 let len = min(self.0.len(), other.0.len());
377
378 // Group the limbs of `self` and `other` so that each group nearly
379 // reaches the capacity `F::MODULUS_MINUS_ONE_DIV_TWO`.
380 // By saying group, we mean the operation `Σ x_i 2^{i * W}`, where `W`
381 // is the initial number of bits in a limb, just as what we do in grade
382 // school arithmetic, e.g.,
383 // 5 9
384 // x 7 3
385 // -------------
386 // 15 27
387 // 35 63
388 // ------------- <- When grouping 35, 15 + 63, and 27, we are computing
389 // 4 3 0 7 35 * 100 + (15 + 63) * 10 + 27 = 4307
390 // Note that this is different from the concatenation `x_0 || x_1 ...`,
391 // since the bit-length of each limb is not necessarily the initial size
392 // `W`.
393 let (steps, x, y, rest) = {
394 // `steps` stores the size of each grouped limb.
395 let mut steps = vec![];
396 // `x_grouped` stores the grouped limbs of `self`.
397 let mut x_grouped = vec![];
398 // `y_grouped` stores the grouped limbs of `other`.
399 let mut y_grouped = vec![];
400 let mut i = 0;
401 while i < len {
402 let mut j = i;
403 // The current grouped limbs of `self` and `other`.
404 let mut xx = LimbVar::zero();
405 let mut yy = LimbVar::zero();
406 while j < len {
407 let shift = BigUint::one() << (Self::bits_per_limb() * (j - i));
408 assert!(shift < F::MODULUS_MINUS_ONE_DIV_TWO.into());
409 let shift = LimbVar::constant(shift.into());
410 match (
411 // Try to group `x` and `y` into `xx` and `yy`.
412 self.0[j].mul(&shift).and_then(|x| xx.add(&x)),
413 other.0[j].mul(&shift).and_then(|y| yy.add(&y)),
414 ) {
415 // Update the result if successful.
416 (Some(x), Some(y)) => (xx, yy) = (x, y),
417 // Break the loop if the upper bound of the result exceeds
418 // the maximum capacity.
419 _ => break,
420 }
421 j += 1;
422 }
423 // Store the grouped limbs and their size.
424 steps.push((j - i) * Self::bits_per_limb());
425 x_grouped.push(xx);
426 y_grouped.push(yy);
427 // Start the next group
428 i = j;
429 }
430 let remaining_limbs = &(if i < self.0.len() { self } else { other }).0[i..];
431 let rest = if remaining_limbs.is_empty() {
432 FpVar::zero()
433 } else {
434 // If there is any remaining limb, the first one should be the
435 // final carry (which will be checked later), and the following
436 // ones should be zero.
437
438 // Enforce the remaining limbs to be zero.
439 // Instead of doing that one by one, we check if their sum is
440 // zero using a single constraint.
441 // This is sound, as the upper bounds of the limbs and their sum
442 // are guaranteed to be less than `F::MODULUS_MINUS_ONE_DIV_TWO`
443 // (i.e., all of them are "non-negative"), implying that all
444 // limbs should be zero to make the sum zero.
445 LimbVar::add_many(&remaining_limbs[1..])
446 .unwrap()
447 .v
448 .enforce_equal(&FpVar::zero())?;
449 remaining_limbs[0].v.clone()
450 };
451 (steps, x_grouped, y_grouped, rest)
452 };
453 let n = steps.len();
454 // `c` stores the current carry of `x_i - y_i`
455 let mut c = FpVar::<F>::zero();
456 // For each group, check the last `step_i` bits of `x_i` and `y_i` are
457 // equal.
458 // The intuition is to check `diff = x_i - y_i = 0 (mod 2^step_i)`.
459 // However, this is only true for `i = 0`, and we need to consider carry
460 // values `diff >> step_i` for `i > 0`.
461 // Therefore, we actually check `diff = x_i - y_i + c = 0 (mod 2^step_i)`
462 // and derive the next `c` by computing `diff >> step_i`.
463 // To enforce `diff = 0 (mod 2^step_i)`, we compute `diff / 2^step_i`
464 // and enforce it to be small (soundness holds because for `a` that does
465 // not divide `b`, `b / a` in the field will be very large.
466 for i in 0..n {
467 let step = steps[i];
468 c = (&x[i].v - &y[i].v + &c)
469 .mul_by_inverse_unchecked(&FpVar::constant(F::from(BigUint::one() << step)))?;
470 if i != n - 1 {
471 // Unlike the code mentioned above which add some offset to the
472 // diff `x_i - y_i + c` to make it always positive, we directly
473 // check if the absolute value of the diff is small.
474 Self::enforce_abs_bit_length(
475 &c,
476 (max(&x[i].ub, &y[i].ub).bits() as usize)
477 .checked_sub(step)
478 .unwrap_or_default(),
479 )?;
480 } else {
481 // For the final carry, we need to ensure that it equals the
482 // remaining limb `rest`.
483 c.enforce_equal(&rest)?;
484 }
485 }
486
487 Ok(())
488 }
489}
490
491impl<F: PrimeField> ToBitsGadget<F> for NonNativeUintVar<F> {
492 fn to_bits_le(&self) -> Result<Vec<Boolean<F>>, SynthesisError> {
493 Ok(self
494 .0
495 .iter()
496 .map(|limb| limb.to_bits_le())
497 .collect::<Result<Vec<_>, _>>()?
498 .concat())
499 }
500}
501
502impl<F: PrimeField> ToConstraintFieldGadget<F> for NonNativeUintVar<F> {
503 fn to_constraint_field(&self) -> Result<Vec<FpVar<F>>, SynthesisError> {
504 let bits_per_limb = F::MODULUS_BIT_SIZE as usize - 1;
505
506 let limbs = self
507 .to_bits_le()?
508 .chunks(bits_per_limb)
509 .map(Boolean::le_bits_to_fp_var)
510 .collect::<Result<Vec<_>, _>>()?;
511
512 Ok(limbs)
513 }
514}
515
516impl<F: PrimeField> CondSelectGadget<F> for NonNativeUintVar<F> {
517 fn conditionally_select(
518 cond: &Boolean<F>,
519 true_value: &Self,
520 false_value: &Self,
521 ) -> Result<Self, SynthesisError> {
522 assert_eq!(true_value.0.len(), false_value.0.len());
523 let mut v = vec![];
524 for i in 0..true_value.0.len() {
525 v.push(cond.select(&true_value.0[i], &false_value.0[i])?);
526 }
527 Ok(Self(v))
528 }
529}
530
531impl<F: PrimeField> NonNativeUintVar<F> {
532 pub fn ubound(&self) -> BigUint {
533 let mut r = BigUint::zero();
534
535 for i in self.0.iter().rev() {
536 r <<= Self::bits_per_limb();
537 r += &i.ub;
538 }
539
540 r
541 }
542
543 fn enforce_bit_length(x: &FpVar<F>, length: usize) -> Result<Vec<Boolean<F>>, SynthesisError> {
544 let cs = x.cs();
545
546 let bits = &x.value().unwrap_or_default().into_bigint().to_bits_le()[..length];
547 let bits = if cs.is_none() {
548 Vec::new_constant(cs, bits)?
549 } else {
550 Vec::new_witness(cs, || Ok(bits))?
551 };
552
553 Boolean::le_bits_to_fp_var(&bits)?.enforce_equal(x)?;
554
555 Ok(bits)
556 }
557
558 fn enforce_abs_bit_length(
559 x: &FpVar<F>,
560 length: usize,
561 ) -> Result<Vec<Boolean<F>>, SynthesisError> {
562 let cs = x.cs();
563 let mode = if cs.is_none() {
564 AllocationMode::Constant
565 } else {
566 AllocationMode::Witness
567 };
568
569 let is_neg = Boolean::new_variable(
570 cs.clone(),
571 || Ok(x.value().unwrap_or_default().into_bigint() > F::MODULUS_MINUS_ONE_DIV_TWO),
572 mode,
573 )?;
574 let bits = Vec::new_variable(
575 cs.clone(),
576 || {
577 Ok({
578 let x = x.value().unwrap_or_default();
579 let mut bits = if is_neg.value().unwrap_or_default() {
580 -x
581 } else {
582 x
583 }
584 .into_bigint()
585 .to_bits_le();
586 bits.resize(length, false);
587 bits
588 })
589 },
590 mode,
591 )?;
592
593 // Below is equivalent to but more efficient than
594 // `Boolean::le_bits_to_fp_var(&bits)?.enforce_equal(&is_neg.select(&x.negate()?, &x)?)?`
595 // Note that this enforces:
596 // 1. The claimed absolute value `is_neg.select(&x.negate()?, &x)?` has
597 // exactly `length` bits.
598 // 2. `is_neg` is indeed the sign of `x`, i.e., `is_neg = false` when
599 // `0 <= x < (|F| - 1) / 2`, and `is_neg = true` when
600 // `(|F| - 1) / 2 <= x < F`, thus the claimed absolute value is
601 // correct.
602 // If `is_neg` is incorrect, then:
603 // a. `0 <= x < (|F| - 1) / 2`, but `is_neg = true`, then
604 // `is_neg.select(&x.negate()?, &x)?` returns `|F| - x`,
605 // which is greater than `(|F| - 1) / 2` and cannot fit in
606 // `length` bits (given that `length` is small).
607 // b. `(|F| - 1) / 2 <= x < F`, but `is_neg = false`, then
608 // `is_neg.select(&x.negate()?, &x)?` returns `x`, which is
609 // greater than `(|F| - 1) / 2` and cannot fit in `length`
610 // bits.
611 FpVar::from(is_neg).mul_equals(&x.double()?, &(x - Boolean::le_bits_to_fp_var(&bits)?))?;
612
613 Ok(bits)
614 }
615
616 /// Compute `self + other`, without aligning the limbs.
617 pub fn add_no_align(&self, other: &Self) -> Self {
618 let mut z = vec![LimbVar::zero(); max(self.0.len(), other.0.len())];
619 for (i, v) in self.0.iter().enumerate() {
620 z[i] = z[i].add(v).unwrap();
621 }
622 for (i, v) in other.0.iter().enumerate() {
623 z[i] = z[i].add(v).unwrap();
624 }
625 Self(z)
626 }
627
628 /// Compute `self * other`, without aligning the limbs.
629 /// Implements the O(n) approach described in xJsnark, Section IV.B.1)
630 pub fn mul_no_align(&self, other: &Self) -> Result<Self, SynthesisError> {
631 let len = self.0.len() + other.0.len() - 1;
632 if self.is_constant() || other.is_constant() {
633 // Use the naive approach for constant operands, which costs no
634 // constraints.
635 let z = (0..len)
636 .map(|i| {
637 let start = max(i + 1, other.0.len()) - other.0.len();
638 let end = min(i + 1, self.0.len());
639 LimbVar::add_many(
640 &(start..end)
641 .map(|j| self.0[j].mul(&other.0[i - j]))
642 .collect::<Option<Vec<_>>>()?,
643 )
644 })
645 .collect::<Option<Vec<_>>>()
646 .unwrap();
647 return Ok(Self(z));
648 }
649 let cs = self.cs().or(other.cs());
650 let mode = if cs.is_none() {
651 AllocationMode::Constant
652 } else {
653 AllocationMode::Witness
654 };
655
656 // Compute the result `z` outside the circuit and provide it as hints.
657 let z = {
658 let mut z = vec![(F::zero(), BigUint::zero()); len];
659 for i in 0..self.0.len() {
660 for j in 0..other.0.len() {
661 z[i + j].0 += self.0[i].value().unwrap_or_default()
662 * other.0[j].value().unwrap_or_default();
663 z[i + j].1 += &self.0[i].ub * &other.0[j].ub;
664 }
665 }
666 z.into_iter()
667 .map(|(v, ub)| {
668 assert!(ub < F::MODULUS_MINUS_ONE_DIV_TWO.into());
669 Ok(LimbVar {
670 v: FpVar::new_variable(cs.clone(), || Ok(v), mode)?,
671 ub,
672 })
673 })
674 .collect::<Result<Vec<_>, _>>()?
675 };
676 for c in 1..=len {
677 let c = F::from(c as u64);
678 let mut t = F::one();
679 let mut c_powers = vec![];
680 for _ in 0..len {
681 c_powers.push(t);
682 t *= c;
683 }
684 // `l = Σ self[i] c^i`
685 let l = self
686 .0
687 .iter()
688 .zip(&c_powers)
689 .map(|(v, t)| (&v.v * *t))
690 .collect::<Vec<_>>()
691 .iter()
692 .sum::<FpVar<_>>();
693 // `r = Σ other[i] c^i`
694 let r = other
695 .0
696 .iter()
697 .zip(&c_powers)
698 .map(|(v, t)| (&v.v * *t))
699 .collect::<Vec<_>>()
700 .iter()
701 .sum::<FpVar<_>>();
702 // `o = Σ z[i] c^i`
703 let o = z
704 .iter()
705 .zip(&c_powers)
706 .map(|(v, t)| &v.v * *t)
707 .collect::<Vec<_>>()
708 .iter()
709 .sum::<FpVar<_>>();
710 // Enforce `o = l * r`
711 l.mul_equals(&r, &o)?;
712 }
713
714 Ok(Self(z))
715 }
716
717 /// Convert `Self` to an element in `M`, i.e., compute `Self % M::MODULUS`.
718 pub fn modulo<M: PrimeField>(&self) -> Result<Self, SynthesisError> {
719 let cs = self.cs();
720 let mode = if cs.is_none() {
721 AllocationMode::Constant
722 } else {
723 AllocationMode::Witness
724 };
725 let m: BigUint = M::MODULUS.into();
726 // Provide the quotient and remainder as hints
727 let (q, r) = {
728 let v = self.value().unwrap_or_default();
729 let (q, r) = v.div_rem(&m);
730 let q_ubound = self.ubound().div_ceil(&m);
731 let r_ubound = &m;
732 (
733 Self::new_variable(
734 cs.clone(),
735 || Ok(BoundedBigUint(q, q_ubound.bits() as usize)),
736 mode,
737 )?,
738 Self::new_variable(
739 cs.clone(),
740 || Ok(BoundedBigUint(r, r_ubound.bits() as usize)),
741 mode,
742 )?,
743 )
744 };
745
746 let m = Self::new_constant(cs.clone(), BoundedBigUint(m, M::MODULUS_BIT_SIZE as usize))?;
747 // Enforce `self = q * m + r`
748 q.mul_no_align(&m)?
749 .add_no_align(&r)
750 .enforce_equal_unaligned(self)?;
751 // Enforce `r < m` (and `r >= 0` already holds)
752 r.enforce_lt(&m)?;
753
754 Ok(r)
755 }
756
757 /// Enforce that `self` is congruent to `other` modulo `M::MODULUS`.
758 pub fn enforce_congruent<M: PrimeField>(&self, other: &Self) -> Result<(), SynthesisError> {
759 let cs = self.cs();
760 let mode = if cs.is_none() {
761 AllocationMode::Constant
762 } else {
763 AllocationMode::Witness
764 };
765 let m: BigUint = M::MODULUS.into();
766 let bits = (max(self.ubound(), other.ubound()) / &m).bits() as usize;
767 // Provide the quotient `|x - y| / m` and a boolean indicating if `x > y`
768 // as hints.
769 let (q, is_ge) = {
770 let x = self.value().unwrap_or_default();
771 let y = other.value().unwrap_or_default();
772 let (d, b) = if x > y {
773 ((x - y) / &m, true)
774 } else {
775 ((y - x) / &m, false)
776 };
777 (
778 Self::new_variable(cs.clone(), || Ok(BoundedBigUint(d, bits)), mode)?,
779 Boolean::new_variable(cs.clone(), || Ok(b), mode)?,
780 )
781 };
782
783 let zero = Self::new_constant(cs.clone(), BoundedBigUint(BigUint::zero(), bits))?;
784 let m = Self::new_constant(cs.clone(), BoundedBigUint(m, M::MODULUS_BIT_SIZE as usize))?;
785 let l = self.add_no_align(&is_ge.select(&zero, &q)?.mul_no_align(&m)?);
786 let r = other.add_no_align(&is_ge.select(&q, &zero)?.mul_no_align(&m)?);
787 // If `self >= other`, enforce `self = other + q * m`
788 // Otherwise, enforce `self + q * m = other`
789 // Soundness holds because if `self` and `other` are not congruent, then
790 // one can never find a `q` satisfying either equation above.
791 l.enforce_equal_unaligned(&r)
792 }
793}
794
795impl<F: PrimeField, B: AsRef<[Boolean<F>]>> From<B> for NonNativeUintVar<F> {
796 fn from(bits: B) -> Self {
797 Self(
798 bits.as_ref()
799 .chunks(Self::bits_per_limb())
800 .map(LimbVar::from)
801 .collect::<Vec<_>>(),
802 )
803 }
804}
805
806/// The out-circuit counterpart of `NonNativeUintVar::to_constraint_field`
807pub fn nonnative_field_to_field_elements<TargetField: PrimeField, BaseField: PrimeField>(
808 f: &TargetField,
809) -> Vec<BaseField> {
810 let bits = f.into_bigint().to_bits_le();
811
812 let bits_per_limb = BaseField::MODULUS_BIT_SIZE as usize - 1;
813 let num_limbs = (TargetField::MODULUS_BIT_SIZE as usize).div_ceil(bits_per_limb);
814
815 let mut limbs = bits
816 .chunks(bits_per_limb)
817 .map(|chunk| {
818 let mut limb = BaseField::zero();
819 let mut w = BaseField::one();
820 for &b in chunk.iter() {
821 limb += BaseField::from(b) * w;
822 w.double_in_place();
823 }
824 limb
825 })
826 .collect::<Vec<BaseField>>();
827 limbs.resize(num_limbs, BaseField::zero());
828
829 limbs
830}
831
832impl<F: PrimeField> VectorGadget<NonNativeUintVar<F>> for [NonNativeUintVar<F>] {
833 fn add(&self, other: &Self) -> Result<Vec<NonNativeUintVar<F>>, SynthesisError> {
834 Ok(self
835 .iter()
836 .zip(other.iter())
837 .map(|(x, y)| x.add_no_align(y))
838 .collect())
839 }
840
841 fn hadamard(&self, other: &Self) -> Result<Vec<NonNativeUintVar<F>>, SynthesisError> {
842 self.iter()
843 .zip(other.iter())
844 .map(|(x, y)| x.mul_no_align(y))
845 .collect()
846 }
847
848 fn mul_scalar(
849 &self,
850 other: &NonNativeUintVar<F>,
851 ) -> Result<Vec<NonNativeUintVar<F>>, SynthesisError> {
852 self.iter().map(|x| x.mul_no_align(other)).collect()
853 }
854}
855
856impl<F: PrimeField, CF: PrimeField> MatrixGadget<NonNativeUintVar<CF>>
857 for SparseMatrixVar<F, CF, NonNativeUintVar<CF>>
858{
859 fn mul_vector(
860 &self,
861 v: &[NonNativeUintVar<CF>],
862 ) -> Result<Vec<NonNativeUintVar<CF>>, SynthesisError> {
863 Ok(self
864 .coeffs
865 .iter()
866 .map(|row| {
867 let len = row
868 .iter()
869 .map(|(value, col_i)| value.0.len() + v[*col_i].0.len() - 1)
870 .max()
871 .unwrap_or(0);
872 // This is a combination of `mul_no_align` and `add_no_align`
873 // that results in more flattened `LinearCombination`s.
874 // Consequently, `ConstraintSystem::inline_all_lcs` costs less
875 // time, thus making trusted setup and proof generation faster.
876 let limbs = (0..len)
877 .map(|i| {
878 LimbVar::add_many(
879 &row.iter()
880 .flat_map(|(value, col_i)| {
881 let start = max(i + 1, v[*col_i].0.len()) - v[*col_i].0.len();
882 let end = min(i + 1, value.0.len());
883 (start..end).map(|j| value.0[j].mul(&v[*col_i].0[i - j]))
884 })
885 .collect::<Option<Vec<_>>>()?,
886 )
887 })
888 .collect::<Option<Vec<_>>>()
889 .unwrap();
890 NonNativeUintVar(limbs)
891 })
892 .collect())
893 }
894}
895
896#[cfg(test)]
897mod tests {
898 use std::error::Error;
899
900 use super::*;
901 use ark_ff::Field;
902 use ark_pallas::{Fq, Fr};
903 use ark_relations::r1cs::ConstraintSystem;
904 use ark_std::{test_rng, UniformRand};
905 use num_bigint::RandBigInt;
906
907 #[test]
908 fn test_mul_biguint() -> Result<(), Box<dyn Error>> {
909 let cs = ConstraintSystem::<Fr>::new_ref();
910
911 let size = 256;
912
913 let rng = &mut test_rng();
914 let a = rng.gen_biguint(size as u64);
915 let b = rng.gen_biguint(size as u64);
916 let ab = &a * &b;
917 let aab = &a * &ab;
918 let abb = &ab * &b;
919
920 let a_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(BoundedBigUint(a, size)))?;
921 let b_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(BoundedBigUint(b, size)))?;
922 let ab_var =
923 NonNativeUintVar::new_witness(cs.clone(), || Ok(BoundedBigUint(ab, size * 2)))?;
924 let aab_var =
925 NonNativeUintVar::new_witness(cs.clone(), || Ok(BoundedBigUint(aab, size * 3)))?;
926 let abb_var =
927 NonNativeUintVar::new_witness(cs.clone(), || Ok(BoundedBigUint(abb, size * 3)))?;
928
929 a_var
930 .mul_no_align(&b_var)?
931 .enforce_equal_unaligned(&ab_var)?;
932 a_var
933 .mul_no_align(&ab_var)?
934 .enforce_equal_unaligned(&aab_var)?;
935 ab_var
936 .mul_no_align(&b_var)?
937 .enforce_equal_unaligned(&abb_var)?;
938
939 assert!(cs.is_satisfied()?);
940 Ok(())
941 }
942
943 #[test]
944 fn test_mul_fq() -> Result<(), Box<dyn Error>> {
945 let cs = ConstraintSystem::<Fr>::new_ref();
946
947 let rng = &mut test_rng();
948 let a = Fq::rand(rng);
949 let b = Fq::rand(rng);
950 let ab = a * b;
951 let aab = a * ab;
952 let abb = ab * b;
953
954 let a_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(a))?;
955 let b_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(b))?;
956 let ab_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(ab))?;
957 let aab_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(aab))?;
958 let abb_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(abb))?;
959
960 a_var
961 .mul_no_align(&b_var)?
962 .enforce_congruent::<Fq>(&ab_var)?;
963 a_var
964 .mul_no_align(&ab_var)?
965 .enforce_congruent::<Fq>(&aab_var)?;
966 ab_var
967 .mul_no_align(&b_var)?
968 .enforce_congruent::<Fq>(&abb_var)?;
969
970 assert!(cs.is_satisfied()?);
971 Ok(())
972 }
973
974 #[test]
975 fn test_pow() -> Result<(), Box<dyn Error>> {
976 let cs = ConstraintSystem::<Fr>::new_ref();
977
978 let rng = &mut test_rng();
979
980 let a = Fq::rand(rng);
981
982 let a_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(a))?;
983
984 let mut r_var = a_var.clone();
985 for _ in 0..16 {
986 r_var = r_var.mul_no_align(&r_var)?.modulo::<Fq>()?;
987 }
988 r_var = r_var.mul_no_align(&a_var)?.modulo::<Fq>()?;
989 assert_eq!(a.pow([65537u64]), Fq::from(r_var.value()?));
990 assert!(cs.is_satisfied()?);
991 Ok(())
992 }
993
994 #[test]
995 fn test_vec_vec_mul() -> Result<(), Box<dyn Error>> {
996 let cs = ConstraintSystem::<Fr>::new_ref();
997
998 let len = 1000;
999
1000 let rng = &mut test_rng();
1001 let a = (0..len).map(|_| Fq::rand(rng)).collect::<Vec<Fq>>();
1002 let b = (0..len).map(|_| Fq::rand(rng)).collect::<Vec<Fq>>();
1003 let c = a.iter().zip(b.iter()).map(|(a, b)| a * b).sum::<Fq>();
1004
1005 let a_var = Vec::<NonNativeUintVar<Fr>>::new_witness(cs.clone(), || Ok(a))?;
1006 let b_var = Vec::<NonNativeUintVar<Fr>>::new_witness(cs.clone(), || Ok(b))?;
1007 let c_var = NonNativeUintVar::new_witness(cs.clone(), || Ok(c))?;
1008
1009 let mut r_var =
1010 NonNativeUintVar::new_constant(cs.clone(), BoundedBigUint(BigUint::zero(), 0))?;
1011 for (a, b) in a_var.into_iter().zip(b_var.into_iter()) {
1012 r_var = r_var.add_no_align(&a.mul_no_align(&b)?);
1013 }
1014 r_var.enforce_congruent::<Fq>(&c_var)?;
1015
1016 assert!(cs.is_satisfied()?);
1017 Ok(())
1018 }
1019}