libcrux An F* Spec for Kyber and ML-KEM

An F* Spec for Kyber and ML-KEM

Open karthikbhargavan opened this issue 1 year ago • 2 comments

trafficstars

We already wrote a spec for Kyber in F*.

We need to refine and extend this spec to more closely match the structure of ML-KEM and be suitable for our proofs.

Dec 04 '23 20:12 karthikbhargavan

This has the wrong priority and is overdue. @karthikbhargavan please update.

Aug 12 '24 08:08 franziskuskiefer

This spec work is done in https://github.com/cryspen/libcrux/pull/475 We will merge this soon and then work more on it if needed for the proofs.

Aug 12 '24 11:08 karthikbhargavan

This is done. Awaiting a hax fix before merging. https://github.com/cryspen/libcrux/pull/475

Aug 18 '24 20:08 karthikbhargavan