A Coq Mechanization of JavaScript Regular Expression Semantics

TL;DR

The paper tackles the challenge of safely and faithfully formalizing JavaScript regex semantics, a notoriously intricate and evolving portion of ECMAScript. It presents a shallow-embedded Coq mechanization that mirrors the ECMA-262 backtracking spec, with line-by-line auditability, an error-monad safety framework, a zipper-based encoding for nonlocal operations, and a fuel-based approach to termination. The authors prove termination and absence of failures, derive a matcher invariant to support reasoning, and validate an optimizer used in real engines, while enabling extraction to OCaml and JavaScript for executable testing with Test262 and differential fuzzing against Irregexp. This work establishes a robust, auditable reference for JS regex semantics that can guide future verification of engines and optimizations, and demonstrates practical executability through cross-language extraction and empirical validation.

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.

Figures (21)

• Figure 1: Features of the ECMAScript regex language.
• Figure 2: Summary of the different types appearing in the compilation process.
• Figure 3: Abstract syntax tree of $r_1 = ({?}{:}\ ({?}{:}\ \texttt{a}\texttt{b}) \mathbin{|}{} \cdot{})\texttt{b}$
• Figure 4: Matching process for $r_1$ on input string "ab".
• Figure 5: Comparison of the paper specification with our mechanization.