Process a command.
(process-command inputs state) → (mv msg state)
The wallet is used via a command line interface
provided by an OS shell script.
The user types
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.
(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)))
(defthm msgp-of-process-command.msg (b* (((mv acl2::?msg acl2::?state) (process-command inputs state))) (msgp msg)) :rule-classes :rewrite)