Encode MemoryOp predicates in circuit

[vezenovm]

Problem

Reference this comment (noir-lang/acvm#503 (review)) for context.

In this PR (#2400) predicates were attached to Memory Ops to avoid unsatisfied constraints during execution. However, this is simply an execution change, and does not change the actual circuit at all.

Happy Case

Encode the predicate when using memory ops, so that we have different circuits for differing predicate values. I think ideally this would be done on the Noir side.

Alternatives Considered

It is also possible to leave the encoding of the predicate to the backend. However, this would require changes to bberg and other backends would have to implement similar encodings for memory ops.

Additional Context

No response

Would you like to submit a PR for this Issue?

No

Support Needs

No response

[vezenovm]

Summary from our call:
It should be possible to encode the predicate without a change to ACIR at all, and we can revert noir-lang/acvm#503.

For this example program:

if pred {
  x[idx] = 25;
}

We should be able to encode the memory write as such:

x[idx * pred] = pred * 25 + (1-pred)x[idx*pred];

If the predicate is false, this would simplify to x[0] = x[0] which is essentially just a no-op.

The main caveat here is that even with a false predicate we will have to make sure that we are not attempting to access the first element of an empty slice. The encoding above is fine for an array of length two, but if the array is length zero we will need an extra check as we will still get an index out of bounds.

So there are two tasks we need to complete:

1. Implement the idx*pred encoding
2. Prevent index out of bounds on length zero slices/arrays