More constraints for Sys

[edwintorok]

Hi,

I've attempted to define constraints for a few more values in the Sys module. Should these all go into the base Gospel stdlib, or would the constraints be better in cameleer with just the declarations in Gospel? (I can raise a PR with what I have so far if it is useful)

Currently values like max_array_length aren't constrained (neither in the base Gospel or Cameleer implementation), which means that using cvc4-ce to generate counter examples quite often picks a very low number for this that might falsify a formula, that could never happen in practice if you look at what the lowest value is on a 32-bit build.

This is what I've come up with so far: word_size is defined as an axiom that can be either 32-bit or 64-bit, and then based on that the ranges of further constants are restricted (using ensures as the docs say for constants doesn't work unfortunately, the counterexampl e generator completely ignores it and generates counterexamples that would fail the constraints - albeit probably a cameleer bug - but using axiom works:

* TODO:
   * word_size is declared in Gospel stdlib but cameleer hasn't caught up yet, declare them all in both cameleer/gospel stdlibs
   * instead of using 'function' to declare various values (e.g. max_string_length) we should use
   val, but can't can't really express constraints on that (it says not declared),
   and if I write 'n = max_string_length' 'ensures n ....' it doesn't take the constraint into
   consideration when building counterexamples.
   * the disadvantage of using 'function' is that these values become unavailable to use from
   regular OCaml code (they can only be used in gospel specifications and in @logic functions)
   * max_array_length in practice has only 2 values (one for 32-bit, one for 64-bit), but it is
   possible to change it via configure, so use a range for now
   * we could add a constraint that max_array_length needs to be 2^wosize_bits where wosize_bits is
   in a certain range but this slows down counterexample generation a lot even for simple cases it
   hits the 5s timeout
   * max_array_length is already defined in the Gospel/Cameleer stdlib, we should add the constraint
   on it there
   * / seems to be missing from cameleer, although it is part of the Gospel stdlib, for now for simple cases it can be defined using `exists` and multiplication.
*)

[@@@gospel {| function word_size : integer |}]

[@@@gospel {| axiom wordsize: word_size = 32 || word_size = 64 |}]

[@@@gospel {| function int_size: integer = word_size - 1 |}]

val big_endian : bool

[@@@gospel
{| axiom maxarrayl: 4194303 <= Sys.max_array_length <= 18014398509481983 |}]

[@@@gospel {| function _word_size_bytes : integer |}]

[@@@gospel {| axiom wsbytes: _word_size_bytes * 8 = word_size |}]

[@@@gospel {| function max_string_length: integer |}]

[@@@gospel
{| axiom maxstring: max_string_length = _word_size_bytes * Sys.max_array_length -1 |}]

[@@@gospel {| function max_floatarray_length: integer |}]

[@@@gospel
{| axiom maxfa:
    (word_size = 64 -> max_floatarray_length = Sys.max_array_length)
    && (word_size = 32 -> 2 * max_floatarray_length = Sys.max_array_length)
|}]

exception Break

val opaque_identity : 'a -> 'a
  [@@gospel {| x = opaque_identity y
    ensures x = y |}]

[fpottier]

I would suggest introducing a predicate isValidArrayLength, and attaching the invariant isValidArrayLength(length a) with the OCaml type array. So, isValidArrayLength would appear both in the precondition of Array.make and in the postcondition of Array.length, for example.

This would allow the user to choose between:

• assuming isValidArrayLength(n) <-> True, which means there is no bound on the length of arrays;
• assuming isValidArrayLength(n) <-> 0 <= n && n <= Sys.max_array_length, which means we there is a bound; and in this case, the user should again have a choice between leaving Sys.max_array_length unspecified or assuming a specific (known) value.

[edwintorok]

Thanks, I think that would provide the needed flexibility in proofs (on 64-bit systems you're very likely to run out of memory and crash long before reaching Sys.max_array_length, so isValidArrayLength <-> True may be in practice equivalent to it).

I think we should have some lower bounds on all of these values, otherwise proofs will fail, and the counterexamples would show impossibly small values of Sys.max_array_length, e.g. Array.make 4 x would need to prove that Sys.max_array_length > 4, and will likely generate a counterexample with a Sys.max_array_length <= 4 but that could never happen in an OCaml program.
If we set a lower bound for Sys.max_array_length based on the lowest value that any OCaml backend implements then at least we don't have to worry about Sys.max_array_length for constant sized arrays (unless they are very very large, in which case it'd already be a portability problem to 32-bit OCaml builds)

The upper bound (or exact value) can then be defined by the user depending on what they want to achieve in their proof,

[pascutto]

My understanding is that this issue is the same as the one discussed in #134 w.r.t. constraints/values for max_int and min_int, and it should be addressed the same way.