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 :eval export
(if (not (boundp 'squid-eval))
    (setq squid-eval nil))

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

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

Main chapters word count: call_wordcount()

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

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

\end{sffamily}

\onehalfspacing
#+end_export

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

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] does not
have a formal semantic description. I designed AMPSL, to mock the Arm
specification language, within in 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 big 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
huge computational demands of post-quantum cryptography, algorithms like the NTT
are presented using hand-written, highly-optimised assembly code. To ensure the
correctness of these cryptographic algorithms, and thus the security of embedded
devices, formal verification of these algorithms is necessary.

This report focuses on 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 properties of their semantics.

To remedy this, I designed AMPSL (Arm M-profile Pseudocode Specification
Language, or AMPSL Mocks Pseudocode Specification Language), which mocks the Arm
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 the explicit computation of the effect of AMPSL on the
processor state. AMPSL also has a set of Hoare logic rules, which form an
axiomatic, syntax-directed approach to describing how a statement in AMPSL
modifies assertions on the processor state.

Due to AMPSL's similarity to ASL, I can convert the ASL description of Armv8-M
instructions into AMPSL. From this AMPSL description of the Armv8-M
instructions, 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 a
big step in formalising the behaviour of many PQC algorithms, formalising
Barrett reduction is a big step in formalising the NTT.

#+name: raw_progress
#+begin_src dot :file progress.pdf :exports none
digraph {
    node [shape=box];
    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. Work with no significant progress made has a dotted
#+caption: border.
call_raw_progress()

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

The main contributions of this report are as follows:
- In [[*AMPSL Syntax]], I introduce the syntax of the AMPSL programming language.
  The primary goal of the syntax is to facilitate easy translation of programs
  from ASL, detailed in [[*Arm Pseudocode]] into AMPSL, whilst allowing AMPSL
  semantics to remain simple.
- The semantics of AMPSL are described in [[*AMPSL Semantics]]. The primary
  achievement of this work is the simple semantics of AMPSL, which facilitates
  straight-forward proofs about various AMPSL programs. I detail both a
  denotational semantics and a Hoare logic for AMPSL.
- 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. The Hoare logic
  used by AMPSL somewhat varies from the traditional presentation, given in
  [[*Hoare Logic]], to enforce that Hoare logic proofs have bounded depth with
  respect to the program syntax.  This proof is possible due to Agda's
  foundation of Martin-Löf's type theory, the significance of which is given in
  [[*Agda]]. Due to the soundness of AMPSL's Hoare logic, the behaviour of the
  computationally-intensive denotational semantics can instead be specified
  using syntax-directed Hoare logic.
- A number of example proofs for AMPSL programs are given in [[*Using AMPSL for
  Proofs]]. This describes how AMPSL is used to give the semantics of Armv8.1-M
  instructions. It also demonstrates the viability of using AMPSL for the formal
  verification of a number of programs, and lays the groundwork for the formal
  verification of the NTT given by [cite/t:@10.46586/tches.v2022.i1.482-505].
- Finally, a formal proof of a Barrett reduction variant is given in [[*Proof of
  Barrett Reduction]]. To my knowledge this is the first such machine-verified
  proof of correctness for Barrett reduction. Further, it is the first proof of
  Barrett reduction on 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, as you would find in most imperative languages. Its primary
purpose is to explain how executing an Armv8-M instruction modifies the visible
processor state. As it is a descriptive aid, ASL features a number of design
choices atypical of other imperative programming languages making execution
difficult.

Something common to nearly all imperative languages is the presence of a
primitive type for Booleans. Other typical type constructors are tuples,
structs, enumerations and fixed-length arrays.

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, the efficiency of code 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 arrays of Booleans. The justification given by [cite/t:@arm/DDI0553B.s
§E1.2.2] is more philosophical than practical: \ldquo{}bitstrings are the only
concrete data type in pseudocode\rdquo{}. In some places, bitstrings can be used
instead of integers in arithmetic operations, by first converting them to an
unsigned integer.

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---a single bit is represented as a bitstring
of length one---so bitstring slicing always returns a bitstring.  Slicing then
works in much the same way as array slicing in languages like Python 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 an integer can be sliced instead of a bitstring. 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 forms of items: procedures,
functions and array-like functions. Procedures and functions behave like
procedures and functions of other imperative languages. The arguments to them
are passed by value, and the only difference between the two is that procedures
do not return values whilst functions do [cite:@arm/DDI0553B.s §E1.4.2].

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

Examples of ASL are given throughout the report, often 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.

Vector instructions can also overlap during execution. To summarise the overlap
rules, vector instructions can overlap if there are no inter-beat data
dependencies, at least beats of the current instruction are complete and at most
two beats of the next instruction are complete.

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

A partial correctness triple is a relation between a precondition \(P\), a
program statement \(s\) and a postcondition \(Q\). If \(\{P\} s \{Q\}\) is a
partial correctness triple, then whenever \(P\) holds for some machine state,
then when executing \(s\), \(Q\) holds for the state after it terminates
[cite:@10.1145/363235.363259]. This is a /partial/ correctness triple because
the postcondition only holds if \(s\) terminates. When all statements terminate,
this relation is called a correctness 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 Hoare introduced for the WHILE language
[cite:@10.1145/363235.363259]. There are two broad classes of Hoare logic rules.
Structural rules that reflect how program syntax affects execution of a program,
and thus how to modify the precondition and postcondition assertions
accordingly. Adaptation rules use the same statement in the premise and
conclusion. They only adapt the preconditions and postconditions used.

Of the structural rules, 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 we take, the
postcondition remains the same; an if statement does no computation after
executing a branch.  Which branch we take depends on the value of ~e~. Because
the value of ~e~ is known before executing a branch, it is added to the
preconditions in the premises.

The ASSIGN rule is perhaps the most unintuitive of the structural rules. In the
postcondition, any use of ~x~ can be replaced by ~v~ and due to the nature of the
assignment the assertion maintains its truth value. In the precondition, ~x~
could have any value, so by applying the substitution of ~v~ for ~x~ to the
precondition, we 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 the fixed-point nature of a while
statement. As ~while e do s~ is equivalent to ~if e then (s ; while e do s) else
skip~, we can use the IF, SEQ and SKIP rules to solve the recursion equation for
the precondition and postcondition of the while statement.

The only adaptation rule in the Hoare logic of WHILE is the rule of consequence,
CSQ. The rule of consequence 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 the rule of consequence redundant.

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

** 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 features of Agda 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. Take for instance fixed-length vectors. They can be defined by the
following snippet:

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

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

Whilst the value of parameters is constant in the return values of constructors,
they can vary across the arguments of constructors, even for the same type. One
example of this is the ~Assertion~ type given in [[*Hoare Logic Assertions]] later
in the report. 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

As the only constructor, ~refl~, requires that the two values are identical,
whenever there is a term of ~x ≡ y~ then ~x~ and ~y~ have the same value. One
useful elimination of propositional equality 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 that two values are equal, this function lets you use dependant
values for one type in place of the other.

*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~, we
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 the operations and properties of a type are well-defined,
but a good representation is unknown.

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

* Related Work

There exist a multitude of formal verification tools designed to describe either
the semantics of ISA instructions or prove the correctness of algorithms. This
section describes some of the most significant work in the field and how the
design of AMPSL improves upon it.

** Sail

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

Sail has many different backends available, including sequential emulators,
concurrency models and theorem-prover definitions. Further, there are tools to
automatically translate documents from the Arm Specification Language into Sail
[cite:@10.1145/3290384].

Despite the many advantages of Sail over other solutions, including the creation
of AMPSL, using Sail in this project is not suitable for a number of 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 the creation of 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 the memory model of
architectures. However, this work attempts to verify the functional correctness
of NTT, an algorithm with very little memory usage. The creation of 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
There are a number of existing tools for proving the 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 three distinct problems with using these tools to verify the functional
correctness of the pre-existing NTT implementation for Armv8-M:
- None of these tools accept assembly as an input language. This means they are
  unable to verify an existing assembly algorithm.
- None of these tools 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 the
  use of a verified compiler, of which none currently target Armv8-M.
- Final point?

The most similar tool to what this project is trying to achieve is a formal
verification tool by [cite:@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.

* Design of AMPSL and its Semantics

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

One downside of denotational semantics is that control flow for looping
constructs is fully evaluated. This is inefficient for loops that undergo many
iterations. This can be resolved by a syntax-directed Hoare logic for AMPSL.
Hoare logic derivations assign a precondition and a postcondition assertion to
each statement. These are chained together though a number of simple logical
implications.

** AMPSL Syntax
AMPSL is a language similar to the Armv8-M pseudocode specification language
written entirely in Agda. Unfortunately, ASL has a number of small features that
make it difficult to work with in Agda directly. AMPSL makes a number of small
changes to ASL to better facilitate this embedding, typically generalising
existing features of ASL.

*** 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 types of AMPSL. Most of
these have a direct analogue to ASL types. For example, ~bool~ is a Boolean,
~int~ mathematical integers, ~real~ is for mathematical real numbers and ~array~
constructs array types. Instead of an enumeration construct, AMPSL uses the ~fin
n~ type, representing a finite set of ~n~ elements. Similarly, structs are
represented by ~tuple~ types.

The most significant difference between ASL and AMPSL is the
representation of bitstrings. Instead of a bitstring type of ASL, AMPSL uses
arrays of Booleans. This lets AMPSL generalise a number of ASL operations and
makes AMPSL more expressive.

ASL specifies three different properties of types: equality comparisons, order
comparisons and arithmetic operations. Whilst using any of 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 has only two differences in types that satisfy these properties compared
to ASL. First, all array types have equality as long as the enumerated type also
has equality. This is a natural generalisation of the equality between types,
and allows for the AMPSL formulation of bitstrings as arrays of Booleans to have
equality. Secondly, finite sets also have ordering.  This change is primarily a
convenience feature for comparing finite representing a subset of integers. As
ASL has no ordering comparisons between enumerations, this causes no problems
for converting pseudocode programs into AMPSL.

The final interesting feature of the types in AMPSL is implicit coercion for
arithmetic. As ASL arithmetic is polymorphic for integers and reals, AMPSL needs
a function to decide the type of the result. By describing the output type as a
function on the input types, the same constructor can be used for all
combinations of numeric inputs.

*** AMPSL Expressions

#+name: AMPSL-literalType
#+caption: Mappings from AMPSL types into Agda types 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 part of the ~literalType~ function, given in
[[AMPSL-literalType]]. Most AMPSL literals accept the corresponding Agda type as a
value. For instance, ~bool~ literals are Agda Booleans, and ~array~ literals are
fixed-length Agda vectors of the corresponding underlying type. The only
exception to this rule is for ~real~ values. As Agda does not have a type
representing mathematical reals, integers are used instead. This is sufficient
as any real value occurring in the ASL of [cite:@arm/DDI0553B.s] is rational.

#+name: AMPSL-expr-prototypes
#+caption: Declarations of the Agda embeddings 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: Grammar of AMPSL. The formal Agda definition is in
#+caption: [[*AMPSL Syntax Definition]].
#+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 declarations of the Agda data types
corresponding to the AMPSL program elements. A summary of the grammar is in
[[AMPSL-grammar]] with the full definitions being given in [[*AMPSL Syntax
Definition]].  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 (like ~+~, ~*~, ~-~), and others are simple renamings
(like ~≟~ instead of ~==~ 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 carries fixed-length vectors listing
the AMPSL types of variables, a variable is referred to by its index into the
context. For example, a variable context \(\{x \mapsto \mathrm{int}, y \mapsto
\mathrm{real}\}\) is represented in AMPSL as the context ~int ∷ real ∷ []~. The
variable \(x\) is then represented by ~var 0F~ in AMPSL, 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. This method of
referring to variables by an index over a name is also commonly used in compiler
construction.

AMPSL expressions also add a number of useful constructs to ASL.  One such pair
is ~[_]~ and ~unbox~, which construct and destruct an array of length one
respectively. Others are ~fin~, which allows for arbitrary computations on
elements of finite sets, and ~asInt~, which converts a finite value into an
integer.

The final three AMPSL operators of note are ~merge~, ~slice~ and ~cut~. These
all perform operations on arrays, by either merging two together, taking out a
slice, or cutting out a slice. Unlike 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 of values
from an array ~xs~, such that the first element in ~slice xs i~ is in ~xs~ at
position ~i~. ~cut xs i~ returns the remainder of ~slice xs i~; the two ends of
~xs~ not in the slice, concatenated. Finally, ~merge xs ys i~ joins ~xs~ and
~ys~ to form a product-projection triple.

The ~Reference~ type is the name AMPSL gives to assignable expressions from 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:@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:@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 type of the
literal statement. The unary plus operation tells us that the literal is an Agda
integer. However, there are two AMPSL types with Agda integers for literal
values: ~int~ and ~real~.

How does Agda correctly infer the type? Recall that
multiplication is polymorphic in AMPSL, with the result type determined by
implicit coercion. Agda knows that the multiplication must return an ~int~, and
that the first argument is also an ~int~, so it can infer that the second
multiplicand is an integer literal.

Another pseudocode operation not yet described in AMPSL is integer slicing. Here
is an expression that slices a single bit from an integer, following the
procedure by [cite/t:@arm/DDI0553B.s §E1.3.3]:

#+begin_src agda2
getBit : ℕ → Expression Σ Γ int → Expression Σ Γ bit
getBit i x =
  inv (x - ((x >> suc i) << suc i) <? 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~.

*** 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.

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 two reasons.  The first is 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 other reason is that
including an ~if_then_~ statement makes the behaviour of a number of functions
that manipulate AMPSL code much easier to reason about.

The form of variable declarations is significantly different in AMPSL than it is
in ASL. As variables in AMPSL are accessed by index into the variable context
instead of by name, AMPSL variable declarations do not need a name. In addition,
Agda can often infer the type of a declared variable from the context in which
it is used, making type annotations unnecessary. The last and most significant
difference is that all variables in AMPSL must be initialised. This simplifies
the semantics of AMPSL greatly, and prevents 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 greatly complicate the denotational encoding of
AMPSL, by removing termination guarantees and requiring a monadic transformation
for the loops and exceptions, respectively.

Thankfully, these three structures are not a vital part of 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 elements from ~y~ into ~x~ if the corresponding
entry in ~mask~ is true:

# FIXME: compare with ASL
#+begin_src agda2
copyMasked :
  Statement Σ
    ( array t n
    ∷ array t n
    ∷ array bool n
    ∷ [])
copyMasked =
  for n (
    let i = var 0F in
    let x = var 1F in
    let y = var 2F in
    let mask = var 3F in

    if index mask i ≟ true
    then
        ,*index x i ≔ index y i
  )
#+end_src

This uses Agda functions ~index~ and ~*index~ to apply the appropriate slices,
casts and unboxing to extract an element from an array expression and reference,
respectively. One thing of note is the use of ~let...in~ to give variables
meaningful names. This is a stylistic choice that works well in this case.
Unfortunately, if the ~if_then_~ statement declared a new variable, these naming
variables would become useless, as the types would be different. For example
consider the following snippet:

# FIXME: compare with ASL
#+begin_src agda2
VPTAdvance : Statement State (beat ∷ [])
VPTAdvance =
  declare (fin div2 (tup (var 0F ∷ []))) (
  declare (elem 4 (! VPR-mask) (var 0F)) (
    let vptState = var 0F in
    let maskId = var 1F in
    let beat = var 2F in

    if ! vptState ≟ lit (true ∷ false ∷ false ∷ false ∷ [])
    then
      vptState ≔ lit (Vec.replicate false)
    else if inv (! vptState ≟ lit (Vec.replicate false))
    then (
      declare (lit false) (
        let i = var 0F in
        let vptState = var 1F in
        -- let mask = var 2F in
        let beat = var 3F in

        cons vptState (cons i nil) ≔ call (LSL-C 0) (! vptState ∷ []) ∙
        if ! i
        then
          ,*elem 4 VPR-P0 beat ≔ not (elem 4 (! VPR-P0) beat))) ∙
    if getBit 0 (asInt beat)
    then
      ,*elem 4 VPR-mask maskId ≔ ! vptState))
#+end_src

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 block of statements,
~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 a simple refactoring, so AMPSL does not lose any expressive
power over ASL.

AMPSL functions are more complex than procedures. A function consists of a pair
of an ~Expression~ and ~LocalStatement~. The statement has the function
arguments and the return value as local variables, where the return value is
initialised to the result of the expression. The return value of the function is
then the final value of the return variable.

**** Example AMPSL Functions and Procedures
As ~Procedure~ is almost an alias for ~Statement~, examples of 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:

# FIXME: compare with ASL
#+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 whatever is initially
assigned to the return variable is the result of calling the function. The
initial value of the return variable is a simple conditional statement, calling
~uint~ or ~sint~ on the first argument as appropriate. Many functions that are
easy to inline have this form.

The next example shows the ~uint~ function, which converts a bitstring into an
unsigned integer.

# FIXME: add pseudocode equivalent
#+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,
we iterate through the bits in turn, adding the place value of a bit into the
return value whenever that bit is true.

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

** AMPSL Semantics
This section starts with a brief discussion of how to model AMPSL types. This
addresses the burning question of how to model real numbers in Agda.  From this,
we discuss the denotational semantics of AMPSL, and how AMPSL program elements
can be converted into a number of different Agda function types. The section
ends with a presentation of a Hoare logic for AMPSL, allowing for efficient
syntax-directed proofs of 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. In this case, we have to be able
to find encodings of AMPSL types within Agda. [[AMPSL-type-models]] shows the full
encoding function. Most of the choices are fairly trivial: Agda Booleans for
~bool~, Agda vectors for ~array t n~ and the Agda finite set type ~Fin n~ for
the AMPSL type ~fin n~.

Tuples are the next simplest type, being encoded as an n-ary product. This is
the action of the ~⟦_⟧ₜₛ~ function in [[AMPSL-type-models]]. Unfortunately the Agda
standard library does not have a dependent n-ary product type. In any case, the
Agda type checker would not accept its usage in this case due to termination
checking, hence the manual inductive definition.

The other two AMPSL types are ~int~, ~real~. Whilst ~int~ could feasibly be
encoded by the Agda integer type, there is no useful Agda encoding for
mathematical real numbers. Because of this, both numeric types are represented
by abstract types with the appropriate properties. ~int~ is represented by a
discrete ordered commutative ring ℤ and ~real~ by a field ℝ. We also require
that there is a split ring monomorphism \(\mathtt{/1} : ℤ \to ℝ\) with
retraction \(\mathtt{⌊\_⌋} : ℝ \to ℤ\). \(\mathtt{⌊\_⌋}\) may not be a ring
homomorphism, but it must preserve \(\le\) ordering and satisfy the floor
property:

\[
\forall x y.\;x < y \mathtt{/1} \implies ⌊ x ⌋ < y
\]

~/1~ represents the usual embedding of integers into real numbers, by division
by one. ~⌊_⌋~ represents the floor function.

*** Denotational Semantics

#+name: AMPSL-denotational-prototypes
#+caption: Function prototypes for the denotational semantics of different AMPSL
#+caption: program elements. All of them become functions from the current
#+caption: variable context into some return value.
#+begin_src agda2
expr      : Expression Σ Γ t        → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ t ⟧ₜ
exprs     : All (Expression Σ Γ) ts → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ ts ⟧ₜₛ
ref       : Reference Σ Γ t         → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ t ⟧ₜ
locRef    : LocalReference Σ Γ t    → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ t ⟧ₜ
stmt      : Statement Σ Γ           → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ
locStmt   : LocalStatement Σ Γ      → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Γ ⟧ₜₛ
fun       : Function Σ Γ t          → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ t ⟧ₜ
proc      : Procedure Σ Γ           → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Σ ⟧ₜₛ
#+end_src

The denotational semantics has to represent the different AMPSL program elements
as mathematical objects. In this case, due to careful design of AMPSL's syntax,
each of the elements is represented by a total function.
[[AMPSL-denotational-prototypes]] shows the prototypes of the different semantic
interpretation functions, and the full definition is in [[*AMPSL Denotational
Semantics]]. Each function accepts the current variable context as an argument.
Because the variable contexts are an ordered sequence of values of different
types, they can be encoded in the same way as tuples.

**** Expression Semantics

The semantic representation of an expression converts the current variable
context into a value with the same type as the expression. Most cases are pretty
simple. For example, addition is the sum of the values of the two subexpressions
computed recursively. One of the more interesting cases are global and local
variables, albeit this is only a lookup in the variable context for the current
value. This lookup is guaranteed to be safe due to variables being a lookup into
the current context. Despite both being a subsets of the ~Expression~ type,
~Reference~ and ~LocalReference~ require their own functions to satisfy the
demands of the termination checker.

One significant omission from this definition is the checking of evaluation
order. Due to the design choices that AMPSL functions cannot modify global state,
and that no AMPSL expression can modify state, expressions have the same value
no matter the order of evaluation for sub-expressions. This is also reflected in
the type of the denotational representation of expressions. It can only possibly
return a value and not a modified version of the state.

**** Assignment Semantics
#+name: AMPSL-denotational-assign-prototypes
#+caption: Function prototypes for the ~assign~ and ~locAssign~ helper
#+caption: functions. The arguments are the reference, new value, original
#+caption: variable context and the context to update. The original context is
#+caption: needed to evaluate expressions within the reference.
#+begin_src agda2
assign    : Reference Σ Γ t      → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ
locAssign : LocalReference Σ Γ t → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Γ ⟧ₜₛ
#+end_src

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

We will consider how to update each of the three types of references in turn,
which is the action performed by helper functions ~assign~ and ~locAssign~, the
signatures of which 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~ is the same as ~ref ≔ unbox v~.

The final type of reference to consider are the projection reference operations.
Assigning into one projection of a reference means that the other part remains
unchanged. Consider the assignment ~head r ≔ v~ as an example. This is
equivalent to ~r ≔ cons v (tail r)~, which makes it clear that the second
projection remains constant. The second projection must be computed using the
original variable context, which is achieved by only updating the context for a
leaf reference.

This interpretation of slice as a projection reference type is a large part of
the 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 encoding of values.  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
Compared to assignment, the semantics of other statements are trivial to
compute. Skip statements map to the identity function and sequencing is function
composition, reflecting that they do nothing and compose statements together
respectively. As expressions cannot modify state, ~if_then_else_~ and ~if_then_~
statements become simple---evaluate the condition and both branches on the input
state, and return the branch depending on the value of the condition. Local
variable declarations are also quite simple. The initial value is computed and
added to the variable context. After evaluating the subsequent statement, the
final value of the new variable is stripped away from the context.

The only looping construct in AMPSL is the ~for~ loop. Because it performs a
fixed number of iterations, it too has a straight-forward denotational
semantics.  This is because it is effectively a fixed number of ~declare~
statements all sequenced together. This is also one of the primary reasons why
the denotational semantics can have poor computational performance; every
iteration of the ~for~ loop must be evaluated individually.

~stmt~ and ~locStmt~ return the full context and only the local variables
respectively. This is because only ~Statement~ can include ~Reference~ which can
reference global state. On the other hand, ~LocalReference~ used by
~LocalStatement~ can only refer to, and hence modify, local state.

**** Function and Procedure Semantics
Finally there are ~proc~ and ~fun~ for denoting procedures and functions. ~proc~
returns the global state only. ~Procedure~ is a thin wrapper around ~Statement~,
which modifies both local and global state. However, the local state is lost
when leaving a procedure, hence ~proc~ only returns the global part.

~fun~ behaves a lot like a ~declare~ statement. It initialises the return
variable to the given expression, then evaluates the ~LocalStatement~ body.
Unlike ~declare~, which discards the added variable upon exiting the statement,
~fun~ instead returns the value of that variable. As ~LocalStatement~ cannot
modify global state, and the other local variables are lost upon exiting the
function, only this one return value is necessary.

*** Hoare Logic Semantics
The final form of semantics specified for AMPSL is a form of Hoare logic. Unlike
the denotational semantics, which must perform a full computation, the Hoare
logic is syntax-directed; loops only require a single proof. This section starts
by explaining how a 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 form of correctness triples for AMPSL.

**** Converting ~Expression~ into ~Term~
As discussed in [[*Hoare Logic]], a simple language such as WHILE can use
expressions as terms in assertions directly. The only modification required is
the addition of auxiliary variables. AMPSL is not as simple a language as WHILE,
thanks to the presence of function calls in expressions. Whilst function calls
do not prevent converting expressions into terms, some care must be taken. In
particular, this conversion is only possible due to the pure nature of AMPSL
functions; it would not be possible if functions modified global variables. The
full definition of ~Term~ and its semantics are given in [[*AMPSL Hoare Logic
Definitions]].

First, a demonstration on why function calls need special care in Hoare logic.
We will work in an environment with a single Boolean-valued global variable.
Consider the following 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 ∙
    let x = var 1F in
    let ret = var 0F in
    if state 0F
      then ret ≔ lit 1ℤ + x
  end
#+end_src

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

The simplest conversion is to keep the function call as-is, and simply
recursively convert ~x~ into a term. This would result in a term ~e′ = call f [
x′ ]~, using ~′~ to indicate 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 of writing ~t~ inside of ~f~. This embedding is not
sufficient.

A working solution comes from the insight that a ~Function~ in AMPSL can only
read from global variables, and never write to them. Instead of thinking of ~f~
as a function with a set of global variables and a list of arguments, you can
consider ~f~ to be a function with two sets of arguments. In an ~Expression~,
the first set of arguments always corresponds exactly with the global variables,
so is elided. We can then define an embedding function ~↓_~, such that ~↓ e =
call f [ state 0F ] [ ↓ x ]~, and all the other expression forms as expected.
This makes the elided arguments to ~f~ explicit.

Doing a substitution on ~↓ e~ is now simple: perform the substitution on both
sets of arguments recursively, and leave ~f~ unchanged. As the first set of
arguments correspond exactly to the global variables in ~f~, the substitution
into those arguments appears like a substitution into ~f~ itself.

The last major consideration of this embedding is how to encode its semantics.
To be able to perform logical implications within Hoare logic, it is necessary
to have a semantic interpretation for assertions and thus terms. Going back to
~↓ e~, we already have a denotational semantics for ~f~. Hence we only need to
consider the global and local variables we pass to ~f~ to get the value. We
simply pass ~f~ the values of the global and local argument lists for the values
of the global and local arguments respectively. Thus ~↓ e~ is a valid conversion
from ~Expression~ to ~Term~.

The only other difference between ~Expression~ and ~Term~ is the use of
auxiliary variables within Hoare logic terms. 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 the type definition of
~Term~.

**** Hoare Logic Assertions
An important part of Hoare logic is the assertion language used within the
correctness triples. The Hoare logic for AMPSL uses a first-order logic, which
allows for the easy proof of many logical implications at the expense of not
being complete over the full set of state properties. The full definition and
semantics of the ~Assertion~ type are in [[*AMPSL Hoare Logic Definitions]].

The ~Assertion~ type has the usual set of Boolean connectives: ~true~, ~false~,
~_∧_~, ~_∨_~, ~¬_~ and ~_→_~. When compared to the ~fin~ AMPSL expression, which
performs arbitrary manipulations on finite sets, using this fixed set of
connectives may appear restrictive. The primary reason in favour of a fixed set
of connectives is that the properties are well-defined. This makes it possible
to prove properties about the ~Assertion~ type within proofs that would not be
possible if assertions could use arbitrary connectives.

Another constructor of ~Assertion~ is ~pred~, which accepts an arbitrary
Boolean-valued ~Term~. This is the only way to test properties of the current
program state within assertions. As nearly all types have equality comparisons,
~pred~ can encode equality and inequality constraints on values. Furthermore, as
~Term~ embeds ~Expression~, many complex computations can be performed within
~pred~. To allow equality between two terms of any type, there is an ~equal~
function to construct an appropriate assertion.

The final two constructors of ~Assertion~ provide first-order quantification
over auxiliary variables. ~all~ provides universal quantification and ~some~
provides existential quantification.

Semantically, an assertion is a predicate on the current state of execution. For
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: the unit type for ~true~, the empty type for ~false~, product
types for ~_∧_~, sum types for ~_∨_~, function types for ~_→_~ and the negation
type for ~¬_~.

Quantifier assertions are also quite easy to give a semantic representation. For
universal quantification, you have a function taking values of the type of the
auxiliary variable, which returns the encoding of the inner assertion with
auxiliary context extended by this value. For existential quantification, you
instead have a dependent pair of a value with the auxiliary variable type, and
semantic encoding of the inner assertion.

The final ~Assertion~ form to consider is ~pred~. This first evaluates the
associated Boolean term. If true, the semantics returns the unit type.
Otherwise, it returns the empty type.

Fortunately, all equalities and inequalities between AMPSL values are decidable,
either by construction of the type for Booleans and finite sets, or by
specification for integers and real numbers. This allows the user to extract
Agda terms for equalities given only knowledge of whether terms are equal.

**** Correctness Triples for AMPSL
In the traditional presentation of Hoare logic ([[*Hoare Logic]]), there are two
types of rule; structural rules based on program syntax and adaptation rules to
modify preconditions and postconditions. The Hoare logic for AMPSL unifies the
two forms of rules, eliminating the need to choose which type of rule to use
next. This allows for purely syntax-directed proofs for any choice of
precondition and postcondition.

#+name: 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

We 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 is as you would expect and 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~. In fact, the ~if-else~ rule
is identical to the corresponding Hoare logic rule from WHILE, and ~if~ only
differs by directly substituting in a ~skip~ statement for the negative branch.

The final trivial rule is ~assign~. Like the ~skip~ rule, the ~assign~ rule
combines the structural and adaptation rules of WHILE into a single Hoare logic
rule for 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.

The ~declare~ rule is the simplest of the three remaining. The goal is to
describe a necessary triple on ~s~ such that ~HoareTriple P Q (declare e s)~ is
a valid correctness triple. First, note that ~P~ and ~Q~ have type ~Assertion Σ
Γ Δ~, whilst ~s~ has type ~Statement Σ (t ∷ Γ)~ due to the declaration
introducing a new variable. To be able to use ~P~ and ~Q~, they have to be
weakened to the type ~Assertion Σ (t ∷ Γ) Δ~, achieved by calling ~Var.weaken
0F~. We will denote the weakened forms ~P′~ and ~Q′~ for brevity. The recursive
triple we have is ~HoareTriple P′ Q′ s~. However, this does not constrain the
new variable. Thus we assert that the new variable ~var 0F~ is equal to the
initial value ~e~.  However, ~e~ has type ~Expression Σ Γ~ and we need a ~Term Σ
(t ∷ Γ) Δ~. Hence we must instead use ~Term.Var.weaken 0F (↓ e)~, denoted ~e′~ ,
which converts ~e~ to a term and introduces the new variable. This finally gives
us the triple we need: ~HoareTriple (P′ ∧ equal (var 0F) e′) Q′ s~.

I will go into less detail whilst discussing ~invoke~ and ~for~, due to an even
greater level of complexity. The ~for~ rule is the simpler case, so I will start
there. The form of the ~for~ rule was inspired from the WHILE rule for a ~while~
loop, but specialised to a form with a fixed number of iterations.

Given a ~for n s~ statement, we first choose a loop invariant ~I : Assertion Σ Γ
(fin (suc n) ∷ Δ)~. The additional auxiliary variable indicates the number of
complete iterations of the loop, from \(0\) to \(n\). We will use ~I(x)~ to
denote the assertion ~I~ with the additional auxiliary variable replaced with
term ~x~, and make weakening variable contexts implicit. We require that ~P ⊆
I(0)~ and ~I(n) ⊆ Q~ to ensure that the precondition and postcondition are an
adaptation of the loop invariant. The final part to consider is the correctness
triple for ~s~. We add in a new auxiliary variable representing the value of the
loop variable. This is necessary to ensure the current iteration number is
preserved between the precondition and postcondition, as the loop variable
itself can be modified by ~s~. We then require that the following triple holds:
~HoareTriple (I(meta 0F) ∧ equal (meta 0F) (var 0F)) I(1+ meta 0F) s~. This
ensures that ~I~ remains true across the loop iteration, for each possible value
of the loop variable.

Notice that unlike the denotational semantics, which would explicitly execute
each iteration of a loop, the Hoare logic instead requires only a single proof
term for all iterations of the loop. This is one of the primary benefits of
using Hoare logic over the denotational semantics; it has a much lower
computational cost.

The final Hoare logic rule for AMPSL is ~invoke~. Procedure invocation is tricky
in AMPSL's Hoare logic due to the changing local variable scope in the procedure
body. Of particular note, any local variables in the precondition and
postcondition for a procedure invocation cannot be accessed nor modified by the
procedure body. This is the inspiration for the form of the ~invoke~ rule.

To construct ~HoareTriple P Q (invoke (s ∙end) es)~, we first consider the form
~P~ and ~Q~ will take in a correctness triple for ~s~. Note that local variables
in ~P~ and ~Q~ are immutable within ~s~, due to the changing local variable
scope. Also note that the local variables cannot be accessed using ~var~; ~P~
and ~Q~ have type ~Assertion Σ Γ Δ~, but ~s~ has type ~Statement Σ Γ′~ for some
context ~Γ′~ independent of ~Γ~. As the original local variables are immutable
during the invocation, we can replace them with auxiliary variables, by
assigning a new auxiliary variable for each one. Within ~P~ and ~Q~, we then
replace all ~var x~ with ~meta x~ to reflect that the local variables have been
moved to auxiliary variables. This is the action performed by the ~varsToMetas~
function. Finally, we have to ensure that the local variables within the
procedure body are initially set to the invocation arguments. Like ~P~ and ~Q~,
the local variables in ~es~ have to be replaced with the corresponding auxiliary
variables. This substitution is done by ~termVarsToMetas~.

* 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 example 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. If there
#+caption: is a correctness triple \(\{P\}\;\texttt{s}\;\{Q\}\) then for any
#+caption: variable contexts σ, γ and δ, a proof that \(P\) holds initially
#+caption: implies that \(Q\) holds after executing \texttt{s} on the global and
#+caption: local variable contexts.
#+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.

#+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

Some cases in this inductive proof are trivial: the premise of the ~skip~ Hoare
logic rule is exactly the proof statement we need, and the ~seq~ rule can be
satisfied by composing the results of the inductive hypothesis on the two
premises. 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. We 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,
you can construct the definition of a full homomorphism.

#+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 "punches
in" the new variable, wrapped in a type cast to satisfy Agda's dependant 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.

#+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 : ∀ i → ⟦ t ⟧ₜ → RecBuilder⇒ (Term.Var.weakenBuilder {Σ = Σ} {Γ = Γ} {Δ = Δ} {t = t} i)
weakenBuilder {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

Returning to the local variable weakening example, the relevant construction for
proof is shown in [[term-weakening-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 we 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 "punched in" 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 a bunch of boilerplate, 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 to any useful degree in propositional equality. Instead,
I give type equalities, which are pairs of functions from one type to the other.

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.

*** Soundness of ~declare~, ~for~ and ~invoke~
Referring back to [[AMPSL-Hoare-logic]] for the Hoare logic definitions, we can now
prove soundness for the other rules. The ~declare~ rule is straight forward.
First, 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 we inductively apply soundness, to obtain a proof that the
weakened post-condition 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, we
can obtain a proof that ~I(0)~ holds from the argument, and convert a proof of
~I(m)~ to a proof of the post-condition. All that remains is a proof that the
loop preserves the invariant.

#+name: foldl-prototype
#+caption: The function signature for proving arbitrary properties about left-folding a vector.
#+begin_src agda2
foldl⁺ : ∀ {a b c} {A : Set a} (B : ℕ → Set b) {m} →
         (P : ∀ {i : Fin (suc m)} → B (Fin.toℕ i) → Set c) →
         (f : ∀ {n} → B n → A → B (suc n)) →
         (y : B 0) →
         (xs : Vec A m) →
         (∀ {i} {x} →
          P {Fin.inject₁ i} x →
          P {suc i}
            (subst B (Finₚ.toℕ-inject₁ (suc i))
                     (f x (Vec.lookup xs i)))) →
         P {0F} y →
         P {Fin.fromℕ m}
           (subst B (sym (Finₚ.toℕ-fromℕ m))
                    (Vec.foldl B f y xs))
#+end_src

To do this, I first had to prove a much more general statement about the action
of left-fold on Agda's ~Vec~ type, the prototype of which is given in
[[foldl-prototype]]. In summary, given a proof of ~P~ for the base case, and a proof
that each step of the fold preserves ~P~, then it shows that ~P~ holds in for
the entire fold.

This means that the remainder of the proof of soundness of ~for~ is a proof that
each iteration maintains the invariant. Using a number of lemma asserting that
various manipulations of assertions are homomorphisms, as well as a few
type-safe substitutions and a recursive proof of soundness for the iterated
statement, the final proof of soundness for ~for~ totals around 220 lines of
Agda.

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 any predicate
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, due to the ~Set~ type in Agda not being a data 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, we need to give two
subproofs: ~P ⊢ s ⊢ R~ and ~R ⊢ s₁ ⊢ Q~. As input, we have 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, we
can now give this formulation for the correctness of AMPSL's Hoare logic, 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₁~, we 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 chapter 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~ 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.

Most vector instructions for the Armv8.1-M architecture are executed beatwise. A
vector register is a 128-bit value with four 32-bit lanes. Beatwise execution
allows some lanes to anticipate future vector instructions and execute them
before a previous instruction has finished on other lanes [cite:@arm/DDI0553B.s
§B5.4]. There are additional conditions on which instructions can be
anticipated, essentially boiling down to any order that has the same result as
executing the instructions linearly.

# FIXME: figure padding?
#+name: ExecBeats-impl
#+caption: A side-by-side comparison of a simplified form of the ~ExecBeats~
#+caption: function from [cite:@arm/DDI0553B.s §E2.1.121] versus the model used
#+caption: in AMPSL.
#+begin_figure
\begin{subfigure}[b]{0.45\textwidth}
\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}
\caption{Arm pseudocode}
\label{ExecBeats-impl-Arm}
\end{subfigure}
\hfill
\begin{subfigure}[b]{0.45\textwidth}
\begin{minted}{agda}
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{minted}
\caption{AMPSL model}
\label{ExecBeats-impl-AMPSL}
\end{subfigure}
#+end_figure

The choice of which instructions beats to schedule is in the ~ExecBeats~
pseudocode function [cite:@arm/DDI0553B.s §E2.1.121]. Compared with my model,
shown side-by-side in [[ExecBeats-impl]], I reduce 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.

# FIXME: side by side code?
#+name: vqmlrdh
#+caption: Definition of the ~VQMLRDH~ instruction.
#+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 elmtMast = head (tail (var 3F)) in
    let curBeat = head (var 3F) in
    -- let op₁ = var 2F in
    -- let result = var 1F 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

# FIXME: side by side code?
#+name: vmla
#+caption: Definition of the ~VMLA~ instruction.
#+begin_src agda2
vmla : Instr.VMLA → Procedure State []
vmla =
  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 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

The Barrett reduction implementation by
[cite/t:@10.46586/tches.v2022.i1.482-505] requires two instructions: ~VQRDMULH~
and ~VMLA~. The ASL and AMPSL definitions are given in [[vqmlrdh]] and [[vmla]]
respectively. 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.

Despite this example being relatively small, the poor performance of AMPSL's
denotational semantics 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.

*** Proving Reusable Results
One fundamental principle of programming is DRY: don't repeat yourself. This is
achieved by using functions and procedures to abstract out common behaviours.
Similarly, to fully utilise the power of Hoare logic, an abstract reusable
correctness triple should be given for the behaviour of invoking functions.

I attempted to do this for the ~copyMasked~ procedure given in [[*Example AMPSL
Statements]], the type of which is given below:

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

Explained briefly, whenever the mask is all true (~I~), the procedure effectively
reduces to a regular assignment rule in for AMPSL's Hoare logic. Expanding the
proof derivation results in the following incomplete Agda term:

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

The missing Agda expressions correspond to a choice of loop invariant and then
four logical implications: entering the loop; leaving the loop; showing the
assignment preserves the loop invariant; and showing that skipping the
assignment preserves the loop invariant.

Whilst none of those steps are particularly tricky, they each require the proofs
of many trivial-on-paper lemmata. Due to the time constraints of the project, I
have been unable to complete these proofs.

* 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 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.

#+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 second ensures that the Barrett reduction of a positive value is remains
positive. 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.

* Summary and Conclusions

In this work, I might vital progress into proving 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, 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 more 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 live up
to the task. Currently, to have any utility, a huge push needs to be made to
complete proofs of many of the missing lemmata.

** 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 for the platform.

Another alternative, particularly for working on pre-existing, hand-written
assembly routines, is to model the Armv8-M semantics using Sail. Unlike AMPSL,
Sail will 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

* AMPSL Syntax Definition

#+begin_src agda2
data Expression Σ Γ where
  lit           : literalType t → Expression Σ Γ t
  state         : ∀ i → Expression Σ Γ (lookup Σ i)
  var           : ∀ i → Expression Σ Γ (lookup Γ i)
  _≟_           : ⦃ HasEquality t ⦄ → Expression Σ Γ t → Expression Σ Γ t → Expression Σ Γ bool
  _<?_          : ⦃ Ordered t ⦄ → Expression Σ Γ t → Expression Σ Γ t → Expression Σ Γ bool
  inv           : Expression Σ Γ bool → Expression Σ Γ bool
  _&&_          : Expression Σ Γ bool → Expression Σ Γ bool → Expression Σ Γ bool
  _||_          : Expression Σ Γ bool → Expression Σ Γ bool → Expression Σ Γ bool
  not           : Expression Σ Γ (bits n) → Expression Σ Γ (bits n)
  _and_         : Expression Σ Γ (bits n) → Expression Σ Γ (bits n) → Expression Σ Γ (bits n)
  _or_          : Expression Σ Γ (bits n) → Expression Σ Γ (bits n) → Expression Σ Γ (bits n)
  [_]           : Expression Σ Γ t → Expression Σ Γ (array t 1)
  unbox         : Expression Σ Γ (array t 1) → Expression Σ Γ t
  merge         : Expression Σ Γ (array t m) → Expression Σ Γ (array t n) → Expression Σ Γ (fin (suc n)) → Expression Σ Γ (array t (n ℕ.+ m))
  slice         : Expression Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc n)) → Expression Σ Γ (array t m)
  cut           : Expression Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc n)) → Expression Σ Γ (array t n)
  cast          : .(eq : m ≡ n) → Expression Σ Γ (array t m) → Expression Σ Γ (array t n)
  -_            : ⦃ IsNumeric t ⦄ → Expression Σ Γ t → Expression Σ Γ t
  _+_           : ⦃ isNum₁ : IsNumeric t₁ ⦄ → ⦃ isNum₂ : IsNumeric t₂ ⦄ → Expression Σ Γ t₁ → Expression Σ Γ t₂ → Expression Σ Γ (isNum₁ +ᵗ isNum₂)
  _*_           : ⦃ isNum₁ : IsNumeric t₁ ⦄ → ⦃ isNum₂ : IsNumeric t₂ ⦄ → Expression Σ Γ t₁ → Expression Σ Γ t₂ → Expression Σ Γ (isNum₁ +ᵗ isNum₂)
  _^_           : ⦃ IsNumeric t ⦄ → Expression Σ Γ t → ℕ → Expression Σ Γ t
  _>>_          : Expression Σ Γ int → (n : ℕ) → Expression Σ Γ int
  rnd           : Expression Σ Γ real → Expression Σ Γ int
  fin           : ∀ {ms} (f : literalTypes (map fin ms) → Fin n) → Expression Σ Γ (tuple {n = k} (map fin ms)) → Expression Σ Γ (fin n)
  asInt         : Expression Σ Γ (fin n) → Expression Σ Γ int
  nil           : Expression Σ Γ (tuple [])
  cons          : Expression Σ Γ t → Expression Σ Γ (tuple ts) → Expression Σ Γ (tuple (t ∷ ts))
  head          : Expression Σ Γ (tuple (t ∷ ts)) → Expression Σ Γ t
  tail          : Expression Σ Γ (tuple (t ∷ ts)) → Expression Σ Γ (tuple ts)
  call          : (f : Function Σ Δ t) → All (Expression Σ Γ) Δ → Expression Σ Γ t
  if_then_else_ : Expression Σ Γ bool → Expression Σ Γ t → Expression Σ Γ t → Expression Σ Γ t

data Reference Σ Γ where
  state : ∀ i → Reference Σ Γ (lookup Σ i)
  var   : ∀ i → Reference Σ Γ (lookup Γ i)
  [_]   : Reference Σ Γ t → Reference Σ Γ (array t 1)
  unbox : Reference Σ Γ (array t 1) → Reference Σ Γ t
  merge : Reference Σ Γ (array t m) → Reference Σ Γ (array t n) → Expression Σ Γ (fin (suc n)) → Reference Σ Γ (array t (n ℕ.+ m))
  slice : Reference Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc n)) → Reference Σ Γ (array t m)
  cut   : Reference Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc n)) → Reference Σ Γ (array t n)
  cast  : .(eq : m ≡ n) → Reference Σ Γ (array t m) → Reference Σ Γ (array t n)
  nil   : Reference Σ Γ (tuple [])
  cons  : Reference Σ Γ t → Reference Σ Γ (tuple ts) → Reference Σ Γ (tuple (t ∷ ts))
  head  : Reference Σ Γ (tuple (t ∷ ts)) → Reference Σ Γ t
  tail  : Reference Σ Γ (tuple (t ∷ ts)) → Reference Σ Γ (tuple ts)

