Final draft

1 files changed, 904 insertions, 1300 deletions

diff --git a/thesis.org b/thesis.org
index a6b81ab..8e9a1c1 100644
--- a/thesis.org
+++ b/thesis.org
@@ -197,20 +197,24 @@ Main chapters (excluding front-matter, references and appendix):
 #+end_export
 
 #+name: wordcount
-#+begin_src elisp :exports none :eval export
+#+begin_src elisp :exports none
 (if (not (boundp 'squid-eval))
     (setq squid-eval nil))
 
 (if (not squid-eval)
     (progn
       (setq squid-eval t)
-      (org-latex-export-to-latex)
-      (setq squid-eval nil)))
+      (org-latex-export-to-latex)))
+
+(setq squid-eval nil)
 
 (let* ((outfile (org-export-output-file-name ".tex")))
   (shell-command-to-string (concat "texcount -0 -sum \'" outfile "\'")))
 #+end_src
 
+#+RESULTS: wordcount
+: 11800
+
 Main chapters word count: call_wordcount()
 
 #+begin_export latex
@@ -219,7 +223,7 @@ Methodology used to generate that word count:
 \begin{quote}
 \begin{verbatim}
 $ texcount -0 -sum report.tex
-xyz
+11800
 \end{verbatim}
 \end{quote}
 
@@ -239,9 +243,9 @@ 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
+describe the instructions within the manual by [cite/t:@arm/DDI0553B.s] did not
+have a formal semantic description. For this project I created AMPSL, to mock
+the Arm specification language, within Agda. The syntax closely follows that of
 ASL, save some minor modifications due to limitations within Agda and
 adjustments to simplify the semantics.
 
@@ -254,8 +258,8 @@ 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.
+[cite:@10.1007/3-540-47721-7_24]. Formalising Barrett reduction is a significant
+step in formalising the NTT.
 
 #+latex: \ifsubmission\else
 
@@ -287,52 +291,50 @@ actionable feedback on the various drafts of my report.
 
 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
+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.
+PQC's huge computational demands, algorithms like the NTT are presented using
+hand-written, highly-optimised assembly code. To ensure these cryptographic
+algorithms are correct, and thus embedded devices are secure, formal
+verification of these algorithms is necessary.
 
 This report focuses on producing the first formalisation of the semantics of the
 Armv8-M architecture, in particular its M-profile vector extension.
 [cite/t:@arm/DDI0553B.s] provides a pseudocode description of the operation of
 Armv8-M instructions using the Arm pseudocode (henceforth ASL). Unfortunately
 this language is primarily designed for describing instructions
-[cite:@arm/DDI0553B.s §E1.1.1] and not proving properties of their semantics.
+[cite:@arm/DDI0553B.s §E1.1.1] and not proving semantic properties.
 
 To remedy this, I designed AMPSL (Arm M-profile Pseudocode Specification
-Language, or AMPSL Mocks Pseudocode Specification Language), 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.
+Language, or AMPSL Mocks Pseudocode Specification Language). AMPSL is written in
+Agda, a dependently-typed proof assistant [cite:@10.1007/978-3-642-03359-9_6].
+The syntax mirrors that of ASL, save some minor modifications due to limitations
+within Agda and adjustments to simplify the semantics.
 
 AMPSL is given semantics in two different forms. The first is a denotational
 semantics, which converts the various program elements into functions within
-Agda. This enables 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.
+Agda. This enables explicitly computing the effect of AMPSL on the processor
+state. AMPSL also has a set of Hoare logic rules, which form an axiomatic,
+syntax-directed approach to describing how a statement in AMPSL modifies
+assertions on the processor state.
 
 Due to AMPSL's similarity to ASL, I can convert the ASL description of Armv8-M
-instructions into AMPSL. From this AMPSL description of the Armv8-M
-instructions, I can derive the semantics of Armv8-M instructions using AMPSL's
-semantics.
+instructions into AMPSL. From this I can derive the semantics of Armv8-M
+instructions using AMPSL's semantics.
 
 I also use Agda to formally verify a variant of Barrett reduction. Barrett
 reduction is an important subroutine used by the NTT, to efficiently find a
 \ldquo{}small\rdquo{} representable of a value modulo some base
