Process a transaction signing command.
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.
(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)))
(defthm msgp-of-process-sign.msg (b* (((mv acl2::?msg acl2::?state) (process-sign arguments state))) (msgp msg)) :rule-classes :rewrite)