		Search-engine friendly clone of the ACL2 documentation.

Rlp-decoding-declarative

Rlp-decode-tree

RLP decoding of a tree.

Signature
(rlp-decode-tree encoding) → (mv error? tree)
Arguments: encoding — Guard (byte-listp encoding).
Returns: error? — Type (booleanp error?).; tree — Type (rlp-treep tree).

If the byte array encodes some tree, we return that tree, along with a nil error flag. Otherwise, we return a t error flag, and an irrelevant tree as second result.

This is a declarative, non-executable definition, which says that decoding is the inverse of encoding. This is the intention of [YP:B], which only specifies encoding, leaving decoding implicit.

More precisely, we define decoding as the right inverse of encoding (with respect to byte arrays that are valid encodings of trees), as explicated by the theorem rlp-encode-tree-of-rlp-decode-tree.

We use the injectivity of rlp-encode-tree, proved here, to prove that decoding is also the left inverse of encoding (with respect to encodable trees), as the theorem rlp-decode-tree-of-rlp-encode-tree. Roughly speaking, the proof goes like this: (1) instantiate the right identity theorem, namely (encode (decode y)) = y, with y replaced with (encode x), obtaining (encode (decode (encode x))) = (encode x); (2) use the injectivity of encode to obtain (decode (encode x)) = x. Note that we disable both the right inverse theorem and the definition of rlp-decode-tree, which would otherwise sabotage this proof.

The decoding code in [Wiki:RLP] provides a reference implementation. Note that it is considerably more complicated than the encoding code. Our high-level specification of decoding is simpler.

Definitions and Theorems

Function: rlp-decode-tree

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

Theorem: booleanp-of-rlp-decode-tree.error?

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

Theorem: rlp-treep-of-rlp-decode-tree.tree

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

Theorem: rlp-encode-tree-of-rlp-decode-tree

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

Theorem: rlp-decode-tree-of-rlp-encode-tree

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

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

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

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

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