Prover fails to identify constraints aren't met

[joss-aztec]

Description

Aim

To see that the prover throws an error when trying to prove over unmet constraints.

Expected behavior

This program should fail to prove, but it in fact succeeds (though the result is invalid):

fn main(xs : [u32; 4], y : pub u32) {
    let mut x_total: u32 = 0;
    for i in 0..4 {
      let x = xs[i];
      x_total = x_total + x;
    };
    constrain x_total <= y;
}
// Prover.toml
xs = ["10","0","0","0"]
y = "1"

However, if I then decrease the array length from 4 to 3 to correctly fails

fn main(xs : [u32; 3], y : pub u32) {
    let mut x_total: u32 = 0;
    for i in 0..3 {
      let x = xs[i];
      x_total = x_total + x;
    };
    constrain x_total <= y;
}
// Prover.toml
xs = ["10","0","0"]
y = "1"

Bug

Screen.Recording.2022-11-29.at.11.03.13.mov

To reproduce

Follow above example

Environment

(Specify your setup and versions of dependencies.)

• OS: macOS 12.4 (Intel)

For nargo users

Whichever nargo build was available at https://github.com/kobyhallx/build-noir/suites/9553357751/artifacts/454490397

[guipublic]

I fixed it in PR #535, but I would like to refactor a bit after #520 is merged, so let's keep this one open until then.