Bitops is a library originally developed at Centaur Technology for reasoning about bit-vector arithmetic. It grew out of an extension to the venerable ACL2::ihs library, and is now fairly comprehensive.

Bitops is a bit-vector arithmetic library. It provides:

- Definitions for single-bit operations like b-and, b-ior, etc., and for extended bit-vector operations, like loghead, logapp, logrev, etc. These are largely inherited from ACL2::ihs.
- Support for reasoning about these new operations, and also about the bit-vector operations that are built into ACL2 like logand, ash, and logbitp.
- Efficient implementations of certain bit-vector operations like fast-logext,
merge operations, fast-logrev, etc., with lemmas or mbe to relate them to the logically nicer definitions. These definitions generally don't add any logical power, but are useful for developing more efficient executable models.

Bitops is **not** a standalone arithmetic library. It has almost no
support for non-integer arithmetic (rationals/complexes) and has few lemmas
about elementary operations like

Instead, you will usually include books from both Bitops **and** from
some other arithmetic library. Bitops is often used in concert with books from

Bitops definitions are typically compatible with ACL2::gl, a framework for bit-blasting ACL2 theorems. GL is mainly applicable to bounded problems, but is highly automatic. This nicely complements Bitops, which is a more traditional library of lemmas that can be applied to unbounded problems.

Bitops is not especially automatic. Merely loading it may allow you to
solve some bit-vector problems automatically. But if you want to use it
*well* and understand what to do when it doesn't solve your problems, you
should expect to invest some effort in learning the library.

One reason Bitops may be less automatic than other libraries is that we use it in proofs about microcode routines. These proofs often involve very large terms. This poses a challenge when writing arithmetic rules: to successfully manage proofs with large terms, case-splitting needs to be carefully controlled. To keep the library more controllable, some good rules are kept disabled by default. So, to get the most out of the library, you may need to explicitly enable these rules as appropriate.

Bitops is a somewhat large library that is compartmentalized into several books, many of which can be loaded independently.

To avoid getting locked into any particular arithmetic library, good practice is to always only locally include arithmetic books, including Bitops. When your own books only mention built-in functions like logand and ash, this is no problem. But you may often write theorems or functions that use new functions like loghead, logcdr, etc., and in this case you need to non-locally include the definitions of these functions.

Because of this, you will usually want to use something like this:

(include-book "ihs/basic-definitions" :dir :system) (local (include-book "centaur/bitops/ihsext-basics" :dir :system)) (local (include-book "centaur/bitops/signed-byte-p" :dir :system)) (local (include-book ... other bitops books ...))

Although there is a **against**
using it. Instead, it's generally best to load the individual bitops-books that address your particular needs.

- Bitops/merge
- Efficient operations for concatenating fixed-sized bit vectors.
- Bitops-compatibility
- Notes about using Bitops with other arithmetic libraries.
- Bitops-books
- Guide to the books in the Bitops library.
- Logbitp-reasoning
- A computed hint for proving bit-twiddling theorems by smartly sampling bits
- Bitops/signed-byte-p
- Lemmas about signed-byte-p and unsigned-byte-p that are often useful when optimizing definitions with ACL2::type-spec declarations.
- Fast-part-select
- Optimized function for selecting a bit range from a big integer.
- Bitops/integer-length
- Basic theorems about integer-length.
- Bitops/extra-defs
- Additional bitwise operations.
- Install-bit
`(install-bit n val x)`setsx[n] = val , wherex is an integer,n is a bit position, andval is a bit.- Trailing-0-count
- Optimized trailing 0 count for integers.
- Bitops/defaults
- (semi-deprecated) Basic theorems about the "default" behavior of bit-vector operations when their inputs are ill-formed (e.g., not integers, not naturals).
- Logbitp-mismatch
`(logbitp-mismatch a b)`finds the minimal bit-position for whicha andb differ, or returnsNIL if no such bit exists.- Trailing-1-count
- Optimized trailing 0 count for integers.
- Bitops/rotate
- Definitions of rotate-left and rotate-right operations, and lemmas for reasoning about them.
- Bitops/equal-by-logbitp
- Introduces
equal-by-logbitp , a strategy for proving thata = b by showing that their bits are equal, and computed hints that can automate the application of this strategy. - Bitops/ash-bounds
- A book with some basic bounding and monotonicity lemmas for ash and logtail.
- Bitops/fast-logrev
- Optimized definitions of logrev at particular sizes.
- Limited-shifts
- Functions for performing shifts that are artificially limited so as to make them more amenable to symbolic execution with AIGs.
- Bitops/part-select
- This book provides a readable nice macro for extracting a portion of an integer. You could use it to, e.g., extract bits 15-8 as a byte.
- Bitops/parity
- Parity (i.e., reduction xor) related functions.
- Bitops/saturate
- Definitions of signed and unsigned saturation operations.
- Bitops/part-install
- This book provides a way to set a portion of an integer to some value.
- Bitops/logbitp-bounds
- A book about logbitp and expt.
- Bitops/ihsext-basics
- A key book in the bitops library. This is intended to be a (still
lightweight) replacement for books such as
ihs/logops-lemmas.lisp . - Bitops/fast-rotate
- This book provides optimized rotate functions, which are proven equivalent to rotate-left and rotate-right via mbe.
- Bitops/fast-logext
- This book provides optimized sign-extension functions, which are proven equivalent to logext via mbe.
- Bitops/ihs-extensions
- Extension of bitops/ihsext-basics with additional lemmas.