Support for fixed-size integers

[edwintorok]

Hi,

Sorry for raising so many different discussions, but I thought it'd be best to separate it into 3 different topics as they are quite orthogonal. I've recently started looking at the possibility of using Gospel to prove some OCaml code.
I'm aware this is quite a young project with some rough edges around the tooling, but I think it already provides quite a lot of value by being able to write down function behaviour in a machine parseable form. In fact writing down the specifications alone in gospel helps in thinking and reviewing code correctness (previously all these constraints were just in my head, and would have to "swap in" when coming back and looking at an old piece of code).

int32, int64 would be good to have, including 2's complement arithmetic or a form where any overflow means an error.
I think the latter is what Why3's stdlib provides, but isn't quite yet easily available in Gospel, but see https://github.com/ocaml-gospel/cameleer/blob/master/examples/cameleer.drv should be possible to add.
It might even be definable in pure Gospel syntax, although it'd duplicate the definitions in Why3.

There is also a question on what to do about int. Cameleer currently defines it the same as integer which is not quite right: it might prove that a function never throws an exception, whereas in practice it would due to integer overflow causing some invariants to not be upheld.
I see the value of defining specifications with arbitrary sized integers, but then verification should ensure no overflow happens (and treat that as a spec failure if it does).
But which integer size should int be? If you're targeting verification only for one platform, e.g. x86-64 then choosing statically the size would make sense.
OTOH for fully portable programs it'd be great if we could prove that they work for both 31-bit and 63-bit sized ints. E.g. one might focus ortac fuzzing on just one build, which would leave the other one less well tested, and this is exactly where formal tools could help prove it works everywhere.

I don't see how to define a type depending on another predicate though, e.g. ideally something like this (IIUC this can't be expressed in Gospel):

(word_size = 32 -> type int = int31) && (word_size = 64 -> type int = int63)

Or perhaps just the various arithmetic operations would define their limits based on word_size, but that means it couldn't reuse the types from Why3...

Alternatively verification tools like Cameleer could build 2 formulas: one for word_size =32 and one for word_size =64 and then merge the 2 formulas with && (perhaps simplifying and dropping duplicate entries along the way to make the proofs simpler).
(Or run 2 separate proofs, once for 32-bit and once for 64-bit wordsizes, which might be the easiest with the addition of a cmdline flag to cameleer)

What do you think the best solution would be here?
I'd be happy to help in adding support for these (either in Gospel or Cameleer, although Cameleer says no support is provided yet, so not sure if it accepts PRs yet)

[fpottier]

Hi!

I would suggest viewing the OCaml type int as an abstract type. The model of an OCaml value i of type int would be a mathematical integer view i of type integer. With the type int, we would attach the invariant isInt, so that whenever i has type int, we can deduce isInt(view i). (We might also need a form of sugar to allow writing just i instead of view i in logical formulae, but that is a somewhat separate issue.)

The predicate isInt could be treated in several different ways:

• the user could assume isInt(j) <-> True, which means they are assuming ideal integers;
• the user could assume isInt(j) <-> min_int <= j <= max_int, without explicitly defining min_int and max_int, which means that they are assuming bounded integers but do not rely on a specific word size;
• the user could assume isInt(j) <-> min_int <= j <= max_int and define min_int and max_int as explicit constants, which means that they are assuming bounded integers and a specific word size;
• the user could regard isInt as abstract and explicitly state (as hypotheses) the stability properties that isInt must satisfy.

[edwintorok]

Thanks, having a few more helper predicates in the gospel stdlib might be the way to go.

I've tried various ways to define max_int based on Sys.word_size though, but it looks like Gospel cannot express the fact that Sys.word_size is either 32 or 64-bit, but consistently the same value across the lifetime of a program.
If I create an axiom that says Sys.word_size = 32 or Sys.word_size = 64 then I eventually get a counterexample (with cvc4-ce as prover) where Sys.word_size is 64 and then later on Sys.word_size is 32 in the same counterexample. Although that may be one valid interpretation of the original constraint, it is an impossible one.
I think the only way out (for now) is to run the prover twice (e.g. using a script that adds an extra definition to a file):

