Verified Reversible Programming for Verified Lossless Compression

TL;DR

This paper introduces 'Flipper', a reversible programming language embedded in Agda, enabling formal verification of lossless compression algorithms by ensuring encoder and decoder functions are inverses, simplifying correctness proofs.

Contribution

The paper presents a novel reversible language in Agda that automatically verifies encoder-decoder inverse properties for lossless compression methods.

Findings

Reversible language 'Flipper' supports formal verification of encoder-decoder pairs.

Implementation in Agda ensures correctness by construction.

Example use-case demonstrates practical applicability.

Abstract

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.