Extract a particular 32-bit slice of an integer.
Logically, (bignum-extract x slice) is essentially:
What does this do? Imagine partitioning the integer
You may optionally, with a trust tag load an raw Lisp replacement which, on 64-bit CCL that takes advantage of the underlying representation of bignums, and on other Lisps implements this function using ldb, which may have or may not be more optimal.
(defun bignum-extract (x slice) (declare (xargs :guard (and (integerp x) (natp slice)))) (let ((__function__ 'bignum-extract)) (declare (ignorable __function__)) (mbe :logic (let ((x (ifix x)) (slice (nfix slice))) (logand (1- (expt 2 32)) (ash x (* -32 slice)))) :exec (the (unsigned-byte 32) (logand (the (unsigned-byte 32) (1- (expt 2 32))) (ash x (* -32 slice)))))))
(defthm natp-of-bignum-extract (b* ((extracted (bignum-extract x slice))) (natp extracted)) :rule-classes :type-prescription)
(defthm unsigned-byte-p-of-bignum-extract (unsigned-byte-p 32 (bignum-extract x slice)))
(defthm upper-bound-of-bignum-extract (< (bignum-extract x slice) 4294967296) :rule-classes :linear)