		Search-engine friendly clone of the ACL2 documentation.

Transactions

Rlp-decode-transaction

RLP decoding of a transaction.

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

If the byte array encodes some transaction, we return that transaction, along with a nil error flag. Otherwise, we return a t error flag, and an irrelevant transaction 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:4.2], 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 transactions), as explicated by the theorem rlp-encode-transaction-of-rlp-decode-transaction.

To prove that decoding is also the left inverse of encoding (with respect to encodable transactions), we need to prove the injectivity of encoding first; this is future work.

Definitions and Theorems

Function: rlp-decode-transaction

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

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

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

Theorem: transactionp-of-rlp-decode-transaction.transaction

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

Theorem: rlp-encode-transaction-of-rlp-decode-transaction

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

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

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

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

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