\documentclass{entcs} \usepackage{prentcsmacro} \usepackage{graphicx} \sloppy \usepackage{latexsym} \usepackage{amsmath} \usepackage{amssymb} \usepackage{url} \renewcommand{\today}{\number\day\ \ifcase\month\or January\or February\or March\or April\or May\or June\or July\or August\or September\or October\or November\or December\fi \ \number\year} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Preamble \newcommand\cfile{} \newcommand\comment[1]{} \newcommand\cc[1]{#1} % for label names % \renewcommand\footnote[1]{} % for footnotes % \pagestyle{myheadings} % \pagestyle{plain} \pagestyle{empty} \renewcommand\theenumi{(\alph{enumi})} \renewcommand\labelenumi{\theenumi} \renewcommand\theenumii{(\roman{enumii})} \renewcommand\labelenumii{\theenumii} \newcommand\sfile[1]{\cite[\texttt{#1}]{l4-word-files}} \newcommand\ie{i.e.{}} \newcommand\eg{e.g.{}} \newcommand\lenof{\texttt{len\_of}} \newcommand\numof{\texttt{number\_of}} \newcommand\TYPE{\texttt{TYPE}} \newcommand\itself{\texttt{itself}} \newcommand\False{\texttt{False}} \newcommand\obin{\texttt{obin}} \newcommand\bin{\texttt{bin}} \newcommand\word{\texttt{word}} \newcommand\arbitrary{\texttt{arbitrary}} \newcommand\bintrunc{\texttt{bintrunc}} \newcommand\norm{\texttt{norm}} \newcommand\uint{\texttt{uint}} \newcommand\sint{\texttt{sint}} \newcommand\unat{\texttt{unat}} \newcommand\Abs{\texttt{Abs}} \newcommand\Rep{\texttt{Rep}} \newcommand\set{\textit{set}} \def\lastname{Dawson} \begin{document} \begin{frontmatter} \title{Isabelle Theories for Machine Words} \author{Jeremy Dawson\thanksref{mywww}} \address{ Logic and Computation Group, \\ School of Computer Science, \\ Australian National University, \\ Canberra, ACT 0200, Australia } \thanks[mywww]{ \href{http://users.rsise.anu.edu.au/~jeremy/} {\url{http://users.rsise.anu.edu.au/~jeremy/}}} \begin{abstract} We describe a collection of Isabelle theories which facilitate reasoning about machine words. For each possible word length, the words of that length form a type, and most of our work consists of generic theorems which can be applied to any such type. We develop the relationships between these words and integers (signed and unsigned), lists of booleans and functions from index to value, noting how these relationships are similar to those between an abstract type and its representing set. We discuss how we used Isabelle's {\tt bin} type, before and after it was changed from a datatype to an abstract type, and the techniques we used to retain, as nearly as possible, the convenience of primitive recursive definitions. We describe other useful techniques, such as encoding the word length in the type. \end{abstract} \begin{keyword} machine words, twos-complement, mechanised reasoning \end{keyword} \end{frontmatter} % ABOVE HERE SOME AVOCS (ENTCS) - SPECIFIC STUFF \section{Introduction} \label{s-intro} In formally verifying machine hardware, we need to be able to % systematically deal with the properties of machine words. These differ from ordinary numbers in that, for example, addition and multiplication can overflow, with overflow bits being lost, and there are bit-wise operations which are simply defined in a natural way. Wai Wong \cite{wong} developed HOL theories in which words are represented as lists of bits. The type is the set of all words of any length; words of a given length form a subset. Some theorems have the word length as an explicit condition. The theories include some bit-wise operations but not the arithmetic operations. In \cite{fox-arm} Fox descibes HOL theories modelling the architecture of the ARM instruction set. There, the HOL datatype \texttt{w32 = W32 of num} is used, that is, the machine word type is isomorphic to the naturals, and the expression \texttt{W32} $n$ is to mean the word with unsigned value $n \bmod 2^{32}$. In this approach, equality of machine words does not correspond to equality of their representations. In \cite{atd} Akbarpour, Tahar \& Dekdouk describe the formalisation in HOL of fixed point quantities, where a single type is used, and the quantities contain fields showing how many bits appear before and after the point. Their focus is on the approximate representation of floating point quantities. In \cite{harrison-euclidean} Harrison describes the problem of encoding vectors of any dimension $n$ of elements of type $A$ (\eg\ reals, or bits) in the type system of HOL, the problem being that a type cannot be parameterised over the value $n$. His solution is to use the function space type $N \to A$, where $N$ is a \emph{type} which has exactly $n$ values. He discusses the problem that an arbitrary type $N$ may in fact have infinitely many values, when infinite dimensional vectors are not wanted. In the bitvector library \cite{pvs-bitvectors} for PVS, which has a more powerful type system, a bit-vector is defined as a function from $\{0,\ldots,N-1\}$ to the booleans. It provides interpretations of a bit-vector as unsigned or signed integers, with relevant theorems. % are provided in that library. In this paper we describe theories for Isabelle/HOL \cite{isabelle}, for reasoning about machine words. We developed these for NICTA's L4.verified project \cite{l4verified}, which aims to provide a mathematical, machine-checked proof of the conformance of the L4 microkernel to a high level, formal description of its expected behaviour. As in \cite{harrison-euclidean}, each type of words in our formalization is of a particular length. In this work we relate our word types both to the integers modulo $2^n$ and to lists of booleans; thus we have access to large bodies of results about both arithmetic and logical (bit-wise) operations. We have defined all the operations referred to in \cite{fox-arm}, and describe several other techniques and classes of theorems. Our theories have been modified recently due to our collaboration with the company Galois Connections, who have developed similar, though less extensive, theories. The Galois theories, though mostly intended to be used for $n$-bit machine words, are based on an abstract type of integers modulo $m$ (where, for machine words, $m = 2 ^ n$). Thus, in combining the theories (since doing the work described here), we used the more general Galois definition of the abstract type $\alpha\ \word$; our theorems apply when $\alpha$ belongs to an axiomatic type class for which $m = 2 ^ n$. In this paper we focus on the techniques used to define the machine word type. We defined numerous operations on words which are not discussed here, such as concatenating, splitting, rotating and shifting words. Some of these are mentioned in the Appendix. The Isabelle code files are available at \cite{l4-word-files}. \section{Description of the word-n theories} \subsection{The \texttt{bin} and \texttt{obin} types} Isabelle's \verb|bin| type explicitly represents bit strings, and is important because \begin{itemize} \item it is used for encoding literal numbers, and an integer entered in an Isabelle expression is converted to a \verb|bin|, thus \verb|read "3"| gives \\ \verb|number_of| \texttt{(Pls BIT bit.B1 BIT bit.B1 ::\ bin)} \\ (where $x$ \verb|::| $T$ means that $x$ is of type $T$) ; \item there is much built-in numeric simplification for numbers expressed as \verb|bin|s, for example for negation, addition and multiplication, using rules which reflect the usual definitions of these operations for twos-complement integers. \end{itemize} Isabelle changed during development of our theories. Formerly the \verb|bin| type was a datatype, with constructors \begin{itemize} \item \verb|Pls| (a sequence of 0, extending infinitely leftwards) \item \verb|Min| (a sequence of 1, extending infinitely leftwards) (for the integer $-1$) \item \verb|BIT| (where \verb|(w::bin) BIT (b::bool)| is \verb|w| with \verb|b| appended on the right) \end{itemize} Subsequently, in Isabelle 2005, Isabelle's \verb|bin| type changed. The new \verb|bin| type in Isabelle 2005 is an abstract type, isomorphic to the set of all integers, with abstraction and representation functions \verb|Abs_Bin| and \verb|Rep_Bin|. % \begin{verbatim} % Abs_Bin :: "int => bin" % Rep_Bin :: "bin => int" % \end{verbatim} % and type definition theorem % \begin{verbatim} % type_definition_Bin = "type_definition Rep_Bin Abs_Bin Bin" % \end{verbatim} % where \verb|Bin| is \verb|UNIV :: int set|, the set of all integers. We found that each of these ways of formulating the \bin\ type has certain advantages. We proceed to discuss these, and how we overcame the disadvantages of the new way of defining \bin s. We first describe using the datatype-based definition. Since at one stage in the course of adapting to this change we were using both the old and new definition of \bin s and associated theorems, we used new names for the old definition, with `\texttt o' or `\texttt O' prepended: thus we had the contructors \verb|oPls, oMin, OBIT|, for the datatype \verb|obin|. (We also kept the old function \verb|number_of|, renaming it \verb|onum_of|). % we kept this type and the associated code % (including some source files from the Isabelle distribution), % using new names, with `\texttt o' or `\texttt O' prepended: % % However following the change in Isabelle's \verb|bin| type, % we kept this structure and the associated code, % calling this type \verb|obin|, % and the constructors \verb|oPls|, \verb|oMin| and \verb|OBIT|. % As we had used the former setup % extensively by the time we learnt of the change in % Isabelle, we kept it, with new names, % with "o" or "O" prepended, thus we have the contructors % \verb|oPls, oMin, OBIT|, for the type \verb|obin|. So in describing our use of \bin s as formerly defined, we use these names. \footnote{ More recently, the \texttt{bin} type changed again, in development versions of Isabelle during 2006, to be identical to the integers rather than an isomorphic type. So we will omit the functions \texttt{Abs\_Bin} and \texttt{Rep\_Bin}, % Thus now, \emph{in effect}, $w\ \texttt{BIT}\ b$ is defined as $2 w + b$. and now our references to the type \texttt{bin} indicate an integer expressed using \texttt{Pls}, \texttt{Min} and \texttt{BIT}.} \subsection{Definitions using the \texttt{obin} datatype} \label{s-def-obin} As these definitions have since been removed, this section is not relevant for using these theories currently. But we give this description to indicate the advantages and disadvantages of the \obin\ type, \ie, the former, datatype-based definition of the \bin\ type. In fact for some time we continued to use the \verb|obin| type because it is defined as a datatype: only a datatype permits the primitive and general recursive definitions described below. Using the \verb|obin| datatype allows us to define functions in the most natural way in terms of their action on bits. For example, to define bit-wise complementation, we just used the following primitive recursive definitions: \begin{verbatim} primrec obin_not_Pls : "obin_not oPls = oMin" obin_not_Min : "obin_not oMin = oPls" obin_not_OBIT : "obin_not (w OBIT x) = (obin_not w OBIT Not x)" \end{verbatim} We mention that, apart from the obvious benefit of using a simple definition, it is easier to be sure that it accurately represents the action of hardware that we intend to describe: this is important in theories to be used in formal verification. Defining bit-wise conjunction using primitive recursion on either of two arguments is conceptually similar, though the expression is not so simple. \footnote{ In Isabelle a set of primitive recursive definitions must be based on the cases of exactly one curried argument. It can be easier to use Isabelle's \texttt{recdef} package. % for such definitions. } \comment{ \begin{verbatim} primrec obin_and_Pls : "obin_and oPls x = (case x of ...)" \end{verbatim} \begin{verbatim} recdef obin_and "measure (%(a,b). size a + size b)" "obin_and (oPls, x) = oPls" "obin_and (x, oPls) = oPls" "obin_and (oMin, x) = x" "obin_and (x, oMin) = x" "obin_and (w OBIT b, v OBIT a) = obin_and (w, v) OBIT (a & b)" \end{verbatim} } We also made considerable use of functions \verb|obin_last| and \verb|obin_rest|, which give the last bit and the remainder, respectively. Again, we defined these functions by primitive recursion using the fact that \verb|obin| is a datatype (the rules correspond to the simplifications \emph{proved} for \verb|bin_last| and \verb|bin_rest|, see \S\ref{s-def-bin}). \comment{ \begin{verbatim} primrec oPls : "obin_rest oPls = oPls" oMin : "obin_rest oMin = oMin" OBIT : "obin_rest (w OBIT x) = w" primrec oPls : "obin_last oPls = False" oMin : "obin_last oMin = True" OBIT : "obin_last (w OBIT x) = x" \end{verbatim} } In working with the \verb|obin| type, we needed to define the concept of a normalized \verb|obin|, where the combination \verb|oPls OBIT False| does not appear, since it denotes the same sequence of bits, and so the same integer, as \verb|oPls|. So we normalise an \verb|obin| by changing \verb|oPls OBIT False| to \verb|oPls|, and likewise \verb|oMin OBIT True| to \verb|oMin|. Thus the set of normalised \verb|obin|s is isomorphic to the set of integers, via the usual twos-complement representation (see theorems \verb|td_int_obin| in \S\ref{s-ptdts}, and \verb|td_ext_int_obin| in \S\ref{s-etdts}). The following functions relate to normalising \verb|obin|s. \begin{verbatim} mk_norm_obin :: "obin => obin" is_norm_obin :: "obin => bool" \end{verbatim} While use of the \obin\ type has the advantage over the \bin\ type of being a datatype, the need to prove a large number of lemmas concerning normalisation of \verb|obin|s was a significant disadvantage. \subsection{Definitions involving the \texttt{bin} type} \label{s-def-bin} Our initial development developed words of length $n$ from the set of \obin s. % , truncated to length $n$. So, for example, we defined the bit-wise complement of a word using \verb|obin_not|, described above, and the addition of two words using addition of \obin s, based on functions to do numerical arithmetic from the Isabelle source files. However we found the need to deal with words entered literally: \verb|6 :: 'a word| is read as \verb|number_of| \texttt{(Pls BIT bit.B1 BIT bit.B1 BIT bit.B0)}. To simplify \verb|6 && 5 :: 'a word| (where \verb|&&| is our notation for bit-wise conjunction), we found it convenient to use simplifications based on the \bin\ type: that is, we wanted to use a function \verb|bin_and|, for bit-wise conjunction of \bin s, rather than \verb|obin_and|. Similarly, dealing with words of length 3, say, we wanted to simplify \verb|11 :: 'a word| to \verb|3| using a function which truncates \bin s, not \obin s. Since \verb|bin| is not a datatype, we could not define functions on \verb|bin|s in the same direct %straightforward way as on \obin s. So, originally, we defined such functions on \verb|bin|s by reference to the corresponding functions on \verb|obin|s. To do this we used the functions \verb|onum_of| and \verb|int_to_obin|, which relate the \verb|int| (isomorphic to \verb|bin|) and \verb|obin| types. \begin{verbatim} bin_and_def : "bin_and v w == onum_of (obin_and (int_to_obin v, int_to_obin w))" \end{verbatim} \comment{ OMIT FOLLOWING TRUNCATION STUFF So, originally, we defined functions such as truncation on \verb|bin|s by reference to the corresponding functions \verb|btrunc| and \verb|sbtrunc| on \verb|obin|s. \begin{verbatim} bintrunc, sbintrunc :: "nat => bin => bin" defs bintrunc_def : "bintrunc n w == onum_of (btrunc (n, int_to_obin w))" sbintrunc_def : "sbintrunc n w == onum_of (sbtrunc (n, int_to_obin w))" \end{verbatim} } % Likewise, we defined \verb|bin_and| from \verb|obin_and|, % and many other functions in a similar way. We had obtained a large number of simplification theorems involving \obin s. Using this approach, we then had to do some rather complex programming to transfer all these simplification theorems, \emph{en masse}, from \verb|obin|s to \verb|bin|s, so as to avoid proving them all again individually. In this way the parallel use of \obin s and \bin s produced significant extra complexity. % While such SML code remains for similar purposes, % such as generating simplification theorems for bit-wise logical operations on % words from corresponding theorems for booleans, In short, we found that, although the fact of \verb|obin| being a datatype %In short, we found that, although the datatype \verb|obin| permits simple recursive definitions, the machinery needed to take these definitions and resulting theorems on \obin s and produce definitions and theorems for corresponding functions involving \verb|bin|s was unpleasantly cumbersome. Therefore we examined alternative ways of defining functions in terms of the bit-representation of a \verb|bin|. First we considered what properties of the \verb|bin| type resemble the properties of a datatype. The properties of a datatype are: \begin{enumerate} \item \label{distinct}Different constructors give distinct values \item \label{inj} Each constructor is injective (in each of its arguments) \item \label{exhaust} All values of the type are obtained using the constructors \end{enumerate} Now we can consider the \verb|bin| type with ``pseudo-constructors'' \verb|Pls|, \verb|Min| and \verb|Bit| (where \verb|Bit w b| is printed and may be entered as \verb|w BIT b|). In terms of these ``pseudo-constructors'' the properties \ref{inj} and \ref{exhaust} above hold: in fact property \ref{exhaust} holds using the ``pseudo-constructor'' \verb|Bit| alone. Thus we have these theorems; % and a sort of \verb|case_tac| for \verb|bin|s which \verb|bin_exhaust| enables us to express any \verb|bin| appearing in a proof as \verb|w BIT b|. Here \verb|!!| is Isabelle notation for the universal quantification provided in the meta-logic. \begin{verbatim} BIT_eq = "u BIT b = v BIT c ==> u = v & b = c" bin_exhaust = "(!!x b. bin = x BIT b ==> Q) ==> Q" \end{verbatim} % fun bin_case_tac var = res_inst_tac [("bin", var)] bin_exhaust ; Then we can define functions \verb|bin_rl|, and thence \verb|bin_last| and \verb|bin_rest|: \begin{verbatim} bin_rl_def : "bin_rl w == SOME (r, l). w = r BIT l" bin_rest_def : "bin_rest w == fst (bin_rl w)" bin_last_def : "bin_last w == snd (bin_rl w)" \end{verbatim} % SomeI : P x ==> P (SOME x. P x) The \verb|SOME| function is (partially) defined in Isabelle, by the axiomatic specification \texttt{"P w ==> P (SOME x.\ P x)"}, so its effect here is that if % The meaning of the \verb|SOME| function is that if there is a unique choice of \verb|r| and \verb|l| to satisfy \texttt{w = r BIT l}, then \texttt{bin\_rl (r BIT l) = (r, l)}. In fact property \ref{inj} gives this uniqueness, % \begin{verbatim} % "(bin_rl (r BIT l) = (r, l))" % \end{verbatim} and so from that the expected simplification rules \verb|bin_last_simps| and \texttt{bin\_rest\_simps'} follow. % We then proved, as \verb|bin_last_mod| and \verb|bin_rest_div|, % numerical characterisations of these functions. We then used the numerical characterisation of the \verb|BIT| operator (effectively, $w\ \texttt{BIT}\ b = 2 w + b$) to obtain the numerical characterisations of these functions as \verb|bin_last_mod| and \verb|bin_rest_div|. \begin{verbatim} bin_last_simps = "bin_last Pls = bit.B0 & bin_last Min = bit.B1 & bin_last (w BIT b) = b" bin_rest_simps' = "bin_rest Pls = Pls & bin_rest Min = Min & bin_rest (w BIT b) = w" bin_last_mod = "bin_last w == if w mod 2 = 0 then bit.B0 else bit.B1" bin_rest_div = "bin_rest w == w div 2" \end{verbatim} We also derived a theorem for proofs by induction involving \verb|bin|s. % SPACE % While the premises of \verb|bin_induct| contain some redundancy, % this is unlikely to make a proof using \verb|bin_induct| more difficult % than it need be. % and a corresponding tactic. \begin{verbatim} bin_induct = "[| P Pls; P Min; !!bin bit. P bin ==> P (bin BIT bit) |] ==> P bin" \end{verbatim} % fun bin_induct_tac var = res_inst_tac [("bin", var)] bin_induct ; Both \verb|bin_exhaust| and \verb|bin_induct| were frequently used in proofs, and they usually made proofs for \verb|bin|s just as easy as the corresponding proofs for \verb|obin|s. Often the theorems and proofs were simpler for \verb|bin|s, \eg\ \begin{verbatim} bin_add_not = "x + bin_not x = Min" obin_add_not = "mk_norm_obin (obin_add x (obin_not x)) = oMin" \end{verbatim} However obtaining a near-equivalent, for \verb|bin|s, of primitive recursive definitions in \verb|obin|s, was a little more intricate. We have already described the definition of \verb|bin_last| and \verb|bin_rest|, and the derivation of simplification rules corresponding to the definitions of \verb|obin_last| and \verb|obin_rest|. Typically a function \verb|f| defined by primitive recursion would, if \verb|bin| were a datatype with its three constructors, be defined by giving values \verb|vp| and \verb|vn| for \verb|f Pls| and \verb|f Min|, and % a value \verb|vn| for \verb|f Min|, and a function \verb|fr|, where \verb|f (w BIT b)| is given by \verb|fr w b (f w)|. (The form of the recursion function returned by \verb|define_type| in the HOL theorem prover makes this explicit). % So, using Isabelle's generic mechanism for defining recursive functions, we defined a function \verb|bin_rec| which, given \verb|vp|, \verb|vn| and \verb|fr| returns a function \verb|f| satisfying % \texttt{f Pls = vp}, % \texttt{f Min = vn}, % and, except where \verb|w BIT b| equals % \verb|Pls| or \verb|Min|, % \texttt{f (w BIT b) = fr w b (f w)}. the three equalities shown, but the last only where \verb|w BIT b| does not equal \verb|Pls| or \verb|Min|. \begin{verbatim} bin_rec :: "'a => 'a => (int => bit => 'a => 'a) => int => 'a" f Pls = vp f Min = vn f (w BIT b) = fr w b (f w) \end{verbatim} \comment{ So we defined a function \verb|bin_rec| \begin{verbatim} bin_rec :: "'a => 'a => (int => bit => 'a => 'a) => int => 'a" \end{verbatim} which, given \verb|vp|, \verb|vn| and \verb|fr| returns a function \verb|f| satisfying \begin{verbatim} f Pls = vp f Min = vn \end{verbatim} and, except where \verb|w BIT b| equals \verb|Pls| or \verb|Min|, \begin{verbatim} f (w BIT b) = fr w b (f w) \end{verbatim} } In the usual case, we can then prove that this last equation in fact holds for \emph{all} \verb|w| and \verb|b|, as we want for a convenient simplification rule. See examples in \sfile{BinGeneral.thy}. % Here are \verb|bin_not| and \verb|bin_and| defined in this way: % Here are the definitions of the \verb|bin_not| and \verb|bin_and| % functions using this framework: \begin{verbatim} defs bin_not_def : "bin_not == bin_rec Min Pls (%w b s. s BIT bit_not b)" bin_and_def : "bin_and == bin_rec (%x. Pls) (%y. y) (%w b s y. s (bin_rest y) BIT (bit_and b (bin_last y)))" \end{verbatim} After making these definitions, the simplification rules in the desired form (such as those shown below) need to be proved. \begin{verbatim} bin_not_simps = [... , "bin_not (w BIT b) = bin_not w BIT bit_not b" ] bin_and_Bits = "bin_and (x BIT b) (y BIT c) = bin_and x y BIT bit_and b c" \end{verbatim} % (\ie, counterparts of the rules given above to define % \verb|obin_not| and \verb|obin_and|) Proving these was virtually automatic for \verb|bin_not| (with one argument), and fairly straightforward for \verb|bin_and| (with two arguments): see examples in \sfile{BinGeneral.thy}. This was much easier than maintaining collections of corresponding theorems for the separate types \verb|bin| \emph{and} \verb|obin|. \subsection{The type of fixed-length words of given length} % \subsubsection{Constructing $n$-bit quantities} As a preliminary step, we define functions which create $n$-bit quantities. We called these ``truncation'' functions, although they also lengthen shorter quantities. Both functions will cut down a longer quantity to the desired length, by deleting high-order bits. For an argument shorter than desired, unsigned truncation extends it to the left with zeroes, whereas signed truncation extends it with its most significant bit. Thus \texttt{bintrunc n w} gives \verb|Pls| followed by $n$ bits, whereas \verb|sbintrunc (n-1) w| (used for fixed-length words of length $n$) gives \verb|Pls| or \verb|Min| followed by $n-1$ bits (so here the \verb|Pls| or \verb|Min|, is treated as a sign bit, as one of the $n$ bits). % We defined \verb|bintrunc| by primitive recursion on the first argument (the number of bits required) and auxiliary functions \verb|bin_last| and \verb|bin_rest|, and \verb|sbintrunc| similarly. \begin{verbatim} bintrunc, sbintrunc :: "nat => bin => bin" primrec Z : "bintrunc 0 bin = Pls" Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)" \end{verbatim} Now we need to set up a type in which the length of words is implicit. The type system of Isabelle is similar to that of HOL in that dependent types are not allowed, so we cannot directly set up a type which consists of (for example) lists of length $n$. Our solution was that the type of words of length $n$ is $\alpha\ \word$ parametrised over the type $\alpha$ where the word length can be deduced from the type $\alpha$. As noted, Harrison did this by letting the word length be the number of values of the type $\alpha$. We use $\lenof\ \TYPE(\alpha)$ for the word length. $\TYPE(\alpha)$ is a polymorphic value, of type $\alpha\ \itself$, whose purpose is essentially to encapsulate a type as a term. \footnote{It is used, for example, to express the assertion that a type belongs to a particular type class.} In the output of $\TYPE(\alpha)$ the type $\alpha$ is printed, which was useful. The function \lenof\ is declared, with polymorphic type ($\alpha$, printed as \verb|'a|, being a type variable) in the library files as shown below. The library files provide the axiom \verb|word_size| which gives the general formula for the length of a word, but the user must define the value of $\lenof\ \TYPE(\alpha)$ for each specific choice of $\alpha$. % %OMIT FOR NON-TPHOLS VERSION \comment{Originally we used $\lenof\ (\arbitrary :: \alpha)$ for the word length, but Isabelle doesn't print the type of a constant such as \arbitrary, which was a difficulty in doing proofs involving different word lengths.} \begin{verbatim} len_of :: "'a :: len0 itself => nat" word_size : "size (w :: 'a :: len0 word) == len_of TYPE ('a)" \end{verbatim} A type of fixed-length words is \verb|'a :: len0 word|, where \verb|len0| is a type class whose only relevance is that it admits a function \lenof, and the word length of any \verb|w :: 'a :: len0 word| is given by the axiom \verb|word_size|. For each desired word length, the user declares a type (say \verb|a|), in the class \verb|len0|, and defines the value \verb|len_of TYPE (a)| to be the chosen word length. This provides a type of words of that given length. (Isabelle notation may be confusing here: in \verb|w :: 'a :: len0 word|, \verb|w| is a term, \verb|'a| is a type variable, \verb|len0| is the type class to which \verb|'a| belongs, and \verb|word| is a type constructor. Thus the implicit bracketing is \verb|w :: (('a :: len0) word)|.) % A type of fixed-length words would be \verb|a :: len0 word|, % where \verb|len0| is a type class % whose only relevance is that it admits a function \lenof, % and the word length of any \verb|w :: a :: len0 word| is given by % the axiom \verb|word_size|. % So for each desired word length, the user declares a type \verb|a| % in the class \verb|len0|, and defines the value % \verb|len_of TYPE (a)| to be the chosen word length. % This provides a type of words of that given length. % Isabelle notation may be confusing here: in \verb|w :: a :: len0 word|, % \verb|w| is a term, % \verb|a| is a type % (or \verb|'a| is a type variable), % \verb|len0| is the type class to which \verb|a| belongs, % and \verb|word| is a type constructor. % Thus the implicit bracketing is \verb|w :: ((a :: len0) word)|. % The actual development is complicated but has the result that % each theorem applies to fixed-length words of any length. An Isabelle type definition defines a new type whose set of values is isomorphic to a given set. To define each word type we used the definition: \begin{verbatim} typedef 'a word = "uword_len (len_of TYPE ('a))" "uword_len len == range (bintrunc len)" \end{verbatim} where \verb|uword_len (len_of TYPE ('a))| is the set of integers, truncated to length $n$ using the function \verb|bintrunc| described earlier. \comment{This is the definition we used \emph{before} combinining our theories with those of Galois Connections, see \S \ref{s-intro}.} %OMIT FOR NON-TPHOLS VERSION, OR MAYBE ALL \comment{ LACK OF SPACE This definition benefits from a recent change in Isabelle. The typedef procedure includes defining a constant (here called \verb|word|) which is the representing set. As with any defined constant, if the definition involves a type variable, then that type variable must be part of the type of the constant being defined. As of Isabelle 2005, the constant \word\ defined as part of the typedef procedure is given an extra argument \verb|TYPE('a)| so as to satisfy this requirement. Prior to Isabelle 2005 the definition above failed and so we had used as the representing set % \begin{verbatim} % "{arbitrary :: 'a :: len0} <*> uword_len (len_of TYPE ('a))" % \end{verbatim} \texttt{"\{arbitrary :: 'a :: len0\} <*> uword\_len (len\_of TYPE ('a))"} \footnote {Alternatively, it is possible to avoid defining the constant \word\ by a command of the form \texttt{typedef (open word)} \ldots.} } \comment{ EARLIER VERSION This may seem unduly complex - why not just define \begin{verbatim} typedef 'a word = "{arbitrary :: 'a :: len0} <*> uword_len (len_of TYPE ('a))" typedef 'a word = "uword_len (len_of TYPE ('a))" \end{verbatim} As of Isabelle 2005, there is in fact no reason not to do this, as we recently discovered by examining the Galois Connections code. Prior to Isabelle 2005, attempting to do this caused the following problem. The typedef procedure includes defining a constant (here called \verb|word|) which is the representing set. As with any defined constant, if the definition involves a type variable, then that type variable must be part of the type of the constant being defined. So we defined \verb|word| as a set of pairs, where the first component of each pair is a value which is of type \verb|'a|; the second component was the part that was actually used. As of Isabelle 2005, the constant \word\ defined as part of the typedef procedure is given an extra argument \verb|TYPE('a)| so as to satisfy this requirement. % Alternatively, one can avoid defining the constant \word\ % by the command \verb|typedef (open word)| \ldots. Alternatively, it is possible to avoid defining the constant \word\ by a command of the form \verb|typedef (open word)| \ldots. } The type class \verb|len| is a subclass of \verb|len0|, defined by the additional requirement that the word length $n$ is non-zero. \begin{verbatim} len_gt_0 = "0 < len_of TYPE('a::len)" \end{verbatim} Results involving a signed interpretation of words are limited to this case (naturally, as the word needs to contain a sign bit). \footnote{ Note that some other results are limited to $n > 0$ because their proof uses theorems from the Isabelle library which apply only in a type class where 0 and 1 are distinct.} % Thus the fixed-length word type is abstract, representing a sequence of bits, but such words can be interpreted as unsigned or signed integers. Although the abstract type is defined to be isormorphic to \texttt{range (bintrunc n)}, it can be viewed as isomorphic to several different sets. So the set of words of length $n$ is isomorphic to each of the following, with the relevant ``type definition theorems'' (explained later) given in brackets: \begin{itemize} % \item the set of \verb|obin|s which consist of \verb|oPls|, % followed by $n$ bits % (\verb|td_uobin|) % \item the set of \verb|obin|s which consist of % \verb|oPls| or \verb|oMin|, followed by $n-1$ bits % (\verb|td_sobin|) \item the set of integers in the range $0 \ldots 2^n -1$ (\verb|td_uint|) \item the set of integers in the range $-2^{n-1} \ldots 2^{n-1}-1$ (\verb|td_sint|) \item the set of naturals up to $2^n - 1$ (\verb|td_unat|) \item the set of lists of booleans of length $n$ (\verb|td_bl|) \item the set of functions $f$ of type \verb|nat -> bool| satisfying the requirement that for $i \geq n$, $f\ i = $ \verb|False| (\verb|td_nth|) \end{itemize} That the type of a word implies its length had some curious consequences. For functions such as \verb|ucast|, which casts a word from one length to another, or \verb|word_rsplit|, which splits a word into a list of words of some given (usually shorter) length, the length of the resulting words is implicit in the result type of the function, not given as an argument. Therefore we get theorems such as \verb|"ucast w = w"| and \verb|"word_rsplit w = [w]"|, where the repeated use of the variable \verb|w| implies that the result word(s) are of the same length as the argument. % \begin{verbatim} % ucast_id = "ucast w = w" % word_rsplit_same = "word_rsplit w = [w]" % \end{verbatim} \subsection{Pseudo type definition theorems} \label{s-ptdts} In Isabelle, defining a new type $\alpha$ from a set $S : \rho\ \set$ causes the creation of an abstraction function $\Abs : \rho \to \alpha$ and a representation function $\Rep : \alpha \to \rho$, such that \Abs\ and \Rep\ are mutually inverse bijections between $S$ and the set of all values of type $\alpha$. Note that the domain of \Abs\ is the type $\rho$, but that nothing is said about the values it takes outside $S$. The predicate \verb|type_definition| expresses these properties, and a theorem, \verb|type_definition_|$\alpha$, stating \verb|type_definition| \Rep\ \Abs\ $S$, is created for the new type $\alpha$. We can use the predicate \verb|type_definition| to express the isormophisms between the set of $n$-bit words and the other sets mentioned above; we have proved the following ``type definition theorems''. \begin{verbatim} td_int_obin = "type_definition int_to_obin onum_of (range mk_norm_obin)" td_uint = "type_definition uint word_of_int (uints (len_of TYPE('a)))" td_sint = "type_definition sint word_of_int (sints (len_of TYPE('a)))" td_unat = "type_definition unat of_nat (unats (len_of TYPE('a)))" td_bl = "type_definition to_bl of_bl {bl::bool list. length bl = len_of TYPE('a)}" td_nth = "type_definition word_nth of_nth {f::nat => bool. ALL i::nat. f i --> i < len_of TYPE('a)}" \end{verbatim} % These use the following functions between the various types (\verb|of_nat| and \verb|onum_of| have more general types, but are used with these types in these theorems): \begin{verbatim} int_to_obin :: "int => obin" onum_of :: "obin => int" word_of_int :: "int => 'a :: len0 word" uint :: "'a :: len0 word => int" sint :: "'a :: len word => int" of_nat :: "nat => 'a :: len0 word" unat :: "'a :: len0 word => nat" of_bl :: "bool list => 'a word" to_bl :: "'a word => bool list" of_nth :: "(nat => bool) => 'a word" word_nth :: "'a word => nat => bool" \end{verbatim} The following define the representing sets referred to above, or were subsequently proved about them: \begin{verbatim} "uints n == range (bintrunc n)" "sints n == range (sbintrunc (n - 1))" "unats n == {i. i < 2 ^ n}" "uints n == {i. 0 <= i & i < 2 ^ n}" "sints n == {i. - (2 ^ (n - 1)) <= i & i < 2 ^ (n - 1)}" \end{verbatim} \subsection{Extended type definition theorems} \label{s-etdts} As noted, however, these type definition theorems do not say anything about the action of \Abs\ outside the set $S$. But in fact we have defined the abstraction functions to behave ``sensibly'' outside $S$, and it is useful to do so. For example, \verb|word_of_int|, which turns an integer in the range $0 \ldots 2^n -1$ into a word, is defined so that it also behaves ``sensibly'' on other integers --- it takes $i$ and $i'$ to the same word iff $i \equiv i' \pmod{2^n}$. This allows us to use the same abstraction function \verb|word_of_int| in both theorems \verb|td_uint| and \verb|td_sint|. \begin{verbatim} "word_of_int (b mod 2 ^ len_of TYPE('a)) = word_of_int b" \end{verbatim} % In general, a theorem \verb|type_definition Rep Abs A| % says nothing about the behaviour of the function % \verb|Abs| outside the set \verb|A|, % but we have generally defined these "\verb|Abs|" functions % in a sensible way. The ``sensible'' definition of \verb|word_of_int| has useful consequences. %convenient consequences. For example, when we \emph{define} addition of words by \verb|word_add_wi|, where \verb|u| and \verb|v| are words of the same length (and this definition does not involve the addition of \verb|bin|s which are not representatives of words), we also can \emph{prove} the result \verb|wi_hom_add| where \verb|a| and \verb|b| can be \emph{any} integers, whether or not they are values which represent words. \begin{verbatim} word_add_wi : "u + v == word_of_int (uint u + uint v)" wi_hom_add = "word_of_int a + word_of_int b = word_of_int (a + b)" \end{verbatim} The following theorems, of the form $\texttt{Rep}\ (\texttt{Abs}\ x) = f\ x$, describe the behaviour of \Abs\ outside the representing set $S$. (It follows that $\textit{range}\ f = S$). % (from which it follows that $S$ is $\textit{range}\ f$ % is the representing set). \begin{verbatim} obin_int_obin = "int_to_obin (onum_of n) = mk_norm_obin n" int_word_uint = "uint (word_of_int a) = a mod 2 ^ len_of TYPE('a)" unat_of_nat = "unat (of_nat (n::nat)) = n mod 2 ^ len_of TYPE('a)" \end{verbatim} % \subsection{Normalisation functions in type definition theorems} We therefore defined an extended type definition predicate, as follows: \begin{verbatim} "td_ext Rep Abs A norm == type_definition Rep Abs A & (ALL y. Rep (Abs y) = norm y)" \end{verbatim} and we have extended type definition theorems including the following: \begin{verbatim} td_ext_int_obin = "td_ext int_to_obin onum_of (Collect is_norm_obin) mk_norm_obin" td_ext_ubin = "td_ext uint word_of_int (uints (len_of TYPE('a))) (bintrunc (len_of TYPE('a)))" td_ext_sbin = "td_ext sint word_of_int (sints (len_of TYPE('a))) (sbintrunc (len_of TYPE('a) - 1))" td_ext_uint = "td_ext uint word_of_int (uints (len_of TYPE('a))) (%i. i mod 2 ^ len_of TYPE('a))" td_ext_unat = "td_ext unat of_nat (unats (len_of TYPE('a))) (%i. i mod 2 ^ len_of TYPE('a))" \end{verbatim} % td_ext_sint = "td_ext sint word_of_int (sints (len_of TYPE('a))) % (%i. (i + 2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) - % 2 ^ (len_of TYPE('a) - 1))" % td_ext_nth = "td_ext word_nth of_nth % {f. ALL i. f i --> i < len_of TYPE('a)} % (%h i. h i & i < len_of TYPE('a))" % It follows from the fact that Since $\texttt{Abs}\ (\texttt{Rep}\ x) = x$ it follows that $\texttt{norm} \circ \texttt{norm} = \texttt{norm}$, so we call it a normalisation function; we say $x$ is normal if $x = \norm\ y$ for some $y$, equivalently if $x = \norm\ x$. % Other useful simplifications also follow: We also have $\texttt{norm} \circ \texttt{Rep} = \texttt{Rep}$, and $\texttt{Abs} \circ \texttt{norm} = \texttt{Abs}$. As we frequently had to transfer results about a function on one type to a corresponding function on another type % (for example, \obin s to \bin s, as mentioned earlier) we formalised some general relevant results. Consider a function $f : \rho \to \rho$, where $\rho$ is the representing type in a type definition theorem with normalisation function \norm. % We write $x \sim y$, $x$ and $y$ are \norm-equiv[alent], We say $x$ and $y$ are \norm-equiv[alent] to mean $\norm\ x = \norm\ y$. Then some or all of the following identities may hold: \\[2ex] % % SPACE HERE % % SPACE HERE %\noindent % \begin{center} \begin{tabular}{l@{\quad}l} $\texttt{norm} \circ f \circ \texttt{norm} = \texttt{norm} \circ f$ & $f$ takes \norm-equiv arguments to \norm-equiv results \\[-1ex] % if $x \sim y$ then $f\ x \sim f\ y$ \\[-1ex] $\texttt{norm} \circ f \circ \texttt{norm} = f \circ \texttt{norm}$ & $f$ takes normal arguments to normal results \\[-1ex] $\texttt{norm} \circ f = f \circ \texttt{norm}$ & both of the above \\[-1ex] $f \circ \texttt{norm} = f$ & $f$ takes \norm-equiv arguments to the same result \\[-1ex] $\texttt{norm} \circ f = f$ & $f$ takes every argument to a normal result \end{tabular} \\[1ex] % \end{center} Consider functions $f : \rho \to \rho$ and function $h : \alpha \to \alpha$, where $\rho$ and $\alpha$ are the representing and abstract types in a type definition theorem. These can be related in any of the following ways. \begin{eqnarray} h &=& \texttt{Abs} \circ f \circ \texttt{Rep} \label{h=afr} \\ \texttt{Rep} \circ h &=& f \circ \texttt{Rep} \label{rh=fr} \\ h \circ \texttt{Abs} &=& \texttt{Abs} \circ f \label{ha=af} \\ \texttt{Rep} \circ h \circ \texttt{Abs} &=& f \label{rha=f} \end{eqnarray} Of these, (\ref{h=afr}) would be the typical way to define $h$ in terms of $f$, and (\ref{rha=f}) provides the most useful properties, as it implies all the rest; they all imply (\ref{h=afr}). As for the inverse implications, we obtained a number of general results showing when they are available, depending on which of the properties about \norm\ and $f$ above are satisfied (see \sfile{TdThs.thy}). For example, where \norm\ is $\bintrunc\ n$, truncation of a \bin\ to $n$ bits, and $f$ is addition (with \emph{two} arguments), then $f$ takes \norm-equiv arguments to \norm-equiv results. This is the key to obtaining the result \verb|wi_hom_add| shown earlier, of the form of (\ref{ha=af}) above, from the definition \verb|word_add_wi|, of the form of (\ref{h=afr}). A similar situation applied in deriving \verb|word_no_log_defs| (see \S\ref{s-simps}). On the other hand, if $f$ is \verb|bin_rest|, or division by 2, and $h$ is \verb|ushiftr1|, unsigned one-bit shift right, then $f$ takes normal arguments to normal results, and when \verb|ushiftr1| is defined from \verb|bin_rest| by (\ref{h=afr}), equality (\ref{rh=fr}) also holds. % These results were also particularly useful % previously, % when we used them to prove properties % of algebraic operations on \bin s from % properties of the corresponding operations on \obin s. Each type definition theorem is used by the Standard ML (SML) functors \texttt{TdThms} or \verb|TdExtThms| to generate a number of consequences, which are collected in structures such as \texttt{word} and \texttt{int\_obin}. \begin{verbatim} structure word = TdThms (struct ... type_definition_word ... end) ; structure int_obin = TdExtThms (struct ... td_ext_int_obin ... end) ; \end{verbatim} \comment{ and likewise in structures \texttt{word\_uint}, \texttt{word\_sint}, \texttt{word\_unat}, \texttt{word\_ubin}, \texttt{word\_sbin}, \texttt{word\_bl} and \texttt{word\_nth} derived from the theorems \texttt{td\_ext\_uint}, \texttt{td\_ext\_sint}, \texttt{td\_ext\_unat}, \texttt{td\_ext\_ubin}, \texttt{td\_ext\_sbin}, \texttt{td\_bl} and \texttt{td\_nth}. The theorems generated are also stored in the theorem database, for example \verb|word_uint.Rep_inverse| is stored as \verb|word_uint_Rep_inverse|. The theorems generated by the functor \verb|TdExtThms| are shown in Appendix~\ref{s-tdfun-out}. } We note in particular % the theorems \verb|word_nth.Rep_eqD| and \verb|word_eqI|, derived from it; \verb|word_nth| selects the $n$th bit of a word, and is written infix as \verb|!!|. \begin{verbatim} word_nth.Rep_eqD = "word_nth x = word_nth y ==> x = y" word_eqI = "(!!n. n < size u ==> u !! n = v !! n) ==> u = v" \end{verbatim} The latter was frequently useful in deriving equalities of words. For example, our function \verb|word_cat| concatenates words. We had proved a theorem \verb|word_nth_cat| which gives an expression for \verb|word_cat a b !! n|. Using results like these we could prove two words equal by starting with \verb|word_eqI|, and simplifying. This approach was often useful for proving identities involving concatenating, splitting, rotating or shifting words. In the same way, the theorem \verb|bin_nth_lem| was useful for proving equality of \verb|bin|s, where \texttt{bin\_nth x n} is bit \verb|n| of \verb|x|, using theorems such as \verb|nth_bintr|. \begin{verbatim} bin_nth_lem = "bin_nth x = bin_nth y ==> x = y" nth_bintr = "bin_nth (bintrunc m w) n = (n < m & bin_nth w n)" \end{verbatim} \subsection{Simplifications, \texttt{number\_of}, literal numbers} \label{s-simps} As noted ealier, the type \verb|bin| is used in connexion with the function \texttt{number\_of :: bin => 'a::number} to express literal numbers. When a number (say 5) is entered, it is syntax-translated to \verb|number_of (Pls BIT B1 BIT B0 BIT B1)|. % (To help see this, fold or rewrite the expression using % \verb|number_of_alt_def|). The function \verb|number_of| is defined variously for various types and classes, \eg: \begin{verbatim} int_number_of_alt = "number_of (w::int) :: int == w" word_number_of_def = "number_of (w::bin) :: 'a::len0 word == word_of_int w" \end{verbatim} \subsubsection{ Simplifications for arithmetic expressions} Certain arithmetic equalities, such as associativity and commutativity of addition and multiplication, and distributivity of multiplication over addition, hold for words. We wrote a function \verb|int2lenw| in Standard ML to generate a number of results for words, in \verb|word_arith_eqs|, from the corresponding results about integers. See the file \sfile{WordArith.thy} for details. From these and other results, we showed that the word type is in many of Isabelle's arithmetical type classes (see \sfile{WordClasses.thy}). Therefore many automatic simplifications for these type classes are available for the word type. Thus, for example \verb|a + b + c = (b + d :: 'a :: len0 word)| is simplified to \verb|a + c = d|. Isabelle is set up to simplify arithmetic expressions involving literal numbers as \bin s very effectively, using simplification rules which in effect do binary arithmetic, provided that the type of the numbers is in the class \verb|number_ring|. This is the case for words of positive length; unfortunately this does not work for zero-length words, since Isabelle's \verb|number_ring| class requires $0 \not= 1$. Thus an expression such as \verb|(6 + 5 :: 'a :: len word)| gets simplified to \verb|11| automatically, regardless of the word length, which need not be known. % Another standard simplification involves the predicate \verb|iszero|, % so \verb|(6 + 5 :: word2) = 7| gets simplified to % \verb|iszero (4 :: word2)|. Another standard simplification takes \verb|(6 + 5 :: 'a :: len word) = 7| to \verb|iszero (4 :: 'a :: len word)|. Further simplification of such expressions, \ie, from \verb|(11 :: word2)| to \verb|3| (where \verb|word2| is a type of words of length 2) and from \verb|iszero (4 :: word2)| to \verb|True| depend on the specific word length. We would want to use a theorem like \verb|num_of_bintr|, but we cannot reverse it to use it as a simplification rule because it would loop. Instead we can simplify using \verb|num_abs_bintr| (which is derived from \verb|num_of_bintr| and \verb|word_number_of_def|). \begin{verbatim} num_of_bintr = "number_of (bintrunc (len_of TYPE('a)) (b::bin)) = number_of b" num_abs_bintr = "number_of (b::bin) = word_of_int (len_of TYPE('a)) b" \end{verbatim} We then need to simplify the word length definition, using the theorem giving \verb|len_of TYPE('a)| for the specific type, then simplify using \verb|bintrunc_pred_simps|, which simplifies an expression like \texttt{bintrunc (number\_of bin) (w BIT b)}, and finally apply \verb|word_number_of_def| in the opposite direction. % Note that \verb|bintrunc_pred_simps| is added to the default simpset, % although \verb|bintrunc_minus_simps| is not, % since it can occasionally be a nuisance. Given an expression such as \verb|iszero (4 :: word2)|, we \emph{can} use the theorem \verb|iszero_word_no| as a simplification rule, and it doesn't loop because the type of \verb|number_of ...| (the argument of \verb|iszero ( )|) is a \verb|word| on the left-hand side but is an \verb|int| on the right-hand side. We would then simplify using the rule giving the word length and \verb|bintrunc_pred_simps|. \begin{verbatim} iszero_word_no = "iszero (number_of (bin::bin)) = iszero (number_of (bintrunc (len_of TYPE('a)) bin))" \end{verbatim} A further approach to simplifying a literal \verb|word| is to simplify an expresssion such as \verb|uint (11 :: word2)|, which means converting \verb|(11 :: word2)| to the integer in the range \verb|uints 2|, \ie\ $0 \ldots 2^n -1$. We would simplify using \verb|uint_bintrunc|, the rule giving the word length and \verb|bintrunc_pred_simps|. \begin{verbatim} uint_bintrunc = "uint (number_of (bin::bin)) = number_of (bintrunc (len_of TYPE('a)) bin)" \end{verbatim} Note that in \verb|uint_bintrunc| the two instances of \verb|number_of| have result types \verb|word| and \verb|int| respectively. Corresponding theorems are available for the signed interpretation of a word, and to simplify \unat\ of a literal. % corresponding theorems are % \verb|num_abs_sbintr| and \verb|sint_sbintrunc|, % and the relevant simplifications are \verb|sbintrunc_minus_simps|. % For the interpretation of a word as a \verb|nat|, % the theorem corresponding to \verb|uint_bintrunc| is % \verb|unat_bintrunc|. % This can be confusing, and unfortunately setting % \verb|show_types| or \verb|show_sorts| does not help. % To view types of constants you have to print out the values of type % \verb|term|, % using (eg) the function \verb|prop_of|, or \verb|read|. % \begin{verbatim} % prop_of uint_bintrunc ; % read "uint (number_of b) = number_of b'" ; % \end{verbatim} \subsubsection{Simplifications for logical expressions} These are more difficult because we do not have a built-in type class. The definition of the bit-wise operations, and how from the definitions we obtained simplifications such as \verb|bin_not_simps| and \verb|bin_and_Bits|, is described in \S\ref{s-def-bin}. A literal expression such as \verb|22 && 11| can be simplified first using the (derived) % pseudo-definitions rules \verb|word_no_log_defs| (the actual definitions being \verb|word_log_defs|) \begin{verbatim} word_log_defs = ["u && v == number_of (bin_and (uint u) (uint v))", ...] word_no_log_defs = ["number_of a && number_of b == number_of (bin_and a b)", ...] \end{verbatim} and then using the simplifications such as \verb|bin_and_Bits| (\verb|word_no_log_defs| and many rules for bit-wise logical operations on \bin s are in the default simpset). We derived counterparts for \bin s of commonplace logical identities such as associativity and commutativity of conjunction and disjunction, and others such as $(x \land y) \lor x = x$. We wrote Standard ML code to use these to generate counterparts of these for words, so that one function, \verb|bin2lenw|, sufficed to generate all the corresponding results, found in \verb|word_bw_simps|, about logical bit-wise operations on words. See the file \sfile{WordBitwise.thy} for details. \comment{ We derived, for words, a number of standard logical rules, some of which (\verb|word_not_not|, \verb|word_bw_same|) have been added to the default simpset, but most need to be added explicitly when desired. These are \verb|word_bw_assocs|, \verb|word_bw_comms| and \verb|word_bw_lcs| for AC-simplification for the three operators \verb|&&|, \verb.||. and \verb|xor|, \verb|word_ao_dist|, \verb|word_oa_dist|, \verb|word_not_dist| and \verb|word_add_not'|. } \comment{ SPACE \subsubsection{Simplifications for literals} It was desirable to have automatic simplifications for literal expressions, and that these should be in the default simpset. But to avoid using these where they were not wanted, for a number of theorems $X = Y$, we added only the theorem $\numof\ X = \numof\ Y$ as a default simplification rule. In other cases, we added an equality as a simplification rule only after instantiating its variables to $\numof\ x$. In some further cases we needed to use simplification procedures, which test the form of a term before deciding whether to apply a simplification rule or not. } \subsubsection{Special-purpose simplification tactics} Consider the result (for words) \verb|"(x < x - z) = (x < z)"|: % Consider the result \verb|sub_wrap_lt| (for words): each inequality holds iff calculating $x - z$ causes underflow. % \begin{verbatim} % sub_wrap_lt = "(x < x - z) = (x < z)" % \end{verbatim} Several results required about words, such as this one, could be proved by translating into goals involving sums or differences of integers, together with case analyses as to whether overflow or underflow occurred or not. So we developed tactics for these: \verb|uint_pm_tac| does the following \begin{itemize} \item unfolds definitions of $\leq$, using \verb|word_le_def| (similarly for $<$) \item unfolds occurrences of \verb|uint (a + b)| using \verb|uint_plus_if'| \\ (similarly for \verb|uint (a - b)|) \item for every occurrence of \verb|uint w| in the goal, inserts \verb|uint_range'| \item solves using \verb|arith_tac|, an Isabelle tactic for solving linear arithmetic \end{itemize} \begin{verbatim} word_le_def = "a <= b == uint a <= uint b" uint_plus_if' = "uint (a + b) = (if uint a + uint b < 2 ^ len_of TYPE('a) then uint a + uint b else uint a + uint b - 2 ^ len_of TYPE('a))" uint_range' = "0 <= uint w & uint w < 2 ^ len_of TYPE('a)" \end{verbatim} This proved effective for a reasonable number of goals that arose in practice; it relies on the fact that \verb|arith_tac| is very effective for goals involving $<$, $<=$, $+$ and $-$ for integers. Details of the code are in \sfile{WordArith.thy}. We developed similar routines for \verb|sint|, which were used to solve a problem posed by a referee: to prove that, in signed $n$-bit arithmetic, the addition \mbox{$x + y$} overflows, that is, \texttt{sint x + sint y} $\neq$ \texttt{sint (x+y)}, iff the C language term \verb|(((x+y)^x) & ((x+y)^y)) >> (n - 1)| is non-zero. \subsection{Types containing information about word length} We have defined types which contain information about the length of words. For example, \verb|len_of TYPE(tb t1 t0 t1 t1 t1)| = 23 because \verb|t1 t0 t1 t1 t1| translates to the binary number 10111, that is, 23. The relevant simplification rules (which are axioms, and so in the default simpset) are \begin{verbatim} len_tb : "len_of TYPE (tb) = 0" len_t0 : "len_of TYPE ('a :: len t0) = 2 * len_of TYPE ('a)" len_t1 : "len_of TYPE ('a :: len0 t1) = 2 * len_of TYPE ('a) + 1" \end{verbatim} and so \verb|len_of TYPE(tb t1 t0 t1 t1 t1)| is simplified to 23 automatically. We use the type class mechanism to prevent use of the type \verb|tb t0| (corresponding to a binary number with a redundant leading zero); the class \verb|len| is used for words whose length is non-zero and we used the arity declarations shown, although the instance declarations shown are then deducible. \begin{verbatim} arities tb :: len0 arities t0 :: (len) len0 instance t0 :: (len) len arities t1 :: (len0) len0 instance t1 :: (len0) len \end{verbatim} % \begin{verbatim} % instance t0 :: (len) len % instance t1 :: (len0) len % \end{verbatim} By the \verb|arities| declaration for \verb|t0|, we can make use of a type $\alpha$ \verb|t0| only where $\alpha$ is in the class \verb|len| (indicating a non-zero word length), which prevents using \verb|tb| as $\alpha$. The deduced \verb|instance| results mean that any type $\alpha$ \verb|t1| is of class \verb|len|, and likewise for $\alpha$ \verb|t0|, when $\alpha$ is of class \verb|len|. It is also possible to specify the word length rather than the type, and have the type generated automatically. For example, for a goal with a variable type, \eg\ % \begin{verbatim} % Goal "len_of TYPE(?'a :: len0) = 23" ; % \end{verbatim} \verb|"len_of TYPE(?'a :: len0) = 23"|, repeated use of appropriate introduction rules (\verb|len_no_intros|) will instantiate the variable type \verb|?'a| to \verb|tb t1 t0 t1 t1 t1|. See \sfile{Autotypes.thy} for details, and for further relevant theorems. Brian Huffman of Galois Connections has developed types in a similar way, and syntax translation so that the length can be entered or printed out as part of the type. \subsection{Length-dependent exhaust theorems} \label{s-exh-thms} Consider the goal % \begin{verbatim} \verb;"((x :: word6) >> 2) || (y >> 2) = (x || y) >> 2"; % \end{verbatim} \newline where \verb|x >> 2| means \verb|x|, with bits shifted two places to the right, and \verb;x || y; is bit-wise disjunction. % SPACE % While this is an example of a general theorem which might well % have been provided in the development of the theories, % there would be a large number of such theorems, % not all of which have been provided. % We could prove such a theorem by expanding \verb|x| by % and \verb|y| by \begin{verbatim} x = Pls BIT xa BIT xb BIT xc BIT xd BIT xe BIT xf \end{verbatim} % y = Pls BIT ya BIT yb BIT yc BIT yd BIT ye BIT yf (similarly \verb|y|) and calculating both sides by simplification. % To enable this we generated a family of theorems, one for each word length. \comment{ USER MANUAL SPECIFIC (Since each theorem for word length $n$ is generated from the one for length $n-1$, it makes sense to generate all the required theorems at once. Currently these have been generated for lengths up to 16, see \verb|word_bin_exhaust_size_eqs| in \sfile{WordDefinition.thy}). Note that these have not been stored in the theorem database since this would flood the output from commands like \verb|thms_containing| and \verb|find_theorems|. } % The theorem for word length 6 is shown. To enable this we generate a theorem for each word length; the one for word length 6 is shown. \begin{verbatim} "[| !!b ba bb bc bd be. w = number_of (Pls BIT b BIT ba BIT bb BIT bc BIT bd BIT be) ==> P; size w = 6 |] ==> P" \end{verbatim} We also generated theorems to express a word as a list of bits; for example, for \verb|x| of length 6, expressing \verb|to_bl x| as \verb|[xf, xe, xd, xc, xb, xa]|. % are in \verb|word_list_exhaust_size_eqs|. \comment{ Each of these lists of theorems has been made into a binary tree (for faster access to particular theorems), so we have the following binary trees: \verb|word_bin_exhaust_size_eqs|, \verb|word_obin_exhaust_size_eqs|, and \verb|word_list_exhaust_size_eqs|. To retrieve a theorem, use (for example) \begin{verbatim} val bex6 = getbt btree_word_bin_exhaust_size_eqs 6 ; \end{verbatim} } Such a theorem can then be instantiated; for example, for the goal above, one would use the theorem for word length 6 twice, instantiating it with \verb|x| and \verb|y| respectively. An example is in \sfile{Word32.ML}. We are also developing techniques for translating a goal into a format suitable for handing over to a SAT solver. This involves expressing a word of length $n$ as a sequence of $n$ bits, and we have used these theorems for this purpose also. \section{Conclusion} The theories we describe have been used extensively in the NICTA's L4.verified project, which requires reasoning about the properties of machine words and their operations. We have discussed how we defined types of words of various lengths, with theorems which apply to words of any length. We have shown how to make definitions about \bin s by a procedure sufficiently resembling primitive recursion to be practical and useful. We have taken advantage of the fact that the set of words is isomorphic to several different sets and used ``pseudo'' type definition theorems to use these and derive relevant results in an efficient and uniform way. Finally we described other useful techniques, such as how to create types which automatically imply the word length, using type constructors corresponding to binary digits. In these theories, where a single type of words has a definite length, definitions and theorems about joining or splitting words were difficult. In this area, using the bit-vector library of PVS \cite{pvs-bitvectors}, with its more powerful type system, might be easier. A noteworthy feature of the work was the value of Standard ML as the user interface language. As described in \S\ref{s-etdts} we used its structures and functors, which were very convenient for generating a large number of theorems of the same pattern without repeating code. We used its capabilities as a programming language to write a number of functions for generating theorems \emph{en masse}, such as the SML function \verb|int2lenw| and \verb|bin2lenw| which were used to generate respectively 15 and 31 theorems about words % in \verb|word_bw_simps| from corresponding theorems about \verb|int|s and \bin s. Coding in SML was also indispensible for the simplification procedures used to provide automatic simplification of literal expressions, for tactics such as \verb|uint_pm_tac|, for generating the theorems of \S\ref{s-exh-thms} for arbitrary $n$, and for HOL-style conversions, which we used in the proofs. Of course, more mundane uses of its capabilities, such as applying a transformation to a list of theorems, was commonplace in our work. \subsubsection{Acknowledgements} %\emph{Acknowledgements} I wish to thank Gerwin Klein and anonymous referees for helpful suggestions, and John Matthews for the contribution of Galois Connections to the present code. \bibliographystyle{plain} \begin{thebibliography}{1} \bibitem{atd} Behzad Akbarpour, Sofi\`ene Tahar \& Abdelkader Dekdouk. Formalization of Fixed-Point Arithmetic in HOL. Formal Methods in System Design 27, 173--200, 2005. \bibitem{pvs-bitvectors} Ricky W Butler, Paul S Miner, Mandayam K Srivas, Dave A Greve, Steven P Miller. A New Bitvectors Library For PVS. NASA, Langley, USA, 1997. \bibitem{l4-word-files} Jeremy Dawson. Isabelle \word\ theory files. NICTA. \url{http://users.rsise.anu.edu.au/~jeremy/isabelle/l4/} \bibitem{fox-arm} Anthony Fox. A HOL Specification of the ARM Instruction Set Architecture. Computer Laboratory, University of Cambridge, 2001. \bibitem{harrison-euclidean} John Harrison. A HOL Theory of Euclidean Space. In Theorem Proving in Higher Order Logics, (TPHOLs 2005). Lecture Notes in Computer Science 3603, 114-129. \bibitem{isabelle} L C Paulson, T Nipkow. Isabelle. \url{http://isabelle.in.tum.de/} \bibitem{l4verified} L4.verified project, NICTA. \url{http://ertos.nicta.com.au/research/l4.verified/} \bibitem{wong} Wai Wong. Modelling Bit Vectors in HOL: the word library. In Higher Order Logic Theorem Proving and its Applications (HUG '93), Lecture Notes in Computer Science 780, 371-384. \end{thebibliography} \comment{ \appendix NOTE - THE APPENDICES ARE NOT INTENDED FOR PUBLICATION \section{Operations in Fox's paper} \label{fox} The paper ``A HOL Specification of the ARM Instruction Set Architecture'' lists a number of operations, as follows. We discuss how these are implemented. Note that none of them are limited to words of length 32, but are available for words of any length (in some cases, except length 0). \subsection{Arithmetic operations: ADD32, MUL32, SUB32, TWO\_COMP32} These are implemented as cases of the overloaded operations: \verb|a + b, a - b, a * b, - a|. In fact we have to use these to make the word types belong to the type class \verb|comm_ring_1|, which gives many useful simplifications and other theorems. Note that since the class \verb|comm_ring_1| requires 0 and 1 to be distinct, some results which are true for words of length zero are not available. \subsection{Bit-wise operations: AND32, OR32, EOR32, ONE\_COMP32} These use the external syntax \verb|a && b|, \verb.a || b., \verb|a xor b| and \verb|~~ a|, with internal names \verb|word_and|, \verb|word_or|, \verb|word_xor| and \verb|word_not| and definitions \verb|word_and_def|, \verb|word_or_def|, \verb|word_xor_def| and \verb|word_not_def|. \subsection{Bit selection operations: LSB32, MSB32, BIT32} These correspond to the functions \verb|word_lsb|, \verb|word_msb| and \verb|word_nth|. \subsection{Operations involving the numerical value of a word: W32\_NUM, BIT} W32\_NUM is simply the representation function \verb|unat| described above. BIT can be represented by translating its second argument to a word, so BIT $m n$ = \verb|word_nth m (of_nat n)|. \subsection{Bit shift operations: LSL32, LSR32, ASR32, RRX32} The functions corresponding to LSL32, LSR32 and ASR32 are based on the definitions \verb|shiftl1|, \verb|ushiftr1| and \verb|sshiftr1|, which shift bits left or right by just one place, and \verb|shiftl|, \verb|ushiftr| and \verb|sshiftr|, which shift bits left or right by a given number of places (these also have infix syntax as shown below). (The \verb|u| and \verb|s| in the right shift functions stand for unsigned or signed). Corresponding to RRX32 is \verb|bshiftr1|. Theorems relating these to the numeric values include \begin{verbatim} ushiftr_div_2n = "uint (?w >> ?n) = uint ?w div 2 ^ ?n" sshiftr_div_2n = "sint (?w >>> ?n) = sint ?w div 2 ^ ?n" shiftl_t2n = "?w << ?n = 2 ^ ?n * ?w" shiftl1_number = "shiftl1 (number_of ?w) = number_of (?w BIT bit.B0)" \end{verbatim} There are also theorems expressing these operations in terms of the corresponding lists of booleans. \begin{verbatim} shiftl1_bl = "to_bl (shiftl1 ?w) = tl (to_bl ?w) @ [False]" ushiftr1_bl = "to_bl (ushiftr1 ?w) = False # butlast (to_bl ?w)" sshiftr1_bl = "to_bl (sshiftr1 ?w) = hd (to_bl ?w) # butlast (to_bl ?w)" bshiftr1_bl = "to_bl (bshiftr1 ?b ?w) = ?b # butlast (to_bl ?w)" \end{verbatim} Notice that, of these results, \verb|shiftl1_t2n| refers to multiplication of \verb|word|s. To simplify a literal, \verb|shiftl_def| and \verb|shiftl1_number| may be used, but note that this will simplify \verb|shiftl1 (27 :: word4)| to \verb|54|. Further simplification can use the word length, as described above. \subsection{Rotation operations: ROL32, ROR32} These are implemented as \verb|word_rotl| and \verb|word_rotr|. These are defined in terms of the corresponding list operations which are in turn defined in terms of the corresponding single-step list operations \verb|rotate| (supplied with Isabelle/HOL) and \verb|rotater| (defined in theory \verb|Flwops|). After proving that these operations are mutually inverse, we then define rotation by an integer (positive or negative) number of places: then the theorems shown encapsulate a number of different theorems which could be proved for words (and in fact were proved for lists, as \verb|rotater_eqs|, \verb|rotate_inv_plus|, \verb|rotate_gal|, etc), about left rotation, right rotation and combinations of them. \begin{verbatim} word_rotl_def = "word_rotl ?n ?w == of_bl (rotate ?n (to_bl ?w))" word_rotr_def = "word_rotr ?n ?w == of_bl (rotater ?n (to_bl ?w))" word_roti_def = "word_roti ?i ?w == if 0 <= ?i then word_rotr (nat ?i) ?w else word_rotl (nat (- ?i)) ?w" word_roti_add = "word_roti (?m + ?n) ?w = word_roti ?m (word_roti ?n ?w)" word_roti_conv_mod' = "word_roti ?n ?w = word_roti (?n mod int (size ?w)) ?w" \end{verbatim} \section{Example result of functor \texttt{TdExtThms}} \label{s-tdfun-out} Here we show the set of consequences of the extended ``type definition'' theorem \verb|td_ext_ubin| (shown below as \verb|td_ext_thm|); the resulting structure is \verb|word_ubin|, produced by \begin{verbatim} structure word_ubin = TdExtThms (struct val td_name = "word_ubin" ; val td_ext_thm = td_ext_ubin end) ; \end{verbatim} The contents of structure \verb|word_ubin| are shown below. \begin{verbatim} open word_ubin ; val norm_eq_iff = "(bintrunc (len_of TYPE(?'a)) ?x = bintrunc (len_of TYPE(?'a)) ?y) = (word_of_int ?x = word_of_int ?y)" val range_norm = "range (bintrunc (len_of TYPE(?'a))) = uints (len_of TYPE(?'a))" : thm val set_Rep_Abs = "uints (len_of TYPE(?'a)) = range (uint o word_of_int)" : thm val td_thm = "type_definition uint word_of_int (uints (len_of TYPE(?'a)))" : thm val Rep_eqD = "uint ?x = uint ?y ==> ?x = ?y" val Rep_comp_inverse = "uint o ?f = ?g ==> word_of_int o ?g = ?f" val eq_norm = "uint (word_of_int ?x) = bintrunc (len_of TYPE(?'a)) ?x" : thm val set_Rep = "uints (len_of TYPE(?'a)) = range uint" val td_name = "word_ubin" : string val Abs_inj_on = "inj_on word_of_int (uints (len_of TYPE(?'a)))" val Abs_induct = "(!!y. y : uints (len_of TYPE(?'a)) ==> ?P (word_of_int y)) ==> ?P ?x" : thm val norm_Rep = "bintrunc (len_of TYPE(?'a)) (uint ?x) = uint ?x" val norm_norm = "bintrunc (len_of TYPE(?'a)) o bintrunc (len_of TYPE(?'a)) = bintrunc (len_of TYPE(?'a))" val Abs_inject = "[| ?x : uints (len_of TYPE(?'a)); ?y : uints (len_of TYPE(?'a)) |] ==> (word_of_int ?x = word_of_int ?y) = (?x = ?y)" val Abs_inverse = "?y : uints (len_of TYPE(?'a)) ==> uint (word_of_int ?y) = ?y" val td_ext_thm = "td_ext uint word_of_int (uints (len_of TYPE(?'a))) (bintrunc (len_of TYPE(?'a)))" val comp_Abs_inverse = "?f o word_of_int = ?g ==> ?g o uint = ?f" val Abs_cases = "(!!y. [| ?x = word_of_int y; y : uints (len_of TYPE(?'a)) |] ==> ?P) ==> ?P" val Rep_induct = "[| ?y : uints (len_of TYPE(?'a)); !!x. ?P (uint x) |] ==> ?P ?y" : thm val eq_norm' = "uint o word_of_int = bintrunc (len_of TYPE(?'a))" val Abs_inverse' = "[| ?r : uints (len_of TYPE(?'a)); word_of_int ?r = ?a |] ==> uint ?a = ?r" val Rep_inject = "(uint ?x = uint ?y) = (?x = ?y)" val Rep_inverse = "word_of_int (uint ?x) = ?x" val Abs_norm = "word_of_int (bintrunc (len_of TYPE(?'a)) ?x) = word_of_int ?x" val Rep_cases = "[| ?y : uints (len_of TYPE(?'a)); !!x. ?y = uint x ==> ?P |] ==> ?P" : thm val Abs_eqD = "[| word_of_int ?x = word_of_int ?y; ?x : uints (len_of TYPE(?'a)); ?y : uints (len_of TYPE(?'a)) |] ==> ?x = ?y" val inverse_norm = "(word_of_int ?n = ?w) = (uint ?w = bintrunc (len_of TYPE(?'a)) ?n)" : thm val Rep = "uint ?x : uints (len_of TYPE(?'a))" val Rep_inverse' = "uint ?a = ?r ==> word_of_int ?r = ?a" \end{verbatim} } \end{document}