		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

Process-init-from-mnemonic

Process a command to initialize the wallet from a mnenonic.

Signature
(process-init-from-mnemonic arguments state) → (mv msg state)
Arguments: arguments — Guard (string-listp arguments).
Returns: msg — Type (msgp msg).

The message returned by this function describes an error if one occurs, otherwise it describes success.

If no error occurs, the wallet state file is created.

Definitions and Theorems

Function: process-init-from-mnemonic

(defun process-init-from-mnemonic (arguments state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (string-listp arguments)))
 (b*
  (((unless (= (len arguments) 2))
    (mv
     (command-error-message
        *command-name-init-from-mnemonic*
        (command-error-wrong-number-of-arguments 2 (len arguments)))
     state))
   ((mv error? state)
    (check-stat-file-absent state))
   ((when error?)
    (mv (command-error-message *command-name-init-from-mnemonic*
                               error?)
        state))
   (mnemonic (first arguments))
   (passphrase (second arguments))
   ((mv error? stat?)
    (init-from-mnemonic mnemonic passphrase))
   ((when error?)
    (mv (command-error-message *command-name-init-from-mnemonic*
                               error?)
        state))
   (state (save-stat stat? state))
   (msg
    (msg
     "The wallet has been successfully initialized ~
                  from the supplied mnemonic (and passphrase).~%~%")))
  (mv msg state)))

Theorem: msgp-of-process-init-from-mnemonic.msg

(defthm msgp-of-process-init-from-mnemonic.msg
  (b* (((mv acl2::?msg acl2::?state)
        (process-init-from-mnemonic arguments state)))
    (msgp msg))
  :rule-classes :rewrite)