\documentclass{beamer}

\usetheme{Frankfurt}
\usecolortheme{seahorse}
% \usetheme{split}

\newcommand\comment[1]{} 
\AtBeginSection[]
{
   \begin{frame}
       \frametitle{Outline}
       \tableofcontents[currentsection]
   \end{frame}
}
\comment% \AtBeginSubsection[]
{
   \begin{frame}
       \frametitle{Outline}
       \tableofcontents[currentsection,currentsubsection]
   \end{frame}
}
\comment% \AtBeginSubsubsection[]
{
   \begin{frame}
       \frametitle{Outline}
       \tableofcontents[currentsection,currentsubsection,currentsubsubsection]
   \end{frame}
}
\comment{
}

\newcommand\Pls{\texttt{Pls}}
\newcommand\Min{\texttt{Min}}
\newcommand\obin{\texttt{obin}}
\newcommand\bin{\texttt{bin}}
\newcommand\lenof{\texttt{len\_of}}
\newcommand\numof{\texttt{number\_of}}
\newcommand\TYPE{\texttt{TYPE}}
\newcommand\word{\texttt{word}}
\newcommand\itself{\texttt{itself}}
\newcommand\Abs{\texttt{Abs}}
\newcommand\Rep{\texttt{Rep}}
\newcommand\norm{\texttt{norm}}

