A formalization of the primitives used by the protocol, as taken from the tezos/tezos node. These primitives include for example:
- elements taken from the standard library of OCaml (numbers, lists, maps, ...);
- cryptographic primitives;
- serialization primitives.
We write the formalization of the environment mostly by hand. We verify that it corresponds to what is in the implementation. We do so by checking that the signatures of the definitions are compatible with what coq-of-ocaml generates in src/Proto_alpha/Environment.v.