• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
      • 100-theorems
      • Arithmetic
      • Bit-vectors
        • Sparseint
        • Bitops
          • Bitops/merge
          • Bitops-compatibility
          • Bitops-books
          • Logbitp-reasoning
          • Bitops/signed-byte-p
          • Fast-part-select
            • Fast-part-extend
          • Bitops/integer-length
          • Bitops/extra-defs
          • Install-bit
          • Trailing-0-count
          • Bitops/defaults
          • Logbitp-mismatch
          • Trailing-1-count
          • Bitops/rotate
          • Bitops/equal-by-logbitp
          • Bitops/ash-bounds
          • Bitops/fast-logrev
          • Limited-shifts
          • Bitops/part-select
          • Bitops/parity
          • Bitops/saturate
          • Bitops/part-install
          • Bitops/logbitp-bounds
          • Bitops/ihsext-basics
          • Bitops/fast-rotate
          • Bitops/fast-logext
          • Bitops/ihs-extensions
        • Bv
        • Ihs
        • Rtl
      • Algebra
    • Testing-utilities
  • Bitops

Fast-part-select

Optimized function for selecting a bit range from a big integer.

Signature
(fast-part-select x width low) → *
Arguments
x — Guard (integerp x).
width — Guard (natp width).
low — Guard (natp low).

Suppose you have a large (perhaps millions of bits) bignum, and you want to extract a small range (maybe only a few thousand bits) from somewhere in the middle. Using regular ACL2 primitives like logand and ash, you don't have any good options that don't require copying a much larger portion of the number. You either have to truncate the big number to the end of the range you want (which may yield a large bignum) and then shift it into place, or else shift the lowest bit into place (which may yield a large bignum) and then truncate it to the width you want. One option requires making a new bignum that is lsb + width - 1 bits, the other requires making a new bignum that is origwidth - lsb bits. Depending on what range you want to extract, sometimes one or the other of these options is small enough, but in some cases neither is palatable.

Fast-part-select is based on bitsets::bignum-extract, which extracts a 32-bit slice from a bignum. It has an optimized implementation on CCL that simply grabs the appropriate array element from within the bignum representation. Fast-part-select stitches together the required range from these 32-bit slices. It isn't particularly efficient if the width of the selection is large, but it is independent of the width of the input integer from which we're selecting and the bit offset at which we're selecting.

It's kind of a pity to have to use this; it would be nice if Lisps had efficient implementations of the Common Lisp ldb operator and we could just use that instead.

Note: For good performance, it is important to use the raw Lisp definition of bignum-extract, loaded by including the book "std/bitsets/bignum-extract-opt".

See also fast-part-extend, which performs the same operation but returns the range sign-extended instead of zero-extended.

Definitions and Theorems

Function: fast-part-select$inline

(defun fast-part-select$inline (x width low)
  (declare (type integer x)
           (type (integer 0 *) width)
           (type (integer 0 *) low))
  (declare (xargs :guard (and (integerp x)
                              (natp width)
                              (natp low))))
  (declare (xargs :split-types t))
  (let ((__function__ 'fast-part-select))
    (declare (ignorable __function__))
    (mbe :logic
         (part-select-width-low x width low)
         :exec
         (b* ((width (lnfix width))
              (low (lnfix low))
              ((when (eql width 0)) 0)
              (low-slice (ash low -5))
              (low-omit (logand 31 low))
              (high (+ -1 low width))
              (high-slice (ash high -5))
              (high-omit (- 31 (logand 31 high)))
              (slices (+ 1 (- high-slice low-slice))))
           (fast-psel x
                      low-slice slices low-omit high-omit)))))

Subtopics

Fast-part-extend
Optimized function for selecting a signed bit range from a big integer.