		Search-engine friendly clone of the ACL2 documentation.

8bitbytes-hexstrings-conversions

Ubyte8s=>hexstring

Convert a list of natural numbers below 256 to a string of hexadecimal digits.

Signature
(ubyte8s=>hexstring bytes) → string
Arguments: bytes — Guard (unsigned-byte-listp 8 bytes).
Returns: string — Type (str::hex-digit-string-p string).

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

Definitions and Theorems

Function: ubyte8s=>hexstring

(defun ubyte8s=>hexstring (bytes)
  (declare (xargs :guard (unsigned-byte-listp 8 bytes)))
  (let ((__function__ 'ubyte8s=>hexstring))
    (declare (ignorable __function__))
    (implode (ubyte8s=>hexchars bytes))))

Theorem: hex-digit-string-p-of-ubyte8s=>hexstring

(defthm hex-digit-string-p-of-ubyte8s=>hexstring
  (b* ((string (ubyte8s=>hexstring bytes)))
    (str::hex-digit-string-p string))
  :rule-classes :rewrite)

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

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

Theorem: evenp-of-length-of-ubyte8s=>hexstring

(defthm evenp-of-length-of-ubyte8s=>hexstring
  (evenp (length (ubyte8s=>hexstring bytes))))

Theorem: ubyte8s=>hexstring-of-append

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

Subtopics

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