		Search-engine friendly clone of the ACL2 documentation.

8bitbytes-hexchars-conversions

Ubyte8s=>hexchars

Convert a list of unsigned 8-bit bytes to a sequence of hexadecimal digit characters.

Signature
(ubyte8s=>hexchars bytes) → chars
Arguments: bytes — Guard (unsigned-byte-listp 8 bytes).
Returns: chars — Type (str::hex-digit-char-list*p chars).

Each input natural number is converted to two hexadecimal digits, with a leading 0 digit if needed. The hexadecimal digits above 9 are uppercase letters. The result is the concatenation of all these digits. The result has always an even length.

Definitions and Theorems

Function: ubyte8s=>hexchars-aux

(defun ubyte8s=>hexchars-aux (bytes rev-chars)
 (declare
      (xargs :guard (and (unsigned-byte-listp 8 bytes)
                         (str::hex-digit-char-list*p rev-chars))))
 (let ((__function__ 'ubyte8s=>hexchars-aux))
  (declare (ignorable __function__))
  (cond
   ((endp bytes) (rev rev-chars))
   (t
    (b* (((mv hi-char lo-char)
          (ubyte8=>hexchars (car bytes))))
      (ubyte8s=>hexchars-aux (cdr bytes)
                             (list* lo-char hi-char rev-chars)))))))

Function: ubyte8s=>hexchars

(defun ubyte8s=>hexchars (bytes)
 (declare (xargs :guard (unsigned-byte-listp 8 bytes)))
 (let ((__function__ 'ubyte8s=>hexchars))
   (declare (ignorable __function__))
   (mbe :logic (cond ((endp bytes) nil)
                     (t (b* (((mv hi-char lo-char)
                              (ubyte8=>hexchars (car bytes))))
                          (list* hi-char lo-char
                                 (ubyte8s=>hexchars (cdr bytes))))))
        :exec (ubyte8s=>hexchars-aux bytes nil))))

Theorem: hex-digit-char-list*p-of-ubyte8s=>hexchars

(defthm hex-digit-char-list*p-of-ubyte8s=>hexchars
  (b* ((chars (ubyte8s=>hexchars bytes)))
    (str::hex-digit-char-list*p chars))
  :rule-classes :rewrite)

Theorem: ubyte8s=>hexchars-of-unsigned-byte-list-fix

(defthm ubyte8s=>hexchars-of-unsigned-byte-list-fix
  (equal (ubyte8s=>hexchars (unsigned-byte-list-fix 8 bytes))
         (ubyte8s=>hexchars bytes)))

Theorem: evenp-of-len-of-ubyte8s=>hexchars

(defthm evenp-of-len-of-ubyte8s=>hexchars
  (evenp (len (ubyte8s=>hexchars bytes))))

Theorem: ubyte8s=>hexchars-of-append

(defthm ubyte8s=>hexchars-of-append
  (equal (ubyte8s=>hexchars (append bytes1 bytes2))
         (append (ubyte8s=>hexchars bytes1)
                 (ubyte8s=>hexchars bytes2))))

Subtopics

Ubyte8s<=>hexchars-inverses-theorems: ubyte8s=>hexchars and hexchars=>ubyte8s are mutual inverses.