Bad translation of ensures with &mut

[W95Psp]

trafficstars

#[hax_lib::ensures(|_| true)]
fn f(x: &mut u8) {}

Open this code snippet in the playground

The bug is that the macro ensures

[karthikbhargavan]

Still seeing some bad examples, e.g. https://github.com/cryspen/libcrux/blob/9097d098ba27f5f99ea14397399ad0d0ee5cf395/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti#L66

[W95Psp]

I'm having a hard time reproducing (see https://hax-playground.cryspen.com/#fstar/2a17a0beef/gist=8689d6b1b90ffbdfde130b3fe5710901). But, re-extracting with this commit I get indeed this bug, I think that might be a interface-only bug

[W95Psp]

@karthikbhargavan, I think this was due to a stale hax-lib actually! I spent a lot of time looking at it, and at the end I think it's only a version issue :facepalm: after a cargo update hax-lib, plus making sure the correct version is used, this disappears for me Closing, but if it comes back feel free to re-open