Logical reflection of OCaml values

[fpottier]

I believe that the Gospel documentation does not clearly explain (and I do not clearly understand) what it means to refer to an OCaml value inside a Gospel formula.

Two questions must be distinguished: first, what names are in scope in a Gospel formula? second, what (logical) type do they have, and what (logical) objects do they denote?

Regarding the first question, it is tempting to state that both the names defined at the OCaml level and the names defined at the logical level are in scope. So, e.g., a formula can refer to length x, where the function length has been defined at the logical level and x is (say) a local variable in the OCaml code. I like this approach, but one must be aware that it quickly runs into collisions. For instance, the OCaml primitive operation + and the mathematical addition + have the same name. This particular example may seem tolerable, because (as noted by Mario) most of the time, when we write + in a formula, we mean mathematical addition. But this means that we must arrange for the mathematical operation + to shadow the (logical reflection of) the OCaml operation +. This convention is somewhat brittle, and breaks if the programmer locally redefines + in the OCaml code; then the mathematical + would become shadowed and would no longer be accessible. More generally, I believe that we have a huge collision problem because the Gospel logical library contains many objects that have the same names as functions in the OCaml standard library: e.g., Array.length denotes both an OCaml function in the OCaml standard library and a logical function in the Gospel library; etc. This does not make sense: when one writes Array.length in a formula, what is meant? Is it (the logical reflection of) the OCaml function Array.length, or the logical function Array.length defined in the Gospel library?

Regarding the second question, it is tempting at first to think that one can refer to an OCaml variable x either inside the OCaml code or inside a Gospel formula, and that x denotes an object of "the same type", in fact "the same object" in both cases. E.g., if x has type bool in OCaml, then x has type bool when mentioned in a Gospel formula, and all is well. But this works only for a subset of types that exist both at the OCaml level and at the logical level, with the same meaning. At abstract types, we must make sure that an OCaml value of abstract type is reflected in the logic as a logical value of abstract type. For example,

• Regarding integers, an OCaml value of type int should be reflected as a logical value of abstract type int, and we should reason separately (say, via a function view : int -> integer and a predicate isInt : integer -> Prop) about the connection between int and integer.
• Regarding functions, because an OCaml function is in general impure, its logical reflection should not be a logical function; it should be an opaque object of type fun. (This is what CFML does.) We should reason separately about the fact that an OCaml function "implements" a certain logical function (say, via nested Hoare triples).
• Because many OCaml functions are in fact pure, it seems desirable to offer good support for this special case. I would suggest making it possible to write isPure(f), in the logic, to assert that a function is pure. Thus, for instance, a map function could require its argument f to be a pure function, if desired. When isPure(f) holds, where f has type t -> u in OCaml, it would be desirable to view f also as an object of type t -> u in the logic (instead of fun as in the general case). (Perhaps a syntactic marker would be needed, for disambiguation: we may for instance have to write %f.) (The predicate isPure may need to also carry an arity, to deal with functions of several arguments.)The predicate isPure would not be magic: the definition of isPure(f) would be that f implements %f. (The details need to be clarified...)

In summary, I think it is absolutely fundamental to clearly define what names are in scope in a logical formula, and with what type. These issues are nontrivial, and I don't think they have been fully spelled out yet in Gospel.

[fpottier]

I note that the OCaml function Array.length has type 'a array -> int, whereas the logical function Array.length in the Gospel stdlib has type 'a array -> integer. Independently, each of these definitions is fine, but giving them the same name creates a very real problem: we end up with two (distinct) mathematical objects (of distinct types) by the same name.

Arguably, we do not need Array.length in the logical library, because the logical model of an array is a sequence, and we already have a logical function that returns the length of a sequence, namely Seq.length. (The fact that there is a collision with the OCaml function Seq.length is another story...)

[pascutto]

I can try to answer some of your questions (there are many!) about the current state of Gospel.

But this means that we must arrange for the mathematical operation + to shadow the (logical reflection of) the OCaml operation +. This convention is somewhat brittle, and breaks if the programmer locally redefines + in the OCaml code; then the mathematical + would become shadowed and would no longer be accessible.

