path: root/thesis.org

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

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

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

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

#+latex_header: \usepackage[hyperref=true,url=true,backend=biber,natbib=true]{biblatex} % citations
#+latex_header: \usepackage[vmargin=20mm,hmargin=25mm]{geometry} % page margins
#+latex_header: \usepackage[chapter]{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_header: \usepackage{caption}        % not sure why this one [[https://www.overleaf.com/learn/latex/How_to_Write_a_Thesis_in_LaTeX_(Part_3)%3A_Figures%2C_Subfigures_and_Tables#Subfigures]]...
#+latex_header: \usepackage{subcaption}     % add subfigures

#+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{^\texttt{i}}}
#+latex_header: \newunicodechar{⁺}{\ensuremath{^{+}}}
#+latex_header: \newunicodechar{₁}{\ensuremath{_1}}
#+latex_header: \newunicodechar{₂}{\ensuremath{_2}}
#+latex_header: \newunicodechar{₃}{\ensuremath{_3}}
#+latex_header: \newunicodechar{ₚ}{\ensuremath{_\texttt{p}}}
#+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{\blacksquare}}
#+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{\le}}
#+latex_header: \newunicodechar{≥}{\ensuremath{\ge}}
#+latex_header: \newunicodechar{⊆}{\ensuremath{\subseteq}}
#+latex_header: \newunicodechar{⊎}{\ensuremath{\uplus}}
#+latex_header: \newunicodechar{⊔}{\ensuremath{\sqcup}}
#+latex_header: \newunicodechar{⊢}{\ensuremath{\vdash}}
#+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
(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

#+RESULTS: wordcount
: 11800

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
11800
\end{verbatim}
\end{quote}

\end{sffamily}

\onehalfspacing
#+end_export

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

The ultimate goal of this work is 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.

This report focuses on producing the first formalisation of the semantics of the
Armv8-M architecture and its M-profile vector extension. The pseudocode used to
describe the instructions within the manual by [cite/t:@arm/DDI0553B.s] did not
have a formal semantic description. For this project I created AMPSL, to mock
the Arm specification language, within Agda. The syntax closely follows that of
ASL, save some minor modifications due to limitations within Agda and
adjustments to simplify the semantics.

This report describes both a denotational semantics and Hoare logic for AMPSL.
The denotational semantics interprets AMPSL statements and expressions as Agda
functions on a variable context. The Hoare logic instead provides a
syntax-directed derivation of AMPSL's action on assertions about the execution
state.

I also use Agda to formally verify a variant 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]. Formalising Barrett reduction is a significant
step in formalising the NTT.

#+latex: \ifsubmission\else

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

I would like to thank Dominic Mulligan, Hanno Becker and Gustavo Petri at Arm
for the initial idea and producing valuable feedback on my project and report
throughout the year.

I would also like to thank Jeremy Yallop for supervising the project and
providing support throughout the project. They also provided useful and
actionable feedback on the various drafts of my report.

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

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

#+latex: %TC:endignore

* Introduction

#+latex: \label{firstcontentpage}

The ultimate goal of this work is 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. PQC is a type of cryptography immune to rapid attack
by large-scale quantum computers. Armv8-M is a common architecture in embedded
devices. Due to the resource-constrained nature of an embedded device, and the
PQC's huge computational demands, algorithms like the NTT are presented using
hand-written, highly-optimised assembly code. To ensure these cryptographic
algorithms are correct, and thus embedded devices are secure, formal
verification of these algorithms is necessary.

This report focuses on producing the first formalisation of the semantics of the
Armv8-M architecture, in particular its M-profile vector extension.
[cite/t:@arm/DDI0553B.s] provides a pseudocode description of the operation of
Armv8-M instructions using the Arm pseudocode (henceforth ASL). Unfortunately
this language is primarily designed for describing instructions
[cite:@arm/DDI0553B.s §E1.1.1] and not proving semantic properties.

To remedy this, I designed AMPSL (Arm M-profile Pseudocode Specification
Language, or AMPSL Mocks Pseudocode Specification Language). AMPSL is written in
Agda, a dependently-typed proof assistant [cite:@10.1007/978-3-642-03359-9_6].
The syntax mirrors that of ASL, save some minor modifications due to limitations
within Agda and adjustments to simplify the semantics.

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 explicitly computing 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.

Due to AMPSL's similarity to ASL, I can convert the ASL description of Armv8-M
instructions into AMPSL. From this I can derive the semantics of Armv8-M
instructions using AMPSL's semantics.

I also use Agda to formally verify a variant 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 an
important step in formalising the behaviour of many PQC algorithms, formalising
Barrett reduction is an important step in formalising the NTT.

#+name: raw_progress
#+begin_src dot :file progress.pdf :exports none
digraph {
    node [shape=box,width=2.5,height=0.6];
    A [label="Functional correctness\nof NTT",style=dotted];
    B [label="Functional correctness\nof Barrett reduction",style=dotted];
    C [label="NTT properties",style=dotted];
    D [label="Armv8-M Instruction\nsemantics",style=dashed];
    E [label="Barrett reduction\nproperties"];
    F [label="AMPSL semantics"];
    G [label="AMPSL properties",style=dashed];
    H [label="Model of Armv8-M\nin AMPSL"];

    H -> D;
    G -> B;
    F -> G;
    F -> D;
    E -> C [style=dashed];
    E -> B;
    D -> B;
    C -> A;
    B -> A [style=dashed];
}
#+end_src

#+name: progress
#+caption: Progress made towards formalising an implementation of NTT for the
#+caption: Armv8.1-M architecture. Work completed in this report has a solid
#+caption: outline. Items where only trivial, time-consuming work is left have a
#+caption: dashed border. Significant outstanding work has a dotted
#+caption: border.
call_raw_progress()

[[progress]] shows the progress this work has made to verifying an NTT
implementation for Armv8.1-M vector extension. Whilst it does not achieve the
final goal, it forms solid foundations towards it.

The main contributions of this report are as follows:
- In [[*AMPSL Syntax]], I introduce the syntax of the AMPSL programming language.
  Its primary goal is to facilitate easy translation of programs from ASL,
  detailed in [[*Arm Pseudocode]] into AMPSL.
- AMPSL's semantics are described in [[*AMPSL Semantics]]. AMPSL has a simple
  semantics 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 eliminate adaptation rules.
- In [[*Soundness of AMPSL's Hoare Logic]], I prove that the set of 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]]. As AMPSL's Hoare logic is sound, the
  behaviour of the computationally-intensive denotational semantics can instead
  be specified using syntax-directed Hoare logic.
- A number of proof outlines for AMPSL programs are given in [[*Using AMPSL for
  Proofs]]. This describes how AMPSL is used to give the semantics of Armv8.1-M
  instructions. It also demonstrates that AMPSL is viable for the formal
  verification of various programs, and lays the groundwork for the formally
  verifying the NTT implementation 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]]. To my knowledge this is the first such machine-verified
  correctness proof for Barrett reduction. Further, it is the first proof for a
  domain other than integers and rationals.

* Background

** Arm Pseudocode
ASL 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. Its primary purpose is to explain how executing an Armv8-M
instruction modifies the processor state. As it is a descriptive aid, ASL
features some design choices atypical for other imperative programming
languages making it difficult to execute.

Something common to ASL and nearly all imperative languages are primitive
types for Booleans, tuples, structs, enumerations and fixed-length arrays.

Two interesting primitive types used by ASL are mathematical integers and real
numbers. Other imperative languages typically use fixed-width integers and
floating point rationals as efficient approximations for these values, with the
downside of having overflow and precision loss errors. As ASL is for
specification over execution, efficiency is of no concern so using the
mathematical types prevents a whole class of errors.

The final primitive type used by ASL is the bitstring; a fixed-length sequence
of 0s and 1s. Some readers may wonder what the difference is between this type
and Boolean arrays. 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 in
arithmetic operations, by first converting them to an unsigned integer.

ASL types have all of the associated standard operations, including equality,
ordering, Boolean connectives and arithmetic.

The most interesting operation in ASL is bitstring slicing. First, there is no
type for a bit outside a bitstring, so slicing always returns a bitstring.
Slicing then works in much the same way as array slicing in languages like
Python and Rust; 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 it can also slice integers.  In that case,
ASL \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 ASL and most imperative languages is
the variety of top-level items. ASL has three item forms: procedures, functions
and array-like functions. Procedures and functions behave like procedures and
functions of other imperative languages. Their arguments 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], due to 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].

An example of ASL is given in [[*Example Armv8-M Instruction Models in AMPSL]],
alongside an AMPSL model of it.

** M-profile Vector Extension

The M-profile vector extension adds vector instructions to the Armv8-M
architecture. A vector in this case is a 128-bit register, logically split into
four 32-bit beats. Each beat is then divided into one, two or four lanes each of 32,
16 or 8 bits respectively [cite:@arm/DDI0553B.s §B5.3].

A processor can execute either one, two or four instruction beats in an
\ldquo{}architecture tick\rdquo{}, an atomic unit of processor time
[cite:@arm/DDI0553B.s §\(\texttt{I}_\texttt{PCBB}\)]. The number of beats executed per
instruction can also change throughout execution.

Processors are allowed but not required to execute two vector instructions
concurrently [cite:@arm/DDI0553B.s §B5.3]. To summarise the overlap rules, at
least the first two beats of the current instruction must be completed before
executing the next one. Then, at most the first two beats of that instruction
can be executed before the current instruction is finished.

