hacspec integration

[tarcieri]

hacspec is a specification language for cryptographic primitives implemented as a subset of Rust:

https://github.com/hacspec/hacspec

The goal is to provide formally verified reference implementations of cryptographic primitives utilizing techniques like equivalence proving to verified implementations in languages like F*.

It'd be interesting to verify our implementations against the hacspec reference versions, potentially leveraging tools like Project Oak's RVT and/or crux-mir.

Relevant algorithms

AEADs

• [ ] AES-GCM
• [ ] ChaCha20Poly1305

Block/Stream Ciphers

• [ ] AES
• [ ] ChaCha20

Elliptic Curves

• [ ] NIST P-256

Hash Functions

• [ ] BLAKE2b
• [ ] SHA-256

Key Derivation Functions

• [ ] HKDF-SHA-256

Message Authentication Codes

• [ ] HMAC-SHA-256

Universal Hashes

• [ ] GF128
• [ ] Poly1305

[daviddrysdale]

cc @alastairreid @BenLaurie