From 1424f863cd3123b802024edcc177940409f52aa8 Mon Sep 17 00:00:00 2001 From: guipublic Date: Thu, 24 Nov 2022 14:34:16 +0000 Subject: [PATCH 1/9] add a binary solver for array equality constraints --- crates/acvm/src/lib.rs | 316 ++++++++++-------- crates/acvm/src/pwg/arithmetic.rs | 93 ++++-- crates/acvm/src/pwg/binary.rs | 234 +++++++++++++ crates/acvm/src/pwg/logic.rs | 12 +- crates/acvm/src/pwg/mod.rs | 1 + crates/nargo/src/cli/prove_cmd.rs | 7 - .../tests/test_data/main_return/Prover.toml | 5 +- .../tests/test_data/main_return/src/main.nr | 16 +- .../nargo/tests/test_data/sha256/Prover.toml | 1 + .../nargo/tests/test_data/sha256/src/main.nr | 3 +- 10 files changed, 505 insertions(+), 183 deletions(-) create mode 100644 crates/acvm/src/pwg/binary.rs diff --git a/crates/acvm/src/lib.rs b/crates/acvm/src/lib.rs index 67b7fd14453..7e03bdccb44 100644 --- a/crates/acvm/src/lib.rs +++ b/crates/acvm/src/lib.rs @@ -14,6 +14,7 @@ use acir::{ native_types::{Expression, Witness}, OPCODE, }; +use pwg::binary::BinarySolver; use crate::pwg::{arithmetic::ArithmeticSolver, logic::LogicSolver}; use num_bigint::BigUint; @@ -38,169 +39,202 @@ pub trait Backend: SmartContract + ProofSystemCompiler + PartialWitnessGenerator /// each OPCODE. /// Returns an Error if the backend does not support that OPCODE pub trait PartialWitnessGenerator { - fn solve( + fn solve_gate( &self, initial_witness: &mut BTreeMap, - gates: Vec, + gate: &Gate, ) -> GateResolution { - if gates.is_empty() { - return GateResolution::Resolved; - } - let mut unsolved_gates: Vec = Vec::new(); - - for gate in gates.into_iter() { - let unsolved = match &gate { - Gate::Arithmetic(arith) => { - let result = ArithmeticSolver::solve(initial_witness, arith); - match result { - GateResolution::Resolved => false, - GateResolution::Skip => true, - _ => return result, + match gate { + Gate::Arithmetic(arith) => ArithmeticSolver::solve(initial_witness, arith), + Gate::Range(w, r) => { + if let Some(w_value) = initial_witness.get(w) { + if w_value.num_bits() > *r { + return GateResolution::UnsatisfiedConstrain; } + GateResolution::Resolved + } else { + GateResolution::Skip } - Gate::Range(w, r) => { - if let Some(w_value) = initial_witness.get(w) { - if w_value.num_bits() > *r { - return GateResolution::UnsatisfiedConstrain; - } - false - } else { - true + } + Gate::And(and_gate) => { + LogicSolver::solve_and_gate(initial_witness, and_gate) + // We compute the result because the other gates may want to use the assignment to generate their assignments + } + Gate::Xor(xor_gate) => { + LogicSolver::solve_xor_gate(initial_witness, xor_gate) + // We compute the result because the other gates may want to use the assignment to generate their assignments + } + Gate::GadgetCall(gc) => { + let mut unsolvable = false; + for i in &gc.inputs { + if !initial_witness.contains_key(&i.witness) { + unsolvable = true; + break; } } - Gate::And(and_gate) => { - !LogicSolver::solve_and_gate(initial_witness, and_gate) - // We compute the result because the other gates may want to use the assignment to generate their assignments - } - Gate::Xor(xor_gate) => { - !LogicSolver::solve_xor_gate(initial_witness, xor_gate) - // We compute the result because the other gates may want to use the assignment to generate their assignments + if unsolvable { + GateResolution::Skip + } else if let Err(op) = Self::solve_gadget_call(initial_witness, gc) { + GateResolution::UnsupportedOpcode(op) + } else { + GateResolution::Resolved } - Gate::GadgetCall(gc) => { - let mut unsolvable = false; - for i in &gc.inputs { - if !initial_witness.contains_key(&i.witness) { - unsolvable = true; - break; - } - } - if unsolvable { - true - } else if let Err(op) = Self::solve_gadget_call(initial_witness, gc) { - return GateResolution::UnsupportedOpcode(op); - } else { - false + } + Gate::Directive(directive) => match directive { + Directive::Invert { x, result } => match initial_witness.get(x) { + None => GateResolution::Skip, + Some(val) => { + let inverse = val.inverse(); + initial_witness.insert(*result, inverse); + GateResolution::Resolved } - } - Gate::Directive(directive) => match directive { - Directive::Invert { x, result } => match initial_witness.get(x) { - None => true, - Some(val) => { - let inverse = val.inverse(); - initial_witness.insert(*result, inverse); - false - } - }, - Directive::Quotient { a, b, q, r, predicate } => { - match ( - Self::get_value(a, initial_witness), - Self::get_value(b, initial_witness), - ) { - (Some(val_a), Some(val_b)) => { - let int_a = BigUint::from_bytes_be(&val_a.to_bytes()); - let int_b = BigUint::from_bytes_be(&val_b.to_bytes()); - let default = Box::new(Expression::one()); - let pred = predicate.as_ref().unwrap_or(&default); - if let Some(pred_value) = Self::get_value(pred, initial_witness) { - let (int_r, int_q) = if pred_value.is_zero() { - (BigUint::zero(), BigUint::zero()) - } else { - (&int_a % &int_b, &int_a / &int_b) - }; - initial_witness.insert( - *q, - FieldElement::from_be_bytes_reduce(&int_q.to_bytes_be()), - ); - initial_witness.insert( - *r, - FieldElement::from_be_bytes_reduce(&int_r.to_bytes_be()), - ); - false + }, + Directive::Quotient { a, b, q, r, predicate } => { + match (Self::get_value(a, initial_witness), Self::get_value(b, initial_witness)) + { + (Some(val_a), Some(val_b)) => { + let int_a = BigUint::from_bytes_be(&val_a.to_bytes()); + let int_b = BigUint::from_bytes_be(&val_b.to_bytes()); + let default = Box::new(Expression::one()); + let pred = predicate.as_ref().unwrap_or(&default); + if let Some(pred_value) = Self::get_value(pred, initial_witness) { + let (int_r, int_q) = if pred_value.is_zero() { + (BigUint::zero(), BigUint::zero()) } else { - true - } + (&int_a % &int_b, &int_a / &int_b) + }; + initial_witness.insert( + *q, + FieldElement::from_be_bytes_reduce(&int_q.to_bytes_be()), + ); + initial_witness.insert( + *r, + FieldElement::from_be_bytes_reduce(&int_r.to_bytes_be()), + ); + GateResolution::Resolved + } else { + GateResolution::Skip } - _ => true, } + _ => GateResolution::Skip, } - Directive::Truncate { a, b, c, bit_size } => match initial_witness.get(a) { - Some(val_a) => { - let pow: BigUint = BigUint::one() << bit_size; + } + Directive::Truncate { a, b, c, bit_size } => match initial_witness.get(a) { + Some(val_a) => { + let pow: BigUint = BigUint::one() << bit_size; - let int_a = BigUint::from_bytes_be(&val_a.to_bytes()); - let int_b: BigUint = &int_a % &pow; - let int_c: BigUint = (&int_a - &int_b) / &pow; + let int_a = BigUint::from_bytes_be(&val_a.to_bytes()); + let int_b: BigUint = &int_a % &pow; + let int_c: BigUint = (&int_a - &int_b) / &pow; - initial_witness.insert( - *b, - FieldElement::from_be_bytes_reduce(&int_b.to_bytes_be()), - ); - initial_witness.insert( - *c, - FieldElement::from_be_bytes_reduce(&int_c.to_bytes_be()), - ); - false - } - _ => true, - }, - Directive::Split { a, b, bit_size } => { - match Self::get_value(a, initial_witness) { - Some(val_a) => { - let a_big = BigUint::from_bytes_be(&val_a.to_bytes()); - for i in 0..*bit_size { - let j = i as usize; - let v = if a_big.bit(j as u64) { - FieldElement::one() - } else { - FieldElement::zero() - }; - initial_witness.insert(b[j], v); - } - false - } - _ => true, + initial_witness + .insert(*b, FieldElement::from_be_bytes_reduce(&int_b.to_bytes_be())); + initial_witness + .insert(*c, FieldElement::from_be_bytes_reduce(&int_c.to_bytes_be())); + GateResolution::Resolved + } + _ => GateResolution::Skip, + }, + Directive::Split { a, b, bit_size } => match Self::get_value(a, initial_witness) { + Some(val_a) => { + let a_big = BigUint::from_bytes_be(&val_a.to_bytes()); + for i in 0..*bit_size { + let j = i as usize; + let v = if a_big.bit(j as u64) { + FieldElement::one() + } else { + FieldElement::zero() + }; + initial_witness.insert(b[j], v); } + GateResolution::Resolved } - Directive::Oddrange { a, b, r, bit_size } => match initial_witness.get(a) { - Some(val_a) => { - let int_a = BigUint::from_bytes_be(&val_a.to_bytes()); - let pow: BigUint = BigUint::one() << (bit_size - 1); - if int_a >= (&pow << 1) { - return GateResolution::UnsatisfiedConstrain; - } - let bb = &int_a & &pow; - let int_r = &int_a - &bb; - let int_b = &bb >> (bit_size - 1); - - initial_witness.insert( - *b, - FieldElement::from_be_bytes_reduce(&int_b.to_bytes_be()), - ); - initial_witness.insert( - *r, - FieldElement::from_be_bytes_reduce(&int_r.to_bytes_be()), - ); - false + _ => GateResolution::Skip, + }, + Directive::Oddrange { a, b, r, bit_size } => match initial_witness.get(a) { + Some(val_a) => { + let int_a = BigUint::from_bytes_be(&val_a.to_bytes()); + let pow: BigUint = BigUint::one() << (bit_size - 1); + if int_a >= (&pow << 1) { + return GateResolution::UnsatisfiedConstrain; } - _ => true, - }, + let bb = &int_a & &pow; + let int_r = &int_a - &bb; + let int_b = &bb >> (bit_size - 1); + + initial_witness + .insert(*b, FieldElement::from_be_bytes_reduce(&int_b.to_bytes_be())); + initial_witness + .insert(*r, FieldElement::from_be_bytes_reduce(&int_r.to_bytes_be())); + GateResolution::Resolved + } + _ => GateResolution::Skip, }, + }, + } + } + + fn solve( + &self, + initial_witness: &mut BTreeMap, + mut gates: Vec, + ) -> GateResolution { + let mut gates2: Vec = Vec::new(); + let mut pass_nb = 0; + let mut gates_to_resolve = &mut gates; + let mut unresolved_gates = &mut gates2; + let mut ctx = BinarySolver::new(); + let mut binary_solve = -1; + + while !gates_to_resolve.is_empty() { + unresolved_gates.clear(); + + let mut process = |gate| { + let mut result = self.solve_gate(initial_witness, gate); + if binary_solve >= 0 && result == GateResolution::Skip { + result = ctx.solve(gate, initial_witness); + } + result }; - if unsolved { - unsolved_gates.push(gate); + + if binary_solve != 0 { + for gate in gates_to_resolve.iter() { + let result = process(gate); + match result { + GateResolution::Skip => unresolved_gates.push(gate.clone()), + GateResolution::Resolved => (), + _ => return result, + } + } + } else { + //we go backward because binary solver should execute only when the program returns an array + //in that case it is a bit more efficient to go backwards, although both ways work. + for gate in gates_to_resolve.iter().rev() { + let result = process(gate); + match result { + GateResolution::Skip => unresolved_gates.push(gate.clone()), + GateResolution::Resolved => (), + _ => return result, + } + } + } + if binary_solve > 0 { + binary_solve -= 1; + } else if gates_to_resolve.len() == unresolved_gates.len() && binary_solve < 0 { + // activate the binary solver with 2 forward passes in order to properly identify booleans first + binary_solve = 2; + } + + if pass_nb % 2 == 0 { + gates_to_resolve = &mut gates2; + unresolved_gates = &mut gates; + } else { + unresolved_gates = &mut gates2; + gates_to_resolve = &mut gates; } + pass_nb += 1; } - self.solve(initial_witness, unsolved_gates) + GateResolution::Resolved } fn solve_gadget_call( diff --git a/crates/acvm/src/pwg/arithmetic.rs b/crates/acvm/src/pwg/arithmetic.rs index 1c7e59f5542..95470b2edd8 100644 --- a/crates/acvm/src/pwg/arithmetic.rs +++ b/crates/acvm/src/pwg/arithmetic.rs @@ -106,6 +106,23 @@ impl ArithmeticSolver { } } + fn solve_mul_term_helper( + term: &(FieldElement, Witness, Witness), + witness_assignments: &BTreeMap, + ) -> MulTerm { + let (q_m, w_l, w_r) = term; + // Check if these values are in the witness assignments + let w_l_value = witness_assignments.get(w_l); + let w_r_value = witness_assignments.get(w_r); + + match (w_l_value, w_r_value) { + (None, None) => MulTerm::TooManyUnknowns, + (Some(w_l), Some(w_r)) => MulTerm::Solved(*q_m * *w_l * *w_r), + (None, Some(w_r)) => MulTerm::OneUnknown(*q_m * *w_r, *w_l), + (Some(w_l), None) => MulTerm::OneUnknown(*q_m * *w_l, *w_r), + } + } + /// Returns the evaluation of the multiplication term in the arithmetic gate /// If the witness values are not known, then the function returns a None /// XXX: Do we need to account for the case where 5xy + 6x = 0 ? We do not know y, but it can be solved given x . But I believe x can be solved with another gate @@ -118,26 +135,24 @@ impl ArithmeticSolver { // We are assuming it has been optimised. match arith_gate.mul_terms.len() { 0 => MulTerm::Solved(FieldElement::zero()), - 1 => { - let q_m = &arith_gate.mul_terms[0].0; - let w_l = &arith_gate.mul_terms[0].1; - let w_r = &arith_gate.mul_terms[0].2; - - // Check if these values are in the witness assignments - let w_l_value = witness_assignments.get(w_l); - let w_r_value = witness_assignments.get(w_r); - - match (w_l_value, w_r_value) { - (None, None) => MulTerm::TooManyUnknowns, - (Some(w_l), Some(w_r)) => MulTerm::Solved(*q_m * *w_l * *w_r), - (None, Some(w_r)) => MulTerm::OneUnknown(*q_m * *w_r, *w_l), - (Some(w_l), None) => MulTerm::OneUnknown(*q_m * *w_l, *w_r), - } - } + 1 => ArithmeticSolver::solve_mul_term_helper( + &arith_gate.mul_terms[0], + witness_assignments, + ), _ => panic!("Mul term in the arithmetic gate must contain either zero or one term"), } } + fn solve_fan_in_term_helper( + term: &(FieldElement, Witness), + witness_assignments: &BTreeMap, + ) -> Option { + let (q_l, w_l) = term; + // Check if we have w_l + let w_l_value = witness_assignments.get(w_l); + w_l_value.map(|a| *q_l * *a) + } + /// Returns the summation of all of the variables, plus the unknown variable /// Returns None, if there is more than one unknown variable /// We cannot assign @@ -154,19 +169,14 @@ impl ArithmeticSolver { let mut result = FieldElement::zero(); for term in arith_gate.linear_combinations.iter() { - let q_l = term.0; - let w_l = &term.1; - - // Check if we have w_l - let w_l_value = witness_assignments.get(w_l); - - match w_l_value { - Some(a) => result += q_l * *a, + let value = ArithmeticSolver::solve_fan_in_term_helper(term, witness_assignments); + match value { + Some(a) => result += a, None => { unknown_variable = *term; num_unknowns += 1; } - }; + } // If we have more than 1 unknown, then we cannot solve this equation if num_unknowns > 1 { @@ -180,6 +190,39 @@ impl ArithmeticSolver { GateStatus::GateSolvable(result, unknown_variable) } + + // Partially evaluate the gate using the known witnesses + pub fn evaluate( + expr: &Expression, + initial_witness: &BTreeMap, + ) -> Expression { + let mut result = Expression::default(); + for &(c, w1, w2) in &expr.mul_terms { + let mul_result = ArithmeticSolver::solve_mul_term_helper(&(c, w1, w2), initial_witness); + match mul_result { + MulTerm::OneUnknown(v, w) => { + if !v.is_zero() { + result.linear_combinations.push((v, w)); + } + } + MulTerm::TooManyUnknowns => { + if !c.is_zero() { + result.mul_terms.push((c, w1, w2)); + } + } + MulTerm::Solved(f) => result.q_c += f, + } + } + for &(c, w) in &expr.linear_combinations { + if let Some(f) = ArithmeticSolver::solve_fan_in_term_helper(&(c, w), initial_witness) { + result.q_c += f; + } else if !c.is_zero() { + result.linear_combinations.push((c, w)); + } + } + result.q_c += expr.q_c; + result + } } #[test] diff --git a/crates/acvm/src/pwg/binary.rs b/crates/acvm/src/pwg/binary.rs new file mode 100644 index 00000000000..317099f78f4 --- /dev/null +++ b/crates/acvm/src/pwg/binary.rs @@ -0,0 +1,234 @@ +use std::collections::{BTreeMap, HashMap, HashSet}; + +use acir::{ + circuit::{gate::Directive, Gate}, + native_types::{Expression, Witness}, + FieldElement, +}; +use num_bigint::BigUint; +use num_traits::{One, Zero}; + +use crate::GateResolution; + +pub struct BinarySolver { + binary_witness: HashSet, + invert_witness: HashMap, + positive_witness: HashMap, +} + +impl Default for BinarySolver { + fn default() -> Self { + Self::new() + } +} + +impl BinarySolver { + pub fn new() -> BinarySolver { + BinarySolver { + binary_witness: HashSet::new(), + invert_witness: HashMap::new(), + positive_witness: HashMap::new(), + } + } + + pub fn is_boolean(&self, w: &Witness) -> bool { + self.binary_witness.contains(w) + } + + pub fn are_inverse(&self, w1: &Witness, w2: &Witness) -> bool { + self.invert_witness.get(w1) == Some(w2) || self.invert_witness.get(w2) == Some(w1) + } + + pub fn are_boolean(&self, w1: &Witness, w2: &Witness) -> bool { + self.are_inverse(w1, w2) || (self.is_boolean(w1) && self.is_boolean(w2)) + } + + pub fn get_max_value(&self, w: &Witness) -> Option { + if self.is_boolean(w) { + Some(BigUint::one()) + } else { + self.positive_witness.get(w).cloned() + } + } + + pub fn solve( + &mut self, + gate: &Gate, + initial_witness: &mut BTreeMap, + ) -> GateResolution { + let mut result = GateResolution::Skip; + if let Gate::Arithmetic(arith) = gate { + let partial_gate = + super::arithmetic::ArithmeticSolver::evaluate(arith, initial_witness); + result = self.solve_booleans(initial_witness, &partial_gate); + self.lookup_booleans(&partial_gate); + } else { + self.lookup_binaries(gate); + } + result + } + + /// Solve (some) arithemtic expression which is only using booleans + pub fn solve_booleans( + &self, + initial_witness: &mut BTreeMap, + gate: &Expression, + ) -> GateResolution { + let result = self.solve_inverse(gate, initial_witness); + match result { + GateResolution::Resolved + | GateResolution::UnsatisfiedConstrain + | GateResolution::UnknownError(_) => return result, + GateResolution::Skip => (), + GateResolution::UnsupportedOpcode(_) => unreachable!(), + } + + if let Some(max) = self.is_binary(gate) { + if max < FieldElement::modulus() { + if gate.q_c == FieldElement::zero() { + for (_, w) in &gate.linear_combinations { + initial_witness.insert(*w, FieldElement::zero()); + } + GateResolution::Resolved + } else { + GateResolution::UnsatisfiedConstrain + } + } else { + GateResolution::Skip + } + } else { + GateResolution::Skip + } + } + + // checks whether the expression uses only booleans/positive witness and returns the max value of the expression in that case + fn is_binary(&self, gate: &Expression) -> Option { + let mut max = BigUint::zero(); + for (c, w1, w2) in &gate.mul_terms { + if !self.are_boolean(w1, w2) { + return None; + } + max += BigUint::from_bytes_be(&c.to_bytes()); + } + for (c, w) in &gate.linear_combinations { + if let Some(v) = self.get_max_value(w) { + max += BigUint::from_bytes_be(&c.to_bytes()) * v; + } else { + return None; + } + } + if max > FieldElement::modulus() { + return None; + } + Some(max + BigUint::from_bytes_be(&gate.q_c.to_bytes())) + } + + fn solve_inverse( + &self, + gate: &Expression, + initial_witness: &mut BTreeMap, + ) -> GateResolution { + if gate.mul_terms.len() == 1 + && self.are_inverse(&gate.mul_terms[0].1, &gate.mul_terms[0].2) + && gate.linear_combinations.is_empty() + { + if gate.q_c.is_zero() { + initial_witness.insert(gate.mul_terms[0].1, FieldElement::zero()); + initial_witness.insert(gate.mul_terms[0].2, FieldElement::zero()); + return GateResolution::Resolved; + } else if !gate.q_c.is_one() { + return GateResolution::UnsatisfiedConstrain; + } + } + + GateResolution::Skip + } + + // look for boolean constraint and add boolean witness to a map + pub fn lookup_booleans(&mut self, arith: &Expression) { + let mut x = usize::MAX; + if arith.mul_terms.len() == 1 && arith.linear_combinations.len() == 1 { + // x*x = x + if arith.mul_terms[0].1 == arith.mul_terms[0].2 + && arith.mul_terms[0].1 == arith.linear_combinations[0].1 + && arith.q_c.is_zero() + && (arith.mul_terms[0].0 + arith.linear_combinations[0].0).is_zero() + { + x = 0; + } else { + // x = a*b, a,b booleans or inverse + if self.are_boolean(&arith.mul_terms[0].1, &arith.mul_terms[0].2) { + if arith.q_c.is_zero() { + if (arith.mul_terms[0].0 + arith.linear_combinations[0].0).is_zero() { + x = 0; + } + } else if (arith.mul_terms[0].0 + arith.q_c).is_zero() + && arith.mul_terms[0].0 == arith.linear_combinations[0].0 + { + x = 0; + } + } + } + } else if arith.mul_terms.is_empty() && arith.linear_combinations.len() == 2 { + //x=y + let z = if self.is_boolean(&arith.linear_combinations[0].1) + && !self.is_boolean(&arith.linear_combinations[1].1) + { + 1 + } else if self.is_boolean(&arith.linear_combinations[1].1) + && !self.is_boolean(&arith.linear_combinations[0].1) + { + 0 + } else { + usize::MAX + }; + if z < usize::MAX { + if arith.q_c.is_zero() { + if (arith.linear_combinations[0].0 + arith.linear_combinations[1].0).is_zero() { + x = z; + } + } else if (arith.q_c + arith.linear_combinations[1].0).is_zero() + && arith.linear_combinations[0].0 == arith.linear_combinations[1].0 + { + x = z; + } + } + } else if arith.mul_terms.is_empty() && arith.linear_combinations.len() > 2 { + //"binary" gates 'optimised' by the optimiser should have an intermediate variable and a bunch of booleans + let mut max = BigUint::from_bytes_be(&arith.q_c.to_bytes()); + for (i, lin) in arith.linear_combinations.iter().enumerate() { + if let Some(v) = self.get_max_value(&lin.1) { + max += v * BigUint::from_bytes_be(&lin.0.to_bytes()); + } else if x != usize::MAX { + x = usize::MAX; + break; + } else { + x = i; + } + } + if max < FieldElement::modulus() + && x != usize::MAX + && arith.linear_combinations[x].0 == -FieldElement::one() + { + self.positive_witness.insert(arith.linear_combinations[x].1, max); + x = usize::MAX; + } + } + if x < usize::MAX { + self.binary_witness.insert(arith.linear_combinations[x].1); + } + } + + // look for boolean and inverse constraints + pub fn lookup_binaries(&mut self, gate: &Gate) { + match gate { + Gate::Directive(Directive::Invert { x, result }) => { + self.invert_witness.insert(*x, *result); + } + Gate::Arithmetic(a) => { + self.lookup_booleans(a); + } + _ => (), + } + } +} diff --git a/crates/acvm/src/pwg/logic.rs b/crates/acvm/src/pwg/logic.rs index becd109c670..b98fe2ef387 100644 --- a/crates/acvm/src/pwg/logic.rs +++ b/crates/acvm/src/pwg/logic.rs @@ -3,6 +3,8 @@ use acir::native_types::Witness; use noir_field::FieldElement; use std::collections::BTreeMap; +use crate::GateResolution; + pub struct LogicSolver {} impl LogicSolver { @@ -14,13 +16,13 @@ impl LogicSolver { result: Witness, num_bits: u32, is_xor_gate: bool, - ) -> bool { + ) -> GateResolution { let w_l = initial_witness.get(a); let w_r = initial_witness.get(b); let (w_l_value, w_r_value) = match (w_l, w_r) { (Some(w_l_value), Some(w_r_value)) => (w_l_value, w_r_value), - (_, _) => return false, + (_, _) => return GateResolution::Skip, }; if is_xor_gate { @@ -30,13 +32,13 @@ impl LogicSolver { let assignment = w_l_value.and(w_r_value, num_bits); initial_witness.insert(result, assignment); } - true + GateResolution::Resolved } pub fn solve_and_gate( initial_witness: &mut BTreeMap, gate: &AndGate, - ) -> bool { + ) -> GateResolution { LogicSolver::solve_logic_gate( initial_witness, &gate.a, @@ -49,7 +51,7 @@ impl LogicSolver { pub fn solve_xor_gate( initial_witness: &mut BTreeMap, gate: &XorGate, - ) -> bool { + ) -> GateResolution { LogicSolver::solve_logic_gate( initial_witness, &gate.a, diff --git a/crates/acvm/src/pwg/mod.rs b/crates/acvm/src/pwg/mod.rs index 50fb4cb7701..f8cf034a34c 100644 --- a/crates/acvm/src/pwg/mod.rs +++ b/crates/acvm/src/pwg/mod.rs @@ -6,6 +6,7 @@ use std::collections::BTreeMap; // XXX: This can possible be refactored to be default trait methods pub mod arithmetic; +pub mod binary; pub mod hash; pub mod logic; pub mod signature; diff --git a/crates/nargo/src/cli/prove_cmd.rs b/crates/nargo/src/cli/prove_cmd.rs index 340cfa29e1f..ca425bf1367 100644 --- a/crates/nargo/src/cli/prove_cmd.rs +++ b/crates/nargo/src/cli/prove_cmd.rs @@ -94,13 +94,6 @@ fn process_abi_with_input( ); return_witness = Some(Witness::new(index + WITNESS_OFFSET)); - //We do not support undefined arrays for now - TODO - if return_witness_len != 1 { - return Err(CliError::Generic( - "Values of array returned from main must be specified in prover toml file" - .to_string(), - )); - } index += return_witness_len; //XXX We do not support (yet) array of arrays } diff --git a/crates/nargo/tests/test_data/main_return/Prover.toml b/crates/nargo/tests/test_data/main_return/Prover.toml index ef1ca7bb7e8..a67c842430a 100644 --- a/crates/nargo/tests/test_data/main_return/Prover.toml +++ b/crates/nargo/tests/test_data/main_return/Prover.toml @@ -1,2 +1,3 @@ -return = "" -x = "8" +x = [5,9,12,66,70] +y = [45,89] +return = "" \ No newline at end of file diff --git a/crates/nargo/tests/test_data/main_return/src/main.nr b/crates/nargo/tests/test_data/main_return/src/main.nr index aefa2532731..4a9241250e8 100644 --- a/crates/nargo/tests/test_data/main_return/src/main.nr +++ b/crates/nargo/tests/test_data/main_return/src/main.nr @@ -1,3 +1,15 @@ -fn main(x: Field) -> pub Field { - x +global N = 100; + +fn main (x: [u8;5], y:[Field;2]) -> pub [Field; N] +{ + let mut r = [0;N]; + for i in 0..N { + let id = i as u32 /5; + let j = i -5*id as Field; + let ic = i as u32/2; + let k = i-2*ic as Field; + r[i] = x[j] as Field + y[k]; + }; + r } + \ No newline at end of file diff --git a/crates/nargo/tests/test_data/sha256/Prover.toml b/crates/nargo/tests/test_data/sha256/Prover.toml index c4df1b749bb..2da5c438059 100644 --- a/crates/nargo/tests/test_data/sha256/Prover.toml +++ b/crates/nargo/tests/test_data/sha256/Prover.toml @@ -34,3 +34,4 @@ result = [ 0x73, 0x2b, ] +return = "" \ No newline at end of file diff --git a/crates/nargo/tests/test_data/sha256/src/main.nr b/crates/nargo/tests/test_data/sha256/src/main.nr index bf2249c4faf..07f0df00305 100644 --- a/crates/nargo/tests/test_data/sha256/src/main.nr +++ b/crates/nargo/tests/test_data/sha256/src/main.nr @@ -11,9 +11,10 @@ // This can be done in ACIR! use dep::std; -fn main(x: Field, result: [u8; 32]) { +fn main(x: Field, result: [u8; 32]) -> pub [u8; 32]{ // We use the `as` keyword here to denote the fact that we want to take just the first byte from the x Field // The padding is taken care of by the program let digest = std::hash::sha256([x as u8]); constrain digest == result; + digest } From 673d03f439adce86df54e5ff5a5bf194cecb4426 Mon Sep 17 00:00:00 2001 From: guipublic Date: Thu, 1 Dec 2022 10:34:16 +0000 Subject: [PATCH 2/9] Code review --- crates/acvm/src/lib.rs | 59 ++++++++++++++----------------- crates/acvm/src/pwg/binary.rs | 42 +++++++++++----------- crates/nargo/src/cli/prove_cmd.rs | 2 +- 3 files changed, 49 insertions(+), 54 deletions(-) diff --git a/crates/acvm/src/lib.rs b/crates/acvm/src/lib.rs index 2e673839643..8d564ed4149 100644 --- a/crates/acvm/src/lib.rs +++ b/crates/acvm/src/lib.rs @@ -31,6 +31,7 @@ pub enum GateResolution { UnknownError(String), //Generic error UnsupportedOpcode(OPCODE), //Unsupported Opcode UnsatisfiedConstrain, //Gate is not satisfied + Solved(usize), //Circuit is solved, after a number of passes } pub trait Backend: SmartContract + ProofSystemCompiler + PartialWitnessGenerator {} @@ -186,64 +187,58 @@ pub trait PartialWitnessGenerator { fn solve( &self, initial_witness: &mut BTreeMap, - mut gates: Vec, + mut gates_to_resolve: Vec, ) -> GateResolution { - let mut gates2: Vec = Vec::new(); - let mut pass_nb = 0; - let mut gates_to_resolve = &mut gates; - let mut unresolved_gates = &mut gates2; + let mut unresolved_gates: Vec = Vec::new(); + let mut pass_number = 0; let mut ctx = BinarySolver::new(); - let mut binary_solve = -1; + //binary_solve is used to manage the binary solving mode: + //binary_solve.is_none() => binary solve is not activated + //binary_solve == Some(forward_pass) => binary solve is activated and will do forward_pass forward passes, decreasing at each pass until it reach 0 where the process will be backward + let mut binary_solve = None; while !gates_to_resolve.is_empty() { unresolved_gates.clear(); let mut process = |gate| { let mut result = self.solve_gate(initial_witness, gate); - if binary_solve >= 0 && result == GateResolution::Skip { + if binary_solve.is_some() && result == GateResolution::Skip { result = ctx.solve(gate, initial_witness); } result }; - if binary_solve != 0 { - for gate in gates_to_resolve.iter() { - let result = process(gate); - match result { + if binary_solve == Some(0) { + //we go backward because binary solver should execute only when the program returns an array + //in that case it is a bit more efficient to go backwards, although both ways work. + for gate in gates_to_resolve.iter().rev() { + match process(gate) { GateResolution::Skip => unresolved_gates.push(gate.clone()), GateResolution::Resolved => (), - _ => return result, + resolution => return resolution, } } } else { - //we go backward because binary solver should execute only when the program returns an array - //in that case it is a bit more efficient to go backwards, although both ways work. - for gate in gates_to_resolve.iter().rev() { - let result = process(gate); - match result { + for gate in gates_to_resolve.iter() { + match process(gate) { GateResolution::Skip => unresolved_gates.push(gate.clone()), GateResolution::Resolved => (), - _ => return result, + resolution => return resolution, } } } - if binary_solve > 0 { - binary_solve -= 1; - } else if gates_to_resolve.len() == unresolved_gates.len() && binary_solve < 0 { - // activate the binary solver with 2 forward passes in order to properly identify booleans first - binary_solve = 2; - } - if pass_nb % 2 == 0 { - gates_to_resolve = &mut gates2; - unresolved_gates = &mut gates; - } else { - unresolved_gates = &mut gates2; - gates_to_resolve = &mut gates; + if let Some(forward_pass) = binary_solve { + if forward_pass > 0 { + binary_solve = Some(forward_pass - 1); + } + } else if gates_to_resolve.len() == unresolved_gates.len() { + binary_solve = Some(2); } - pass_nb += 1; + std::mem::swap(&mut gates_to_resolve, &mut unresolved_gates); + pass_number += 1; } - GateResolution::Resolved + GateResolution::Solved(pass_number) } fn solve_gadget_call( diff --git a/crates/acvm/src/pwg/binary.rs b/crates/acvm/src/pwg/binary.rs index 317099f78f4..9c4140feed4 100644 --- a/crates/acvm/src/pwg/binary.rs +++ b/crates/acvm/src/pwg/binary.rs @@ -61,7 +61,7 @@ impl BinarySolver { let partial_gate = super::arithmetic::ArithmeticSolver::evaluate(arith, initial_witness); result = self.solve_booleans(initial_witness, &partial_gate); - self.lookup_booleans(&partial_gate); + self.identify_booleans(&partial_gate); } else { self.lookup_binaries(gate); } @@ -80,7 +80,7 @@ impl BinarySolver { | GateResolution::UnsatisfiedConstrain | GateResolution::UnknownError(_) => return result, GateResolution::Skip => (), - GateResolution::UnsupportedOpcode(_) => unreachable!(), + GateResolution::UnsupportedOpcode(_) | GateResolution::Solved(_) => unreachable!(), } if let Some(max) = self.is_binary(gate) { @@ -145,8 +145,8 @@ impl BinarySolver { } // look for boolean constraint and add boolean witness to a map - pub fn lookup_booleans(&mut self, arith: &Expression) { - let mut x = usize::MAX; + pub fn identify_booleans(&mut self, arith: &Expression) { + let mut x = None; if arith.mul_terms.len() == 1 && arith.linear_combinations.len() == 1 { // x*x = x if arith.mul_terms[0].1 == arith.mul_terms[0].2 @@ -154,18 +154,18 @@ impl BinarySolver { && arith.q_c.is_zero() && (arith.mul_terms[0].0 + arith.linear_combinations[0].0).is_zero() { - x = 0; + x = Some(0); } else { // x = a*b, a,b booleans or inverse if self.are_boolean(&arith.mul_terms[0].1, &arith.mul_terms[0].2) { if arith.q_c.is_zero() { if (arith.mul_terms[0].0 + arith.linear_combinations[0].0).is_zero() { - x = 0; + x = Some(0); } } else if (arith.mul_terms[0].0 + arith.q_c).is_zero() && arith.mul_terms[0].0 == arith.linear_combinations[0].0 { - x = 0; + x = Some(0); } } } @@ -174,15 +174,15 @@ impl BinarySolver { let z = if self.is_boolean(&arith.linear_combinations[0].1) && !self.is_boolean(&arith.linear_combinations[1].1) { - 1 + Some(1) } else if self.is_boolean(&arith.linear_combinations[1].1) && !self.is_boolean(&arith.linear_combinations[0].1) { - 0 + Some(0) } else { - usize::MAX + None }; - if z < usize::MAX { + if z.is_some() { if arith.q_c.is_zero() { if (arith.linear_combinations[0].0 + arith.linear_combinations[1].0).is_zero() { x = z; @@ -190,7 +190,7 @@ impl BinarySolver { } else if (arith.q_c + arith.linear_combinations[1].0).is_zero() && arith.linear_combinations[0].0 == arith.linear_combinations[1].0 { - x = z; + x = Some(0); } } } else if arith.mul_terms.is_empty() && arith.linear_combinations.len() > 2 { @@ -199,22 +199,22 @@ impl BinarySolver { for (i, lin) in arith.linear_combinations.iter().enumerate() { if let Some(v) = self.get_max_value(&lin.1) { max += v * BigUint::from_bytes_be(&lin.0.to_bytes()); - } else if x != usize::MAX { - x = usize::MAX; + } else if x.is_some() { + x = None; break; } else { - x = i; + x = Some(i); } } if max < FieldElement::modulus() - && x != usize::MAX - && arith.linear_combinations[x].0 == -FieldElement::one() + && x.is_some() + && arith.linear_combinations[x.unwrap()].0 == -FieldElement::one() { - self.positive_witness.insert(arith.linear_combinations[x].1, max); - x = usize::MAX; + self.positive_witness.insert(arith.linear_combinations[x.unwrap()].1, max); + x = None; } } - if x < usize::MAX { + if let Some(x) = x { self.binary_witness.insert(arith.linear_combinations[x].1); } } @@ -226,7 +226,7 @@ impl BinarySolver { self.invert_witness.insert(*x, *result); } Gate::Arithmetic(a) => { - self.lookup_booleans(a); + self.identify_booleans(a); } _ => (), } diff --git a/crates/nargo/src/cli/prove_cmd.rs b/crates/nargo/src/cli/prove_cmd.rs index 3870e62e1d5..49dca3031a1 100644 --- a/crates/nargo/src/cli/prove_cmd.rs +++ b/crates/nargo/src/cli/prove_cmd.rs @@ -182,7 +182,7 @@ pub fn solve_witness>( GateResolution::UnsatisfiedConstrain => return Err(CliError::Generic( "could not satisfy all constraints".to_string() )), - GateResolution::Resolved => (), + GateResolution::Resolved | GateResolution::Solved(_)=> (), _ => unreachable!(), } From 719d8d24508db92e1efc3a2edfd42d0ed4f1c1cb Mon Sep 17 00:00:00 2001 From: guipublic Date: Fri, 2 Dec 2022 08:58:32 +0000 Subject: [PATCH 3/9] Code review --- crates/acvm/src/pwg/binary.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/crates/acvm/src/pwg/binary.rs b/crates/acvm/src/pwg/binary.rs index 9c4140feed4..789b10da812 100644 --- a/crates/acvm/src/pwg/binary.rs +++ b/crates/acvm/src/pwg/binary.rs @@ -63,7 +63,7 @@ impl BinarySolver { result = self.solve_booleans(initial_witness, &partial_gate); self.identify_booleans(&partial_gate); } else { - self.lookup_binaries(gate); + self.identify_binaries(gate); } result } @@ -219,8 +219,8 @@ impl BinarySolver { } } - // look for boolean and inverse constraints - pub fn lookup_binaries(&mut self, gate: &Gate) { + // identify boolean and inverse constraints in the gate + pub fn identify_binaries(&mut self, gate: &Gate) { match gate { Gate::Directive(Directive::Invert { x, result }) => { self.invert_witness.insert(*x, *result); From e4166c0f97495675457ad05a0773f103d9af6121 Mon Sep 17 00:00:00 2001 From: guipublic Date: Fri, 2 Dec 2022 18:40:24 +0000 Subject: [PATCH 4/9] Code review --- crates/acvm/src/lib.rs | 23 +++++++++-------------- 1 file changed, 9 insertions(+), 14 deletions(-) diff --git a/crates/acvm/src/lib.rs b/crates/acvm/src/lib.rs index 8d564ed4149..f23a1303c52 100644 --- a/crates/acvm/src/lib.rs +++ b/crates/acvm/src/lib.rs @@ -208,23 +208,18 @@ pub trait PartialWitnessGenerator { result }; - if binary_solve == Some(0) { + let gates: Box> = if binary_solve == Some(0) { //we go backward because binary solver should execute only when the program returns an array //in that case it is a bit more efficient to go backwards, although both ways work. - for gate in gates_to_resolve.iter().rev() { - match process(gate) { - GateResolution::Skip => unresolved_gates.push(gate.clone()), - GateResolution::Resolved => (), - resolution => return resolution, - } - } + Box::new(gates_to_resolve.iter().rev()) } else { - for gate in gates_to_resolve.iter() { - match process(gate) { - GateResolution::Skip => unresolved_gates.push(gate.clone()), - GateResolution::Resolved => (), - resolution => return resolution, - } + Box::new(gates_to_resolve.iter()) + }; + for gate in gates { + match process(gate) { + GateResolution::Skip => unresolved_gates.push(gate.clone()), + GateResolution::Resolved => (), + resolution => return resolution, } } From eb2555e5f00a0d7c254fdb5b5a1c30887011e163 Mon Sep 17 00:00:00 2001 From: guipublic Date: Wed, 7 Dec 2022 17:25:15 +0000 Subject: [PATCH 5/9] code review: remove the closure --- crates/acvm/src/lib.rs | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/crates/acvm/src/lib.rs b/crates/acvm/src/lib.rs index f23a1303c52..fe5bdb52e7c 100644 --- a/crates/acvm/src/lib.rs +++ b/crates/acvm/src/lib.rs @@ -200,14 +200,6 @@ pub trait PartialWitnessGenerator { while !gates_to_resolve.is_empty() { unresolved_gates.clear(); - let mut process = |gate| { - let mut result = self.solve_gate(initial_witness, gate); - if binary_solve.is_some() && result == GateResolution::Skip { - result = ctx.solve(gate, initial_witness); - } - result - }; - let gates: Box> = if binary_solve == Some(0) { //we go backward because binary solver should execute only when the program returns an array //in that case it is a bit more efficient to go backwards, although both ways work. @@ -216,7 +208,11 @@ pub trait PartialWitnessGenerator { Box::new(gates_to_resolve.iter()) }; for gate in gates { - match process(gate) { + let mut result = self.solve_gate(initial_witness, gate); + if binary_solve.is_some() && result == GateResolution::Skip { + result = ctx.solve(gate, initial_witness); + } + match result { GateResolution::Skip => unresolved_gates.push(gate.clone()), GateResolution::Resolved => (), resolution => return resolution, From 3d430db98d7c3db50579aaf468f250743be042be Mon Sep 17 00:00:00 2001 From: guipublic Date: Fri, 9 Dec 2022 10:27:06 +0000 Subject: [PATCH 6/9] Code review --- crates/acvm/src/pwg/binary.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/crates/acvm/src/pwg/binary.rs b/crates/acvm/src/pwg/binary.rs index 789b10da812..3ad8a643d38 100644 --- a/crates/acvm/src/pwg/binary.rs +++ b/crates/acvm/src/pwg/binary.rs @@ -10,6 +10,8 @@ use num_traits::{One, Zero}; use crate::GateResolution; +// This structure tracks un-resolved witnesses which are constrained to be booleans or sum of booleans, so that gates which uses only those can be solved. +// This is the case for array equality constraints which are unsolved when the value of arrays returned from main are not supplied in the .toml pub struct BinarySolver { binary_witness: HashSet, invert_witness: HashMap, From aa7093d2e9e2440a4346c2c62167342843ea8f6a Mon Sep 17 00:00:00 2001 From: guipublic Date: Mon, 12 Dec 2022 14:11:53 +0000 Subject: [PATCH 7/9] Code review: remove pass number --- crates/acvm/src/lib.rs | 6 ++---- crates/acvm/src/pwg/binary.rs | 2 +- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/crates/acvm/src/lib.rs b/crates/acvm/src/lib.rs index 1c79bb47dd5..0b28eb1a812 100644 --- a/crates/acvm/src/lib.rs +++ b/crates/acvm/src/lib.rs @@ -31,7 +31,7 @@ pub enum GateResolution { UnknownError(String), //Generic error UnsupportedOpcode(OPCODE), //Unsupported Opcode UnsatisfiedConstrain, //Gate is not satisfied - Solved(usize), //Circuit is solved, after a number of passes + Solved, //Circuit is solved, after a number of passes } pub trait Backend: SmartContract + ProofSystemCompiler + PartialWitnessGenerator {} @@ -190,7 +190,6 @@ pub trait PartialWitnessGenerator { mut gates_to_resolve: Vec, ) -> GateResolution { let mut unresolved_gates: Vec = Vec::new(); - let mut pass_number = 0; let mut ctx = BinarySolver::new(); //binary_solve is used to manage the binary solving mode: //binary_solve.is_none() => binary solve is not activated @@ -227,9 +226,8 @@ pub trait PartialWitnessGenerator { binary_solve = Some(2); } std::mem::swap(&mut gates_to_resolve, &mut unresolved_gates); - pass_number += 1; } - GateResolution::Solved(pass_number) + GateResolution::Solved } fn solve_gadget_call( diff --git a/crates/acvm/src/pwg/binary.rs b/crates/acvm/src/pwg/binary.rs index 3ad8a643d38..ffbf32634cb 100644 --- a/crates/acvm/src/pwg/binary.rs +++ b/crates/acvm/src/pwg/binary.rs @@ -82,7 +82,7 @@ impl BinarySolver { | GateResolution::UnsatisfiedConstrain | GateResolution::UnknownError(_) => return result, GateResolution::Skip => (), - GateResolution::UnsupportedOpcode(_) | GateResolution::Solved(_) => unreachable!(), + GateResolution::UnsupportedOpcode(_) | GateResolution::Solved => unreachable!(), } if let Some(max) = self.is_binary(gate) { From e0e03ab8db9a96ce70faff37683bc6e5b454dad0 Mon Sep 17 00:00:00 2001 From: guipublic Date: Mon, 12 Dec 2022 14:40:43 +0000 Subject: [PATCH 8/9] fix the build --- crates/nargo/src/cli/prove_cmd.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/nargo/src/cli/prove_cmd.rs b/crates/nargo/src/cli/prove_cmd.rs index 04dac7733f5..fc8107af92a 100644 --- a/crates/nargo/src/cli/prove_cmd.rs +++ b/crates/nargo/src/cli/prove_cmd.rs @@ -114,7 +114,7 @@ fn solve_witness( GateResolution::UnsatisfiedConstrain => return Err(CliError::Generic( "could not satisfy all constraints".to_string() )), - GateResolution::Resolved | GateResolution::Solved(_)=> (), + GateResolution::Resolved | GateResolution::Solved => (), _ => unreachable!(), } From da10422319970245252e0a101a9c015cb95a0504 Mon Sep 17 00:00:00 2001 From: guipublic Date: Tue, 13 Dec 2022 09:07:50 +0000 Subject: [PATCH 9/9] Code review --- crates/nargo/src/cli/prove_cmd.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/nargo/src/cli/prove_cmd.rs b/crates/nargo/src/cli/prove_cmd.rs index fc8107af92a..ee840f7813b 100644 --- a/crates/nargo/src/cli/prove_cmd.rs +++ b/crates/nargo/src/cli/prove_cmd.rs @@ -114,7 +114,7 @@ fn solve_witness( GateResolution::UnsatisfiedConstrain => return Err(CliError::Generic( "could not satisfy all constraints".to_string() )), - GateResolution::Resolved | GateResolution::Solved => (), + GateResolution::Solved => (), _ => unreachable!(), }