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