# Ihs

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: books/ihs/*.lisp.

### Subtopics

- Logops-definitions
- A book a definitions of logical operations on numbers.
- Math-lemmas
- A book of theories about +, -, *, /, and EXPT, built on the
arithmetic package of Matt Kaufmann.
- Ihs-theories
- Subtheories of the ACL2 initialization theory.
- Ihs-init
- The root of the IHS (Integer Hardware Specification) library hierarchy.
- Logops
- Definitions and lemmas about logical operations on integers.