-[cite:@10.1007/3-540-47721-7_24]. Much like how a formalisation of the NTT is a
-big step in formalising the behaviour of many PQC algorithms, formalising
-Barrett reduction is a big step in formalising the NTT.
+[cite:@10.1007/3-540-47721-7_24]. Much like how a formalisation of the NTT is an
+important step in formalising the behaviour of many PQC algorithms, formalising
+Barrett reduction is an important step in formalising the NTT.
 
 #+name: raw_progress
 #+begin_src dot :file progress.pdf :exports none
 digraph {
-    node [shape=box];
+    node [shape=box,width=2.5,height=0.6];
     A [label="Functional correctness\nof NTT",style=dotted];
     B [label="Functional correctness\nof Barrett reduction",style=dotted];
     C [label="NTT properties",style=dotted];
@@ -358,103 +360,97 @@ digraph {
 #+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: dashed border. Significant outstanding work 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.
+[[progress]] shows the progress this work has made to verifying an NTT
+implementation for Armv8.1-M vector extension. Whilst it does not achieve the
+final goal, it forms solid foundations towards it.
 
 The main contributions of this report are as follows:
 - In [[*AMPSL Syntax]], I introduce the syntax of the AMPSL programming language.
-  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.
+  Its primary goal is to facilitate easy translation of programs from ASL,
+  detailed in [[*Arm Pseudocode]] into AMPSL.
+- AMPSL's semantics are described in [[*AMPSL Semantics]]. AMPSL has a simple
+  semantics which facilitates straight-forward proofs about various AMPSL
+  programs. I detail both a denotational semantics and a Hoare logic for AMPSL.
+  The Hoare logic used by AMPSL somewhat varies from the traditional
+  presentation, given in [[*Hoare Logic]], to eliminate adaptation rules.
 - In [[*Soundness of AMPSL's Hoare Logic]], I prove that the set of Hoare logic rules for
-  AMPSL are sound with respect to the denotational semantics. 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
+  AMPSL are sound with respect to the denotational semantics. This proof is
+  possible due to Agda's foundation of Martin-Löf's type theory, the
+  significance of which is given in [[*Agda]]. As AMPSL's Hoare logic is sound, the
+  behaviour of the computationally-intensive denotational semantics can instead
+  be specified using syntax-directed Hoare logic.
+- A number of proof outlines for AMPSL programs are given in [[*Using AMPSL for
   Proofs]]. This describes how AMPSL is used to give the semantics of Armv8.1-M
-  instructions. It also demonstrates 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].
+  instructions. It also demonstrates that AMPSL is viable for the formal
+  verification of various programs, and lays the groundwork for the formally
+  verifying the NTT implementation given by
+  [cite/t:@10.46586/tches.v2022.i1.482-505].
 - Finally, a formal proof of a Barrett reduction variant is given in [[*Proof of
   Barrett Reduction]]. To my knowledge this is the first such machine-verified
-  proof of correctness for Barrett reduction. Further, it is the first proof of
-  Barrett reduction on a domain other than integers and rationals.
+  correctness proof for Barrett reduction. Further, it is the first proof for a
+  domain other than integers and rationals.
 
 * Background
 
 ** Arm Pseudocode
 ASL is a strongly-typed imperative programming language [cite:@arm/DDI0553B.s
 §E1.2.1]. It has a first-order type system, a small set of operators and basic
-control flow, 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.
+control flow. Its primary purpose is to explain how executing an Armv8-M
+instruction modifies the processor state. As it is a descriptive aid, ASL
+features some design choices atypical for other imperative programming
+languages making it difficult to execute.
 
-Something common to 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.
+Something common to ASL and nearly all imperative languages are primitive
+types for Booleans, tuples, structs, enumerations and fixed-length arrays.
 
 Two interesting primitive types used by ASL are mathematical integers and real
 numbers. Other imperative languages typically use fixed-width integers and
 floating point rationals as efficient approximations for these values, with the
 downside of having overflow and precision loss errors. As ASL is for
-specification over execution, the efficiency of code is of no concern so using
-the mathematical types prevents a whole class of errors.
+specification over execution, efficiency is of no concern so using the
+mathematical types prevents a whole class of errors.
 
 The final primitive type used by ASL is the bitstring; a fixed-length sequence
 of 0s and 1s. Some readers may wonder what the difference is between this type
-and 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.
+and Boolean arrays. The justification given by [cite/t:@arm/DDI0553B.s §E1.2.2]
+is more philosophical than practical: \ldquo{}bitstrings are the only concrete
+data type in pseudocode\rdquo{}. In some places, bitstrings can be used in
+arithmetic operations, by first converting them to an unsigned integer.
 
 ASL types have all of the associated standard operations, including equality,
 ordering, Boolean connectives and arithmetic.
 
 The most interesting operation in ASL is bitstring slicing. First, there is no
-type for a bit outside a bitstring---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,
+type for a bit outside a bitstring, so slicing always returns a bitstring.
+Slicing then works in much the same way as array slicing in languages like
+Python and Rust; slicing an integer range from a bitstring returns a new
+bitstring with values corresponding to the indexed bits. The other special
+feature of bitstring slicing is that it can also slice integers.  In that case,
 ASL \ldquo{}treats an integer as equivalent to a sufficiently long [\ldots]
 bitstring\rdquo{} [cite:@arm/DDI0553B.s §E1.3.3].
 
 The final interesting difference between ASL and most imperative languages is
-the variety of top-level items. ASL has three 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].
+the variety of top-level items. ASL has three item forms: procedures, functions
+and array-like functions. Procedures and functions behave like procedures and
+functions of other imperative languages. Their arguments are passed by value,
+and the only difference between the two is that procedures do not return values
+whilst functions do [cite:@arm/DDI0553B.s §E1.4.2].
 
 Array-like functions act as getters and setters for machine state. Every
 array-like function has a reader form, and most have a writer form. This
 distinction exists because \ldquo{}reading from and writing to an array element
-require different functions\rdquo{}, [cite:@arm/DDI0553B.s §E1.4.2], 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].
+require different functions\rdquo{}, [cite:@arm/DDI0553B.s §E1.4.2], due to some
+machine registers being read-only instead of read-writeable. The writer form
+acts as one of the targets of assignment expressions, along with variables and
+the result of bitstring concatenation and slicing [cite:@arm/DDI0553B.s
+§E1.3.5].
 
-Examples of ASL are given throughout the report, often alongside an AMPSL model
-of it.
+An example of ASL is given in [[*Example Armv8-M Instruction Models in AMPSL]],
+alongside an AMPSL model of it.
 
 ** M-profile Vector Extension
 
@@ -468,17 +464,18 @@ A processor can execute either one, two or four instruction beats in an
 [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.
+Processors are allowed but not required to execute two vector instructions
+concurrently [cite:@arm/DDI0553B.s §B5.3]. To summarise the overlap rules, at
+least the first two beats of the current instruction must be completed before
+executing the next one. Then, at most the first two beats of that instruction
+can be executed before the current instruction is finished.
 
 ** Hoare Logic
 Hoare logic is a proof system for programs written in imperative programming
 languages. At its core, the logic describes how to build partial correctness
 triples, which describe how program statements affect assertions about machine
-state. The bulk of a Hoare logic derivation is dependent only on the syntax of
-the program the proof targets.
+state. The bulk of a Hoare logic derivation is dependent only on the program
+syntax the proof targets.
 
 A partial correctness triple is a relation between a precondition \(P\), a
 program statement \(s\) and a postcondition \(Q\). If \(\{P\} s \{Q\}\) is a
@@ -507,80 +504,76 @@ this relation is called a correctness total triple.
 \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.
+[[WHILE-Hoare-logic]] shows the rules [cite/t:@10.1145/363235.363259] introduced for
+the WHILE language. There are two broad classes of Hoare logic rules. The
+structural rules SKIP, SEQ, IF, ASSIGN and WHILE reflect how program syntax
+affects program execution, and thus how to modify the precondition and
+postcondition assertions accordingly. The adaptation rule CSQ uses the same
+statement in the premise and conclusion changing only the preconditions and
+postconditions used.
+
+The SKIP and SEQ rules reflect the idea that the skip statement has no effect on
+state, and sequencing statements composes their effects. The IF rule is also
+uncomplicated. No matter which branch is taken, the postcondition remains the
+same; an if statement does no computation after executing a branch. The branch
+choice depends on the value of ~e~. Because this value is known before executing
+a branch, it is added to the preconditions in the premises.
+
+The ASSIGN rule is the most unintuitive structural rule. In the postcondition,
+any use of ~x~ can be replaced by ~v~ and, due to the assignment, the assertion
+maintains its truth value. In the precondition ~x~ could have any value. By
+applying the substitution of ~v~ for ~x~ to the precondition, the fact that ~x~
+changes value is irrelevant.
 
 The final structural Hoare logic rule for the WHILE language is the WHILE rule.
-This rule can be derived by observing 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.
+This rule can be derived by observing that a while statement is a fixed-point.
+As ~while e do s~ is equivalent to ~if e then (s ; while e do s) else skip~, the
+IF, SEQ and SKIP rules can be used to solve the recursion equations for the
+precondition and postcondition of the while statement.
 
-The only adaptation rule in 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.
+The only adaptation rule in WHILE's Hoare logic is the rule of consequence, CSQ.
+CSQ is necessary in this Hoare logic so that the assertions can be manipulated
+into forms suitable for use by each structural rule. Other forms of Hoare logic,
+like the one for AMPSL given in [[*Hoare Logic Semantics]], make adaptation rules
+redundant.
 
 [cite/t:@10.1145/363235.363259] does not specify the logic used to evaluate the
-implications in 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.
+implications in rule premises. Regular choices are first-order logic and
+higher-order logic [cite:@10.1007/s00165-019-00501-3;@10.1007/s001650050057].
+For specifying program behaviour, having auxiliary variables in the logic is
+vital [cite:@10.1007/s001650050057]. Auxiliary variables are a set of variables
+that cannot be used within a program, so remain constant between the
+precondition and postcondition. This allows for proofs about arbitrary values
+without requiring them to appear in the program.
 
 ** Agda
 Agda is a dependently-typed proof assistant and functional programming language,
 based on Martin-Löf's type theory [cite:@10.1007/978-3-642-03359-9_6].
 [cite/t:@10.1007/978-3-642-03359-9_6] provide an excellent introduction to the
-language. I will now summarise the most important features of Agda for the
+language. I will now summarise the most important Agda features for the
 implementation of AMPSL.
 
 *Inductive families*. Agda generalises ML-style datatypes allowing them to be
-indexed by values as well as types. This is best illustrated by an
-example. Take for instance fixed-length vectors. They can be defined by the
-following snippet:
+indexed by values as well as types. This is best illustrated by an example.
+Fixed-length vectors can be defined by the following snippet:
 
 #+begin_src agda2
-data Vec (A : Set) : ℕ → Set where
+data Vec (A : Set) : (n : ℕ) → Set where
   []  : Vec A 0
   _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)
 #+end_src
 
-Note the type of ~Vec~. It is a function that accepts a type ~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.
+Note the type of ~Vec~. It is a function that accepts a type (or ~Set~) ~A~ and
+a natural number, and returns a type. ~A~ is a /parameter/ of ~Vec~ whilst ~n~
+is an /index/. Parameters are required to be the same for all constructors,
+whilst indices can vary between constructors [cite:@agda.readthedocs.io p.
 \texttt{language/data-types.html}].
 
-Whilst 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.
+Whilst parameter values must be constant across the constructor return values,
+they can vary within the constructor arguments, even for the same type. One
+example of this is the ~Assertion~ type given in [[*Hoare Logic Assertions]]. The
+~all~ and ~some~ constructors both accept an ~Assertion Σ Γ (t ∷ Δ)~, but
+because they return an ~Assertion Σ Γ Δ~ the definition is valid.
 
 *Propositional equality*. One very important datatype in Agda is propositional
 equality, shown in the following snippet:
@@ -590,17 +583,18 @@ 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:
+The only constructor, ~refl~, requires that the two values in the type are
+identical. Hence whenever there is a value of type ~x ≡ y~, ~x~ and ~y~ have
+the same value, even when Agda cannot compute that value. One useful
+propositional-equality eliminator is in the ~subst~ function:
 
 #+begin_src agda2
 subst : (B : A → Set) → x ≡ y → B x → B y
 subst _ refl Bx = Bx
 #+end_src
 
-Given a proof that two values are equal, this function lets you use dependant
-values for one type in place of the other.
+Given a proof ~x ≡ y~ that ~x~ and ~y~ are equal, this function makes uses of
+~x~ and ~y~ within types interchangeable.
 
 *Parameterised modules and records*. Agda modules can accept parameters, which
 can be used anywhere in the module. This works well with Agda's record types,
@@ -626,7 +620,7 @@ 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
+a type within Agda, it must itself have a type. If ~Set~ was within ~Set~, Agda
 would be subject to a logical inconsistency known as Girard's paradox
 [cite:@cs.cmu.edu/girard-72-thesis]. Thus, ~Set~ has type ~Set 1ℓ~, and ~Set i~
 has type ~Set (ℓsuc i)~.
@@ -634,97 +628,90 @@ 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.
+This is useful when a type's operations and properties are well-defined, but a
+good representation is unknown.
 
 *Instance arguments* Instance arguments are analogous to the type class
-constraints you find in Haskell [cite:@agda.readthedocs.io p.
+constraints found in Haskell [cite:@agda.readthedocs.io p.
 \texttt{language/instance-arguments.html}]. They are a special form of implicit
-argument that are solved via /instance resolution/ over unification.  Instance
+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.
+arguments to be specified explicitly. Using instance arguments instead can force
+a particular solution onto Agda, reducing the volume of explicit code.
 
 * Related Work
 
-There exist 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.
+There exist many formal verification tools designed to describe either ISA
+instruction semantics or prove algorithms correct. This section describes some
+significant work in the field and how the AMPSL's design improves
+upon it.
 
 ** Sail
 
-Sail [cite:@10.1145/3290384] is a language for describing the instruction-set
-architecture semantics of processors. It has a syntax similar to the pseudocode
+Sail [cite:@10.1145/3290384] is a language for describing processor instruction-set
+architecture semantics. It has a syntax similar to the pseudocode
 specification of most architectures and a first-order type system with dependent
 bitvector and numeric types. It is officially used by
-[cite/t:@riscv/spec-20191213] to specify the concurrent memory semantics of the
-RISC-V architecture.
+[cite/t:@riscv/spec-20191213] to specify the RISC-V concurrent memory semantics.
 
 Sail has many different backends available, including sequential emulators,
 concurrency models and theorem-prover definitions. Further, there are tools to
 automatically translate documents from the Arm Specification Language into Sail
 [cite:@10.1145/3290384].
 
-Despite 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.
+Despite Sail's advantages over other solutions, including AMPSL, using Sail in
+this project is not suitable for a few reasons. First is a lack of
+documentation for the Sail theorem-proving backends. Without prior knowledge in
+using Sail, deciphering the automatically-generated statements from Sail would
+likely consume more time than creating AMPSL.
 
 Another reason to avoid Sail is the unnecessary complexity in modelling the ISA
-semantics. One of Sail's highlights is in its description of 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.
+semantics. One of Sail's highlights is in its description of architectural
+memory models. However, this work attempts to verify the functional correctness
+of NTT, an algorithm with very little memory usage. Creating a simpler language
+like AMPSL removes the need to reason about these complex memory interactions
+and focus on the computation itself.
 
 ** Other Functional Correctness Tools
-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
+Various tools exist for proving functional correctness of programs. These
+include tools that target C such as CryptoLine [cite:@10.1145/3319535.3354199],
+Fiat Crypto [cite:@10.1109/SP.2019.00005], Frama-C
+[cite:@10.1007/s00165-014-0326-7] and VST [cite:@10.1007/978-3-642-19718-5_1],
+as well as tools that target assembly directly such as Jasmin
+[cite:@10.1145/3133956.3134078] and Vale [cite:@10.1145/3290376].
+
+There are two distinct problems with using these tools to verify
+that a pre-existing NTT implementation for Armv8-M is functionally correct:
+- These tools do not accept assembly as an input language. This means they are
   unable to verify an existing assembly algorithm.
-- None of these tools target Armv8-M assembly as output. Jasmin and Vale, whilst
+- These tools do not target Armv8-M assembly as output. Jasmin and Vale, whilst
   targeting assembly, do not currently target the Armv8-M architecture, let
-  alone the M-profile vector extension. The other tools target C and require the
-  use of a verified compiler, of which none currently target Armv8-M.
-- Final point?
+  alone the M-profile vector extension. The other tools target C and require
+  using verified compiler, of which none currently target Armv8-M.
 
 The most similar tool to what this project is trying to achieve is a formal
-verification tool by [cite:@10.1145/3391900], which targets the REDFIN
+verification tool by [cite/t:@10.1145/3391900], which targets the REDFIN
 instruction set. REDFIN has much less complex semantics than Armv8-M, to the
 point where the semantics can be expressed directly without the need for a
-specification language.
+specification language, making using REDFIN in proofs much easier than Armv8-M
+instructions.
 
 * Design of AMPSL and its Semantics
 
-In this chapter I introduce AMPSL, an Agda embedding of ASL. I also describe the
-semantics of AMPSL via a denotational semantics interpreting AMPSL expressions
-and statements as Agda functions
+In this chapter I introduce AMPSL, an Agda embedding of ASL. I also describe
+AMPSL's semantics via a denotational semantics that interprets AMPSL expressions
+and statements as Agda functions.
 
-One downside of 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.
+One downside of AMPSL's simple denotational semantics is that control flow for
+looping constructs is fully evaluated. This is inefficient for loops that
+undergo many iterations. This can be resolved by a syntax-directed Hoare logic
+for AMPSL.
 
 ** AMPSL Syntax
-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.
+ASL has some small features that make it difficult to work with in Agda
+directly. AMPSL makes minor changes to ASL to better facilitate this embedding,
+typically generalising existing ASL features.
 
 *** AMPSL Types
 
@@ -741,38 +728,33 @@ data Type : Set where
   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-types]] gives the Agda datatype representing the AMPSL types. Most of these
