Test slice_dynamic_index fails with inliner = -Inf and brillig

[aakoshh]

Aim

Trying to run test_programs with different --inliner-aggressiveness in #6429

Expected Behavior

Tests under execution_success should work.

Bug

❯ nargo execute --force --inliner-aggressiveness -9223372036854775808 --force-brillig
error: Failed to solve program: 'Failed to solve brillig function'
   ┌─ /Users/aakoshh/Work/aztec/noir/test_programs/execution_success/slice_dynamic_index/src/main.nr:47:12
   │
47 │     assert(slice[y] == 1);
   │            -------------
   │
   = Call stack:
     1. /Users/aakoshh/Work/aztec/noir/test_programs/execution_success/slice_dynamic_index/src/main.nr:3:5
     2. /Users/aakoshh/Work/aztec/noir/test_programs/execution_success/slice_dynamic_index/src/main.nr:14:5
     3. /Users/aakoshh/Work/aztec/noir/test_programs/execution_success/slice_dynamic_index/src/main.nr:47:12

Failed to solve program: 'Failed to solve brillig function'

To Reproduce

1. cd test_programs/execution_success/slice_dynamic_index
2. nargo execute --force --force-brillig --inliner-aggressiveness -9223372036854775808

Workaround

None

Workaround Description

No response

Additional Context

No response

Project Impact

None

Blocker Context

No response

Nargo Version

nargo version = 0.36.0 noirc version = 0.36.0+2f0cb3e80f3d93a1dee77fffacc397811e300257 (git version hash: 2f0cb3e, is dirty: false)

NoirJS Version

No response

Proving Backend Tooling & Version

No response

Would you like to submit a PR for this Issue?

None

Support Needs

No response

[aakoshh]

Reduced the program to bring out the problem to this:

fn main(x: Field) {
    // The parameters to this function must come directly from witness values (inputs to main).
    regression_dynamic_slice_index(x - 1, x - 4);
}

fn regression_dynamic_slice_index(x: Field, y: Field) {
    let mut slice = &[];
    for i in 0..5 {
        slice = slice.push_back(i as Field);
    }
    assert(slice.len() == 5);

    dynamic_slice_index_set_if(slice, x, y);
    dynamic_slice_index_set_else(slice, x, y);
}

fn dynamic_slice_index_set_if(mut slice: [Field], x: Field, y: Field) {
    slice[y] = 0;
    assert(slice[y] == 0);
    assert(slice[x] == 4);
}

fn dynamic_slice_index_set_else(mut slice: [Field], x: Field, y: Field) {
    assert(slice[x] == 4);
    assert(slice[y] == 1);
    if x as u32 > 10 {
        slice[x] = slice[x] - 2;
        slice[x - 1] = slice[x];
    } else {
        slice[x] = 0;
    }
    assert(slice[4] == 0);
}

It looks like the second function expects that slice is unchanged, but it's not, it carries the changes done by the first:

❯ cargo run -q -p nargo_cli --  --program-dir . execute --force --force-brillig --inliner-aggressiveness -9223372036854775808
error: Failed to solve program: 'Failed to solve brillig function'
   ┌─ /Users/aakoshh/Work/aztec/noir/test_programs/execution_success/slice_dynamic_index/src/main.nr:25:12
   │
25 │     assert(slice[y] == 1);
   │            -------------
   │
   = Call stack:
     1. /Users/aakoshh/Work/aztec/noir/test_programs/execution_success/slice_dynamic_index/src/main.nr:3:5
     2. /Users/aakoshh/Work/aztec/noir/test_programs/execution_success/slice_dynamic_index/src/main.nr:14:5
     3. /Users/aakoshh/Work/aztec/noir/test_programs/execution_success/slice_dynamic_index/src/main.nr:25:12

Failed to solve program: 'Failed to solve brillig function'

If we run it with --inliner-aggressiveness 0 it passes, but removing almost any line from either methods it fail the same way.

[aakoshh]

The SSA for the failing case with inliner = -Inf looks as follows

After Array Set Optimizations:

