		Search-engine friendly clone of the ACL2 documentation.

8bitbytes-hexchars-conversions

Ubyte8=>hexchars

Convert an unsigned 8-bit byte to two hexadecimal digit characters.

Signature
(ubyte8=>hexchars byte) → (mv hi-char lo-char)
Arguments: byte — Guard (unsigned-byte-p 8 byte).
Returns: hi-char — Type (str::hex-digit-char-p hi-char).; lo-char — Type (str::hex-digit-char-p lo-char).

The most significant digit comes first, followed by the least significant one. If the byte is below 16, the first digit is zero. The hexadecimal digits above 9 are uppercase letters.

Definitions and Theorems

Function: ubyte8=>hexchars

(defun ubyte8=>hexchars (byte)
  (declare (xargs :guard (unsigned-byte-p 8 byte)))
  (let ((__function__ 'ubyte8=>hexchars))
    (declare (ignorable __function__))
    (b* ((byte (mbe :logic (unsigned-byte-fix 8 byte)
                    :exec byte)))
      (mv (str::hex-digit-to-char (floor byte 16))
          (str::hex-digit-to-char (mod byte 16))))))

Theorem: hex-digit-char-p-of-ubyte8=>hexchars.hi-char

(defthm hex-digit-char-p-of-ubyte8=>hexchars.hi-char
  (b* (((mv ?hi-char ?lo-char)
        (ubyte8=>hexchars byte)))
    (str::hex-digit-char-p hi-char))
  :rule-classes :rewrite)

Theorem: hex-digit-char-p-of-ubyte8=>hexchars.lo-char

(defthm hex-digit-char-p-of-ubyte8=>hexchars.lo-char
  (b* (((mv ?hi-char ?lo-char)
        (ubyte8=>hexchars byte)))
    (str::hex-digit-char-p lo-char))
  :rule-classes :rewrite)

Theorem: mv-nth-0-of-ubyte8=>hexchars-of-unsigned-byte-fix

(defthm mv-nth-0-of-ubyte8=>hexchars-of-unsigned-byte-fix
  (equal (mv-nth 0
                 (ubyte8=>hexchars (unsigned-byte-fix 8 byte)))
         (mv-nth 0 (ubyte8=>hexchars byte))))

Theorem: mv-nth-1-of-ubyte8=>hexchars-of-unsigned-byte-fix

(defthm mv-nth-1-of-ubyte8=>hexchars-of-unsigned-byte-fix
  (equal (mv-nth 1
                 (ubyte8=>hexchars (unsigned-byte-fix 8 byte)))
         (mv-nth 1 (ubyte8=>hexchars byte))))

Subtopics

Ubyte8<=>hexchars-inverses-theorems: ubyte8=>hexchars and hexchars=>ubyte8 are mutual inverses.