RLP encoding of a tree.

- Signature
(rlp-encode-tree tree) → (mv error? encoding)

- Arguments
`tree`—Guard (rlp-treep tree) .- Returns
`error?`—Type (booleanp error?) .`encoding`—Type (byte-listp encoding) .

This corresponds to
`rlp-encode-tree` corresponds to `rlp-encode-tree`
corresponds to `rlp-encode-tree-list` corresponds to

The first result of
`rlp-encode-tree` and `rlp-encode-tree-list`
is an error flag,
which is

Encodings are never empty,
i.e. they always consist of at least one byte:
see theorem

The first byte of the encoding of a leaf tree is always below 192:
see theorems

The total length of an encoding can be determined
from the first few bytes (i.e. a prefix) of the encoding:
see theorem

The total length of an encoding that uses a ``long'' length field
(i.e. when the initial byte is followed by the length of the length,
and the actual length consists of one or more bytes)
is larger than the length field itself:
see theorems

Once `rlp-encode-tree` is defined,
`rlp-encode-bytes` could be alternatively ``defined''
by wrapping the byte array in a tree and encoding the tree.
This alternative definition rule is disabled by default,
but may be useful sometimes.
It should not be enabled
if the definition of `rlp-encode-tree` is enabled
(since the latter is defined in terems of `rlp-encode-bytes`,
so we add a theory invariant to that effect.

**Function: **

(defun rlp-encode-tree (tree) (declare (xargs :guard (rlp-treep tree))) (rlp-tree-case tree :leaf (rlp-encode-bytes tree.bytes) :branch (b* (((mv error? subencoding) (rlp-encode-tree-list tree.subtrees)) ((when error?) (mv t nil))) (cond ((< (len subencoding) 56) (b* ((encoding (cons (+ 192 (len subencoding)) subencoding))) (mv nil encoding))) ((< (len subencoding) (expt 2 64)) (b* ((be (nat=>bebytes* (len subencoding))) (encoding (cons (+ 247 (len be)) (append be subencoding)))) (mv nil encoding))) (t (mv t nil))))))

**Function: **

(defun rlp-encode-tree-list (trees) (declare (xargs :guard (rlp-tree-listp trees))) (b* (((when (endp trees)) (mv nil nil)) ((mv error? encoding1) (rlp-encode-tree (car trees))) ((when error?) (mv t nil)) ((mv error? encoding2) (rlp-encode-tree-list (cdr trees))) ((when error?) (mv t nil))) (mv nil (append encoding1 encoding2))))

**Theorem: **

(defthm return-type-of-rlp-encode-tree.error? (b* (((mv ?error? ?encoding) (rlp-encode-tree tree))) (booleanp error?)) :rule-classes :rewrite)

**Theorem: **

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

**Theorem: **

(defthm return-type-of-rlp-encode-tree-list.error? (b* (((mv ?error? ?encoding) (rlp-encode-tree-list trees))) (booleanp error?)) :rule-classes :rewrite)

**Theorem: **

(defthm return-type-of-rlp-encode-tree-list.encoding (b* (((mv ?error? ?encoding) (rlp-encode-tree-list trees))) (byte-listp encoding)) :rule-classes :rewrite)

**Theorem: **

(defthm rlp-encode-tree-of-rlp-tree-fix-tree (equal (rlp-encode-tree (rlp-tree-fix tree)) (rlp-encode-tree tree)))

**Theorem: **

(defthm rlp-encode-tree-list-of-rlp-tree-list-fix-trees (equal (rlp-encode-tree-list (rlp-tree-list-fix trees)) (rlp-encode-tree-list trees)))

**Theorem: **

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

**Theorem: **

(defthm rlp-encode-tree-list-rlp-tree-list-equiv-congruence-on-trees (implies (rlp-tree-list-equiv trees trees-equiv) (equal (rlp-encode-tree-list trees) (rlp-encode-tree-list trees-equiv))) :rule-classes :congruence)

**Theorem: **

(defthm consp-of-rlp-encode-tree-when-no-error (implies (not (mv-nth 0 (rlp-encode-tree tree))) (consp (mv-nth 1 (rlp-encode-tree tree)))) :rule-classes :type-prescription)

**Theorem: **

(defthm car-of-rlp-encode-tree-leaf-upper-bound-when-no-error (implies (and (not (mv-nth 0 (rlp-encode-tree tree))) (rlp-tree-case tree :leaf)) (<= (car (mv-nth 1 (rlp-encode-tree tree))) 191)) :rule-classes :linear)

**Theorem: **

(defthm car-of-rlp-encode-tree-branch-upper-bound-when-no-error (implies (and (not (mv-nth 0 (rlp-encode-tree tree))) (rlp-tree-case tree :branch)) (>= (car (mv-nth 1 (rlp-encode-tree tree))) 192)) :rule-classes :linear)

**Theorem: **

(defthm rlp-encode-tree-car-ineq-to-tree-leaf (implies (not (mv-nth 0 (rlp-encode-tree tree))) (equal (<= (car (mv-nth 1 (rlp-encode-tree tree))) 191) (rlp-tree-case tree :leaf))))

**Theorem: **

(defthm rlp-encode-tree-car-ineq-to-tree-branch (implies (not (mv-nth 0 (rlp-encode-tree tree))) (equal (>= (car (mv-nth 1 (rlp-encode-tree tree))) 192) (rlp-tree-case tree :branch))))

**Theorem: **

(defthm len-of-rlp-encode-tree-from-prefix (b* (((mv error? encoding) (rlp-encode-tree tree))) (implies (not error?) (equal (len encoding) (cond ((< (car encoding) 128) 1) ((< (car encoding) (+ 128 56)) (1+ (- (car encoding) 128))) ((< (car encoding) 192) (b* ((lenlen (- (car encoding) 183))) (+ 1 lenlen (bebytes=>nat (take lenlen (cdr encoding)))))) ((< (car encoding) (+ 192 56)) (1+ (- (car encoding) 192))) (t (b* ((lenlen (- (car encoding) 247))) (+ 1 lenlen (bebytes=>nat (take lenlen (cdr encoding)))))))))))

**Theorem: **

(defthm len-of-rlp-encode-tree-lower-bound-when-len-len-1 (b* (((mv error? encoding) (rlp-encode-tree tree))) (implies (and (not error?) (>= (car encoding) (+ 128 56)) (< (car encoding) 192)) (> (len encoding) (- (car encoding) 183)))) :rule-classes :linear)

**Theorem: **

(defthm len-of-rlp-encode-tree-lower-bound-when-len-len-2 (b* (((mv error? encoding) (rlp-encode-tree tree))) (implies (and (not error?) (>= (car encoding) (+ 192 56))) (> (len encoding) (- (car encoding) 247)))) :rule-classes :linear)

**Theorem: **

(defthm consp-of-rlp-encode-tree-list-when-no-error (implies (not (mv-nth 0 (rlp-encode-tree-list trees))) (equal (consp (mv-nth 1 (rlp-encode-tree-list trees))) (consp trees))))

**Theorem: **

(defthm nonnil-rlp-encode-tree-list-when-no-error (implies (not (mv-nth 0 (rlp-encode-tree-list trees))) (iff (mv-nth 1 (rlp-encode-tree-list trees)) (consp trees))))

**Theorem: **

(defthm rlp-encode-bytes-alt-def (equal (rlp-encode-bytes bytes) (rlp-encode-tree (rlp-tree-leaf bytes))))