fix(engine) Attempt to fix double return bug.

[maximebuyse]

This is an attempt to make things better for #720.

As far as we know, this bug happens when there is a loop with side effects at the end of a function. Then AndMutDefSite transforms this to:

let hax_temp_output: tuple0 = <loop>
hax_temp_output

And LocalMutation transforms this binding to:

let Tuple2(modified_var, hax_temp_output) = <loop>
...

but the transformation of the loop is made in such a way that here <loop> has the type of <modified_var>.

This fix is modifying AndMutDefSite so that if the expression has type unit, instead of the previous binding it produces:

let _ = <loop>
()

This works better with the assumptions of LocalMutation and fixes the bug (at least for the last reproducer that I added as a test). A more in depth rework of both those phases with a formalization of the invariants would be a better long-term solution.

[W95Psp]

Libcrux job: https://github.com/cryspen/libcrux/actions/runs/12687761706

[W95Psp]

Thanks, that looks great to me :)
Let's merge whenever libcrux is green!

[karthikbhargavan]

This needs a bit more testing. Let's create a branch/PR for libcrux where we remove all instances of the workaround (these are marked by a comment referencing #720) and make sure it still laxes.

[maximebuyse]

This needs a bit more testing. Let's create a branch/PR for libcrux where we remove all instances of the workaround (these are marked by a comment referencing #720) and make sure it still laxes.

I started a libcrux branch called remove-double-return-workarounds where I removed the unit expressions added to the code for this issue. I started https://github.com/cryspen/libcrux/actions/runs/12690891533/job/35372725600 to see if everything works ok using this hax branch.

[maximebuyse]

This needs a bit more testing. Let's create a branch/PR for libcrux where we remove all instances of the workaround (these are marked by a comment referencing #720) and make sure it still laxes.

I started a libcrux branch called remove-double-return-workarounds where I removed the unit expressions added to the code for this issue. I started https://github.com/cryspen/libcrux/actions/runs/12690891533/job/35372725600 to see if everything works ok using this hax branch.

The job failed, here is a reproducer:

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

Open this code snippet in the playground
This is because the macro #[hax_lib::fstar::verification_status(panic_free)] puts the result of the function (here the loop) inside a let binding. There could be two ways to fix this:

• Have a visitor that removes all let bindings with a unit rhs (We would also need to replace all occurrences of the binding by a unit expression). That should be quite easy.
• Actually fix LocalMutation. That will probably require a bit more work but is probably the right thing to do.

[maximebuyse]

This needs a bit more testing. Let's create a branch/PR for libcrux where we remove all instances of the workaround (these are marked by a comment referencing #720) and make sure it still laxes.

I started a libcrux branch called remove-double-return-workarounds where I removed the unit expressions added to the code for this issue. I started https://github.com/cryspen/libcrux/actions/runs/12690891533/job/35372725600 to see if everything works ok using this hax branch.

The job failed, here is a reproducer:

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

Open this code snippet in the playground This is because the macro #[hax_lib::fstar::verification_status(panic_free)] puts the result of the function (here the loop) inside a let binding. There could be two ways to fix this:

* Have a visitor that removes all let bindings with a unit rhs (We would also need to replace all occurrences of the binding by a unit expression). That should be quite easy.

* Actually fix `LocalMutation`. That will probably require a bit more work but is probably the right thing to do.

I went with the actual fix in LocalMutation which was not that complicated in the end. Here is the CI for libcrux to try this out: https://github.com/cryspen/libcrux/actions/runs/12692388677/job/35377610353

[maximebuyse]

This needs a bit more testing. Let's create a branch/PR for libcrux where we remove all instances of the workaround (these are marked by a comment referencing #720) and make sure it still laxes.

I started a libcrux branch called remove-double-return-workarounds where I removed the unit expressions added to the code for this issue. I started https://github.com/cryspen/libcrux/actions/runs/12690891533/job/35372725600 to see if everything works ok using this hax branch.

The job failed, here is a reproducer:

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

Open this code snippet in the playground This is because the macro #[hax_lib::fstar::verification_status(panic_free)] puts the result of the function (here the loop) inside a let binding. There could be two ways to fix this:

* Have a visitor that removes all let bindings with a unit rhs (We would also need to replace all occurrences of the binding by a unit expression). That should be quite easy.

