diff --git a/crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/generated_acir.rs b/crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/generated_acir.rs index 37fac411e26..6660f654b4a 100644 --- a/crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/generated_acir.rs +++ b/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(