This directory contains specifications for primitives in libcrux. These are the basis for the correctness proofs of the efficient primitives in src.
| Algorithm | HACL | libjade | AU curves |
|---|---|---|---|
| Chacha20 | ✔✍🏻 | ✔ | |
| Poly1305 | ✔✍🏻 | ✔ | |
| Chacha20Poly1305 | ✔✍🏻 | ||
| Curve25519 | ✔ | ✔ | |
| Sha2 256 | ✔ | ||
| Bls12-381 | ✔🧪✍🏻 |
- ✔ implementation
- ✍🏻 proof
- 🧪 property based testing