Asymptotically Faster Bignum Multiplication in a Proven Correct Arithmetic Library

Abstract

Arithmetic functions, such as +, -, *, div and mod on arbitrary precision integers (not only machine integers), are used in many important computer programs such as cryptographic software and computer algebra systems. Formal guarantees of the correctness of these systems heavily rely on the correctness of the underlying arithmetic functions. Cryptography algorithms such as RSA and Diffie–Hellman require efficient operations over large numbers. Arbitrary precision arithmetic, also called bignum arithmetic, is arithmetic of large numbers that exceeds the size of machine words. In this thesis, we describe and implement two asymptotically fast bignum multiplication algorithms, namely the Karatsuba and Toom-3 algorithms, using the interactive theorem prover HOL4. Further, we take steps towards integrating the Karatsuba algorithm into CakeML’s verified bignum library by specifying an implementation which satisfies parts of the required format by the integration infrastructure.