Double return bug

[mamonet]

trafficstars

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

[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.

[W95Psp]

My reproducer:

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

works now, let's find another reproducer or close otherwise

[franziskuskiefer]

Looks like this is working for the cases in libcrux as well 🥳 Let's link the PR that fixed it. Are there tests? If not we should add some and close this issue with that.

[W95Psp]

Well, we did no any work towards this 😅 Somehow something fixed it. I think that's one of the new phases added by @maximebuyse that interact with this. Shall we just close or shall we bisect to find out what fixed it?

[karthikbhargavan]

lets eliminate all instances in libcrux to test first

On Thu, Nov 28, 2024, 09:44 Lucas Franceschino @.***> wrote:

Well, we did no any work towards this 😅 Somehow something fixed it. I think that's one of the new phases added by @maximebuyse https://github.com/maximebuyse that interact with this. Shall we just close or shall we bisect to find out what fixed it?

— Reply to this email directly, view it on GitHub https://github.com/hacspec/hax/issues/720#issuecomment-2505555412, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFUVS5ZOTLID3DVFOJZ3CD2C3JX3AVCNFSM6AAAAABJJWJEOOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDKMBVGU2TKNBRGI . You are receiving this because you commented.Message ID: @.***>

[franziskuskiefer]

I'm still seeing this in the ML-DSA code in libcrux. Here's an example https://hax-playground.cryspen.com/#fstar+tc/de59826b83/gist=b2613b7c8515f901ecc1a2bd77339e17

[franziskuskiefer]

Somehow something fixed it.

This is still generally broken. For example

fn looping(array: &mut [u8; 5]) {
    for i in 0..array.len() {
        array[i] = i as u8;
    }
}

[maximebuyse]

Fixed by https://github.com/cryspen/hax/pull/1223