+have a direct analogue to ASL types. Instead of an enumeration construct, AMPSL
+uses the ~fin n~ type, representing a set of ~n~ elements. Similarly,
+structs are represented by ~tuple~ types.
+
+The most significant difference between ASL and AMPSL is the representation of
+bitstrings. Instead of a separate bitstring type, AMPSL uses Boolean arrays.
+This lets AMPSL generalise some ASL operations to other array types and makes
+AMPSL more expressive.
+
+ASL specifies three different type properties: equality comparisons, order
+comparisons and arithmetic operations. Whilst using the relevant operations in
+AMPSL requires a proof that the types have the required property, using instance
+arguments allows for these proofs to be elided in almost all cases.
+
+AMPSL maintains the ASL type properties with two additions. First, array types
+have equality if the enumerated type also has equality. This is a natural
+generalisation of equality and allows for AMPSL's formulation of bitstrings as
+Boolean arrays to have equality. Second, finite sets also have ordering. This
+change is primarily a convenience feature for comparing finite sets representing
+an integer subset.
+
+The final interesting type feature in AMPSL is implicit coercion for arithmetic.
+As ASL arithmetic is polymorphic for integers and reals, AMPSL needs a function
+to decide the result type. By describing the output type as a function on
+the input types, the same constructor can be used for all combinations of
+numeric inputs.
 
 *** AMPSL Expressions
 
@@ -789,16 +771,15 @@ 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.
+has a literal form. This mapping is given by the ~literalType~ function, shown
+in [[AMPSL-literalType]]. Most AMPSL literals accept the corresponding Agda type as
+a value. The only exception to this rule is for ~real~ values. As Agda does not
+have a type representing mathematical reals, integers are used instead. This is
+sufficient as any literal real value in ASL is represented as a decimal; a
+rational value.
 
 #+name: AMPSL-expr-prototypes
-#+caption: Declarations of the Agda embeddings of the AMPSL program elements.
+#+caption: Agda declarations of the AMPSL program elements.
 #+attr_latex: :float t
 #+begin_src agda
 data Expression     (Σ : Vec Type o) (Γ : Vec Type n) : Type → Set
@@ -811,8 +792,8 @@ 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]].
+#+caption: AMPSL's grammar. The formal Agda definition is in the provided
+#+caption: source code.
 #+begin_figure
 \begin{align*}
 \mathrm{Natural}\;{}n = & \texttt{0} \mid \texttt{suc}\;{}n \\
@@ -838,67 +819,64 @@ data Procedure      (Σ : Vec Type o) (Γ : Vec Type n) : Set
 \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.
+[[AMPSL-expr-prototypes]] lists the Agda data type declarations corresponding to the
+AMPSL program elements. The grammar is summarised in [[AMPSL-grammar]]. Each type is
+parameterised by two variable contexts: Σ for global variables and Γ for local
+variables. The two variable contexts are split to simplify the types for
+function calls and procedure invocations. As the set of global variables does
+not change across a program, functions and procedures keep the same value of
+parameter Σ in their types. As functions and procedures have different local
+variables than the calling context, having the local variable context as a
+separate parameter makes the change simple.
 
 An ~Expression~ in AMPSL corresponds to expressions in ASL. Many operators are
