arnaucube/ark-r1cs-std
1
0
Fork 0
mirror of https://github.com/arnaucube/ark-r1cs-std.git synced 2026-01-08 15:01:29 +01:00
Code Issues Projects Releases Wiki Activity

Experimental features

Browse Source
This commit is contained in:
winderica
2024-06-01 03:57:18 +08:00
parent 65e7fb1ef1
commit ee8a42312b
8 changed files with 357 additions and 166 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
Cargo.toml
View File

@@ -87,4 +87,4 @@ ark-mnt4-753 = { git = "https://github.com/arkworks-rs/curves/" }
ark-mnt6-298 = { git = "https://github.com/arkworks-rs/curves/" }
ark-mnt6-753 = { git = "https://github.com/arkworks-rs/curves/" }
ark-pallas = { git = "https://github.com/arkworks-rs/curves/" }
ark-relations = { git = "https://github.com/winderica/snark/", branch = "cp" }
ark-relations = { git = "https://github.com/winderica/snark/", branch = "experimental" }

2
src/alloc.rs
View File

@@ -1,7 +1,7 @@
use crate::Vec;
use ark_ff::Field;
use ark_relations::r1cs::{Namespace, SynthesisError};
use core::borrow::Borrow;
use ark_std::vec::Vec;
/// Describes the mode that a variable should be allocated in within
/// a `ConstraintSystem`.

139
src/boolean/allocated.rs
View File

