Make libcrux_ml_kem lax-check in F*

[mamonet]

Make sure the extracted F* files of libcrux_ml_kem pass lax-check.
This work is being tracked in branches dev_ml_kem_hax on libcrux and on hax.

• https://github.com/cryspen/libcrux/tree/dev_ml_kem_lax/libcrux-ml-kem/proofs/fstar/extraction
• https://github.com/hacspec/hax/tree/dev_ml_kem_lax/proof-libs/fstar

("*" indicates that some hax changes, not yet upstreamed, are required to make the module pass)

• Libcrux_ml_kem.Constant_time_ops.fst
• Libcrux_ml_kem.Constant_time_ops.fsti
• Libcrux_ml_kem.Constants.fsti
• Libcrux_ml_kem.Hash_functions.Avx2.fsti
• Libcrux_ml_kem.Hash_functions.Neon.fsti
• Libcrux_ml_kem.Hash_functions.Portable.fsti
• Libcrux_ml_kem.Hash_functions.fsti
• Libcrux_ml_kem.Ind_cca.Instantiations.Avx2.fst
• Libcrux_ml_kem.Ind_cca.Instantiations.Avx2.fsti
• Libcrux_ml_kem.Ind_cca.Instantiations.Portable.fst
• Libcrux_ml_kem.Ind_cca.Instantiations.Portable.fsti
• Libcrux_ml_kem.Ind_cca.Multiplexing.fst
• Libcrux_ml_kem.Ind_cca.Multiplexing.fsti
• Libcrux_ml_kem.Ind_cca.fst*
• Libcrux_ml_kem.Ind_cca.fsti
• Libcrux_ml_kem.Ind_cpa.fst*
• Libcrux_ml_kem.Ind_cpa.fsti
• Libcrux_ml_kem.Invert_ntt.fst*
• Libcrux_ml_kem.Invert_ntt.fsti
• Libcrux_ml_kem.Matrix.fst
• Libcrux_ml_kem.Matrix.fsti
• Libcrux_ml_kem.Mlkem1024.Avx2.fst
• Libcrux_ml_kem.Mlkem1024.Avx2.fsti
• Libcrux_ml_kem.Mlkem1024.Portable.fst
• Libcrux_ml_kem.Mlkem1024.Portable.fsti
• Libcrux_ml_kem.Mlkem1024.fst
• Libcrux_ml_kem.Mlkem1024.fsti
• Libcrux_ml_kem.Mlkem512.Avx2.fst
• Libcrux_ml_kem.Mlkem512.Avx2.fsti
• Libcrux_ml_kem.Mlkem512.Portable.fst
• Libcrux_ml_kem.Mlkem512.Portable.fsti
• Libcrux_ml_kem.Mlkem512.fst
• Libcrux_ml_kem.Mlkem512.fsti
• Libcrux_ml_kem.Mlkem768.Avx2.fst
• Libcrux_ml_kem.Mlkem768.Avx2.fsti
• Libcrux_ml_kem.Mlkem768.Portable.fst
• Libcrux_ml_kem.Mlkem768.Portable.fsti
• Libcrux_ml_kem.Mlkem768.fst
• Libcrux_ml_kem.Mlkem768.fsti
• Libcrux_ml_kem.Ntt.fst*
• Libcrux_ml_kem.Ntt.fsti
• Libcrux_ml_kem.Polynomial.fst*
• Libcrux_ml_kem.Polynomial.fsti
• Libcrux_ml_kem.Sampling.fst*
• Libcrux_ml_kem.Sampling.fsti
• Libcrux_ml_kem.Serialize.fst*
• Libcrux_ml_kem.Serialize.fsti
• Libcrux_ml_kem.Types.fst
• Libcrux_ml_kem.Types.fsti
• Libcrux_ml_kem.Utils.fst
• Libcrux_ml_kem.Utils.fsti
• Libcrux_ml_kem.Vector.Avx2.Arithmetic.fst
• Libcrux_ml_kem.Vector.Avx2.Arithmetic.fsti
• Libcrux_ml_kem.Vector.Avx2.Compress.fst
• Libcrux_ml_kem.Vector.Avx2.Compress.fsti
• Libcrux_ml_kem.Vector.Avx2.Ntt.fst
• Libcrux_ml_kem.Vector.Avx2.Ntt.fsti
• Libcrux_ml_kem.Vector.Avx2.Portable.fst
• Libcrux_ml_kem.Vector.Avx2.Portable.fsti
• Libcrux_ml_kem.Vector.Avx2.Sampling.fst
• Libcrux_ml_kem.Vector.Avx2.Sampling.fsti
• Libcrux_ml_kem.Vector.Avx2.Serialize.fst
• Libcrux_ml_kem.Vector.Avx2.Serialize.fsti
• Libcrux_ml_kem.Vector.Avx2.fst
• Libcrux_ml_kem.Vector.Avx2.fsti
• Libcrux_ml_kem.Vector.Portable.fsti
• Libcrux_ml_kem.Vector.Rej_sample_table.fsti
• Libcrux_ml_kem.Vector.Traits.fst
• Libcrux_ml_kem.Vector.Traits.fsti
• Libcrux_ml_kem.Vector.fst (File seems to be too big to verify)
• Libcrux_ml_kem.Vector.fsti

[franziskuskiefer]

Blocked on some hax fixes (@W95Psp please update here with which PRs need to get merged for this) and restructuring of vector (PR incoming, please update here @karthikbhargavan).

[W95Psp]

Needs hacspec/hax#726, and a fix for hacspec/hax#719.
Note I added a workaround in hacspec/hax#719.

[franziskuskiefer]

What's the state here? Can we get this on CI and close it?

[karthikbhargavan]

There is still a bug in hax that needs to be fixed. Hopefully can be closed today or tomorrow.

[karthikbhargavan]

hacspec/hax#719 is reopened

[W95Psp]

...and soon re-closed I hope: hacspec/hax#738 🤞