		Search-engine friendly clone of the ACL2 documentation.

Signed-saturate

Signed-saturate-fn

Logical definition of signed-saturate, and also its executable implementation in the general case.

Signature
(signed-saturate-fn n x) → saturated
Arguments: n — Guard (posp n).; x — Guard (integerp x).
Returns: saturated — Type (natp saturated).

Definitions and Theorems

Function: signed-saturate-fn

(defun signed-saturate-fn (n x)
  (declare (xargs :guard (and (posp n) (integerp x))))
  (let ((__function__ 'signed-saturate-fn))
    (declare (ignorable __function__))
    (b* ((n (lnfix n))
         (x (lifix x))
         ((when (mbe :logic (zp n) :exec nil)) 0)
         (2^{n-1} (ash 1 (1- n)))
         (max (+ -1 2^{n-1}))
         ((when (>= x max)) max)
         (min (- 2^{n-1}))
         ((when (<= x min)) 2^{n-1})
         (mask (+ -1 (ash 1 n))))
      (logand mask x))))

Theorem: natp-of-signed-saturate-fn

(defthm acl2::natp-of-signed-saturate-fn
  (b* ((saturated (signed-saturate-fn n x)))
    (natp saturated))
  :rule-classes :type-prescription)

Theorem: unsigned-byte-p-of-signed-saturate-fn

(defthm unsigned-byte-p-of-signed-saturate-fn
  (implies (natp n)
           (unsigned-byte-p n (signed-saturate-fn n x))))

Theorem: nat-equiv-implies-equal-signed-saturate-fn-1

(defthm nat-equiv-implies-equal-signed-saturate-fn-1
  (implies (nat-equiv n n-equiv)
           (equal (signed-saturate-fn n x)
                  (signed-saturate-fn n-equiv x)))
  :rule-classes (:congruence))

Theorem: int-equiv-implies-equal-signed-saturate-fn-2

(defthm int-equiv-implies-equal-signed-saturate-fn-2
  (implies (int-equiv x x-equiv)
           (equal (signed-saturate-fn n x)
                  (signed-saturate-fn n x-equiv)))
  :rule-classes (:congruence))