Executable RLP decoding of a tree.

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

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

We simply parse the tree and ensure that there are no remaining bytes. In case of error, we return an irrelevant tree as second result.

The `rlp-decode-tree`.

The left inverse theorem

The right inverse theorem `append`
and so we use it with a

Using these left and right inverse theorems,
we prove that the executable decoder
is equivalent to `rlp-decode-tree`,
i.e. the executable decoder is correct.
The equivalence is `iff` for the error result,
because the executable decoder returns various kinds of errors,
while the declaratively defined decoder returns just one kind.

Since `rlp-decode-tree` is defined
as a case split on `rlp-tree-encoding-p`,
we first show that the latter is equivalent to
`rlp-decodex-tree` not returning an error
(note that this equivalence does not hold for `rlp-parse-tree`,
which accepts any extensions of the valid encodings).
The `if' part is proved via the right inverse theorem,
which says that the encoding is in the image of `rlp-encode-tree`.
The `only if' part is proved via the part of the left inverse theorem
that says that if the encoding returns no error
then decoding on the encoding returns no error
(roughly speaking, `rlp-tree-encoding-p` hypothesis establishes the antecedent,
and the right inverse property of the witness reduces the consequent
to just

With the above equivalence in hand,
the equality of `rlp-decode-tree` and `rlp-decodex-tree`
is proved by case splitting on `rlp-tree-encoding-p`.
If that predicate is false,
both definitions immediately return the same result.
Otherwise,
the error results are the same because of the above equivalence,
and the fact that the tree results are the same is proved
from the injectivity of `rlp-encode-tree`
and the fact that both `rlp-decode-tree` and `rlp-decodex-tree`
are right inverses of `rlp-encode-tree`.

**Function: **

(defun rlp-decodex-tree (encoding) (declare (xargs :guard (byte-listp encoding))) (let ((__function__ 'rlp-decodex-tree)) (declare (ignorable __function__)) (b* (((mv error? tree rest) (rlp-parse-tree encoding)) ((when error?) (mv error? (rlp-tree-leaf nil))) ((when (consp rest)) (mv (rlp-error-extra-bytes rest) (rlp-tree-leaf nil)))) (mv nil tree))))

**Theorem: **

(defthm maybe-rlp-error-p-of-rlp-decodex-tree.error? (b* (((mv ?error? ?tree) (rlp-decodex-tree encoding))) (maybe-rlp-error-p error?)) :rule-classes :rewrite)

**Theorem: **

(defthm rlp-treep-of-rlp-decodex-tree.tree (b* (((mv ?error? ?tree) (rlp-decodex-tree encoding))) (rlp-treep tree)) :rule-classes :rewrite)

**Theorem: **

(defthm rlp-decodex-tree-of-byte-list-fix-encoding (equal (rlp-decodex-tree (byte-list-fix encoding)) (rlp-decodex-tree encoding)))

**Theorem: **

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

**Theorem: **

(defthm rlp-decodex-tree-of-rlp-encode-tree (b* (((mv e-error? encoding) (rlp-encode-tree tree)) ((mv d-error? tree1) (rlp-decodex-tree encoding))) (implies (not e-error?) (and (not d-error?) (equal tree1 (rlp-tree-fix tree))))))

**Theorem: **

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

**Theorem: **

(defthm rlp-tree-encoding-p-iff-rlp-decodex-tree-not-error (equal (rlp-tree-encoding-p encoding) (not (mv-nth 0 (rlp-decodex-tree encoding)))))

**Theorem: **

(defthm rlp-decode-tree-is-rlp-decodex-tree (and (iff (mv-nth 0 (rlp-decode-tree encoding)) (mv-nth 0 (rlp-decodex-tree encoding))) (equal (mv-nth 1 (rlp-decode-tree encoding)) (mv-nth 1 (rlp-decodex-tree encoding)))))