karthikbhargavan

This is blocked on ind_cca decap breaking CI. We need to debug this.

This now relies on https://github.com/hacspec/hax/pull/854

Fixed decap using https://github.com/hacspec/hax/pull/854

Let's follow the folliowng procedure for this and subsequent PRs: - [x] Have the preconditions for const-generics been added? - [x] Have the postconditions relating the code to the spec...

https://github.com/cryspen/libcrux/pull/475 is now merged. Could you check if there were some changes here that did not make it into that PR? Otherwise, let's close this.

We have started formally verifying modules, and will be incrementally doing PRs to dev, which is not the proof-oriented branch. The main reason to use dev and not main is...

We still have three tasks ongoing: * Lucas: https://github.com/cryspen/libcrux/issues/535 * Mamone: https://github.com/cryspen/libcrux/issues/565 * Karthik: https://github.com/cryspen/libcrux/issues/566

We should allocate some resources for secret independence: * https://github.com/cryspen/libcrux/issues/453 This can either be done just for ML-KEM, or for ML-KEM+ML-DSA, or for libcrux more generally.

We delivered the proofs. Some todos remain which will be tracked in a new issue.

We never got around to doing this.