#+options: ':t *:t -:t ::t <:t H:4 \n:nil ^:t arch:headline author:t #+options: broken-links:nil c:nil creator:nil d:(not "LOGBOOK") date:t e:t #+options: email:nil f:t inline:t num:t p:nil pri:nil prop:nil stat:t tags:t #+options: tasks:t tex:t timestamp:t title:t toc:nil todo:t |:t #+title: Semantics of an embedded vector architecture for formal verification of software #+date: May 2022 #+author: Greg Brown #+latex_header: \newcommand{\candidatenumber}{2487C} #+latex_header: \newcommand{\college}{Queens' College} #+latex_header: \newcommand{\course}{Computer Science Tripos, Part III} #+email: greg.brown@cl.cam.ac.uk #+language: en-GB #+select_tags: export #+exclude_tags: noexport #+creator: Emacs 27.2 (Org mode 9.6) #+cite_export: biblatex #+bibliography: ./thesis.bib #+latex_class: thesis #+latex_class_options: [12pt,a4paper,twoside] #+latex_header: \usepackage[hyperref=true,url=true,backend=biber,natbib=true]{biblatex} % citations #+latex_header: \usepackage[vmargin=20mm,hmargin=25mm]{geometry} % page margins #+latex_header: \usepackage{minted} % code snippets #+latex_header: \usepackage{parskip} % vertical space for paragraphs #+latex_header: \usepackage{setspace} % line spacing #+latex_header: \usepackage{newunicodechar} % unicode in code snippets #+latex_header: \usepackage{ebproof} % Hoare logic rules #+latex_header: \usepackage{mathtools} % a math character? #+latex_header: \usepackage{stmaryrd} % some math characters #+latex_header: \usepackage{refcount} % for counting pages #+latex_header: \usepackage{upquote} % for correct quotation marks in verbatim text #+latex_compiler: pdflatex #+latex_header: \newunicodechar{ʳ}{\ensuremath{^\texttt{r}}} #+latex_header: \newunicodechar{ˡ}{\ensuremath{^\texttt{l}}} #+latex_header: \newunicodechar{Γ}{\ensuremath{\Gamma}} #+latex_header: \newunicodechar{Δ}{\ensuremath{\Delta}} #+latex_header: \newunicodechar{Κ}{\ensuremath{K}} #+latex_header: \newunicodechar{Σ}{\ensuremath{\Sigma}} #+latex_header: \newunicodechar{γ}{\ensuremath{\gamma}} #+latex_header: \newunicodechar{δ}{\ensuremath{\delta}} #+latex_header: \newunicodechar{ε}{\ensuremath{\epsilon}} #+latex_header: \newunicodechar{λ}{\ensuremath{\lambda}} #+latex_header: \newunicodechar{σ}{\ensuremath{\sigma}} #+latex_header: \newunicodechar{ᵗ}{\ensuremath{^\texttt{t}}} #+latex_header: \newunicodechar{′}{\ensuremath{'}} #+latex_header: \newunicodechar{₁}{\ensuremath{_1}} #+latex_header: \newunicodechar{₂}{\ensuremath{_2}} #+latex_header: \newunicodechar{ₛ}{\ensuremath{_\texttt{s}}} #+latex_header: \newunicodechar{ₜ}{\ensuremath{_\texttt{t}}} #+latex_header: \newunicodechar{ℓ}{l} #+latex_header: \newunicodechar{ℕ}{\ensuremath{\mathbb{N}}} #+latex_header: \newunicodechar{ℚ}{\ensuremath{\mathbb{Q}}} #+latex_header: \newunicodechar{ℝ}{\ensuremath{\mathbb{R}}} #+latex_header: \newunicodechar{ℤ}{\ensuremath{\mathbb{Z}}} #+latex_header: \newunicodechar{⇒}{\ensuremath{\rightarrow}} #+latex_header: \newunicodechar{∀}{\ensuremath{\forall}} #+latex_header: \newunicodechar{∃}{\ensuremath{\exists}} #+latex_header: \newunicodechar{∘}{\ensuremath{\circ}} #+latex_header: \newunicodechar{∙}{\ensuremath{\cdot}} #+latex_header: \newunicodechar{∧}{\ensuremath{\wedge}} #+latex_header: \newunicodechar{∨}{\ensuremath{\vee}} #+latex_header: \newunicodechar{∷}{\texttt{::}} #+latex_header: \newunicodechar{≈}{\ensuremath{\approx}} #+latex_header: \newunicodechar{≉}{\ensuremath{\not\approx}} #+latex_header: \newunicodechar{≔}{\ensuremath{\coloneqq}} #+latex_header: \newunicodechar{≟}{\ensuremath{\buildrel ?\over =}} #+latex_header: \newunicodechar{≡}{\ensuremath{\equiv}} #+latex_header: \newunicodechar{≢}{\ensuremath{\not\equiv}} #+latex_header: \newunicodechar{⊆}{\ensuremath{\subseteq}} #+latex_header: \newunicodechar{⊎}{\ensuremath{\uplus}} #+latex_header: \newunicodechar{⊔}{\ensuremath{\sqcup}} #+latex_header: \newunicodechar{⊤}{\ensuremath{\top}} #+latex_header: \newunicodechar{⊥}{\ensuremath{\bot}} #+latex_header: \newunicodechar{⌊}{\ensuremath{\lfloor}} #+latex_header: \newunicodechar{⌋}{\ensuremath{\rfloor}} #+latex_header: \newunicodechar{⟦}{\ensuremath{\llbracket}} #+latex_header: \newunicodechar{⟧}{\ensuremath{\rrbracket}} #+latex_header: \newunicodechar{⟶}{\ensuremath{\rightarrow}} #+latex_header: \newunicodechar{⦃}{\{\{} #+latex_header: \newunicodechar{⦄}{\}\}} #+latex_header: \newunicodechar{𝕀}{\ensuremath{\mathbb{I}}} #+latex_header: \newtheorem{theorem}{Theorem} #+latex_header: %TC:envir minted 1 ignore #+latex_header: \newif\ifsubmission # Uncomment when anonymous # #+latex_header: \submissiontrue #+begin_src elisp :exports results :results none :eval export (make-variable-buffer-local 'org-latex-title-command) (setq org-latex-title-command " %%TC:ignore \\begin{sffamily} \\begin{titlepage} \\makeatletter \\hspace*{-14mm}\\includegraphics[width=65mm]{logo-dcst-colour} \\ifsubmission %% submission proforma cover page for blind marking \\begin{Large} \\vspace{20mm} Research project report title page \\vspace{35mm} Candidate \\candidatenumber \\vspace{42mm} \\textsl{\`\`\\@title\'\'} \\end{Large} \\else %% regular cover page \\begin{center} \\Huge \\vspace{\\fill} \\@title \\vspace{\\fill} \\@author \\vspace{10mm} \\Large \\college \\vspace{\\fill} \\@date \\vspace{\\fill} \\end{center} \\fi \\vspace{\\fill} \\begin{center} Submitted in partial fulfillment of the requirements for the\\\\ \\course \\end{center} \\end{titlepage} \\end{sffamily} \\makeatother \\newpage %%TC:endignore ") #+end_src #+begin_export latex %TC:ignore \begin{sffamily} Total page count: \pageref{lastpage} % calculate number of pages from % \label{firstcontentpage} to \label{lastcontentpage} inclusive \makeatletter \@tempcnta=\getpagerefnumber{lastcontentpage}\relax% \advance\@tempcnta by -\getpagerefnumber{firstcontentpage}% \advance\@tempcnta by 1% \xdef\contentpages{\the\@tempcnta}% \makeatother Main chapters (excluding front-matter, references and appendix): \contentpages~pages (pp~\pageref{firstcontentpage}--\pageref{lastcontentpage}) #+end_export #+name: wordcount #+begin_src elisp :exports none :eval export (if (not (boundp 'squid-eval)) (setq squid-eval nil)) (if (not squid-eval) (progn (setq squid-eval t) (org-latex-export-to-latex) (setq squid-eval nil))) (let* ((outfile (org-export-output-file-name ".tex"))) (shell-command-to-string (concat "texcount -0 -sum \'" outfile "\'"))) #+end_src Main chapters word count: call_wordcount() #+begin_export latex Methodology used to generate that word count: \begin{quote} \begin{verbatim} $ texcount -0 -sum report.tex xyz \end{verbatim} \end{quote} \end{sffamily} \onehalfspacing #+end_export * Abstract :PROPERTIES: :unnumbered: t :END: #+latex: \ifsubmission\else * Acknowledgements :PROPERTIES: :unnumbered: t :END: #+latex: \fi #+latex: \cleardoublepage #+toc: headlines 2 # #+toc: listings # #+toc: tables #+latex: %TC:endignore * Introduction #+latex: \label{firstcontentpage} The ultimate goal of this work was to formally verify an implementation [cite:@10.46586/tches.v2022.i1.482-505] of the number-theoretic transform (NTT) for the Armv8.1-M architecture. The NTT is a vital procedure for lattice-based post-quantum cryptography (FIXME: cite). To ensure internet-connected embedded devices remain secure in the future of large-scale quantum computers, implementations of these algorithms, and hence the NTT, are required for the architectures they use. One common architecture used by embedded devices is Armv8-M (FIXME: cite). Due to the resource-constrained nature of an embedded device, and the huge computational demands of post-quantum cryptography, algorithms like the NTT are presented using hand-written, highly-optimised assembly code. To ensure the correctness of these cryptographic algorithms, and thus the security of embedded devices, formal verification of these algorithms is necessary. This report focuses on formalising the semantics of the Armv8-M architecture. [cite/t:@arm/DDI0553B.s] provides a pseudocode description of the operation of Armv8-M instructions using the Arm pseudocode (henceforth \ldquo{}the pseudocode\rdquo{}). Unfortunately this language is primarily designed for describing instructions (FIXME: cite) and not proving properties of executing them. To remedy this, I designed AMPSL, which mocks the pseudocode specification language. AMPSL is written in the dependently-typed Agda proof assistant [cite:@10.1007/978-3-642-03359-9_6]. The syntax mirrors that of the pseudocode, save some minor modifications due to limitations within Agda and adjustments to simplify the semantics. Using Agda enables AMPSL, its semantics, and proofs using and about the semantics to be written using a single language. AMPSL is given semantics in two different forms. The first is a denotational semantics, which converts the various program elements into functions within Agda. This enables the explicit computation of the effect of AMPSL on the processor state. AMPSL also has a set of Hoare logic rules, which form an axiomatic, syntax-directed approach to describing how a statement in AMPSL modifies assertions on the processor state. Another significant line of work undertaken by this report is the formal verification of Barrett reduction. Barrett reduction is an important subroutine used by the NTT, to efficiently find a \ldquo{}small\rdquo{} representable of a value modulo some base [cite:@10.1007/3-540-47721-7_24]. Much like how a formalisation of the NTT is a big step in formalising the behaviour of many PQC algorithms, formalising Barrett reduction is a big step in formalising the NTT. The main contributions of this report are as follows: - In [[*AMPSL Syntax]], I introduce the syntax of the AMPSL programming language. The primary goal of the syntax is to facilitate easy translation of programs from the Arm pseudocode, detailed in [[*Arm Pseudocode]] into AMPSL, whilst allowing AMPSL semantics to remain simple. - The semantics of AMPSL are described in [[*AMPSL Semantics]]. The primary achievement of this work is the simple semantics of AMPSL, which facilitates straight-forward proofs about various AMPSL programs. I detail both a denotational semantics and a Hoare logic for AMPSL. The Hoare logic used by AMPSL somewhat varies from the traditional presentation, given in [[*Hoare Logic]], to enforce that Hoare logic proofs have bounded depth with respect to the program syntax. - In [[*Soundness of AMPSL's Hoare Logic]], I prove that the Hoare logic rules for AMPSL are sound with respect to the denotational semantics. This proof is possible due to Agda's foundation of Martin-Löf's type theory, the significance of which is given in [[*Agda]]. Due to the soundness of AMPSL's Hoare logic, the behaviour of the computationally-intensive denotational semantics can instead be specified using syntax-directed Hoare logic. - A number of example proofs for AMPSL programs are given in [[*Using AMPSL for Proofs]]. This demonstrates the viability of using AMPSL for the formal verification of a number of programs, and lays the groundwork for the formal verification of the NTT given by [cite/t:@10.46586/tches.v2022.i1.482-505]. - Finally, a formal proof of a Barrett reduction variant is given in [[*Proof of Barrett Reduction]]. (FIXME: As far as I can tell) giving this well-used algorithm a formal machine proof is a novel endeavour. Further, it is the first proof of Barrett reduction on a domain other than integers and rationals. # This is the introduction where you should introduce your work. In # general the thing to aim for here is to describe a little bit of the # context for your work -- why did you do it (motivation), what was the # hoped-for outcome (aims) -- as well as trying to give a brief overview # of what you actually did. # It's often useful to bring forward some ``highlights'' into this # chapter (e.g.\ some particularly compelling results, or a particularly # interesting finding). # It's also traditional to give an outline of the rest of the document, # although without care this can appear formulaic and tedious. Your # call. * Background # A more extensive coverage of what's required to understand your work. # In general you should assume the reader has a good undergraduate # degree in computer science, but is not necessarily an expert in the # particular area you have been working on. Hence this chapter may need to # summarize some ``text book'' material. # This is not something you'd normally require in an academic paper, and # it may not be appropriate for your particular circumstances. Indeed, # in some cases it's possible to cover all of the ``background'' # material either in the introduction or at appropriate places in the # rest of the dissertation. ** Arm Pseudocode The Armv8.1-M pseudocode specification language is a strongly-typed imperative programming language [cite:@arm/DDI0553B.s §E1.2.1]. It has a first-order type system, a small set of operators and basic control flow, as you would find in most imperative languages. Its primary purpose is to explain how executing an Armv8-M instruction modifies the visible processor state. As it is a descriptive aid, the pseudocode features a number of design choices atypical of other imperative programming languages making execution difficult. Something common to nearly all imperative languages is the presence of a primitive type for Booleans. Other typical type constructors are tuples, structs, enumerations and fixed-length arrays. The first interesting type used by the pseudocode is mathematical integers as a primitive type. Most imperative languages use fixed-width integers for primitive types, with exact integers available through some library. Examples include Rust (FIXME: cite), C (FIXME: cite), Java (FIXME: cite) and Go (FIXME: cite). This is because the performance benefits of using fixed-width integers in code far outweigh the risk of overflow. As checking for integer overflow complicates algorithms, and the pseudocode is not designed to execute, the pseudocode can make use of exact mathematical integers to eliminate overflow errors without any of the drawbacks [cite:@arm/DDI0553B.s §E1.3.4]. Another odd type present in the pseudocode is mathematical real numbers. As most real numbers are impossible to record using finite storage, any executable programming language must make compromises to the precision of real numbers. This is usually achieved through floating-point numbers, which represent only a negligible fraction of possible real number values. However, as the pseudocode is not executable, the types it use do not need to have a finite representation. Thus it is free to use real numbers and have exact precision in real-number arithmetic [cite:@arm/DDI0553B.s §E1.2.4]. The final primitive type used by the pseudocode is the bitstring; a fixed-length sequence of 0s and 1s. Some readers may wonder what the difference is between this type and arrays of Booleans. The justification given by [cite/t:@arm/DDI0553B.s §E1.2.2] is more philosophical than practical: \ldquo{}bitstrings are the only concrete data type in pseudocode\rdquo{}. In some places, bitstrings can be used instead of integers in arithmetic operations, by first converting them to an unsigned integer. Most of the operators used by the pseudocode are unsurprising. For instance, Booleans have the standard set of short-circuiting operations; integers and reals have addition, subtraction and multiplication; reals have division; integers have integer division (division rounding to \(-\infty\)) and modulus (the remainder of division); and concatenation of bitstrings. The most interesting operation in the pseudocode is bitstring slicing. First, there is no type for a bit outside a bitstring---a single bit is represented as a bitstring of length one---so bitstring slicing always returns a bitstring. Slicing then works in much the same way as array slicing in languages like Python (FIXME: cite?) and Rust (FIXME: cite?); slicing an integer range from a bitstring returns a new bitstring with values corresponding to the indexed bits. The other special feature of bitstring slicing is that an integer can be sliced instead of a bitstring. In that case, the pseudocode \ldquo{}treats an integer as equivalent to a sufficiently long [\ldots] bitstring\rdquo{} [cite:@arm/DDI0553B.s §E1.3.3]. The final interesting difference between the pseudocode and most imperative languages is the variety of top-level items. The pseudocode has three forms of items: procedures, functions and array-like functions. Procedures and functions behave like procedures and functions of other imperative languages. The arguments to them are passed by value, and the only difference between the two is that procedures do not return values whilst functions do [cite:@arm/DDI0553B.s §E1.4.2]. Array-like functions act as getters and setters for machine state. Every array-like function has a reader form, and most have a writer form. This distinction exists because \ldquo{}reading from and writing to an array element require different functions\rdquo{}, [cite:@arm/DDI0553B.s §E1.4.2], likely due to the nature of some machine registers being read-only instead of read-writeable. The writer form acts as one of the targets of assignment expressions, along with variables and the result of bitstring concatenation and slicing [cite:@arm/DDI0553B.s §E1.3.5]. (FIXME: examples) ** Hoare Logic Hoare logic is a proof system for programs written in imperative programming languages. At its core, the logic describes how to build partial correctness triples, which describe how program statements affect assertions about machine state. The bulk of a Hoare logic derivation is dependent only on the syntax of the program the proof targets. A partial correctness triple is a relation between a precondition \(P\), a program statement \(s\) and a postcondition \(Q\). If \(\{P\} s \{Q\}\) is a partial correctness triple, then whenever \(P\) holds for some machine state, then when executing \(s\), \(Q\) holds for the state after it terminates [cite:@10.1145/363235.363259]. This is a /partial/ correctness triple because the postcondition only holds if \(s\) terminates. When all statements terminate, this relation is called a correctness triple. #+name: WHILE-Hoare-logic #+caption: Hoare logic rules for the WHILE language, consisting of assignment, #+caption: if statements and while loops. The top three lines show the structural #+caption: rules, and the bottom shows the adaptation rule. #+begin_figure \begin{center} \begin{prooftree} \infer0[SKIP]{\{P\}\;\texttt{s}\;\{P\}} \infer[rule style=no rule,rule margin=3ex]1{\{P\}\;\texttt{s₁}\;\{Q\}\qquad\{Q\}\;\texttt{s₂}\;\{R\}} \infer1[SEQ]{\{P\}\;\texttt{s₁;s₂}\;\{Q\}} \infer0[ASSIGN]{\{P[\texttt{x}/\texttt{v}]\}\;\texttt{x:=v}\;\{P\}} \infer[rule style=no rule,rule margin=3ex]1{\{P \wedge \texttt{e}\}\;\texttt{s₁}\;\{Q\}\qquad\{P \wedge \neg \texttt{e}\}\;\texttt{s₂}\;\{Q\}} \infer1[IF]{\{P\}\;\texttt{if e then s₁ else s₂}\;\{Q\}} \infer[rule style=no rule,rule margin=3ex]2{\{P \wedge \texttt{e}\}\;\texttt{s}\;\{P\}} \infer1[WHILE]{\{P\}\;\texttt{while e do s}\;\{P \wedge \neg \texttt{e}\}} \infer[rule style=no rule,rule margin=3ex]1{\models P_1 \rightarrow P_2\qquad\{P_2\}\;\texttt{s}\;\{Q_2\}\qquad\models Q_2 \rightarrow Q_1} \infer1[CSQ]{\{P_1\}\;\texttt{s}\;\{Q_1\}} \end{prooftree} \end{center} #+end_figure [[WHILE-Hoare-logic]] shows the rules Hoare introduced for the WHILE language [cite:@10.1145/363235.363259]. The SKIP and SEQ rules are straight-forward: the skip statement has no effect on state, and sequencing statements composes their effects. The IF rule is also uncomplicated. No matter which branch we take, the postcondition remains the same; an if statement does no computation after executing a branch. Which branch we take depends on the value of ~e~. Because the value of ~e~ is known before executing a branch, it is added to the preconditions in the premises. The ASSIGN rule appears backwards upon first reading; the substitution is performed in the precondition, before the assignment occurs! When considered more deeply, you realise the reason for this reversal. Due to the assignment, any occurrence of ~v~ in the precondition can be replaced by ~x~, and the original value of ~x~ is lost. Hence the postcondition can only use ~x~ exactly where there was ~v~ in the precondition. This is enforced by the substitution. The final structural Hoare logic rule for the WHILE language is the WHILE rule. This rule can be derived by observing the fixed-point nature of a while statement. As ~while e do s~ is equivalent to ~if e then (s ; while e do s) else skip~, we can use the IF, SEQ and SKIP rules to solve the recursion equation for the precondition and postcondition of the while statement. The final Hoare logic rule is the rule of consequence, CSQ. This rule does not recurse on the structure of the statement ~s~, but instead adapts the precondition and postcondition. In this case, we can weaken the precondition and postcondition using logical implication. [cite/t:@10.1145/363235.363259] does not specify the logic used to evaluate the implications in the rule of consequence. Regular choices are first-order logic and higher-order logic [cite:@10.1007/s00165-019-00501-3;@10.1007/s001650050057]. For specifying program behaviour, one vital aspect of the choice of logic is the presence of auxiliary variables [cite:@10.1007/s001650050057]. Auxiliary variables are a set of variables that cannot be used within a program, but they can be quantified over within assertions or left as free variables. A free auxiliary variable remains constant between the precondition and postcondition, and are universally-quantified within proofs. (FIXME: examples) ** Agda Agda is a dependently-typed proof assistant and functional programming language, based on Martin-Löf's type theory. The work of [cite/t:@10.1007/978-3-642-03359-9_6] provides an excellent introduction to the language. This section provides a summary of the most important features for the implementation of AMPSL. *Inductive families*. Data types like you would find in ML or Haskell can not only be indexed by types, but by specific values. This is best illustrated by an example. Take for instance fixed-length vectors. They can be defined by the following snippet: #+begin_src agda2 data Vec (A : Set) : ℕ → Set where [] : Vec A 0 _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n) #+end_src First consider the type of ~Vec~. It is a function that accepts a type ~A~ and a natural number, and returns a type. The position of ~A~ to the left of the colon is significant; it is a /parameter/ of ~Vec~ instead of an /index/. Parameters are required to be the same for all constructors, whilst indices can vary between constructors [cite:@agda.readthedocs.io p. \texttt{language/data-types.html}]. This means the following definition of ~Vec~ is invalid: #+begin_src agda2 data Vec (A : Set) (n : ℕ) : Set where [] : Vec A 0 -- 0 ≢ n -^ _\::_ : ∀ {n} → A → Vec A n → Vec A (suc n) -- and suc n ≢ n -------------------^ #+end_src Whilst the value of parameters is constant in the return values of constructors, they can vary across the arguments of constructors, even for the same type. One example of this is the ~Assertion~ type given in (FIXME: forwardref) later in the report. The ~all~ and ~some~ constructors both accept an ~Assertion Σ Γ (t ∷ Δ)~, but because they return an ~Assertion Σ Γ Δ~ the definition is valid. *Parameterised modules and records*. Agda modules can accept parameters, which can be used anywhere in the module. This works well with Agda's record types, are a generalisation of a dependent product. (In fact, the builtin Σ type is defined using a record [cite:@agda.readthedocs.io p. \texttt{language/built-ins.html}].) The following snippet shows how records can be used to define a setoid-enriched monoid: #+begin_src agda2 record Monoid ℓ₁ ℓ₂ : Set (ℓsuc (ℓ₁ ⊔ ℓ₂)) where infixl 5 _∙_ infix 4 _≈_ field Carrier : Set ℓ₁ _≈_ : Rel A ℓ₂ _∙_ : Op₂ Carrier ε : Carrier refl : ∀ {x} → x ≈ x sym : ∀ {x y} → x ≈ y → y ≈ x trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z ∙-cong : ∀ {x y u v} → x ≈ y → u ≈ v → x ∙ y ≈ u ∙ v ∙-assoc : ∀ {x y z} → (x ∙ y) ∙ z ≈ x ∙ (y ∙ z) ∙-idˡ : ∀ {x} → ε ∙ x ≈ x ∙-idʳ : ∀ {x} → x ∙ ε ≈ x #+end_src This record bundles together an underlying ~Carrier~ type with an equality relation ~_≈_~, binary operator ~_∙_~ and identity element ~ε~. It also contains all the proofs necessary to show that ~_≈_~ is really an equality and that ~_∙_~ and ~ε~ form a monoid. When a module is parameterised by a ~Monoid~, then the module has an abstract monoid. It can use the structure and laws given in the record freely, but it cannot use additional laws (e.g. commutativity) without an additional argument. This is useful when the operations and properties of a type are well-defined, but a good representation is unknown. *Instance arguments* Instance arguments are analogous to the type class constraints you find in Haskell [cite:@agda.readthedocs.io p. \texttt{language/instance-arguments.html}]. They are a special form of implicit argument that are solved via /instance resolution/ over unification. Instance arguments are a good solution for cases where Agda tries \ldquo{}too hard\rdquo{} to find a solution for implicit arguments, and needs the implicit arguments to be specified implicitly. Using instance arguments instead can force a particular solution onto Agda without needing to give the arguments explicitly. * Related Work # This chapter covers relevant (and typically, recent) research # which you build upon (or improve upon). There are two complementary # goals for this chapter: # \begin{enumerate} # \item to show that you know and understand the state of the art; and # \item to put your work in context # \end{enumerate} # Ideally you can tackle both together by providing a critique of # related work, and describing what is insufficient (and how you do # better!) # The related work chapter should usually come either near the front or # near the back of the dissertation. The advantage of the former is that # you get to build the argument for why your work is important before # presenting your solution(s) in later chapters; the advantage of the # latter is that don't have to forward reference to your solution too # much. The correct choice will depend on what you're writing up, and # your own personal preference. There exist a multitude of formal verification tools designed to describe either the semantics of ISA instructions or prove the correctness of algorithms. This section describes some of the most significant work in the field and how the design of AMPSL improves upon it. ** Sail Sail [cite:@10.1145/3290384] is a language for describing the instruction-set architecture semantics of processors. It has a syntax similar to the pseudocode specification of architectures and a first-order type system with dependent bitvector and numeric types. It is officially used by [cite/t:@riscv/spec-20191213] to specify the concurrent memory semantics of the RISC-V architecture. Sail has many different backends available, including sequential emulators, concurrency models and theorem-prover definitions. Further, there are tools to automatically translate documents from the Arm Specification Language into Sail (FIXME: cite). Despite the many advantages of Sail over other solutions, using Sail in this project is not suitable for a number of reasons. First is the poor or nonexistent documentation of the Sail theorem-proving backends. Trying to decode the output of these tools, given that the input for the RISC-V model is 1.2MiB, would be time consuming. Another reason to avoid Sail is the unnecessary complexity in modelling the ISA semantics. Sail attempts to model the full complexity of the semantics, particularly in the face of concurrent memory access. This complexity is unnecessary for the Arm M-profile architecture, as it has a single thread of execution. This makes the semantics much simpler to reason about. ** ? * Design of AMPSL and its Semantics In this chapter I introduce AMPSL, a language mocking the Arm pseudocode. AMPSL is defined within Agda, and makes judicious use of Agda's dependent-typing features to eliminate assertions and ensure programs cannot fail. To construct proofs about how AMPSL 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 AMPSL. Hoare logic derivations assign a precondition and a postcondition assertion to each statement. These are chained together though a number of simple logical implications. ** AMPSL Syntax AMPSL 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. AMPSL makes a number of small changes to the pseudocode to better facilitate this embedding, typically generalising existing features of the pseudocode. *** AMPSL Types #+name: AMPSL-types #+caption: The Agda datatype representing the types present in AMPSL. 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 [[AMPSL-types]] gives the Agda datatype representing the types of AMPSL. Most of these have a direct analogue to the pseudocode types. For example, ~bool~ is a Boolean, ~int~ mathematical integers, ~real~ is for mathematical real numbers and ~array~ constructs array types. Instead of an enumeration construct, AMPSL uses the ~fin n~ type, representing a finite set of ~n~ elements. Similarly, structs are represented by ~tuple~ types. The most significant difference between the pseudocode and AMPSL is the representation of bitstrings. Whilst the pseudocode has the ~bits~ datatype, AMPSL instead treats bitstrings as an array of Booleans. This removes the distinction between arrays and bitstrings, and allows a number of operations to be generalised to work on both types. This makes AMPSL more expressive than the pseudocode, in the sense that there are a greater number and more concise ways to write expressions that are functionally equivalent. 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. AMPSL 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 AMPSL 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 AMPSL. The final interesting feature of the types in AMPSL is implicit coercion for arithmetic. As pseudocode arithmetic is polymorphic for integers and reals, AMPSL needs a function to decide the type of the result. By describing the output type as a function on the input types, the same constructor can be used for all combinations of numeric inputs. *** AMPSL Expressions #+name: AMPSL-literalType #+caption: Mappings from AMPSL 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 Unlike the pseudocode, where only a few types have literal expressions, every type in AMPSL has a literal form. This mapping is part of the ~literalType~ function, given in [[AMPSL-literalType]]. Most AMPSL 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. This is sufficient as any real value occurring in the pseudocode in [cite:@arm/DDI0553B.s] is rational. # TODO: why is this sufficient? #+name: AMPSL-expr-prototypes #+caption: Prototypes of the numerous AMPSL 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 [[AMPSL-expr-prototypes]] lists the prototypes for the various AMPSL program elements, with the full definitions being given in [[*AMPSL Syntax Definition]]. Each of the AMPSL program element types are parameterised by two variable contexts: Σ for global variables and Γ for local variables. The two variable contexts are split to simplify the types for function calls and procedure invocations. As the set of global variables does not change across a program, functions and procedures keep the same value of parameter Σ in their types. As functions and procedures have different local variables than the calling context, having the local variable context as a separate parameter makes the change simple. An ~Expression~ in AMPSL 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, AMPSL literals are introduced by the ~lit~ constructor. The most immediate change for programming in AMPSL versus the pseudocode is how variables are handled. Because the ~Expression~ type carries fixed-length vectors listing the AMPSL 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 AMPSL as the context ~int ∷ real ∷ []~. The variable \(x\) is then represented by ~var 0F~ in AMPSL. Because the global and local variable contexts are disjoint for the ~Expression~ type, variables are constructed using ~state~ or ~var~ respectively. Whilst this decision introduces much complexity to programming using AMPSL, it greatly simplifies the language for use in constructing proofs. It is also a technique used in the internal representation of many compilers (FIXME: cite). AMPSL 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. Others are ~fin~, which allows for arbitrary computations on elements of finite sets, and ~asInt~, which converts a finite value into an integer. The final three AMPSL operators of note are ~merge~, ~slice~ and ~cut~. These all perform operations on arrays, by either merging two together, taking out a slice, or cutting out a slice. Unlike the pseudocode where bitstring slicing requires a range, these three operators use Agda's dependent types and type inference so that only a base offset is necessary. ~slice xs i~, like bitstring slicing, extracts a contiguous subset of values from an array ~xs~, such that the first element in ~slice xs i~ is in ~xs~ at position ~i~. ~cut xs i~ returns the remainder of ~slice xs i~; the two ends of ~xs~ not in the slice, concatenated. Finally, ~merge xs ys i~ joins ~xs~ and ~ys~ to form a product-projection triple. The ~Reference~ type is the name AMPSL gives to assignable expressions from the pseudocode. The ~LocalReference~ type is identical to ~Reference~, except it does not include global variables. Due to complications to the semantics of multiple assignments to one location, "product" operations like ~merge~ and ~cons~ are excluded from being references, despite concatenated bitstrings and tuples being assignable expressions in the pseudocode. Whilst (FIXME: textcite) requires that no position in a bitstring is referenced twice, enforcing this in AMPSL for ~merge~ and ~cons~ would make their use unergonomic in practice for writing code or proofs. (FIXME: necessary?) In an earlier form of AMPSL, 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 AMPSL programs is transparent. **** Example AMPSL Expressions One arithmetic operator used in the pseudocode is left shift. (FIXME: textcite) explains how this can be encoded using other arithmetic operators in AMPSL, as shown below: #+begin_src agda2 _<<_ : Expression Σ Γ int → (n : ℕ) → Expression Σ Γ int e << n = e * lit (ℤ.+ (2 ℕ.^ n)) #+end_src 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 AMPSL types with Agda integers for literal values: ~int~ and ~real~. How does Agda correctly infer the type? Recall that multiplication is polymorphic in AMPSL, with the result type determined by implicit coercion. Agda knows that the multiplication must return an ~int~, and that the first argument is also an ~int~, so it can infer that the second multiplicand is an integer literal. Another pseudocode operation not yet described in AMPSL is integer slicing. 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 = inv (x - ((x >> suc i) << suc i)