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

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

The RLP-encoded tuple is hashed with Keccak-256 [YP:F].
The hash

If the ECDSA signature operation succeeds,
the resulting

Besides communicating the chain id, the resulting `secp256k1-sign-det-rec`,
the

[YP:(281)] requires the `secp256k1-sign-det-rec`,
the

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

**Function: **

(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: **

(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: **

(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: **

(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: **

(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: **

(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: **

(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: **

(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: **

(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: **

(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: **

(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: **

(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: **

(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: **

(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: **

(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: **

(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: **

(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: **

(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: **

(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)