# A Coq Mechanization of JavaScript Regular Expression Semantics

Noé De Santo<EMAIL_ADDRESS>https://orcid.org/0009-0006-5119-3895
EPFLSwitzerland ,  Aurèle Barrière<EMAIL_ADDRESS>https://orcid.org/0000-0002-7297-2170 EPFLSwitzerland and  Clément Pit-Claudel
<EMAIL_ADDRESS>https://orcid.org/0000-0002-1900-3901
EPFLSwitzerland

###### Abstract.

We present an executable, proven-safe, faithful, and future-proof Coq
mechanization of JavaScript regular expression (regex) matching, as specified
by the last 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 spec 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 identifying 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 linked with Unicode libraries
to produce an executable engine that passes the relevant parts of the official
Test262 conformance test suite.

##  1\. Introduction

Like most modern programming languages, JavaScript natively offers a way to
write and match regular expressions (or regexes). These regexes are a
convenient tool for text processing — so convenient in fact that a large
proportion of JavaScript programs rely on them, including more than 30% of
JavaScript npm packages (Davis et al., 2018, 2021a). The JavaScript semantics
is described in an open standard, ECMAScript (ECMA, 2023), that specifies the
behavior of the entire language with pseudocode.

The regex part of ECMAScript is surprisingly subtle and complex. This
complexity comes from the presence of extended regex features not found in
traditional regular expressions (_capture groups_ , _backreferences_ ,
_lookarounds_ , _character classes_ , _lazy quantifiers_ , etc.; section 2),
but also from some unconventional choices in the design of these features:
even though other regex languages (like the ones in Python, Java, Go, Rust,
Perl) share some of them, they often have subtle semantic differences (Davis
et al., 2021a). For instance, JavaScript lookarounds are different from Java
lookarounds, and JavaScript quantifiers and capture groups have unique
semantics (Barrière and Pit-Claudel, 2023). To make matters worse, the
ECMAScript regex standard is in continuous evolution: every recent revision of
the standard contained significant additions to or refactorings of the regex
section, with dozens of individual edits every year (this churn has caused
Mozilla to abandon the development of its regular expression engine and switch
to V8’s Irregexp engine, the engine used in Google Chrome and NodeJS, to
better keep up with new features (Ireland, 2020)).

With all these features, JavaScript regex matching becomes significantly
different from traditional regular expression recognition. First, the addition
of backreferences changes the matching complexity from linear to NP-hard
(Dominus, 2000). Second, the addition of capture groups changes the problem
from recognition to segmentation: engines must not just compute whether a
pattern matches a string, but also where the match occurred and which
substrings were matched by each individual capture group (subexpressions in
parentheses; this process is called submatch extraction). For instance, when
matching the regex $a(b^{*}{})c$ on the string “abbcd”, an engine should
return that there is a match, but also that the regex matched the four first
characters “abbc” and that the capture group is defined and set to the value
“bb”. Supporting capture groups is very convenient, but it introduces
ambiguity in the matching problem: when there are several ways to match a
regex on a string, the language semantics must specify which way has highest
priority. In JavaScript, priority is given to the left branch of disjunctions.
For instance, matching the regex $(a\mathbin{|}{}ab)$ on string “ab” returns a
result that only matches the substring “a” (this is in line with PCRE leftmost
longest match semantics, but not with POSIX longest match semantics). This
disambiguation policy is particularly easy to implement — and to specify —
using a backtracking algorithm.

For all the reasons above, the ECMAScript specification describes the
JavaScript regex semantics with English pseudocode for a backtracking
algorithm. There are multiple issues with this approach.

First, the pseudocode is not executable. It cannot be used directly to
validate implementations of JavaScript, and it cannot be run to clarify
ambiguities or validate proposed test cases. As a result, bugs continue to be
found even in implementations of long-standing features (until recently, one
of the engines included in V8 contained bugs because of a misunderstanding of
the semantics of the Kleene star quantifier (Barrière and Pit-Claudel, 2023)).

Second, the length and style of this paper specification make it unsuitable
for formal reasoning. Mechanized semantics exist for substantial parts of the
ECMAScript standard (Park et al., 2020; Bodin et al., 2014; Politz et al.,
2012; Maffeis et al., 2008; Park et al., 2015), but none of them support
JavaScript regexes. As a result, previous work that tried to reason about
JavaScript regexes had to redefine their own models of the semantics (Chida
and Terauchi, 2023; Loring et al., 2019). Unfortunately, the published models
that we are aware off are incomplete, and we found mistakes in both of them
(section 2.4). To enable trustworthy formal reasoning about JavaScript
regexes, one needs a faithful, auditable transcription of the ECMAScript
pseudocode, without simplifications.

In that context, we present an executable, proven-safe, faithful and future-
proof Coq mechanization of ECMAScript regexes. By _executable_ , we mean that
we can extract our mechanization to OCaml and run it. By _proven-safe_ , we
mean that we have a Coq proof that the compilation and matching processes
described in the spec terminate and cannot trigger an assertion failure. By
_faithful_ , we mean that the mechanization conforms to the letter of the
specification and can be audited (it is written in such a way that one can
easily compare the pseudocode to the Coq definitions: we purposefully do not
attempt to simplify the specification or capture its core or essence), and
that it agrees with the spirit of the specification as understood by existing
implementations (we resolved ambiguities in line with the prevailing
consensus). Finally, by _future-proof_ , we mean that changes to the
ECMAScript pseudocode require changes of comparable size to the mechanization,
ensuring that it can be modified in the future as the standard evolves.

We claim the following contributions:

  * •

A shallow-embedded Coq mechanization We show that ECMAScript regex semantics
can be shallowly embed in Coq, and we describe the encoding techniques
required to represent exceptions, nonlocality, and possible nontermination in
that style (section 3). We match the original specification as closely as
possible: throughout the development, we interleave Coq code and English
statements so that one can easily audit the mechanization. We translate more
than 33 pages of pseudocode into Coq definitions.

  * •

Safety and termination proofs Using our mechanization, we prove the
correctness of several non-trivial properties of the ECMAScript regex
semantics, demonstrating that our mechanization enables formal reasoning about
JavaScript regexes. In section 4, we prove that the specification always
terminates and that it cannot crash. In the process, we surface and mechanize
crucial invariants.

  * •

A usable foundation for regex research We show that our mechanization style is
compatible with traditional program proofs and provides a usable formal
foundation for regular expression compilation and optimization research by
verifying a regex optimization excerpted from the Irregexp engine (section 5).

  * •

An executable ground-truth for JavaScript regexes We show that our
mechanization style is compatible with extraction to OCaml; link the result
with Unicode libraries, and show that we can plug it into a browser in a way
that passes all relevant standard tests, albeit slowly in some cases (section
6.1). To the best of our knowledge, this is the first time that a candidate
reference interpreter has been proposed for JavaScript regexes.

We start by giving a presentation of JavaScript regexes, their semantics, and
related work formalizing them in section 2. We then describe our mechanization
in section 3, highlighting the translation challenges that arise and the
encoding techniques that make a shallow embedding possible and scalable (an
error monad for failing operations of the specification, zipper contexts for
non-local operations, and a proven-correct fuel encoding for general
recursion). In section 4, we conjecture and formally verify a fundamental
invariant of the ECMAScript regex specification, and we use it to prove that
the specification always terminates and cannot fail. Then in section 5, we
present the formal verification of a regex transformation performed in
Irregexp. Finally, in section 6, we present evidence that our mechanization is
indeed executable, proven-safe, faithful, and future-proof. Specifically, we
explain how to use extraction to generate an executable OCaml engine, we show
that this engine can execute the Test262 official ECMAScript compliance test
suite, and we evaluate on an example the effort required to extend our
mechanization to support a new feature.

##  2\. Understanding ECMAScript Regexes

We begin this section with an overview of JavaScript regex features in section
2.1. We then describe their backtracking ECMAScript specification in section
2.2. In section 2.3, we give an informal explanation of a crucial property of
all the functions generated by the specification, that we mechanize later in
section 4 to prove properties about the semantics. Finally, in section 2.4, we
present some problems that we uncovered in previous formalizations of
JavaScript regexes and illustrate the semantic subtleties that led to them.

###  2.1. ECMAScript Regex Features

The ECMAScript standard for regexes includes not only standard regular
expression features (concatenation, disjunction, simple characters and simple
Kleene quantifiers like ∗ or +), but also a number of extended features (ECMA,
2023, Section 22.2). Figure 1 summarizes the syntax of most of these features
(we deviate from the plain-text JavaScript syntax in minor ways for
readability purposes: for example, we write $\epsilon$ instead of nothing at
all and $({?}{\leq}\ r)$ instead of (?<=r)).

Feature name | Explanation | Syntax
---|---|---
Empty regex |  | $\epsilon$
Character |  | a, b, c, \$n$, …
Character classes |  | [abc], [^A-Z], $\cdot$, \d, …
Concatenation |  | $r_{1}r_{2}$
Disjunction (union) |  | $r_{1}\mathbin{|}{}r_{2}$
Greedy quantifiers | (a) |  $r^{*}{}$, $r^{+}{}$, $r^{?}{}$, $r^{\\{n,n\\}}$, …
Lazy quantifiers | (a) |  $r^{*?}{}$, $r^{+?}{}$, $r^{??}{}$, $r^{\\{n,n\\}?}$, …
Capturing groups | (b) |  $(r)$, $(_{\textup{\scriptsize<$\mathit{id}$>}}r)$
Non-capturing groups | (c) | $({?}{:}\ r)$
Backreferences | (d) |  $\textbackslash{}p$, $\textbackslash{}\textup{$\mathit{id}$}$
Lookarounds | (e) |  $({?}{=}\ r)$, $({?}{\leq}\ r)$, $({?}{\not=}\ r)$, $({?}{\not\leq}\ r)$
Anchors | (f) |  $\textasciicircum{}{}$, $\mathdollar{}$, $\textbackslash{}\textup{b}{}$, $\textbackslash{}\textup{B}{}$

where $n$ is a nonnegative integer, $p$ is a positive integer, $\mathit{id}$
is a named group identifier (a string), $r$, $r_{1}$ and $r_{2}$ are regexes.

Figure 1. Features of the ECMAScript regex language.

We now explain some of the extended features relevant to the remainder of this
work, then contrast their semantics with those of the same features in other
languages.

  1. (a)

Quantifiers allow to specify that a regex should be matched repeatedly.
$e^{\\{a,b\\}}$ means that the regex $e$ should be matched between $a$ and $b$
times. If $b$ is not specified, then $e$ can be matched an unbounded number of
times. By definition $e^{*}{}=e^{\\{0,\\}}$, $e^{+}{}=e^{\\{1,\\}}$, and
$e^{?}{}=e^{\\{0,1\\}}$.

_Greedy_ quantifiers, like ∗, + and {a,b}, give priority to matching the inner
regex as many times as possible, while _Lazy_ quantifiers, like ∗?, +? or
{a,b}? give priority to matching the inner regex as few times as possible. To
avoid infinite repetitions, the JavaScript semantics forbids optional
repetitions of $e$ that match the empty string. For instance, when matching
$()^{+}{}$, the semantics allows only one iteration of the plus. This first
iteration is allowed (in fact, mandated), because the plus has one minimal
mandatory repetition. All further iterations, on the other hand, are
disallowed: they are optional, the body $()$ of the quantifier matches only
the empty string, and empty matches are not allowed for empty strings.

  2. (b)