** 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 program
syntax 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 total triple.

#+name: WHILE-Hoare-logic
#+caption: Hoare logic rules for the WHILE language.
#+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 [cite/t:@10.1145/363235.363259] introduced for
the WHILE language. There are two broad classes of Hoare logic rules. The
structural rules SKIP, SEQ, IF, ASSIGN and WHILE reflect how program syntax
affects program execution, and thus how to modify the precondition and
postcondition assertions accordingly. The adaptation rule CSQ uses the same
statement in the premise and conclusion changing only the preconditions and
postconditions used.

The SKIP and SEQ rules reflect the idea that the skip statement has no effect on
state, and sequencing statements composes their effects. The IF rule is also
uncomplicated. No matter which branch is taken, the postcondition remains the
same; an if statement does no computation after executing a branch. The branch
choice depends on the value of ~e~. Because this value is known before executing
a branch, it is added to the preconditions in the premises.

The ASSIGN rule is the most unintuitive structural rule. In the postcondition,
any use of ~x~ can be replaced by ~v~ and, due to the assignment, the assertion
maintains its truth value. In the precondition ~x~ could have any value. By
applying the substitution of ~v~ for ~x~ to the precondition, the fact that ~x~
changes value is irrelevant.

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

The only adaptation rule in WHILE's Hoare logic is the rule of consequence, CSQ.
CSQ is necessary in this Hoare logic so that the assertions can be manipulated
into forms suitable for use by each structural rule. Other forms of Hoare logic,
like the one for AMPSL given in [[*Hoare Logic Semantics]], make adaptation rules
redundant.

[cite/t:@10.1145/363235.363259] does not specify the logic used to evaluate the
implications in rule premises. Regular choices are first-order logic and
higher-order logic [cite:@10.1007/s00165-019-00501-3;@10.1007/s001650050057].
For specifying program behaviour, having auxiliary variables in the logic is
vital [cite:@10.1007/s001650050057]. Auxiliary variables are a set of variables
that cannot be used within a program, so remain constant between the
precondition and postcondition. This allows for proofs about arbitrary values
without requiring them to appear in the program.

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

*Inductive families*. Agda generalises ML-style datatypes allowing them to be
indexed by values as well as types. This is best illustrated by an example.
Fixed-length vectors can be defined by the following snippet:

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

Note the type of ~Vec~. It is a function that accepts a type (or ~Set~) ~A~ and
a natural number, and returns a type. ~A~ is a /parameter/ of ~Vec~ whilst ~n~
is 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}].

Whilst parameter values must be constant across the constructor return values,
they can vary within the constructor arguments, even for the same type. One
example of this is the ~Assertion~ type given in [[*Hoare Logic Assertions]]. The
~all~ and ~some~ constructors both accept an ~Assertion Σ Γ (t ∷ Δ)~, but
because they return an ~Assertion Σ Γ Δ~ the definition is valid.

*Propositional equality*. One very important datatype in Agda is propositional
equality, shown in the following snippet:

#+begin_src agda2
data _≡_ {A : Set} : A → A → Set where
  refl : ∀ {x} → x ≡ x
#+end_src

The only constructor, ~refl~, requires that the two values in the type are
identical. Hence whenever there is a value of type ~x ≡ y~, ~x~ and ~y~ have
the same value, even when Agda cannot compute that value. One useful
propositional-equality eliminator is in the ~subst~ function:

#+begin_src agda2
subst : (B : A → Set) → x ≡ y → B x → B y
subst _ refl Bx = Bx
#+end_src

Given a proof ~x ≡ y~ that ~x~ and ~y~ are equal, this function makes uses of
~x~ and ~y~ within types interchangeable.

*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,
whose fields are able to depend on values of other fields. The following snippet
shows how records can be used to define a monoid:

#+begin_src agda2
record Monoid ℓ : Set (ℓsuc ℓ) where
  infixl 5 _∙_
  field
    Carrier : Set ℓ
    _∙_     : Op₂ Carrier
    ε       : Carrier
    ∙-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 a binary operator
~_∙_~ and identity element ~ε~. It also contains all the proofs necessary to
show that ~_∙_~ and ~ε~ form a monoid.

Note that unlike the previous ~Vec~ example, ~Set~ has now been given a
parameter. This is to encode different universe levels within Agda. As ~Set~ is
a type within Agda, it must itself have a type. If ~Set~ was within ~Set~, Agda
would be subject to a logical inconsistency known as Girard's paradox
[cite:@cs.cmu.edu/girard-72-thesis]. Thus, ~Set~ has type ~Set 1ℓ~, and ~Set i~
has type ~Set (ℓsuc i)~.

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 a type's operations and properties are well-defined, but a
good representation is unknown.

*Instance arguments* Instance arguments are analogous to the type class
constraints found 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 explicitly. Using instance arguments instead can force
a particular solution onto Agda, reducing the volume of explicit code.

* Related Work

There exist many formal verification tools designed to describe either ISA
instruction semantics or prove algorithms correct. This section describes some
significant work in the field and how the AMPSL's design improves
upon it.

** Sail

Sail [cite:@10.1145/3290384] is a language for describing processor instruction-set
architecture semantics. It has a syntax similar to the pseudocode
specification of most 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 RISC-V concurrent memory semantics.

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
[cite:@10.1145/3290384].

Despite Sail's advantages over other solutions, including AMPSL, using Sail in
this project is not suitable for a few reasons. First is a lack of
documentation for the Sail theorem-proving backends. Without prior knowledge in
using Sail, deciphering the automatically-generated statements from Sail would
likely consume more time than creating AMPSL.

Another reason to avoid Sail is the unnecessary complexity in modelling the ISA
semantics. One of Sail's highlights is in its description of architectural
memory models. However, this work attempts to verify the functional correctness
of NTT, an algorithm with very little memory usage. Creating a simpler language
like AMPSL removes the need to reason about these complex memory interactions
and focus on the computation itself.

** Other Functional Correctness Tools
Various tools exist for proving functional correctness of programs. These
include tools that target C such as CryptoLine [cite:@10.1145/3319535.3354199],
Fiat Crypto [cite:@10.1109/SP.2019.00005], Frama-C
[cite:@10.1007/s00165-014-0326-7] and VST [cite:@10.1007/978-3-642-19718-5_1],
as well as tools that target assembly directly such as Jasmin
[cite:@10.1145/3133956.3134078] and Vale [cite:@10.1145/3290376].

There are two distinct problems with using these tools to verify
that a pre-existing NTT implementation for Armv8-M is functionally correct:
- These tools do not accept assembly as an input language. This means they are
  unable to verify an existing assembly algorithm.
- These tools do not target Armv8-M assembly as output. Jasmin and Vale, whilst
  targeting assembly, do not currently target the Armv8-M architecture, let
  alone the M-profile vector extension. The other tools target C and require
  using verified compiler, of which none currently target Armv8-M.

The most similar tool to what this project is trying to achieve is a formal
verification tool by [cite/t:@10.1145/3391900], which targets the REDFIN
instruction set. REDFIN has much less complex semantics than Armv8-M, to the
point where the semantics can be expressed directly without the need for a
specification language, making using REDFIN in proofs much easier than Armv8-M
instructions.

* Design of AMPSL and its Semantics

In this chapter I introduce AMPSL, an Agda embedding of ASL. I also describe
AMPSL's semantics via a denotational semantics that interprets AMPSL expressions
and statements as Agda functions.

One downside of AMPSL's simple 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.

** AMPSL Syntax
ASL has some small features that make it difficult to work with in Agda
directly. AMPSL makes minor changes to ASL to better facilitate this embedding,
typically generalising existing ASL features.

*** AMPSL Types

#+name: AMPSL-types
#+caption: The Agda datatype representing the primitive AMPSL types.
#+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 AMPSL types. Most of these
have a direct analogue to ASL types. Instead of an enumeration construct, AMPSL
uses the ~fin n~ type, representing a set of ~n~ elements. Similarly,
structs are represented by ~tuple~ types.

The most significant difference between ASL and AMPSL is the representation of
bitstrings. Instead of a separate bitstring type, AMPSL uses Boolean arrays.
This lets AMPSL generalise some ASL operations to other array types and makes
AMPSL more expressive.

ASL specifies three different type properties: equality comparisons, order
comparisons and arithmetic operations. Whilst using the relevant operations in
AMPSL requires a proof that the types have the required property, using instance
arguments allows for these proofs to be elided in almost all cases.

AMPSL maintains the ASL type properties with two additions. First, array types
have equality if the enumerated type also has equality. This is a natural
generalisation of equality and allows for AMPSL's formulation of bitstrings as
Boolean arrays to have equality. Second, finite sets also have ordering. This
change is primarily a convenience feature for comparing finite sets representing
an integer subset.

The final interesting type feature in AMPSL is implicit coercion for arithmetic.
As ASL arithmetic is polymorphic for integers and reals, AMPSL needs a function
to decide the result type. 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 for specifying literals.
#+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 ASL, where only a few types have literal expressions, every type in AMPSL
has a literal form. This mapping is given by the ~literalType~ function, shown
in [[AMPSL-literalType]]. Most AMPSL literals accept the corresponding Agda type as
a value. 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 literal real value in ASL is represented as a decimal; a
rational value.

