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

(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)))))

wherebit 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 ofbit .

The main work done by this computed hint is to decide how to instantiate

- 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

- 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 settingibit 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.

: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 variablesx andy 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.