Parse a string into a list of 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
(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)))
(defthm booleanp-of-string-to-byte-list.error? (b* (((mv ?error? ?bytes) (string-to-byte-list string))) (booleanp error?)) :rule-classes :rewrite)
(defthm byte-listp-of-string-to-byte-list.bytes (b* (((mv ?error? ?bytes) (string-to-byte-list string))) (byte-listp bytes)) :rule-classes :rewrite)