A Coq Mechanization of JavaScript Regular Expression Semantics

TL;DR

This paper presents the first faithful mechanization of JavaScript regex semantics in Coq, enabling formal verification, analysis, and extraction of an executable regex engine aligned with the official specification.

Contribution

It introduces a verified, executable Coq model of JavaScript regex matching, addressing encoding challenges and corner cases, and demonstrating its practical utility and adaptability.

Findings

Proves JavaScript regex matching always terminates and is safe.

Identifies subtle corner cases and corrects previous misconceptions.

Demonstrates the mechanization can be extracted to executable code and integrated with Unicode libraries.

Abstract

We present an executable, proven-safe, faithful, and future-proof Coq mechanization of JavaScript regular expression (regex) matching, as specified by the latest published edition of ECMA-262 section 22.2. This is, to our knowledge, the first time that an industrial-strength regex language has been faithfully mechanized in an interactive theorem prover. We highlight interesting challenges that arose in the process (including issues of encoding, corner cases, and executability), and we document the steps that we took to ensure that the result is straightforwardly auditable and that our understanding of the specification aligns with existing implementations. We demonstrate the usability and versatility of the mechanization through a broad collection of analyses, case studies, and experiments: we prove that JavaScript regex matching always terminates and is safe (no assertion failures); we identify subtle corner cases that led to mistakes in previous publications; we verify an optimization extracted from a state-of-the-art regex engine; we show that some classic properties described in automata textbooks and used in derivatives-based matchers do not hold in JavaScript regexes; and we demonstrate that the cost of updating the mechanization to account for changes in the original specification is reasonably low. Our mechanization can be extracted to OCaml and JavaScript and linked with Unicode libraries to produce an executable regex engine that passes the relevant parts of the official Test262 conformance test suite.