Interface documentation ----------------------- 1. Usage Require Import machint. You don't need (and shouldn't import directly) any of the infrastructure. 2. Modules and types. This library provides the following modules: int8 uint8 mint8 int16 uint16 mint16 int32 uint32 mint32 int64 uint64 mint64 int128 uint128 mint128 Each comes equipped with a type t (e.g. int8.t) - the intent is that you not import these modules directly, but always refer to them by name when using them. The "int" modules are signed integers of the given size; the "uint" modules are unsigned; and the "mint" modules are both, in that there is one type with both the signed operations and unsigned versions of operations where these differ. The signed operations are found in a submodule 's' and the unsigned operations are found in a submodule 'u'; e.g. 32-bit signed divide is mint32.s.div. The "int" and "uint" modules are intended for front-end or user-facing purposes where signedness of the value is a type property, and keeping track of it strictly is useful for all the same reasons types are useful in general. The "mint" modules are intended for back-end or machine-facing uses where such type information has been discarded and the signedness is determined by the choice of operation, as is the case in essentially all machines and assembly languages. Providing all of these increases the complexity of the development, but it is important to have both sets. I have been disappointed to find these missing from machine integer libraries in other languages, particularly some languages purportedly committed to strong typing. Note that the signed integers are two's complement. If you want to work with vintage machines using one's complement or sign-magnitude integers, you are on your own. (Likewise, the library only provides the natural sizes for machines based on 8-bit bytes.) For convenience the bulk of this document specifically describes the int32, uint32, and mint32 modules and ignores the other sizes; but except as explicitly discussed the various sizes offer exactly the same material. 3. Constants Each of the modules comes with these constants: width: nat The bit width of the type. zero: t The zero value one: t The one value. two: t The two value. allones: t The value with all-bits-one, aka "-1". min: t The minimum value. max: t The maximum value. However, for the mint modules the min and max constants are separated based on signedness and are not the same; thus mint32.u.min, mint32.u.max, mint32.s.min, and mint32.s.max are all defined, but mint32.min and mint32.max are not. 4. Sign-independent Operations getbit: t -> nat -> bool getbit x k extracts the k'th bit of x. This is defined for all k; bits beyond the end of the value are 0 (false). shl: t -> nat -> t shl x k shifts x left by k bits. Zeros are shifted in. Only shifts up to (not including) the width are defined, as is the case on most machines. Note that unlike in C the results of shifting into the sign bit (on signed values) are well defined. bitnot: t -> t bitand: t -> t -> t bitor: t -> t -> t bitxor: t -> t -> t Bitwise operations. Note that unlike in C these are fully defined on signed values. eqb: t -> t -> bool Runtime comparison. (Ordered comparisons are signedness-dependent and can be found below.) neg: t -> t add: t -> t -> t sub: t -> t -> t mul: t -> t -> t Basic arithmetic. Note that multiplication is sign-independent because we do not provide the upper word of the result. (If you want the upper word, promote to the larger size first and multiply after.) Division and modulus are sign-dependent and can be found below. 5. Sign-dependent operations In the "int" modules these have the signed form; in the "uint" modules these have the unsigned form. In the "mint" modules the signed form is found in "mint.s" and the unsigned in "mint.u". shr: t -> nat -> t shr x k shifts the value x right by k bits. For unsigned values, zeros are shifted in; for signed values the sign bit is duplicated. ltb: t -> t -> bool leb: t -> t -> bool gtb: t -> t -> bool geb: t -> t -> bool compare: t -> t -> comparison Less than, less than or equal to, greater than, and greater then or equal to, plus the 3-way version. These are runtime forms, suitable for use in code. div: t -> t -> option t mod_: t -> t -> option t Divide and modulus. Because "mod" is a reserved word, it is written with a trailing underscore. If the second argument is zero these return None. getsignbit: t -> bool (Signed types only.) This is a shorthand for getbit x (width - 1). 6. Reduction Lemmas In general, a lemma is provided for every operation and every case where one of the arguments is a constant. These are named operation_constant_position, e.g. bitand_zero_r. Note that for machine integer arguments the written-out names of the constants are used (zero, one, two allones, etc.) but for arguments of type nat (or Z) the digit spellings (0, 1, etc.) are used. For nat (and Z) the names of the other constructors are used directly. The position is left off if there is only one argument. Some lemmas exist for cases where all arguments are constants, in which case the positions are also left off. E.g. getbit_one_0 states that bit 0 of one is true. While some of these lemmas are trivial, in general a library should always have all of them, even those that readily follow from "simpl", because often in the field "simpl" (or its siblings like "cbn") unfold other elements in ways that make a mess. Controlling this explicitly is a nuisance and it is usually easier and more robust to use the reduction lemmas. Also, in the case of this library the module sealing needed for managing the types makes direct evaluation chancy. Note that as of these writings not all combinations actually exist. Missing ones are bugs. 7. Combination Lemmas Similarly, in general a lemma is provided for every operation and every case where one of the arguments is another operation. These are named the same way as the reduction lemmas. The same logic for including them applies as well. Intentional exceptions to this pattern: - Anything reasoning about the bit pattern of multiply, divide, and modulus results. (These are in general too complicated to state to be worthwhile or useful.) - Things that fall into one of the categories below, like add a (add b c). - Most cases involving eqb, which are usually best converted to = instead. 8. Property Lemmas The following lemmas are provided for all comparison-type/boolean operations where they are true: op_refl, reflexivity: op a a = true op_irrefl, non-reflexivity: op a a = false op_symm, symmetry: op a b = op b a op_asymm, asymmetry: op a b = negb (op b a) op_trans, transitivity: op a b = true -> op b c = true -> op a c = true The following lemmas are provided for all arithmetic operations where they are true: op_comm, commutativity: op a b = op b a op_anticomm, anticommutativity: op a b = neg (op b a) op_assoc, associativity: op a (op b c) = op (op a b) c op_involutive, self-cancellation: op (op a) = a 9. Additional Lemmas width_nonzero: width <> 0. zero_not_one: zero <> one. one_not_two: one <> two. zero_not_allones: zero <> allones. Facts about constants. Note that because for width = 1, zero = two and one = allones, lemmas that these are distinct are not available in general, and for now the internal machinery is not adequate to provide them only when width > 1. getbit_beyond: width <= k -> getbit x k = false (Note that width <= k would be more naturally written as k >= width.) This tells us that getbit returns false for positions beyond the width of the type. getbit_eq: (forall k, getbit a k = getbit b k) <-> a = b. getbit_eq': (forall k, k < width -> getbit a k = getbit b k) <-> a = b. Two values are equal if all their bits are the same. The second form uses getbit_beyond to fill in for out-of-range bits, which is sometimes convenient. getbit_shl_right: k < amt < width -> getbit (shl x amt) k = false getbit_shl_left: amt <= k < width -> getbit (shl x amt) k = getbit x (k - amt) getbit_shr_right: amt < width -> k < width - amt -> getbit (shr x amt) k = getbit x (k + amt) getbit_shr_left: amt < width -> width - amt <= k < width -> getbit (shl x amt) k = getsignbit x These are the two halves of getbit_shl and getbit_shr. getbit_shr_left and getbit_shr_right are provided for both signed and unsigned, but are different. In fact, the statement of getbit_shr_left is different; the version above is the signed form. In the unsigned form the conclusion is "false" rather than "getsignbit x". eq_dec: {a = b} + {a <> b} Equality is decidable. compare_eq_eq: compare a b = Eq <-> a = b compare_opp: compare a b = CompOpp (compare b a) compare_trans_lt_lt: compare a b = Lt -> compare b c = Lt -> compare a c = Lt compare_trans_lt_eq: compare a b = Lt -> compare b c = Eq -> compare a c = Lt compare_trans_eq_lt: compare a b = Eq -> compare b c = Lt -> compare a c = Lt compare_trans_eq_eq: compare a b = Eq -> compare b c = Eq -> compare a c = Eq Various properties of comparison. These are provided for both unsigned and signed, but the unsigned and signed versions are necessarily different. 10. Ordering Hooks For all of the modules, submodules for ordering according to both the Orders and OrderedType modules from the standard library are provided. Note that these define an arbitrary ordering suitable for use by the clients of these standard library elements -- the various set and map types in the standard library -- and should not be used for circumstances where a specific ordering is needed. For this reason the elements within the submodules should not in general be used. The submodule OTnew (thus, e.g. uint32.OTnew or int32.OTnew or mint32.OTnew) is an instance of Orders.OrderedType, and the submodule OTold is an instance of OrderedType.OrderedType. You can create a finite map whose key type is int32.t like this: Require Import FMapAVL. Require Import machint. Module uint32map := FMapAVL.Make int32.OTold.