data LocalReference Σ Γ where
  var   : ∀ i → LocalReference Σ Γ (lookup Γ i)
  [_]   : LocalReference Σ Γ t → LocalReference Σ Γ (array t 1)
  unbox : LocalReference Σ Γ (array t 1) → LocalReference Σ Γ t
  merge : LocalReference Σ Γ (array t m) → LocalReference Σ Γ (array t n) → Expression Σ Γ (fin (suc n)) → LocalReference Σ Γ (array t (n ℕ.+ m))
  slice : LocalReference Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc n)) → LocalReference Σ Γ (array t m)
  cut   : LocalReference Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc n)) → LocalReference Σ Γ (array t n)
  cast  : .(eq : m ≡ n) → LocalReference Σ Γ (array t m) → LocalReference Σ Γ (array t n)
  nil   : LocalReference Σ Γ (tuple [])
  cons  : LocalReference Σ Γ t → LocalReference Σ Γ (tuple ts) → LocalReference Σ Γ (tuple (t ∷ ts))
  head  : LocalReference Σ Γ (tuple (t ∷ ts)) → LocalReference Σ Γ t
  tail  : LocalReference Σ Γ (tuple (t ∷ ts)) → LocalReference Σ Γ (tuple ts)

data Statement Σ Γ where
  _∙_           : Statement Σ Γ → Statement Σ Γ → Statement Σ Γ
  skip          : Statement Σ Γ
  _≔_           : Reference Σ Γ t → Expression Σ Γ t → Statement Σ Γ
  declare       : Expression Σ Γ t → Statement Σ (t ∷ Γ) → Statement Σ Γ
  invoke        : (f : Procedure Σ Δ) → All (Expression Σ Γ) Δ → Statement Σ Γ
  if_then_      : Expression Σ Γ bool → Statement Σ Γ → Statement Σ Γ
  if_then_else_ : Expression Σ Γ bool → Statement Σ Γ → Statement Σ Γ → Statement Σ Γ
  for           : ∀ n → Statement Σ (fin n ∷ Γ) → Statement Σ Γ