Capturing groups Capture groups are used to record which part of the input
string matched each parens-delimited sub-group of the original regex. When a
regex matches a string, the engine must return not only the substring that was
matched by the entire regex, but also all the substrings that were last
matched by each capture group. For instance, consider the regex
$a^{*}{}(b^{*}{})(a^{*}{})$, with two capture groups, being matched on string
“abbaaac”. The expected result is that the entire regex matched the substring
“abbaaa”, that the first capture group $(b^{*}{})$ matched the substring “bb”
and that the second capture group $(a^{*}{})$ matched the substring “aaa”.
Capture groups are numbered from 1 in order of appearance of their left
parenthesis (this corresponds to a pre-order traversal of the AST). It is also
possible to name capture groups (e.g.
$a^{*}{}(_{\textup{\scriptsize<B>}}b^{*}{})(_{\textup{\scriptsize<A>}}a^{*}{})$):
this makes it possible to retrieve submatches by name and to refer to the
group by name in backreferences.

  3. (c)

Non-capturing groups _Non-capturing groups_ act as parentheses usually do in
mathematics: they override (or make explicit) operator priorities. For
instance, the ∗ quantifier is applied to $b$ in $ab^{*}{}$ but to $ab$ in
$({?}{:}\ ab)^{*}{}$.

  4. (d)

Backreferences _Backreferences_ match the text that was captured by an earlier
group. For instance, the regex
$(_{\textup{\scriptsize<A>}}a^{*}{})(_{\textup{\scriptsize<B>}}b^{*}{})\textbackslash{}\textup{A}$
matches strings of the form anbman (two sequences of ‘a’s of the same length
separated by a sequence of ‘b’s). Backreferences can also refer to unnamed
groups by index. For instance, $(a|b)\textbackslash{}\textup{1}$ matches “aa”
or “bb” but not “ab”. Referring to a yet-undefined capture group (for instance
for the regex $\textbackslash{}\textup{1}(a)$) is not an error: the
backreference matches the empty string.

  5. (e)

Lookarounds Lookarounds condition matching on the surrounding context (they
allow matching to proceed only if the preceding or following text matches
another regex). For instance, the regex $({?}{\not\leq}\
c)(_{\textup{\scriptsize<A>}}a^{*}{})(_{\textup{\scriptsize<B>}}b^{*}{})\textbackslash{}\textup{A}$
matches the same strings anbman as in the paragraph above, but only when not
preceded by a $c$. Similarly, $({?}{\leq}\
b)(_{\textup{\scriptsize<A>}}a^{*}{})(_{\textup{\scriptsize<B>}}b^{*}{})\textbackslash{}\textup{A}$
matches strings of the form anbman but only when preceded by a $b$
(lookarounds are _zero-width_ , meaning that the initial $b$ is not part of
the matched substring: the assertion only ensures that there is a $b$ before
the match). Lookarounds include both lookaheads and lookbehinds, and can be
either positive or negative.

  6. (f)

Anchors (sometimes also called _boundary assertions_) Just like lookarounds,
anchors condition the match on surrounding characters. $\textasciicircum{}{}$
and $\mathdollar{}$ assert that there are no characters before and after them
respectively. $\textbackslash{}\textup{b}{}$ asserts that either the character
before it or after is a word character, but the other is not. Word characters
are letters and numbers, or Unicode characters that are equivalent for case-
insentivity to letters and numbers (ECMA, 2023, Section 22.2.2.9.3).

##### ECMAScript flags

JavaScript regexes may be annotated with flags to configure the matching
process. Examples include the i flag to make the matching process case-
insensitive, the d flag to compute submatch positions, or the u flag to enable
Unicode mode (we give more details about this mode in section 6.1).

####  2.1.1. Comparison to other regex languages

While similar features are found in most other regex languages, each language
can make different choices of syntax and semantics (Davis et al., 2021a).
These differences can be as simple as not using the same syntax:
$\textbackslash{}\textup{A}$ is an anchor in languages like Python and PCRE
and in JavaScript with the u flag, but simply matches the character ‘A’ in
JavaScript without flags.

But these differences can also be much more subtle. For instance, capture
groups inside quantifiers have unique semantics in JavaScript (Barrière and
Pit-Claudel, 2023). Each time a quantifier is entered, the values of all
capture groups inside it are reset to undefined (ECMA, 2023, Section
22.2.2.3.1). This is specific to ECMAScript regexes, and it implies, for
instance, that matching the regex $({?}{:}\ (a)\mathbin{|}{}(b))^{*}$ on the
string “ab” defines group 2 ((b)) but not group 1 ($(a)$): the first iteration
of the start defines group 1, but upon entering the second iteration of the
loop all groups are reset and after the second iteration only ‘b’ is set.
Similarly, quantifiers that can match the empty string behave differently in
ECMAScript and in other regex languages (Barrière and Pit-Claudel, 2023).

###  2.2. ECMAScript Regex Matching

To understand our mechanization, we now present the inner workings of the
ECMAScript pseudocode algorithm. The specification divides the process of
matching a regex such as $(a)\mathbin{|}{}bc$ against an input string into
four steps: parsing, validation, compilation, and execution:

  1. (1)

Parsing (ECMA, 2023, Section 22.2.1) The textual representation of the regex
is turned into an _Abstract Syntax Tree_ (AST).

  2. (2)

Early errors (ECMA, 2023, Section 22.2.1.1) Regexes with undesirable
properties (called _early errors_) are rejected. Examples include:

     * •

$a^{\\{n,m\\}}$ when $n>m$;

     * •

$(_{\textup{\scriptsize<G>}}a)(_{\textup{\scriptsize<G>}}b)$ which defines the
group G twice;

     * •

$\textbackslash{}\textup{G}$ which has a dangling backreference: the group G
is never defined, yet is being referred to by the backreference.

  3. (3)

Compilation (ECMA, 2023, Section 22.2.2) The AST of the regex is transformed
into a matcher function which takes two arguments:  1 an input string, where
the regex tries to find a match  2 and an index (a position in the string), at
which the match should start  . This function returns either mismatch111Named
failure in the specification, but we prefer mismtach to avoid confusion with
assertion failures., indicating that no match was found, or a MatchState
(ECMA, 2023, 22.2.2.1) containing the input string, the index at which the
match ended, and a description of the capture groups defined during the
matching process.

  4. (4)

Execution (ECMA, 2023, Section 22.2.5) At a later point, when the user calls
one of the JavaScript RegExp API functions (match, matchAll, exec, etc.), the
generated matcher function is called through the RegExp.prototype.exec
function.

Our mechanization covers the last three: we delegate parsing to a preexisting
regex parsing library for reasons that we detail in section 6.1 (briefly: the
practice of browser vendors has diverged from the specification when it comes
to parsing). Our mechanization handles regexes described with an inductive
type, of which each constructor corresponds to a production rule of the
ECMAScript regex parsing grammar.

####  2.2.1. ECMAScript regex compilation and execution

Perhaps surprisingly, the paper specification ECMAScript regular expression
matching does not define an interpreter or an inductive matching relation.
Instead, the specification defines a compilation algorithm that transforms the
parsed regex AST into a matching function, and separately explains how to
execute the matching function on the input string.

Figure 2 summarizes the different types used by the regex specification.
MatchState represents the internal state of the backtracking engine. It
contains the original input string, the current position in that string
(called endIndex, an integer), as well as the capture indices of each group
that has already been defined (Captures, an array of indices). A MatchResult
is either the MatchState obtained at the end of a match or the special value
mismatch indicating that no match was found. A MatcherContinuation is a
function from a MatchState to a MatchResult. Finally, a Matcher is a function
taking a MatchState and a MatcherContinuation and returning a MatchResult.

MatchState | := | (String * endIndex * Captures)
---|---|---
MatchResult | := |  MatchState or mismatch
MatcherContinuation | := | MatchState $\rightarrow\;$ MatchResult
Matcher | := | MatchState $\rightarrow\;$ MatcherContinuation $\rightarrow\;$ MatchResult
Figure 2. Summary of the different types appearing in the compilation process.

The compilation is done by the compilePattern function (ECMA, 2023, 22.2.2.2),
with most of the work happening in compileSubPattern (ECMA, 2023, 22.2.2.3).
The Matcher’s first argument is its initial state. The second argument is a
continuation function used to continue the matching if this matcher succeeds
(initially, this continuation is the identity function). During the execution
of the matcher functions, this continuation function is used to encode regex
concatenation.

Let us illustrate the backtracking behavior on an example. Consider matching
the string “ab” with the regex $r_{1}=({?}{:}\ ({?}{:}\
ab)\mathbin{|}{}\cdot{})b$, whose AST is pictured in Figure 3. The dot $\cdot$
is a regex feature matching any single character. We write $m_{i}$ for the
matcher compiled from the regex $r_{i}$. A trace of the execution is showed in
Figure 4; we explain it here in more details.

[Concatenation, name=1 [Disjunction, name=2 [Concatenation, name=3 [$a$,
name=4] [$b$, name=5]] [$\cdot{}$, name=6]] [$b$, name=7] ] [left = 0.25cm of
1] (label_1) $r_{1}$; [-¿] (label_1) to[out = east, in = west] (1); [left =
0.25cm of 2] (label_2) $r_{2}$; [-¿] (label_2) to[out = east, in = west] (2);
[left = 0.25cm of 3] (label_3) $r_{3}$; [-¿] (label_3) to[out = east, in =
west] (3); [left = 0.25cm of 4] (label_4) $r_{4}$; [-¿] (label_4) to[out =
east, in = west] (4); [right = 0.25cm of 5] (label_5) $r_{5}$; [-¿] (label_5)
to[out = west, in = east] (5); [right = 0.25cm of 6] (label_6) $r_{6}$; [-¿]
(label_6) to[out = west, in = east] (6); [right = 0.25cm of 7] (label_7)
$r_{7}$; [-¿] (label_7) to[out = west, in = east] (7);

Figure 3. Abstract syntax tree of
$r_{1}=({?}{:}\ ({?}{:}\ ab)\mathbin{|}{}\cdot{})b$

  * •

Step 0 First, $m_{1}$ is called with a state x0 at index 0 and a trivial
continuation c0 (the identity).

  * •

Step 1 $r1$ is a concatenation: as such, its compiled matcher first creates a
new continuation c7. This continuation encodes the matching of the right side
of the concatenation ($r_{7}=b$). It uses the matcher of $r_{7}$ (m7) and the
initial continuation c0 it was called with. With this new definition, m1 calls
the matcher of its left-hand side (m2) with the new continuation c7.

  * •

Step 2 This matcher m2 is a disjunction. This is called a choice point: the
backtracking pseudocode must try the first alternative, and maybe backtrack to
try the other one. The matcher first calls the matcher of the left
alternative, m3 with continuation c7, to try to match $r_{3}=ab$ followed by
$r_{7}=b$.

  * •

Step 3 This matcher m3 is again a concatenation, so m4 is called with a new
continuation (c5), as in step 1.

  * •

Steps 4–5 m4 tries and succeeds in consuming an ‘a’. It advances the state,
yielding x1 at position 1, and calls its continuation c5 with it. This
continuation in turn invokes m5 x1 c7.

  * •

Steps 6–7 m5 tries and succeeds in consuming a ‘b’. It advances the state,
yielding x2 at position 2, and calls its continuation c7, which in turn
invokes m7 x2 c0. At this point, the execution successfully matched “ab” using
the left part of the disjunction. But now, it must match $r_{7}=b$.

  * •

Step 8 m7 tries to consume a ‘b’ but fails since the end of the string has
been reached. It hence returns mismatch.

  * •

Step 9: backtracking Since the call to m3 x0 c7 returned mismatch, we return
to the call of m2. It now attempts a match using m6, its right-hand side.

  * •

Steps 10-13 The process continues as before for a few steps. At the end, the
state x4 is returned, which indicates that a match has been found.

The recursive structure of the generated matchers makes it so that their call
stack acts as an implicit backtracking stack: every time a matcher has
multiple ways to match a regex (for instance for a disjunction or a
quantifier), it tries them one by one until one succeeds. In contrast, when
there is only one way to match, the matcher calls its continuation in tail
position.

