Montgomery and signed Barrett reduction

Stream: Program verification

[Alix Trieu]

In case this is of interest to others, I have formalized some modular reduction algorithms here https://github.com/atrieu/lean-cryptolib while trying out Lean a couple months ago.

[Bas Spitters]

Nice! How does your experience compare to Fiat Cryptography which also contains these components?

[Alix Trieu]

I'm not sure what comparison you mean?

[Bas Spitters]

I'm curious both any kind of comparison, usability issues, code size, ...
Do you have plans to develop this further? Fiat-Crypto is very well developed and used in industry.

[Alix Trieu]

I don't think there is much difference in terms of using the specifications I wrote to verify code in Lean, versus directly using the same specs in Fiat-Crypto to verify code in Rocq. The main strength of Fiat-Crypto in my opinion is that one mostly does not need to do that and can automatically derive correct code. Not much difference in proof size either I think.
As a side note, I also contributed the signed Barrett reduction algorithm to Fiat-Crypto, it took me less than a day of work to prove in Rocq, versus a bit more than a week for the same thing in Lean. But I think that's mostly due to how little I know/knew about Lean/Mathlib.
No immediate future plan, though I will probably add some more stuff when I have time.