search

cryspen / libcrux

The formally verified crypto library for Rust
https://cryspen.com/libcrux
Apache License 2.0
89 stars 15 forks source link

Remove modules from ADMIT_MODULES #670

Closed mamonet closed 1 week ago

mamonet commented 1 week ago

Merging dev branch to mainstream generates additional modules in ADMIT_MODULES list to pass the verification process.

Libcrux_ml_kem.Ind_cca.Instantiations.Avx2.fst
Libcrux_ml_kem.Ind_cca.Instantiations.Avx2.Unpacked.fst
Libcrux_ml_kem.Ind_cca.Instantiations.Neon.Unpacked.fst
Libcrux_ml_kem.Ind_cca.Instantiations.Portable.Unpacked.fst
Libcrux_ml_kem.Mlkem1024.Avx2.Unpacked.fst
Libcrux_ml_kem.Mlkem1024.Neon.Unpacked.fst
Libcrux_ml_kem.Mlkem1024.Portable.Unpacked.fst
Libcrux_ml_kem.Mlkem768.Avx2.Unpacked.fst
Libcrux_ml_kem.Mlkem768.Neon.Unpacked.fst
Libcrux_ml_kem.Mlkem768.Portable.Unpacked.fst
Libcrux_ml_kem.Mlkem512.Avx2.Unpacked.fst
Libcrux_ml_kem.Mlkem512.Neon.Unpacked.fst
Libcrux_ml_kem.Mlkem512.Portable.Unpacked.fst
Libcrux_ml_kem.Vector.Portable.fsti
Libcrux_ml_kem.Vector.Portable.fst
Libcrux_ml_kem.Vector.Avx2.Serialize.fst

I will go through these modules one by one in order to remove them from the list and unblock https://github.com/cryspen/libcrux/pull/662

mamonet commented 1 week ago

@W95Psp I will get into Libcrux_ml_kem.Vector.Avx2.Serialize.fst once I am done with the other modules, if you have time could you please investigate why that module fails in dev-merge-main branch. I use main branch of hax with latest changes, when I run make run/Libcrux_ml_kem.Vector.Avx2.Serialize.fst I get the following error

* Error 19 at Libcrux_ml_kem.Vector.Avx2.Serialize.fst(15,51-28,74):
  - Assertion failed
  - See also Prims.fst(356,46-356,58)

Admitting deserialize_1___deserialize_1_i16s will trigger the same error for deserialize_4___deserialize_4_i16s and so on.

mamonet commented 1 week ago

Thanks Lucas for verifying Avx2.Serialize. This issue is completed.