|
|
|---|
|
|
|
|---|
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.