-identical to those in ASL (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.
+identical to those in ASL, and others are simple renamings (like ~≟~ for
+~==~ for equality comparisons). Unlike ASL, where literals can appear
+unqualified, AMPSL literals are introduced by the ~lit~ constructor.
 
 The most immediate change for programming in AMPSL versus ASL is how variables
-are handled. Because the ~Expression~ type 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
+are handled. Because the ~Expression~ type depends on the values of variable
+contexts, a variable is referred to by its index into the context. For example,
+a variable context \(\{x \mapsto \mathrm{int}, y \mapsto \mathrm{real}\}\) is
+represented in AMPSL as the context ~int ∷ real ∷ []~. The variable \(x\) is
+then represented by ~var 0F~ in AMPSL, where the ~F~ indicates the index is from
+a finite set. Because the global and local variable contexts are disjoint for
+the ~Expression~ type, variables are constructed using ~state~ or ~var~
+respectively.
+
+Whilst this decision makes programming using AMPSL more complex, it greatly
+simplifies the language for use in constructing proofs.
+
+AMPSL expressions also add a number of useful constructs to ASL. One such pair
+are ~[_]~ and ~unbox~, which construct and destruct a length-one array
 respectively. Others are ~fin~, which allows for arbitrary computations on
 elements of finite sets, and ~asInt~, which converts a finite value into an
 integer.
 
-The final three 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.
+The final three noteworthy operators are ~merge~, ~slice~ and ~cut~. These all
+perform operations on arrays, by either merging two together, taking out a
+slice, or dropping a slice. Unlike ASL where bitstring slicing requires a range,
+these three operators use Agda's dependent types and type inference so that only
+a base offset is necessary.
 
-~slice xs i~, like bitstring slicing, extracts a contiguous subset 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.
+~slice xs i~, like bitstring slicing, extracts a contiguous subset from an array
+~xs~, such that the first element in ~slice xs i~ is in ~xs~ at position ~i~.
+~cut xs i~ returns the remainder of ~slice xs i~; the two ends of ~xs~ not in
+the slice, concatenated. Finally, ~merge xs ys i~ joins ~xs~ and ~ys~ to form a
+product-projection triple with ~slice~ and ~cut~.
 
 The ~Reference~ type is the name AMPSL gives to assignable expressions from ASL.
 The ~LocalReference~ type is identical to ~Reference~, except it does not
 include global variables. Due to complications in the semantics of multiple
 assignments to one location, \ldquo{}product\rdquo operations like ~merge~ and
 ~cons~ are excluded from being references, despite concatenated bitstrings and
-tuples being assignable expressions in ASL. Whilst [cite:@arm/DDI0553B.s
+tuples being assignable expressions in ASL. Whilst [cite/t:@arm/DDI0553B.s
 §E1.3.3] requires that no position in a bitstring is referenced twice, enforcing
 this in AMPSL for ~merge~ and ~cons~ would make their use unergonomic in
 practice for writing code or proofs.
 
 **** Example AMPSL Expressions
-One arithmetic operator used in ASL is left shift.  [cite:@arm/DDI0553B.s
+One arithmetic operator used in ASL is left shift. [cite/t:@arm/DDI0553B.s
 §E1.3.4] explains how this can be encoded using other arithmetic operators in
 AMPSL, as shown below:
 
@@ -907,16 +885,13 @@ _<<_ : 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
+There is a lot of hidden complexity here. First, consider the literal
+statement's type. The unary plus operation indicates the literal is an Agda
 integer. However, there are two AMPSL types with Agda integers for literal
-values: ~int~ and ~real~.
-
-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.
+values: ~int~ and ~real~. The multiplication result must be an ~int~, and the
+first argument is also an ~int~. Because multiplication's type is determined by
+implicit coercion, Agda can unwind the function defining the coercion and finds
+that the literal must be an ~int~.
 
 Another pseudocode operation not yet described in AMPSL is integer slicing. Here
 is an expression that slices a single bit from an integer, following the
@@ -929,10 +904,11 @@ getBit i x =
 #+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
+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~.
+complement representation of ~x~ is ~0~, otherwise it is ~1~, hence the whole
+condition is inverted.
 
 *** AMPSL Statements
 Most statements in AMPSL are straight forward. The ~skip~ and sequencing (~_∙_~)
@@ -940,21 +916,19 @@ statements are familiar from the discussion on Hoare logic; the assignment
 statement (~_≔_~) assigns a value into a reference; the ~invoke~ statement calls
 a procedure; and the ~if_then_else_~ statement starts a conditional block.
 
+# FIXME: why not a typedef?
 Given that AMPSL has a ~skip~ statement and an ~if_then_else_~ control-flow
 structure, including the ~if_then_~ statement is redundant. It is included in
-AMPSL for 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.
+AMPSL for ergonomics. ~if_then_~ statements appear many times more often in ASL
+than ~if_then_else_~ statements such that omitting it would only serve to
+complicate embedded code.
 
 The form of variable declarations is significantly different in AMPSL than it is
-in ASL. 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.
+in ASL. AMPSL variable declarations do not need a name as they are accessed by
+index. Type annotations are unnecessary as Agda can often infer a declared
+variable's type from the context in which it is used. All variables in AMPSL
+must be initialised, simplifying the AMPSL's semantics and preventing the use
+of uninitialised variables.
 
 AMPSL makes a small modification to ~for~ loops that greatly improve the type
 safety over what is achieved by ASL. Instead of looping over a range of dynamic
@@ -964,14 +938,14 @@ 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],
+loops, ~repeat...until~ loops and ~try...catch~ exception handling. Including
+these three statements would complicate AMPSL's denotational encoding, by
+removing termination guarantees and requiring a monadic transformation for the
+loops and exceptions, respectively.
+
+Thankfully, these three structures are not vital in ASL, each either having a
+functional alternative [cite:@arm/DDI0553B.s §E2.1.166] or forming part of
+internal processor bookkeeping [cite:@arm/DDI0553B.s §E2.1.397],
 [cite:@arm/DDI0553B.s §E2.1.366]. Hence their omission from AMPSL is not a
 significant loss.
 
@@ -981,41 +955,35 @@ To encode effectless functions, AMPSL has a ~LocalStatement~ type as well as a
 ~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:
+Here is a statement that copies bytes from ~x~ into the machine register ~Q[
+dest , i ]~ 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
-    ∷ [])
+  Statement State ( fin 8 ∷ array (bits 8) 4 ∷ array bool 4 ∷ [])
 copyMasked =
   for n (
-    let i = var 0F in
-    let x = var 1F in
-    let y = var 2F in
+    let i    = var 0F in
+    let dest = var 1F in
+    let x    = var 2F in
     let mask = var 3F in
 
-    if index mask i ≟ true
-    then
-        ,*index x i ≔ index y i
+    if index mask i then
+      Q[ dest , i ] ≔ index x 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.
+This uses the Agda function ~index~ to apply the appropriate slices, casts and
+unboxing to extract a single byte from the array ~x~. Note the use of Agda's
+~let...in~ construct to give variables meaningful names. This is a stylistic
+choice that works well in this case.
+
 Unfortunately, if the ~if_then_~ statement declared a new variable, these naming
 variables would become useless, as the types would be different. For example
 consider the following snippet:
 
-# FIXME: compare with ASL
 #+begin_src agda2
-VPTAdvance : Statement State (beat ∷ [])
+VPTAdvance : Procedure State (beat ∷ [])
 VPTAdvance =
   declare (fin div2 (tup (var 0F ∷ []))) (
   declare (elem 4 (! VPR-mask) (var 0F)) (
@@ -1023,24 +991,20 @@ VPTAdvance =
     let maskId = var 1F in
     let beat = var 2F in
 
-    if ! vptState ≟ lit (true ∷ false ∷ false ∷ false ∷ [])
-    then
+    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
+    else if inv (! vptState ≟ lit (Vec.replicate false)) then (
+      declare (call (LSL-C 0) (! vptState ∷ [])) (
+        let vptState′,i = var 0F in
         let vptState = var 1F in
-        -- let mask = var 2F in
         let beat = var 3F in
 
-        cons vptState (cons i nil) ≔ call (LSL-C 0) (! vptState ∷ []) ∙
-        if ! i
-        then
+        vptState ≔ head vptState′,i ∙
+        if head (tail vptState′,i) then
           ,*elem 4 VPR-P0 beat ≔ not (elem 4 (! VPR-P0) beat))) ∙
-    if getBit 0 (asInt beat)
-    then
+    if getBit 0 (asInt beat) then
       ,*elem 4 VPR-mask maskId ≔ ! vptState))
+  ∙end
 #+end_src
 
 This corresponds to the ~VPTAdvance~ procedure by [cite/t:@arm/DDI0553B.s
@@ -1051,47 +1015,45 @@ 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,
+Much like how a procedure in ASL is a wrapper around a statement block,
 ~Procedure~ in AMPSL is a wrapper around ~Statement~. Note that AMPSL procedures
 only have one exit point, the end of a statement, unlike ASL which has ~return~
 statements. Any procedure using a ~return~ statement can be transformed into one
-that does not by a simple refactoring, so AMPSL does not lose any expressive
-power over ASL.
+that does not by 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.
+AMPSL functions are more complex than procedures. A function is a pair of an
+~Expression~ and ~LocalStatement~. The statement has the function arguments and
+the return value as local variables, where the return value is initialised to
+the result of the expression. The return value is the final value of the return
+variable after executing the statement.
 
 **** Example AMPSL Functions and Procedures
-As ~Procedure~ is almost an alias for ~Statement~, examples of procedures can be
+As ~Procedure~ is almost an alias for ~Statement~, example procedures can be
 found in [[*Example AMPSL Statements]]. This is a simple function that converts a
 bitstring to an unsigned or signed integer, depending on whether the second
 argument is true or false:
 
-# 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
+    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 function body is the ~skip~ statement, meaning that the result of calling
+the function is whatever is initially assigned to the return variable. The
+initial value here is a simple conditional statement, calling ~uint~ or ~sint~
+on the first argument as appropriate. Many functions that are easy to inline
+have this form.
 
 The next example shows the ~uint~ function, which converts a bitstring into an
 unsigned integer.
 
-# FIXME: add pseudocode equivalent
 #+begin_src agda2
 uint : Function Σ (bits n ∷ []) int
 uint {n = 0}     = init lit 0ℤ ∙ skip end
@@ -1104,8 +1066,7 @@ uint {n = suc n} =
       let ret = var 2F in
       let scale = var 1F in
       let i = var 0F in
-      if index x i
-      then (
+      if index x i then (
         ret ≔ !! ret + !! scale
       ) ∙
       scale ≔ lit (ℤ.+ 2) * !! scale
@@ -1113,24 +1074,23 @@ uint {n = suc n} =
   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
+The AMSPL function has two forms, depending on the number of input bits. If the
+input is a zero-length bitstring, then its integer value is zero. Otherwise, the
+function iterates through the bits in turn, adding a bit's place value into the
 return value whenever that bit is true.
 
 This example highlights the similarities between functions and ~declare~
-statements. 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.
+statements. A local variable is declared with some initial value. It is then
+used in some further computation. The only difference is the action when leaving
+scope. A declare statement would simply discard the local variable. A function
+instead returns that value.
 
 ** AMPSL Semantics
 This section starts with a brief discussion of how to model AMPSL types. This
-addresses 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.
+addresses how to model real numbers in Agda. From this, I describe AMPSL's
+denotational semantics, and how AMPSL can be converted into Agda functions. The
+section ends with a Hoare logic for AMPSL, allowing for efficient
+syntax-directed proofs about statements.
 
 *** AMPSL Datatype Models
 #+name: AMPSL-type-models
@@ -1153,41 +1113,37 @@ syntax-directed proofs of statements.
 #+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
+to find a suitable encoding for the data types. [[AMPSL-type-models]] shows the full
+encoding function for AMPSL.
+
+Tuples are encoded as an n-ary product. This is computed by the ~⟦_⟧ₜₛ~
+function in [[AMPSL-type-models]]. The Agda type checker would not accept using a
+library-provided n-ary product in this case due to termination checking, hence
+the manual inductive definition.
+
+The other two AMPSL types are ~int~ and ~real~. Whilst ~int~ could feasibly be
 encoded by the Agda integer type, there is no useful Agda encoding for
-mathematical real numbers. 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:
+mathematical real numbers. Hence both numeric types are represented by abstract
+types with the appropriate properties. ~int~ is represented by a discrete
+ordered commutative ring ℤ and ~real~ by a field ℝ. There must also be a split
+ring monomorphism \(\mathtt{/1} : ℤ \to ℝ\) with retraction \(\mathtt{⌊\_⌋} : ℝ
+\to ℤ\). \(\mathtt{⌊\_⌋}\) may not be a ring homomorphism, but it must preserve
+\(\le\) ordering and satisfy the floor property:
 
 \[
 \forall x y.\;x < y \mathtt{/1} \implies ⌊ x ⌋ < y
 \]
 
-~/1~ represents the usual embedding of integers into real numbers, by division
-by one. ~⌊_⌋~ represents the floor function.
+~/1~ represents the usual embedding of integers into real numbers. ~⌊_⌋~
+represents the floor function. Because ~/1~ is a monomorphism, we have
+\(\mathtt{⌊ x /1 ⌋} = \mathtt{x}\) for all \(\mathtt{x} \in ℤ\).
 
 *** Denotational Semantics
 
 #+name: AMPSL-denotational-prototypes
-#+caption: Function prototypes for the denotational semantics of different AMPSL
-#+caption: program elements. All of them become functions from the current
-#+caption: variable context into some return value.
+#+caption: Function prototypes for AMPSL's denotational semantics. All program
+#+caption: elements become functions from the current variable context into some
+#+caption: return value.
 #+begin_src agda2
 expr      : Expression Σ Γ t        → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ t ⟧ₜ
 exprs     : All (Expression Σ Γ) ts → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ ts ⟧ₜₛ
@@ -1199,78 +1155,74 @@ fun       : Function Σ Γ 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.
+Due to careful design of AMPSL's syntax, each of its program elements is
+denotationally represented by a total Agda function.
 [[AMPSL-denotational-prototypes]] shows the prototypes of the different semantic
-interpretation functions, and the full 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.
+interpretation functions, and the full definitions are in the provided source
+code. Each function accepts the current variable context as an argument.
+Because the variable contexts are an ordered sequence of values, they can be
+encoded in the same way as tuples.
 
 **** Expression Semantics
 
 The semantic representation of an expression converts the current variable
 context into a value with the same type as the expression. Most cases are pretty
 simple. For example, addition is the sum of the values of the two subexpressions
-computed recursively. 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.
+computed recursively. Two more interesting cases are global and local variables,
+albeit this is only a lookup in the variable context for the current value. This
+lookup is guaranteed to be safe due to variables themselves being a lookup into
+the current type context. Despite both being contained within the ~Expression~
+type, ~Reference~ and ~LocalReference~ require their own functions to satisfy
+the Agda termination checker.
+
+One significant omission from this definition is the expression evaluation
+order. The order is irrelevant due to the design choice that AMPSL functions
+cannot modify global state, meaning expressions have no side effects. This is
+also reflected in the type of ~Expression~'s denotational representation. It
+can only possibly return a value and not a modified state.
 
 **** Assignment Semantics
 #+name: AMPSL-denotational-assign-prototypes
 #+caption: Function prototypes for the ~assign~ and ~locAssign~ helper
-#+caption: functions. 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.
+#+caption: functions.
 #+begin_src agda2
-assign    : Reference Σ Γ t      → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ
-locAssign : LocalReference Σ Γ t → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜₛ × ⟦ Γ ⟧ₜₛ → ⟦ Γ ⟧ₜₛ
+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~.
+I first describe assignment statements before discussing the other statement
+forms. If assignments were only into variables this would be trivial. Using
+~Reference~, in attempt for AMPSL to keep the same form as ASL, makes things
+more tricky. Broadly speaking, there are three kinds of ~Reference~: terminal
+references like ~state~ and ~var~; isomorphism operations like ~unbox~, ~[_]~
+and ~cast~; and projection operations like ~slice~, ~cut~, ~head~ and ~tail~.
 
-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]].
+I will describe how to update each kind of reference in turn. This is the action
+performed by helper functions ~assign~ and ~locAssign~, whose signatures are
+given in [[AMPSL-denotational-assign-prototypes]].
 
 Terminal references are the base case and easy. Assigning into ~state~ and ~var~
 updates the relevant part of the variable context. Isomorphic reference
 operations are also relatively simple to assign into. First, transform the
 argument using the inverse operation, and assign that into the sub-reference.
-For example, the assignment ~[ ref ] ≔ v~ 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.
+For example, the assignment ~[ ref ] ≔ v~ has the same behaviour as ~ref ≔ unbox
+v~.
+
+For reference projections, assigning into one projection of a reference means
+that the other projection remains unchanged. Consider the assignment ~head r ≔
+v~ as an example. This is equivalent to ~r ≔ cons v (tail r)~, which makes it
+clear that the second projection remains constant. The second projection must be
+computed using the original variable context, which is achieved by only updating
+the context for a leaf reference.
+
+Interpreting slice as a projection reference type is a major reason why AMPSL
+has ~merge~, ~cut~ and ~slice~ instead of the bitstring concatenation and
+slicing present in ASL. There is no way to form a product-projection triple with
+only bitstring joining and slicing, so any denotational semantics with these
+operations would require merge and cut operations on the value encodings. AMPSL
+takes these semantic necessities and makes them available to programmers.
 
 ~assign~ and ~locAssign~, when given a reference and initial context, return the
 full and local variable contexts respectively. As ~Reference~ includes both
@@ -1279,22 +1231,21 @@ 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.
+Other AMPSL statements have straightforward semantics. Skip statements map to
+the identity function and sequencing is function composition, reflecting that
+they do nothing and compose statements together respectively. As expressions
+cannot modify state, ~if_then_else_~ and ~if_then_~ statements become
+simple---evaluate the condition and both branches on the input state, and return
+the branch depending on the condition's value. ~declare~ statements are also
+simple. The initial value is computed and added to the variable context. After
+evaluating the subsequent statement, the added variable is stripped away from
+the context.
 
 The only looping construct in AMPSL is the ~for~ loop. Because it performs a
-fixed number of iterations, it 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.
+fixed number of iterations, it is effectively a sequence of ~declare~
+statements. This is also one of the primary reasons why the denotational
+semantics can have poor computational performance; every ~for~ loop iteration
+must be evaluated individually.
 
 ~stmt~ and ~locStmt~ return the full context and only the local variables
 respectively. This is because only ~Statement~ can include ~Reference~ which can
@@ -1315,44 +1266,40 @@ 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.
+AMPSL has also been given a form of Hoare Logic rules. The Hoare logic is
+syntax-directed; loops only require a single proof. This section starts by
+explaining how a AMPSL ~Expression~ is converted into a ~Term~ for use in Hoare
+logic assertions. Then the syntax and semantics of the ~Assertion~ type is
+discussed before finally giving the total correctness triples for AMPSL.
 
 **** Converting ~Expression~ into ~Term~
-As 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]].
+
+As shown in [[*Hoare Logic]], a simple language such as WHILE can use expressions as
+terms in assertions directly. The only modification required is the addition of
+auxiliary variables. AMPSL is not as simple a language as WHILE, thanks to
+function calls within expressions. Whilst function calls do not prevent
+converting expressions into terms, some care must be taken. In particular, this
+conversion is only as functions not modify global variables. The full definition
+of ~Term~ and its semantics are given in the provided source code.
 
 First, a demonstration on why function calls need special care in Hoare logic.
