4 posts tagged with "data_encoding"

Tezos uses the json-data-encoding library throughout the protocol to serialize data for use in RPC, writing to disk or placing in a block. RPC is a synchronous operation. Consequently, it is paramount to verify the correctness of code as well as the logical equivalence and semantics of performance-enhanced procedures to proven ones.

This library has been subject to stack overflows, as seen in issues like this. We will translate and verify this library to validate its logic and simplify debugging these issues.

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.

In the protocol of Tezos, we define the serialization of values using the data-encoding library. We make these definitions by hand to be able to audit the code and fine-tune the serialization.

The serialization and deserialization functions must be inverse. Missing this property can lead to bugs or exploits. We present a solution to formally verify the definition of data-encodings in Coq. As a result, we increase our confidence in the correctness of our encodings. We even found a mistake in a development code and fixed it before release. This mistake was found by TriliTech.