		Search-engine friendly clone of the ACL2 documentation.

Bitops

Logbitp-reasoning

A computed hint for proving bit-twiddling theorems by smartly sampling bits

Logbitp-reasoning is a computed hint for proving theorems about bitvector operations. Example usage:

(defthm pass-context-of-ash
  (implies (equal (logand (ash mask (- (ifix n))) a1)
                  (logand (ash mask (- (ifix n))) a2))
           (equal (logand mask (ash a1 n))
                  (logand mask (ash a2 n))))
  :hints ((logbitp-reasoning)))

It works by:

Creating witnesses for inequality hyps/equality conclusions, replacing (not (equal a b)) with:

(implies (and (integerp x) (integerp y))
         (and (natp bit)
              (not (equal (logbitp bit x)
                          (logbitp bit y)))))

where bit is a fresh variable,

Instantiating equality hyps/inequality conclusions, replacing (equal a b) with (equal (logbitp bit a) (logbitp bit b)), for one or more several values of bit.

The main work done by this computed hint is to decide how to instantiate bit for each of the equality hyps/inequality conclusions. To do this we:

Keep track of a list of logbitp term "targets", which we think of as already appearing in our goal either due to witnessing or instantiation.
Try to instantiate equality hyps so as to create more occurrences of existing targets.

We take pass-context-of-ash above as an example.

First we find the literals of the clause that we'll create witnesses for -- in this case, the conclusion. We'll introduce some new variable wbit and our new conclusion will be (omitting some type info that isn't directly relevant)
```
(equal (logbitp wbit (logand mask (ash a1 n)))
       (logbitp wbit (logand mask (ash a2 n))))
```
Next we simplify this new conclusion and extract the logbitp terms that the simplified term contains:
```
(logbitp wbit mask)
(logbitp (+ (- (ifix n)) wbit) a1)
(logbitp (+ (- (ifix n)) wbit) a2)
```
These are now our target terms.
Next we look for instantiations of our hypothesis that, when simplified, will contain one or more of these target terms. To do this, we first instantiate it with a variable ibit, obtaining:
```
(equal (logbitp ibit (logand (ash mask (- (ifix n))) a1))
       (logbitp ibit (logand (ash mask (- (ifix n))) a1)))
```

Then we simplify the result and extract the resulting logbitp terms:

(logbitp ibit a1)
(logbitp ibit a2)
(logbitp (+ (ifix n) (nfix ibit)) mask)

Now we try to find values of ibit that will make one or more of these results match one or more of the target terms. We immediately find that by setting ibit to (+ (- (nfix n)) wbit) we create some matches. So we decide to instantiate the hyp using this term as our bit index.
All of the above was done just to compute a hint. The actual hint we provide is a call to witness-cp, a clause processor that supports this sort of witness creation and instantiation, with instructions to do the witnessing and instantiation steps that we've settled on. Once this clause processor runs, the resulting proof splits into 8 subgoals that are all quickly proved.

Logbitp-reasoning is a macro that can take a few optional arguments, but reasonable defaults (in the invocation below) are provided:

:hints ((logbitp-reasoning
         :restrict t
         :passes 1
         :verbosep nil
         :simp-hint (:in-theory
                      (enable* logbitp-case-splits
                               logbitp-when-bit
                               logbitp-of-const-split))
         :add-hints (:in-theory
                     (enable* logbitp-case-splits
                              logbitp-when-bit
                              logbitp-of-const-split))))

The meanings of these:

:restrict is a term in the variables x and y that restricts the equality literals to which we will apply witnessing/instantiation. For example,
```
:restrict (or (and (consp x) (eq (car x) 'binary-logand))
              (and (consp y) (eq (car y) 'binary-logand)))
```
will cause the hint to ignore any equality literals that don't have an argument that is a call of logand.
:passes determines the number of passes through the clause we use to collect instantiations and target terms. Instantiations can add new targets, and the more targets there are, the more instantiations may be found.
:simp-hint is the hint given to the simplifier while deciding on the instantiations.
:add-hints are hints given at the same time as the clause processor hint.