Srinath Setty
1 year ago
committed by
GitHub
GitHub
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 1146 additions and 388 deletions
Split View
Diff Options
-
+4 -3Cargo.toml
-
+0 -371src/bellperson/mod.rs
-
+4 -4src/gadgets/mod.rs
-
+830 -0src/gadgets/nonnative/bignat.rs
-
+39 -0src/gadgets/nonnative/mod.rs
-
+261 -0src/gadgets/nonnative/util.rs
-
+6 -8src/gadgets/r1cs.rs
-
+1 -1src/gadgets/utils.rs
-
+1 -1src/r1cs.rs
@ -1,5 +1,5 @@ |
|||
//! This module implements various gadgets necessary for Nova
|
|||
//! and applications built with Nova.
|
|||
//! This module implements various gadgets necessary for Nova and applications built with Nova.
|
|||
pub mod ecc;
|
|||
pub mod r1cs;
|
|||
pub mod utils;
|
|||
pub(crate) mod nonnative;
|
|||
pub(crate) mod r1cs;
|
|||
pub(crate) mod utils;
|
|||
@ -0,0 +1,830 @@ |
|||
use super::{
|
|||
util::{
|
|||
Bitvector, Num, {f_to_nat, nat_to_f},
|
|||
},
|
|||
OptionExt,
|
|||
};
|
|||
use bellperson::{ConstraintSystem, LinearCombination, SynthesisError};
|
|||
use ff::PrimeField;
|
|||
use num_bigint::BigInt;
|
|||
use num_traits::cast::ToPrimitive;
|
|||
use std::borrow::Borrow;
|
|||
use std::cmp::{max, min};
|
|||
use std::convert::From;
|
|||
|
|||
/// Compute the natural number represented by an array of limbs.
|
|||
/// The limbs are assumed to be based the `limb_width` power of 2.
|
|||
pub fn limbs_to_nat<Scalar: PrimeField, B: Borrow<Scalar>, I: DoubleEndedIterator<Item = B>>(
|
|||
limbs: I,
|
|||
limb_width: usize,
|
|||
) -> BigInt {
|
|||
limbs.rev().fold(BigInt::from(0), |mut acc, limb| {
|
|||
acc <<= limb_width as u32;
|
|||
acc += f_to_nat(limb.borrow());
|
|||
acc
|
|||
})
|
|||
}
|
|||
|
|||
fn int_with_n_ones(n: usize) -> BigInt {
|
|||
let mut m = BigInt::from(1);
|
|||
m <<= n as u32;
|
|||
m -= 1;
|
|||
m
|
|||
}
|
|||
|
|||
/// Compute the limbs encoding a natural number.
|
|||
/// The limbs are assumed to be based the `limb_width` power of 2.
|
|||
pub fn nat_to_limbs<Scalar: PrimeField>(
|
|||
nat: &BigInt,
|
|||
limb_width: usize,
|
|||
n_limbs: usize,
|
|||
) -> Result<Vec<Scalar>, SynthesisError> {
|
|||
let mask = int_with_n_ones(limb_width);
|
|||
let mut nat = nat.clone();
|
|||
if nat.bits() as usize <= n_limbs * limb_width {
|
|||
Ok(
|
|||
(0..n_limbs)
|
|||
.map(|_| {
|
|||
let r = &nat & &mask;
|
|||
nat >>= limb_width as u32;
|
|||
nat_to_f(&r).unwrap()
|
|||
})
|
|||
.collect(),
|
|||
)
|
|||
} else {
|
|||
eprintln!(
|
|||
"nat {} does not fit in {} limbs of width {}",
|
|||
nat, n_limbs, limb_width
|
|||
);
|
|||
Err(SynthesisError::Unsatisfiable)
|
|||
}
|
|||
}
|
|||
|
|||
#[derive(Clone, PartialEq, Eq)]
|
|||
pub struct BigNatParams {
|
|||
pub min_bits: usize,
|
|||
pub max_word: BigInt,
|
|||
pub limb_width: usize,
|
|||
pub n_limbs: usize,
|
|||
}
|
|||
|
|||
impl BigNatParams {
|
|||
pub fn new(limb_width: usize, n_limbs: usize) -> Self {
|
|||
let mut max_word = BigInt::from(1) << limb_width as u32;
|
|||
max_word -= 1;
|
|||
BigNatParams {
|
|||
max_word,
|
|||
n_limbs,
|
|||
limb_width,
|
|||
min_bits: 0,
|
|||
}
|
|||
}
|
|||
}
|
|||
|
|||
/// A representation of a large natural number (a member of {0, 1, 2, ... })
|
|||
#[derive(Clone)]
|
|||
pub struct BigNat<Scalar: PrimeField> {
|
|||
/// The linear combinations which constrain the value of each limb of the number
|
|||
pub limbs: Vec<LinearCombination<Scalar>>,
|
|||
/// The witness values for each limb (filled at witness-time)
|
|||
pub limb_values: Option<Vec<Scalar>>,
|
|||
/// The value of the whole number (filled at witness-time)
|
|||
pub value: Option<BigInt>,
|
|||
/// Parameters
|
|||
pub params: BigNatParams,
|
|||
}
|
|||
|
|||
impl<Scalar: PrimeField> std::cmp::PartialEq for BigNat<Scalar> {
|
|||
fn eq(&self, other: &Self) -> bool {
|
|||
self.value == other.value && self.params == other.params
|
|||
}
|
|||
}
|
|||
impl<Scalar: PrimeField> std::cmp::Eq for BigNat<Scalar> {}
|
|||
|
|||
impl<Scalar: PrimeField> From<BigNat<Scalar>> for Polynomial<Scalar> {
|
|||
fn from(other: BigNat<Scalar>) -> Polynomial<Scalar> {
|
|||
Polynomial {
|
|||
coefficients: other.limbs,
|
|||
values: other.limb_values,
|
|||
}
|
|||
}
|
|||
}
|
|||
|
|||
impl<Scalar: PrimeField> BigNat<Scalar> {
|
|||
/// Allocates a `BigNat` in the circuit with `n_limbs` limbs of width `limb_width` each.
|
|||
/// If `max_word` is missing, then it is assumed to be `(2 << limb_width) - 1`.
|
|||
/// The value is provided by a closure returning limb values.
|
|||
pub fn alloc_from_limbs<CS, F>(
|
|||
mut cs: CS,
|
|||
f: F,
|
|||
max_word: Option<BigInt>,
|
|||
limb_width: usize,
|
|||
n_limbs: usize,
|
|||
) -> Result<Self, SynthesisError>
|
|||
where
|
|||
CS: ConstraintSystem<Scalar>,
|
|||
F: FnOnce() -> Result<Vec<Scalar>, SynthesisError>,
|
|||
{
|
|||
let values_cell = f();
|
|||
let mut value = None;
|
|||
let mut limb_values = None;
|
|||
let limbs = (0..n_limbs)
|
|||
.map(|limb_i| {
|
|||
cs.alloc(
|
|||
|| format!("limb {}", limb_i),
|
|||
|| match values_cell {
|
|||
Ok(ref vs) => {
|
|||
if vs.len() != n_limbs {
|
|||
eprintln!("Values do not match stated limb count");
|
|||
return Err(SynthesisError::Unsatisfiable);
|
|||
}
|
|||
if value.is_none() {
|
|||
value = Some(limbs_to_nat::<Scalar, _, _>(vs.iter(), limb_width));
|
|||
}
|
|||
if limb_values.is_none() {
|
|||
limb_values = Some(vs.clone());
|
|||
}
|
|||
Ok(vs[limb_i])
|
|||
}
|
|||
// Hack b/c SynthesisError and io::Error don't implement Clone
|
|||
Err(ref e) => Err(SynthesisError::from(std::io::Error::new(
|
|||
std::io::ErrorKind::Other,
|
|||
format!("{}", e),
|
|||
))),
|
|||
},
|
|||
)
|
|||
.map(|v| LinearCombination::zero() + v)
|
|||
})
|
|||
.collect::<Result<Vec<_>, _>>()?;
|
|||
Ok(Self {
|
|||
value,
|
|||
limb_values,
|
|||
limbs,
|
|||
params: BigNatParams {
|
|||
min_bits: 0,
|
|||
n_limbs,
|
|||
max_word: max_word.unwrap_or_else(|| int_with_n_ones(limb_width)),
|
|||
limb_width,
|
|||
},
|
|||
})
|
|||
}
|
|||
|
|||
/// Allocates a `BigNat` in the circuit with `n_limbs` limbs of width `limb_width` each.
|
|||
/// The `max_word` is gauranteed to be `(2 << limb_width) - 1`.
|
|||
/// The value is provided by a closure returning a natural number.
|
|||
pub fn alloc_from_nat<CS, F>(
|
|||
mut cs: CS,
|
|||
f: F,
|
|||
limb_width: usize,
|
|||
n_limbs: usize,
|
|||
) -> Result<Self, SynthesisError>
|
|||
where
|
|||
CS: ConstraintSystem<Scalar>,
|
|||
F: FnOnce() -> Result<BigInt, SynthesisError>,
|
|||
{
|
|||
let all_values_cell =
|
|||
f().and_then(|v| Ok((nat_to_limbs::<Scalar>(&v, limb_width, n_limbs)?, v)));
|
|||
let mut value = None;
|
|||
let mut limb_values = Vec::new();
|
|||
let limbs = (0..n_limbs)
|
|||
.map(|limb_i| {
|
|||
cs.alloc(
|
|||
|| format!("limb {}", limb_i),
|
|||
|| match all_values_cell {
|
|||
Ok((ref vs, ref v)) => {
|
|||
if value.is_none() {
|
|||
value = Some(v.clone());
|
|||
}
|
|||
limb_values.push(vs[limb_i]);
|
|||
Ok(vs[limb_i])
|
|||
}
|
|||
// Hack b/c SynthesisError and io::Error don't implement Clone
|
|||
Err(ref e) => Err(SynthesisError::from(std::io::Error::new(
|
|||
std::io::ErrorKind::Other,
|
|||
format!("{}", e),
|
|||
))),
|
|||
},
|
|||
)
|
|||
.map(|v| LinearCombination::zero() + v)
|
|||
})
|
|||
.collect::<Result<Vec<_>, _>>()?;
|
|||
Ok(Self {
|
|||
value,
|
|||
limb_values: if !limb_values.is_empty() {
|
|||
Some(limb_values)
|
|||
} else {
|
|||
None
|
|||
},
|
|||
limbs,
|
|||
params: BigNatParams::new(limb_width, n_limbs),
|
|||
})
|
|||
}
|
|||
|
|||
/// Allocates a `BigNat` in the circuit with `n_limbs` limbs of width `limb_width` each.
|
|||
/// The `max_word` is gauranteed to be `(2 << limb_width) - 1`.
|
|||
/// The value is provided by an allocated number
|
|||
pub fn from_num<CS: ConstraintSystem<Scalar>>(
|
|||
mut cs: CS,
|
|||
n: Num<Scalar>,
|
|||
limb_width: usize,
|
|||
n_limbs: usize,
|
|||
) -> Result<Self, SynthesisError> {
|
|||
let bignat = Self::alloc_from_nat(
|
|||
cs.namespace(|| "bignat"),
|
|||
|| {
|
|||
Ok({
|
|||
n.value
|
|||
.as_ref()
|
|||
.map(|n| f_to_nat(n))
|
|||
.ok_or(SynthesisError::AssignmentMissing)?
|
|||
})
|
|||
},
|
|||
limb_width,
|
|||
n_limbs,
|
|||
)?;
|
|||
|
|||
// check if bignat equals n
|
|||
// (1) decompose `bignat` into a bitvector `bv`
|
|||
let bv = bignat.decompose(cs.namespace(|| "bv"))?;
|
|||
// (2) recompose bits and check if it equals n
|
|||
n.is_equal(cs.namespace(|| "n"), &bv)?;
|
|||
|
|||
Ok(bignat)
|
|||
}
|
|||
|
|||
pub fn as_limbs<CS: ConstraintSystem<Scalar>>(&self) -> Vec<Num<Scalar>> {
|
|||
let mut limbs = Vec::new();
|
|||
for (i, lc) in self.limbs.iter().enumerate() {
|
|||
limbs.push(Num::new(
|
|||
self.limb_values.as_ref().map(|vs| vs[i]),
|
|||
lc.clone(),
|
|||
));
|
|||
}
|
|||
limbs
|
|||
}
|
|||
|
|||
pub fn assert_well_formed<CS: ConstraintSystem<Scalar>>(
|
|||
&self,
|
|||
mut cs: CS,
|
|||
) -> Result<(), SynthesisError> {
|
|||
// swap the option and iterator
|
|||
let limb_values_split =
|
|||
(0..self.limbs.len()).map(|i| self.limb_values.as_ref().map(|vs| vs[i]));
|
|||
for (i, (limb, limb_value)) in self.limbs.iter().zip(limb_values_split).enumerate() {
|
|||
Num::new(limb_value, limb.clone())
|
|||
.fits_in_bits(cs.namespace(|| format!("{}", i)), self.params.limb_width)?;
|
|||
}
|
|||
Ok(())
|
|||
}
|
|||
|
|||
/// Break `self` up into a bit-vector.
|
|||
pub fn decompose<CS: ConstraintSystem<Scalar>>(
|
|||
&self,
|
|||
mut cs: CS,
|
|||
) -> Result<Bitvector<Scalar>, SynthesisError> {
|
|||
let limb_values_split =
|
|||
(0..self.limbs.len()).map(|i| self.limb_values.as_ref().map(|vs| vs[i]));
|
|||
let bitvectors: Vec<Bitvector<Scalar>> = self
|
|||
.limbs
|
|||
.iter()
|
|||
.zip(limb_values_split)
|
|||
.enumerate()
|
|||
.map(|(i, (limb, limb_value))| {
|
|||
Num::new(limb_value, limb.clone()).decompose(
|
|||
cs.namespace(|| format!("subdecmop {}", i)),
|
|||
self.params.limb_width,
|
|||
)
|
|||
})
|
|||
.collect::<Result<Vec<_>, _>>()?;
|
|||
let mut bits = Vec::new();
|
|||
let mut values = Vec::new();
|
|||
let mut allocations = Vec::new();
|
|||
for bv in bitvectors {
|
|||
bits.extend(bv.bits);
|
|||
if let Some(vs) = bv.values {
|
|||
values.extend(vs)
|
|||
};
|
|||
allocations.extend(bv.allocations);
|
|||
}
|
|||
let values = if !values.is_empty() {
|
|||
Some(values)
|
|||
} else {
|
|||
None
|
|||
};
|
|||
Ok(Bitvector {
|
|||
bits,
|
|||
values,
|
|||
allocations,
|
|||
})
|
|||
}
|
|||
|
|||
pub fn enforce_limb_width_agreement(
|
|||
&self,
|
|||
other: &Self,
|
|||
location: &str,
|
|||
) -> Result<usize, SynthesisError> {
|
|||
if self.params.limb_width == other.params.limb_width {
|
|||
Ok(self.params.limb_width)
|
|||
} else {
|
|||
eprintln!(
|
|||
"Limb widths {}, {}, do not agree at {}",
|
|||
self.params.limb_width, other.params.limb_width, location
|
|||
);
|
|||
Err(SynthesisError::Unsatisfiable)
|
|||
}
|
|||
}
|
|||
|
|||
pub fn from_poly(poly: Polynomial<Scalar>, limb_width: usize, max_word: BigInt) -> Self {
|
|||
Self {
|
|||
params: BigNatParams {
|
|||
min_bits: 0,
|
|||
max_word,
|
|||
n_limbs: poly.coefficients.len(),
|
|||
limb_width,
|
|||
},
|
|||
limbs: poly.coefficients,
|
|||
value: poly
|
|||
.values
|
|||
.as_ref()
|
|||
.map(|limb_values| limbs_to_nat::<Scalar, _, _>(limb_values.iter(), limb_width)),
|
|||
limb_values: poly.values,
|
|||
}
|
|||
}
|
|||
|
|||
/// Constrain `self` to be equal to `other`, after carrying both.
|
|||
pub fn equal_when_carried<CS: ConstraintSystem<Scalar>>(
|
|||
&self,
|
|||
mut cs: CS,
|
|||
other: &Self,
|
|||
) -> Result<(), SynthesisError> {
|
|||
self.enforce_limb_width_agreement(other, "equal_when_carried")?;
|
|||
|
|||
// We'll propegate carries over the first `n` limbs.
|
|||
let n = min(self.limbs.len(), other.limbs.len());
|
|||
let target_base = BigInt::from(1u8) << self.params.limb_width as u32;
|
|||
let mut accumulated_extra = BigInt::from(0usize);
|
|||
let max_word = std::cmp::max(&self.params.max_word, &other.params.max_word);
|
|||
let carry_bits = (((max_word.to_f64().unwrap() * 2.0).log2() - self.params.limb_width as f64)
|
|||
.ceil()
|
|||
+ 0.1) as usize;
|
|||
let mut carry_in = Num::new(Some(Scalar::zero()), LinearCombination::zero());
|
|||
|
|||
for i in 0..n {
|
|||
let carry = Num::alloc(cs.namespace(|| format!("carry value {}", i)), || {
|
|||
Ok(
|
|||
nat_to_f(
|
|||
&((f_to_nat(&self.limb_values.grab()?[i])
|
|||
+ f_to_nat(&carry_in.value.unwrap())
|
|||
+ max_word
|
|||
- f_to_nat(&other.limb_values.grab()?[i]))
|
|||
/ &target_base),
|
|||
)
|
|||
.unwrap(),
|
|||
)
|
|||
})?;
|
|||
accumulated_extra += max_word;
|
|||
|
|||
cs.enforce(
|
|||
|| format!("carry {}", i),
|
|||
|lc| lc,
|
|||
|lc| lc,
|
|||
|lc| {
|
|||
lc + &carry_in.num + &self.limbs[i] - &other.limbs[i]
|
|||
+ (nat_to_f(max_word).unwrap(), CS::one())
|
|||
- (nat_to_f(&target_base).unwrap(), &carry.num)
|
|||
- (
|
|||
nat_to_f(&(&accumulated_extra % &target_base)).unwrap(),
|
|||
CS::one(),
|
|||
)
|
|||
},
|
|||
);
|
|||
|
|||
accumulated_extra /= &target_base;
|
|||
|
|||
if i < n - 1 {
|
|||
carry.fits_in_bits(cs.namespace(|| format!("carry {} decomp", i)), carry_bits)?;
|
|||
} else {
|
|||
cs.enforce(
|
|||
|| format!("carry {} is out", i),
|
|||
|lc| lc,
|
|||
|lc| lc,
|
|||
|lc| lc + &carry.num - (nat_to_f(&accumulated_extra).unwrap(), CS::one()),
|
|||
);
|
|||
}
|
|||
carry_in = carry;
|
|||
}
|
|||
|
|||
for (i, zero_limb) in self.limbs.iter().enumerate().skip(n) {
|
|||
cs.enforce(
|
|||
|| format!("zero self {}", i),
|
|||
|lc| lc,
|
|||
|lc| lc,
|
|||
|lc| lc + zero_limb,
|
|||
);
|
|||
}
|
|||
for (i, zero_limb) in other.limbs.iter().enumerate().skip(n) {
|
|||
cs.enforce(
|
|||
|| format!("zero other {}", i),
|
|||
|lc| lc,
|
|||
|lc| lc,
|
|||
|lc| lc + zero_limb,
|
|||
);
|
|||
}
|
|||
Ok(())
|
|||
}
|
|||
|
|||
/// Constrain `self` to be equal to `other`, after carrying both.
|
|||
/// Uses regrouping internally to take full advantage of the field size and reduce the amount
|
|||
/// of carrying.
|
|||
pub fn equal_when_carried_regroup<CS: ConstraintSystem<Scalar>>(
|
|||
&self,
|
|||
mut cs: CS,
|
|||
other: &Self,
|
|||
) -> Result<(), SynthesisError> {
|
|||
self.enforce_limb_width_agreement(other, "equal_when_carried_regroup")?;
|
|||
let max_word = std::cmp::max(&self.params.max_word, &other.params.max_word);
|
|||
let carry_bits = (((max_word.to_f64().unwrap() * 2.0).log2() - self.params.limb_width as f64)
|
|||
.ceil()
|
|||
+ 0.1) as usize;
|
|||
let limbs_per_group = (Scalar::CAPACITY as usize - carry_bits) / self.params.limb_width;
|
|||
let self_grouped = self.group_limbs(limbs_per_group);
|
|||
let other_grouped = other.group_limbs(limbs_per_group);
|
|||
self_grouped.equal_when_carried(cs.namespace(|| "grouped"), &other_grouped)
|
|||
}
|
|||
|
|||
pub fn add<CS: ConstraintSystem<Scalar>>(
|
|||
&self,
|
|||
other: &Self,
|
|||
) -> Result<BigNat<Scalar>, SynthesisError> {
|
|||
self.enforce_limb_width_agreement(other, "add")?;
|
|||
let n_limbs = max(self.params.n_limbs, other.params.n_limbs);
|
|||
let max_word = &self.params.max_word + &other.params.max_word;
|
|||
let limbs: Vec<LinearCombination<Scalar>> = (0..n_limbs)
|
|||
.map(|i| match (self.limbs.get(i), other.limbs.get(i)) {
|
|||
(Some(a), Some(b)) => a.clone() + b,
|
|||
(Some(a), None) => a.clone(),
|
|||
(None, Some(b)) => b.clone(),
|
|||
(None, None) => unreachable!(),
|
|||
})
|
|||
.collect();
|
|||
let limb_values: Option<Vec<Scalar>> = self.limb_values.as_ref().and_then(|x| {
|
|||
other.limb_values.as_ref().map(|y| {
|
|||
(0..n_limbs)
|
|||
.map(|i| match (x.get(i), y.get(i)) {
|
|||
(Some(a), Some(b)) => {
|
|||
let mut t = *a;
|
|||
t.add_assign(b);
|
|||
t
|
|||
}
|
|||
(Some(a), None) => *a,
|
|||
(None, Some(a)) => *a,
|
|||
(None, None) => unreachable!(),
|
|||
})
|
|||
.collect()
|
|||
})
|
|||
});
|
|||
let value = self
|
|||
.value
|
|||
.as_ref()
|
|||
.and_then(|x| other.value.as_ref().map(|y| x + y));
|
|||
Ok(Self {
|
|||
limb_values,
|
|||
value,
|
|||
limbs,
|
|||
params: BigNatParams {
|
|||
min_bits: max(self.params.min_bits, other.params.min_bits),
|
|||
n_limbs,
|
|||
max_word,
|
|||
limb_width: self.params.limb_width,
|
|||
},
|
|||
})
|
|||
}
|
|||
|
|||
/// Compute a `BigNat` contrained to be equal to `self * other % modulus`.
|
|||
pub fn mult_mod<CS: ConstraintSystem<Scalar>>(
|
|||
&self,
|
|||
mut cs: CS,
|
|||
other: &Self,
|
|||
modulus: &Self,
|
|||
) -> Result<(BigNat<Scalar>, BigNat<Scalar>), SynthesisError> {
|
|||
self.enforce_limb_width_agreement(other, "mult_mod")?;
|
|||
let limb_width = self.params.limb_width;
|
|||
let quotient_bits = (self.n_bits() + other.n_bits()).saturating_sub(modulus.params.min_bits);
|
|||
let quotient_limbs = quotient_bits.saturating_sub(1) / limb_width + 1;
|
|||
let quotient = BigNat::alloc_from_nat(
|
|||
cs.namespace(|| "quotient"),
|
|||
|| {
|
|||
Ok({
|
|||
let mut x = self.value.grab()?.clone();
|
|||
x *= other.value.grab()?;
|
|||
x /= modulus.value.grab()?;
|
|||
x
|
|||
})
|
|||
},
|
|||
self.params.limb_width,
|
|||
quotient_limbs,
|
|||
)?;
|
|||
quotient.assert_well_formed(cs.namespace(|| "quotient rangecheck"))?;
|
|||
let remainder = BigNat::alloc_from_nat(
|
|||
cs.namespace(|| "remainder"),
|
|||
|| {
|
|||
Ok({
|
|||
let mut x = self.value.grab()?.clone();
|
|||
x *= other.value.grab()?;
|
|||
x %= modulus.value.grab()?;
|
|||
x
|
|||
})
|
|||
},
|
|||
self.params.limb_width,
|
|||
modulus.limbs.len(),
|
|||
)?;
|
|||
remainder.assert_well_formed(cs.namespace(|| "remainder rangecheck"))?;
|
|||
let a_poly = Polynomial::from(self.clone());
|
|||
let b_poly = Polynomial::from(other.clone());
|
|||
let mod_poly = Polynomial::from(modulus.clone());
|
|||
let q_poly = Polynomial::from(quotient.clone());
|
|||
let r_poly = Polynomial::from(remainder.clone());
|
|||
|
|||
// a * b
|
|||
let left = a_poly.alloc_product(cs.namespace(|| "left"), &b_poly)?;
|
|||
let right_product = q_poly.alloc_product(cs.namespace(|| "right_product"), &mod_poly)?;
|
|||
// q * m + r
|
|||
let right = right_product.sum(&r_poly);
|
|||
|
|||
let left_max_word = {
|
|||
let mut x = BigInt::from(min(self.limbs.len(), other.limbs.len()));
|
|||
x *= &self.params.max_word;
|
|||
x *= &other.params.max_word;
|
|||
x
|
|||
};
|
|||
let right_max_word = {
|
|||
let mut x = BigInt::from(std::cmp::min(quotient.limbs.len(), modulus.limbs.len()));
|
|||
x *= "ient.params.max_word;
|
|||
x *= &modulus.params.max_word;
|
|||
x += &remainder.params.max_word;
|
|||
x
|
|||
};
|
|||
|
|||
let left_int = BigNat::from_poly(left, limb_width, left_max_word);
|
|||
let right_int = BigNat::from_poly(right, limb_width, right_max_word);
|
|||
left_int.equal_when_carried_regroup(cs.namespace(|| "carry"), &right_int)?;
|
|||
Ok((quotient, remainder))
|
|||
}
|
|||
|
|||
/// Compute a `BigNat` contrained to be equal to `self * other % modulus`.
|
|||
pub fn red_mod<CS: ConstraintSystem<Scalar>>(
|
|||
&self,
|
|||
mut cs: CS,
|
|||
modulus: &Self,
|
|||
) -> Result<BigNat<Scalar>, SynthesisError> {
|
|||
self.enforce_limb_width_agreement(modulus, "red_mod")?;
|
|||
let limb_width = self.params.limb_width;
|
|||
let quotient_bits = self.n_bits().saturating_sub(modulus.params.min_bits);
|
|||
let quotient_limbs = quotient_bits.saturating_sub(1) / limb_width + 1;
|
|||
let quotient = BigNat::alloc_from_nat(
|
|||
cs.namespace(|| "quotient"),
|
|||
|| Ok(self.value.grab()? / modulus.value.grab()?),
|
|||
self.params.limb_width,
|
|||
quotient_limbs,
|
|||
)?;
|
|||
quotient.assert_well_formed(cs.namespace(|| "quotient rangecheck"))?;
|
|||
let remainder = BigNat::alloc_from_nat(
|
|||
cs.namespace(|| "remainder"),
|
|||
|| Ok(self.value.grab()? % modulus.value.grab()?),
|
|||
self.params.limb_width,
|
|||
modulus.limbs.len(),
|
|||
)?;
|
|||
remainder.assert_well_formed(cs.namespace(|| "remainder rangecheck"))?;
|
|||
let mod_poly = Polynomial::from(modulus.clone());
|
|||
let q_poly = Polynomial::from(quotient.clone());
|
|||
let r_poly = Polynomial::from(remainder.clone());
|
|||
|
|||
// q * m + r
|
|||
let right_product = q_poly.alloc_product(cs.namespace(|| "right_product"), &mod_poly)?;
|
|||
let right = right_product.sum(&r_poly);
|
|||
|
|||
let right_max_word = {
|
|||
let mut x = BigInt::from(std::cmp::min(quotient.limbs.len(), modulus.limbs.len()));
|
|||
x *= "ient.params.max_word;
|
|||
x *= &modulus.params.max_word;
|
|||
x += &remainder.params.max_word;
|
|||
x
|
|||
};
|
|||
|
|||
let right_int = BigNat::from_poly(right, limb_width, right_max_word);
|
|||
self.equal_when_carried_regroup(cs.namespace(|| "carry"), &right_int)?;
|
|||
Ok(remainder)
|
|||
}
|
|||
|
|||
/// Combines limbs into groups.
|
|||
pub fn group_limbs(&self, limbs_per_group: usize) -> BigNat<Scalar> {
|
|||
let n_groups = (self.limbs.len() - 1) / limbs_per_group + 1;
|
|||
let limb_values = self.limb_values.as_ref().map(|vs| {
|
|||
let mut values: Vec<Scalar> = vec![Scalar::zero(); n_groups];
|
|||
let mut shift = Scalar::one();
|
|||
let limb_block = (0..self.params.limb_width).fold(Scalar::one(), |mut l, _| {
|
|||
l = l.double();
|
|||
l
|
|||
});
|
|||
for (i, v) in vs.iter().enumerate() {
|
|||
if i % limbs_per_group == 0 {
|
|||
shift = Scalar::one();
|
|||
}
|
|||
let mut a = shift;
|
|||
a *= v;
|
|||
values[i / limbs_per_group].add_assign(&a);
|
|||
shift.mul_assign(&limb_block);
|
|||
}
|
|||
values
|
|||
});
|
|||
let limbs = {
|
|||
let mut limbs: Vec<LinearCombination<Scalar>> = vec![LinearCombination::zero(); n_groups];
|
|||
let mut shift = Scalar::one();
|
|||
let limb_block = (0..self.params.limb_width).fold(Scalar::one(), |mut l, _| {
|
|||
l = l.double();
|
|||
l
|
|||
});
|
|||
for (i, limb) in self.limbs.iter().enumerate() {
|
|||
if i % limbs_per_group == 0 {
|
|||
shift = Scalar::one();
|
|||
}
|
|||
limbs[i / limbs_per_group] =
|
|||
std::mem::replace(&mut limbs[i / limbs_per_group], LinearCombination::zero())
|
|||
+ (shift, limb);
|
|||
shift.mul_assign(&limb_block);
|
|||
}
|
|||
limbs
|
|||
};
|
|||
let max_word = (0..limbs_per_group).fold(BigInt::from(0u8), |mut acc, i| {
|
|||
acc.set_bit((i * self.params.limb_width) as u64, true);
|
|||
acc
|
|||
}) * &self.params.max_word;
|
|||
BigNat {
|
|||
params: BigNatParams {
|
|||
min_bits: self.params.min_bits,
|
|||
limb_width: self.params.limb_width * limbs_per_group,
|
|||
n_limbs: limbs.len(),
|
|||
max_word,
|
|||
},
|
|||
limbs,
|
|||
limb_values,
|
|||
value: self.value.clone(),
|
|||
}
|
|||
}
|
|||
|
|||
pub fn n_bits(&self) -> usize {
|
|||
assert!(self.params.n_limbs > 0);
|
|||
self.params.limb_width * (self.params.n_limbs - 1) + self.params.max_word.bits() as usize
|
|||
}
|
|||
}
|
|||
|
|||
pub struct Polynomial<Scalar: PrimeField> {
|
|||
pub coefficients: Vec<LinearCombination<Scalar>>,
|
|||
pub values: Option<Vec<Scalar>>,
|
|||
}
|
|||
|
|||
impl<Scalar: PrimeField> Polynomial<Scalar> {
|
|||
pub fn alloc_product<CS: ConstraintSystem<Scalar>>(
|
|||
&self,
|
|||
mut cs: CS,
|
|||
other: &Self,
|
|||
) -> Result<Polynomial<Scalar>, SynthesisError> {
|
|||
let n_product_coeffs = self.coefficients.len() + other.coefficients.len() - 1;
|
|||
let values = self.values.as_ref().and_then(|self_vs| {
|
|||
other.values.as_ref().map(|other_vs| {
|
|||
let mut values: Vec<Scalar> = std::iter::repeat_with(Scalar::zero)
|
|||
.take(n_product_coeffs)
|
|||
.collect();
|
|||
for (self_i, self_v) in self_vs.iter().enumerate() {
|
|||
for (other_i, other_v) in other_vs.iter().enumerate() {
|
|||
let mut v = *self_v;
|
|||
v.mul_assign(other_v);
|
|||
values[self_i + other_i].add_assign(&v);
|
|||
}
|
|||
}
|
|||
values
|
|||
})
|
|||
});
|
|||
let coefficients = (0..n_product_coeffs)
|
|||
.map(|i| {
|
|||
Ok(
|
|||
LinearCombination::zero()
|
|||
+ cs.alloc(|| format!("prod {}", i), || Ok(values.grab()?[i]))?,
|
|||
)
|
|||
})
|
|||
.collect::<Result<Vec<LinearCombination<Scalar>>, SynthesisError>>()?;
|
|||
let product = Polynomial {
|
|||
coefficients,
|
|||
values,
|
|||
};
|
|||
let one = Scalar::one();
|
|||
let mut x = Scalar::zero();
|
|||
for _ in 1..(n_product_coeffs + 1) {
|
|||
x.add_assign(&one);
|
|||
cs.enforce(
|
|||
|| format!("pointwise product @ {:?}", x),
|
|||
|lc| {
|
|||
let mut i = Scalar::one();
|
|||
self.coefficients.iter().fold(lc, |lc, c| {
|
|||
let r = lc + (i, c);
|
|||
i.mul_assign(&x);
|
|||
r
|
|||
})
|
|||
},
|
|||
|lc| {
|
|||
let mut i = Scalar::one();
|
|||
other.coefficients.iter().fold(lc, |lc, c| {
|
|||
let r = lc + (i, c);
|
|||
i.mul_assign(&x);
|
|||
r
|
|||
})
|
|||
},
|
|||
|lc| {
|
|||
let mut i = Scalar::one();
|
|||
product.coefficients.iter().fold(lc, |lc, c| {
|
|||
let r = lc + (i, c);
|
|||
i.mul_assign(&x);
|
|||
r
|
|||
})
|
|||
},
|
|||
)
|
|||
}
|
|||
Ok(product)
|
|||
}
|
|||
|
|||
pub fn sum(&self, other: &Self) -> Self {
|
|||
let n_coeffs = max(self.coefficients.len(), other.coefficients.len());
|
|||
let values = self.values.as_ref().and_then(|self_vs| {
|
|||
other.values.as_ref().map(|other_vs| {
|
|||
(0..n_coeffs)
|
|||
.map(|i| {
|
|||
let mut s = Scalar::zero();
|
|||
if i < self_vs.len() {
|
|||
s.add_assign(&self_vs[i]);
|
|||
}
|
|||
if i < other_vs.len() {
|
|||
s.add_assign(&other_vs[i]);
|
|||
}
|
|||
s
|
|||
})
|
|||
.collect()
|
|||
})
|
|||
});
|
|||
let coefficients = (0..n_coeffs)
|
|||
.map(|i| {
|
|||
let mut lc = LinearCombination::zero();
|
|||
if i < self.coefficients.len() {
|
|||
lc = lc + &self.coefficients[i];
|
|||
}
|
|||
if i < other.coefficients.len() {
|
|||
lc = lc + &other.coefficients[i];
|
|||
}
|
|||
lc
|
|||
})
|
|||
.collect();
|
|||
Polynomial {
|
|||
coefficients,
|
|||
values,
|
|||
}
|
|||
}
|
|||
}
|
|||
|
|||
#[cfg(test)]
|
|||
mod tests {
|
|||
use super::*;
|
|||
use bellperson::Circuit;
|
|||
|
|||
pub struct PolynomialMultiplier<Scalar: PrimeField> {
|
|||
pub a: Vec<Scalar>,
|
|||
pub b: Vec<Scalar>,
|
|||
}
|
|||
|
|||
impl<Scalar: PrimeField> Circuit<Scalar> for PolynomialMultiplier<Scalar> {
|
|||
fn synthesize<CS: ConstraintSystem<Scalar>>(self, cs: &mut CS) -> Result<(), SynthesisError> {
|
|||
let a = Polynomial {
|
|||
coefficients: self
|
|||
.a
|
|||
.iter()
|
|||
.enumerate()
|
|||
.map(|(i, x)| {
|
|||
Ok(LinearCombination::zero() + cs.alloc(|| format!("coeff_a {}", i), || Ok(*x))?)
|
|||
})
|
|||
.collect::<Result<Vec<LinearCombination<Scalar>>, SynthesisError>>()?,
|
|||
values: Some(self.a),
|
|||
};
|
|||
let b = Polynomial {
|
|||
coefficients: self
|
|||
.b
|
|||
.iter()
|
|||
.enumerate()
|
|||
.map(|(i, x)| {
|
|||
Ok(LinearCombination::zero() + cs.alloc(|| format!("coeff_b {}", i), || Ok(*x))?)
|
|||
})
|
|||
.collect::<Result<Vec<LinearCombination<Scalar>>, SynthesisError>>()?,
|
|||
values: Some(self.b),
|
|||
};
|
|||
let _prod = a.alloc_product(cs.namespace(|| "product"), &b)?;
|
|||
Ok(())
|
|||
}
|
|||
}
|
|||
}
|
|||
@ -0,0 +1,39 @@ |
|||
//! This module implements various gadgets necessary for doing non-native arithmetic
|
|||
//! Code in this module is adapted from [bellman-bignat](https://github.com/alex-ozdemir/bellman-bignat), which is licenced under MIT
|
|||
|
|||
use bellperson::SynthesisError;
|
|||
use ff::PrimeField;
|
|||
|
|||
trait OptionExt<T> {
|
|||
fn grab(&self) -> Result<&T, SynthesisError>;
|
|||
fn grab_mut(&mut self) -> Result<&mut T, SynthesisError>;
|
|||
}
|
|||
|
|||
impl<T> OptionExt<T> for Option<T> {
|
|||
fn grab(&self) -> Result<&T, SynthesisError> {
|
|||
self.as_ref().ok_or(SynthesisError::AssignmentMissing)
|
|||
}
|
|||
fn grab_mut(&mut self) -> Result<&mut T, SynthesisError> {
|
|||
self.as_mut().ok_or(SynthesisError::AssignmentMissing)
|
|||
}
|
|||
}
|
|||
|
|||
trait BitAccess {
|
|||
fn get_bit(&self, i: usize) -> Option<bool>;
|
|||
}
|
|||
|
|||
impl<Scalar: PrimeField> BitAccess for Scalar {
|
|||
fn get_bit(&self, i: usize) -> Option<bool> {
|
|||
if i as u32 >= Scalar::NUM_BITS {
|
|||
return None;
|
|||
}
|
|||
|
|||
let (byte_pos, bit_pos) = (i / 8, i % 8);
|
|||
let byte = self.to_repr().as_ref()[byte_pos];
|
|||
let bit = byte >> bit_pos & 1;
|
|||
Some(bit == 1)
|
|||
}
|
|||
}
|
|||
|
|||
pub mod bignat;
|
|||
pub mod util;
|
|||
@ -0,0 +1,261 @@ |
|||
use super::{BitAccess, OptionExt};
|
|||
use bellperson::{
|
|||
gadgets::num::AllocatedNum,
|
|||
{ConstraintSystem, LinearCombination, SynthesisError, Variable},
|
|||
};
|
|||
use byteorder::WriteBytesExt;
|
|||
use ff::PrimeField;
|
|||
use num_bigint::{BigInt, Sign};
|
|||
use std::convert::From;
|
|||
use std::io::{self, Write};
|
|||
|
|||
#[derive(Clone)]
|
|||
/// A representation of a bit
|
|||
pub struct Bit<Scalar: PrimeField> {
|
|||
/// The linear combination which constrain the value of the bit
|
|||
pub bit: LinearCombination<Scalar>,
|
|||
/// The value of the bit (filled at witness-time)
|
|||
pub value: Option<bool>,
|
|||
}
|
|||
|
|||
#[derive(Clone)]
|
|||
/// A representation of a bit-vector
|
|||
pub struct Bitvector<Scalar: PrimeField> {
|
|||
/// The linear combination which constrain the values of the bits
|
|||
pub bits: Vec<LinearCombination<Scalar>>,
|
|||
/// The value of the bits (filled at witness-time)
|
|||
pub values: Option<Vec<bool>>,
|
|||
/// Allocated bit variables
|
|||
pub allocations: Vec<Bit<Scalar>>,
|
|||
}
|
|||
|
|||
impl<Scalar: PrimeField> Bit<Scalar> {
|
|||
/// Allocate a variable in the constraint system which can only be a
|
|||
/// boolean value.
|
|||
pub fn alloc<CS>(mut cs: CS, value: Option<bool>) -> Result<Self, SynthesisError>
|
|||
where
|
|||
CS: ConstraintSystem<Scalar>,
|
|||
{
|
|||
let var = cs.alloc(
|
|||
|| "boolean",
|
|||
|| {
|
|||
if *value.grab()? {
|
|||
Ok(Scalar::one())
|
|||
} else {
|
|||
Ok(Scalar::zero())
|
|||
}
|
|||
},
|
|||
)?;
|
|||
|
|||
// Constrain: (1 - a) * a = 0
|
|||
// This constrains a to be either 0 or 1.
|
|||
cs.enforce(
|
|||
|| "boolean constraint",
|
|||
|lc| lc + CS::one() - var,
|
|||
|lc| lc + var,
|
|||
|lc| lc,
|
|||
);
|
|||
|
|||
Ok(Self {
|
|||
bit: LinearCombination::zero() + var,
|
|||
value,
|
|||
})
|
|||
}
|
|||
}
|
|||
|
|||
pub struct Num<Scalar: PrimeField> {
|
|||
pub num: LinearCombination<Scalar>,
|
|||
pub value: Option<Scalar>,
|
|||
}
|
|||
|
|||
impl<Scalar: PrimeField> Num<Scalar> {
|
|||
pub fn new(value: Option<Scalar>, num: LinearCombination<Scalar>) -> Self {
|
|||
Self { value, num }
|
|||
}
|
|||
pub fn alloc<CS, F>(mut cs: CS, value: F) -> Result<Self, SynthesisError>
|
|||
where
|
|||
CS: ConstraintSystem<Scalar>,
|
|||
F: FnOnce() -> Result<Scalar, SynthesisError>,
|
|||
{
|
|||
let mut new_value = None;
|
|||
let var = cs.alloc(
|
|||
|| "num",
|
|||
|| {
|
|||
let tmp = value()?;
|
|||
|
|||
new_value = Some(tmp);
|
|||
|
|||
Ok(tmp)
|
|||
},
|
|||
)?;
|
|||
|
|||
Ok(Num {
|
|||
value: new_value,
|
|||
num: LinearCombination::zero() + var,
|
|||
})
|
|||
}
|
|||
|
|||
pub fn fits_in_bits<CS: ConstraintSystem<Scalar>>(
|
|||
&self,
|
|||
mut cs: CS,
|
|||
n_bits: usize,
|
|||
) -> Result<(), SynthesisError> {
|
|||
let v = self.value;
|
|||
|
|||
// Allocate all but the first bit.
|
|||
let bits: Vec<Variable> = (1..n_bits)
|
|||
.map(|i| {
|
|||
cs.alloc(
|
|||
|| format!("bit {}", i),
|
|||
|| {
|
|||
let r = if *v.grab()?.get_bit(i).grab()? {
|
|||
Scalar::one()
|
|||
} else {
|
|||
Scalar::zero()
|
|||
};
|
|||
Ok(r)
|
|||
},
|
|||
)
|
|||
})
|
|||
.collect::<Result<_, _>>()?;
|
|||
|
|||
for (i, v) in bits.iter().enumerate() {
|
|||
cs.enforce(
|
|||
|| format!("{} is bit", i),
|
|||
|lc| lc + *v,
|
|||
|lc| lc + CS::one() - *v,
|
|||
|lc| lc,
|
|||
)
|
|||
}
|
|||
|
|||
// Last bit
|
|||
cs.enforce(
|
|||
|| "last bit",
|
|||
|mut lc| {
|
|||
let mut f = Scalar::one();
|
|||
lc = lc + &self.num;
|
|||
for v in bits.iter() {
|
|||
f = f.double();
|
|||
lc = lc - (f, *v);
|
|||
}
|
|||
lc
|
|||
},
|
|||
|mut lc| {
|
|||
lc = lc + CS::one();
|
|||
let mut f = Scalar::one();
|
|||
lc = lc - &self.num;
|
|||
for v in bits.iter() {
|
|||
f = f.double();
|
|||
lc = lc + (f, *v);
|
|||
}
|
|||
lc
|
|||
},
|
|||
|lc| lc,
|
|||
);
|
|||
Ok(())
|
|||
}
|
|||
|
|||
/// Computes the natural number represented by an array of bits.
|
|||
/// Checks if the natural number equals `self`
|
|||
pub fn is_equal<CS: ConstraintSystem<Scalar>>(
|
|||
&self,
|
|||
mut cs: CS,
|
|||
other: &Bitvector<Scalar>,
|
|||
) -> Result<(), SynthesisError> {
|
|||
let allocations = other.allocations.clone();
|
|||
let mut f = Scalar::one();
|
|||
let sum = allocations
|
|||
.iter()
|
|||
.fold(LinearCombination::zero(), |lc, bit| {
|
|||
let l = lc + (f, &bit.bit);
|
|||
f = f.double();
|
|||
l
|
|||
});
|
|||
let sum_lc = LinearCombination::zero() + &self.num - ∑
|
|||
cs.enforce(|| "sum", |lc| lc + &sum_lc, |lc| lc + CS::one(), |lc| lc);
|
|||
Ok(())
|
|||
}
|
|||
|
|||
/// Compute the natural number represented by an array of limbs.
|
|||
/// The limbs are assumed to be based the `limb_width` power of 2.
|
|||
/// Low-index bits are low-order
|
|||
pub fn decompose<CS: ConstraintSystem<Scalar>>(
|
|||
&self,
|
|||
mut cs: CS,
|
|||
n_bits: usize,
|
|||
) -> Result<Bitvector<Scalar>, SynthesisError> {
|
|||
let values: Option<Vec<bool>> = self.value.as_ref().map(|v| {
|
|||
let num = *v;
|
|||
(0..n_bits).map(|i| num.get_bit(i).unwrap()).collect()
|
|||
});
|
|||
let allocations: Vec<Bit<Scalar>> = (0..n_bits)
|
|||
.map(|bit_i| {
|
|||
Bit::alloc(
|
|||
cs.namespace(|| format!("bit{}", bit_i)),
|
|||
values.as_ref().map(|vs| vs[bit_i]),
|
|||
)
|
|||
})
|
|||
.collect::<Result<Vec<_>, _>>()?;
|
|||
let mut f = Scalar::one();
|
|||
let sum = allocations
|
|||
.iter()
|
|||
.fold(LinearCombination::zero(), |lc, bit| {
|
|||
let l = lc + (f, &bit.bit);
|
|||
f = f.double();
|
|||
l
|
|||
});
|
|||
let sum_lc = LinearCombination::zero() + &self.num - ∑
|
|||
cs.enforce(|| "sum", |lc| lc + &sum_lc, |lc| lc + CS::one(), |lc| lc);
|
|||
let bits: Vec<LinearCombination<Scalar>> = allocations
|
|||
.clone()
|
|||
.into_iter()
|
|||
.map(|a| LinearCombination::zero() + &a.bit)
|
|||
.collect();
|
|||
Ok(Bitvector {
|
|||
allocations,
|
|||
values,
|
|||
bits,
|
|||
})
|
|||
}
|
|||
|
|||
pub fn as_allocated_num<CS: ConstraintSystem<Scalar>>(
|
|||
&self,
|
|||
mut cs: CS,
|
|||
) -> Result<AllocatedNum<Scalar>, SynthesisError> {
|
|||
let new = AllocatedNum::alloc(cs.namespace(|| "alloc"), || Ok(*self.value.grab()?))?;
|
|||
cs.enforce(
|
|||
|| "eq",
|
|||
|lc| lc,
|
|||
|lc| lc,
|
|||
|lc| lc + new.get_variable() - &self.num,
|
|||
);
|
|||
Ok(new)
|
|||
}
|
|||
}
|
|||
|
|||
impl<Scalar: PrimeField> From<AllocatedNum<Scalar>> for Num<Scalar> {
|
|||
fn from(a: AllocatedNum<Scalar>) -> Self {
|
|||
Self::new(a.get_value(), LinearCombination::zero() + a.get_variable())
|
|||
}
|
|||
}
|
|||
|
|||
fn write_be<F: PrimeField, W: Write>(f: &F, mut writer: W) -> io::Result<()> {
|
|||
for digit in f.to_repr().as_ref().iter().rev() {
|
|||
writer.write_u8(*digit)?;
|
|||
}
|
|||
|
|||
Ok(())
|
|||
}
|
|||
|
|||
/// Convert a field element to a natural number
|
|||
pub fn f_to_nat<Scalar: PrimeField>(f: &Scalar) -> BigInt {
|
|||
let mut s = Vec::new();
|
|||
write_be(f, &mut s).unwrap(); // f.to_repr().write_be(&mut s).unwrap();
|
|||
BigInt::from_bytes_le(Sign::Plus, f.to_repr().as_ref())
|
|||
}
|
|||
|
|||
/// Convert a natural number to a field element.
|
|||
/// Returns `None` if the number is too big for the field.
|
|||
pub fn nat_to_f<Scalar: PrimeField>(n: &BigInt) -> Option<Scalar> {
|
|||
Scalar::from_str_vartime(&format!("{}", n))
|
|||
}
|
|||