		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

Sign

Transaction signature in the wallet.

Signature
(sign nonce-string gas-price-string gas-limit-string to-string value-string data-string address-key-index-string stat) → (mv error? signed-transaction)
Arguments: nonce-string — Guard (stringp nonce-string).; gas-price-string — Guard (stringp gas-price-string).; gas-limit-string — Guard (stringp gas-limit-string).; to-string — Guard (stringp to-string).; value-string — Guard (stringp value-string).; data-string — Guard (stringp data-string).; address-key-index-string — Guard (stringp address-key-index-string).; stat — Guard (statp stat).
Returns: error? — Type (maybe-command-error-p error?).; signed-transaction — Type (byte-listp signed-transaction).

This models the command used to sign a transaction with a key in the wallet.

In Ethereum, a transaction is a 9-tuple, as formalized here. The first six components are inputs of this function: nonce, gas price, gas limit, recipient, value, and data. For now, we do not support contract creation transactions; thus, the sixth component is always data bytes, not initialization bytes. The other three components are the signature, which this function calculates.

The address key to use is specified by another input of this function. This index is used to retrieve the key from the state. The index must be below the number of address keys generated so far, otherwise an error saying that the index is too large is returned. In addition, the index must correspond to an existing key, one whose derivation has not failed; otherwise an error saying that the key was skipped was returned.

We construct a signed transaction with chain id 1, which is for the Ethereum mainnet. We return the RLP encoding of that transaction.

The guard proofs of this operation need some of the constraints formalized in stat-wfp.

Since this operation does not change the (and does not return a) state, it trivially preserves the state constraints stat-wfp.

The six components of the transaction are passed as string inputs, which we parse and validate. Is validation fails, specific error values are returned.

Definitions and Theorems

Function: sign

(defun sign (nonce-string gas-price-string gas-limit-string
                          to-string value-string data-string
                          address-key-index-string stat)
  (declare (xargs :guard (and (stringp nonce-string)
                              (stringp gas-price-string)
                              (stringp gas-limit-string)
                              (stringp to-string)
                              (stringp value-string)
                              (stringp data-string)
                              (stringp address-key-index-string)
                              (statp stat))))
  (declare (xargs :guard (stat-wfp stat)))
  (b*
   (((mv error? nonce)
     (string-to-word nonce-string))
    ((when error?)
     (mv (command-error-malformed-nonce nonce-string)
         nil))
    ((mv error? gas-price)
     (string-to-word gas-price-string))
    ((when error?)
     (mv (command-error-malformed-gas-price gas-price-string)
         nil))
    ((mv error? gas-limit)
     (string-to-word gas-limit-string))
    ((when error?)
     (mv (command-error-malformed-gas-limit gas-limit-string)
         nil))
    ((mv error? to)
     (string-to-byte-list to-string))
    ((when (or error? (not (= (len to) 20))))
     (mv (command-error-malformed-to to-string)
         nil))
    ((mv error? value)
     (string-to-word value-string))
    ((when error?)
     (mv (command-error-malformed-value value-string)
         nil))
    ((mv error? data)
     (string-to-byte-list data-string))
    ((when error?)
     (mv (command-error-malformed-data data-string)
         nil))
    ((mv error? address-key-index)
     (string-to-nat address-key-index-string))
    ((when error?)
     (mv (command-error-malformed-address-key-index
              address-key-index-string)
         nil))
    ((unless (< address-key-index
                (stat->addresses stat)))
     (mv (command-error-address-key-index-too-large
              address-key-index
              (stat->addresses stat))
         nil))
    ((unless (bip32-path-in-tree-p
                  (rcons address-key-index *key-path-prefix*)
                  (stat->keys stat)))
     (mv (command-error-address-key-index-skipped address-key-index)
         nil))
    (path (rcons address-key-index *key-path-prefix*))
    (key (bip32-get-priv-key-at-path (stat->keys stat)
                                     path))
    (chain-id 1)
    ((mv error? transaction)
     (make-signed-transaction nonce gas-price
                              gas-limit to value data chain-id key))
    ((when (eq error? :rlp))
     (mv (command-error-pretransaction-rlp-fail)
         nil))
    ((when (eq error? :ecdsa))
     (mv (command-error-transaction-sign-fail)
         nil))
    ((mv error? transaction-rlp)
     (rlp-encode-transaction transaction))
    ((when error?)
     (mv (command-error-transaction-rlp-fail)
         nil)))
   (mv nil transaction-rlp)))

Theorem: maybe-command-error-p-of-sign.error?

(defthm maybe-command-error-p-of-sign.error?
  (b* (((mv ?error? ?signed-transaction)
        (sign nonce-string
              gas-price-string gas-limit-string
              to-string value-string data-string
              address-key-index-string stat)))
    (maybe-command-error-p error?))
  :rule-classes :rewrite)

Theorem: byte-listp-of-sign.signed-transaction

(defthm byte-listp-of-sign.signed-transaction
  (b* (((mv ?error? ?signed-transaction)
        (sign nonce-string
              gas-price-string gas-limit-string
              to-string value-string data-string
              address-key-index-string stat)))
    (byte-listp signed-transaction))
  :rule-classes :rewrite)