• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • Soft
      • C
      • Bv
      • Imp-language
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
        • Mmp-trees
        • Semaphore
        • Database
        • Cryptography
        • Rlp
        • Transactions
          • Make-signed-transaction
          • Transaction
          • Maybe-byte-list20
          • Rlp-decode-transaction
          • Rlp-encode-transaction
          • Rlp-transaction-encoding-p
        • Hex-prefix
        • Basics
        • Addresses
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Lists-light
      • Axe
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Transactions

Make-signed-transaction

Construction of a signed transaction.

Signature

(make-signed-transaction nonce gas-price gas-limit 
                         to value init/data chain-id key) 
 
  → 
(mv error? transaction)

Arguments

nonce — Guard (wordp nonce).

gas-price — Guard (wordp gas-price).

gas-limit — Guard (wordp gas-limit).

to — Guard (maybe-byte-list20p to).

value — Guard (wordp value).

init/data — Guard (byte-listp init/data).

chain-id — Guard (natp chain-id).

key — Guard (secp256k1-priv-key-p key).

Returns

error? — Type (member error? '(nil :rlp :ecdsa)).

transaction — Type (transactionp transaction).

This operation is described in [YP:F]. Two flavors exist, corresponding to the two cases in [YP:(285)]: one before and one after the `Spurious Dragon' hard fork [EIP155].

In both flavors, one starts with the first six components of a transaction: nonce, gas price, gas limit, recipient, value, and initialization/data; these are all inputs of this function. A tuple is then formed, which differs slightly depending on the flavor [YP:(285)]: in the ``old'' flavor, the tuple just consists of these six components; in the ``new'' flavor, a 9-tuple is formed consisting of these six components, a chain id, and two empty byte arrays. The 6-tuple is like a partial transaction, whose last three components are missing. The 9-tuple is like a pre-transaction whose last three components contain preliminary values.

The chain id is the seventh input of this function. [EIP155] suggests that the chain id is never zero; at least, it lists only non-zero chain ids. Thus, we use 0 as input to this function to select the old flavor, and any non-zero value to select the new flavor; we do not constrain the non-zero value to be among the chain ids listed in [EIP155].

[YP:(285)] uses the v result of the ECDSA signature [YP:(279)] to distinguish between old and new flavors. This is a bit confusing, because the ECDSA signature is calculated after forming the tuple, not before. The choice of flavor should be determined by external means, such as the chain id input of this function. (Since we are past the Spurious Dragon hard fork, new transactions should always use the new flavor; however, this function models the construction of transactions before that hard fork as well.)

The tuple notation in [YP:(285)], and the fact that the tuples must be hashed, suggests that the tuples are in fact RLP trees. In the new flavor, the () in the last two components could denote the branching tree with no subtrees, but it is more reasonable that it denotes the empty byte array instead. This is also consistent with the fact that, in a transaction, the last two components are words, and that the scalar 0 (which is a reasonable value for the pre-transaction) is encoded in the same way as the empty byte array.

The RLP-encoded tuple is hashed with Keccak-256 [YP:F]. The hash e = h(T) (using the notation in [YP:F], where h is Keccak-256) is passed to the ECDSA signature operation, along with a private key that is also an input of this function. If the ECDSA signature operation fails, the construction of the signed transaction fails; this is not explicit in [YP:F].

If the ECDSA signature operation succeeds, the resulting v, r, and s are used to construct the last three components of the final signed transaction, whose first six components are the same as the first six in in the 6-tuple or 9-tuple. r and s are used directly as the last two components, i.e. T_\mathrm{r} and T_\mathrm{s} [YP:(15)]. The component T_\mathrm{w} depends on the flavor (before or after the Spurious Dragon hard fork) [YP:F]: in the old flavor, T_\mathrm{w} is 27 if v indicates an even ephemeral public key y value, or 28 if v indicates odd; in the new flavor, T_\mathrm{w} is the chain identifier doubled plus 35 if v indicates an even ephemeral public key y value, or the chain identifier doubled plus 36 if v indicates odd. The formulation in [YP:F] suggests that the ECDSA signature operation already returns these values as the v result, but these are Ethereum-specific: our Ethereum-independent library function for ECDSA signatures returns a boolean v, which represents an even ephemeral public key y value as t and odd as nil.

Besides communicating the chain id, the resulting v component of the signature can be used for public key recovery. Based on the discussion in secp256k1-sign-det-rec, the small-x? flag passed to this signing function must be t, so that the parity of the y coordinate suffices to recover the public key.

[YP:(281)] requires the s component of the signature to be below half of the order of the curve. Based on the discussion in secp256k1-sign-det-rec, the small-s? flag passed to this signing function must be t, so that an s suitable for Ethereum is returned.

This function returns the signed transaction as a high-level structure. This must be RLP-encoded (via rlp-encode-transaction) to obtain something that can be sent to the Ethereum network.

This function returns :rlp as the error result if the RLP encoding of the 6-tuple or 9-tuple fails. If the ECDSA signature operation fails, the error result is :ecdsa. In both cases, the second result is an irrelevant transaction value.

Definitions and Theorems

Function: make-signed-transaction

(defun make-signed-transaction
       (nonce gas-price gas-limit
              to value init/data chain-id key)
 (declare (xargs :guard (and (wordp nonce)
                             (wordp gas-price)
                             (wordp gas-limit)
                             (maybe-byte-list20p to)
                             (wordp value)
                             (byte-listp init/data)
                             (natp chain-id)
                             (secp256k1-priv-key-p key))))
 (let ((__function__ 'make-signed-transaction))
  (declare (ignorable __function__))
  (b* ((nonce (word-fix nonce))
       (gas-price (word-fix gas-price))
       (gas-limit (word-fix gas-limit))
       (to (maybe-byte-list20-fix to))
       (value (word-fix value))
       (6/9-tuple
            (if (zp chain-id)
                (rlp-tree-branch
                     (list (rlp-tree-leaf (nat=>bebytes* nonce))
                           (rlp-tree-leaf (nat=>bebytes* gas-price))
                           (rlp-tree-leaf (nat=>bebytes* gas-limit))
                           (rlp-tree-leaf to)
                           (rlp-tree-leaf (nat=>bebytes* value))
                           (rlp-tree-leaf init/data)))
              (rlp-tree-branch
                   (list (rlp-tree-leaf (nat=>bebytes* nonce))
                         (rlp-tree-leaf (nat=>bebytes* gas-price))
                         (rlp-tree-leaf (nat=>bebytes* gas-limit))
                         (rlp-tree-leaf to)
                         (rlp-tree-leaf (nat=>bebytes* value))
                         (rlp-tree-leaf init/data)
                         (rlp-tree-leaf (nat=>bebytes* chain-id))
                         (rlp-tree-leaf nil)
                         (rlp-tree-leaf nil)))))
       ((mv error? message)
        (rlp-encode-tree 6/9-tuple))
       ((when error?)
        (mv :rlp (transaction 0 0 0 nil 0 nil 0 0 0)))
       (hash (keccak-256-bytes message))
       ((mv error? & even? sign-r sign-s)
        (secp256k1-sign-det-rec hash key t t))
       ((when error?)
        (mv :ecdsa (transaction 0 0 0 nil 0 nil 0 0 0)))
       (sign-v (if (zp chain-id)
                   (if even? 27 28)
                 (+ (* 2 chain-id) (if even? 35 36)))))
    (mv nil
        (make-transaction :nonce nonce
                          :gas-price gas-price
                          :gas-limit gas-limit
                          :to to
                          :value value
                          :init/data init/data
                          :sign-v sign-v
                          :sign-r sign-r
                          :sign-s sign-s)))))

Theorem: return-type-of-make-signed-transaction.error?

(defthm return-type-of-make-signed-transaction.error?
  (b* (((mv ?error? ?transaction)
        (make-signed-transaction nonce gas-price gas-limit
                                 to value init/data chain-id key)))
    (member error? '(nil :rlp :ecdsa)))
  :rule-classes :rewrite)

Theorem: transactionp-of-make-signed-transaction.transaction

(defthm transactionp-of-make-signed-transaction.transaction
  (b* (((mv ?error? ?transaction)
        (make-signed-transaction nonce gas-price gas-limit
                                 to value init/data chain-id key)))
    (transactionp transaction))
  :rule-classes :rewrite)

Theorem: make-signed-transaction-of-word-fix-nonce

(defthm make-signed-transaction-of-word-fix-nonce
  (equal (make-signed-transaction (word-fix nonce)
                                  gas-price gas-limit
                                  to value init/data chain-id key)
         (make-signed-transaction nonce gas-price gas-limit
                                  to value init/data chain-id key)))

Theorem: make-signed-transaction-word-equiv-congruence-on-nonce

(defthm make-signed-transaction-word-equiv-congruence-on-nonce
 (implies
  (word-equiv nonce nonce-equiv)
  (equal (make-signed-transaction nonce gas-price gas-limit
                                  to value init/data chain-id key)
         (make-signed-transaction nonce-equiv gas-price gas-limit
                                  to value init/data chain-id key)))
 :rule-classes :congruence)

Theorem: make-signed-transaction-of-word-fix-gas-price

(defthm make-signed-transaction-of-word-fix-gas-price
  (equal (make-signed-transaction nonce (word-fix gas-price)
                                  gas-limit
                                  to value init/data chain-id key)
         (make-signed-transaction nonce gas-price gas-limit
                                  to value init/data chain-id key)))

Theorem: make-signed-transaction-word-equiv-congruence-on-gas-price

(defthm make-signed-transaction-word-equiv-congruence-on-gas-price
 (implies
  (word-equiv gas-price gas-price-equiv)
  (equal (make-signed-transaction nonce gas-price gas-limit
                                  to value init/data chain-id key)
         (make-signed-transaction nonce gas-price-equiv gas-limit
                                  to value init/data chain-id key)))
 :rule-classes :congruence)

Theorem: make-signed-transaction-of-word-fix-gas-limit

(defthm make-signed-transaction-of-word-fix-gas-limit
  (equal
       (make-signed-transaction nonce gas-price (word-fix gas-limit)
                                to value init/data chain-id key)
       (make-signed-transaction nonce gas-price gas-limit
                                to value init/data chain-id key)))

Theorem: make-signed-transaction-word-equiv-congruence-on-gas-limit

(defthm make-signed-transaction-word-equiv-congruence-on-gas-limit
 (implies
  (word-equiv gas-limit gas-limit-equiv)
  (equal (make-signed-transaction nonce gas-price gas-limit
                                  to value init/data chain-id key)
         (make-signed-transaction nonce gas-price gas-limit-equiv
                                  to value init/data chain-id key)))
 :rule-classes :congruence)

Theorem: make-signed-transaction-of-maybe-byte-list20-fix-to

(defthm make-signed-transaction-of-maybe-byte-list20-fix-to
  (equal
       (make-signed-transaction nonce gas-price
                                gas-limit (maybe-byte-list20-fix to)
                                value init/data chain-id key)
       (make-signed-transaction nonce gas-price gas-limit
                                to value init/data chain-id key)))

Theorem: make-signed-transaction-maybe-byte-list20-equiv-congruence-on-to

(defthm
   make-signed-transaction-maybe-byte-list20-equiv-congruence-on-to
 (implies
  (maybe-byte-list20-equiv to to-equiv)
  (equal
   (make-signed-transaction nonce gas-price gas-limit
                            to value init/data chain-id key)
   (make-signed-transaction nonce gas-price gas-limit
                            to-equiv value init/data chain-id key)))
 :rule-classes :congruence)

Theorem: make-signed-transaction-of-word-fix-value

(defthm make-signed-transaction-of-word-fix-value
 (equal
    (make-signed-transaction nonce
                             gas-price gas-limit to (word-fix value)
                             init/data chain-id key)
    (make-signed-transaction nonce gas-price gas-limit
                             to value init/data chain-id key)))

Theorem: make-signed-transaction-word-equiv-congruence-on-value

(defthm make-signed-transaction-word-equiv-congruence-on-value
 (implies
  (word-equiv value value-equiv)
  (equal
   (make-signed-transaction nonce gas-price gas-limit
                            to value init/data chain-id key)
   (make-signed-transaction nonce gas-price gas-limit
                            to value-equiv init/data chain-id key)))
 :rule-classes :congruence)

Theorem: make-signed-transaction-of-byte-list-fix-init/data

(defthm make-signed-transaction-of-byte-list-fix-init/data
  (equal (make-signed-transaction nonce gas-price gas-limit
                                  to value (byte-list-fix init/data)
                                  chain-id key)
         (make-signed-transaction nonce gas-price gas-limit
                                  to value init/data chain-id key)))

Theorem: make-signed-transaction-byte-list-equiv-congruence-on-init/data

(defthm
    make-signed-transaction-byte-list-equiv-congruence-on-init/data
 (implies
  (byte-list-equiv init/data init/data-equiv)
  (equal
   (make-signed-transaction nonce gas-price gas-limit
                            to value init/data chain-id key)
   (make-signed-transaction nonce gas-price gas-limit
                            to value init/data-equiv chain-id key)))
 :rule-classes :congruence)

Theorem: make-signed-transaction-of-nfix-chain-id

(defthm make-signed-transaction-of-nfix-chain-id
  (equal (make-signed-transaction nonce gas-price gas-limit
                                  to value init/data (nfix chain-id)
                                  key)
         (make-signed-transaction nonce gas-price gas-limit
                                  to value init/data chain-id key)))

Theorem: make-signed-transaction-nat-equiv-congruence-on-chain-id

(defthm make-signed-transaction-nat-equiv-congruence-on-chain-id
 (implies
  (acl2::nat-equiv chain-id chain-id-equiv)
  (equal
   (make-signed-transaction nonce gas-price gas-limit
                            to value init/data chain-id key)
   (make-signed-transaction nonce gas-price gas-limit
                            to value init/data chain-id-equiv key)))
 :rule-classes :congruence)

Theorem: make-signed-transaction-of-secp256k1-priv-key-fix-key

(defthm make-signed-transaction-of-secp256k1-priv-key-fix-key
 (equal
      (make-signed-transaction nonce gas-price
                               gas-limit to value init/data chain-id
                               (ecurve::secp256k1-priv-key-fix key))
      (make-signed-transaction nonce gas-price gas-limit
                               to value init/data chain-id key)))

Theorem: make-signed-transaction-secp256k1-priv-key-equiv-congruence-on-key

(defthm
 make-signed-transaction-secp256k1-priv-key-equiv-congruence-on-key
 (implies
  (ecurve::secp256k1-priv-key-equiv key key-equiv)
  (equal
   (make-signed-transaction nonce gas-price gas-limit
                            to value init/data chain-id key)
   (make-signed-transaction nonce gas-price gas-limit
                            to value init/data chain-id key-equiv)))
 :rule-classes :congruence)