• 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
            • Merge-64-u8s
            • Merge-64-bits
            • Merge-32-u8s
            • Merge-32-u4s
            • Merge-32-u2s
            • Merge-32-u16s
            • Merge-32-bits
            • Merge-16-bits
            • Merge-16-u32s
            • Merge-16-u16s
            • Merge-16-u8s
            • Merge-16-u4s
            • Merge-16-u2s
            • Merge-8-bits
            • Merge-8-u2s
            • Merge-8-u64s
            • Merge-8-u4s
            • Merge-8-u32s
            • Merge-8-u16s
            • Merge-8-u8s
            • Merge-4-bits
            • Merge-4-u8s
            • Merge-4-u4s
            • Merge-4-u16s
            • Merge-4-u2s
            • Merge-4-u64s
            • Merge-4-u32s
            • Merge-4-u128s
            • Merge-2-u64s
            • Merge-2-u256s
            • Merge-2-u16s
            • Merge-2-u128s
            • Merge-2-bits
            • Merge-2-u8s
            • Merge-2-u4s
            • Merge-2-u32s
            • Merge-2-u2s
            • Merge-unsigneds
            • Merge-unsigneds-aux
            • Indexed-subst-templates
          • Bitops-compatibility
          • Bitops-books
          • Logbitp-reasoning
          • Bitops/signed-byte-p
          • Fast-part-select
          • 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

Bitops/merge

Efficient operations for concatenating fixed-sized bit vectors.

We now introduce many operations that concatenate together bit vectors of some fixed size to create a new, merged bit vector. For example, merge-4-u8s joins together four 8-bit vectors into a 32-bit result.

In general, the function logapp is a more flexible alternative to the operations below—it can be used to merge bit vectors of different sizes. However, since it can only merge two bit-vectors at a time, using logapp directly can become quite tedious when you have a lot of vectors to merge. For instance, these merging operations may be especially useful for describing SIMD style operations, byte swapping operations, and so forth.

Each of our merging operations is logically simple. However, we go to some lengths to make them execute more efficiently. This is accomplished by providing ample ACL2::type-spec declarations and arranging the order of operations to use fixnums for as long as possible. This provides significant speedups, for instance:

;; logic mode version: 11.112 seconds
;; exec mode version:   1.404 seconds
(let ((a7 1)
      (a6 2)
      (a5 3)
      (a4 4)
      (a3 5)
      (a2 6)
      (a1 7)
      (a0 8))
  (time (loop for i fixnum from 1 to 100000000 do
              (merge-8-u8s a7 a6 a5 a4 a3 a2 a1 a0))))

Note that when designing these functions, we typically assume that fixnums are large enough to hold 56-bit results. Our definitions should therefore perform well on 64-bit Lisps including at least CCL and SBCL.

We prove that each merge produces a result of the correct size (expressed as a theorem about unsigned-byte-p), and that it has a nat-equiv ACL2::congruence for each of its arguments.

Subtopics

Merge-64-u8s
Concatenate 64 bytes together to form an 512-bit result.
Merge-64-bits
Concatenate 64 bits together to form an 64-bit natural.
Merge-32-u8s
Concatenate 32 bytes together to form an 256-bit result.
Merge-32-u4s
Concatenate 32 nibbles together to form an 128-bit result.
Merge-32-u2s
Concatenate 32 2-bit numbers together to form an 64-bit result.
Merge-32-u16s
Concatenate 32 16-bit numbers together to form an 512-bit result.
Merge-32-bits
Concatenate 32 bits together to form an 32-bit natural.
Merge-16-bits
Concatenate 16 bits together to form an 16-bit natural.
Merge-16-u32s
Concatenate 16 32-bit numbers together to form an 512-bit result.
Merge-16-u16s
Concatenate 16 16-bit numbers together to form an 256-bit result.
Merge-16-u8s
Concatenate 16 bytes together to form an 128-bit result.
Merge-16-u4s
Concatenate 16 nibbles together to form an 64-bit result.
Merge-16-u2s
Concatenate 16 2-bit numbers together to form an 32-bit result.
Merge-8-bits
Concatenate 8 bits together to form an 8-bit natural.
Merge-8-u2s
Concatenate 8 2-bit numbers together to form an 16-bit result.
Merge-8-u64s
Concatenate 8 64-bit numbers together to form an 512-bit result.
Merge-8-u4s
Concatenate 8 nibbles together to form an 32-bit result.
Merge-8-u32s
Concatenate 8 32-bit numbers together to form an 256-bit result.
Merge-8-u16s
Concatenate 8 16-bit numbers together to form an 128-bit result.
Merge-8-u8s
Concatenate 8 bytes together to form an 64-bit result.
Merge-4-bits
Concatenate 4 bits together to form an 4-bit natural.
Merge-4-u8s
Concatenate 4 bytes together to form an 32-bit result.
Merge-4-u4s
Concatenate 4 nibbles together to form an 16-bit result.
Merge-4-u16s
Concatenate 4 16-bit numbers together to form an 64-bit result.
Merge-4-u2s
Concatenate 4 2-bit numbers together to form an 8-bit result.
Merge-4-u64s
Concatenate 4 64-bit numbers together to form an 256-bit result.
Merge-4-u32s
Concatenate 4 32-bit numbers together to form an 128-bit result.
Merge-4-u128s
Concatenate 4 128-bit numbers together to form an 512-bit result.
Merge-2-u64s
Concatenate 2 64-bit numbers together to form an 128-bit result.
Merge-2-u256s
Concatenate 2 256-bit numbers together to form an 512-bit result.
Merge-2-u16s
Concatenate 2 16-bit numbers together to form an 32-bit result.
Merge-2-u128s
Concatenate 2 128-bit numbers together to form an 256-bit result.
Merge-2-bits
Concatenate 2 bits together to form an 2-bit natural.
Merge-2-u8s
Concatenate 2 bytes together to form an 16-bit result.
Merge-2-u4s
Concatenate 2 nibbles together to form an 8-bit result.
Merge-2-u32s
Concatenate 2 32-bit numbers together to form an 64-bit result.
Merge-2-u2s
Concatenate 2 2-bit numbers together to form an 4-bit result.
Merge-unsigneds
Concatenate the given list of integers together at the given width, most-significant first, to form a single natural number.
Merge-unsigneds-aux
Indexed-subst-templates