C++ Logo

std-proposals

Advanced search

Re: [std-proposals] D3666R0 Bit-precise integers

From: Julien Villemure-Fréchette <julien.villemure_at_[hidden]>
Date: Tue, 02 Sep 2025 15:56:02 -0400
> That is the mathematically correct answer for a modular arithmetic ring.

But the signed integer types are not intended to model modular arithmetic on a finite ring of characteristic 2^N. An operation "a + b" is meant to express the mathematical operation on the integers, not modular arithmetic.

Signed integers and their operations are intended to model the integers (Z) with a representation that is suitable to be directly operated on by the ALU. Since the set of integers is infinite, but the ALU can only operate on fixed inputs, there is necessarily a limited subset of the integers [-2^(N-1) .. 2^(N-1) - 1] that can be represented and limited subsets of pairs of integers that can be added, subtracted, multiplied or divided. i.e. the result of "a + b" performed by the ALU is the same as its mathematical meaning iff
"(a, b)€{(x, y): x + y € [-2^(N-1)..2^(N-1) - 1]}"
The signed integers are made to represent the most common way of doing arithmetic on integers and does so in such a way that it can be done directly in the ALU.

Under the constraints stated above (i.e. the domain of the binary operations is limited), the operations on the signed integer types do actually preserve mathematical properties of the integers (associativity, commutativity, distributivity, etc). As such, under these assumptions (and possibly other information deductible from surrounding code) the compiler can rearrange integer operands around arithmetic operations by applying a transformation permitted by these properties (and only if this would not result in an overflow in the rearranged operands).

In mathematical terms, this is the same as stating a premise that for each signed integer arithmetic operations, the operands are within the domain permitted by that operation. If a signed integer overflow actually occurs in an expression in the source code, then this instance of the program is actually proving that this arithmetic expression has a pair of operands "(a, b)" which is outside the domain of the operator applied to those. But this is in contradiction with the premise that "(a, b)" is with the domain of the operation: the program reaches a contradiction. The C++ term for a contradiction is Undefined Behavior and the outcome of it is essentially the same as reaching a contradiction in a proof: you might as well give up on trying to infer more statements as they are likely logically invalid (in C++, have the program crash immediately), or you keep on trying to infer more statements to try and gain insights how you could build up an abstract system like building the real number line with Cantor's set theory and later find a solution to paradoxes involved (in C++, keep running in a best effort to perform as much computations as it can, but exclude those that depend on the UB).


On September 2, 2025 10:47:14 a.m. EDT, connor horman via Std-Proposals <std-proposals_at_[hidden]> wrote:
>On Tue, 2 Sept 2025 at 10:14, David Brown via Std-Proposals <
>std-proposals_at_[hidden]> wrote:
>
>> On 02/09/2025 15:38, Marcin Jaczewski wrote:
>> > wt., 2 wrz 2025 o 14:49 David Brown via Std-Proposals
>> > <std-proposals_at_[hidden]> napisał(a):
>> >>
>> >> On 02/09/2025 14:24, Hans Åberg via Std-Proposals wrote:
>> >>>
>> >>>
>> >>>> On 2 Sep 2025, at 14:14, Jan Schultke <janschultke_at_[hidden]>
>> wrote:
>> >>>>
>> >>>> You seem to be confusing some mostly unrelated concepts.
>> >>>>
>> >>>>>> 1. C does not allow _BitInt(1); should C++ to make generic
>> programming
>> >>>>>> more comfortable?
>> >>>>>
>> >>>>> The ring ℤ/2ℤ of integers modulo 2, also a field, is isomorphic to
>> the Boolean ring 𝔹 having exclusive or as addition and logical conjunction
>> as multiplication.
>> >>>>>
>> >>>>> If bool 1+1 is defined to 0, then it is already in C++.
>> >>>>
>> >>>> Whether there is some other C++ thing that works mathematically the
>> >>>> same doesn't say anything about whether _BitInt(1) is valid or should
>> >>>> be valid. The issue is regarding a specific type.
>> >>>
>> >>> It could have been defined to be the same as bool.
>> >>
>> >> No, it could not. _BitInt(1), if it is to exist, has the two values -1
>> >> and 0. Like all signed integer types, arithmetic overflow on it is
>> >> undefined, and like all _BitInt types, there is no integer promotion.
>> >> Thus for _BitInt(1), (-1) + (-1) is UB.
>> >>
>> >
>> > Do we need UB here? This is not `int` and we could have all operations
>> > defined. What would we gain from it?
>>
>> Do we /need/ UB on signed arithmetic overflow? No. Do we /want/ UB on
>> signed arithmetic overflow? Yes, IMHO. I am of the opinion that it
>> makes no sense to add two negative numbers and end up with a positive
>> number. There are very, very few situations where wrapping behaviour on
>> signed integer arithmetic is helpful - making it defined as wrapping is
>> simply saying that the language will pick a nonsensical result that can
>> lead to bugs and confusion, limit optimisations and debugging, and
>> cannot possibly give you a mathematically correct answer, all in the
>> name of claiming to avoid undefined behaviour.
>>
>That is the mathematically correct answer for a modular arithmetic ring. In
>fact, as far as I can tell, any other result (other than an impossible one)
>is mathematically incorrect, because they are not invertible or associative
>(pick one or more, saturation is not invertible, trapping or other
>undefined behaviour shenanigans are none of the above). Whether or not it
>limits optimizations or debugging is another story, but it does produce the
>most mathematically correct answer. In fact, a good number of mathematical
>proofs do not apply to signed integers in C or C++, because they rely on
>the additive inverse. There are also optimizations that are not available
>to users (though compilers that define overflow as wrapping will have
>access to them). Namely, division through modular inverse requires all odd
>numbers to have a multiplicative inverse, which is only the case if the
>type forms a ring.
>
>Remember, if you first /define/ a behaviour in the standards, you are
>> stuck with it. Leave it as UB, and the compiler can do what it wants -
>> perhaps helped by developer choices. Thus in gcc, you can choose to
>> give signed integer arithmetic modulo behaviour by using the "-fwrapv"
>> flag. You can choose to have the compiler generate run-time checks and
>> stop the program with an error message on overflow using the
>> "-fsanitize=signed-integer-overflow" flag. A compiler for a DSP could
>> choose to use saturating arithmetic. A C interpreter could choose to
>> use arbitrary precision arithmetic and give a run-time error for out of
>> range values when assigning the result to a variable. A C++ compiler
>> could have an option to throw an exception on overflow. And of course C
>> and C++ compilers can optimise code on the assumption that overflow,
>> being UB, does not occur, leading to smaller and faster code in some
>> situations (typically in loops, and also noticeable in some kinds of
>> array indexing on 64-bit machines).
>>
>> But if the standards say overflow is wrapping, you are stuck with it.
>> Your code gives results that are almost certainly incorrect and
>> unhelpful on overflow, but your tools can't help you find your mistake.
>
>
>
>
>> This is why the C and C++ standards committees have both refused to
>> define the behaviour of arithmetic overflow even when they have both
>> restricted the latest language versions to requiring two's complement
>> representation of signed integers.
>>
>> In C23, signed integer arithmetic overflow with _BitInt types is UB,
>> just like for other signed integer types. That makes perfect sense to
>> me. Hopefully the same will apply to C++23 _BitInt.
>>
>
>> (Sorry for the long and slightly ranting answer to a two line question!)
>>
>> --
>> Std-Proposals mailing list
>> Std-Proposals_at_[hidden]
>> https://lists.isocpp.org/mailman/listinfo.cgi/std-proposals
>>

Received on 2025-09-02 19:56:15