Step |  Call stack |  States and continuations | TC | Comment
---|---|---|---|---
0 |  [] |  x0 := ab (position 0) |  | Initialization
|  |  c0 := fun s $\Rightarrow\;$ s |  |
1 |  [m1 x0 c0] |  c7 := fun s $\Rightarrow\;$ m7 s c0 | X | Concatenation
2 |  [m2 x0 c7] |  |  | Choice point (disjunction)
3 |  [m3 x0 c7, m2 x0 c7] |  c5 := fun s $\Rightarrow\;$ m5 s c7 | X | Concatenation
4 |  [m4 x0 c5, m2 x0 c7] |  x1 := ab (position 1) | X | Consumes “a”
5 |  [c5 x1, m2 x0 c7] |  | X |
6 |  [m5 x1 c7, m2 x0 c7] |  x2 := ab (position 2) | X | Consumes “b”
7 |  [c2 x2, m2 x0 c7] |  | X |
8 |  [m7 x2 c0, m2 x0 c7] |  |  | Cannot consume “b”
Match failed $\implies{}$ Backtracking to last choice point
9 |  [m2 x0 c7] |  | X |
10 |  [m6 x0 c7] |  | X |
11 |  [c7 x3] |  x3 := ab (position 1) | X | Consumes “a”
12 |  [m7 x3 c0] |  x4 := ab (position 2) | X | Consumes “b”
13 |  [c0 x4] |  |  | Returns x4

A “X” in the “TC” column indicates that a call in tail position is performed.
The underlined part of a MatchState indicates the characters which have
already been consumed.

Figure 4. Matching process for $r_{1}$ on input string “ab”.

###  2.3. Matcher Invariant

The details given above are enough to understand a key invariant of matcher
functions generated by the specification, which we conjectured and proved it
in the course of our mechanization effort.

Matcher Invariant: any call to a Matcher function with a state x and a
continuation c either returns a mismatch, or calls its continuation c on
another state y, such that the endIndex of y is greater or equal to the one of
x and that both x and y have the same input string.222In the particular case
of lookbehinds, this inequality can be reversed since lookbehinds traverse the
string backwards. We first omit the case of lookbehinds, then discuss it in
section 4.3. This particular control-flow is what allows regex concatenations
to be encoded as continuations.

This invariant is not only critical to understand the compilation process and
the generated matchers, but also to formally reason about them. We formalize
and prove this invariant in section 4, as it turns out to be instrumental to
some of our semantic property proofs.

###  2.4. Semantic Subtleties missed by previous JavaScript Regex
Formalization

We are the first to attempt a mechanization of the ECMAScript regex standard,
but not the first to attempt formal reasoning about JavaScript regexes: paper-
based formal models of ECMAScript regex matching have appeared in multiple
past publications (Loring et al., 2019; Chida and Terauchi, 2023). These
models are incomplete (missing features, such as lookbehinds (Loring et al.,
2019)). More worryingly, our efforts to faithfully mechanize the specification
revealed that these models are also incorrect. In this section, we illustrate
some of the most subtle issues.

##### Rewriting greedy and lazy quantifiers

Relatedly, both the model of (Loring et al., 2019) and one used for regex
repair (Chida and Terauchi, 2023) incorrectly handle greedy and lazy question
mark operators, ? and ??. They assume that $r^{?}{}$ can be equivalently
rewritten to $({?}{:}\ r\mathbin{|}{}\epsilon)$, and that $r^{??}{}$ can be
rewritten to the regex $({?}{:}\ \epsilon\mathbin{|}{}r)$, allowing them to
eliminate ? and ?? from the semantics.

Unfortunately, both of these transformations are incorrect in general. A
mismatch happens when $r$ can match the empty string while also changing the
captured groups.

###### $r^{?}{}$

For greedy question marks, consider the regex $r=()$, and compare the
semantics of $r^{?}{}$ and $({?}{:}\ r\mathbin{|}{}\epsilon)$ on the empty
string. In the $r^{?}{}$ case, the specification (section 2.1) allows at most
one optional iteration of $r$, but this iteration may not match the empty
string. Hence, the correct behavior is to not match $r$ at all (the quantifier
does 0 iterations). The final result simply matches the empty string and does
not define any capture groups. In contrast, $({?}{:}\ r\mathbin{|}{}\epsilon)$
allows $r$ to match the empty string. Hence, the correct behavior is to define
the first capture group (the one contained in $r$).

###### $r^{??}{}$

For lazy question marks, the reasoning is more subtle. Consider the regex
$r=({?}{=}\ (a))^{??}{}ab\textbackslash{}\textup{1}c$ being matched on string
“abac”. A compliant engine would not find a match. Matching would proceed as
follows: the engine would first skip the lazy quantifier (doing so, the first
capture group would not be defined), then consume “ab”, then match the empty
string with the backreference (backreferences to undefined group match the
empty string), and finally attempt to match “c”. Because the input is “abac”,
the last step would fail, and the engine would backtrack. Backtracking would
lead the engine to attempt to match the body of the lazy question mark and
define the capture group $(a)$. Unfortunately, because lookaheads are zero-
width, this would lead to an empty iteration of the quantifier, which the spec
disallows. Having exhausted all backtracking opportunities, a correct engine
would then return a match failure.

Rewriting the regex to $({?}{:}\ \epsilon\mathbin{|}{}({?}{=}\
(a)))ab\textbackslash{}\textup{1}c$ would not preserve this subtle behavior:
unlike the original regex, this one does matches “abac”. Taking the empty left
branch $\epsilon$ would not find a match, since it would not define the
capture group. The semantics then backtracks and takes the right branch of the
disjunction (unlike previously, this would now be allowed). Doing so, the
engine would go into the lookahead and set the first capture group to “a”.
With that, matching as a whole would (incorrectly) succeed.

##### Incorrect claims about infinite loops

It is sometimes mentioned (Sakuma et al., 2012) that JavaScript and RE2 have
the same way to prevent infinite looping in a star matching the empty string,
which is not true and can lead to different match results, for instance for
the regex $({?}{:}\ a^{?}{}b^{??}{})^{*}{}$ on string “ab” (Barrière and Pit-
Claudel, 2023).

##### Leveraging mechanized specs to validate simplified semantics

Although we quickly found a counterexample for the first transformation, we
initially believed that the second one was correct. We then tried using our
mechanization to formally verify it, and this attempt led us to the counter-
example above.

The official ECMAScript regex standard is verbose and complex: it is no
surprise that previously published models of JavaScript regular expressions
attempted to capture regex semantics in a more succinct and practical style
(Chida and Terauchi, 2023; Loring et al., 2019). We believe that style to be
preferable for formally reasoning about about regexes, but this cannot come at
the cost of correctness: to be trustworthy, formalizations of JavaScript
regexes must follow the ECMAScript standard to the letter and avoid
semantically incorrect simplifications.

We hope that our mechanization will provide foundations to _prove_ , rather
than posit, the correctness of more succinct, readable, and practical
specifications for JavaScript regex semantics.

##  3\. A Shallow-Embedded Coq Mechanization of ECMAScript Regexes

In this section, we present our Coq mechanization of the ECMAScript standard
for JavaScript regexes. This section presents a collection of encoding and
translation techniques that make a manual faithful shallow embedding possible
in Coq, and scalable to the size of the specification (about 33 printed
pages). Our main goal was to produce a mechanization as faithful and close as
possible to the original pseudocode specification, and we use two key
ingredients to ensure that.

##### Shallow embedding

First, we use a shallow embedding, where each function and type that appears
in the pseudocode is directly translated to a similar function or type in the
mechanization. This is the most natural and straightforward way to have an
equivalent mechanization.333Historical comments made by one of the original
authors of the ECMAScript regex specification (TC39, 2022) suggest that this
backtracking pseudocode may have been derived from a lambda-calculus-based
model. In that sense, mechanizing the specification in Coq may be returning it
to its roots.

##### Line-by-line auditability

Second, we interleave each line of our Coq mechanization with English
statements taken directly from the corresponding pseudocode in the ECMAScript
specification. We see two main benefits to this style. First, it eases the
burden of auditing our mechanization to check that it performs the same
operations as the ECMAScript standard. Figure 5 shows an example of how close
the two are once we define adequate notations and encodings. Second, it gives
us a measure of future-proofness: if the ECMAScript standard evolves (for
instance, by adding new regex features), this style ensures that changes to
our mechanization remain proportionate to the changes in the original
specification.

We first present in section 3.1 our solution to encode the potentially failing
operations used by the ECMAScript pseudocode in a pure Coq implementation.
Some operations are even _non-local_ : they refer to the parent or siblings of
the current AST node. We propose an adequate zipper encoding in section 3.2.
Another issue when defining Coq functions is that Coq enforces termination. In
section 3.3, we show how we encoded the loops and recursive functions used in
the standard.

(a) A sample of the specification.

⬇

(** Disjunction :: Alternative | Disjunction *)

| Disjunction r1 r2 $\Rightarrow\;$

(* 1. Let m1 be CompileSubpattern of Alternative with arguments rer and
direction. *)

let! m1 $=\\!\\!\ll\;$ compileSubPattern r1 (Disjunction_left r2 :: ctx) rer
direction in

(* 2. Let m2 be CompileSubpattern of Disjunction with arguments rer and
direction. *)

let! m2 $=\\!\\!\ll\;$ compileSubPattern r2 (Disjunction_right r1 :: ctx) rer
direction in

(* 3. Return a new Matcher with parameters (x, c) that captures m1 and m2 and
performs the following steps when called: *)

(fun (x: MatchState) (c: MatcherContinuation) $\Rightarrow\;$

(* a. Assert: x is a MatchState. *)

(* b. Assert: c is a MatcherContinuation. *)

(* c. Let r be m1(x, c). *)

let! r $=\\!\\!\ll\;$ m1 x c in

(* d. If r is not failure, return r. *)

if r is not failure then r else

(* e. Return m2(x, c). *)

m2 x c): Matcher

(b) Our mechanization of the sample above.

Figure 5. Comparison of the paper specification and our mechanization.

###  3.1. Faithfully encoding potentially failing pseudocode in Coq

In various places, the specification makes use of language features that are
not available in Gallina, the programming language of Coq. The most common
ones are _assertions_ and other potentially _failing_ operations. Assertions
are used extensively in the specification, but there is no such feature in
Gallina. One possible solution would be to ignore assertions entirely. In
fact, the ECMAScript standard itself states that:

> “Such assertions are used to make explicit algorithmic invariants that would
> otherwise be implicit. Such assertions add no additional semantic
> requirements and hence need not be checked by an implementation. They are
> used simply to clarify algorithms.” (ECMA, 2023, Section 5.2).

Instead of ignoring assertions, our approach consists in encoding assertions
within the Coq mechanization, using both the Coq type system and an error
monad. Assertions can be split into two categories:

  * •

Type assertions: assertions of the form Assert: x is a MatchState (e.g. Figure
5 step 3.a). For these, we use the type system of Gallina to ensure that the
assertion holds.

  * •

Other assertions: assertions such as Assert: xe $\leqslant\;$ ye are
implemented using the error monad.

This approach has multiple benefits. First, we keep the mechanization close to
the pseudocode specification. Second, it allows us to encode other potentially
failing operations of the specification, like accessing the arrays holding the
capture information in each MatchState. Third, keeping assertions helps
understand and reason formally about JavaScript regex behavior.

On the other hand, by adding assertions, we introduce potential failures where
the paper specification claimed that assertions add no additional semantic
requirements. Consequently, we go even further and prove, in Coq, (section
4.2) that all assertions always hold, and that other potentially failing
operations never fail.

##### Proving safety with an error monad

⬇

Inductive Result (S: Type) :=

| Success (s: S)

| Failure

| OutOfFuel.

Definition bind m f :=

