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.
