		Search-engine friendly clone of the ACL2 documentation.

Rlp-encoding

Rlp-tree-encoding-p

Check if a byte array is an RLP encoding of a tree.

This is a declarative, non-executable definition, which essentially characterizes the image of rlp-encode-tree (over trees that can be encoded, i.e. such that rlp-encode-tree returns a nil error flag).

By definition, the witness function is right inverse of the encoding function, over the valid encodings.

Definitions and Theorems

Theorem: rlp-tree-encoding-p-suff

(defthm rlp-tree-encoding-p-suff
  (implies (and (rlp-treep tree)
                (b* (((mv error? encoding1)
                      (rlp-encode-tree tree)))
                  (and (not error?)
                       (equal encoding1 (byte-list-fix encoding)))))
           (rlp-tree-encoding-p encoding)))

Theorem: booleanp-of-rlp-tree-encoding-p

(defthm booleanp-of-rlp-tree-encoding-p
  (b* ((yes/no (rlp-tree-encoding-p encoding)))
    (booleanp yes/no))
  :rule-classes :rewrite)

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

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

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

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

Theorem: rlp-treep-of-rlp-tree-encoding-witness

(defthm rlp-treep-of-rlp-tree-encoding-witness
  (implies (rlp-tree-encoding-p encoding)
           (rlp-treep (rlp-tree-encoding-witness encoding))))

Theorem: rlp-encode-tree-of-rlp-tree-encoding-witness

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

Theorem: rlp-tree-encoding-p-of-rlp-tree-encode-when-no-error

(defthm rlp-tree-encoding-p-of-rlp-tree-encode-when-no-error
  (implies (not (mv-nth 0 (rlp-encode-tree tree)))
           (rlp-tree-encoding-p (mv-nth 1 (rlp-encode-tree tree)))))