data LocalStatement Σ Γ where
  _∙_           : LocalStatement Σ Γ → LocalStatement Σ Γ → LocalStatement Σ Γ
  skip          : LocalStatement Σ Γ
  _≔_           : LocalReference Σ Γ t → Expression Σ Γ t → LocalStatement Σ Γ
  declare       : Expression Σ Γ t → LocalStatement Σ (t ∷ Γ) → LocalStatement Σ Γ
  if_then_      : Expression Σ Γ bool → LocalStatement Σ Γ → LocalStatement Σ Γ
  if_then_else_ : Expression Σ Γ bool → LocalStatement Σ Γ → LocalStatement Σ Γ → LocalStatement Σ Γ
  for           : ∀ n → LocalStatement Σ (fin n ∷ Γ) → LocalStatement Σ Γ

data Function Σ Γ ret where
  init_∙_end : Expression Σ Γ ret → LocalStatement Σ (ret ∷ Γ) → Function Σ Γ ret

data Procedure Σ Γ where
  _∙end : Statement Σ Γ → Procedure Σ Γ
#+end_src

* AMPSL Denotational Semantics

#+begin_src agda2
expr (lit {t = t} x)        = const (Κ[ t ] x)
expr {Σ = Σ} (state i)      = fetch i Σ ∘ proj₁
expr {Γ = Γ} (var i)        = fetch i Γ ∘ proj₂
expr (e ≟ e₁)               = lift ∘ does ∘ uncurry ≈-dec ∘ < expr e , expr e₁ >
expr (e <? e₁)              = lift ∘ does ∘ uncurry <-dec ∘ < expr e , expr e₁ >
expr (inv e)                = lift ∘ Bool.not ∘ lower ∘ expr e
expr (e && e₁)              = lift ∘ uncurry (Bool._∧_ on lower) ∘ < expr e , expr e₁ >
expr (e || e₁)              = lift ∘ uncurry (Bool._∨_ on lower) ∘ < expr e , expr e₁ >
expr (not e)                = map (lift ∘ Bool.not ∘ lower) ∘ expr e
expr (e and e₁)             = uncurry (zipWith (lift ∘₂ Bool._∧_ on lower)) ∘ < expr e , expr e₁ >
expr (e or e₁)              = uncurry (zipWith (lift ∘₂ Bool._∨_ on lower)) ∘ < expr e , expr e₁ >
expr [ e ]                  = (_∷ []) ∘ expr e
expr (unbox e)              = Vec.head ∘ expr e
expr (merge e e₁ e₂)        = uncurry (uncurry mergeVec) ∘ < < expr e , expr e₁ > , lower ∘ expr e₂ >
expr (slice e e₁)           = uncurry sliceVec ∘ < expr e , lower ∘ expr e₁ >
expr (cut e e₁)             = uncurry cutVec ∘ < expr e , lower ∘ expr e₁ >
expr (cast eq e)            = castVec eq ∘ expr e
expr (- e)                  = neg ∘ expr e
expr (e + e₁)               = uncurry add ∘ < expr e , expr e₁ >
expr (e * e₁)               = uncurry mul ∘ < expr e , expr e₁ >
expr (e ^ x)                = flip pow x ∘ expr e
expr (e >> n)               = lift ∘ flip (shift 2≉0) n ∘ lower ∘ expr e
expr (rnd e)                = lift ∘ ⌊_⌋ ∘ lower ∘ expr e
expr (fin {ms = ms} f e)    = lift ∘ f ∘ lowerFin ms ∘ expr e
expr (asInt e)              = lift ∘ 𝕀⇒ℤ ∘ 𝕀.+_ ∘ Fin.toℕ ∘ lower ∘ expr e
expr nil                    = const _
expr (cons {ts = ts} e e₁)  = uncurry (cons′ ts) ∘ < expr e , expr e₁ >
expr (head {ts = ts} e)     = head′ ts ∘ expr e
expr (tail {ts = ts} e)     = tail′ ts ∘ expr e
expr (call f es)            = fun f ∘ < proj₁ , exprs es >
expr (if e then e₁ else e₂) = uncurry (uncurry Bool.if_then_else_) ∘ < < lower ∘ expr e , expr e₁ > , expr e₂ >

