Make ML-KEM F* extraction panic-free

mamonet commented 3 months ago

Make sure the extracted F* files of libcrux_ml_kem are verifiable. This work is being tracked in branches dev_ml_kem_hax on libcrux and on hax.

[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
[ ] Libcrux_ml_kem.Ind_cca.fst (Lack of pre-conditions for index ranges)
[x] Libcrux_ml_kem.Ind_cca.fsti
[ ] Libcrux_ml_kem.Ind_cpa.fst (Loop invariant)
[x] Libcrux_ml_kem.Ind_cpa.fsti
[ ] Libcrux_ml_kem.Invert_ntt.fst (Loop invariant)
[x] Libcrux_ml_kem.Invert_ntt.fsti
[ ] Libcrux_ml_kem.Matrix.fst (Loop invariant)
[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
[ ] Libcrux_ml_kem.Ntt.fst (Loop invariant)
[x] Libcrux_ml_kem.Ntt.fsti
[ ] Libcrux_ml_kem.Polynomial.fst (Lack of pre-conditions for index ranges)
[x] Libcrux_ml_kem.Polynomial.fsti
[ ] Libcrux_ml_kem.Sampling.fst (Loop invariant)
[x] Libcrux_ml_kem.Sampling.fsti
[ ] Libcrux_ml_kem.Serialize.fst (Loop invariant)
[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
[ ] 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
[ ] Libcrux_ml_kem.Vector.fsti

franziskuskiefer commented 2 months ago

Catch up with the code changes and push as far as possible this week. Try to get it merged next week.

franziskuskiefer commented 2 months ago

This (loops) are blocked on https://github.com/hacspec/hax/issues/394

karthikbhargavan commented 2 months ago

We have made a plan for this and will update this issue on Monday after finalizing the plan. The high-level point is that for some modules, proving panic freedom requires doing many of the steps needed for full functional verification. So, for these, we believe it would be best to skip panic freedom and go straight to functional proofs. Consequently, we will mark those modules accordingly and close this issue, opening a new one for full verification.

karthikbhargavan commented 1 month ago

We are closing this issue. The rest of the proofs will be done as part of the ML-KEM verificaition: https://github.com/cryspen/libcrux/issues/454

cryspen / libcrux

Make ML-KEM F* extraction panic-free #319