feat: implement euclidean division and signed division in terms of AcirVars

compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/generated_acir.rs

@@ -290,24 +290,6 @@ 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 intermediate =
-            self.mul_with_witness(&(&Expression::from(max_power_of_two) - lhs), &leading.into());
-
-        lhs.add_mul(FieldElement::from(2_i128), &intermediate)
-    }
-
     /// Returns an expression which represents `lhs * rhs`
     ///
     /// If one has multiplicative term and the other is of degree one or more,
@@ -357,220 +339,6 @@ impl GeneratedAcir {
         (&*lhs_reduced * &*rhs_reduced).expect("Both expressions are reduced to be degree <= 1")
     }
 
-    /// Signed division lhs /  rhs
-    /// We derive the signed division from the unsigned euclidean division.
-    /// note that this is not euclidean 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), RuntimeError> {
-        // 2^{max_bit size-1}
-        let max_power_of_two =
-            FieldElement::from(2_i128).pow(&FieldElement::from(max_bit_size as i128 - 1));
-
-        // Get the sign bit of rhs by computing rhs / max_power_of_two
-        let (rhs_leading_witness, _) = self.euclidean_division(
-            rhs,
-            &max_power_of_two.into(),
-            max_bit_size,
-            &Expression::one(),
-        )?;
-
-        // Get the sign bit of lhs by computing lhs / max_power_of_two
-        let (lhs_leading_witness, _) = self.euclidean_division(
-            lhs,
-            &max_power_of_two.into(),
-            max_bit_size,
-            &Expression::one(),
-        )?;
-
-        // Signed to unsigned:
-        let unsigned_lhs = self.two_complement(lhs, lhs_leading_witness, max_bit_size);
-        let unsigned_rhs = self.two_complement(rhs, rhs_leading_witness, 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(),
-            max_bit_size - 1,
-            &Expression::one(),
-        )?;
-
-        // 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 sign_sum =
-            &Expression::from(lhs_leading_witness) + &Expression::from(rhs_leading_witness);
-        let sign_prod = (&Expression::from(lhs_leading_witness)
-            * &Expression::from(rhs_leading_witness))
-            .expect("Product of two witnesses so result is degree 2");
-        let q_sign = sign_sum.add_mul(-FieldElement::from(2_i128), &sign_prod);
-
-        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_witness, max_bit_size);
-        Ok((quotient, remainder))
-    }
-
-    /// Computes lhs/rhs by using euclidean division.
-    ///
-    /// Returns `q` for quotient and `r` for remainder such
-    /// that lhs = rhs * q + r
-    pub(crate) fn euclidean_division(
-        &mut self,
-        lhs: &Expression,
-        rhs: &Expression,
-        max_bit_size: u32,
-        predicate: &Expression,
-    ) -> Result<(Witness, Witness), RuntimeError> {
-        // lhs = rhs * q + r
-        //
-        // If predicate is zero, `q_witness` and `r_witness` will be 0
-
-        // Check that we the rhs is not zero.
-        // Otherwise, when executing the brillig quotient we may attempt to divide by zero, causing a VM panic.
-        //
-        // When the predicate is 0, the equation always passes.
-        // When the predicate is 1, the rhs must not be 0.
-        let rhs_is_nonzero_const = rhs.is_const() && !rhs.is_zero();
-        if !rhs_is_nonzero_const {
-            match predicate.to_const() {
-                Some(predicate) if predicate.is_zero() => {
-                    // If predicate is known to be inactive, we don't need to lay down constraints.
-                }
-
-                Some(predicate) if predicate.is_one() => {
-                    // If the predicate is known to be active, we simply assert that an inverse must exist.
-                    // This implies that `rhs != 0`.
-                    let unsafe_inverse = self.brillig_inverse(rhs.clone());
-                    let rhs_has_inverse =
-                        self.mul_with_witness(rhs, &unsafe_inverse.into()) - FieldElement::one();
-                    self.assert_is_zero(rhs_has_inverse);
-                }
-
-                _ => {
-                    // Otherwise we must handle both potential cases.
-                    let rhs_is_zero = self.is_zero(rhs);
-                    let rhs_is_not_zero = self.mul_with_witness(&rhs_is_zero.into(), predicate);
-                    self.assert_is_zero(rhs_is_not_zero);
-                }
-            }
-        }
-
-        // maximum bit size for q and for [r and rhs]
-        let mut max_q_bits = max_bit_size;
-        let mut max_rhs_bits = max_bit_size;
-        // when rhs is constant, we can better estimate the maximum bit sizes
-        if let Some(rhs_const) = rhs.to_const() {
-            max_rhs_bits = rhs_const.num_bits();
-            if max_rhs_bits != 0 {
-                if max_rhs_bits > max_bit_size {
-                    let zero = self.get_or_create_witness(&Expression::zero());
-                    return Ok((zero, zero));
-                }
-                max_q_bits = max_bit_size - max_rhs_bits + 1;
-            }
-        }
-
-        // Avoids overflow: 'q*b+r < 2^max_q_bits*2^max_rhs_bits'
-        let mut avoid_overflow = false;
-        if max_q_bits + max_rhs_bits >= FieldElement::max_num_bits() - 1 {
-            // q*b+r can overflow; we avoid this when b is constant
-            if rhs.is_const() {
-                avoid_overflow = true;
-            } else {
-                // we do not support unbounded division
-                unreachable!("overflow in unbounded division");
-            }
-        }
-
-        let (q_witness, r_witness) =
-            self.brillig_quotient(lhs.clone(), rhs.clone(), predicate.clone(), max_bit_size + 1);
-
-        // Constrain `q < 2^{max_q_bits}`.
-        self.range_constraint(q_witness, max_q_bits)?;
-
-        // Constrain `r < 2^{max_rhs_bits}`.
-        //
-        // If `rhs` is a power of 2, then is just a looser version of the following bound constraint.
-        // In the case where `rhs` isn't a power of 2 then this range constraint is required
-        // as the bound constraint creates a new witness.
-        // This opcode will be optimized out if it is redundant so we always add it for safety.
-        self.range_constraint(r_witness, max_rhs_bits)?;
-
-        // Constrain `r < rhs`.
-        self.bound_constraint_with_offset(&r_witness.into(), rhs, predicate, max_rhs_bits)?;
-
-        // a * predicate == (b * q + r) * predicate
-        // => predicate * (a - b * q - r) == 0
-        // When the predicate is 0, the equation always passes.
-        // When the predicate is 1, the euclidean division needs to be
-        // true.
-        let rhs_constraint = &self.mul_with_witness(rhs, &q_witness.into()) + r_witness;
-        let div_euclidean = &self.mul_with_witness(lhs, predicate)
-            - &self.mul_with_witness(&rhs_constraint, predicate);
-
-        if let Some(rhs_const) = rhs.to_const() {
-            if avoid_overflow {
-                // we compute q0 = p/rhs
-                let rhs_big = BigUint::from_bytes_be(&rhs_const.to_be_bytes());
-                let q0_big = FieldElement::modulus() / &rhs_big;
-                let q0 = FieldElement::from_be_bytes_reduce(&q0_big.to_bytes_be());
-                // when q == q0, b*q+r can overflow so we need to bound r to avoid the overflow.
-                let size_predicate =
-                    self.is_equal(&Expression::from_field(q0), &Expression::from(q_witness));
-                let predicate = self.mul_with_witness(&size_predicate.into(), predicate);
-                // Ensure that there is no overflow, under q == q0 predicate
-                let max_r_big = FieldElement::modulus() - q0_big * rhs_big;
-                let max_r = FieldElement::from_be_bytes_reduce(&max_r_big.to_bytes_be());
-                let max_r_predicate =
-                    self.mul_with_witness(&predicate, &Expression::from_field(max_r));
-                let r_predicate = self.mul_with_witness(&Expression::from(r_witness), &predicate);
-                // Bound the remainder to be <p-q0*b, if the predicate is true.
-                self.bound_constraint_with_offset(
-                    &r_predicate,
-                    &max_r_predicate,
-                    &predicate,
-                    rhs_const.num_bits(),
-                )?;
-            }
-        }
-
-        self.push_opcode(AcirOpcode::Arithmetic(div_euclidean));
-
-        Ok((q_witness, r_witness))
-    }
-
-    /// Adds a brillig opcode which injects witnesses with values `q = a / b` and `r = a % b`.
-    ///
-    /// Suitable range constraints for `q` and `r` must be applied externally.
-    pub(crate) fn brillig_quotient(
-        &mut self,
-        lhs: Expression,
-        rhs: Expression,
-        predicate: Expression,
-        max_bit_size: u32,
-    ) -> (Witness, Witness) {
-        // Create the witness for the result
-        let q_witness = self.next_witness_index();
-        let r_witness = self.next_witness_index();
-
-        let quotient_code = brillig_directive::directive_quotient(max_bit_size);
-        let inputs = vec![BrilligInputs::Single(lhs), BrilligInputs::Single(rhs)];
-        let outputs = vec![BrilligOutputs::Simple(q_witness), BrilligOutputs::Simple(r_witness)];
-        self.brillig(Some(predicate), quotient_code, inputs, outputs);
-
-        (q_witness, r_witness)
-    }
-
     /// Generate constraints that are satisfied iff
     /// lhs < rhs , when offset is 1, or
     /// lhs <= rhs, when offset is 0
