Warblre

A mechanization of ECMAScript regexes

The goal of this project was to mechanize in the Coq proof assistant the regexes defined in the ECMA-262 standard, the specification follow by the JavaScript language.

The mechanization was designed to be auditable, executable, proven-safe, and faithful. Since it was written in a proof assistant, it also opens the door to mechanized proofs about these regexes.

(*>> Disjunction :: Alternative | Disjunction <<*)
| Disjunction r11 r22 ⇒
  (*>> 1. Let m1 be CompileSubpattern of Alternative with arguments rer and direction. <<*)
  let! m11 =<< compileSubPattern r11 (Disjunction_left r22 ∷ ctx) rer direction in
  (*>> 2. Let m2 be CompileSubpattern of Disjunction with arguments rer and direction. <<*)
  let! m22 =<< compileSubPattern r22 (Disjunction_right r11 ∷ ctx) rer direction in
  (*>> 3. Return a new Matcher with parameters (x, c) that captures m1 and m2 and performs
        the following steps when called: <<*)
  (λ (x: MatchState) (c: MatcherContinuation) ⇒
    (*>> a. Assert: x is a MatchState. <<*)
    (*>> b. Assert: c is a MatcherContinuation. <<*)
    (*>> c. Let r be m1(x, c). <<*)
    let! r =<< m11 x c in
    (*>> d. If r is not failure, return r. <<*)
    if r is not failure then r
    (*>> e. Return m2(x, c). <<*)
    else m22 x c): Matcher