Logical reflection of arrays / treatment of aliasing

[fpottier]

Hello, sorry to be making so much noise today! I have thought some more about the current treatment of arrays and aliasing. Playing with Cameleer, I believe I am getting close to the point where I can prove something false.

The root of the problem is the logical reflection of the type int array * int array, and the fact that OCaml's mutable arrays are reflected at the logical level as sequences of elements. Such a logical reflection is sound only if one cannot create aliased arrays. But Gospel per se doesn't prevent aliasing. Why3 (which is used internally by Cameleer) prevents aliasing inside a single module, but cannot prevent it if the code is split into several modules, connected by Gospel specifications.

The code is as follows:

let dup x =
  (x, x)
(*@ y = dup x
    ensures y = (x, x) *)

let init x =
  Array.make 1 x
(*@ a = init x
   ensures a.(0) = x
   ensures Array.length a > 0 *)

let danger x =
  dup (init x)
(*@ (a, b) = danger x
    ensures a.(0) = x
    ensures b.(0) = x
    ensures Array.length a > 0
    ensures Array.length b > 0 *)

let write (a, b) =
  b.(0) <- 1
(*@ write ab
    requires Array.length (snd ab) > 0
    ensures (snd ab).(0) = 1 *)
(* I am not sure why it is OK to omit a modifies clause here? *)

(* Rejected by Why3: this application creates an illegal alias
let main =
  write (danger 0)
 *)

(* Why3 saves the day, but relies on an internal alias analysis
   whose results are not visible in Gospel specifications, so it
   should be possible to work around Why3's safeguards by
   breaking the program into several components. *)

module Make (X : sig
  val danger: 'a -> 'a array * 'a array
  (*@ (a, b) = danger x
      ensures a.(0) = x
      ensures b.(0) = x
      ensures Array.length a > 0
      ensures Array.length b > 0 *)
  val write: int array * int array -> unit
  (*@ write ab
      requires Array.length (snd ab) > 0
      ensures (snd ab).(0) = 1 *)
end) = struct
  let main () =
    let (a, b) = X.danger 0 in
    X.write (a, b);
    a
  (*@ a = main()
      ensures Array.length a > 0
      ensures a.(0) = 0 *) (* NOT TRUE IF danger RETURNS A PAIR OF TWICE THE SAME ARRAY! *)
end

(* Apparently functor applications are not yet supported by Cameleer? *)
module M = Make(struct
  let danger = danger
  let write = write
end)

My first main function is rejected by Why3, but the second main function inside the functor Make is accepted, even though its postcondition is intuitively false if the function danger is allowed to return a pair of aliased arrays.

If the final functor application was accepted, then we would have a real problem (I think). And, intuitively, it looks as though this functor application should be accepted: the specs of the formal and actual arguments are identical. But at the moment, functor applications are not handled by Cameleer, it seems (@mariojppereira).

This is up for discussion. As far as I understand, Why3 internally uses an alias analysis (based on a notion of region), but the results of such an analysis cannot currently be expressed in Gospel specs, so Gospel cannot rely on such an analysis in order to guarantee sound reasoning.

[mariojppereira]

This is a very interesting example. I will write by hand in WhyML this very same implementation, making use of the Why3 module system to emulate functors definition and applications.

And yes, I can confirm that for the moment Cameleer does not support functors application. This would require typing information issued by the OCaml compiler, which I currently do not use.

[backtracking]

@mariojppereira I'm puzzled, as you can't write function dup in WhyML.

[mariojppereira]

I am sorry @backtracking , maybe I misunderstand your comment, but why can't you write dup in WhyML? I mean the following implementation:

let dup x =
  (x, x)

is accepted by Why3.

[pascutto]

I think we should move most of the Why3/Cameleer/DV specific questions to the relevant repository (cameleer or why3gospel I guess) instead of the Gospel repo which only handles the surface language; the semantics wrt Why3 is given by Cameleer.

[edwintorok]

Thanks for the clarification. Would you take pull-requests on the gospel/cameleer repositories to bring the two stdlibs closer to each-other?

I've noticed small differences between what is available in Gospel's stdlib and what is available in Cameleer's, but I think this may be just due to the different rate of evolution, and not intentional e.g. Cameleer provides div and Gospel stdlib provides /, so I'd do a PR to cameleer to provide / implemented via div (I'll have to double-check whether its semantics matches OCaml's though, but thats best discussed in cameleer repo).
Similarly there are also situations where Cameleer's stdlib implementations provides more than is available in Gospel stdlib (e.g. power functions), are these meant to be part of Gospel's stdlib, should I attempt to provide PRs to gospel to add them, or are they still experimental and best left only as part of cameleer for now?

I'm discovering these because I'm writing some gospel specs in a .ml file and proving them with cameleer, and then attempting to put them into a .mli for ortac to use, and gospel check would complain it doesn't know them (or the other way around), and it might be easier if I attempt to fix these as I discover them.

[pascutto]

I think the misalignment between the two can be caused by:

• A different rate of evolution, as you mentioned. We should fix those.
• A deliberate difference, e.g. if cameleer is not able to support some parts of the Gospel stdlib (I don't know if this is the case, but it's definitely the case in ortac at the moment). In those cases, it's more tricky to understand if they can even be fixed or if it's a limitation of the tool.

To try to clarify how these standard libraries should work:

• Gospel's standard library (in this repo) is the source of truth for the Gospel ecosystem. We can add items there, but we should have a careful discussion about this as this should remain a standard library close to the OCaml one (and following the same standards and consistency).
• The tools reflection of this standard library is responsible for giving it its semantics (whatever that means depending on the tool). Discrepancies should be reduced to a minimum there, so for instance your div suggestion seems sensible to me (although @mariojppereira is the one to decide this).

[pascutto]

I agree the misalignment is a bit unfortunate, we'll work on reducing that over the next weeks!

[fpottier]

I think we should move most of the Why3/Cameleer/DV specific questions to the relevant repository

I'm fine with that, but in my mind, the questions I am trying to raise here are related to the semantics of Gospel. The logical meaning of a Gospel spec should be defined independently of which tool is used to test or verify it.