chore: remove GeneratedAcir::is_equal

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

@@ -597,97 +597,6 @@ impl GeneratedAcir {
         self.push_opcode(AcirOpcode::Arithmetic(expr));
     }
 
-    /// Returns a `Witness` that is constrained to be:
-    /// - `1` if `lhs == rhs`
-    /// - `0` otherwise
-    ///
-    /// Intuition: the equality of two Expressions is linked to whether
-    /// their difference has an inverse; `a == b` implies that `a - b == 0`
-    /// which implies that a - b has no inverse. So if two variables are equal,
-    /// their difference will have no inverse.
-    ///
-    /// First, lets create a new variable that is equal to the difference
-    /// of the two expressions: `t = lhs - rhs` (constraint has been applied)
-    ///
-    /// Next lets create a new variable `y` which will be the Witness that we will ultimately
-    /// return indicating whether `lhs == rhs`.
-    /// Note: During this process we need to apply constraints that ensure that it is a boolean.
-    /// But right now with no constraints applied to it, it is essentially a free variable.
-    ///
-    /// Next we apply the following constraint `y * t == 0`.
-    /// This implies that either `y` or `t` or both is `0`.
-    /// - If `t == 0`, then this means that `lhs == rhs`.
-    /// - If `y == 0`, this does not mean anything at this point in time, due to it having no
-    /// constraints.
-    ///
-    /// Naively, we could apply the following constraint: `y == 1 - t`.
-    /// This along with the previous `y * t == 0` constraint means that
-    /// `y` or `t` needs to be zero, but they both cannot be zero.
-    ///
-    /// This equation however falls short when lhs != rhs because then `t`
-    /// may not be `1`. If `t` is non-zero, then `y` is also non-zero due to
-    /// `y == 1 - t` and the equation `y * t == 0` fails.  
-    ///
-    /// To fix, we introduce another free variable called `z` and apply the following
-    /// constraint instead: `y == 1 - t * z`.
-    ///
-    /// When `lhs == rhs`, `t` is `0` and so `y` is `1`.
-    /// When `lhs != rhs`, `t` is non-zero, however the prover can set `z = 1/t`
-    /// which will make `y = 1 - t * 1/t = 0`.
-    ///
-    /// We now arrive at the conclusion that when `lhs == rhs`, `y` is `1` and when
-    /// `lhs != rhs`, then `y` is `0`.
-    ///  
-    /// Bringing it all together, We introduce three variables `y`, `t` and `z`,
-    /// With the following equations:
-    /// - `t == lhs - rhs`
-    /// - `y == 1 - tz` (`z` is a value that is chosen to be the inverse of `t` by the prover)
-    /// - `y * t == 0`
-    ///
-    /// Lets convince ourselves that the prover cannot prove an untrue statement.
-    ///
-    /// Assume that `lhs == rhs`, can the prover return `y == 0`?
-    ///
-    /// When `lhs == rhs`, `t` is 0. There is no way to make `y` be zero
-    /// since `y = 1 - 0 * z = 1`.
-    ///
-    /// Assume that `lhs != rhs`, can the prover return `y == 1`?
-    ///
-    /// When `lhs != rhs`, then `t` is non-zero.
-    /// By setting `z` to be `0`, we can make `y` equal to `1`.
-    /// This is easily observed: `y = 1 - t * 0`
-    /// Now since `y` is one, this means that `t` needs to be zero, or else `y * t == 0` will fail.
-    pub(crate) fn is_equal(&mut self, lhs: &Expression, rhs: &Expression) -> Witness {
-        let t = lhs - rhs;
-        // We avoid passing the expression to `self.brillig_inverse` directly because we need
-        // the `Witness` representation for constructing `y_is_boolean_constraint`.
-        let t_witness = self.get_or_create_witness(&t);
-
-        // Call the inversion directive, since we do not apply a constraint
-        // the prover can choose anything here.
-        let z = self.brillig_inverse(t_witness.into());
-
-        let y = self.next_witness_index();
-
-        // Add constraint y == 1 - tz => y + tz - 1 == 0
-        let y_is_boolean_constraint = Expression {
-            mul_terms: vec![(FieldElement::one(), t_witness, z)],
-            linear_combinations: vec![(FieldElement::one(), y)],
-            q_c: -FieldElement::one(),
-        };
-        self.assert_is_zero(y_is_boolean_constraint);
-
-        // Add constraint that y * t == 0;
-        let ty_zero_constraint = Expression {
-            mul_terms: vec![(FieldElement::one(), t_witness, y)],
-            linear_combinations: vec![],
-            q_c: FieldElement::zero(),
-        };
-        self.assert_is_zero(ty_zero_constraint);
-
-        y
-    }
-
     /// Adds a constraint which ensure thats `witness` is an
     /// integer within the range `[0, 2^{num_bits} - 1]`
     pub(crate) fn range_constraint(