# Rlp-decoding-executable

Executable definitions of RLP decoding.

We provide executable definitions of RLP decoding for
trees, byte arrays, and scalars.
We prove the correctness of these executable definitions with respect to
the declarative
definitions.

We start with an executable RLP parser for trees
that accepts extra bytes after the encoding
and that returns those extra bytes as additional result;
this is a natural approach for this kind of recursive parsing.
We prove that this parser is both left and right inverse,
modulo the extra bytes,
of the RLP tree encoder.

Then we define executable RLP decoders for trees, bytes, and scalars
based on the parser.
These decoders return an error
if there are extra bytes after the encodings.
We prove these decoders equivalent to the
declaratively defined
ones,
using the left and right inverse properties of the parser.

While the declaratively defined decoders return a boolean error result,
which therefore conveys a single kind of error,
the executable parser and decoders return more detailed error information.
Thus, the equivalence relation for the error result
of the declaratively defined decoders and of the executable ones
is `iff` instead of `equal`; see the theorems.

### Subtopics

- Rlp-error
- Possible errors when parsing or decoding RLP encodings.
- Rlp-parse-tree
- Parse the RLP encoding of a tree,
returning any extra bytes for further parsing.
- Rlp-decodex-tree
- Executable RLP decoding of a tree.
- Maybe-rlp-error
- Type of the error result of the parsing and decoding functions
(nil if no error).
- Rlp-decodex-bytes
- Executable RLP decoding of a byte array.
- Rlp-decodex-scalar
- Executable RLP decoding of a scalar.