-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.
+For this example, the environment contains a single Boolean-valued global
+variable. Consider the following AMPSL function, a unary operator on an
+integer, which is the identity when ~state 0F~ is false and otherwise performs
+an increment.
 
 #+begin_src agda2
 f : Function [ bool ] [ int ] int
 f =
   init
     var 0F ∙
-    let x = var 1F in
-    let ret = var 0F in
-    if state 0F
-      then ret ≔ lit 1ℤ + x
+    if state 0F then var 0F ≔ lit 1ℤ + var 1F
   end
 #+end_src
 
 Consider the expression ~e = call f [ x ]~ of type ~Expression [ bool ] Γ int~.
-There are three important aspects we need to consider for converting ~e~ into a
-term: the initial conversion; substitution of variables; and the semantics.
+There are two important aspects to consider for converting ~e~ into a term:
+the initial conversion and substitution of references.
 
 The simplest conversion is to keep the function call as-is, and simply
 recursively convert ~x~ into a term. This would result in a term ~e′ = call f [
@@ -1362,97 +1309,69 @@ 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.
+]~, so there is no way to the term ~t~ inside the function ~f~. This embedding is
+not sufficient.
+
+A solution comes by thinking of global variables in ~f~ as an additional
+argument set. In an ~Expression~, these arguments always corresponds exactly
+with the global variables, so are elided. In a term, they can be made explicit.
+An embedding function ~↓_~ can be defined, such that ~↓ e = call f [ state 0F ]
+[ ↓ x ]~, and all the other expression forms as expected.
 
 Doing a substitution on ~↓ e~ is now simple: perform the substitution on both
-sets of arguments recursively, and leave ~f~ unchanged. As the first set of
+argument lists recursively, and leave ~f~ unchanged. As the first set of
 arguments correspond exactly to the global variables in ~f~, the substitution
 into those arguments appears like a substitution into ~f~ itself.
 
-The 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~.
+new auxiliary variable context, Δ, which forms part of ~Term~'s type definition.
 
 **** 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 Hoare logic for AMPSL uses a first-order logic for assertions, which allows
+for the easy proof of many logical implications at the expense of not being
+complete over the full set of state properties. The full definition and
+semantics of the ~Assertion~ type are in the provided source code.
+
+The ~Assertion~ type has the usual set of Boolean connectives. Another
+constructor is ~pred~, which accepts an arbitrary Boolean-valued ~Term~. This is
+the only way to test properties of the current program state within assertions.
+As nearly all types have equality comparisons, ~pred~ can encode equality and
+inequality constraints on values. Furthermore, as ~Term~ embeds ~Expression~,
+many complex computations can be performed within ~pred~.  There is an ~equal~
+function to construct an assertion comparing any two values with the same type,
+even if their type does not have equality.
 
 The final two constructors of ~Assertion~ provide first-order quantification
 over auxiliary variables. ~all~ provides universal quantification and ~some~
 provides existential quantification.
 
-Semantically, an assertion is a predicate on the current state of execution. For
+Semantically, an assertion is a predicate on the current execution state. For
 AMPSL, this state is the current global, local and auxiliary variable contexts.
 The predicates are encoded as an indexed family of sets.
 
 The Boolean connectives are represented by their usual type-theoretic
-counterparts: 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.
+counterparts. Quantifier assertions are also quite easy to give a semantic
+representation. Universal quantification is represented by a function taking
+values for the quantified variable and returning a proof of the inner assertion.
+Existential quantification is represented by a dependent pair of a value for the
+quantified variable, and a proof the inner assertion.
 
 The final ~Assertion~ form to consider is ~pred~. This first evaluates the
 associated Boolean term. If true, the semantics returns the unit type.
