A blog post by Paolo Soravia describing this work is available here.
This repository contains:
- The mechanization of the XSD semantics. This mechanization follows the XSD specification as closely as possible. The syntax is defined in
Patterns.v. The semantics is defined inSemantics.v. A WellFormedness predicate specifying the validity of Character Ranges is defined inWellFormedness.v. - The mechanization of the I-Regexp semantics. The RFC describes it as a subset of XSD semantics, so we implement a predicate that determines if an XSD regex is an I-regexp. This predicate is defined in
IRegexp.v. - The mechanization of the translation function from I-Regexp to ECMAScript regex described in the I-Regexp specification. Because there are two ways to represent and reason about ECMAScript regexes in Rocq, we have two translations. The translation to Linden regexes is easier to follow and audit, and is in file
Translation.v. A translation to Warblre regexes is also available inWarblreTranslation.v. A proof that the two translations produce the same regexes (once the Warblre regex is translated to Linden) is also inWarblreTranslation.v. - We prove that the translations from I-Regexp to ECMAScript are correct, meaning that an I-regexp matches a string if and only if the translated ECMAScript regex finds a match on that string. The proof of the Linden translation is in
EquivProof.v. The proof of the Warblre translation is inWarblreEquivProof.v.
-
Create a local opam switch:
opam switch create . 5.2.0 --no-install eval $(opam env) -
Add rocq-released dependency repository:
opam repo add rocq-released https://rocq-prover.org/opam/released -
Pin the two dependencies, Linden and Warblre:
opam pin add warblre.0.1.0 https://github.com/epfl-systemf/Warblre.git#4321379b887d590a42759818f6d9b1fd2351688e opam pin add linden.0.1.0 https://github.com/LindenRegex/Linden.git#19d360d6d1728ef4ba45cc99088384292a59c31b -
Install dependencies:
opam install --deps-only . -
Build all proofs with
dune build.