Verified Reversible Programming for Verified Lossless Compression
This provides a formal verification solution for developers implementing compression algorithms, particularly those based on asymmetric numeral systems, though it is incremental as it builds on existing reversible programming concepts.
The paper tackles the problem of ensuring correctness in lossless compression by introducing a reversible programming language called Flipper, embedded in Agda, which automatically generates verified encoder-decoder pairs with proofs of invertibility, demonstrated through a small example.
Lossless compression implementations typically contain two programs, an encoder and a decoder, which are required to be inverse to one another. We observe that a significant class of compression methods, based on asymmetric numeral systems (ANS), have shared structure between the encoder and decoder -- the decoder program is the 'reverse' of the encoder program -- allowing both to be simultaneously specified by a single, reversible function. To exploit this, we have implemented a small reversible language, embedded in Agda, which we call 'Flipper' (available at https://github.com/j-towns/flipper). Agda supports formal verification of program properties, and the compiler for our reversible language (which is implemented as an Agda macro), produces not just an encoder/decoder pair of functions but also a proof that they are inverse to one another. Thus users of the language get formal verification 'for free'. We give a small example use-case of Flipper in this paper, and plan to publish a full compression implementation soon.