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

[Bug] ternary in loop causes conditional select unsatisfiable #772

Closed
0rphon opened this issue Mar 12, 2021 · 3 comments · Fixed by #862
Closed

[Bug] ternary in loop causes conditional select unsatisfiable #772

0rphon opened this issue Mar 12, 2021 · 3 comments · Fixed by #862
Assignees
Labels
bug Something isn't working

Comments

@0rphon
Copy link
Contributor

0rphon commented Mar 12, 2021

🐛 Bug Report

Code snippet to reproduce

function main () {
    for x in 0u8..10u8 {
        let y = (false? 1u8 : x) == 2u8? 3u8 : 4u8;
    }
}

Stack trace & error message

D:\Work\leo_playground>D:\Work\leo_repos\leo\target\release\leo clean && D:\Work\leo_repos\leo\target\release\leo run
      Done Finished in 5 milliseconds 

     Build Starting...
     Build Compiling main program... ("D:\\Work\\leo_playground\\src/main.leo")
      Done Finished in 7 milliseconds

Error:     -->  3:18
     |
     |                   ^^^^^^^^^^^^^^
     |
     = the gadget operation `conditional select` failed due to synthesis error `Unsatisfiable`

Your Environment

  • leo commit 6d378c3
  • rustc version 1.50.0
  • Windows 10.0.19042 (Windows 10 Pro) [64-bit]
@0rphon 0rphon added bug Something isn't working fuzz-bug labels Mar 12, 2021
@0rphon
Copy link
Contributor Author

0rphon commented Mar 12, 2021

most likely related to #758

@ljedrz
Copy link
Contributor

ljedrz commented Mar 12, 2021

I investigated this a bit, and it looks like the loop index is wrongly assigned the U32 type; this is how the 2 compared values (1u8 : x) look like internally in the Integer::conditionally_select operation that fails with SynthesisError::Unsatisfiable:

a: U8(
    UInt8 { 
        bits: [
            Constant(true), Constant(false), Constant(false), Constant(false), Constant(false), Constant(false), Constant(false), Constant(false),
        ], 
        negated: false, 
        value: Some(1) 
    }
)

b: U32(
    UInt32 { 
        bits: [
            Constant(false), Constant(false), Constant(false), Constant(false), Constant(false), Constant(false), Constant(false), Constant(false), 
            Constant(false), Constant(false), Constant(false), Constant(false), Constant(false), Constant(false), Constant(false), Constant(false),
            Constant(false), Constant(false), Constant(false), Constant(false), Constant(false), Constant(false), Constant(false), Constant(false), 
            Constant(false), Constant(false), Constant(false), Constant(false), Constant(false), Constant(false), Constant(false), Constant(false),
        ], 
        negated: false, 
        value: Some(0) 
    }
)

@ljedrz
Copy link
Contributor

ljedrz commented Mar 12, 2021

Confirmed; this is essentially a duplicate of #758 that just throws a different error.

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

Successfully merging a pull request may close this issue.

3 participants