Double return bug

[mamonet]

There are cases where extracted F files in libcrux-ml-kem have redundant third return value where just double are supposed to be at the receiving side. This breaks lax-check of affected F files. Here is an example of this bug https://github.com/cryspen/libcrux/blob/dev/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fst#L34

It's fixed manually here https://github.com/cryspen/libcrux/blob/dev_ml_kem_lax/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fst#L34

Workaround: add () at the end of your function, see the comment below.

[W95Psp]

Thanks for the bug report Mamone!

I'm looking at it now, here is a minimized reproducer:

fn f(n: &mut usize) {
    for _ in 0..10 {
        *n += 1;
    }
}

The problem shows up only when n is a &mut.

[W95Psp]

Thanks for the issue! I spent a few hours on that, I don't have a fix yet.

I think this issue shows up mainly in functions that ends with a loop. A workaround is to add a () at the end of the function, e.g.:

fn f(n: &mut usize) {
    for _ in 0..10 {
        *n += 1;
    }
}

becomes:

fn f(n: &mut usize) {
    for _ in 0..10 {
        *n += 1;
    };
   ()
}

[franziskuskiefer]

@W95Psp this is overdue for a while now. What's the status and plan to get it fixed?

[W95Psp]

I removed the due date and set the priority to low. We have a workaround, and loads of other things to do, so let's pick that whenever we have time.

[karthikbhargavan]

I found a few other instances of this. I think this has to have a higher priority since the bug and its fix are quite obscure.