Stream: Coq workshop 2020

Topic: [M5] High-assurance field inversion for pairing-friendly...


view this post on Zulip Théo Zimmermann (Jun 24 2020 at 11:21):

This is the topic to ask questions on the talk "High-assurance field inversion for pairing-friendly primes".

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 12:31):

Presentation starting now

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 12:47):

Thanks!

view this post on Zulip Maxime Dénès (Jul 06 2020 at 12:47):

Q: Where does the overhead between your code and the hand-optimized version of the same algorithm come from, mainly? I.e. what do human experts do better?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 12:48):

Q: Do you think Jasmin could be useful to you? https://github.com/jasmin-lang/jasmin

view this post on Zulip Bas Spitters (Jul 06 2020 at 12:48):

@Emilio Jesús Gallego Arias Yes:
https://github.com/mit-plv/fiat-crypto/issues/783

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 12:49):

Thanks!

view this post on Zulip Bas Spitters (Jul 06 2020 at 12:49):

@Maxime Dénès We would also like to use constant time compcert, but 128bits is missing

view this post on Zulip Maxime Dénès (Jul 06 2020 at 12:49):

Thanks!

view this post on Zulip Bas Spitters (Jul 06 2020 at 12:50):

@Maxime Dénès
https://github.com/AbsInt/CompCert/issues/337

view this post on Zulip Maxime Dénès (Jul 06 2020 at 12:51):

@Bas Spitters Thanks for the pointer, looks interesting!

view this post on Zulip Bas Spitters (Jul 06 2020 at 12:52):

Yes, it's really exciting, and it could use a bit of coordination between projects as you can see.

view this post on Zulip Maxime Dénès (Jul 06 2020 at 12:53):

I remember Xavier explaining the various problems he had when adding 64-bit arithmetic to CompCert

view this post on Zulip Maxime Dénès (Jul 06 2020 at 12:54):

some of these problems being actually issues on the Coq side e.g. with functors and opacity

view this post on Zulip Maxime Dénès (Jul 06 2020 at 12:54):

so I can imagine why it's not so easy to add 128-bit arithmetic

view this post on Zulip Bas Spitters (Jul 06 2020 at 12:57):

Interesting. On the other hand, it's probably something we'd like to have in the long run.
@Jason Gross and Jade are currently mostly working on targeting bedrock2.

view this post on Zulip Diego F. Aranha (Jul 06 2020 at 13:00):

Maxime Dénès said:

Q: Where does the overhead between your code and the hand-optimized version of the same algorithm come from, mainly? I.e. what do human experts do better?

As replied online, essentially register allocation and occupation. The CIOS approach to Montgomery modular multiplication used by Fiat may complicate this further by adding too many intermediate variables, which makes the compiler introduce housekeeping code to switch context between multiplication and reduction. We believe an SOS strategy used in the ASM code could improve this, as mentioned in the GitHub thread linked by @Bas Spitters .

view this post on Zulip Maxime Dénès (Jul 06 2020 at 13:01):

Thanks, @Diego F. Aranha !


Last updated: Feb 06 2023 at 05:03 UTC