# Fast-logrev-u8

Fast implementation of (logrev 8 x) for bytes.

- Signature
(fast-logrev-u8 x) → reverse-x

This function is based on the *Reverse the bits in a byte with 7
operations (no 64-bit)* algorithm, described on Sean Anderson's Bit
Twiddling Hacks page.

I use this non-64-bit version, even though it takes more operations than
some of the other algorithms, because it uses at most a 49-bit integer, which
is a fixnum on CCL and probably most other 64-bit Lisps. In contrast, the
64-bit algorithms (probably) would require bignums.

Anyway, it's at least a pretty good improvement over logrev.

(let ((byte #b101010)
(times 100000000))
;; 12.18 seconds
(time (loop for i fixnum from 1 to times do (logrev 8 byte)))
;; .32 seconds
(time (loop for i fixnum from 1 to times do (fast-logrev-u8 byte))))

### Definitions and Theorems

**Function: **fast-logrev-u8$inline

(defun acl2::fast-logrev-u8$inline (x)
(declare (type (unsigned-byte 8) x))
(let ((__function__ 'fast-logrev-u8))
(declare (ignorable __function__))
(mbe :logic (logrev 8 x)
:exec
(b* (((the (unsigned-byte 32) t1)
(logand (the (unsigned-byte 32)
(* (the (unsigned-byte 16) x)
(the (unsigned-byte 16) 2050)))
(the (unsigned-byte 32) 139536)))
((the (unsigned-byte 32) t2)
(logand (the (unsigned-byte 32)
(* (the (unsigned-byte 16) x)
(the (unsigned-byte 16) 32800)))
(the (unsigned-byte 32) 558144)))
((the (unsigned-byte 32) t3)
(logior (the (unsigned-byte 32) t1)
(the (unsigned-byte 32) t2)))
((the (unsigned-byte 49) t4)
(* (the (unsigned-byte 32) t3)
(the (unsigned-byte 17) 65793)))
((the (unsigned-byte 33) t5)
(ash t4 -16)))
(the (unsigned-byte 8)
(logand t5 255))))))