RLP encoding of a transaction.

- Signature
(rlp-encode-transaction trans) → (mv error? encoding)

- Arguments
`trans`—Guard (transactionp trans) .- Returns
`error?`—Type (booleanp error?) .`encoding`—Type (byte-listp encoding) .

The first step towards RLP-encoding a transaction is to turn it into an RLP tree. This is implied by [YP:4.2], which in fact uses a tuple notation for transactions.

Each scalar component
is turned into its big-endian byte array representation,
consistently with `rlp-encode-scalar`.
Note that here we are just constructing the RLP tree,
not encoding it yet;
RLP trees cannot contain scalars.
The other components are byte arrays that are left unchanged.

We put all nine components under a branching tree,
which we RLP-encode.
Encoding may fail,
if the

**Function: **

(defun rlp-encode-transaction (trans) (declare (xargs :guard (transactionp trans))) (b* (((transaction trans) trans) (tree (rlp-tree-branch (list (rlp-tree-leaf (nat=>bebytes* trans.nonce)) (rlp-tree-leaf (nat=>bebytes* trans.gas-price)) (rlp-tree-leaf (nat=>bebytes* trans.gas-limit)) (rlp-tree-leaf trans.to) (rlp-tree-leaf (nat=>bebytes* trans.value)) (rlp-tree-leaf trans.init/data) (rlp-tree-leaf (nat=>bebytes* trans.sign-v)) (rlp-tree-leaf (nat=>bebytes* trans.sign-r)) (rlp-tree-leaf (nat=>bebytes* trans.sign-s)))))) (rlp-encode-tree tree)))

**Theorem: **

(defthm booleanp-of-rlp-encode-transaction.error? (b* (((mv ?error? ?encoding) (rlp-encode-transaction trans))) (booleanp error?)) :rule-classes :rewrite)

**Theorem: **

(defthm byte-listp-of-rlp-encode-transaction.encoding (b* (((mv ?error? ?encoding) (rlp-encode-transaction trans))) (byte-listp encoding)) :rule-classes :rewrite)

**Theorem: **

(defthm rlp-encode-transaction-of-transaction-fix-trans (equal (rlp-encode-transaction (transaction-fix trans)) (rlp-encode-transaction trans)))

**Theorem: **

(defthm rlp-encode-transaction-transaction-equiv-congruence-on-trans (implies (transaction-equiv trans trans-equiv) (equal (rlp-encode-transaction trans) (rlp-encode-transaction trans-equiv))) :rule-classes :congruence)