diff --git a/src/plonk/circuit/allocated_num.rs b/src/plonk/circuit/allocated_num.rs index de0698f5..ded8995f 100644 --- a/src/plonk/circuit/allocated_num.rs +++ b/src/plonk/circuit/allocated_num.rs @@ -22,6 +22,7 @@ use crate::bellman::plonk::better_better_cs::cs::{ MainGateTerm, MainGate, }; +use crate::plonk::circuit::utils::is_naive_main_gate; use super::utils::is_selector_specialized_gate; @@ -214,6 +215,74 @@ impl Num { masked_a.enforce_equal(cs, &masked_b) } + /// Takes two allocated numbers (a, b) and returns + /// (b, a) if the condition is true, and (a, b) + /// otherwise + pub fn conditionally_reverse_with_naive_gate( + cs: &mut CS, + a: &Self, + b: &Self, + condition: &Boolean + ) -> Result<(Self, Self), SynthesisError> + where CS: ConstraintSystem + { + assert!(is_naive_main_gate::()); + + let c = AllocatedNum::alloc( + cs, + || { + if *condition.get_value().get()? { + Ok(*b.get_value().get()?) + } else { + Ok(*a.get_value().get()?) + } + } + )?; + + let d = AllocatedNum::alloc( + cs, + || { + if *condition.get_value().get()? { + Ok(*a.get_value().get()?) + } else { + Ok(*b.get_value().get()?) + } + } + )?; + + let c = Num::Variable(c); + let d = Num::Variable(d); + + // we have two inputs (a, b) and two outputs (c, d) + // if condition is + // - true then reverse values a == d and b == c + // - false then keep values the same a == c and b == d + + // so the constraints would be + // (a-b)*condition + b - d = 0 + // (b-a)*condition + a - c = 0 + let mut minus_one = E::Fr::one(); + minus_one.negate(); + + let a_minus_b = a.sub(cs, &b)?; + let ab_condition = Num::mask(cs, &a_minus_b, &condition)?; + + let mut lc = LinearCombination::zero(); + lc.add_assign_number_with_coeff(&ab_condition, E::Fr::one()); + lc.add_assign_number_with_coeff(&b, E::Fr::one()); + lc.add_assign_number_with_coeff(&d, minus_one); + lc.enforce_zero(cs)?; + + let mut lc = LinearCombination::zero(); + lc.add_assign_number_with_coeff(&ab_condition, minus_one); + lc.add_assign_number_with_coeff(&a, E::Fr::one()); + lc.add_assign_number_with_coeff(&c, minus_one); + lc.enforce_zero(cs)?; + + Ok((c, d)) + } + + /// Takes two allocated numbers (a, b) and returns /// (b, a) if the condition is true, and (a, b) /// otherwise. @@ -234,6 +303,9 @@ impl Num { return Ok((a.clone(), b.clone())) } } + if is_naive_main_gate::(){ + return Self::conditionally_reverse_with_naive_gate(cs, a, b, condition); + } if is_selector_specialized_gate::() { let c = Num::conditionally_select(cs, &condition, &b, &a)?; @@ -643,34 +715,37 @@ impl Num { }) }, (Num::Variable(var1), Num::Variable(var2), Num::Variable(var3)) => { - let mut value = None; - - let addition_result = cs.alloc(|| { - let mut tmp = *var1.value.get()?; - let tmp2 = *var2.value.get()?; - let tmp3 = *var3.value.get()?; - tmp.add_assign(&tmp2); - tmp.add_assign(&tmp3); - value = Some(tmp); - Ok(tmp) + let sum = AllocatedNum::alloc(cs, || { + let mut sum = *var1.get_value().get()?; + sum.add_assign(var2.get_value().get()?); + sum.add_assign(var3.get_value().get()?); + Ok(sum) })?; - - let self_term = ArithmeticTerm::from_variable(var1.variable); - let other_term = ArithmeticTerm::from_variable(var2.variable); - let third_term = ArithmeticTerm::from_variable(var3.variable); - let result_term = ArithmeticTerm::from_variable(addition_result); - let mut term = MainGateTerm::new(); - term.add_assign(self_term); - term.add_assign(other_term); - term.add_assign(third_term); - term.sub_assign(result_term); - - cs.allocate_main_gate(term)?; - - Num::Variable(AllocatedNum { - value: value, - variable: addition_result - }) + if is_naive_main_gate::(){ + let mut minus_one = E::Fr::one(); + minus_one.negate(); + let mut lc = LinearCombination::zero(); + lc.add_assign_variable_with_coeff(var1, E::Fr::one()); + lc.add_assign_variable_with_coeff(var2, E::Fr::one()); + lc.add_assign_variable_with_coeff(var3, E::Fr::one()); + lc.add_assign_variable_with_coeff(&sum, minus_one); + lc.enforce_zero(cs)?; + }else{ + let self_term = ArithmeticTerm::from_variable(var1.variable); + let other_term = ArithmeticTerm::from_variable(var2.variable); + let third_term = ArithmeticTerm::from_variable(var3.variable); + let result_term = ArithmeticTerm::from_variable(sum.get_variable()); + + let mut term = MainGateTerm::new(); + term.add_assign(self_term); + term.add_assign(other_term); + term.add_assign(third_term); + term.sub_assign(result_term); + + cs.allocate_main_gate(term)?; + + } + Num::Variable(sum) }, }; @@ -945,13 +1020,65 @@ impl Num { }, } } + + /// Takes two allocated numbers (a, b) and returns + /// (b, a) if the condition is true, and (a, b) + /// otherwise in case of a width3 cs. + pub fn conditionally_select_with_naive_gate( + cs: &mut CS, + condition: &Boolean, + a: &Self, + b: &Self, + ) -> Result + where CS: ConstraintSystem + { + assert!(is_naive_main_gate::()); + let c = AllocatedNum::alloc( + cs, + || { + if *condition.get_value().get()? { + Ok(*a.get_value().get()?) + } else { + Ok(*b.get_value().get()?) + } + } + )?; + + let c = Num::Variable(c); + + // we have two inputs (a, b) and one output c + // if condition is + // - true then reverse values a ==c + // - false then keep values the same b == c + + // so the constraints would be + // a*condition + b*(1-condition) - c = 0 + // a*condition + b - b*condition - c = 0 + // a*condition - b*condition + b - c = 0 + // condition*(a - b) + b - c = 0 + let mut minus_one = E::Fr::one(); + minus_one.negate(); + + let a_minus_b = a.sub(cs, &b)?; + let a_minus_b_cond = Self::mask(cs, &a_minus_b, &condition)?; + let mut lc = LinearCombination::zero(); + lc.add_assign_number_with_coeff(&a_minus_b_cond, E::Fr::one()); + lc.add_assign_number_with_coeff(&b, E::Fr::one()); + lc.add_assign_number_with_coeff(&c, minus_one); + lc.enforce_zero(cs)?; + + Ok(c) + } pub fn conditionally_select>( cs: &mut CS, condition_flag: &Boolean, a: &Self, b: &Self ) -> Result { + if is_naive_main_gate::(){ + return Self::conditionally_select_with_naive_gate(cs, condition_flag, a, b); + } match (a, b) { (Num::Variable(ref a), Num::Variable(ref b)) => { let num = AllocatedNum::conditionally_select(cs, a, b, condition_flag)?; @@ -1554,6 +1681,71 @@ impl AllocatedNum { Ok(flag.into()) } + /// Takes two allocated numbers (a, b) and returns + /// (b, a) if the condition is true, and (a, b) + /// otherwise + pub fn conditionally_reverse_with_naive_gate( + cs: &mut CS, + a: &Self, + b: &Self, + condition: &Boolean + ) -> Result<(Self, Self), SynthesisError> + where CS: ConstraintSystem + { + assert!(is_naive_main_gate::()); + + let c = AllocatedNum::alloc( + cs, + || { + if *condition.get_value().get()? { + Ok(*b.get_value().get()?) + } else { + Ok(*a.get_value().get()?) + } + } + )?; + + let d = AllocatedNum::alloc( + cs, + || { + if *condition.get_value().get()? { + Ok(*a.get_value().get()?) + } else { + Ok(*b.get_value().get()?) + } + } + )?; + + // we have two inputs (a, b) and two outputs (c, d) + // if condition is + // - true then reverse values a == d and b == c + // - false then keep values the same a == c and b == d + + // co the constraints would be + // (a-b)*condition + b - d = 0 + // (b-a)*condition + a - c = 0 + let mut minus_one = E::Fr::one(); + minus_one.negate(); + + let a_minus_b = a.sub(cs, &b)?; + let ab_condition = AllocatedNum::mask(cs, &a_minus_b, &condition)?; + + let mut lc = LinearCombination::zero(); + lc.add_assign_variable_with_coeff(&ab_condition, E::Fr::one()); + lc.add_assign_variable_with_coeff(&b, E::Fr::one()); + lc.add_assign_variable_with_coeff(&d, minus_one); + lc.enforce_zero(cs)?; + + let mut lc = LinearCombination::zero(); + lc.add_assign_variable_with_coeff(&ab_condition, minus_one); + lc.add_assign_variable_with_coeff(&a, E::Fr::one()); + lc.add_assign_variable_with_coeff(&c, minus_one); + lc.enforce_zero(cs)?; + + Ok((c, d)) + } + + /// Takes two allocated numbers (a, b) and returns /// (b, a) if the condition is true, and (a, b) /// otherwise. @@ -1575,6 +1767,10 @@ impl AllocatedNum { } } + if is_naive_main_gate::(){ + return Self::conditionally_reverse_with_naive_gate(cs, a, b, condition); + } + if is_selector_specialized_gate::() { let c = Self::conditionally_select(cs, &b, &a, &condition)?; let d = Self::conditionally_select(cs, &a, &b, &condition)?; @@ -1934,18 +2130,42 @@ impl AllocatedNum { let mut minus_one = E::Fr::one(); minus_one.negate(); - - let self_term = ArithmeticTerm::from_variable_and_coeff(self.get_variable(), minus_one).mul_by_variable(not_bit.get_variable()); - let a_term = ArithmeticTerm::from_variable(self.get_variable()); - let other_term = ArithmeticTerm::from_variable(accumulator.variable); - let result_term = ArithmeticTerm::from_variable(result); - let mut term = MainGateTerm::new(); - term.add_assign(self_term); - term.add_assign(a_term); - term.add_assign(other_term); - term.sub_assign(result_term); - - cs.allocate_main_gate(term)?; + + if is_naive_main_gate::(){ + let result = Self::alloc(cs, ||{ + let mut tmp = *self.value.get()?; + let not_bit_value = not_bit_value.get()?; + let acc_value = accumulator.value.get()?; + if *not_bit_value { + tmp = E::Fr::zero(); + } + tmp.add_assign(&acc_value); + value = Some(tmp); + + Ok(tmp) + })?; + // a + (1-condition)*b - c = 0 + // a + b - b*condition - c = 0; + let masked = Self::mask(cs, self, boolean)?; + let mut lc = LinearCombination::zero(); + lc.add_assign_variable_with_coeff(self, E::Fr::one()); + lc.add_assign_variable_with_coeff(accumulator, E::Fr::one()); + lc.add_assign_variable_with_coeff(&masked, minus_one); + lc.add_assign_variable_with_coeff(&result, minus_one); + lc.enforce_zero(cs)?; + }else{ + let self_term = ArithmeticTerm::from_variable_and_coeff(self.get_variable(), minus_one).mul_by_variable(not_bit.get_variable()); + let a_term = ArithmeticTerm::from_variable(self.get_variable()); + let other_term = ArithmeticTerm::from_variable(accumulator.variable); + let result_term = ArithmeticTerm::from_variable(result); + let mut term = MainGateTerm::new(); + term.add_assign(self_term); + term.add_assign(a_term); + term.add_assign(other_term); + term.sub_assign(result_term); + + cs.allocate_main_gate(term)?; + } Ok(AllocatedNum { value: value, @@ -1956,35 +2176,36 @@ impl AllocatedNum { } pub fn add_two>(&self, cs: &mut CS, x: Self, y: Self) -> Result - { - let mut value = None; - - let addition_result = cs.alloc(|| { - let mut tmp = *self.value.get()?; - let tmp2 = x.value.get()?; - let tmp3 = y.value.get()?; - tmp.add_assign(&tmp2); - tmp.add_assign(&tmp3); - value = Some(tmp); - Ok(tmp) + { + let sum = AllocatedNum::alloc(cs, || { + let mut sum = *self.get_value().get()?; + sum.add_assign(x.get_value().get()?); + sum.add_assign(y.get_value().get()?); + Ok(sum) })?; - - let self_term = ArithmeticTerm::from_variable(self.variable); - let other_term = ArithmeticTerm::from_variable(x.variable); - let third_term = ArithmeticTerm::from_variable(y.variable); - let result_term = ArithmeticTerm::from_variable(addition_result); - let mut term = MainGateTerm::new(); - term.add_assign(self_term); - term.add_assign(other_term); - term.add_assign(third_term); - term.sub_assign(result_term); - - cs.allocate_main_gate(term)?; - - Ok(AllocatedNum { - value: value, - variable: addition_result - }) + if is_naive_main_gate::(){ + let mut minus_one = E::Fr::one(); + minus_one.negate(); + let mut lc = LinearCombination::zero(); + lc.add_assign_variable_with_coeff(self, E::Fr::one()); + lc.add_assign_variable_with_coeff(&x, E::Fr::one()); + lc.add_assign_variable_with_coeff(&y, E::Fr::one()); + lc.add_assign_variable_with_coeff(&sum, minus_one); + lc.enforce_zero(cs)?; + }else{ + let self_term = ArithmeticTerm::from_variable(self.variable); + let other_term = ArithmeticTerm::from_variable(x.variable); + let third_term = ArithmeticTerm::from_variable(y.variable); + let result_term = ArithmeticTerm::from_variable(sum.get_variable()); + let mut term = MainGateTerm::new(); + term.add_assign(self_term); + term.add_assign(other_term); + term.add_assign(third_term); + term.sub_assign(result_term); + + cs.allocate_main_gate(term)?; + } + Ok(sum) } pub fn mul_constant( @@ -2060,6 +2281,54 @@ impl AllocatedNum { self.mul(cs, &self) } + /// Takes two allocated numbers (a, b) and returns + /// (b, a) if the condition is true, and (a, b) + /// otherwise in case of a width3 cs. + pub fn conditionally_select_with_naive_gate( + cs: &mut CS, + a: &Self, + b: &Self, + condition: &Boolean, + ) -> Result + where CS: ConstraintSystem + { + assert!(is_naive_main_gate::()); + + let c = AllocatedNum::alloc( + cs, + || { + if *condition.get_value().get()? { + Ok(*a.get_value().get()?) + } else { + Ok(*b.get_value().get()?) + } + } + )?; + + // we have two inputs (a, b) and one output c + // if condition is + // - true then reverse values a ==c + // - false then keep values the same b == c + + // so the constraints would be + // a*condition + b*(1-condition) - c = 0 + // a*condition + b - b*condition - c = 0 + // a*condition - b*condition + b - c = 0 + // condition*(a - b) + b - c = 0 + let mut minus_one = E::Fr::one(); + minus_one.negate(); + + let a_minus_b = a.sub(cs, &b)?; + let a_minus_b_cond = Self::mask(cs, &a_minus_b, &condition)?; + let mut lc = LinearCombination::zero(); + lc.add_assign_variable_with_coeff(&a_minus_b_cond, E::Fr::one()); + lc.add_assign_variable_with_coeff(&b, E::Fr::one()); + lc.add_assign_variable_with_coeff(&c, minus_one); + lc.enforce_zero(cs)?; + + Ok(c) + } + /// Takes two allocated numbers (a, b) and returns /// a if the condition is true, and b @@ -2078,6 +2347,10 @@ impl AllocatedNum { return Ok(a.clone()); } + if is_naive_main_gate::(){ + return Self::conditionally_select_with_naive_gate(cs, a, b, condition); + } + if is_selector_specialized_gate::() { return Self::conditionally_select_for_special_main_gate(cs, a, b, condition); } diff --git a/src/plonk/circuit/bigint_new/range_checks.rs b/src/plonk/circuit/bigint_new/range_checks.rs index 99d28ecf..b6027cd8 100644 --- a/src/plonk/circuit/bigint_new/range_checks.rs +++ b/src/plonk/circuit/bigint_new/range_checks.rs @@ -249,7 +249,9 @@ pub fn enforce_range_check_using_naive_approach Hash for GoldilocksField { } } -fn range_check_for_num_bits>( +pub fn range_check_for_num_bits>( cs: &mut CS, num: &Num, num_bits: usize @@ -94,11 +94,34 @@ fn range_check_for_num_bits>( // Name of the table should be checked if let Ok(table) = cs.get_table(BITWISE_LOGICAL_OPS_TABLE_NAME) { enforce_range_check_using_bitop_table(cs, &num.get_variable(), num_bits, table, true)?; - } else { + }else if >::CAN_ACCESS_NEXT_TRACE_STEP { enforce_range_check_using_naive_approach(cs, &num.get_variable(), num_bits)?; - } + }else { + use crate::plonk::circuit::boolean::*; + let has_value = num.get_value().is_some(); + let value = num.get_value().unwrap_or(E::Fr::zero()); + let bits: Vec<_> = BitIterator::new(value.into_repr()).collect(); + let allocated_bits: Vec = bits + .into_iter() + .rev() + .take(num_bits) + .map(|bit| { + let t = if has_value { Some(bit) } else { None }; + AllocatedBit::alloc(cs, t) + }) + .collect::, SynthesisError>>()?; + let mut lc = LinearCombination::zero(); + let mut coeff = E::Fr::one(); + for b in allocated_bits.iter() { + lc.add_assign_bit_with_coeff(b, coeff); + coeff.double(); + } + let mut minus_one = E::Fr::one(); + minus_one.negate(); + lc.add_assign_number_with_coeff(&num, minus_one); + lc.enforce_zero(cs)?; + } } - Ok(()) } diff --git a/src/plonk/circuit/linear_combination.rs b/src/plonk/circuit/linear_combination.rs index c7f9e420..7c4c4a6b 100644 --- a/src/plonk/circuit/linear_combination.rs +++ b/src/plonk/circuit/linear_combination.rs @@ -20,6 +20,7 @@ use crate::bellman::plonk::better_better_cs::cs::{ MainGateTerm }; +use crate::plonk::circuit::utils::is_naive_main_gate; use crate::plonk::circuit::Assignment; use super::allocated_num::{ @@ -365,7 +366,7 @@ impl LinearCombination { self.constant ) } else { - unimplemented!() + enforce_zero_naive(cs, &self.terms, self.constant) } } @@ -406,7 +407,9 @@ impl LinearCombination { terms, self.constant )?; - } else { + } else if is_naive_main_gate::() { + enforce_zero_naive(cs, &terms, self.constant)?; + }else{ unimplemented!() } @@ -716,6 +719,86 @@ impl LinearCombination { } } +pub fn enforce_zero_naive>( + cs: &mut CS, + terms: &[(E::Fr, Variable)], // includes value as last term + constant: E::Fr, +) -> Result<(), SynthesisError> { + assert!(is_naive_main_gate::()); + use crate::bellman::plonk::better_better_cs::cs::PlonkConstraintSystemParams; + assert!(CS::Params::CAN_ACCESS_NEXT_TRACE_STEP == false); + let chunk_size = CS::Params::STATE_WIDTH -1; + // c0, c1, c2 + k + // v0, v1, v2 + + // c0*v0 + c1*v1 + k = s0 + // s0 + c2*v2 = s1 + // s1 - sum == 0 + let mut intermediate_sums = vec![]; + let mut used_constant = false; + + let has_value = cs.get_value(terms[0].1).is_ok(); + + let mut sum_terms = |chunk: &[(E::Fr, Variable)]| -> Result<(), SynthesisError> { + assert!(chunk.len() <= 2); + let mut sum = if used_constant { E::Fr::zero() } else { constant }; + for (c, v) in chunk.iter() { + assert_eq!(cs.get_value(*v).is_ok(), has_value); + let mut tmp = cs.get_value(*v).unwrap_or(E::Fr::zero()); + tmp.mul_assign(&c); + sum.add_assign(&tmp); + } + + let allocated_sum = AllocatedNum::alloc(cs, || { + if has_value{ + Ok(sum) + }else{ + Err(SynthesisError::AssignmentMissing) + } + })?; + let mut terms = MainGateTerm::new(); + for (coeff, var) in chunk.iter() { + let term = ArithmeticTerm::from_variable_and_coeff(*var, *coeff); + terms.add_assign(term); + } + + if used_constant == false { + let term = ArithmeticTerm::constant(constant); + terms.add_assign(term); + used_constant = true; + } + let term = + ArithmeticTerm::from_variable_and_coeff(allocated_sum.get_variable(), E::Fr::one()); + terms.sub_assign(term); + + cs.allocate_main_gate(terms)?; + + intermediate_sums.push(allocated_sum); + + Ok(()) + }; + + for chunk in terms.chunks_exact(chunk_size){ + sum_terms(chunk)?; + } + // remainder term can fit into single gate + sum_terms(terms.chunks_exact(chunk_size).remainder())?; + + assert_eq!(used_constant, true); + + if used_constant == false { + intermediate_sums.push(AllocatedNum::alloc_cnst(cs, constant)?); + } + + let mut final_sum = AllocatedNum::zero(cs); + for intermediate_sum in intermediate_sums.iter() { + final_sum = final_sum.add(cs, &intermediate_sum)?; + } + final_sum.is_zero(cs)?; + + Ok(()) +} + #[cfg(test)] mod test { use super::*; diff --git a/src/plonk/circuit/utils.rs b/src/plonk/circuit/utils.rs index 4cc3415d..854f323f 100644 --- a/src/plonk/circuit/utils.rs +++ b/src/plonk/circuit/utils.rs @@ -212,6 +212,14 @@ pub fn fe_to_lsb_first_bits(el: &F) -> Vec { use crate::bellman::pairing::Engine; use crate::bellman::plonk::better_better_cs::cs::ConstraintSystem; +pub fn is_naive_main_gate>() -> bool { + use bellman::plonk::better_better_cs::gates::naive_main_gate::NaiveMainGate; + use bellman::plonk::better_better_cs::cs::PlonkConstraintSystemParams; + use bellman::plonk::better_better_cs::cs::GateInternal; + use std::any::Any; + Any::type_id(&CS::MainGate::default()) == Any::type_id(&NaiveMainGate) +} + pub fn is_selector_specialized_gate>() -> bool { use bellman::plonk::better_better_cs::cs::GateInternal; use bellman::plonk::better_better_cs::gates::selector_optimized_with_d_next::SelectorOptimizedWidth4MainGateWithDNext;