search

cfrg / draft-irtf-cfrg-hash-to-curve

Hashing to Elliptic Curves
Other
78 stars 27 forks source link

Formal methods #331

Open spitters opened 2 years ago

spitters commented 2 years ago

We describe our approach to formal methods here: https://github.com/cfrg/draft-irtf-cfrg-bls-signature/issues/47

A hacspec specification of the slow algorithm for hashing to curve is now available here.

Any suggestions on how to best interact with the standardization process would be welcome.

chris-wood commented 2 years ago

Thanks for filing this issue! This draft previously had hacspec specifications of some algorithms, back before hacspec moved to Rust. We abandoned this and reverted to the current algorithm descriptions and formulations since hacspec didn't appear to be well maintained at the time. Has that changed? Perhaps @franziskuskiefer knows the latest here.

franziskuskiefer commented 2 years ago

Right there has been some downtime after abandoning the Python version. The new (Rust) hacspec is well and alive and I hope we can keep it that way. @spitters and his team is actively using it with the coq backend and we are using it as frontend for more and more for F* things.

For the hacspec specification @spitters links we have an open PR https://github.com/hacspec/hacspec/pull/200 I'd appreciate a review of the PR with respect to correctness of the spec. Some feedback would also be interesting in terms of esthetics, e.g. is the code readable for someone unfamiliar with hacspec etc.

spitters commented 2 years ago

I see that @kasserne has meanwhile also implemented the optimized algorithm :tada: Indeed, it would be great to get feedback on how faithful hacspec is wrt the informal specification in the standard.

chris-wood commented 2 years ago

@spitters we can review the hacspec implementation. @franziskuskiefer, is there interest in hacspec implementations of the other algorithms in this spec?

spitters commented 2 years ago

I think there is, we'd like to experiment with testing efficient implementations against the spec.

chris-wood commented 2 years ago

@spitters how should we go about adding them? Would one of us send PRs to hacspec, for example?

spitters commented 2 years ago

Yes, a PR to hacspec seems like the canonical way. Feel free to come and discuss with us on the hacspec zulip.

franziskuskiefer commented 2 years ago

@franziskuskiefer, is there interest in hacspec implementations of the other algorithms in this spec?

There certainly is :)