karthikbhargavan

* I have created a new branch: https://github.com/cryspen/libcrux/tree/libcrux-secret-independence/libcrux-ml-kem * The secret independence (aka secret integers) crate is now here: https://github.com/cryspen/libcrux/tree/libcrux-secret-independence/libcrux-secret-independence * I extended libcrux-intrinsics to support secret-independent SIMD instructions: use...

Tested on multiple platforms and compilers. Some observations: - compiling with gcc on x64 does not appear to enable HACL_CAN_COMPILE_INTRINSICS in lib_intrinsics.h, leading to a performance degradation. enabling this flag...

It is not yet clear whether CRT is needed in this round (although I would like to do it.)

Currently, this does not appear to be a priority since our signing code is already faster than Linux. We will do this in the fall as time permits.

As a first step, we will target: https://github.com/cryspen/hax/issues/1478

The plan for the ML-DSA proofs are as follows: 1. Prove the arithmetic code (by porting them from ML-KEM where possible) 2. Prove the serialization code (by adapting and reusing...

Most of our goals have been reached. It is now a matter of cleaning up and documenting what we proved which is on my plate.

Yes, I'll do a round of cleanups, likely on Friday.

We will close this after the meeting next week.

We reached our milestone. Some TODOs and cleanups are collected here: https://github.com/cryspen/libcrux/issues/1084