We present the first mechanized, succinct, practical, complete, and proven-faithful semantics for a modern regular expression language with backtracking semantics. We ensure its faithfulness by proving it equivalent to a preexisting line-by-line embedding of the official ECMAScript specification of JavaScript regular expressions. We demonstrate its practicality by presenting two real-world applications. First, a new notion of contextual equivalence for modern regular expressions, which we use to prove or disprove rewrites drawn from previous work. Second, the first formal proof of the PikeVM algorithm used in many real-world engines. In contrast with the specification and other formalization work, our semantics captures not only the top-priority match, but a full backtracking tree recording all possible matches and their respective priority. All our definitions and results have been mechanized in the Rocq proof assistant.

翻译：我们首次为现代支持回溯语义的正则表达式语言提出了机械化、简洁、实用、完备且具有证明忠实性的语义。通过证明该语义与ECMAScript官方规范中JavaScript正则表达式的逐行嵌入等价，我们确保了其忠实性。通过展示两个实际应用，我们证明了其实用性：其一，针对现代正则表达式提出了一种新的上下文等价概念，用于证明或证伪先前工作中的重写规则；其二，对多个现实引擎中使用的PikeVM算法进行了首次形式化证明。与规范和其它形式化工作不同，我们的语义不仅捕获最高优先级匹配，还记录了所有可能匹配及其优先级的完整回溯树。所有定义和结果均已在Rocq证明助手中机械化实现。