Verified Reversible Programming for Verified Lossless Compression
James Townsend
Date: Wed, June 28, 2023
Time: 12:00
Room: Turing 0.E420
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.
Previous:
| An evaluation of algorithms for conversion checking
Next:
Sára Juhošová | Bringing Formal Verification into Widespread Programming Language Ecosystems