karthikbhargavan

This is a preliminary (draft) PR to extend the pattern language of hacspec. The idea is to more-or-less allow the full range of Rust patterns in match and let statements....

P-256 Code Failing Test Vectors

5

We've been running a bunch of test vectors (from NIST and Wycheproof) on the micro-ecc code (32-bit P-256) and found three test failures, as documented below. The first failing test...

Experimental code from HACL* for AES128-GCM

7

This is a first (version 0) commit of HACL* code for AES128-GCM. The code is not yet verified. It relies on AES-NI and PCLMUL instruction sets. The API it provides...

- [ ] aarch64 - [ ] avx2 - [ ] Portable

- [x] CI: use diffs for auto-generation of `extraction-{edited,secret-independent}` folders (see #193) - [ ] Proof cleanup: minimize a bit the initial diff

Verify matrix operations in `Matrix`

Verify functional correctness of compression and serialization in `Compress`, `Serialize`, and `Ind_cpa` ## Roadmap - [x] `serialize_uncompress_ring_element` (PR #202) - [ ] `compress_then_serialize_5_` - *in progress* - almost TCing, I...

An F* Spec for Kyber and ML-KEM

2

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...

Secret independence for Kyber

1

This issue tracks work on secret independence proofs for Kyber using the F* type system and HACL* secret integers library: - [x] Libcrux.Kem.fst - [x] Libcrux.Kem.Kyber.Constants.fst - [x] Libcrux.Digest.fsti -...