Formal methods

[spitters]

We describe our approach to formal methods here:
cfrg/draft-irtf-cfrg-bls-signature#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]

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]

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 hacspec/hacspec#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]

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

[chris-wood]

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

[spitters]

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

[chris-wood]

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

[spitters]

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

[franziskuskiefer]

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

There certainly is :)