def RegexCorrectness.Spec.SearchProblem {s : String} (e : Regex.Data.Expr) (pos : s.ValidPos) : Prop

The search problem regex engines intend to solve.

Intuitively, the problem is to find a substring that matches the regex (e) after the current position (pos).

We are interested in the following two properties:

• Soundness: when an engine returns a positive result, there must be a match in the later part of the string.
  • Additionally, NFA engines must return the correct capture group buffers corresponding groups.
• Completeness: when an engine returns a negative result, there must be no match in the later part of the string.
  • By contraposition, if there is a match in the later part of the string, the engine must return a positive result.

In other words, we prove that the regex engines are decision procedures of this search problem.

Equations

• RegexCorrectness.Spec.SearchProblem e pos = ∃ (pos' : s.ValidPos) (pos'' : s.ValidPos) (groups : Regex.Data.CaptureGroups s), pos ≤ pos' ∧ Regex.Data.Expr.Captures pos' pos'' groups e