一句话：用 Coq 策略从无冗余二进制格式规范自动推导互为逆的解码器与编码器，并重实现网络协议栈。
本文关注从二进制格式规范同时生成解码器与编码器的问题。尽管函数式 parser combinator 能快速构造解码器，但面对真实网络协议包格式时，既有方法通常难以处理，或需要在语法中手工添加冗余提示。作者提出 Narcissus，允许使用自然且无冗余的格式规范，并借助 Coq 证明助手与 tactic 自动推导解码器和编码器，且保证二者互为逆。该方法覆盖常见网络包格式，并已用于重新实现完整 Internet 协议栈的数据包处理，替换进基于 OCaml 的 MirageOS unikernel 中，性能下降很小。
It is a neat result from functional programming that libraries of parser combinators can support rapid construction of decoders for quite a range of formats. With a little more work, the same combinator program can denote both a decoder and an encoder. Unfortunately, the real world is full of gnarly formats, as with the packet formats that make up the standard Internet protocol stack. Most past parser-combinator approaches cannot handle these formats, and the few exceptions require redundancy – one part of the natural grammar needs to be hand-translated into hints in multiple parts of a parser program. We show how to recover very natural and nonredundant format specifications, covering all popular network packet formats and generating both decoders and encoders automatically. The catch is that we use the Coq proof assistant to derive both kinds of artifacts using tactics, automatically, in a way that guarantees that they form inverses of each other. We used our approach to reimplement packet processing for a full Internet protocol stack, inserting our replacement into the OCaml-based MirageOS unikernel, resulting in minimal performance degradation.
@article{paperbot580,
title = {Narcissus: correct-by-construction derivation of decoders and encoders from binary formats},
author = {Benjamin Delaware and Sorawit Suriyakarn and Clément Pit-Claudel and Qianchuan Ye and Adam Chlipala},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341686}
}