From 08281ff3709d8e40cf3921ec881585ab747e9d4c Mon Sep 17 00:00:00 2001 From: guipublic Date: Tue, 19 Dec 2023 11:32:51 +0000 Subject: [PATCH] comparison for signed integers --- .../src/ssa/acir_gen/acir_ir/acir_variable.rs | 50 +++++++++++++++++++ .../noirc_evaluator/src/ssa/acir_gen/mod.rs | 17 ++++--- .../signed_comparison/Nargo.toml | 6 +++ .../signed_comparison/Prover.toml | 3 ++ .../signed_comparison/src/main.nr | 13 +++++ 5 files changed, 83 insertions(+), 6 deletions(-) create mode 100644 test_programs/execution_success/signed_comparison/Nargo.toml create mode 100644 test_programs/execution_success/signed_comparison/Prover.toml create mode 100644 test_programs/execution_success/signed_comparison/src/main.nr diff --git a/compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs b/compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs index 712913841f3..813a2d5740a 100644 --- a/compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs +++ b/compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs @@ -936,6 +936,56 @@ impl AcirContext { Ok(remainder) } + /// Returns an 'AcirVar' containing the boolean value lhs diff<2^n, because the 2-complement representation keeps the ordering (e.g in 8 bits -1 is 255 > -2 = 254) + /// If not, lhs positive => diff > 2^n + /// and lhs negative => diff <= 2^n => diff < 2^n (because signs are not the same, so lhs != rhs and so diff != 2^n) + pub(crate) fn less_than_signed( + &mut self, + lhs: AcirVar, + rhs: AcirVar, + bit_count: u32, + predicate: AcirVar, + ) -> Result { + let pow_last = self.add_constant(FieldElement::from(1_u128 << (bit_count - 1))); + let pow = self.add_constant(FieldElement::from(1_u128 << (bit_count))); + + // We check whether the inputs have same sign or not by computing the XOR of their bit sign + let lhs_sign = self.div_var( + lhs, + pow_last, + AcirType::NumericType(NumericType::Unsigned { bit_size: bit_count }), + predicate, + )?; + let rhs_sign = self.div_var( + rhs, + pow_last, + AcirType::NumericType(NumericType::Unsigned { bit_size: bit_count }), + predicate, + )?; + let same_sign = self.xor_var( + lhs_sign, + rhs_sign, + AcirType::NumericType(NumericType::Signed { bit_size: 1 }), + )?; + + // We compute the input difference + let no_underflow = self.add_var(lhs, pow)?; + let diff = self.sub_var(no_underflow, rhs)?; + + // We check the 'bit sign' of the difference + let diff_sign = self.less_than_var(diff, pow, bit_count + 1, predicate)?; + + // Then the result is simply diff_sign XOR same_sign (can be checked with a truth table) + self.xor_var( + diff_sign, + same_sign, + AcirType::NumericType(NumericType::Signed { bit_size: 1 }), + ) + } + /// Returns an `AcirVar` which will be `1` if lhs >= rhs /// and `0` otherwise. pub(crate) fn more_than_eq_var( diff --git a/compiler/noirc_evaluator/src/ssa/acir_gen/mod.rs b/compiler/noirc_evaluator/src/ssa/acir_gen/mod.rs index d73bb514e02..01056355915 100644 --- a/compiler/noirc_evaluator/src/ssa/acir_gen/mod.rs +++ b/compiler/noirc_evaluator/src/ssa/acir_gen/mod.rs @@ -1569,12 +1569,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), - BinaryOp::Lt => self.acir_context.less_than_var( - lhs, - rhs, - bit_count, - self.current_side_effects_enabled_var, - ), + BinaryOp::Lt => match binary_type { + AcirType::NumericType(NumericType::Signed { .. }) => self + .acir_context + .less_than_signed(lhs, rhs, bit_count, self.current_side_effects_enabled_var), + _ => self.acir_context.less_than_var( + lhs, + rhs, + bit_count, + self.current_side_effects_enabled_var, + ), + }, BinaryOp::Xor => self.acir_context.xor_var(lhs, rhs, binary_type), BinaryOp::And => self.acir_context.and_var(lhs, rhs, binary_type), BinaryOp::Or => self.acir_context.or_var(lhs, rhs, binary_type), diff --git a/test_programs/execution_success/signed_comparison/Nargo.toml b/test_programs/execution_success/signed_comparison/Nargo.toml new file mode 100644 index 00000000000..c8de162877b --- /dev/null +++ b/test_programs/execution_success/signed_comparison/Nargo.toml @@ -0,0 +1,6 @@ +[package] +name = "signed_comparison" +type = "bin" +authors = [""] + +[dependencies] diff --git a/test_programs/execution_success/signed_comparison/Prover.toml b/test_programs/execution_success/signed_comparison/Prover.toml new file mode 100644 index 00000000000..e0e584b7380 --- /dev/null +++ b/test_programs/execution_success/signed_comparison/Prover.toml @@ -0,0 +1,3 @@ +x = "5" +y = "8" +z = "-15" diff --git a/test_programs/execution_success/signed_comparison/src/main.nr b/test_programs/execution_success/signed_comparison/src/main.nr new file mode 100644 index 00000000000..d020be380fb --- /dev/null +++ b/test_programs/execution_success/signed_comparison/src/main.nr @@ -0,0 +1,13 @@ +use dep::std; + +fn main(mut x: i8, mut y: i8, z: i8) { + let mut s1: i8 = 5; + let mut s2: i8 = 8; + assert(-1 as i8 < 0); + assert(x < y); + assert(-x < y); + assert(-y < -x); + assert((z > x) == false); + assert(x <= s1); + assert(z < x - y - s2); +}