% \marginpar{Totally rewritten introduction}

% Formal proofs, 

\marginpar{rephrasing following Christian comment}

Regular expressions, since their inception in the 1950s

\cite{RegularExpressions}, 

\verb|[a-z0-9._]+@[a-z0-9.-]+\.[a-z]{2,6}|

This expression assumes all letters in the email have been converted into lower-case.

The local-part is recognised by the first 

bracketed expression $[a-z0-9.\_]^+$ 

where the

operator ``+'' (should be viewed as a superscript) 

means that it must be some non-empty string

made of alpha-numeric characters.

After the ``@'' sign

is the sub-expression that recognises the domain of that email, 

where $[a-z]^{\{2, 6\}}$ specifically

matches the top-level domain, such as ``org'', ``com'', ``uk'' and etc.

The counters in the superscript 

$2, 6$ specifies that all top-level domains

should have between two to six characters.

This regular expression does not represent all possible email addresses 

(e.g. those involving ``-'' cannot be recognised), but patterns

of similar shape and using roughly the same set of syntax are used

everywhere in our daily life,

% Indeed regular expressions are used everywhere 

% in a computer user's daily life--for example searching for a string

% in a text document using ctrl-F.

% When such regex searching 

% a useful and simple way to handle email-processing when the task does

% not require absolute precision. 

%The same can be said about

%applications like .

% The picture gets more blurry when we start to ask questions like 

% why 

%TODO: Insert corresponding bibliography

%There are many more scenarios in which regular exp% %use cases for regular expressions in computer science,

for example in compilers \cite{LEX}, networking \cite{Snort1999}, 

software engineering (IDEs) \cite{Atom}

and operating systems \cite{GREP}, where the correctness

of matching can be crucially important.

Implementations of regular expression matching out in the wild, however, 

are surprisingly unreliable.

%are not always reliable as %people think

%they

%should be. %Given the importance of the correct functioning

% Indeed they have been heavily relied on and

% extensively implemented and studied in modern computer systems--whenever you do

% a 

%TODO: double check this is true

An example is the regular expresion $(a^*)^*b$ and the string

$aa\ldots a$. The expectation is that any regex engine should

be able to solve this (return a no match) in no time.

However, if this 

%regular expression and string pair 

is tried out in an

regex engine like that of Java 8, the runtime would quickly grow beyond 100 seconds

with just dozens of characters 

%in the string. 

Such behaviour can result in Denial-of-Service (ReDoS) attacks

with minimal resources--just the pair of ``evil'' 

regular expression and string.

The outage of the web service provider Cloudflare \cite{Cloudflare} 

in 2019 \cite{CloudflareOutage} is a recent example

where such issues caused serious negative impact.

The reason why these regex matching engines get so slow

is because they use backtracking or a depth-first-search (DFS) on the 

search space of possible matches. They employ backtracking algorithms to 

support back-references, a mechanism allowing

expressing languages which repeating an arbitrary long string 

such as 

$\{ww| w\in \Sigma*\}$. Such a constructs makes matching

NP-complete, for which no known non-backtracking algorithms exist.

More modern programming languages' regex engines such as

Rust and GO's do promise linear-time behaviours 

with respect to input string,

but they do not support back-references, and often 

impose ad-hoc restrictions on the input patterns.

More importantly, these promises are purely empirical,

making them prone to future ReDoS attacks and other types of errors.

The other unreliability of industry regex engines

is that they do not produce the desired output. 

Kuklewicz have found out during his testing

of practical regex engines that almost all of them are incorrect with respect

to the POSIX standard, a disambiguation strategy adopted most

widely in computer science. Roughly speaking POSIX lexing means to always

go for the longest initial submatch possible, 

for instance a single iteration

$aa$ is preferred over two iterations $a,a$ 

when matching $(a|aa)^*$ with the string $aa$.

The POSIX strategy as summarised by Kuklewicz goes

as follows:

\marginpar{\em Deleted some peripheral specifications.}

\begin{quote}

	\begin{itemize}

		\item

regular expressions (REs) take the leftmost starting match, and the longest match starting there

earlier subpatterns have leftmost-longest priority over later subpatterns\\

\item

higher-level subpatterns have leftmost-longest priority over their component subpatterns\\

\item

	$\ldots$

%REs have right associative concatenation which can be changed with parenthesis\\

%\item

%parenthesized subexpressions return the match from their last usage\\

%\item

%text of component subexpressions must be contained in the text of the 

%higher-level subexpressions\\

%\item

%if "p" and "q" can never match the same text then "p|q" and "q|p" are equivalent, up to trivial renumbering of captured subexpressions\\

%\item

%if "p" in "p*" is used to capture non-empty text then additional repetitions of "p" will not capture an empty string\\

\end{itemize}

\end{quote}

The author noted that various lexers that come with POSIX operating systems

are rarely correct according to this standard.

A test case that exposes the bugs 

is the regular expression $(aba|ab|a)^*$ and string $ababa$.

A correct match would split the string into $ab, aba$, involving

two repetitions of the Kleene star $(aba|ab|a)^*$.

Most regex engines would instead return two (partial) matches

