• 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-error-fix
                • Rlp-error-p
                • Rlp-error-case
                • Rlp-error-equiv
                • Rlp-error-count
                • Rlp-error-fewer-bytes-than-short-length
                • Rlp-error-fewer-bytes-than-long-length
                • Rlp-error-fewer-bytes-than-length-of-length
                • Rlp-error-kind
                • Rlp-error-subtree
                • Rlp-error-non-optimal-short-length
                • Rlp-error-non-optimal-long-length
                • Rlp-error-leading-zeros-in-scalar
                • Rlp-error-leading-zeros-in-long-length
                • Rlp-error-extra-bytes
                • Rlp-error-branch-tree
                • Rlp-error-no-bytes
              • 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-error

Possible errors when parsing or decoding RLP encodings.

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types
:no-bytes → rlp-error-no-bytes
:fewer-bytes-than-short-length → rlp-error-fewer-bytes-than-short-length
:fewer-bytes-than-length-of-length → rlp-error-fewer-bytes-than-length-of-length
:fewer-bytes-than-long-length → rlp-error-fewer-bytes-than-long-length
:leading-zeros-in-long-length → rlp-error-leading-zeros-in-long-length
:non-optimal-short-length → rlp-error-non-optimal-short-length
:non-optimal-long-length → rlp-error-non-optimal-long-length
:subtree → rlp-error-subtree
:extra-bytes → rlp-error-extra-bytes
:branch-tree → rlp-error-branch-tree
:leading-zeros-in-scalar → rlp-error-leading-zeros-in-scalar

These values provide information about the reason why an RLP encoding is erroneous and cannot be parsed or decoded.

The :no-bytes error occurs when starting to parse or decode a (sub)tree but no bytes are available.

The :fewer-bytes-than-... errors occur when, after successfully reading a length, there are fewer bytes available than the required length. The length may be a short length (i.e. below 56, part of the first byte), the length of a long length (i.e. between 1 and 8, part of the first byte), or a long length (i.e. a big endian length). In these errors, the fragment field consists of the first byte, possibly followed by the big endian length bytes as applicable.

The :leading-zeros-in-long-length errors occurs when a long length has leading zeros. See the discussion in rlp-parse-tree. The fragment field consists of the first byte followed by the big endian length.

The :non-optimal-... errors occur when the encoding is longer than it must be. See the discussion in rlp-parse-tree. The fragment field consists of the first byte, possibly followed by the big endian length bytes as applicable.

Since parsing and decoding are recursive, errors from subtree encodings must be propagated upward, because the supertree encodings are therefore erroneous. The :error-in-subtree errors propagate and wrap the error from a subtree. Note that this makes the definition of this fixtype of errors recursive.

The :extra-bytes errors occur only in decoding, not in parsing. Parsing always returns any remaining bytes as a result, while decoding requires the input bytes to have the right length. The bytes field of these errors consists of the extra bytes.

The :branch-tree errors occur when attempting to decode a byte array (i.e. a leaf tree) results in a branching tree instead. The fragment field contains the starting byte of the encoding.

The :leading-zeros-in-scalar errors occur when attempting to decode a scalar results in a byte array with leading zeros.

Subtopics

Rlp-error-fix
Fixing function for rlp-error structures.
Rlp-error-p
Recognizer for rlp-error structures.
Rlp-error-case
Case macro for the different kinds of rlp-error structures.
Rlp-error-equiv
Basic equivalence relation for rlp-error structures.
Rlp-error-count
Measure for recurring over rlp-error structures.
Rlp-error-fewer-bytes-than-short-length
Rlp-error-fewer-bytes-than-long-length
Rlp-error-fewer-bytes-than-length-of-length
Rlp-error-kind
Get the kind (tag) of a rlp-error structure.
Rlp-error-subtree
Rlp-error-non-optimal-short-length
Rlp-error-non-optimal-long-length
Rlp-error-leading-zeros-in-scalar
Rlp-error-leading-zeros-in-long-length
Rlp-error-extra-bytes
Rlp-error-branch-tree
Rlp-error-no-bytes