#+name: AMPSL-expr-prototypes
#+caption: Agda declarations of the AMPSL program elements.
#+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

#+name: AMPSL-grammar
#+caption: AMPSL's grammar. The formal Agda definition is in the provided
#+caption: source code.
#+begin_figure
\begin{align*}
\mathrm{Natural}\;{}n = & \texttt{0} \mid \texttt{suc}\;{}n \\
\mathrm{Fin}\;{}i = & \texttt{0F} \mid \texttt{suc}\;{}i \\
\mathrm{LocalReference}\;{}R = & \texttt{var}\;{}i \mid \\
& \texttt{[}\;{}R\;{}\texttt{]} \mid \texttt{unbox}\;{}R \mid \texttt{cast eq}\;{}e \\
& \texttt{merge}\;{}R\;{}R\;{}R \mid \texttt{slice}\;{}R\;{}R \mid \texttt{cut}\;{}R\;{}R \mid \\
& \texttt{head}\;{}R \mid \texttt{tail}\;{}R \\
\mathrm{Reference}\;{}r = & \textrm{Like LocalReference} \mid \texttt{state}\;{}i\\
\mathrm{Expression}\;{}e = & \textrm{Like Reference} \mid \texttt{lit}\;{}x \mid e\;{}\texttt{≟}\;{}e \mid e\;{}\texttt{<?}\;{}e \mid \\
& \texttt{inv}\;{}e \mid e\;{}\texttt{\&\&}\;{}e \mid e\;{}\texttt{||}\;{}e \mid \texttt{not}\;{}e \mid e\;{}\texttt{and}\;{}e \mid e\;{}\texttt{or}\;{}e \mid \\
& \texttt{-}\;{}e \mid e\;{}\texttt{+}\;{}e \mid e\;{}\texttt{*}\;{}e \mid e\;{}\texttt{>>}\;{}n \mid e\;{}\texttt{\textasciicircum}\;{}n \mid \texttt{rnd}\;{}e \mid \\
& \texttt{fin}\;{}f\;{}e \mid \texttt{asInt}\;{}e \mid \\
& \texttt{nil} \mid \texttt{cons}\;{}e\;{}e \mid \\
& \texttt{call}\;{}F\;{}es \mid \texttt{if}\;{}e\;{}\texttt{then}\;{}e\;{}\texttt{else}\;{}e \\
\mathrm{LocalStatement}\;{}S = & \texttt{skip} \mid S\;{}\texttt{∙}\;{}S \mid R\;{}\texttt{≔}\;{}e \mid \\
& \texttt{declare}\;{}e\;{}S \mid \texttt{for}\;{}n\;{}S \mid \\
& \texttt{if}\;{}e\;{}\texttt{then}\;{}S \mid \texttt{if}\;{}e\;{}\texttt{then}\;{}S\;{}\texttt{else}\;{}S \\
\mathrm{Statement}\;{}s = & \textrm{Like LocalStatement} \mid \\
& r\;{}\texttt{≔}\;{}e \mid \texttt{invoke}\;{}P\;{}es \\
\mathrm{Function}\;{}F = & \texttt{init}\;{}e\;{}\texttt{∙}\;{}S\;{}\texttt{end} \\
\mathrm{Procedure}\;{}P = & s\;{}\texttt{∙end}
\end{align*}
#+end_figure

[[AMPSL-expr-prototypes]] lists the Agda data type declarations corresponding to the
AMPSL program elements. The grammar is summarised in [[AMPSL-grammar]]. Each type is
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 to expressions in ASL. Many operators are
identical to those in ASL, and others are simple renamings (like ~≟~ for
~==~ for equality comparisons). Unlike ASL, where literals can appear
unqualified, AMPSL literals are introduced by the ~lit~ constructor.

The most immediate change for programming in AMPSL versus ASL is how variables
are handled. Because the ~Expression~ type depends on the values of variable
contexts, 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, where the ~F~ indicates the index is from
a finite set. Because the global and local variable contexts are disjoint for
the ~Expression~ type, variables are constructed using ~state~ or ~var~
respectively.

Whilst this decision makes programming using AMPSL more complex, it greatly
simplifies the language for use in constructing proofs.

AMPSL expressions also add a number of useful constructs to ASL. One such pair
are ~[_]~ and ~unbox~, which construct and destruct a length-one array
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 noteworthy operators are ~merge~, ~slice~ and ~cut~. These all
perform operations on arrays, by either merging two together, taking out a
slice, or dropping a slice. Unlike ASL 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 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 with ~slice~ and ~cut~.

The ~Reference~ type is the name AMPSL gives to assignable expressions from ASL.
The ~LocalReference~ type is identical to ~Reference~, except it does not
include global variables. Due to complications in the semantics of multiple
assignments to one location, \ldquo{}product\rdquo operations like ~merge~ and
~cons~ are excluded from being references, despite concatenated bitstrings and
tuples being assignable expressions in ASL. Whilst [cite/t:@arm/DDI0553B.s
§E1.3.3] 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.

**** Example AMPSL Expressions
One arithmetic operator used in ASL is left shift. [cite/t:@arm/DDI0553B.s
§E1.3.4] 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

There is a lot of hidden complexity here. First, consider the literal
statement's type. The unary plus operation indicates the literal is an Agda
integer. However, there are two AMPSL types with Agda integers for literal
values: ~int~ and ~real~. The multiplication result must be an ~int~, and the
first argument is also an ~int~. Because multiplication's type is determined by
implicit coercion, Agda can unwind the function defining the coercion and finds
that the literal must be an ~int~.

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) <? lit (ℤ.+ (2 ℕ.^ i)))
#+end_src

This makes use of AMPSL unifying the ~bit~ and ~bool~ types. 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~, hence the whole
condition is inverted.

*** AMPSL Statements
Most statements in AMPSL are straight forward. The ~skip~ and sequencing (~_∙_~)
statements are 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.

# FIXME: why not a typedef?
Given that AMPSL has a ~skip~ statement and an ~if_then_else_~ control-flow
structure, including the ~if_then_~ statement is redundant. It is included in
AMPSL for ergonomics. ~if_then_~ statements appear many times more often in ASL
than ~if_then_else_~ statements such that omitting it would only serve to
complicate embedded code.

The form of variable declarations is significantly different in AMPSL than it is
in ASL. AMPSL variable declarations do not need a name as they are accessed by
index. Type annotations are unnecessary as Agda can often infer a declared
variable's type from the context in which it is used. All variables in AMPSL
must be initialised, simplifying the AMPSL's semantics and preventing the use
of uninitialised variables.

AMPSL makes a small modification to ~for~ loops that greatly improve the type
safety over what is achieved by ASL. Instead of looping over a range of dynamic
values [cite:@arm/DDI0553B.s §E1.4.4], AMPSL loops perform a static number of
iterations, determined by an Agda natural ~n~. Then, instead of the loop
variable being an assignable integer expression, AMPSL introduces a new variable
with type ~fin n~.

There are three ASL statement forms that AMPSL omits. These are ~while...do~
loops, ~repeat...until~ loops and ~try...catch~ exception handling. Including
these three statements would complicate AMPSL's denotational encoding, by
removing termination guarantees and requiring a monadic transformation for the
loops and exceptions, respectively.

Thankfully, these three structures are not vital in ASL, each either having a
functional alternative [cite:@arm/DDI0553B.s §E2.1.166] or forming part of
internal processor bookkeeping [cite:@arm/DDI0553B.s §E2.1.397],
[cite:@arm/DDI0553B.s §E2.1.366]. Hence their omission from AMPSL is not a
significant loss.

To encode effectless functions, AMPSL 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 AMPSL Statements
Here is a statement that copies bytes from ~x~ into the machine register ~Q[
dest , i ]~ if the corresponding entry in ~mask~ is true:

#+begin_src agda2
copyMasked :
  Statement State ( fin 8 ∷ array (bits 8) 4 ∷ array bool 4 ∷ [])
copyMasked =
  for n (
    let i    = var 0F in
    let dest = var 1F in
    let x    = var 2F in
    let mask = var 3F in

    if index mask i then
      Q[ dest , i ] ≔ index x i
  )
#+end_src

