Authors: Aurèle Barrière, Victor Deng and Clément Pit-Claudel.
Related Preprint: Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications. Appendix A provides a correspondence between paper definitions and the code.
This repository contains mechanized proofs, in Rocq, about JavaScript Regular Expressions. This includes:
- a new backtracking tree semantics for JavaScript regexes, in folder
Semantics. - a proof that this semantics is equivalent to the Warblre mechanization of JavaScript regexes, in folder
WarblreEquiv. - a proof of the PikeVM linear-time matching algorithm supporting a subset of JavaScript regexes, in folder
Engine. The algorithm is adapted to fit JavaScript unique quantifier semantics, following section 4.1 of Linear Matching of JavaScript Regular Expressions. - proof of JavaScript regex contextual equivalences, in folder
Rewriting.
- coq 8.18.0
- Warblre 0.1.0
- dune >= 3.14
Build all proofs with dune build.