-Otherwise, it returns the empty type.
-
-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.
+Otherwise, it returns the empty type. Whilst directly providing a richer type is
+difficult, due to having to find a normal form for the ~Term~ type, all
+equalities and inequalities between AMPSL values are recomputable. This allows
+the user to extract Agda terms for equalities given only knowledge of whether
+terms are equal.
 
 **** Correctness Triples for AMPSL
 In the traditional presentation of Hoare logic ([[*Hoare Logic]]), there are two
-types of rule; structural rules based on program syntax and adaptation rules to
+rule types; 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.
+two rule types, allowing for purely syntax-directed proofs for any precondition
+and postcondition.
 
 #+name: AMPSL-Hoare-logic
 #+caption: The Hoare logic correctness triples for AMPSL. The unusual argument
@@ -1462,21 +1381,28 @@ 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₁)
+  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 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
+  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))
+              ∧ equal (↓ tup (All.tabulate var))
+                      (termVarsToMetas (↓ tup es))
               )
               (varsToMetas Q)
               s →
@@ -1503,21 +1429,20 @@ data HoareTriple (P : Assertion Σ Γ Δ) (Q : Assertion Σ Γ Δ) :
             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
+I will now talk through each of the Hoare logic rules for AMPSL, which are given
+in [[AMPSL-Hoare-logic]]. The simplest rule to consider is ~skip~. This immediately
+demonstrates how AMPSL Hoare logic combines structural and adaptation rules. A
+purely structural rule for ~skip~ would be ~HoareTriple P P skip~; the ~skip~
+statement has no effect on the current state. By combining this with the rule of
+consequence, a ~skip~ statement allows for logical implication.
+
+The ~seq~ rule mirrors the SEQ rule of WHILE's Hoare logic. The only potential
+surprise is that the intermediate assertion has to be given explicitly. This is
+due to Agda being unable to infer the assertion ~Q~ from the numerous
+manipulations applied to it by the other correctness rules.
+
+Another pair of simple rules are ~if~ and ~if-else~. The ~if-else~ rule is
+identical to the corresponding Hoare logic rule from WHILE, and ~if~ only
 differs by directly substituting in a ~skip~ statement for the negative branch.
 
 The final trivial rule is ~assign~. Like the ~skip~ rule, the ~assign~ rule
@@ -1532,39 +1457,43 @@ trivial to add a free variable to an assertion on paper, doing so in a type-safe
 way for the ~Assertion~ type requires constructing a whole new Agda term, as the
 variable context forms part of the type.
 
+# (FIXME: describe substitution?)
+
 The ~declare~ rule is the simplest of the three remaining. The goal is to
 describe a necessary triple on ~s~ such that ~HoareTriple P Q (declare e s)~ is
 a valid correctness triple. First, note that ~P~ and ~Q~ have type ~Assertion Σ
 Γ Δ~, whilst ~s~ has type ~Statement Σ (t ∷ Γ)~ due to the declaration
 introducing a new variable. To be able to use ~P~ and ~Q~, they have to be
 weakened to the type ~Assertion Σ (t ∷ Γ) Δ~, achieved by calling ~Var.weaken
-0F~. 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~.
+0F~. I will denote the weakened forms ~P′~ and ~Q′~ for brevity. So far the
+rule's premise is ~HoareTriple P′ Q′ s~. However, this does not constrain the
+new variable. Thus an assertion that the new variable ~var 0F~ is equal to the
+initial value ~e~ must be added to the precondition. As ~e~ has type ~Expression
+Σ Γ t~ and a term in the precondition needs type ~Term Σ (t ∷ Γ) Δ t~, the Agda
+expression ~Term.Var.weaken 0F (↓ e)~, denoted ~e′~ , is used instead. This Agda
+expression converts ~e~ to a term and introduces the new variable. This leads to
+the final form of the premise: ~HoareTriple (P′ ∧ equal (var 0F) e′) Q′ s~.
 
 I will go into less detail whilst discussing ~invoke~ and ~for~, due to an even
 greater level of complexity. The ~for~ rule is the simpler case, so I will start
 there. The form of the ~for~ rule was inspired from the WHILE rule for a ~while~
 loop, but specialised to a form with a fixed number of iterations.
 
-Given a ~for n s~ statement, 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
+Given a ~for n s~ statement, a loop invariant ~I : Assertion Σ Γ (fin (suc n) ∷
+Δ)~ is chosen. The additional auxiliary variable indicates the number of
+complete iterations of the loop, from \(0\) to \(n\). I will use ~I(x)~ to
 denote the assertion ~I~ with the additional auxiliary variable replaced with
-term ~x~, and make weakening variable contexts implicit. 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.
+term ~x~, and make weakening variable contexts implicit. The rule's premise
+requires that ~P ⊆ I(0)~ and ~I(n) ⊆ Q~ to ensure that the precondition and
+postcondition are an adaptation of the loop invariant. The final part to
+consider is the correctness triple for ~s~. By adding in a new auxiliary
+variable to represent the initial value of the loop variable on each iteration,
+the current iteration number can be preserved between the precondition and
+postcondition. The loop variable itself can be modified by ~s~. By ensuring that
+the following triple holds, there is a proof that the loop preserves the
+invariant: ~HoareTriple (I(meta 0F) ∧ equal (meta 0F) (var 0F)) I(1+ meta 0F)
+s~. This ensures that ~I~ remains true across the loop iteration, for each
+possible value of the loop variable.
 
 Notice that unlike the denotational semantics, which would explicitly execute
 each iteration of a loop, the Hoare logic instead requires only a single proof
@@ -1574,24 +1503,26 @@ 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~.
+body. This is similar to reasons why converting functions calls into terms
+presented challenges, back in [[*Converting ~Expression~ into ~Term~]]. Of
+particular note, any local variables in the precondition and postcondition for a
+procedure invocation cannot be accessed nor modified by the procedure body. This
+is the inspiration for the form of the ~invoke~ rule.
+
+To construct ~HoareTriple P Q (invoke (s ∙end) es)~, first consider the form ~P~
+and ~Q~ will take in a correctness triple for ~s~. Note that local variables in
+~P~ and ~Q~ are immutable within ~s~, due to the changing local variable scope.
+Also note that the local variables cannot be accessed using ~var~; ~P~ and ~Q~
+have type ~Assertion Σ Γ Δ~, but ~s~ has type ~Statement Σ Γ′~ for some context
+~Γ′~ independent of ~Γ~. As the original local variables are immutable during
+the invocation, they can be replaced with auxiliary variables, by assigning a
+new auxiliary variable for each one. Within ~P~ and ~Q~, all ~var x~ are
+replaced with ~meta x~ to reflect that the local variables have been moved to
+auxiliary variables. This is the action performed by the ~varsToMetas~ function.
+To complete the premise, the local variables within the procedure body must be
+initially set to the invocation arguments. Like ~P~ and ~Q~, the local variables
+in ~es~ have to be replaced with the corresponding auxiliary variables. This
+substitution is done by ~termVarsToMetas~.
 
 * Properties and Evaluation of AMPSL
 
@@ -1600,7 +1531,7 @@ 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
+The other half of this chapter will give a practical attempt of using AMPSL to
 prove a proposition. I will give the AMPSL encoding of ASL form of the Barrett
 reduction algorithm given by [cite/t:@10.46586/tches.v2022.i1.482-505]. I will
 demonstrate how this works on some concrete values, and explain what work is
@@ -1609,23 +1540,18 @@ 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.
+#+caption: The theorem statement for soundness of AMPSL's Hoare Logic.
 #+begin_src agda2
 sound : P ⊢ s ⊢ Q →
         ∀ σ γ δ →
         Assertion.⟦ P ⟧ σ γ δ →
-        uncurry Assertion.⟦ Q ⟧
-          (Semantics.stmt s (σ , γ))
-          δ
+        uncurry Assertion.⟦ Q ⟧ (Semantics.stmt s (σ , γ)) δ
 #+end_src
 
 I first define what is meant by soundness. [[AMPSL-soundness-statement]] shows the
 Agda type corresponding to the proposition.
 
+#+attr_latex: :options [Soundness]
 #+begin_theorem
 Given a Hoare logic proof that \(\{P\}\;\texttt{s}\;\{Q\}\) holds, then for any
 concrete instantiation of the global, local and auxiliary variable contexts, if
@@ -1633,14 +1559,14 @@ concrete instantiation of the global, local and auxiliary variable contexts, if
 \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~.
+A proof can be given by a recursive function in Agda. Some cases in this
+function are trivial: the premise of the ~skip~ Hoare logic rule is exactly the
+proof statement needed, and the ~seq~ rule can be satisfied by composing the
+results of the inductive hypothesis on the two premises. The cases for the ~if~
+and ~if-else~ rules pattern match on the result of evaluating the condition
+expression, then it recurses into the true or false branch respectively. This
+relies on a trivial proof that the semantics of an ~Expression~ are
+propositionally equal to the semantics of that expression embedded as a ~Term~.
 
 The ~assign~ rule is also relatively simple. Because the ~Reference~ type
 excludes product references, it is sufficient to show that substituting into a
@@ -1648,8 +1574,8 @@ 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
+to the use of helper functions like variable weakening and elimination. I will
+take a quick diversion into how to prove these manipulations do not affect the
 semantics of terms and assertions before discussing how soundness is shown for
 these more complex Hoare logic rules.
 
@@ -1661,18 +1587,23 @@ these more complex Hoare logic rules.
 #+caption: variables.
 #+begin_src agda2
 module State where
