path: root/thesis.org

#+options: ':t *:t -:t ::t <:t H:4 \n:nil ^:t arch:headline author:t
#+options: broken-links:nil c:nil creator:nil d:(not "LOGBOOK") date:t e:t
#+options: email:nil f:t inline:t num:t p:nil pri:nil prop:nil stat:t tags:t
#+options: tasks:t tex:t timestamp:t title:t toc:nil todo:t |:t

#+title: Semantics of an embedded vector architecture for formal verification of software
#+date: May 2022
#+author: Greg Brown
#+latex_header: \newcommand{\candidatenumber}{2487C}
#+latex_header: \newcommand{\college}{Queens' College}
#+latex_header: \newcommand{\course}{Computer Science Tripos, Part III}

#+email: greg.brown@cl.cam.ac.uk
#+language: en-GB
#+select_tags: export
#+exclude_tags: noexport
#+creator: Emacs 27.2 (Org mode 9.6)
#+cite_export: biblatex
#+bibliography: ./thesis.bib

#+latex_class: thesis
#+latex_class_options: [12pt,a4paper,twoside]

#+latex_header: \usepackage[hyperref=true,url=true,backend=biber,natbib=true]{biblatex} % citations
#+latex_header: \usepackage[vmargin=20mm,hmargin=25mm]{geometry} % page margins
#+latex_header: \usepackage{minted}         % code snippets
#+latex_header: \usepackage{parskip}        % vertical space for paragraphs
#+latex_header: \usepackage{setspace}       % line spacing
#+latex_header: \usepackage{newunicodechar} % unicode in code snippets
#+latex_header: \usepackage{ebproof}        % Hoare logic rules
#+latex_header: \usepackage{mathtools}      % a math character?
#+latex_header: \usepackage{stmaryrd}       % some math characters
#+latex_header: \usepackage{refcount}       % for counting pages
#+latex_header: \usepackage{upquote}        % for correct quotation marks in verbatim text

#+latex_compiler: pdflatex


#+latex_header: \newunicodechar{ʳ}{\ensuremath{^\texttt{r}}}
#+latex_header: \newunicodechar{ˡ}{\ensuremath{^\texttt{l}}}
#+latex_header: \newunicodechar{Γ}{\ensuremath{\Gamma}}
#+latex_header: \newunicodechar{Δ}{\ensuremath{\Delta}}
#+latex_header: \newunicodechar{Κ}{\ensuremath{K}}
#+latex_header: \newunicodechar{Σ}{\ensuremath{\Sigma}}
#+latex_header: \newunicodechar{γ}{\ensuremath{\gamma}}
#+latex_header: \newunicodechar{δ}{\ensuremath{\delta}}
#+latex_header: \newunicodechar{ε}{\ensuremath{\epsilon}}
#+latex_header: \newunicodechar{λ}{\ensuremath{\lambda}}
#+latex_header: \newunicodechar{σ}{\ensuremath{\sigma}}
#+latex_header: \newunicodechar{ᵗ}{\ensuremath{^\texttt{t}}}
#+latex_header: \newunicodechar{′}{\ensuremath{'}}
#+latex_header: \newunicodechar{₁}{\ensuremath{_1}}
#+latex_header: \newunicodechar{₂}{\ensuremath{_2}}
#+latex_header: \newunicodechar{ₛ}{\ensuremath{_\texttt{s}}}
#+latex_header: \newunicodechar{ₜ}{\ensuremath{_\texttt{t}}}
#+latex_header: \newunicodechar{ℓ}{l}
#+latex_header: \newunicodechar{ℕ}{\ensuremath{\mathbb{N}}}
#+latex_header: \newunicodechar{ℚ}{\ensuremath{\mathbb{Q}}}
#+latex_header: \newunicodechar{ℝ}{\ensuremath{\mathbb{R}}}
#+latex_header: \newunicodechar{ℤ}{\ensuremath{\mathbb{Z}}}
#+latex_header: \newunicodechar{⇒}{\ensuremath{\rightarrow}}
#+latex_header: \newunicodechar{∀}{\ensuremath{\forall}}
#+latex_header: \newunicodechar{∃}{\ensuremath{\exists}}
#+latex_header: \newunicodechar{∘}{\ensuremath{\circ}}
#+latex_header: \newunicodechar{∙}{\ensuremath{\cdot}}
#+latex_header: \newunicodechar{∧}{\ensuremath{\wedge}}
#+latex_header: \newunicodechar{∨}{\ensuremath{\vee}}
#+latex_header: \newunicodechar{∷}{\texttt{::}}
#+latex_header: \newunicodechar{≈}{\ensuremath{\approx}}
#+latex_header: \newunicodechar{≉}{\ensuremath{\not\approx}}
#+latex_header: \newunicodechar{≔}{\ensuremath{\coloneqq}}
#+latex_header: \newunicodechar{≟}{\ensuremath{\buildrel ?\over =}}
#+latex_header: \newunicodechar{≡}{\ensuremath{\equiv}}
#+latex_header: \newunicodechar{≢}{\ensuremath{\not\equiv}}
#+latex_header: \newunicodechar{⊆}{\ensuremath{\subseteq}}
#+latex_header: \newunicodechar{⊎}{\ensuremath{\uplus}}
#+latex_header: \newunicodechar{⊔}{\ensuremath{\sqcup}}
#+latex_header: \newunicodechar{⊤}{\ensuremath{\top}}
#+latex_header: \newunicodechar{⊥}{\ensuremath{\bot}}
#+latex_header: \newunicodechar{⌊}{\ensuremath{\lfloor}}
#+latex_header: \newunicodechar{⌋}{\ensuremath{\rfloor}}
#+latex_header: \newunicodechar{⟦}{\ensuremath{\llbracket}}
#+latex_header: \newunicodechar{⟧}{\ensuremath{\rrbracket}}
#+latex_header: \newunicodechar{⟶}{\ensuremath{\rightarrow}}
#+latex_header: \newunicodechar{⦃}{\{\{}
#+latex_header: \newunicodechar{⦄}{\}\}}
#+latex_header: \newunicodechar{𝕀}{\ensuremath{\mathbb{I}}}

