		Search-engine friendly clone of the ACL2 documentation.

Rlp-decoding-executable

Rlp-decodex-bytes

Executable RLP decoding of a byte array.

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

This has the same form as the alternative definition rule of rlp-decode-bytes in terms of rlp-decode-tree. As such, it is immediate to prove equal (i.e. correct with respect) to rlp-decode-bytes, using the correctness theorem of rlp-decodex-tree.

Definitions and Theorems

Function: rlp-decodex-bytes

(defun rlp-decodex-bytes (encoding)
  (declare (xargs :guard (byte-listp encoding)))
  (let ((__function__ 'rlp-decodex-bytes))
    (declare (ignorable __function__))
    (b* (((mv error? tree)
          (rlp-decodex-tree encoding))
         ((when error?) (mv error? nil))
         ((unless (rlp-tree-case tree :leaf))
          (mv (rlp-error-branch-tree (list (car encoding)))
              nil))
         (bytes (rlp-tree-leaf->bytes tree)))
      (mv nil bytes))))

Theorem: maybe-rlp-error-p-of-rlp-decodex-bytes.error?

(defthm maybe-rlp-error-p-of-rlp-decodex-bytes.error?
  (b* (((mv ?error? ?bytes)
        (rlp-decodex-bytes encoding)))
    (maybe-rlp-error-p error?))
  :rule-classes :rewrite)

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

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

Theorem: rlp-decode-bytes-is-rlp-decodex-bytes

(defthm rlp-decode-bytes-is-rlp-decodex-bytes
  (and (iff (mv-nth 0 (rlp-decode-bytes encoding))
            (mv-nth 0 (rlp-decodex-bytes encoding)))
       (equal (mv-nth 1 (rlp-decode-bytes encoding))
              (mv-nth 1 (rlp-decodex-bytes encoding)))))

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

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

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

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