Verified invertible lexer using regular expressions and DFAs

TL;DR

This work develops a formally verified lexer framework in Scala using Stainless to guarantee invertibility between token streams and their character representations. It implements two matchers, regex-based with Brzozowski derivatives and DFA-based, alongside a verified lexer that adheres to the maximal munch principle and a defined invertibility regime. The authors introduce two practical invertibility conditions for token streams, including a separator-based approach and a disjoint-use of characters between separator and non-separator rules, and prove corresponding theorems ensuring round-trip correctness under these constraints. The framework also explores optimizations (memoization and zipper representation) and detours (NFA/Computable Languages) to balance correctness with performance, providing multiple realizations (regex and DFA) to support extensibility and future verification. Overall, the work offers a rigorous, mechanically verified path from regular-language specification to executable, invertible lexers, with potential impact on secure and reversible data parsing pipelines.

Abstract

In this project, we explore the concept of invertibility applied to serialisation and lexing frameworks. Recall that, on one hand, serialisation is the process of taking a data structure and writing it to a bit array while parsing is the reverse operation, i.e., reading the bit array and constructing the data structure back. While lexing, on the other hand, is the process of reading a stream of characters and splitting them into tokens, by following a list of given rules. While used in different applications, both are similar in their abstract operation: they both take a list of simple characters and extract a more complex structure. Applications in which these two operations are used are different but they share a need for the invertibility of the process. For example, when tokenising a code file that was prettyprinted by a compiler, one would expect to get the same sequence of tokens. Similarly, when a spacecraft sends scientific data to the ground, one would expect the parsed data to be the same as the one serialised by the spacecraft. The idea of this project is to explore the idea of having a framework capable of generating parser/serialiser or lexer/prettyprinter pairs with a formally verified notion of invertibility. We first explore related works and frameworks. After that, we present our verified lexer framework developed in Scala and verified using the Stainless framework1. We explain the implementation choices we make and present the specifications and their proofs. The code of the lexer with the proofs is available on Github2. The main branch contains the regular expression (called regex from now on) matcher version and the verified Computable Languages while the dfa match branch contains the version using the DFA matcher.