• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
      • Bitsets
        • Bitset-members
          • Ttag-bitset-members
            • Bignum-extract
        • Bitset-insert
        • Bitset-delete
        • Bitset-intersectp
        • Bitset-intersect
        • Bitset-difference
        • Bitset-subsetp
        • Bitset-union
        • Bitset-memberp
        • Bitset-singleton
        • Bitset-list
        • Bitset-cardinality
        • Bitset-list*
        • Utilities
      • Sbitsets
      • Reasoning
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Community
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Ttag-bitset-members

Bignum-extract

Extract a particular 32-bit slice of an integer.

Signature

(bignum-extract x slice) → extracted

Arguments

x — Integer to extract from.
    Guard (integerp x).

slice — Which 32 bit slice to extract.
    Guard (natp slice).

Returns

extracted — Type (natp extracted).

Logically, (bignum-extract x slice) is essentially:

(logand (ash x (* -32 slice)) (1- (expt 2 32)))

What does this do? Imagine partitioning the integer x into a list of 32-bit slices. Say that the least-significant 32 bits are the 0th slice, and so on. The bignum-extract function is just extracting the sliceth slice of x.

The logical definition of bignum-extract is not very efficient; when x is a bignum, the (ash x (* -32 slice)) term will generally require us to create a new bignum.

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.

Definitions and Theorems

Function: bignum-extract

(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)))))))

Theorem: natp-of-bignum-extract

(defthm natp-of-bignum-extract
  (b* ((extracted (bignum-extract x slice)))
    (natp extracted))
  :rule-classes :type-prescription)

Theorem: unsigned-byte-p-of-bignum-extract

(defthm unsigned-byte-p-of-bignum-extract
  (unsigned-byte-p 32 (bignum-extract x slice)))

Theorem: upper-bound-of-bignum-extract

(defthm upper-bound-of-bignum-extract
  (< (bignum-extract x slice) 4294967296)
  :rule-classes :linear)