From 83de289712872c1c9a4592b84ba20b619c61ba9a Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 27 May 2023 18:34:19 +0100 Subject: [PATCH 01/18] add field mul and div --- .../arithmetic_binary_operations/Nargo.toml | 5 +++++ .../arithmetic_binary_operations/Prover.toml | 3 +++ .../arithmetic_binary_operations/src/main.nr | 12 ++++++++++++ 3 files changed, 20 insertions(+) create mode 100644 crates/nargo_cli/tests/test_data_ssa_refactor/arithmetic_binary_operations/Nargo.toml create mode 100644 crates/nargo_cli/tests/test_data_ssa_refactor/arithmetic_binary_operations/Prover.toml create mode 100644 crates/nargo_cli/tests/test_data_ssa_refactor/arithmetic_binary_operations/src/main.nr diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/arithmetic_binary_operations/Nargo.toml b/crates/nargo_cli/tests/test_data_ssa_refactor/arithmetic_binary_operations/Nargo.toml new file mode 100644 index 00000000000..e0b467ce5da --- /dev/null +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/arithmetic_binary_operations/Nargo.toml @@ -0,0 +1,5 @@ +[package] +authors = [""] +compiler_version = "0.1" + +[dependencies] \ No newline at end of file diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/arithmetic_binary_operations/Prover.toml b/crates/nargo_cli/tests/test_data_ssa_refactor/arithmetic_binary_operations/Prover.toml new file mode 100644 index 00000000000..63382a9f640 --- /dev/null +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/arithmetic_binary_operations/Prover.toml @@ -0,0 +1,3 @@ +x = "3" +y = "4" +z = "5" diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/arithmetic_binary_operations/src/main.nr b/crates/nargo_cli/tests/test_data_ssa_refactor/arithmetic_binary_operations/src/main.nr new file mode 100644 index 00000000000..391aa27049d --- /dev/null +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/arithmetic_binary_operations/src/main.nr @@ -0,0 +1,12 @@ +// Tests a very simple program. +// +// The features being tested are: +// Binary addition, multiplication, division +// x = 3, y = 4, z = 5 +fn main(x : Field, y : Field, z : Field) -> pub Field { + let a = x + x; // 3 + 3 = 6 + let b = a - y; // 6 - 4 = 2 + let c = b * z; // 2 * 5 = 10 + let d = c / a; // 10 / 6 (This uses field inversion, so we test it by multiplying by `a`) + d * a +} \ No newline at end of file From 1ef2ca99363b3f503cb7cc324b109348435c1ccf Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 27 May 2023 18:34:35 +0100 Subject: [PATCH 02/18] add code to process field mul and div --- crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs index 07c78b2a377..f38ade7679e 100644 --- a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs +++ b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs @@ -110,7 +110,8 @@ impl Context { _ => unreachable!("ICE: Program must have a singular return"), }; - let is_return_unit_type = return_values.len() == 1 && dfg.type_of_value(return_values[0]) == Type::Unit; + let is_return_unit_type = + return_values.len() == 1 && dfg.type_of_value(return_values[0]) == Type::Unit; if is_return_unit_type { return; } @@ -157,6 +158,8 @@ impl Context { match binary.operator { BinaryOp::Add => self.acir_context.add_var(lhs, rhs), BinaryOp::Sub => self.acir_context.sub_var(lhs, rhs), + BinaryOp::Mul => self.acir_context.mul_var(lhs, rhs), + BinaryOp::Div => self.acir_context.div_var(lhs, rhs), _ => todo!(), } } From 063762608f305fbac67761ff3427251d7f080278 Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 27 May 2023 21:56:49 +0100 Subject: [PATCH 03/18] add assert example --- .../test_data_ssa_refactor/assert_statement/Nargo.toml | 5 +++++ .../test_data_ssa_refactor/assert_statement/Prover.toml | 2 ++ .../test_data_ssa_refactor/assert_statement/src/main.nr | 6 ++++++ 3 files changed, 13 insertions(+) create mode 100644 crates/nargo_cli/tests/test_data_ssa_refactor/assert_statement/Nargo.toml create mode 100644 crates/nargo_cli/tests/test_data_ssa_refactor/assert_statement/Prover.toml create mode 100644 crates/nargo_cli/tests/test_data_ssa_refactor/assert_statement/src/main.nr diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/assert_statement/Nargo.toml b/crates/nargo_cli/tests/test_data_ssa_refactor/assert_statement/Nargo.toml new file mode 100644 index 00000000000..e0b467ce5da --- /dev/null +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/assert_statement/Nargo.toml @@ -0,0 +1,5 @@ +[package] +authors = [""] +compiler_version = "0.1" + +[dependencies] \ No newline at end of file diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/assert_statement/Prover.toml b/crates/nargo_cli/tests/test_data_ssa_refactor/assert_statement/Prover.toml new file mode 100644 index 00000000000..5d1dc99124f --- /dev/null +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/assert_statement/Prover.toml @@ -0,0 +1,2 @@ +x = "3" +y = "3" diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/assert_statement/src/main.nr b/crates/nargo_cli/tests/test_data_ssa_refactor/assert_statement/src/main.nr new file mode 100644 index 00000000000..7dab317d924 --- /dev/null +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/assert_statement/src/main.nr @@ -0,0 +1,6 @@ +// Tests a very simple program. +// +// The features being tested is assertion +fn main(x : Field, y : Field) { + assert(x == y); +} \ No newline at end of file From 18c427450d261feb59a06188f2fbb328cdb6ea8e Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 27 May 2023 21:59:20 +0100 Subject: [PATCH 04/18] add `is_equal` constraint --- .../acir_gen/acir_ir/generated_acir.rs | 107 +++++++++++++++++- 1 file changed, 102 insertions(+), 5 deletions(-) diff --git a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs index bd53136557c..1720945ca33 100644 --- a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs +++ b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs @@ -55,7 +55,7 @@ impl GeneratedAcir { /// This means you cannot multiply an infinite amount of Expressions together. /// Once the expression goes over degree-2, then it needs to be reduced to a Witness /// which has degree-1 in order to be able to continue the multiplication chain. - pub(crate) fn expression_to_witness(&mut self, expression: &Expression) -> Witness { + fn expression_to_witness(&mut self, expression: &Expression) -> Witness { let fresh_witness = self.next_witness_index(); // Create a constraint that sets them to be equal to each other @@ -81,6 +81,15 @@ impl GeneratedAcir { } impl GeneratedAcir { + /// If `expr` can be represented as a `Witness` this function will + /// return it, else a new opcode will be added to create a Witness + /// that is equal to `expr`. + pub(crate) fn get_or_create_witness(&mut self, expr: &Expression) -> Witness { + match expr.to_witness() { + Some(witness) => witness, + None => self.expression_to_witness(expr), + } + } /// Adds an inversion directive. /// /// This directive will invert `expr` without applying constraints @@ -94,10 +103,7 @@ impl GeneratedAcir { // the inputs be Witness, so we need this potential extra // reduction constraint. // Note: changing this in ACIR would allow us to remove it - let witness = match expr.to_witness() { - Some(witness) => witness, - None => self.expression_to_witness(expr), - }; + let witness = self.get_or_create_witness(expr); // Create the witness for the result let inverted_witness = self.next_witness_index(); @@ -118,6 +124,97 @@ impl GeneratedAcir { self.push_opcode(AcirOpcode::Arithmetic(expr)); } + /// Returns a `Witness` that is constrained to be: + /// - `1` if lhs == rhs + /// - `0` otherwise + /// + /// Intuition: the equality of two Expressions is linked to whether + /// their difference has an inverse. a == b implies that a - b == 0 + /// which implies that a - b has no inverse. So if two variables are equal + /// their difference will have no inverse. + /// + /// First, lets create a new variable that is equal to the difference + /// of the two expressions: `t = lhs - rhs` (constraint has been applied) + /// + /// Next lets create a new variable `y` which will the Witness, we will ultimately + /// return indicating whether lhs == rhs. + /// Note: We eventually need to apply constraints that ensure that it is a boolean. + /// But right now with no constraints applied to it, it is essentially a free variable. + /// + /// Next we apply the following constraint `y * t == 0`. + /// This implies that either `y` or `t` or both is `0`. + /// - If t == 0, then this means that lhs == rhs. + /// - If y == 0, this does not mean anything at this point in time, due to it having no + /// constraints. + /// + /// Naively, we could apply the following constraint: y == 1 - t. + /// This along with the previous `y * t == 0` constraint means that + /// `y` or `t` needs to be zero, but they both cannot be zero. + /// + /// This equation however falls short when lhs != rhs because then `t` + /// may not be `1`. If `t` is non-zero, then `y` is also non-zero due to + /// `y == 1 - t` and the equation `y * t == 0` fails. + /// + /// To fix, we introduce another free variable called `z` and apply the following + /// constraint instead: y == 1 - tz. + /// + /// When lhs == rhs, t is zero and so `y` is `1`. + /// When lhs != rhs, t is non-zero, however the prover can set `z = 1/t` + /// which will make `y` = 1 - t * 1/t = `0`. + /// + /// We now arrive at the conclusion that when lhs == rhs, `y` is `1` and when + /// lhs != rhs, then `y` is zero. + /// + /// We introduce three variables `y`, `t` and `z`. + /// With the following equations: + /// - t == lhs - rhs + /// - y == 1 - tz (z is a value that is chosen to be the inverse by the prover) + /// - y * t == 0 + /// + /// Lets convince ourselves that the prover cannot prove something that is untrue. + /// + /// Assume that lhs == rhs, can the prover return y == 0 ? + /// when lhs == rhs, `t` is 0. There is no way to make `y` be zero + /// since `y = 1 - 0 * z = 1`. + /// + /// Assume that lhs != rhs, can the prover return y == 1 ? + /// When lhs != rhs, then `t` is non-zero. by setting `z` to be 0, we can make `y` equal to `1` + /// This is easily observed: `y = 1 - t * 0` + /// Now since `y` is one, this means that `t` needs to be zero, or else `y * t == 0` will fail. + pub(crate) fn is_equal(&mut self, lhs: &Expression, rhs: &Expression) -> Witness { + let t = lhs - rhs; + + // This conversion is needed due to us calling Directive::Inverse; + // + // We avoid calling directive::inverse(expr) because we need + // the Witness representation for the Expression. + let t_witness = self.get_or_create_witness(&t); + + // Call the inversion directive, since we do not apply a constraint + // the prover can choose anything here. + let z = self.directive_inverse(&Expression::from(t_witness)); + + let y = self.next_witness_index(); + + // Add constraint y == 1 - tz => y + tz - 1 == 0 + let y_booleanity_constraint = Expression { + mul_terms: vec![(FieldElement::one(), t_witness, z)], + linear_combinations: vec![(FieldElement::one(), y)], + q_c: -FieldElement::one(), + }; + self.assert_is_zero(y_booleanity_constraint); + + // Add constraint that y * t == 0; + let ty_zero_constraint = Expression { + mul_terms: vec![(FieldElement::one(), t_witness, y)], + linear_combinations: vec![], + q_c: FieldElement::zero(), + }; + self.assert_is_zero(ty_zero_constraint); + + y + } + /// Adds a constraint which ensure thats `witness` is an /// integer within the range [0, 2^{num_bits} - 1] pub(crate) fn range_constraint( From 171d5d9729ecba6b3ac8616ff2ae778135c7353b Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 27 May 2023 22:00:30 +0100 Subject: [PATCH 05/18] add `eq_var` method for AcirVar --- .../acir_gen/acir_ir/acir_variable.rs | 33 +++++++++++++++---- 1 file changed, 27 insertions(+), 6 deletions(-) diff --git a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/acir_variable.rs b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/acir_variable.rs index 90bae15dbc1..2544f9a28e6 100644 --- a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/acir_variable.rs +++ b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/acir_variable.rs @@ -3,7 +3,7 @@ use acvm::{ acir::native_types::{Expression, Witness}, FieldElement, }; -use std::{collections::HashMap, hash::Hash}; +use std::{borrow::Cow, collections::HashMap, hash::Hash}; #[derive(Debug, Default)] /// Context object which holds the relationship between @@ -100,6 +100,18 @@ impl AcirContext { self.assert_eq_var(var, one_var); } + /// Returns an `AcirVar` that is `1` if `lhs` equals `rhs` and + /// 0 otherwise. + pub(crate) fn eq_var(&mut self, lhs: AcirVar, rhs: AcirVar) -> AcirVar { + let lhs_data = &self.data[&lhs]; + let rhs_data = &self.data[&rhs]; + + let lhs_expr = lhs_data.to_expression(); + let rhs_expr = rhs_data.to_expression(); + + let is_equal_witness = self.acir_ir.is_equal(&lhs_expr, &rhs_expr); + self.add_data(AcirVarData::Witness(is_equal_witness)) + } /// Constrains the `lhs` and `rhs` to be equal. pub(crate) fn assert_eq_var(&mut self, lhs: AcirVar, rhs: AcirVar) { // TODO: could use sub_var and then assert_eq_zero @@ -151,7 +163,7 @@ impl AcirContext { match (lhs_data, rhs_data) { (AcirVarData::Witness(witness), AcirVarData::Expr(expr)) | (AcirVarData::Expr(expr), AcirVarData::Witness(witness)) => { - let expr_as_witness = self.acir_ir.expression_to_witness(expr); + let expr_as_witness = self.acir_ir.get_or_create_witness(expr); let mut expr = Expression::default(); expr.push_multiplication_term(FieldElement::one(), *witness, expr_as_witness); @@ -176,8 +188,8 @@ impl AcirContext { self.add_data(AcirVarData::Const(*lhs_constant * *rhs_constant)) } (AcirVarData::Expr(lhs_expr), AcirVarData::Expr(rhs_expr)) => { - let lhs_expr_as_witness = self.acir_ir.expression_to_witness(lhs_expr); - let rhs_expr_as_witness = self.acir_ir.expression_to_witness(rhs_expr); + let lhs_expr_as_witness = self.acir_ir.get_or_create_witness(lhs_expr); + let rhs_expr_as_witness = self.acir_ir.get_or_create_witness(rhs_expr); let mut expr = Expression::default(); expr.push_multiplication_term( FieldElement::one(), @@ -234,9 +246,9 @@ impl AcirContext { // TODO: Add caching to prevent expressions from being needlessly duplicated let witness = match acir_var_data { AcirVarData::Const(constant) => { - self.acir_ir.expression_to_witness(&Expression::from(*constant)) + self.acir_ir.get_or_create_witness(&Expression::from(*constant)) } - AcirVarData::Expr(expr) => self.acir_ir.expression_to_witness(expr), + AcirVarData::Expr(expr) => self.acir_ir.get_or_create_witness(expr), AcirVarData::Witness(witness) => *witness, }; self.acir_ir.push_return_witness(witness); @@ -300,6 +312,15 @@ impl AcirVarData { } None } + /// Converts all enum variants to an Expression. + /// TODO: can refactor code in this file to use this + pub(crate) fn to_expression(&self) -> Cow { + match self { + AcirVarData::Witness(witness) => Cow::Owned(Expression::from(*witness)), + AcirVarData::Expr(expr) => Cow::Borrowed(expr), + AcirVarData::Const(constant) => Cow::Owned(Expression::from(*constant)), + } + } } /// A Reference to an `AcirVarData` From f1bfdc65fbb2cb6a4267faa31d5eab98e5abbfdd Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sat, 27 May 2023 22:00:56 +0100 Subject: [PATCH 06/18] process `Constrain` instruction and BinaryOp::Eq --- crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs index f38ade7679e..6234cdd9e4c 100644 --- a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs +++ b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs @@ -99,6 +99,10 @@ impl Context { assert_eq!(result_ids.len(), 1, "Binary ops have a single result"); self.ssa_value_to_acir_var.insert(result_ids[0], result_acir_var); } + Instruction::Constrain(value_id) => { + let constrain_condition = self.convert_ssa_value(*value_id, dfg); + self.acir_context.assert_eq_one(constrain_condition); + } _ => todo!(), } } @@ -160,6 +164,9 @@ impl Context { BinaryOp::Sub => self.acir_context.sub_var(lhs, rhs), BinaryOp::Mul => self.acir_context.mul_var(lhs, rhs), BinaryOp::Div => self.acir_context.div_var(lhs, rhs), + // Note: that this produces unnecessary constraints when + // this Eq instruction is being used for a constrain statement + BinaryOp::Eq => self.acir_context.eq_var(lhs, rhs), _ => todo!(), } } From 58edbc98d3ec2b1359157c22597b97b2c6e1dd7c Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sun, 28 May 2023 16:57:52 +0100 Subject: [PATCH 07/18] add TODO for more than the maximum number of bits --- .../src/ssa_refactor/acir_gen/acir_ir/errors.rs | 4 ++-- .../src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs | 7 ++++++- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/errors.rs b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/errors.rs index 95bcaf42637..1373a54fe65 100644 --- a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/errors.rs +++ b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/errors.rs @@ -8,9 +8,9 @@ impl AcirGenError { pub(crate) fn message(&self) -> String { match self { AcirGenError::InvalidRangeConstraint { num_bits } => { - // Don't apply any constraints if the range is for the maximum number of bits + // Don't apply any constraints if the range is for the maximum number of bits or more. format!( - "All Witnesses are by default u{num_bits}. Applying this type does not apply any constraints.") + "All Witnesses are by default u{num_bits} Applying this type does not apply any constraints.\n We also currently do not allow integers of size more than {num_bits}, this will be handled by BigIntegers.") } AcirGenError::IndexOutOfBounds { index, array_size } => { format!("Index out of bounds, array has size {array_size}, but index was {index}") diff --git a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs index 1720945ca33..46d72a73ccc 100644 --- a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs +++ b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs @@ -222,7 +222,12 @@ impl GeneratedAcir { witness: Witness, num_bits: u32, ) -> Result<(), AcirGenError> { - if num_bits == FieldElement::max_num_bits() { + // We class this as an error because users should instead + // do `as Field`. + // TODO: Since these are compiler time knowns, + // TODO this could be changed into a compiler panic and enforced + // TODO on the frontend instead. + if num_bits >= FieldElement::max_num_bits() { return Err(AcirGenError::InvalidRangeConstraint { num_bits: FieldElement::max_num_bits(), }); From 3c8c901a386a6803469d7e99c152dacf30f2d40a Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sun, 28 May 2023 16:58:26 +0100 Subject: [PATCH 08/18] add numeric_cast_var method which constrains a variable to be equal to a NumericType --- .../acir_gen/acir_ir/acir_variable.rs | 28 ++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/acir_variable.rs b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/acir_variable.rs index 2544f9a28e6..ed0946f8dcd 100644 --- a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/acir_variable.rs +++ b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/acir_variable.rs @@ -1,4 +1,6 @@ -use super::generated_acir::GeneratedAcir; +use crate::ssa_refactor::ir::types::NumericType; + +use super::{errors::AcirGenError, generated_acir::GeneratedAcir}; use acvm::{ acir::native_types::{Expression, Witness}, FieldElement, @@ -254,6 +256,30 @@ impl AcirContext { self.acir_ir.push_return_witness(witness); } + /// Constrains the `AcirVar` variable to be of type `NumericType`. + pub(crate) fn numeric_cast_var( + &mut self, + variable: AcirVar, + numeric_type: &NumericType, + ) -> Result { + let data = &self.data[&variable]; + match numeric_type { + NumericType::Signed { .. } => todo!("signed integer conversion is unimplemented"), + NumericType::Unsigned { bit_size } => { + let data_expr = data.to_expression(); + let witness = self.acir_ir.get_or_create_witness(&data_expr); + self.acir_ir.range_constraint(witness, *bit_size)?; + } + NumericType::NativeField => { + // If someone has made a cast to a `Field` type then this is a Noop. + // + // The reason for doing this in code is for type safety; ie you have an + // integer, but a function requires the parameter to be a Field. + } + } + Ok(variable) + } + /// Terminates the context and takes the resulting `GeneratedAcir` pub(crate) fn finish(self) -> GeneratedAcir { self.acir_ir From a58f7a4b206ae5a5a86065702a3b0caf87ac95e1 Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sun, 28 May 2023 16:58:49 +0100 Subject: [PATCH 09/18] implement casting for numeric types --- .../src/ssa_refactor/acir_gen/mod.rs | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs index 6234cdd9e4c..3ede55f35c0 100644 --- a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs +++ b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs @@ -103,7 +103,10 @@ impl Context { let constrain_condition = self.convert_ssa_value(*value_id, dfg); self.acir_context.assert_eq_one(constrain_condition); } - _ => todo!(), + Instruction::Cast(value_id, typ) => { + self.convert_ssa_cast(value_id, typ, dfg); + } + _ => todo!("{instruction:?}"), } } @@ -170,4 +173,16 @@ impl Context { _ => todo!(), } } + /// Returns an `AcirVar` that is constrained to be + fn convert_ssa_cast(&mut self, value_id: &ValueId, typ: &Type, dfg: &DataFlowGraph) -> AcirVar { + let variable = self.convert_ssa_value(*value_id, dfg); + + match typ { + Type::Numeric(numeric_type) => self + .acir_context + .numeric_cast_var(variable, numeric_type) + .expect("invalid range constraint was applied {numeric_type}"), + _ => unimplemented!("The cast operation is only valid for integers."), + } + } } From ca60032c3990b0557b30f32c3056e0b9524a8366 Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sun, 28 May 2023 16:59:32 +0100 Subject: [PATCH 10/18] add simple range constraint example --- .../tests/test_data_ssa_refactor/simple_range/Nargo.toml | 5 +++++ .../tests/test_data_ssa_refactor/simple_range/Prover.toml | 1 + .../tests/test_data_ssa_refactor/simple_range/src/main.nr | 6 ++++++ 3 files changed, 12 insertions(+) create mode 100644 crates/nargo_cli/tests/test_data_ssa_refactor/simple_range/Nargo.toml create mode 100644 crates/nargo_cli/tests/test_data_ssa_refactor/simple_range/Prover.toml create mode 100644 crates/nargo_cli/tests/test_data_ssa_refactor/simple_range/src/main.nr diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/simple_range/Nargo.toml b/crates/nargo_cli/tests/test_data_ssa_refactor/simple_range/Nargo.toml new file mode 100644 index 00000000000..e0b467ce5da --- /dev/null +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/simple_range/Nargo.toml @@ -0,0 +1,5 @@ +[package] +authors = [""] +compiler_version = "0.1" + +[dependencies] \ No newline at end of file diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/simple_range/Prover.toml b/crates/nargo_cli/tests/test_data_ssa_refactor/simple_range/Prover.toml new file mode 100644 index 00000000000..07890234a19 --- /dev/null +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/simple_range/Prover.toml @@ -0,0 +1 @@ +x = "3" diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/simple_range/src/main.nr b/crates/nargo_cli/tests/test_data_ssa_refactor/simple_range/src/main.nr new file mode 100644 index 00000000000..9a4b9033493 --- /dev/null +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/simple_range/src/main.nr @@ -0,0 +1,6 @@ +// Tests a very simple program. +// +// The features being tested is casting to an integer +fn main(x : Field) { + let _z = x as u32; +} \ No newline at end of file From fbdfefa733e2a2fdf479e476f855f2949aff15fc Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sun, 28 May 2023 19:20:13 +0100 Subject: [PATCH 11/18] add constraints for `more_than_eq` --- .../acir_gen/acir_ir/generated_acir.rs | 60 ++++++++++++++++++- 1 file changed, 59 insertions(+), 1 deletion(-) diff --git a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs index 46d72a73ccc..80a8ddc741b 100644 --- a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs +++ b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs @@ -2,7 +2,10 @@ //! program as it is being converted from SSA form. use super::errors::AcirGenError; use acvm::acir::{ - circuit::opcodes::{BlackBoxFuncCall, FunctionInput, Opcode as AcirOpcode}, + circuit::{ + directives::QuotientDirective, + opcodes::{BlackBoxFuncCall, FunctionInput, Opcode as AcirOpcode}, + }, native_types::Witness, }; use acvm::{ @@ -240,4 +243,59 @@ impl GeneratedAcir { Ok(()) } + + /// Returns a `Witness` that is constrained to be: + /// - `1` if lhs >= rhs + /// - `0` otherwise + /// + /// See [R1CS Workshop - Section 10](https://github.com/mir-protocol/r1cs-workshop/blob/master/workshop.pdf) + /// for an explanation. + pub(crate) fn more_than_eq_comparison( + &mut self, + a: &Expression, + b: &Expression, + max_bits: u32, + ) -> Result { + // Ensure that 2^{max_bits + 1} is less than the field size + // + // TODO: perhaps this should be a user error, instead of an assert + assert!(max_bits + 1 < FieldElement::max_num_bits()); + + // Compute : 2^max_bits + a - b + let mut comparison_evaluation = a - b; + let two = FieldElement::from(2_i128); + let two_max_bits = two.pow(&FieldElement::from(max_bits as i128)); + comparison_evaluation.q_c += two_max_bits; + + let q_witness = self.next_witness_index(); + let r_witness = self.next_witness_index(); + + // Add constraint : 2^{max_bits} + a - b = q * 2^{max_bits} + r + let mut expr = Expression::default(); + expr.push_addition_term(two_max_bits, q_witness); + expr.push_addition_term(FieldElement::one(), r_witness); + self.push_opcode(AcirOpcode::Arithmetic(&comparison_evaluation - &expr)); + + self.push_opcode(AcirOpcode::Directive(Directive::Quotient(QuotientDirective { + a: comparison_evaluation, + b: Expression::from_field(two_max_bits), + q: q_witness, + r: r_witness, + predicate: None, + }))); + + // Add constraint to ensure `r` is correctly bounded + // between [0, 2^{max_bits}-1] + self.range_constraint(r_witness, max_bits)?; + // Add constraint to ensure that `q` is a boolean value + // in particular it should be the `n` bit of the comparison_evaluation + // which will indicate whether a >= b + // + // In the document linked above, they mention negating the value of `q` + // which would tell us whether a < b. Since we do not negate `q` + // what we get is a boolean indicating whether a >= b. + self.range_constraint(q_witness, 1)?; + + Ok(q_witness) + } } From 327c2f6a53ef7dc97f619a9a3bdc9397cf8523b1 Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sun, 28 May 2023 19:22:02 +0100 Subject: [PATCH 12/18] - add more_than_eq method - This method needs to know the bit size, so we cache this information whenever we do a range constraint. We should ideally also cache it for constants too since we can figure out their bit-sizes easily --- .../acir_gen/acir_ir/acir_variable.rs | 51 +++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/acir_variable.rs b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/acir_variable.rs index ed0946f8dcd..bf3455f7c0a 100644 --- a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/acir_variable.rs +++ b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/acir_variable.rs @@ -31,6 +31,9 @@ pub(crate) struct AcirContext { /// then the `acir_ir` will be populated to assert this /// addition. acir_ir: GeneratedAcir, + + /// Maps an `AcirVar` to its known bit size. + variables_to_bit_sizes: HashMap, } impl AcirContext { @@ -269,6 +272,8 @@ impl AcirContext { let data_expr = data.to_expression(); let witness = self.acir_ir.get_or_create_witness(&data_expr); self.acir_ir.range_constraint(witness, *bit_size)?; + // Log the bit size for this variable + self.variables_to_bit_sizes.insert(variable, *bit_size); } NumericType::NativeField => { // If someone has made a cast to a `Field` type then this is a Noop. @@ -280,6 +285,52 @@ impl AcirContext { Ok(variable) } + /// Returns an `AcirVar` which will be `1` if lhs >= rhs + /// and `0` otherwise. + fn more_than_eq_var(&mut self, lhs: AcirVar, rhs: AcirVar) -> Result { + let lhs_data = &self.data[&lhs]; + let rhs_data = &self.data[&rhs]; + + let lhs_expr = lhs_data.to_expression(); + let rhs_expr = rhs_data.to_expression(); + + let lhs_bit_size = self.variables_to_bit_sizes.get(&lhs).expect("comparisons cannot be made on variables with no known max bit size. This should have been caught by the frontend"); + let rhs_bit_size = self.variables_to_bit_sizes.get(&rhs).expect("comparisons cannot be made on variables with no known max bit size. This should have been caught by the frontend"); + + // This is a conservative choice. Technically, we should just be able to take + // the bit size of the `lhs` (upper bound), but we need to check/document what happens + // if the bit_size is not enough to represent both witnesses. + // An example is the following: (a as u8) >= (b as u32) + // If the equality is true, then it means that `b` also fits inside + // of a u8. + // But its not clear what happens if the equality is false, + // and we 8 bits to `more_than_eq_comparison`. The conservative + // choice chosen is to use 32. + let bit_size = *std::cmp::max(lhs_bit_size, rhs_bit_size); + + let is_greater_than_eq = + self.acir_ir.more_than_eq_comparison(&lhs_expr, &rhs_expr, bit_size)?; + + Ok(self.add_data(AcirVarData::Witness(is_greater_than_eq))) + } + + /// Returns an `AcirVar` which will be `1` if lhs < rhs + /// and `0` otherwise. + pub(crate) fn less_than_var( + &mut self, + lhs: AcirVar, + rhs: AcirVar, + ) -> Result { + // Flip the result of calling more than equal method to + // compute less than. + let comparison = self.more_than_eq_var(lhs, rhs)?; + + let one = self.add_constant(FieldElement::one()); + let comparison_negated = self.sub_var(one, comparison); + + Ok(comparison_negated) + } + /// Terminates the context and takes the resulting `GeneratedAcir` pub(crate) fn finish(self) -> GeneratedAcir { self.acir_ir From 90c2102898e2d51136b470b09cb7f5361028839d Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sun, 28 May 2023 19:22:35 +0100 Subject: [PATCH 13/18] add method to process less than binary operation --- .../src/ssa_refactor/acir_gen/mod.rs | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs index 3ede55f35c0..1ac9b6f7545 100644 --- a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs +++ b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs @@ -151,7 +151,7 @@ impl Context { Value::Intrinsic(..) => todo!(), Value::Function(..) => unreachable!("ICE: All functions should have been inlined"), Value::Instruction { .. } | Value::Param { .. } => { - unreachable!("ICE: Should have been in cache") + unreachable!("ICE: Should have been in cache {value:?}") } }; self.ssa_value_to_acir_var.insert(value_id, acir_var); @@ -170,6 +170,17 @@ impl Context { // Note: that this produces unnecessary constraints when // this Eq instruction is being used for a constrain statement BinaryOp::Eq => self.acir_context.eq_var(lhs, rhs), + // TODO: This is going to be somewhat inefficient initially since + // TODO: ACIR generates constraint using more_than_eq and then adds + // TODO: an opcode to switch it to less than, whereas + // TODO: SSA IR adds an instruction to do less_than + // TODO and then adds a not instruction to make it more_than_eq + // TODO: We can handle this on the ACIR side by adding an optimization + // TODO: though perhaps we can just switch SSA IR to use MoreThanEq? + BinaryOp::Lt => self + .acir_context + .less_than_var(lhs, rhs) + .expect("add Result types to all methods so errors bubble up"), _ => todo!(), } } From 99f414b30ee2e2f27a59c8ddb8d5778ce0cacb74 Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Sun, 28 May 2023 19:22:54 +0100 Subject: [PATCH 14/18] add example --- .../test_data_ssa_refactor/simple_comparison/Nargo.toml | 5 +++++ .../test_data_ssa_refactor/simple_comparison/Prover.toml | 1 + .../test_data_ssa_refactor/simple_comparison/src/main.nr | 6 ++++++ 3 files changed, 12 insertions(+) create mode 100644 crates/nargo_cli/tests/test_data_ssa_refactor/simple_comparison/Nargo.toml create mode 100644 crates/nargo_cli/tests/test_data_ssa_refactor/simple_comparison/Prover.toml create mode 100644 crates/nargo_cli/tests/test_data_ssa_refactor/simple_comparison/src/main.nr diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/simple_comparison/Nargo.toml b/crates/nargo_cli/tests/test_data_ssa_refactor/simple_comparison/Nargo.toml new file mode 100644 index 00000000000..e0b467ce5da --- /dev/null +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/simple_comparison/Nargo.toml @@ -0,0 +1,5 @@ +[package] +authors = [""] +compiler_version = "0.1" + +[dependencies] \ No newline at end of file diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/simple_comparison/Prover.toml b/crates/nargo_cli/tests/test_data_ssa_refactor/simple_comparison/Prover.toml new file mode 100644 index 00000000000..07890234a19 --- /dev/null +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/simple_comparison/Prover.toml @@ -0,0 +1 @@ +x = "3" diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/simple_comparison/src/main.nr b/crates/nargo_cli/tests/test_data_ssa_refactor/simple_comparison/src/main.nr new file mode 100644 index 00000000000..671ea6cf35e --- /dev/null +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/simple_comparison/src/main.nr @@ -0,0 +1,6 @@ +// Tests a very simple program. +// +// The features being tested is comparison +fn main(x : Field, y : Field) { + assert(x as u32 < y as u32); +} \ No newline at end of file From 8d7f7f905af3436d0c9ac17c2cd184dfa52ba665 Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Mon, 29 May 2023 18:24:01 +0100 Subject: [PATCH 15/18] assign result of cast operation --- crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs index 3ede55f35c0..f8a5e14bcc5 100644 --- a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs +++ b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs @@ -104,7 +104,10 @@ impl Context { self.acir_context.assert_eq_one(constrain_condition); } Instruction::Cast(value_id, typ) => { - self.convert_ssa_cast(value_id, typ, dfg); + let result_acir_var = self.convert_ssa_cast(value_id, typ, dfg); + let result_ids = dfg.instruction_results(instruction_id); + assert_eq!(result_ids.len(), 1, "Cast ops have a single result"); + self.ssa_value_to_acir_var.insert(result_ids[0], result_acir_var); } _ => todo!("{instruction:?}"), } From 6b159eec90327a6c21342a8b4e03235d41d38b7b Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Mon, 29 May 2023 18:51:37 +0100 Subject: [PATCH 16/18] add `y` as an input value --- .../tests/test_data_ssa_refactor/simple_comparison/Prover.toml | 1 + 1 file changed, 1 insertion(+) diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/simple_comparison/Prover.toml b/crates/nargo_cli/tests/test_data_ssa_refactor/simple_comparison/Prover.toml index 07890234a19..ed94d313315 100644 --- a/crates/nargo_cli/tests/test_data_ssa_refactor/simple_comparison/Prover.toml +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/simple_comparison/Prover.toml @@ -1 +1,2 @@ x = "3" +y = "4" From 1c2cee56f61e8122c7d62e617dd407a55d08a3ce Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Mon, 29 May 2023 18:52:27 +0100 Subject: [PATCH 17/18] return optimized circuit --- crates/noirc_evaluator/src/ssa_refactor.rs | 27 ++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) diff --git a/crates/noirc_evaluator/src/ssa_refactor.rs b/crates/noirc_evaluator/src/ssa_refactor.rs index 2959aef9661..199f6328090 100644 --- a/crates/noirc_evaluator/src/ssa_refactor.rs +++ b/crates/noirc_evaluator/src/ssa_refactor.rs @@ -50,8 +50,8 @@ pub(crate) fn optimize_into_acir(program: Program) -> GeneratedAcir { /// to use the new ssa module to process Noir code. pub fn experimental_create_circuit( program: Program, - _np_language: Language, - _is_opcode_supported: &impl Fn(&AcirOpcode) -> bool, + np_language: Language, + is_opcode_supported: &impl Fn(&AcirOpcode) -> bool, _enable_logging: bool, _show_output: bool, ) -> Result<(Circuit, Abi), RuntimeError> { @@ -65,8 +65,27 @@ pub fn experimental_create_circuit( let public_parameters = PublicInputs(public_abi.param_witnesses.values().flatten().copied().collect()); let return_values = PublicInputs(return_witnesses.into_iter().collect()); - let circuit = Circuit { current_witness_index, opcodes, public_parameters, return_values }; - Ok((circuit, abi)) + + // This region of code will optimize the ACIR bytecode for a particular backend + // it will be removed in the near future and we will subsequently only return the + // unoptimized backend-agnostic bytecode here + let optimized_circuit = { + use crate::errors::RuntimeErrorKind; + use acvm::compiler::optimizers::simplify::CircuitSimplifier; + + let abi_len = abi.field_count(); + + let simplifier = CircuitSimplifier::new(abi_len); + acvm::compiler::compile( + Circuit { current_witness_index, opcodes, public_parameters, return_values }, + np_language, + is_opcode_supported, + &simplifier, + ) + .map_err(|_| RuntimeErrorKind::Spanless(String::from("produced an acvm compile error")))? + }; + + Ok((optimized_circuit, abi)) } impl Ssa { From 7d8753b8d66ef48930e66b6029a7dcdca93fe535 Mon Sep 17 00:00:00 2001 From: Kevaundray Wedderburn Date: Tue, 30 May 2023 15:30:57 +0100 Subject: [PATCH 18/18] Addressed in Address GtEq extra opcodes #1444 --- crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs | 7 ------- 1 file changed, 7 deletions(-) diff --git a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs index dd2ab196215..f7f39c686ab 100644 --- a/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs +++ b/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs @@ -173,13 +173,6 @@ impl Context { // Note: that this produces unnecessary constraints when // this Eq instruction is being used for a constrain statement BinaryOp::Eq => self.acir_context.eq_var(lhs, rhs), - // TODO: This is going to be somewhat inefficient initially since - // TODO: ACIR generates constraint using more_than_eq and then adds - // TODO: an opcode to switch it to less than, whereas - // TODO: SSA IR adds an instruction to do less_than - // TODO and then adds a not instruction to make it more_than_eq - // TODO: We can handle this on the ACIR side by adding an optimization - // TODO: though perhaps we can just switch SSA IR to use MoreThanEq? BinaryOp::Lt => self .acir_context .less_than_var(lhs, rhs)