Skip to main content

Data-encoding

Gitlab

  • The data-encodings are there to serialize values to binary or JSON format. They are used for API calls or storage into the database.
  • The source of the library is https://gitlab.com/nomadic-labs/data-encoding/-/blob/master/src/data_encoding.mli
  • We want to check that we have bijections between the values and the binary/JSON format. This is necessary to make sure that:
    • We read what we have written in the database.
    • There exists a unique binary representation for each value, to use for equality tests or hashing.
  • We verify the encodings on a certain domain a -> Prop of a given set a.
  • Since this library is axiomatized, we do not get back to the definition of Data_encoding.Valid.t but use axioms about the primitives. So using constructor to verify an encoding is a bad idea.
  • The tactic Data_encoding.Valid.data_encoding_auto solves most of the cases apart from properties over the domain. It should always be used.
  • The hint database Data_encoding_db contains all the hints about the encodings and should be updated after each encoding proof with:
#[global] Hint Resolve unsigned_encoding_is_valid : Data_encoding_db.
  • If a hint is not called, this is probably because its file is not in the Require list of files, as the hints must be required.