Change `Instruction::Constrain(lhs, rhs, msg)` to `Instruction::Constrain(bool, msg)`

[jfecher]

Problem

Including the equality as part of the constrain statement can lead to some missed bugs (https://github.com/noir-lang/noir/pull/3740) and extra needed optimizations (https://github.com/noir-lang/noir/pull/3708) stemming from the need to implement code twice - once for Instruction::Constrain, and once for the equality operator in a binary instruction.

Happy Case

We can change Instruction::Constrain back to taking a single ValueId argument. To ensure the generated Acir is just as efficient, when converting the new constrain to acir we can check if its argument is an equality node and if so keep the current codepath for an equality constraint. If it is not an equality we can fallback to an == true like we do today in SSA.

Alternatives Considered

No response

Additional Context

No response

Would you like to submit a PR for this Issue?

No

Support Needs

No response

[TomAFrench]

I've been doing some thinking on this and I don't think that it would be useful for us to make Instruction::Constrain to be unary.

The bug in #3740 is due to us (me) allowing an array equality to slip into SSA by trying to do an optimisation during codegen, this is fully fixed in #3916. After this Instruction::Constrain will be defined to only work on primitive values - either primitive types directly or a predicate for more complex types. An unary constrain instruction can't protect against it holding a ValueId which doesn't correspond to a boolean value any more than a boolean constrain can however.

I don't believe that the optimizations in #3708 are unnecessary if we want to maintain performance. If constrains are going to be working on predicate values then we need to be able to work backwards to build the actual set of constraints which the predicate encodes.

We then could switch to an unary constrain instruction but it has a number of downsides:

1. A unary constrain would slow down SSA
   • The construct Constrain(lhs, rhs) would have to turn into Constrain(Not(Eq(lhs, rhs))). This has the knock-on effect of slowing down the SSA passes due to the number of new instructions.
2. A boolean constraints are easier to decompose into simpler constraints.
   • The less expressive form of the constrain instruction adds some hurdles to decomposing constraints as done in #3892. Rather than being able to just return a new list of constraints and insert them all at once, we'd need to insert extra instructions to calculate the values being constrained and then use the results from this in our new constraints.
3. A boolean constraint makes it easier to inline the constrained value elsewhere in the program.
   • See https://github.com/noir-lang/noir/pull/3708#issuecomment-1852323673
4. Boolean constrains are easier to reason about.
   • Personally I find it much easier to reason about Constrain(lhs, rhs) vs Constrain(Not(Eq(lhs, rhs))) and it results in a much more readable SSA.

[TomAFrench]

To ensure the generated Acir is just as efficient, when converting the new constrain to acir we can check if its argument is an equality node and if so keep the current codepath for an equality constraint.

I'm not a fan of this solution as we'd need to perform look-ahead behaviour as otherwise the ACIR for the equality predicate will already have been generated.

[TomAFrench]

Should we keep this open @jfecher?

[jfecher]

@TomAFrench yes, I still think this could be an improvement. We can explore it later when we focus on code quality & documentation before 1.0