		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

String-to-byte-list

Parse a string into a list of bytes.

Signature
(string-to-byte-list string) → (mv error? bytes)
Arguments: string — Guard (stringp string).
Returns: error? — Type (booleanp error?).; bytes — Type (byte-listp bytes).

Certain wallet commands take byte lists as inputs, which are supplied by the wallet's user as strings. These must be an even-length strings of hexadecimal digits, where the letters may be uppercase or lowercase. Each pair of hexadecimal digits is turned into a byte, with the first digit becoming the most significant nibble of the byte. If the string cannot be converted to a byte list, the error result is t.

Definitions and Theorems

Function: string-to-byte-list

(defun string-to-byte-list (string)
  (declare (xargs :guard (stringp string)))
  (if (and (stringp string)
           (hex-digit-string-p string)
           (evenp (length string)))
      (mv nil (hexstring=>ubyte8s string))
    (mv t nil)))

Theorem: booleanp-of-string-to-byte-list.error?

(defthm booleanp-of-string-to-byte-list.error?
  (b* (((mv ?error? ?bytes)
        (string-to-byte-list string)))
    (booleanp error?))
  :rule-classes :rewrite)

Theorem: byte-listp-of-string-to-byte-list.bytes

(defthm byte-listp-of-string-to-byte-list.bytes
  (b* (((mv ?error? ?bytes)
        (string-to-byte-list string)))
    (byte-listp bytes))
  :rule-classes :rewrite)