Skip to main content

Specify

Gitlab

For most of the code, there is not a single rule to decide what should be verified. So one should read the code and comments in the OCaml version (especially .mli files) to understand what needs to be verified. There are also the unit-tests, located in https://gitlab.com/tezos/tezos/-/tree/master/src/proto_alpha/lib_protocol/test to help find the specification.

As standard properties to verify there are:

  • The validity properties, showing that a function or value respects a Valid.t predicate (safety). We suffix these properties by _is_valid.
  • The equality properties, where we show that under certain conditions (typically success conditions) a function behaves as a simpler expression (soundness). We suffix these properties by _eq.
  • Inverse functions. If we have two functions to_string and of_string, very probably of_string (to_string x) = Some x. We name this property of_string_to_string.