#+options: ':t *:t -:t ::t <:t H:4 \n:nil ^:t arch:headline author:t #+options: broken-links:nil c:nil creator:nil d:(not "LOGBOOK") date:t e:t #+options: email:nil f:t inline:t num:t p:nil pri:nil prop:nil stat:t tags:t #+options: tasks:t tex:t timestamp:t title:t toc:nil todo:t |:t #+title: Semantics of an embedded vector architecture for formal verification of software #+date: May 2022 #+author: Greg Brown #+latex_header: \newcommand{\candidatenumber}{2487C} #+latex_header: \newcommand{\college}{Queens' College} #+latex_header: \newcommand{\course}{Computer Science Tripos, Part III} #+email: greg.brown@cl.cam.ac.uk #+language: en-GB #+select_tags: export #+exclude_tags: noexport #+creator: Emacs 27.2 (Org mode 9.6) #+cite_export: biblatex #+bibliography: ./thesis.bib #+latex_class: thesis #+latex_class_options: [12pt,a4paper,twoside] #+latex_header: \usepackage[hyperref=true,url=true,backend=biber,natbib=true]{biblatex} % citations #+latex_header: \usepackage[vmargin=20mm,hmargin=25mm]{geometry} % page margins #+latex_header: \usepackage[chapter]{minted} % code snippets #+latex_header: \usepackage{parskip} % vertical space for paragraphs #+latex_header: \usepackage{setspace} % line spacing #+latex_header: \usepackage{newunicodechar} % unicode in code snippets #+latex_header: \usepackage{ebproof} % Hoare logic rules #+latex_header: \usepackage{mathtools} % a math character? #+latex_header: \usepackage{stmaryrd} % some math characters #+latex_header: \usepackage{refcount} % for counting pages #+latex_header: \usepackage{upquote} % for correct quotation marks in verbatim text #+latex_header: \usepackage{caption} % not sure why this one [[https://www.overleaf.com/learn/latex/How_to_Write_a_Thesis_in_LaTeX_(Part_3)%3A_Figures%2C_Subfigures_and_Tables#Subfigures]]... #+latex_header: \usepackage{subcaption} % add subfigures #+latex_compiler: pdflatex #+latex_header: \newunicodechar{ʳ}{\ensuremath{^\texttt{r}}} #+latex_header: \newunicodechar{ˡ}{\ensuremath{^\texttt{l}}} #+latex_header: \newunicodechar{Γ}{\ensuremath{\Gamma}} #+latex_header: \newunicodechar{Δ}{\ensuremath{\Delta}} #+latex_header: \newunicodechar{Κ}{\ensuremath{K}} #+latex_header: \newunicodechar{Σ}{\ensuremath{\Sigma}} #+latex_header: \newunicodechar{γ}{\ensuremath{\gamma}} #+latex_header: \newunicodechar{δ}{\ensuremath{\delta}} #+latex_header: \newunicodechar{ε}{\ensuremath{\epsilon}} #+latex_header: \newunicodechar{λ}{\ensuremath{\lambda}} #+latex_header: \newunicodechar{σ}{\ensuremath{\sigma}} #+latex_header: \newunicodechar{ᵗ}{\ensuremath{^\texttt{t}}} #+latex_header: \newunicodechar{′}{\ensuremath{'}} #+latex_header: \newunicodechar{ⁱ}{\ensuremath{^\texttt{i}}} #+latex_header: \newunicodechar{⁺}{\ensuremath{^{+}}} #+latex_header: \newunicodechar{₁}{\ensuremath{_1}} #+latex_header: \newunicodechar{₂}{\ensuremath{_2}} #+latex_header: \newunicodechar{₃}{\ensuremath{_3}} #+latex_header: \newunicodechar{ₚ}{\ensuremath{_\texttt{p}}} #+latex_header: \newunicodechar{ₛ}{\ensuremath{_\texttt{s}}} #+latex_header: \newunicodechar{ₜ}{\ensuremath{_\texttt{t}}} #+latex_header: \newunicodechar{ℓ}{l} #+latex_header: \newunicodechar{ℕ}{\ensuremath{\mathbb{N}}} #+latex_header: \newunicodechar{ℚ}{\ensuremath{\mathbb{Q}}} #+latex_header: \newunicodechar{ℝ}{\ensuremath{\mathbb{R}}} #+latex_header: \newunicodechar{ℤ}{\ensuremath{\mathbb{Z}}} #+latex_header: \newunicodechar{⇒}{\ensuremath{\rightarrow}} #+latex_header: \newunicodechar{∀}{\ensuremath{\forall}} #+latex_header: \newunicodechar{∃}{\ensuremath{\exists}} #+latex_header: \newunicodechar{∎}{\ensuremath{\blacksquare}} #+latex_header: \newunicodechar{∘}{\ensuremath{\circ}} #+latex_header: \newunicodechar{∙}{\ensuremath{\cdot}} #+latex_header: \newunicodechar{∧}{\ensuremath{\wedge}} #+latex_header: \newunicodechar{∨}{\ensuremath{\vee}} #+latex_header: \newunicodechar{∷}{\texttt{::}} #+latex_header: \newunicodechar{≈}{\ensuremath{\approx}} #+latex_header: \newunicodechar{≉}{\ensuremath{\not\approx}} #+latex_header: \newunicodechar{≔}{\ensuremath{\coloneqq}} #+latex_header: \newunicodechar{≟}{\ensuremath{\buildrel ?\over =}} #+latex_header: \newunicodechar{≡}{\ensuremath{\equiv}} #+latex_header: \newunicodechar{≢}{\ensuremath{\not\equiv}} #+latex_header: \newunicodechar{≤}{\ensuremath{\le}} #+latex_header: \newunicodechar{≥}{\ensuremath{\ge}} #+latex_header: \newunicodechar{⊆}{\ensuremath{\subseteq}} #+latex_header: \newunicodechar{⊎}{\ensuremath{\uplus}} #+latex_header: \newunicodechar{⊔}{\ensuremath{\sqcup}} #+latex_header: \newunicodechar{⊢}{\ensuremath{\vdash}} #+latex_header: \newunicodechar{⊤}{\ensuremath{\top}} #+latex_header: \newunicodechar{⊥}{\ensuremath{\bot}} #+latex_header: \newunicodechar{⌊}{\ensuremath{\lfloor}} #+latex_header: \newunicodechar{⌋}{\ensuremath{\rfloor}} #+latex_header: \newunicodechar{⟦}{\ensuremath{\llbracket}} #+latex_header: \newunicodechar{⟧}{\ensuremath{\rrbracket}} #+latex_header: \newunicodechar{⟶}{\ensuremath{\rightarrow}} #+latex_header: \newunicodechar{⦃}{\{\{} #+latex_header: \newunicodechar{⦄}{\}\}} #+latex_header: \newunicodechar{𝕀}{\ensuremath{\mathbb{I}}} #+latex_header: \newtheorem{theorem}{Theorem} #+latex_header: %TC:envir minted 1 ignore #+latex_header: \newif\ifsubmission # Uncomment when anonymous # #+latex_header: \submissiontrue #+begin_src elisp :exports results :results none :eval export (make-variable-buffer-local 'org-latex-title-command) (setq org-latex-title-command " %%TC:ignore \\begin{sffamily} \\begin{titlepage} \\makeatletter \\hspace*{-14mm}\\includegraphics[width=65mm]{logo-dcst-colour} \\ifsubmission %% submission proforma cover page for blind marking \\begin{Large} \\vspace{20mm} Research project report title page \\vspace{35mm} Candidate \\candidatenumber \\vspace{42mm} \\textsl{\`\`\\@title\'\'} \\end{Large} \\else %% regular cover page \\begin{center} \\Huge \\vspace{\\fill} \\@title \\vspace{\\fill} \\@author \\vspace{10mm} \\Large \\college \\vspace{\\fill} \\@date \\vspace{\\fill} \\end{center} \\fi \\vspace{\\fill} \\begin{center} Submitted in partial fulfillment of the requirements for the\\\\ \\course \\end{center} \\end{titlepage} \\end{sffamily} \\makeatother \\newpage %%TC:endignore ") #+end_src #+begin_export latex %TC:ignore \begin{sffamily} Total page count: \pageref{lastpage} % calculate number of pages from % \label{firstcontentpage} to \label{lastcontentpage} inclusive \makeatletter \@tempcnta=\getpagerefnumber{lastcontentpage}\relax% \advance\@tempcnta by -\getpagerefnumber{firstcontentpage}% \advance\@tempcnta by 1% \xdef\contentpages{\the\@tempcnta}% \makeatother Main chapters (excluding front-matter, references and appendix): \contentpages~pages (pp~\pageref{firstcontentpage}--\pageref{lastcontentpage}) #+end_export #+name: wordcount #+begin_src elisp :exports none :eval export (if (not (boundp 'squid-eval)) (setq squid-eval nil)) (if (not squid-eval) (progn (setq squid-eval t) (org-latex-export-to-latex) (setq squid-eval nil))) (let* ((outfile (org-export-output-file-name ".tex"))) (shell-command-to-string (concat "texcount -0 -sum \'" outfile "\'"))) #+end_src Main chapters word count: call_wordcount() #+begin_export latex Methodology used to generate that word count: \begin{quote} \begin{verbatim} $ texcount -0 -sum report.tex xyz \end{verbatim} \end{quote} \end{sffamily} \onehalfspacing #+end_export * Abstract :PROPERTIES: :unnumbered: t :END: The ultimate goal of this work is to formally verify an implementation [cite:@10.46586/tches.v2022.i1.482-505] of the number-theoretic transform (NTT) for the Armv8.1-M architecture. This report focuses on producing the first formalisation of the semantics of the Armv8-M architecture and its M-profile vector extension. The pseudocode used to describe the instructions within the manual by [cite/t:@arm/DDI0553B.s] does not have a formal semantic description. I designed AMPSL, to mock the Arm specification language, within in Agda. The syntax closely follows that of ASL, save some minor modifications due to limitations within Agda and adjustments to simplify the semantics. This report describes both a denotational semantics and Hoare logic for AMPSL. The denotational semantics interprets AMPSL statements and expressions as Agda functions on a variable context. The Hoare logic instead provides a syntax-directed derivation of AMPSL's action on assertions about the execution state. I also use Agda to formally verify a variant of Barrett reduction. Barrett reduction is an important subroutine used by the NTT, to efficiently find a \ldquo{}small\rdquo{} representable of a value modulo some base [cite:@10.1007/3-540-47721-7_24]. Formalising Barrett reduction is a big step in formalising the NTT. #+latex: \ifsubmission\else * Acknowledgements :PROPERTIES: :unnumbered: t :END: I would like to thank Dominic Mulligan, Hanno Becker and Gustavo Petri at Arm for the initial idea and producing valuable feedback on my project and report throughout the year. I would also like to thank Jeremy Yallop for supervising the project and providing support throughout the project. They also provided useful and actionable feedback on the various drafts of my report. #+latex: \fi #+latex: \cleardoublepage #+toc: headlines 2 # #+toc: listings # #+toc: tables #+latex: %TC:endignore * Introduction #+latex: \label{firstcontentpage} The ultimate goal of this work is to formally verify an implementation [cite:@10.46586/tches.v2022.i1.482-505] of the number-theoretic transform (NTT) for the Armv8.1-M architecture. The NTT is a vital procedure for lattice-based post-quantum cryptography. PQC is a type of cryptography immune to rapid attack by large-scale quantum computers. Armv8-M is a common architecture in embedded devices. Due to the resource-constrained nature of an embedded device, and the huge computational demands of post-quantum cryptography, algorithms like the NTT are presented using hand-written, highly-optimised assembly code. To ensure the correctness of these cryptographic algorithms, and thus the security of embedded devices, formal verification of these algorithms is necessary. This report focuses on producing the first formalisation of the semantics of the Armv8-M architecture, in particular its M-profile vector extension. [cite/t:@arm/DDI0553B.s] provides a pseudocode description of the operation of Armv8-M instructions using the Arm pseudocode (henceforth ASL). Unfortunately this language is primarily designed for describing instructions [cite:@arm/DDI0553B.s §E1.1.1] and not proving properties of their semantics. To remedy this, I designed AMPSL (Arm M-profile Pseudocode Specification Language, or AMPSL Mocks Pseudocode Specification Language), which mocks the Arm pseudocode specification language. AMPSL is written in Agda, a dependently-typed proof assistant [cite:@10.1007/978-3-642-03359-9_6]. The syntax mirrors that of ASL, save some minor modifications due to limitations within Agda and adjustments to simplify the semantics. AMPSL is given semantics in two different forms. The first is a denotational semantics, which converts the various program elements into functions within Agda. This enables the explicit computation of the effect of AMPSL on the processor state. AMPSL also has a set of Hoare logic rules, which form an axiomatic, syntax-directed approach to describing how a statement in AMPSL modifies assertions on the processor state. Due to AMPSL's similarity to ASL, I can convert the ASL description of Armv8-M instructions into AMPSL. From this AMPSL description of the Armv8-M instructions, I can derive the semantics of Armv8-M instructions using AMPSL's semantics. I also use Agda to formally verify a variant of Barrett reduction. Barrett reduction is an important subroutine used by the NTT, to efficiently find a \ldquo{}small\rdquo{} representable of a value modulo some base [cite:@10.1007/3-540-47721-7_24]. Much like how a formalisation of the NTT is a big step in formalising the behaviour of many PQC algorithms, formalising Barrett reduction is a big step in formalising the NTT. #+name: raw_progress #+begin_src dot :file progress.pdf :exports none digraph { node [shape=box]; A [label="Functional correctness\nof NTT",style=dotted]; B [label="Functional correctness\nof Barrett reduction",style=dotted]; C [label="NTT properties",style=dotted]; D [label="Armv8-M Instruction\nsemantics",style=dashed]; E [label="Barrett reduction\nproperties"]; F [label="AMPSL semantics"]; G [label="AMPSL properties",style=dashed]; H [label="Model of Armv8-M\nin AMPSL"]; H -> D; G -> B; F -> G; F -> D; E -> C [style=dashed]; E -> B; D -> B; C -> A; B -> A [style=dashed]; } #+end_src #+name: progress #+caption: Progress made towards formalising an implementation of NTT for the #+caption: Armv8.1-M architecture. Work completed in this report has a solid #+caption: outline. Items where only trivial, time-consuming work is left have a #+caption: dashed border. Work with no significant progress made has a dotted #+caption: border. call_raw_progress() [[progress]] shows the progress this work has made to verifying an implementation of the NTT for Armv8.1-M vector extension. Whilst it does not achieve the final goal, it forms the foundations towards it. The main contributions of this report are as follows: - In [[*AMPSL Syntax]], I introduce the syntax of the AMPSL programming language. The primary goal of the syntax is to facilitate easy translation of programs from ASL, detailed in [[*Arm Pseudocode]] into AMPSL, whilst allowing AMPSL semantics to remain simple. - The semantics of AMPSL are described in [[*AMPSL Semantics]]. The primary achievement of this work is the simple semantics of AMPSL, which facilitates straight-forward proofs about various AMPSL programs. I detail both a denotational semantics and a Hoare logic for AMPSL. - In [[*Soundness of AMPSL's Hoare Logic]], I prove that the set of Hoare logic rules for AMPSL are sound with respect to the denotational semantics. The Hoare logic used by AMPSL somewhat varies from the traditional presentation, given in [[*Hoare Logic]], to enforce that Hoare logic proofs have bounded depth with respect to the program syntax. This proof is possible due to Agda's foundation of Martin-Löf's type theory, the significance of which is given in [[*Agda]]. Due to the soundness of AMPSL's Hoare logic, the behaviour of the computationally-intensive denotational semantics can instead be specified using syntax-directed Hoare logic. - A number of example proofs for AMPSL programs are given in [[*Using AMPSL for Proofs]]. This describes how AMPSL is used to give the semantics of Armv8.1-M instructions. It also demonstrates the viability of using AMPSL for the formal verification of a number of programs, and lays the groundwork for the formal verification of the NTT given by [cite/t:@10.46586/tches.v2022.i1.482-505]. - Finally, a formal proof of a Barrett reduction variant is given in [[*Proof of Barrett Reduction]]. To my knowledge this is the first such machine-verified proof of correctness for Barrett reduction. Further, it is the first proof of Barrett reduction on a domain other than integers and rationals. * Background ** Arm Pseudocode ASL is a strongly-typed imperative programming language [cite:@arm/DDI0553B.s §E1.2.1]. It has a first-order type system, a small set of operators and basic control flow, as you would find in most imperative languages. Its primary purpose is to explain how executing an Armv8-M instruction modifies the visible processor state. As it is a descriptive aid, ASL features a number of design choices atypical of other imperative programming languages making execution difficult. Something common to nearly all imperative languages is the presence of a primitive type for Booleans. Other typical type constructors are tuples, structs, enumerations and fixed-length arrays. Two interesting primitive types used by ASL are mathematical integers and real numbers. Other imperative languages typically use fixed-width integers and floating point rationals as efficient approximations for these values, with the downside of having overflow and precision loss errors. As ASL is for specification over execution, the efficiency of code is of no concern so using the mathematical types prevents a whole class of errors. The final primitive type used by ASL is the bitstring; a fixed-length sequence of 0s and 1s. Some readers may wonder what the difference is between this type and arrays of Booleans. The justification given by [cite/t:@arm/DDI0553B.s §E1.2.2] is more philosophical than practical: \ldquo{}bitstrings are the only concrete data type in pseudocode\rdquo{}. In some places, bitstrings can be used instead of integers in arithmetic operations, by first converting them to an unsigned integer. ASL types have all of the associated standard operations, including equality, ordering, Boolean connectives and arithmetic. The most interesting operation in ASL is bitstring slicing. First, there is no type for a bit outside a bitstring---a single bit is represented as a bitstring of length one---so bitstring slicing always returns a bitstring. Slicing then works in much the same way as array slicing in languages like Python and Rust; slicing an integer range from a bitstring returns a new bitstring with values corresponding to the indexed bits. The other special feature of bitstring slicing is that an integer can be sliced instead of a bitstring. In that case, ASL \ldquo{}treats an integer as equivalent to a sufficiently long [\ldots] bitstring\rdquo{} [cite:@arm/DDI0553B.s §E1.3.3]. The final interesting difference between ASL and most imperative languages is the variety of top-level items. ASL has three forms of items: procedures, functions and array-like functions. Procedures and functions behave like procedures and functions of other imperative languages. The arguments to them are passed by value, and the only difference between the two is that procedures do not return values whilst functions do [cite:@arm/DDI0553B.s §E1.4.2]. Array-like functions act as getters and setters for machine state. Every array-like function has a reader form, and most have a writer form. This distinction exists because \ldquo{}reading from and writing to an array element require different functions\rdquo{}, [cite:@arm/DDI0553B.s §E1.4.2], likely due to the nature of some machine registers being read-only instead of read-writeable. The writer form acts as one of the targets of assignment expressions, along with variables and the result of bitstring concatenation and slicing [cite:@arm/DDI0553B.s §E1.3.5]. Examples of ASL are given throughout the report, often alongside an AMPSL model of it. ** M-profile Vector Extension The M-profile vector extension adds vector instructions to the Armv8-M architecture. A vector in this case is a 128-bit register, logically split into four 32-bit beats. Each beat is then divided into one, two or four lanes each of 32, 16 or 8 bits respectively [cite:@arm/DDI0553B.s §B5.3]. A processor can execute either one, two or four instruction beats in an \ldquo{}architecture tick\rdquo{}, an atomic unit of processor time [cite:@arm/DDI0553B.s §\(\texttt{I}_\texttt{PCBB}\)]. The number of beats executed per instruction can also change throughout execution. Vector instructions can also overlap during execution. To summarise the overlap rules, vector instructions can overlap if there are no inter-beat data dependencies, at least beats of the current instruction are complete and at most two beats of the next instruction are complete. ** Hoare Logic Hoare logic is a proof system for programs written in imperative programming languages. At its core, the logic describes how to build partial correctness triples, which describe how program statements affect assertions about machine state. The bulk of a Hoare logic derivation is dependent only on the syntax of the program the proof targets. A partial correctness triple is a relation between a precondition \(P\), a program statement \(s\) and a postcondition \(Q\). If \(\{P\} s \{Q\}\) is a partial correctness triple, then whenever \(P\) holds for some machine state, then when executing \(s\), \(Q\) holds for the state after it terminates [cite:@10.1145/363235.363259]. This is a /partial/ correctness triple because the postcondition only holds if \(s\) terminates. When all statements terminate, this relation is called a correctness total triple. #+name: WHILE-Hoare-logic #+caption: Hoare logic rules for the WHILE language. #+begin_figure \begin{center} \begin{prooftree} \infer0[SKIP]{\{P\}\;\texttt{s}\;\{P\}} \infer[rule style=no rule,rule margin=3ex]1{\{P\}\;\texttt{s₁}\;\{Q\}\qquad\{Q\}\;\texttt{s₂}\;\{R\}} \infer1[SEQ]{\{P\}\;\texttt{s₁;s₂}\;\{Q\}} \infer0[ASSIGN]{\{P[\texttt{x}/\texttt{v}]\}\;\texttt{x:=v}\;\{P\}} \infer[rule style=no rule,rule margin=3ex]1{\{P \wedge \texttt{e}\}\;\texttt{s₁}\;\{Q\}\qquad\{P \wedge \neg \texttt{e}\}\;\texttt{s₂}\;\{Q\}} \infer1[IF]{\{P\}\;\texttt{if e then s₁ else s₂}\;\{Q\}} \infer[rule style=no rule,rule margin=3ex]2{\{P \wedge \texttt{e}\}\;\texttt{s}\;\{P\}} \infer1[WHILE]{\{P\}\;\texttt{while e do s}\;\{P \wedge \neg \texttt{e}\}} \infer[rule style=no rule,rule margin=3ex]1{\models P_1 \rightarrow P_2\qquad\{P_2\}\;\texttt{s}\;\{Q_2\}\qquad\models Q_2 \rightarrow Q_1} \infer1[CSQ]{\{P_1\}\;\texttt{s}\;\{Q_1\}} \end{prooftree} \end{center} #+end_figure [[WHILE-Hoare-logic]] shows the rules Hoare introduced for the WHILE language [cite:@10.1145/363235.363259]. There are two broad classes of Hoare logic rules. Structural rules that reflect how program syntax affects execution of a program, and thus how to modify the precondition and postcondition assertions accordingly. Adaptation rules use the same statement in the premise and conclusion. They only adapt the preconditions and postconditions used. Of the structural rules, the SKIP and SEQ rules reflect the idea that the skip statement has no effect on state, and sequencing statements composes their effects. The IF rule is also uncomplicated. No matter which branch we take, the postcondition remains the same; an if statement does no computation after executing a branch. Which branch we take depends on the value of ~e~. Because the value of ~e~ is known before executing a branch, it is added to the preconditions in the premises. The ASSIGN rule is perhaps the most unintuitive of the structural rules. In the postcondition, any use of ~x~ can be replaced by ~v~ and due to the nature of the assignment the assertion maintains its truth value. In the precondition, ~x~ could have any value, so by applying the substitution of ~v~ for ~x~ to the precondition, we fact that ~x~ changes value is irrelevant. The final structural Hoare logic rule for the WHILE language is the WHILE rule. This rule can be derived by observing the fixed-point nature of a while statement. As ~while e do s~ is equivalent to ~if e then (s ; while e do s) else skip~, we can use the IF, SEQ and SKIP rules to solve the recursion equation for the precondition and postcondition of the while statement. The only adaptation rule in the Hoare logic of WHILE is the rule of consequence, CSQ. The rule of consequence is necessary in this Hoare logic so that the assertions can be manipulated into forms suitable for use by each structural rule. Other forms of Hoare logic, like the one for AMPSL given in [[*Hoare Logic Semantics]], make the rule of consequence redundant. [cite/t:@10.1145/363235.363259] does not specify the logic used to evaluate the implications in the rule of consequence. Regular choices are first-order logic and higher-order logic [cite:@10.1007/s00165-019-00501-3;@10.1007/s001650050057]. For specifying program behaviour, one vital aspect of the choice of logic is the presence of auxiliary variables [cite:@10.1007/s001650050057]. Auxiliary variables are a set of variables that cannot be used within a program, but they can be quantified over within assertions or left as free variables. A free auxiliary variable remains constant between the precondition and postcondition, and are universally-quantified within proofs. ** Agda Agda is a dependently-typed proof assistant and functional programming language, based on Martin-Löf's type theory [cite:@10.1007/978-3-642-03359-9_6]. [cite/t:@10.1007/978-3-642-03359-9_6] provide an excellent introduction to the language. I will now summarise the most important features of Agda for the implementation of AMPSL. *Inductive families*. Agda generalises ML-style datatypes allowing them to be indexed by values as well as types. This is best illustrated by an example. Take for instance fixed-length vectors. They can be defined by the following snippet: #+begin_src agda2 data Vec (A : Set) : ℕ → Set where [] : Vec A 0 _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n) #+end_src Note the type of ~Vec~. It is a function that accepts a type ~A~ and a natural number, and returns a type. The position of ~A~ to the left of the colon is significant; it is a /parameter/ of ~Vec~ instead of an /index/. Parameters are required to be the same for all constructors, whilst indices can vary between constructors [cite:@agda.readthedocs.io p. \texttt{language/data-types.html}]. Whilst the value of parameters is constant in the return values of constructors, they can vary across the arguments of constructors, even for the same type. One example of this is the ~Assertion~ type given in [[*Hoare Logic Assertions]] later in the report. The ~all~ and ~some~ constructors both accept an ~Assertion Σ Γ (t ∷ Δ)~, but because they return an ~Assertion Σ Γ Δ~ the definition is valid. *Propositional equality*. One very important datatype in Agda is propositional equality, shown in the following snippet: #+begin_src agda2 data _≡_ {A : Set} : A → A → Set where refl : ∀ {x} → x ≡ x #+end_src As the only constructor, ~refl~, requires that the two values are identical, whenever there is a term of ~x ≡ y~ then ~x~ and ~y~ have the same value. One useful elimination of propositional equality is in the ~subst~ function: #+begin_src agda2 subst : (B : A → Set) → x ≡ y → B x → B y subst _ refl Bx = Bx #+end_src Given a proof that two values are equal, this function lets you use dependant values for one type in place of the other. *Parameterised modules and records*. Agda modules can accept parameters, which can be used anywhere in the module. This works well with Agda's record types, whose fields are able to depend on values of other fields. The following snippet shows how records can be used to define a monoid: #+begin_src agda2 record Monoid ℓ : Set (ℓsuc ℓ) where infixl 5 _∙_ field Carrier : Set ℓ _∙_ : Op₂ Carrier ε : Carrier ∙-cong : ∀ {x y u v} → x ≡ y → u ≡ v → x ∙ y ≡ u ∙ v ∙-assoc : ∀ {x y z} → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z) ∙-idˡ : ∀ {x} → ε ∙ x ≡ x ∙-idʳ : ∀ {x} → x ∙ ε ≡ x #+end_src This record bundles together an underlying ~Carrier~ type with a binary operator ~_∙_~ and identity element ~ε~. It also contains all the proofs necessary to show that ~_∙_~ and ~ε~ form a monoid. Note that unlike the previous ~Vec~ example, ~Set~ has now been given a parameter. This is to encode different universe levels within Agda. As ~Set~ is a type within Agda, it must itself have a type. If ~Set~ was within ~Set~, we would be subject to a logical inconsistency known as Girard's paradox [cite:@cs.cmu.edu/girard-72-thesis]. Thus, ~Set~ has type ~Set 1ℓ~, and ~Set i~ has type ~Set (ℓsuc i)~. When a module is parameterised by a ~Monoid~, then the module has an abstract monoid. It can use the structure and laws given in the record freely, but it cannot use additional laws (e.g. commutativity) without an additional argument. This is useful when the operations and properties of a type are well-defined, but a good representation is unknown. *Instance arguments* Instance arguments are analogous to the type class constraints you find in Haskell [cite:@agda.readthedocs.io p. \texttt{language/instance-arguments.html}]. They are a special form of implicit argument that are solved via /instance resolution/ over unification. Instance arguments are a good solution for cases where Agda tries \ldquo{}too hard\rdquo{} to find a solution for implicit arguments, and needs the implicit arguments to be specified implicitly. Using instance arguments instead can force a particular solution onto Agda without needing to give the arguments explicitly. * Related Work There exist a multitude of formal verification tools designed to describe either the semantics of ISA instructions or prove the correctness of algorithms. This section describes some of the most significant work in the field and how the design of AMPSL improves upon it. ** Sail Sail [cite:@10.1145/3290384] is a language for describing the instruction-set architecture semantics of processors. It has a syntax similar to the pseudocode specification of most architectures and a first-order type system with dependent bitvector and numeric types. It is officially used by [cite/t:@riscv/spec-20191213] to specify the concurrent memory semantics of the RISC-V architecture. Sail has many different backends available, including sequential emulators, concurrency models and theorem-prover definitions. Further, there are tools to automatically translate documents from the Arm Specification Language into Sail [cite:@10.1145/3290384]. Despite the many advantages of Sail over other solutions, including the creation of AMPSL, using Sail in this project is not suitable for a number of reasons. First is a lack of documentation for the Sail theorem-proving backends. Without prior knowledge in using Sail, deciphering the automatically-generated statements from Sail would likely consume more time than the creation of AMPSL. Another reason to avoid Sail is the unnecessary complexity in modelling the ISA semantics. One of Sail's highlights is in its description of the memory model of architectures. However, this work attempts to verify the functional correctness of NTT, an algorithm with very little memory usage. The creation of a simpler language like AMPSL removes the need to reason about these complex memory interactions and focus on the computation itself. ** Other Functional Correctness Tools There are a number of existing tools for proving the functional correctness of programs. These include tools that target C such as CryptoLine [cite:@10.1145/3319535.3354199], Fiat Crypto [cite:@10.1109/SP.2019.00005], Frama-C [cite:@10.1007/s00165-014-0326-7] and VST [cite:@10.1007/978-3-642-19718-5_1], as well as tools that target assembly directly such as Jasmin [cite:@10.1145/3133956.3134078] and Vale [cite:@10.1145/3290376]. There are three distinct problems with using these tools to verify the functional correctness of the pre-existing NTT implementation for Armv8-M: - None of these tools accept assembly as an input language. This means they are unable to verify an existing assembly algorithm. - None of these tools target Armv8-M assembly as output. Jasmin and Vale, whilst targeting assembly, do not currently target the Armv8-M architecture, let alone the M-profile vector extension. The other tools target C and require the use of a verified compiler, of which none currently target Armv8-M. - Final point? The most similar tool to what this project is trying to achieve is a formal verification tool by [cite:@10.1145/3391900], which targets the REDFIN instruction set. REDFIN has much less complex semantics than Armv8-M, to the point where the semantics can be expressed directly without the need for a specification language. * Design of AMPSL and its Semantics In this chapter I introduce AMPSL, an Agda embedding of ASL. I also describe the semantics of AMPSL via a denotational semantics interpreting AMPSL expressions and statements as Agda functions One downside of denotational semantics is that control flow for looping constructs is fully evaluated. This is inefficient for loops that undergo many iterations. This can be resolved by a syntax-directed Hoare logic for AMPSL. Hoare logic derivations assign a precondition and a postcondition assertion to each statement. These are chained together though a number of simple logical implications. ** AMPSL Syntax AMPSL is a language similar to the Armv8-M pseudocode specification language written entirely in Agda. Unfortunately, ASL has a number of small features that make it difficult to work with in Agda directly. AMPSL makes a number of small changes to ASL to better facilitate this embedding, typically generalising existing features of ASL. *** AMPSL Types #+name: AMPSL-types #+caption: The Agda datatype representing the primitive AMPSL types. #+attr_latex: :float t #+begin_src agda2 data Type : Set where bool : Type int : Type fin : (n : ℕ) → Type real : Type tuple : Vec Type n → Type array : Type → (n : ℕ) → Type #+end_src [[AMPSL-types]] gives the Agda datatype representing the types of AMPSL. Most of these have a direct analogue to ASL types. For example, ~bool~ is a Boolean, ~int~ mathematical integers, ~real~ is for mathematical real numbers and ~array~ constructs array types. Instead of an enumeration construct, AMPSL uses the ~fin n~ type, representing a finite set of ~n~ elements. Similarly, structs are represented by ~tuple~ types. The most significant difference between ASL and AMPSL is the representation of bitstrings. Instead of a bitstring type of ASL, AMPSL uses arrays of Booleans. This lets AMPSL generalise a number of ASL operations and makes AMPSL more expressive. ASL specifies three different properties of types: equality comparisons, order comparisons and arithmetic operations. Whilst using any of the relevant operations in AMPSL requires a proof that the types have the required property, using instance arguments allows for these proofs to be elided in almost all cases. AMPSL has only two differences in types that satisfy these properties compared to ASL. First, all array types have equality as long as the enumerated type also has equality. This is a natural generalisation of the equality between types, and allows for the AMPSL formulation of bitstrings as arrays of Booleans to have equality. Secondly, finite sets also have ordering. This change is primarily a convenience feature for comparing finite representing a subset of integers. As ASL has no ordering comparisons between enumerations, this causes no problems for converting pseudocode programs into AMPSL. The final interesting feature of the types in AMPSL is implicit coercion for arithmetic. As ASL arithmetic is polymorphic for integers and reals, AMPSL needs a function to decide the type of the result. By describing the output type as a function on the input types, the same constructor can be used for all combinations of numeric inputs. *** AMPSL Expressions #+name: AMPSL-literalType #+caption: Mappings from AMPSL types into Agda types for specifying literals. #+begin_src agda literalType : Type → Set literalType bool = Bool literalType int = ℤ literalType (fin n) = Fin n literalType real = ℤ literalType (tuple ts) = literalTypes ts literalType (array t n) = Vec (literalType t) n #+end_src Unlike ASL, where only a few types have literal expressions, every type in AMPSL has a literal form. This mapping is part of the ~literalType~ function, given in [[AMPSL-literalType]]. Most AMPSL literals accept the corresponding Agda type as a value. For instance, ~bool~ literals are Agda Booleans, and ~array~ literals are fixed-length Agda vectors of the corresponding underlying type. The only exception to this rule is for ~real~ values. As Agda does not have a type representing mathematical reals, integers are used instead. This is sufficient as any real value occurring in the ASL of [cite:@arm/DDI0553B.s] is rational. #+name: AMPSL-expr-prototypes #+caption: Declarations of the Agda embeddings of the AMPSL program elements. #+attr_latex: :float t #+begin_src agda data Expression (Σ : Vec Type o) (Γ : Vec Type n) : Type → Set data Reference (Σ : Vec Type o) (Γ : Vec Type n) : Type → Set data LocalReference (Σ : Vec Type o) (Γ : Vec Type n) : Type → Set data Statement (Σ : Vec Type o) (Γ : Vec Type n) : Set data LocalStatement (Σ : Vec Type o) (Γ : Vec Type n) : Set data Function (Σ : Vec Type o) (Γ : Vec Type n) (ret : Type) : Set data Procedure (Σ : Vec Type o) (Γ : Vec Type n) : Set #+end_src #+name: AMPSL-grammar #+caption: Grammar of AMPSL. The formal Agda definition is in #+caption: [[*AMPSL Syntax Definition]]. #+begin_figure \begin{align*} \mathrm{Natural}\;{}n = & \texttt{0} \mid \texttt{suc}\;{}n \\ \mathrm{Fin}\;{}i = & \texttt{0F} \mid \texttt{suc}\;{}i \\ \mathrm{LocalReference}\;{}R = & \texttt{var}\;{}i \mid \\ & \texttt{[}\;{}R\;{}\texttt{]} \mid \texttt{unbox}\;{}R \mid \texttt{cast eq}\;{}e \\ & \texttt{merge}\;{}R\;{}R\;{}R \mid \texttt{slice}\;{}R\;{}R \mid \texttt{cut}\;{}R\;{}R \mid \\ & \texttt{head}\;{}R \mid \texttt{tail}\;{}R \\ \mathrm{Reference}\;{}r = & \textrm{Like LocalReference} \mid \texttt{state}\;{}i\\ \mathrm{Expression}\;{}e = & \textrm{Like Reference} \mid \texttt{lit}\;{}x \mid e\;{}\texttt{≟}\;{}e \mid e\;{}\texttt{>}\;{}n \mid e\;{}\texttt{\textasciicircum}\;{}n \mid \texttt{rnd}\;{}e \mid \\ & \texttt{fin}\;{}f\;{}e \mid \texttt{asInt}\;{}e \mid \\ & \texttt{nil} \mid \texttt{cons}\;{}e\;{}e \mid \\ & \texttt{call}\;{}F\;{}es \mid \texttt{if}\;{}e\;{}\texttt{then}\;{}e\;{}\texttt{else}\;{}e \\ \mathrm{LocalStatement}\;{}S = & \texttt{skip} \mid S\;{}\texttt{∙}\;{}S \mid R\;{}\texttt{≔}\;{}e \mid \\ & \texttt{declare}\;{}e\;{}S \mid \texttt{for}\;{}n\;{}S \mid \\ & \texttt{if}\;{}e\;{}\texttt{then}\;{}S \mid \texttt{if}\;{}e\;{}\texttt{then}\;{}S\;{}\texttt{else}\;{}S \\ \mathrm{Statement}\;{}s = & \textrm{Like LocalStatement} \mid \\ & r\;{}\texttt{≔}\;{}e \mid \texttt{invoke}\;{}P\;{}es \\ \mathrm{Function}\;{}F = & \texttt{init}\;{}e\;{}\texttt{∙}\;{}S\;{}\texttt{end} \\ \mathrm{Procedure}\;{}P = & s\;{}\texttt{∙end} \end{align*} #+end_figure [[AMPSL-expr-prototypes]] lists the declarations of the Agda data types corresponding to the AMPSL program elements. A summary of the grammar is in [[AMPSL-grammar]] with the full definitions being given in [[*AMPSL Syntax Definition]]. Each type is parameterised by two variable contexts: Σ for global variables and Γ for local variables. The two variable contexts are split to simplify the types for function calls and procedure invocations. As the set of global variables does not change across a program, functions and procedures keep the same value of parameter Σ in their types. As functions and procedures have different local variables than the calling context, having the local variable context as a separate parameter makes the change simple. An ~Expression~ in AMPSL corresponds to expressions in ASL. Many operators are identical to those in ASL (like ~+~, ~*~, ~-~), and others are simple renamings (like ~≟~ instead of ~==~ for equality comparisons). Unlike ASL, where literals can appear unqualified, AMPSL literals are introduced by the ~lit~ constructor. The most immediate change for programming in AMPSL versus ASL is how variables are handled. Because the ~Expression~ type carries fixed-length vectors listing the AMPSL types of variables, a variable is referred to by its index into the context. For example, a variable context \(\{x \mapsto \mathrm{int}, y \mapsto \mathrm{real}\}\) is represented in AMPSL as the context ~int ∷ real ∷ []~. The variable \(x\) is then represented by ~var 0F~ in AMPSL, where the ~F~ indicates the index is from a finite set. Because the global and local variable contexts are disjoint for the ~Expression~ type, variables are constructed using ~state~ or ~var~ respectively. Whilst this decision makes programming using AMPSL more complex, it greatly simplifies the language for use in constructing proofs. This method of referring to variables by an index over a name is also commonly used in compiler construction. AMPSL expressions also add a number of useful constructs to ASL. One such pair is ~[_]~ and ~unbox~, which construct and destruct an array of length one respectively. Others are ~fin~, which allows for arbitrary computations on elements of finite sets, and ~asInt~, which converts a finite value into an integer. The final three AMPSL operators of note are ~merge~, ~slice~ and ~cut~. These all perform operations on arrays, by either merging two together, taking out a slice, or cutting out a slice. Unlike ASL where bitstring slicing requires a range, these three operators use Agda's dependent types and type inference so that only a base offset is necessary. ~slice xs i~, like bitstring slicing, extracts a contiguous subset of values from an array ~xs~, such that the first element in ~slice xs i~ is in ~xs~ at position ~i~. ~cut xs i~ returns the remainder of ~slice xs i~; the two ends of ~xs~ not in the slice, concatenated. Finally, ~merge xs ys i~ joins ~xs~ and ~ys~ to form a product-projection triple. The ~Reference~ type is the name AMPSL gives to assignable expressions from ASL. The ~LocalReference~ type is identical to ~Reference~, except it does not include global variables. Due to complications in the semantics of multiple assignments to one location, \ldquo{}product\rdquo operations like ~merge~ and ~cons~ are excluded from being references, despite concatenated bitstrings and tuples being assignable expressions in ASL. Whilst [cite:@arm/DDI0553B.s §E1.3.3] requires that no position in a bitstring is referenced twice, enforcing this in AMPSL for ~merge~ and ~cons~ would make their use unergonomic in practice for writing code or proofs. **** Example AMPSL Expressions One arithmetic operator used in ASL is left shift. [cite:@arm/DDI0553B.s §E1.3.4] explains how this can be encoded using other arithmetic operators in AMPSL, as shown below: #+begin_src agda2 _<<_ : Expression Σ Γ int → (n : ℕ) → Expression Σ Γ int e << n = e * lit (ℤ.+ (2 ℕ.^ n)) #+end_src There is a lot of hidden complexity here. First, consider the type of the literal statement. The unary plus operation tells us that the literal is an Agda integer. However, there are two AMPSL types with Agda integers for literal values: ~int~ and ~real~. How does Agda correctly infer the type? Recall that multiplication is polymorphic in AMPSL, with the result type determined by implicit coercion. Agda knows that the multiplication must return an ~int~, and that the first argument is also an ~int~, so it can infer that the second multiplicand is an integer literal. Another pseudocode operation not yet described in AMPSL is integer slicing. Here is an expression that slices a single bit from an integer, following the procedure by [cite/t:@arm/DDI0553B.s §E1.3.3]: #+begin_src agda2 getBit : ℕ → Expression Σ Γ int → Expression Σ Γ bit getBit i x = inv (x - ((x >> suc i) << suc i) > toℕ esize in let result′,sat = call (SignedSatQ (toℕ esize-1) (value ∷ [])) in let sat = head (tail result′,sat) in let result′ = head result′,sat in ,*index-32 size result i ≔ result′ ∙ if sat && hasBit elmtMask (fin e*esize>>3 (tup (i ∷ []))) then FPSCR-QC ≔ lit true )) ∙ invoke copyMasked (lit acc ∷ result ∷ curBeat ∷ elmtMask ∷ []) ))) ∙end where open Instr.VQRDMULH d op₂ = -- let elmtMast = head (tail (var 3F)) in let curBeat = head (var 3F) in -- let op₁ = var 2F in -- let result = var 1F in let i = var 0F in [ (λ src₂ → index-32 size (index (! R) (lit src₂)) i) , (λ src₂ → index-32 size (! Q[ lit src₂ , curBeat ]) i) ]′ src₂ rVal = lit 1ℤ << toℕ esize-1 #+end_src # FIXME: side by side code? #+name: vmla #+caption: Definition of the ~VMLA~ instruction. #+begin_src agda2 vmla : Instr.VMLA → Procedure State [] vmla = declare (call GetCurInstrBeat []) ( -- let elmtMask = head (tail (var 0F)) in let curBeat = head (var 0F) in declare (! Q[ lit src₁ , curBeat ]) ( declare (lit (Vec.replicate false)) ( let elmtMask = head (tail (var 2F)) in let curBeat = head (var 2F) in -- let op₁ = var 1F in let result = var 0F in for (toℕ elements) ( let curBeat = head (var 3F) in let op₁ = var 2F in let element₁ = call sint (index-32 size op₁ i ∷ []) in let result = var 1F in let i = var 0F in let op₂ = ! Q[ lit acc , curBeat ] in let element₃ = call sint (index-32 size op₂ i ∷ []) in ,*index-32 size result i ≔ call (sliceⁱ 0) ((element₁ * element₂ + element₃) ∷ []) )) ∙ invoke copyMasked (lit acc ∷ result ∷ curBeat ∷ elmtMask ∷ []) )) ∙end where open Instr.VMLA d element₂ = call sint (index-32 size (index (! R) (lit src₂)) (lit 0F) ∷ []) #+end_src The Barrett reduction implementation by [cite/t:@10.46586/tches.v2022.i1.482-505] requires two instructions: ~VQRDMULH~ and ~VMLA~. The ASL and AMPSL definitions are given in [[vqmlrdh]] and [[vmla]] respectively. Like most beatwise instructions, both procedures end with a loop that copies the masked bytes of an intermediate result into the destination register. This is the action performed by the ~copyMasked~ procedure given back in [[*Example AMPSL Statements]]. #+name: barrett-impl #+caption: AMPSL model of Barrett reduction. #+begin_src agda2 barrett : (n : ℕ) → ⦃ NonZero n ⦄ → (t z : VecReg) (im : GenReg) → Procedure State [] barrett n t z im = ,*index R (lit im) ≔ call (sliceⁱ 0) (lit (ℤ.+ (2147483648 div n)) ∷ []) ∙ invoke vqrdmulh-s32,t,z,m [] ∙ ,*index R (lit im) ≔ call (sliceⁱ 0) (lit (ℤ.- n) ∷ []) ∙ invoke vmla-s32,z,t,-n [] ∙end where vqrdmulh-s32,t,z,m = ExecBeats (vqrdmulh (record { size = 32bit ; dest = t ; src₁ = z ; src₂ = inj₁ im })) vmla-s32,z,t,-n = ExecBeats (vmla (record { size = 32bit ; acc = z ; src₁ = t ; src₂ = im })) #+end_src The final AMPSL procedure used to calculate Barrett reduction is in [[barrett-impl]]. As Barrett reduction is performed with a fixed positive base, the procedure takes the base as a non-zero Agda natural number. This definition was tested by using the following snippet, instantiating the ~int~ and ~real~ types with Agda integers and rationals respectively. #+begin_src do-barrett : (n : ℕ) → (zs : Vec ℤ 4) → Statement State [] do-barrett n zs = for 4 ( Q[ lit 0F , var 0F ] ≔ call (sliceⁱ 0) (index (lit zs) (var 0F) ∷ [])) ∙ invoke (barrett n 1F 0F 0F) [] barrett-101 : Statement State [] barrett-101 = do-barrett 101 (+ 1 ∷ + 7387 ∷ + 102 ∷ - 7473 ∷ []) #+end_src Asking Agda to normalise the ~barrett-101~ value, which expands the function definitions to produce a single ~Statement~, results in a 16KB ~Statement~. When I tried to evaluate this denotationally, Agda exhausted heap memory after 45 minutes. Despite this example being relatively small, the poor performance of AMPSL's denotational semantics highlights the necessity of the syntax-directed Hoare logic proof system. Using the Hoare logic rules to attempt to directly prove that ~barrett-101~ has the desired effect leads to a very tedious proof of expanding out the whole derivation tree. *** Proving Reusable Results One fundamental principle of programming is DRY: don't repeat yourself. This is achieved by using functions and procedures to abstract out common behaviours. Similarly, to fully utilise the power of Hoare logic, an abstract reusable correctness triple should be given for the behaviour of invoking functions. I attempted to do this for the ~copyMasked~ procedure given in [[*Example AMPSL Statements]], the type of which is given below: #+begin_src agda2 copyMasked-mask-true : ∀ {i v beat mask} {P Q : Assertion State Γ Δ} → P ⊆ equal (↓ mask) (lit (replicate (lift Bool.true))) → P ⊆ Assertion.subst Q Q[ i , beat ] (↓ v) → P ⊢ invoke copyMasked (i ∷ v ∷ beat ∷ mask ∷ []) ⊢ Q #+end_src Explained briefly, whenever the mask is all true (~I~), the procedure effectively reduces to a regular assignment rule in for AMPSL's Hoare logic. Expanding the proof derivation results in the following incomplete Agda term: #+begin_src agda2 invoke (for {!!} {!!} (if (assign {!!}) {!!}) {!!}) #+end_src The missing Agda expressions correspond to a choice of loop invariant and then four logical implications: entering the loop; leaving the loop; showing the assignment preserves the loop invariant; and showing that skipping the assignment preserves the loop invariant. Whilst none of those steps are particularly tricky, they each require the proofs of many trivial-on-paper lemmata. Due to the time constraints of the project, I have been unable to complete these proofs. * Proof of Barrett Reduction Barrett reduction is an algorithm to find a small representative of a value \(z\) modulo some base \(n\). Instead of having to perform expensive integer division, Barrett reduction instead uses an approximation function to precompute a coefficient \(m = \llbracket 2^k / n \rrbracket\). The integer division \(z / n\) is then approximated by the value \(\left\llbracket \frac{zm}{2^k} \right\rrbracket\). There are many choices of function that are suitable for the two approximations. [cite/t:@10.1007/3-540-47721-7_24] used the floor function in both cases, whereas the Barrett reduction implementation by [cite/t:@10.46586/tches.v2022.i1.482-505] instead uses \(\llbracket z \rrbracket = 2 \left\lfloor \frac{z}{2} \right\rfloor\). Work by [cite/t:@10.46586/tches.v2022.i1.211-244] proves results for regular rounding at runtime, but any \ldquo{}integer approximation\rdquo{} for precomputing the coefficient \(m\). The simplest form of Barrett reduction is that of Barrett, using two floor approximations. Thus this is the version for which I have produced my initial proof. Unlike the previous authors, who all dealt explicitly with integers and rationals, I instead proved a more abstract result for an arbitrary commutative ordered ring \(ℤ\) and ordered field \(ℝ\) with a homomorphism \(\cdot/1 : ℤ \to ℝ\) and a floor function \(\lfloor\cdot\rfloor : ℝ \to ℤ\) that is /not necessarily/ a homomorphism. This decision will eventually allow for the direct use of this result in abstract proofs about the AMPSL Barrett reduction algorithm. This is due to the choice of AMPSL's type models for ~int~ and ~real~ as abstract structures, discussed in [[*AMPSL Datatype Models]]. One major time sink for this abstraction was the complete lack of support from preexisting Agda proofs. Ordered structures like the rings and fields required are not present in the Agda standard library version 1.7, and the discoverability of other Agda libraries is lacking. Thus much work was spent encoding these structures and proving many trivial lemmata about them, such as sign-preservation, monotonicity and cancelling proofs. #+name: barrett-properties #+caption: Three properties I was able to prove about flooring Barrett reduction #+caption: for an abstract ordered ring and field. #+begin_src agda2 barrett-mods : ∀ z → ∃ λ a → barrett z + a * n ≈ z barrett-positive : ∀ {z} → z ≥ 0ℤ → barrett z ≥ 0ℤ barrett-limit : ∀ {z} → 0ℤ ≤ z → z ≤ 2ℤ ^ k → barrett z < 2 × n #+end_src In total I was able to prove three important properties of the flooring variants of Barrett reduction, listed using Agda in [[barrett-properties]]. The first property states that Barrett reduction does indeed perform a modulo reduction. The second ensures that the Barrett reduction of a positive value is remains positive. The final property states that for sufficiently small values of \(z\), Barrett reduction produces a representable no more than twice the size of the base. * Summary and Conclusions In this work, I might vital progress into proving an implementation of the NTT algorithm for the M-profile vector extension of the Armv8.1-M architecture is functionally correct. I made progress on two fronts: giving a formal semantics for Armv8-M instructions, and proving properties about Barrett reduction. To provide formal semantics for Armv8-M instructions, I designed AMSPL, a language with formal semantics that models the ASL used to describe instruction semantics in the reference manual by [cite/t:@arm/DDI0553B.s]. As AMPSL models ASL, the behaviour of instructions can be modelled in AMPSL. Then, given enough time to prove a number of trivial lemmata, it is possible to specify the semantics of Armv8-M instructions through the semantics of AMPSL. To my knowledge, I have produced the first computer-assisted proof about the properties of Barrett reduction on arbitrary inputs. Further, I have not only proven this result for integers and rationals, but for any abstract ring and field with a suitable floor function. Barrett reduction is a vital subroutine in NTT so these proofs form a solid foundation towards the final goal. ** Future Work on AMPSL Whilst the core syntax and semantics of AMPSL is complete, there are a wide range of proofs that are currently incomplete, due to the shear amount of trivial bookwork required to prove them. Here is a short list of some incomplete results: - Soundness of Hoare Logic :: There is proof that AMPSL's Hoare logic is sound with respect to its denotational semantics for all rules excluding ~invoke~ ([[*Soundness of ~declare~, ~for~ and ~invoke~ ]]). The proof of this rule should be relatively straight forward, the ~Term~ and ~Assertion~ homomorphisms it performs are the most complex and still without proof. - Completeness of Hoare Logic :: I have only conjectured that AMPSL's Hoare logic is complete, in the sense given in [[*Argument for a Proof of Correctness]]. Actually creating the weakest-precondition function requires the creation of more ~Term~ and ~Assertion~ homomorphisms with more complex effects, and using them in proofs requires proving more trivial lemmata. - Evaluating Denotational Semantics :: Asking Agda to normalise the denotational semantics of any reasonable computation often results in Agda running out of memory ([[*Using AMPSL for Proofs]]). Investigating and eliminating the cause of this behaviour would make the user experience for AMPSL significantly better. - Using Hoare Logic Rules :: Using AMPSL's Hoare logic rules for any large statement is tedious and cumbersome ([[*Using AMPSL for Proofs]]). Trying to create abstract proofs of correctness for smaller statements requires the manual proof of many trivial implications ([[*Proving Reusable Results]]). Whilst AMPSL has the potential to be an enormously useful tool for the formal verification of Armv8-M assembly algorithms, its current state does not live up to the task. Currently, to have any utility, a huge push needs to be made to complete proofs of many of the missing lemmata. ** Future Work for Functional Correctness Whilst AMPSL is able to model ASL to a degree suitable for basic functional correctness proofs, a more rigorous tool is necessary for future endeavours. One option is to add Armv8-M as a backend in pre-existing functional correctness tools like Jasmin [cite:@10.1145/3133956.3134078] and Vale [cite:@10.1145/3290376]. Another option is to add the architecture as a backend in formally-verified compilers like CompCert [cite:@hal/01238879], enabling the use of high-level functional correctness tools for the platform. Another alternative, particularly for working on pre-existing, hand-written assembly routines, is to model the Armv8-M semantics using Sail. Unlike AMPSL, Sail will the full complexity of the ASL description of instructions, allowing for more rigorous proofs about the program semantics. #+latex: \label{lastcontentpage} #+latex: %TC:ignore #+print_bibliography: \appendix * AMPSL Syntax Definition #+begin_src agda2 data Expression Σ Γ where lit : literalType t → Expression Σ Γ t state : ∀ i → Expression Σ Γ (lookup Σ i) var : ∀ i → Expression Σ Γ (lookup Γ i) _≟_ : ⦃ HasEquality t ⦄ → Expression Σ Γ t → Expression Σ Γ t → Expression Σ Γ bool _>_ : Expression Σ Γ int → (n : ℕ) → Expression Σ Γ int rnd : Expression Σ Γ real → Expression Σ Γ int fin : ∀ {ms} (f : literalTypes (map fin ms) → Fin n) → Expression Σ Γ (tuple {n = k} (map fin ms)) → Expression Σ Γ (fin n) asInt : Expression Σ Γ (fin n) → Expression Σ Γ int nil : Expression Σ Γ (tuple []) cons : Expression Σ Γ t → Expression Σ Γ (tuple ts) → Expression Σ Γ (tuple (t ∷ ts)) head : Expression Σ Γ (tuple (t ∷ ts)) → Expression Σ Γ t tail : Expression Σ Γ (tuple (t ∷ ts)) → Expression Σ Γ (tuple ts) call : (f : Function Σ Δ t) → All (Expression Σ Γ) Δ → Expression Σ Γ t if_then_else_ : Expression Σ Γ bool → Expression Σ Γ t → Expression Σ Γ t → Expression Σ Γ t data Reference Σ Γ where state : ∀ i → Reference Σ Γ (lookup Σ i) var : ∀ i → Reference Σ Γ (lookup Γ i) [_] : Reference Σ Γ t → Reference Σ Γ (array t 1) unbox : Reference Σ Γ (array t 1) → Reference Σ Γ t merge : Reference Σ Γ (array t m) → Reference Σ Γ (array t n) → Expression Σ Γ (fin (suc n)) → Reference Σ Γ (array t (n ℕ.+ m)) slice : Reference Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc n)) → Reference Σ Γ (array t m) cut : Reference Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc n)) → Reference Σ Γ (array t n) cast : .(eq : m ≡ n) → Reference Σ Γ (array t m) → Reference Σ Γ (array t n) nil : Reference Σ Γ (tuple []) cons : Reference Σ Γ t → Reference Σ Γ (tuple ts) → Reference Σ Γ (tuple (t ∷ ts)) head : Reference Σ Γ (tuple (t ∷ ts)) → Reference Σ Γ t tail : Reference Σ Γ (tuple (t ∷ ts)) → Reference Σ Γ (tuple ts) data LocalReference Σ Γ where var : ∀ i → LocalReference Σ Γ (lookup Γ i) [_] : LocalReference Σ Γ t → LocalReference Σ Γ (array t 1) unbox : LocalReference Σ Γ (array t 1) → LocalReference Σ Γ t merge : LocalReference Σ Γ (array t m) → LocalReference Σ Γ (array t n) → Expression Σ Γ (fin (suc n)) → LocalReference Σ Γ (array t (n ℕ.+ m)) slice : LocalReference Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc n)) → LocalReference Σ Γ (array t m) cut : LocalReference Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc n)) → LocalReference Σ Γ (array t n) cast : .(eq : m ≡ n) → LocalReference Σ Γ (array t m) → LocalReference Σ Γ (array t n) nil : LocalReference Σ Γ (tuple []) cons : LocalReference Σ Γ t → LocalReference Σ Γ (tuple ts) → LocalReference Σ Γ (tuple (t ∷ ts)) head : LocalReference Σ Γ (tuple (t ∷ ts)) → LocalReference Σ Γ t tail : LocalReference Σ Γ (tuple (t ∷ ts)) → LocalReference Σ Γ (tuple ts) data Statement Σ Γ where _∙_ : Statement Σ Γ → Statement Σ Γ → Statement Σ Γ skip : Statement Σ Γ _≔_ : Reference Σ Γ t → Expression Σ Γ t → Statement Σ Γ declare : Expression Σ Γ t → Statement Σ (t ∷ Γ) → Statement Σ Γ invoke : (f : Procedure Σ Δ) → All (Expression Σ Γ) Δ → Statement Σ Γ if_then_ : Expression Σ Γ bool → Statement Σ Γ → Statement Σ Γ if_then_else_ : Expression Σ Γ bool → Statement Σ Γ → Statement Σ Γ → Statement Σ Γ for : ∀ n → Statement Σ (fin n ∷ Γ) → Statement Σ Γ data LocalStatement Σ Γ where _∙_ : LocalStatement Σ Γ → LocalStatement Σ Γ → LocalStatement Σ Γ skip : LocalStatement Σ Γ _≔_ : LocalReference Σ Γ t → Expression Σ Γ t → LocalStatement Σ Γ declare : Expression Σ Γ t → LocalStatement Σ (t ∷ Γ) → LocalStatement Σ Γ if_then_ : Expression Σ Γ bool → LocalStatement Σ Γ → LocalStatement Σ Γ if_then_else_ : Expression Σ Γ bool → LocalStatement Σ Γ → LocalStatement Σ Γ → LocalStatement Σ Γ for : ∀ n → LocalStatement Σ (fin n ∷ Γ) → LocalStatement Σ Γ data Function Σ Γ ret where init_∙_end : Expression Σ Γ ret → LocalStatement Σ (ret ∷ Γ) → Function Σ Γ ret data Procedure Σ Γ where _∙end : Statement Σ Γ → Procedure Σ Γ #+end_src * AMPSL Denotational Semantics #+begin_src agda2 expr (lit {t = t} x) = const (Κ[ t ] x) expr {Σ = Σ} (state i) = fetch i Σ ∘ proj₁ expr {Γ = Γ} (var i) = fetch i Γ ∘ proj₂ expr (e ≟ e₁) = lift ∘ does ∘ uncurry ≈-dec ∘ < expr e , expr e₁ > expr (e expr (inv e) = lift ∘ Bool.not ∘ lower ∘ expr e expr (e && e₁) = lift ∘ uncurry (Bool._∧_ on lower) ∘ < expr e , expr e₁ > expr (e || e₁) = lift ∘ uncurry (Bool._∨_ on lower) ∘ < expr e , expr e₁ > expr (not e) = map (lift ∘ Bool.not ∘ lower) ∘ expr e expr (e and e₁) = uncurry (zipWith (lift ∘₂ Bool._∧_ on lower)) ∘ < expr e , expr e₁ > expr (e or e₁) = uncurry (zipWith (lift ∘₂ Bool._∨_ on lower)) ∘ < expr e , expr e₁ > expr [ e ] = (_∷ []) ∘ expr e expr (unbox e) = Vec.head ∘ expr e expr (merge e e₁ e₂) = uncurry (uncurry mergeVec) ∘ < < expr e , expr e₁ > , lower ∘ expr e₂ > expr (slice e e₁) = uncurry sliceVec ∘ < expr e , lower ∘ expr e₁ > expr (cut e e₁) = uncurry cutVec ∘ < expr e , lower ∘ expr e₁ > expr (cast eq e) = castVec eq ∘ expr e expr (- e) = neg ∘ expr e expr (e + e₁) = uncurry add ∘ < expr e , expr e₁ > expr (e * e₁) = uncurry mul ∘ < expr e , expr e₁ > expr (e ^ x) = flip pow x ∘ expr e expr (e >> n) = lift ∘ flip (shift 2≉0) n ∘ lower ∘ expr e expr (rnd e) = lift ∘ ⌊_⌋ ∘ lower ∘ expr e expr (fin {ms = ms} f e) = lift ∘ f ∘ lowerFin ms ∘ expr e expr (asInt e) = lift ∘ 𝕀⇒ℤ ∘ 𝕀.+_ ∘ Fin.toℕ ∘ lower ∘ expr e expr nil = const _ expr (cons {ts = ts} e e₁) = uncurry (cons′ ts) ∘ < expr e , expr e₁ > expr (head {ts = ts} e) = head′ ts ∘ expr e expr (tail {ts = ts} e) = tail′ ts ∘ expr e expr (call f es) = fun f ∘ < proj₁ , exprs es > expr (if e then e₁ else e₂) = uncurry (uncurry Bool.if_then_else_) ∘ < < lower ∘ expr e , expr e₁ > , expr e₂ > exprs [] = const _ exprs (e ∷ []) = expr e exprs (e ∷ e₁ ∷ es) = < expr e , exprs (e₁ ∷ es) > ref {Σ = Σ} (state i) = fetch i Σ ∘ proj₁ ref {Γ = Γ} (var i) = fetch i Γ ∘ proj₂ ref [ r ] = (_∷ []) ∘ ref r ref (unbox r) = Vec.head ∘ ref r ref (merge r r₁ e) = uncurry (uncurry mergeVec) ∘ < < ref r , ref r₁ > , lower ∘ expr e > ref (slice r e) = uncurry sliceVec ∘ < ref r , lower ∘ expr e > ref (cut r e) = uncurry cutVec ∘ < ref r , lower ∘ expr e > ref (cast eq r) = castVec eq ∘ ref r ref nil = const _ ref (cons {ts = ts} r r₁) = uncurry (cons′ ts) ∘ < ref r , ref r₁ > ref (head {ts = ts} r) = head′ ts ∘ ref r ref (tail {ts = ts} r) = tail′ ts ∘ ref r locRef {Γ = Γ} (var i) = fetch i Γ ∘ proj₂ locRef [ r ] = (_∷ []) ∘ locRef r locRef (unbox r) = Vec.head ∘ locRef r locRef (merge r r₁ e) = uncurry (uncurry mergeVec) ∘ < < locRef r , locRef r₁ > , lower ∘ expr e > locRef (slice r e) = uncurry sliceVec ∘ < locRef r , lower ∘ expr e > locRef (cut r e) = uncurry cutVec ∘ < locRef r , lower ∘ expr e > locRef (cast eq r) = castVec eq ∘ locRef r locRef nil = const _ locRef (cons {ts = ts} r r₁) = uncurry (cons′ ts) ∘ < locRef r , locRef r₁ > locRef (head {ts = ts} r) = head′ ts ∘ locRef r locRef (tail {ts = ts} r) = tail′ ts ∘ locRef r assign {Σ = Σ} (state i) val σ,γ = < updateAt i Σ val ∘ proj₁ , proj₂ > assign {Γ = Γ} (var i) val σ,γ = < proj₁ , updateAt i Γ val ∘ proj₂ > assign [ r ] val σ,γ = assign r (Vec.head val) σ,γ assign (unbox r) val σ,γ = assign r (val ∷ []) σ,γ assign (merge r r₁ e) val σ,γ = assign r₁ (cutVec val (lower (expr e σ,γ))) σ,γ ∘ assign r (sliceVec val (lower (expr e σ,γ))) σ,γ assign (slice r e) val σ,γ = assign r (mergeVec val (cutVec (ref r σ,γ) (lower (expr e σ,γ))) (lower (expr e σ,γ))) σ,γ assign (cut r e) val σ,γ = assign r (mergeVec (sliceVec (ref r σ,γ) (lower (expr e σ,γ))) val (lower (expr e σ,γ))) σ,γ assign (cast eq r) val σ,γ = assign r (castVec (sym eq) val) σ,γ assign nil val σ,γ = id assign (cons {ts = ts} r r₁) val σ,γ = assign r₁ (tail′ ts val) σ,γ ∘ assign r (head′ ts val) σ,γ assign (head {ts = ts} r) val σ,γ = assign r (cons′ ts val (ref (tail r) σ,γ)) σ,γ assign (tail {ts = ts} r) val σ,γ = assign r (cons′ ts (ref (head r) σ,γ) val) σ,γ locAssign {Γ = Γ} (var i) val σ,γ = updateAt i Γ val locAssign [ r ] val σ,γ = locAssign r (Vec.head val) σ,γ locAssign (unbox r) val σ,γ = locAssign r (val ∷ []) σ,γ locAssign (merge r r₁ e) val σ,γ = locAssign r₁ (cutVec val (lower (expr e σ,γ))) σ,γ ∘ locAssign r (sliceVec val (lower (expr e σ,γ))) σ,γ locAssign (slice r e) val σ,γ = locAssign r (mergeVec val (cutVec (locRef r σ,γ) (lower (expr e σ,γ))) (lower (expr e σ,γ))) σ,γ locAssign (cut r e) val σ,γ = locAssign r (mergeVec (sliceVec (locRef r σ,γ) (lower (expr e σ,γ))) val (lower (expr e σ,γ))) σ,γ locAssign (cast eq r) val σ,γ = locAssign r (castVec (sym eq) val) σ,γ locAssign nil val σ,γ = id locAssign (cons {ts = ts} r r₁) val σ,γ = locAssign r₁ (tail′ ts val) σ,γ ∘ locAssign r (head′ ts val) σ,γ locAssign (head {ts = ts} r) val σ,γ = locAssign r (cons′ ts val (locRef (tail r) σ,γ)) σ,γ locAssign (tail {ts = ts} r) val σ,γ = locAssign r (cons′ ts (locRef (head r) σ,γ) val) σ,γ stmt (s ∙ s₁) = stmt s₁ ∘ stmt s stmt skip = id stmt (ref ≔ val) = uncurry (uncurry (assign ref)) ∘ < < expr val , id > , id > stmt {Γ = Γ} (declare e s) = < proj₁ , tail′ Γ ∘ proj₂ > ∘ stmt s ∘ < proj₁ , uncurry (cons′ Γ) ∘ < expr e , proj₂ > > stmt (invoke p es) = < proc p ∘ < proj₁ , exprs es > , proj₂ > stmt (if e then s) = uncurry (uncurry Bool.if_then_else_) ∘ < < lower ∘ expr e , stmt s > , id > stmt (if e then s else s₁) = uncurry (uncurry Bool.if_then_else_) ∘ < < lower ∘ expr e , stmt s > , stmt s₁ > stmt {Γ = Γ} (for m s) = Vec.foldl _ (flip λ i → (< proj₁ , tail′ Γ ∘ proj₂ > ∘ stmt s ∘ < proj₁ , cons′ Γ (lift i) ∘ proj₂ >) ∘_) id (Vec.allFin m) locStmt (s ∙ s₁) = locStmt s₁ ∘ < proj₁ , locStmt s > locStmt skip = proj₂ locStmt (ref ≔ val) = uncurry (uncurry (locAssign ref)) ∘ < < expr val , id > , proj₂ > locStmt {Γ = Γ} (declare e s) = tail′ Γ ∘ locStmt s ∘ < proj₁ , uncurry (cons′ Γ) ∘ < expr e , proj₂ > > locStmt (if e then s) = uncurry (uncurry Bool.if_then_else_) ∘ < < lower ∘ expr e , locStmt s > , proj₂ > locStmt (if e then s else s₁) = uncurry (uncurry Bool.if_then_else_) ∘ < < lower ∘ expr e , locStmt s > , locStmt s₁ > locStmt {Γ = Γ} (for m s) = proj₂ ∘ Vec.foldl _ (flip λ i → (< proj₁ , tail′ Γ ∘ locStmt s > ∘ < proj₁ , cons′ Γ (lift i) ∘ proj₂ >) ∘_) id (Vec.allFin m) fun {Γ = Γ} (init e ∙ s end) = fetch zero (_ ∷ Γ) ∘ locStmt s ∘ < proj₁ , uncurry (cons′ Γ) ∘ < expr e , proj₂ > > proc (s ∙end) = proj₁ ∘ stmt s #+end_src * AMPSL Hoare Logic Definitions #+begin_src agda2 data Term (Σ : Vec Type i) (Γ : Vec Type j) (Δ : Vec Type k) : Type → Set ℓ where lit : ⟦ t ⟧ₜ → Term Σ Γ Δ t state : ∀ i → Term Σ Γ Δ (lookup Σ i) var : ∀ i → Term Σ Γ Δ (lookup Γ i) meta : ∀ i → Term Σ Γ Δ (lookup Δ i) _≟_ : ⦃ HasEquality t ⦄ → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ bool _>_ : 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 > n ⟧ σ γ δ = lift ∘ flip (shift 2≉0) n ∘ lower $ ⟦ e ⟧ σ γ δ ⟦ rnd e ⟧ σ γ δ = lift ∘ ⌊_⌋ ∘ lower $ ⟦ e ⟧ σ γ δ ⟦ fin {ms = ms} f e ⟧ σ γ δ = lift ∘ f ∘ lowerFin ms $ ⟦ e ⟧ σ γ δ ⟦ asInt e ⟧ σ γ δ = lift ∘ 𝕀⇒ℤ ∘ 𝕀.+_ ∘ Fin.toℕ ∘ lower $ ⟦ e ⟧ σ γ δ ⟦ nil ⟧ σ γ δ = _ ⟦ cons {ts = ts} e e₁ ⟧ σ γ δ = cons′ ts (⟦ e ⟧ σ γ δ) (⟦ e₁ ⟧ σ γ δ) ⟦ head {ts = ts} e ⟧ σ γ δ = head′ ts (⟦ e ⟧ σ γ δ) ⟦ tail {ts = ts} e ⟧ σ γ δ = tail′ ts (⟦ e ⟧ σ γ δ) ⟦ call f es es₁ ⟧ σ γ δ = Den.Semantics.fun 2≉0 f (⟦ es ⟧ₛ σ γ δ , ⟦ es₁ ⟧ₛ σ γ δ) ⟦ if e then e₁ else e₂ ⟧ σ γ δ = Bool.if lower (⟦ e ⟧ σ γ δ) then ⟦ e₁ ⟧ σ γ δ else ⟦ e₂ ⟧ σ γ δ ⟦_⟧ₛ [] σ γ δ = _ ⟦_⟧ₛ {ts = _ ∷ ts} (e ∷ es) σ γ δ = cons′ ts (⟦ e ⟧ σ γ δ) (⟦ es ⟧ₛ σ γ δ) #+end_src #+begin_src agda2 data Assertion (Σ : Vec Type o) (Γ : Vec Type n) (Δ : Vec Type m) : Set (L.suc ℓ) where all : Assertion Σ Γ (t ∷ Δ) → Assertion Σ Γ Δ some : Assertion Σ Γ (t ∷ Δ) → Assertion Σ Γ Δ pred : Term Σ Γ Δ bool → Assertion Σ Γ Δ true : Assertion Σ Γ Δ false : Assertion Σ Γ Δ ¬_ : Assertion Σ Γ Δ → Assertion Σ Γ Δ _∧_ : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ _∨_ : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ _⟶_ : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ #+end_src #+begin_src agda2 ⟦_⟧ : Assertion Σ Γ Δ → ⟦ Σ ⟧ₜₛ → ⟦ Γ ⟧ₜₛ → ⟦ Δ ⟧ₜₛ → Set ℓ ⟦_⟧ {Δ = Δ} (all P) σ γ δ = ∀ x → ⟦ P ⟧ σ γ (cons′ Δ x δ) ⟦_⟧ {Δ = Δ} (some P) σ γ δ = ∃ λ x → ⟦ P ⟧ σ γ (cons′ Δ x δ) ⟦ pred p ⟧ σ γ δ = Lift ℓ (Bool.T (lower (Term.⟦ p ⟧ σ γ δ))) ⟦ true ⟧ σ γ δ = Lift ℓ ⊤ ⟦ false ⟧ σ γ δ = Lift ℓ ⊥ ⟦ ¬ P ⟧ σ γ δ = ⟦ P ⟧ σ γ δ → ⊥ ⟦ P ∧ Q ⟧ σ γ δ = ⟦ P ⟧ σ γ δ × ⟦ Q ⟧ σ γ δ ⟦ P ∨ Q ⟧ σ γ δ = ⟦ P ⟧ σ γ δ ⊎ ⟦ Q ⟧ σ γ δ ⟦ P ⟶ Q ⟧ σ γ δ = ⟦ P ⟧ σ γ δ → ⟦ Q ⟧ σ γ δ #+end_src #+latex: \label{lastpage} #+latex: %TC:endignore # LocalWords: AMPSL Hoare NTT PQC structs bitstring bitstrings