Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

BadConstantEquality with conditionals in SSA refactor #1792

Closed
sirasistant opened this issue Jun 22, 2023 · 1 comment · Fixed by #1811
Closed

BadConstantEquality with conditionals in SSA refactor #1792

sirasistant opened this issue Jun 22, 2023 · 1 comment · Fixed by #1811
Assignees
Labels
bug Something isn't working refactor ssa

Comments

@sirasistant
Copy link
Contributor

sirasistant commented Jun 22, 2023

Aim

The following code generates a BadConstantEquality for the is_real assertions
EDIT(ludamad): See comment below for a minimal example!

struct Context {
    read_requests: Field,
}

impl Context {
    fn new() -> Context {
        Context { read_requests: 0 }
    }

    fn push_read_request(mut self: Self, request: Field) -> Context {
        self.read_requests += request;
        self
    }
}

struct Note {
    value: Field,
    is_real: bool,
}

fn read_2_notes_oracle(storage_slot: Field) -> (Note, Note) {
  let randomness = dep::std::hash::pedersen_with_separator([storage_slot], 0)[0];
  let note0_is_real =  ((randomness as u32) % 2) as bool;
    let note0 = Note {
        value: randomness + 1,
        is_real: note0_is_real,
    };

    let note1 = Note {
        value: randomness + 2,
        is_real: !note0_is_real,
    };

    (note0, note1)
}

fn is_real_note(note: Note) -> bool {
    note.is_real
}

fn note_hash(note: Note) -> Field {
    note.value
}

fn read_test(mut context: Context, storage_slot: Field) -> (Context, (Note,Note)) {
    let notes = read_2_notes_oracle(storage_slot);
    
    let mut note0_hash = 0;
    if is_real_note(notes.0) {
        note0_hash = note_hash(notes.0);
    }
    let mut note1_hash = 0;
    if is_real_note(notes.1) {
        note1_hash = note_hash(notes.1);
    }

    context = context.push_read_request(note0_hash);
    context = context.push_read_request(note1_hash);

    (context, notes)
}

#[test]
fn test_set() {
    let mut context = Context::new();
    let result = read_test(context, 0);
    context = result.0;
    assert(context.read_requests != 0);
    let (note0, note1) = result.1;
    assert(note0.is_real == true);
    assert(note1.is_real == false);
}

However if I remove the if branches inside read_test, it passes

struct Context {
    read_requests: Field,
}

impl Context {
    fn new() -> Context {
        Context { read_requests: 0 }
    }

    fn push_read_request(mut self: Self, request: Field) -> Context {
        self.read_requests += request;
        self
    }
}

struct Note {
    value: Field,
    is_real: bool,
}

fn read_2_notes_oracle(storage_slot: Field) -> (Note, Note) {
  let randomness = dep::std::hash::pedersen_with_separator([storage_slot], 0)[0];
  let note0_is_real =  ((randomness as u32) % 2) as bool;
    let note0 = Note {
        value: randomness + 1,
        is_real: note0_is_real,
    };

    let note1 = Note {
        value: randomness + 2,
        is_real: !note0_is_real,
    };

    (note0, note1)
}

fn is_real_note(note: Note) -> bool {
    note.is_real
}

fn note_hash(note: Note) -> Field {
    note.value
}

fn read_test(mut context: Context, storage_slot: Field) -> (Context, (Note,Note)) {
    let notes = read_2_notes_oracle(storage_slot);
    
    let mut note0_hash = note_hash(notes.0);
    let mut note1_hash = note_hash(notes.1);

    context = context.push_read_request(note0_hash);
    context = context.push_read_request(note1_hash);

    (context, notes)
}

#[test]
fn test_set() {
    let mut context = Context::new();
    let result = read_test(context, 0);
    context = result.0;
    assert(context.read_requests != 0);
    let (note0, note1) = result.1;
    assert(note0.is_real == true);
    assert(note1.is_real == false);
}

Expected Behavior

It should not generate a always false assertion

Bug

After Dead Instruction Elimination:
fn test_set f7 {
  b0():
    v81 = call pedersen([Field 0], u32 0)
    v82 = array_get v81, index Field 0
    v83 = cast v82 as u32
    v84 = mod v83, u32 2
    v85 = cast v84 as u1
    v86 = add v82, Field 1
    v87 = add v82, Field 2
    v88 = not v85
    enable_side_effects v85
    enable_side_effects u1 1
    v91 = cast v85 as Field
    v93 = mul v91, v86
    enable_side_effects v88
    enable_side_effects u1 1
    v95 = cast v88 as Field
    v97 = mul v95, v87
    v100 = add v93, v97
    v101 = eq v100, Field 0
    v102 = not v101
    constrain v102
    constrain u1 0
    return 
}

The application panicked (crashed).
Message:  add Result types to all methods so errors bubble up: BadConstantEquality { lhs: 0, rhs: 1 }
Location: crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs:165

