		Search-engine friendly clone of the ACL2 documentation.

8bitbytes-hexchars-conversions

Hexchars=>ubyte8s

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

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

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

Definitions and Theorems

Function: hexchars=>ubyte8s-aux

(defun hexchars=>ubyte8s-aux (chars rev-bytes)
 (declare (xargs :guard (and (and (str::hex-digit-char-list*p chars)
                                  (true-listp chars)
                                  (evenp (len chars)))
                             (unsigned-byte-listp 8 rev-bytes))))
 (let ((__function__ 'hexchars=>ubyte8s-aux))
   (declare (ignorable __function__))
   (cond ((endp chars) (rev rev-bytes))
         (t (b* ((byte (hexchars=>ubyte8 (car chars)
                                         (cadr chars))))
              (hexchars=>ubyte8s-aux (cddr chars)
                                     (cons byte rev-bytes)))))))

Function: hexchars=>ubyte8s

(defun hexchars=>ubyte8s (chars)
 (declare (xargs :guard (and (str::hex-digit-char-list*p chars)
                             (true-listp chars)
                             (evenp (len chars)))))
 (let ((__function__ 'hexchars=>ubyte8s))
  (declare (ignorable __function__))
  (mbe
      :logic (cond ((endp chars) nil)
                   (t (b* ((byte (hexchars=>ubyte8 (car chars)
                                                   (cadr chars)))
                           (bytes (hexchars=>ubyte8s (cddr chars))))
                        (cons byte bytes))))
      :exec (hexchars=>ubyte8s-aux chars nil))))

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

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

Theorem: hexchars=>ubyte8s-of-append

(defthm hexchars=>ubyte8s-of-append
  (implies (evenp (len chars1))
           (equal (hexchars=>ubyte8s (append chars1 chars2))
                  (append (hexchars=>ubyte8s chars1)
                          (hexchars=>ubyte8s chars2)))))

Subtopics

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