Logical definition of unsigned-saturate, and also its executable implementation in the general case.
Function:
(defun unsigned-saturate-fn (n x) (declare (xargs :guard (and (posp n) (integerp x)))) (let ((__function__ 'unsigned-saturate-fn)) (declare (ignorable __function__)) (b* ((n (lnfix n)) (x (lifix x)) (|2^N| (ash 1 n)) (max (+ -1 |2^N|)) ((when (>= x max)) max) ((when (<= x 0)) 0)) x)))
Theorem:
(defthm acl2::natp-of-unsigned-saturate-fn (b* ((saturated (unsigned-saturate-fn n x))) (natp saturated)) :rule-classes :type-prescription)
Theorem:
(defthm unsigned-byte-p-of-unsigned-saturate-fn (implies (natp n) (unsigned-byte-p n (unsigned-saturate-fn n x))))
Theorem:
(defthm nat-equiv-implies-equal-unsigned-saturate-fn-1 (implies (nat-equiv n n-equiv) (equal (unsigned-saturate-fn n x) (unsigned-saturate-fn n-equiv x))) :rule-classes (:congruence))
Theorem:
(defthm int-equiv-implies-equal-unsigned-saturate-fn-2 (implies (int-equiv x x-equiv) (equal (unsigned-saturate-fn n x) (unsigned-saturate-fn n x-equiv))) :rule-classes (:congruence))