diff --git a/Cargo.toml b/Cargo.toml index 00e8bf1..e6df8b7 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -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" } diff --git a/src/alloc.rs b/src/alloc.rs index 2afa550..dbe87ad 100644 --- a/src/alloc.rs +++ b/src/alloc.rs @@ -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`. diff --git a/src/boolean/allocated.rs b/src/boolean/allocated.rs index 9397f12..acc8736 100644 --- a/src/boolean/allocated.rs +++ b/src/boolean/allocated.rs @@ -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 { pub(super) variable: Variable, pub(super) cs: ConstraintSystemRef, -} - -pub(crate) fn bool_to_field(val: impl Borrow) -> F { - F::from(*val.borrow()) + pub(super) enable_lc: bool, + pub(super) value: Option, } impl AllocatedBool { /// Get the assigned value for `self`. pub fn value(&self) -> Result { - 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 AllocatedBool { cs: ConstraintSystemRef, f: impl FnOnce() -> Result, ) -> Result { - 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 { - 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 AllocatedBool { // -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 AllocatedBool { // 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 AllocatedBool { // 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 AllocatedBool { // 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 AllocatedBool { // 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 AllocVar for AllocatedBool { 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(), + }) } } } diff --git a/src/boolean/eq.rs b/src/boolean/eq.rs index 43bc7da..9c9d397 100644 --- a/src/boolean/eq.rs +++ b/src/boolean/eq.rs @@ -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 EqGadget for Boolean { 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 EqGadget for Boolean { 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(()) } diff --git a/src/boolean/select.rs b/src/boolean/select.rs index 78eb044..75b4168 100644 --- a/src/boolean/select.rs +++ b/src/boolean/select.rs @@ -78,11 +78,15 @@ impl CondSelectGadget for Boolean { // 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) }, diff --git a/src/eq.rs b/src/eq.rs index 1692edc..62dbb78 100644 --- a/src/eq.rs +++ b/src/eq.rs @@ -123,11 +123,16 @@ impl + R1CSVar, F: PrimeField> EqGadget 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(()) } } } diff --git a/src/fields/fp/cmp.rs b/src/fields/fp/cmp.rs index f3304e4..7b5a1d9 100644 --- a/src/fields/fp/cmp.rs +++ b/src/fields/fp/cmp.rs @@ -144,10 +144,14 @@ impl FpVar { /// verify that. fn enforce_smaller_than_unchecked(&self, other: &FpVar) -> 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(()) } } diff --git a/src/fields/fp/mod.rs b/src/fields/fp/mod.rs index 71fcdf6..b9b9efb 100644 --- a/src/fields/fp/mod.rs +++ b/src/fields/fp/mod.rs @@ -26,6 +26,7 @@ pub struct AllocatedFp { pub variable: Variable, /// The constraint system that `self` was allocated in. pub cs: ConstraintSystemRef, + enable_lc: bool, } impl AllocatedFp { @@ -35,6 +36,7 @@ impl AllocatedFp { Self { value, variable, + enable_lc: cs.should_construct_matrices(), cs, } } @@ -52,7 +54,8 @@ pub enum FpVar { } impl FpVar { - /// 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 From> for FpVar { } 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 AllocatedFp { /// `zero`, else it outputs `one`. pub fn from(other: Boolean) -> 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 { - self.cs.assigned_value(self.variable).get() + self.value.ok_or(SynthesisError::AssignmentMissing) } /// Outputs `self + other`. @@ -151,7 +162,11 @@ impl AllocatedFp { 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 AllocatedFp { } 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 AllocatedFp { 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 AllocatedFp { 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 AllocatedFp { 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 AllocatedFp { 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 AllocatedFp { #[tracing::instrument(target = "r1cs")] pub fn double(&self) -> Result { 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 AllocatedFp { 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 AllocatedFp { 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 AllocatedFp { /// 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 AllocatedFp { /// 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 AllocatedFp { // 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 AllocatedFp { other: &Self, should_enforce: &Boolean, ) -> 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 AllocatedFp { // 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 AllocatedFp { } })?; - 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 ToBitsGadget for AllocatedFp { 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 CondSelectGadget for AllocatedFp { false_val: &Self, ) -> Result { 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 CondSelectGadget for AllocatedFp { // 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 TwoBitLookupGadget for AllocatedFp { fn two_bit_lookup(b: &[Boolean], c: &[Self::TableConstant]) -> Result { 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 ThreeBitCondNegLookupGadget for AllocatedFp { ) -> Result { 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 ThreeBitCondNegLookupGadget for AllocatedFp { 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 AllocVar for AllocatedFp { 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;