Turn a sequence of bytes into a sequence of nibbles.
(bytelist-to-nibblelist-keys-aux bytes) → nibbles
This corresponds to [YP:(191)], but here the conversion is expressed via recursion instead of indexing.
Function:
(defun bytelist-to-nibblelist-keys-aux (bytes) (declare (xargs :guard (byte-listp bytes))) (b* (((when (endp bytes)) nil) (byte (byte-fix (car bytes))) (nibble-hi (floor byte 16)) (nibble-lo (mod byte 16)) (nibbles (bytelist-to-nibblelist-keys-aux (cdr bytes)))) (list* nibble-hi nibble-lo nibbles)))
Theorem:
(defthm nibble-listp-of-bytelist-to-nibblelist-keys-aux (b* ((nibbles (bytelist-to-nibblelist-keys-aux bytes))) (nibble-listp nibbles)) :rule-classes :rewrite)
Theorem:
(defthm bytelist-to-nibblelist-keys-aux-of-byte-list-fix-bytes (equal (bytelist-to-nibblelist-keys-aux (byte-list-fix bytes)) (bytelist-to-nibblelist-keys-aux bytes)))
Theorem:
(defthm bytelist-to-nibblelist-keys-aux-byte-list-equiv-congruence-on-bytes (implies (byte-list-equiv bytes bytes-equiv) (equal (bytelist-to-nibblelist-keys-aux bytes) (bytelist-to-nibblelist-keys-aux bytes-equiv))) :rule-classes :congruence)