Stream: Coq devs & plugin devs

Topic: Unsigned vs signed integers

Thomas Letan (Dec 05 2019 at 16:10):

Is there any reason why the int type (primitive integers) is actually for unsigned integers?

Ana de Almeida Borges (Nov 17 2020 at 10:34):

I second this question. (See also https://github.com/coq/coq/issues/12109) Assuming there is no deep reason, is someone working on extending the Coq primitive integers to actual signed integers? And if there isn't, would there be interest in this?

My team wants to use primitive signed integers and we're probably going to come up with a way of doing it, more or less hacky. We would be glad to do it in a way that actually improves Coq for everyone.

Paolo Giarrusso (Nov 17 2020 at 11:52):

I'd also motion for fixing the name, beyond all other things. A bit disappointed nobody noticed (me included), especially since this was a recent addition.

Guillaume Melquiond (Nov 17 2020 at 12:35):

Fixing the name is pointless. This is modulo arithmetic. Whether the type is signed or not, the results will be absolutely identical for addition, subtraction, multiplication, and so on. The only operations that actually care about signedness are comparison and division. So, it would be much more productive to just add a signed comparison and a signed division.

Paolo Giarrusso (Nov 17 2020 at 13:00):

What about shift and sign-extension (conversion to Z)?

Cyril Cohen (Nov 17 2020 at 13:00):

Guillaume Melquiond said:

Fixing the name is pointless. This is modulo arithmetic. Whether the type is signed or not, the results will be absolutely identical for addition, subtraction, multiplication, and so on. The only operations that actually care about signedness are comparison and division. So, it would be much more productive to just add a signed comparison and a signed division.

This is not entirely true, the interpretation from and to Z would also differ.

Cyril Cohen (Nov 17 2020 at 13:00):

And the printing...

Cyril Cohen (Nov 17 2020 at 13:01):

Actually, it would be more accurate to say that only the addition, subtraction and multiplication are the same....

Cyril Cohen (Nov 17 2020 at 13:01):

(i.e. the ring structure)

Paolo Giarrusso (Nov 17 2020 at 13:02):

uh, https://coq.github.io/doc/v8.12/refman/changes.html#id420 claims that this was the UInt63 module?

Paolo Giarrusso (Nov 17 2020 at 13:03):

but https://coq.github.io/doc/v8.12/refman/language/core/primitive.html#primitive-integers suggests that Coq's Int maps to OCaml UInt.

Karl Palmskog (Nov 17 2020 at 13:06):

the UInt63 ref might be to this file: https://github.com/coq/coq/blob/master/kernel/uint63.mli

Guillaume Melquiond (Nov 17 2020 at 15:34):

Cyril Cohen said:

(i.e. the ring structure)

That is a rather restrictive view. There are also: clz (head0), ctz (tail0), and, or, xor, lsl, lsr, funnel shifter (addmuldiv), sqrt. But I agree that conversion to Z would be different (and thus printing too).

Ana de Almeida Borges (Nov 24 2020 at 12:28):

I think there are at least two options:

1. Define signed comparison, division, etc by, for example, taking [0, max_int/2] as the positive numbers and ]max_int/2, max_int] as the negative numbers.
2. Actually use the OCaml integers, instead of only OCaml's unsigned integers.

As far as I can tell, Option 1 is more high-level, possibly easier, but less efficient, while Option 2 would imply increasing the kernel, but it would then allow for efficient extraction to Ocaml's int, including int functions such as comparison.

Am I accurately describing reality? Which of these options would you prefer?

Guillaume Melquiond (Nov 24 2020 at 13:30):

I am not sure why you say that Option 1 is higher level. I would call it lower level, as it is much closer to the actual hardware. Most (if not all) processors do not have separate signed and unsigned registers. They do not have signed and unsigned additions. By the way, even for OCaml, the situation is not that clear cut. For example, the Int32 module provides both a signed division div and an unsigned one unsigned_div (and similarly for comparison).

Paolo Giarrusso (Nov 24 2020 at 16:29):

I think processors have at least distinct (1) shifts (2) number extensions — but that's not so important.

Paolo Giarrusso (Nov 24 2020 at 16:30):

the efficiency question is important

Paolo Giarrusso (Nov 24 2020 at 16:31):

@Guillaume Melquiond can one make primitive integers (and their axiom) match standard processors, and then do the remaining reasoning in Coq?

Paolo Giarrusso (Nov 24 2020 at 16:32):

for shared operations, instead of having 2 copies of the same axioms, maybe one could have only 1 copy (say, for addition), and some "adapters".

Paolo Giarrusso (Nov 24 2020 at 16:34):

so one axiom on "primitive addition" can imply theorems both about "Coq unsigned integers" (today) and "Coq signed integers".

Paolo Giarrusso (Nov 24 2020 at 16:35):

I realize this sounds like option 1, except this should not affect efficiency of the actual code.

Paolo Giarrusso (Nov 24 2020 at 16:37):

OTOH, @Guillaume Melquiond, signed and unsigned comparisons _are_ distinct operations even in assembly, IIUC (on x86 there's a single operation, but you test different flags for the signed and unsigned cases)

Last updated: Oct 13 2024 at 01:02 UTC