This post is a continuation of the previous blog post on proof automation for the data_encoding proofs.
data_encoding is a library used in the Tezos codebase to define binary and JSON encodings, by using some primitives and then combining these primitives with combinators.
The data_encoding library is used throughout the Tezos codebase for various serializing/deserializing tasks. Because of this, in our effort to formally verify the protocol, there are many proofs involving encoding.
Simply speaking, data_encoding has a series of primitives for encoding/decoding scalar
data types and combinators for non-scalar data types, combinators work by
combining primitives together with functions and letting users compose smaller
encodings into bigger ones.
Having axioms and lemmas for primitives and combinators enable us to verify the encodings, but in practice, these proofs can be very mechanical.