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

Presentation starting now

Thanks!

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?

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

@Emilio Jesús Gallego Arias Yes:

https://github.com/mit-plv/fiat-crypto/issues/783

Thanks!

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

Thanks!

@Maxime Dénès

https://github.com/AbsInt/CompCert/issues/337

@Bas Spitters Thanks for the pointer, looks interesting!

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

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

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

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

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.

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 .

Thanks, @Diego F. Aranha !

Last updated: May 31 2023 at 03:30 UTC