This is exactly what we do at the moment. You can indeed shadow Gospel's stdlib by redefining symbols with the same name, but this is a very natural behaviour for OCaml developers, so I do not quite understand why this is an issue?

This does not make sense: when one writes Array.length in a formula, what is meant? Is it (the logical reflection of) the OCaml function Array.length, or the logical function Array.length defined in the Gospel library?

It refers to the logical definition. An (*@ open Gospelstdlib *) is added at the beginning of every file, so the usual shadowing rules apply.

Regarding integers, an OCaml value of type int should be reflected as a logical value of abstract type int, and we should reason separately (say, via a function view : int -> integer and a predicate isInt : integer -> Prop) about the connection between int and integer.

That is already what we do. There is an abstract int type in the stdlib, and an integer_of_int logical function that does what your view means. There is no isInt predicate, but it's trivial to write as there are also min_int and max_int. See here.

Regarding functions, because an OCaml function is in general impure, its logical reflection should not be a logical function; it should be an opaque object of type fun. (This is what CFML does.) We should reason separately about the fact that an OCaml function "implements" a certain logical function (say, via nested Hoare triples).

OCaml functions are not represented as logical functions unless their contract contains a pure clause. There is an exception for higher order functions, but we require that those are always pure in Gospel.

Because many OCaml functions are in fact pure, it seems desirable to offer good support for this special case. I would suggest making it possible to write isPure(f), in the logic, to assert that a function is pure.

We already have support for a pure clause in a contract that does just this. Again this does not apply for higher order functions arguments, where we solve the issue by requiring those to always be pure. In other word there is no support for impure function arguments at the moment.

Arguably, we do not need Array.length in the logical library, because the logical model of an array is a sequence, and we already have a logical function that returns the length of a sequence, namely Seq.length.

Arrays and sequences are now two distinct types in the stdlib, although there is a coercion from arrays to sequences. It is indeed possible to write Seq.length over an array, but it is definitely more natural to an OCaml developer to use a function with the same same they're used to, so I think it makes sense to have Array.length for arrays

[fpottier]

Thanks Clément for your replies!

I think it is fine to have a single namespace for OCaml names and Gospel names, with shadowing. I wasn't sure that this was the rule. I also wasn't aware that (*@ open Gospelstdlib *) is added at the beginning of every file; this makes sense.

The fact that a Gospel symbol can be shadowed by a local definition in the OCaml program is fine in theory (this behavior is easy to understand and well-defined) but I think it may lead to undesirable shadowing problems in practice. E.g., assume I have written (*@ open Seq *) because I want easy access to the logical functions on logical sequences. If my OCaml code happens to define a variable named empty, singleton, length, etc., then this shadows the definition by the same name in the Gospel library, which is problematic, as it prevents me from using unqualified names in logical formulae. We might wish to have a way of adding a syntactic marker that clarifies which namespace we want; e.g. #x for an OCaml name x and %x for a Gospel name x and just x for whichever of these two names was bound most recently.

I suppose that a similar rule exists at the level of modules. So the OCaml module Array in the OCaml standard library is shadowed by the Gospel module Array in the Gospel standard library, right? At the moment, if I want to refer to the OCaml module Array, I suppose I can do so under the full name Stdlib.Array. So, Stdlib.Array.length is an OCaml function, which happens to be pure and (maybe) is reflected in the logic as a function of type 'a array -> int (is this true?), whereas Array.length is a Gospel function, whose type is 'a array -> integer. Is this correct? I believe that there is potential for confusion here; I am not yet convinced that it is a good idea to intentionally use the name Array to name two distinct modules in two distinct libraries at two distinct levels.

[edwintorok]

ocamldoc and odoc has a way to disambiguate which namespace to use for references (modules, types, etc.), see https://ocaml.github.io/odoc/odoc_for_authors.html#links-and-references, might be useful to adopt something similar to Gospel.
Or there could be 2 aliases available by default:
OCaml. and Gospel, and one could use OCaml.foo or Gospel.foo if they want to be explicit.

[fpottier]

I do see a need to distinguish in the logic the type 'a array and the type 'a seq, but I think there is a large potential misunderstanding about the meaning of the type 'a array at the logical level.

