		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

Process-init-from-entropy

Process a command to initialize the wallet from an entropy value.

Signature
(process-init-from-entropy 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 and the generated mnemonic.

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

Definitions and Theorems

Function: process-init-from-entropy

(defun process-init-from-entropy (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-entropy*
        (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-entropy* error?)
     state))
   (entropy-string (first arguments))
   (passphrase (second arguments))
   ((mv error? mnemonic stat?)
    (init-from-entropy entropy-string passphrase))
   ((when error?)
    (mv
     (command-error-message *command-name-init-from-entropy* error?)
     state))
   (msg
    (msg
     "The wallet has been successfully initialized ~
                  from the supplied entropy (and passphrase). ~
                  The generated mnemonic consists of the following words:~%~%~
                  ~@0~%~
                  Store this list of words in a safe place, ~
                  since it can be used to re-create this wallet. ~
                  Recall that, in order to do that, ~
                  these words must be passed to the initialization command ~
                  as a single string with single spaces separating them.~%~%"
     (mnemonic-message mnemonic)))
   (state (save-stat stat? state)))
  (mv msg state)))

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

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