Tony Arcieri

If you haven't seen it before, check out this proposal from the "pi type trilogy": https://github.com/ticki/rfcs/blob/pi-types-ext-1/text/0000-with-bounds-in-pi-types.md#examples

Pie-in-the-sky idea: Annotate functions with the information needed to generate an equivalence proof with some reference implementation contained within the same repo. ```rust #[hacspec(prove_equivalence_to = "specs/SBox.cry")] fn sub_bytes(...) { [...]...

To get started on something like #55, it might be easiest to do as you suggest and extract the hacspec-compatible portions into their own modules and potentially even upstream those...

I was mostly spitballing, but yeah, that's the general idea: have a reference implementation which is expected to be functionally equivalent checked in somewhere in the same directory structure, and...

One option is to have a GitHub Action which regenerates the files, which can be triggered when any of the input files are touched. It can run the codegen and...

I got to play with crux-mir a little at HACS earlier this year. It also seemed interesting.

Great!

At one point we were [using `fiat-rust` with `proptest` to check our secp256k1 field implementation](https://github.com/RustCrypto/elliptic-curves/blob/93e7a40b8b048a7ff5007ab7cffa559f6d0c0e6d/k256/src/arithmetic/field.rs#L676-L766), but we removed it when we changed the field representation.

The new field implementation in the RustCrypto `k256` crate incorporates lazy reduction as a performance optimization. As far as I am aware `fiat-rust` does not support the same representation (vs...

Following up from the discussion on #97 If there's interest in upstreaming the hacspec-compatible parts of the RustCrypto `aes` implementation to this repo that'd be great. I'd imagine you'd want...