#+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{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{\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{\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{\subseteq}}
#+latex_header: \newunicodechar{⊎}{\ensuremath{\uplus}}
#+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 4
# #+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 "the pseudocode").
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 "small" 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
** Hoare Logic
** Agda

* 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