		Search-engine friendly clone of the ACL2 documentation.

Rlp-decoding-declarative

Rlp-decode-bytes

RLP decoding of a byte array.

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

This is analogous to rlp-decode-tree. If the returned error flag is t, we return nil as the (irrelevant) second result.

As proved in rlp-bytes-encoding-p, the encoding of a byte array is also the encoding of the leaf tree containing the byte array. Because rlp-encode-tree is injective, the two witnesses (decoders) rlp-bytes-encoding-witness and rlp-tree-encoding-witness are related accordingly. Roughly speaking, the proof goes like this: (1) start with the fact that rlp-bytes-encoding-witness is right inverse of rlp-encode-bytes, i.e. rlp-encode-bytes o rlp-bytes-encoding-witness = id, where o is function composition and id is the identity function; (2) use the alternative definition of rlp-encode-bytes in terms of rlp-encode-tree to obtain rlp-encode-tree o rlp-tree-leaf o rlp-bytes-encoding-witness = id; (3) use the fact that rlp-tree-encoding-witness is right inverse of rlp-encode-tree, i.e. rlp-encode-tree o rlp-tree-encoding-witness = id; (4) from (2) and (3) and the injectivity of rlp-encode-tree, derive rlp-tree-encoding-witness = rlp-tree-leaf o rlp-bytes-encoding-witness. It is generally the case that if an injective function has two right inverses, they are equal.

This relationship among these witnesses lets us prove a theorem that provides an alternative definition of rlp-decode-bytes in terms of rlp-decode-tree.

Definitions and Theorems

Function: rlp-decode-bytes

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

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

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

Theorem: byte-listp-of-rlp-decode-bytes.bytes

(defthm byte-listp-of-rlp-decode-bytes.bytes
  (b* (((mv ?error? ?bytes)
        (rlp-decode-bytes encoding)))
    (byte-listp bytes))
  :rule-classes :rewrite)

Theorem: rlp-encode-bytes-of-rlp-decode-bytes

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

Theorem: rlp-decode-bytes-of-rlp-encode-bytes

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

Theorem: rlp-tree-encoding-witness-as-rlp-bytes-encoding-witness

(defthm rlp-tree-encoding-witness-as-rlp-bytes-encoding-witness
 (implies
     (rlp-bytes-encoding-p encoding)
     (equal (rlp-tree-encoding-witness encoding)
            (rlp-tree-leaf (rlp-bytes-encoding-witness encoding)))))

Theorem: rlp-bytes-encoding-witness-as-rlp-tree-encoding-witness

(defthm rlp-bytes-encoding-witness-as-rlp-tree-encoding-witness
 (implies
  (rlp-bytes-encoding-p encoding)
  (equal
      (rlp-bytes-encoding-witness encoding)
      (rlp-tree-leaf->bytes (rlp-tree-encoding-witness encoding)))))

Theorem: rlp-decode-bytes-alt-def

(defthm rlp-decode-bytes-alt-def
  (equal (rlp-decode-bytes encoding)
         (b* (((mv error? tree)
               (rlp-decode-tree encoding))
              ((when error?) (mv t nil))
              ((unless (rlp-tree-case tree :leaf))
               (mv t nil))
              (bytes (rlp-tree-leaf->bytes tree)))
           (mv nil bytes))))

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

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

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

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