Verify the data-encoding library

This is a follow-up to https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml/-/issues/67

The goal is to verify the specification we wrote in the previous task.