		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

Process-command

Process a command.

Signature
(process-command inputs state) → (mv msg state)
Arguments: inputs — Guard (string-listp inputs).
Returns: msg — Type (msgp msg).

The wallet is used via a command line interface provided by an OS shell script. The user types <script> <command> <argument1> ..., where <script> is the name of the shell script, <command> is a wallet command (e.g. sign), and <argument1> etc. are zero or more arguments for the command. The <command>, argument1, etc. arguments of the script are passed to this function as strings: thus, this function takes a list of strings as input. This function also takes the ACL2 state as input, necessary to manipulate the file that stores the persistent state of the wallet.

This function returns a message and a new ACL2 state. Implicit in the new ACL2 state is the creation or update of the file that stores the wallet state. The message is the user-oriented and user-visible outcome of the command. It may be an error message or a success message.

The shell script may be called with zero or more arguments. If it is called with zero arguments, there is no wallet command and it is an error.

Otherwise, we check whether the first argument is one of the wallet command, and if it is we process it accordingly; if it is not a valid command, it is an error. Each wallet command requires a certain number of inputs: these are all but the first arguments of the shell script.

Definitions and Theorems

Function: process-command

(defun process-command (inputs state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (string-listp inputs)))
 (b* (((when (endp inputs))
       (mv (command-error-message "" (command-error-no-command))
           state))
      (command (car inputs))
      (arguments (cdr inputs))
      ((when (equal command
                    *command-name-init-from-entropy*))
       (process-init-from-entropy arguments state))
      ((when (equal command
                    *command-name-init-from-mnemonic*))
       (process-init-from-mnemonic arguments state))
      ((when (equal command *command-name-sign*))
       (process-sign arguments state))
      ((when (equal command *command-name-next-key*))
       (process-next-key arguments state)))
   (mv (command-error-message command
                              (command-error-wrong-command command))
       state)))

Theorem: msgp-of-process-command.msg

(defthm msgp-of-process-command.msg
  (b* (((mv acl2::?msg acl2::?state)
        (process-command inputs state)))
    (msgp msg))
  :rule-classes :rewrite)