RLP decoding of a byte array.

- Signature
(rlp-decode-bytes encoding) → (mv error? bytes)

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

This is analogous to `rlp-decode-tree`.
If the returned error flag is

As proved in `rlp-bytes-encoding-p`,
the encoding of a byte array
is also the encoding of the leaf tree containing the byte array.
Because `rlp-encode-tree` is injective,
the two witnesses (decoders)
`rlp-encode-bytes`,
i.e. `rlp-encode-bytes`
in terms of `rlp-encode-tree` to obtain
`rlp-encode-tree`,
i.e. `rlp-encode-tree`, derive

This relationship among these witnesses lets us prove a theorem
that provides an alternative definition of `rlp-decode-bytes`
in terms of `rlp-decode-tree`.

**Function: **

(defun rlp-decode-bytes (encoding) (declare (xargs :guard (byte-listp encoding))) (b* ((encoding (byte-list-fix encoding))) (if (rlp-bytes-encoding-p encoding) (mv nil (rlp-bytes-encoding-witness encoding)) (mv t nil))))

**Theorem: **

(defthm booleanp-of-rlp-decode-bytes.error? (b* (((mv ?error? ?bytes) (rlp-decode-bytes encoding))) (booleanp error?)) :rule-classes :rewrite)

**Theorem: **

(defthm byte-listp-of-rlp-decode-bytes.bytes (b* (((mv ?error? ?bytes) (rlp-decode-bytes encoding))) (byte-listp bytes)) :rule-classes :rewrite)

**Theorem: **

(defthm rlp-encode-bytes-of-rlp-decode-bytes (implies (rlp-bytes-encoding-p encoding) (b* (((mv d-error? bytes) (rlp-decode-bytes encoding)) ((mv e-error? encoding1) (rlp-encode-bytes bytes))) (and (not d-error?) (not e-error?) (equal encoding1 (byte-list-fix encoding))))))

**Theorem: **

(defthm rlp-decode-bytes-of-rlp-encode-bytes (b* (((mv e-error? encoding) (rlp-encode-bytes bytes)) ((mv d-error? bytes1) (rlp-decode-bytes encoding))) (implies (not e-error?) (and (not d-error?) (equal bytes1 (byte-list-fix bytes))))))

**Theorem: **

(defthm rlp-tree-encoding-witness-as-rlp-bytes-encoding-witness (implies (rlp-bytes-encoding-p encoding) (equal (rlp-tree-encoding-witness encoding) (rlp-tree-leaf (rlp-bytes-encoding-witness encoding)))))

**Theorem: **

(defthm rlp-bytes-encoding-witness-as-rlp-tree-encoding-witness (implies (rlp-bytes-encoding-p encoding) (equal (rlp-bytes-encoding-witness encoding) (rlp-tree-leaf->bytes (rlp-tree-encoding-witness encoding)))))

**Theorem: **

(defthm rlp-decode-bytes-alt-def (equal (rlp-decode-bytes encoding) (b* (((mv error? tree) (rlp-decode-tree encoding)) ((when error?) (mv t nil)) ((unless (rlp-tree-case tree :leaf)) (mv t nil)) (bytes (rlp-tree-leaf->bytes tree))) (mv nil bytes))))

**Theorem: **

(defthm rlp-decode-bytes-of-byte-list-fix-encoding (equal (rlp-decode-bytes (byte-list-fix encoding)) (rlp-decode-bytes encoding)))

**Theorem: **

(defthm rlp-decode-bytes-byte-list-equiv-congruence-on-encoding (implies (byte-list-equiv encoding encoding-equiv) (equal (rlp-decode-bytes encoding) (rlp-decode-bytes encoding-equiv))) :rule-classes :congruence)