exprs []            = const _
exprs (e ∷ [])      = expr e
exprs (e ∷ e₁ ∷ es) = < expr e , exprs (e₁ ∷ es) >

ref {Σ = Σ} (state i)     = fetch i Σ ∘ proj₁
ref {Γ = Γ} (var i)       = fetch i Γ ∘ proj₂
ref [ r ]                 = (_∷ []) ∘ ref r
ref (unbox r)             = Vec.head ∘ ref r
ref (merge r r₁ e)        = uncurry (uncurry mergeVec) ∘ < < ref r , ref r₁ > , lower ∘ expr e >
ref (slice r e)           = uncurry sliceVec ∘ < ref r , lower ∘ expr e >
ref (cut r e)             = uncurry cutVec ∘ < ref r , lower ∘ expr e >
ref (cast eq r)           = castVec eq ∘ ref r
ref nil                   = const _
ref (cons {ts = ts} r r₁) = uncurry (cons′ ts) ∘ < ref r , ref r₁ >
ref (head {ts = ts} r)    = head′ ts ∘ ref r
ref (tail {ts = ts} r)    = tail′ ts ∘ ref r

locRef {Γ = Γ} (var i)       = fetch i Γ ∘ proj₂
locRef [ r ]                 = (_∷ []) ∘ locRef r
locRef (unbox r)             = Vec.head ∘ locRef r
locRef (merge r r₁ e)        = uncurry (uncurry mergeVec) ∘ < < locRef r , locRef r₁ > , lower ∘ expr e >
locRef (slice r e)           = uncurry sliceVec ∘ < locRef r , lower ∘ expr e >
locRef (cut r e)             = uncurry cutVec ∘ < locRef r , lower ∘ expr e >
locRef (cast eq r)           = castVec eq ∘ locRef r
locRef nil                   = const _
locRef (cons {ts = ts} r r₁) = uncurry (cons′ ts) ∘ < locRef r , locRef r₁ >
locRef (head {ts = ts} r)    = head′ ts ∘ locRef r
locRef (tail {ts = ts} r)    = tail′ ts ∘ locRef r

