# Rlp-decodability

Proofs that RLP encodings can be decoded.

We prove that the encoding functions for byte arrays, trees, and scalars
are injective over the encodable byte arrays, trees, and scalars.
This means that each valid encoding corresponds to exactly one entity,
i.e. that encoding is reversible, i.e. that decoding is possible.
If an encoding function were not injective over encodable entities,
then two or more distinct entities would be encoded identically.

We also prove the stronger property
that no valid encoding is a strict prefix of another valid encoding.
This means that it is possible to unambiguously decode valid encodings
even when these encodings are not well-delimited segments of bytes,
but they are read from a stream of bytes (e.g. over a network connection).
If some valid encoding were a strict prefix of another valid encoding,
then after reading the former we would not know whether we are done
or whether we should continue reading the longer encoding.

### Subtopics

- Rlp-encode-trees-injectivity-proof
- Injectivity of
`rlp-encode-tree`
and `rlp-encode-tree-list`,
over the encodable trees and lists thereof. - Rlp-encode-bytes-injectivity-proof
- Injectivity of
`rlp-encode-bytes`,
over the encodable byte arrays. - Rlp-encode-bytes-prefix-unambiguity-proof
- Property that no valid RLP byte array encoding
is a strict prefix of another one.
- Rlp-encode-tree-prefix-unambiguity-proof
- Property that no valid RLP tree encoding
is a strict prefix of another one.
- Rlp-encode-scalar-injectivity-proof
- Injectivity of
`rlp-encode-scalar`,
over the encodable scalars. - Rlp-encode-scalar-prefix-unambiguity-proof
- Property that no valid RLP scalar encoding
is a strict prefix of another one.