Integration with RustCrypto about hacspec HOT 12 OPEN

Hi Tony, thank you very much for this heads up! Using RVT to perform some symbolic execution of property-based testing would maybe work for proving functional equivalence between Hacspec specs and RustCrypto implementations. Another tool to use would be crux-mir. The question is whether these tools are sufficiently advanced to deal with hacspec-lib, which has a lot of stuff going on.

I was planning to try and see if crux-mir can handle it next week, I'll have a go at RVT too.

from hacspec.

We're currently in the process of making everything in here a little bit more user friendly. Getting more usage would certainly help with this.

FWIW, I've also started looking into using hacspec with Orion.

from hacspec.

@tarcieri I started adding an implementation of the RustCrypto traits on top of the specs (only chachapoly for now) https://github.com/hacspec/hacspec/tree/master/provider. This gives us the same entry points for the specs and implementations.

from hacspec.

We (=@RasmusHoldsbjergCSAU) are working on the in Aarhus :-)
Still work in progress...
https://github.com/RasmusHoldsbjergCSAU/QuadraticFieldExtensions/tree/master/LazyReduction

from hacspec.

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 to keep what you have currently as an easier-to-understand reference version as what we have is a heavily optimized "fixsliced" implementation based on this paper:

https://eprint.iacr.org/2020/1123.pdf

Perhaps it would even be possible to prove equivalence between the reference and optimized implementations (even if only for select parts like the SBox implementation)

from hacspec.

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

from hacspec.

Thanks for the heads up @tarcieri. This is certainly a direction we're interested in exploring. We're currently in the process of making everything in here a little bit more user friendly. Getting more usage would certainly help with this.
I'm actually considering implementing the RustCrypto traits for the specs we have here. I think this would be a good start for RustCrypto/meta#9 as well.
I'd expect @atomb to be interested to look at this from the crux-mir angle as well.

from hacspec.

Great!

from hacspec.

https://github.com/mit-plv/fiat-crypto allows one to generate efficient rust code directly.
@huitseeker will also be interested.

from hacspec.

At one point we were using fiat-rust with proptest to check our secp256k1 field implementation, but we removed it when we changed the field representation.

from hacspec.

Interesting. Are these changes so big that this cannot be reintroduced in the future?
Fiat provides quite a big suite of primitives and curves.

from hacspec.

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 before where we implemented the same Montgomery representation)

from hacspec.