assign {Σ = Σ} (state i)     val σ,γ = < updateAt i Σ val ∘ proj₁ , proj₂ >
assign {Γ = Γ} (var i)       val σ,γ = < proj₁ , updateAt i Γ val ∘ proj₂ >
assign [ r ]                 val σ,γ = assign r (Vec.head val) σ,γ
assign (unbox r)             val σ,γ = assign r (val ∷ []) σ,γ
assign (merge r r₁ e)        val σ,γ = assign r₁ (cutVec val (lower (expr e σ,γ))) σ,γ ∘ assign r (sliceVec val (lower (expr e σ,γ))) σ,γ
assign (slice r e)           val σ,γ = assign r (mergeVec val (cutVec (ref r σ,γ) (lower (expr e σ,γ))) (lower (expr e σ,γ))) σ,γ
assign (cut r e)             val σ,γ = assign r (mergeVec (sliceVec (ref r σ,γ) (lower (expr e σ,γ))) val (lower (expr e σ,γ))) σ,γ
assign (cast eq r)           val σ,γ = assign r (castVec (sym eq) val) σ,γ
assign nil                   val σ,γ = id
assign (cons {ts = ts} r r₁) val σ,γ = assign r₁ (tail′ ts val) σ,γ ∘ assign r (head′ ts val) σ,γ
assign (head {ts = ts} r)    val σ,γ = assign r (cons′ ts val (ref (tail r) σ,γ)) σ,γ
assign (tail {ts = ts} r)    val σ,γ = assign r (cons′ ts (ref (head r) σ,γ) val) σ,γ

