Skip to main content

Naming

Gitlab

Valid predicate​

To express invariants we define a Valid.t predicate. For example, for the Tez values there is:

Module Valid.
  Definition t (tz : Tez_repr.t) : Prop :=
    0 <= tz <= Int64.max_int.
End Valid.

We express the properties in Prop rather than in bool and prefer to use operators in Prop as much as possible as this is more direct for the proofs.

Preserving invariants​

To show that a certain value respects an invariant, or that a function returns values with an invariant, we state a lemma named value_or_function_name_is_valid.

  • An example with functions:
Lemma op_minusquestion_is_valid : forall {t1 t2 : Tez_repr.tez},
  Valid.t t1 ->
  Valid.t t2 ->
  match Tez_repr.op_minusquestion t1 t2 with
  | Pervasives.Ok t => Valid.t t
  | Pervasives.Error _ => False
  end.
  • An example with values:
Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Tez_repr.encoding.

Equalities and simplifications​

To show that an expression is equal to another simpler expression given the right pre-condition (typically in the success case), we use a lemma named function_name_eq. For example:

Lemma of_int_opt_eq (i : int) :
  Strictly_valid.t i ->
  Saturation_repr.of_int_opt i = Some i.

Inverses​

To show that two functions are inverse, we concatenate their names to get a lemma name:

Lemma of_path_to_path v :
  P.(Path_encoding.S.of_path) (P.(Path_encoding.S.to_path) v []) =
  Some v.