Hey there, so Coq.Numbers.Cyclic has implementations of Int63 and Int31, which to my understanding represents signed 64-bit and 32-bit integers, respectively.

But has there been any work in making *un*signed integers using Cyclic? If not, would this be relatively straightforward, or could there be any issues? I haven't worked with Cyclic before.

To elaborate, the unsigned integers are also available in ocaml, so there seems to be a good reason for having them in Coq. Quick googling:

https://github.com/andrenth/ocaml-stdint

https://github.com/ocamllabs/ocaml-integers

https://ocamllabs.io/ocaml-ctypes/Unsigned.html

As of Coq 8.13, `Int63`

are actually unsigned 63-bit integers, and AFAIK `Int31`

is deprecated. The names are misleading. A PR introducing signed primitive integers is already merged in master, and there is an in-progress PR to rename `Int63`

to `Uint63`

(although it's been a while since I last worked on it). Coq 8.14 should have both versions with saner names.

But @Thomas Letan was asking for using the extra bit. I.e. UInt64. Is this now available?

BTW @lthms for wasm verification there is

https://github.com/WasmCert/WasmCert-Coq

in development

@Ana de Almeida Borges is my understanding correct that your work should now faithfully model ocaml's usigned integers?

In fact, we'd like to model rusts u64, but my hope is that they are all the same ...

But @Thomas Letan was asking for using the extra bit. I.e. UInt64. Is this now available?

It's not. Arguably his issue should not have been closed.

Reopened

is my understanding correct that your work should now faithfully model ocaml's usigned integers?

I didn't change anything related to unsigned integers, just added extra stuff for signed ones. I'm not completely sure of this, but as far as I understand, Coq unsigned integers are just the subset of non-negative ocaml signed integers, whence the missing bit.

And then the Coq signed integers we introduced are just Coq's unsigned integers with the first bit interpreted as a sign, so `Sint63.max_int = 2^62 - 1`

I would hope that we can just write

```
Definition size := 64%nat.
```

in https://coq.inria.fr/library/Coq.Numbers.Cyclic.Int63.Int63.html, but someone most have looked at the already, and can tell me whether that would work.

Ana de Almeida Borges said:

is my understanding correct that your work should now faithfully model ocaml's usigned integers?

I didn't change anything related to unsigned integers, just added extra stuff for signed ones. I'm not completely sure of this, but as far as I understand, Coq unsigned integers are just the subset of non-negative ocaml signed integers, whence the missing bit.

My undersanding is a bit different. The missing bit is used by the OCaml GC

also OCaml does not have usigned integers (no `uint`

)

`Int63`

is a signed 63bit unsigned integer implemented using a 63bit signed integer, as far as I know

Bas Spitters said:

I would hope that we can just write

`Definition size := 64%nat.`

in https://coq.inria.fr/library/Coq.Numbers.Cyclic.Int63.Int63.html, but someone most have looked at the already, and can tell me whether that would work.

It wouldn't. The type still only has 2^63 possible values, so changing `size`

would just confuse everything. For example, it would no longer be the case that `to_Z max_int = wB - 1`

. Adding more bits would have to be done at the level of the kernel. Maybe messing around with it here instead.

@Ana de Almeida Borges I don't want to change the kernel or native compute. I'd like to get a good model for the uint in rust/wasm, and if I understand the links I posted above correctly, ocaml.

I haven't looked at the ocaml libraries in detail. It looks like some of them do not use the extra bit for the GC.

I'm wondering, if you're looking for a formalization of uint, why not use the integers library from compcert https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v or something else ?

Thomas Letan said:

`Int63`

is a signed 63bit unsigned integer implemented using a 63bit signed integer, as far as I know

You mean "is a 63bit unsigned integer"?

Alix Trieu said:

I'm wondering, if you're looking for a formalization of uint, why not use the integers library from compcert https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v or something else ?

The license of CompCert is not open-source. That is the main limitation I have heard to re-use parts of CompCert.

maybe they could open-source the parts which can be re-used, as many people would like to re-use, and keep the rest (what is C related) with a restricted license

Guillaume Claret said:

maybe they could open-source the parts which can be re-used, as many people would like to and keep the rest (what is C related) with a restricted license

Some parts are already open source.

Ah OK, nice, I did not know about that!

so as per https://github.com/AbsInt/CompCert/blob/master/LICENSE , the dual licensing (non-free / open-source) includes the files in `lib/`

and `common/`

the open-source license is GPL though if I understand correctly, so if one wants to reuse it has to be GPL too

the files for flocq and menhir are LGPL, and `runtime/`

is BSD

Alix Trieu said:

I'm wondering, if you're looking for a formalization of uint, why not use the integers library from compcert https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v or something else ?

At a glance, this looks like what I need, since I can choose the wordsize to what I need (e.g. 32, 64). It's interesting that the `int`

type is used for both signed and unsigned integers, and signedness is only interpreted through functions from/to `Z`

, rather than having two types, say `uint`

and `sint`

.

Thanks @Alix Trieu , I think @Guillaume Claret makes a good point. It will be hard to combine with hacspec, which is MIT.

Or am I mistaken?

I am not a lawyer, but my understanding is that only modifications must also be kept GPL licensed, if you only use it as a *library*, i don't see why the rest can't be in whatever license you want.

Alix Trieu said:

I am not a lawyer, but my understanding is that only modifications must also be kept GPL licensed, if you only use it as a

library, i don't see why the rest can't be in whatever license you want.

This is the main difference between GPL and LGPL. Even if you use it as a library, it has to be GPL too, as I understand.

(if that was not the case, I would not see the point of having LGPL in addition to GPL)

And even the status of LGPL for Coq proofs has not been clarified, as far as I understand...

@Xavier Leroy What would be the best way to make these unbounded integers available to the wider Coq community ?

Any chance to get them included in e.g. the platform ?

I have a general understanding of why compcert is using a non-standard license, but perhaps it is possible to release these parts with a more compatible license. It seems like a duplication of work in the coq stdlib, but I could be wrong.

(Cc: @Michael Soegtrop )

@Bas Spitters : they are included in the Platform. What would help for some people though would be to have a proper way to install only the GPL part of CompCert. I had this in the 8.12 Coq Platform but patching the make files is a bit of work and I don't want to get it wrong.

Thanks! Yes, that might help for some.

However, I'm not sure it would be useful for the use case @Thomas Letan has in mind. A formalization of wasm, such as https://github.com/WasmCert/WasmCert-Coq or the one we're currently working on: hac-spec.

Both are under MIT. I don't know what the intention of the compcert developers is with the GPL license.

Maybe they are willing to have a more permissive license, one recommended by the coq-community.

@Guillaume Melquiond (or perhaps @Maxime Dénès ), what would be the best way to relate the compcert numbers with the machine integers in of the stdlib. It would be nice to avoid duplication, if possible.

I would simply exhibit a bijection between both types and prove that the various arithmetic operations are morphisms for it. But there is nothing specific about Coq or CompCert here, so I am not sure to fully understand the question.

@Bas Spitters : I would say that the CompCert integers and Coq's machine integers are fairly unrelated since they have a different bit size (8/16/32/64 vs 63). The operations of the CompCert integers are defined based on standard library Z modulo arithmetic. The CompCert integers would more relate to the standard library cyclic numbers than to the machine integers.

When I work with the CompCert integers, I convert as quickly as possible to Z arithmetic by proving that things can't overflow.

I was talking about the cyclic numbers (some people use "machine arithmetic" for that). I understand people use "machine integers" for the BigInts build out of that.

So, let me try to rephrase:

- Are the compcert integers supposed to be isomorphic to the 64bits Cyclic numbers ?
- If so, would it make sense to add such a library to the coq stdlib. E.g. for the use case Thomas mentioned in the issue above by @Ana de Almeida Borges

@Guillaume Melquiond does that clarify ?

I think the definitions are slightly different. Afair the cyclic integers have a modulo equality while the CompCert integers are Z numbers with a proof that they are in range (unsigned) and Leibnitz equality on the Z part. I am not sure what practical implications this has - the CompCert integers are easy to work with, not sure about the cyclic integers.

But I guess one could use modulo equality to define an isomophism between the two.

See

(https://github.com/AbsInt/CompCert/blob/45af10b3ac30f8e4f5904824259b04df17e1c6b1/lib/Integers.v#L102)

(https://github.com/AbsInt/CompCert/blob/45af10b3ac30f8e4f5904824259b04df17e1c6b1/lib/Integers.v#L131)

(https://github.com/AbsInt/CompCert/blob/45af10b3ac30f8e4f5904824259b04df17e1c6b1/lib/Integers.v#L173)

I did give the cyclic integers a try in the past and found them harder to work with, but this might be because I was less experienced then or because CompCert has a richer set of lemmas. But in the end usually one treats C integers as anti-abstraction of Z with a limited range and proves that the range is not exceeded and only rarely makes use of the cyclic feature. E.g. for most C programs it wouldn't make a difference if arithmetic would be defined such that integer overflows lead to an error (like integer division by 0 does). So it might be that the CompCert definition is more natural, but I really can't tell.

In the end both should be equivalent.

So, should either of them be in the stdlib? Or would a package in platform be a better solution.

You suggested before to have a separate package for the GPL part of Compcert.

I'm inclined to go with the Cyclic integers as it gives less of a hassle with licenses.

It might be that *a lot* of lemmas are missing from the cyclic integers to be usable in practice, especially around shifting and bit arithmetic - say that if you right shift and bit-and you get the same as if you bit-and and the right shift. But of cause one could add these.

But don't we expect these to be useful for Cyclic 31 and Cyclic 63 too ?

the `int63`

(historically the `int31`

) were there just to be the base case of our cyclic number construction to have a way to compute quickly with arbitrary precision arithmetic in Coq. There were not meant to be a library for unsigned integer.

Thanks @Laurent Théry , so what would be the best way forward?

I believe you have another version of these modulo integers in your coqprime library, don't you?

@Bas Spitters yes and no, there is a variant of the same construction to get arbirtrary precision modulo arithmetic.

Coming to the initial question, yes an integration of an arbitrary precision OCaml library could replace Cycliic. For a library of integer arithmetic, do you want it to compute in Coq efficently too?

IMHO efficient computation is a must.

@Laurent Théry From the thread above, it looks like there are at least 5 use cases:

- compcert
- cyclic integers in the stdlib
- coqprime
- wasm (Thomas) library in progress?
- hacspec (rust) we're trying to pick one of the above libraries to target.

They all have the equivalent implementations. Perhaps, we can limit code duplication.

I guess hacspec should be very close to compcert do you need fast computation too?

hacspec is aimed at specification, so fast computation is not immediately necessary, but of course, being a specification, at some point one might want to refine to fast computation. We'd like to connect to fiat-crypto for that, but that builds on coq-prime ;-)

I also think wasm should be similar to compcert.

Thanks to Xavier, the compcert integers are now under LGPL :tada:

https://github.com/AbsInt/CompCert/releases/tag/v3.9

There are a few other libraries:

https://github.com/jasmin-lang/coqword

https://github.com/mit-plv/coqutil/tree/master/src/coqutil/Word

Maybe it is worth coordinating more ...

@Jason Gross @Pierre-Yves Strub @Vincent Laporte or others?

Are there any opportunities for synergy here?

There is also https://gitlab.mpi-sws.org/iris/bitvector (which I wrote because I was not happy with any of the other libraries).

recall also: https://coq.discourse.group/t/best-practices-for-machine-level-representation-of-numbers-and-bitwise-operations/482/2

which mentions these additional ones:

- https://github.com/coq-community/bits
- https://github.com/mit-plv/bbv
- https://github.com/ekiciburak/bitvector/tree/pxtp2019

Hi. I personally do not have any cycle left for this task :/

Last updated: Jun 18 2024 at 21:01 UTC