Varray example

[n-osborne]

This PR add the varray example.
It is bassed on the not yet merged #177, please consider only the two last commits.

There were four challenges, of different importance:

• The specifications are in an ml file and Gospel does not read ml file. The proposed solution/workaround is to extract the content of the module signature we are interested in.
• Writing specifications with Gospel sequence type is not that easy (it is very possible that review reveals some off-by-one mistakes!)
• User have to write some dune machinery in order to test different Functor instantiations.
• The included module is a bit bigger than the one for the Initiate ortac-example package #177 example and need to be included in two different tests. We had to make it a library. The size of the included module is what triggered Add an include option to qcheck-stm cli #181.

[shym]

This is nice, well done! (I confess I didn’t review the generated tests :-).
I’ve pushed on my varray-bis branch a fix for a couple of typos in the README. (By the way, I wondered at what width you split lines, so I didn’t reformat after editing, but you probably should).

A couple of small suggestions for the specs.

• Calling the helper function valid is ambiguous to me (especially as it is documented as checking whether an index is valid :-). As it is only used in one function specification, I would simply inline it there.
• In sub (examples/varray_sig.ml at line 318), you prohibit n=0: why? Same thing in blit. This is allowed in fill, for instance, where the informal documentation is stating the same constraint.
• In fill, I was surprised the ensures was not reversed, ie if pos <= i < pos+len then proj x else ..., as a more direct formalisation of the informal documentation. But it might be the purpose, of rewriting it in another way to avoid repeating the same mistake?

[n-osborne]

Waiting for varray.0.2 so that minimal version for varray can be added.

[n-osborne]

CI failure seems unrelated. I merge.