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

32-bit p521 uses uint128 #655

Closed JasonGross closed 4 years ago

JasonGross commented 4 years ago

https://github.com/mit-plv/fiat-crypto/blob/b3c26501432fd1ec5dd75e0ba136b667106fd097/p521_32.c#L129-L143

The issue is that we claim to synthesize 17-limb 32-bit p521, but 1.1 * (521 / 17) > 32. (We can't have a bounds multiplier greater than 1.044 in this case). What should be done?

@andres-erbsen ?

JasonGross commented 4 years ago

Maybe we should also have a check that the bounds are all within the bitwidth...

andres-erbsen commented 4 years ago

I think we don't care about p521 on 32-bit right now, so let's drop it and figure out these issues when we need it?