vocal-project / vocal Goto Github PK

Consider the following example, contained in file test.mli:

type t
(*@ model v: integer *)

When I run gospel_tc test.mli I get

 type t
    (*@ 
        mutable model v : integer *)

Also, in gospel/ocaml-lib/tast.ml a field is defined as an lsymbol, which in turn is defined as

type lsymbol = {
  ls_name   : ident;
  ls_args   : ty list;
  ls_value  : ty option;
  ls_constr : bool;
}

so I have no way to test the mutability of a field.

Does this mean that fields are always considered mutable?

Would it be possible to provide a small tutorial or enhance the README? I manage to:

• install the vocal package
• create an interface .mli-file based on the examples in the README

However, from there, I do not understand how to use the why3gospel
plugin to generate the Why3 module, and how to give use the Why3
module to provide a verified implementation of the interface.

I have been thinking for a while about the separation conditions that GOSPEL offers and how to deal with those from a proof point of view. I am mainly considering here proofs done via Why3, but I think the discussion is general and can be of interest for those using CFML/Coq.

The Problem

In GOSPEL, we assume that function arguments are separated from each other and from the result. For instance, if we consider the following type declaration

type 'a t
(*@ mutable model view: 'a seq *)

and the following function declaration

val f: 'a t -> 'a t -> 'a t
(*@ r = f x y
       ... *)

we assume, in the GOSPEL specification, that no aliasing occurs between x, y, or r. Since this is a design-choice, there is no need to state this condition explicitly, e.g., by providing in GOSPEL a disjoint clause.

When it comes to Why3 proofs, I believe we need to make some explicit treatment of separation conditions, depending on the underlying implementation of the data structure we are dealing with. Let us first consider the case of the Vector data structure. We have in the Vector.mli file:

type 'a t
(*@ mutable model view: 'a seq *)

which indicates this is a mutable data structure. Nonetheless, the underlying WhyML implementation relies only on arrays:

type t 'a = {
           dummy: 'a;
    mutable size: int63;
    mutable data: A.array 'a;
    ghost mutable view: seq 'a;
  }

Hence, for operations such as the following merge_right:

val merge_right: 'a t -> 'a t -> unit
(** [merge_right a1 a2] moves all elements of [a2] to the end
    of [a1]. Empties [a2]. Assumes [a1] and [a2] to be disjoint. *)
(*@ merge_right a1 a2
         ... *)

the WhyML type system ensures that the internal arrays data, of both a1 and a2, belong to separated memory regions.

However, things are not that simple when the WhyML implementation relies on an explicit memory model. Let us consider the Queue data structure example. On one hand, in the Queue.mli file, we have:

type 'a t
(*@ mutable model view: 'a seq *)

val transfer : 'a t -> 'a t -> unit
(** [transfer q1 q2] adds all of [q1]'s elements at the end of
    the queue [q2], then clears [q1]. *)
(*@ transfer q1 q2
         ... *)

The GOSPEL specification states, again, that this is a mutable data structure and that for the transfer function, q1 and q2 are separated. On the other hand, on the WhyML implementation we have:

type t 'a = {
    mutable ghost length   : int;
    mutable       first    : loc 'a;
    mutable       last     : loc 'a;
    mutable ghost view     : seq 'a;
    mutable ghost list     : seq (loc 'a);
    mutable ghost used_mem : mem 'a;
  }

where used_mem is the footprint of a queue, represented using an explicit memory model. The WhyML specification of the transfer is as follows:

let transfer (q1 q2: t 'a) : unit
  requires { disjoint_mem q1.used_mem q2.used_mem }
   ...

When it comes to refinement proof, we are not able to show that the implementation of transfer refines that of the interface, since no pre-condition from the GOSPEL specification implies the pre-condition disjoint_mem.

A Possible Solution

I believe that, whenever we use the why3gospel plugin to translate GOSPEL specification into a WhyML counterpart, we must sistematically generate a disjoint predicate and use it in required pre-conditions. From a practical point of view, what I propose is the following: for every type declaration containing mutable models

type t
(*@ mutable model x: a
    mutable model y: b *)

generate, during the translation from GOSPEL to WhyML, the following abstract predicate:

predicate disjoint_t t t

and automatically include it in the pre-condition of functions that take two or more arguments of type t. The following GOSPEL specification:

val ff: t -> t -> unit
(*@ ff x y
       requires P
       ensures Q *)

would be converted in the WhyML function

val ff (x y: t) : unit
  requires { P }
  requires { disjoint_t x y }
  ensures { Q }

(This might also be the case for postconditions, to assert that the result is separated from the arguments). Finally, when it comes to implement and verify the data structure in WhyML, one would do:

predicate disjoint_t (x y: t) = (* concret implementation for disjoint_t *)

let ff (x y: t) : unit
  requires { P }
  requires { disjoint_t x y }
  ensures { Q }
= ...

and for the refinement proof:

clone XXX.Sig with
  type t = t,
  predicate disjoint_t = disjoint_t,
  val ff = ff

There is, however, a small caveat with this approach. Since, from a GOSPEL specification point of view, we cannot distinguish mutable data structures implemented using a memory model from those implemented without one, we would need to generate the disjoint predicate even when the WhyML type system would be enough to ensure separation. This is the case for the Vector data structure. In such a case, I believe we would need to always give the trivial implementation to the disjoint predicate:

module VectorImpl
  type t 'a = {
           dummy: 'a;
    mutable size: int63;
    mutable data: A.array 'a;
    ghost mutable view: seq 'a;
  }

  predicate disjoint_t (x y: t) = true
  
  let merge_right (a1: t 'a) (a2: t 'a)
    requires { disjoint_t a1 a2 }
    ...
end