chore: Document GeneratedAcir::more_than_eq_comparison

crates/noirc_evaluator/src/ssa_refactor/acir_gen/acir_ir/generated_acir.rs

@@ -680,8 +680,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 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. 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 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,