Logops-definitions
A book a definitions of logical operations on numbers.
This book, along with logops-lemmas, includes a theory of
the Common Lisp logical operations on numbers, a portable implementation of the
Common Lisp byte operations, extensions to those theories, and some useful
macros.
This book contains only definitions, lemmas necessary to admit those
definitions, and selected type lemmas. By "type lemmas" we mean any lemmas
about the logical operations that we have found necessary to verify the guards
of functions that use these operations. We have separated these "type
lemmas" from the large body of other lemmas in logops-lemmas to allow a
user to use this book to define guard-verified functions without having to also
include the extensive theory in logops-lemmas.
The standard Common Lisp logical operations on numbers are defined on the
signed integers, and return signed integers as appropriate. This allows a high
level, signed interpretation of hardware operations if that is appropriate for
the specification at hand. We also provide unsigned versions of several of the
standard logical operations for use in specifications where fixed-length
unsigned integers are used to model hardware registers and busses. This view
of hardware is used, for example, in Yuan Yu's Nqthm specification of the
Motorola MC68020.
Subtopics
- Logops-byte-functions
- A portable implementation and extension of Common Lisp byte
functions.
- Defword
- A macro to define packed integer data structures.
- Defbytetype
- A macro for defining integer subrange types.
- Logext
- (logext size i) sign-extends i to a size-bit signed
integer.
- Logrev
- Logical reverse. (logrev size i) bit-reverses the size
low-order bits of i, discarding the high-order bits.
- Loghead
- (loghead size i) returns the size low-order bits of i.
- Logops-bit-functions
- Versions of the standard logical operations that operate on single bits.
- Logtail
- (logtail pos i) returns the high-order part of i, starting
at bit position pos.
- Logapp
- (logapp size i j) is a binary append of i to j, where i
effectively becomes the 'low' bits and j becomes the 'high' bits.
- Logsat
- Signed saturation. (logsat size i) coerces i to a
size-bit signed integer by saturation.
- Binary--
- (binary-- x y) is the same as (- x y), but may symbolically
simulate more efficiently in gl.
- Logcdr
- All but the least significant bit of a number.
- Logcar
- Least significant bit of a number.
- Logbit
- (logbit pos i) returns the bit of i at bit-position pos
as a bitp, 0 or 1.
- Logextu
- Logical sign extension, unsigned version. (logextu final-size
ext-size i) "sign-extends" i with (logext ext-size i), then truncates
the result to final-size bits, creating an unsigned integer.
- Logcons
- (logcons b i) is the cons operation for integers,
conceptualized as bit-vectors, where the least significant bit is at the head
of the list.
- Lshu
- Logical shift, unsigned version.
- Logrpl
- Logical replace. (logrpl size i j) replaces the size
low-order bits of j with the size low-order bits of i.
- Ashu
- Arithmetic shift, unsigned version.
- Logmaskp
- (logmaskp i) recognizes positive bit-masks, i.e., numbers of the
form 2^n - 1.
- Lognotu
- Logical negation, unsigned version. (lognotu size i) is an
unsigned logical not. It just truncates (lognot i) to size
bits.
- Logmask
- (logmask size) creates a low-order, size-bit mask.
- Imod
- (imod i j) is the same as mod, except that it coerces its
arguments to integers.
- Ifloor
- (ifloor i j) is the same as floor, except that it coerces
its arguments to integers.
- Bfix
- Bit fix. (bfix b) is a fixing function for bitps. It
coerces any object to a bit (0 or 1) by coercing non-1 objects to 0.
- Bitmaskp
- (bitmaskp i) recognizes positive masks, i.e., numbers of the form
2^n - 1. It is like logmaskp but properly treats non-integers as 0.
- Logite
- Bitwise if-then-else among integers.
- Expt2
- (expt2 n) is the same as (expt 2 n), except that it coerces
its argument to a natural.
- Zbp
- Zero bit recognizer. (zbp x) tests for zero bits. Any object
other than 1 is considered to be a zero bit.
- *logops-functions*
- A list of all functions considered to be part of the theory of logical
operations on numbers.
- Word/bit-macros
- Macros for manipulating integer words defined as contiguous bits.
- Logops-definitions-theory
- The "minimal" theory for the book "logops-definitions".
- Logops-functions
- A theory consisting of all function names of functions considered to
be logical operations on numbers.
- Lbfix
- Logical bit fix. (lbfix b) is logically identical to (bfix
b) but executes as the identity. It requires (bitp b) as a guard, and
expands to just b.
- Logextu-guard
- (logextu-guard final-size ext-size i) is a macro form of the guards for logextu.
- Lshu-guard
- (lshu-guard size i cnt) is a macro form of the guards for lshu.
- Logtail-guard
- (logtail-guard pos i) is a macro form of the guards for logtail.
- Logrpl-guard
- (logrpl-guard size i j) is a macro form of the guards for logrpl.
- Logrev-guard
- (logrev-guard size i) is a macro form of the guards for logrev.
- Lognotu-guard
- (lognotu-guard size i) is a macro form of the guards for lognotu.
- Logmask-guard
- (logmask-guard size) is a macro form of the guards for logmask.
- Loghead-guard
- (loghead-guard size i) is a macro form of the guards for loghead.
- Logext-guard
- (logext-guard size i) is a macro form of the guards for logext.
- Logbit-guard
- (logbit-guard pos i) is a macro form of the guards for logbit.
- Logapp-guard
- (logapp-guard size i j) is a macro form of the guards for logapp.
- Ashu-guard
- (ashu-guard size i cnt) is a macro form of the guards for ashu.