match m with

| Success v $\Rightarrow\;$ f v

| Failure $\Rightarrow\;$ Failure

| OutOfFuel $\Rightarrow\;$ OutOfFuel

end.

⬇

Notation "’let!’ r ’$=\\!\\!\ll\;$’ y ’in’ z" :=

(bind y (fun r $\Rightarrow\;$ z)).

Notation "’assert!’ b ’;’ z" :=

(if (negb b) then Failure else z).

(* Non-exhaustive match *)

Notation "’destruct!’ r ’$\leftarrow\;$’ y ’in’ z" :=

(match y with

| r $\Rightarrow\;$ z

| _ $\Rightarrow\;$ Failure

end).

Figure 6. A simple error monad and its notations.

A simple error monad, as shown on Figure 6, can faithfully encode assertions
and other potentially failing operations of the specifications. Failure
represents assertion failures and other kinds of failing operations (array
accesses out of bounds), and OutOfFuel is a special case of failure that we
use when encoding potentially non-terminating functions (see section 3.3). The
bind notation allows chaining operations together and achieve a result that is
visually very close to the pseudocode specification, as demonstrated in Figure
5. Note that the specification also sometimes uses non-exhaustive pattern
matching (for instance, assuming that some match result is not a mismatch),
which can be encoded with our destruct! notation (and which we later prove
never to happen).

Every function of the specification is then wrapped in the error monad, from
the compilation phase (compilation can fail, for instance, if a backreference
referred to an undefined group) to the execution phase (the generated matcher
functions can fail, for instance, if they accessed the capture array of a
MatchState out of bounds).

All assertions of the ECMAScript standard were encoded either with type
annotations or within the error monad. All functions of the pseudocode
returning a value of type T and including potentially failing operations
instead return a result of type Result T in the Coq mechanization.

Figure 7. Modifying a list in the compilation of groups (ECMA, 2023,
22.2.2.7).

##### Avoiding mutation by recognizing specific usage patterns

Besides potential failures, the specification uses another imperative feature:
mutable lists. In general, we would need a special encoding to handle mutable
lists in a Coq mechanization. For instance, we could augment our monadic
encoding with a state monad, with a state holding the current value of each
mutable list. However, the regex specification only uses mutable lists in very
restricted cases, and they are always copied right before being modified. For
instance, when compiling capture groups (ECMA, 2023, Section 22.2.2.6), a list
is mutated at step 3.c.viii, but this list is a local copy which was done at
step 3.c.ii. These two instructions are shown on Figure 7. In that light, we
chose to only use functional immutable lists in our Coq mechanization. This
keeps the mechanization efforts simple to write and reason about while
following the spirit of the standard.

###  3.2. Encoding non-local operations with a zipper context

An implicit feature of the AST representation of regexes used by the
specification is that it is possible to navigate the AST upward, which in
particular allows it to retrieve the _root_ of the regex AST. This is used in
a few functions of the specification. For example, as mentioned earlier, the
index of a group is determined by counting the number of left parentheses
appearing before it in the whole AST. This is done by the
CountLeftCapturingParenthesesBefore function (ECMA, 2023, 22.2.1.3), shown in
Figure 8. Consider the regex $r=({?}{:}\ (a)\mathbin{|}{}(a))b$ defined in
Figure 9. CountLeftCapturingParenthesesBefore should return 0 when called on
its sub-regex $r_{1}$ (its first capture group), as no parentheses appear
above or to the left of it. When called on $r_{2}$ (its second capture group),
the function should return 1 as there is one parentheses on its left, namely
the one in $r_{1}$. This is one of the few functions in the ECMAScript regex
pseudocode that are specified with such high-level descriptions, and without
precise pseudocode instructions for each step.

Figure 8. Specification of the CountLeftCapturingParensBefore function (ECMA,
2023, 22.2.1.3)

This effectively means that regexes should include some form of context to
relate them to the full regex they belong to, so that this function becomes
feasible to implement. We model this pattern using zippers (Huet, 1997). The
zipper holds both the current AST node and its _context_ , allowing
reconstruction of the root regex. Additionally, comparing the context of two
regexes allows us to differentiate between two sub-regexes which are identical
but appear at different locations. Going back to the regex $r$, its child
$r_{2}$ is represented by a pair of the AST for $(a)$ and a context describing
that this sub-regex is located on the left of the top-level concatenation, and
then on the right of the disjunction: the context acts as a description of the
path from the child to the root of the regex. Additionally, since we also want
to be able to reconstruct the root regex, this path is augmented with all the
data necessary to perform the reconstruction: the contexts can be implemented
with a linked list of incomplete AST nodes. These contexts are depicted on the
right of Figure 9, where $\square$ shows the incomplete parts of each sub-
regex in their contexts. During compilation, as we traverse the AST of a
regex, we manually maintain the associated context of each visited sub-regex.

[Concatenation, name=root [Disjunction [$($Group$)$, name=g1 [$a$]]
[$($Group$)$, name=g2 [$a$]]] [$b$] ] [left = 0.5cm of root] (root_label) $r$
(root); [-¿] (root_label) to[out = east, in = west] (root); [left = 0.25cm of
g1] (g1_label) $r_{1}$; [-¿] (g1_label) to[out = east, in = west] (g1); [right
= 0.25cm of g2] (g2_label) $r_{2}$; [-¿] (g2_label) to[out = west, in = east]
(g2);

(a) A regex $r$.

for tree=text=gray, edge=gray, [$\square b$, name=root [$\square|(a)$
[$($Group$)$, name=g1,for tree=text=black, for descendants=edge=black,
[$a$]]]] [left = 0.5cm of g2] (g1_label) focus; [-¿] (g1_label) to[out = east,
in = west] (g1);

(b) The sub-regex $r_{1}$
and its context.

for tree=text=gray, edge=gray, [$\square b$, name=root [$(a)|\square$
[$($Group$)$, name=g2,for tree=text=black, for descendants=edge=black,
[$a$]]]] [right = 0.5cm of g2] (g2_label) focus; [-¿] (g2_label) to[out =
west, in = east] (g2);

(c) The sub-regex $r_{2}$
and its context.

Figure 9. A regex and its contextualized sub-regexes. Contexts are represented
in gray.

###  3.3. Handling arbitrary recursion

The termination of most functions in the specification derives directly from
the fact that these functions are structurally recursive on a regex. There
are, however, notable exceptions: the RepeatMatcher function (ECMA, 2023,
22.2.2.3.1) and some functions of section 22.2.23 (ECMA, 2023). Since these
are not structurally recursive, they are not accepted as-is by Coq, which
cannot ensure their termination.

There are multiple ways to encode non-terminating functions in Coq
developments, for instance using coinductive definitions. We opted for a
_fuel_ -based solution. As such, an extra fuel argument of type nat was added
to these functions. If the function is called with a positive amount of fuel,
then any subsequent recursive call is handed one unit fewer fuel; if the fuel
is zero, then the function fails and returns OutOfFuel. From Coq’s point of
view, the function is then structurally recursive on this extra argument, and
hence acceptable. Of course, this raises the question of whether there exists
an upper bound on the amount of fuel required to ensure that OutOfFuel is
never returned. In section 4.2, we provide such a bound as a function of the
regex and input string sizes, and formally prove in Coq that this amount of
fuel is sufficient to rule out all OutOfFuel failures. Given that termination
can be proved, we find this to be a very pleasant way to encode such non-
terminating functions (alternative encodings such as coinductive functions are
often perceived as much harder to reason about, and would force us to deviate
further from the original pseudocode).

##  4\. Deriving and Mechanizing New Semantic Properties: Validating the
ECMAScript Specification

The ECMAScript specification itself could be incorrect, in the sense that its
pseudocode could contain mistakes: for instance producing functions that crash
or do not terminate. In this section, we show that one crucial advantage of
our mechanization is that we can, for the first time, formally verify semantic
properties about the ECMAScript regex specification. In particular, we prove
that for any regex and any input string, the specification does not crash (no
assert instruction fail, and no arrays are accessed out of bounds) and that it
always terminates. Although these are natural properties that one could expect
from any regex specification, these can be quite difficult to infer just by
looking at the pseudocode. With our mechanization, we can prove these
properties in Coq with high assurance, and as a result validate the
correctness of the ECMAScript specification.

Historically, we first proved these two properties in Coq separately. However,
we realized that both properties were direct consequences of the stronger
matcher invariant that we informally described in section 2.3. We first show
our mechanized matcher invariant and show how it can be used to prove
termination and absence of failures. We present interesting cases of our proof
that the matcher invariant holds for any matcher generated by the
specification. Finally, in section 4.3, we present how the simplified notion
of progress we used throughout this paper can be generalized to a definition
that also accounts for lookbehinds traversing the string backwards and that we
used in our mechanization.

###  4.1. Mechanizing the Matcher Invariant

⬇

Definition matcher_invariant (m: Matcher) :=

(* For all valid state x & continuation c *)

$\forall\;$ x c, Valid x $\rightarrow\;$

(* then either there is no match or *)

(m x c = mismatch) \/

(* m produced a new valid state y which *)

($\exists\;$ y, valid y /\

(* is a progress with respect to x *)

x $\leqslant\;$ y /\

(* and was passed to c *)

m x c = c y).

Figure 10. Mechanized Matcher Invariant.

As explained in section 2.2, the matcher functions and the continuations
compiled by the ECMAScript standard follow a particular control-flow, where
each matcher function ends in a mismatch or in a call to its continuation.
This call to the continuation is performed on a matcher state whose endIndex
is greater or equal to the state given as argument to the matcher, meaning
that the matcher may have consumed some characters in the string before
calling its continuation. In other words, every result of a matcher function
call is either a mismatch or the result of calling its continuation after
having progressed in the string. As it turns out, this invariant can be used
to prove the termination and the absence of failures in the specification.

Once again, for presentation purposes we make the assumption that regexes only
ever traverse the string forward, from its beginning to its end. This
assumption is not true for lookbehinds (both positive and negative), which
traverse the string backwards. We discuss how our approach can be generalized
to both directions in section 4.3.

We first define the invariant in Coq as depicted in Figure 10. This invariant
also captures that matchers functions are only ever called on _valid_ states,
i.e. states such that their endIndex is a valid index of input. To encode this
notion of progress in the string, we define a relation between match states,
$\leqslant$, such that $x\leqslant y$ when x and y have the same input string
and endIndex(x) $\leq$ endIndex(y).

##### Proving the Matcher Invariant

With this definition, it is possible to prove that all matchers generated by
compiling a regex actually satisfy this invariant. We proved the theorem shown
on Figure 11. There are several challenges in proving this theorem, that we
explain in section 4.2.

⬇

Theorem compiled_regex_invariant :

(* For all compiled matcher m *)

$\forall\;$ r m, compileSubPattern r = Success m $\rightarrow\;$

early_errors r = OK $\rightarrow\;$

(* the matcher invariant holds for m. *)

matcher_invariant m.

Figure 11. Proving the Matcher Invariant.

##### ECMAScript Regex Properties

Two important non-trivial properties of the ECMAScript regex semantics can be
proved using the theorem of Figure 11: the fact that the functions generated
by the specification always _terminate_ (meaning that they never run out of
fuel), and that they _cannot fail_ (e.g. that the assertions always hold, and
that arrays and strings are never accessed out-of-bounds).

We state and prove the two theorem of Figure 12, where init_state is an
initial matcher state containing the string to match and starting at index 0,
and identity_cont is the continuation that always returns a success. The two
proofs are an immediate consequence of the compiled_regex_invariant theorem by
contradiction. If the call to a matcher resulted in a lack of fuel or a
failure, then because this result is not a mismatch, the continuation
identity_cont itself would result in a lack of fuel or a failure, which is a
contradiction.

