		Search-engine friendly clone of the ACL2 documentation.

Unsigned-byte-fix

Fixing function for unsigned-byte-p.

Signature
(unsigned-byte-fix bits x) → fixed-x
Arguments: bits — Guard (natp bits).; x — Guard (unsigned-byte-p bits x).
Returns: fixed-x — Type (unsigned-byte-p bits fixed-x), given (natp bits).

Since the set denoted by unsigned-byte-p is empty for some values of bits (namely, when bits is not a natural number), this fixing function cannot always return a value satisfying the predicate. Even though unsigned-byte-p does not fix its bits to natp, this fixing function does, i.e. it treats bits as a natural number. Thus, the set denoted by unsigned-byte-p is never empty. If x is not in the range of unsigned-byte-p, we return 0; another option is to return loghead (or its equivalent with built-in functions, to avoid a dependency on the IHS library).

Since unsigned-byte-p is enabled by default, this fixing function is also enabled by default. When these functions are enabled, they are meant as abbreviations, and theorems triggered by them may not fire during proofs.

Definitions and Theorems

Function: unsigned-byte-fix

(defun unsigned-byte-fix (bits x)
       (declare (xargs :guard (and (natp bits)
                                   (unsigned-byte-p bits x))))
       (let ((__function__ 'unsigned-byte-fix))
            (declare (ignorable __function__))
            (mbe :logic (b* ((bits (nfix bits)))
                            (if (unsigned-byte-p bits x) x 0))
                 :exec x)))

Theorem: return-type-of-unsigned-byte-fix

(defthm return-type-of-unsigned-byte-fix
        (implies (natp bits)
                 (b* ((fixed-x (unsigned-byte-fix bits x)))
                     (unsigned-byte-p bits fixed-x)))
        :rule-classes :rewrite)

Theorem: unsigned-byte-fix-when-unsigned-byte-p

(defthm unsigned-byte-fix-when-unsigned-byte-p
        (implies (unsigned-byte-p (nfix bits) x)
                 (equal (unsigned-byte-fix bits x) x)))

Theorem: unsigned-byte-fix-of-nfix-bits

(defthm unsigned-byte-fix-of-nfix-bits
        (equal (unsigned-byte-fix (nfix bits) x)
               (unsigned-byte-fix bits x)))

Theorem: unsigned-byte-fix-of-nfix-bits-normalize-const

(defthm unsigned-byte-fix-of-nfix-bits-normalize-const
        (implies (syntaxp (and (quotep bits)
                               (not (natp (cadr bits)))))
                 (equal (unsigned-byte-fix bits x)
                        (unsigned-byte-fix (nfix bits) x))))

Subtopics

Unsigned-byte-list-fix: Fixing function for unsigned-byte-listp.