fix Core.Clone

[Parrot7483]

No description provided.

[W95Psp]

LGTM, thanks!

Edit: I pushed a minor change, fixing the template code for Clone produced by the F* backend in the engine.

[Parrot7483]

Can this be merged?

[W95Psp]

The rustc coverage tests had to be updated, I pushed the update

[W95Psp]

Waiting for #1558

[franziskuskiefer]

Looks like this fails ml-kem laxing

[Parrot7483]

This might be the same problem I had with charon dependency. The build script pulls in all FStar files from everywhere, including the ones from ~/.cargo. Charon has its own fork of HAX.

The Libcrux_ml_kem.Vector.Neon.Vector_type.fsti is correct when checking with VSCode interactive mode. I fixed in like this in my sha3 branch.

[W95Psp]

I think this failure is because of #1094.
I will test locally: if that goes through, I will force merge.

[W95Psp]

Indeed, this is working locally, using a git dependency for hax-lib.
Since hax-lib is pinned to a crates.io version, but hax itself is not pinned, this PR will break Libcrux. Thus, either:

• we change hax-lib to be a git dependency
• we pin hax itself to the version given by hax-lib

WDYT @franziskuskiefer?

[W95Psp]

Requires cryspen/libcrux#1074 and #1279.

[W95Psp]

The CI should probably be happy now, let's push to merge queue again.