Skip to main content

Conventions

Gitlab

File names​

We name our files as the files generated by coq-of-ocaml (which are themselves named like the OCaml files, and capitalized to follow the Coq convention). We have two folders along the code:

  • Proofs/ for our proof files (most of our files)
  • Simulations/ for our definition files when we reason by simulation (typically on the storage and the Michelson interpreter)

Style​

  • Line length: 80 characters (no more than 80 characters per line).

  • Indentation: double spaces

  • Spaces before and after colons :.

  • Comments

    • amount of comments we think it is always good to have more comments than less
    • inlined comments for the developers should be placed in (* ... *), example: comments1
    • documentation (typically) at the start of each lemma should be placed in (** ... *), example: comments2
    • documentation title, can be used to separate sections in a long file should be placed in (** ** ... *), example: comments3

  • Proof keyword. We use the Proof keyword (in transition, old proofs do not have the Proof keyword).

  • Require/Import

    • We prefer to use Require rather than Require Import when it is not too heavy, and explicitly prefix the names with the corresponding module.
    • It is better to write Require list in alphabetical order, especially if the list is long.
    • Here is a typical list of "requires":
(* Default coq-of-ocaml requires *)
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

(* The environment file and the file we are verifying *)
Require Import TezosOfOCaml.Environment.V5.
Require TezosOfOCaml.Proto_J.Operation_repr.

(* A few proof files on which we depend, either for the environment
   or the protocol code. These requires are by alphabetical order. *)
Require TezosOfOCaml.Proto_J.Environment.Proofs.Ed25519.
Require TezosOfOCaml.Proto_J.Environment.Proofs.Operation.
Require TezosOfOCaml.Proto_J.Proofs.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_J.Proofs.Block_payload_hash.
  • -/+/* vs { and }: we prefer
(* correct style *)
destruct x. 
{ proof; here; for; goal; one }
{ proof; here; for; goal; two }

instead of

(* wrong style *)
destruct x. 
- proof; here; for; goal; one.
- proof; here; for; goal; two.