Fresh start.

2 files changed, 286 insertions, 1820 deletions

diff --git a/thesis.bib b/thesis.bib
index adf7e5e..ef2797f 100644
--- a/thesis.bib
+++ b/thesis.bib
@@ -144,3 +144,17 @@ date = {2019-12},
 pages = {751–807},
 numpages = {57}
 }
+
+@InProceedings{10.1007/3-540-47721-7_24,
+author="Barrett, Paul",
+editor="Odlyzko, Andrew M.",
+title="Implementing the Rivest Shamir and Adleman Public Key Encryption Algorithm on a Standard Digital Signal Processor",
+booktitle="Advances in Cryptology --- CRYPTO' 86",
+date="1987",
+publisher="Springer Berlin Heidelberg",
+address="Berlin, Heidelberg",
+pages="311--323",
+abstract="A description of the techniques employed at Oxford University to obtain a high speed implementation of the RSA encryption algorithm on an ``off-the-shelf'' digital signal processing chip. Using these techniques a two and a half second (average) encrypt time (for 512 bit exponent and modulus) was achieved on a first generation DSP (The Texas Instruments TMS 32010) and times below one second are achievable on second generation parts. Furthermore the techniques of algorithm development employed lead to a provably correct implementation.",
+isbn="978-3-540-47721-1",
+doi = {10.1007/3-540-47721-7_24}
+}
diff --git a/thesis.org b/thesis.org
index fc1df6a..7cfdaab 100644
--- a/thesis.org
+++ b/thesis.org
@@ -1,10 +1,15 @@
 #+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:t todo:t |: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: \today
+#+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
@@ -12,16 +17,21 @@
 #+creator: Emacs 27.2 (Org mode 9.6)
 #+cite_export: biblatex
 #+bibliography: ./thesis.bib
+
 #+latex_class: thesis
-#+latex_class_options: [twoside,a4paper,11pt]
-#+latex_header: \usepackage[hyperref=true,url=true,backend=biber,natbib=true]{biblatex}
-#+latex_header: \usepackage[moderate]{savetrees}
-#+latex_header: \usepackage[a4paper]{geometry}
-#+latex_header: \usepackage{minted}
-#+latex_header: \usepackage{newunicodechar}
-#+latex_header: \usepackage{mathtools}
-#+latex_header: \usepackage{stmaryrd}
-#+latex_header: \usepackage[english=british]{csquotes}
+#+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}}
@@ -38,6 +48,7 @@
 #+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}}}
@@ -69,1887 +80,328 @@
 #+latex_header: \newunicodechar{⦄}{\}\}}
 #+latex_header: \newunicodechar{𝕀}{\ensuremath{\mathbb{I}}}
 
-#+latex_header: %TC:envir minted 1 other
-
-#+begin_abstract
-All good implementations of any algorithm should be correct and fast. To
-maximise performance some algorithms are written in hand-tuned assembly. This
-can introduce subtle bugs that invalidate correctness or other safety
-properties. Whilst tools exists to help formally verify these algorithms, none
-are designed to target the recent M-profile Vector Extension for the Armv8.1-M
-architecture. This work describes a denotational and Hoare logic semantics for
-the language used to specify the instructions, and attempts to use them to
-formally verify the correctness of hand-written assembly for cryptographic
-applications.
-#+end_abstract
-
-# Flip this all around. What am I doing? What is the stuff? Why is it hard? (Why
-# am I smart?)
-* Introduction
+#+latex_header: %TC:envir minted 1 ignore
 
-# Merge these two paras
-In nearly all cases, the best implementation of an algorithm for a particular
-purpose is both correct and fast. If the implementation is not correct, then it
-does not implement the algorithm. If the implementation is slow, then resources are
-wasted executing this algorithm over performing other useful work. Ensuring
-implementations are both performant and correct is typically difficult.
-
-One case that proves particularly tricky is writing assembly code.
-# dubious claim
-Most modern handwritten assembly is for cryptographic algorithms, where it is
-vital that compilers do not introduce timing attacks or other side channels.
-Hand written assembly can also take advantage of microarchitectural differences
-to gain a slight performance benefit.
-
-Another domain that frequently deals with assembly code is the output of
-compilers. Optimising compilers take the semantic operations described by
-high-level code and attempt to produce the optimal machine code to perform those
-actions.
-
-In both of these cases, either humans or machines shuffle around instructions in
-an attempt to eek out the best performance from hardware. The resulting code
-warps the original algorithms in ways that make it difficult to determine
-whether the actions performed actually have the same result. The correctness of
-the assembly code comes into question.
-
-It is only possible to prove the assembly code is correct if there is a model
-describing how it should behave. Suitable mathematical models of the behaviour
-allow for the construction of formal proofs certifying the assembly code has the
-correct behaviour. Due to the size and complexity of different instruction set
-architectures (ISAs), formal verification of software in this manner makes use
-of a number of software tools.
-
-Formal verification software is well-developed for the x86-64 and Arm A-profile
-ISAs. For instance, Jasmin [cite:@10.1145/3133956.3134078] is a programming
-language which verifies that compiling to x86-64 preserves a set of user-defined
-safety properties. Another similar tool is CompCert [cite:@hal/01238879] which
-is a verified C compiler, ensuring that the program semantics are preserved
-during compilation.
-
-Unfortunately, little work has been done to formally verify software written for
-the Arm M-profile architecture. This architecture is designed for low-power and
-low-latency microcontrollers, which operate in resource-constrained
-environments.
-
-The goal of this project is to formally verify an assembly function for the Arm
-M-profile architecture. The specific algorithm
-[cite:@10.46586/tches.v2022.i1.482-505] is a hand-written highly-optimised
-assembly-code implementation of the number-theoretic transform, which is an
-important procedure for post-quantum cryptography.
-
-This work has made progress on two fronts. Most work has been spent developing
-an embedding and semantic model of the Armv8.1-M pseudocode specification
-language for the Agda programming language [cite:@10.1007/978-3-642-03359-9_6].
-All instructions in the Armv8.1-M architecture are given a "precise description"
-[cite:@arm/DDI0553B.s §\(\texttt{I}_\texttt{RTDZ}\)] using the pseudocode, and
-by developing an embedding within Agda, it is possible to use its powerful type
-system to construct formal proofs of correctness.
-
-Progress has also been made on the formal algebraic verification of Barrett
-reduction, a subroutine of the NTT.  Whilst there exists a paper proof of the
-correctness of Barrett reduction, a proof of Barrett reduction within Agda is
-necessary to be able to prove the correctness of the given implementation of the
-NTT.
-
-# Focus on contributions
-# Structure of the paper:
-# - [[Armv8.1-M Pseudocode Specification Language]] describes the Armv8.1-M pseudocode
-#   specification language. This is an imperative programming language used by the
-#   Armv8.1-M manual to describe the operation of the instructions.
-# - A simple recap of Hoare logic is given in [[Hoare Logic]]. This is the backbone of
-#   one of the formal verification techniques used in this work.
-# - [[Formal Definition of MSL]] contains a description of MSL. This is a language
-#   similar to the Armv8.1-M pseudocode embedded within the Agda programming
-#   language.
-# - The denotational semantics and a Hoare logic semantics of MSL are detailed in
-#   [[Semantics of MSL]]. Due to Agda's nature of being a dependently-typed language,
-#   these are both given using Agda code.
-# - [[Application to Proofs]] describes the experience of using the Hoare logic and
-#   denotational semantics of MSL to prove the correctness of some simple
-#   routines, given in [[Proofs using Hoare Semantics]] and [[Proofs using Denotational
-#   Semantics]] respectively.
-# - Formal verification of Barrett reduction, an important subroutine in the NTT,
-#   is given in [[Proofs of Barrett Reduction]]. In particular, it proves that Barrett
-#   reduction performs a modulo reduction and gives bounds on the size of the
-#   result.
-# - Finally, [[Future Work]] describes the steps necessary to complete the formal
-#   verification of the NTT, as well as listing some other directions this work
-#   can be taken.
+#+latex_header: \newif\ifsubmission
 
-* Background
-The Armv8.1-M pseudocode specification language is used to describe the
-operation of instructions in the Armv8-M instruction set [cite:@arm/DDI0553B.s §E1.1]. If the semantics of this pseudocode can be formalised, then it is
-possible to formulate proofs about the action of all Armv8-M instructions, and
-hence construct proofs about the algorithms written with them. The language is
-rather simple, being pseudocode used as a descriptive aid, but has some
-interesting design choices atypical of regular imperative programming languages.
-
-As the pseudocode is an imperative language, one useful proof system for it is
-Hoare logic. Hoare logic is a proof system driven by the syntax of a program,
-with most of the hard work of proofs being in the form of choosing suitable
-program invariants and solving simple logical implications
-[cite:@10.1145/363235.363259]. As the logic is syntax driven, proofs using Hoare
-logic are less impacted than other proof systems by the large number of loops
-used in Armv8-M instruction descriptions.  Further, solving simple logical
-implications is a task well-suited to Agda and other proof assistants, making
-proofs even simpler to construct.
-
-** Armv8.1-M Pseudocode Specification Language
-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. There are some interesting design choices atypical of
-regular imperative languages to better fulfil the requirements of being a
-descriptive aid over an executable language.
-
-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. This is because the performance benefits of
-using fixed-width integers in code far outweigh the risk of overflow. However,
-as the pseudocode is a descriptive aid, with no intention of being executed, it
-can use exact mathematical integers and eliminate overflow errors without any
-performance cost [cite:@arm/DDI0553B.s §E1.3.4].
-
-Another such 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.
-Because the pseudocode does not concern itself with being executable, 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:
-"bitstrings are the only concrete data type in pseudocode". In some places,
-bitstrings can be used instead of integers in arithmetic operations.
-
-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; and
-integers have integer division (division rounding to \(-\infty\)) and modulus
-(the remainder of division).
-
-By far the two most interesting operations in the pseudocode are bitstring
-concatenation and slicing. Bitstring concatenation is much like appending two
-arrays together, or regular string concatenation. Bitstring slicing is a more
-nuanced process. Slicing a bitstring by a single index is no different from a
-regular array access. If instead a bitstring is sliced by a range of integers,
-the result is the concatenation of each single-bit access. Finally, when
-integers are sliced instead of bitstring, the pseudocode "treats an integer as
-equivalent to a sufficiently long \textelp{} bitstring" [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 "reading from and writing to an array element require
-different functions", [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].
+# Uncomment when anonymous
+# #+latex_header: \submissiontrue
 
