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.
An issue with recursive functions is that they may raise a stack-overflow error if the number of recursive calls is too high. To avoid these errors, many functions in Tezos are written in tail-recursive style. This style is usually harder to read and this could lead to mistakes in the code. We show in this post how we verify a tail-recursive function by comparing it to its naive non tail-recursive version.
Welcome to the blog of the project "Coq Tezos of OCaml". Here we will report regularly on what we are doing. Our main aims with this project are:
- to improve the quality of the formalization of Tezos in Coq, and
- to write as many formal proofs as possible to prevent critical bugs.