search

mit-plv / bedrock2

A work-in-progress language and compiler for verified low-level programming
http://adam.chlipala.net/papers/LightbulbPLDI21/
MIT License
297 stars 45 forks source link

Add verified Bedrock implementation of a full multiplier. #365

Closed wrharris closed 1 year ago

wrharris commented 1 year ago

Adds and proves correct a Bedrock function that is a translation of the C function secp256k1_umul128 (https://github.com/bitcoin-core/secp256k1/blob/master/src/int128_struct_impl.h#L32-L40)

Changes discussed with @andres-erbsen