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 $2^n$, so mostly not prime, and the division you get from finite fields is a very different operation to integer division (for example, in $\mathbb{Z}_5$, $2/4 = 3$).

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: Jun 10 2023 at 06:31 UTC