ubyte8s=>hexstring and hexstring=>ubyte8s are mutual inverses.
Theorem:
(defthm hexstring=>ubyte8s-of-ubyte8s=>hexstring (equal (hexstring=>ubyte8s (ubyte8s=>hexstring bytes)) (unsigned-byte-list-fix 8 bytes)))
Theorem:
(defthm ubyte8s=>hexstring-of-hexstring=>ubyte8s (implies (and (stringp string) (str::hex-digit-char-list*p (explode string)) (evenp (length string))) (equal (ubyte8s=>hexstring (hexstring=>ubyte8s string)) (str::upcase-string string))))