Make libcrux_ml_kem lax-check in F*

mamonet commented 3 weeks ago

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.

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

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

franziskuskiefer commented 5 days ago

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 commented 5 days ago

Needs https://github.com/hacspec/hax/pull/726, and a fix for https://github.com/hacspec/hax/issues/719. Note I added a workaround in https://github.com/hacspec/hax/issues/719.

franziskuskiefer commented 3 days ago

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

karthikbhargavan commented 3 days ago

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

karthikbhargavan commented 3 days ago

https://github.com/hacspec/hax/issues/719 is reopened

W95Psp commented 2 days ago

...and soon re-closed I hope: https://github.com/hacspec/hax/pull/738 :crossed_fingers:

cryspen / libcrux

Make libcrux_ml_kem lax-check in F* #301