incorrect inference from conditional assertion
Closed this issue ยท 3 comments
Aim
I run into an extremely confusing scenario in which the presence of assert_eq
statements seems to put the program in an inconsistent state in which variables are equal to multiple values at the same time, or have different values depending on how they are inspected.
Expected Behavior
The following example may seem a bit convoluted, but it originates from a legitimate use-case in the Aztec codebase, and it seems all of the elements present here are required to trigger the bug.
trait ToField {
fn to_field(self) -> Field;
}
impl ToField for bool { fn to_field(self) -> Field { self as Field } }
unconstrained fn get_unconstrained_option() -> Option<u32> {
Option::some(13)
}
unconstrained fn should_i_assert() -> bool {
false
}
fn get_magical_boolean() -> bool {
let option = get_unconstrained_option();
let pre_assert = option.is_some().to_field();
if should_i_assert() {
// Note that `should_i_assert` is unconstrained, so Noir should not be able to infer
// any behavior from the contents of this block. In this case it is actually false, so the
// assertion below is not even executed (if it did it'd fail since the values are not equal).
assert_eq(option, Option::some(42)); /// <- this seems to be the trigger for the bug
}
// In my testing, the `option` value exhibits weird behavior from this point on, as if it had been mutated
let post_assert = option.is_some().to_field();
// The following expression should be true, but I can get it to evaluate to false depending on how I call it
pre_assert == post_assert
}
#[test]
fn test() {
let magic = get_magical_boolean();
// One of these asserts should fail, but both pass.
assert_eq(magic, true);
assert_eq(magic, false);
}
As mentioned in the comments, nargo test
passes, so magic
is both true and false.
Bug
It took me a fair bit of effort to realize that this was a Noir issue, and then to further narrow down the issue to the code sample above. This was quite hard to analyse as it seems the results I get from testing depend on how I inspect the values. I'll share here some of my findings, hoping they might be useful to whomever looks into this.
The trigger for the weird behavior seems to be the assert_eq
statement. I don't think this is a red-herring: I did not find a single instance of strange behavior that did not include the assertion.
It looks like the presence of assert_eq
somehow confuses Noir when it comes to what the value of the thing being asserted is. Note that in my example option
is a some
value, I then do assert_eq
to a different some
value, and yet I later get that is_some
is not the same before and after the assert_eq
statement. In the example above I only produce a magic boolean that is both true and false, but in testing with extended infrastructure I got Noir to emit oracle calls in which pre_assert
is 1 (as expected) and post_assert
is 0. This is why I had to use to_field
: my logging function only receives fields.
Making the unconstrained functions constrained causes for the issue to not occur, so this must be somehow related.
I also noticed that performing boolean comparison instead of using to_field
seemingly causes the issue to go way, but I'm not sure this is entirely true. I only called to_field
in order to get logging working (and to produce this failing example), but in my original code this was not present.
Project Impact
Blocker
Nargo Version
nargo version = 0.30.0 noirc version = 0.30.0+5c3772f09e812a05882039ad888089c238f14001 (git version hash: 5c3772f, is dirty: false)
Spoke in DMs. This is a duplicate of #5202 but with a much nicer reproduction ๐
Given that we now have a smaller failing example, perhaps this could be used to look into why the optimization disabled in #5240 was faulty so that it can be fixed instead of removed? That'd also increase our confidence in the fix if we understood exactly why things broke.
As of current master, running nargo test
produces the following error:
error: Failed constraint
โโ src/main.nr:41:5
โ
41 โ assert_eq(magic, false);
โ -----------------------
โ
= Call stack:
1. src/main.nr:41:5
[short] 1 test failed
(commenting out assert_eq(magic, true);
before that still leads to a failure so it is not just that we're replacing magic
with true
causing the second to fail. It still fails independently)