ACIR != Brillig: ACIR prints result of overflow and fails on other constraint

[aakoshh]

Aim

Reproduce a nightly failure from https://github.com/noir-lang/noir/actions/runs/16559377316/job/46826043334

The following program fails correctly in Brillig and the SSA interpreter, but behaves in a strange way in ACIR:

global G_B: u64 = 2288862572;
fn main(a: u64) -> pub u64 {
    let b = a * 18259827970668162041_u64;
    println(f"b = {b}");
    assert(b == G_B, "YHV");
    b
}

Input:

a = "0x000000000000000000000000000000000000000000000000000000006f3c2bda"

Expected Behavior

They should agree on the outcome, which is an overflow in the multiplication.

Bug

❯ cargo run -q -p nargo_cli -- execute --force --silence-warnings 
b = 16372204933514773770
error: Assertion failed: YHV
  ┌─ src/main.nr:5:13
  │
5 │     assert(((b as u128) == (G_B as u128)), "YHV");
  │             ----------------------------
  │
  = Call stack:
    1. src/main.nr:5:13

Failed assertion

Note how it even printed the value of b. But if we comment out the assert, or run it with --force-brillig, we get a different failure:

❯ cargo run -q -p nargo_cli -- execute --force --silence-warnings --force-brillig
error: Assertion failed: attempt to multiply with overflow
  ┌─ src/main.nr:3:13
  │
3 │     let b = (a as u64) * 18259827970668162041_u64;
  │             -------------------------------------
  │
  = Call stack:
    1. src/main.nr:3:13

Failed assertion

I see nothing suspicious in the SSA:

After Initial SSA:
g0 = u64 2288862572

acir(inline) fn main f0 {
  b0(v1: u64):
    v3 = mul v1, u64 18259827970668162041         	// src/main.nr:3:13
    v9 = make_array b"b = {b}"                    	// src/main.nr:3:13
    call f1(v9, Field 1, v3)                      	// src/main.nr:4:5
    v12 = eq v3, u64 2288862572                   	// src/main.nr:5:12
    constrain v3 == u64 2288862572, "YHV"         	// src/main.nr:5:12
    return v3
}
acir(inline) fn println f1 {
  b0(v1: [u8; 7], v2: Field, v3: u64):
    call f2(u1 1, v1, v2, v3)                     	// std/lib.nr:40:9
    return
}
brillig(inline) fn print_unconstrained f2 {
  b0(v1: u1, v2: [u8; 7], v3: Field, v4: u64):
    v24 = make_array b"{\"kind\":\"unsignedinteger\",\"width\":64}"	// std/lib.nr:40:9
    call print(v1, v2, v3, v4, v24, u1 1)         	// std/lib.nr:34:5
    return
}

Since we can actually observe a different side effect (the print) in ACIR, we can't consider these equivalent failures.

To Reproduce

NOIR_AST_FUZZER_SEED=0x2422539c00100000 cargo test -q -p noir_ast_fuzzer_fuzz acir_vs_brillig

Workaround

None

Workaround Description

No response

Additional Context

No response

Project Impact

None

Blocker Context

No response

Nargo Version

nargo version = 1.0.0-beta.9 noirc version = 1.0.0-beta.9+e7fb7f3bf083de9fc6d430e7c30a571ea94534e4 (git version hash: e7fb7f3, is dirty: true)

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]

Here's the ACIR without the println but including the assert:

❯ cargo run -q -p nargo_cli -- compile --force --silence-warnings --show-ssa-pass Initial --print-acir
After Initial SSA:
g0 = u64 2288862572

acir(inline) fn main f0 {
  b0(v1: u64):
    v3 = mul v1, u64 18259827970668162041         	// src/main.nr:3:13
    v4 = eq v3, u64 2288862572                    	// src/main.nr:5:12
    constrain v3 == u64 2288862572, "YHV"         	// src/main.nr:5:12
    return v3
}

Compiled ACIR for main (unoptimized):
func 0
current witness index : _2
private parameters indices : [_0]
public parameters indices : []
return value indices : [_1]
BLACKBOX::RANGE [(_0, 64)] []
EXPR [ (18259827970668162041, _0) (-1, _2) 0 ]
EXPR [ (1, _2) -2288862572 ]
EXPR [ (1, _1) -2288862572 ]

And here it is with the assert removed as well:

❯ cargo run -q -p nargo_cli -- execute --force --silence-warnings --show-ssa-pass Initial --print-acir
After Initial SSA:
acir(inline) fn main f0 {
  b0(v0: u64):
    v2 = mul v0, u64 18259827970668162041         	// src/main.nr:3:13
    return v2
}

Compiled ACIR for main (unoptimized):
func 0
current witness index : _2
private parameters indices : [_0]
public parameters indices : []
return value indices : [_1]
BLACKBOX::RANGE [(_0, 64)] []
EXPR [ (18259827970668162041, _0) (-1, _2) 0 ]
BLACKBOX::RANGE [(_2, 64)] []
EXPR [ (1, _1) (-1, _2) 0 ]

For some reason the range constraint is not included when we have another constraint on the result of the multiplication.

This is what it looks like with both the println and assert:

Compiled ACIR for main (unoptimized):
func 0
current witness index : _2
private parameters indices : [_0]
public parameters indices : []
return value indices : [_1]
BLACKBOX::RANGE [(_0, 64)] []
EXPR [ (18259827970668162041, _0) (-1, _2) 0 ]
BRILLIG CALL func 0: inputs: [EXPR [ 1 ], [EXPR [ 98 ], EXPR [ 32 ], EXPR [ 61 ], EXPR [ 32 ], EXPR [ 123 ], EXPR [ 98 ], EXPR [ 125 ]], EXPR [ 1 ], EXPR [ (1, _2) 0 ]], outputs: []
EXPR [ (1, _2) -2288862572 ]
EXPR [ (1, _1) -2288862572 ]

And finally with println but no assert:

Compiled ACIR for main (unoptimized):
func 0
current witness index : _2
private parameters indices : [_0]
public parameters indices : []
return value indices : [_1]
BLACKBOX::RANGE [(_0, 64)] []
EXPR [ (18259827970668162041, _0) (-1, _2) 0 ]
BLACKBOX::RANGE [(_2, 64)] []
BRILLIG CALL func 0: inputs: [EXPR [ 1 ], [EXPR [ 98 ], EXPR [ 32 ], EXPR [ 61 ], EXPR [ 32 ], EXPR [ 123 ], EXPR [ 98 ], EXPR [ 125 ]], EXPR [ 1 ], EXPR [ (1, _2) 0 ]], outputs: []
EXPR [ (1, _1) (-1, _2) 0 ]