% Chapter 1

\chapter{Introduction} % Main chapter title

\label{Introduction} % For referencing the chapter elsewhere, use \ref{Chapter1} 

%----------------------------------------------------------------------------------------

% Define some commands to keep the formatting separated from the content 

\newcommand{\keyword}[1]{\textbf{#1}}

\newcommand{\tabhead}[1]{\textbf{#1}}

\newcommand{\code}[1]{\texttt{#1}}

\newcommand{\file}[1]{\texttt{\bfseries#1}}

\newcommand{\option}[1]{\texttt{\itshape#1}}

%boxes

\newcommand*{\mybox}[1]{\framebox{\strut #1}}

%\newcommand{\sflataux}[1]{\textit{sflat}\_\textit{aux} \, #1}

\newcommand\sflat[1]{\llparenthesis #1 \rrparenthesis }

\newcommand{\ASEQ}[3]{\textit{ASEQ}_{#1} \, #2 \, #3}

\newcommand{\bderssimp}[2]{#1 \backslash_{bsimps} #2}

\newcommand{\rderssimp}[2]{#1 \backslash_{rsimps} #2}

\def\derssimp{\textit{ders}\_\textit{simp}}

\def\rders{\textit{rders}}

\newcommand{\bders}[2]{#1 \backslash #2}

\newcommand{\bsimp}[1]{\textit{bsimp}(#1)}

\def\bsimps{\textit{bsimp}}

\newcommand{\rsimp}[1]{\textit{rsimp}\; #1}

\newcommand{\sflataux}[1]{\llparenthesis #1 \rrparenthesis'}

\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%

\newcommand{\denote}{\stackrel{\mbox{\scriptsize denote}}{=}}%

\newcommand{\ZERO}{\mbox{\bf 0}}

\newcommand{\ONE}{\mbox{\bf 1}}

\newcommand{\AALTS}[2]{\oplus {\scriptstyle #1}\, #2}

\newcommand{\rdistinct}[2]{\textit{rdistinct} \;\; #1 \;\; #2}

\def\rdistincts{\textit{rdistinct}}

\def\rDistinct{\textit{rdistinct}}

\newcommand\hflat[1]{\llparenthesis  #1 \rrparenthesis_*}

\newcommand\hflataux[1]{\llparenthesis #1 \rrparenthesis_*'}

\newcommand\createdByStar[1]{\textit{createdByStar}(#1)}

\def\cbn{\textit{createdByNtimes}}

\def\hpa{\textit{highestPowerAux}}

\def\hpower{\textit{highestPower}}

\def\ntset{\textit{ntset}}

\def\optermsimp{\textit{optermsimp}}

\def\optermOsimp{\textit{optermOsimp}}

\def\optermosimp{\textit{optermosimp}}

\def\opterm{\textit{opterm}}

\def\nString{\textit{nonemptyString}}

\newcommand\myequiv{\mathrel{\stackrel{\makebox[0pt]{\mbox{\normalfont\tiny equiv}}}{=}}}

\def\SEQ{\textit{SEQ}}

\def\SEQs{\textit{SEQs}}

\def\case{\textit{case}}

\def\sequal{\stackrel{\mbox{\scriptsize rsimp}}{=}}

\def\rsimpalts{\textit{rsimp}_{ALTS}}

\def\good{\textit{good}}

\def\btrue{\textit{true}}

\def\bfalse{\textit{false}}

\def\bnullable{\textit{bnullable}}

\def\bnullables{\textit{bnullables}}

\def\Some{\textit{Some}}

\def\None{\textit{None}}

\def\code{\textit{code}}

\def\decode{\textit{decode}}

\def\internalise{\textit{internalise}}

\def\lexer{\mathit{lexer}}

\def\mkeps{\textit{mkeps}}

\newcommand{\rder}[2]{#2 \backslash_r #1}

\def\rerases{\textit{rerase}}

\def\nonnested{\textit{nonnested}}

\def\AZERO{\textit{AZERO}}

\def\sizeNregex{\textit{sizeNregex}}

\def\AONE{\textit{AONE}}

\def\ACHAR{\textit{ACHAR}}

\def\simpsulz{\textit{simp}_{Sulz}}

\def\scfrewrites{\stackrel{*}{\rightsquigarrow_{scf}}}

\def\frewrite{\rightsquigarrow_f}

\def\hrewrite{\rightsquigarrow_h}

\def\grewrite{\rightsquigarrow_g}

\def\frewrites{\stackrel{*}{\rightsquigarrow_f}}

\def\hrewrites{\stackrel{*}{\rightsquigarrow_h}}

\def\grewrites{\stackrel{*}{\rightsquigarrow_g}}

\def\fuse{\textit{fuse}}

\def\bder{\textit{bder}}

\def\der{\textit{der}}

\def\POSIX{\textit{POSIX}}

\def\ALTS{\textit{ALTS}}

\def\ASTAR{\textit{ASTAR}}

\def\DFA{\textit{DFA}}

\def\NFA{\textit{NFA}}

\def\bmkeps{\textit{bmkeps}}

\def\bmkepss{\textit{bmkepss}}

\def\retrieve{\textit{retrieve}}

\def\blexer{\textit{blexer}}

\def\flex{\textit{flex}}

\def\inj{\textit{inj}}

\def\Empty{\textit{Empty}}

\def\Left{\textit{Left}}

\def\Right{\textit{Right}}

\def\Stars{\textit{Stars}}

\def\Char{\textit{Char}}

\def\Seq{\textit{Seq}}

\def\Alt{\textit{Alt}}

\def\Der{\textit{Der}}

\def\Ders{\textit{Ders}}

\def\nullable{\mathit{nullable}}

\def\Z{\mathit{Z}}

\def\S{\mathit{S}}

\def\rup{r^\uparrow}

%\def\bderssimp{\mathit{bders}\_\mathit{simp}}

\def\distinctWith{\textit{distinctWith}}

\def\lf{\textit{lf}}

\def\PD{\textit{PD}}

\def\suffix{\textit{Suffix}}

\def\distinctBy{\textit{distinctBy}}

\def\starupdate{\textit{starUpdate}}

\def\starupdates{\textit{starUpdates}}

\def\nupdate{\textit{nupdate}}

\def\nupdates{\textit{nupdates}}

\def\size{\mathit{size}}

\def\rexp{\mathbf{rexp}}

\def\simp{\mathit{simp}}

\def\simpALTs{\mathit{simp}\_\mathit{ALTs}}

\def\map{\mathit{map}}

\def\distinct{\mathit{distinct}}

\def\blexersimp{\mathit{blexer}\_\mathit{simp}}

\def\blexerStrong{\textit{blexerStrong}}

\def\bsimpStrong{\textit{bsimpStrong}}

\def\bdersStrongs{\textit{bdersStrong}}

\newcommand{\bdersStrong}[2]{#1 \backslash_{bsimpStrongs} #2}

\def\map{\textit{map}}

\def\rrexp{\textit{rrexp}}

\newcommand\rnullable[1]{\textit{rnullable} \; #1 }

\newcommand\rsize[1]{\llbracket #1 \rrbracket_r}

\newcommand\asize[1]{\llbracket #1 \rrbracket}

\newcommand\rerase[1]{ (#1)_{\downarrow_r}}

\newcommand\ChristianComment[1]{\textcolor{blue}{#1}\\}

\def\rflts{\textit{rflts}}

\def\rrewrite{\textit{rrewrite}}

\def\bsimpalts{\textit{bsimp}_{ALTS}}

\def\bsimpaseq{\textit{bsimp}_{ASEQ}}

\def\rsimlalts{\textit{rsimp}_{ALTs}}

\def\rsimpseq{\textit{rsimp}_{SEQ}}

\def\erase{\textit{erase}}

\def\STAR{\textit{STAR}}

\def\flts{\textit{flts}}

\def\zeroable{\textit{zeroable}}

\def\nub{\textit{nub}}

\def\filter{\textit{filter}}

%\def\not{\textit{not}}

\def\RZERO{\mathbf{0}_r }

\def\RONE{\mathbf{1}_r}

\newcommand\RCHAR[1]{\mathbf{#1}_r}

\newcommand\RSEQ[2]{#1 \cdot #2}

\newcommand\RALTS[1]{\sum #1}

\newcommand\RSTAR[1]{#1^*}

\newcommand\vsuf[2]{\textit{Suffix} \;#1\;#2}

\lstdefinestyle{myScalastyle}{

  frame=tb,

  language=scala,

  aboveskip=3mm,

  belowskip=3mm,

  showstringspaces=false,

  columns=flexible,

  basicstyle={\small\ttfamily},

  numbers=none,

  numberstyle=\tiny\color{gray},

  keywordstyle=\color{blue},

  commentstyle=\color{dkgreen},

  stringstyle=\color{mauve},

  frame=single,

  breaklines=true,

  breakatwhitespace=true,

  tabsize=3,

}

%----------------------------------------------------------------------------------------

%This part is about regular expressions, Brzozowski derivatives,

%and a bit-coded lexing algorithm with proven correctness and time bounds.

%TODO: look up snort rules to use here--give readers idea of what regexes look like

Regular expressions, since their inception in the 1940s, 

have been subject to extensive study and implementation. 

Their primary application lies in text processing--finding

matches and identifying patterns in a string.

%It is often used to match strings that comprises of numerous fields, 

%where certain fields may recur or be omitted. 

For example, a simple regular expression that tries 

to recognise email addresses is

\marginpar{rephrased from "the regex for recognising" to "a simple regex that tries to match email"}

\begin{center}

%$[a-z0-9._]^+@[a-z0-9.-]^+\.[a-z]{2,6}$.

\end{center}

\marginpar{Simplified example, but the distinction between . and escaped . is correct

%Using this, regular expression matchers and lexers are able to extract 

%the domain names by the use of \verb|[a-zA-Z0-9.-]+|. 

\marginpar{Rewrote explanation for the expression.}

The bracketed sub-expressions are used to extract specific parts of an email address.

The local part is recognised by the expression enclosed in 

the first pair of brackets: $[a-z0-9._]$, and after the ``@'' sign

is the part that recognises the domain, where $[a-z]{2, 6}$ specifically

matches the top-level domain.

%Consequently, they are an indispensible components in text processing tools 

%of software systems such as compilers, IDEs, and firewalls.

The study of regular expressions is ongoing due to an

issue known as catastrophic backtracking. 

This phenomenon refers to scenarios in which the regular expression 

matching or lexing engine exhibits a disproportionately long 

runtime despite the simplicity of the input and expression.

One cause of catastrophic backtracking lies within the 

ambiguities of lexing.\marginpar{rephrased "the origin of catastrophic ...} 

In the process of matching a multi-character string with 

a regular expression that encompasses several sub-expressions, 

different positions can be designated to mark 

the boundaries of corresponding substrings of the sub-expressions. 

For instance, in matching the string $aaa$ with the 

regular expression $(a+aa)^*$, the divide between 

the initial match and the subsequent iteration could either be 

set between the first and second characters ($a | aa$) or between the second and third characters ($aa | a$). As both the length of the input string and the structural complexity of the regular expression increase, the number of potential delimiter combinations can grow exponentially, leading to a corresponding increase in complexity for algorithms that do not optimally navigate these possibilities.

Catastrophic backtracking facilitates a category of computationally inexpensive attacks known as Regular Expression Denial of Service (ReDoS) attacks. Here, an attacker merely dispatches a small attack string to a server, provoking high-complexity behaviours in the server's regular expression engine. Such attacks, whether intentional or accidental, have led to the failure of real-world systems (additional details can be found in the practical overview section in chapter \ref{Introduction}).

Various disambiguation strategies are 

employed to select sub-matches, notably including Greedy and POSIX strategies. POSIX, the strategy most widely adopted in practice, invariably opts for the longest possible sub-match. Kuklewicz \cite{KuklewiczHaskell}, for instance, offers a descriptive definition of the POSIX rule in section 1, last paragraph:

%Regular expressions 

%have been extensively studied and

%implemented since their invention in 1940s.

%It is primarily used in lexing, where an unstructured input string is broken

%down into a tree of tokens.

%That tree's construction is guided by the shape of the regular expression.

%This is particularly useful in expressing the shape of a string

%with many fields, where certain fields might repeat or be omitted.

%Regular expression matchers and Lexers allow us to 

%identify and delimit different subsections of a string and potentially 

%extract information from inputs, making them

%an indispensible component in modern software systems' text processing tasks

%such as compilers, IDEs, and firewalls.

%Research on them is far from over due to the well-known issue called catastrophic-backtracking,

%which means the regular expression matching or lexing engine takes an unproportional time to run 

%despite the input and the expression being relatively simple.

%

%Catastrophic backtracking stems from the ambiguities of lexing: 

%when matching a multiple-character string with a regular 

%exression that includes serveral sub-expressions, there might be different positions to set 

%the border between sub-expressions' corresponding sub-strings.

%For example, matching the string $aaa$ against the regular expression

%$(a+aa)^*$, the border between the initial match and the second iteration

%could be between the first and second character ($a | aa$) 

%or between the second and third character ($aa | a$).

%As the size of the input string and the structural complexity 

%of the regular expression increase,

%the number of different combinations of delimiters can grow exponentially, and

%algorithms that explore these possibilities unwisely will also see an exponential complexity.

%

%Catastrophic backtracking allow a class of computationally inexpensive attacks called

%Regular expression Denial of Service attacks (ReDoS), in which the hacker 

%simply sends out a small attack string to a server, 

%triggering high-complexity behaviours in its regular expression engine. 

%These attacks, be it deliberate or not, have caused real-world systems to go down (see more 

%details of this in the practical overview section in chapter \ref{Introduction}).

%There are different disambiguation strategies to select sub-matches, most notably Greedy and POSIX.

%The widely adopted strategy in practice is POSIX, which always go for the longest sub-match possible.

%There have been prose definitions like the following

%by Kuklewicz \cite{KuklewiczHaskell}: 

%described the POSIX rule as (section 1, last paragraph):

\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}

However, the author noted that various lexers that claim to be POSIX 

are rarely correct according to this standard.

There are numerous occasions where programmers realised the subtlety and

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

\footnote{\url{https://pkg.go.dev/regexp\#pkg-overview}}

\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.

Formal proofs are

machine checked programs

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

for computer scientists to be certain 

about the correctness of their algorithms.

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.

Formal proofs provides an unprecendented level of asssurance

that an algorithm will perform as expected under all inputs.

The software systems that help people interactively build and check

such proofs are called theorem-provers or 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 is a theorem prover 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).

There have been many interesting steps in the theorem-proving community 

about formalising regular expressions and lexing.

One flavour is to build from the regular expression an automaton, and determine

acceptance in terms of the resulting 

state after executing the input string on that automaton.

Automata formalisations are in general harder and more cumbersome to deal

with for theorem provers than working directly on regular expressions.

One such example is by Nipkow \cite{Nipkow1998}.

%They 

%made everything recursive (for example the next state function),

As a core idea, they

used a list of booleans to name each state so that 

after composing sub-automata together, renaming the states to maintain

the distinctness of each state is recursive and simple.

The result was the obvious lemmas incorporating  

``a painful amount of detail'' in their formalisation.

Sometimes the automata are represented as graphs. 

But graphs are not inductive datatypes.

Having to set the induction principle on the number of nodes

in a graph makes formal reasoning non-intuitive and convoluted,

resulting in large formalisations \cite{Lammich2012}. 

When combining two graphs, one also needs to make sure that the nodes in

both graphs are distinct, which almost always involve

renaming of the nodes.

A theorem-prover which provides dependent types such as Coq 

can alleviate the issue of representing graph nodes

\cite{Doczkal2013}. There the representation of nodes is made

easier by the use of $\textit{FinType}$.

Another representation for automata are matrices. 

But the induction for them is not as straightforward either.

There are some more clever representations, for example one by Paulson 

using hereditarily finite sets \cite{Paulson2015}. 

There the problem with combining graphs can be solved better. 

%but we believe that such clever tricks are not very obvious for 

%the John-average-Isabelle-user.

The approach that operates directly on regular expressions circumvents the problem of

conversion between a regular expression and an automaton, thereby avoiding representation

problems altogether, despite that regular expressions may be seen as a variant of a

non-deterministic finite automaton (ref Laurikari tagged NFA paper).

To matching a string, a sequence of algebraic transformations called 

(Brzozowski) $\textit{derivatives}$ (ref Brzozowski) is carried out on that regular expression.

Each derivative takes a character and a regular expression, 

and returns a new regular expression whose language is closely related to 

the original regular expression's language:

strings prefixed with that input character will have their head removed

and strings not prefixed

with that character will be eliminated. 

After taking derivatives with respect to all the characters the string is

exhausted. Then an algorithm checks whether the empty string is in that final 

regular expression's language.

If so, a match exists and the string is in the language of the input regular expression.

Again this process can be seen as the simulation of an NFA running on a string,

but the recursive nature of the datatypes and functions involved makes

derivatives a perfect object of study for theorem provers.

That is why there has been numerous formalisations of regular expressions

and Brzozowski derivatives in the functional programming and 

theorem proving community (a large list of refs to derivatives formalisation publications).

Ribeiro and Du Bois \cite{RibeiroAgda2017} have 

formalised the notion of bit-coded regular expressions

and proved their relations with simple regular expressions in

the dependently-typed proof assistant Agda.

They also proved the soundness and completeness of a matching algorithm

based on the bit-coded regular expressions. Their algorithm is a decision procedure

that gives a Yes/No answer, which does not produce

lexical values.

%X also formalised derivatives and regular expressions, producing "parse trees".

%(Some person who's a big name in formal methods)

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

children of alternatives at different levels by merging them together.

Proving $\blexersimp$ requires a different

proof strategy compared to that by Ausaf \cite{FahadThesis}.

We invent a rewriting relation as an

inductive predicate which captures 

a strong enough invariance that ensures correctness,

which commutes with the derivative operation. 

This predicate allows a simple

induction on the input string to go through.

%This idea has been repeatedly used in different variants of lexing

%algorithms in their paper, one of which involves bit-codes. The bit-coded