|
|
|---|
|
|
|
|---|
The Integer Hardware Specification (IHS) library is a collection of arithmetic books, mainly geared toward bit-vector arithmetic.
This is a classic ACL2 arithmetic library wherein bit-vectors are represented as ordinary ACL2 integers, which has some nice efficiency properties.
Despite the underlying integer-based representation, the library allows you to easily treat integers akin to lsb-first lists of bits, with the functions logcar and logcdr acting as analogues for car and cdr.
To help you make use of this view, the library introduces alternate, list-style, recursive definitions for operations like logand. Once you understand how to induct in the right way to use these definitions, it becomes an extremely useful way to prove theorems about these bit functions.
The IHS library is found in: