• 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-decodability
            • Rlp-encoding
            • Rlp-decoding-declarative
              • Rlp-decode-bytes
              • Rlp-decode-tree
              • Rlp-decode-scalar
            • 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

Rlp-decoding-declarative

Declarative definitions of RLP decoding.

We specify RLP decoding via functions from byte arrays to byte arrays, trees, and scalars. These functions are declaratively defined as inverses of the RLP encoding functions. They are not executable.

Note that [YP:B] only defines RLP encoding explicitly, not RLP decoding. Clearly, the intention is that decoding is the inverse of encoding: this is the implicit specification of decoding in [YP:B].

Subtopics

Rlp-decode-bytes
RLP decoding of a byte array.
Rlp-decode-tree
RLP decoding of a tree.
Rlp-decode-scalar
RLP decoding of a scalar.