Separation conditions #10
Description
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