Verified Reversible Programming for Verified Lossless Compression
James Townsend, Jan-Willem van de Meent

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsNumerical Methods and Algorithms · Computability, Logic, AI Algorithms · Logic, programming, and type systems
