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

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.

- 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-extendsi to asize -bit signed integer.- Logrev
- Logical reverse.
(logrev size i) bit-reverses thesize low-order bits ofi , discarding the high-order bits. - Loghead
(loghead size i) returns thesize low-order bits ofi .- Logops-bit-functions
- Versions of the standard logical operations that operate on single bits.
- Logtail
(logtail pos i) returns the high-order part ofi , starting at bit positionpos .- 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) coercesi to asize -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 ofi at bit-positionpos 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 tofinal-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 thesize low-order bits ofj with thesize low-order bits ofi . - Ashu
- Arithmetic shift, unsigned version.
- Logmaskp
(logmaskp i) recognizes positive bit-masks, i.e., numbers of the form2^n - 1 .- Lognotu
- Logical negation, unsigned version.
(lognotu size i) is an unsigned logicalnot . It just truncates(lognot i) tosize 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 form2^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 than1 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 justb . - 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.