#+latex_header: %TC:envir minted 1 ignore

#+latex_header: \newif\ifsubmission

# Uncomment when anonymous
# #+latex_header: \submissiontrue

#+begin_src elisp :exports results :results none :eval export
(make-variable-buffer-local 'org-latex-title-command)
(setq org-latex-title-command
"
%%TC:ignore

\\begin{sffamily}

\\begin{titlepage}

\\makeatletter
\\hspace*{-14mm}\\includegraphics[width=65mm]{logo-dcst-colour}

\\ifsubmission

%% submission proforma cover page for blind marking
\\begin{Large}
\\vspace{20mm}
Research project report title page

\\vspace{35mm}
Candidate \\candidatenumber

\\vspace{42mm}
\\textsl{\`\`\\@title\'\'}

\\end{Large}

\\else

%% regular cover page
\\begin{center}
\\Huge
\\vspace{\\fill}

\\@title
\\vspace{\\fill}

\\@author
\\vspace{10mm}

\\Large
\\college
\\vspace{\\fill}

\\@date
\\vspace{\\fill}

\\end{center}

\\fi

\\vspace{\\fill}
\\begin{center}
Submitted in partial fulfillment of the requirements for the\\\\
\\course
\\end{center}

\\end{titlepage}

\\end{sffamily}

\\makeatother
\\newpage

%%TC:endignore
")
#+end_src

#+begin_export latex

%TC:ignore

\begin{sffamily}

Total page count: \pageref{lastpage}

% calculate number of pages from
% \label{firstcontentpage} to \label{lastcontentpage} inclusive
\makeatletter
\@tempcnta=\getpagerefnumber{lastcontentpage}\relax%
\advance\@tempcnta by -\getpagerefnumber{firstcontentpage}%
\advance\@tempcnta by 1%
\xdef\contentpages{\the\@tempcnta}%
\makeatother

Main chapters (excluding front-matter, references and appendix):
\contentpages~pages
(pp~\pageref{firstcontentpage}--\pageref{lastcontentpage})

#+end_export

#+name: wordcount
#+begin_src elisp :exports none :eval export
(if (not (boundp 'squid-eval))
    (setq squid-eval nil))

(if (not squid-eval)
    (progn
      (setq squid-eval t)
      (org-latex-export-to-latex)
      (setq squid-eval nil)))

(let* ((outfile (org-export-output-file-name ".tex")))
  (shell-command-to-string (concat "texcount -0 -sum \'" outfile "\'")))
#+end_src

Main chapters word count: call_wordcount()

#+begin_export latex
Methodology used to generate that word count:

\begin{quote}
\begin{verbatim}
$ texcount -0 -sum report.tex
xyz
\end{verbatim}
\end{quote}

\end{sffamily}

\onehalfspacing
#+end_export

* Abstract
:PROPERTIES:
:unnumbered: t
:END:

#+latex: \ifsubmission\else

* Acknowledgements
:PROPERTIES:
:unnumbered: t
:END:

#+latex: \fi
#+latex: \cleardoublepage

#+toc: headlines 2
# #+toc: listings
# #+toc: tables

#+latex: %TC:endignore

* Introduction

#+latex: \label{firstcontentpage}

The ultimate goal of this work was to formally verify an implementation
[cite:@10.46586/tches.v2022.i1.482-505] of the number-theoretic transform (NTT)
for the Armv8.1-M architecture.  The NTT is a vital procedure for lattice-based
post-quantum cryptography (FIXME: cite). To ensure internet-connected embedded
devices remain secure in the future of large-scale quantum computers,
implementations of these algorithms, and hence the NTT, are required for the
architectures they use. One common architecture used by embedded devices is
Armv8-M (FIXME: cite). Due to the resource-constrained nature of an embedded
device, and the huge computational demands of post-quantum cryptography,
algorithms like the NTT are presented using hand-written, highly-optimised
assembly code. To ensure the correctness of these cryptographic algorithms, and
thus the security of embedded devices, formal verification of these algorithms
is necessary.

This report focuses on formalising the semantics of the Armv8-M architecture.
[cite/t:@arm/DDI0553B.s] provides a pseudocode description of the operation of
Armv8-M instructions using the Arm pseudocode (henceforth \ldquo{}the
pseudocode\rdquo{}).  Unfortunately this language is primarily designed for
describing instructions (FIXME: cite) and not proving properties of executing
them.

To remedy this, I designed AMPSL, which mocks the pseudocode specification
language. AMPSL is written in the dependently-typed Agda proof assistant
[cite:@10.1007/978-3-642-03359-9_6]. The syntax mirrors that of the pseudocode,
save some minor modifications due to limitations within Agda and adjustments to
simplify the semantics. Using Agda enables AMPSL, its semantics, and proofs
using and about the semantics to be written using a single language.

AMPSL is given semantics in two different forms. The first is a denotational
semantics, which converts the various program elements into functions within
Agda. This enables the explicit computation of the effect of AMPSL on the
processor state. AMPSL also has a set of Hoare logic rules, which form an
axiomatic, syntax-directed approach to describing how a statement in AMPSL
modifies assertions on the processor state.

Another significant line of work undertaken by this report is the formal
verification of Barrett reduction. Barrett reduction is an important subroutine
used by the NTT, to efficiently find a \ldquo{}small\rdquo{} representable of a
value modulo some base [cite:@10.1007/3-540-47721-7_24]. Much like how a
formalisation of the NTT is a big step in formalising the behaviour of many PQC
algorithms, formalising Barrett reduction is a big step in formalising the NTT.

The main contributions of this report are as follows:
- In [[*AMPSL Syntax]], I introduce the syntax of the AMPSL programming language.
  The primary goal of the syntax is to facilitate easy translation of programs
  from the Arm pseudocode, detailed in [[*Arm Pseudocode]] into AMPSL, whilst
  allowing AMPSL semantics to remain simple.
- The semantics of AMPSL are described in [[*AMPSL Semantics]]. The primary
  achievement of this work is the simple semantics of AMPSL, which facilitates
  straight-forward proofs about various AMPSL programs. I detail both a
  denotational semantics and a Hoare logic for AMPSL. The Hoare logic used by
  AMPSL somewhat varies from the traditional presentation, given in [[*Hoare
  Logic]], to enforce that Hoare logic proofs have bounded depth with respect to
  the program syntax.
- In [[*Soundness of AMPSL's Hoare Logic]], I prove that the Hoare logic rules for
  AMPSL are sound with respect to the denotational semantics. This proof is
  possible due to Agda's foundation of Martin-Löf's type theory, the
  significance of which is given in [[*Agda]]. Due to the soundness of AMPSL's Hoare
  logic, the behaviour of the computationally-intensive denotational semantics
  can instead be specified using syntax-directed Hoare logic.
- A number of example proofs for AMPSL programs are given in [[*Using AMPSL for
  Proofs]]. This demonstrates the viability of using AMPSL for the formal
  verification of a number of programs, and lays the groundwork for the formal
  verification of the NTT given by [cite/t:@10.46586/tches.v2022.i1.482-505].
- Finally, a formal proof of a Barrett reduction variant is given in [[*Proof of
  Barrett Reduction]]. (FIXME: As far as I can tell) giving this well-used
  algorithm a formal machine proof is a novel endeavour. Further, it is the
  first proof of Barrett reduction on a domain other than integers and
  rationals.


# This is the introduction where you should introduce your work. In
# general the thing to aim for here is to describe a little bit of the
# context for your work -- why did you do it (motivation), what was the
# hoped-for outcome (aims) -- as well as trying to give a brief overview
# of what you actually did.

# It's often useful to bring forward some ``highlights'' into this
# chapter (e.g.\ some particularly compelling results, or a particularly
# interesting finding).

# It's also traditional to give an outline of the rest of the document,
# although without care this can appear formulaic and tedious. Your
# call.

* Background

# A more extensive coverage of what's required to understand your work.
# In general you should assume the reader has a good undergraduate
# degree in computer science, but is not necessarily an expert in the
# particular area you have been working on. Hence this chapter may need to
# summarize some ``text book'' material.

# This is not something you'd normally require in an academic paper, and
# it may not be appropriate for your particular circumstances. Indeed,
# in some cases it's possible to cover all of the ``background''
# material either in the introduction or at appropriate places in the
# rest of the dissertation.

** Arm Pseudocode
The Armv8.1-M pseudocode specification language is a strongly-typed imperative
programming language [cite:@arm/DDI0553B.s §E1.2.1]. It has a first-order type
system, a small set of operators and basic control flow, as you would find in
most imperative languages. Its primary purpose is to explain how executing an
Armv8-M instruction modifies the visible processor state. As it is a descriptive
aid, the pseudocode features a number of design choices atypical of other
imperative programming languages making execution difficult.

Something common to nearly all imperative languages is the presence of a
primitive type for Booleans. Other typical type constructors are tuples,
structs, enumerations and fixed-length arrays. The first interesting type used
by the pseudocode is mathematical integers as a primitive type. Most imperative
languages use fixed-width integers for primitive types, with exact integers
available through some library. Examples include Rust (FIXME: cite), C (FIXME:
cite), Java (FIXME: cite) and Go (FIXME: cite). This is because the performance
benefits of using fixed-width integers in code far outweigh the risk of
overflow. As checking for integer overflow complicates algorithms, and the
pseudocode is not designed to execute, the pseudocode can make use of exact
mathematical integers to eliminate overflow errors without any of the drawbacks
[cite:@arm/DDI0553B.s §E1.3.4].

Another odd type present in the pseudocode is mathematical real numbers. As most
real numbers are impossible to record using finite storage, any executable
programming language must make compromises to the precision of real numbers.
This is usually achieved through floating-point numbers, which represent only a
negligible fraction of possible real number values. However, as the pseudocode
is not executable, the types it use do not need to have a finite representation.
Thus it is free to use real numbers and have exact precision in real-number
arithmetic [cite:@arm/DDI0553B.s §E1.2.4].

The final primitive type used by the pseudocode is the bitstring; a fixed-length
sequence of 0s and 1s. Some readers may wonder what the difference is between
this type and arrays of Booleans. The justification given by
[cite/t:@arm/DDI0553B.s §E1.2.2] is more philosophical than practical:
\ldquo{}bitstrings are the only concrete data type in pseudocode\rdquo{}. In
some places, bitstrings can be used instead of integers in arithmetic
operations, by first converting them to an unsigned integer.

Most of the operators used by the pseudocode are unsurprising. For instance,
Booleans have the standard set of short-circuiting operations; integers and
reals have addition, subtraction and multiplication; reals have division;
integers have integer division (division rounding to \(-\infty\)) and modulus
(the remainder of division); and concatenation of bitstrings.

The most interesting operation in the pseudocode is bitstring slicing. First,
there is no type for a bit outside a bitstring---a single bit is represented as
a bitstring of length one---so bitstring slicing always returns a bitstring.
Slicing then works in much the same way as array slicing in languages like
Python (FIXME: cite?) and Rust (FIXME: cite?); slicing an integer range from a
bitstring returns a new bitstring with values corresponding to the indexed bits.
The other special feature of bitstring slicing is that an integer can be sliced
instead of a bitstring. In that case, the pseudocode \ldquo{}treats an integer
as equivalent to a sufficiently long [\ldots] bitstring\rdquo{}
[cite:@arm/DDI0553B.s §E1.3.3].

The final interesting difference between the pseudocode and most imperative
languages is the variety of top-level items. The pseudocode has three forms of
items: procedures, functions and array-like functions. Procedures and functions
behave like procedures and functions of other imperative languages. The
arguments to them are passed by value, and the only difference between the two
is that procedures do not return values whilst functions do
[cite:@arm/DDI0553B.s §E1.4.2].

Array-like functions act as getters and setters for machine state. Every
array-like function has a reader form, and most have a writer form. This
distinction exists because \ldquo{}reading from and writing to an array element
require different functions\rdquo{}, [cite:@arm/DDI0553B.s §E1.4.2], likely due
to the nature of some machine registers being read-only instead of
read-writeable. The writer form acts as one of the targets of assignment
expressions, along with variables and the result of bitstring concatenation and
slicing [cite:@arm/DDI0553B.s §E1.3.5].

(FIXME: examples)

** Hoare Logic
Hoare logic is a proof system for programs written in imperative programming
languages. At its core, the logic describes how to build partial correctness
triples, which describe how program statements affect assertions about machine
state. The bulk of a Hoare logic derivation is dependent only on the syntax of
the program the proof targets.

A partial correctness triple is a relation between a precondition \(P\), a
program statement \(s\) and a postcondition \(Q\). If \(\{P\} s \{Q\}\) is a
partial correctness triple, then whenever \(P\) holds for some machine state,
then when executing \(s\), \(Q\) holds for the state after it terminates
[cite:@10.1145/363235.363259]. This is a /partial/ correctness triple because
the postcondition only holds if \(s\) terminates. When all statements terminate,
this relation is called a correctness triple.

#+name: WHILE-Hoare-logic
#+caption: Hoare logic rules for the WHILE language, consisting of assignment,
#+caption: if statements and while loops. The top three lines show the structural
#+caption: rules, and the bottom shows the adaptation rule.
#+begin_figure
\begin{center}
\begin{prooftree}
  \infer0[SKIP]{\{P\}\;\texttt{s}\;\{P\}}
  \infer[rule style=no rule,rule margin=3ex]1{\{P\}\;\texttt{s₁}\;\{Q\}\qquad\{Q\}\;\texttt{s₂}\;\{R\}}
  \infer1[SEQ]{\{P\}\;\texttt{s₁;s₂}\;\{Q\}}
  \infer0[ASSIGN]{\{P[\texttt{x}/\texttt{v}]\}\;\texttt{x:=v}\;\{P\}}
  \infer[rule style=no rule,rule margin=3ex]1{\{P \wedge \texttt{e}\}\;\texttt{s₁}\;\{Q\}\qquad\{P \wedge \neg \texttt{e}\}\;\texttt{s₂}\;\{Q\}}
  \infer1[IF]{\{P\}\;\texttt{if e then s₁ else s₂}\;\{Q\}}
  \infer[rule style=no rule,rule margin=3ex]2{\{P \wedge \texttt{e}\}\;\texttt{s}\;\{P\}}
  \infer1[WHILE]{\{P\}\;\texttt{while e do s}\;\{P \wedge \neg \texttt{e}\}}
  \infer[rule style=no rule,rule margin=3ex]1{\models P_1 \rightarrow P_2\qquad\{P_2\}\;\texttt{s}\;\{Q_2\}\qquad\models Q_2 \rightarrow Q_1}
  \infer1[CSQ]{\{P_1\}\;\texttt{s}\;\{Q_1\}}
\end{prooftree}
\end{center}
#+end_figure

[[WHILE-Hoare-logic]] shows the rules Hoare introduced for the WHILE language
[cite:@10.1145/363235.363259]. The SKIP and SEQ rules are straight-forward: the
skip statement has no effect on state, and sequencing statements composes their
effects. The IF rule is also uncomplicated. No matter which branch we take, the
postcondition remains the same; an if statement does no computation after
executing a branch.  Which branch we take depends on the value of ~e~. Because
the value of ~e~ is known before executing a branch, it is added to the
preconditions in the premises.

The ASSIGN rule appears backwards upon first reading; the substitution is
performed in the precondition, before the assignment occurs! When considered
more deeply, you realise the reason for this reversal. Due to the assignment,
any occurrence of ~v~ in the precondition can be replaced by ~x~, and the
original value of ~x~ is lost. Hence the postcondition can only use ~x~ exactly
where there was ~v~ in the precondition. This is enforced by the substitution.

The final structural Hoare logic rule for the WHILE language is the WHILE rule.
This rule can be derived by observing the fixed-point nature of a while
statement. As ~while e do s~ is equivalent to ~if e then (s ; while e do s) else
skip~, we can use the IF, SEQ and SKIP rules to solve the recursion equation for
the precondition and postcondition of the while statement.

The final Hoare logic rule is the rule of consequence, CSQ. This rule does not
recurse on the structure of the statement ~s~, but instead adapts the
precondition and postcondition. In this case, we can weaken the precondition and
postcondition using logical implication.

[cite/t:@10.1145/363235.363259] does not specify the logic used to evaluate the
implications in the rule of consequence. Regular choices are first-order logic
and higher-order logic
[cite:@10.1007/s00165-019-00501-3;@10.1007/s001650050057]. For specifying
program behaviour, one vital aspect of the choice of logic is the presence of
auxiliary variables [cite:@10.1007/s001650050057]. Auxiliary variables are a set
of variables that cannot be used within a program, but they can be quantified
over within assertions or left as free variables. A free auxiliary variable
remains constant between the precondition and postcondition, and are
universally-quantified within proofs.

 (FIXME: examples)

** Agda
Agda is a dependently-typed proof assistant and functional programming language,
based on Martin-Löf's type theory.  The work of
[cite/t:@10.1007/978-3-642-03359-9_6] provides an excellent introduction to the
language. This section provides a summary of the most important features for the
implementation of AMPSL.

*Inductive families*. Data types like you would find in ML or Haskell can not
only be indexed by types, but by specific values. This is best illustrated by an
example. Take for instance fixed-length vectors. They can be defined by the
following snippet:

#+begin_src agda2
data Vec (A : Set) : ℕ → Set where
  []  : Vec A 0
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)
#+end_src

First consider the type of ~Vec~. It is a function that accepts a type ~A~ and a
natural number, and returns a type. The position of ~A~ to the left of the colon
is significant; it is a /parameter/ of ~Vec~ instead of an /index/. Parameters
are required to be the same for all constructors, whilst indices can vary
between constructors [cite:@agda.readthedocs.io p.
\texttt{language/data-types.html}]. This means the following definition of ~Vec~
is invalid:

#+begin_src agda2
data Vec (A : Set) (n : ℕ) : Set where
  [] : Vec A 0
  -- 0 ≢ n  -^
  _\::_ : ∀ {n} → A → Vec A n → Vec A (suc n)
  -- and suc n ≢ n -------------------^
#+end_src

Whilst the value of parameters is constant in the return values of constructors,
they can vary across the arguments of constructors, even for the same type. One
example of this is the ~Assertion~ type given in (FIXME: forwardref) later in
the report. The ~all~ and ~some~ constructors both accept an ~Assertion Σ Γ (t ∷
Δ)~, but because they return an ~Assertion Σ Γ Δ~ the definition is valid.

*Parameterised modules and records*. Agda modules can accept parameters, which
can be used anywhere in the module. This works well with Agda's record types,
are a generalisation of a dependent product. (In fact, the builtin Σ type is
defined using a record [cite:@agda.readthedocs.io p.
\texttt{language/built-ins.html}].) The following snippet shows how records can
be used to define a setoid-enriched monoid:

#+begin_src agda2
record Monoid ℓ₁ ℓ₂ : Set (ℓsuc (ℓ₁ ⊔ ℓ₂)) where
  infixl 5 _∙_
  infix 4 _≈_
  field
    Carrier : Set ℓ₁
    _≈_     : Rel A ℓ₂
    _∙_     : Op₂ Carrier
    ε       : Carrier
    refl    : ∀ {x} → x ≈ x
    sym     : ∀ {x y} → x ≈ y → y ≈ x
    trans   : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
    ∙-cong  : ∀ {x y u v} → x ≈ y → u ≈ v → x ∙ y ≈ u ∙ v
    ∙-assoc : ∀ {x y z} → (x ∙ y) ∙ z ≈ x ∙ (y ∙ z)
    ∙-idˡ   : ∀ {x} → ε ∙ x ≈ x
    ∙-idʳ   : ∀ {x} → x ∙ ε ≈ x
#+end_src

This record bundles together an underlying ~Carrier~ type with an equality
relation ~_≈_~, binary operator ~_∙_~ and identity element ~ε~. It also contains
all the proofs necessary to show that ~_≈_~ is really an equality and that ~_∙_~
and ~ε~ form a monoid.

When a module is parameterised by a ~Monoid~, then the module has an abstract
monoid. It can use the structure and laws given in the record freely, but it
cannot use additional laws (e.g. commutativity) without an additional argument.
This is useful when the operations and properties of a type are well-defined,
but a good representation is unknown.

*Instance arguments* Instance arguments are analogous to the type class
constraints you find in Haskell [cite:@agda.readthedocs.io p.
\texttt{language/instance-arguments.html}]. They are a special form of implicit
argument that are solved via /instance resolution/ over unification.  Instance
arguments are a good solution for cases where Agda tries \ldquo{}too
hard\rdquo{} to find a solution for implicit arguments, and needs the implicit
arguments to be specified implicitly. Using instance arguments instead can force
a particular solution onto Agda without needing to give the arguments
explicitly.

* Related Work

# This chapter covers relevant (and typically, recent) research
# which you build upon (or improve upon). There are two complementary
# goals for this chapter:
# \begin{enumerate}
#   \item to show that you know and understand the state of the art; and
#   \item to put your work in context
# \end{enumerate}

# Ideally you can tackle both together by providing a critique of
# related work, and describing what is insufficient (and how you do
# better!)

# The related work chapter should usually come either near the front or
# near the back of the dissertation. The advantage of the former is that
# you get to build the argument for why your work is important before
# presenting your solution(s) in later chapters; the advantage of the
# latter is that don't have to forward reference to your solution too
# much. The correct choice will depend on what you're writing up, and
# your own personal preference.

* Design of AMPSL and its Semantics

# This chapter may be called something else... but in general the
# idea is that you have one (or a few) ``meat'' chapters which describe
# the work you did in technical detail.

** AMPSL Syntax

** AMPSL Semantics

* Properties and Evaluation of AMPSL

# For any practical projects, you should almost certainly have some kind
# of evaluation, and it's often useful to separate this out into its own
# chapter.

** Soundness of AMPSL's Hoare Logic

** Using AMPSL for Proofs

* Proof of Barrett Reduction

# This chapter may be called something else\ldots but in general the
# idea is that you have one (or a few) ``meat'' chapters which describe
# the work you did in technical detail.

* Summary and Conclusions

# As you might imagine: summarizes the dissertation, and draws any
# conclusions. Depending on the length of your work, and how well you
# write, you may not need a summary here.

# You will generally want to draw some conclusions, and point to
# potential future work.

#+latex: \label{lastcontentpage}

#+latex: %TC:ignore

#+print_bibliography:

\appendix

#+latex: \label{lastpage}
#+latex: %TC:endignore

#  LocalWords:  AMPSL Hoare NTT PQC structs bitstring bitstrings