|
|
|---|
|
|
|
|---|
Guide to the books in the Bitops library.
Here is a summary of some of the books in the library.
This is a key book in the library and is generally a good starting point.
It is intended to be a (still lightweight) replacement for books such as
For instance, it has rules such as
A lot of the rules in
This book is sort of a continuation of
This is included in
This is a nice, light-weight book that adds a number of "obvious" lemmas
about
These rules can be very helpful when you are trying to write optimized
functions using Common Lisp ACL2::type-specs and need to satisfy the
guard obligations that come from terms such as
You can use this book independently of the rest of the library. It
currently has some support for reasoning about +, -, *, lognot, ash, logcdr,
loghead, and logtail, and will likely be extended as we find it lacking. You
may often wish to at least also load
This is a very cool book that allows you to carry out pick-a-point proofs:
to show that integers
This is an advanced book that implements an n-ary like mechanism for
rewriting terms in an
This book adds some basic bounding and monotonicity lemmas for ash and logtail.
This book adds some basic lemmas about logbitp and expt.
This book just has basic theorems about the "default" behavior of bit-vector operations when their inputs are ill-formed (e.g., not integers, not naturals). You probably shouldn't load it; most of this should be subsumed by more recent congruence reasoning for nat-equiv and int-equiv.
This book is a random assortment of functions for slicing integers, manipulating individual bits, and bit scanning. It will likely be split up and organized into separate books in the future.
This book provides several optimized functions for merging together, e.g., four bytes into a 32-bit value, or four 16-bit unsigned values into a 64-bit result, etc.
This book provides optimized implementations of logrev at various
widths; these definitions are logically just the ordinary, nice, logical
definition of
This book provides a simple recursive definition of a parity (i.e., reduction xor) function, and also a faster version for execution.
This book provides a readable nice macro for extracting a portion of an integer, e.g., bits 15-8.
This book provides a function and a macro to set a portion of an
integer to some value. It also includes some theorems about the
interaction of
This book defines rotate-left and rotate-right operations. It
provides lemmas explaining how logbitp interacts with these operations,
and it makes use of the
This book defines fast-rotate operations that are proved equivalent to rotate-left and rotate-right.
This book defines some optimized signed and unsigned saturation functions.
This book provides an optimized sign-extension functions, and proves them equivalent to logext. These optimizations don't impact reasoning because we carry them out with mbe.