feat: decompose Instruction::Constrain into multiple more basic constraints

[TomAFrench]

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 and/or cargo fmt on default settings.

[github-actions]

Changes to circuit sizes

Generated at commit: 01c01fc456913fe863967ed5df30d057ce604e85, compared to commit: cc3c2c22644f0b5d8369bad2362ea6e9112a0713

🧾 Summary (10% most significant diffs)

Program	ACIR opcodes (+/-)	%	Circuit size (+/-)	%
simple_2d_array	-7 ✅	-63.64%	-5 ✅	-35.71%
brillig_blake2s	-127 ✅	-64.47%	-95 ✅	-42.60%
brillig_sha256	-127 ✅	-66.15%	-95 ✅	-43.78%
array_eq	-127 ✅	-79.87%	-95 ✅	-71.97%

---

Full diff report 👇

Program	ACIR opcodes (+/-)	%	Circuit size (+/-)	%
6	70 (-127)	-64.47%	38,799 (0)	0.00%
7	70 (-127)	-64.47%	19,350 (0)	0.00%
blake3	70 (-127)	-64.47%	18,774 (0)	0.00%
conditional_regression_short_circuit	96 (-127)	-56.95%	38,799 (0)	0.00%
ecdsa_secp256k1	233 (-127)	-35.28%	41,049 (0)	0.00%
keccak256	76 (-127)	-62.56%	54,830 (0)	0.00%
regression	207 (-19)	-8.41%	4,130 (0)	0.00%
sha256	75 (-127)	-62.87%	38,799 (0)	0.00%
strings	69 (-49)	-41.53%	14,373 (0)	0.00%
sha2_byte	40,133 (-382)	-0.94%	154,258 (-286)	-0.19%
slice_struct_field	33,241 (-583)	-1.72%	104,584 (-424)	-0.40%
to_be_bytes	83 (0)	0.00%	167 (-1)	-0.60%
tuple_inputs	48 (-33)	-40.74%	3,678 (-24)	-0.65%
u128	857 (-43)	-4.78%	4,689 (-31)	-0.66%
nested_slice_dynamic	1,700 (-113)	-6.23%	12,548 (-83)	-0.66%
nested_array_dynamic	4,450 (-202)	-4.34%	13,845 (-151)	-1.08%
struct_inputs	27 (-48)	-64.00%	2,840 (-41)	-1.42%
brillig_keccak	132 (-127)	-49.03%	3,062 (-95)	-3.01%
bit_and	24 (-28)	-53.85%	4,106 (-374)	-8.35%
simple_2d_array	4 (-7)	-63.64%	9 (-5)	-35.71%
brillig_blake2s	70 (-127)	-64.47%	128 (-95)	-42.60%
brillig_sha256	65 (-127)	-66.15%	122 (-95)	-43.78%
array_eq	32 (-127)	-79.87%	37 (-95)	-71.97%

[TomAFrench]

One trouble I'm running into is that we can only propagate the simplification back one level per constant folding pass. In general we need to be able to propagate back simplifications as many levels as there are fields in the type being constrained.

We could just rerun the constant folding pass until it stabilises but that's slow and can result in memory issues. One solution that seems plausible is recursively inspect all of the precursor instructions to the Constrain to build up a full list of requirements, generate all of the primitive Constrains which made up the original and then rely on DIE to clean up everything. We may need some special sauce to apply the constrained values within a "side-effect-enabled block" to do this satisfactorily however.

[TomAFrench]

The increase in constraints for to_be_bytes comes from the fact that we now take the snippet

if (bytes[30] != 60) | (bytes[29] != 33) | (bytes[28] != 31) {
    assert(false);
}

which has the SSA

v679 = array_get v621, index u64 28
v680 = lt u64 29, v620
constrain v680 == u1 1 'Index out of bounds'
v681 = array_get v621, index u64 29
v682 = lt u64 30, v620
constrain v682 == u1 1 'Index out of bounds'
v683 = array_get v621, index u64 30
v684 = eq v683, u8 60
v685 = not v684
v686 = eq v681, u8 33
v687 = not v686
v688 = or v685, v687
v689 = eq v679, u8 31
v690 = not v689
v691 = or v688, v690
enable_side_effects v691
constrain u1 0 == v691
enable_side_effects u1 1

And seeing that this is equivalent to constraining the values used to calculate v691 such that we never enter that if-branch.

v681 = array_get v621, index u64 29
v682 = lt u64 30, v620
constrain v682 == u1 1 'Index out of bounds'
v683 = array_get v621, index u64 30
v684 = eq v683, u8 60
v685 = not v684
v686 = eq v681, u8 33
v687 = not v686
v688 = or v685, v687
v689 = eq v679, u8 31
v690 = not v689
v691 = or v688, v690
enable_side_effects v691
constrain v683 == u8 60
constrain v681 == u8 33
constrain v679 == u8 31
enable_side_effects u1 1

We should be able to remove v684-v691 with DIE but the enable_side_effects instruction prevents this, we could get around this with a pass which removes these instructions if they're not followed by another instructions which uses the condition value before the next enable_side_effects instruction We can't remove this cleanly but this is also a fairly non-idiomatic piece of noir code.

[TomAFrench]

cc @jfecher, do you have any issues with this PR in principle (thinking about how we're returning multiple instructions to insert)? I'll clean up the actual implementation and mark ready for review if not

[jfecher]

cc @jfecher, do you have any issues with this PR in principle (thinking about how we're returning multiple instructions to insert)? I'll clean up the actual implementation and mark ready for review if not

This PR is interesting and a good optimization if we can get it to work, but I worry that it will be obsolete once we have operator overloading for == and start disallowing primitive == on arrays which has always been broken (it does not check if the element type implements Eq). When array == becomes a normal function call this optimization becomes more difficult I think. That being said, if we could get it to work for all == method calls somehow, that'd be great.

[TomAFrench]

I worry that it will be obsolete once we have operator overloading for == and start disallowing primitive == on arrays which has always been broken (it does not check if the element type implements Eq). When array == becomes a normal function call this optimization becomes more difficult I think.

This should be fine as long as we are still in-lining the eq function in SSA. There's nothing tying this optimization to array equalities as they're currently performed, it's generic over any constraint so will work for arbitrary types including structs.

I've added an integration test to show this which compiles down to

Compiled ACIR for main (unoptimized):
current witness index : 5
public parameters indices : []
return value indices : []
EXPR [ (1, _2, _2) (-1, _2) 0 ]
BLACKBOX::RANGE [(_3, num_bits: 8)] [ ]
BLACKBOX::RANGE [(_4, num_bits: 8)] [ ]
BLACKBOX::RANGE [(_5, num_bits: 8)] [ ]
EXPR [ (1, _1) -42 ]
EXPR [ (1, _2) -1 ]
EXPR [ (1, _3) -1 ]
EXPR [ (1, _4) -2 ]
EXPR [ (1, _5) -3 ]

[TomAFrench]

@jfecher @kevaundray This should be good for a final review now.

[TomAFrench]

Bumping this.

[jfecher]

👍