Support for strings/bytes and extending Seq

[edwintorok]

Hi,

I think it would be useful for Gospel (or its stdlib) to include support for strings. It is quite hard to avoid using strings in some form in a module, and some basic support in the stdlib for it would be useful.

It might be possible to write the Bytes interface using the existing Gospel syntax and stdlib, but not everything is easily definable.
Going through the exercise of providing a spec for something like Bytes or Buffer would be a useful way to enhance the expresiveness of Seq.

See below for my attempt on getting started on this. Would it be useful if I continue this and present a fully specced Bytes and Buffer interface (or at least as much as definable in Gospel currently), or would that duplicate what you're already working on?

Predicates and some easy Bytes specs

E.g. I think the initial comments in the Bytes module can be quite nicely translated into Gospel as they're already semi-formal:

** Byte sequence operations.

    A byte sequence is a mutable data structure that contains a fixed-length sequence of bytes.
*)
(*@ type bytes*)
(*@ mutable model contents: char seq
    model length: int
    invariant Seq.length contents = length
    invariant 0 <= length <= Sys.max_string_length
*)

(** Each byte can be indexed in constant time for reading or writing. *)

(**
   Given a byte sequence [s] of length [l], we can access each of the
   [l] bytes of [s] via its index in the sequence. Indexes start at
   [0], and we will call an index valid in [s] if it falls within the
   range [[0...l-1]] (inclusive).
*)
(*@ predicate is_valid_index(b: bytes)(i: int) = 0 <= i <= b.length-1 *)

(** A position is the point between two
   bytes or at the beginning or end of the sequence.  We call a
   position valid in [s] if it falls within the range [[0...l]]
   (inclusive). Note that the byte at index [n] is between positions
   [n] and [n+1].
*)
(*@ predicate is_valid_position(b: bytes)(i: integer) = 0 <= i <= b.length *)

(** Two parameters [start] and [len] are said to designate a valid
   range of [s] if [len >= 0] and [start] and [start+len] are valid
   positions in [s].
*)
(*@ predicate is_valid_range(b: bytes)(start: int)(len: int) =
      len >= 0 && is_valid_position b start && is_valid_position b (start+len) *)

And these predicates can be used quite nicely when defining properties:

external set : bytes -> int -> char -> unit = "%bytes_safe_set"
(** [set s n c] modifies [s] in place, replacing the byte at index [n]
    with [c].
    @raise Invalid_argument if [n] is not a valid index in [s]. *)
(*@ set b i c
    checks is_valid_index b i
    modifies b
    ensures b.contents = Seq.set (old b.contents) i c
*)

Specifying unchanged sequence elements

However some of the other functions' specifications turn out to be quite long if I also want to specify what doesn't change:

val fill : bytes -> int -> int -> char -> unit
(** [fill s pos len c] modifies [s] in place, replacing [len]
    characters with [c], starting at [pos].
    @raise Invalid_argument if [pos] and [len] do not designate a
    valid range of [s]. *)
(*@ fill s pos len c
    checks is_valid_range s pos len
    modifies s
    ensures forall i.
      pos <= i <= pos+len-1
      && s.contents[i] = c
      && s.contents[..(pos-1)] = old s.contents[..(pos-1)]
      && s.contents[pos+len..] = old s.contents[pos+len..]
*)

For fill this is doable, but I'm just worried that in a more complex data structure having to manually specify everything that stays the same would be quite error-prone and easy to forget some crucial part. Would be nice if there was a way to say: s is identical to old s, except for anything that is explicitly defined to be different (although I realize it'd then be quite hard for a prover like cameleer to come up with a way to formally express that).
I think lenses might give an idea for a good way out of this: if I could get a mutable view on an 'a seq and define properties just on that, and have a default 'everything not part of the view is the same' it might simplify specifications:

(*@ predicate seq_view (s: 'a seq) (p: integer -> bool)(f: 'a seq -> integer -> bool) =
     forall i.  (p i -> f s i) && (not (p i) -> s[i] = old s[i]) 
*)

And then fill could be specificied as:

ensures seq_view s.contents (fun i -> pos <= i <= pos+len-1) (fun s i -> s[i] = c)

(although I'm not sure how convenient it'd be to work with that form in proofs)

The problem is you wouldn't be able to use more than one of these because then the first view would add an incorrect = old s constraint, it'd probably have to a predicate that handles a list of ranges, uses fold_left (or fold_right) on them to build up a growing list of ranges, and then at the end add the old constraints for anything not part of that range (being able to easily turn intervals into sets would probably be useful here to translate all this into set membership in the end).

I'm probably missing something obvious here, is there an easier way to specify old?

I was thinking to use Seq.set here, but IIUC the forall would make all those sets apply in parallel which would end up with equations like this for pos=1, len=2:

s[0] = old s[0]
s[1] = c
s[2] = old s[2]
&&
s[0] = old s[0]
s[1] = old s[1]
s[2] = c

(which would be a contradiction)

Perhaps it is writable using Seq.fold_left and passing in the old value just once? (But cameleer doesn't implement fold_left yet, so I wouldn't be able to try that out).

Seq.iter?

There are also functions that are difficult to specify in the Gospel language in the first place, like iter (I'm thinking this can be done as Seq.fold_left on a unit, but it looks a bit unnatural), and iteration would come up in almost any data structure, so having a Seq.iter would be useful (even if they desugar to fold_left, etc.)