locAssign {Γ = Γ} (var i)       val σ,γ = updateAt i Γ val
locAssign [ r ]                 val σ,γ = locAssign r (Vec.head val) σ,γ
locAssign (unbox r)             val σ,γ = locAssign r (val ∷ []) σ,γ
locAssign (merge r r₁ e)        val σ,γ = locAssign r₁ (cutVec val (lower (expr e σ,γ))) σ,γ ∘ locAssign r (sliceVec val (lower (expr e σ,γ))) σ,γ
locAssign (slice r e)           val σ,γ = locAssign r (mergeVec val (cutVec (locRef r σ,γ) (lower (expr e σ,γ))) (lower (expr e σ,γ))) σ,γ
locAssign (cut r e)             val σ,γ = locAssign r (mergeVec (sliceVec (locRef r σ,γ) (lower (expr e σ,γ))) val (lower (expr e σ,γ))) σ,γ
locAssign (cast eq r)           val σ,γ = locAssign r (castVec (sym eq) val) σ,γ
locAssign nil                   val σ,γ = id
locAssign (cons {ts = ts} r r₁) val σ,γ = locAssign r₁ (tail′ ts val) σ,γ ∘ locAssign r (head′ ts val) σ,γ
locAssign (head {ts = ts} r)    val σ,γ = locAssign r (cons′ ts val (locRef (tail r) σ,γ)) σ,γ
locAssign (tail {ts = ts} r)    val σ,γ = locAssign r (cons′ ts (locRef (head r) σ,γ) val) σ,γ