* Actually fix `LocalMutation`. That will probably require a bit more work but is probably the right thing to do.

I went with the actual fix in LocalMutation which was not that complicated in the end. Here is the CI for libcrux to try this out: https://github.com/cryspen/libcrux/actions/runs/12692388677/job/35377610353

This succeeds 🥳 . However this reveals another bug:

fn range() {
    let mut count = 0u8;
    for i in 0u8..10u8 {
        hax_lib::loop_invariant!(|i: u8| i <= 10);
        count = i;
    }
}

fn f() {
    range()
}

Open this code snippet in the playground
Here range has the following type signature in the generated F*: range (_: Prims.unit) : u8 but it should actually return unit. The problem is that we don't hoist the loop inside a let _ = <loop>; () so this is probably a problem in HoistSideEffects. This issue is already present in the tests, my PR modifies the output so we could either accept the new output (which is equally wrong as the previous one) and treat this in a separate issue. Or try to fix it here if it is easy.

[maximebuyse]

This succeeds 🥳 . However this reveals another bug:

fn range() {
    let mut count = 0u8;
    for i in 0u8..10u8 {
        hax_lib::loop_invariant!(|i: u8| i <= 10);
        count = i;
    }
}

fn f() {
    range()
}

Open this code snippet in the playground Here range has the following type signature in the generated F*: range (_: Prims.unit) : u8 but it should actually return unit. The problem is that we don't hoist the loop inside a let _ = <loop>; () so this is probably a problem in HoistSideEffects. This issue is already present in the tests, my PR modifies the output so we could either accept the new output (which is equally wrong as the previous one) and treat this in a separate issue. Or try to fix it here if it is easy.

I implemented a fix that binds all expression of type unit in let _ = e; (). That seems to work but changes the output of a lot of tests. We could limit that to only happen when there are side effects (but this requires calling another visitor, which complexifies the code and degrades performance). Let's see if we want to do that or merge this version.

[maximebuyse]

This succeeds 🥳 . However this reveals another bug:

fn range() {
    let mut count = 0u8;
    for i in 0u8..10u8 {
        hax_lib::loop_invariant!(|i: u8| i <= 10);
        count = i;
    }
}

fn f() {
    range()
}

Open this code snippet in the playground Here range has the following type signature in the generated F*: range (_: Prims.unit) : u8 but it should actually return unit. The problem is that we don't hoist the loop inside a let _ = <loop>; () so this is probably a problem in HoistSideEffects. This issue is already present in the tests, my PR modifies the output so we could either accept the new output (which is equally wrong as the previous one) and treat this in a separate issue. Or try to fix it here if it is easy.

I implemented a fix that binds all expression of type unit in let _ = e; (). That seems to work but changes the output of a lot of tests. We could limit that to only happen when there are side effects (but this requires calling another visitor, which complexifies the code and degrades performance). Let's see if we want to do that or merge this version.

I improved a bit to check if there are side effects before changing anything. It is less disruptive to test snapdhots but there is still a diff in a few places. @W95Psp do you think this is ok?

[maximebuyse]

This succeeds 🥳 . However this reveals another bug:

fn range() {
    let mut count = 0u8;
    for i in 0u8..10u8 {
        hax_lib::loop_invariant!(|i: u8| i <= 10);
        count = i;
    }
}

fn f() {
    range()
}

Open this code snippet in the playground Here range has the following type signature in the generated F*: range (_: Prims.unit) : u8 but it should actually return unit. The problem is that we don't hoist the loop inside a let _ = <loop>; () so this is probably a problem in HoistSideEffects. This issue is already present in the tests, my PR modifies the output so we could either accept the new output (which is equally wrong as the previous one) and treat this in a separate issue. Or try to fix it here if it is easy.

I implemented a fix that binds all expression of type unit in let _ = e; (). That seems to work but changes the output of a lot of tests. We could limit that to only happen when there are side effects (but this requires calling another visitor, which complexifies the code and degrades performance). Let's see if we want to do that or merge this version.

I improved a bit to check if there are side effects before changing anything. It is less disruptive to test snapdhots but there is still a diff in a few places. @W95Psp do you think this is ok?

Let's deal with this in a separate issue (#1231). And merge the fix for this one now.