This is a bug. We may have already fixed this in newer versions of Nargo so try searching for similar issues at https://github.com/noir-lang/noir/issues/.
If there isn't an open issue for this bug, consider opening one at https://github.com/noir-lang/noir/issues/new?labels=bug&template=bug_report.yml

Flattening seems to be the one that breaks the SSA in this case, but not sure:

After Simplifying:
fn test_set f7 {
  b0():
    v2 = allocate
    store Field 0 at v2
    v3 = load v2
    v5 = allocate
    store v3 at v5
    v10 = call pedersen([Field 0], u32 0)
    v11 = array_get v10, index Field 0
    v12 = cast v11 as u32
    v14 = mod v12, u32 2
    v15 = cast v14 as u1
    v17 = add v11, Field 1
    v19 = add v11, Field 2
    v20 = not v15
    v21 = allocate
    store Field 0 at v21
    jmpif v15 then: b1, else: b2
  b1():
    store v17 at v21
    jmp b2()
  b2():
    v23 = allocate
    store Field 0 at v23
    jmpif v20 then: b3, else: b4
  b3():
    store v19 at v23
    jmp b4()
  b4():
    v25 = load v5
    v26 = load v21
    v28 = allocate
    store v25 at v28
    v29 = load v28
    v30 = add v29, v26
    store v30 at v28
    v31 = load v28
    store v31 at v5
    v32 = load v5
    v33 = load v23
    v35 = allocate
    store v32 at v35
    v36 = load v35
    v37 = add v36, v33
    store v37 at v35
    v38 = load v35
    store v38 at v5
    v39 = load v5
    store v39 at v2
    v42 = load v2
    v43 = eq v42, Field 0
    v44 = not v43
    constrain v44
    v46 = eq v15, u1 1
    constrain v46
    v48 = eq v20, u1 0
    constrain v48
    return 
}

After Flattening:
fn test_set f7 {
  b0():
    v2 = allocate
    store Field 0 at v2
    v3 = load v2
    v5 = allocate
    store v3 at v5
    v10 = call pedersen([Field 0], u32 0)
    v11 = array_get v10, index Field 0
    v12 = cast v11 as u32
    v14 = mod v12, u32 2
    v15 = cast v14 as u1
    v17 = add v11, Field 1
    v19 = add v11, Field 2
    v20 = not v15
    v21 = allocate
    store Field 0 at v21
    enable_side_effects v15
    v49 = load v21
    store v17 at v21
    v50 = not v15
    enable_side_effects u1 1
    v51 = cast v15 as Field
    v52 = cast v50 as Field
    v53 = mul v51, v17
    v54 = mul v52, v49
    v55 = add v53, v54
    store v55 at v21
    v56 = allocate
    store Field 0 at v56
    enable_side_effects v20
    v57 = load v56
    store v19 at v56
    enable_side_effects u1 1
    v58 = cast v20 as Field
    v59 = cast v15 as Field
    v60 = mul v58, v19
    v61 = mul v59, v57
    v62 = add v60, v61
    store v62 at v56
    v63 = load v5
    v64 = load v21
    v65 = allocate
    store v63 at v65
    v66 = load v65
    v67 = add v66, v64
    store v67 at v65
    v68 = load v65
    store v68 at v5
    v69 = load v5
    v70 = load v56
    v71 = allocate
    store v69 at v71
    v72 = load v71
    v73 = add v72, v70
    store v73 at v71
    v74 = load v71
    store v74 at v5
    v75 = load v5
    store v75 at v2
    v76 = load v2
    v77 = eq v76, Field 0
    v78 = not v77
    constrain v78
    constrain u1 0
    return 
}

To Reproduce

Installation Method

None

Nargo Version

No response

Additional Context

No response

Would you like to submit a PR for this Issue?

No

Support Needs

No response

@sirasistant sirasistant added the bug Something isn't working label Jun 22, 2023
@github-project-automation github-project-automation bot moved this to 📋 Backlog in Noir Jun 22, 2023
@ludamad ludamad self-assigned this Jun 22, 2023
@ludamad
Copy link
Collaborator

ludamad commented Jun 23, 2023

Minimal reproducer, this falsely fails:

fn main() {
    let randomness = dep::std::hash::pedersen_with_separator([0], 0)[0];
    let note0_is_real = ((randomness as u32) % 2) as bool;

    let mut note0_value = 0;
    if note0_is_real { 
        note0_value = randomness + 1;
    } else {
        note0_value = 0;
    }
    
    assert(note0_is_real == true);
}

While this falsely works (simplifies away assert):

fn main() {
    let randomness = dep::std::hash::pedersen_with_separator([0], 0)[0];
    let note0_is_real = ((randomness as u32) % 2 - 1) as bool;

    let mut note0_value = 0;
    if note0_is_real { 
        note0_value = randomness + 1;
    }

    assert(note0_is_real == true);
}

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working refactor ssa
Projects
Archived in project
Development

Successfully merging a pull request may close this issue.

2 participants