一句话：首次在 Coq 中忠实机器化 ECMA-262 的 JavaScript 正则语义，证明匹配必然终止且安全，并可提取为通过 Test262 的引擎。
本文首次在交互式定理证明器中忠实机器化工业级正则语言：ECMA-262 第 22.2 节所定义的 JavaScript 正则匹配。作者在 Coq 中给出可执行、可证明安全且便于随规范演进的语义实现，并讨论编码、边界情形与可执行性等挑战。基于该机器化，他们证明 JS 正则匹配必然终止且不触发断言失败，指出既有文献中的细微边界错误，验证了取自先进正则引擎的优化，并表明自动机教科书中的若干经典性质及基于导数的匹配器假设在 JS 正则下并不成立。该实现可提取为 OCaml 与 JavaScript，链接 Unicode 库后通过官方 Test262 一致性测试的相关部分。
We present an executable, proven-safe, faithful, and future-proof Coq mechanization of JavaScript regular expression (regex) matching, as specified by the latest published edition of ECMA-262 section 22.2. This is, to our knowledge, the first time that an industrial-strength regex language has been faithfully mechanized in an interactive theorem prover. We highlight interesting challenges that arose in the process (including issues of encoding, corner cases, and executability), and we document the steps that we took to ensure that the result is straightforwardly auditable and that our understanding of the specification aligns with existing implementations. We demonstrate the usability and versatility of the mechanization through a broad collection of analyses, case studies, and experiments: we prove that JavaScript regex matching always terminates and is safe (no assertion failures); we identify subtle corner cases that led to mistakes in previous publications; we verify an optimization extracted from a state-of-the-art regex engine; we show that some classic properties described in automata textbooks and used in derivatives-based matchers do not hold in JavaScript regexes; and we demonstrate that the cost of updating the mechanization to account for changes in the original specification is reasonably low. Our mechanization can be extracted to OCaml and JavaScript and linked with Unicode libraries to produce an executable regex engine that passes the relevant parts of the official Test262 conformance test suite.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2403-11919,
title = {A Coq Mechanization of JavaScript Regular Expression Semantics},
author = {Noé De Santo and Aurèle Barrière and Clément Pit-Claudel},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674666}
}