		Search-engine friendly clone of the ACL2 documentation.

Rlp-decoding-executable

Rlp-decodex-tree

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 x in the name of this function stands for `executable', in contrast with the declaratively specified rlp-decode-tree.

The left inverse theorem rlp-decodex-tree-of-rlp-encode-tree readily follows from rlp-parse-tree-of-rlp-encode-tree.

The right inverse theorem rlp-encode-tree-of-rlp-decodex-tree easily follows from rlp-encode-tree-of-rlp-parse-tree, but the latter theorem involves append and so we use it with a :use hint.

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, encode /= error ==> decode o encode /= error), with the argument instantiated to the rlp-tree-encoding-witness (i.e. encode o witness /= error ==> decode o encode o witness /= error). The rlp-tree-encoding-p hypothesis establishes the antecedent, and the right inverse property of the witness reduces the consequent to just decode /= error.

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.

Definitions and Theorems

Function: rlp-decodex-tree

(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: maybe-rlp-error-p-of-rlp-decodex-tree.error?

(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: rlp-treep-of-rlp-decodex-tree.tree

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

Theorem: rlp-decodex-tree-of-byte-list-fix-encoding

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

Theorem: rlp-decodex-tree-byte-list-equiv-congruence-on-encoding

(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: rlp-decodex-tree-of-rlp-encode-tree

(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: rlp-encode-tree-of-rlp-decodex-tree

(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: rlp-tree-encoding-p-iff-rlp-decodex-tree-not-error

(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: rlp-decode-tree-is-rlp-decodex-tree

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