From f9b141b66769dbdda231b7e64a80539db35bfb83 Mon Sep 17 00:00:00 2001 From: guipublic Date: Fri, 28 Jul 2023 16:20:32 +0000 Subject: [PATCH 1/3] document comparison --- .../acir_gen/acir_ir/generated_acir.rs | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 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 18c7216a6fa..17603e66615 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 @@ -673,8 +673,20 @@ impl GeneratedAcir { /// - `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. + /// We essentially computes the sign bit of b-a + /// For this we sign-extend b-a with c = 2^{max_bits} - (b - a), since both a and b are < 2^{max_bits} + /// Then we get the bit sign of c, the 2-complement representation of (b-a), which is a max_bits+1 integer, + /// by doing the euclidian division c / 2^{max_bits} + /// + /// To see why it really works; + /// We first note that c is an integer of (max_bits+1) bits. Therfore, + /// if b-a>0, then c < 2^{max_bits}, so the division by 2^{max_bits} will give 0 + /// If b-a<=0, then c >= 2^{max_bits}, so the division by 2^{max_bits} will give 1. + /// + /// In other words, 1 means a >= b and 0 means b > a. + /// The important thing here is that c does not overflow nor underflow the field; + /// - By construction we have c >= 0, so there is no underflow + /// - We assert at the begining that 2^{max_bits+1} does not overflow the field, so neither c. pub(crate) fn more_than_eq_comparison( &mut self, a: &Expression, From 7abb0eb2628299efb68abd09e6f4d84bb6fd3554 Mon Sep 17 00:00:00 2001 From: guipublic Date: Mon, 31 Jul 2023 14:14:58 +0000 Subject: [PATCH 2/3] code review --- .../acir_gen/acir_ir/generated_acir.rs | 24 +++++++++---------- 1 file changed, 12 insertions(+), 12 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 657589f816f..ec015fd2666 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 @@ -680,20 +680,20 @@ impl GeneratedAcir { /// - `1` if lhs >= rhs /// - `0` otherwise /// - /// We essentially computes the sign bit of b-a - /// For this we sign-extend b-a with c = 2^{max_bits} - (b - a), since both a and b are < 2^{max_bits} - /// Then we get the bit sign of c, the 2-complement representation of (b-a), which is a max_bits+1 integer, - /// by doing the euclidian division c / 2^{max_bits} + /// We essentially computes the sign bit of `b-a` + /// For this we sign-extend `b-a` with `c = 2^{max_bits} - (b - a)`, since both `a` and `b` are less than `2^{max_bits}` + /// Then we get the bit sign of `c`, the 2-complement representation of `(b-a)`, which is a `max_bits+1` integer, + /// by doing the euclidean division `c / 2^{max_bits}` /// /// To see why it really works; - /// We first note that c is an integer of (max_bits+1) bits. Therfore, - /// if b-a>0, then c < 2^{max_bits}, so the division by 2^{max_bits} will give 0 - /// If b-a<=0, then c >= 2^{max_bits}, so the division by 2^{max_bits} will give 1. - /// - /// In other words, 1 means a >= b and 0 means b > a. - /// The important thing here is that c does not overflow nor underflow the field; - /// - By construction we have c >= 0, so there is no underflow - /// - We assert at the begining that 2^{max_bits+1} does not overflow the field, so neither c. + /// We first note that `c` is an integer of `(max_bits+1)` bits. Therefore, + /// if `b-a>0`, then `c < 2^{max_bits}`, so the division by `2^{max_bits}` will give `0` + /// If `b-a<=0`, then `c >= 2^{max_bits}`, so the division by `2^{max_bits}` will give `1`. + /// + /// In other words, `1` means `a >= b` and `0` means `b > a`. + /// The important thing here is that `c` does not overflow nor underflow the field; + /// - By construction we have `c >= 0`, so there is no underflow + /// - We assert at the begining that `2^{max_bits+1}` does not overflow the field, so neither c. pub(crate) fn more_than_eq_comparison( &mut self, a: &Expression, From 0919b0ef53c8f3ac03a8d1dfe4d982b8ee1ee718 Mon Sep 17 00:00:00 2001 From: Tom French <15848336+TomAFrench@users.noreply.github.com> Date: Tue, 1 Aug 2023 09:49:13 +0100 Subject: [PATCH 3/3] Update crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs --- .../src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs | 2 +- 1 file changed, 1 insertion(+), 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 ec015fd2666..77ca298e164 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 @@ -693,7 +693,7 @@ impl GeneratedAcir { /// In other words, `1` means `a >= b` and `0` means `b > a`. /// The important thing here is that `c` does not overflow nor underflow the field; /// - By construction we have `c >= 0`, so there is no underflow - /// - We assert at the begining that `2^{max_bits+1}` does not overflow the field, so neither c. + /// - We assert at the beginning that `2^{max_bits+1}` does not overflow the field, so neither c. pub(crate) fn more_than_eq_comparison( &mut self, a: &Expression,