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

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.

- 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-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-8-bits
- Concatenate 8 bits together to form an 8-bit natural.
- Merge-8-u64s
- Concatenate 8 64-bit numbers together to form an 512-bit result.
- Merge-8-u32s
- Concatenate 8 32-bit numbers together to form an 256-bit result.
- Merge-8-u2s
- Concatenate 8 2-bit numbers together to form an 16-bit result.
- Merge-8-u16s
- Concatenate 8 16-bit numbers together to form an 128-bit result.
- Merge-8-u4s
- Concatenate 8 nibbles together to form an 32-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-u2s
- Concatenate 4 2-bit numbers together to form an 8-bit result.
- Merge-4-u16s
- Concatenate 4 16-bit numbers together to form an 64-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-bits
- Concatenate 2 bits together to form an 2-bit natural.
- 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-u8s
- Concatenate 2 bytes together to form an 16-bit result.
- Merge-2-u64s
- Concatenate 2 64-bit numbers together to form an 128-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