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.
-
Create a local opam switch:
opam switch --no-install create . -
Pin the version of Warblre:
opam pin add warblre https://github.com/epfl-systemf/Warblre.git#a1ffc3f2e47d942ad9e1194dfb71f0783ead6d8a -
Build all proofs with
dune build.