Byte-to-bits
Convert a byte to a list of bits (big-endian).
;; Convert a byte into a list of 8 bits. The most significant bit comes first,
;; so this is "big endian." We could define this as (unpackbv 8 1 byte), but
;; that seems too complicated.
(defund byte-to-bits (byte)
(declare (xargs :guard (integerp byte)
;;(unsigned-byte-p 8 byte) ;todo: strengthen guard to this
))
(list (getbit 7 byte)
(getbit 6 byte)
(getbit 5 byte)
(getbit 4 byte)
(getbit 3 byte)
(getbit 2 byte)
(getbit 1 byte)
(getbit 0 byte)))