$aba$ and  $a$ \footnote{Try it out here: \url{https://regex101.com/r/c5hga5/1}, last accessed 22-Aug-2023}.

There are numerous occasions where programmers realised the subtlety and

difficulty to implement POSIX correctly, one such quote from Go's regexp library author:

\footnote{\url{https://pkg.go.dev/regexp\#pkg-overview}, last accessed 22-Aug-2023}

\begin{quote}\it

``

The POSIX rule is computationally prohibitive

and not even well-defined.

''

\end{quote}

% Being able to formally define and capture the idea of 

% POSIX rules and prove 

% the correctness of regular expression matching/lexing 

% algorithms against the POSIX semantics definitions

% is valuable.

These all point towards a formal treatment of 

POSIX lexing to clear up inaccuracies and errors

in understanding and implementation of regex. The work presented

in this thesis uses formal proofs to ensure the correctness 

and runtime properties

of POSIX regular expression lexing.

Formal proofs or mechanised proofs are

computer checked programs

 %such as the ones written in Isabelle/HOL, is a powerful means 

that certify the correctness of facts

with respect to a set of axioms and definitions.

% This is done by 

% recursively checking that every fact in a proof script 

% is either an axiom or a fact that is derived from

% known axioms or verified facts.

%The problem of regular expressions lexing and catastrophic backtracking are a suitable problem for such

%methods as their implementation and complexity analysis tend to be error-prone.

They provide an unprecendented level of asssurance

that an algorithm will perform as expected under all inputs.

We believe such proofs can help eliminate catastrophic backtracking

once and for all.

The software systems that help people interactively build and check

formal proofs are called proof assitants.

% Many  theorem-provers have been developed, such as Mizar,

% Isabelle/HOL, HOL-Light, HOL4,

% Coq, Agda, Idris, Lean and so on.

Isabelle/HOL \cite{Isabelle} is a widely-used proof assistant with a simple type theory

and powerful automated proof generators like sledgehammer.

We chose to use Isabelle/HOL for its powerful automation

and ease and simplicity in expressing regular expressions and 

regular languages.

%Some of those employ

%dependent types like Mizar, Coq, Agda, Lean and Idris.

%Some support a constructivism approach, such as Coq.

% Formal proofs on regular expression matching and lexing

% complements the efforts in

% industry which tend to focus on overall speed

% with techniques like parallelization (FPGA paper), tackling 

% the problem of catastrophic backtracking 

% in an ad-hoc manner (cloudflare and stackexchange article).

The algorithm we work on is based on Brzozowski derivatives.

Brzozowski invented the notion of ``derivatives'' on 

regular expressions \cite{Brzozowski1964}, and the idea is

that we can reason about what regular expressions can match

by taking derivatives of them. 

A derivative operation takes a regular expression $r$ and a character

$c$,

and returns a new regular expression $r\backslash c$.

The derivative is taken with respect to $c$:

it transforms $r$ in such a way that the resulting derivative

$r\backslash c$ contains all strings in the language of $r$ that

starts with $c$, but now with the head character $c$ thrown away.

For example, for $r$ equal to $(aba | ab | a)^*$

as discussed earlier, its derivative with respect to character $a$ is

\[

  r\backslash a = (ba | b| \ONE)(aba | ab | a)^*.

\]

% By applying derivatives repeatedly one can c

Taking derivatives repeatedly with respect to the sequence

of characters in the string $s$, one obtain a regular expression

containing the information of how $r$ matched $s$.

Brzozowski derivatives are purely algebraic operations

that can be implemented as a recursive function

that does a pattern match on the structure of the regular expression.

For example, the derivatives of character regular expressions,

Kleene star and bounded repetitions can be described by the following

code equations:

% For example some clauses

\begin{center}

	\begin{tabular}{lcl}

    $d \backslash c$     & $\dn$ & 

		$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\

% $(r_1 + r_2)\backslash c$     & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\

% $(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, [] \in L(r_1)$\\

% 	&   & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\

% 	&   & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\

	$(r^*)\backslash c$           & $\dn$ & $(r\backslash c) \cdot r^*$\\

		$r^{\{n\}} \backslash c$     & $\dn$ & $r \backslash c \cdot

		r^{\{n-1\}} (\text{when} \; n > 0)$\\

	\end{tabular}

\end{center}

(end of ready work, rest construction site)

In particular, we are working on an improvement of the work

by Ausaf et al. \cite{Ausaf} \cite{AusafDyckhoffUrban2016} 

and Sulzmann and Lu \cite{Sulzmann2014}.

The variant of the problem we are looking at centers around

an algorithm (which we call $\blexer$) developed by Sulzmann and Lu \ref{Sulzmann2014}.

The reason we chose to look at $\blexer$ and its simplifications 

is because it allows a lexical tree to be generated

by some elegant and subtle procedure based on Brzozowski derivatives.

The procedures are made of recursive functions and inductive datatypes just like derivatives, 

allowing intuitive and concise formal reasoning with theorem provers.

Most importantly, $\blexer$ opens up a path to an optimized version

of $\blexersimp$ possibilities to improve

performance with simplifications that aggressively change the structure of regular expressions.

While most derivative-based methods

rely on structures to be maintained to allow induction to

go through.

For example, Egolf et al. \ref{Verbatim} have developed a verified lexer

with derivatives, but as soon as they started introducing

optimizations such as memoization, they reverted to constructing

DFAs first.

Edelmann \ref{Edelmann2020} explored similar optimizations in his

work on verified LL(1) parsing, with additional enhancements with data structures like

zippers.

%Sulzmann and Lu have worked out an algorithm

%that is especially suited for verification

%which utilized the fact

%that whenever ambiguity occurs one may duplicate a sub-expression and use

%different copies to describe different matching choices.

The idea behind the correctness of $\blexer$ is simple: during a derivative,

multiple matches might be possible, where an alternative with multiple children

each corresponding to a 

different match is created. In the end of

a lexing process one always picks up the leftmost alternative, which is guarnateed 

to be a POSIX value.

This is done by consistently keeping sub-regular expressions in an alternative

with longer submatches

to the left of other copies (

Remember that POSIX values are roughly the values with the longest inital

submatch).

The idea behind the optimized version of $\blexer$, which we call $\blexersimp$,

is that since we only take the leftmost copy, then all re-occurring copies can be

eliminated without losing the POSIX property, and this can be done with