• One way of understanding 'a array at the logical level is that it is (isomorphic to) a subset of 'a seq: a logical array is essentially a sequence of elements, perhaps with some extra properties (e.g., its length is at most max_array_length).
• Another way of understanding 'a array at the logical level is that it is an opaque object: essentially just a memory location. Indeed, OCaml arrays are mutable, so when we talk in the logic about "the array a", we are referring to the address of a, not to its content.

In the first view, a logical function such as Array.get : 'a array -> integer -> 'a makes sense, but in the second view, it does not: the content of an array is not a function of its address.

As far as I understand, Gospel and Cameleer (@mariojppereira) currently use the first view, where an array is reflected at the logical level by its content, and there is no way at the logical level to talk or reason about the address of an array. This seems sound (even though OCaml arrays are mutable) because some aliasing restrictions are imposed (by Cameleer?). But, in this approach, some OCaml types cannot be reflected in the logic at all: for instance, the OCaml type int array list cannot (reasonably) be reflected by the logical type int array list. An OCaml list of arrays can contain several occurrences of the same physical array. If we allowed this kind of reflection, then we would perform program verification under the assumption that all arrays in a list must be disjoint, an assumption that is invalid in reality. So, how is the type int array list reflected today in Gospel? I don't know the answer.

CFML (@charguer) uses the second view, where an array is reflected in the logic as a memory location, and a separate "points-to" predicate is used to connect the array with its content. This second view is heavier but seems more general and necessary in order to reason about aliasing and ownership.

As a middle ground, it would be possible to let the OCaml type-checker distinguish between two (distinct, incompatible) types of mutable arrays and immutable arrays. An immutable array could be reflected in the logic directly as a logical array (a sequence of elements), whereas a mutable array would more likely have to be reflected in the logic as an address.

[fpottier]

Regarding pure clauses, I know about them, and I know about the implicit hypothesis that every higher-order function is pure (and requires pure arguments), but I would like to remove this hypothesis. Hence my suggestion to view isPure as a logical proposition, allowing a higher-order function (such as map) to explicitly indicate that its argument f must be pure (if desired).

[pascutto]

I agree allowing impure higher-order function arguments would be interesting, in particular as a step towards specifying iter functions (/cc @mariojppereira).
(As a side note I would consider that bad practice in the case of a map or a fold for instance.)
I created #150 to track this feature.

[fpottier]

Aliasing, ownership, and logical reflection of mutable objects

This post is intended to summarize my current thoughts on the treatment of mutable objects: how are these objects described at the logical level, in the specification of a function?

Motivation

In Gospel, every OCaml value is automatically and implicitly reflected, or lifted, to the logical level: whenever a variable x is in scope at the level of the OCaml code, it is permitted to refer to x in a Gospel formula. Although the name x is used at both levels, two conceptually distinct objects are involved: whereas the OCaml variable x denotes an OCaml value and has an OCaml type t, the Gospel variable x denotes a mathematical value and has some Gospel type T, which may or may not be a function of t. The universes of OCaml types and Gospel types are distinct, so we definitely cannot expect t and T to be "the same type", except in some special cases like unit, bool, and (more generally) the first-order algebraic data types, which exist both in OCaml and in Gospel. In summary, when we speak about the logical reflection of an OCaml value of type t denoted by an OCaml variable x, we mean the mathematical value of type T denoted by the variable x in Gospel formulae.

It is crucial to clearly define this connection between OCaml values and types and Gospel values and types.

Mutable objects (references; records with mutable fields; arrays) are problematic because there is a tension between two conflicting desires: we sometimes wish to refer to their address, and sometimes to their content. If a is a mutable array of type bool array at the level of OCaml, what should a denote at the level of Gospel? Should it denote a sequence of elements, of type (say) bool seq, or should it denote an address, of type (say) loc?

This question arises only when both mutable state and aliasing are present. In the absence of mutable state, there would be no need to ever mention the address of an object; one would reason always in terms of its content. In the absence of aliasing (that is, roughly, if two distinct OCaml variables are never allowed to denote the same mutable object), the same is true: the address of a mutable object is irrelevant, and one can reason always in terms of its content (even though this content evolves through time). Gospel as it stands today (February 2022) allows mutability but disallows aliasing: the logical reflection of a mutable object is always its content, never its address. As a result, there is no way of describing data structures that involve aliasing (multiple pointers to a single mutable object), such as a list of not-necessarily-distinct references.

