Integer arithmetic verification

One of the points of concern in the Tezos code is integer overflows. To ensure that no overflow occurs, the development team created abstractions over the native OCaml integers. This makes it possible to check if an overflow happened and to return an error if that is the case.

But how to be sure that such abstractions are correct? In this post, we will explain how integer arithmetic can be verified using Coq.

As it is known, OCaml native integers are bounded by some bit width. We have int with 63 bits, int32 and int64 with 32 and 64 bits respectively. When an operation exceeds its width capacity, we say that an overflow occurred.

In Coq this is another story, we have infinite integers, so the first thing we need to do is to define the modular arithmetic found in OCaml. We will use the int64 as an example, but the same reasoning applies to int and int32, we just have to adjust the boundaries.

To define an OCaml integer we use Z and define a Valid.t type which encloses a value between OCaml Int64.max_int and Int64.min_int, here is it:

Module Valid.
  Defintion t (x : Z) : Prop := Int64.min_int <= x <= Int64.max_int.
End Valid.

The second thing is to define the operations, we need to ensure that operations are closed under Valid.t, that they respect the bounds Int64.min_int and Int64.max_int. To do this, we define a normalize_int64 function that uses Z.modulo to ensure that the results are kept between the bounds. Here is it:

Definition two_pow_63 : Z := 9223372036854775808.
Definition two_pow_64 : Z := 18446744073709551616.

Definition normalize_int64 (n : Z) : int64 :=
  Z.modulo (n + two_pow_63) two_pow_64 - two_pow_63.

Now we are ready to define the operations. We define them as the same operations in Z, but surrounded by normalize_int64

Definition add (a : t) (b : t) : t := normalize_int64 (Z.add a b).
Definition sub (a : t) (b : t) : t := normalize_int64 (Z.sub a b).
Definition mul (a : t) (b : t) : t := normalize_int64 (Z.mul a b).
Definition div (a : t) (b : t) : t := normalize_int64 (Z.div a b).

At this point we have our definitions, now we need to ensure that they are valid and check for some properties. There are two main properties that we want to check.

First, we want to ensure that the operations are closed under Valid.t, in English, this would be something like "The sum of two int64 is always a valid int64".

We verify the four operations as follows:

Lemma int64_add_is_valid a b : Valid.t (a +i64 b). lia. Qed.
Lemma int64_mul_is_valid a b : Valid.t (a *i64 b). lia. Qed.
Lemma int64_div_is_valid a b : Valid.t (a /i64 b). lia. Qed.
Lemma int64_sub_is_valid a b : Valid.t (a -i64 b). lia. Qed.

Here, a +i64 b is a Coq notation to represent OCaml's Int64.(a + b).

At this point, we are sure that our definition is valid, that for any two int64 we always yield a valid int64. But this is not enough, if we define all the operations as 0, for example, this specification would still be satisfied.

To fix this, we want to verify that the operation we defined is equivalent to the same operation in Z. I mean, we want to ensure that the sum is equal to the sum in Z, the subtraction is equal to the subtraction in Z, so on and so forth.

We verify the addition as follows:

Lemma add_eq : forall a b,
  Valid.t (a +Z b) -> a +i64 b = a +Z b.
Proof.
  lia.
Qed.

And we do the same for all the three remaining operations.

At this point, we verified that our definition of OCaml's integer arithmetic is correct, but we have not verified any Tezos code yet. Tezos abstractions are built over OCaml integers, so knowing that our definition of OCaml integers is fine we can proceed to verify a higher abstraction. The Tez_repr module is used as an example here.

Tez_repr.t is a wrapper over an OCaml's int64. The procedure for the verification follows the same reasoning used before. We derive a domain over where a Tez_repr.t is valid, in this case, it is defined as a non-negative int64.

Module Valid.
  Definition t (x : int64) : Prop := 0 <= x <= Int64.max_int
End Valid.t

Now comes the cool part, the definition of the operations are translated from OCaml code using coq-of-ocaml. So we are left to verify that each operation is valid, and that, under the right domain, they are equivalent to the same operation in Z.

Here is an example for the addition of two Tez_repr.t,

(** On success, addition is closed under Tez_rept.Valid.t *)
Lemma op_plusquestion_is_valid : forall {t1 t2 : Tez_repr.t},
    Valid.t t1 ->
    Valid.t t2 ->
    match Tez_repr.op_plusquestion t1 t2 with
    | Pervasives.Ok t => Valid.t t
    | Pervasives.Error _ => True
    end.
Proof.
  intros; unfold Tez_repr.op_plusquestion.
  destruct_all Tez_repr.t.
  destruct (_ <i64 _) eqn:?; simpl; lia.
Qed.

(** On success, Tez_repr.op_plusquestion equals to addition in Z *)
Lemma op_plusquestion_eq : forall {t t1 t2 : int64},
  Valid.t (Tez_repr.Tez_tag t1) ->
  Valid.t (Tez_repr.Tez_tag t2) ->
  match Tez_repr.op_plusquestion 
    (Tez_repr.Tez_tag t1) 
    (Tez_repr.Tez_tag t2) with
  | Pervasives.Ok (Tez_repr.Tez_tag t) => t = t1 +Z t2
  | Pervasives.Error _ => True
  end.
Proof.
  Utils.tezos_z_autounfold. simpl.
  intros t t1 t2 H1 H2.
  destruct (_ <? _) eqn:H_lt; hfcrush.
Qed.

So with these two proofs, we verified that the sum of two Tez_repr.t is always a non-negative int64, and, if no overflow occurs, the sum of two Tez_rept.t will be just the same as the sum of two numbers in Z, we just have a more restricted domain than Z.