		Search-engine friendly clone of the ACL2 documentation.

Rlp-encoding

Rlp-bytes-encoding-p

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

This is analogous to rlp-tree-encoding-p.

The encoding of a byte array is also the encoding of the tree consisting of a single leaf with that byte array. The encoding of a leaf tree is also the encoding of the byte array in the tree.

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

Definitions and Theorems

Theorem: rlp-bytes-encoding-p-suff

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

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

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

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

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

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

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

Theorem: byte-listp-of-rlp-bytes-encoding-witness

(defthm byte-listp-of-rlp-bytes-encoding-witness
  (implies (rlp-bytes-encoding-p encoding)
           (byte-listp (rlp-bytes-encoding-witness encoding))))

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

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

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

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

Theorem: rlp-tree-encoding-p-when-rlp-bytes-encoding-p

(defthm rlp-tree-encoding-p-when-rlp-bytes-encoding-p
  (implies (rlp-bytes-encoding-p encoding)
           (rlp-tree-encoding-p encoding)))

Theorem: rlp-bytes-encoding-p-when-rlp-tree-encoding-p-and-leaf

(defthm rlp-bytes-encoding-p-when-rlp-tree-encoding-p-and-leaf
  (implies (and (rlp-tree-encoding-p encoding)
                (rlp-tree-case (rlp-tree-encoding-witness encoding)
                               :leaf))
           (rlp-bytes-encoding-p encoding)))