Bitops
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.
Introduction
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.
Compatibility
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 + and * beyond how they relate to
the bit-vector operations.
Instead, you will usually include books from both Bitops and from
some other arithmetic library. Bitops is often used in concert with books from
arithmetic, arithmetic-3, and arithmetic-5. See bitops-compatibility for notes about using these libraries with Bitops.
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.
Philosophy and Expectations
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.
Loading the Library
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 top book, we generally recommend against
using it. Instead, it's generally best to load the individual bitops-books that address your particular needs.
Subtopics
- 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) sets x[n] = val, where x is an integer,
n is a bit position, and val 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 which
a and b differ, or returns NIL 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 that a =
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.
