		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

String-to-word

Parse a string into a word.

Signature
(string-to-word string) → (mv error? word)
Arguments: string — Guard (stringp string).
Returns: error? — Type (booleanp error?).; word — Type (wordp 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 t.

Definitions and Theorems

Function: string-to-word

(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)))

Theorem: booleanp-of-string-to-word.error?

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

Theorem: wordp-of-string-to-word.word

(defthm wordp-of-string-to-word.word
  (b* (((mv ?error? ?word)
        (string-to-word string)))
    (wordp word))
  :rule-classes :rewrite)