Skip to main content

2 posts tagged with "automation"

View All Tags

ยท 2 min read
Daniel Hilst

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.