		Search-engine friendly clone of the ACL2 documentation.

Std/bitsets

Reasoning

How to reason about bitsets.

Note: for now this discussion is only about plain bitsets. In the future, we intend this discussion to apply equally well to sbitsets.

A general goal of the bitsets library is to let you take advantage of efficient operations like logand and logior without having to do any arithmetic reasoning. Instead, ideally, you should be able to carry out all of your reasoning on the level of sets.

Basic Approach

To achieve this, we try to cast everything in terms of bitset-members. If you want to reason about some bitset-producing function foo, then you should typically try to write your theorems about:

(bitset-members (foo ...))

instead of directly proving something about:

(foo ...)

For example, to reason about bitset-union we prove:

Theorem: bitset-members-of-bitset-union

(defthm bitset-members-of-bitset-union
  (equal (bitset-members (bitset-union x y))
         (union (bitset-members x)
                (bitset-members y))))

In most cases, this theorem is sufficient for reasoning about the behavior of bitset-union.

Equivalence Proofs

The bitset-members approach is good most of the time, but in some cases you may wish to show that two bitset-producing functions literally create the same bitset. That is, instead of showing:

(bitset-members (foo ...)) = (bitset-members (bar ...))

it is perhaps better to prove:

(foo ...) = (bar ...)

It should be automatic to prove this stronger form (after first proving the weaker form) by using the theorem:

Theorem: equal-bitsets-by-membership

(defthm equal-bitsets-by-membership
  (implies (and (natp x) (natp y))
           (equal (equal x y)
                  (equal (bitset-members x)
                         (bitset-members y)))))