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