-  subst     : ∀ i → Term Σ Γ Δ t → Term Σ Γ Δ (lookup Σ i) → Term Σ Γ Δ t
+  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
+  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
+  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
+  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
+  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
@@ -1685,7 +1616,7 @@ 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.
+the definition of a full homomorphism can be constructed.
 
 #+name: term-weakening
 #+caption: A record that defines the three interesting cases for weakening a
@@ -1695,7 +1626,8 @@ you can construct the definition of a full homomorphism.
 weakenBuilder : ∀ i → RecBuilder Σ Γ Δ Σ (insert Γ i t) Δ
 weakenBuilder {Γ = Γ} i = record
   { onState = state
-  ; onVar   = λ j → Cast.type (Vecₚ.insert-punchIn Γ i _ j) (var (punchIn i j))
+  ; onVar   = λ j → Cast.type (Vecₚ.insert-punchIn Γ i _ j)
+                              (var (punchIn i j))
   ; onMeta  = meta
   }
 #+end_src
@@ -1703,8 +1635,9 @@ weakenBuilder {Γ = Γ} i = record
 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.
+case, the ~state~ and ~meta~ cases are identities. The ~var~ case then
+\ldquo{}punches in\rdquo{} the new variable, wrapped in a type cast to satisfy
+Agda's dependent typing.
 
 Proving that the term manipulations are indeed homomorphisms in the semantics
 also requires fewer lines than the 320 naive cases. Like with the manipulation
@@ -1713,50 +1646,16 @@ 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
+proof is shown in [[*Example ~Term~ Homomorphism Proof]]. First I specify how to
+modify the variable contexts. The global and auxiliary variable contexts are
+unchanged, whereas a value for the weakened variable is inserted into the local
+variable context. Then I prove the homomorphism is correct on each of ~state~,
+~var~ and ~meta~. As ~state~ and ~meta~ were unchanged, the proof is trivial by
 reflexivity. The variable case is also quite simple, first proving that the
 ~Cast.type~ function is denotationally the same as a substitution, and then
-showing that fetching a "punched in" index from a list with an insertion is the
-same as fetching the original index from an unmodified list.
+showing that fetching a \ldquo{}punched in\rdquo{} index from a list with an
+insertion is the same as fetching the original index from an unmodified list.
 
 In total, these two optimisations save roughly 580 lines of Agda code in
 the definition and proofs of term manipulations. However, there are still
@@ -1766,7 +1665,7 @@ 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
+feature many trivial cases, it occurs at a much lower ratio compared to the
 amount of useful code. The second reason is that the ~all~ and ~some~
 constructors introduce new auxiliary variables. This means that the subterms of
 these constructors have a different type from other assertions, making a generic
@@ -1777,60 +1676,41 @@ 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.
+are impossible to use in propositional equality, as Agda does not allow for
+meaningful propositional equality of functions, which appear in these types.
+Instead, I prove the types are equivalent.
 
 Only three constructors for ~Assertion~ have interesting cases in these proofs.
 The ~pred~ constructor delegates the work to proofs on the ~Term~ manipulations,
-using the resulting propositional equality to safely return the input term.
+using the resulting propositional equality to safely return the input term. The
+~all~ and ~some~ constructors first have to show that homomorphisms on the inner
+assertions and other arguments preserve type equality before they can recurse.
 
 *** Soundness of ~declare~, ~for~ and ~invoke~
-Referring back to [[AMPSL-Hoare-logic]] for the Hoare logic definitions, 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.
+Referring back to [[AMPSL-Hoare-logic]] for the Hoare logic definitions, the
+soundness proof cases for the final three rules can be completed. The ~declare~
+rule is straight forward. To satisfy the recursive precondition, I instantiate
+the new auxiliary variable to the initial value of the new variable. Then, I
+prove that the weakened precondition holds, and add to it a proof that the
+additional variable is indeed the initial value of the newly-declared variable.
+Then I inductively apply soundness, to obtain a proof that the weakened
+postcondition holds. Finally, I apply the weakening proof for ~Assertion~ in
+reverse, obtaining a proof that the postcondition holds.
 
 The proof for ~for~ is much more involved, and only an outline will be given. I
 will also reuse the syntax from [[*Correctness Triples for AMPSL]] for the
-invariant.  By using the implication premises for the ~for~ Hoare logic rule, 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.
+invariant. By using the implication premises for the ~for~ Hoare logic rule, I
+can obtain a proof that ~I(0)~ holds from the proof of the initial precondition,
+and convert a proof of ~I(m)~ to a proof of the final postcondition. All that
+remains is a proof that the loop preserves the invariant.
+
+This required two parts. The first part is a proof that each individual loop
+iteration maintains the invariant. This required using a number of lemmata
+asserting that various assertion manipulations are homomorphisms, as well as a
+few type-safe substitutions. The second part was a proof that all these
+individual steps can be combined together to make a proof that the whole loop
+preserves the invariant. The soundness proof case of ~for~ totals around 220
+lines of Agda, excluding the additional lemmata.
 
 Unfortunately, the proof of soundness for ~invoke~ is currently incomplete, due
 to time constraints for the project. The proof itself should be simpler than the
@@ -1839,12 +1719,13 @@ 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.
+A general proof of correctness of the AMPSL Hoare logic rules for arbitrary
+predicates on the input and output states is impossible within Agda. There are a
+large class of predicate that fall outside the scope of what can be created
+using the ~Assertion~ type. Additionally, even if a predicate could be the
+denotational representation of an assertion, there is no algorithm to decide the
+assertion given the predicate, as there is no way to pattern match on the
+predicate type.
 
 Due to this, any statement about correctness must be given the precondition and
 postcondition assertions explicitly. This results in the following theorem
@@ -1854,17 +1735,15 @@ statement for the most general proof of correctness:
 -- impossible to prove
 correct : (∀ σ γ δ →
            Assertion.⟦ P ⟧ σ γ δ →
-           uncurry Assertion.⟦ Q ⟧
-             (Semantics.stmt s (σ , γ))
-             δ) →
+           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
+Unfortunately this also very quickly causes a problem in Agda. Consider the
+statement ~s ∙ s₁~. To prove this in AMPSL's Hoare logic, it is necessary to
+give two subproofs: ~P ⊢ s ⊢ R~ and ~R ⊢ s₁ ⊢ Q~. As input, there is a single
+function transforming proofs of the precondition to proofs of the postcondition.
+The problem occurs because there is no way to decompose this function into two
 parts, one for the first statement and another for the second.
 
 To resolve this, I anticipate that proving correctness in AMPSL's Hoare logic
@@ -1886,21 +1765,19 @@ 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
+With the additional step of proving the rule of consequence as a meta rule, a
+valid formulation for the correctness of AMPSL's Hoare logic can be given, which
 follows trivially from the four steps above:
 
 #+begin_src agda2
-correct : (∀ σ γ δ →
-           Assertion.⟦ P ⟧ σ γ δ →
-           Assertion.⟦ wp s Q ⟧ σ γ δ) →
+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
+~invoke~ cases. For ~if e then s else s₁~, I can recursively construct the
+weakest preconditions ~P~ and ~P₁~ for ~s~ and ~s₁~ respectively. The weakest
 precondition of the full statement will then be ~P ∧ e ∨ P₁ ∧ inv e~.
 
 To find the weakest precondition of a function invocation ~invoke (s ∙end) es~
@@ -1914,7 +1791,7 @@ the procedure-local variables with the arguments.
 
 ** Using AMPSL for Proofs
 
-This chapter will describe how I converted ASL representing a Barrett reduction
+This section will describe how I converted ASL representing a Barrett reduction
 implementation [cite:@10.46586/tches.v2022.i1.482-505] into AMPSL, focusing on
 the modelling choices I made. I will then discuss how to use the AMPSL code in
 concrete proofs for specific values, before concluding with the steps necessary
@@ -1922,217 +1799,44 @@ 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
+[cite:@arm/DDI0553B.s §E2.1.225] ASL functions.  ~TopLevel~ is the ASL function
+describing the actions of an architecture tick. It primarily deals with
 debugging, halt and lockup processor states, none of which are relevant for the
 Barrett reduction or NTT correctness proofs I am working towards.
 ~InstructionExecute~ deals with fetching instructions and deciding whether to
-execute an instruction "beatwise" or linearly.
-
-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
+execute an instruction beatwise or linearly.
 
 The choice of which instructions beats to schedule is in the ~ExecBeats~
-pseudocode function [cite:@arm/DDI0553B.s §E2.1.121]. 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.
+pseudocode function [cite:@arm/DDI0553B.s §E2.1.121]. My model, shown
+side-by-side in [[*Example Armv8-M Instruction Models in AMPSL]], reduces the
+scheduling part to a linear order where all beats of a beatwise instruction are
+executed in a tick.
 
 Another pseudocode function I have decided to omit is  ~DecodeExecute~. This
 performs instruction decoding as specified in Chapter C2 of
 [cite/t:@arm/DDI0553B.s §E2.1.121], and then performs the execution step
 specified further down the instruction descriptions. I instead decided to give
-~ExecBeats~ a procedure that performs the execution of a single instruction.
-
-# 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
+~ExecBeats~ a procedure that performs the execution of a single instruction, as
+decoding a known sequence of instructions is infallible.
 
 The Barrett reduction implementation by
 [cite/t:@10.46586/tches.v2022.i1.482-505] requires two instructions: ~VQRDMULH~
-and ~VMLA~. The 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
+and ~VMLA~. The AMPSL definitions are given in [[*Example Armv8-M Instruction
+Models in AMPSL]]. Like most beatwise instructions, both procedures end with a
+loop that copies the masked bytes of an intermediate result into the destination
+register. This is the action performed by the ~copyMasked~ procedure given back
 in [[*Example AMPSL Statements]].
 
 #+name: barrett-impl
 #+caption: AMPSL model of Barrett reduction.
 #+begin_src agda2