brillig(inline) fn main f0 {
  b0(v0: Field):
    v2 = sub v0, Field 1
    v4 = sub v0, Field 4
    call f1(v2, v4)
    return 
}
brillig(inline) fn regression_dynamic_slice_index f1 {
  b0(v0: Field, v1: Field):
    v3 = allocate
    store u32 0 at v3
    inc_rc []
    v6 = allocate
    store [] at v6
    jmp b1(u32 0)
  b1(v2: u32):
    v8 = lt v2, u32 5
    jmpif v8 then: b3, else: b2
  b3():
    v16 = load v3
    v17 = load v6
    v18 = cast v2 as Field
    v20, v21 = call slice_push_back(v16, v17, v18)
    inc_rc v21
    store v20 at v3
    store v21 at v6
    v23 = add v2, u32 1
    jmp b1(v23)
  b2():
    v9 = load v3
    constrain v9 == u32 5
    v10 = load v3
    v11 = load v6
    call f2(v10, v11, v0, v1)
    v13 = load v3
    v14 = load v6
    call f3(v13, v14, v0, v1)
    return 
}
brillig(inline) fn dynamic_slice_index_set_if f2 {
  b0(v0: u32, v1: [Field], v2: Field, v3: Field):
    inc_rc v1
    v4 = cast v3 as u32
    v6 = array_set mut v1, index v4, value Field 0
    v7 = lt v4, v0
    constrain v7 == u1 1 '"Index out of bounds"'
    v9 = array_get v6, index v4
    constrain v9 == Field 0
    v10 = cast v2 as u32
    v11 = lt v10, v0
    constrain v11 == u1 1 '"Index out of bounds"'
    v12 = array_get v6, index v10
    constrain v12 == Field 4
    dec_rc v1
    return 
}
brillig(inline) fn dynamic_slice_index_set_else f3 {
  b0(v0: u32, v1: [Field], v2: Field, v3: Field):
    v4 = allocate
    store v1 at v4
    inc_rc v1
    v5 = cast v2 as u32
    v6 = lt v5, v0
    constrain v6 == u1 1 '"Index out of bounds"'
    v8 = array_get v1, index v5
    constrain v8 == Field 4
    v10 = cast v3 as u32
    v11 = lt v10, v0
    constrain v11 == u1 1 '"Index out of bounds"'
    v12 = array_get v1, index v10
    constrain v12 == Field 1
    v14 = truncate v2 to 32 bits, max_bit_size: 254
    v15 = cast v14 as u32
    v17 = lt u32 10, v15
    jmpif v17 then: b2, else: b1
  b2():
    v21 = cast v2 as u32
    v22 = lt v21, v0
    constrain v22 == u1 1 '"Index out of bounds"'
    v23 = array_get v1, index v21
    v25 = sub v23, Field 2
    v26 = array_set mut v1, index v21, value v25
    v27 = sub v2, Field 1
    v28 = array_get v26, index v21
    v29 = cast v27 as u32
    v30 = array_set mut v26, index v29, value v28
    store v30 at v4
    jmp b3()
  b3():
    v31 = load v4
    v33 = lt u32 4, v0
    constrain v33 == u1 1 '"Index out of bounds"'
    v34 = array_get v31, index u32 4
    constrain v34 == Field 0
    dec_rc v1
    return 
  b1():
    v18 = cast v2 as u32
    v20 = array_set v1, index v18, value Field 0
    store v20 at v4
    jmp b3()
}

The problem is similar to #6349

In the comments Alvaro noted that:

As you can see in fn push, it's using array_set mut, which ignores reference counters, so it's mutating [Field 0, Field 0, Field 0] which is shared in two variables (if it wasn't mut, it would work correctly, since its reference counter is correct, 2)

Similarly here we have:

brillig(inline) fn dynamic_slice_index_set_if f2 {
  b0(v0: u32, v1: [Field], v2: Field, v3: Field):
    inc_rc v1
    v4 = cast v3 as u32
    v6 = array_set mut v1, index v4, value Field 0

My interpretation is that the shared slice v1 for which we increased the ref counter is mutated, where it shouldn't be.