• once where I define Sys.word_size = 32
• another where I define Sys.word_size = 64

(and then various other constraints can define what min_int and max_int is based on that)

If they both come out OK then my program is proven to work with both word sizes (of course if I can prove that my program works even with Sys.word_size changing its value between 32 and 64 then the above 2 cases would be implied)

[pascutto]

max_int and min_int already exist in the Gospel standard library (here).
What's wrong with using those directly?

[edwintorok]

On 17 February 2022 13:47:16 GMT, "Clément Pascutto" ***@***.***> wrote: `max_int` and `min_int` already exist in the Gospel standard library ([here](https://github.com/ocaml-gospel/gospel/blob/main/src/stdlib/gospelstdlib.mli#L108-L109)). What's wrong with using those directly?

I can use those definitions, but will likely need to add some range constraints separately (otherwise a solver can pick something like max_int=1 and min_int=2 in theory that could cause some pre/postcondition to fail). Perhaps the gospel stdlib could have just some very minimal constraints: `min_int < 0 < max_int). -- Sent from my Android device with K-9 Mail. Please excuse my brevity.

[pascutto]

Maybe I misunderstand the issue, but I think it's cameleer's responsibility (or any other tool) to give the correct meaning to these constants (/cc @mariojppereira), just like for the rest of the standard library; Gospel is not aware of (and not specifically designed for) the further usage that you make of these specs (in particular when it comes to solvers).

[mariojppereira]

Yes, this is exactly the case. In Cameleer, I am mapping the names max_int and min_int into their Why3 counterparts max_int63 and min_int63 (cf, http://why3.lri.fr/stdlib/mach.int.html#Int63_)

[edwintorok]

On 17 February 2022 13:55:12 GMT, "Clément Pascutto" ***@***.***> wrote: Maybe I misunderstand the issue, but I think it's cameleer's responsibility (or any other tool) to give the correct meaning to these constants (/cc @mariojppereira), just like for the rest of the standard library; Gospel is not aware of (and not specifically designed for) the further usage that you make of these specs (in particular when it comes to solvers).

Indeed, `ortac` would probably not need these, since it can just read the values at runtime. Perhaps as you say the additional constraints should be provided by cameleer's implementation of the gospel stdlib, and gospel should just ensure that the needed constants and predicates are declared. -- Sent from my Android device with K-9 Mail. Please excuse my brevity.

[fpottier]

I think it might be good to introduce a predicate isInt at the level of Gospel, and to not necessarily publish the fact that isInt(j) <-> min_int <= j <= max_int, so the user can choose to reason with unbounded integers, if they so wish.

Also, as Edwin notes, at the level of Cameleer, it might be good to not specify the exact values of min_int and max_int. We could specify min_int = -2^k and 2^k - 1 = max_int where k = Sys.word_size - 1 and Sys.word_size >= 32.

[pascutto]

I think it might be good to introduce a predicate isInt at the level of Gospel, and to not necessarily publish the fact that isInt(j) <-> min_int <= j <= max_int, so the user can choose to reason with unbounded integers, if they so wish.

I'm curious what would be a concrete use-case for this? My experience is that when specifying your program, you're mostly interested in talking about:

• ints that come from your program (they are obviously ints)
• integers that are introduced in the specification (why do you need them to be within the int range?)

Very few programs actually rely on overflowing as a normal behaviour, and these can introduce isInt or inline it themselves.

With other words: it can be useful, but is it useful enough to introduce it in the stdlib (while max_int and min_int are already there) ? I haven't seen a use case for it so far

[fpottier]

As you said, the integers that come from the program have type int, whereas mathematical integers have type integer. Now, suppose I want to pretend that machine integers are unbounded. I want the types int and integer to be isomorphic, and I want to be allowed to perform arithmetic operations without any proof obligations regarding the absence of overflows. How can I do this? My suggestion for this scenario is to adopt the axiom isInt(j) <-> True. (The precondition of machine addition i1 + i2 would be isInt(view i1 + view i2), or just isInt(i1 + i2) if we are allowed to omit the coercion from int to integer.) Do you have a different way in mind?