def RegexCorrectness.Spec.SearchProblem (e : Regex.Data.Expr) (it : String.Iterator) : 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 (it).

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

• One or more equations did not get rendered due to their size.