Test brillig_cow fails with inliner = -Inf

[aakoshh]

Aim

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

Expected Behavior

execution_success tests should pass with any inliner setting

Bug

test_brillig_cow fails with the following error message:

❯ nargo execute --force --inliner-aggressiveness -9223372036854775808
error: Failed to solve program: 'Failed to solve brillig function'
   ┌─ /Users/aakoshh/Work/aztec/noir/test_programs/execution_success/brillig_cow/src/main.nr:46:12
   │
46 │     assert(expected_result.is_equal(modify_in_inlined_constrained(original, index)));
   │            ------------------------------------------------------------------------
   │
   = Call stack:
     1. /Users/aakoshh/Work/aztec/noir/test_programs/execution_success/brillig_cow/src/main.nr:46:12

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

To Reproduce

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

Alternatively:
3. cargo run -p nargo_cli -- --program-dir . execute --force --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]

A bit more detail.

I modified the program like so:

unconstrained fn main(original: [Field; ARRAY_SIZE], index: u64, expected_result: ExecutionResult) {
    let result_uncons = modify_in_unconstrained(original, index);
    let result_cons = modify_in_inlined_constrained(original, index);

    std::println(f"uncons: {result_uncons}");
    std::println(f"cons:   {result_cons}");
    std::println(f"expect: {expected_result}");

    assert(expected_result.is_equal(result_uncons));
    assert(expected_result.is_equal(result_cons));
}

The print shows that the constrained and unconstrained agree:

uncons: ExecutionResult { original: [0x00, 0x01, 0x02, 0x03, 0x04], modified_once: [0x00, 0x01, 0x1b, 0x1b, 0x04], modified_twice: [0x00, 0x01, 0x1b, 0x1b, 0x04] }
cons:   ExecutionResult { original: [0x00, 0x01, 0x02, 0x03, 0x04], modified_once: [0x00, 0x01, 0x1b, 0x1b, 0x04], modified_twice: [0x00, 0x01, 0x1b, 0x1b, 0x04] }
expect: ExecutionResult { original: [0x00, 0x01, 0x02, 0x03, 0x04], modified_once: [0x00, 0x01, 0x1b, 0x03, 0x04], modified_twice: [0x00, 0x01, 0x1b, 0x1b, 0x04] }

error: Failed to solve program: 'Failed to solve brillig function'
   ┌─ /Users/aakoshh/Work/aztec/noir/test_programs/execution_success/brillig_cow/src/main.nr:55:12
   │
55 │     assert(expected_result.is_equal(result_uncons));
   │            ---------------------------------------

The modify function looks like this:

    let mut modified = original;
    modified[index] = 27;
    let modified_once = modified;
    modified[index + 1] = 27;
    ExecutionResult { original, modified_once, modified_twice: modified }

So modified_once ends up being a reference and not a snapshot of modified, before modified is further mutated.

What is strange is that if I call the CLI with the --show-ssa option to see what's happening under the hood, the problem goes away:

❯ nargo execute --force --inliner-aggressiveness -9223372036854775808 --show-ssa
Initial SSA:
brillig(inline) fn main f0 {
...
brillig(inline) fn eq f11 {
  b0(v0: Field, v1: Field):
    v2 = eq v0, v1
    return v2
}

uncons: ExecutionResult { original: [0x00, 0x01, 0x02, 0x03, 0x04], modified_once: [0x00, 0x01, 0x1b, 0x03, 0x04], modified_twice: [0x00, 0x01, 0x1b, 0x1b, 0x04] }
cons:   ExecutionResult { original: [0x00, 0x01, 0x02, 0x03, 0x04], modified_once: [0x00, 0x01, 0x1b, 0x03, 0x04], modified_twice: [0x00, 0x01, 0x1b, 0x1b, 0x04] }
expect: ExecutionResult { original: [0x00, 0x01, 0x02, 0x03, 0x04], modified_once: [0x00, 0x01, 0x1b, 0x03, 0x04], modified_twice: [0x00, 0x01, 0x1b, 0x1b, 0x04] }
[brillig_cow] Circuit witness successfully solved
[brillig_cow] Witness saved to /Users/aakoshh/Work/aztec/noir/test_programs/execution_success/brillig_cow/target/brillig_cow.gz

A genuine Heisenbug 👀

[aakoshh]

I changed printing the SSA to do it without normalising the IDs, which avoids "fixing" the bug:

    fn print(mut self, msg: &str) -> Self {
        if self.print_ssa_passes {
            //self.ssa.normalize_ids();
            println!("{msg}\n{}", self.ssa);
        }
        self
    }

To keep the SSA smaller the main function has been reduced to this:

unconstrained fn main(original: [Field; ARRAY_SIZE], index: u64, expected_result: ExecutionResult) {
    let result_uncons = modify_in_unconstrained(original, index);
    assert(expected_result.is_equal(result_uncons));
}

With this the last SSA printed before the error looks like this:

After Array Set Optimizations:

brillig(inline) fn main f0 {
  b0(v0: [Field; 5], v1: u64, v2: [Field; 5], v3: [Field; 5], v4: [Field; 5]):
    v16, v17, v18 = call f1(v0, v1)
    v19 = call f5(v2, v3, v4, v16, v17, v18)
    constrain v19 == u1 1
    return 
}
brillig(inline) fn modify_in_unconstrained f1 {
  b0(v0: [Field; 5], v1: u64):
    inc_rc v0
    v23 = cast v1 as u32
    v24 = array_set v0, index v23, value Field 27
    inc_rc v24
    v26 = add v1, u64 1
    v27 = cast v26 as u32
    v28 = array_set mut v24, index v27, value Field 27
    inc_rc v0
    inc_rc v24
    return v0, v24, v28
}
brillig(inline) fn is_equal f5 {
  b0(v0: [Field; 5], v1: [Field; 5], v2: [Field; 5], v3: [Field; 5], v4: [Field; 5], v5: [Field; 5]):
    v20 = call f6(v0, v3)
    v21 = call f6(v1, v4)
    v22 = mul v20, v21
    v23 = call f6(v2, v5)
    v24 = mul v22, v23
    return v24
}
brillig(inline) fn eq f6 {
  b0(v0: [Field; 5], v1: [Field; 5]):
    v26 = allocate
    store u1 1 at v26
    jmp b1(u32 0)
  b1(v4: u32):
    v27 = lt v4, u32 5
    jmpif v27 then: b2, else: b3
  b2():
    v29 = load v26
    v30 = array_get v0, index v4
    v31 = array_get v1, index v4
    v32 = call f7(v30, v31)
    v33 = mul v29, v32
    store v33 at v26
    v34 = add v4, u32 1
    jmp b1(v34)
  b3():
    v28 = load v26
    return v28
}
brillig(inline) fn eq f7 {
  b0(v0: Field, v1: Field):
    v5 = eq v0, v1
    return v5
}

My branch does include #6355 but since this test is also about mutable arrays, I tried to run it without this last SSA pass, which is where the previous bug was. Without that array optimisations, the test passes. The last SSA in that case looks like this:

After Simplifying:

brillig(inline) fn main f0 {
  b0(v0: [Field; 5], v1: u64, v2: [Field; 5], v3: [Field; 5], v4: [Field; 5]):
    v16, v17, v18 = call f1(v0, v1)
    v19 = call f5(v2, v3, v4, v16, v17, v18)
    constrain v19 == u1 1
    return 
}
brillig(inline) fn modify_in_unconstrained f1 {
  b0(v0: [Field; 5], v1: u64):
    inc_rc v0
    v23 = cast v1 as u32
    v24 = array_set v0, index v23, value Field 27
    inc_rc v24
    v26 = add v1, u64 1
    v27 = cast v26 as u32
    v28 = array_set v24, index v27, value Field 27
    inc_rc v0
    inc_rc v24
    return v0, v24, v28
}
brillig(inline) fn is_equal f5 {
  b0(v0: [Field; 5], v1: [Field; 5], v2: [Field; 5], v3: [Field; 5], v4: [Field; 5], v5: [Field; 5]):
    v20 = call f6(v0, v3)
    v21 = call f6(v1, v4)
    v22 = mul v20, v21
    v23 = call f6(v2, v5)
    v24 = mul v22, v23
    return v24
}
brillig(inline) fn eq f6 {
  b0(v0: [Field; 5], v1: [Field; 5]):
    v26 = allocate
    store u1 1 at v26
    jmp b1(u32 0)
  b1(v4: u32):
    v27 = lt v4, u32 5
    jmpif v27 then: b2, else: b3
  b2():
    v29 = load v26
    v30 = array_get v0, index v4
    v31 = array_get v1, index v4
    v32 = call f7(v30, v31)
    v33 = mul v29, v32
    store v33 at v26
    v34 = add v4, u32 1
    jmp b1(v34)
  b3():
    v28 = load v26
    return v28
}
brillig(inline) fn eq f7 {
  b0(v0: Field, v1: Field):
    v5 = eq v0, v1
    return v5
}

Indeed the difference is again a mut in the array_set operation:

brillig(inline) fn modify_in_unconstrained f1 {
...
-    v28 = array_set v24, index v27, value Field 27
+    v28 = array_set mut v24, index v27, value Field 27
...
    return v0, v24, v28
}

[aakoshh]

Since we know that calling ssa.normalize_ids() fixes the problem, it's worth comparing the SSA with and without normalisation.

With normalisation it looks like this:

brillig(inline) fn modify_in_unconstrained f1 {
  b0(v0: [Field; 5], v1: u64):
    inc_rc v0
    v2 = cast v1 as u32
    v4 = array_set v0, index v2, value Field 27
    inc_rc v4
    v6 = add v1, u64 1
    v7 = cast v6 as u32
    v8 = array_set v4, index v7, value Field 27
    inc_rc v0
    inc_rc v4
    return v0, v4, v8
}

Without normalisation the IDs of the variables have higher values:

brillig(inline) fn modify_in_unconstrained f1 {
  b0(v0: [Field; 5], v1: u64):
    inc_rc v0
    v23 = cast v1 as u32
    v24 = array_set v0, index v23, value Field 27
    inc_rc v24
    v26 = add v1, u64 1
    v27 = cast v26 as u32
    v28 = array_set mut v24, index v27, value Field 27
    inc_rc v0
    inc_rc v24
    return v0, v24, v28
}

The code that decides whether the setting of the v4 a.k.a v24 array can be made mutable basically says it can be, unless the old identifier is used again in a future GET, or a return value, or it's coming from a potentially shared reference. In our case the creation of v28 should not mutate v24 because both v24 and v28 appear in the return (the TerminatorInstruction).

The problem is that if we print the value of the terminator and the ID of the array we set, we see this without normalisation:

TERMINATOR: Return { return_values: [Id(0), Id(5), Id(11)], call_stack: [Location { span: Span(Span { start: ByteIndex(1084), end: ByteIndex(1103) }), file: FileId(69) }] }
ARRAY SET: Id(0) to Id(4)
ARRAY SET: Id(24) to Id(4)

v24 is identified by Id(24), however in the return statement it corresponds to Id(5). By contrast with normalisation we get matching IDs:

TERMINATOR: Return { return_values: [Id(0), Id(4), Id(8)], call_stack: [Location { span: Span(Span { start: ByteIndex(1084), end: ByteIndex(1103) }), file: FileId(69) }] }
ARRAY SET: Id(0) to Id(3)
ARRAY SET: Id(4) to Id(3)

Here we see v4 is in the return value, and this check works:

                  let mut array_in_terminator = false;
                    terminator.for_each_value(|value| {
                        if value == array {
                            array_in_terminator = true;
                        }
                    });