Both termination and absence of failures are properties that one would expect
about the specification, but that one cannot check formally without a
mechanization. These proofs demonstrate that our mechanization enables for the
first time formal reasoning about the JavaScript regex semantics in a proof
assistant.

⬇

Theorem termination :

(* For all regex r and string s *)

$\forall\;$ r m s, compileSubPattern r = Success m $\rightarrow\;$

early_errors r = OK $\rightarrow\;$

(* the matcher cannot run out of fuel. *)

m (init_state s) (identity_cont) $\neq\;$ OutOfFuel.

⬇

Theorem no_failure :

(* For regex r and string s *)

$\forall\;$ r m s, compileSubPattern r = Success m $\rightarrow\;$

early_errors r = OK $\rightarrow\;$

(* the matcher cannot fail an assertion. *)

m (init_state s) (identity_cont) $\neq\;$ Failure.

Figure 12. Termination and No Failure mechanized theorems.

###  4.2. Proving Termination and Non-Failure

Proving termination and non-failure then amounts to proving the theorem of
Figure 11. This theorem can be proved by induction on regexes, but some cases
of the proof are more complex than others. In this section, we describe some
of the interesting cases.

##### Termination of the RepeatMatcher

To compile quantifiers, the ECMAScript standard defines a function
RepeatMatcher, which takes as argument a matcher function for the the inner
regex, and returns a matcher function for the quantified regex. We show in
Figure 13 a simplified version of our mechanization of this RepeatMatcher
function, for the special case of matching the quantifier
$e^{\\{\texttt{min},\\}}$, where m is the matcher function for $e$. In
essence, this function computes a new continuation d, which repeats the
matcher m as many times as possible and at least min times. The first min
repetitions are allowed to match the empty string, but subsequent repetitions
are required to make some progress in the string; otherwise endIndex(y) =
endIndex(x) and the continuation returns without performing any additional
recursive calls.

⬇

Definition RepeatMatcher (m: Matcher) (min: nat) (x: MatchState)

(c: MatcherContinuation) (fuel: nat) :=

match fuel with

| 0 $\Rightarrow\;$ out_of_fuel

| S fuel’ $\Rightarrow\;$

let d := fun (y: MatchState) $\Rightarrow\;$

if min = 0 and endIndex(y) = endIndex(x) then mismatch

else

let nextmin := if min = 0 then 0 else min - 1 in

RepeatMatcher m nextmin y c fuel’

in

if min $\neq\;$ 0 then m x d

else let z := m x d in

if z is not mismatch then z

else c x.

Figure 13. Simplified pseudocode of RepeatMatcher (ECMA, 2023, 22.2.2.3.1).

Recall (from section 3.3) that we used fuel to define this function in Coq, as
the function is not structurally recursive. Whenever we call this function, we
call it with an extra argument, its fuel. To be able to prove by induction on
the regex the theorem of Figure 11, in the particular case where the regex is
a quantifier, we have to prove as an intermediate theorem that we can compute
an initial fuel value to give to the RepeatMatcher such that it cannot run out
of fuel. We then state and prove the intermediate lemma described in Figure
14, using the bound $\textup{min}{}+\textup{remainingChars}(x)+1$ as initial
fuel, where $\textup{remainingChars}(x)$ is the number of characters in the
string which were not yet consumed in the match, i.e.
$\textup{remainingChars}(x)=\textup{length}(\textup{input}(x))-\textup{endIndex}(x)\geq{}0$.

Informally, this bound comes from the fact that each time the RepeatMatcher
iterates, either the value of min has decreased, or the matcher has made some
progress in the string (because the matcher invariant holds for m). In the
latter case, either m has not matched any character, and the RepeatMatcher
immediately terminates, or m has matched some characters and the number of
remaining characters decreases.

⬇

Lemma repeat_matcher_terminates :

$\forall\;$ m x c min,

(* for any continuation c that terminates *)

($\forall\;$ y, c y $\neq\;$ OutOfFuel) $\rightarrow\;$

(* for any matcher m with the invariant *)

matcher_invariant m $\rightarrow\;$

(* then the matcher constructed by RepeatMatcher terminates *)

RepeatMatcher m min x c (min+remainingChars(x)+1) $\neq\;$ OutOfFuel.

Figure 14. Mechanizing termination of the RepeatMatcher.

####  4.2.1. Absence of failures

When proving that the matcher invariant holds for any matcher function
generated by the specification, it is also required to prove that each
assertion holds. We highlight here two interesting cases.

  * •

Surprisingly, the notion of progress in the matcher invariant is not only
helpful for the termination of RepeatMatcher, but is also useful to show that
assertions cannot fail. For instance, this allows to prove that the assertion
at step 3.c.vi of the compilation of capture groups (ECMA, 2023, Section
22.2.2.7) holds when compiling capture groups, since the assertion tests that
progress has been made in the string.

  * •

When compiling a named backreference, the compilation function first finds all named capturing groups using that name, then asserts that this list contains exactly one element.  ⬇ (** AtomEscape :: k GroupName *) | AtomEsc (AtomEscape.GroupEsc gn) $\Rightarrow\;$ (*> 1. Let matchingGroupSpecifiers be GroupSpecifiersThatMatch(GroupName). <*) let matchingGroupSpecifiers := groupSpecifiersThatMatch self ctx gn in (*> 2. Assert: matchingGroupSpecifiers contains a single GroupSpecifier. <*) assert! (List.length matchingGroupSpecifiers =? 1)%nat ;

This assertion holds because the early errors phase rules out regexes defining
the same named capture group twice and regexes with a backreference to an
undefined capture group. As a result, we proved that compilation always
succeeds when the early errors phase succeeds, as follows:

⬇

Theorem early_errors_compile :

(* For all regexes without early errors *)

$\forall\;$ r, early_errors r = OK $\rightarrow\;$

(* compiling it to a matcher is a success *)

$\exists\;$ m, compileSubPattern r = Success m.

###  4.3. Generalizing Progress

Up to this point, our definition of the matcher invariant assumed that the
regex matcher functions always progress forward in the string. The proof we
presented that matchers satisfy the matcher invariant, from which both
termination and no failure followed, crucially relied on this property.

However, JavaScript regexes include lookbehinds, which traverse the string
backwards. In the actual specification, the compilation functions take an
additional parameter indicating the direction of the compiled matcher, i.e.
whether it should go through the input string forward or backward. This is
notably used when compiling lookbehinds: when compiling $({?}{\leq}\ r)$, $r$
is compiled with the direction set to backward, regardless of the direction
used when compiling the lookbehind. In our mechanization, we use a generalized
notion of progress $\leqslant$ that it is parameterized by a direction. In the
context of the termination of RepeatMatcher (section 4.2), the definition of
$\textup{remainingChars}(x)$ is also parametrized on the direction. Since the
repeated matcher always goes in the same direction, our termination argument
holds whether the matcher is going forward or backward.

##  5\. Formally Verifying an Optimization using our Mechanization

Mechanized semantics open the door to new research, and our mechanization of
ECMAScript regexes enables new possibilities for the first time. In this
section, we present a case study showing that our mechanization can be used to
formally verify regex optimizations that are used in widely deployed
JavaScript implementations like Irregexp.

As noted in section 2.4, the subtle JavaScript regex semantics invalidate many
natural and intuitive regex transformations that engines could use to simplify
regexes. V8’s Irregexp engine nonetheless performs regex rewriting during
parsing: it replaces $r^{*}{}$ with the empty regex $\epsilon$ whenever $r$
can only match the empty
string444https://github.com/v8/v8/blob/dd8d0b44d5d5b4bc3912026bf78f25ed3cafda1a/src/regexp/regexp-
parser.cc#L3201. In this section, we build upon our Coq mechanization of the
JavaScript semantics to provide a Coq proof that this optimization is correct.
Informally, this transformation is valid because iterations of a star that do
not consume any character in the string should be rejected by the star,
meaning that the only acceptable behavior of the star is to perform zero
iterations.

Our proof is conducted in four steps. We first define a syntax-directed
analysis of regexes, identifying regexes we call strictly nullable regexes,
that can only match the empty string. This analysis is depicted on Figure 15,
where $\mathit{SN}~{}r$ means that the regex $r$ is strictly nullable. We
include any anchors and lookaround. The definition is recursive for
disjunction, concatenation, quantifiers and groups. Note that strictly
nullable regexes can still look at the surrounding string with lookarounds or
anchors; lookarounds can even be used to capture non-empty strings, despite
not consuming any character from the input.

$\mathit{SN}~{}\epsilon$ $\mathit{SN}~{}\textasciicircum{}{}$
$\mathit{SN}~{}\mathdollar{}$ $\mathit{SN}~{}\textbackslash{}\textup{b}{}$
$\mathit{SN}~{}\textbackslash{}\textup{B}{}$

$\mathit{SN}~{}({?}{=}\ r)$ $\mathit{SN}~{}({?}{\not=}\ r)$
$\mathit{SN}~{}({?}{\leq}\ r)$ $\mathit{SN}~{}({?}{\not\leq}\ r)$

$\mathit{SN}~{}r_{1}\mathbin{|}{}r_{2}\mathit{SN}~{}r_{1}\quad\mathit{SN}~{}r_{2}$
$\mathit{SN}~{}r_{1}r_{2}\mathit{SN}~{}r_{1}\quad\mathit{SN}~{}r_{2}$

$\mathit{SN}~{}r^{\\{n,\\}}\mathit{SN}~{}r$
$\mathit{SN}~{}r^{\\{n,m\\}}\mathit{SN}~{}r$
$\mathit{SN}~{}r^{\\{n,\\}?}\mathit{SN}~{}r$
$\mathit{SN}~{}r^{\\{n,m\\}?}\mathit{SN}~{}r$

$\mathit{SN}~{}({?}{:}\ r)\mathit{SN}~{}r$ $\mathit{SN}~{}(r)\mathit{SN}~{}r$
$\mathit{SN}~{}(_{\textup{\scriptsize<name>}}r)\mathit{SN}~{}r$

Figure 15. Our strictly nullable analysis

In our second step, we define a property of the matcher functions of such
strictly nullable regexes. This property encodes the fact that such matcher
functions cannot make any progress in the string. This can be seen as a
stronger version of the matcher invariant mechanization of Figure 10, where
the endIndex inequality has been replaced by an equality. This is defined on
Figure 17.

⬇

Definition strictly_nullable_matcher (m: Matcher) :=

(* For all valid state x and continuation c *)

$\forall\;$ x c, Valid x $\rightarrow\;$

(* then either there is no match *)

(m x c = mismatch) \/

(* or m produced a new valid state y *)

($\exists\;$ y, valid y /\

(* which hasn’t made progress in the string *)

endIndex x = endIndex y /\

(* that is passed to c to complete the match. *)

m x c = c y).

Figure 16. Strictly Nullable Matcher definition.

⬇

Theorem strictly_nullable_analysis_correct:

$\forall\;$ (r:Regex) (m:Matcher),

strictly_nullable r = true $\rightarrow\;$

compileSubPattern r = Success m $\rightarrow\;$

strictly_nullable_matcher m.

Figure 17. Correctness of the $\mathit{SN}$ analysis.

In a third step, we can prove that every strictly nullable regex, according to
our analysis of the first step, is compiled to a strictly nullable matcher
according to our new definition. This theorem is shown in Figure 17. Its proof
proceeds by induction on the regex. It closely resembles the proof of the
theorem of Figure 11, except that we use the fact that the regex is strictly
nullable to show that the intermediate state y on which the continuation is
called has made no progress in the string.

Finally, we can conclude and prove that it is correct to replace $r^{*}{}$
with the empty regex when $r$ is strictly nullable. We prove the theorem on
Figure 18, showing that both $r^{*}{}$ and the empty regex are compiled to
equivalent matchers, returning the same results when called with the same
inputs.

⬇

Theorem strictly_nullable_same_matcher:

$\forall\;$ (r:Regex) (mstar: Matcher) (mempty: Matcher),

strictly_nullable r = true $\rightarrow\;$

compileSubPattern (Quantified r (Greedy Star)) = Success mstar $\rightarrow\;$

compileSubPattern Empty = Success mempty $\rightarrow\;$

$\forall\;$ x c, mstar x c = mempty x c.

Figure 18. Correctness of the strictly nullable optimization

Even simple, seemingly intuitive transformations can be incorrect in
JavaScript semantics (see section 2.4), and our Coq mechanization enables for
the first time the formal verification of regex engine optimizations. One
direction of possible future work could be to make the strictly nullable
analysis even more precise. Currently, backreferences are never considered
strictly nullable, and this is the case in both our analysis of Figure 15 and
in the V8
optimization555https://github.com/v8/v8/blob/74530c3ff422d6e10ece2d9b68f0caec74c94a63/src/regexp/regexp-
ast.h#L721. But when a backreference refers to a capture group whose body is
itself strictly nullable, then the backreference itself should be strictly
nullable. We believe that our analysis and proof could both be extended to
justify even more aggressive optimizations.

##  6\. Evaluation

We claim that our mechanization of ECMAScript regexes is proven-safe,
executable, faithful and future-proof. In this section, we evaluate each of
these adjectives.

First, section 4 has described that our mechanization is proven-safe. We have
formally verified that our mechanization cannot fail and terminates in around
two thousands lines of Coq. This is the first time that such a property is
proved for ECMAScript regexes.

###  6.1. An executable mechanization

Using Coq’s extraction mechanism (Letouzey, 2008), we can generate OCaml code
from our mechanization. This OCaml code (around three thousands lines of code)
can then be executed and constitutes an independent engine for JavaScript
regexes. We detail below interesting aspects of extracting our Coq code to a
full executable OCaml engine.

##### Parsing

To parse regular expressions, we decided not to mechanize the ECMAScript
semantics rules and turn them into parsing rules, but instead use an existing
JavaScript regex parser library, regexp-tree (Soshnikov, 2024). We use this
library to turn any string representing a regex into an AST in JSON format.
Our engine is then able to decode this JSON into its own representation of
regexes. Our choice of using an external library is motivated by the fact that
the ECMAScript regex parsing rules are too restrictive compared to what most
JavaScript implementations consider valid regexes. For instance, ] is not
considered to be a valid regex if one strictly follows the parsing rules, yet
modern JavaScript implementations like V8 or JavaScriptCore parse it as a
valid regex matching the character ]. Implementers of the Chakra JavaScript
engine previously reported the same issue when developing their own regex
engine (Wirfs-Brock, 2010). As JavaScript implementations try to follow the
parts we mechanized to the letter, but not parsing, the faithful translation
of the regex grammar rules is out-of-scope of our mechanization.

##### Unicode Support

JavaScript regexes support Unicode through the Unicode u flag. In JavaScript,
strings are encoded in UTF-16. Depending on the presence of this Unicode flag,
strings are then tokenized differently (ECMA, 2023, Section 22.2.2). When the
u flag is active, the input string is interpreted as a list of Unicode code
units. Otherwise, the input string is interpreted as a list of BMP codepoints.
As an example, ‘’ is a unicode character made of two code units in UTF-16
(0xD83D and 0xDC22). Matching this string with the regex $\cdot{}$ (matching a
single character) can produce two different results. When the unicode flag is
active, then the regex matches the entire string, considered to be a single
character. Otherwise, the regex matches only 0xD83D, and considers that the
string contains two distinct characters.

The parsing rules also differ depending on the u flag. For instance,
$\textbackslash A$ is a valid regex without the u flag, matching a ‘A’
character, but is an invalid regex with the u flag.

After parsing and string tokenization however, the behavior of the matcher
functions generated by the specification is similar in both cases. As such in
our mechanization, the Coq functions are parameterized by an abstract type
representing characters and functions manipulating characters (_e.g._ case
foldings for case-insensivity). We then provide two ways to instantiate this
parameter, one corresponding to regexes with the u flag, and one without.
During extraction, we provide OCaml implementations of these types and
functions. Without Unicode mode, characters are encoded with the uint16 type
from the integers library. In Unicode mode, characters use the int type (able
to represent any Unicode code point), and we use several OCaml libraries
(uucp, uutf) to implement character manipulation functions, like case
foldings.

For case foldings or Unicode properties, the ECMAScript specification
implicitely depends on independent external Unicode definitions. As such, our
Coq mechanization simply abstracts these definitions. To demonstrate the
practicality of this approach, we have instantiated most of these functions on
the OCaml side using existing Unicode libraries. We implemented all character
manipulation functions, and we added support for one of the \p property
classes as a sanity check.

###  6.2. A faithful mechanization

Despite the care which was put into following the specification to the letter,
in this section we show how we empirically rule out any mistakes as we
transformed the standard into a Coq development. To evaluate the faithfulness
of our mechanization, we used three different techniques: we wrote and
executed tests by hand, we performed differential fuzzing, and executed an
established test suite.

##### Differential fuzzing

We implemented a differential fuzzer to cross-validate the correctness of our
implementation with the Irregexp implementation from V8 (V8, 2024), using
randomly generated regexes and randomly generated strings. The regexes and
strings are generated on a small restricted alphabet of a few characters to
improve the chances of finding matches. Our tests use randomly generated flags
and start at random positions in the string. When comparing the results of our
extracted engine and of Irregexp, we compare the value of every match and
every capture group.

In this process, we directly generate regexes ASTs, meaning that our fuzzer
does not test the parser but rather the three phases of section 2.2 that we
mechanized in Coq. After thousands of such random tests, our extracted Ocaml
engine has agreed with Irregexp on all tests.

##### Executing the Test262 suite

Test2622 (TC39, 2010) is the official ECMAScript test suite, for all of
JavaScript. As such, it contains regular expression tests. To ensure that we
faithfully mechanized the ECMAScript regex specification, we made sure that
the regex tests included in Test262 were correctly executed by our extracted
OCaml engine.

However, the regex tests of Test262 are not standalone tests that can be run
with a regex engine alone. Instead, Test262 defines full JavaScript programs
with assertions, and some of them thoroughly test regex matching. Our solution
was to use the V8 JavaScript engine, but intercept any calls to the
RegExp.prototype.exec function, and then resume the execution in V8 and check
if all assertions hold. To achieve this, we use test262-harness (Terlson,
2022) to launch all tests with a modified RegExp.prototype.exec function. This
function uses regexp-tree to parse the provided regex, and then invokes our
engine on this parsed regex and input string. Once our engine is done, the
function parses its output and returns it as the result of the match.

This way, we can check that 492 tests of Test262 using regexes hold. We detail
below tests that had to be excluded or failed:

  * •

There are some cases where matching with the extracted OCaml engine is so slow
(taking several hours) that they had to be excluded. These correspond to tests
where each possible Unicode character is checked to belong to a large set of
characters, for instance when testing the character classes like \D (3 tests)
or for Unicode property classes (588 tests). The specification uses
particularly slow algorithms for character classes, and so does our faithful
mechanization.

  * •

Some checks test for the prototype of the JavaScript objects returned by the
matcher (486 tests). As this is orthogonal to the matching process itself
(prototypes are a JavaScript language feature), our wrapper does not implement
those prototypes. We discard these tests.

  * •

We fail 6 tests of the form assertFalse(/[\u0390]/ui.test("\u1fd3")) for a few
unicode characters listed below. In these cases, Test262 itself is not up-to-
date with recent changes to Unicode dating from July
2023666https://www.unicode.org/L2/L2023/23076.htm#175-C19 that changed the
simple case folding rules of exactly these characters. More specifically,
these new Unicode changes state that some Unicode characters are now
equivalent for case-insensitivity matching. Just like ‘a’ is equivalent to ‘A’
for case-insentivity, ‘’ becomes equivalent to ‘’, ‘’ becomes equivalent to ‘’
and ‘’ becomes equivalent to ‘’. The regex specification uses these case
folding rules when matching unicode characters with the case-insensitivity
flag i and the unicode flag u. In fact, the regex implementations of V8 and
JavaScriptCore agree with our
behavior777https://bugs.chromium.org/p/v8/issues/detail?id=13377, and not the
one currently expected from the test. These tests were added to Test262 at a
time where these equivalences were not true. We intend to submit a patch
updating these tests to the new Unicode foldings definitions.

As we ran all tests, we encountered a few bugs in the regexp-tree parser
library. For instance, backreferences being incorrectly parsed as decimal
escapes888A previously reported bug:
https://github.com/DmitrySoshnikov/regexp-tree/issues/69, or the d not being
recognized. We wrote patches so that the library correctly parses all of
Test262, and intend to submit them to the main repository.

###  6.3. A future-proof mechanization

Since the ECMAScript specification is being updated every year, chances are
that parts of the regex specification will be modified as well, for instance
to include more regex features. Our mechanization can easily be modified as
the prose ECMAScript standard evolves. We claim that the changes required in
our mechanization should be in the same order of magnitude as the changes to
the pseudocode itself.

As a case study, we implemented the word boundary assertions, or _anchors_ ,
($\textasciicircum{}{}$, $\mathdollar{}$, $\textbackslash{}\textup{b}{}$ and
$\textbackslash{}\textup{B}{}$) after every other features. In this section,
we document which changes were needed to accommodate the introduction of
anchors into the specification.

The first step is to extend the Regex type to add the four new constructors
(one for each boundary assertion). Since these constructors are leaves of the
AST, there is no need to extend the Zipper with new context constructors.

Because we introduced new AST constructors, we are also required to update
some methods of section 2.2.1 such has CountLeftCapturingParensBefore as well
as CompileSubPattern, the main compilation function. Next, we need to
implement the new cases in CompileSubPattern to compile boundary assertions.
This process is made straightforward by our notations: most of the pseudo-code
can be transcribed almost literally, as shown in Figure 19. The most difficult
line to translate is the one for the case 1.e. The condition requires to index
the input string, which is an operation whose result is wrapped in the error
monad as explained in section 3.1. As such, its result must be unwrapped using
let! before passing it to CharSet.contains. We defined new boolean monadic
notations if!, &&! and ||! to encode such potentially failing conditions.

⬇

(** Assertion :: ^ *)

| AssertInputStart $\Rightarrow\;$

(* 1. Return a new Matcher with parameters (x, c) that captures rer and

performs the following steps when called: *)

(fun (x: MatchState) (c: MatcherContinuation) $\Rightarrow\;$

(* a. Assert: x is a MatchState. *)

(* b. Assert: c is a MatcherContinuation. *)

(* c. Let Input be x’s input. *)

let input := MatchState.input x in

(* d. Let e be x’s endIndex. *)

let e := MatchState.endIndex x in

(* e. If e = 0, or if rer.[[Multiline]] is true and the character

Input[e - 1] is matched by LineTerminator, then *)

if! (e =? 0)%Z ||! (

(RegExp.multiline rer is true) &&!

(let! c $=\\!\\!\ll\;$ input[(e-1)%Z] in CharSet.contains
CharSet.line_terminators c))

then

(* i. Return c(x). *)

c x

else

(* f. Return failure. *)

failure): Matcher

Figure 19. Extension of CompileSubPattern for the $\textbackslash{}\textup{b}$
construct.

The changes above are enough to fully add boundary assertions to the
semantics. We also adapted the proofs described in section 4 to these new
constructs. As boundary assertions are not particularly involved in
termination or failures, this only required a few additional lines of proofs.

One feature currently being added into the ECMAScript regex specification is
the new v flag. This flag has already been implemented in most JavaScript
implementations. It provides new Unicode features and improvements, like
Unicode properties of strings which extend the Unicode properties of
characters available through the u flag (V8, 2022). This flag should integrate
the standard in the next 2024 version. This case study has strengthened our
confidence that our mechanization will be straightforward to update when the v
flag is finally added in ECMAScript.

