• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • Soft
      • C
      • Bv
      • Imp-language
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
        • Mmp-trees
        • Semaphore
        • Database
        • Cryptography
        • Rlp
          • Rlp-tree
          • Rlp-decoding-executable
            • Rlp-error
            • Rlp-parse-tree
            • Rlp-decodex-tree
            • Maybe-rlp-error
            • Rlp-decodex-bytes
            • Rlp-decodex-scalar
          • Rlp-decodability
          • Rlp-encoding
          • Rlp-decoding-declarative
          • Rlp-big-endian-representations
        • Transactions
        • Hex-prefix
        • Basics
        • Addresses
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Lists-light
      • Axe
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• 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)