Asymptotically Faster Bignum Multiplication in a Proven Correct Arithmetic Library

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/253913
Download file(s):
File Description SizeFormat 
253913.pdfFulltext683.07 kBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: Asymptotically Faster Bignum Multiplication in a Proven Correct Arithmetic Library
Authors: Lindeman, Olle
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.
Keywords: Data- och informationsvetenskap;Computer and Information Science
Issue Date: 2017
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
URI: https://hdl.handle.net/20.500.12380/253913
Collection:Examensarbeten för masterexamen // Master Theses



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.