This uses the Agda function ~index~ to apply the appropriate slices, casts and
unboxing to extract a single byte from the array ~x~. Note the use of Agda's
~let...in~ construct 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 : Procedure 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 (call (LSL-C 0) (! vptState ∷ [])) (
        let vptState′,i = var 0F in
        let vptState = var 1F in
        let beat = var 3F in

        vptState ≔ head vptState′,i ∙
        if head (tail vptState′,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
#+end_src

This corresponds to the ~VPTAdvance~ procedure by [cite/t:@arm/DDI0553B.s
§E2.1.424], which is used in the AMPSL model for Barrett reduction discussed in
[[*Using AMPSL for Proofs]]. 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 AMPSL, the type-safety guarantees and simplified proofs over
using named variables more than make up the difference.

*** AMPSL Functions and Procedures
Much like how a procedure in ASL is a wrapper around a statement block,
~Procedure~ in AMPSL is a wrapper around ~Statement~. Note that AMPSL procedures
only have one exit point, the end of a statement, unlike ASL which has ~return~
statements. Any procedure using a ~return~ statement can be transformed into one
that does not by refactoring, so AMPSL does not lose any expressive power over
ASL.

AMPSL functions are more complex than procedures. A function is 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 is the final value of the return
variable after executing the statement.

**** Example AMPSL Functions and Procedures
As ~Procedure~ is almost an alias for ~Statement~, example procedures can be
found in [[*Example AMPSL 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 Σ (bits n ∷ bool ∷ []) int
Int =
  init
    if var 1F
    then call uint (var 0F ∷ [])
    else call sint (var 0F ∷ [])
    ∙ skip
  end
#+end_src

The function body is the ~skip~ statement, meaning that the result of calling
the function is whatever is initially assigned to the return variable. The
initial value here 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 next example shows the ~uint~ function, which converts a bitstring into an
unsigned integer.

#+begin_src agda2
uint : Function Σ (bits n ∷ []) int
uint {n = 0}     = init lit 0ℤ ∙ skip end
uint {n = suc n} =
  init
    lit 0ℤ ∙
    declare (lit 1ℤ) (
    for (suc m) (
      let x = var 3F in
      let ret = var 2F in
      let scale = var 1F in
      let i = var 0F in
      if index x i then (
        ret ≔ !! ret + !! scale
      ) ∙
      scale ≔ lit (ℤ.+ 2) * !! scale
    ))
  end
#+end_src

The AMSPL function has two forms, depending on the number of input bits. If the
input is a zero-length bitstring, then its integer value is zero. Otherwise, the
function iterates through the bits in turn, adding a bit's place value into the
return value whenever that bit is true.

This example highlights the similarities between functions and ~declare~
statements. A local variable is declared with some initial value. It is then
used in some further computation. The only difference is the action when leaving
scope. A declare statement would simply discard the local variable. A function
instead returns that value.

** AMPSL Semantics
This section starts with a brief discussion of how to model AMPSL types. This
addresses how to model real numbers in Agda. From this, I describe AMPSL's
denotational semantics, and how AMPSL can be converted into Agda functions. The
section ends with a Hoare logic for AMPSL, allowing for efficient
syntax-directed proofs about statements.

*** AMPSL Datatype Models
#+name: AMPSL-type-models
#+caption: The semantic encoding of AMPSL data types. I use ~Lift~ is to ensure
#+caption: 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

To be able to write a denotational semantics for a language, the first step is
to find a suitable encoding for the data types. [[AMPSL-type-models]] shows the full
encoding function for AMPSL.

Tuples are encoded as an n-ary product. This is computed by the ~⟦_⟧ₜₛ~
function in [[AMPSL-type-models]]. The Agda type checker would not accept using a
library-provided n-ary product in this case due to termination checking, hence
the manual inductive definition.

The other two AMPSL types are ~int~ and ~real~. Whilst ~int~ could feasibly be
encoded by the Agda integer type, there is no useful Agda encoding for
mathematical real numbers. Hence 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 ℝ. There must also be 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
\]

~/1~ represents the usual embedding of integers into real numbers. ~⌊_⌋~
represents the floor function. Because ~/1~ is a monomorphism, we have
\(\mathtt{⌊ x /1 ⌋} = \mathtt{x}\) for all \(\mathtt{x} \in ℤ\).

*** Denotational Semantics

#+name: AMPSL-denotational-prototypes
#+caption: Function prototypes for AMPSL's denotational semantics. All program
#+caption: elements become functions from the current variable context into some
#+caption: 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

Due to careful design of AMPSL's syntax, each of its program elements is
denotationally represented by a total Agda function.
[[AMPSL-denotational-prototypes]] shows the prototypes of the different semantic
interpretation functions, and the full definitions are in the provided source
code. Each function accepts the current variable context as an argument.
Because the variable contexts are an ordered sequence of values, 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. Two 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 themselves being a lookup into
the current type context. Despite both being contained within the ~Expression~
type, ~Reference~ and ~LocalReference~ require their own functions to satisfy
the Agda termination checker.

One significant omission from this definition is the expression evaluation
order. The order is irrelevant due to the design choice that AMPSL functions
cannot modify global state, meaning expressions have no side effects. This is
also reflected in the type of ~Expression~'s denotational representation. It
can only possibly return a value and not a modified state.

**** Assignment Semantics
#+name: AMPSL-denotational-assign-prototypes
#+caption: Function prototypes for the ~assign~ and ~locAssign~ helper
#+caption: functions.
#+begin_src agda2
assign    : Reference Σ Γ t      → ⟦ t ⟧ₜ →
            ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ
locAssign : LocalReference Σ Γ t → ⟦ t ⟧ₜ →
            ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Γ ⟧ₜₛ
#+end_src

I first describe assignment statements before discussing the other statement
forms. If assignments were only into variables this would be trivial. Using
~Reference~, in attempt for AMPSL to keep the same form as ASL, makes things
more tricky. Broadly speaking, there are three kinds of ~Reference~: terminal
references like ~state~ and ~var~; isomorphism operations like ~unbox~, ~[_]~
and ~cast~; and projection operations like ~slice~, ~cut~, ~head~ and ~tail~.

I will describe how to update each kind of reference in turn. This is the action
performed by helper functions ~assign~ and ~locAssign~, whose signatures are
given in [[AMPSL-denotational-assign-prototypes]].

Terminal references are the base case and easy. Assigning into ~state~ and ~var~
updates the relevant part of the variable context. 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~ has the same behaviour as ~ref ≔ unbox
v~.

For reference projections, assigning into one projection of a reference means
that the other projection 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, which is achieved by only updating
the context for a leaf reference.

Interpreting slice as a projection reference type is a major reason why AMPSL
has ~merge~, ~cut~ and ~slice~ instead of the bitstring concatenation and
slicing present in ASL. 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 value encodings. AMPSL
takes these semantic necessities and makes them available to programmers.

~assign~ and ~locAssign~, when given a reference and initial context, return 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
Other AMPSL statements have straightforward semantics. 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 condition's value. ~declare~ statements are also
simple. The initial value is computed and added to the variable context. After
evaluating the subsequent statement, the added variable is stripped away from
the context.

The only looping construct in AMPSL is the ~for~ loop. Because it performs a
fixed number of iterations, it is effectively a sequence of ~declare~
statements. This is also one of the primary reasons why the denotational
semantics can have poor computational performance; every ~for~ loop iteration
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
AMPSL has also been given a form of Hoare Logic rules. The Hoare logic is
syntax-directed; loops only require a single proof. This section starts by
explaining how a AMPSL ~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 total correctness triples for AMPSL.

**** Converting ~Expression~ into ~Term~

As shown 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. AMPSL is not as simple a language as WHILE, thanks to
function calls within expressions. Whilst function calls do not prevent
converting expressions into terms, some care must be taken. In particular, this
conversion is only as functions not modify global variables. The full definition
of ~Term~ and its semantics are given in the provided source code.

First, a demonstration on why function calls need special care in Hoare logic.
For this example, the environment contains a single Boolean-valued global
variable. Consider the following AMPSL function, a unary operator on an
integer, which is the identity when ~state 0F~ is false and otherwise performs
an increment.

#+begin_src agda2
f : Function [ bool ] [ int ] int
f =
  init
    var 0F ∙
    if state 0F then var 0F ≔ lit 1ℤ + var 1F
  end
#+end_src

Consider the expression ~e = call f [ x ]~ of type ~Expression [ bool ] Γ int~.
There are two important aspects to consider for converting ~e~ into a term:
the initial conversion and substitution of references.

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 this term embedding function.

Unfortunately this embedding has problems with substitution. Consider attempting
to substitute a term ~t~, which depends on local variables in ~Γ~, for the
reference ~state 0F~ inside of ~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 to the term ~t~ inside the function ~f~. This embedding is
not sufficient.

A solution comes by thinking of global variables in ~f~ as an additional
argument set. In an ~Expression~, these arguments always corresponds exactly
with the global variables, so are elided. In a term, they can be made explicit.
An embedding function ~↓_~ can be defined, such that ~↓ e = call f [ state 0F ]
[ ↓ x ]~, and all the other expression forms as expected.

Doing a substitution on ~↓ e~ is now simple: perform the substitution on both
argument lists 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 only other difference between ~Expression~ and ~Term~ is the use of
auxiliary variables within Hoare logic terms. AMPSL accomplishes this by
providing a ~meta~ constructor much like ~state~ and ~var~. This indexes into a
new auxiliary variable context, Δ, which forms part of ~Term~'s type definition.

**** Hoare Logic Assertions
The Hoare logic for AMPSL uses a first-order logic for assertions, 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 the provided source code.

The ~Assertion~ type has the usual set of Boolean connectives. Another
constructor 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~.  There is an ~equal~
function to construct an assertion comparing any two values with the same type,
even if their type does not have equality.

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 execution state. For
AMPSL, this state is the current global, local and auxiliary variable contexts.
The predicates are encoded as an indexed family of sets.

The Boolean connectives are represented by their usual type-theoretic
counterparts. Quantifier assertions are also quite easy to give a semantic
representation. Universal quantification is represented by a function taking
values for the quantified variable and returning a proof of the inner assertion.
Existential quantification is represented by a dependent pair of a value for the
quantified variable, and a proof 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. Whilst directly providing a richer type is
difficult, due to having to find a normal form for the ~Term~ type, all
equalities and inequalities between AMPSL values are recomputable. This allows
the user to extract Agda terms for equalities given only knowledge of whether
terms are equal.

**** Correctness Triples for AMPSL
In the traditional presentation of Hoare logic ([[*Hoare Logic]]), there are two
rule types; structural rules based on program syntax and adaptation rules to
modify preconditions and postconditions. The Hoare logic for AMPSL unifies the
two rule types, allowing for purely syntax-directed proofs for any precondition
and postcondition.

#+name: AMPSL-Hoare-logic
#+caption: The Hoare logic correctness triples for AMPSL. The unusual argument
#+caption: order to ~HoareTriple~ allows for different constructors for the
#+caption: different statement forms whilst requiring that ~HoareTriple~ is
#+caption: defined for every precondition and postcondition.
#+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

I will now talk through each of the Hoare logic rules for AMPSL, which are given
in [[AMPSL-Hoare-logic]]. The simplest rule to consider is ~skip~. This immediately
demonstrates how AMPSL 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 mirrors the SEQ rule of WHILE's 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~. 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 AMPSL. A purely structural rule would have ~subst Q ref (↓ val)~ as the
precondition of the statement. AMPSL combines this with the rule of consequence
to allow for an arbitrary precondition.

The other Hoare logic rules for AMPSL are less simple. Most of the added
complexity is a consequence of AMPSL'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.

# (FIXME: describe substitution?)

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~. I will denote the weakened forms ~P′~ and ~Q′~ for brevity. So far the
rule's premise is ~HoareTriple P′ Q′ s~. However, this does not constrain the
new variable. Thus an assertion that the new variable ~var 0F~ is equal to the
initial value ~e~ must be added to the precondition. As ~e~ has type ~Expression
Σ Γ t~ and a term in the precondition needs type ~Term Σ (t ∷ Γ) Δ t~, the Agda
expression ~Term.Var.weaken 0F (↓ e)~, denoted ~e′~ , is used instead. This Agda
expression converts ~e~ to a term and introduces the new variable. This leads to
the final form of the premise: ~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, a loop invariant ~I : Assertion Σ Γ (fin (suc n) ∷
Δ)~ is chosen. The additional auxiliary variable indicates the number of
complete iterations of the loop, from \(0\) to \(n\). I will use ~I(x)~ to
denote the assertion ~I~ with the additional auxiliary variable replaced with
term ~x~, and make weakening variable contexts implicit. The rule's premise
requires 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~. By adding in a new auxiliary
variable to represent the initial value of the loop variable on each iteration,
the current iteration number can be preserved between the precondition and
postcondition. The loop variable itself can be modified by ~s~. By ensuring that
the following triple holds, there is a proof that the loop preserves the
invariant: ~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 AMPSL is ~invoke~. Procedure invocation is tricky
in AMPSL's Hoare logic due to the changing local variable scope in the procedure
body. This is similar to reasons why converting functions calls into terms
presented challenges, back in [[*Converting ~Expression~ into ~Term~]]. 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)~, 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, they can be replaced with auxiliary variables, by assigning a
new auxiliary variable for each one. Within ~P~ and ~Q~, all ~var x~ are
replaced with ~meta x~ to reflect that the local variables have been moved to
auxiliary variables. This is the action performed by the ~varsToMetas~ function.
To complete the premise, the local variables within the procedure body must be
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~.

* Properties and Evaluation of AMPSL

This chapter has two major concerns. The first is to prove that AMPSL's Hoare
logic is sound with respect to the denotational semantics. If the logic is not
sound, it is unsuitable for use in proofs. I will also discuss what steps need
to be taken to show a restricted form of completeness for AMPSL.

The other half of this chapter will give a practical attempt of using AMPSL to
prove a proposition. I will give the AMPSL encoding of ASL form of the Barrett
reduction algorithm given by [cite/t:@10.46586/tches.v2022.i1.482-505]. I will
demonstrate how this works on some concrete values, and explain what work is
left to be done to prove a more general statement.

** Soundness of AMPSL's Hoare Logic

#+name: AMPSL-soundness-statement
#+caption: The theorem statement for soundness of AMPSL's Hoare Logic.
#+begin_src agda2
sound : P ⊢ s ⊢ Q →
        ∀ σ γ δ →
        Assertion.⟦ P ⟧ σ γ δ →
        uncurry Assertion.⟦ Q ⟧ (Semantics.stmt s (σ , γ)) δ
#+end_src

I first define what is meant by soundness. [[AMPSL-soundness-statement]] shows the
Agda type corresponding to the proposition.

#+attr_latex: :options [Soundness]
#+begin_theorem
Given a Hoare logic proof that \(\{P\}\;\texttt{s}\;\{Q\}\) holds, then for any
concrete instantiation of the global, local and auxiliary variable contexts, if
\(P\) holds on the initial state, \(Q\) holds on the state after evaluating
\texttt{s}.
#+end_theorem

A proof can be given by a recursive function in Agda. Some cases in this
function are trivial: the premise of the ~skip~ Hoare logic rule is exactly the
proof statement needed, and the ~seq~ rule can be satisfied by composing the
results of the inductive hypothesis on the two premises. The cases for the ~if~
and ~if-else~ rules pattern match on the result of evaluating the condition
expression, then it recurses into the true or false branch respectively. This
relies on a trivial proof that the semantics of an ~Expression~ are
propositionally equal to the semantics of that expression embedded as a ~Term~.

The ~assign~ rule is also relatively simple. Because the ~Reference~ type
excludes product references, it is sufficient to show that substituting into a
single global or local variable is sound. Due to the recursive nature of
substitution, this simply requires a propositional proof of equality for terms.

Other cases like ~declare~, ~invoke~ and ~for~ are much more complex, mostly due
to the use of helper functions like variable weakening and elimination. I will
take a quick diversion into how to prove these manipulations do not affect the
semantics of terms and assertions before discussing how soundness is shown for
these more complex Hoare logic rules.

*** Proving Properties of Term and Assertion Manipulations
#+name: term-homomorphisms
#+caption: The types of all the ~Term~ homomorphisms required to define AMPSL's
#+caption: Hoare Logic. They are logically split into three groups depending on
#+caption: whether the homomorphism targets global, local or auxiliary
#+caption: variables.
#+begin_src agda2
module State where
  subst     : ∀ i → Term Σ Γ Δ t → Term Σ Γ Δ (lookup Σ i) →
              Term Σ Γ Δ t
module Var where
  weaken    : ∀ i → Term Σ Γ Δ t → Term Σ (insert Γ i t′) Δ t
  weakenAll : Term Σ [] Δ t → Term Σ Γ Δ t
  elim      : ∀ i → Term Σ (insert Γ i t′) Δ t → Term Σ Γ Δ t′ →
              Term Σ Γ Δ t
  elimAll   : Term Σ Γ Δ t → All (Term Σ ts Δ) Γ → Term Σ ts Δ t
  subst     : ∀ i → Term Σ Γ Δ t → Term Σ Γ Δ (lookup Γ i) →
              Term Σ Γ Δ t
module Meta where
  weaken    : ∀ i → Term Σ Γ Δ t → Term Σ Γ (insert Δ i t′) t
  weakenAll : ∀ (Δ′ : Vec Type k) (ts : Vec Type m) →
              Term Σ Γ (Δ′ ++ Δ) t → Term Σ Γ (Δ′ ++ ts ++ Δ) t
  inject    : ∀ (ts : Vec Type n) → Term Σ Γ Δ t → Term Σ Γ (Δ ++ ts) t
  elim      : ∀ i → Term Σ Γ (insert Δ i t′) t → Term Σ Γ Δ t′ →
              Term Σ Γ Δ t
#+end_src

Three out of eight of AMPSL's Hoare logic rules require manipulating the form of
terms and assertions to introduce free variables, rename existing variables, or
perform eliminations or substitutions of variables. [[term-homomorphisms]] gives the
types of each the ten homomorphisms on terms. Given that the ~Term~ type has 32
constructors, this means a naive definition would require 320 cases, each at
least a line long, and most duplicates.

This number can be greatly reduced by realising that the only interesting cases
in these homomorphisms are the constructors for variables: ~state~, ~var~ and
~meta~. By giving the action of a homomorphism on these three constructors,
the definition of a full homomorphism can be constructed.

#+name: term-weakening
#+caption: A record that defines the three interesting cases for weakening a
#+caption: ~Term~ by adding a new local variable. A generic function extends a
#+caption: ~RecBuilder~ into a full term homomorphism.
#+begin_src agda2
weakenBuilder : ∀ i → RecBuilder Σ Γ Δ Σ (insert Γ i t) Δ
weakenBuilder {Γ = Γ} i = record
  { onState = state
  ; onVar   = λ j → Cast.type (Vecₚ.insert-punchIn Γ i _ j)
                              (var (punchIn i j))
  ; onMeta  = meta
  }
#+end_src

This is best illustrated by an example. [[term-weakening]] shows how weakening local
variables can be extended to a full homomorphism by only giving the ~state~,
~var~ and ~meta~ cases. As weakening local variables only affects the ~var~
case, the ~state~ and ~meta~ cases are identities. The ~var~ case then
\ldquo{}punches in\rdquo{} the new variable, wrapped in a type cast to satisfy
Agda's dependent typing.

Proving that the term manipulations are indeed homomorphisms in the semantics
also requires fewer lines than the 320 naive cases. Like with the manipulation
definitions, the proofs only need to be given for the ~state~, ~var~ and ~meta~
cases. However, it is not enough for a proof to simply show that the ~state~
~var~ and ~meta~ cases are homomorphisms. The proof must also state how to
extend or reduce the variable contexts to the correct form.

Returning to the local variable weakening example, the relevant construction for
proof is shown in [[*Example ~Term~ Homomorphism Proof]]. First I specify how to
modify the variable contexts. The global and auxiliary variable contexts are
unchanged, whereas a value for the weakened variable is inserted into the local
variable context. Then I prove the homomorphism is correct on each of ~state~,
~var~ and ~meta~. As ~state~ and ~meta~ were unchanged, the proof is trivial by
reflexivity. The variable case is also quite simple, first proving that the
~Cast.type~ function is denotationally the same as a substitution, and then
showing that fetching a \ldquo{}punched in\rdquo{} index from a list with an
insertion is the same as fetching the original index from an unmodified list.

In total, these two optimisations save roughly 580 lines of Agda code in
the definition and proofs of term manipulations. However, there are still
roughly 800 lines remaining that would be difficult to reduce further.

Assertion manipulations have a similar amount of repetition as term
manipulations. However, there are two important differences that make a generic
builder pattern unnecessarily complex. First, the ~Assertion~ type has fewer
constructors, totalling nine instead of 32. Whilst homomorphisms will still
feature many trivial cases, it occurs at a much lower ratio compared to the
amount of useful code. The second reason is that the ~all~ and ~some~
constructors introduce new auxiliary variables. This means that the subterms of
these constructors have a different type from other assertions, making a generic
solution much more complex.

Proofs that assertion manipulations are homomorphisms are also fundamentally
different that those for term homomorphisms. Whilst the denotational semantics
of a term produces the same type regardless of whether it is under homomorphism,
the denotational representation of an assertion is itself a type. In particular,
the dependent types created by the denotations of ~all~ and ~some~ assertions
are impossible to use in propositional equality, as Agda does not allow for
meaningful propositional equality of functions, which appear in these types.
Instead, I prove the types are equivalent.

Only three constructors for ~Assertion~ have interesting cases in these proofs.
The ~pred~ constructor delegates the work to proofs on the ~Term~ manipulations,
using the resulting propositional equality to safely return the input term. The
~all~ and ~some~ constructors first have to show that homomorphisms on the inner
assertions and other arguments preserve type equality before they can recurse.

*** Soundness of ~declare~, ~for~ and ~invoke~
Referring back to [[AMPSL-Hoare-logic]] for the Hoare logic definitions, the
soundness proof cases for the final three rules can be completed. The ~declare~
rule is straight forward. To satisfy the recursive precondition, I instantiate
the new auxiliary variable to the initial value of the new variable. Then, I
prove that the weakened precondition holds, and add to it a proof that the
additional variable is indeed the initial value of the newly-declared variable.
Then I inductively apply soundness, to obtain a proof that the weakened
postcondition holds. Finally, I apply the weakening proof for ~Assertion~ in
reverse, obtaining a proof that the postcondition holds.

The proof for ~for~ is much more involved, and only an outline will be given. I
will also reuse the syntax from [[*Correctness Triples for AMPSL]] for the
invariant. By using the implication premises for the ~for~ Hoare logic rule, I
can obtain a proof that ~I(0)~ holds from the proof of the initial precondition,
and convert a proof of ~I(m)~ to a proof of the final postcondition. All that
remains is a proof that the loop preserves the invariant.

This required two parts. The first part is a proof that each individual loop
iteration maintains the invariant. This required using a number of lemmata
asserting that various assertion manipulations are homomorphisms, as well as a
few type-safe substitutions. The second part was a proof that all these
individual steps can be combined together to make a proof that the whole loop
preserves the invariant. The soundness proof case of ~for~ totals around 220
lines of Agda, excluding the additional lemmata.

Unfortunately, the proof of soundness for ~invoke~ is currently incomplete, due
to time constraints for the project. The proof itself should be simpler than the
proof for the ~for~ rule, as the ~invoke~ rule uses fewer ~Assertion~
manipulations. Whilst each individual step in the rule is trivial, writing them
formally takes a considerable amount of time.

*** Argument for a Proof of Correctness
A general proof of correctness of the AMPSL Hoare logic rules for arbitrary
predicates on the input and output states is impossible within Agda. There are a
large class of predicate that fall outside the scope of what can be created
using the ~Assertion~ type. Additionally, even if a predicate could be the
denotational representation of an assertion, there is no algorithm to decide the
assertion given the predicate, as there is no way to pattern match on the
predicate type.

Due to this, any statement about correctness must be given the precondition and
postcondition assertions explicitly. This results in the following theorem
statement for the most general proof of correctness:

#+begin_src agda2
-- impossible to prove
correct : (∀ σ γ δ →
           Assertion.⟦ P ⟧ σ γ δ →
           uncurry Assertion.⟦ Q ⟧ (Semantics.stmt s (σ , γ)) δ) →
          P ⊢ s ⊢ Q
#+end_src

Unfortunately this also very quickly causes a problem in Agda. Consider the
statement ~s ∙ s₁~. To prove this in AMPSL's Hoare logic, it is necessary to
give two subproofs: ~P ⊢ s ⊢ R~ and ~R ⊢ s₁ ⊢ Q~. As input, there is a single
function transforming proofs of the precondition to proofs of the postcondition.
The problem occurs because there is no way to decompose this function into two
parts, one for the first statement and another for the second.

To resolve this, I anticipate that proving correctness in AMPSL's Hoare logic
will require the following steps:

1. Construction of a function ~wp : Statement Σ Γ → Assertion Σ Γ Δ → Assertion
   Σ Γ Δ~ that computes the weakest precondition of an assertion.
2. A proof that for all statements ~s~ and assertions ~P~, ~wp s P ⊢ s ⊢ P~ is
   satisfiable.
3. A proof that for all statements ~s~ and assertions ~P~ and ~Q~, ~P ⊢ s ⊢ Q~
   implies ~P ⊆ wp s Q~.
4. A proof that the rule of consequence is derivable from the other AMPSL Hoare
   logic rules.

The first three steps form the definition of the weakest precondition for an
assertion [cite:@10.1145/360933.360975]: step one asserts that such an assertion
exists for all statements and assertions; step two asserts that the assertion is
indeed a valid precondition for the choice of statement and postcondition; and
step three asserts that any other precondition for ~s~ that derives ~Q~ must
entail the weakest precondition.

With the additional step of proving the rule of consequence as a meta rule, a
valid formulation for the correctness of AMPSL's Hoare logic can be given, which
follows trivially from the four steps above:

#+begin_src agda2
correct : (∀ σ γ δ → Assertion.⟦ P ⟧ σ γ δ → Assertion.⟦ wp s Q ⟧ σ γ δ) →
          P ⊢ s ⊢ Q
#+end_src

Constructing the weakest preconditions from an ~Assertion~ and ~Statement~
should be a relatively simple recursion. I will sketch the ~if_then_else~ and
~invoke~ cases. For ~if e then s else s₁~, I can recursively construct the
weakest preconditions ~P~ and ~P₁~ for ~s~ and ~s₁~ respectively. The weakest
precondition of the full statement will then be ~P ∧ e ∨ P₁ ∧ inv e~.

To find the weakest precondition of a function invocation ~invoke (s ∙end) es~
and ~Q~, first find the weakest precondition of ~s~ and ~Q′~ , where ~Q′~ is the
result of replacing local variables in ~Q~ with auxiliary variables in the same
manner as the ~invoke~ AMPSL Hoare logic rule. Then, apply the inverse
transformation to the auxiliary variables, and finally replace occurrences of
the procedure-local variables with the arguments.

# (FIXME: sketch the for case?)

** Using AMPSL for Proofs

This section will describe how I converted ASL representing a Barrett reduction
implementation [cite:@10.46586/tches.v2022.i1.482-505] into AMPSL, focusing on
the modelling choices I made. I will then discuss how to use the AMPSL code in
concrete proofs for specific values, before concluding with the steps necessary
to abstract the proof to arbitrary values.

The most significant modelling decisions are the omissions of the ~TopLevel~
[cite:@arm/DDI0553B.s §E2.1.400] and the ~InstructionExecute~
[cite:@arm/DDI0553B.s §E2.1.225] ASL functions.  ~TopLevel~ is the ASL function
describing the actions of an architecture tick. It primarily deals with
debugging, halt and lockup processor states, none of which are relevant for the
Barrett reduction or NTT correctness proofs I am working towards.
~InstructionExecute~ deals with fetching instructions and deciding whether to
execute an instruction beatwise or linearly.

The choice of which instructions beats to schedule is in the ~ExecBeats~
pseudocode function [cite:@arm/DDI0553B.s §E2.1.121]. My model, shown
side-by-side in [[*Example Armv8-M Instruction Models in AMPSL]], reduces the
scheduling part to a linear order where all beats of a beatwise instruction are
executed in a tick.

Another pseudocode function I have decided to omit is  ~DecodeExecute~. This
performs instruction decoding as specified in Chapter C2 of
[cite/t:@arm/DDI0553B.s §E2.1.121], and then performs the execution step
specified further down the instruction descriptions. I instead decided to give
~ExecBeats~ a procedure that performs the execution of a single instruction, as
decoding a known sequence of instructions is infallible.

The Barrett reduction implementation by
[cite/t:@10.46586/tches.v2022.i1.482-505] requires two instructions: ~VQRDMULH~
and ~VMLA~. The AMPSL definitions are given in [[*Example Armv8-M Instruction
Models in AMPSL]]. Like most beatwise instructions, both procedures end with a
loop that copies the masked bytes of an intermediate result into the destination
register. This is the action performed by the ~copyMasked~ procedure given back
in [[*Example AMPSL Statements]].

#+name: barrett-impl
#+caption: AMPSL model of Barrett reduction.
#+begin_src agda2
barrett : (n : ℕ) → ⦃ NonZero n ⦄ → (t z : VecReg) (im : GenReg) →
          Procedure State []
barrett n t z im =
  ,*index R (lit im) ≔
    call (sliceⁱ 0) (lit (ℤ.+ (2147483648 div n)) ∷ []) ∙
  invoke vqrdmulh-s32,t,z,m [] ∙
  ,*index R (lit im) ≔ call (sliceⁱ 0) (lit (ℤ.- n) ∷ []) ∙
  invoke vmla-s32,z,t,-n [] ∙end
  where
  vqrdmulh-s32,t,z,m =
    ExecBeats (vqrdmulh (record
      { size = 32bit
      ; dest = t
      ; src₁ = z
      ; src₂ = inj₁ im
      }))
  vmla-s32,z,t,-n =
    ExecBeats (vmla (record
      { size     = 32bit
      ; acc      = z
      ; src₁     = t
      ; src₂     = im
      }))
#+end_src

The final AMPSL procedure used to calculate Barrett reduction is in
[[barrett-impl]]. As Barrett reduction is performed with a fixed positive base, the
procedure takes the base as a non-zero Agda natural number.

This definition was tested by using the following snippet, instantiating
the ~int~ and ~real~ types with Agda integers and rationals respectively.

#+begin_src
do-barrett : (n : ℕ) →
             (zs : Vec ℤ 4) →
             Statement State []
do-barrett n zs =
  for 4 (
    Q[ lit 0F , var 0F ] ≔
      call (sliceⁱ 0) (index (lit zs) (var 0F) ∷ [])) ∙
  invoke (barrett n 1F 0F 0F) []

barrett-101 : Statement State []
barrett-101 = do-barrett 101 (+ 1 ∷ + 7387 ∷ + 102 ∷ - 7473 ∷ [])
#+end_src

Asking Agda to normalise the ~barrett-101~ value, which expands the function
definitions to produce a single ~Statement~, results in a 16KB ~Statement~. When
I tried to evaluate this denotationally, Agda exhausted heap memory after 45
minutes.

The poor performance of AMPSL's denotational semantics on this small example
highlights the necessity of the syntax-directed Hoare logic proof system. Using
the Hoare logic rules to attempt to directly prove that ~barrett-101~ has the
desired effect leads to a very tedious proof of expanding out the whole
derivation tree requiring 64 loop invariants or logical implications to
complete.

*** Proving Reusable Results
Whilst being able to prove results about concrete computations is useful, being
able to prove results on abstract variables is more so. As discussed in the
previous section, the ~copyMasked~ procedure given in [[*Example AMPSL Statements]]
is used in most Armv8-M vector instructions. Having some proofs about its
properties would make giving the semantics of Armv8-M instructions much simpler.

Notice that when each bit of the ~mask~ argument to the procedure is true, the
procedure reduces to an assignment of ~x~ into the machine register ~Q[ dest ,
beat ]~. This is reflected in the following Agda type:

#+begin_src agda2
copyMasked-mask≡true : ∀ {dest x beat mask} {P Q : Assertion State Γ Δ} →
    P ⊆ equal (↓ mask) (lit (replicate (lift Bool.true))) →
    P ⊆ Assertion.subst Q Q[ dest , beat ] (↓ x) →
    P ⊢ invoke copyMasked (dest ∷ x ∷ beat ∷ mask ∷ []) ⊢ Q
#+end_src

The first implication requires that the precondition ensures that the mask is
initially true. The second implication is the same one as from the ~assign~
Hoare logic rule, specialised for the reference ~Q[ dest , beat ]~.

By using the Hoare logic rules as defined in [[*Correctness Triples for AMPSL]], the
following incomplete Agda term for a proof skeleton can be found:

#+begin_src agda2
invoke
  (for {!!} {!!}
     (if (assign {!!})
         {!!}))
#+end_src

To complete the proof, it is sufficient to fill in these four missing terms.
These consist of: a choice of loop invariant; a proof the initial state inside
the procedure body entails the loop condition; a proof that, given a bit in
~mask~ is true, performing the assignment for that byte preserves the invariant; a
proof that, given a bit in ~mask~ is false, the loop invariant is preserved; and
a proof that the loop invariant entails the postcondition when the loop is complete.

Because the loop does not change the value of the ~mask~ variable, the loop
invariant can include an assertion that the ~mask~ is always true. This makes
the implication for the ~else~ branch of the loop body a trivial proof by
contradiction.

The other three missing values are simple when presented for a paper proof.
Unfortunately, the ~Assertion~ and ~Term~ manipulations applied by AMPSL's Hoare
logic rules make formulation within Agda more complex. The full proof is
currently incomplete due to a number of missing trivial lemmata, due to project
time constraints.

* Proof of Barrett Reduction

Barrett reduction is an algorithm to find a small representative of a value
\(z\) modulo some base \(n\). Instead of having to perform expensive integer
division, Barrett reduction instead uses an approximation function to precompute
a coefficient \(m = \llbracket \frac{2^k}{n} \rrbracket\). The integer division
\(z / n\) is then approximated by the value \(\left\llbracket \frac{zm}{2^k}
\right\rrbracket\).

There are many choices of function that are suitable for the two approximations.
[cite/t:@10.1007/3-540-47721-7_24] used the floor function in both cases,
whereas the Barrett reduction implementation by
[cite/t:@10.46586/tches.v2022.i1.482-505] instead uses \(\llbracket z \rrbracket
= 2 \left\lfloor \frac{z}{2} \right\rfloor\). Work by
[cite/t:@10.46586/tches.v2022.i1.211-244] proves results for regular rounding at
runtime, but any \ldquo{}integer approximation\rdquo{} for precomputing the
coefficient \(m\).

The simplest form of Barrett reduction is that of Barrett, using two floor
approximations. Thus this is the version for which I have produced my initial
proof.

Unlike the previous authors, who all dealt explicitly with integers and
rationals, I instead proved a more abstract result for an arbitrary commutative
ordered ring \(ℤ\) and ordered field \(ℝ\) with a homomorphism \(\cdot/1 : ℤ
\to ℝ\) and a floor function \(\lfloor\cdot\rfloor : ℝ \to ℤ\) that is /not
necessarily/ a homomorphism.

This decision will eventually allow for the direct use of this result in
abstract proofs about the AMPSL Barrett reduction algorithm. This is due to the
choice of AMPSL's type models for ~int~ and ~real~ as abstract structures,
discussed in [[*AMPSL Datatype Models]].

One major time sink for this abstraction was the complete lack of support from
preexisting Agda proofs. Ordered structures like the rings and fields required
are not present in the Agda standard library version 1.7, and the
discoverability of other Agda libraries is lacking. Thus much work was spent
encoding these structures and proving many trivial lemmata about them, such as
sign-preservation, monotonicity and cancelling proofs. This totals roughly 2600
lines of Agda.

#+name: barrett-properties
#+caption: Three properties I was able to prove about flooring Barrett reduction
#+caption: for an abstract ordered ring and field.
#+begin_src agda2
barrett-mods     : ∀ z → ∃ λ a → barrett z + a * n ≈ z
barrett-positive : ∀ {z} → z ≥ 0ℤ → barrett z ≥ 0ℤ
barrett-limit    : ∀ {z} → 0ℤ ≤ z → z ≤ 2ℤ ^ k → barrett z < 2 × n
#+end_src

In total I was able to prove three important properties of the flooring variants
of Barrett reduction, listed using Agda in [[barrett-properties]]. The first
property states that Barrett reduction does indeed perform a modulo reduction,
the entire purpose of the algorithm. The second ensures that the Barrett
reduction of a positive value is remains positive, meaning that flooring Barrett
reduction can safely use unsigned integer types. The final property states that
for sufficiently small values of \(z\), Barrett reduction produces a
representable no more than twice the size of the base, thus reducing values to a
small representable module the base.

* Summary and Conclusions

In this work, I made significant progress into proving that an implementation of
the NTT algorithm for the M-profile vector extension of the Armv8.1-M
architecture is functionally correct. I made progress on two fronts: giving a
formal semantics for Armv8-M instructions, and proving properties about Barrett
reduction.

To provide formal semantics for Armv8-M instructions, I designed AMSPL, a
language with formal semantics that models the ASL used to describe instruction
semantics in the reference manual by [cite/t:@arm/DDI0553B.s]. As AMPSL models
ASL, the behaviour of instructions can be modelled in AMPSL. Then, given enough
time to prove a number of trivial lemmata, it is possible to specify the
semantics of Armv8-M instructions through the semantics of AMPSL.

To my knowledge, I have produced the first computer-assisted proof about the
properties of Barrett reduction on arbitrary inputs. Further, I have not only
proven this result for integers and rationals, but for any abstract ring and
field with a suitable floor function. Barrett reduction is a vital subroutine in
NTT so these proofs form a solid foundation towards the final goal.

** Future Work on AMPSL

Whilst the core syntax and semantics of AMPSL is complete, there are a wide
range of proofs that are currently incomplete, due to the shear amount of
trivial bookwork required to prove them. Here is a short list of some incomplete
results:

- Soundness of Hoare Logic :: There is proof that AMPSL's Hoare logic is sound
  with respect to its denotational semantics for all rules excluding ~invoke~
  ([[*Soundness of ~declare~, ~for~ and ~invoke~ ]]). The proof of this rule should
  be relatively straight forward, but the ~Term~  and ~Assertion~ homomorphisms
  it performs are the most complex and still without proof.
- Completeness of Hoare Logic :: I have only conjectured that AMPSL's Hoare
  logic is complete, in the sense given in [[*Argument for a Proof of Correctness]].
  Actually creating the weakest-precondition function requires the creation of
  more ~Term~ and ~Assertion~ homomorphisms with more complex effects, and using
  them in proofs requires proving trivial lemmata.
- Evaluating Denotational Semantics :: Asking Agda to normalise the denotational
  semantics of any reasonable computation often results in Agda running out of
  memory ([[*Using AMPSL for Proofs]]). Investigating and eliminating the cause of
  this behaviour would make the user experience for AMPSL significantly better.
- Using Hoare Logic Rules :: Using AMPSL's Hoare logic rules for any large
  statement is tedious and cumbersome ([[*Using AMPSL for Proofs]]). Trying to
  create abstract proofs of correctness for smaller statements requires the
  manual proof of many trivial implications ([[*Proving Reusable Results]]).

Whilst AMPSL has the potential to be an enormously useful tool for the formal
verification of Armv8-M assembly algorithms, its current state does not yet live
up to the promise. Currently a huge push needs to be made to complete proofs of
many of the missing lemmata which I did not have time to complete in this
project.

** Future Work for Functional Correctness

Whilst AMPSL is able to model ASL to a degree suitable for basic functional
correctness proofs, a more rigorous tool is necessary for future endeavours. One
option is to add Armv8-M as a backend in pre-existing functional correctness
tools like Jasmin [cite:@10.1145/3133956.3134078] and Vale
[cite:@10.1145/3290376]. Another option is to add the architecture as a backend
in formally-verified compilers like CompCert [cite:@hal/01238879], enabling the
use of high-level functional correctness tools targetting C.

Another alternative, particularly for working on pre-existing, hand-written
assembly routines, is to model the Armv8-M semantics using Sail. Unlike AMPSL,
Sail would model the full complexity of the ASL description of instructions,
allowing for more rigorous proofs about the program semantics.

#+latex: \label{lastcontentpage}

#+latex: %TC:ignore

#+print_bibliography:

\appendix

* Example ~Term~ Homomorphism Proof
# #+name: term-weakening-proof
# #+caption: A record that shows that ~Term.Var.weaken~ is a homomorphism that
# #+caption: preserves semantics. Because the variable contexts change between the
# #+caption: two sides of the homomorphism, this record has to describe how to
# #+caption: extend the variable contexts first. Then it has to show the actions
# #+caption: of ~Term.Var.weaken~ on global, local and auxiliary variables are
# #+caption: indeed homomorphisms. A similar record type exists for homomorphisms
# #+caption: that restrict the variable contexts like variable elimination.
#+begin_src agda2
weakenBuilder-proof : ∀ i → ⟦ t ⟧ₜ → RecBuilder⇒ (Term.Var.weakenBuilder i)
weakenBuilder-proof {t = t} {Γ = Γ} i v = record
  { onState⇒ = λ σ γ δ → σ
  ; onVar⇒   = λ σ γ δ → Core.insert′ i Γ γ v
  ; onMeta⇒  = λ σ γ δ → δ
  ; onState-iso = λ _ _ _ _ → refl
  ; onVar-iso   = onVar⇒
  ; onMeta-iso  = λ _ _ _ _ → refl
  }
  where

  onVar⇒ : ∀ j σ γ δ → _
  onVar⇒ j σ γ δ = begin
    Term.⟦ Term.Cast.type eq (var (punchIn i j)) ⟧ σ γ′ δ
      ≡⟨ Cast.type eq (var (punchIn i j)) σ γ′ δ ⟩
    subst ⟦_⟧ₜ eq (Core.fetch (punchIn i j) (insert Γ i t) γ′)
      ≡⟨ Coreₚ.fetch-punchIn Γ i t j γ v ⟩
    Core.fetch j Γ γ
      ∎
    where
    open ≡-Reasoning
    γ′ = Core.insert′ i Γ γ v
    eq = Vecₚ.insert-punchIn Γ i t j
#+end_src
* Example Armv8-M Instruction Models in AMPSL
~ExecBeats~ in Arm pseudocode:

\begin{verbatim}
boolean ExecBeats()
  newBeatComplete = BeatComplete
  _InstId = instId;
  _CurrentInstrExecState = GetInstrExecState(instId);
  InstStateCheck(ThisInstr());
  for beatInTick = 0 to BEATS_PER_TICK-1
    beatId = beatInTick
    beatFlagIdx = (instId * MAX_BEATS) + beatId;
    if newBeatComplete[beatFlagIdx] == '0'
    then
      _BeatId          = beatId;
      _AdvanceVPTState = TRUE;
      cond             = DefaultCond();
      DecodeExecute(ThisInstr(),
                    ThisInstrAddr(),
                    ThisInstrLength() == 2,
                    cond);
      newBeatComplete[beatFlagIdx] = '1';
      if _AdvanceVPTState then
        VPTAdvance(beatId);
  commitState = newBeatComplete[MAX_BEATS-1:0] == Ones(MAX_BEATS);
  if commitState then
    newBeatComplete = LSR(newBeatComplete, MAX_BEATS);
  BeatComplete = newBeatComplete
  return commitState;
\end{verbatim}

Simplified ~ExecBeats~ in AMPSL:

#+begin_src agda2
ExecBeats : Procedure State [] → Procedure State []
ExecBeats DecodeExec =
  for 4 (
    let beatId = var 0F in
    BeatId ≔ beatId ∙
    AdvanceVPTState ≔ lit true ∙
    invoke DecodeExec [] ∙
    if ! AdvanceVPTState then
      invoke VPTAdvance (beatId ∷ []))
  ∙end
#+end_src

\newpage
~VQMLRD~ in AMPSL:

#+begin_src agda2
vqrdmulh : Instr.VQRDMULH → Procedure State []
vqrdmulh =
  declare (call GetCurInstrBeat []) (
    -- let elmtMask = head (tail (var 0F)) in
    let curBeat = head (var 0F) in
    declare (! Q[ lit src₁ , curBeat ]) (
    declare (lit (Vec.replicate false)) (
    let elmtMask = head (tail (var 2F)) in
    let curBeat = head (var 2F) in
    -- let op₁ = var 1F in
    let result = var 0F in
    for (toℕ elements) (
      let curBeat     = head (var 3F) in
      let op₁         = var 2F in
      let result      = var 1F in
      let i           = var 0F in
      let value       = (lit (ℤ.+ 2) * call sint (index-32 size op₁ i ∷ [])
                      * call sint (op₂ ∷ []) + rVal) >> toℕ esize in
      let result′,sat = call (SignedSatQ (toℕ esize-1) (value ∷ [])) in
      let sat         = head (tail result′,sat) in
      let result′     = head result′,sat in
      ,*index-32 size result i ≔ result′ ∙
      if sat && hasBit elmtMask (fin e*esize>>3 (tup (i ∷ []))) then
        FPSCR-QC ≔ lit true
    )) ∙
    invoke copyMasked (lit acc ∷ result ∷ curBeat ∷ elmtMask ∷ [])
    ))) ∙end
  where
  open Instr.VQRDMULH d
  op₂ =
    let curBeat = head (var 3F) in
    let i = var 0F in
    [ (λ src₂ → index-32 size (index (! R) (lit src₂)) i)
    , (λ src₂ → index-32 size (! Q[ lit src₂ , curBeat ]) i)
    ]′ src₂
  rVal = lit 1ℤ << toℕ esize-1
#+end_src

\newpage
~VMLA~ in AMPSL:

#+begin_src agda2
vmla : Instr.VMLA → Procedure State []
vmla =
  declare (call GetCurInstrBeat []) (
    let curBeat = head (var 0F) in
    declare (! Q[ lit src₁ , curBeat ]) (
    declare (lit (Vec.replicate false)) (
    let elmtMask = head (tail (var 2F)) in
    let curBeat = head (var 2F) in
    let result = var 0F in
    for (toℕ elements) (
      let curBeat  = head (var 3F) in
      let op₁      = var 2F in
      let element₁ = call sint (index-32 size op₁ i ∷ []) in
      let result   = var 1F in
      let i        = var 0F in
      let op₂      = ! Q[ lit acc , curBeat ] in
      let element₃ = call sint (index-32 size op₂ i ∷ []) in
      ,*index-32 size result i ≔
        call (sliceⁱ 0) ((element₁ * element₂ + element₃) ∷ [])
    )) ∙
    invoke copyMasked (lit acc ∷ result ∷ curBeat ∷ elmtMask ∷ [])
    )) ∙end
  where
  open Instr.VMLA d
  element₂ = call sint (index-32 size (index (! R) (lit src₂)) (lit 0F) ∷ [])
#+end_src

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

#  LocalWords:  AMPSL Hoare NTT PQC structs bitstring bitstrings