A Deflate-like compressor in HOL, Creating executable binaries using CakeML

Abstract

Deflate is a well-known file format specification of lossless compression, with implementations in software like gzip and zip. Proving that a compressor following the Deflate algorithm has the property of being entirely reversible is of interest, as Deflate is widely used. The aim of this project is to produce verified binaries for the Deflate algorithm using the interactive theorem prover HOL4 and the CakeML compiler. The implementation consists of three main parts: the LZSS compression algorithm, the Huffman encoding algorithm, and the Deflate algorithm. Since the focus was to properly implement Deflate, the majority of our effort was put into developing the algorithm itself. Due to time constraints however, our implementation reached an executable implementation of a Deflate-like algorithm. While the Deflate algorithm has been implemented and verified before, the work described here is the first to produce an executable binary of a compression specification.