hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
174 stars 19 forks source link

`return`/`break`/`continue` within loops #196

Open franziskuskiefer opened 1 year ago

franziskuskiefer commented 1 year ago

Some for loop issues


pub fn loop1() -> Result<u8, u8> {
    let p1 = vec![1, 2, 3];
    for i in 0..p1.len() {
        if p1[i] == 3 {
            return Ok(p1[i]);
        }
    }
    Err(1)
}

pub fn loop2() -> Result<u8, u8> {
    let p1 = vec![1, 2, 3];
    for _ in 0..p1.len() {
        continue;
    }
    Err(1)
}

produces

error[HAX0001]: CfIntoMonads:something is not implemented yet.This is discussed in issue https://github.com/hacspec/hacspec-v2/issues/96.
                Please upvote or comment this issue if you see this error message.
                TODO: Monad for loop-related control flow
  --> src/lib.rs:26:5
   |
26 | /     for _ in 0..p1.len() {
27 | |         continue;
28 | |     }
   | |_____^

error[HAX0001]: FunctionalizeLoops:something is not implemented yet.
                Loop without mutation?
  --> src/lib.rs:16:5
   |
16 | /     for i in 0..p1.len() {
17 | |         if p1[i] == 3 {
18 | |             return Ok(p1[i]);
19 | |         }
20 | |     }
   | |_____^

error[HAX0001]: FunctionalizeLoops:something is not implemented yet.
                Only for loop are being functionalized for now
  --> src/lib.rs:26:5
   |
26 | /     for _ in 0..p1.len() {
27 | |         continue;
28 | |     }
   | |_____^
franziskuskiefer commented 1 year ago

Also see #96

W95Psp commented 3 months ago

Would be nice to have for ML-Kem