		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Loghead

(loghead size i) returns the size low-order bits of i.

Signature
(loghead size i) → nat
Arguments: size — Guard (and (integerp size) (<= 0 size)).; i — Guard (integerp i).
Returns: nat — Type (natp nat).

In languages like C, this might be written as i & ((1 << size) - 1).

By convention we define (loghead 0 i) as 0. This definition is a bit arbitrary but generally leads to nice lemmas.

Definitions and Theorems

Function: loghead$inline

(defun loghead$inline (size i)
 (declare (type unsigned-byte size))
 (declare (xargs :guard (and (and (integerp size) (<= 0 size))
                             (integerp i))))
 (declare (xargs :split-types t))
 (let ((__function__ 'loghead))
  (declare (ignorable __function__))
  (mbe :logic (imod i (expt2 size))
       :exec
       (the unsigned-byte
            (logand i
                    (the unsigned-byte
                         (1- (the unsigned-byte (ash 1 size)))))))))

Theorem: loghead-type

(defthm loghead-type
  (b* ((nat (loghead$inline size i)))
    (natp nat))
  :rule-classes :type-prescription)

Subtopics

Ihs/loghead-lemmas: Lemmas about loghead from the logops-lemmas book.
Loghead*: Recursive definition of loghead.
Loghead-basics