		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

Process-next-key

Process a key generation command.

Signature
(process-next-key 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 along with the index and the address of the generated key.

The file is overwritten with the new wallet state.

Definitions and Theorems

Function: process-next-key

(defun process-next-key (arguments state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (string-listp arguments)))
 (b*
  (((unless (= (len arguments) 0))
    (mv
     (command-error-message
        *command-name-next-key*
        (command-error-wrong-number-of-arguments 2 (len arguments)))
     state))
   ((mv error? state)
    (check-stat-file-present state))
   ((when error?)
    (mv (command-error-message *command-name-next-key* error?)
        state))
   ((mv error? stat? state)
    (load-stat state))
   ((when error?)
    (mv (command-error-message *command-name-next-key* error?)
        state))
   ((mv error? index address stat)
    (next-key stat?))
   ((when error?)
    (mv (command-error-message *command-name-next-key* error?)
        state))
   (state (save-stat stat state))
   (msg
    (msg
     "The address key with index ~x0 ~
                  has been successfully generated. ~
                  Its associated 20-byte address is~%~%~
                  ~s1~s2~%"
     index
     "  " (ubyte8s=>hexstring address))))
  (mv msg state)))

Theorem: msgp-of-process-next-key.msg

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