How should gospel handle model names?

Hello

Opening an issue so we can discuss how we wish to name gospel models. Right now, when we want to give a logical model to a type we have to give it a name like so:

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

And if we want to use it in a specification:

val append : 'a t -> 'a ->  unit
(*@ append c e
       ensures c.view = cons e (old c.view) *)

The upside of this naming convention is that it makes explicit the jump from the OCaml world into the logical world, thereby making the specifications easy to understand. The problem is that it introduces a lot of clutter which makes specs cumbersome to write as well as analyze. There is also the issue of there not being a clear semantics of what c is in the Gospel specs (is it an OCaml type? if so, what does it mean for an OCaml type to live in a Gospel spec?). Therefore, there is some incentive to imagine different ways to express our models. One that François has suggested a few times is having a single unnamed model as so:

type 'a t
(*@ mutable model : 'a sequence *)

val append : 'a t -> 'a ->  unit
(*@ append c e
       ensures c = cons e (old c) *)

The advantage of this representation, besides being a bit more concise, is that it disallows OCaml types to live within Gospel specifications, thereby creating a clear separation between the values that are allowed to exist in logical formulae and program values. One of the downsides is that it implicitly lifts OCaml values into Gospel values which might be confusing to newcomers. Additionally, this means that if you want to have multiple model fields, you would have to create a record type and make that your model. For example, in the case of an array where we would like the model to express the elements within as well as its length:

(*@ type 'a array_model = {length : int; view : 'a sequence} *)

type 'a array
(*@ mutable model  : 'a array_model *)

Although we could imagine having some syntatic sugar to make this more concise, it still leaves us with the fact that both of the model's fields are now mutable, although the length will never change. It is unclear to me what the implications would be in terms of difficulty in proofs, perhaps greater minds can weigh in.

One solution to this problem would be to have a single default "model" (which can be mutable or not) along with multiple named models. For instance, the array example would be expressed as:

type 'a  array
(*@ mutable model : 'a sequence
            model length : int
            with arr invariant arr.length >= 0
*)

With the following get and set functions:

val set : 'a array -> 'a -> int -> unit
(*@ set arr e i
    requires 0 <= i < arr.length
    modifies arr
    ensures arr = Sequence.set (old arr) e i *)

val get : 'a array -> int -> 'a
(*@ e = get arr i
    requires 0 <= i < arr.length
    ensures e = Sequence.get arr i *)

Please feel free to offer your critiques and discuss which representation you think is best for Gospel.

Thanks for opening this issue!

Here are some thoughts.

There is also the issue of there not being a clear semantics of what c is in the Gospel specs (is it an OCaml type? if so, what does it mean for an OCaml type to live in a Gospel spec?).

c could be a record with the logical model as fields. Or the Gospel type-checker could forbid the use of c without any destructor/field access.

One solution to this problem would be to have a single default "model" (which can be mutable or not) along with multiple named models.

I'm not really convinced by this option. IUC, named models are immutable, while the unnamed ones can be mutable. This introduce a relation between being named and being immutable which does not really have any logical basis.

With the simple record type as model, I would write the specifications for set as follow (which I believe forbid to modify the length of the array):

(*@ type 'a array_model = { length : int; contents : 'a sequence } *)

type 'a array
(*@ mutable model : 'a array_model *)

val set : 'a array -> 'a -> int -> unit
(*@ set arr e i
    checks 0 <= i < arr.length
    modifies arr.contents
    ensures arr = Sequence.set (old arr) e i *)

Of course, this means that we have to be precise in the modifies clauses and it could lead to some verbosity with complex models.

ocaml-gospel / gospel

How should gospel handle model names? #392