hacspec integration #9
Description
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.