\newcommand\set{\textit{set}}
\title{Isabelle Theories for Machine Words}
\author{Jeremy Dawson}
\institute{
Logic and Computation Program, NICTA
\thanks{National ICT Australia is funded by the Australian Government's
Dept of Communications, Information Technology and the Arts and
the Australian Research Council through Backing Australia's Ability
and the ICT Centre of Excellence program.}
\and
Automated Reasoning Group,
\\ Australian National University,
   Canberra, ACT 0200, Australia
\\ \url{http://users.rsise.anu.edu.au/~jeremy/} 
}

\begin{document}

\frame{\titlepage}

% \section[Outline]{}
\frame{
  \frametitle{Outline}
  \tableofcontents}

\section{Introduction}
\frame
{
  \frametitle{Introduction}
NICTA's L4.verified project:
to provide a mathematical, machine-checked proof of the
correctness of the L4 microkernel \\ ~

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, 

  \begin{itemize}
\item 
addition and multiplication can overflow, with overflow bits being lost,
\item 
and there are bit-wise operations which are simply defined in a natural way.
  \end{itemize}
  }

\subsection{The Isabelle theorem prover}
\frame
{
  \frametitle{The Isabelle theorem prover}
  \begin{itemize}
\item 
Logical framework: logic (``meta-logic'') is 
intuitionistic polymorphically-typed higher-order logic
\item 
Choice of ``object logic'': we use HOL, ``Higher-Order Logic'':
\begin{itemize}
\item uses type system of meta-logic
\item classical
\item Axiom of Choice
\end{itemize}
\item This HOL object logic inspired by HOL theorem prover
\item Both Isabelle and HOL are LCF-based, written in Standard ML
\item User interaction via Standard ML or Isar
  \end{itemize} 
  }

\subsection{Comparing Related Work}
\frame
{
  \frametitle{Related Work in the HOL prover}
Wai Wong
  \begin{itemize}
\item words are lists of bits.
\item The type is all words of any length; 
\item Some theorems conditional on word length 
\item Bit-wise operations, but no arithmetic operations.
  \end{itemize}
\pause 
Fox
  \begin{itemize}
\item machine word type is isomorphic to the naturals,
\item \texttt{W32} $n$ is the word with unsigned value 
$n \bmod 2^{32}$.
\item equality of machine words is \emph{not} equality of
their representations.
  \end{itemize}
\pause 
Harrison
  \begin{itemize}
\item  encodes vectors of dimension $n$ of (reals, bits, etc)
\item  a type cannot be parameterised over the value $n$.
\item uses type $N \to A$, 
where $N$ is a \emph{type} with exactly $n$ values.
  \end{itemize}
  }

\frame
{
  \frametitle{Other Related Work}
PVS
  \begin{itemize}
\item in PVS,
 a type \emph{can} be parameterised over a value $n$
\item a bit-vector is a function from $\{0,\ldots,N-1\}$ to the booleans
\item PVS bit-vector library provides interpretations of a bit-vector as 
unsigned or signed integers
\item may be better when concatenating or splitting words 
(involving words of length $n$, $m$, $n + m$) 
  \end{itemize}
  }

\frame
{
  \frametitle{Our Formalisation}
  \begin{itemize}
  \item 
 each type of words in our formalization
is of a given length.
  \item
word types related to integers mod $2^n$ and to
lists of booleans
\item many results re
arithmetic and logical (bit-wise) operations.
  \item recent collaboration with Galois Connections \\
(theirs more general: integers modulo $m$, for ours $m = 2 ^ n$).
\item Lots of operations on words which are not discussed here
\item Isabelle code files are available 
  \end{itemize}
  }

\section{The word-$n$ theories}

\subsection{Numerical $n$-bit quantities: 
  the \texttt{bin} and \texttt{obin} types}

\frame
{
  \frametitle{the \texttt{bin} type}
Isabelle's \texttt{bin} type explicitly represents bit strings, 
important as
\begin{itemize}
\item used for encoding numbers literally,
an integer entered is converted to 
  a \texttt{bin}, thus \texttt{read "3"} gives \\
  \texttt{number\_of} \texttt{(Pls BIT B1 BIT B1 ::\ bin)} \\
\item much built-in numeric simplification 
  for numbers expressed as \texttt{bin}s, for example for 
  negation, addition and multiplication, using usual rules
  for twos-complement integers.
\end{itemize}
  }

\frame
{
  \frametitle{the old and new \texttt{bin} types}
Isabelle had changed:
formerly \texttt{bin} was a datatype: constructors

\begin{itemize}
\item \texttt{Pls} (a sequence of 0, extending infinitely leftwards)
\item \texttt{Min} (a sequence of 1, extending infinitely leftwards)
(for the integer $-1$)
\item \texttt{BIT} (where \texttt{(w::bin) BIT (b::bool)} is \texttt{w} with
\texttt{b} appended on the right)
\end{itemize}

% Omit following lines for short version 
Now call these \texttt{oPls, oMin, OBIT},
for the datatype \texttt{obin}. \\ ~

After the change (in Isabelle 2005) \texttt{bin} is an abstract type,
isomorphic to the set of all integers \\
$w\ \texttt{BIT}\ b = 2 w + b$ \qquad \texttt{Pls} = 0 \qquad \texttt{Min} = -1
}

% following slide for short version
\comment% \frame
{
  \frametitle{Issues about the definitions of \bin s} 
  Advantages of the datatype (constructor-based) definition: 
  \begin{itemize}
  \item primitive recursive definitions
  \item structural induction
  \item structure-based case analysis
  \end{itemize}

  ~

  Disadvantages of the datatype definition: \\
\texttt{Pls OBIT False} and 
\texttt{Pls} represent the same sequence of bits 
(also \texttt{Min BIT True} to \texttt{Min})

So we \emph{normalised} \bin s
by changing \texttt{oPls OBIT False} to 
\texttt{oPls}

Similarly \texttt{oMin OBIT True} to \texttt{oMin}. 
(This added complexity) \\ ~

The paper tells how, using the new definition,
we (in part) recovered the 
advantages of a datatype based on constructors
}

% \comment{ following slides for longer version 
\frame
{
  \frametitle{Natural definitions using the \texttt{obin} datatype} 
Using \texttt{obin} datatype allows 
natural definition of functions by their action on bits \\[1ex]

% Eg, for bit-wise complementation:

\begin{tt}
primrec \\
  ~~ obin\_not\_Pls : "obin\_not oPls = oMin" \\
  ~~ obin\_not\_Min : "obin\_not oMin = oPls" \\
  ~~ obin\_not\_OBIT : \\
  \hfill
  "obin\_not (w OBIT x) = (obin\_not w OBIT Not x)"
\end{tt} \\[1ex]

% Defining bit-wise conjunction (two
% arguments) conceptually similar  \\[1ex]

Defining arithmetic operations: close to twos-complement arithmetic
as in the hardware \\[1ex]

Easy to be sure that it is accurate: 
this is important for formal verification!!
}

\comment% don't really need this slide \frame
{
  \frametitle{\texttt{obin\_last} and \texttt{obin\_rest}}
These give the last bit and the remainder, respectively.

Also defined by primitive recursion
as \texttt{obin} is a datatype 

~

\begin{tt}
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{tt}
}

\frame
{
  \frametitle{Normalising {\obin}s}
% In a \emph{normalised} {\obin}, \texttt{oPls OBIT False} does not appear,
% as it represents the 
% same sequence of bits as \texttt{oPls}. \\ ~

We normalise an \texttt{obin} by changing \texttt{oPls OBIT False} to 
\texttt{oPls}, as they represent the same sequence of bits \\ 
and likewise \texttt{oMin OBIT True} to \texttt{oMin}. \\ ~

Set of normalised \texttt{obin}s
isomorphic to the set of integers, \\
via the usual twos-complement representation (PROVE IT!) \\ ~

This issue added to the complexity of using \obin s
}

\comment% briefer above \frame
{
  \frametitle{Normalising {\obin}s}
In a \emph{normalised} {\obin}, \texttt{oPls OBIT False} does not appear,
as it represents the 
same sequence of bits as \texttt{oPls}. \\ ~

We normalise an \texttt{obin} by changing \texttt{oPls OBIT False} to 
\texttt{oPls}, and likewise \texttt{oMin OBIT True} to \texttt{oMin}. \\ ~

Set of normalised \texttt{obin}s
isomorphic to the set of integers, \\
via the usual twos-complement representation (PROVE IT!) \\ ~

The following functions relate to normalising {\obin}s:

\begin{tt}
mk\_norm\_obin ::\ "obin => obin" \\
is\_norm\_obin ::\ "obin => bool"
\end{tt} \\ ~

Need to prove lots of lemmas
about normalisation of \texttt{obin}s 

}

\frame
{
  \frametitle{More problems of using the \obin\ type}

need to deal with words entered literally:
\texttt{6 :: 'a word} is read as \texttt{number\_of}
\texttt{(Pls BIT B1 BIT B1 BIT B0)} \\ ~

% want simplifications acting on the \bin\ type: 
% needed a function \texttt{bin\_and},
need simplifications
for bit-wise (eg) conjunction of such \bin s \\ ~

As \texttt{bin} is not a datatype, 
we first defined \texttt{bin\_and} from \texttt{obin\_and} 

\begin{tt}
bin\_and\_def : "bin\_and v w ==  \\
  \hfill onum\_of (obin\_and (int\_to\_obin v, int\_to\_obin w))"
\end{tt} \\ ~

Lots of simplification theorems about \obin s
had to be transferred to \bin s --- complex programming required
}

\subsubsection{Using datatype-like properties of \bin s}
\frame
{
  \frametitle{Using datatype-like properties of \bin s}
Want to define functions 
in terms of the bit-representation of a \bin \\[1ex]

What properties of \bin\ type
resemble properties of a datatype? \\[1ex]

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}
\vspace{1ex}

consider \bin\ type with ``pseudo-constructors''
\texttt{Pls}, \texttt{Min} and \texttt{BIT} \\[1ex]

In terms of these ``pseudo-constructors'' 
\ref{inj} and \ref{exhaust} above hold:
in fact \ref{exhaust} holds using \texttt{BIT} alone
}

\frame
{
  \frametitle{Defining functions on \bin s}
Those properties give these theorems; 
\texttt{bin\_exhaust} enables us to express any \bin\ 
appearing in a proof as \texttt{w BIT b} \\[1ex]

\begin{tt}
BIT\_eq = "u BIT b = v BIT c ==> u = v \& b = c" \\
bin\_exhaust = "(!!x b. bin = x BIT b ==> Q) ==> Q"
\end{tt} \\[1ex]
\begin{tt}
bin\_rl\_def : "bin\_rl w == SOME (r, l).\ w = r BIT l" \\[1ex]
\end{tt} 

% The \texttt{SOME} function:
% \texttt{"P w ==> P (SOME x.\ P x)"}, \\
Since there is a unique choice of \texttt{r} and \texttt{l} to satisfy
\texttt{w = r BIT l}, this means that
\texttt{bin\_rl (r BIT l) = (r, l)} \\[1ex]

% \begin{tt}
% bin\_rest\_def : "bin\_rest w == fst (bin\_rl w)" \\
% bin\_last\_def : "bin\_last w == snd (bin\_rl w)"
% \end{tt} \\[1ex]
% 
% Then simplification rules follow: \\
% \texttt{bin\_last (w BIT b) = b} \\
% \texttt{bin\_rest (w BIT b) = w} \\
% \texttt{bin\_last Pls = bit.B0}, etc. \\[1ex]

Induction principle for \bin s:

\begin{tt}
bin\_induct = "[| P Pls; P Min; \\
  \hfill !!bin bit. P bin ==> P (bin BIT bit) |] ==> P bin"
\end{tt}

}

\frame
{
  \frametitle{Imitating primitive recursion for \bin s}
To define a function \texttt{f} by primitive recursion, \\
if \bin\ were a datatype with its three constructors, 
require 
\begin{itemize}
\item values \texttt{vp} and \texttt{vn} 
for \texttt{f Pls} and \texttt{f Min},
\item a function \texttt{fr}, where \texttt{f (w BIT b)} is given by 
\texttt{fr w b (f w)}
\end{itemize}

So, using Isabelle's \texttt{recdef} (for recursive functions),
we defined 
$$\texttt{bin\_rec} : \alpha \to \alpha \to 
  (\texttt{int} \to \texttt{bit} \to \alpha \to \alpha) 
  \to \texttt{int} \to \alpha$$
which, given \texttt{vp} \texttt{vn} and \texttt{fr},
returns a function \texttt{f} satisfying

\begin{tt}
f Pls = vp\\
f Min = vn
\end{tt}

and, \alert{except} where \texttt{w BIT b} equals \texttt{Pls} or \texttt{Min}, 

\begin{tt}
f (w BIT b) = fr w b (f w)
\end{tt} \\ ~

Usually
we can prove that this last equation holds for \emph{all} 
\texttt{w} and \texttt{b}
% making a convenient simplification rule.
}

\frame
{
  \frametitle{Examples of definitions on \bin s} 
\begin{tt}
  bin\_not\_def : "bin\_not == bin\_rec Min Pls  \\
    ~ (\%w b s.\ s BIT bit\_not b)" \\[1ex]
\end{tt} 

After making these definitions, the simplification rules in the desired form
(such as those shown below) need to be proved.  \\[1ex] 

\begin{tt}
bin\_not\_simps = [... , \\
    ~~ "bin\_not (w BIT b) = bin\_not w BIT bit\_not b" ]  \\[1ex]
\end{tt} 

Proving these was fairly straightforward \\ ~
\pause

\begin{tt}
  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))" \\[1ex]
