Mikkel Milo (Apr 15 2021 at 12:33): Mikkel Milo (Apr 15 2021 at 12:33):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 unsigned integers using Cyclic? If not, would this be relatively straightforward, or could there be any issues? I haven't worked with Cyclic before.
Bas Spitters (Apr 15 2021 at 12:52):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
Ana de Almeida Borges (Apr 15 2021 at 23:04):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.
Bas Spitters (Apr 16 2021 at 07:02):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 ...
Ana de Almeida Borges (Apr 16 2021 at 12:07):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.
Bas Spitters (Apr 16 2021 at 12:11):Reopened
Ana de Almeida Borges (Apr 16 2021 at 12:19):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.
Ana de Almeida Borges (Apr 16 2021 at 12:20):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
Bas Spitters (Apr 16 2021 at 12:31):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.
Thomas Letan (Apr 16 2021 at 12:44):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
Thomas Letan (Apr 16 2021 at 12:45):also OCaml does not have usigned integers (no uint)
Thomas Letan (Apr 16 2021 at 12:46):Int63 is a signed 63bit unsigned integer implemented using a 63bit signed integer, as far as I know
Ana de Almeida Borges (Apr 16 2021 at 12:50):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.
Bas Spitters (Apr 16 2021 at 13:11):@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.
Alix Trieu (Apr 16 2021 at 13:20):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 ?
Guillaume Claret (Apr 16 2021 at 13:23):Thomas Letan said:
Int63is a signed 63bit unsigned integer implemented using a 63bit signed integer, as far as I know
You mean "is a 63bit unsigned integer"?
Guillaume Claret (Apr 16 2021 at 13:24):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.
Guillaume Claret (Apr 16 2021 at 13:26):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
Alix Trieu (Apr 16 2021 at 13:27):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.
Guillaume Claret (Apr 16 2021 at 13:27):Ah OK, nice, I did not know about that!
Guillaume Claret (Apr 16 2021 at 13:30):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/
Guillaume Claret (Apr 16 2021 at 13:32):the open-source license is GPL though if I understand correctly, so if one wants to reuse it has to be GPL too
Guillaume Claret (Apr 16 2021 at 13:32):the files for flocq and menhir are LGPL, and runtime/ is BSD
Mikkel Milo (Apr 16 2021 at 13:39):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.
Bas Spitters (Apr 16 2021 at 14:08):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?
Alix Trieu (Apr 16 2021 at 14:17):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.
Guillaume Claret (Apr 16 2021 at 14:26):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.
Guillaume Claret (Apr 16 2021 at 14:26):(if that was not the case, I would not see the point of having LGPL in addition to GPL)
Bas Spitters (Apr 16 2021 at 14:28):And even the status of LGPL for Coq proofs has not been clarified, as far as I understand...
Bas Spitters (Apr 16 2021 at 17:34):@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 )
Michael Soegtrop (Apr 17 2021 at 07:38):@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.
Bas Spitters (Apr 17 2021 at 08:02):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.
Bas Spitters (Apr 19 2021 at 10:32):@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.
Guillaume Melquiond (Apr 19 2021 at 11:51):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.
Michael Soegtrop (Apr 19 2021 at 12:04):@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.
Michael Soegtrop (Apr 19 2021 at 12:05):When I work with the CompCert integers, I convert as quickly as possible to Z arithmetic by proving that things can't overflow.
Bas Spitters (Apr 19 2021 at 12:34):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:
Michael Soegtrop (Apr 19 2021 at 13:02):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)
Michael Soegtrop (Apr 19 2021 at 13:07):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.
Michael Soegtrop (Apr 19 2021 at 13:07):In the end both should be equivalent.
Bas Spitters (Apr 19 2021 at 13:20):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.
Michael Soegtrop (Apr 19 2021 at 13:31):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.
Bas Spitters (Apr 19 2021 at 13:33):But don't we expect these to be useful for Cyclic 31 and Cyclic 63 too ?
Laurent Théry (Apr 19 2021 at 13:36):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.
Bas Spitters (Apr 19 2021 at 13:47):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?
Laurent Théry (Apr 19 2021 at 13:54):@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?
Michael Soegtrop (Apr 19 2021 at 13:54):IMHO efficient computation is a must.
Bas Spitters (Apr 19 2021 at 14:00):@Laurent Théry From the thread above, it looks like there are at least 5 use cases:
They all have the equivalent implementations. Perhaps, we can limit code duplication.
Laurent Théry (Apr 19 2021 at 14:06):I guess hacspec should be very close to compcert do you need fast computation too?
Bas Spitters (Apr 19 2021 at 14:23):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.
Bas Spitters (May 12 2021 at 19:22):Thanks to Xavier, the compcert integers are now under LGPL :tada:
https://github.com/AbsInt/CompCert/releases/tag/v3.9
Bas Spitters (Feb 08 2022 at 11:05):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 ...
Bas Spitters (Feb 09 2022 at 11:43):@Jason Gross @Pierre-Yves Strub @Vincent Laporte or others?
Are there any opportunities for synergy here?
MackieLoeffel (Feb 09 2022 at 15:30):There is also https://gitlab.mpi-sws.org/iris/bitvector (which I wrote because I was not happy with any of the other libraries).
Karl Palmskog (Feb 09 2022 at 15:33):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:
Pierre-Yves Strub (Feb 10 2022 at 19:39):Hi. I personally do not have any cycle left for this task :/
Last updated: Oct 13 2024 at 01:02 UTC