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