fix: 9_conditional end to end test

[kevaundray]

Description

Resolves #1802

Problem*

Resolves

Summary*

Documentation

• This PR requires documentation updates when merged.

  • I will submit a noir-lang/docs PR.
  • I will request for and support Dev Rel's help in documenting this PR.

Additional Context

PR Checklist*

• I have tested the changes locally.
• I have formatted the changes with Prettier and/or cargo fmt on default settings.

[kevaundray]

The above is the new error that we get due to the else branch being taken, even though a == 0

[kevaundray]

minimal circuit to reproduce:

use dep::std;



fn main(a: u32) -> pub u32{
    if a == 0 {
        3
    } else {
        1 / a
    }
}

When a == 0, we are getting a constraint failed for 1/a which should not be triggering.

[kevaundray]

checking euclidean division, the predicate is 1 (constant) which triggers the subsequent constraints.

The ssa is:

After Dead Instruction Elimination:
acir fn main f1 {
  b0(v0: u32):
    v16 = eq v0, u32 0
    enable_side_effects v16
    v17 = not v16
    enable_side_effects v17
    v18 = div u32 1, v0
    enable_side_effects u1 1
    v19 = cast v16 as u32
    v20 = cast v17 as u32
    v21 = mul v19, u32 3
    v22 = mul v20, v18
    v23 = add v21, v22
    return v23
}

Which means that the predicate should not be a constant for division. The error can then be seen in euclidean_division_var with let predicate = Expression::one();

[kevaundray]

New error is because we are multiplying two Expressions which should be Linear expressions, but they are not -- we will need to reduce the lhs and rhs before multiplying

[kevaundray]

New minimal reproducable error is now:

use dep::std;

fn main(a: u32){
    if a == 0 {
  
    } else{
        let f1 = a as Field;
        assert(10/f1 == 0);
    }
}

10/f1 is failing with constraint failed -- implying that even though a == 0, the else branch is not being handled correctly

SSA for this is:

After Dead Instruction Elimination:
acir fn main f1 {
  b0(v0: u32):
    v16 = eq v0, u32 0
    enable_side_effects v16
    v17 = not v16
    enable_side_effects v17
    v18 = cast v0 as Field
    v19 = div Field 10, v18
    v20 = eq v19, Field 0
    v21 = mul v20, v17
    v22 = eq v21, v17
    constrain v22
    enable_side_effects u1 1
    return 
}

Noting that:

    enable_side_effects v16
    v17 = not v16
    enable_side_effects v17

Is somewhat confusing to read in the case that v16 is not enabled

[kevaundray]

The problem; inv_var unconditionally asserts that the result has an inverse, so for the case of 1, it will always fail

[kevaundray]

A bigger refactor will be needed to remove the idea of an optional predicate. Since Option is a compile time known concept, this implies that predicates are known at compile time which is not correct.

Another problem with Option or Option is that its not quite clear as to why/if None is different to Some(Expression::zero()).

[kevaundray]

Blocking this PR until the issue above is created for Option<Expression/AcirVar>

[jfecher]

Blocking this PR until the issue above is created for Option<Expression/AcirVar>

Created #1972

[kevaundray]

Blocking this PR until the issue above is created for Option<Expression/AcirVar>

Created #1972

Thanks @jfecher!

[kevaundray]

@guipublic spoke offline, though could you give an official approval? @jfecher pinging for comments!

[jfecher]

LGTM