• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • 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
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • 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)