3.1  Binary Operations

The binary functions logand, logior, and logxor are ACL2 primitives. The “definitions” presented below are actually formalized as theorems derived from ACL2 axioms.

Definition 3.1.1   (logand-def) For all and ,

The definition is extended recursively to arguments for arbitrary :

It is not obvious that Definition 3.1.1 is an admissible recursive definition. In order to establish that it is satisfied by a unique function, it will suffice to demonstrate the existence of a measure function that strictly decreases on each recursive call. Thus, we define

We must show that satisfies the following two inequalities, corresponding to the two recusive calls of logand, under the restrictions , , and :

(1) .

(2) .

Since the restrictions imply that at least one of and is neither 0 nor -1, (1) follows from Lemma 1.1.6. To establish (2), note that either , , or . In any case,

Precisely the same argument applies to the following two definitions.

Definition 3.1.2   (logior-def) For all and ,

The definition is extended recursively to arguments for arbitrary :

Definition 3.1.3   (logxor-def) For all and ,

The definition is extended recursively to arguments for arbitrary :

Notation: We adopt the following standard notation:

;

;

.

PROOF: We may assume that , , and . Thus,

and by induction,

(logand-bvecp) If is an -bit vector, where , and , then is an -bit vectors.

PROOF: By Lemma 3.1.1,

(logior-bvecp, logxor-bvecp) If and and -bit vectors, where , then so are and .

PROOF: The same argument applies to both operations. The claim is trivial if , , , or . In all other cases, and are -bit vectors and by induction, so is, for example, . Thus,

(logand-mod,logior-mod,logxor-mod) For all , , and ,

 (a) (b) (c)

PROOF: We present the proof for (a); (b) and (c) are similar.

We may assume that , , , and . By Definition 3.1.1 and Lemma 1.2.18,

By Lemma 1.2.22, induction, Lemma 2.2.4, and Lemma 2.2.17, the first addend my be written as

and by Lemmas 2.3.2 and 2.3.16, the second addend is

Thus, by Definition 3.1.1 and Lemmas 3.1.2 and 2.2.4,

(fl-logand,fl-logior,fl-logxor) For all , , and ,

 (a) ; (b) ; (c) .

PROOF: We present the proof for (a); (b) and (c) are similar.

We may assume that , , , and . By Lemma 1.1.5, induction, and Definition 3.1.1,

(logand-cat,logior-cat,logxor-cat)
For all , , , , , and ,

(a) ----
= ----

(b) ----
= ----

(c) ----
= ----

PROOF: We present the proof for (a); (b) and (c) are similar.

Let ----. By Lemmas 3.1.4 and 2.4.13,

 ------ --

By Lemma 3.1.5,

----

where, by Definition 2.4.1 and the properties of the floor,
 -- -- -- -

Thus,

--

Finally, by Definitions 1.2.1 and 2.4.1,
 ---- ----

(logand-shift,logior-shift,logxor-shift) For all , , and ,

 (a) ; (b) ; (c) .

PROOF: We present the proof for (a); (b) and (c) are similar.

We may assume that , , , and . By induction and Definition 3.1.1,

(logand-expt,logior-expt,logxor-expt) For all , , and ,

 (a) ; (b) ; (c) .

PROOF:

(a) The claim is trivial if , , or ; otherwise, by Definition 3.1.1, induction, and Lemma 1.1.5,

(b) Similarly,

where, by Lemmas 2.2.4 and 2.2.16,

(c) is similar to (b).

(logior-expt-cor) Let and let be an -bit vector, where . Then

PROOF: By Lemmas 3.1.8 and 1.2.6 and Definition 3.1.2,

PROOF: By Definition 2.0.1 and Lemmas 3.1.4, 3.1.6, and 2.3.17,

By Lemma 3.1.5,

The lemma follows from Definition 1.2.1

The logical “and” operator may be used to extract a bit slice:

PROOF: The proof is by induction on . If , then and

If and , then by induction and Lemmas 2.2.16 and 2.3.17,

In the remaining case, and

PROOF: By Lemma 3.1.11,

All three binary logical operators commute with the bit slice operator:

(bits-logand,bits-logior,bits-logxor) For all , , , and ,
 (a) ; (b) ; (c) .

PROOF: We present the proof for (a); (b) and (c) are similar.

We may assume that , , , and . By Definition 2.0.1 and Lemmas 3.1.4 and 3.1.5,

Corollary 3.1.14   (bitn-logand,bitn-logior,bitn-logxor) For all , , and ,
 (a) ; (b) ; (c) .

Notation: If and are expressions of sizes and , respectively, then we define the size of each of the expressions , , and to be . As a consequence of Lemma 3.1.2, it remains true that if is any expression of size , then the value of is a bit vector of width .

Thus, for example, by Lemma 3.1.13,

David Russinoff 2017-08-01