Introduction  The word-n theories

Isabelle Theories for Machine Words

Jeremy Dawson

Logic and Computation Program, NICTA ^{1}

Automated Reasoning Group, Australian National University, Canberra, ACT 0200, Australia

                 http://users.rsise.anu.edu.au/^{∼}jeremy/

August 29, 2007

1National 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.

Outline

1 Introduction

2 The word-n theories

Numerical n-bit quantities: the bin and obin types The type of fixed-length words of given length Sets isomorphic to the set of words Simplifications for arithmetic expressions Miscellaneous techniques

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,

addition and multiplication can overflow, with overflow bits being lost, and there are bit-wise operations which are simply defined in a natural way.

Our Formalisation

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

the bin type

Isabelle’s bin type explicitly represents bit strings, important as used for encoding numbers literally, an integer entered is converted to a bin, thus read "3" gives

number of (Pls BIT B1 BIT B1 :: bin)

much built-in numeric simplification for numbers expressed as bins, for example for negation, addition and multiplication, using usual rules for twos-complement integers.

the old and new bin types

Isabelle had changed: formerly bin was a datatype: constructors

Pls (a sequence of 0, extending infinitely leftwards) Min (a sequence of 1, extending infinitely leftwards) (for the integer −1)

BIT (where (w::bin) BIT (b::bool) is w with b appended

on the right)

After the change (in Isabelle 2005) bin is an abstract type, isomorphic to the set of all integers

w BIT b = 2w + b  Pls = 0  Min = -1

Issues about the definitions of bins

Advantages of the datatype (constructor-based) definition: primitive recursive definitions structural induction structure-based case analysis

Disadvantages of the datatype definition: Pls OBIT False and Pls represent the same sequence of bits

(also Min BIT True to Min)

So we normalised bins by changing oPls OBIT False to oPls Similarly oMin OBIT True to oMin. (This added complexity)

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

Introduction  The word-n theories

A type for n-bit quantities

Need to set up a type in which the length of words is implicit. dependent types not allowed: lists of length n cannot be a type Our solution: the type of words of length n is α word where the word length can be deduced from the type α. We use len of TYPE(α) for the word length. TYPE(α) is a polymorphic value (a “canonical” value for each type)

len of :: "'a :: len0 itself => nat"
word size : "size (w :: 'a word) = len of TYPE('a)"

user must define the value of len of TYPE(α) for each specific α.

Constructing n-bit quantities; the type definition:

“truncation” functions bintrunc (unsigned), and sbintrunc (signed) to create n-bit quantities.

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

Isabelle typedef defines a new type isomorphic to a given set.

typedef 'a word = "uword len (len of TYPE('a))"
"uword len len == range (bintrunc len)"

Isomorphisms of set of words

type of words of length n defined isormorphic to range (bintrunc n), but also isomorphic to the set of

integers in the range 0 … 2^{n} − 1 integers in the range −2^{n−1} … 2^{n−1} − 1 naturals up to 2^{n} − 1 lists of booleans of length n functions f : nat → bool such that for i ≥ n, f i = False

Introduction  The word-n theories

Pseudo type definition theorems

defining new type α from S : ρ set gives Abs : ρ → α and Rep : α → ρ: mutually inverse bijections between S and the values of type α nothing known about values of Abs outside S Theorem (axiom) type definition α created for the new type α

type definition Rep Abs S

We can use the predicate type definition to express the other isomophisms of the set of n-bit words mentioned above We used SML functors to prove a collection of useful consequences of each such isomophism (can also use locales)

Introduction  The word-n theories

Extended type definition theorems

type definition theorems do not say anything about the action of Abs outside the set S But our Abs functions behave “sensibly” outside S Thus word of int (ie, Abs) which turns an integer in 0 … 2^{n} − 1 into a word, takes i and i′ to the same word iff i ≡ i′ (mod 2^{n}) Call Rep ∘ Abs normalise, norm. (eg, norm i = i (mod 2^{n})) Say x is normal if x = norm y for some y, iff x = norm x In many cases, have extended “extended type definition theorems”,

of the form td ext Rep Abs A norm

Generated numerous results from each of these eg

norm ∘ Rep = Rep, and Abs ∘ norm = Abs

Simplifications for arithmetic expressions

Certain arithmetic equalities hold for words, eg associativity and commutativity of addition and multiplication and distributivity of multiplication over addition

Single function int2lenw in Standard ML to generate these from corresponding results for integers

showed word type in many of Isabelle’s arithmetical type classes

Therefore many automatic simplifications for these type classes are available for the word type

Thus a + b + c = (b + d :: 'a :: len0 word) is simplified

to a + c = d (uses Isabelle’s simplification procedures)

Simplifications of literals

Literal numbers syntax-translated, eg

5 becomes number of (Pls BIT B1 BIT B0 BIT B1)

For words, define function number of by

"number of (w::bin) :: 'a::len0 word == word of int w"

Isabelle simplifies arithmetic expressions involving literal words by binary arithmetic (requires word type in class number ring)

Thus (6 + 5 :: 'a :: len word) gets simplified to 11

automatically, regardless of the word length

Further simplification from (11 :: word2) to 3 and from iszero (4 :: word2) to True depend on the specific word length

Simplifications for bit-wise (logical) operations depend on simplifications for bin and, bin not, etc (discussed earlier)

One ML function translates many logical identities on bins to words

Special-purpose simplification tactics

result (for words) "(x < x - z) = (x < z)": each inequality holds iff calculating x − z causes underflow

tactic uint pm tac useful for such goals:

unfolds definitions, gets goal using uint x, uint z (integers) and case analysis (if z ≤ x then … else …) for every uint w in the goal, inserts w ≥ 0 and w < 2^{n} solves using arith tac, an Isabelle tactic for linear arithmetic

Similar tactic for sint: solved test for signed overflow: to prove that, in signed n-bit arithmetic, the addition x + y overflows, that is, sint x + sint y ≠ sint (x+y), iff the C language term

(((x+y)∧x) & ((x+y)∧y)) >> (n - 1) is non-zero.

Types containing information about word length

For example, len of TYPE(tb t1 t0 t1 t1 t1) = 23 because

t1 t0 t1 t1 t1 translates to the binary number 10111, ie, 23

"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"

We use the type class mechanism to prevent use of the type tb t0 (corresponding to a binary number with a redundant leading zero)

Can also specify the word length and generate the type

automatically. For goal "len of TYPE(?'a :: len0) = 23",

this instantiates the variable type ?'a to tb t1 t0 t1 t1 t1

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.

Length-dependent exhaust theorems

goal ((x :: word4) >> 2) || (y >> 2) = (x || y) >> 2

We could prove this by expanding

x = Pls BIT xa BIT xb BIT xc BIT xd

(similarly y) and calculating both sides by simplification

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

"[| !!b ba bb bc bd.
w = number of (Pls BIT b BIT ba BIT bb BIT bc) ==> P;
size w = 4 |] ==> P"

also theorems to express a word as a list of bits; eg, for x of length

4, expressing to bl x as [xd, xc, xb, xa]