		Search-engine friendly clone of the ACL2 documentation.

Signed-byte-fix

Fixing function for signed-byte-p.

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

Since the set denoted by signed-byte-p is empty for some values of bits (namely, when bits is not a positive integer), this fixing function cannot always return a value satisfying the predicate. Even though signed-byte-p does not fix its bits to posp, this fixing function does, i.e. it treats bits as a positive integer. Thus, the set denoted by signed-byte-p is never empty. If x is not in the range of signed-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 signed-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: signed-byte-fix

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

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

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

Theorem: signed-byte-fix-when-signed-byte-p

(defthm signed-byte-fix-when-signed-byte-p
  (implies (signed-byte-p (pos-fix bits) x)
           (equal (signed-byte-fix bits x) x)))

Theorem: signed-byte-fix-of-pos-fix-bits

(defthm signed-byte-fix-of-pos-fix-bits
  (equal (signed-byte-fix (pos-fix bits) x)
         (signed-byte-fix bits x)))

Theorem: signed-byte-fix-of-pos-fix-bits-normalize-const

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

Subtopics

Signed-byte-list-fix: Fixing function for signed-byte-listp.