From dd1b60e07bdadcd6756653ae7110997bff00daf2 Mon Sep 17 00:00:00 2001 From: guipublic Date: Tue, 27 Jun 2023 15:39:32 +0000 Subject: [PATCH 1/4] *WIP* --- .../acir_gen/acir_ir/acir_variable.rs | 45 ++++++++++++++--- .../acir_gen/acir_ir/generated_acir.rs | 50 +++++++++++++++++++ 2 files changed, 89 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 b4aa7258726..03db4885600 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 @@ -298,8 +298,10 @@ impl AcirContext { self.euclidean_division_var(lhs, rhs, bit_size)?; Ok(quotient_var) } - NumericType::Signed { .. } => { - todo!("Signed division"); + NumericType::Signed { bit_size } => { + let (quotient_var, _remainder_var) = + self.signed_division_var(lhs, rhs, bit_size)?; + Ok(quotient_var) } } } @@ -431,6 +433,37 @@ impl AcirContext { Ok((quotient_var, remainder_var)) } + /// Returns the quotient and remainder such that lhs = rhs * quotient + remainder + /// and |remainder| < |rhs| + /// and remainder has the same sign than lhs + /// Note that this is not the euclidian division, where we have instead remainder < |rhs| + /// + /// + /// + /// + + fn signed_division_var( + &mut self, + lhs: AcirVar, + rhs: AcirVar, + bit_size: u32, + ) -> Result<(AcirVar, AcirVar), AcirGenError> { + let lhs_data = &self.vars[&lhs].clone(); + let rhs_data = &self.vars[&rhs].clone(); + + let lhs_expr = lhs_data.to_expression(); + let rhs_expr = rhs_data.to_expression(); + let l_witness = self.acir_ir.get_or_create_witness(&lhs_expr); + let r_witness = self.acir_ir.get_or_create_witness(&rhs_expr); + assert_ne!(bit_size, 0); + let (q, r) = + self.acir_ir.signed_division(&l_witness.into(), &r_witness.into(), bit_size)?; + + let q_vd = AcirVarData::Expr(q); + let r_vd = AcirVarData::Expr(r); + Ok((self.add_data(q_vd), self.add_data(r_vd))) + } + /// Returns a variable which is constrained to be `lhs mod rhs` pub(crate) fn modulo_var( &mut self, @@ -493,8 +526,7 @@ impl AcirContext { ) -> Result { let data = &self.vars[&variable]; match numeric_type { - NumericType::Signed { .. } => todo!("signed integer constraining is unimplemented"), - NumericType::Unsigned { bit_size } => { + NumericType::Signed { bit_size } | 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)?; @@ -823,7 +855,7 @@ impl AcirContext { }); // Enforce the outputs to be sorted for i in 0..(outputs_var.len() - 1) { - self.less_than_constrain(outputs_var[i], outputs_var[i + 1], bit_size)?; + self.less_than_constrain(outputs_var[i], outputs_var[i + 1], bit_size, None)?; } // Enforce the outputs to be a permutation of the inputs self.acir_ir.permutation(&inputs_expr, &output_expr); @@ -837,8 +869,9 @@ impl AcirContext { lhs: AcirVar, rhs: AcirVar, bit_size: u32, + predicate: Option, ) -> Result<(), AcirGenError> { - let lhs_less_than_rhs = self.more_than_eq_var(rhs, lhs, bit_size, None)?; + let lhs_less_than_rhs = self.more_than_eq_var(rhs, lhs, bit_size, predicate)?; self.assert_eq_one(lhs_less_than_rhs) } } 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 11b1b6a6d92..4072ba7924c 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 @@ -307,6 +307,56 @@ impl GeneratedAcir { Ok(limb_witnesses) } + pub(crate) fn signed_division( + &mut self, + lhs: &Expression, + rhs: &Expression, + max_bit_size: u32, + ) -> Result<(Expression, Expression), AcirGenError> { + // maximum power of two for the bit size + let max_power_of_two = + FieldElement::from(2_i128).pow(&FieldElement::from(max_bit_size as i128 - 1)); + + //rhs / max_power_of_two + let (rhs_leading, rhs_mantissa) = self.euclidean_division( + rhs, + &max_power_of_two.into(), + max_bit_size, + &Expression::one(), + )?; + + //lhs / max_power_of_two + let (lhs_leading, lhs_mantissa) = self.euclidean_division( + lhs, + &max_power_of_two.into(), + max_bit_size, + &Expression::one(), + )?; + + // signed to unsigned + let l_inter = &Expression::from(lhs_leading) * &Expression::from(lhs_mantissa); + let r_inter = &Expression::from(rhs_leading) * &Expression::from(rhs_mantissa); + let unsigned_l = lhs.add_mul(FieldElement::from(2_i128), &l_inter); + let unsigned_r = rhs.add_mul(FieldElement::from(2_i128), &r_inter); + let unsigned_l_witness = self.get_or_create_witness(&unsigned_l); + let unsigned_r_witness = self.get_or_create_witness(&unsigned_r); + + let (q1, r1) = self.euclidean_division( + &unsigned_l_witness.into(), + &unsigned_r_witness.into(), + max_bit_size - 1, + &Expression::one(), + )?; + + // unsigned to signed + let q1_inter = &(&Expression::from_field(max_power_of_two) - &Expression::from(q1)) + * &rhs_leading.into(); + let quotient = Expression::from(q1).add_mul(FieldElement::from(2_i128), &q1_inter); + let r1_inter = &(&Expression::from_field(max_power_of_two) - &Expression::from(r1)) + * &lhs_leading.into(); + let remainder = Expression::from(r1).add_mul(FieldElement::from(2_i128), &r1_inter); + Ok((quotient, remainder)) + } /// Computes lhs/rhs by using euclidean division. /// /// Returns `q` for quotient and `r` for remainder such From eaf10fc21092c07d8f496bbeb04c0323922f7e30 Mon Sep 17 00:00:00 2001 From: guipublic Date: Tue, 4 Jul 2023 12:38:49 +0000 Subject: [PATCH 2/4] signed division through unsigned division --- .../acir_gen/acir_ir/generated_acir.rs | 63 +++++++++++++------ 1 file changed, 44 insertions(+), 19 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 4072ba7924c..6d4094323d3 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 @@ -307,40 +307,62 @@ impl GeneratedAcir { Ok(limb_witnesses) } + // Returns the 2-complement of lhs, using the provided sign bit in 'leading' + // if leading is zero, it returns lhs + // if leading is one, it returns 2^bit_size-lhs + fn two_complement( + &mut self, + lhs: &Expression, + leading: Witness, + max_bit_size: u32, + ) -> Expression { + let max_power_of_two = + FieldElement::from(2_i128).pow(&FieldElement::from(max_bit_size as i128 - 1)); + let inter = &(&Expression::from_field(max_power_of_two) - lhs) * &leading.into(); + lhs.add_mul(FieldElement::from(2_i128), &inter) + } + + /// Signed division lhs / rhs + /// We derive the signed division from the unsigned euclidian division. + /// note that this is not euclidian division! + // if x is a signed integer, then sign(x)x >= 0 + // so if a and b are signed integers, we can do the unsigned division: + // sign(a)a = q1*sign(b)b + r1 + // => a = sign(a)sign(b)q1*b + sign(a)r1 + // => a = qb+r, with |r|<|b| and a and r have the same sign. pub(crate) fn signed_division( &mut self, lhs: &Expression, rhs: &Expression, max_bit_size: u32, ) -> Result<(Expression, Expression), AcirGenError> { - // maximum power of two for the bit size + // 2^{max_bit size-1} let max_power_of_two = FieldElement::from(2_i128).pow(&FieldElement::from(max_bit_size as i128 - 1)); - //rhs / max_power_of_two - let (rhs_leading, rhs_mantissa) = self.euclidean_division( + // Get the sign bit of rhs by computing rhs / max_power_of_two + let (rhs_leading, _) = self.euclidean_division( rhs, &max_power_of_two.into(), max_bit_size, &Expression::one(), )?; - //lhs / max_power_of_two - let (lhs_leading, lhs_mantissa) = self.euclidean_division( + // Get the sign bit of lhs by computing lhs / max_power_of_two + let (lhs_leading, _) = self.euclidean_division( lhs, &max_power_of_two.into(), max_bit_size, &Expression::one(), )?; - // signed to unsigned - let l_inter = &Expression::from(lhs_leading) * &Expression::from(lhs_mantissa); - let r_inter = &Expression::from(rhs_leading) * &Expression::from(rhs_mantissa); - let unsigned_l = lhs.add_mul(FieldElement::from(2_i128), &l_inter); - let unsigned_r = rhs.add_mul(FieldElement::from(2_i128), &r_inter); - let unsigned_l_witness = self.get_or_create_witness(&unsigned_l); - let unsigned_r_witness = self.get_or_create_witness(&unsigned_r); + // Signed to unsigned: + let unsigned_lhs = self.two_complement(lhs, lhs_leading, max_bit_size); + let unsigned_rhs = self.two_complement(rhs, rhs_leading, max_bit_size); + let unsigned_l_witness = self.get_or_create_witness(&unsigned_lhs); + let unsigned_r_witness = self.get_or_create_witness(&unsigned_rhs); + // Performs the division using the unsigned values of lhs and rhs let (q1, r1) = self.euclidean_division( &unsigned_l_witness.into(), &unsigned_r_witness.into(), @@ -348,15 +370,18 @@ impl GeneratedAcir { &Expression::one(), )?; - // unsigned to signed - let q1_inter = &(&Expression::from_field(max_power_of_two) - &Expression::from(q1)) - * &rhs_leading.into(); - let quotient = Expression::from(q1).add_mul(FieldElement::from(2_i128), &q1_inter); - let r1_inter = &(&Expression::from_field(max_power_of_two) - &Expression::from(r1)) - * &lhs_leading.into(); - let remainder = Expression::from(r1).add_mul(FieldElement::from(2_i128), &r1_inter); + // Unsigned to signed: derive q and r from q1,r1 and the signs of lhs and rhs + // Quotient sign is lhs sign * rhs sign, whose resulting sign bit is the XOR of the sign bits + let q_sign = (&Expression::from(lhs_leading) + &Expression::from(rhs_leading)).add_mul( + -FieldElement::from(2_i128), + &(&Expression::from(lhs_leading) * &Expression::from(rhs_leading)), + ); + let q_sign_witness = self.get_or_create_witness(&q_sign); + let quotient = self.two_complement(&q1.into(), q_sign_witness, max_bit_size); + let remainder = self.two_complement(&r1.into(), lhs_leading, max_bit_size); Ok((quotient, remainder)) } + /// Computes lhs/rhs by using euclidean division. /// /// Returns `q` for quotient and `r` for remainder such From 7c212c14cdd947f24d453569f81a973c4cd911e6 Mon Sep 17 00:00:00 2001 From: guipublic Date: Tue, 4 Jul 2023 12:51:02 +0000 Subject: [PATCH 3/4] signed division unit test --- .../unsigned_division/Nargo.toml | 5 ++++ .../unsigned_division/Prover.toml | 3 ++ .../unsigned_division/src/main.nr | 28 +++++++++++++++++++ 3 files changed, 36 insertions(+) create mode 100644 crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/Nargo.toml create mode 100644 crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/Prover.toml create mode 100644 crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/src/main.nr diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/Nargo.toml b/crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/Nargo.toml new file mode 100644 index 00000000000..e0b467ce5da --- /dev/null +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/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/unsigned_division/Prover.toml b/crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/Prover.toml new file mode 100644 index 00000000000..ee6f0ef229a --- /dev/null +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/Prover.toml @@ -0,0 +1,3 @@ +x = "7" +y = "3" +z = "2" \ No newline at end of file diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/src/main.nr b/crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/src/main.nr new file mode 100644 index 00000000000..cd0f2ee4776 --- /dev/null +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/src/main.nr @@ -0,0 +1,28 @@ +use dep::std; + +// Testing signed integer division: +// 7/3 = 2 +// -7/3 = -2 +// -7/-3 = 2 +// 7/-3 = -2 +fn main(mut x: i32, mut y: i32, mut z: i32) { + // 7/3 = 2 + assert(x / y == z); + + // -7/3 = -2 + x = 0-x; + z = 0-z; + assert(x+7==0); + assert(z+2==0); + assert(x / y == z); + + // -7/-3 = 2 + y = 0 - y; + z = 0-z; + assert(x / y == z); + + // 7/-3 = -2 + x = 0 - x; + z = 0-z; + assert(x / y == z); +} From 6021ec8cb85523e4c0294cf2ee9cde40b4f80db1 Mon Sep 17 00:00:00 2001 From: guipublic Date: Tue, 4 Jul 2023 16:27:02 +0000 Subject: [PATCH 4/4] code review --- .../Nargo.toml | 0 .../Prover.toml | 0 .../src/main.nr | 19 ++++++++----------- .../acir_gen/acir_ir/acir_variable.rs | 2 +- 4 files changed, 9 insertions(+), 12 deletions(-) rename crates/nargo_cli/tests/test_data_ssa_refactor/{unsigned_division => signed_division}/Nargo.toml (100%) rename crates/nargo_cli/tests/test_data_ssa_refactor/{unsigned_division => signed_division}/Prover.toml (100%) rename crates/nargo_cli/tests/test_data_ssa_refactor/{unsigned_division => signed_division}/src/main.nr (52%) diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/Nargo.toml b/crates/nargo_cli/tests/test_data_ssa_refactor/signed_division/Nargo.toml similarity index 100% rename from crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/Nargo.toml rename to crates/nargo_cli/tests/test_data_ssa_refactor/signed_division/Nargo.toml diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/Prover.toml b/crates/nargo_cli/tests/test_data_ssa_refactor/signed_division/Prover.toml similarity index 100% rename from crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/Prover.toml rename to crates/nargo_cli/tests/test_data_ssa_refactor/signed_division/Prover.toml diff --git a/crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/src/main.nr b/crates/nargo_cli/tests/test_data_ssa_refactor/signed_division/src/main.nr similarity index 52% rename from crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/src/main.nr rename to crates/nargo_cli/tests/test_data_ssa_refactor/signed_division/src/main.nr index cd0f2ee4776..22f0109ad1e 100644 --- a/crates/nargo_cli/tests/test_data_ssa_refactor/unsigned_division/src/main.nr +++ b/crates/nargo_cli/tests/test_data_ssa_refactor/signed_division/src/main.nr @@ -10,19 +10,16 @@ fn main(mut x: i32, mut y: i32, mut z: i32) { assert(x / y == z); // -7/3 = -2 - x = 0-x; - z = 0-z; - assert(x+7==0); - assert(z+2==0); - assert(x / y == z); + let minus_x = 0-x; + let minus_z = 0-z; + let minus_y = 0-y; + assert(x+minus_x==0); + assert(z+minus_z==0); + assert(minus_x / y == minus_z); // -7/-3 = 2 - y = 0 - y; - z = 0-z; - assert(x / y == z); + assert(minus_x / minus_y == z); // 7/-3 = -2 - x = 0 - x; - z = 0-z; - assert(x / y == z); + assert(x / minus_y == minus_z); } 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 03db4885600..80a1fa02a8a 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 @@ -455,7 +455,7 @@ impl AcirContext { let rhs_expr = rhs_data.to_expression(); let l_witness = self.acir_ir.get_or_create_witness(&lhs_expr); let r_witness = self.acir_ir.get_or_create_witness(&rhs_expr); - assert_ne!(bit_size, 0); + assert_ne!(bit_size, 0, "signed integer should have at least one bit"); let (q, r) = self.acir_ir.signed_division(&l_witness.into(), &r_witness.into(), bit_size)?;