• 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
        • 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
          • Bits-between
          • Bits-0-31
          • 60bits-0-59
          • Add-to-each
          • Bits-0-7
          • 60bits-0-7
          • 60bits-0-3
      • Sbitsets
      • Reasoning
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Utilities

60bits-0-59

Partially unrolled version of bits-between that collects the bits from a 60-bit unsigned x and adds offset to each.

Signature

(60bits-0-59 offset x acc) → *

In CCL, 60-bit unsigned numbers are fixnums and, according to the following loops, this is about 3.6x faster than bits-between.

(progn
 (gc$)
 ;; 21.540 seconds
 (time (loop for x fixnum from 1 to 30000000 do
             (bits-between 0 60 x)))
 ;; 6.013 seconds
 (gc$)
 (time (loop for x fixnum from 1 to 30000000 do
             (60bits-0-59 0 x nil))))

Definitions and Theorems

Function: 60bits-0-59

(defun 60bits-0-59 (offset x acc)
  (declare (type unsigned-byte offset)
           (type (unsigned-byte 60) x))
  (let ((__function__ '60bits-0-59))
    (declare (ignorable __function__))
    (b* ((acc (60bits-0-3 (+ offset 56)
                          (the (unsigned-byte 60) (ash x -56))
                          acc))
         (acc (60bits-0-7 (+ offset 48)
                          (the (unsigned-byte 60) (ash x -48))
                          acc))
         (acc (60bits-0-7 (+ offset 40)
                          (the (unsigned-byte 60) (ash x -40))
                          acc))
         (acc (60bits-0-7 (+ offset 32)
                          (the (unsigned-byte 60) (ash x -32))
                          acc))
         (acc (60bits-0-7 (+ offset 24)
                          (the (unsigned-byte 60) (ash x -24))
                          acc))
         (acc (60bits-0-7 (+ offset 16)
                          (the (unsigned-byte 60) (ash x -16))
                          acc))
         (acc (60bits-0-7 (+ offset 8)
                          (the (unsigned-byte 60) (ash x -8))
                          acc)))
      (60bits-0-7 offset x acc))))

Theorem: 60bits-0-59-redef

(defthm 60bits-0-59-redef
  (implies (natp offset)
           (equal (60bits-0-59 offset x acc)
                  (append (add-to-each offset (bits-between 0 60 x))
                          acc))))