##  7\. Limitations and Future Work: Looking Ahead

We have formalized the ECMAScript regex matching process in its entirety, but
not the external data that it depends on (Unicode property tables and
character manipulation functions, although we link the latter at the OCaml
level, as shown in section 6.1) nor the APIs that expose it.

In our mechanization, we have included as a comment, for each Coq line, the
corresponding pseudocode line from the ECMAScript specification. To ensure
completeness of our mechanization, we could build a tool to extract these
comments and check that each and every line of the ECMAScript standard has
been translated.

##### Formal verification of regex engines

As future work, we believe that our mechanized semantics would constitute the
best specification for the correctness theorem of a formally verified
JavaScript regex engine. Some JavaScript engines employ techniques
fundamentally different than backtracking to avoid the particular cases where
backtracking has exponential time complexity. For instance, both the
Experimental engine in V8 (V8, 2021) and recent work on linear matching of
JavaScript regexes (Barrière and Pit-Claudel, 2023) use a technique known as
NFA simulation, which explores several paths in parallel. This approach is so
different from backtracking that subtle semantic bugs have been uncovered (V8,
2023). Proving the correctness of this approach using our mechanization as a
specification would provide high assurance that engines with linear-time
complexity can be used to match JavaScript regexes.

Backtracking implementations sometimes use more advanced optimizations than
the one we formally verified in section 5. For instance, Irregexp generates
native code when the same regex is being executed several time (V8, 2019), and
recent work has explored the use of memoization to speed up backtracking
engines even with modern extended regex features such as lookarounds or
backreferences (Davis et al., 2021b). One could also use our mechanization to
formally verify these techniques in Coq, for instance proving the correctness
of a native code compiler for JavaScript regexes, or proving the correctness
of an efficient memoized backtracking implementation.

Another kind of engines use regex derivatives. Derivatives (Brzozowski, 1964)
present an elegant way to define the semantics of standard regular
expressions. A recent addition to the .NET framework is a linear-time
derivatives-based engine for a subset of .NET regexes (without backreferences
or lookarounds) (Moseley et al., 2023). To our knowledge, no derivatives-based
engine exist for JavaScript regexes. One crucial step in defining a
derivatives-based engine is to use regex rewriting rules to group together
semantically equivalent regexes. In essence, for standard regular expressions,
this ensures that the algorithm explores a minimal equivalent automata . A
list of such rewriting rules for standard regular expressions (extended with
regex intersection, complement and the empty-set regex) is available in (Owens
et al., 2009, Section 4.1) and combining these rules has been proven to make
the set of derivatives (up to equivalence) finite. However, for JavaScript
regexes, we have already used our executable engine to show that several of
these rules are incorrect in JavaScript, as shown on Figure 20. For the first
rule, deleting branches may change the index of capture groups. For the second
one, disjunction is notoriously non-commutative in JavaScript because the left
branch has higher priority than the right one. This raises a new open
question: is it possible to find a combination of rewriting rules leading to
the same finiteness result for JavaScript regexes? If there is, we believe we
could use our mechanization to formally verify each transformation, just like
we did in section 5.

Derivative equivalence rules (Owens et al., 2009)
---
Rewriting Rule |  | JavaScript Counter-example
$r\mathbin{|}{}r$ | $\equiv$ |  $r$ |  $({?}{:}\ (a)\mathbin{|}{}(a))\textbackslash{}\textup{2}()\$$ on string “aa”.
$r_{1}\mathbin{|}{}r_{2}$ | $\equiv$ |  $r_{2}\mathbin{|}{}r_{1}$ |  $a\mathbin{|}{}ab$ on string “ab”.

Rules from (Loring et al., 2019; Chida and Terauchi, 2023) (see section 2.4)
---
Rewriting Rule |  | JavaScript Counter-example
$r^{?}{}$ | $\equiv$ |  $r\mathbin{|}{}\epsilon$ |  $()^{?}{}$ on the empty string .
$r^{??}{}$ | $\equiv$ |  $\epsilon\mathbin{|}{}r$ |  $({?}{=}\ (a))^{??}{}ab\textbackslash{}\textup{1}c$ on string “abac”.

Figure 20. Counter-examples to standard regular expression rewriting rules we
found during our mechanization.

##### Formal verification of other JavaScript regex semantics

Previous work reasoning about JavaScript regexes (Loring et al., 2019; Chida
and Terauchi, 2023) have preferred a more denotational style of semantics,
rather than mimicking the operational backtacking algorithm of the ECMAScript
specification. We believe that these models could benefit greatly from our
mechanization by being proved equivalent to it in Coq. Similarly, the
transducers semantics of (Chen et al., 2022) have been tested against
JavaScript semantics, and with our mechanization we could prove that the
semantics are in fact equivalent.

##### Completing an existing JavaScript mechanization

Our mechanization could be used to complete the JSCert (Bodin et al., 2014)
JavaScript mechanization in Coq. To do so, we would also need to mechanize
some regex API functions that call our RegExp.prototype.exec function. As an
experiment, we already mechanized the search, test, match and matchAll
functions, and included these functions in our differential fuzzer. Our
specification style seemed to work just as well for these functions as for the
regex matching specification. We did not attempt to mechanize replace and
split, because they call out to more generic functions about strings defined
in other chapters of the ECMAScript specification.

##  8\. Related Work

##### JavaScript Mechanizations

Several works have tackled the mechanization of the ECMAScript standard.
However, none of them covered the regex chapter. The common explanation is
that the style used to define the regex semantics is quite different from the
style used in other chapters999Personal communication.

For instance, the JSCert project (Bodin et al., 2014; Charguéraud et al.,
2018) manually translated most of the ECMAScript 5 specification into Coq
definitions. Just like in our case, JSCert can then extract these Coq
definitions to OCaml to obtain a reference interpreter, JSRef. JSCert models
the complex control-flow of JavaScript semantics using pretty-big-step
semantics (Charguéraud, 2013), and also uses monadic operators to encode
possibly failing operations. Our monadic definitions are more specialized to
the kind of failures that occur in the regex chapter. An interesting direction
for further work would consist in combining the JSCert development with our
regex mechanization.

Instead of manually translating ECMAScript pseudocode, the ESMeta project uses
JISET, an automatic translator, to transpile ECMAScript pseudocode into a
custom intermediate representation (Park et al., 2020). This allows the
mechanization to be updated almost automatically when the ECMAScript standard
evolves. This intermediate representation can then be used to define
differential testers (Park et al., 2021b) and static analysers (Park et al.,
2021a, 2022) for JavaScript. Despite JISET being able to translate more than
90% of the ECMAScript standard automatically, it also does not support the
regex chapter (here, too, this is due to the peculiarities of the regex
specification). Unfortunately, it also does not support generation of
definitions suitable for use in an interactive theorem prover such as Coq. To
be able to rebuild our work on top of ESMeta, we would need to extend the
JISET intermediate representation and translator to work with the regex
specification style, and to add a translator from it to Coq; this could
constitute interesting future work, and we hope that this paper would provide
a good ground truth to evaluate against.

##### Regex Formalizations

Other than related work formalizing JavaScript regexes (Loring et al., 2019;
Chida and Terauchi, 2023) (see section 2.4), there has been numerous
formalizations of other regex languages, with various combinations of
features. We present a selection of different semantic choices here, although
the list is not exhaustive.

A formal model of a subset of .NET regexes has been presented in (Moseley et
al., 2023), where the semantics are defined using derivatives extended with
locations to support features like anchors and lookarounds. A similar approach
has recently been mechanized in Lean (Zhuchko et al., 2024) for regexes with
lookarounds and POSIX longest match semantics. Using derivatives to define the
semantics of lookahead had been previously investigated in (Miyazaki and
Minamide, 2019). In contrast with JavaScript regexes, these models do not
include capture groups and backreferences.

There has also been different definitions of regex semantics using
transducers, either prioritized finite transducers (PFTs) (Berglund and van
der Merwe, 2017a; Berglund et al., 2014) and later prioritized streaming
string transducers (PSSTs) (Chen et al., 2022). Using PSSTs has allowed not
only to define semantics for regexes with capture groups, but also to define
semantics API functions like replace or replaceAll. While these API functions
are not part of our mechanization (see section 7), this model does not support
lookarounds and backreferences.

The semantics proposed in (Chida and Terauchi, 2022) support a combination of
capture groups, lookahead and backreferences, to prove theorems about the
expressive power of combining these features. Interestingly, the combination
of lookaheads and backreferences raises new semantic design choices, and these
semantics are different than in JavaScript. In JavaScript, lookaheads are
atomic (see (ECMA, 2023, 22.2.2.4, Note 3)), meaning that if there are several
ways to match a lookahead, only the first one will be tried and a
backreference cannot cause the engine to backtrack inside a lookahead.

##### Regex Semantics

Differences between regex languages have been studied in various contexts. A
number of syntactic and semantic differences have been documented in (Davis et
al., 2021a) for JavaScript, Java, PHP, Python, Ruby, Go, Perl and Rust
regexes, with JavaScript being different from all others in several cases.
That study already presented the JavaScript peculiarities of section 2.1.1,
but not the first, third and fourth counter-examples of Figure 20. Recently,
algorithms for matching a large subset of JavaScript regexes in linear time
have been presented (Barrière and Pit-Claudel, 2023), showing that
misunderstandings of quantifier semantics (see section 2.1) have caused bugs
in V8. Unfortunately, the algorithms of (Barrière and Pit-Claudel, 2023) are
presented without proofs or formal models of regexes. For the semantics of
backreferences, there are significant differences in different languages.
Backreferences can either match the empty string or nothing when the
corresponding group is undefined, and some languages can allow multiple
definitions of named groups with the same name. In (Berglund and van der
Merwe, 2017b), it was shown how these different semantics have an impact on
the expressivity of the regex language. JavaScript backreferences correspond
to their No-label repetitions, $\epsilon$-semantics category.

##  9\. Conclusion

We presented an executable, proven-safe, faithful and future-proof Coq
mechanization. We have shown that with the right combination of encoding
techniques, a manual shallow embedding of the ECMAScript backtracking
algorithm is possible in Coq and can scale to the size of the specification.
We additionally proved that the specification is safe, in the sense that it
does always terminate and that failures never occur, some properties that
could never have been formally verified without a mechanization. Our work can
be used to conduct more proofs about JavaScript regex semantics, for instance
proving the correctness of optimizations used in widely deployed
implementations. Finally, our development can be extracted to OCaml, providing
an executable OCaml engine. We validated the correctness of this engine with
the Test262 official conformance test suite and cross-validated it with the V8
Irregexp engine bundled with NodeJS and Google Chrome. To our knowledge, this
is the first mechanization of the ECMAScript specification of regexes in a
proof assistant.

This work lays the foundations for future formal work about this regex
language. In particular, we hope it will allow proving the correctness of
alternative matching algorithms and rewriting-based optimizations for regexes.
We also hope this will help researchers restate the semantics in a way that
better suits their field, without sacrificing the assurance that these new
formulations correctly reflect the ECMAScript regex language.