\end{tt} 

\begin{tt}
bin\_and\_Bits = "bin\_and (x BIT b) (y BIT c) =  \\
~~     bin\_and x y BIT bit\_and b c"  
\end{tt} 
}
% end of comment, slides omitted for shorter version}

\subsection{The type of fixed-length words of given length}

\frame
{
  \frametitle{A type for $n$-bit quantities}

Need to set up a type in which the length of words is implicit. \\[1ex]

dependent types not allowed:
lists of length $n$ cannot be a type  \\[1ex]

Our solution: the type of words of length $n$ is $\alpha\ \word$ \\[1ex]

where the word length can be deduced from
the type $\alpha$. \\[1ex]

% (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
(a ``canonical'' value for each type) \\[1ex]

% The function \lenof\ is declared, with polymorphic type 
% ($\alpha$, printed as \texttt{'a}, being a type variable)

\begin{tt}
len\_of ::\ "'a ::\ len0 itself => nat" \\
word\_size :\ "size (w ::\ 'a word) = len\_of TYPE('a)"
\end{tt} \\[1ex]

user must define the value of $\lenof\ \TYPE(\alpha)$
for each specific $\alpha$.
}

\frame
{
  \frametitle{Constructing $n$-bit quantities; the type definition: }
``truncation'' functions  \texttt{bintrunc} (unsigned), \\
and \texttt{sbintrunc} (signed)
 to create $n$-bit quantities. 

\begin{itemize}
\item cut down a longer argument
by deleting high-order bits.
\item 
extend a shorter argument it to the left with 
zeroes (unsigned) or its most significant bit (signed)
\end{itemize}

Isabelle \texttt{typedef} defines a new type isomorphic to a given set. \\ ~

\begin{tt}
typedef 'a word = "uword\_len (len\_of TYPE('a))" \\
"uword\_len len == range (bintrunc len)"\\
\end{tt}
}

  \subsection{Sets isomorphic to the set of words}
\frame
{
  \frametitle{Isomorphisms of set of words}
type of words of length $n$ defined isormorphic to \\
\texttt{range (bintrunc n)}, but also isomorphic to
the set of 
\begin{itemize}
\item integers in the range $0 \ldots 2^n -1$
\item integers in the range 
$-2^{n-1} \ldots 2^{n-1}-1$
\item naturals up to $2^n - 1$
\item lists of booleans of length $n$
\item functions $f : \textit{nat} \to \textit{bool}$
such that for $i \geq n$, $f\ i = $ \texttt{False} 
\end{itemize}
}

\frame
{
\frametitle{Pseudo type definition theorems} 
defining new type $\alpha$ from $S : \rho\ \set$ gives \\[1ex]

$\Abs : \rho \to \alpha$ and $\Rep : \alpha \to \rho$: \\[1ex]

mutually inverse bijections between $S$ and the 
values of type $\alpha$  \\[1ex]

% Domain of \Abs\ is the type $\rho$,
nothing known about values of \Abs\ outside $S$   \\[1ex]

Theorem (axiom) \texttt{type\_definition\_}$\alpha$
created for the new type $\alpha$ \\
\texttt{type\_definition} \Rep\ \Abs\ $S$ \\[1ex] 

We can use the predicate \texttt{type\_definition} to express the 
other isomophisms of the set of $n$-bit words mentioned above \\[1ex]

We used SML functors to prove a collection of useful consequences 
of each such isomophism (can also use locales)
}

\frame
{
  \frametitle{Extended type definition theorems} 
type definition theorems do not say anything about
the action of \Abs\ outside the set $S$ \\[1ex]

But our \Abs\ functions
behave ``sensibly'' outside $S$ \\[1ex]

Thus \texttt{word\_of\_int} (ie, \Abs)
which turns an integer in 
$0 \ldots 2^n -1$ into a word, 
takes $i$ and $i'$ to the same word iff $i \equiv i' \pmod{2^n}$ \\[1ex]

Call $\Rep \circ \Abs$ \emph{normalise}, \norm.
(eg, $\norm\ i = i \pmod{2^n}$) \\[1ex]

Say $x$ is normal if $x = \norm\ y$ for some $y$,
iff $x = \norm\ x$ \\[1ex]

In many cases, have extended 
``extended type definition theorems'', of the form
\texttt{td\_ext Rep Abs A norm} \\[1ex]

Generated numerous results from each of these
eg ${\norm} \circ {\Rep} = {\Rep}$,
and ${\Abs} \circ {\norm} = {\Abs}$ \\[1ex]
}

\comment% omit for AVoCS talk \frame
{
  \frametitle{normalisation properties of functions}
Let $\rho$ and $\alpha$ be the
representing and abstract types in a type definition
theorem with normalisation function \norm\ \\[1ex]

We say $x$ and $y$ are \norm-equiv[alent]
to mean $\norm\ x = \norm\ y$ \\[1ex]

Consider a function $f : \rho \to \rho$ \\[1ex]

Then some or all of the following identities may hold: 
\begin{enumerate}
\item \label{n1}
  $\texttt{norm} \circ f \circ \texttt{norm} = \texttt{norm} \circ f$ \\ 
\hfill $f$ takes \norm-equiv arguments to \norm-equiv results 

\item \label{n2}
  $\texttt{norm} \circ f \circ \texttt{norm} = f \circ \texttt{norm}$ \\ 
\hfill $f$ takes normal arguments to normal results 
\item \label{n3} $\texttt{norm} \circ f = f \circ \texttt{norm}$  
\hfill both of the above 
\end{enumerate}

Examples: addition of integers satisfies \ref{n1} only; \\
1-bit shift right ($i \to i/2$) satisfies \ref{n2} only
}


\comment% omit for AVoCS talk \frame
{
  \frametitle{Functions defined on the representing type}

Consider functions $f : \rho \to \rho$ 
and function $h : \alpha \to \alpha$ \\[1ex]

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}
(\ref{h=afr}) would be the typical way to define $h$ in terms of $f$ \\[1ex]
(\ref{rha=f}) implies all the rest; they all imply (\ref{h=afr}) \\[1ex]
Reverse implications may hold, related to 
properties about \norm\ and $f$ above 
}

