Change Instruction::Constrain(lhs, rhs, msg) to Instruction::Constrain(bool, msg)
#3782
Comments
|
I've been doing some thinking on this and I don't think that it would be useful for us to make 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 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:
|
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. |
…straints (#3892) # Description ## Problem\* Some experimentation related to #3782. ## Summary\* If we switch to an unary constrain instruction then we will want to be able to decompose an assertion on a composite type to perform assertions directly on its fields. Otherwise we have to create a predicate for each field and then collect these all together before constraining that. For example consider this program which simulates an unary constrain ``` fn main(x: [Field; 2], y: [Field; 2]) { let equal = x == y; assert(equal); } ``` Currently this produces: ``` acir fn main f0 { b0(v0: [Field; 2], v1: [Field; 2]): v66 = array_get v0, index Field 0 v67 = array_get v1, index Field 0 v68 = eq v66, v67 v69 = array_get v0, index Field 1 v70 = array_get v1, index Field 1 v71 = eq v69, v70 v72 = mul v68, v71 constrain v72 == u1 1 return } Compiled ACIR for main (unoptimized): current witness index : 10 public parameters indices : [] return value indices : [] EXPR [ (-1, _1) (1, _3) (-1, _5) 0 ] BRILLIG: inputs: [Single(Expression { mul_terms: [], linear_combinations: [(1, Witness(5))], q_c: 0 })] outputs: [Simple(Witness(6))] [JumpIfNot { condition: RegisterIndex(0), location: 3 }, Const { destination: RegisterIndex(1), value: Value { inner: 1 } }, BinaryFieldOp { destination: RegisterIndex(0), op: Div, lhs: RegisterIndex(1), rhs: RegisterIndex(0) }, Stop] EXPR [ (1, _5, _6) (1, _7) -1 ] EXPR [ (1, _5, _7) 0 ] EXPR [ (-1, _2) (1, _4) (-1, _8) 0 ] BRILLIG: inputs: [Single(Expression { mul_terms: [], linear_combinations: [(1, Witness(8))], q_c: 0 })] outputs: [Simple(Witness(9))] [JumpIfNot { condition: RegisterIndex(0), location: 3 }, Const { destination: RegisterIndex(1), value: Value { inner: 1 } }, BinaryFieldOp { destination: RegisterIndex(0), op: Div, lhs: RegisterIndex(1), rhs: RegisterIndex(0) }, Stop] EXPR [ (1, _8, _9) (1, _10) -1 ] EXPR [ (1, _8, _10) 0 ] EXPR [ (1, _7, _10) -1 ] ``` After this PR we can recover the current optimisations for `assert(x == y)` ``` acir fn main f0 { b0(v0: [Field; 2], v1: [Field; 2]): v66 = array_get v0, index Field 0 v67 = array_get v1, index Field 0 v68 = array_get v0, index Field 1 v69 = array_get v1, index Field 1 constrain v66 == v67 constrain v68 == v69 return } Compiled ACIR for main (unoptimized): current witness index : 4 public parameters indices : [] return value indices : [] EXPR [ (1, _1) (-1, _3) 0 ] EXPR [ (1, _2) (-1, _4) 0 ] ``` ## Additional Context ## Documentation\* Check one: - [ ] No documentation needed. - [ ] Documentation included in this PR. - [ ] **[Exceptional Case]** Documentation to be submitted in a separate PR. # PR Checklist\* - [ ] I have tested the changes locally. - [ ] I have formatted the changes with [Prettier](https://prettier.io/) and/or `cargo fmt` on default settings. --------- Co-authored-by: jfecher <jake@aztecprotocol.com>
|
Should we keep this open @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 |
Problem
Including the equality as part of the constrain statement can lead to some missed bugs (#3740) and extra needed optimizations (#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::Constrainback 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== truelike 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
The text was updated successfully, but these errors were encountered: