Despite widespread use, the complexity class of modern regular expression matching was not well-understood. Previous work proved that regular expression matching with backreferences and lookarounds was PSPACE-complete, but the proof was not mechanized and applied to an abstract regex language. This paper clarifies the question for JavaScript regular expressions. In this paper, we prove the following new results, with most core proofs mechanized in the Rocq proof assistant. We prove that JavaScript regex matching is indeed PSPACE-hard, even without negative lookarounds, and OptP-hard as well; that JavaScript regex matching without lower-bounded quantifiers (i.e. quantifiers with a non-zero minimum number of repetitions) is PSPACE-complete; and that JavaScript regex matching without lower-bounded quantifiers and without lookarounds is OptP-complete.

翻译：尽管现代正则表达式被广泛使用，其复杂性类别此前尚未被充分理解。先前的研究证明，带反向引用和环视的正则表达式匹配是PSPACE完全的，但该证明未经过机械验证且应用于抽象正则表达式语言。本文厘清了JavaScript正则表达式的这一问题。我们证明了以下新结果，其中大部分核心证明已在Rocq证明助手中完成机械验证：我们证明JavaScript正则表达式匹配确实是PSPACE难的（即使不含否定环视），同时也是OptP难的；不含下限量词（即非零最小重复次数量词）的JavaScript正则表达式匹配是PSPACE完全的；既不含下限量词也不含环视的JavaScript正则表达式匹配是OptP完全的。