Verified Reversible Programming for Verified Lossless Compression

arXiv2211.09676MaRDI QIDQ6417606FDOQ6417606

Jan-Willem van de Meent, James Townsend

Publication date: 2 November 2022

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.

Has companion code repository: https://github.com/j-towns/flipper

This page was built for publication: Verified Reversible Programming for Verified Lossless Compression

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6417606)