-** 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].  Those last three words, "after it terminates",
-are what leads the relation being a /partial/ correctness triple. If all
-statements terminate, which we will see later, then this relation is called a
-correctness triple.
-
-Along with the syntactic rules for derivations, Hoare logic typically also
-features a number of adaptation rules. The most-widely known of these is the
-rule of consequence, which can strengthen the precondition and weaken the
-postcondition. This requires an additional logic for assertions. Typically, this
-is first-order or higher-order logic
-[cite:@10.1007/s00165-019-00501-3;@10.1007/s001650050057].
-
-One vital feature of Hoare logic with regards to specification is auxiliary
-variables. These are variables that cannot be used by programs, hence remain
-constant between the precondition and postcondition
-[cite:@10.1007/s001650050057].
-
-* The MIPSL Language
-The ultimate goal of this project is to formally verify an implementation of the
-number theoretic transform using the M-profile vector extension of the Armv8.1-M
-architecture. Work has proceeded on two fronts. This chapter discusses the
-first; a formal definition of a language similar to the Armv8-M pseudocode
-specification language, which I will call MIPSL (MIPSL imitates pseudocode
-specification language). This definition exists within Agda, allowing for the
-use of Agda's dependent-typing features to construct proofs about programs
-written in MIPSL.
-
-To construct proofs about how MIPSL behaves, it is necessary to describe its
-semantics. This is done through providing a denotational semantics. Denotational
-semantics interpret program expressions and statements as mathematical
-functions, something which Agda is well-suited to do.
-
-One downside of denotational semantics is that control flow for looping
-constructs is fully evaluated. This is inefficient for loops that undergo many
-iterations. This can be resolved by a syntax-directed Hoare logic for MIPSL.
-Hoare logic derivations assign a precondition and a postcondition assertion to
-each statement. These are chained together though a number of simple logical
-implications.
-
-** Definition of MIPSL
-MIPSL is a language similar to the Armv8-M pseudocode specification language
-written entirely in Agda. Unfortunately, the pseudocode has a number of small
-features that make it difficult to work with in Agda directly. MIPSL makes a
-number of small changes to the pseudocode to better facilitate this embedding,
-typically generalising existing features of the pseudocode.
-
-*** MIPSL Types
-
-#+name: MIPSL-types
-#+caption: The Agda datatype representing the types present in MIPSL. Most have
-#+caption: a direct analogue in the Armv8-M pseudocode specification language
-#+attr_latex: :float t
-#+begin_src agda2
-data Type : Set where
-  bool  : Type
-  int   : Type
-  fin   : (n : ℕ) → Type
-  real  : Type
-  tuple : Vec Type n → Type
-  array : Type → (n : ℕ) → Type
-#+end_src
+#+begin_src elisp :exports results :results none :eval export
+(make-variable-buffer-local 'org-latex-title-command)
+(setq org-latex-title-command
+"
+%%TC:ignore
 
-[[MIPSL-types]] gives the Agda datatype representing the types of MIPSL. Most of
-these have a direct analogue to the pseudocode types. For example, ~bool~ is a
-Boolean, ~int~ mathematical integers, ~real~ is for real numbers and ~array~
-constructs array types. Instead of an enumeration construct, MIPSL uses the ~fin
-n~ type, representing a finite set of ~n~ elements. Similarly, structs are
-represented by ~tuple~ types.
+\\begin{sffamily}
 
-The most significant difference between the pseudocode and MIPSL is the
-representation of bitstrings. Whilst the pseudocode has the ~bits~ datatype,
-MIPSL instead treats bitstrings as an array of Booleans, demonstrated by this
-code fragment:
+\\begin{titlepage}
 
-#+begin_src agda2
-bit : Type
-bit = bool
+\\makeatletter
+\\hspace*{-14mm}\\includegraphics[width=65mm]{logo-dcst-colour}
 
-bits : ℕ → Type
-bits = array bit
-#+end_src
+\\ifsubmission
 
-This removes the distinction between arrays and bitstrings, and allows a number
-of operations to be generalised to work on both types. This makes MIPSL more
-expressive than the pseudocode, in the sense that there are a greater number and
-more concise ways to write programs that are functionally equivalent.
-
-#+name: MIPSL-type-properties
-#+caption: Prototypes for the three predicates on types.
-#+attr_latex: :float t
-#+begin_src agda2
-data HasEquality : Type → Set
-data Ordered     : Type → Set
-data IsNumeric   : Type → Set
-#+end_src
+%% submission proforma cover page for blind marking
+\\begin{Large}
+\\vspace{20mm}
+Research project report title page
 
-The pseudocode implicitly specifies three different properties of types: equality
-comparisons, order comparisons and arithmetic operations. Whilst the types
-satisfying these properties need to be listed explicitly in Agda, using instance
-arguments allows for these proofs to be elided whenever they are required.
-[[MIPSL-type-properties]] gives the type signatures of the three predicates.
-
-MIPSL has only two differences in types that satisfy these properties compared
-to the pseudocode. First, all array types have equality as long as the
-enumerated type also has equality. This is a natural generalisation of the
-equality between types, and allows for the MIPSL formulation of bitstrings as
-arrays of Booleans to have equality. Secondly, finite sets also have ordering.
-This change is primarily a convenience feature for comparing finite representing
-a subset of integers. As the pseudocode has no ordering comparisons between
-enumerations, this causes no problems for converting pseudocode programs into
-MIPSL.
-
-#+name: MIPSL-type-addition
-#+caption: Definition of the "type addition" feature of MIPSL.
-#+attr_latex: :float t
-#+begin_src agda2
-_+ᵗ_ : IsNumeric t₁ → IsNumeric t₂ → Type
-int  +ᵗ int  = int
-int  +ᵗ real = real
-real +ᵗ t₂   = real
-#+end_src
+\\vspace{35mm}
+Candidate \\candidatenumber
 
-The final interesting feature of the types in MIPSL is "type addition". As
-pseudocode arithmetic is polymorphic for integers and reals, MIPSL needs a
-function to decide the type of the result. [[MIPSL-type-addition]] gives the
-definition of this function.
-
-*** MIPSL Expressions
-
-#+name: MIPSL-literalType
-#+caption: Mappings from MIPSL types into Agda types which can be used as
-#+caption: literal values. ~literalTypes~ is a function that returns a product
-#+caption: of the types given in the argument.
-#+begin_src agda
-literalType : Type → Set
-literalType bool        = Bool
-literalType int         = ℤ
-literalType (fin n)     = Fin n
-literalType real        = ℤ
-literalType (tuple ts)  = literalTypes ts
-literalType (array t n) = Vec (literalType t) n
-#+end_src
+\\vspace{42mm}
+\\textsl{\`\`\\@title\'\'}
 
-Unlike the pseudocode, where only a few types have literal expressions, every
-type in MIPSL has a literal form. This mapping is part of the ~literalType~
-function, given in [[MIPSL-literalType]]. Most MIPSL literals accept the
-corresponding Agda type as a value. For instance, ~bool~ literals are Agda
-Booleans, and ~array~ literals are fixed-length Agda vectors of the
-corresponding underlying type. The only exception to this rule is for ~real~
-values. As Agda does not have a type representing mathematical reals, integers
-are used instead.
-
-# TODO: why is this sufficient?
-
-#+name: MIPSL-expr-prototypes
-#+caption: Prototypes of the numerous MIPSL program elements. Each one takes two
-#+caption: variable contexts: ~Σ~ for global variables and ~Γ~ for local variables.
-#+attr_latex: :float t
-#+begin_src agda
-data Expression     (Σ : Vec Type o) (Γ : Vec Type n) : Type → Set
-data Reference      (Σ : Vec Type o) (Γ : Vec Type n) : Type → Set
-data LocalReference (Σ : Vec Type o) (Γ : Vec Type n) : Type → Set
-data Statement      (Σ : Vec Type o) (Γ : Vec Type n) : Set
-data LocalStatement (Σ : Vec Type o) (Γ : Vec Type n) : Set
-data Function       (Σ : Vec Type o) (Γ : Vec Type n) (ret : Type) : Set
-data Procedure      (Σ : Vec Type o) (Γ : Vec Type n) : Set
-#+end_src
-
-One important benefit of using Agda to write MIPSL is that expressions and
-statements can have the MIPSL types of variables be part of the Agda type.
-This makes checking type safety of variable usage trivial.
-
-For reasons which will be discussed later, MIPSL uses two variable contexts, ~Σ~
-for global variables and ~Γ~ for local variables. [[MIPSL-expr-prototypes]] lists
-the prototypes for the various MIPSL program elements. The full definitions of
-these types are given in [[*MIPSL Syntax Definition]].
-
-An ~Expression~ in MIPSL corresponds with expressions in the pseudocode. Many
-operators are identical to those in the pseudocode (like ~+~, ~*~, ~-~), and
-others are simple renamings (like ~≟~ instead of ~==~ for equality comparisons).
-Unlike the pseudocode, where literals can appear unqualified, MIPSL literals
-are introduced by the ~lit~ constructor.
-
-The most immediate change for programming in MIPSL versus the pseudocode is how
-variables are handled. Because the ~Expression~ type carries fixed-length
-vectors listing the MIPSL types of variables, a variable is referred to by its
-index into the context. For example, a variable context \(\{x \mapsto
-\mathrm{int}, y \mapsto \mathrm{real}\}\) is represented in MIPSL as the
-context ~int ∷ real ∷ []~. The variable \(x\) is then represented by ~var 0F~ in
-MIPSL. Because the global and local variable contexts are disjoint for the
-~Expression~ types, variables are constructed using ~state~ or ~var~ respectively.
-
-Whilst this decision introduces much complexity to programming using MIPSL, it
-greatly simplifies the language for use in constructing proofs. For instance, by
-referring to variables by their index in the variable context, variable
-shadowing, where two variables share a name, is completely eliminated from
-MIPSL.
-
-MIPSL expressions also add a number of useful constructs to the pseudocode type.
-One such pair is ~[_]~ and ~unbox~, which construct and destruct an array of
-length one respectively. Another pair are ~fin~, which allows for arbitrary
-computations on elements of finite sets, and ~asInt~, which converts a finite
-value into an integer.
-
-The three MIPSL operators most likely to cause confusion are ~merge~, ~slice~
-and ~cut~. ~slice~ is analogous to bitstring slicing from the pseudocode, but
-has some important differences. Instead of operating on bitstrings and integers,
-~slice~ acts on ~array~ types. Integer slicing can be expressed using the
-other operators of MIPSL, and in MIPSL a bitstring is a form of array. Another
-difference is that the number of bits to take from the string is not specified
-by a range, but is instead inferred from the output type. This is only possible
-due to the powerful type inference features of Agda. Finally, the user only
-needs to provide a single index into the array. By giving the index a ~fin~
-datatype, and taking care with the length of arrays, MIPSL can guarantee that
-the array indices are always in bounds for the entire range that is required.
-
-The ~cut~ operation is an opposite to ~slice~. Whilst ~slice~ takes a contiguous
-range of elements from the middle of an array, ~cut~ returns the two ends of the
-array outside of the range. Finally, ~merge~ is a generalisation of
-concatenation that allows inserting one array into another. These three
-operations are part of an equivalence; for any arrays ~x~ and ~y~ and an
-appropriate index ~i~, we have the following equalities:
-- ~merge (slice x i) (cut x i) i ≟ x~
-- ~slice (merge x y i) i ≟ x~
-- ~cut (merge x y i) i ≟ y~
-
-The ~Reference~ type is the name MIPSL gives to assignable expressions from the
-pseudocode. The ~LocalReference~ type is identical to ~Reference~, except it
-does not include global variables. In an earlier form of MIPSL, instead of
-separate types for assignable expressions which can and cannot assign to state,
-there were two predicates. However, this required carrying around a proof that
-the predicate holds with each assignment. Whilst the impacts on performance were
-unmeasured, it made proving statements with assignable expressions significantly
-more difficult. Thankfully, Agda is able to resolve overloaded data type
-constructors without much difficulty, meaning the use of ~Reference~ and
-~LocalReference~ in MIPSL programs is transparent.
-
-**** Example MIPSL Expressions
-For those who have read [[*MIPSL Syntax Definition]], you may notice that whilst the
-pseudocode defines a left-shift operator, there is no such operator in MIPSL.
-Left shift can be defined in the following way:
-
-#+begin_src agda2
-_<<_ : Expression Σ Γ int → (n : ℕ) → Expression Σ Γ int
-e << n = e * lit (ℤ.+ (2 ℕ.^ n))
-#+end_src
+\\end{Large}
 
-This simple-looking expression has a lot of hidden complexity. First, consider
-the type of the literal statement. The unary plus operation tells us that the
-literal is an Agda integer. However, there are two MIPSL types with Agda
-integers for literal values: ~int~ and ~real~. How does Agda correctly infer the
-type? Recall that multiplication is polymorphic in MIPSL, with the result type
-determined by "type addition" ([[MIPSL-type-addition]]). Agda knows that the
-multiplication must return an ~int~, and that the first argument is also an
-~int~, so by following the definition of ~_+ᵗ_~, it can infer that the second
-multiplicand is an integer literal.
-
-The previous section claimed that it is possible to define integer slicing
-entirely using the other operations in MIPSL. Here is an expression that slices
-a single bit from an integer, following the procedure by [cite/t:@arm/DDI0553B.s
-§E1.3.3]:
-
-#+begin_src agda2
-getBit : ℕ → Expression Σ Γ int → Expression Σ Γ bit
-getBit i x =
-  if x - x >> suc i << suc i <? lit (ℤ.+ (2 ℕ.^ i))
-  then lit false
-  else lit true
-#+end_src
+\\else
 
-The left-side of the inequality finds the residual of ~x~ modulo \(2 ^ {i+1}\).
-Note that right-shift is defined to always round values down hence the modulus
-is always positive. If the modulus is less than \(2^i\), then the bit in the
-two's complement representation of ~x~ is ~0~, otherwise it is ~1~. This is
-reflected in the output values of ~lit false~ and ~lit true~ respectively.
-
-The last expression I will present is the ~uint~ function, which converts a
-bitstring into an unsigned integer.
-
-#+begin_src agda2
-uint : Expression Σ Γ (bits m) → Expression Σ Γ int
-uint {m = 0}           x = lit ℤ.0ℤ
-uint {m = 1}           x =
-  if unbox x
-  then lit ℤ.1ℤ
-  else lit ℤ.0ℤ
-uint {m = suc (suc m)} x =
-  lit (ℤ.+ 2) * uint (slice x (lit 1F)) +
-  uint (cut x (lit 1F))
-#+end_src
+%% regular cover page
+\\begin{center}
+\\Huge
+\\vspace{\\fill}
 
-This Agda function is inductive on the number of bits in the argument. In the
-first case, the unique zero-length bitstring is represented by the constant
-\(0\). In the second case, a single bit can be represented by a conditional
-statement: the integer \(1\) if the bit is true and \(0\) otherwise. If there
-are two or more bits, the resulting expression sums two expressions. The left
-addend is twice the recursive call on the high bits of the input. The right
-addend is the representation of the least-significant bit as an integer.
-
-In more concrete terms, here's the result of ~uint~ on a 4-bit string:
-
-#+begin_src agda2
-lit 2 *
-(lit 2 *
- (lit 2 *
-  (if unbox (slice (slice (slice x (lit 1F)) (lit 1F)) (lit 1F))
-   then lit 1
-   else lit 0)
-  +
-  (if unbox (cut (slice (slice x (lit 1F)) (lit 1F)) (lit 1F))
-   then lit 1
-   else lit 0))
- +
- (if unbox (cut (slice x (lit 1F)) (lit 1F))
-  then lit 1
-  else lit 0))
-+
-(if unbox (cut x (lit 1F))
- then lit 1
- else lit 0)
-#+end_src
+\\@title
+\\vspace{\\fill}
 
-FIXME: why did I give this example at all? It's ugly, hard to understand, and if
-anything only demonstrates why my project fails to work efficiently. This will
-be cut if no one can find a purpose for it during review.
-
-*** MIPSL Statements
-MIPSL statements form a subset of statements allowed in the pseudocode. There
-are three omissions: ~while...do~ loops, ~repeat...until~ loops and
-~try...catch~ exception handling. Each of these structures is only used in
-high-level constructs, such as the top-level execution loop
-[cite:@arm/DDI0553B.s §E2.1.397], converting reals into floating-point
-bitstrings [cite:@arm/DDI0553B.s §E2.1.166] and inserting instructions into the
-instruction queue [cite:@arm/DDI0553B.s §E2.1.366].
-
-The ultimate goal of MIPSL is to accurately represent the operation of a
-specific instruction sequence on visible registers and memory, over simulating
-the entirety of processor state.  Hence these high-level parts of the processor
-behaviour, like managing the instruction queue, are not relevant.
-
-Another argument for excluding these constructs is that it vastly complicates
-the semantics of MIPSL. Of particular concern to Agda is that the presence of
-potentially-unending loops, such as a ~while...do~ loop, would violate the
-termination condition of Agda functions if it were included in a denotational
-semantics.
-
-Most of the statements that are present in MIPSL are unsurprising. The ~skip~
-and sequencing (~_∙_~) statements should be familiar from the discussion on
-Hoare logic, the assignment statement (~_≔_~) assigns a value into a reference,
-the ~invoke~ statement calls a procedure and the ~if_then_else_~ statement
-starts a conditional block.
-
-Given that MIPSL has a ~skip~ statement and an ~if_then_else_~ control-flow
-structure, including the ~if_then_~ statement may appear redundant. Ultimately,
-the statement is redundant. It is regardless included in MIPSL for two reasons.
-The first is ergonomics. ~if_then_~ statements appear many times more often in
-the pseudocode than ~if_then_else_~ statements that omitting it would only serve
-to complicate the code. The other reason is that including an ~if_then_else_~
-statement makes the behaviour of a number of functions that manipulate MIPSL
-code much easier to reason about.
-
-The form of variable declarations is significantly different in MIPSL than it is
-in the pseudocode. As variables in MIPSL are accessed by index into the variable
-context instead of by name, MIPSL variable declarations do not need a name. In
-addition, Agda can often infer the type of a declared variable from the context
-in which it is used, making type annotations unnecessary. The last difference is
-that all variables in MIPSL must be initialised. This simplifies the semantics
-of MIPSL greatly, and prevents the use of uninitialised variables.
-
-MIPSL makes a small modification to ~for~ loops that greatly improve the type
-safety over what is achieved by the pseudocode. Instead of looping over a range
-of dynamic values [cite:@arm/DDI0553B.s §E1.4.4], MIPSL loops perform a static
-number of iterations, determined by an Agda natural ~n~. Then, instead of the
-loop variable being an assignable integer expression, MIPSL introduces a new
-variable with type ~fin n~.
-
-MIPSL has a ~LocalStatement~ type as well as a ~Statement~ type. Whilst
-~Statement~ can assign values into any ~Reference~, a ~LocalStatement~ can only
-assign values into a ~LocalReference~. This means that ~LocalStatement~ cannot
-modify global state, only local state.
-
-**** Example MIPSL Statements
-Here is a statement that copies elements from ~y~ into ~x~ if the corresponding
-entry in ~mask~ is true:
-
-#+begin_src agda2
-copy : Statement Σ (array t n ∷ array t n ∷ array bool n ∷ [])
-copy =
-  for n (
-    let i = var 0F in
-    let x = var 1F in
-    let y = var 2F in
-    let mask = var 3F in
-
-    if index mask i ≟ true
-    then
-        *index x i ≔ index y i
-  )
-#+end_src
+\\@author
+\\vspace{10mm}
 
-This uses Agda functions ~index~ and ~*index~ to apply the appropriate slices,
-casts and unboxing to extract an element from an array expression and reference,
-respectively. One thing of note is the use of ~let...in~ to give variables
-meaningful names. This is a stylistic choice that works well in this case.
-Unfortunately, if the ~if_then_~ statement declared a new variable, these naming
-variables would become useless, as the types would be different. For example
-consider the following snippet:
-
-#+begin_src agda2
-VPTAdvance : Statement State (beat ∷ [])
-VPTAdvance =
-  declare (fin div2 (tup (var 0F ∷ []))) (
-  declare (elem 4 (! VPR-mask) (var 0F)) (
-    let vptState = var 0F in
-    let maskId = var 1F in
-    let beat = var 2F in
-
-    if ! vptState ≟ lit (true ∷ false ∷ false ∷ false ∷ [])
-    then
-      vptState ≔ lit (Vec.replicate false)
-    else if inv (! vptState ≟ lit (Vec.replicate false))
-    then (
-      declare (lit false) (
-        let i = var 0F in
-        let vptState = var 1F in
-        -- let mask = var 2F in
-        let beat = var 3F in
-
-        cons vptState (cons i nil) ≔ call (LSL-C 0) (! vptState ∷ []) ∙
-        if ! i
-        then
-          *elem 4 VPR-P0 beat ≔ not (elem 4 (! VPR-P0) beat))) ∙
-    if getBit 0 (asInt beat)
-    then
-      *elem 4 VPR-mask maskId ≔ ! vptState))
-#+end_src
+\\Large
+\\college
+\\vspace{\\fill}
 
-This corresponds to the ~VPTAdvance~ procedure by [cite/t:@arm/DDI0553B.s
-§E2.1.424]. Notice how every time a new variable is introduced, the variable
-names have to be restated. Whilst this is a barrier when trying to write
-programs in MIPSL, the type-safety guarantees and simplified proofs over using
-named variables more than make up the difference.
-
-*** MIPSL Functions and Procedures
-Much like how a procedure in the pseudocode is a wrapper around a block of
-statements, ~Procedure~ in MIPSL is a wrapper around ~Statement~. Note that
-MIPSL procedures only have one exit point, the end of a statement, unlike the
-pseudocode which has ~return~ statements. Any procedure using a ~return~
-statement can be transformed into one that does not by a simple refactoring, so
-MIPSL does not lose any expressive power over the pseudocode.
-
-MIPSL functions are more complex than procedures. A function consists of a pair
-of an ~Expression~ and ~LocalStatement~. The statement has the function
-arguments and the return value as local variables, where the return value is
-initialised to the result of the expression. The return value of the function is
-then the final value of the return variable.
-
-Functions and procedures are the reason MIPSL has two variable contexts, one
-each for the global and local variables. The set of global variables is
-unchanged across function and procedure boundaries. However, the set of local
-variables is completely different. Having a separate variable for each in the
-type is the cleanest way to represent this separation in Agda.
-
-**** Example MIPSL Functions and Procedures
-As ~Procedure~ is almost an alias for ~Statement~, examples of procedures can be
-found in [[*Example MIPSL Statements]]. This is a simple function that converts a
-bitstring to an unsigned or signed integer, depending on whether the second
-argument is true or false:
-
-#+begin_src agda2
-Int : Function State (bits n ∷ bool ∷ []) int
-Int =
-  init
-    if var 1F
-    then uint (var 0F)
-    else sint (var 0F) ∙
-    skip
-  end
-#+end_src
+\\@date
+\\vspace{\\fill}
 
-The function body is the ~skip~ statement, meaning that whatever is initially
-assigned to the return variable is the result of calling the function. The
-initial value of the return variable is a simple conditional statement, calling
-~uint~ or ~sint~ on the first argument as appropriate. Many functions that are
-easy to inline have this form.
-
-The ~GetCurInstBeat~ function by [cite/t:@arm/DDI0553B.s §E2.1.185] is one
-function that benefits from the unusual representation of functions. A
-simplified MIPSL version is given below.
-
-#+begin_src agda2
-GetCurInstrBeat : Function State [] (tuple (beat ∷ elmtMask ∷ []))
-GetCurInstrBeat =
-  init
-    tup (! BeatId ∷ lit (Vec.replicate true) ∷ []) ∙ (
-      let outA = head (var 0F) in
-      let outB = head (tail (var 0F)) in
-      if call VPTActive (! BeatId ∷ [])
-      then
-        outB ≔ !! outB and elem 4 (! VPR-P0) outA
-    )
-  end
-#+end_src
+\\end{center}
 
-The function initialises a default return value, and then modifies it based on
-the current state of execution. This is easy to encode in the MIPSL function
-syntax. The return variable is initialised to the default value, and the
-function body performs the necessary manipulations.
-
-In this way a function is much like a ~declare~ statement. However, instead of
-discarding the declared variable when it leaves scope, a function returns it to
-the caller.
-
-** MIPSL Semantics
-The ultimate goal of this work is to formally verify an assembly algorithm
-written for the Armv8.1-M architecture that performs the number theoretic
-transform. So far we have discussed the syntactic form of MIPSL, which is a
-language similar to the Armv8-M pseudocode specification language, written in
-Agda. We have also given a brief high-level semantics of MIPSL. Formal
-verification requires a much more detailed description of the semantics than
-what has been given so far.
-
-This section starts with a brief discussion of how to model MIPSL types. This
-addresses the burning question of how to model real numbers in Agda.  From this,
-we discuss the denotational semantics of MIPSL, and how MIPSL program elements
-can be converted into a number of different Agda function types. The section
-ends with a presentation of a Hoare logic for MIPSL, allowing for efficient
-syntax-directed proofs of statements.
-
-*** MIPSL Datatype Models
-#+name: MIPSL-type-models
-#+caption: The semantic encoding of MIPSL data types. The use of ~Lift~ is to
-#+caption: ensure all the encodings occupy the same Agda universe level.
-#+begin_src agda2
-⟦_⟧ₜ  : Type → Set ℓ
-⟦_⟧ₜₛ : Vec Type n → Set ℓ
-
-⟦ bool ⟧ₜ      = Lift ℓ Bool
-⟦ int ⟧ₜ       = Lift ℓ ℤ
-⟦ fin n ⟧ₜ     = Lift ℓ (Fin n)
-⟦ real ⟧ₜ      = Lift ℓ ℝ
-⟦ tuple ts ⟧ₜ  = ⟦ ts ⟧ₜₛ
-⟦ array t n ⟧ₜ = Vec ⟦ t ⟧ₜ n
-
-⟦ [] ⟧ₜₛ          = Lift ℓ ⊤
-⟦ t ∷ [] ⟧ₜₛ      = ⟦ t ⟧ₜ
-⟦ t ∷ t₁ ∷ ts ⟧ₜₛ = ⟦ t ⟧ₜ × ⟦ t₁ ∷ ts ⟧ₜₛ
-#+end_src
+\\fi
 
-To be able to write a denotational semantics for a language, the first step is
-to find a suitable encoding for the data types. In this case, we have to be able
-to find encodings of MIPSL types within Agda. [[MIPSL-type-models]] shows the full
-encoding function. Most of the choices are fairly trivial; Agda Booleans for
-~bool~, Agda vectors for ~array t n~ and the Agda finite set type ~Fin n~ for
-the MIPSL type ~fin n~.
-
-# RESOLVED: bit is an alias for bool.
-# In this encoding, ~bool~ and ~bit~ are both represented by Agda Booleans. This
-# again begs the question of why they are distinct types in MIPSL and are not
-# unified into one. The philosophical reasoning used by (FIXME: textcite) is now
-# diluted; ~array~ is used for abstract arrays and physical bitstrings. (FIXME:
-# why are they distinct?)
-
-Tuples are the next simplest type, being encoded as an n-ary product. This is
-the action of the ~⟦_⟧ₜₛ~ function in [[MIPSL-type-models]]. Unfortunately the Agda
-standard library does not have a dependent n-ary product type. In any case, the
-Agda type checker would not accept its usage in this case due to termination
-checking, hence the manual inductive definition.
-
-(ALTERNATIVE 1: ~int~ stays as abstract discrete ordered commutative ring)
-
-The other two MIPSL types are ~int~, ~real~. Whilst ~int~ could feasibly be
-encoded by the Agda integer type, there is no useful Agda encoding for
-mathematical real numbers. Because of this, both numeric types are represented
-by abstract types with the appropriate properties. ~int~ is represented by a
-discrete ordered commutative ring ℤ and ~real~ by a field ℝ. We also require
-that there is a split ring monomorphism \(\mathtt{/1} : ℤ \to ℝ\) with
-retraction \(\mathtt{⌊\_⌋} : ℝ \to ℤ\). \(\mathtt{⌊\_⌋}\) may not be a ring
-homomorphism, but it must preserve \(\le\) ordering and satisfy the floor
-property:
-
-\[
-\forall x y. x < y \mathtt{/1} \implies ⌊ x ⌋ < y
-\]
-
-(ALTERNATIVE 2: ~int~ becomes integer and ~real~ stays abstract)
-
-The other two MIPSL types are ~int~ and ~real~. ~int~ is encoded by the Agda
-integer type. However, there is no useful Agda encoding for mathematical real
-numbers. Because of this, it is represented by an abstract type ℝ such that ℝ is
-a field. We also require that there is a split ring monomorphism \(\mathtt{/1} :
-ℤ \to ℝ\) with retraction \(\mathtt{⌊\_⌋} : ℝ \to ℤ\). \(\mathtt{⌊\_⌋}\) may not
-be a ring homomorphism, but it must preserve \(\le\) ordering and satisfy the
-floor property:
-
-\[
-\forall x y. x < y \mathtt{/1} \implies ⌊ x ⌋ < y
-\]
-
-(ALTERNATIVE 3: ~real~ becomes rational.)
-
-The other two MIPSL types are ~int~ and ~real~. ~int~ is encoded by the Agda
-integer type. However, there is no useful Agda encoding for mathematical real
-numbers. This can be approximated using the Agda rational type ℚ. Whilst this
-clearly cannot encode all real numbers, it satisfies nearly all of the
-properties required by the pseudocode real-number type. The only missing
-operation is square-root, which is unnecessary for the proofs MIPSL is designed
-for.
-
-(END ALTERNATIVES)
-
-*** Denotational Semantics
-
-#+name: MIPSL-denotational-prototypes
-#+caption: Function prototypes for the denotational semantics of different MIPSL
-#+caption: program elements. All of them become functions from the current
-#+caption: variable context into some return value.
-#+begin_src agda2
-expr      : Expression Σ Γ t        → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ t ⟧ₜ
-exprs     : All (Expression Σ Γ) ts → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ ts ⟧ₜₛ
-ref       : Reference Σ Γ t         → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ t ⟧ₜ
-locRef    : LocalReference Σ Γ t    → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ t ⟧ₜ
-stmt      : Statement Σ Γ           → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ
-locStmt   : LocalStatement Σ Γ      → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Γ ⟧ₜₛ
-fun       : Function Σ Γ t          → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ t ⟧ₜ
-proc      : Procedure Σ Γ           → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Σ ⟧ₜₛ
-#+end_src
+\\vspace{\\fill}
+\\begin{center}
+Submitted in partial fulfillment of the requirements for the\\\\
+\\course
+\\end{center}
 
-The denotational semantics has to represent the different MIPSL program elements
-as mathematical objects. In this case, due to careful design of MIPSL's syntax,
-each of the elements is represented by a total function.
-[[MIPSL-denotational-prototypes]] shows the prototypes of the different semantic
-interpretation functions, and the full definition is in [[*MIPSL Denotational
-Semantics]]. Each function accepts the current variable context as an argument.
-Because the variable contexts are an ordered sequence of values of different
-types, they can be encoded in the same way as tuples.
-
-**** Expression Semantics
-
-The semantic representation of an expression converts the current variable
-context into a value with the same type as the expression. Most cases are pretty
-simple. For example, addition is the sum of the values of the two subexpressions
-computed recursively. One of the more interesting cases are global and local
-variables, albeit this is only a lookup in the variable context for the current
-value. This lookup is guaranteed to be safe due to variables being a lookup into
-the current context. Despite both being a subsets of the ~Expression~ type,
-~Reference~ and ~LocalReference~ require their own functions to satisfy the
-demands of the termination checker.
-
-One significant omission from this definition is the checking of evaluation
-order. Due to the design choice that MIPSL functions cannot modify global state,
-and that no MIPSL expression can modify state, expressions have the same value
-no matter the order of evaluation for sub-expressions. This is also reflected in
-the type of the denotational representation of expressions. It can only possibly
-return a value and not a modified version of the state.
-
-**** Assignment Semantics
-#+name: MIPSL-denotational-assign-prototypes
-#+caption: Function prototypes for the ~assign~ and ~locAssign~ helper
-#+caption: functions. The arguments are the reference, new value, original
-#+caption: variable context and the context to update. The original context is
-#+caption: needed to evaluate expressions within the reference.
-#+begin_src agda2
-assign    : Reference Σ Γ t      → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ →
-            ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ
-locAssign : LocalReference Σ Γ t → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ →
-            ⟦ Γ ⟧ₜₛ → ⟦ Γ ⟧ₜₛ
-#+end_src
+\\end{titlepage}
 
-Before considering statements as a whole, we start with assignment statements.
-If assignments were only into variables, this would be a trivial update to the
-relevant part of the context. However, the use of ~Reference~ makes things more
-tricky. Broadly speaking, there are four types of ~Reference~: terminal
-references like ~state~, ~var~ and ~nil~; isomorphism operations like ~unbox~,
-~[_]~ and ~cast~; product operations like ~merge~ and ~cons~; and projection
-operations like ~slice~, ~cut~, ~head~ and ~tail~.
-
-We will consider how to update each of the four types of references in turn,
-which is the action performed by helper functions ~assign~ and ~locAssign~, the
-signatures of which are given in [[MIPSL-denotational-assign-prototypes]].
-
-Terminal references are the base case and easy. Assigning into ~state~ and ~var~
-updates the relevant part of the variable context, whilst assigning into
-~nil~---the unique nullary product---is a no-op. Isomorphic reference operations
-are also relatively simple to assign into. First, transform the argument using
-the inverse operation, and assign that into the sub-reference. For example, the
-assignment ~[ ref ] ≔ v~ is the same as ~ref ≔ unbox v~.
-
-Assigning into product reference operations is also not too complex, by
-assigning into each projection in turn. For example, ~cons r₁ r₂ ≔ v~ is
-equivalent to ~r₁ ≔ head v ∙ r₂ ≔ tail v~. However, some care must be taken to
-ensure only that any expressions in the second assignment use the original, and
-not updated, variable context. This is why ~assign~ and ~locAssign~ have the
-extra context argument.
-
-The final type of reference to consider are the projection reference operations.
-Assigning into one projection of a reference means that the other part remains
-unchanged. Consider the assignment ~head r ≔ v~ as an example. This is
-equivalent to ~r ≔ cons v (tail r)~, which makes it clear that the second
-projection remains constant. The second projection must be computed using the
-original variable context.
-
-This interplay between product and projection reference types is a large part of
-the reason why MIPSL has ~merge~, ~cut~ and ~slice~ instead of the bitstring
-concatenation and slicing present in the Armv8-M pseudocode specification
-language.  There is no way to form a product-projection triple with only
-bitstring joining and slicing, so any denotational semantics with these
-operations would require merge and cut operations on the encoding of values.
-MIPSL takes these semantic necessities and makes them available to programmers.
-
-~assign~ and ~locAssign~, when given a reference and initial context, return
-unary operations on the full and local variable contexts respectively. As
-~Reference~ includes both ~state~ and ~var~, assigning into a reference can
-modify both global and local references. In contrast, ~LocalReference~ only
-features ~var~, so can only modify local variables.
-
-**** Statement Semantics
-Compared to assignment, the semantics of other statements are trivial to
-compute. Skip statements map to the identity function and sequencing is function
-composition, reflecting that they do nothing and compose statements together
-respectively. As expressions cannot modify state, ~if_then_else_~ and ~if_then_~
-statements become simple---evaluate the condition and both branches on the input
-state, and return the branch depending on the value of the condition. Local
-variable declarations are also quite simple. The initial value is computed and
-added to the variable context. After evaluating the subsequent statement, the
-final value of the new variable is stripped away from the context.
-
-The only looping construct in MIPSL is the ~for~ loop. Because it performs a
-fixed number of iterations, it too has easy-to-implement denotational semantics.
-This is because it is effectively a fixed number of ~declare~ statements all
-sequenced together. This is also one of the primary reasons why the denotational
-semantics can have poor computational performance; every iteration of the ~for~
-loop must be evaluated individually.
-
-~stmt~ and ~locStmt~ return the full context and only the local variables
-respectively. This is because only ~Statement~ can include ~Reference~ which can
-reference global state. On the other hand, ~LocalReference~ used by
-~LocalStatement~ can only refer to, and hence modify, local state.
-
-**** Function and Procedure Semantics
-Finally there are ~proc~ and ~fun~ for denoting procedures and functions. ~proc~
-returns the global state only; ~Procedure~ is a thin wrapper around ~Statement~,
-which modifies both local and global state. However, the local state is lost
-when leaving a procedure, hence ~proc~ only returns the global part. ~fun~
-behaves a lot like a ~declare~ statement. It initialises the return variable to
-the given expression, then evaluates the ~LocalStatement~ body. Unlike
-~declare~, which discards the added variable upon exiting the statement, ~fun~
-instead returns the value of that variable. As ~LocalStatement~ cannot modify
-global state, and the other local variables are lost upon exiting the function,
-only this one return value is necessary.
-
-*** Hoare Logic Semantics
-The final form of semantics specified for MIPSL is a form of Hoare logic. Unlike
-the denotational semantics, which must perform a full computation, the Hoare
-logic is syntax-directed; loops only require a single proof. This section starts
-by explaining how a MIPSL ~Expression~ is converted into a ~Term~ for use in
-Hoare logic assertions. Then the syntax and semantics of the ~Assertion~ type is
-discussed before finally giving the form of correctness triples for MIPSL.
-
-**** Converting ~Expression~ into ~Term~
-As discussed in [[*Hoare Logic]], a simple language such as WHILE can use
-expressions as terms in assertions directly. The only modification required is
-the addition of auxiliary variables. MIPSL is not as simple a language as WHILE,
-thanks to the presence of function calls in expressions. Whilst function calls
-do not prevent converting expressions into terms, some care must be taken. In
-particular, this conversion is only possible due to the pure nature of MIPSL
-functions; it would not be possible if functions modified global variables. The
-full definition of ~Term~ and its semantics are given in [[*MIPSL Hoare Logic
-Definitions]].
-
-First, a demonstration on why function calls need special care in Hoare logic.
-We will work in an environment with a single Boolean-valued global variable.
-Consider the following MIPSL function, a unary operator on an integer:
-
-#+begin_src agda2
-f : Function [ bool ] [ int ] int
-f =
-  init
-    var 0F ∙
-    let x = var 1F in
-    let ret = var 0F in
-    if state 0F
-      then ret ≔ lit 1ℤ + x
-  end
-#+end_src
+\\end{sffamily}
 
-When the global variable ~state 0F~ is false, this is the identity function.
-However, when ~state 0F~ is true, ~f~ performs an increment.
-
-Consider an expression ~e : Expression [ bool ] Γ int~ of ~call f [ x ]~.  There
-are three important aspects we need to consider for converting ~e~ into a term:
-the initial conversion; substitution of variables; and the semantics. The
-simplest conversion is to keep the function call as-is, and simply recursively
-convert ~x~ into a term. This would result in a term ~e′ = call f [ x′ ]~, using
-~′~ to indicate the term embedding.
-
-What would happen when we try and substitute ~state 0F~ for ~t~, a term
-involving local variables in ~Γ~, into ~e′~? As ~f~ refers to ~state 0F~, it
-must be modified in some way. However, ~Γ~ is a different variable context from
-~[ int ]~, so there is no way of writing ~t~ inside of ~f~. This embedding is
-not sufficient.
-
-A working solution comes from the insight that a ~Function~ in MIPSL can only
-read from global variables, and never write to them. Instead of thinking of ~f~
-as a function with a set of global variables and a list of arguments, you can
-consider ~f~ to be a function with two sets of arguments. In an ~Expression~,
-the first set of arguments always corresponds exactly with the global variables,
-so is elided. We can then define an embedding function ~↓_~, such that ~↓ e =
-call f [ state 0F ] [ ↓ x ]~, and all the other expression forms as expected.
-This makes the elided arguments to ~f~ explicit.
-
-Doing a substitution on ~↓ e~ is now simple: perform the substitution on both
-sets of arguments recursively, and leave ~f~ unchanged. As the first set of
-arguments correspond exactly to the global variables in ~f~, the substitution
-into those arguments appears like a substitution into ~f~ itself.
-
-The last major consideration of this embedding is how to encode its semantics.
-To be able to perform logical implications within Hoare logic, it is necessary
-to have a semantic interpretation for assertions and thus terms. Going back to
-~↓ e~, we already have a denotational semantics for ~f~. Hence we only need to
-consider the global and local variables we pass to ~f~ to get the value. We
-simply pass ~f~ the values of the global and local argument lists for the values
-of the global and local arguments respectively. Thus ~↓ e~ is a valid conversion
-from ~Expression~ to ~Term~.
-
-The only other difference between ~Expression~ and ~Term~ is the use of
-auxiliary variables within Hoare logic terms. MIPSL accomplishes this by
-providing a ~meta~ constructor much like ~state~ and ~var~. This indexes into a
-new auxiliary variable context which forms part of the type definition of
-~Term~.
-
-**** Hoare Logic Assertions
-An important part of Hoare logic is the assertion language used within the
-correctness triples. The Hoare logic for MIPSL uses a first-order logic, which
-allows for the easy proof of many logical implications at the expense of not
-being complete over the full set of state properties. The full definition and
-semantics of the ~Assertion~ type are in [[*MIPSL Hoare Logic Definitions]].
-
-The ~Assertion~ type has the usual set of Boolean connectives: ~true~, ~false~,
-~_∧_~, ~_∨_~, ~¬_~ and ~_→_~. When compared to the ~fin~ MIPSL expression, which
-performs arbitrary manipulations on finite sets, using this fixed set of
-connectives may appear restrictive. The primary reason in favour of a fixed set
-of connectives is that the properties are well-defined. This makes it possible
-to prove properties about the ~Assertion~ type within proofs that would not be
-possible if assertions could use arbitrary connectives.
-
-Another constructor of ~Assertion~ is ~pred~, which accepts an arbitrary
-Boolean-valued ~Term~. This is the only way to test properties of the current
-program state within assertions. As nearly all types have equality comparisons,
-~pred~ can encode equality and inequality constraints on values. Furthermore, as
-~Term~ embeds ~Expression~, many complex computations can be performed within
-~pred~. To allow equality between two terms of any type, there is an ~equal~
-function to construct an appropriate assertion.
-
-The final two constructors of ~Assertion~ provide first-order quantification
-over auxiliary variables. ~all~ provides universal quantification and ~some~
-provides existential quantification.
-
-Semantically, an assertion is a predicate on the current state of execution. For
-MIPSL, this state is the current global, local and auxiliary variable contexts.
-As is usual in Agda, the predicates encoded as an indexed family of sets.
-
-The Boolean connectives are represented by their usual type-theoretic
-counterparts: the unit type for ~true~, the empty type for ~false~, product
-types for ~_∧_~, sum types for ~_∨_~, function types for ~_→_~ and the negation
-type for ~¬_~.
-
-Quantifier assertions are also quite easy to give a semantic representation. For
-universal quantification, you have a function taking values of the type of the
-auxiliary variable, which returns the encoding of the inner assertion with
-auxiliary context extended by this value. For existential quantification, you
-instead have a dependent pair of a value with the auxiliary variable type, and
-semantic encoding of the inner assertion.
-
-The final ~Assertion~ form to consider is ~pred~. This first evaluates the
-associated Boolean term. If true, the semantics returns the unit type.
-Otherwise, it returns the empty type. For a language where value equality can
-have many different values, some readers may feel like reducing those equalities
-to a binary result loses information. Providing this information to the user
-would require a way to convert Boolean-valued terms into a normal form,
-with an inequality operator at the root. This conversion would be highly
-non-trivial, especially due to the presence of function calls in terms.
-
-Fortunately, all equalities and inequalities between MIPSL values are decidable,
-either by construction of the type for Booleans and finite sets, or by
-specification for integers and real numbers. This allows the user to extract
-Agda terms for equalities given only knowledge of whether terms are equal.
-
-**** Correctness Triples for MIPSL
-In the traditional presentation of Hoare logic ([[*Hoare Logic]]), there are two
-types of rule; structural rules based on program syntax and adaptation rules to
-modify preconditions and postconditions. The Hoare logic for MIPSL unifies the
-two forms of rules, eliminating the need to choose which type of rule to use
-next. This allows for purely syntax-directed proofs for any choice of
-precondition and postcondition.
-
-#+name: MIPSL-correctness-triples
-#+caption: The Hoare logic correctness triples for MIPSL. This combines the
-#+caption: structural and adaptation rules you would find in traditional
-#+caption: renderings of Hoare logic into a single set of structural rules.
-#+begin_src agda2
-data HoareTriple (P : Assertion Σ Γ Δ) (Q : Assertion Σ Γ Δ) :
-                 Statement Σ Γ → Set (ℓsuc ℓ) where
-  seq     : ∀ R → HoareTriple P R s → HoareTriple R Q s₁ → HoareTriple P Q (s ∙ s₁)
-  skip    : P ⊆ Q → HoareTriple P Q skip
-  assign  : P ⊆ subst Q ref (↓ val) → HoareTriple P Q (ref ≔ val)
-  declare : HoareTriple
-              (Var.weaken 0F P ∧ equal (var 0F) (Term.Var.weaken 0F (↓ e)))
-              (Var.weaken 0F Q)
-              s →
-            HoareTriple P Q (declare e s)
-  invoke  : let metas = All.map (Term.Meta.inject Δ) (All.tabulate meta) in
-            let varsToMetas = λ P → Var.elimAll (Meta.weakenAll [] Γ P) metas in
-            let termVarsToMetas =
-              λ t → Term.Var.elimAll (Term.Meta.weakenAll [] Γ t) metas in
-            HoareTriple
-              ( varsToMetas P
-              ∧ equal (↓ tup (All.tabulate var)) (termVarsToMetas (↓ tup es))
-              )
-              (varsToMetas Q)
-              s →
-            HoareTriple P Q (invoke (s ∙end) es)
-  if      : HoareTriple (P ∧ pred (↓ e)) Q s →
-            P ∧ pred (↓ inv e) ⊆ Q →
-            HoareTriple P Q (if e then s)
-  if-else : HoareTriple (P ∧ pred (↓ e)) Q s →
-            HoareTriple (P ∧ pred (↓ inv e)) Q s₁ →
-            HoareTriple P Q (if e then s else s₁)
-  for     : (I : Assertion _ _ (fin _ ∷ _)) →
-            P ⊆ Meta.elim 0F I (↓ lit 0F) →
-            HoareTriple {Δ = _ ∷ Δ}
-              ( Var.weaken 0F
-                  (Meta.elim 1F (Meta.weaken 0F I)
-                                (fin inject₁ (cons (meta 0F) nil)))
-              ∧ equal (meta 0F) (var 0F)
-              )
-              (Var.weaken 0F
-                 (Meta.elim 1F (Meta.weaken 0F I)
-                               (fin suc (cons (meta 0F) nil))))
-              s →
-            Meta.elim 0F I (↓ lit (fromℕ m)) ⊆ Q →
-            HoareTriple P Q (for m s)
-#+end_src
+\\makeatother
+\\newpage
 
-We will now talk through each of the Hoare logic rules for MIPSL, which are
-given in [[MIPSL-correctness-triples]]. The simplest rule to consider is ~skip~.
-This immediately demonstrates how MIPSL Hoare logic combines structural and
-adaptation rules. A purely structural rule for ~skip~ would be ~HoareTriple P P
-skip~; the ~skip~ statement has no effect on the current state. By combining
-this with the rule of consequence, a ~skip~ statement allows for logical
-implication.
-
-The ~seq~ rule is as you would expect for anyone familiar with Hoare logic. The
-only potential surprise is that the intermediate assertion has to be given
-explicitly. This is due to Agda being unable to infer the assertion ~Q~ from the
-numerous manipulations applied to it by the other correctness rules.
-
-Another pair of simple rules are ~if~ and ~if-else~. In fact, the ~if-else~ rule
-is identical to the corresponding Hoare logic rule from WHILE, and ~if~ only
-differs by directly substituting in a ~skip~ statement for the negative branch.
-
-The final trivial rule is ~assign~. Like the ~skip~ rule, the ~assign~ rule
-combines the structural and adaptation rules of WHILE into a single Hoare logic
-rule for MIPSL. A purely structural rule would have ~subst Q ref (↓ val)~ as the
-precondition of the statement. MIPSL combines this with the rule of consequence
-to allow for an arbitrary precondition.
-
-The other Hoare logic rules for MIPSL are decidedly less simple. Most of the
-added complexity is a consequence of MIPSL's type safety. For example, whilst it
-is trivial to add a free variable to an assertion on paper, doing so in a
-type-safe way for the ~Assertion~ type requires constructing a whole new Agda
-term, as the variable context forms part of the type.
-
-The ~declare~ rule is the simplest of the three remaining. The goal is to
-describe a necessary triple on ~s~ such that ~HoareTriple P Q (declare e s)~ is
-a valid correctness triple. First, note that ~P~ and ~Q~ have type ~Assertion Σ
-Γ Δ~, whilst ~s~ has type ~Statement Σ (t ∷ Γ)~ due to the declaration
-introducing a new variable. To be able to use ~P~ and ~Q~, they have to be
-weakened to the type ~Assertion Σ (t ∷ Γ) Δ~, achieved by calling ~Var.weaken
-0F~. We will denote the weakened forms ~P′~ and ~Q′~ for brevity. The new triple
-we have is ~HoareTriple P′ Q′ s~. However, this does not constrain the new
-variable. Thus we assert that the new variable ~var 0F~ is equal to the initial
-value ~e~.  However, ~e~ has type ~Expression Σ Γ~ and we need a ~Term Σ (t ∷ Γ)
-Δ~. Hence we must instead use ~Term.Var.weaken 0F (↓ e)~, denoted ~e′~ , which
-converts ~e~ to a term and introduces the new variable. This finally gives us
-the triple we need: ~HoareTriple (P′ ∧ equal (var 0F) e′) Q′ s~.
-
-I will go into less detail whilst discussing ~invoke~ and ~for~, due to an even
-greater level of complexity. The ~for~ rule is the simpler case, so I will start
-there. The form of the ~for~ rule was inspired from the WHILE rule for a ~while~
-loop, but specialised to a form with a fixed number of iterations.
-
-Given a ~for n s~ statement, we first choose a loop invariant ~I : Assertion Σ Γ
-(fin (suc n) ∷ Δ)~. The additional auxiliary variable indicates the number of
-complete iterations of the loop, from \(0\) to \(n\). We will use ~I(x)~ to
-denote the assertion ~I~ with the additional auxiliary variable replaced with
-term ~x~, and make weakening variable contexts implicit. We require that ~P ⊆
-I(0)~ and ~I(n) ⊆ Q~ to ensure that the precondition and postcondition are an
-adaptation of the loop invariant. The final part to consider is the correctness
-triple for ~s~. We add in a new auxiliary variable representing the value of the
-loop variable. This is necessary to ensure the current iteration number is
-preserved between the precondition and postcondition, as the loop variable
-itself can be modified by ~s~. We then require that the following triple holds:
-~HoareTriple (I(meta 0F) ∧ equal (meta 0F) (var 0F)) I(1+ meta 0F) s~. This
-ensures that ~I~ remains true across the loop iteration, for each possible value
-of the loop variable.
-
-Notice that unlike the denotational semantics, which would explicitly execute
-each iteration of a loop, the Hoare logic instead requires only a single proof
-term for all iterations of the loop. This is one of the primary benefits of
-using Hoare logic over the denotational semantics; it has a much lower
-computational cost.
-
-The final Hoare logic rule for MIPSL is ~invoke~. Procedure invocation is tricky
-in MIPSL's Hoare logic due to the changing local variable scope in the procedure
-body. Of particular note, any local variables in the precondition and
-postcondition for a procedure invocation cannot be accessed nor modified by the
-procedure body. This is the inspiration for the form of the ~invoke~ rule.
-
-To construct ~HoareTriple P Q (invoke (s ∙end) es)~, we first consider the form
-~P~ and ~Q~ will take in a correctness triple for ~s~. Note that local variables
-in ~P~ and ~Q~ are immutable within ~s~, due to the changing local variable
-scope. Also note that the local variables cannot be accessed using ~var~; ~P~
-and ~Q~ have type ~Assertion Σ Γ Δ~, but ~s~ has type ~Statement Σ Γ′~ for some
-context ~Γ′~ independent of ~Γ~. As the original local variables are immutable
-during the invocation, we can replace them with auxiliary variables, by
-assigning a new auxiliary variable for each one. Within ~P~ and ~Q~, we then
-replace all ~var x~ with ~meta x~ to reflect that the local variables have been
-moved to auxiliary variables. This is the action performed by the ~varsToMetas~
-function. Finally, we have to ensure that the local variables within the
-procedure body are initially set to the invocation arguments. Like ~P~ and ~Q~,
-the local variables in ~es~ have to be replaced with the corresponding auxiliary
-variables. This substitution is done by ~termVarsToMetas~.
-
-Example uses of these rules, particularly ~invoke~ and ~for~, are given in
-(FIXME: forward reference).
-
-* Using MIPSL in Proofs
-We have now fully defined MIPSL, a programming language that imitates the
-Armv8-M pseudocode specification language. Whilst the specification of a new
-language is interesting by itself, the purpose of MIPSL was to enable the formal
-verification of algorithms written for the Armv8-M instruction set.
-
-This chapter demonstrates the suitability of MIPSL for this purpose by first
-using MIPSL to encode the behaviour of vector-based Barrett reduction, as
-specified by (FIXME: textcite). Then we will instantiate MIPSL with a concrete
-model for its ~int~ and ~real~ types and explore how MIPSL is used to verify a
-number of concrete examples, giving evidence for the correctness of MIPSL's
-semantics. This will be followed up by a discussion on how to abstract away
-details of this proof to show the Barrett reduction algorithm is correct on any
-set of inputs. The chapter will conclude with a proof sketch for the correctness
-of the MIPSL Hoare logic rules compared to the denotational semantics, showing
-they are a useful tool.
-
-** Vector Barrett Reduction in MIPSL
-Barrett reduction is a useful subroutine in the NTT algorithm. Briefly, it takes
-an integer and finds a "small" representable modulo some fixed base. Using the
-M-profile vector extension for the Armv8.1-M instruction set, the algorithm can
-be applied to a vector of four 32-bit values using only two instructions, given
-in [[barrett-asm]].
-
-#+name: barrett-asm
-#+caption: Assembly instructions for Barrett reduction of a vector of values
-#+caption: using the M-profile vector extension (FIXME: cite).
-#+begin_src asm
-; Logical inputs:
-; - n : modulo base
-; Register inputs:
-; - -n : general register with value -n
-; - m  : general register with value ⌊ 2^32 / n ⌉
-; - z  : input vector register
-; - t  : output vector register
-VQRDMULH.s32 t z m
-VMLA.s32     z t -n
+%%TC:endignore
+")
 #+end_src
 
-(FIXME: how much detail is needed? The word limit exists)
-
-** Concrete Examples of Semantics
-
-
-* Conclusions
-** Future Work
-
-#+print_bibliography:
-
-\appendix
-
-
-
-#+latex: %TC:ignore
-* MIPSL Syntax Definition
-#+begin_src agda2
-data Expression     (Σ : Vec Type o) (Γ : Vec Type n) : Type → Set
-data Reference      (Σ : Vec Type o) (Γ : Vec Type n) : Type → Set
-data LocalReference (Σ : Vec Type o) (Γ : Vec Type n) : Type → Set
-data Statement      (Σ : Vec Type o) (Γ : Vec Type n) : Set
-data LocalStatement (Σ : Vec Type o) (Γ : Vec Type n) : Set
-data Function       (Σ : Vec Type o) (Γ : Vec Type n) (ret : Type) : Set
-data Procedure      (Σ : Vec Type o) (Γ : Vec Type n) : Set
-
-data Expression Σ Γ where
-  lit           : literalType t → Expression Σ Γ t
-
-  state         : ∀ i → Expression Σ Γ (lookup Σ i)
-
-  var           : ∀ i → Expression Σ Γ (lookup Γ i)
+#+begin_export latex
 
-  _≟_           : ⦃ HasEquality t ⦄ →
-                  Expression Σ Γ t →
-                  Expression Σ Γ t →
-                  Expression Σ Γ bool
+%TC:ignore
 
-  _<?_          : ⦃ Ordered t ⦄ →
-                  Expression Σ Γ t →
-                  Expression Σ Γ t →
-                  Expression Σ Γ bool
+\begin{sffamily}
 
-  inv           : Expression Σ Γ bool → Expression Σ Γ bool
+Total page count: \pageref{lastpage}
 
-  _&&_          : Expression Σ Γ bool →
-                  Expression Σ Γ bool →
-                  Expression Σ Γ bool
+% 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
 
-  _||_          : Expression Σ Γ bool →
-                  Expression Σ Γ bool →
-                  Expression Σ Γ bool
+Main chapters (excluding front-matter, references and appendix):
+\contentpages~pages
+(pp~\pageref{firstcontentpage}--\pageref{lastcontentpage})
 
-  not           : Expression Σ Γ (bits n) → Expression Σ Γ (bits n)
+#+end_export
 
-  _and_         : Expression Σ Γ (bits n) →
-                  Expression Σ Γ (bits n) →
-                  Expression Σ Γ (bits n)
+#+name: wordcount
+#+begin_src elisp :exports none :eval export
+(if (not (boundp squid-eval))
+    (setq squid-eval nil))
 
-  _or_          : Expression Σ Γ (bits n) →
-                  Expression Σ Γ (bits n) →
-                  Expression Σ Γ (bits n)
+(if (not squid-eval)
+    (progn
+      (setq squid-eval t)
+      (org-latex-export-to-latex)
+      (setq squid-eval nil)))
 
-  [_]           : Expression Σ Γ t → Expression Σ Γ (array t 1)
-
-  unbox         : Expression Σ Γ (array t 1) → Expression Σ Γ t
-
-  merge         : Expression Σ Γ (array t m) →
-                  Expression Σ Γ (array t n) →
-                  Expression Σ Γ (fin (suc n)) →
-                  Expression Σ Γ (array t (n ℕ.+ m))
-
-  slice         : Expression Σ Γ (array t (n ℕ.+ m)) →
-                  Expression Σ Γ (fin (suc n)) →
-                  Expression Σ Γ (array t m)
-
-  cut           : Expression Σ Γ (array t (n ℕ.+ m)) →
-                  Expression Σ Γ (fin (suc n)) →
-                  Expression Σ Γ (array t n)
-
-  cast          : .(eq : m ≡ n) →
-                  Expression Σ Γ (array t m) →
-                  Expression Σ Γ (array t n)
-
-  -_            : ⦃ IsNumeric t ⦄ → Expression Σ Γ t → Expression Σ Γ t
-
-  _+_           : ⦃ isNum₁ : IsNumeric t₁ ⦄ →
-                  ⦃ isNum₂ : IsNumeric t₂ ⦄ →
-                  Expression Σ Γ t₁ →
-                  Expression Σ Γ t₂ →
-                  Expression Σ Γ (isNum₁ +ᵗ isNum₂)
-
-  _*_           : ⦃ isNum₁ : IsNumeric t₁ ⦄ →
-                  ⦃ isNum₂ : IsNumeric t₂ ⦄ →
-                  Expression Σ Γ t₁ →
-                  Expression Σ Γ t₂ →
-                  Expression Σ Γ (isNum₁ +ᵗ isNum₂)
-
-  _^_           : ⦃ IsNumeric t ⦄ →
-                  Expression Σ Γ t →
-                  (n : ℕ) →
-                  Expression Σ Γ t
-
-  _>>_          : Expression Σ Γ int →
-                  (n : ℕ) →
-                  Expression Σ Γ int
-
-  rnd           : Expression Σ Γ real → Expression Σ Γ int
-
-  fin           : ∀ {ms} →
-                  (f : literalTypes (map fin ms) → Fin n) →
-                  Expression Σ Γ (tuple {n = k} (map fin ms)) →
-                  Expression Σ Γ (fin n)
-
-  asInt         : Expression Σ Γ (fin n) → Expression Σ Γ int
-
-  nil           : Expression Σ Γ (tuple [])
-
-  cons          : Expression Σ Γ t →
-                  Expression Σ Γ (tuple ts) →
-                  Expression Σ Γ (tuple (t ∷ ts))
+(let* ((outfile (org-export-output-file-name ".tex")))
+  (shell-command-to-string (concat "texcount -0 -sum \'" outfile "\'")))
+#+end_src
 
-  head          : Expression Σ Γ (tuple (t ∷ ts)) → Expression Σ Γ t
+Main chapters word count: call_wordcount()
 
-  tail          : Expression Σ Γ (tuple (t ∷ ts)) → Expression Σ Γ (tuple ts)
+#+begin_export latex
+Methodology used to generate that word count:
 
-  call          : (f : Function Σ Δ t) →
-                  All (Expression Σ Γ) Δ →
-                  Expression Σ Γ t
+\begin{quote}
+\begin{verbatim}
+$ texcount -0 -sum report.tex
+xyz
+\end{verbatim}
+\end{quote}
 
-  if_then_else_ : Expression Σ Γ bool →
-                  Expression Σ Γ t →
-                  Expression Σ Γ t →
-                  Expression Σ Γ t
+\end{sffamily}
 
+\onehalfspacing
+#+end_export
 
-data Reference Σ Γ where
-  state : ∀ i → Reference Σ Γ (lookup Σ i)
+* Abstract
+:PROPERTIES:
+:unnumbered: t
+:END:
 
-  var   : ∀ i → Reference Σ Γ (lookup Γ i)
+#+latex: \ifsubmission\else
 
-  [_]   : Reference Σ Γ t → Reference Σ Γ (array t 1)
+* Acknowledgements
+:PROPERTIES:
+:unnumbered: t
+:END:
 
-  unbox : Reference Σ Γ (array t 1) → Reference Σ Γ t
+#+latex: \fi
+#+latex: \cleardoublepage
 
-  merge : Reference Σ Γ (array t m) →
-          Reference Σ Γ (array t n) →
-          Expression Σ Γ (fin (suc n)) →
-          Reference Σ Γ (array t (n ℕ.+ m))
+#+toc: headlines 4
+# #+toc: listings
+# #+toc: tables
 
-  slice : Reference Σ Γ (array t (n ℕ.+ m)) →
-          Expression Σ Γ (fin (suc n)) →
-          Reference Σ Γ (array t m)
+#+latex: %TC:endignore
 
-  cut   : Reference Σ Γ (array t (n ℕ.+ m)) →
-          Expression Σ Γ (fin (suc n)) →
-          Reference Σ Γ (array t n)
+* Introduction
 
-  cast  : .(eq : m ≡ n) →
-          Reference Σ Γ (array t m) →
-          Reference Σ Γ (array t n)
+#+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.
 
-  nil   : Reference Σ Γ (tuple [])
+* Background
 
-  cons  : Reference Σ Γ t →
-          Reference Σ Γ (tuple ts) →
-          Reference Σ Γ (tuple (t ∷ ts))
+# 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.
 
-  head  : Reference Σ Γ (tuple (t ∷ ts)) → Reference Σ Γ t
+# 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.
 
-  tail  : Reference Σ Γ (tuple (t ∷ ts)) → Reference Σ Γ (tuple ts)
+** Arm Pseudocode
+** Hoare Logic
+** Agda
 
+* Related Work
 
-data LocalReference Σ Γ where
-  var   : ∀ i → LocalReference Σ Γ (lookup Γ i)
+# 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}
 
-  [_]   : LocalReference Σ Γ t → LocalReference Σ Γ (array t 1)
+# Ideally you can tackle both together by providing a critique of
+# related work, and describing what is insufficient (and how you do
+# better!)
 
-  unbox : LocalReference Σ Γ (array t 1) → LocalReference Σ Γ t
+# 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.
 
-  merge : LocalReference Σ Γ (array t m) →
-          LocalReference Σ Γ (array t n) →
-          Expression Σ Γ (fin (suc n)) →
-          LocalReference Σ Γ (array t (n ℕ.+ m))
+* Design of AMPSL and its Semantics
 
-  slice : LocalReference Σ Γ (array t (n ℕ.+ m)) →
-          Expression Σ Γ (fin (suc n)) →
-          LocalReference Σ Γ (array t m)
+# 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.
 
-  cut   : LocalReference Σ Γ (array t (n ℕ.+ m)) →
-          Expression Σ Γ (fin (suc n)) →
-          LocalReference Σ Γ (array t n)
+** AMPSL Syntax
 
-  cast  : .(eq : m ≡ n) →
-          LocalReference Σ Γ (array t m) →
-          LocalReference Σ Γ (array t n)
+** AMPSL Semantics
 
-  nil   : LocalReference Σ Γ (tuple [])
+* Properties and Evaluation of AMPSL
 
-  cons  : LocalReference Σ Γ t →
-          LocalReference Σ Γ (tuple ts) →
-          LocalReference Σ Γ (tuple (t ∷ ts))
+# 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.
 
-  head  : LocalReference Σ Γ (tuple (t ∷ ts)) → LocalReference Σ Γ t
+** Soundness of AMPSL's Hoare Logic
 
-  tail  : LocalReference Σ Γ (tuple (t ∷ ts)) → LocalReference Σ Γ (tuple ts)
+** Using AMPSL for Proofs
 
+* Proof of Barrett Reduction
 
-data Statement Σ Γ where
-  _∙_           : Statement Σ Γ → Statement Σ Γ → Statement Σ Γ
-  skip          : Statement Σ Γ
-  _≔_           : Reference Σ Γ t → Expression Σ Γ t → Statement Σ Γ
-  declare       : Expression Σ Γ t → Statement Σ (t ∷ Γ) → Statement Σ Γ
-  invoke        : (f : Procedure Σ Δ) → All (Expression Σ Γ) Δ → Statement Σ Γ
-  for           : ∀ n → Statement Σ (fin n ∷ Γ) → Statement Σ Γ
-  if_then_      : Expression Σ Γ bool → Statement Σ Γ → Statement Σ Γ
-  if_then_else_ : Expression Σ Γ bool → Statement Σ Γ → Statement Σ Γ → Statement Σ Γ
+# 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
 
-data LocalStatement Σ Γ where
-  _∙_           : LocalStatement Σ Γ → LocalStatement Σ Γ → LocalStatement Σ Γ
-  skip          : LocalStatement Σ Γ
-  _≔_           : LocalReference Σ Γ t → Expression Σ Γ t → LocalStatement Σ Γ
-  declare       : Expression Σ Γ t → LocalStatement Σ (t ∷ Γ) → LocalStatement Σ Γ
-  for           : ∀ n → LocalStatement Σ (fin n ∷ Γ) → LocalStatement Σ Γ
-  if_then_      : Expression Σ Γ bool → LocalStatement Σ Γ → LocalStatement Σ Γ
-  if_then_else_ : Expression Σ Γ bool →
-                  LocalStatement Σ Γ →
-                  LocalStatement Σ Γ →
-                  LocalStatement Σ Γ
+# 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.
 
-data Function Σ Γ ret where
-  init_∙_end : Expression Σ Γ ret →
-               LocalStatement Σ (ret ∷ Γ) →
-               Function Σ Γ ret
+#+latex: \label{lastcontentpage}
 
-data Procedure Σ Γ where
-  _∙end : Statement Σ Γ → Procedure Σ Γ
-#+end_src
+#+latex: %TC:ignore
 
-* MIPSL Denotational Semantics
-#+begin_src agda2
-expr      : Expression Σ Γ t        → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ t ⟧ₜ
-exprs     : All (Expression Σ Γ) ts → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ ts ⟧ₜₛ
-ref       : Reference Σ Γ t         → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ t ⟧ₜ
-locRef    : LocalReference Σ Γ t    → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ t ⟧ₜ
-stmt      : Statement Σ Γ           → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ
-locStmt   : LocalStatement Σ Γ      → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Γ ⟧ₜₛ
-fun       : Function Σ Γ t          → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ t ⟧ₜ
-proc      : Procedure Σ Γ           → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Σ ⟧ₜₛ
-
-assign    : Reference Σ Γ t      → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ →
-            ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ
-locAssign : LocalReference Σ Γ t → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ →
-            ⟦ Γ ⟧ₜₛ → ⟦ Γ ⟧ₜₛ
-
-expr (lit {t = t} x)        = const (Κ[ t ] x)
-expr {Σ = Σ} (state i)      = fetch i Σ ∘ proj₁
-expr {Γ = Γ} (var i)        = fetch i Γ ∘ proj₂
-expr (e ≟ e₁)               = lift ∘ does ∘ uncurry ≈-dec ∘ < expr e , expr e₁ >
-expr (e <? e₁)              = lift ∘ does ∘ uncurry <-dec ∘ < expr e , expr e₁ >
-expr (inv e)                = lift ∘ Bool.not ∘ lower ∘ expr e
-expr (e && e₁)              = lift ∘ uncurry (Bool._∧_ on lower) ∘
-                                < expr e , expr e₁ >
-expr (e || e₁)              = lift ∘ uncurry (Bool._∨_ on lower) ∘
-                                < expr e , expr e₁ >
-expr (not e)                = map (lift ∘ Bool.not ∘ lower) ∘ expr e
-expr (e and e₁)             = uncurry (zipWith (lift ∘₂ Bool._∧_ on lower)) ∘
-                                < expr e , expr e₁ >
-expr (e or e₁)              = uncurry (zipWith (lift ∘₂ Bool._∨_ on lower)) ∘
-                                < expr e , expr e₁ >
-expr [ e ]                  = (_∷ []) ∘ expr e
-expr (unbox e)              = Vec.head ∘ expr e
-expr (merge e e₁ e₂)        = uncurry (uncurry mergeVec) ∘
-                                < < expr e , expr e₁ > , lower ∘ expr e₂ >
-expr (slice e e₁)           = uncurry sliceVec ∘ < expr e , lower ∘ expr e₁ >
-expr (cut e e₁)             = uncurry cutVec ∘ < expr e , lower ∘ expr e₁ >
-expr (cast eq e)            = castVec eq ∘ expr e
-expr (- e)                  = neg ∘ expr e
-expr (e + e₁)               = uncurry add ∘ < expr e , expr e₁ >
-expr (e * e₁)               = uncurry mul ∘ < expr e , expr e₁ >
-expr (e ^ x)                = flip pow x ∘ expr e
-expr (e >> n)               = lift ∘ flip shift n ∘ lower ∘ expr e
-expr (rnd e)                = lift ∘ ⌊_⌋ ∘ lower ∘ expr e
-expr (fin {ms = ms} f e)    = lift ∘ f ∘ lowerFin ms ∘ expr e
-expr (asInt e)              = lift ∘ 𝕀⇒ℤ ∘ 𝕀.+_ ∘ Fin.toℕ ∘ lower ∘ expr e
-expr nil                    = const _
-expr (cons {ts = ts} e e₁)  = uncurry (cons′ ts) ∘ < expr e , expr e₁ >
-expr (head {ts = ts} e)     = head′ ts ∘ expr e
-expr (tail {ts = ts} e)     = tail′ ts ∘ expr e
-expr (call f es)            = fun f ∘ < proj₁ , exprs es >
-expr (if e then e₁ else e₂) = uncurry (uncurry Bool.if_then_else_) ∘
-                                < < lower ∘ expr e , expr e₁ > , expr e₂ >
-
-exprs []            = const _
-exprs (e ∷ [])      = expr e
-exprs (e ∷ e₁ ∷ es) = < expr e , exprs (e₁ ∷ es) >
-
-ref {Σ = Σ} (state i)     = fetch i Σ ∘ proj₁
-ref {Γ = Γ} (var i)       = fetch i Γ ∘ proj₂
-ref [ r ]                 = (_∷ []) ∘ ref r
-ref (unbox r)             = Vec.head ∘ ref r
-ref (merge r r₁ e)        = uncurry (uncurry mergeVec) ∘
-                              < < ref r , ref r₁ > , lower ∘ expr e >
-ref (slice r e)           = uncurry sliceVec ∘ < ref r , lower ∘ expr e >
-ref (cut r e)             = uncurry cutVec ∘ < ref r , lower ∘ expr e >
-ref (cast eq r)           = castVec eq ∘ ref r
-ref nil                   = const _
-ref (cons {ts = ts} r r₁) = uncurry (cons′ ts) ∘ < ref r , ref r₁ >
-ref (head {ts = ts} r)    = head′ ts ∘ ref r
-ref (tail {ts = ts} r)    = tail′ ts ∘ ref r
-
-locRef {Γ = Γ} (var i)       = fetch i Γ ∘ proj₂
-locRef [ r ]                 = (_∷ []) ∘ locRef r
-locRef (unbox r)             = Vec.head ∘ locRef r
-locRef (merge r r₁ e)        = uncurry (uncurry mergeVec) ∘
-                                 < < locRef r , locRef r₁ > , lower ∘ expr e >
-locRef (slice r e)           = uncurry sliceVec ∘ < locRef r , lower ∘ expr e >
-locRef (cut r e)             = uncurry cutVec ∘ < locRef r , lower ∘ expr e >
-locRef (cast eq r)           = castVec eq ∘ locRef r
-locRef nil                   = const _
-locRef (cons {ts = ts} r r₁) = uncurry (cons′ ts) ∘ < locRef r , locRef r₁ >
-locRef (head {ts = ts} r)    = head′ ts ∘ locRef r
-locRef (tail {ts = ts} r)    = tail′ ts ∘ locRef r
-
-assign {Σ = Σ} (state i)     val σ,γ = < updateAt i Σ val ∘ proj₁ , proj₂ >
-assign {Γ = Γ} (var i)       val σ,γ = < proj₁ , updateAt i Γ val ∘ proj₂ >
-assign [ r ]                 val σ,γ = assign r (Vec.head val) σ,γ
-assign (unbox r)             val σ,γ = assign r (val ∷ []) σ,γ
-assign (merge r r₁ e)        val σ,γ = let i = expr e σ,γ in
-                                       assign r₁ (cutVec val (lower i)) σ,γ ∘
-                                       assign r (sliceVec val (lower i)) σ,γ
-assign (slice r e)           val σ,γ = let i = expr e σ,γ in
-                                       let cut = cutVec (ref r σ,γ) (lower i) in
-                                       assign r (mergeVec val cut (lower i)) σ,γ
-assign (cut r e)             val σ,γ = let i = expr e σ,γ in
-                                       let slice = sliceVec (ref r σ,γ) (lower i) in
-                                       assign r (mergeVec slice val (lower i)) σ,γ
-assign (cast eq r)           val σ,γ = assign r (castVec (sym eq) val) σ,γ
-assign nil                   val σ,γ = id
-assign (cons {ts = ts} r r₁) val σ,γ = assign r₁ (tail′ ts val) σ,γ ∘
-                                         assign r (head′ ts val) σ,γ
-assign (head {ts = ts} r)    val σ,γ = assign r (cons′ ts val (ref (tail r) σ,γ)) σ,γ
-assign (tail {ts = ts} r)    val σ,γ = assign r (cons′ ts (ref (head r) σ,γ) val) σ,γ
-
-locAssign {Γ = Γ} (var i)       val σ,γ = updateAt i Γ val
-locAssign [ r ]                 val σ,γ = locAssign r (Vec.head val) σ,γ
-locAssign (unbox r)             val σ,γ = locAssign r (val ∷ []) σ,γ
-locAssign (merge r r₁ e)        val σ,γ = let i = expr e σ,γ in
-                                          locAssign r₁ (cutVec val (lower i)) σ,γ ∘
-                                          locAssign r (sliceVec val (lower i)) σ,γ
-locAssign (slice r e)           val σ,γ = let i = expr e σ,γ in
-                                          let cut = cutVec (ref r σ,γ) (lower i) in
-                                          locAssign r (mergeVec val cut (lower i)) σ,γ
-locAssign (cut r e)             val σ,γ = let i = expr e σ,γ in
-                                          let slice = sliceVec (ref r σ,γ) (lower i) in
-                                          locAssign r (mergeVec slice val (lower i)) σ,γ
-locAssign (cast eq r)           val σ,γ = locAssign r (castVec (sym eq) val) σ,γ
-locAssign nil                   val σ,γ = id
-locAssign (cons {ts = ts} r r₁) val σ,γ = locAssign r₁ (tail′ ts val) σ,γ ∘
-                                            locAssign r (head′ ts val) σ,γ
-locAssign (head {ts = ts} r)    val σ,γ = locAssign r (cons′ ts val (locRef (tail r) σ,γ)) σ,γ
-locAssign (tail {ts = ts} r)    val σ,γ = locAssign r (cons′ ts (locRef (head r) σ,γ) val) σ,γ
-
-stmt (s ∙ s₁)              = stmt s₁ ∘ stmt s
-stmt skip                  = id
-stmt (ref ≔ val)           = uncurry (uncurry (assign ref)) ∘
-                               < < expr val , id > , id >
-stmt {Γ = Γ} (declare e s) = < proj₁ , tail′ Γ ∘ proj₂ > ∘
-                               stmt s ∘
-                               < proj₁ , uncurry (cons′ Γ) ∘ < expr e , proj₂ > >
-stmt (invoke p es)         = < proc p ∘ < proj₁ , exprs es > , proj₂ >
-stmt (if e then s)         = uncurry (uncurry Bool.if_then_else_) ∘
-                               < < lower ∘ expr e , stmt s > , id >
-stmt (if e then s else s₁) = uncurry (uncurry Bool.if_then_else_) ∘
-                               < < lower ∘ expr e , stmt s > , stmt s₁ >
-stmt {Γ = Γ} (for m s)     = Vec.foldl _
-                               (flip λ i → (
-                                 < proj₁ , tail′ Γ ∘ proj₂ > ∘
-                                 stmt s ∘
-                                 < proj₁ , cons′ Γ (lift i) ∘ proj₂ >) ∘_)
-                               id
-                               (Vec.allFin m)
-
-locStmt (s ∙ s₁)              = locStmt s₁ ∘ < proj₁ , locStmt s >
-locStmt skip                  = proj₂
-locStmt (ref ≔ val)           = uncurry (uncurry (locAssign ref)) ∘
-                                  < < expr val , id > , proj₂ >
-locStmt {Γ = Γ} (declare e s) = tail′ Γ ∘
-                                  locStmt s ∘
-                                  < proj₁ , uncurry (cons′ Γ) ∘ < expr e , proj₂ > >
-locStmt (if e then s)         = uncurry (uncurry Bool.if_then_else_) ∘
-                                  < < lower ∘ expr e , locStmt s > , proj₂ >
-locStmt (if e then s else s₁) = uncurry (uncurry Bool.if_then_else_) ∘
-                                  < < lower ∘ expr e , locStmt s > , locStmt s₁ >
-locStmt {Γ = Γ} (for m s)     = proj₂ ∘ Vec.foldl _
-                                  (flip λ i → (
-                                    < proj₁ , tail′ Γ ∘ locStmt s > ∘
-                                    < proj₁ , cons′ Γ (lift i) ∘ proj₂ >) ∘_)
-                                  id
-                                  (Vec.allFin m)
-
-fun {Γ = Γ} (init e ∙ s end) = fetch zero (_ ∷ Γ) ∘
-                                 locStmt s ∘
-                                 < proj₁ , uncurry (cons′ Γ) ∘ < expr e , proj₂ > >
-
-proc (s ∙end) = proj₁ ∘ stmt s
-#+end_src
+#+print_bibliography:
 
-#  LocalWords:  Hoare ISAs Jasmin CompCert structs bitstring bitstrings getters MIPSL
+\appendix
 
+#+latex: \label{lastpage}
 #+latex: %TC:endignore
-
-* MIPSL Hoare Logic Definitions
-First, the definition and semantics of ~Term~.
-#+begin_src agda2
-data Term (Σ : Vec Type i) (Γ : Vec Type j) (Δ : Vec Type k) : Type → Set ℓ where
-  lit           : ⟦ t ⟧ₜ → Term Σ Γ Δ t
-
-  state         : ∀ i → Term Σ Γ Δ (lookup Σ i)
-
-  var           : ∀ i → Term Σ Γ Δ (lookup Γ i)
-
-  meta          : ∀ i → Term Σ Γ Δ (lookup Δ i)
-
-  _≟_           : ⦃ HasEquality t ⦄ →
-                  Term Σ Γ Δ t →
-                  Term Σ Γ Δ t →
-                  Term Σ Γ Δ bool
-
-  _<?_          : ⦃ Ordered t ⦄ →
-                  Term Σ Γ Δ t →
-                  Term Σ Γ Δ t →
-                  Term Σ Γ Δ bool
-
-  inv           : Term Σ Γ Δ bool → Term Σ Γ Δ bool
-
-  _&&_          : Term Σ Γ Δ bool → Term Σ Γ Δ bool → Term Σ Γ Δ bool
-
-  _||_          : Term Σ Γ Δ bool → Term Σ Γ Δ bool → Term Σ Γ Δ bool
-
-  not           : Term Σ Γ Δ (bits n) → Term Σ Γ Δ (bits n)
-
-  _and_         : Term Σ Γ Δ (bits n) →
-                  Term Σ Γ Δ (bits n) →
-                  Term Σ Γ Δ (bits n)
-
-  _or_          : Term Σ Γ Δ (bits n) →
-                  Term Σ Γ Δ (bits n) →
-                  Term Σ Γ Δ (bits n)
-
-  [_]           : Term Σ Γ Δ t → Term Σ Γ Δ (array t 1)
-
-  unbox         : Term Σ Γ Δ (array t 1) → Term Σ Γ Δ t
-
-  merge         : Term Σ Γ Δ (array t m) →
-                  Term Σ Γ Δ (array t n) →
-                  Term Σ Γ Δ (fin (suc n)) →
-                  Term Σ Γ Δ (array t (n ℕ.+ m))
-
-  slice         : Term Σ Γ Δ (array t (n ℕ.+ m)) →
-                  Term Σ Γ Δ (fin (suc n)) →
-                  Term Σ Γ Δ (array t m)
-
-  cut           : Term Σ Γ Δ (array t (n ℕ.+ m)) →
-                  Term Σ Γ Δ (fin (suc n)) →
-                  Term Σ Γ Δ (array t n)
-
-  cast          : .(eq : m ≡ n) →
-                  Term Σ Γ Δ (array t m) →
-                  Term Σ Γ Δ (array t n)
-
-  -_            : ⦃ IsNumeric t ⦄ → Term Σ Γ Δ t → Term Σ Γ Δ t
-
-  _+_           : ⦃ isNum₁ : IsNumeric t₁ ⦄ →
-                  ⦃ isNum₂ : IsNumeric t₂ ⦄ →
-                  Term Σ Γ Δ t₁ →
-                  Term Σ Γ Δ t₂ →
-                  Term Σ Γ Δ (isNum₁ +ᵗ isNum₂)
-
-  _*_           : ⦃ isNum₁ : IsNumeric t₁ ⦄ →
-                  ⦃ isNum₂ : IsNumeric t₂ ⦄ →
-                  Term Σ Γ Δ t₁ →
-                  Term Σ Γ Δ t₂ →
-                  Term Σ Γ Δ (isNum₁ +ᵗ isNum₂)
-
-  _^_           : ⦃ IsNumeric t ⦄ → Term Σ Γ Δ t → ℕ → Term Σ Γ Δ t
-
-  _>>_          : Term Σ Γ Δ int → (n : ℕ) → Term Σ Γ Δ int
-
-  rnd           : Term Σ Γ Δ real → Term Σ Γ Δ int
-
-  fin           : ∀ {ms} →
-                  (f : literalTypes (map fin ms) → Fin n) →
-                  Term Σ Γ Δ (tuple {n = o} (map fin ms)) →
-                  Term Σ Γ Δ (fin n)
-
-  asInt         : Term Σ Γ Δ (fin n) → Term Σ Γ Δ int
-
-  nil           : Term Σ Γ Δ (tuple [])
-
-  cons          : Term Σ Γ Δ t →
-                  Term Σ Γ Δ (tuple ts) →
-                  Term Σ Γ Δ (tuple (t ∷ ts))
-
-  head          : Term Σ Γ Δ (tuple (t ∷ ts)) → Term Σ Γ Δ t
-
-  tail          : Term Σ Γ Δ (tuple (t ∷ ts)) → Term Σ Γ Δ (tuple ts)
-
-  call          : Function ts ts₁ t →
-                  All (Term Σ Γ Δ) ts →
-                  All (Term Σ Γ Δ) ts₁ →
-                  Term Σ Γ Δ t
-
-  if_then_else_ : Term Σ Γ Δ bool →
-                  Term Σ Γ Δ t →
-                  Term Σ Γ Δ t →
-                  Term Σ Γ Δ t
-
-⟦_⟧  : Term Σ Γ Δ t → ⟦ Σ ⟧ₜₛ → ⟦ Γ ⟧ₜₛ → ⟦ Δ ⟧ₜₛ → ⟦ t ⟧ₜ
-⟦_⟧ₛ : All (Term Σ Γ Δ) ts → ⟦ Σ ⟧ₜₛ → ⟦ Γ ⟧ₜₛ → ⟦ Δ ⟧ₜₛ → ⟦ ts ⟧ₜₛ
-
-⟦ lit x ⟧                σ γ δ = x
-⟦ state i ⟧              σ γ δ = fetch i Σ σ
-⟦ var i ⟧                σ γ δ = fetch i Γ γ
-⟦ meta i ⟧               σ γ δ = fetch i Δ δ
-⟦ e ≟ e₁ ⟧               σ γ δ = (lift ∘₂ does ∘₂ ≈-dec)
-                                   (⟦ e ⟧ σ γ δ)
-                                   (⟦ e₁ ⟧ σ γ δ)
-⟦ e <? e₁ ⟧              σ γ δ = (lift ∘₂ does ∘₂ <-dec)
-                                   (⟦ e ⟧ σ γ δ)
-                                   (⟦ e₁ ⟧ σ γ δ)
-⟦ inv e ⟧                σ γ δ = lift ∘ Bool.not ∘ lower $ ⟦ e ⟧ σ γ δ
-⟦ e && e₁ ⟧              σ γ δ = (lift ∘₂ Bool._∧_ on lower)
-                                   (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
-⟦ e || e₁ ⟧              σ γ δ = (lift ∘₂ Bool._∨_ on lower)
-                                   (⟦ e ⟧ σ γ δ)
-                                   (⟦ e₁ ⟧ σ γ δ)
-⟦ not e ⟧                σ γ δ = map (lift ∘ Bool.not ∘ lower) (⟦ e ⟧ σ γ δ)
-⟦ e and e₁ ⟧             σ γ δ = zipWith (lift ∘₂ Bool._∧_ on lower)
-                                  (⟦ e ⟧ σ γ δ)
-                                  (⟦ e₁ ⟧ σ γ δ)
-⟦ e or e₁ ⟧              σ γ δ = zipWith (lift ∘₂ Bool._∨_ on lower)
-                                  (⟦ e ⟧ σ γ δ)
-                                  (⟦ e₁ ⟧ σ γ δ)
-⟦ [ e ] ⟧                σ γ δ = ⟦ e ⟧ σ γ δ ∷ []
-⟦ unbox e ⟧              σ γ δ = Vec.head (⟦ e ⟧ σ γ δ)
-⟦ merge e e₁ e₂ ⟧        σ γ δ = mergeVec
-                                  (⟦ e ⟧ σ γ δ)
-                                  (⟦ e₁ ⟧ σ γ δ)
-                                  (lower (⟦ e₂ ⟧ σ γ δ))
-⟦ slice e e₁ ⟧           σ γ δ = sliceVec
-                                  (⟦ e ⟧ σ γ δ)
-                                  (lower (⟦ e₁ ⟧ σ γ δ))
-⟦ cut e e₁ ⟧             σ γ δ = cutVec
-                                  (⟦ e ⟧ σ γ δ)
-                                  (lower (⟦ e₁ ⟧ σ γ δ))
-⟦ cast eq e ⟧            σ γ δ = castVec eq (⟦ e ⟧ σ γ δ)
-⟦ - e ⟧                  σ γ δ = neg (⟦ e ⟧ σ γ δ)
-⟦ e + e₁ ⟧               σ γ δ = add (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
-⟦ e * e₁ ⟧               σ γ δ = mul (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
-⟦ e ^ x ⟧                σ γ δ = pow (⟦ e ⟧ σ γ δ) x
-⟦ e >> n ⟧               σ γ δ = lift ∘ flip shift n ∘ lower $ ⟦ e ⟧ σ γ δ
-⟦ rnd e ⟧                σ γ δ = lift ∘ ⌊_⌋ ∘ lower $ ⟦ e ⟧ σ γ δ
-⟦ fin {ms = ms} f e ⟧    σ γ δ = lift ∘ f ∘ lowerFin ms $ ⟦ e ⟧ σ γ δ
-⟦ asInt e ⟧              σ γ δ = lift ∘ 𝕀⇒ℤ ∘ 𝕀.+_ ∘ Fin.toℕ ∘ lower $ ⟦ e ⟧ σ γ δ
-⟦ nil ⟧                  σ γ δ = _
-⟦ cons {ts = ts} e e₁ ⟧  σ γ δ = cons′ ts (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
-⟦ head {ts = ts} e ⟧     σ γ δ = head′ ts (⟦ e ⟧ σ γ δ)
-⟦ tail {ts = ts} e ⟧     σ γ δ = tail′ ts (⟦ e ⟧ σ γ δ)
-⟦ call f es es₁ ⟧        σ γ δ = Den.Semantics.fun f
-                                  (⟦ es ⟧ₛ σ γ δ , ⟦ es₁ ⟧ₛ σ γ δ)
-⟦ if e then e₁ else e₂ ⟧ σ γ δ = Bool.if lower (⟦ e ⟧ σ γ δ)
-                                 then ⟦ e₁ ⟧ σ γ δ
-                                 else ⟦ e₂ ⟧ σ γ δ
-
-⟦_⟧ₛ               []            σ γ δ = _
-⟦_⟧ₛ {ts = _ ∷ ts} (e ∷ es)      σ γ δ = cons′ ts (⟦ e ⟧ σ γ δ) (⟦ es ⟧ₛ σ γ δ)
-#+end_src
-
-And here is the definition of ~Assertion~ with its semantics.
-
-#+begin_src agda2
-data Assertion (Σ : Vec Type o) (Γ : Vec Type n) (Δ : Vec Type m)
-               : Set (ℓsuc ℓ) where
-  all    : Assertion Σ Γ (t ∷ Δ) → Assertion Σ Γ Δ
-  some   : Assertion Σ Γ (t ∷ Δ) → Assertion Σ Γ Δ
-  pred   : Term Σ Γ Δ bool → Assertion Σ Γ Δ
-  true   : Assertion Σ Γ Δ
-  false  : Assertion Σ Γ Δ
-  ¬_     : Assertion Σ Γ Δ → Assertion Σ Γ Δ
-  _∧_    : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ
-  _∨_    : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ
-  _⟶_    : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ
-
-⟦_⟧ : Assertion Σ Γ Δ → ⟦ Σ ⟧ₜₛ → ⟦ Γ ⟧ₜₛ → ⟦ Δ ⟧ₜₛ → Set ℓ
-⟦_⟧ {Δ = Δ} (all P)  σ γ δ = ∀ x → ⟦ P ⟧ σ γ (cons′ Δ x δ)
-⟦_⟧ {Δ = Δ} (some P) σ γ δ = ∃ λ x → ⟦ P ⟧ σ γ (cons′ Δ x δ)
-⟦ pred p ⟧           σ γ δ = Lift ℓ (Bool.T (lower (TS.⟦ p ⟧ σ γ δ)))
-⟦ true ⟧             σ γ δ = Lift ℓ ⊤
-⟦ false ⟧            σ γ δ = Lift ℓ ⊥
-⟦ ¬ P ⟧              σ γ δ = ⟦ P ⟧ σ γ δ → ⊥
-⟦ P ∧ Q ⟧            σ γ δ = ⟦ P ⟧ σ γ δ × ⟦ Q ⟧ σ γ δ
-⟦ P ∨ Q ⟧            σ γ δ = ⟦ P ⟧ σ γ δ ⊎ ⟦ Q ⟧ σ γ δ
-⟦ P ⟶ Q ⟧            σ γ δ = ⟦ P ⟧ σ γ δ → ⟦ Q ⟧ σ γ δ
-#+end_src