\subsection{Simplifications for arithmetic expressions}
\frame
{
  \frametitle{Simplifications for arithmetic expressions}

Certain arithmetic equalities hold for words, eg \\
associativity and commutativity of addition and multiplication \\
and distributivity of multiplication over addition \\[1ex]

Single function \texttt{int2lenw} in Standard ML to generate 
these from corresponding results for integers \\[1ex]

showed word type in many of Isabelle's arithmetical \emph{type classes} \\[1ex]
Therefore many automatic simplifications for these type classes
are available for the word type \\[1ex]
Thus
\texttt{a + b + c = (b + d ::\ 'a ::\ len0 word)} is simplified to 
\texttt{a + c = d} (uses Isabelle's \emph{simplification procedures})

}

\frame
{
  \frametitle{Simplifications of literals}
Literal numbers syntax-translated, eg \\
5 becomes \texttt{number\_of (Pls BIT B1 BIT B0 BIT B1)} \\[1ex]

For words, define function \texttt{number\_of} by \\
\begin{tt}
  "number\_of (w::bin) ::\ 'a::len0 word == word\_of\_int w"
\end{tt} \\[1ex]

Isabelle simplifies arithmetic expressions involving literal words
by binary arithmetic 
(requires word type in class \texttt{number\_ring}) \\[1ex]

Thus \texttt{(6 + 5 ::\ 'a ::\ len word)} gets simplified
to \texttt{11} automatically, regardless of the word length \\[1ex]

Further simplification
from \texttt{(11 ::\ word2)} to \texttt{3} 
% (where \texttt{word2} is a type of words of length 2)
and from \texttt{iszero (4 ::\ word2)} to \texttt{True}
depend on the specific word length \\[1ex]

Simplifications for bit-wise (logical) operations
depend on simplifications for 
\texttt{bin\_and}, 
\texttt{bin\_not}, etc (discussed earlier) \\[1ex]

\mbox{One ML function translates many logical identities on \bin s to words}
}
\frame
{
  \frametitle{Special-purpose simplification tactics}
result (for words) \texttt{"(x < x - z) = (x < z)"}: \\
each inequality holds iff calculating $x - z$ causes underflow \\[1ex]

tactic \texttt{uint\_pm\_tac} useful for such goals:
 
\begin{itemize}
\item 
unfolds definitions,
 gets goal using \texttt{uint x}, \texttt{uint z}
(integers) and case analysis (if $z \leq x$ then \ldots else \ldots)
\item for every \texttt{uint} $w$ in the goal,
inserts $w \geq 0$ and $w < 2^n$
\item solves using \texttt{arith\_tac}, an Isabelle tactic for 
linear arithmetic
\end{itemize}
Similar tactic for \texttt{sint}: solved test for signed overflow:
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 
\texttt{(((x+y)$\wedge$x) \& ((x+y)$\wedge$y)) >> (n - 1)} is non-zero.
}
  \subsection{Miscellaneous techniques}
\frame
{
  \frametitle{Types containing information about word length}
For example, 
\texttt{len\_of TYPE(tb t1 t0 t1 t1 t1)} = 23
because \texttt{t1 t0 t1 t1 t1}
translates to the binary number 10111, ie, 23 \\[1ex]

\begin{tt}
"len\_of TYPE(tb) = 0" \\
"len\_of TYPE('a ::\ len t0) = 2 * len\_of TYPE('a)" \\
"len\_of TYPE('a ::\ len0 t1) = 2 * len\_of TYPE('a) + 1" \\[1ex]
\end{tt} 

We use the type class mechanism to prevent use of the type \texttt{tb t0}
(corresponding to a binary number with a redundant leading zero) \\[1ex]

Can also specify the word length 
and generate the type automatically.
For goal 
\texttt{"len\_of TYPE(?'a ::\ len0) = 23"},
this instantiates the variable type \texttt{?'a} to 
\texttt{tb t1 t0 t1 t1 t1} \\[1ex]

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.

}
\frame
{
  \frametitle{Length-dependent exhaust theorems} 
goal 
\begin{tt}
((x ::\ word4) >> 2) || (y >> 2) = (x || y) >> 2
\end{tt} 
\\[1ex]
We could prove this by expanding \\
\begin{tt}
x = Pls BIT xa BIT xb BIT xc BIT xd 
\end{tt} \\
(similarly \texttt{y}) and calculating both sides by simplification \\ ~

To enable this we generate a theorem for each word length, eg

\begin{tt}
"[| !!b ba bb bc bd.\\
   w = number\_of (Pls BIT b BIT ba BIT bb BIT bc) ==> P; \\
   size w = 4 |] ==> P" 
\end{tt} \\ ~

also theorems to express a word as a list of bits;
eg, for \texttt{x} of length 4, 
expressing \texttt{to\_bl x} as \texttt{[xd, xc, xb, xa]}
}
\end{document}

\frame
{
  \frametitle{Examples of beamer use}
\begin{block}{title}
block
\end{block}
  \begin{itemize}
  \item<1-2> Normal LaTeX class.
  \item<3-4> \emph{Easy} \alert{overlays}.
  \item<2-3> No external programs needed.      
  \end{itemize}
\color<2-3>{green} green
\color<1-2>{blue} blue

\only<1>{only slide 1}

\only<2-3>{only slide 2-3}

\textbf<1-2>{bf on slide 1-2}

\textbf<3>{bf on slide 3}

\uncover<1>{uncover 1}
\visible<2-3>{visible 2-3}
xxx
\onslide<1-2>{onslide 1-2}
\onslide<3>{onslide 3}
yyy
}