To remedy this lack of expressive power, it seems that we must introduce a way of disambiguating whether we wish to speak about the address of a mutable object or about its content. Furthermore, in order to give a sound specification to an operation that updates a mutable object, describing the content of a mutable object should be permitted only when this object is uniquely owned. Thus, for example, if r is an OCaml reference of type bool ref, then we must somehow indicate whether we own this reference, in which case r could have Gospel type { contents: bool } and !r could have Gospel type bool; or we do not own this reference, in which case r could have Gospel type bool ref (a synonym for loc?) and the Gospel term !r would not make sense.

Goals and Considerations

Here is a list of goals, or considerations to keep in mind.

• We want to keep the most common case (absence of aliasing) simple and lightweight. Objects should be considered owned and disjoint by default. A heavier syntax must be used when this is not the case.

• It may be desirable to maintain a visual analogy between Gospel formulae and OCaml code, and perhaps even to go so far as to ensure that a subset of Gospel formulae can be executed. (Ortac requires this.) This encourages using !r to refer to the content of an (owned) reference, a.(i) to refer to the content of an (owned) array, etc. Is this tenable?

• It is not entirely clear in my mind when (in a formula) we want to refer to a data structure, say q, and when we want to refer to its model, view q.
  Do we need to distinguish between them? Probably yes, because they do not have the same Gospel type: q has type (say) 'a Queue.t, an abstract
  type, whereas view q has type 'a seq, a logical sequence. Probably the type of q varies depending on whether q is owned or not owned. Probably view q is permitted only when q is owned.

• We want to avoid forcing the user to introduce separate names for a data structure q and for its logical model Q. I think we can always achieve
  this by writing view q for the model. Even in cases where the logical model is not a function of the concrete state, we can artificially make it a
  function of the state by making the model a ghost field.

• There will be a need for "group regions", that is, iterated conjunctions of ownership assertions. In other words, we need a way of saying, "for every
  location l in the set L, (we own l and) some property P(!l) holds". We will also need to quantify existentially over the set L. Examples where
  this is needed: union-find; persistent arrays. We should try and write down exactly how these examples will be verified.

• Clarifying the logical reflection (the correspondence between OCaml values/types and Gospel values/types) is essential. Spelling out the
  translation of Gospel specs to Separation Logic (CFML) specs will also help.

• Plan ahead. Ideally, Gospel should not just allow reasoning about the ownership of mutable objects. Like Separation Logic, it should also allow
  reasoning about ownership of other resources, and should encourage several form of local reasoning (one function versus its caller; one module versus the rest of the program; one thread versus all other threads; etc.). In Separation Logic, an assertion reflects a piece of information that is stable under interference. In other words, it describes something that "we" know (and "others" cannot destroy); dually, it describes something that "we" can destroy (and "others" cannot know). A number of general concepts that might make sense in Gospel are: a distinction between pure, persistent, affine, linear assertions; mechanisms for ownership transfer (that is, the ability for assertions to be consumed or produced); ghost state in user-defined monoids; shared invariants. Some of these features can be axiomatized (made available as special libraries) provided the specification language is expressive enough.

Technical Remarks

• At the level of Gospel, should addresses be homogeneous or heterogeneous? If 'a ref is the Gospel type of an unowned reference, should it be defined as a synonym for loc, or should it be viewed as an abstract type? Using an abstract type allows rejecting formulae where references of distinct types are confused by mistake. Using an abstract type implies that group regions must be homogeneous: one cannot construct a set of locations that contains locations of distinct types. A similar question concerns other kinds of mutable objects (arrays, mutable records, etc.).

• We may wish to introduce a type of immutable arrays in OCaml (as a library module). Its spec would be simple; the logical model of an immutable array would be a logical sequence.

• The length of a mutable array can be viewed as an immutable property, so it should be possible to refer to the length of an array even when this array is not owned.

• The length of an array comes with an invariant: it is an integer that inhabits a certain range. I suggest reflecting this via a predicate isValidArrayLength. This is independent of mutability and ownership considerations.