Over/underflow checks are performed in inactive conditional branches resulting in unwanted constraints

[TomAFrench]

Aim

Consider the program

fn main(x: u4) {
    if x == 10 {
        x + 15;
    }
}

Expected Behavior

We should expect that this program should execute correctly for x != 10 but fail in the case of x == 10 due to an overflow.

Bug

The ACIR generated for this program is as below (annotated)

Compiled ACIR for main (unoptimized):
current witness index : 5
public parameters indices : []
return value indices : []
BLACKBOX::RANGE [(_1, num_bits: 4)] [ ]

// Processing `if` condition.
EXPR [ (-1, _1) (-1, _2) 10 ]
BRILLIG: inputs: [Single(Expression { mul_terms: [], linear_combinations: [(1, Witness(2))], q_c: 0 })]
outputs: [Simple(Witness(3))]
[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, _2, _3) (1, _4) -1 ]
EXPR [ (1, _2, _4) 0 ]

// Addition inside the if statement.
EXPR [ (1, _1) (-1, _5) 15 ]
BLACKBOX::RANGE [(_5, num_bits: 4)] [ ]

We can see that we're not actually applying the condition to the addition which results in the range check failing due to an overflow in all cases.

The simplest solution to this is to just multiply the value being range checked by the condition which will turn off any under/overflow checks. The value which is being written to witness 5 will still be an invalid u32 but we won't use this outside of the conditional branch so this isn't important. This then gives the ACIR:

Compiled ACIR for main (unoptimized):
current witness index : 6
public parameters indices : []
return value indices : []
BLACKBOX::RANGE [(_1, num_bits: 4)] [ ]
EXPR [ (-1, _1) (-1, _2) 10 ]
BRILLIG: inputs: [Single(Expression { mul_terms: [], linear_combinations: [(1, Witness(2))], q_c: 0 })]
outputs: [Simple(Witness(3))]
[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, _2, _3) (1, _4) -1 ]
EXPR [ (1, _2, _4) 0 ]
EXPR [ (1, _1) (-1, _5) 15 ]
EXPR [ (1, _4, _5) (-1, _6) 0 ] // Application of condition
BLACKBOX::RANGE [(_6, num_bits: 4)] [ ]

We could potentially be a bit smarter about this in order to avoid unnecessary constraints but this is fine for the time being.

To Reproduce

nargo execute supplied program on master.

Installation Method

None

Nargo Version

No response

Additional Context

No response

Would you like to submit a PR for this Issue?

No

Support Needs

No response