An implementation of Deflate in Coq

TL;DR

This paper presents a rigorously formalized and verified implementation of the Deflate compression algorithm in Coq, clarifying ambiguities in the standard and proving the correctness of compression and decompression as inverse functions.

Contribution

It provides the first verified Coq implementation of Deflate, including a formal specification of prefix-free codes and a proof of inverse correctness for compression and decompression.

Findings

Achieved competitive performance on large inputs

First formal proof of inverse relationship between compression and decompression

Demonstrated compatibility with existing Deflate implementations

Abstract

The widely-used compression format "Deflate" is defined in RFC 1951 and is based on prefix-free codings and backreferences. There are unclear points about the way these codings are specified, and several sources for confusion in the standard. We tried to fix this problem by giving a rigorous mathematical specification, which we formalized in Coq. We produced a verified implementation in Coq which achieves competitive performance on inputs of several megabytes. In this paper we present the several parts of our implementation: a fully verified implementation of canonical prefix-free codings, which can be used in other compression formats as well, and an elegant formalism for specifying sophisticated formats, which we used to implement both a compression and decompression algorithm in Coq which we formally prove inverse to each other -- the first time this has been achieved to our knowledge. The compatibility to other Deflate implementations can be shown empirically. We furthermore discuss some of the difficulties, specifically regarding memory and runtime requirements, and our approaches to overcome them.