Formal verification of property based tests

Property based tests are a way to find bugs in the code by running a boolean function (representing an expected property) on randomly generated inputs. In this blog post, we show how we translate these tests to corresponding Coq theorems. Once we have a formal representation, we prove them correct on any inputs. Thanks to this technique, we can:

• have a bridge between the specification given by the tests and the specification in Coq;
• make sure that the properties verified in the tests are true with a mathematical degree of certainty.

We have done this work with students from the University of Groningen:

• Joris Peters https://github.com/jorisptrs
• Rienk Bergsma https://github.com/Dragonflew17
• Tait van Strien https://gitlab.com/7A1T
• Tino Alferink https://gitlab.com/Tinoalfie
• Tudor Roscoiu https://gitlab.com/tudoroscoiu

Here is a short presentation that we gave at a meeting with developers of Tezos: Property based tests with Coq. To see an example of a formally verified test, you can look at:

• Test_sc_rollup_tick_repr.v: the tests for Sc_rollup_tick_repr.v translated into Coq together with their proofs;
• test_sc_rollup_tick_repr.ml: the corresponding test file in OCaml.

Example in OCaml

As an example, we take the file sc_rollup_tick_repr.ml defining a notion of "tick":

include Z

let initial = zero

let next = succ

let pp = pp_print

let encoding = Data_encoding.n

let distance tick1 tick2 = Z.abs (Z.sub tick1 tick2)

(* ... other definitions ... *)

with its associated property based tests in test_sc_rollup_tick_repr.ml. An example of test is:

(** A generator for ticks *)
let tick : Tick.t QCheck.arbitrary =
  QCheck.(
    Gen.(make (Option.value ~default:Tick.initial <$> map Tick.of_int nat)))

let test_distance_triangle_inequality =
  QCheck.Test.make
    ~name:"distance is a distance (triangle inequality)"
    (triple tick tick tick)
  @@ fun (x, y, z) ->
  Tick.(Z.(geq (distance x y + distance y z) (distance x z)))

This checks that, for all x, y, and z, the following property holds:

distance x y + distance y z >= distance x z

We use the OCaml framework QCheck to write these property based tests. The value tick is a generator, that is to say a function generating random values of a tick. We create this generator using combinators:

• nat generates non-negative int values;
• map Tick.of_int nat applies to these values the conversion Tick.of_int from int to ticks;
• Option.value ~default:Tick.initial <$> map Tick.of_int nat returns a default value Tick.initial in case Tick.of_int returns None.

Translation in Coq

We run coq-of-ocaml to translate the code and the tests to Coq. The generated files are the followings:

• Sc_rollup_tick_repr.v for the code;
• Test_sc_rollup_tick_repr.v for the tests.

For the test files, we do some manual transformation in addition to what coq-of-ocaml generates to fix some missing library imports. However, given more work on the translation pipeline, these manual transformations should not be needed.

To represent property based tests as Coq theorems, we replace the randomly generated values with "forall" quantifiers. We restrict these "forall" quantifiers to the domain of values that can be generated. We do this transformation for the combinators of the generators so that the tests look the same when expressed in Coq theorems:

Definition tick : QCheck.arbitrary Sc_rollup_tick_repr.t :=
  QCheck.make None None None None None
    (QCheck.Gen.op_ltdollargt
      (fun x_1 =>
        Option.value_value x_1
          Sc_rollup_tick_repr.initial)
      (QCheck.Gen.map
        Sc_rollup_tick_repr.of_int
        QCheck.Gen.nat)).

Definition test_distance_triangle_inequality : QCheck.Test.t :=
  QCheck.Test.make None None None None None None
    (Some "distance is a distance (triangle inequality)")
    (QCheck.triple_value tick tick tick)
    (fun (function_parameter :
      Sc_rollup_tick_repr.t *
        Sc_rollup_tick_repr.t *
        Sc_rollup_tick_repr.t) =>
      let '(x_value, y_value, z_value) := function_parameter in
      Z.geq
        (Z.add
          (Sc_rollup_tick_repr.distance x_value y_value)
          (Sc_rollup_tick_repr.distance y_value z_value))
        (Sc_rollup_tick_repr.distance x_value z_value)).

Combinators

The differences with the original OCaml code are mostly syntactical. However, the type QCheck.arbitrary for the generators is now:

Definition arbitrary (a : Set) : Type := a -> Prop.

so a predicate over a type a. The definition tick is a predicate over values of type Sc_rollup_tick_repr.t, corresponding to the values that can be generated by the OCaml generator tick. As an example, here is how we define the combinator QCheck.Gen.map:

Definition map {a b : Set} (f : a -> b)
  (gen : arbitrary a) : arbitrary b :=
  fun v =>
  ∃ v', gen v' ∧ f v' = v.

It says that a value can be generated by a map if there exists a predecessor for the function f that we can generate using gen. You can find the definition of all the combinators we are using in QCheck.v.

Theorem

In Coq, the definition test_distance_triangle_inequality is of type QCheck.Test.t that is a synonym of Prop. We define the function make to create a test as:

Definition make {a : Set}
  (_ _ _ _ _ _ _ : option string)
  (generator : QCheck.arbitrary a)
  (test_function : a -> bool) : t :=
  forall x,
    generator x ->
    test_function x = true.

All the _ parameters represent optional parameters in OCaml and are here for typing reasons. The important part is that we check:

forall x,
  generator x ->
  test_function x = true.

that is to say that the property function always returns true when applied to a value in the domain of the generator. We state the theorem for the validity of our test as follows:

Lemma test_distance_triangle_inequality_proof :
  test_distance_triangle_inequality.

Proof

We generally proceed in two steps:

1. We state in a clear way what is the domain of the generators:

Lemma tick_is_non_negative_int (n : Z.t) :
  tick n ->
  Pervasives.Int.Valid.non_negative n.
Proof.
  (* ... *)
Qed.

This states that: "the generator tick produces non-negative integers in the range of values of the type int".

2. We write the proof using the domain of the generators. We follow the structure of the property test showing that the result must be true in all possible branches.

Here is the proof for the lemma test_distance_triangle_inequality_proof. Note that we did not need to use the domain of the generator in this particular example:

Lemma test_distance_triangle_inequality_proof :
  test_distance_triangle_inequality.
Proof.
  unfold test_distance_triangle_inequality, QCheck.Test.make.
  intros.
  destruct x eqn:?.
  destruct p eqn:?.
  unfold Sc_rollup_tick_repr.distance.
  lia.
Qed.

General translation

Here we summarize the general translation process from a property based test to a theorem. We translate a random generator to a predicate describing its domain. We translate a boolean property, applied to this generator, to a statement saying that this property is always true on the corresponding domain.

Language	Generator	Property
OCaml	gen : seed → a	p : a → bool
Coq	pre : a → Prop pre(x) = (x ∈ image(gen))	∀ x, pre(x) ⇒ p(x) = true

What we have

We have a translation in Coq and a part of the proofs for the following test files:

• Saturation_fuzzing.v
• Test_bitset.v
• Test_carbonated_map.v
• Test_sc_rollup_tick_repr.v
• Test_tez_repr.v

Next

We plan to continue writing the proofs and translating other test files. We would also like to completely automate the translation from the OCaml test files to Coq. This task is complex because the tests depend on many other files from the shell part of Tezos, that we would need to translate also.

The techniques we described are not restricted to OCaml and Coq, and could be used for other languages and proof systems.