论文标题
验证的可逆编程用于验证的无损压缩
Verified Reversible Programming for Verified Lossless Compression
论文作者
论文摘要
无损压缩实现通常包含两个程序，一个编码器和一个解码器，这些程序必须相互倒数。我们观察到，基于非对称数字系统（ANS）的一类重要类型的压缩方法在编码器和解码器之间具有共享结构 - 解码器程序是编码器程序的“反向” - 允许两者同时由单个可逆函数指定。为了利用这一点，我们实现了一种嵌入AGDA的小型可逆语言，我们称之为“ flipper”（可在https://github.com/j-towns/flipper上找到）。 AGDA支持对程序属性的形式验证，以及我们可逆语言的编译器（以AGDA宏的实现），不仅会产生编码器/解码器对的功能，而且还可以证明它们彼此相反。因此，该语言的用户“免费”获得正式验证。在本文中，我们给出了一个小示例flipper的用例，并计划很快发布完整的压缩实现。
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.
