		Search-engine friendly clone of the ACL2 documentation.

8bitbytes-hexstrings-conversions

Hexstring=>ubyte8s

Convert an even-length string of hexadecimal digit characters to a list of natural numbers below 256.

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

Each pair of hexadecimal digit characters is turned into sa number. Each such two-digit hexadecimal notation is treated as big endian, i.e. the most significant digit appears first.

Definitions and Theorems

Function: hexstring=>ubyte8s

(defun hexstring=>ubyte8s (string)
  (declare (xargs :guard (and (stringp string)
                              (str::hex-digit-string-p string)
                              (evenp (length string)))))
  (let ((__function__ 'hexstring=>ubyte8s))
    (declare (ignorable __function__))
    (hexchars=>ubyte8s (explode string))))

Theorem: return-type-of-hexstring=>ubyte8s

(defthm return-type-of-hexstring=>ubyte8s
  (b* ((bytes (hexstring=>ubyte8s string)))
    (unsigned-byte-listp 8 bytes))
  :rule-classes :rewrite)

Theorem: hexstring=>ubyte8s-of-string-append

(defthm hexstring=>ubyte8s-of-string-append
  (implies
       (evenp (length string1))
       (equal (hexstring=>ubyte8s (string-append string1 string2))
              (append (hexstring=>ubyte8s string1)
                      (hexstring=>ubyte8s string2)))))

Subtopics

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