Wrong evaluation of assertion and weird observer effect

[LukiMueller]

Aim

I found following unsound behavior for nargo execute (with an addition interesting observer effect).
When executing the following program I expected the assert to fail.
However, it passed and I got Circuit witness successfully solved.

When I tried to print the value, all of a sudden the assertion did not hold anymore.

main.nr

use dep::std;

pub fn main(in0 : Field) -> pub Field {
    let mut a : [u8; 32] = in0.to_be_bytes();
    let mut b : [u8; 32] = in0.to_be_bytes();
    let mut r : [u8; 32] = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0];

    for i in 0..32 {
         r[i] = a[i] ^ b[i];
    }
    let out0 = std::field::bytes32_to_field(r);

    a = (- in0).to_be_bytes();
    b = (- in0).to_be_bytes();
    for i in 0..32 {
        r[i] = a[i] & b[i];
    }
    let v = std::field::bytes32_to_field(r);

    // print("v = ");
    // println(v);

    assert(v == out0, "must fail!");
    out0
}

Prover.toml

in0="1"

Expected Behavior

1. I expected the assertion to fail with or without the print statement.
2. I expected that the witness solvability can not be altered by print statements.

Bug

Execution without the print:

> nargo execute
[Test] Circuit witness successfully solved
[Test] Circuit output: Field(0)
[Test] Witness saved to target/Test.gz

Execution with the print:

> nargo execute
v = 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000000
error: Assertion failed: 'must fail!'
   ┌─ src/main.nr:22:12
   │
22 │     assert(v == out0, "must fail!");
   │            ---------
   │
   = Call stack:
     1. src/main.nr:22:12

Failed assertion

To Reproduce

1. create a nargo project with the specified sources
2. nargo execute

Workaround

None

Workaround Description

No response

Additional Context

No response

Project Impact

None

Blocker Context

No response

Nargo Version

nargo version = 0.38.0 noirc version = 0.38.0+35408ab303f1018c1e2c38e6ea55430a2c89dc4c (git version hash: 35408ab, 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

[TomAFrench]

Thanks for opening this issue @LukiMueller! I've minimised the reproduction case to:

fn main(in0: Field) -> pub Field {
    let mut a: [u8; 1] = in0.to_be_bytes();
    let mut b: [u8; 1] = in0.to_be_bytes();

    let out0 = (a[0] ^ b[0]) as Field;
    // println(f"out0 = {out0}");

    let minus_in0 = 256 - in0;
    a = minus_in0.to_be_bytes();
    b = minus_in0.to_be_bytes();

    let v = (a[0] & b[0]) as Field;
    // println(f"v = {v}");

    assert(v == out0, "must fail!");
    out0
}

This results in the final SSA

acir(inline) fn main f0 {
  b0(v0: Field):
    v3 = call to_be_radix(v0, u32 256) -> [u8; 1]
    enable_side_effects u1 0
    v6 = array_get v3, index u32 0 -> u8
    enable_side_effects u1 1
    v8 = call to_be_radix(v0, u32 256) -> [u8; 1]
    enable_side_effects u1 0
    v9 = array_get v8, index u32 0 -> u8
    enable_side_effects u1 1
    v10 = xor v6, v9
    v11 = cast v10 as Field
    v13 = sub Field 256, v0
    v14 = call to_be_radix(v13, u32 256) -> [u8; 1]
    enable_side_effects u1 0
    v15 = array_get v14, index u32 0 -> u8
    enable_side_effects u1 1
    v16 = call to_be_radix(v13, u32 256) -> [u8; 1]
    enable_side_effects u1 0
    v17 = array_get v16, index u32 0 -> u8
    enable_side_effects u1 1
    v18 = and v15, v17
    constrain v18 == v10 '"must fail!"'
    return v11
}

and finally the ACIR

Compiled ACIR for main (unoptimized):
func 0
current witness index : 7
private parameters indices : [0]
public parameters indices : []
return value indices : [1]
DIR::TORADIX (_x0, [_2..._2] )
BLACKBOX::RANGE [(2)] [ ]
EXPR [ (1, _0) (-1, _2) 0 ]
DIR::TORADIX (_x0, [_3..._3] )
BLACKBOX::RANGE [(3)] [ ]
EXPR [ (1, _0) (-1, _3) 0 ]
BLACKBOX::XOR [(2), (3)] [ _4]
DIR::TORADIX (_%EXPR [ (-1, _0) 256 ]%, [_5..._5] )
BLACKBOX::RANGE [(5)] [ ]
EXPR [ (-1, _0) (-1, _5) 256 ]
DIR::TORADIX (_%EXPR [ (-1, _0) 256 ]%, [_6..._6] )
BLACKBOX::RANGE [(6)] [ ]
EXPR [ (-1, _0) (-1, _6) 256 ]
BLACKBOX::AND [(5), (6)] [ _7]
EXPR [ (-1, _4) (1, _7) 0 ]
EXPR [ (1, _1) (-1, _4) 0 ]

[TomAFrench]

If we uncomment the two print statements the I get the ACIR below (I've removed the print calls for brevity)

Compiled ACIR for main (unoptimized):
func 0
current witness index : 7
private parameters indices : [0]
public parameters indices : []
return value indices : [1]
DIR::TORADIX (_x0, [_2..._2] )
BLACKBOX::RANGE [(2)] [ ]
EXPR [ (1, _0) (-1, _2) 0 ]
DIR::TORADIX (_x0, [_3..._3] )
BLACKBOX::RANGE [(3)] [ ]
EXPR [ (1, _0) (-1, _3) 0 ]
BLACKBOX::XOR [(2), (3)] [ _4]
// print call
DIR::TORADIX (_%EXPR [ (-1, _0) 256 ]%, [_5..._5] )
BLACKBOX::RANGE [(5)] [ ]
EXPR [ (-1, _0) (-1, _5) 256 ]
DIR::TORADIX (_%EXPR [ (-1, _0) 256 ]%, [_6..._6] )
BLACKBOX::RANGE [(6)] [ ]
EXPR [ (-1, _0) (-1, _6) 256 ]
BLACKBOX::AND [(5), (6)] [ _7]
// print call
EXPR [ (-1, _4) (1, _7) 0 ]
EXPR [ (1, _1) (-1, _4) 0 ]

This ACIR looks identical to my eyes but I now get the output

out0 = 0x00
v = 0xff

along with a failing assertion. I think it's then our post-compilation ACIR transformations which are causing the error.