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.
there is a cottage industry of Coq word libraries. One example that is in the Coq Platform: https://github.com/jasmin-lang/coqword
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.
I am not actually surprised, but I was hoping I could just use all the lemmas from some algebra textbook on machine words
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 , ).
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
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"
Can't one define three commutative rings on machine integers - one for arithmetic, one for bitwise operations (| & ~
) and one for boolean operations (|| && !
) ?
I thought maybe this process of formalizing word sized integers is as mature as formalizing normal integers (mathematics wise)
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.
hmm, I think CompCert uses only LGPL for the open source part nowadays? Or are you using an old CompCert?
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).
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.
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.
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.
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 ?
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