@@ -1,4 +1,4 @@
use core::borrow::Borrow;
use core::borrow::{Borrow, BorrowMut};
use ark_ff::{Field, PrimeField};
use ark_relations::r1cs::{ConstraintSystemRef, Namespace, SynthesisError, Variable};
@@ -6,7 +6,6 @@ use ark_relations::r1cs::{ConstraintSystemRef, Namespace, SynthesisError, Variab
use crate::{
alloc::{AllocVar, AllocationMode},
select::CondSelectGadget,
Assignment,
};
use super::Boolean;
@@ -22,23 +21,14 @@ use super::Boolean;
pub struct AllocatedBool<F: Field> {
pub(super) variable: Variable,
pub(super) cs: ConstraintSystemRef<F>,
}
pub(crate) fn bool_to_field<F: Field>(val: impl Borrow<bool>) -> F {
F::from(*val.borrow())
pub(super) enable_lc: bool,
pub(super) value: Option<bool>,
}
impl<F: Field> AllocatedBool<F> {
/// Get the assigned value for `self`.
pub fn value(&self) -> Result<bool, SynthesisError> {
let value = self.cs.assigned_value(self.variable).get()?;
if value.is_zero() {
Ok(false)
} else if value.is_one() {
Ok(true)
} else {
unreachable!("Incorrect value assigned: {:?}", value);
}
self.value.ok_or(SynthesisError::AssignmentMissing)
}
/// Get the R1CS variable for `self`.
@@ -52,18 +42,29 @@ impl<F: Field> AllocatedBool<F> {
cs: ConstraintSystemRef<F>,
f: impl FnOnce() -> Result<T, SynthesisError>,
) -> Result<Self, SynthesisError> {
let variable = cs.new_witness_variable(|| f().map(bool_to_field))?;
Ok(Self { variable, cs })
let value = f().map(|b| *b.borrow());
Ok(Self {
variable: cs.new_witness_variable(|| value.map(F::from))?,
enable_lc: cs.should_construct_matrices(),
cs,
value: value.ok(),
})
}
/// Performs an XOR operation over the two operands, returning
/// an `AllocatedBool`.
#[tracing::instrument(target = "r1cs")]
pub fn not(&self) -> Result<Self, SynthesisError> {
let variable = self.cs.new_lc(lc!() + Variable::One - self.variable)?;
let variable = self.cs.new_lc(if self.enable_lc {
lc!() + Variable::One - self.variable
} else {
lc!()
})?;
Ok(Self {
variable,
cs: self.cs.clone(),
value: self.value.map(|v| !v),
enable_lc: self.cs.should_construct_matrices()
})
}
@@ -90,11 +91,15 @@ impl<F: Field> AllocatedBool<F> {
// -2a * b = c - a - b
// 2a * b = a + b - c
// (a + a) * b = a + b - c
self.cs.enforce_constraint(
lc!() + self.variable + self.variable,
lc!() + b.variable,
lc!() + self.variable + b.variable - result.variable,
)?;
if self.enable_lc {
self.cs.enforce_constraint(
lc!() + self.variable + self.variable,
lc!() + b.variable,
lc!() + self.variable + b.variable - result.variable,
)?;
} else {
self.cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(result)
}
@@ -109,11 +114,15 @@ impl<F: Field> AllocatedBool<F> {
// Constrain (a) * (b) = (c), ensuring c is 1 iff
// a AND b are both 1.
self.cs.enforce_constraint(
lc!() + self.variable,
lc!() + b.variable,
lc!() + result.variable,
)?;
if self.enable_lc {
self.cs.enforce_constraint(
lc!() + self.variable,
lc!() + b.variable,
lc!() + result.variable,
)?;
} else {
self.cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(result)
}
@@ -128,11 +137,15 @@ impl<F: Field> AllocatedBool<F> {
// Constrain (1 - a) * (1 - b) = (1 - c), ensuring c is 0 iff
// a and b are both false, and otherwise c is 1.
self.cs.enforce_constraint(
lc!() + Variable::One - self.variable,
lc!() + Variable::One - b.variable,
lc!() + Variable::One - result.variable,
)?;
if self.enable_lc {
self.cs.enforce_constraint(
lc!() + Variable::One - self.variable,
lc!() + Variable::One - b.variable,
lc!() + Variable::One - result.variable,
)?;
} else {
self.cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(result)
}
@@ -146,11 +159,15 @@ impl<F: Field> AllocatedBool<F> {
// Constrain (a) * (1 - b) = (c), ensuring c is 1 iff
// a is true and b is false, and otherwise c is 0.
self.cs.enforce_constraint(
lc!() + self.variable,
lc!() + Variable::One - b.variable,
lc!() + result.variable,
)?;
if self.enable_lc {
self.cs.enforce_constraint(
lc!() + self.variable,
lc!() + Variable::One - b.variable,
lc!() + result.variable,
)?;
} else {
self.cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(result)
}
@@ -164,11 +181,15 @@ impl<F: Field> AllocatedBool<F> {
// Constrain (1 - a) * (1 - b) = (c), ensuring c is 1 iff
// a and b are both false, and otherwise c is 0.
self.cs.enforce_constraint(
lc!() + Variable::One - self.variable,
lc!() + Variable::One - b.variable,
lc!() + result.variable,
)?;
if self.enable_lc {
self.cs.enforce_constraint(
lc!() + Variable::One - self.variable,
lc!() + Variable::One - b.variable,
lc!() + result.variable,
)?;
} else {
self.cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(result)
}
@@ -189,25 +210,37 @@ impl<F: Field> AllocVar<bool, F> for AllocatedBool<F> {
let ns = cs.into();
let cs = ns.cs();
if mode == AllocationMode::Constant {
let variable = if *f()?.borrow() {
Variable::One
} else {
Variable::Zero
};
Ok(Self { variable, cs })
let value = *f()?.borrow();
Ok(Self {
variable: if value { Variable::One } else { Variable::Zero },
enable_lc: cs.should_construct_matrices(),
cs,
value: Some(value),
})
} else {
let value = f().map(|b| *b.borrow());
let variable = if mode == AllocationMode::Input {
cs.new_input_variable(|| f().map(bool_to_field))?
cs.new_input_variable(|| value.map(F::from))?
} else {
cs.new_witness_variable(|| f().map(bool_to_field))?
cs.new_witness_variable(|| value.map(F::from))?
};
let enable_lc = cs.should_construct_matrices();
// Constrain: (1 - a) * a = 0
// This constrains a to be either 0 or 1.
if enable_lc {
cs.enforce_constraint(lc!() + Variable::One - variable, lc!() + variable, lc!())?;
} else {
cs.borrow_mut().unwrap().num_constraints += 1;
}
cs.enforce_constraint(lc!() + Variable::One - variable, lc!() + variable, lc!())?;
Ok(Self { variable, cs })
Ok(Self {
variable,
enable_lc,
cs,
value: value.ok(),
})
}
}
}

71
src/boolean/eq.rs
View File

@@ -1,7 +1,6 @@
use ark_relations::r1cs::SynthesisError;
use crate::boolean::Boolean;
use crate::eq::EqGadget;
use crate::{boolean::Boolean, eq::EqGadget};
use super::*;
@@ -26,24 +25,46 @@ impl<F: Field> EqGadget<F> for Boolean<F> {
use Boolean::*;
let one = Variable::One;
// We will use the following trick: a == b <=> a - b == 0
// This works because a - b == 0 if and only if a = 0 and b = 0, or a = 1 and b = 1,
// which is exactly the definition of a == b.
// This works because a - b == 0 if and only if a = 0 and b = 0, or a = 1 and b
// = 1, which is exactly the definition of a == b.
let difference = match (self, other) {
// 1 == 1; 0 == 0
(Constant(true), Constant(true)) | (Constant(false), Constant(false)) => return Ok(()),
// false != true
(Constant(_), Constant(_)) => return Err(SynthesisError::Unsatisfiable),
// 1 - a
(Constant(true), Var(a)) | (Var(a), Constant(true)) => lc!() + one - a.variable(),
(Constant(true), Var(a)) | (Var(a), Constant(true)) => {
if a.enable_lc {
lc!() + one - a.variable()
} else {
lc!()
}
},
// a - 0 = a
(Constant(false), Var(a)) | (Var(a), Constant(false)) => lc!() + a.variable(),
(Constant(false), Var(a)) | (Var(a), Constant(false)) => {
if a.enable_lc {
lc!() + a.variable()
} else {
lc!()
}
},
// b - a,
(Var(a), Var(b)) => lc!() + b.variable() - a.variable(),
(Var(a), Var(b)) => {
if a.enable_lc || b.enable_lc {
lc!() + b.variable() - a.variable()
} else {
lc!()
}
},
};
if condition != &Constant(false) {
let cs = self.cs().or(other.cs()).or(condition.cs());
cs.enforce_constraint(lc!() + difference, condition.lc(), lc!())?;
if cs.should_construct_matrices() {
cs.enforce_constraint(lc!() + difference, condition.lc(), lc!())?;
} else {
cs.borrow_mut().unwrap().num_constraints += 1;
}
}
Ok(())
}
@@ -57,24 +78,46 @@ impl<F: Field> EqGadget<F> for Boolean<F> {
use Boolean::*;
let one = Variable::One;
// We will use the following trick: a != b <=> a + b == 1
// This works because a + b == 1 if and only if a = 0 and b = 1, or a = 1 and b = 0,
// which is exactly the definition of a != b.
// This works because a + b == 1 if and only if a = 0 and b = 1, or a = 1 and b
// = 0, which is exactly the definition of a != b.
let sum = match (self, other) {
// 1 != 0; 0 != 1
(Constant(true), Constant(false)) | (Constant(false), Constant(true)) => return Ok(()),
// false == false and true == true
(Constant(_), Constant(_)) => return Err(SynthesisError::Unsatisfiable),
// 1 + a
(Constant(true), Var(a)) | (Var(a), Constant(true)) => lc!() + one + a.variable(),
(Constant(true), Var(a)) | (Var(a), Constant(true)) => {
if a.enable_lc {
lc!() + one + a.variable()
} else {
lc!()
}
},
// a + 0 = a
(Constant(false), Var(a)) | (Var(a), Constant(false)) => lc!() + a.variable(),
(Constant(false), Var(a)) | (Var(a), Constant(false)) => {
if a.enable_lc {
lc!() + a.variable()
} else {
lc!()
}
},
// b + a,
(Var(a), Var(b)) => lc!() + b.variable() + a.variable(),
(Var(a), Var(b)) => {
if a.enable_lc || b.enable_lc {
lc!() + b.variable() + a.variable()
} else {
lc!()
}
},
};
if should_enforce != &Constant(false) {
let cs = self.cs().or(other.cs()).or(should_enforce.cs());
cs.enforce_constraint(sum, should_enforce.lc(), lc!() + one)?;
if cs.should_construct_matrices() {
cs.enforce_constraint(sum, should_enforce.lc(), lc!() + one)?;
} else {
cs.borrow_mut().unwrap().num_constraints += 1;
}
}
Ok(())
}

14
src/boolean/select.rs
View File

@@ -78,11 +78,15 @@ impl<F: PrimeField> CondSelectGadget<F> for Boolean<F> {
// 0 | 1 | 0 | 1
// 1 | 0 | 0 | 0
// 1 | 1 | 0 | 1
cs.enforce_constraint(
cond.lc(),
lc!() + a.lc() - b.lc(),
lc!() + result.lc() - b.lc(),
)?;
if cs.should_construct_matrices() {
cs.enforce_constraint(
cond.lc(),
lc!() + a.lc() - b.lc(),
lc!() + result.lc() - b.lc(),
)?;
} else {
cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(result)
},

15
src/eq.rs
View File

@@ -123,11 +123,16 @@ impl<T: EqGadget<F> + R1CSVar<F>, F: PrimeField> EqGadget<F> for [T] {
Ok(())
} else {
let cs = [&some_are_different, should_enforce].cs();
cs.enforce_constraint(
some_are_different.lc(),
should_enforce.lc(),
should_enforce.lc(),
)
if cs.should_construct_matrices() {
cs.enforce_constraint(
some_are_different.lc(),
should_enforce.lc(),
should_enforce.lc(),
)?;
} else {
cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(())
}
}
}

12
src/fields/fp/cmp.rs
View File

@@ -144,10 +144,14 @@ impl<F: PrimeField> FpVar<F> {
/// verify that.
fn enforce_smaller_than_unchecked(&self, other: &FpVar<F>) -> Result<(), SynthesisError> {
let is_smaller_than = self.is_smaller_than_unchecked(other)?;
let lc_one = lc!() + Variable::One;
[self, other]
.cs()
.enforce_constraint(is_smaller_than.lc(), lc_one.clone(), lc_one)
let cs = [self, other].cs();
if cs.should_construct_matrices() {
let lc_one = lc!() + Variable::One;
cs.enforce_constraint(is_smaller_than.lc(), lc_one.clone(), lc_one)?;
} else {
cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(())
}
}

268
src/fields/fp/mod.rs
View File

@@ -26,6 +26,7 @@ pub struct AllocatedFp<F: PrimeField> {
pub variable: Variable,
/// The constraint system that `self` was allocated in.
pub cs: ConstraintSystemRef<F>,
enable_lc: bool,
}
impl<F: PrimeField> AllocatedFp<F> {
@@ -35,6 +36,7 @@ impl<F: PrimeField> AllocatedFp<F> {
Self {
value,
variable,
enable_lc: cs.should_construct_matrices(),
cs,
}
}
@@ -52,7 +54,8 @@ pub enum FpVar<F: PrimeField> {
}
impl<F: PrimeField> FpVar<F> {
/// Decomposes `self` into a vector of `bits` and a remainder `rest` such that
/// Decomposes `self` into a vector of `bits` and a remainder `rest` such
/// that
/// * `bits.len() == size`, and
/// * `rest == 0`.
pub fn to_bits_le_with_top_bits_zero(
@@ -105,7 +108,11 @@ impl<F: PrimeField> From<Boolean<F>> for FpVar<F> {
} else {
// `other` is a variable
let cs = other.cs();
let variable = cs.new_lc(other.lc()).unwrap();
let variable = cs.new_lc(if cs.should_construct_matrices() {
other.lc()
} else {
lc!()
}).unwrap();
Self::Var(AllocatedFp::new(
other.value().ok().map(|b| F::from(b as u8)),
variable,
@@ -129,14 +136,18 @@ impl<F: PrimeField> AllocatedFp<F> {
/// `zero`, else it outputs `one`.
pub fn from(other: Boolean<F>) -> Self {
let cs = other.cs();
let variable = cs.new_lc(other.lc()).unwrap();
let variable = cs.new_lc(if cs.should_construct_matrices() {
other.lc()
} else {
lc!()
}).unwrap();
Self::new(other.value().ok().map(|b| F::from(b as u8)), variable, cs)
}
/// Returns the value assigned to `self` in the underlying constraint system
/// (if a value was assigned).
pub fn value(&self) -> Result<F, SynthesisError> {
self.cs.assigned_value(self.variable).get()
self.value.ok_or(SynthesisError::AssignmentMissing)
}
/// Outputs `self + other`.
@@ -151,7 +162,11 @@ impl<F: PrimeField> AllocatedFp<F> {
let variable = self
.cs
.new_lc(lc!() + self.variable + other.variable)
.new_lc(if self.enable_lc {
lc!() + self.variable + other.variable
} else {
lc!()
})
.unwrap();
AllocatedFp::new(value, variable, self.cs.clone())
}
@@ -177,7 +192,9 @@ impl<F: PrimeField> AllocatedFp<F> {
} else {
value += variable.value.unwrap();
}
new_lc = new_lc + variable.variable;
if variable.enable_lc {
new_lc = new_lc + variable.variable;
}
num_iters += 1;
}
assert_ne!(num_iters, 0);
@@ -203,7 +220,11 @@ impl<F: PrimeField> AllocatedFp<F> {
let variable = self
.cs
.new_lc(lc!() + self.variable - other.variable)
.new_lc(if self.enable_lc {
lc!() + self.variable - other.variable
} else {
lc!()
})
.unwrap();
AllocatedFp::new(value, variable, self.cs.clone())
}
@@ -217,13 +238,18 @@ impl<F: PrimeField> AllocatedFp<F> {
Ok(self.value.get()? * &other.value.get()?)
})
.unwrap();
self.cs
.enforce_constraint(
lc!() + self.variable,
lc!() + other.variable,
lc!() + product.variable,
)
.unwrap();
if self.enable_lc {
self.cs
.enforce_constraint(
lc!() + self.variable,
lc!() + other.variable,
lc!() + product.variable,
)
.unwrap();
} else {
self.cs.borrow_mut().unwrap().num_constraints += 1;
}
product
}
@@ -238,7 +264,11 @@ impl<F: PrimeField> AllocatedFp<F> {
let value = self.value.map(|val| val + other);
let variable = self
.cs
.new_lc(lc!() + self.variable + (other, Variable::One))
.new_lc(if self.enable_lc {
lc!() + self.variable + (other, Variable::One)
} else {
lc!()
})
.unwrap();
AllocatedFp::new(value, variable, self.cs.clone())
}
@@ -261,7 +291,14 @@ impl<F: PrimeField> AllocatedFp<F> {
self.clone()
} else {
let value = self.value.map(|val| val * other);
let variable = self.cs.new_lc(lc!() + (other, self.variable)).unwrap();
let variable = self
.cs
.new_lc(if self.enable_lc {
lc!() + (other, self.variable)
} else {
lc!()
})
.unwrap();
AllocatedFp::new(value, variable, self.cs.clone())
}
}
@@ -272,7 +309,11 @@ impl<F: PrimeField> AllocatedFp<F> {
#[tracing::instrument(target = "r1cs")]
pub fn double(&self) -> Result<Self, SynthesisError> {
let value = self.value.map(|val| val.double());
let variable = self.cs.new_lc(lc!() + self.variable + self.variable)?;
let variable = self.cs.new_lc(if self.enable_lc {
lc!() + self.variable + self.variable
} else {
lc!()
})?;
Ok(Self::new(value, variable, self.cs.clone()))
}
@@ -294,7 +335,14 @@ impl<F: PrimeField> AllocatedFp<F> {
if let Some(val) = self.value.as_mut() {
*val = -(*val);
}
self.variable = self.cs.new_lc(lc!() - self.variable).unwrap();
self.variable = self
.cs
.new_lc(if self.enable_lc {
lc!() - self.variable
} else {
lc!()
})
.unwrap();
self
}
@@ -315,11 +363,16 @@ impl<F: PrimeField> AllocatedFp<F> {
Ok(self.value.get()?.inverse().unwrap_or_else(F::zero))
})?;
self.cs.enforce_constraint(
lc!() + self.variable,
lc!() + inverse.variable,
lc!() + Variable::One,
)?;
if self.enable_lc {
self.cs.enforce_constraint(
lc!() + self.variable,
lc!() + inverse.variable,
lc!() + Variable::One,
)?;
} else {
self.cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(inverse)
}
@@ -334,11 +387,16 @@ impl<F: PrimeField> AllocatedFp<F> {
/// This requires *one* constraint.
#[tracing::instrument(target = "r1cs")]
pub fn mul_equals(&self, other: &Self, result: &Self) -> Result<(), SynthesisError> {
self.cs.enforce_constraint(
lc!() + self.variable,
lc!() + other.variable,
lc!() + result.variable,
)
if self.enable_lc {
self.cs.enforce_constraint(
lc!() + self.variable,
lc!() + other.variable,
lc!() + result.variable,
)?;
} else {
self.cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(())
}
/// Enforces that `self * self = result`.
@@ -346,11 +404,16 @@ impl<F: PrimeField> AllocatedFp<F> {
/// This requires *one* constraint.
#[tracing::instrument(target = "r1cs")]
pub fn square_equals(&self, result: &Self) -> Result<(), SynthesisError> {
self.cs.enforce_constraint(
lc!() + self.variable,
lc!() + self.variable,
lc!() + result.variable,
)
if self.enable_lc {
self.cs.enforce_constraint(
lc!() + self.variable,
lc!() + self.variable,
lc!() + result.variable,
)?;
} else {
self.cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(())
}
/// Outputs the bit `self == other`.
@@ -424,16 +487,20 @@ impl<F: PrimeField> AllocatedFp<F> {
// and constraint 2 enforces that if self != other, then `is_not_equal = 1`.
// Since these are the only possible two cases, `is_not_equal` is always
// constrained to 0 or 1.
self.cs.enforce_constraint(
lc!() + self.variable - other.variable,
lc!() + multiplier,
is_not_equal.lc(),
)?;
self.cs.enforce_constraint(
lc!() + self.variable - other.variable,
(!&is_not_equal).lc(),
lc!(),
)?;
if self.enable_lc {
self.cs.enforce_constraint(
lc!() + self.variable - other.variable,
lc!() + multiplier,
is_not_equal.lc(),
)?;
self.cs.enforce_constraint(
lc!() + self.variable - other.variable,
(!&is_not_equal).lc(),
lc!(),
)?;
} else {
self.cs.borrow_mut().unwrap().num_constraints += 2;
}
Ok(is_not_equal)
}
@@ -446,11 +513,16 @@ impl<F: PrimeField> AllocatedFp<F> {
other: &Self,
should_enforce: &Boolean<F>,
) -> Result<(), SynthesisError> {
self.cs.enforce_constraint(
lc!() + self.variable - other.variable,
lc!() + should_enforce.lc(),
lc!(),
)
if self.enable_lc {
self.cs.enforce_constraint(
lc!() + self.variable - other.variable,
lc!() + should_enforce.lc(),
lc!(),
)?;
} else {
self.cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(())
}
/// Enforces that self != other if `should_enforce.is_eq(&Boolean::TRUE)`.
@@ -465,8 +537,9 @@ impl<F: PrimeField> AllocatedFp<F> {
// The high level logic is as follows:
// We want to check that self - other != 0. We do this by checking that
// (self - other).inverse() exists. In more detail, we check the following:
// If `should_enforce == true`, then we set `multiplier = (self - other).inverse()`,
// and check that (self - other) * multiplier == 1. (i.e., that the inverse exists)
// If `should_enforce == true`, then we set `multiplier = (self -
// other).inverse()`, and check that (self - other) * multiplier == 1.
// (i.e., that the inverse exists)
//
// If `should_enforce == false`, then we set `multiplier == 0`, and check that
// (self - other) * 0 == 0, which is always satisfied.
@@ -478,11 +551,16 @@ impl<F: PrimeField> AllocatedFp<F> {
}
})?;
self.cs.enforce_constraint(
lc!() + self.variable - other.variable,
lc!() + multiplier.variable,
should_enforce.lc(),
)?;
if self.enable_lc {
self.cs.enforce_constraint(
lc!() + self.variable - other.variable,
lc!() + multiplier.variable,
should_enforce.lc(),
)?;
} else {
self.cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(())
}
}
@@ -532,14 +610,20 @@ impl<F: PrimeField> ToBitsGadget<F> for AllocatedFp<F> {
let mut coeff = F::one();
for bit in bits.iter() {
lc = &lc + bit.lc() * coeff;
if self.enable_lc {
lc = &lc + bit.lc() * coeff;
}
coeff.double_in_place();
}
lc = lc - &self.variable;
if self.enable_lc {
lc = lc - &self.variable;
cs.enforce_constraint(lc!(), lc!(), lc)?;
cs.enforce_constraint(lc!(), lc!(), lc)?;
} else {
self.cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(bits)
}
@@ -594,8 +678,8 @@ impl<F: PrimeField> CondSelectGadget<F> for AllocatedFp<F> {
false_val: &Self,
) -> Result<Self, SynthesisError> {
match cond {
&Boolean::Constant(true) => Ok(true_val.clone()),
&Boolean::Constant(false) => Ok(false_val.clone()),
Boolean::Constant(true) => Ok(true_val.clone()),
Boolean::Constant(false) => Ok(false_val.clone()),
_ => {
let cs = cond.cs();
let result = Self::new_witness(cs.clone(), || {
@@ -607,11 +691,15 @@ impl<F: PrimeField> CondSelectGadget<F> for AllocatedFp<F> {
// r = c * a + (1 - c) * b
// r = b + c * (a - b)
// c * (a - b) = r - b
cs.enforce_constraint(
cond.lc(),
lc!() + true_val.variable - false_val.variable,
lc!() + result.variable - false_val.variable,
)?;
if cs.should_construct_matrices() {
cs.enforce_constraint(
cond.lc(),
lc!() + true_val.variable - false_val.variable,
lc!() + result.variable - false_val.variable,
)?;
} else {
cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(result)
},
@@ -627,18 +715,23 @@ impl<F: PrimeField> TwoBitLookupGadget<F> for AllocatedFp<F> {
fn two_bit_lookup(b: &[Boolean<F>], c: &[Self::TableConstant]) -> Result<Self, SynthesisError> {
debug_assert_eq!(b.len(), 2);
debug_assert_eq!(c.len(), 4);
let result = Self::new_witness(b.cs(), || {
let cs = b.cs();
let result = Self::new_witness(cs.clone(), || {
let lsb = usize::from(b[0].value()?);
let msb = usize::from(b[1].value()?);
let index = lsb + (msb << 1);
Ok(c[index])
})?;
let one = Variable::One;
b.cs().enforce_constraint(
lc!() + b[1].lc() * (c[3] - &c[2] - &c[1] + &c[0]) + (c[1] - &c[0], one),
lc!() + b[0].lc(),
lc!() + result.variable - (c[0], one) + b[1].lc() * (c[0] - &c[2]),
)?;
if cs.should_construct_matrices() {
cs.enforce_constraint(
lc!() + b[1].lc() * (c[3] - &c[2] - &c[1] + &c[0]) + (c[1] - &c[0], one),
lc!() + b[0].lc(),
lc!() + result.variable - (c[0], one) + b[1].lc() * (c[0] - &c[2]),
)?;
} else {
cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(result)
}
@@ -655,7 +748,8 @@ impl<F: PrimeField> ThreeBitCondNegLookupGadget<F> for AllocatedFp<F> {
) -> Result<Self, SynthesisError> {
debug_assert_eq!(b.len(), 3);
debug_assert_eq!(c.len(), 4);
let result = Self::new_witness(b.cs(), || {
let cs = b.cs();
let result = Self::new_witness(cs.clone(), || {
let lsb = usize::from(b[0].value()?);
let msb = usize::from(b[1].value()?);
let index = lsb + (msb << 1);
@@ -670,16 +764,20 @@ impl<F: PrimeField> ThreeBitCondNegLookupGadget<F> for AllocatedFp<F> {
Ok(y)
})?;
let y_lc = b0b1.lc() * (c[3] - &c[2] - &c[1] + &c[0])
+ b[0].lc() * (c[1] - &c[0])
+ b[1].lc() * (c[2] - &c[0])
+ (c[0], Variable::One);
// enforce y * (1 - 2 * b_2) == res
b.cs().enforce_constraint(
y_lc.clone(),
b[2].lc() * F::from(2u64).neg() + (F::one(), Variable::One),
lc!() + result.variable,
)?;
if cs.should_construct_matrices() {
let y_lc = b0b1.lc() * (c[3] - &c[2] - &c[1] + &c[0])
+ b[0].lc() * (c[1] - &c[0])
+ b[1].lc() * (c[2] - &c[0])
+ (c[0], Variable::One);
// enforce y * (1 - 2 * b_2) == res
cs.enforce_constraint(
y_lc.clone(),
b[2].lc() * F::from(2u64).neg() + (F::one(), Variable::One),
lc!() + result.variable,
)?;
} else {
cs.borrow_mut().unwrap().num_constraints += 1;
}
Ok(result)
}
@@ -695,7 +793,11 @@ impl<F: PrimeField> AllocVar<F, F> for AllocatedFp<F> {
let cs = ns.cs();
if mode == AllocationMode::Constant {
let v = *f()?.borrow();
let lc = cs.new_lc(lc!() + (v, Variable::One))?;
let lc = cs.new_lc(if cs.should_construct_matrices() {
lc!() + (v, Variable::One)
} else {
lc!()
})?;
Ok(Self::new(Some(v), lc, cs))
} else {
let mut value = None;