		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

Process-sign

Process a transaction signing command.

Signature
(process-sign 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 signed transaction.

The file is left unchanged, because this command does not change the state of the wallet.

Definitions and Theorems

Function: process-sign

(defun process-sign (arguments state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (string-listp arguments)))
 (b*
  (((unless (= (len arguments) 7))
    (mv
     (command-error-message
        *command-name-sign*
        (command-error-wrong-number-of-arguments 7 (len arguments)))
     state))
   ((mv error? state)
    (check-stat-file-present state))
   ((when error?)
    (mv (command-error-message *command-name-sign* error?)
        state))
   (nonce-string (first arguments))
   (gas-price-string (second arguments))
   (gas-limit-string (third arguments))
   (to-string (fourth arguments))
   (value-string (fifth arguments))
   (data-string (sixth arguments))
   (address-key-index-string (seventh arguments))
   ((mv error? stat? state)
    (load-stat state))
   ((when error?)
    (mv (command-error-message *command-name-sign* error?)
        state))
   ((mv error? signed-transaction)
    (sign nonce-string
          gas-price-string gas-limit-string
          to-string value-string data-string
          address-key-index-string stat?))
   ((when error?)
    (mv (command-error-message *command-name-sign* error?)
        state))
   (msg
    (msg
     "The transaction has been successfully signed ~
                  with the address key with index ~s0. ~
                  The signed transaction consists of the bytes~%~%~
                  ~@1~%"
     address-key-index-string
     (transaction-message signed-transaction))))
  (mv msg state)))

Theorem: msgp-of-process-sign.msg

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