-barrett : (n : ℕ) → ⦃ NonZero n ⦄ →
-          (t z : VecReg) (im : GenReg) →
+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) ∷ []) ∙
+  ,*index R (lit im) ≔ call (sliceⁱ 0) (lit (ℤ.- n) ∷ []) ∙
   invoke vmla-s32,z,t,-n [] ∙end
   where
   vqrdmulh-s32,t,z,m =
@@ -2177,59 +1881,70 @@ 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.
+The poor performance of AMPSL's denotational semantics on this small example
+highlights the necessity of the syntax-directed Hoare logic proof system. Using
+the Hoare logic rules to attempt to directly prove that ~barrett-101~ has the
+desired effect leads to a very tedious proof of expanding out the whole
+derivation tree requiring 64 loop invariants or logical implications to
+complete.
 
 *** Proving Reusable Results
-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.
+Whilst being able to prove results about concrete computations is useful, being
+able to prove results on abstract variables is more so. As discussed in the
+previous section, the ~copyMasked~ procedure given in [[*Example AMPSL Statements]]
+is used in most Armv8-M vector instructions. Having some proofs about its
+properties would make giving the semantics of Armv8-M instructions much simpler.
 
-I attempted to do this for the ~copyMasked~ procedure given in [[*Example AMPSL
-Statements]], the type of which is given below:
+Notice that when each bit of the ~mask~ argument to the procedure is true, the
+procedure reduces to an assignment of ~x~ into the machine register ~Q[ dest ,
+beat ]~. This is reflected in the following Agda type:
 
 #+begin_src agda2
-copyMasked-mask-true : ∀ {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
+copyMasked-mask≡true : ∀ {dest x beat mask} {P Q : Assertion State Γ Δ} →
+    P ⊆ equal (↓ mask) (lit (replicate (lift Bool.true))) →
+    P ⊆ Assertion.subst Q Q[ dest , beat ] (↓ x) →
+    P ⊢ invoke copyMasked (dest ∷ x ∷ beat ∷ mask ∷ []) ⊢ Q
 #+end_src
 
-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:
+The first implication requires that the precondition ensures that the mask is
+initially true. The second implication is the same one as from the ~assign~
+Hoare logic rule, specialised for the reference ~Q[ dest , beat ]~.
+
+By using the Hoare logic rules as defined in [[*Correctness Triples for AMPSL]], the
+following incomplete Agda term for a proof skeleton can be found:
 
 #+begin_src agda2
 invoke
-  (for
-    {!!}
-    {!!}
-    (if
-      (assign {!!})
-      {!!})
-    {!!})
+  (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.
+To complete the proof, it is sufficient to fill in these four missing terms.
+These consist of: a choice of loop invariant; a proof the initial state inside
+the procedure body entails the loop condition; a proof that, given a bit in
+~mask~ is true, performing the assignment for that byte preserves the invariant; a
+proof that, given a bit in ~mask~ is false, the loop invariant is preserved; and
+a proof that the loop invariant entails the postcondition when the loop is complete.
+
+Because the loop does not change the value of the ~mask~ variable, the loop
+invariant can include an assertion that the ~mask~ is always true. This makes
+the implication for the ~else~ branch of the loop body a trivial proof by
+contradiction.
 
-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.
+The other three missing values are simple when presented for a paper proof.
+Unfortunately, the ~Assertion~ and ~Term~ manipulations applied by AMPSL's Hoare
+logic rules make formulation within Agda more complex. The full proof is
+currently incomplete due to a number of missing trivial lemmata, due to project
+time constraints.
 
 * Proof of Barrett Reduction
 
 Barrett reduction is an algorithm to find a small representative of a value
 \(z\) modulo some base \(n\). Instead of having to perform expensive integer
 division, Barrett reduction instead uses an approximation function to precompute
-a coefficient \(m = \llbracket 2^k / n \rrbracket\). The integer division \(z /
-n\) is then approximated by the value \(\left\llbracket \frac{zm}{2^k}
+a coefficient \(m = \llbracket \frac{2^k}{n} \rrbracket\). The integer division
+\(z / n\) is then approximated by the value \(\left\llbracket \frac{zm}{2^k}
 \right\rrbracket\).
 
 There are many choices of function that are suitable for the two approximations.
@@ -2261,7 +1976,8 @@ 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.
+sign-preservation, monotonicity and cancelling proofs. This totals roughly 2600
+lines of Agda.
 
 #+name: barrett-properties
 #+caption: Three properties I was able to prove about flooring Barrett reduction
@@ -2274,18 +1990,21 @@ barrett-limit    : ∀ {z} → 0ℤ ≤ z → z ≤ 2ℤ ^ k → barrett z < 2 �
 
 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.
+property states that Barrett reduction does indeed perform a modulo reduction,
+the entire purpose of the algorithm. The second ensures that the Barrett
+reduction of a positive value is remains positive, meaning that flooring Barrett
+reduction can safely use unsigned integer types. The final property states that
+for sufficiently small values of \(z\), Barrett reduction produces a
+representable no more than twice the size of the base, thus reducing values to a
+small representable module the base.
 
 * Summary and Conclusions
 
-In this work, I 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.
+In this work, I made significant progress into proving that an implementation of
+the NTT algorithm for the M-profile vector extension of the Armv8.1-M
+architecture is functionally correct. I made progress on two fronts: giving a
+formal semantics for Armv8-M instructions, and proving properties about Barrett
+reduction.
 
 To provide formal semantics for Armv8-M instructions, I designed AMSPL, a
 language with formal semantics that models the ASL used to describe instruction
@@ -2310,13 +2029,13 @@ 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.
+  be relatively straight forward, but the ~Term~  and ~Assertion~ homomorphisms
+  it performs are the most complex and still without proof.
 - Completeness of Hoare Logic :: I have only conjectured that AMPSL's Hoare
   logic is complete, in the sense given in [[*Argument for a Proof of Correctness]].
   Actually creating the weakest-precondition function requires the creation of
   more ~Term~ and ~Assertion~ homomorphisms with more complex effects, and using
-  them in proofs requires proving more trivial lemmata.
+  them in proofs requires proving trivial lemmata.
 - Evaluating Denotational Semantics :: Asking Agda to normalise the denotational
   semantics of any reasonable computation often results in Agda running out of
   memory ([[*Using AMPSL for Proofs]]). Investigating and eliminating the cause of
@@ -2327,9 +2046,10 @@ results:
   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.
+verification of Armv8-M assembly algorithms, its current state does not yet live
+up to the promise. Currently a huge push needs to be made to complete proofs of
+many of the missing lemmata which I did not have time to complete in this
+project.
 
 ** Future Work for Functional Correctness
 
@@ -2339,12 +2059,12 @@ 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.
+use of high-level functional correctness tools targetting C.
 
 Another alternative, particularly for working on pre-existing, hand-written
 assembly routines, is to model the Armv8-M semantics using Sail. Unlike AMPSL,
-Sail will the full complexity of the ASL description of instructions, allowing
-for more rigorous proofs about the program semantics.
+Sail would model the full complexity of the ASL description of instructions,
+allowing for more rigorous proofs about the program semantics.
 
 #+latex: \label{lastcontentpage}
 
@@ -2354,311 +2074,195 @@ for more rigorous proofs about the program semantics.
 
 \appendix
 
-* AMPSL Syntax Definition
+* Example ~Term~ Homomorphism Proof
+# #+name: term-weakening-proof
+# #+caption: A record that shows that ~Term.Var.weaken~ is a homomorphism that
+# #+caption: preserves semantics. Because the variable contexts change between the
+# #+caption: two sides of the homomorphism, this record has to describe how to
+# #+caption: extend the variable contexts first. Then it has to show the actions
+# #+caption: of ~Term.Var.weaken~ on global, local and auxiliary variables are
+# #+caption: indeed homomorphisms. A similar record type exists for homomorphisms
+# #+caption: that restrict the variable contexts like variable elimination.
+#+begin_src agda2
+weakenBuilder-proof : ∀ i → ⟦ t ⟧ₜ → RecBuilder⇒ (Term.Var.weakenBuilder i)
+weakenBuilder-proof {t = t} {Γ = Γ} i v = record
+  { onState⇒ = λ σ γ δ → σ
+  ; onVar⇒   = λ σ γ δ → Core.insert′ i Γ γ v
+  ; onMeta⇒  = λ σ γ δ → δ
+  ; onState-iso = λ _ _ _ _ → refl
+  ; onVar-iso   = onVar⇒
+  ; onMeta-iso  = λ _ _ _ _ → refl
+  }
+  where
 
+  onVar⇒ : ∀ j σ γ δ → _
+  onVar⇒ j σ γ δ = begin
+    Term.⟦ Term.Cast.type eq (var (punchIn i j)) ⟧ σ γ′ δ
+      ≡⟨ Cast.type eq (var (punchIn i j)) σ γ′ δ ⟩
+    subst ⟦_⟧ₜ eq (Core.fetch (punchIn i j) (insert Γ i t) γ′)
+      ≡⟨ Coreₚ.fetch-punchIn Γ i t j γ v ⟩
+    Core.fetch j Γ γ
+      ∎
+    where
+    open ≡-Reasoning
+    γ′ = Core.insert′ i Γ γ v
+    eq = Vecₚ.insert-punchIn Γ i t j
+#+end_src
+* Example Armv8-M Instruction Models in AMPSL
 #+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 Σ Γ
+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
 
-* 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
+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
 
-* AMPSL Hoare Logic Definitions
+#+begin_figure
+\begin{subfigure}[b]{0.45\textwidth}
+\begin{verbatim}
+boolean ExecBeats()
 
-#+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
+  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 =
 
-#+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
+
+
+
+  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
 
 #+latex: \label{lastpage}
 #+latex: %TC:endignore