walker (Nov 17 2022 at 09:33): walker (Nov 17 2022 at 09:33):I checked some stuff related to ZArith and was wondering, what would an abstract model for working with singed integers/ and unsigned integerts of arbitrary n-bits (with add substract multiply divide and modulu).
I was thinking a ring but that does not account for the divide and the modulu operator.
Karl Palmskog (Nov 17 2022 at 10:11):there is a cottage industry of Coq word libraries. One example that is in the Coq Platform: https://github.com/jasmin-lang/coqword
walker (Nov 17 2022 at 10:32):mmm, it doesn't look like a machine word would map cleanly to any math structure I am familiar with. I didn't see all the details, but they look like they are using ring structures for some parts.
walker (Nov 17 2022 at 10:34):I am not actually surprised, but I was hoping I could just use all the lemmas from some algebra textbook on machine words
James Wood (Nov 17 2022 at 11:35):They're commutative rings, and as far as I know, the next interesting structure people care about related to modular arithmetic is that, at prime order, they form fields (finite fields). However, your rings are going to be of order , so mostly not prime, and the division you get from finite fields is a very different operation to integer division (for example, in , ).
Paolo Giarrusso (Nov 17 2022 at 13:02):What kind of usecase do you have in mind? If you're verifying C, sometimes you need to show that "bitmask operations" let you encode categorical products of bitfields
walker (Nov 17 2022 at 13:10):I wasn't having anything in mind in particular. I was just thinking of verifying C-like integer operations in a style similar to that of nat.... I am not sure what is "categorical products"
Michael Soegtrop (Nov 17 2022 at 13:22):Can't one define three commutative rings on machine integers - one for arithmetic, one for bitwise operations (| & ~) and one for boolean operations (|| && !) ?
walker (Nov 17 2022 at 13:52):I thought maybe this process of formalizing word sized integers is as mature as formalizing normal integers (mathematics wise)
Michael Soegtrop (Nov 17 2022 at 13:59):I would say it is as mature but the resulting structure is not generic, not clean and not nice.
I btw. mostly use the CompCert definitions (which are GPL) which are quite complete - the main downside here is that the word size is a module parameter.
Karl Palmskog (Nov 17 2022 at 14:32):hmm, I think CompCert uses only LGPL for the open source part nowadays? Or are you using an old CompCert?
James Wood (Nov 17 2022 at 14:52):Michael Soegtrop said:
Can't one define three commutative rings on machine integers - one for arithmetic, one for bitwise operations (
| & ~) and one for boolean operations (|| && !) ?
! can't be involutive on all non-zero values (unless you quotient them all together, but in that case your commutative ring is really over just the Booleans).
James Wood (Nov 17 2022 at 14:54):Actually, I don't think even ~ (or ! on Booleans) can be an additive inverse. Only xor has inverses, and the inverse operation there is just identity.
Paolo Giarrusso (Nov 17 2022 at 18:51):When I say "categorical products", I just mean that e.g. pair(a, b) := a << 4 || (b & 0xf) is a pairing function as long as a and b are within certain ranges.
Bas Spitters (Nov 18 2022 at 08:47):Yes, that part of compcert now has a more permissive license, precisely to make it more available to other projects.
It would be interesting to have a better understanding of how these libraries related. I believe we collected three or four of them at some point.
Karl Palmskog (Nov 18 2022 at 08:52): walker (Nov 18 2022 at 08:54):Bas Spitters said:
Yes, that part of compcert now has a more permissive license, precisely to make it more available to other projects.
It would be interesting to have a better understanding of how these libraries related. I believe we collected three or four of them at some point.
where can I find the permessive version ?
Karl Palmskog (Nov 18 2022 at 08:55):See "Licensing and distribution" here: https://github.com/AbsInt/CompCert/releases/tag/v3.9 (first version with LGPL open source parts)
Last updated: Sep 25 2023 at 12:01 UTC