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