Incomplete computation warning on inbuilt return types

[nikolaushuber]

Certain types currently raise incomplete computation warnings which causes them to not be shown in error traces. One example is Array.mem:

File "array.mli", line 55, characters 0-89:
55 | val mem : 'a -> 'a t -> bool
56 | (*@ b = mem a t
57 |     ensures b = Sequence.mem t.contents a *)
Warning: Incomplete computation of the returned value in the specification of mem. Failure message won't be able to display the expected returned value.

If mem is adapted to

let mem c t = not (mem c t)

The error message reads:

Messages for test Array STM tests:

Gospel specification violation in function mem

  File "array.mli", line 57, characters 12-41:
    b = Sequence.mem t.contents a
  
when executing the following sequence of operations:

  [@@@ocaml.warning "-8"]
  open Array
  let protect f = try Ok (f ()) with e -> Error e
  let sut0 = make 16 'a'
  let sut1 = make 16 'a'
  let r = mem '%' sut1
  (* returned true *)

Similar things can be observed for tuples (see for example tuple_errors.expected) and optionals (e.g. queue_errors.expected). In the latter case ortac should be able to print it, since the type variable is already instantiated at that point.

[n-osborne]

Thanks for raising this issue!

There are in fact two problems here.

Regarding the bool type, Gospel is transforming equality between terms of type prop into a double equivalence. Meaning:

ensures b = Sequence.mem t.contents a

becomes in the typed ast:

ensures b <-> Sequence.mem t.contents a

This will disappear in the next Gospel release with this PR. So I believe there is no need to amend the way we look at postconditions for this particular case in Ortac/QCheck-STM.

Regarding Options and tuples, the .mli files don't contain any suitable (as defined by Ir_of_gospel.returned_value_description code) postconditions.

In the Queue.peek_opt case, the postcondition is not stated as a description of the returned value (and I believe there is no syntactic transformation that would give us such a description).

In the tuples case, which can be generalised to records too, the fields are described in separate postconditions. Here, we could make Ir_of_gospel.returned_value_description more clever and look whether it is possible to re-build the (named) tuple with all the information in the postconditions rather than looking at them one by one.