## References

  * (1)
  * Barrière and Pit-Claudel (2023) Aurèle Barrière and Clément Pit-Claudel. 2023\.  Linear Matching of JavaScript Regular Expressions.  _CoRR_ abs/2311.17620 (2023).  https://doi.org/10.48550/ARXIV.2311.17620 arXiv:2311.17620
  * Berglund et al. (2014) Martin Berglund, Frank Drewes, and Brink van der Merwe. 2014\.  Analyzing Catastrophic Backtracking Behavior in Practical Regular Expression Matching. In _Proceedings 14th International Conference on Automata and Formal Languages, AFL 2014, Szeged, Hungary, May 27-29, 2014_ _(EPTCS, Vol. 151)_ , Zoltán Ésik and Zoltán Fülöp (Eds.). 109–123.  https://doi.org/10.4204/EPTCS.151.7
  * Berglund and van der Merwe (2017a) Martin Berglund and Brink van der Merwe. 2017a.  On the semantics of regular expression parsing in the wild.  _Theor. Comput. Sci._ 679 (2017), 69–82.  https://doi.org/10.1016/J.TCS.2016.09.006
  * Berglund and van der Merwe (2017b) Martin Berglund and Brink van der Merwe. 2017b.  Regular Expressions with Backreferences Re-examined. In _Proceedings of the Prague Stringology Conference 2017, Prague, Czech Republic, August 28-30, 2017_ , Jan Holub and Jan Zdárek (Eds.). Department of Theoretical Computer Science, Faculty of Information Technology, Czech Technical University in Prague, 30–41.  http://www.stringology.org/event/2017/p04.html
  * Bodin et al. (2014) Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, and Gareth Smith. 2014.  A Trusted Mechanised JavaScript Specification. In _The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014_ , Suresh Jagannathan and Peter Sewell (Eds.). ACM, 87–100.  https://doi.org/10.1145/2535838.2535876
  * Brzozowski (1964) Janusz A. Brzozowski. 1964\.  Derivatives of Regular Expressions.  _J. ACM_ 11, 4 (1964), 481–494.  https://doi.org/10.1145/321239.321249
  * Charguéraud (2013) Arthur Charguéraud. 2013\.  Pretty-Big-Step Semantics. In _Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings_ _(Lecture Notes in Computer Science, Vol. 7792)_ , Matthias Felleisen and Philippa Gardner (Eds.). Springer, 41–60.  https://doi.org/10.1007/978-3-642-37036-6_3
  * Charguéraud et al. (2018) Arthur Charguéraud, Alan Schmitt, and Thomas Wood. 2018\.  JSExplain: A Double Debugger for JavaScript. In _Companion of the The Web Conference 2018 on The Web Conference 2018, WWW 2018, Lyon , France, April 23-27, 2018_ , Pierre-Antoine Champin, Fabien Gandon, Mounia Lalmas, and Panagiotis G. Ipeirotis (Eds.). ACM, 691–699.  https://doi.org/10.1145/3184558.3185969
  * Chen et al. (2022) Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. 2022.  Solving string constraints with Regex-dependent functions through transducers with priorities and variables.  _Proc. ACM Program. Lang._ 6, POPL (2022), 1–31.  https://doi.org/10.1145/3498707
  * Chida and Terauchi (2022) Nariyoshi Chida and Tachio Terauchi. 2022.  On Lookaheads in Regular Expressions with Backreferences. In _7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, August 2-5, 2022, Haifa, Israel_ _(LIPIcs, Vol. 228)_ , Amy P. Felty (Ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 15:1–15:18.  https://doi.org/10.4230/LIPICS.FSCD.2022.15
  * Chida and Terauchi (2023) Nariyoshi Chida and Tachio Terauchi. 2023.  Repairing Regular Expressions for Extraction.  _Proc. ACM Program. Lang._ 7, PLDI (2023), 1633–1656.  https://doi.org/10.1145/3591287
  * Davis et al. (2018) James C. Davis, Christy A. Coghlan, Francisco Servant, and Dongyoon Lee. 2018.  The impact of regular expression denial of service (ReDoS) in practice: an empirical study at the ecosystem scale. In _Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2018, Lake Buena Vista, FL, USA, November 04-09, 2018_ , Gary T. Leavens, Alessandro Garcia, and Corina S. Pasareanu (Eds.). ACM, 246–256.  https://doi.org/10.1145/3236024.3236027
  * Davis et al. (2021a) James C. Davis, Louis G. Michael IV, Christy A. Coghlan, Francisco Servant, and Dongyoon Lee. 2021a.  Why Aren’t Regular Expressions a Lingua Franca? An Empirical Study on the Re-use and Portability of Regular Expressions.  (2021).  arXiv:2105.04397
  * Davis et al. (2021b) James C. Davis, Francisco Servant, and Dongyoon Lee. 2021b.  Using Selective Memoization to Defeat Regular Expression Denial of Service (ReDoS). In _42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021_. IEEE, 1–17.  https://doi.org/10.1109/SP40001.2021.00032
  * Dominus (2000) Mark Jason Dominus. 2000\.  Perl Regular Expression Matching is NP-Hard.  https://perl.plover.com/NPC/NPC-3SAT.html.
  * ECMA (2023) ECMA. 2023.  ECMA-262.  https://ecma-international.org/publications-and-standards/standards/ecma-262/
  * Huet (1997) Gérard Huet. 1997\.  The zipper.  _Journal of functional programming_ 7, 5 (1997), 549–554.
  * Ireland (2020) Iain Ireland. 2020\.  A New RegExp Engine in SpiderMonkey.  https://hacks.mozilla.org/2020/06/a-new-regexp-engine-in-spidermonkey/.
  * Letouzey (2008) Pierre Letouzey. 2008\.  Extraction in Coq: An Overview. In _Logic and Theory of Algorithms, 4th Conference on Computability in Europe, CiE 2008, Athens, Greece, June 15-20, 2008, Proceedings_ _(Lecture Notes in Computer Science, Vol. 5028)_ , Arnold Beckmann, Costas Dimitracopoulos, and Benedikt Löwe (Eds.). Springer, 359–369.  https://doi.org/10.1007/978-3-540-69407-6_39
  * Loring et al. (2019) Blake Loring, Duncan Mitchell, and Johannes Kinder. 2019\.  Sound Regular Expression Semantics for Dynamic Symbolic Execution of JavaScript. In _Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019_ , Kathryn S. McKinley and Kathleen Fisher (Eds.). ACM, 425–438.  https://doi.org/10.1145/3314221.3314645
  * Maffeis et al. (2008) Sergio Maffeis, John C. Mitchell, and Ankur Taly. 2008\.  An Operational Semantics for JavaScript. In _Programming Languages and Systems, 6th Asian Symposium, APLAS 2008, Bangalore, India, December 9-11, 2008. Proceedings_ _(Lecture Notes in Computer Science, Vol. 5356)_ , G. Ramalingam (Ed.). Springer, 307–325.  https://doi.org/10.1007/978-3-540-89330-1_22
  * Miyazaki and Minamide (2019) Takayuki Miyazaki and Yasuhiko Minamide. 2019.  Derivatives of Regular Expressions with Lookahead.  _J. Inf. Process._ 27 (2019), 422–430.  https://doi.org/10.2197/IPSJJIP.27.422
  * Moseley et al. (2023) Dan Moseley, Mario Nishio, Jose Perez Rodriguez, Olli Saarikivi, Stephen Toub, Margus Veanes, Tiki Wan, and Eric Xu. 2023\.  Derivative Based Nonbacktracking Real-World Regex Matching with Backtracking Semantics.  _Proc. ACM Program. Lang._ 7, PLDI (2023), 1026–1049.  https://doi.org/10.1145/3591262
  * Owens et al. (2009) Scott Owens, John Reppy, and Aaron Turon. 2009.  Regular-expression derivatives re-examined.  _Journal of Functional Programming_ 19, 2 (2009), 173–190.
  * Park et al. (2015) Daejun Park, Andrei Stefanescu, and Grigore Rosu. 2015\.  KJS: a complete formal semantics of JavaScript. In _Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015_ , David Grove and Stephen M. Blackburn (Eds.). ACM, 346–356.  https://doi.org/10.1145/2737924.2737991
  * Park et al. (2022) Jihyeok Park, Seungmin An, and Sukyoung Ryu. 2022.  Automatically deriving JavaScript static analyzers from specifications using Meta-level static analysis. In _Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2022, Singapore, Singapore, November 14-18, 2022_ , Abhik Roychoudhury, Cristian Cadar, and Miryung Kim (Eds.). ACM, 1022–1034.  https://doi.org/10.1145/3540250.3549097
  * Park et al. (2021a) Jihyeok Park, Seungmin An, Wonho Shin, Yusung Sim, and Sukyoung Ryu. 2021a.  JSTAR: JavaScript Specification Type Analyzer using Refinement. In _36th IEEE/ACM International Conference on Automated Software Engineering, ASE 2021, Melbourne, Australia, November 15-19, 2021_. IEEE, 606–616.  https://doi.org/10.1109/ASE51524.2021.9678781
  * Park et al. (2021b) Jihyeok Park, Seungmin An, Dongjun Youn, Gyeongwon Kim, and Sukyoung Ryu. 2021b.  JEST: N+1 -version Differential Testing of Both JavaScript Engines and Specification. In _43rd IEEE/ACM International Conference on Software Engineering, ICSE 2021, Madrid, Spain, 22-30 May 2021_. IEEE, 13–24.  https://doi.org/10.1109/ICSE43902.2021.00015
  * Park et al. (2020) Jihyeok Park, Jihee Park, Seungmin An, and Sukyoung Ryu. 2020\.  JISET: JavaScript IR-based Semantics Extraction Toolchain. In _35th IEEE/ACM International Conference on Automated Software Engineering, ASE 2020, Melbourne, Australia, September 21-25, 2020_. IEEE, 647–658.  https://doi.org/10.1145/3324884.3416632
  * Politz et al. (2012) J. G. Politz, B. S. Lerner, H. Q. de la Vallee, T. Nelson, A. Guha, M. Carroll, and S. Krishnamurthi. 2012.  Mechanized LambdaJS.  https://blog.brownplt.org/2012/06/04/lambdajs-coq.html.
  * Sakuma et al. (2012) Yuto Sakuma, Yasuhiko Minamide, and Andrei Voronkov. 2012\.  Translating regular expression matching into transducers.  _J. Appl. Log._ 10, 1 (2012), 32–51.  https://doi.org/10.1016/J.JAL.2011.11.003
  * Soshnikov (2024) Dmitry Soshnikov. 2024\.  Regular expressions processor in JavaScript.  https://github.com/DmitrySoshnikov/regexp-tree.
  * TC39 (2010) TC39. 2010.  test262.  {https://github.com/tc39/test262}
  * TC39 (2022) TC39. 2022.  TC39 Meeting Notes.  https://github.com/tc39/notes/blob/main/meetings/2022-01/jan-26.md.
  * Terlson (2022) Brian Terlson. 2022\.  Test262-Harness.  https://github.com/bterlson/test262-harness.
  * V8 (2019) V8. 2019.  Improving V8 regular expressions.  https://v8.dev/blog/regexp-tier-up.
  * V8 (2021) V8. 2021.  An Additional Non-backtracking RegExp Engine.  https://v8.dev/blog/non-backtracking-regexp.
  * V8 (2022) V8. 2022.  RegExp v flag with set notation and properties of strings.  https://v8.dev/features/regexp-v-flag.
  * V8 (2023) V8. 2023.  Issue 14098: [Regexp] Mismatch between the Experimental engine and the backtracking engine on empty repetitions.  https://bugs.chromium.org/p/v8/issues/detail?id=14098.
  * V8 (2024) V8. 2024.  The V8 JavaScript engine.  https://v8.dev/
  * Wirfs-Brock (2010) Allen Wirfs-Brock. 2010\.  Chakra: Interoperability Means More Than Just Standards.  https://learn.microsoft.com/en-us/archive/blogs/ie/chakra-interoperability-means-more-than-just-standards#whats-the-real-regular-expression-grammar.
  * Zhuchko et al. (2024) Ekaterina Zhuchko, Margus Veanes, and Gabriel Ebner. 2024\.  Lean Formalization of Extended Regular Expression Matching with Lookarounds. In _Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024_ , Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy (Eds.). ACM, 118–131.  https://doi.org/10.1145/3636501.3636959