Théo Zimmermann (Jun 24 2020 at 11:21): 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".
Emilio Jesús Gallego Arias (Jul 06 2020 at 12:31):Presentation starting now
Emilio Jesús Gallego Arias (Jul 06 2020 at 12:47):Thanks!
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?
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
Bas Spitters (Jul 06 2020 at 12:48):@Emilio Jesús Gallego Arias Yes:
https://github.com/mit-plv/fiat-crypto/issues/783
Emilio Jesús Gallego Arias (Jul 06 2020 at 12:49):Thanks!
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
Maxime Dénès (Jul 06 2020 at 12:49):Thanks!
Bas Spitters (Jul 06 2020 at 12:50):@Maxime Dénès
https://github.com/AbsInt/CompCert/issues/337
Maxime Dénès (Jul 06 2020 at 12:51):@Bas Spitters Thanks for the pointer, looks interesting!
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.
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
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
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
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.
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 .
Maxime Dénès (Jul 06 2020 at 13:01):Thanks, @Diego F. Aranha !
Last updated: Apr 19 2024 at 10:02 UTC