Asymptotically Faster Bignum Multiplication in a Proven Correct Arithmetic Library
Ladda ner
Typ
Examensarbete för masterexamen
Master Thesis
Master Thesis
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2017
Författare
Lindeman, Olle
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
Data- och informationsvetenskap , Computer and Information Science