Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: comparison for signed integers #3873

Merged
merged 2 commits into from
Dec 19, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
50 changes: 50 additions & 0 deletions compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs
Original file line number Diff line number Diff line change
Expand Up @@ -936,6 +936,56 @@ impl AcirContext {
Ok(remainder)
}

/// Returns an 'AcirVar' containing the boolean value lhs<rhs, assuming lhs and rhs are signed integers of size bit_count.
/// Like in the unsigned case, we compute the difference diff = lhs-rhs+2^n (and we avoid underflow)
/// The result depends on the diff and the signs of the inputs:
/// If same sign, lhs<rhs <=> 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<AcirVar, RuntimeError> {
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(
Expand Down
17 changes: 11 additions & 6 deletions compiler/noirc_evaluator/src/ssa/acir_gen/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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),
Expand Down
6 changes: 6 additions & 0 deletions test_programs/execution_success/signed_comparison/Nargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
[package]
name = "signed_comparison"
type = "bin"
authors = [""]

[dependencies]
3 changes: 3 additions & 0 deletions test_programs/execution_success/signed_comparison/Prover.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
x = "5"
y = "8"
z = "-15"
13 changes: 13 additions & 0 deletions test_programs/execution_success/signed_comparison/src/main.nr
Original file line number Diff line number Diff line change
@@ -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);
}
Loading