@@ -582,7 +350,7 @@ impl GeneratedAcir {
     /// n.b: we do NOT check here that lhs and rhs are indeed 'bits' size
     /// lhs < rhs <=> a+1<=b
     /// TODO: Consolidate this with bounds_check function.
-    fn bound_constraint_with_offset(
+    pub(super) fn bound_constraint_with_offset(
         &mut self,
         lhs: &Expression,
         rhs: &Expression,
@@ -616,7 +384,7 @@ impl GeneratedAcir {
             // we now have lhs+offset <= rhs <=> lhs_offset <= rhs_offset
 
             let bit_size = bit_size_u128(rhs_offset);
-            // r = 2^bit_size - rhs_offset -1, is of bit size  'bit_size' by construtction
+            // r = 2^bit_size - rhs_offset -1, is of bit size  'bit_size' by construction
             let r = (1_u128 << bit_size) - rhs_offset - 1;
             // however, since it is a constant, we can compute it's actual bit size
             let r_bit_size = bit_size_u128(r);
@@ -786,75 +554,6 @@ impl GeneratedAcir {
         Ok(())
     }
 
-    /// Returns a `Witness` that is constrained to be:
-    /// - `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 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,
-        b: &Expression,
-        max_bits: u32,
-        predicate: Expression,
-    ) -> Result<Witness, RuntimeError> {
-        // Ensure that 2^{max_bits + 1} is less than the field size
-        //
-        // TODO: perhaps this should be a user error, instead of an assert
-        assert!(max_bits + 1 < FieldElement::max_num_bits());
-
-        // Compute : 2^{max_bits} + a - b
-        let two = FieldElement::from(2_i128);
-        let two_max_bits: FieldElement = two.pow(&FieldElement::from(max_bits as i128));
-        let comparison_evaluation = (a - b) + two_max_bits;
-
-        // euclidean division by 2^{max_bits}  : 2^{max_bits} + a - b = q * 2^{max_bits} + r
-        //
-        // 2^{max_bits} is of max_bits+1 bit size
-        // If a>b, then a-b is less than 2^{max_bits} - 1, so 2^{max_bits} + a - b is less than 2^{max_bits} + 2^{max_bits} - 1 = 2^{max_bits+1} - 1
-        // If a <= b, then 2^{max_bits} + a - b is less than 2^{max_bits} <= 2^{max_bits+1} - 1
-        // This means that both operands of the division have at most max_bits+1 bit size.
-        //
-        // case: a == b
-        //
-        //   let k = 0;
-        // - 2^{max_bits} == q *  2^{max_bits} + r
-        // - This is only the case when q == 1 and r == 0 (assuming r is bounded to be less than 2^{max_bits})
-        //
-        // case: a > b
-        //
-        //   let k = a - b;
-        // - k + 2^{max_bits} == q * 2^{max_bits} + r
-        // - This is the case when q == 1 and r = k
-        //
-        // case: a < b
-        //
-        //   let k = b - a
-        // - 2^{max_bits} - k == q * 2^{max_bits} + r
-        // - This is only the case when q == 0 and r == 2^{max_bits} - k
-        //
-        let (q, _) = self.euclidean_division(
-            &comparison_evaluation,
-            &Expression::from(two_max_bits),
-            max_bits + 1,
-            &predicate,
-        )?;
-        Ok(q)
-    }
-
     pub(crate) fn brillig(
         &mut self,
         predicate: Option<Expression>,