I-Regexp

The regex standard RFC 9485 "I-Regexp" was created in 2023 by C. Bormann and T. Bray with the goal of being a regex flavor that can be matched in linear time, is interoperable across programming language implementations, and yet expressive enough for most real-world uses. They do not support lookarounds, capture groups, or backreferences, and only offer a Boolean matching function (matching a regex only returns true when a regex matches the entire string, and does not return a substring).

An I-Regexp [RFC9485] is essentially defined as an XSD regex [XSD-2] (described below), with the exception of the following constructs:

• Character class subtraction: regexes like [a-z-[abc]] are not allowed (in XSD, this would match all the lowercase letters of the Latin alphabet except letters a, b and c)

• Multi-character escapes: for example, \s (matching white space characters) or \d (matching decimal digits characters) are not supported

• Unicode blocks: for example, \p{IsBasicLatin} (matching all Unicode code points between #x0000 and #x007F) is not allowed.

These features are not supported by I-Regexp because they either exhibit a large amount of variation between regex flavors (multi-character escapes), or are not compatible with severely constrained environments (Unicode blocks), or are mostly absent from parsing-regex dialects (character class subtraction) [RFC9485]. An I-Regexp must also fully support Unicode characters.

The I-Regexp specification describes a function to translate I-Regexps to ECMAScript regexes:

• every unescaped dot . outside character classes must be replaced by [^\n\r]

• the resulting regex should be enveloped in ^(?: and )$

• the resulting ECMAScript regex is to be interpreted as a Unicode pattern (u flag)

XSD regexes

XSD regexes are defined in the specification of the XML Schema language [XSD-2]. XSD regexes provide many standard features of regexes: concatenation, disjunction, simple characters, quantifiers (*, +, ?, {n,m}, {n,} and {n}). Moreover, XSD regexes are implicitly anchored at the head and tail, hence anchor specifiers ^ and $ are not supported.

XSD Regex Syntax

We modeled grammar rules with an inductive type in Rocq. For example the main type for an XSD regex is the following:

Inductive XSDRegex : Type :=
   | Empty
   | Char (c: Character.type)
   | CharacterClass (cc: CharClass)
   | Sequence (r1 r2: XSDRegex)
   | Disjunction (r1 r2: XSDRegex)
   | Quantified (r: XSDRegex) (q: Quantifier).

Moreover, for our mechanization to be as auditable and faithful as possible, we added comments from the spec in all of our mechanization. So this snippet is actually written in the following way:

Inductive XSDRegex : Type :=
   (** >> (empty string) <<*)
   | Empty

   (** >> [Definition:] An atom is either a ·normal character·,
   a ·character class·, or a parenthesized ·regular expression·. <<*)
   (** >> [9] atom ::= Char | charClass | ( '(' regExp ')' ) <<*)
   (** >> [Definition:] A normal character is any XML character
   that is not a metacharacter. <<*)
   (** >> [10] Char ::= [^.\?*+()|#x5B#x5D] <<*)
   | Char (c: Character.type)
   (** >> [Definition:] A character class is an ·atom·  R
   that identifies a set of characters  C(R). <<*)
   (** >> [11] charClass ::= charClassEsc | charClassExpr | WildcardEsc <<*)
   | CharacterClass (cc: CharClass)

   (** >> [Definition:] A branch consists of zero or more ·piece·s,
   concatenated together. <<*)
   (** >> [2] branch ::= piece* <<*)
   | Sequence (r1 r2: XSDRegex)

   (** >> [Definition:]  A regular expression is composed from zero
   or more ·branch·es, separated by | characters. <<*)
   (** >> [1] regExp ::= branch ( '|' branch )* <<*)
   | Disjunction (r1 r2: XSDRegex)

   (** >> [Definition:] A piece is an ·atom·, possibly followed by a ·quantifier·. <<*)
   (** >> [3] piece ::= atom quantifier? <<*)
   | Quantified (r: XSDRegex) (q: Quantifier).

Each comment is directly taken from the XSD specification. This mechanization style, inspired by Warblre [Warblre_DeSanto+ICFP24], helps a reader check that all the rules in the specification were correctly translated to Rocq. All these grammar rules are mechanized in the file Patterns.v.

XSD Regex Semantics

We then mechanized the tables describing the semantics of each term (see example above) using inductively defined propositions, in file Semantics.v. The main one being xsdregex_match, which describes what it means for an XSD regex to match a string.

Reserved Notation "s =~ r" (at level 80).

Inductive xsdregex_match : list Character.type -> XSDRegex -> Prop :=
   | MEmpty :
       [] =~ Empty
   | MChar c :
       [c] =~ (Char c)
   | MCharClass c C
       (H : char_in_class c C) :
       [c] =~ (CharacterClass C)
   | MSequence s t S_p T_b
       (H1 : s =~ S_p)
       (H2 : t =~ T_b) :
       (s ++ t) =~ (Sequence S_p T_b)
   | MDisjunctionLeft str S_b T_r
       (H : str =~ S_b) :
       str =~ (Disjunction S_b T_r)
   | MDisjunctionRight str S_b T_r
       (H : str =~ T_r) :
       str =~ (Disjunction S_b T_r)
   | MStarQuestion str S_a
       (H : str =~ (Quantified S_a Question)) :
       str =~ (Quantified S_a Star)
   | MStarS s t S_a
       (H1 : s =~ (Quantified S_a Star))
       (H2 : t =~ S_a) :
       (s ++ t) =~ (Quantified S_a Star)
   | MPlus s t S_a
       (H1 : s =~ S_a)
       (H2 : t =~ (Quantified S_a Star)) :
       (s ++ t) =~ (Quantified S_a Plus)
   | MQuestionZero S_a :
       [] =~ (Quantified S_a Question)
   | MQuestionOne str S_a
       (H : str =~ S_a) :
       str =~ (Quantified S_a Question)
   | MRangeRep_0_0 S_a :
       [] =~ (Quantified S_a (RangeRep 0 0))
   | MRangeRep_0_S_empty m S_a :
       [] =~ (Quantified S_a (RangeRep 0 (S m)))
   | MRangeRep_0_S_step m s t S_a
       (H1 : s =~ Quantified S_a Question)
       (H2 : t =~ (Quantified S_a (RangeRep 0 m))) :
       (s ++ t) =~ (Quantified S_a (RangeRep 0 (S m)))
   | MRangeRep_S_S n m s t S_a
       (H1 : s =~ S_a)
       (H2 : t =~ (Quantified S_a (RangeRep n m))) :
       (s ++ t) =~ (Quantified S_a (RangeRep (S n) (S m)))
   | MExactRep n str S_a
       (H : str =~ (Quantified S_a (RangeRep n n))) :
       str =~ (Quantified S_a (ExactRep n))
   | MPartialRangeRep n s t S_a
       (H1 : s =~ Quantified S_a (ExactRep n))
       (H2 : t =~ (Quantified S_a Star)) :
       (s ++ t) =~ (Quantified S_a (PartialRep n))

where "s =~ r" := (xsdregex_match s r).

Each constructor corresponds to a specific line of a semantics table. Similarly to the syntax, we also include comments from the specification above each constructor. For instance, the rules of the star (*) are written as follows:

(** >>
      | ------- | ------------------------------------------- |
      |         |  All strings in L(S?) and all strings st    |
      |         |  with s in L( S* ) and t in L(S).           |
      |   S*    | ( all concatenations of zero or more strings|
      |         | from L(S) )                                 |
      | ------- | ------------------------------------------- |
<<*)
| MStarQuestion str S_a
      (H : str =~ (Quantified S_a Question)) :
      str =~ (Quantified S_a Star)
| MStarS s t S_a
      (H1 : s =~ (Quantified S_a Star))
      (H2 : t =~ S_a) :
      (s ++ t) =~ (Quantified S_a Star)

From the corresponding line in the XSD specification:

The XSD semantics also specifies that some XSD regexes are not valid, and have no semantics. These ill-formed regexes contain things like illegal character class ranges [z-a] where the codepoint of the first character is greater than the second one, or illegal quantifiers like r{3,1} where the minimum number of iterations is greater than the maximum. These two things are also illegal in ECMAScript regexes, so we need to formalize the validity of XSD regexes in order to prove the correctness of the translation. We encode this well-formedness with a property wf_regex: XSDRegex -> Prop, in file WellFormedness.v.

I-Regexp semantics

We then define what it means for an XSD regex to be an I-Regexp. We do that using an inductively defined proposition is_iregexp: XSDRegex -> Prop.

This property ensures that a regex only contains allowed constructors. For instance, multi-character escapes are allowed in XSD but not in I-Regexp. So to represent that in Rocq, we write a constructor for every other character escape in the inductive proposition, but not for multi-character escapes:

Inductive is_iregexp_char_class_esc : CharClassEsc -> Prop :=
   | IregexpEscSingle s : is_iregexp_char_class_esc (EscSingle s)
   | IregexpCatEsc p (H : is_iregexp_char_prop p) : is_iregexp_char_class_esc (CatEsc p)
   | IregexpComplEsc p (H : is_iregexp_char_prop p) : is_iregexp_char_class_esc (ComplEsc p).

Those code snippets and the rest of the inductively defined proposition needed to define when an XSD regex is an I-Regexp can be found in Iregexp.v.

Related work on JavaScript regexes done at SYSTEMF

This work builds upon previous projects related to JavaScript/ECMAScript regexes, that were developed at SYSTEMF:

• Warblre [Warblre_DeSanto+ICFP24] is a faithful and proven safe Rocq mechanization of JavaScript regular expressions semantics. This mechanization translated the full regex chapter of ECMAScript (14th edition) as closely as possible: each line of pseudo-code in the ECMAScript specification was translated into an equivalent line of Rocq.

• Linden [Linden_Barrière+POPL26] contains a rephrasing of JavaScript regex semantics. This new backtracking tree semantics is designed to be more succinct and practical for formal verification than the Warblre semantics. It has been proven to also be faithful to ECMAScript, thanks to a Rocq proof that relates the Linden semantics and the Warblre semantics.

• RegElk [LinearJS_Barrière+PLDI24] is a linear regular expression engine for a subset of JavaScript regexes. Because the I-Regexp to ECMAScript translation presented in the RFC falls within the supported subset of RegElk, RegElk could also be used as an I-Regexp linear-time engine.

Mechanizing the translation from I-Regexp to ECMAScript

We provide a mechanization of the translation function, by writing a Rocq function that translates XSD regexes into Linden regexes. Note that we also generated a second mechanization that targets the Warblre AST (slightly different from Linden's), then proved that the translations coincide: translating from XSD to Linden, or from XSD to Warblre then from Warblre to Linden produce the exact same regex.

In the I-Regexp specification [RFC9485], the translation function from I-Regexp to ECMAScript regex is defined by:

• For any unescaped dots (.) outside character classes, replace the dot with [^\n\r].

• Envelope the result in ^(?: and )$.

We hence faithfully mechanized this function, in file Translation.v, using two functions: one function that recursively translates the regex AST of the I-Regexp into an equivalent Linden regex AST, and a second one that wraps the result between two anchors.

Fixpoint translate_inner (r : Patterns.XSDRegex) : regex :=
   match r with
   | Patterns.Empty =>
       Epsilon
   | Patterns.Char c =>
       Character (char_to_descr c)
   | Patterns.CharacterClass cc =>
       Character (char_class_to_descr cc)
   | Patterns.Sequence r1 r2 =>
       Sequence (translate_inner r1) (translate_inner r2)
   | Patterns.Disjunction r1 r2 =>
       Disjunction (translate_inner r1) (translate_inner r2)
   | Patterns.Quantified r q =>
       let (min, delta) := translate_quantifier q in
       Quantified true min delta (translate_inner r)
   end.

Definition translate_to_ecmascript (r : Patterns.XSDRegex) : regex :=
   Sequence (Anchor BeginInput) (Sequence (translate_inner r) (Anchor EndInput)).

Correctness Proof

We now turn to the correctness of the translation: given an I-Regexp and a string, matching this I-Regexp according to XSD semantics should return the same result as matching its ECMAScript translation according to ECMAScript semantics.

To model what we just described, we state and prove the two following Rocq theorems (one for each translation):

Theorem iregexp_linden_equiv:
   forall (r : XSDRegex) (s : LWParameters.string) (t : tree),
   RegExpRecord.multiline rer = false ->
   is_iregexp r -> wf_regex r ->
   is_tree rer [Areg (translate_to_ecmascript r)] (init_input s) GroupMap.empty forward t ->
   (xsdregex_match s r <-> tree_leaves t GroupMap.empty (init_input s) forward <> []).

Corollary iregexp_warblre_equiv:
   forall (r : XSDRegex) (s : LWParameters.string),
   RegExpRecord.multiline rer = false ->
   RegExpRecord.capturingGroupsCount rer = 0 ->
   is_iregexp r -> wf_regex r ->
   (xsdregex_match s r <-> compilePattern (translate_to_warblre r) rer s 0 <> None).

To understand the first theorem, let us first describe the idea behind Linden's backtracking tree semantics [Linden_Barrière+POPL26]. A backtracking tree represents all choices that a backtracking algorithm would make when trying to match a specific regex on a specific string. These choices include choosing the right or left branch of a disjunction, and choosing to iterate a quantifier one more time, or stopping. The leaves of this tree are outcomes: a Match means that the regex matches the string along that path and a Mismatch means the opposite. In Linden, a regex matches a string if the corresponding backtracking tree contains at least one Match leaf.

is_tree rer [Areg (translate_to_ecmascript r)] (init_input s) GroupMap.empty forward t

means that t is the backtracking tree for input string s and regex translate_to_ecmascript r.

tree_leaves t GroupMap.empty (init_input s) forward <> []

means that there was at least one Match leaf in t, which is the same as saying that translate_to_ecmascript r matches s in the Linden semantics. And the first theorem states that this is equivalent to the original regex r matching s according to XSD semantics.

Similarly, the second theorem states that the XSD semantics agrees with the Warblre mechanization. It is a direct consequence of two proofs: the proof that our Warblre translation, when chained with the Warblre to Linden translation, produces the same regex as the Linden translation; and the existing proof relating Linden and Warblre semantics.

Both theorems rely on the properties stating that the regex is indeed part of the I-Regexp subset, and that it is well-formed. Both theorems also rely on assumptions on the value of the flags: the RFC clearly states that only flag u should be set, so we can assume that the multiline flag m is off.

Details about how to prove the first theorems are in the appendix.

Related work

There are also some other projects whose goal was to mechanize a regex flavor using a theorem prover:

• [Warblre_DeSanto+ICFP24] fully and faithfully mechanized JavaScript regular expressions semantics.

• [Zhuchko+2024] formalized in Lean a matching algorithm for extended regular expression matching based on locations and symbolic derivatives whose implementation mirrors an extension of the .NET NonBacktracking regular expression engine.

• [Perry+2025] formalized in Lean different regex disambiguation strategies (leftmost-longest and leftmost-greedy), and verified matching algorithms based on derivatives.

References

The helper lemma

We focus here on the $\to$ direction of the main correctness theorem for the Linden translation.

Wanting to prove it directly by induction posed some problems, since the theorem talks about translate_to_ecmascript r which is not recursive: it does call a recursive function, but then wraps the result in anchors.

Indeed the wrapping between anchors is what makes it impossible to prove the main direction by induction: since the anchor wrapping is part of the hypothesis of the theorem, it will also be transferred to the inductive hypotheses which we absolutely don't want. For example, if we want to prove that Sequence r1 r2 matches, the translated version is ^r1 r2$ (here we use the usual symbols and not the AST nodes for simplicity), but then our inductive hypotheses are about ^r1$ and ^r2$, but we cannot use those to prove that ^r1 r2$ matches since r1 is supposed to match a prefix of the string matched by ^r1 r2$. So the $ anchor on r1 will fail. In other words, those anchors break the inductive structure of the regexes since they don't distribute over the regex AST.

The idea to solve this problem is to create the following intermediate lemma:

Lemma translate_inner_equiv_fwd :
   forall (r : XSDRegex) (s : LWParameters.string) (inp : input) (gm : group_map) (cont : actions),
     is_iregexp r ->
     xsdregex_match s r ->
     s = firstn (length s) (next_str inp) ->

     (* if the continuation succeeds after we advanced the input by the length of the string s *)
     (tree_leaves (compute_tr rer cont (advance_input_n inp (length s) forward) gm forward) gm
                  (advance_input_n inp (length s) forward) forward <> []) ->

     (* then the whole tree (regex + continuation) succeeds from the starting input. *)
     tree_leaves (compute_tr rer (Areg (translate_inner r) :: cont) inp gm forward) gm inp forward <> [].

What this lemma allows us to do is to peel off those anchors and then do the proof by induction on the regex inside the anchors, which has a recursive structure. From this helper lemma we managed to prove the $\to$ direction of the main theorem.

Proof of the helper lemma for the $\to$ direction

Initially we tried to prove this lemma by induction on xsdregex_match but it did not work and created inductive hypotheses that were too weak. For example, for the star case (MStarQuestion case) it created an inductive hypothesis for Question S_a and not S_a which is needed in that case of the proof.

We hence decided to prove this lemma by induction on r, the regex. Therefore, we have many cases to solve. We will only describe the proof of the most interesting ones.

induction r; intros s inp gm cont H_iregexp H_xsd_match H_prefix H_tree_leaves_cont.

Disjunction case

- (* Disjunction *)
     inversion H_iregexp; subst.
     compute_tr_step.
     inversion H_xsd_match; subst.
     + (* left branch (r1) *)
       apply tree_leaves_app_not_nil_l.
       apply (IHr1 s inp gm cont).
         * exact H2.
         * exact H1.
         * exact H_prefix.
         * exact H_tree_leaves_cont.
     + (* right branch (r2) *)
       apply tree_leaves_app_not_nil_r.
       apply (IHr2 s inp gm cont).
         * exact H3.
         * exact H1.
         * exact H_prefix.
         * exact H_tree_leaves_cont.

Here we apply compute_tr_step to transform the goal into the concatenation of the tree leaves of each possible path created at the disjunction. Then we finish with two cases: either the left path is a match or the right path is a match. In either case, we have that the concatenation of their tree leaves is not empty.

Character class case

This case was long but pretty repetitive. In order to prove this case, we had to create a multitude of helper lemmas that bridge all dependencies of CharClass (for example CharacterClassExpr) and their Linden counterparts.

In order to complete the proof of this case, we had to introduce five hypotheses to take care of some assertions that we could not prove:

Hypothesis H_case : RegExpRecord.ignoreCase rer = false.

Hypothesis H_nv10_inv : Character.numeric_value (Character.from_numeric_value 10) = 10.

Hypothesis H_nv13_inv : Character.numeric_value (Character.from_numeric_value 13) = 13.

Hypothesis H_cat :
   forall (c : Character.type) (cat : IsCategory),
      is_char_in_category c cat <->
      char_match rer c (CdUnicodeProp (translate_char_prop (PropCategory cat))) = true.

Hypothesis H_compl :
   forall (c : Character.type) (cat : IsCategory),
   ~ is_char_in_category c cat <->
   char_match rer c (CdNonUnicodeProp (translate_char_prop (PropCategory cat))) = true.

These are the only hypotheses needed in our whole proof.

We justify the creation of H_case by the fact that the RFC only says to turn on the u flag, not the case insensitivity flag i.

We needed H_nv10_inv and H_nv13_inv because we could not otherwise simplify parts of our proof. In general the following assertion

forall n, Character.numeric_value (Character.from_numeric_value n) = n

does not hold because from_numeric_value is not injective. Indeed, by the pigeonhole principle it cannot be injective, since there is a finite number of Unicode characters but the natural numbers are infinite. It is however reasonable to assume that this holds for small values like 10 and 13 since we would define this function so that the above formula holds for all n that is a Unicode code point. But it will not hold for a bigger n!

Finally H_cat and H_compl are needed because translate_char_prop is left abstract (mechanizing the full Unicode property database is out of scope).

Star case

This was the most interesting case and solving it was challenging. Moreover, the technique used to solve it can be re-used to help solve the other quantifier cases.

A star can iterate any number of times, so we cannot induct on a predefined fixed count. The only natural way to measure advancement by the engine is to measure the length of the matched string. Since each non-empty iteration consumes at least one character, the remaining string's length will shrink.

However, ordinary induction is not strong enough because an iteration can consume more than one character (for example if we consider (ab)* then the first iteration of it will consume ab). We do not necessarily go from length n to n-1: we might directly jump to length n-k (k >=1). This hence motivates the use of strong induction to prove our lemma for the star case.

What we did is hence to create a new lemma that is the helper lemma but specialized for the Star case. It also has some additional hypotheses, but these are there just to be able to pass the inductive hypothesis on r IHr from the proof of the main lemma to this new lemma.

Lemma translate_inner_equiv_fwd_star_strong_ind :
   forall r,
     (forall (s : LWParameters.string) (inp : input) (gm : group_map) (cont : actions),
       is_iregexp r ->
       xsdregex_match s r ->
       s = firstn (length s) (next_str inp) ->
       tree_leaves (compute_tr rer cont (advance_input_n inp (length s) forward) gm forward)
                     gm (advance_input_n inp (length s) forward) forward <> [] ->
       tree_leaves (compute_tr rer (Areg (translate_inner r) :: cont) inp gm forward)
                     gm inp forward <> []) ->
     is_iregexp r ->
     forall n s',
       length s' = n ->
       xsdregex_match s' (Quantified r Star) ->
       forall inp' gm' cont',
       s' = firstn (length s') (next_str inp') ->
       tree_leaves (compute_tr rer cont' (advance_input_n inp' (length s') forward) gm' forward)
                     gm' (advance_input_n inp' (length s') forward) forward <> [] ->
       tree_leaves (compute_tr rer (Areg (translate_inner (Quantified r Star)) :: cont') inp' gm' forward)
                     gm' inp' forward <> [].

We could just have formulated this lemma as an assertion inside the proof of the helper lemma, but we extracted it to a new lemma since we re-used it for other cases.

A greedy Quantified true 0 ∞ unfolds into a Choice between two subtrees:

• an iterate branch : match one copy of r, then check progress, then start the star again with a smaller input string

• a skip branch : skip the iteration and directly continue with the continuation cont

Because we have a Choice, its leaf list is the concatenation of the leaf list for the iterate branch and of the leaf list for the skip branch. We want to show that their concatenation is not empty so our strategy is to choose the branch depending on the matched string s':

• s' = [] : then there is nothing to match so we take the skip branch and apply the hypothesis for the continuation to finish the goal

• s' = c :: s'' : then we take the iterate branch to consume one iteration of r

  To solve this case, we split our input string into a prefix which is a non-empty match of r and rest which matches r*. Then we only have three steps left:

  1. Consume the first iteration of r which will consume prefix

  2. Pass the progress check. We show this one by using the fact that we know that prefix is non-empty and we know we consumed it, so we know we made progress.

  3. Finally what is left to prove is that (translate_inner r)* matches rest which we conclude directly using our strong induction hypothesis since rest is a suffix of the original input string s' so its length is smaller.

The details of the proof of this case and of all the other cases can be found in file EquivProof.v.