search

mit-plv / fiat-crypto

Cryptographic Primitive Code Generation by Fiat
http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf
Other
713 stars 147 forks source link

Montgomery: support rolled loops #1190

Open JasonGross opened 2 years ago

JasonGross commented 2 years ago

We can actually support very large primes with minimal changes:

  1. Export redc_step
  2. Thunk synthesis so that when mul is not requested it's not computed
  3. Write a wrapper in C to turn redc_step into redc into mul, a la div step
Bandt2022 commented 1 year ago

C - mul

cpitclaudel commented 1 year ago

Don't we now have code to synthesize loops as well? (I guess I'm misunderstanding the title)