ubyte8s=>hexchars and hexchars=>ubyte8s are mutual inverses.
Theorem:
(defthm hexchars=>ubyte8s-of-ubyte8s=>hexchars (equal (hexchars=>ubyte8s (ubyte8s=>hexchars bytes)) (unsigned-byte-list-fix 8 bytes)))
Theorem:
(defthm ubyte8s=>hexchars-of-hexchars=>ubyte8s (implies (and (str::hex-digit-char-list*p chars) (true-listp chars) (evenp (len chars))) (equal (ubyte8s=>hexchars (hexchars=>ubyte8s chars)) (str::upcase-charlist chars))))