## Stream: Miscellaneous

### Topic: What would be a theory for dealing with n-bits arithmetics ?

#### 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 $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$).

#### 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):

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

#### 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: Jul 13 2024 at 02:02 UTC