# Verified Reversible Programming for Verified Lossless Compression

arXiv: https://arxiv.org/abs/2211.09676 · HTML: https://mlsanity.com/paper/2211.09676/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 8 of its 17 references that are in the map.
- First posted on arXiv 2 Nov 2022.

## Builds on (most cited first, 8 of 8)

- [Variational Diffusion Models](https://mlsanity.com/paper/2107.00630/) (2021)
- [Practical Lossless Compression with Latent Variables using Bits Back Coding](https://mlsanity.com/paper/1901.04866/) (2019)
- [Integer Discrete Flows and Lossless Compression](https://mlsanity.com/paper/1905.07376/) (2019)
- [Bit-Swap: Recursive Bits-Back Coding for Lossless Compression with Hierarchical Latent Variables](https://mlsanity.com/paper/1905.06845/) (2019)
- [HiLLoC: Lossless Image Compression with Hierarchical Latent Variable Models](https://mlsanity.com/paper/1912.09953/) (2019)
- [IDF++: Analyzing and Improving Integer Discrete Flows for Lossless Compression](https://mlsanity.com/paper/2006.12459/) (2020)
- [On the Out-of-distribution Generalization of Probabilistic Image Modelling](https://mlsanity.com/paper/2109.02639/) (2021)
- [Improving Lossless Compression Rates via Monte Carlo Bits-Back Coding](https://mlsanity.com/paper/2102.11086/) (2021)

## Abstract (arXiv)

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.