stmt (s ∙ s₁)              = stmt s₁ ∘ stmt s
stmt skip                  = id
stmt (ref ≔ val)           = uncurry (uncurry (assign ref)) ∘ < < expr val , id > , id >
stmt {Γ = Γ} (declare e s) = < proj₁ , tail′ Γ ∘ proj₂ > ∘ stmt s ∘ < proj₁ , uncurry (cons′ Γ) ∘ < expr e , proj₂ > >
stmt (invoke p es)         = < proc p ∘ < proj₁ , exprs es > , proj₂ >
stmt (if e then s)         = uncurry (uncurry Bool.if_then_else_) ∘ < < lower ∘ expr e , stmt s > , id >
stmt (if e then s else s₁) = uncurry (uncurry Bool.if_then_else_) ∘ < < lower ∘ expr e , stmt s > , stmt s₁ >
stmt {Γ = Γ} (for m s)     = Vec.foldl _ (flip λ i → (< proj₁ , tail′ Γ ∘ proj₂ > ∘ stmt s ∘ < proj₁ , cons′ Γ (lift i) ∘ proj₂ >) ∘_) id (Vec.allFin m)

locStmt (s ∙ s₁)              = locStmt s₁ ∘ < proj₁ , locStmt s >
locStmt skip                  = proj₂
locStmt (ref ≔ val)           = uncurry (uncurry (locAssign ref)) ∘ < < expr val , id > , proj₂ >
locStmt {Γ = Γ} (declare e s) = tail′ Γ ∘ locStmt s ∘ < proj₁ , uncurry (cons′ Γ) ∘ < expr e , proj₂ > >
locStmt (if e then s)         = uncurry (uncurry Bool.if_then_else_) ∘ < < lower ∘ expr e , locStmt s > , proj₂ >
locStmt (if e then s else s₁) = uncurry (uncurry Bool.if_then_else_) ∘ < < lower ∘ expr e , locStmt s > , locStmt s₁ >
locStmt {Γ = Γ} (for m s)     = proj₂ ∘ Vec.foldl _ (flip λ i → (< proj₁ , tail′ Γ ∘ locStmt s > ∘ < proj₁ , cons′ Γ (lift i) ∘ proj₂ >) ∘_) id (Vec.allFin m)

fun {Γ = Γ} (init e ∙ s end) = fetch zero (_ ∷ Γ) ∘ locStmt s ∘ < proj₁ , uncurry (cons′ Γ) ∘ < expr e , proj₂ > >

proc (s ∙end) = proj₁ ∘ stmt s
#+end_src

* AMPSL Hoare Logic Definitions

#+begin_src agda2
data Term (Σ : Vec Type i) (Γ : Vec Type j) (Δ : Vec Type k) : Type → Set ℓ where
  lit           : ⟦ t ⟧ₜ → Term Σ Γ Δ t
  state         : ∀ i → Term Σ Γ Δ (lookup Σ i)
  var           : ∀ i → Term Σ Γ Δ (lookup Γ i)
  meta          : ∀ i → Term Σ Γ Δ (lookup Δ i)
  _≟_           : ⦃ HasEquality t ⦄ → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ bool
  _<?_          : ⦃ Ordered t ⦄ → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ bool
  inv           : Term Σ Γ Δ bool → Term Σ Γ Δ bool
  _&&_          : Term Σ Γ Δ bool → Term Σ Γ Δ bool → Term Σ Γ Δ bool
  _||_          : Term Σ Γ Δ bool → Term Σ Γ Δ bool → Term Σ Γ Δ bool
  not           : Term Σ Γ Δ (bits n) → Term Σ Γ Δ (bits n)
  _and_         : Term Σ Γ Δ (bits n) → Term Σ Γ Δ (bits n) → Term Σ Γ Δ (bits n)
  _or_          : Term Σ Γ Δ (bits n) → Term Σ Γ Δ (bits n) → Term Σ Γ Δ (bits n)
  [_]           : Term Σ Γ Δ t → Term Σ Γ Δ (array t 1)
  unbox         : Term Σ Γ Δ (array t 1) → Term Σ Γ Δ t
  merge         : Term Σ Γ Δ (array t m) → Term Σ Γ Δ (array t n) → Term Σ Γ Δ (fin (suc n)) → Term Σ Γ Δ (array t (n ℕ.+ m))
  slice         : Term Σ Γ Δ (array t (n ℕ.+ m)) → Term Σ Γ Δ (fin (suc n)) → Term Σ Γ Δ (array t m)
  cut           : Term Σ Γ Δ (array t (n ℕ.+ m)) → Term Σ Γ Δ (fin (suc n)) → Term Σ Γ Δ (array t n)
  cast          : .(eq : m ≡ n) → Term Σ Γ Δ (array t m) → Term Σ Γ Δ (array t n)
  -_            : ⦃ IsNumeric t ⦄ → Term Σ Γ Δ t → Term Σ Γ Δ t
  _+_           : ⦃ isNum₁ : IsNumeric t₁ ⦄ → ⦃ isNum₂ : IsNumeric t₂ ⦄ → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ (isNum₁ +ᵗ isNum₂)
  _*_           : ⦃ isNum₁ : IsNumeric t₁ ⦄ → ⦃ isNum₂ : IsNumeric t₂ ⦄ → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ (isNum₁ +ᵗ isNum₂)
  _^_           : ⦃ IsNumeric t ⦄ → Term Σ Γ Δ t → ℕ → Term Σ Γ Δ t
  _>>_          : Term Σ Γ Δ int → (n : ℕ) → Term Σ Γ Δ int
  rnd           : Term Σ Γ Δ real → Term Σ Γ Δ int
  fin           : ∀ {ms} (f : literalTypes (map fin ms) → Fin n) → Term Σ Γ Δ (tuple {n = o} (map fin ms)) → Term Σ Γ Δ (fin n)
  asInt         : Term Σ Γ Δ (fin n) → Term Σ Γ Δ int
  nil           : Term Σ Γ Δ (tuple [])
  cons          : Term Σ Γ Δ t → Term Σ Γ Δ (tuple ts) → Term Σ Γ Δ (tuple (t ∷ ts))
  head          : Term Σ Γ Δ (tuple (t ∷ ts)) → Term Σ Γ Δ t
  tail          : Term Σ Γ Δ (tuple (t ∷ ts)) → Term Σ Γ Δ (tuple ts)
  call          : Function ts ts₁ t → All (Term Σ Γ Δ) ts → All (Term Σ Γ Δ) ts₁ → Term Σ Γ Δ t
  if_then_else_ : Term Σ Γ Δ bool → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ t
