ubyte8=>hexchars and hexchars=>ubyte8 are mutual inverses.
Theorem:
(defthm hexchars=>ubyte8-of-ubyte8=>hexchars (b* (((mv hi-char lo-char) (ubyte8=>hexchars byte))) (equal (hexchars=>ubyte8 hi-char lo-char) (unsigned-byte-fix 8 byte))))
Theorem:
(defthm ubyte8=>hexchars-of-hexchars=>ubyte8 (implies (and (str::hex-digit-char-p hi-char) (str::hex-digit-char-p lo-char)) (b* ((byte (hexchars=>ubyte8 hi-char lo-char))) (and (equal (mv-nth 0 (ubyte8=>hexchars byte)) (str::upcase-char hi-char)) (equal (mv-nth 1 (ubyte8=>hexchars byte)) (str::upcase-char lo-char))))))