From f933b8f8e08e11ae5910cf99c16d6db09c1b874a Mon Sep 17 00:00:00 2001 From: kevaundray Date: Sat, 16 Dec 2023 19:44:14 +0000 Subject: [PATCH 01/14] rename Arithmetic Opcode to AssertZero --- acvm-repo/acir/src/circuit/opcodes.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/acvm-repo/acir/src/circuit/opcodes.rs b/acvm-repo/acir/src/circuit/opcodes.rs index 62566fee7fe..eb623d73c4b 100644 --- a/acvm-repo/acir/src/circuit/opcodes.rs +++ b/acvm-repo/acir/src/circuit/opcodes.rs @@ -13,7 +13,7 @@ pub use memory_operation::{BlockId, MemOp}; #[derive(Clone, PartialEq, Eq, Serialize, Deserialize)] pub enum Opcode { - Arithmetic(Expression), + AssertZero(Expression), /// Calls to "gadgets" which rely on backends implementing support for specialized constraints. /// /// Often used for exposing more efficient implementations of SNARK-unfriendly computations. @@ -38,7 +38,7 @@ impl Opcode { // TODO concat!("directive:", directive.name) pub fn name(&self) -> &str { match self { - Opcode::Arithmetic(_) => "arithmetic", + Opcode::AssertZero(_) => "arithmetic", Opcode::Directive(directive) => directive.name(), Opcode::BlackBoxFuncCall(g) => g.name(), Opcode::Brillig(_) => "brillig", @@ -48,12 +48,12 @@ impl Opcode { } pub fn is_arithmetic(&self) -> bool { - matches!(self, Opcode::Arithmetic(_)) + matches!(self, Opcode::AssertZero(_)) } pub fn arithmetic(self) -> Option { match self { - Opcode::Arithmetic(expr) => Some(expr), + Opcode::AssertZero(expr) => Some(expr), _ => None, } } @@ -62,7 +62,7 @@ impl Opcode { impl std::fmt::Display for Opcode { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { - Opcode::Arithmetic(expr) => { + Opcode::AssertZero(expr) => { write!(f, "EXPR [ ")?; for i in &expr.mul_terms { write!(f, "({}, _{}, _{}) ", i.0, i.1.witness_index(), i.2.witness_index())?; From 8196c31d29e1796f75d0ebf0abc6a43e9fa4eb9a Mon Sep 17 00:00:00 2001 From: kevaundray Date: Sat, 16 Dec 2023 19:44:35 +0000 Subject: [PATCH 02/14] refactor code --- acvm-repo/acir/src/circuit/mod.rs | 2 +- .../acir/src/native_types/expression/mod.rs | 2 +- .../acir/tests/test_program_serialization.rs | 2 +- acvm-repo/acvm/src/compiler/optimizers/mod.rs | 4 ++-- .../compiler/optimizers/redundant_range.rs | 10 ++++----- .../acvm/src/compiler/transformers/mod.rs | 4 ++-- acvm-repo/acvm/src/pwg/mod.rs | 2 +- acvm-repo/acvm/tests/solver.rs | 22 +++++++++---------- .../ssa/acir_gen/acir_ir/generated_acir.rs | 4 ++-- .../backend_interface/src/smart_contract.rs | 2 +- tooling/debugger/src/context.rs | 2 +- 11 files changed, 28 insertions(+), 28 deletions(-) diff --git a/acvm-repo/acir/src/circuit/mod.rs b/acvm-repo/acir/src/circuit/mod.rs index 99ab389e31e..df58b949b85 100644 --- a/acvm-repo/acir/src/circuit/mod.rs +++ b/acvm-repo/acir/src/circuit/mod.rs @@ -277,7 +277,7 @@ mod tests { let circuit = Circuit { current_witness_index: 0, opcodes: vec![ - Opcode::Arithmetic(crate::native_types::Expression { + Opcode::AssertZero(crate::native_types::Expression { mul_terms: vec![], linear_combinations: vec![], q_c: FieldElement::from(8u128), diff --git a/acvm-repo/acir/src/native_types/expression/mod.rs b/acvm-repo/acir/src/native_types/expression/mod.rs index fe729720663..c7f2c573ce3 100644 --- a/acvm-repo/acir/src/native_types/expression/mod.rs +++ b/acvm-repo/acir/src/native_types/expression/mod.rs @@ -42,7 +42,7 @@ impl std::fmt::Display for Expression { if let Some(witness) = self.to_witness() { write!(f, "x{}", witness.witness_index()) } else { - write!(f, "%{:?}%", crate::circuit::opcodes::Opcode::Arithmetic(self.clone())) + write!(f, "%{:?}%", crate::circuit::opcodes::Opcode::AssertZero(self.clone())) } } } diff --git a/acvm-repo/acir/tests/test_program_serialization.rs b/acvm-repo/acir/tests/test_program_serialization.rs index ff69ba34437..1f25b665573 100644 --- a/acvm-repo/acir/tests/test_program_serialization.rs +++ b/acvm-repo/acir/tests/test_program_serialization.rs @@ -24,7 +24,7 @@ use brillig::{HeapArray, RegisterIndex, RegisterOrMemory}; #[test] fn addition_circuit() { - let addition = Opcode::Arithmetic(Expression { + let addition = Opcode::AssertZero(Expression { mul_terms: Vec::new(), linear_combinations: vec![ (FieldElement::one(), Witness(1)), diff --git a/acvm-repo/acvm/src/compiler/optimizers/mod.rs b/acvm-repo/acvm/src/compiler/optimizers/mod.rs index 85a97c2c7dc..dd27c0bb937 100644 --- a/acvm-repo/acvm/src/compiler/optimizers/mod.rs +++ b/acvm-repo/acvm/src/compiler/optimizers/mod.rs @@ -31,8 +31,8 @@ pub(super) fn optimize_internal(acir: Circuit) -> (Circuit, Vec) { .opcodes .into_iter() .map(|opcode| { - if let Opcode::Arithmetic(arith_expr) = opcode { - Opcode::Arithmetic(GeneralOptimizer::optimize(arith_expr)) + if let Opcode::AssertZero(arith_expr) = opcode { + Opcode::AssertZero(GeneralOptimizer::optimize(arith_expr)) } else { opcode } diff --git a/acvm-repo/acvm/src/compiler/optimizers/redundant_range.rs b/acvm-repo/acvm/src/compiler/optimizers/redundant_range.rs index 766d3674113..9bd91d495cc 100644 --- a/acvm-repo/acvm/src/compiler/optimizers/redundant_range.rs +++ b/acvm-repo/acvm/src/compiler/optimizers/redundant_range.rs @@ -132,7 +132,7 @@ fn extract_range_opcode(opcode: &Opcode) -> Option<(Witness, u32)> { fn optimized_range_opcode(witness: Witness, num_bits: u32) -> Opcode { if num_bits == 1 { - Opcode::Arithmetic(Expression { + Opcode::AssertZero(Expression { mul_terms: vec![(FieldElement::one(), witness, witness)], linear_combinations: vec![(-FieldElement::one(), witness)], q_c: FieldElement::zero(), @@ -237,10 +237,10 @@ mod tests { // The four Arithmetic opcodes should remain unchanged. let mut circuit = test_circuit(vec![(Witness(1), 16), (Witness(1), 16)]); - circuit.opcodes.push(Opcode::Arithmetic(Expression::default())); - circuit.opcodes.push(Opcode::Arithmetic(Expression::default())); - circuit.opcodes.push(Opcode::Arithmetic(Expression::default())); - circuit.opcodes.push(Opcode::Arithmetic(Expression::default())); + circuit.opcodes.push(Opcode::AssertZero(Expression::default())); + circuit.opcodes.push(Opcode::AssertZero(Expression::default())); + circuit.opcodes.push(Opcode::AssertZero(Expression::default())); + circuit.opcodes.push(Opcode::AssertZero(Expression::default())); let acir_opcode_positions = circuit.opcodes.iter().enumerate().map(|(i, _)| i).collect(); let optimizer = RangeOptimizer::new(circuit); let (optimized_circuit, _) = optimizer.replace_redundant_ranges(acir_opcode_positions); diff --git a/acvm-repo/acvm/src/compiler/transformers/mod.rs b/acvm-repo/acvm/src/compiler/transformers/mod.rs index fc406ba2b54..56e461a7dbb 100644 --- a/acvm-repo/acvm/src/compiler/transformers/mod.rs +++ b/acvm-repo/acvm/src/compiler/transformers/mod.rs @@ -70,7 +70,7 @@ pub(super) fn transform_internal( let mut intermediate_variables: IndexMap = IndexMap::new(); for (index, opcode) in acir.opcodes.into_iter().enumerate() { match opcode { - Opcode::Arithmetic(arith_expr) => { + Opcode::AssertZero(arith_expr) => { let len = intermediate_variables.len(); let arith_expr = transformer.transform( @@ -93,7 +93,7 @@ pub(super) fn transform_internal( new_opcodes.push(arith_expr); for opcode in new_opcodes { new_acir_opcode_positions.push(acir_opcode_positions[index]); - transformed_opcodes.push(Opcode::Arithmetic(opcode)); + transformed_opcodes.push(Opcode::AssertZero(opcode)); } } Opcode::BlackBoxFuncCall(ref func) => { diff --git a/acvm-repo/acvm/src/pwg/mod.rs b/acvm-repo/acvm/src/pwg/mod.rs index 859ad010dcd..435dbd357b0 100644 --- a/acvm-repo/acvm/src/pwg/mod.rs +++ b/acvm-repo/acvm/src/pwg/mod.rs @@ -253,7 +253,7 @@ impl<'a, B: BlackBoxFunctionSolver> ACVM<'a, B> { let opcode = &self.opcodes[self.instruction_pointer]; let resolution = match opcode { - Opcode::Arithmetic(expr) => ArithmeticSolver::solve(&mut self.witness_map, expr), + Opcode::AssertZero(expr) => ArithmeticSolver::solve(&mut self.witness_map, expr), Opcode::BlackBoxFuncCall(bb_func) => { blackbox::solve(self.backend, &mut self.witness_map, bb_func) } diff --git a/acvm-repo/acvm/tests/solver.rs b/acvm-repo/acvm/tests/solver.rs index d578555c5dc..b4011a994a5 100644 --- a/acvm-repo/acvm/tests/solver.rs +++ b/acvm-repo/acvm/tests/solver.rs @@ -111,18 +111,18 @@ fn inversion_brillig_oracle_equivalence() { let opcodes = vec![ Opcode::Brillig(brillig_data), - Opcode::Arithmetic(Expression { + Opcode::AssertZero(Expression { mul_terms: vec![], linear_combinations: vec![(fe_1, w_x), (fe_1, w_y), (-fe_1, w_z)], q_c: fe_0, }), // Opcode::Directive(Directive::Invert { x: w_z, result: w_z_inverse }), - Opcode::Arithmetic(Expression { + Opcode::AssertZero(Expression { mul_terms: vec![(fe_1, w_z, w_z_inverse)], linear_combinations: vec![], q_c: -fe_1, }), - Opcode::Arithmetic(Expression { + Opcode::AssertZero(Expression { mul_terms: vec![], linear_combinations: vec![(-fe_1, w_oracle), (fe_1, w_z_inverse)], q_c: fe_0, @@ -238,18 +238,18 @@ fn double_inversion_brillig_oracle() { let opcodes = vec![ Opcode::Brillig(brillig_data), - Opcode::Arithmetic(Expression { + Opcode::AssertZero(Expression { mul_terms: vec![], linear_combinations: vec![(fe_1, w_x), (fe_1, w_y), (-fe_1, w_z)], q_c: fe_0, }), // Opcode::Directive(Directive::Invert { x: w_z, result: w_z_inverse }), - Opcode::Arithmetic(Expression { + Opcode::AssertZero(Expression { mul_terms: vec![(fe_1, w_z, w_z_inverse)], linear_combinations: vec![], q_c: -fe_1, }), - Opcode::Arithmetic(Expression { + Opcode::AssertZero(Expression { mul_terms: vec![], linear_combinations: vec![(-fe_1, w_oracle), (fe_1, w_z_inverse)], q_c: fe_0, @@ -377,9 +377,9 @@ fn oracle_dependent_execution() { }; let opcodes = vec![ - Opcode::Arithmetic(equality_check), + Opcode::AssertZero(equality_check), Opcode::Brillig(brillig_data), - Opcode::Arithmetic(inverse_equality_check), + Opcode::AssertZero(inverse_equality_check), ]; let witness_assignments = @@ -516,7 +516,7 @@ fn unsatisfied_opcode_resolved() { values.insert(c, FieldElement::from(1_i128)); values.insert(d, FieldElement::from(2_i128)); - let opcodes = vec![Opcode::Arithmetic(opcode_a)]; + let opcodes = vec![Opcode::AssertZero(opcode_a)]; let mut acvm = ACVM::new(&StubbedBackend, &opcodes, values); let solver_status = acvm.solve(); assert_eq!( @@ -595,7 +595,7 @@ fn unsatisfied_opcode_resolved_brillig() { values.insert(w_y, FieldElement::from(1_i128)); values.insert(w_result, FieldElement::from(0_i128)); - let opcodes = vec![brillig_opcode, Opcode::Arithmetic(opcode_a)]; + let opcodes = vec![brillig_opcode, Opcode::AssertZero(opcode_a)]; let mut acvm = ACVM::new(&StubbedBackend, &opcodes, values); let solver_status = acvm.solve(); @@ -630,7 +630,7 @@ fn memory_operations() { predicate: None, }; - let expression = Opcode::Arithmetic(Expression { + let expression = Opcode::AssertZero(Expression { mul_terms: Vec::new(), linear_combinations: vec![ (FieldElement::one(), Witness(7)), diff --git a/compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/generated_acir.rs b/compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/generated_acir.rs index f29d3c9ec05..0ea4d99123c 100644 --- a/compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/generated_acir.rs +++ b/compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/generated_acir.rs @@ -372,7 +372,7 @@ impl GeneratedAcir { /// If `expr` is not zero, then the constraint system will /// fail upon verification. pub(crate) fn assert_is_zero(&mut self, expr: Expression) { - self.push_opcode(AcirOpcode::Arithmetic(expr)); + self.push_opcode(AcirOpcode::AssertZero(expr)); } /// Returns a `Witness` that is constrained to be: @@ -552,7 +552,7 @@ impl GeneratedAcir { // Constrain the network output to out_expr for (b, o) in b.iter().zip(out_expr) { - self.push_opcode(AcirOpcode::Arithmetic(b - o)); + self.push_opcode(AcirOpcode::AssertZero(b - o)); } Ok(()) } diff --git a/tooling/backend_interface/src/smart_contract.rs b/tooling/backend_interface/src/smart_contract.rs index 5dac57c4072..2548079f8e3 100644 --- a/tooling/backend_interface/src/smart_contract.rs +++ b/tooling/backend_interface/src/smart_contract.rs @@ -47,7 +47,7 @@ mod tests { #[test] fn test_smart_contract() -> Result<(), BackendError> { let expression = &(Witness(1) + Witness(2)) - &Expression::from(Witness(3)); - let constraint = Opcode::Arithmetic(expression); + let constraint = Opcode::AssertZero(expression); let circuit = Circuit { current_witness_index: 4, diff --git a/tooling/debugger/src/context.rs b/tooling/debugger/src/context.rs index 1475827fbea..a033d846ae7 100644 --- a/tooling/debugger/src/context.rs +++ b/tooling/debugger/src/context.rs @@ -492,7 +492,7 @@ mod tests { // z = x + y Opcode::Brillig(brillig_opcodes), // x + y - z = 0 - Opcode::Arithmetic(Expression { + Opcode::AssertZero(Expression { mul_terms: vec![], linear_combinations: vec![(fe_1, w_x), (fe_1, w_y), (-fe_1, w_z)], q_c: fe_0, From 7fc1c20b708057882c517a6b45fda56b62a238d9 Mon Sep 17 00:00:00 2001 From: kevaundray Date: Sat, 16 Dec 2023 20:02:11 +0000 Subject: [PATCH 03/14] rename ArithmeticSolver -> ExpressionSolver --- acvm-repo/acvm/src/pwg/arithmetic.rs | 30 ++++++++++++++-------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/acvm-repo/acvm/src/pwg/arithmetic.rs b/acvm-repo/acvm/src/pwg/arithmetic.rs index 93a39fb249c..81462ea495e 100644 --- a/acvm-repo/acvm/src/pwg/arithmetic.rs +++ b/acvm-repo/acvm/src/pwg/arithmetic.rs @@ -5,9 +5,9 @@ use acir::{ use super::{insert_value, ErrorLocation, OpcodeNotSolvable, OpcodeResolutionError}; -/// An Arithmetic solver will take a Circuit's arithmetic opcodes with witness assignments +/// An Expression solver will take a Circuit's assert-zero opcodes with witness assignments /// and create the other witness variables -pub(super) struct ArithmeticSolver; +pub(super) struct ExpressionSolver; #[allow(clippy::enum_variant_names)] pub(super) enum OpcodeStatus { @@ -22,17 +22,17 @@ pub(crate) enum MulTerm { Solved(FieldElement), } -impl ArithmeticSolver { +impl ExpressionSolver { /// Derives the rest of the witness based on the initial low level variables pub(super) fn solve( initial_witness: &mut WitnessMap, opcode: &Expression, ) -> Result<(), OpcodeResolutionError> { - let opcode = &ArithmeticSolver::evaluate(opcode, initial_witness); + let opcode = &ExpressionSolver::evaluate(opcode, initial_witness); // Evaluate multiplication term - let mul_result = ArithmeticSolver::solve_mul_term(opcode, initial_witness); + let mul_result = ExpressionSolver::solve_mul_term(opcode, initial_witness); // Evaluate the fan-in terms - let opcode_status = ArithmeticSolver::solve_fan_in_term(opcode, initial_witness); + let opcode_status = ExpressionSolver::solve_fan_in_term(opcode, initial_witness); match (mul_result, opcode_status) { (MulTerm::TooManyUnknowns, _) | (_, OpcodeStatus::OpcodeUnsolvable) => { @@ -126,7 +126,7 @@ impl ArithmeticSolver { } } - /// Returns the evaluation of the multiplication term in the arithmetic opcode + /// Returns the evaluation of the multiplication term in the expression /// 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 opcode /// XXX: What about making a mul opcode = a constant 5xy + 7 = 0 ? This is the same as the above. @@ -135,11 +135,11 @@ impl ArithmeticSolver { // We are assuming it has been optimized. match arith_opcode.mul_terms.len() { 0 => MulTerm::Solved(FieldElement::zero()), - 1 => ArithmeticSolver::solve_mul_term_helper( + 1 => ExpressionSolver::solve_mul_term_helper( &arith_opcode.mul_terms[0], witness_assignments, ), - _ => panic!("Mul term in the arithmetic opcode must contain either zero or one term"), + _ => panic!("Mul term in the assert-zero opcode must contain either zero or one term"), } } @@ -186,7 +186,7 @@ impl ArithmeticSolver { let mut result = FieldElement::zero(); for term in arith_opcode.linear_combinations.iter() { - let value = ArithmeticSolver::solve_fan_in_term_helper(term, witness_assignments); + let value = ExpressionSolver::solve_fan_in_term_helper(term, witness_assignments); match value { Some(a) => result += a, None => { @@ -212,7 +212,7 @@ impl ArithmeticSolver { pub(super) fn evaluate(expr: &Expression, initial_witness: &WitnessMap) -> 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); + let mul_result = ExpressionSolver::solve_mul_term_helper(&(c, w1, w2), initial_witness); match mul_result { MulTerm::OneUnknown(v, w) => { if !v.is_zero() { @@ -228,7 +228,7 @@ impl ArithmeticSolver { } } for &(c, w) in &expr.linear_combinations { - if let Some(f) = ArithmeticSolver::solve_fan_in_term_helper(&(c, w), initial_witness) { + if let Some(f) = ExpressionSolver::solve_fan_in_term_helper(&(c, w), initial_witness) { result.q_c += f; } else if !c.is_zero() { result.linear_combinations.push((c, w)); @@ -240,7 +240,7 @@ impl ArithmeticSolver { } #[test] -fn arithmetic_smoke_test() { +fn expression_solver_smoke_test() { let a = Witness(0); let b = Witness(1); let c = Witness(2); @@ -274,8 +274,8 @@ fn arithmetic_smoke_test() { values.insert(c, FieldElement::from(1_i128)); values.insert(d, FieldElement::from(1_i128)); - assert_eq!(ArithmeticSolver::solve(&mut values, &opcode_a), Ok(())); - assert_eq!(ArithmeticSolver::solve(&mut values, &opcode_b), Ok(())); + assert_eq!(ExpressionSolver::solve(&mut values, &opcode_a), Ok(())); + assert_eq!(ExpressionSolver::solve(&mut values, &opcode_b), Ok(())); assert_eq!(values.get(&a).unwrap(), &FieldElement::from(4_i128)); } From 8aef05d8924ff5037a5c81f068c8af79d9160b60 Mon Sep 17 00:00:00 2001 From: kevaundray Date: Sat, 16 Dec 2023 20:02:27 +0000 Subject: [PATCH 04/14] modify code and comments to match --- acvm-repo/acir/src/native_types/expression/mod.rs | 12 +++++++++--- .../src/compiler/optimizers/redundant_range.rs | 2 +- acvm-repo/acvm/src/compiler/transformers/csat.rs | 14 +++++++------- acvm-repo/acvm/src/compiler/transformers/mod.rs | 2 +- acvm-repo/acvm/src/pwg/memory_op.rs | 4 ++-- acvm-repo/acvm/src/pwg/mod.rs | 10 +++++----- .../acvm_js/test/browser/execute_circuit.test.ts | 4 ++-- .../acvm_js/test/node/execute_circuit.test.ts | 4 ++-- 8 files changed, 29 insertions(+), 23 deletions(-) diff --git a/acvm-repo/acir/src/native_types/expression/mod.rs b/acvm-repo/acir/src/native_types/expression/mod.rs index c7f2c573ce3..d2fbdc4d6c8 100644 --- a/acvm-repo/acir/src/native_types/expression/mod.rs +++ b/acvm-repo/acir/src/native_types/expression/mod.rs @@ -8,7 +8,7 @@ mod ordering; // In the addition polynomial // We can have arbitrary fan-in/out, so we need more than wL,wR and wO -// When looking at the arithmetic opcode for the quotient polynomial in standard plonk +// When looking at the assert zero opcode for the quotient polynomial in standard plonk // You can think of it as fan-in 2 and fan out-1 , or you can think of it as fan-in 1 and fan-out 2 // // In the multiplication polynomial @@ -16,7 +16,7 @@ mod ordering; #[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Hash)] pub struct Expression { // To avoid having to create intermediate variables pre-optimization - // We collect all of the multiplication terms in the arithmetic opcode + // We collect all of the multiplication terms in the assert-zero opcode // A multiplication term if of the form q_M * wL * wR // Hence this vector represents the following sum: q_M1 * wL1 * wR1 + q_M2 * wL2 * wR2 + .. + pub mul_terms: Vec<(FieldElement, Witness, Witness)>, @@ -178,7 +178,13 @@ impl Expression { self.linear_combinations.sort_by(|a, b| a.1.cmp(&b.1)); } - /// Checks if this polynomial can fit into one arithmetic identity + /// Checks if this expression can fit into one arithmetic identity + /// TODO: This needs to be reworded, arithmetic identity only makes sense in the context + /// TODO of PLONK, whereas we want expressions to be generic. + /// TODO: We just need to reword it to say exactly what its doing and + /// TODO then reference the fact that this is what plonk will accept. + /// TODO alternatively, we can define arithmetic identity in the context of expressions + /// TODO and then reference that. pub fn fits_in_one_identity(&self, width: usize) -> bool { // A Polynomial with more than one mul term cannot fit into one opcode if self.mul_terms.len() > 1 { diff --git a/acvm-repo/acvm/src/compiler/optimizers/redundant_range.rs b/acvm-repo/acvm/src/compiler/optimizers/redundant_range.rs index 9bd91d495cc..7b40c35960a 100644 --- a/acvm-repo/acvm/src/compiler/optimizers/redundant_range.rs +++ b/acvm-repo/acvm/src/compiler/optimizers/redundant_range.rs @@ -234,7 +234,7 @@ mod tests { #[test] fn non_range_opcodes() { // The optimizer should not remove or change non-range opcodes - // The four Arithmetic opcodes should remain unchanged. + // The four AssertZero opcodes should remain unchanged. let mut circuit = test_circuit(vec![(Witness(1), 16), (Witness(1), 16)]); circuit.opcodes.push(Opcode::AssertZero(Expression::default())); diff --git a/acvm-repo/acvm/src/compiler/transformers/csat.rs b/acvm-repo/acvm/src/compiler/transformers/csat.rs index 9f89ac4671a..1f1b33dbc4a 100644 --- a/acvm-repo/acvm/src/compiler/transformers/csat.rs +++ b/acvm-repo/acvm/src/compiler/transformers/csat.rs @@ -62,7 +62,7 @@ impl CSatTransformer { } // Still missing dead witness optimization. - // To do this, we will need the whole set of arithmetic opcodes + // To do this, we will need the whole set of assert-zero opcodes // I think it can also be done before the local optimization seen here, as dead variables will come from the user pub(crate) fn transform( &mut self, @@ -84,7 +84,7 @@ impl CSatTransformer { opcode } - // This optimization will search for combinations of terms which can be represented in a single arithmetic opcode + // This optimization will search for combinations of terms which can be represented in a single assert-zero opcode // Case 1 : qM * wL * wR + qL * wL + qR * wR + qO * wO + qC // This polynomial does not require any further optimizations, it can be safely represented in one opcode // ie a polynomial with 1 mul(bi-variate) term and 3 (univariate) terms where 2 of those terms match the bivariate term @@ -93,13 +93,13 @@ impl CSatTransformer { // // // Case 2: qM * wL * wR + qL * wL + qR * wR + qO * wO + qC + qM2 * wL2 * wR2 + qL * wL2 + qR * wR2 + qO * wO2 + qC2 - // This polynomial cannot be represented using one arithmetic opcode. + // This polynomial cannot be represented using one assert-zero opcode. // // This algorithm will first extract the first full opcode(if possible): // t = qM * wL * wR + qL * wL + qR * wR + qO * wO + qC // // The polynomial now looks like so t + qM2 * wL2 * wR2 + qL * wL2 + qR * wR2 + qO * wO2 + qC2 - // This polynomial cannot be represented using one arithmetic opcode. + // This polynomial cannot be represented using one assert-zero opcode. // // This algorithm will then extract the second full opcode(if possible): // t2 = qM2 * wL2 * wR2 + qL * wL2 + qR * wR2 + qO * wO2 + qC2 @@ -121,7 +121,7 @@ impl CSatTransformer { // If the opcode only has one mul term, then this algorithm cannot optimize it any further // Either it can be represented in a single arithmetic equation or it's fan-in is too large and we need intermediate variables for those // large-fan-in optimization is not this algorithms purpose. - // If the opcode has 0 mul terms, then it is an add opcode and similarly it can either fit into a single arithmetic opcode or it has a large fan-in + // If the opcode has 0 mul terms, then it is an add opcode and similarly it can either fit into a single assert-zero opcode or it has a large fan-in if opcode.mul_terms.len() <= 1 { return opcode; } @@ -194,7 +194,7 @@ impl CSatTransformer { } } - // Now we have used up 2 spaces in our arithmetic opcode. The width now dictates, how many more we can add + // Now we have used up 2 spaces in our assert-zero opcode. The width now dictates, how many more we can add let mut remaining_space = self.width - 2 - 1; // We minus 1 because we need an extra space to contain the intermediate variable // Keep adding terms until we have no more left, or we reach the width let mut remaining_linear_terms = @@ -325,7 +325,7 @@ impl CSatTransformer { // Then use intermediate variables again to squash the fan-in, so that it can fit into the appropriate width // First check if this polynomial actually needs a partial opcode optimization - // There is the chance that it fits perfectly within the arithmetic opcode + // There is the chance that it fits perfectly within the assert-zero opcode if opcode.fits_in_one_identity(self.width) { return opcode; } diff --git a/acvm-repo/acvm/src/compiler/transformers/mod.rs b/acvm-repo/acvm/src/compiler/transformers/mod.rs index 56e461a7dbb..bc3d2c7eb87 100644 --- a/acvm-repo/acvm/src/compiler/transformers/mod.rs +++ b/acvm-repo/acvm/src/compiler/transformers/mod.rs @@ -60,7 +60,7 @@ pub(super) fn transform_internal( // TODO or at the very least, we could put all of it inside of CSatOptimizer pass let mut new_acir_opcode_positions: Vec = Vec::with_capacity(acir_opcode_positions.len()); - // Optimize the arithmetic gates by reducing them into the correct width and + // Optimize the assert zero gates by reducing them into the correct width and // creating intermediate variables when necessary let mut transformed_opcodes = Vec::new(); diff --git a/acvm-repo/acvm/src/pwg/memory_op.rs b/acvm-repo/acvm/src/pwg/memory_op.rs index 42951dfa3c1..c1da2cd95cf 100644 --- a/acvm-repo/acvm/src/pwg/memory_op.rs +++ b/acvm-repo/acvm/src/pwg/memory_op.rs @@ -6,7 +6,7 @@ use acir::{ FieldElement, }; -use super::{arithmetic::ArithmeticSolver, get_value, insert_value, witness_to_value}; +use super::{arithmetic::ExpressionSolver, get_value, insert_value, witness_to_value}; use super::{ErrorLocation, OpcodeResolutionError}; type MemoryIndex = u32; @@ -75,7 +75,7 @@ impl MemoryOpSolver { // // In read operations, this corresponds to the witness index at which the value from memory will be written. // In write operations, this corresponds to the expression which will be written to memory. - let value = ArithmeticSolver::evaluate(&op.value, initial_witness); + let value = ExpressionSolver::evaluate(&op.value, initial_witness); // `operation == 0` implies a read operation. (`operation == 1` implies write operation). let is_read_operation = operation.is_zero(); diff --git a/acvm-repo/acvm/src/pwg/mod.rs b/acvm-repo/acvm/src/pwg/mod.rs index 435dbd357b0..41b96572658 100644 --- a/acvm-repo/acvm/src/pwg/mod.rs +++ b/acvm-repo/acvm/src/pwg/mod.rs @@ -10,7 +10,7 @@ use acir::{ }; use acvm_blackbox_solver::BlackBoxResolutionError; -use self::{arithmetic::ArithmeticSolver, directives::solve_directives, memory_op::MemoryOpSolver}; +use self::{arithmetic::ExpressionSolver, directives::solve_directives, memory_op::MemoryOpSolver}; use crate::BlackBoxFunctionSolver; use thiserror::Error; @@ -69,8 +69,8 @@ pub enum StepResult<'a, B: BlackBoxFunctionSolver> { // The most common being that one of its input has not been // assigned a value. // -// TODO: ExpressionHasTooManyUnknowns is specific for arithmetic expressions -// TODO: we could have a error enum for arithmetic failure cases in that module +// TODO: ExpressionHasTooManyUnknowns is specific for expression solver +// TODO: we could have a error enum for expression solver failure cases in that module // TODO that can be converted into an OpcodeNotSolvable or OpcodeResolutionError enum #[derive(Clone, PartialEq, Eq, Debug, Error)] pub enum OpcodeNotSolvable { @@ -253,7 +253,7 @@ impl<'a, B: BlackBoxFunctionSolver> ACVM<'a, B> { let opcode = &self.opcodes[self.instruction_pointer]; let resolution = match opcode { - Opcode::AssertZero(expr) => ArithmeticSolver::solve(&mut self.witness_map, expr), + Opcode::AssertZero(expr) => ExpressionSolver::solve(&mut self.witness_map, expr), Opcode::BlackBoxFuncCall(bb_func) => { blackbox::solve(self.backend, &mut self.witness_map, bb_func) } @@ -397,7 +397,7 @@ pub fn get_value( expr: &Expression, initial_witness: &WitnessMap, ) -> Result { - let expr = ArithmeticSolver::evaluate(expr, initial_witness); + let expr = ExpressionSolver::evaluate(expr, initial_witness); match expr.to_const() { Some(value) => Ok(value), None => Err(OpcodeResolutionError::OpcodeNotSolvable( diff --git a/acvm-repo/acvm_js/test/browser/execute_circuit.test.ts b/acvm-repo/acvm_js/test/browser/execute_circuit.test.ts index 925c1a07eb8..259c51ed1c6 100644 --- a/acvm-repo/acvm_js/test/browser/execute_circuit.test.ts +++ b/acvm-repo/acvm_js/test/browser/execute_circuit.test.ts @@ -53,7 +53,7 @@ it('successfully processes simple brillig foreign call opcodes', async () => { expect(observedInputs).to.be.deep.eq(oracleCallInputs); // If incorrect value is written into circuit then execution should halt due to unsatisfied constraint in - // arithmetic opcode. Nevertheless, check that returned value was inserted correctly. + // assert-zero opcode. Nevertheless, check that returned value was inserted correctly. expect(solved_witness).to.be.deep.eq(expectedWitnessMap); }); @@ -79,7 +79,7 @@ it('successfully processes complex brillig foreign call opcodes', async () => { expect(observedInputs).to.be.deep.eq(oracleCallInputs); // If incorrect value is written into circuit then execution should halt due to unsatisfied constraint in - // arithmetic opcode. Nevertheless, check that returned value was inserted correctly. + // assert-zero opcode. Nevertheless, check that returned value was inserted correctly. expect(solved_witness).to.be.deep.eq(expectedWitnessMap); }); diff --git a/acvm-repo/acvm_js/test/node/execute_circuit.test.ts b/acvm-repo/acvm_js/test/node/execute_circuit.test.ts index b28b9e72591..adee3c15312 100644 --- a/acvm-repo/acvm_js/test/node/execute_circuit.test.ts +++ b/acvm-repo/acvm_js/test/node/execute_circuit.test.ts @@ -46,7 +46,7 @@ it('successfully processes simple brillig foreign call opcodes', async () => { expect(observedInputs).to.be.deep.eq(oracleCallInputs); // If incorrect value is written into circuit then execution should halt due to unsatisfied constraint in - // arithmetic opcode. Nevertheless, check that returned value was inserted correctly. + // assert-zero opcode. Nevertheless, check that returned value was inserted correctly. expect(solved_witness).to.be.deep.eq(expectedWitnessMap); }); @@ -72,7 +72,7 @@ it('successfully processes complex brillig foreign call opcodes', async () => { expect(observedInputs).to.be.deep.eq(oracleCallInputs); // If incorrect value is written into circuit then execution should halt due to unsatisfied constraint in - // arithmetic opcode. Nevertheless, check that returned value was inserted correctly. + // assert-zero opcode. Nevertheless, check that returned value was inserted correctly. expect(solved_witness).to.be.deep.eq(expectedWitnessMap); }); From 560074930947df840456524781aea86de63dbbe1 Mon Sep 17 00:00:00 2001 From: kevaundray Date: Sat, 16 Dec 2023 20:02:45 +0000 Subject: [PATCH 05/14] docs: change Arithmetic to AssertZero --- acvm-repo/acir/acir_docs.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/acvm-repo/acir/acir_docs.md b/acvm-repo/acir/acir_docs.md index eb532c9ae0c..843b3604eb8 100644 --- a/acvm-repo/acir/acir_docs.md +++ b/acvm-repo/acir/acir_docs.md @@ -55,14 +55,14 @@ Some opcodes are not constrained, which mean they will not be used by the provin Finally, some opcodes will have a predicate, whose value is 0 or 1. Its purpose is to nullify the opcode when the value is 0, so that it has no effect. Note that removing the opcode is not a solution because this modifies the circuit (the circuit being mainly the list of the opcodes). -*Remark*: Opcodes operate on witnesses, but we will see that some opcode work on Arithmetic expressions of witnesses. We call an arithmetic expression a linear combination of witnesses and/or products of two witnesses (and also a constant term). A single witness is a (simple) arithmetic expression, and conversly, an arithmetic expression can be turned into a single witness using an arithmetic opcode (see below). So basically, using witnesses or arithmetic expressions is equivalent, but the latter can avoid the creation of witness in some cases. +*Remark*: Opcodes operate on witnesses, but we will see that some opcode work on expressions of witnesses. We call an expression a linear combination of witnesses and/or products of two witnesses (and also a constant term). A single witness is a (simple) expression, and conversely, an expression can be turned into a single witness using an assert zero opcode (see below). So basically, using witnesses or expressions is equivalent, but the latter can avoid the creation of witness in some cases. -### Arithmetic opcode -An arithmetic opcode adds the constraint that P(w) = 0, where w=(w_1,..w_n) is a tuple of n witnesses, and P is a multi-variate polynomial of total degree at most 2. +### AssertZero opcode +An AssertZero opcode adds the constraint that P(w) = 0, where w=(w_1,..w_n) is a tuple of n witnesses, and P is a multi-variate polynomial of total degree at most 2. The coefficients ${q_M}_{i,j}, q_i,q_c$ of the polynomial are known values which define the opcode. -A general expression of arithmetic opcode is the following: $\sum_{i,j} {q_M}_{i,j}w_iw_j + \sum_i q_iw_i +q_c = 0$ +A general expression of assert zero opcode is the following: $\sum_{i,j} {q_M}_{i,j}w_iw_j + \sum_i q_iw_i +q_c = 0$ -An arithmetic opcode can be used to: +An assert-zero opcode can be used to: - **express a constraint** on witnesses; for instance to express that a witness $w$ is a boolean, you can add the opcode: $w*w-w=0$ - or, to **compute the value** of an arithmetic operation of some inputs. For instance, to multiply two witnesses $x$ and $y$, you would use the opcode $z-x*y=0$, which would constraint $z$ to be $x*y$. @@ -70,7 +70,7 @@ An arithmetic opcode can be used to: The solver expects that at most one witness is not known when executing the opcode. ### BlackBoxFuncCall opcode -These opcodes represent a specific computation. Even if any computation can be done using only arithmetic opcodes, it is not always efficient. Some proving systems, and in particular the proving system from Aztec, can implement several computations more efficiently using for instance look-up tables. The BlackBoxFuncCall opcode is used to ask the proving system to handle the computation by itself. +These opcodes represent a specific computation. Even if any computation can be done using only assert zero opcodes, it is not always efficient. Some proving systems, and in particular the proving system from Aztec, can implement several computations more efficiently using for instance look-up tables. The BlackBoxFuncCall opcode is used to ask the proving system to handle the computation by itself. All black box functions takes as input a tuple (witness, num_bits), where num_bits is a constant representing the bit size of the input witness, and they have one or several witnesses as output. Some more advanced computations assume that the proving system has an 'embedded curve'. It is a curve that cycle with the main curve of the proving system, i.e the scalar field of the embedded curve is the base field of the main one, and vice-versa. The curves used by the proving system are dependent on the proving system (and/or its configuration). Aztec's Barretenberg uses BN254 as the main curve and Grumpkin as the embedded curve. @@ -180,7 +180,7 @@ This opcode is used as a hint for the solver when executing (solving) the circui - predicate: an arithmetic expression that disable the opcode when it is null. Let's see an example with euclidian division. -The normal way to compute a/b, where a and b are 8-bits integers, is to implement Euclid algorithm which computes in a loop (or recursively) modulos of the kind 'a mod b'. Doing this computation requires a lot of steps to be properly implemented in ACIR, especially the loop with a condition. However, euclidian division can be easily constrained with one arithmetic opcode: a = bq+r, assuming q is 8 bits and r Date: Sat, 16 Dec 2023 20:09:11 +0000 Subject: [PATCH 06/14] fmt --- acvm-repo/acir/src/native_types/expression/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/acvm-repo/acir/src/native_types/expression/mod.rs b/acvm-repo/acir/src/native_types/expression/mod.rs index d2fbdc4d6c8..5bb3a355324 100644 --- a/acvm-repo/acir/src/native_types/expression/mod.rs +++ b/acvm-repo/acir/src/native_types/expression/mod.rs @@ -181,7 +181,7 @@ impl Expression { /// Checks if this expression can fit into one arithmetic identity /// TODO: This needs to be reworded, arithmetic identity only makes sense in the context /// TODO of PLONK, whereas we want expressions to be generic. - /// TODO: We just need to reword it to say exactly what its doing and + /// TODO: We just need to reword it to say exactly what its doing and /// TODO then reference the fact that this is what plonk will accept. /// TODO alternatively, we can define arithmetic identity in the context of expressions /// TODO and then reference that. From 0d3f19b5c2c1666531ada7a84a8e7465328146d5 Mon Sep 17 00:00:00 2001 From: kevaundray Date: Sat, 16 Dec 2023 20:10:35 +0000 Subject: [PATCH 07/14] regen cpp --- acvm-repo/acir/codegen/acir.cpp | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/acvm-repo/acir/codegen/acir.cpp b/acvm-repo/acir/codegen/acir.cpp index c31fc4abd00..21a98b3ee2c 100644 --- a/acvm-repo/acir/codegen/acir.cpp +++ b/acvm-repo/acir/codegen/acir.cpp @@ -767,12 +767,12 @@ namespace Circuit { struct Opcode { - struct Arithmetic { + struct AssertZero { Circuit::Expression value; - friend bool operator==(const Arithmetic&, const Arithmetic&); + friend bool operator==(const AssertZero&, const AssertZero&); std::vector bincodeSerialize() const; - static Arithmetic bincodeDeserialize(std::vector); + static AssertZero bincodeDeserialize(std::vector); }; struct BlackBoxFuncCall { @@ -818,7 +818,7 @@ namespace Circuit { static MemoryInit bincodeDeserialize(std::vector); }; - std::variant value; + std::variant value; friend bool operator==(const Opcode&, const Opcode&); std::vector bincodeSerialize() const; @@ -4268,20 +4268,20 @@ Circuit::Opcode serde::Deserializable::deserialize(Deserializer namespace Circuit { - inline bool operator==(const Opcode::Arithmetic &lhs, const Opcode::Arithmetic &rhs) { + inline bool operator==(const Opcode::AssertZero &lhs, const Opcode::AssertZero &rhs) { if (!(lhs.value == rhs.value)) { return false; } return true; } - inline std::vector Opcode::Arithmetic::bincodeSerialize() const { + inline std::vector Opcode::AssertZero::bincodeSerialize() const { auto serializer = serde::BincodeSerializer(); - serde::Serializable::serialize(*this, serializer); + serde::Serializable::serialize(*this, serializer); return std::move(serializer).bytes(); } - inline Opcode::Arithmetic Opcode::Arithmetic::bincodeDeserialize(std::vector input) { + inline Opcode::AssertZero Opcode::AssertZero::bincodeDeserialize(std::vector input) { auto deserializer = serde::BincodeDeserializer(input); - auto value = serde::Deserializable::deserialize(deserializer); + auto value = serde::Deserializable::deserialize(deserializer); if (deserializer.get_buffer_offset() < input.size()) { throw serde::deserialization_error("Some input bytes were not read"); } @@ -4292,14 +4292,14 @@ namespace Circuit { template <> template -void serde::Serializable::serialize(const Circuit::Opcode::Arithmetic &obj, Serializer &serializer) { +void serde::Serializable::serialize(const Circuit::Opcode::AssertZero &obj, Serializer &serializer) { serde::Serializable::serialize(obj.value, serializer); } template <> template -Circuit::Opcode::Arithmetic serde::Deserializable::deserialize(Deserializer &deserializer) { - Circuit::Opcode::Arithmetic obj; +Circuit::Opcode::AssertZero serde::Deserializable::deserialize(Deserializer &deserializer) { + Circuit::Opcode::AssertZero obj; obj.value = serde::Deserializable::deserialize(deserializer); return obj; } From 50f1518e470f2fe6daf20e712857b56f6cc7f3fa Mon Sep 17 00:00:00 2001 From: kevaundray Date: Sat, 16 Dec 2023 20:11:02 +0000 Subject: [PATCH 08/14] change function names --- acvm-repo/acir/src/circuit/opcodes.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/acvm-repo/acir/src/circuit/opcodes.rs b/acvm-repo/acir/src/circuit/opcodes.rs index eb623d73c4b..b61cd80e45a 100644 --- a/acvm-repo/acir/src/circuit/opcodes.rs +++ b/acvm-repo/acir/src/circuit/opcodes.rs @@ -38,7 +38,7 @@ impl Opcode { // TODO concat!("directive:", directive.name) pub fn name(&self) -> &str { match self { - Opcode::AssertZero(_) => "arithmetic", + Opcode::AssertZero(_) => "assert_zero", Opcode::Directive(directive) => directive.name(), Opcode::BlackBoxFuncCall(g) => g.name(), Opcode::Brillig(_) => "brillig", @@ -47,11 +47,11 @@ impl Opcode { } } - pub fn is_arithmetic(&self) -> bool { + pub fn is_assert_zero(&self) -> bool { matches!(self, Opcode::AssertZero(_)) } - pub fn arithmetic(self) -> Option { + pub fn assert_zero(self) -> Option { match self { Opcode::AssertZero(expr) => Some(expr), _ => None, From e4b0390daff6df159c6c05b9255a6a20afe5df87 Mon Sep 17 00:00:00 2001 From: kevaundray Date: Tue, 19 Dec 2023 15:54:42 +0000 Subject: [PATCH 09/14] Update acvm-repo/acvm/src/compiler/transformers/mod.rs Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com> --- acvm-repo/acvm/src/compiler/transformers/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/acvm-repo/acvm/src/compiler/transformers/mod.rs b/acvm-repo/acvm/src/compiler/transformers/mod.rs index 9f0a0ed43aa..eef8d7bee44 100644 --- a/acvm-repo/acvm/src/compiler/transformers/mod.rs +++ b/acvm-repo/acvm/src/compiler/transformers/mod.rs @@ -63,7 +63,7 @@ pub(super) fn transform_internal( // TODO or at the very least, we could put all of it inside of CSatOptimizer pass let mut new_acir_opcode_positions: Vec = Vec::with_capacity(acir_opcode_positions.len()); - // Optimize the assert zero gates by reducing them into the correct width and + // Optimize the assert-zero gates by reducing them into the correct width and // creating intermediate variables when necessary let mut transformed_opcodes = Vec::new(); From 9986990b06da3e8f1d9191ba0b18ff594c0837e2 Mon Sep 17 00:00:00 2001 From: kevaundray Date: Tue, 19 Dec 2023 15:54:53 +0000 Subject: [PATCH 10/14] Update acvm-repo/acir/src/native_types/expression/mod.rs Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com> --- acvm-repo/acir/src/native_types/expression/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/acvm-repo/acir/src/native_types/expression/mod.rs b/acvm-repo/acir/src/native_types/expression/mod.rs index 5bb3a355324..402aa3eb3a6 100644 --- a/acvm-repo/acir/src/native_types/expression/mod.rs +++ b/acvm-repo/acir/src/native_types/expression/mod.rs @@ -8,7 +8,7 @@ mod ordering; // In the addition polynomial // We can have arbitrary fan-in/out, so we need more than wL,wR and wO -// When looking at the assert zero opcode for the quotient polynomial in standard plonk +// When looking at the assert-zero opcode for the quotient polynomial in standard plonk // You can think of it as fan-in 2 and fan out-1 , or you can think of it as fan-in 1 and fan-out 2 // // In the multiplication polynomial From f7c0d0e81620609bdd24dd326018a87f9922823a Mon Sep 17 00:00:00 2001 From: kevaundray Date: Tue, 19 Dec 2023 15:54:59 +0000 Subject: [PATCH 11/14] Update acvm-repo/acir/acir_docs.md Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com> --- acvm-repo/acir/acir_docs.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/acvm-repo/acir/acir_docs.md b/acvm-repo/acir/acir_docs.md index 843b3604eb8..2068e72d895 100644 --- a/acvm-repo/acir/acir_docs.md +++ b/acvm-repo/acir/acir_docs.md @@ -55,7 +55,7 @@ Some opcodes are not constrained, which mean they will not be used by the provin Finally, some opcodes will have a predicate, whose value is 0 or 1. Its purpose is to nullify the opcode when the value is 0, so that it has no effect. Note that removing the opcode is not a solution because this modifies the circuit (the circuit being mainly the list of the opcodes). -*Remark*: Opcodes operate on witnesses, but we will see that some opcode work on expressions of witnesses. We call an expression a linear combination of witnesses and/or products of two witnesses (and also a constant term). A single witness is a (simple) expression, and conversely, an expression can be turned into a single witness using an assert zero opcode (see below). So basically, using witnesses or expressions is equivalent, but the latter can avoid the creation of witness in some cases. +*Remark*: Opcodes operate on witnesses, but we will see that some opcode work on expressions of witnesses. We call an expression a linear combination of witnesses and/or products of two witnesses (and also a constant term). A single witness is a (simple) expression, and conversely, an expression can be turned into a single witness using an assert-zero opcode (see below). So basically, using witnesses or expressions is equivalent, but the latter can avoid the creation of witness in some cases. ### AssertZero opcode An AssertZero opcode adds the constraint that P(w) = 0, where w=(w_1,..w_n) is a tuple of n witnesses, and P is a multi-variate polynomial of total degree at most 2. From b4a22809a2be8ca0d30d02a1111ddf68f0a01c92 Mon Sep 17 00:00:00 2001 From: kevaundray Date: Tue, 19 Dec 2023 15:55:06 +0000 Subject: [PATCH 12/14] Update acvm-repo/acir/acir_docs.md Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com> --- acvm-repo/acir/acir_docs.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/acvm-repo/acir/acir_docs.md b/acvm-repo/acir/acir_docs.md index 2068e72d895..fc80332b9f0 100644 --- a/acvm-repo/acir/acir_docs.md +++ b/acvm-repo/acir/acir_docs.md @@ -60,7 +60,7 @@ Finally, some opcodes will have a predicate, whose value is 0 or 1. Its purpose ### AssertZero opcode An AssertZero opcode adds the constraint that P(w) = 0, where w=(w_1,..w_n) is a tuple of n witnesses, and P is a multi-variate polynomial of total degree at most 2. The coefficients ${q_M}_{i,j}, q_i,q_c$ of the polynomial are known values which define the opcode. -A general expression of assert zero opcode is the following: $\sum_{i,j} {q_M}_{i,j}w_iw_j + \sum_i q_iw_i +q_c = 0$ +A general expression of assert-zero opcode is the following: $\sum_{i,j} {q_M}_{i,j}w_iw_j + \sum_i q_iw_i +q_c = 0$ An assert-zero opcode can be used to: - **express a constraint** on witnesses; for instance to express that a witness $w$ is a boolean, you can add the opcode: $w*w-w=0$ From 65a437492d8860b11f550919fe8b62ff5c31ed16 Mon Sep 17 00:00:00 2001 From: kevaundray Date: Tue, 19 Dec 2023 15:55:12 +0000 Subject: [PATCH 13/14] Update acvm-repo/acir/acir_docs.md Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com> --- acvm-repo/acir/acir_docs.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/acvm-repo/acir/acir_docs.md b/acvm-repo/acir/acir_docs.md index fc80332b9f0..ffdd360e94b 100644 --- a/acvm-repo/acir/acir_docs.md +++ b/acvm-repo/acir/acir_docs.md @@ -70,7 +70,7 @@ An assert-zero opcode can be used to: The solver expects that at most one witness is not known when executing the opcode. ### BlackBoxFuncCall opcode -These opcodes represent a specific computation. Even if any computation can be done using only assert zero opcodes, it is not always efficient. Some proving systems, and in particular the proving system from Aztec, can implement several computations more efficiently using for instance look-up tables. The BlackBoxFuncCall opcode is used to ask the proving system to handle the computation by itself. +These opcodes represent a specific computation. Even if any computation can be done using only assert-zero opcodes, it is not always efficient. Some proving systems, and in particular the proving system from Aztec, can implement several computations more efficiently using for instance look-up tables. The BlackBoxFuncCall opcode is used to ask the proving system to handle the computation by itself. All black box functions takes as input a tuple (witness, num_bits), where num_bits is a constant representing the bit size of the input witness, and they have one or several witnesses as output. Some more advanced computations assume that the proving system has an 'embedded curve'. It is a curve that cycle with the main curve of the proving system, i.e the scalar field of the embedded curve is the base field of the main one, and vice-versa. The curves used by the proving system are dependent on the proving system (and/or its configuration). Aztec's Barretenberg uses BN254 as the main curve and Grumpkin as the embedded curve. From 27cd5ee93eeb60c5d057eefd00db2c8c67746ab6 Mon Sep 17 00:00:00 2001 From: kevaundray Date: Tue, 19 Dec 2023 15:55:19 +0000 Subject: [PATCH 14/14] Update acvm-repo/acir/acir_docs.md Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com> --- acvm-repo/acir/acir_docs.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/acvm-repo/acir/acir_docs.md b/acvm-repo/acir/acir_docs.md index ffdd360e94b..fd89b3f292b 100644 --- a/acvm-repo/acir/acir_docs.md +++ b/acvm-repo/acir/acir_docs.md @@ -180,7 +180,7 @@ This opcode is used as a hint for the solver when executing (solving) the circui - predicate: an arithmetic expression that disable the opcode when it is null. Let's see an example with euclidian division. -The normal way to compute a/b, where a and b are 8-bits integers, is to implement Euclid algorithm which computes in a loop (or recursively) modulos of the kind 'a mod b'. Doing this computation requires a lot of steps to be properly implemented in ACIR, especially the loop with a condition. However, euclidian division can be easily constrained with one assert zero opcode: a = bq+r, assuming q is 8 bits and r