A Verified Low-Level Formatting EDSL in Agda

Abstract

Data is of little use when it stays inside one program's memory -- almost always, information needs to be serialised for storage, or sent to other programs via a low-level interface. Binary storage format and communication protocol definitions strive to establish a precise description of files or messages in order to ensure senders and receivers will agree on their interpretation of their communication. Unfortunately, many standards rely on complex and potentially ambiguous descriptions, some purely textual, some based on C struct definitions, to accomplish this. As a result, there can be multiple subtly different implementations conforming to these specifications, leading to hard-to-find bugs. A more formal approach has the potential to avoid this issue by fixing formats rigidly.

Agda is a dependently typed total functional programming language and a proof assistant. We develop a domain-specific language embedded in Agda that is both precise enough to avoid any confusion and powerful enough to describe real-world formats and protocols. The former is ensured by a pair of encoding and decoding algorithms (a pretty-printer and a parser), accompanied by a proof that they are (half)inverses; the latter is demonstrated by describing the format of IPv4 packets in this EDSL.