#+end_src

#+begin_src agda2
⟦_⟧  : Term Σ Γ Δ t → ⟦ Σ ⟧ₜₛ → ⟦ Γ ⟧ₜₛ → ⟦ Δ ⟧ₜₛ → ⟦ t ⟧ₜ
⟦_⟧ₛ : All (Term Σ Γ Δ) ts → ⟦ Σ ⟧ₜₛ → ⟦ Γ ⟧ₜₛ → ⟦ Δ ⟧ₜₛ → ⟦ ts ⟧ₜₛ

⟦ lit x ⟧                σ γ δ = x
⟦ state i ⟧              σ γ δ = fetch i Σ σ
⟦ var i ⟧                σ γ δ = fetch i Γ γ
⟦ meta i ⟧               σ γ δ = fetch i Δ δ
⟦ e ≟ e₁ ⟧               σ γ δ = (lift ∘₂ does ∘₂ ≈-dec) (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
⟦ e <? e₁ ⟧              σ γ δ = (lift ∘₂ does ∘₂ <-dec) (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
⟦ inv e ⟧                σ γ δ = lift ∘ Bool.not ∘ lower $ ⟦ e ⟧ σ γ δ
⟦ e && e₁ ⟧              σ γ δ = (lift ∘₂ Bool._∧_ on lower) (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
⟦ e || e₁ ⟧              σ γ δ = (lift ∘₂ Bool._∨_ on lower) (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
⟦ not e ⟧                σ γ δ = map (lift ∘ Bool.not ∘ lower) (⟦ e ⟧ σ γ δ)
⟦ e and e₁ ⟧             σ γ δ = zipWith (lift ∘₂ Bool._∧_ on lower) (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
⟦ e or e₁ ⟧              σ γ δ = zipWith (lift ∘₂ Bool._∨_ on lower) (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
⟦ [ e ] ⟧                σ γ δ = ⟦ e ⟧ σ γ δ ∷ []
⟦ unbox e ⟧              σ γ δ = Vec.head (⟦ e ⟧ σ γ δ)
⟦ merge e e₁ e₂ ⟧        σ γ δ = mergeVec (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ) (lower (⟦ e₂ ⟧ σ γ δ))
⟦ slice e e₁ ⟧           σ γ δ = sliceVec (⟦ e ⟧ σ γ δ) (lower (⟦ e₁ ⟧ σ γ δ))
⟦ cut e e₁ ⟧             σ γ δ = cutVec (⟦ e ⟧ σ γ δ) (lower (⟦ e₁ ⟧ σ γ δ))
⟦ cast eq e ⟧            σ γ δ = castVec eq (⟦ e ⟧ σ γ δ)
⟦ - e ⟧                  σ γ δ = neg (⟦ e ⟧ σ γ δ)
⟦ e + e₁ ⟧               σ γ δ = add (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
⟦ e * e₁ ⟧               σ γ δ = mul (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
⟦ e ^ x ⟧                σ γ δ = pow (⟦ e ⟧ σ γ δ) x
⟦ e >> n ⟧               σ γ δ = lift ∘ flip (shift 2≉0) n ∘ lower $ ⟦ e ⟧ σ γ δ
⟦ rnd e ⟧                σ γ δ = lift ∘ ⌊_⌋ ∘ lower $ ⟦ e ⟧ σ γ δ
⟦ fin {ms = ms} f e ⟧    σ γ δ = lift ∘ f ∘ lowerFin ms $ ⟦ e ⟧ σ γ δ
⟦ asInt e ⟧              σ γ δ = lift ∘ 𝕀⇒ℤ ∘ 𝕀.+_ ∘ Fin.toℕ ∘ lower $ ⟦ e ⟧ σ γ δ
⟦ nil ⟧                  σ γ δ = _
⟦ cons {ts = ts} e e₁ ⟧  σ γ δ = cons′ ts (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ)
⟦ head {ts = ts} e ⟧     σ γ δ = head′ ts (⟦ e ⟧ σ γ δ)
⟦ tail {ts = ts} e ⟧     σ γ δ = tail′ ts (⟦ e ⟧ σ γ δ)
⟦ call f es es₁ ⟧        σ γ δ = Den.Semantics.fun 2≉0 f (⟦ es ⟧ₛ σ γ δ , ⟦ es₁ ⟧ₛ σ γ δ)
⟦ if e then e₁ else e₂ ⟧ σ γ δ = Bool.if lower (⟦ e ⟧ σ γ δ) then ⟦ e₁ ⟧ σ γ δ else ⟦ e₂ ⟧ σ γ δ

⟦_⟧ₛ               []            σ γ δ = _
⟦_⟧ₛ {ts = _ ∷ ts} (e ∷ es)      σ γ δ = cons′ ts (⟦ e ⟧ σ γ δ) (⟦ es ⟧ₛ σ γ δ)
#+end_src

#+begin_src agda2
data Assertion (Σ : Vec Type o) (Γ : Vec Type n) (Δ : Vec Type m) : Set (L.suc ℓ) where
  all    : Assertion Σ Γ (t ∷ Δ) → Assertion Σ Γ Δ
  some   : Assertion Σ Γ (t ∷ Δ) → Assertion Σ Γ Δ
  pred   : Term Σ Γ Δ bool → Assertion Σ Γ Δ
  true   : Assertion Σ Γ Δ
  false  : Assertion Σ Γ Δ
  ¬_     : Assertion Σ Γ Δ → Assertion Σ Γ Δ
  _∧_    : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ
  _∨_    : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ
  _⟶_    : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ
#+end_src

#+begin_src agda2
  ⟦_⟧ : Assertion Σ Γ Δ → ⟦ Σ ⟧ₜₛ → ⟦ Γ ⟧ₜₛ → ⟦ Δ ⟧ₜₛ → Set ℓ

  ⟦_⟧ {Δ = Δ} (all P)  σ γ δ = ∀ x → ⟦ P ⟧ σ γ (cons′ Δ x δ)
  ⟦_⟧ {Δ = Δ} (some P) σ γ δ = ∃ λ x → ⟦ P ⟧ σ γ (cons′ Δ x δ)
  ⟦ pred p ⟧           σ γ δ = Lift ℓ (Bool.T (lower (Term.⟦ p ⟧ σ γ δ)))
  ⟦ true ⟧             σ γ δ = Lift ℓ ⊤
  ⟦ false ⟧            σ γ δ = Lift ℓ ⊥
  ⟦ ¬ P ⟧              σ γ δ = ⟦ P ⟧ σ γ δ → ⊥
  ⟦ P ∧ Q ⟧            σ γ δ = ⟦ P ⟧ σ γ δ × ⟦ Q ⟧ σ γ δ
  ⟦ P ∨ Q ⟧            σ γ δ = ⟦ P ⟧ σ γ δ ⊎ ⟦ Q ⟧ σ γ δ
  ⟦ P ⟶ Q ⟧            σ γ δ = ⟦ P ⟧ σ γ δ → ⟦ Q ⟧ σ γ δ
#+end_src

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

#  LocalWords:  AMPSL Hoare NTT PQC structs bitstring bitstrings