Parse a string into a word.
Certain wallet commands take words (in the Ethereum sense) as inputs,
which are supplied by the wallet's user as strings.
These must be non-empty sequences of decimal digits,
which are turned into their big-endian value.
If the string cannot be converted to a word,
the error result is
(defun string-to-word (string) (declare (xargs :guard (stringp string))) (b* (((mv error? val) (string-to-nat string)) ((when error?) (mv error? 0)) ((unless (wordp val)) (mv t 0))) (mv nil val)))
(defthm booleanp-of-string-to-word.error? (b* (((mv ?error? ?word) (string-to-word string))) (booleanp error?)) :rule-classes :rewrite)
(defthm wordp-of-string-to-word.word (b* (((mv ?error? ?word) (string-to-word string))) (wordp word)) :rule-classes :rewrite)