3 ms·

I believe the main issue lies in most programming languages lacking theorem proving capabilities to prove the safety of integer operations. The safety conditio

by amavect 3mo ago

I believe the main issue lies in most programming languages lacking theorem proving capabilities to prove the safety of integer operations. The safety conditions for unsigned arithmetic: Ensure y+x ≤ INT_MAX. If x ≤ UINT_MAX-y, then x+y evaluates correctly: ∀x∀y(x ≤ UINT_MAX-y → ∃z(z = y+x)) Ensure y-x ≤ INT_MAX. If x≤y, then y-x evaluates correctly: ∀x∀y(x≤y → ∃z(z = y-x)) The safety conditions for signed arithmetic: Ensure INT_MIN ≤ y+x and y+x ≤ INT_MAX. To avoid overflow or underflow, first compare x to 0. In the case x≤0, INT_MIN-x cannot underflow, and y+x cannot overflow. If y compares greater than INT_MIN-x, then y+x evaluates correctly. In the case 0≤x, then INT_MAX-x cannot overflow, and y+x cannot underflow. And if y compares less than INT_MAX-x, then y+x evaluates correctly. ∀x∀y((x≤0 ∧ INT_MIN-x≤y)∨(0≤x ∧ y≤INT_MAX-x) → ∃z(z = y-x)) Ensure INT_MIN ≤ y-x and y-x ≤ INT_MAX. To avoid overflow or underflow, first compare x to 0. In the case 0≤x, INT_MIN+x cannot underflow, and y-x cannot overflow. If y compares greater than INT_MIN+x, then y-x evaluates correctly. In the case x≤0, INT_MAX+x cannot overflow, and y-x cannot underflow. If y compares less than INT_MAX+x, then y-x evaluates correctly. ∀x∀y((0≤x ∧ INT_MIN-x≤y)∨(x≤0 ∧ y≤INT_MAX+x) → ∃z(z = y-x)) The programmers that prefer unsigned arithmetic intuitively feel the greater simplicity compared to signed integers, but without any theorem proving, I agree that your assumption of small integers strongly supports signed integers.

derdi 3mo ago
What do you mean by notation like: Ensure y+x ≤ INT_MAX. Is this supposed to be a precondition? Why would I want this precondition when using unsigned arithmetic?
- amavect 3mo ago
  I included that to try to explain the symbol soup that correctly encodes the preconditions (the ∀ lines). I intended that to mean "I need to make sure that y+x doesn't overflow", even that unsigned arithmetic cannot express that precondition in that way, as you point out. From there, derive y ≤ INT_MAX-x as the actual precondition for unsigned addition. I forgot that "ensure" actually means something in some programming languages, sorry for the confusion. More simply put, unsigned addition needs to check that y+x doesn't overflow, while signed addition needs to check that y+x doesn't overflow and doesn't underflow. So, unsigned arithmetic has a simpler precondition that would win a technical debate on whether to use signed or unsigned arithmetic, but since most programming languages lack theorem proving, signed arithmetic wins on the small integer assumption.
  - kazinator 3mo ago
    In two's complement, calculating the overflow for addition is nearly exactly as complex as calculating carry for unsigned arithmetic. Various versions of the Motorola 68000 programmer's manuals have a table which succinctly shows the Boolean formulas for calculating the flags for various operations. In the following document it is Table 3-18. Integer Unit Condition Code Computations: https://www.nxp.com/docs/en/reference-manual/M68000PRM.pdf https://www.nxp.com/docs/en/reference-manual/M68000PRM.pdf The ADD operation is in the second row of the table. See how in the right column, the calculation of C (carry out of highest bit) and V (overflow) have about the same complexity. V has only two "not" inversions compared to C's three, but otherwise both have six operands reduced via five "and" or "or" operations. C is a sum of two three-term products, V is a sum of three two-term products. These calculations assume that we perform the addition as unsigned, and so we then have access to all three operands: the S, D, and R (source, destination and result). (That terminology is specific to the MC68K whose instruction set doesn't support the result going to a third operand which is not one of the two input operands.) All the difficulties come from the higher level language semantics that don't provide a way to safely perform an overflowing operation and then detect overflow from a calculation applied to the two inputs and result. I.e. some assembly-language-like "higher level" languages make things worse than assembly language, for the sake of abstraction and portability.
    - amavect 3mo ago
      Cool!! I really like how the overflow condition reads. "When the source and destination have the same sign, but the result a different sign, then signed addition overflows." x86 has SETC/SETNC and SETO/SETNO to pull the carry/overflow bits out of the status register. u+: ADD then SETNC u-: CMP then SETNC s+: ADD then SETNO s-: CMP then SETNO C23 adds checked arithmetic, and gcc implements them as built-in, generating SETO/SETNO. I can't find a way to generate SETNO otherwise. https://godbolt.org/z/4EjecdW1d https://godbolt.org/z/4EjecdW1d #include <stdint.h> #include <stdckdint.h> int add_u(unsigned x, unsigned y){ return x <= ~y; } int sub_u(unsigned x, unsigned y) { return x <= y; } int add_u2(unsigned x, unsigned y){ return !ckd_add(&x, x, y); } int sub_u2(unsigned x, unsigned y) { return !ckd_sub(&x, x, y); } int add_s(int x, int y){ return !ckd_add(&x, x, y); } int sub_s(int x, int y) { return !ckd_sub(&x, x, y); } Now, I the difficulty you talk about goes deeper than high level language semantics. Math and predicate logic can't easily talk about a carry flag or an overflow flag. Math equivocates unsigned comparisons with signed comparisons: unsigned < means carry flag, signed < means sign flag != overflow flag. Thus, by coincidence, unsigned < can talk about carry, but < cannot talk about only overflow (without the sign flag). Furthermore, a theorem-proving language wants to prove that overflow cannot happen before attempting to calculate it. So, despite you clearly showing that carry and overflow have the same calculation cost, I don't know how to represent those predicates in a usual math language with equal symbol length or complexity.

by amavect 3mo ago

derdi 3mo ago

What do you mean by notation like: Ensure y+x ≤ INT_MAX. Is this supposed to be a precondition? Why would I want this precondition when using unsigned arithmetic?

amavect 3mo ago
I included that to try to explain the symbol soup that correctly encodes the preconditions (the ∀ lines). I intended that to mean "I need to make sure that y+x doesn't overflow", even that unsigned arithmetic cannot express that precondition in that way, as you point out. From there, derive y ≤ INT_MAX-x as the actual precondition for unsigned addition. I forgot that "ensure" actually means something in some programming languages, sorry for the confusion. More simply put, unsigned addition needs to check that y+x doesn't overflow, while signed addition needs to check that y+x doesn't overflow and doesn't underflow. So, unsigned arithmetic has a simpler precondition that would win a technical debate on whether to use signed or unsigned arithmetic, but since most programming languages lack theorem proving, signed arithmetic wins on the small integer assumption.
- kazinator 3mo ago
  In two's complement, calculating the overflow for addition is nearly exactly as complex as calculating carry for unsigned arithmetic. Various versions of the Motorola 68000 programmer's manuals have a table which succinctly shows the Boolean formulas for calculating the flags for various operations. In the following document it is Table 3-18. Integer Unit Condition Code Computations: https://www.nxp.com/docs/en/reference-manual/M68000PRM.pdf https://www.nxp.com/docs/en/reference-manual/M68000PRM.pdf The ADD operation is in the second row of the table. See how in the right column, the calculation of C (carry out of highest bit) and V (overflow) have about the same complexity. V has only two "not" inversions compared to C's three, but otherwise both have six operands reduced via five "and" or "or" operations. C is a sum of two three-term products, V is a sum of three two-term products. These calculations assume that we perform the addition as unsigned, and so we then have access to all three operands: the S, D, and R (source, destination and result). (That terminology is specific to the MC68K whose instruction set doesn't support the result going to a third operand which is not one of the two input operands.) All the difficulties come from the higher level language semantics that don't provide a way to safely perform an overflowing operation and then detect overflow from a calculation applied to the two inputs and result. I.e. some assembly-language-like "higher level" languages make things worse than assembly language, for the sake of abstraction and portability.
  - amavect 3mo ago
    Cool!! I really like how the overflow condition reads. "When the source and destination have the same sign, but the result a different sign, then signed addition overflows." x86 has SETC/SETNC and SETO/SETNO to pull the carry/overflow bits out of the status register. u+: ADD then SETNC u-: CMP then SETNC s+: ADD then SETNO s-: CMP then SETNO C23 adds checked arithmetic, and gcc implements them as built-in, generating SETO/SETNO. I can't find a way to generate SETNO otherwise. https://godbolt.org/z/4EjecdW1d https://godbolt.org/z/4EjecdW1d #include <stdint.h> #include <stdckdint.h> int add_u(unsigned x, unsigned y){ return x <= ~y; } int sub_u(unsigned x, unsigned y) { return x <= y; } int add_u2(unsigned x, unsigned y){ return !ckd_add(&x, x, y); } int sub_u2(unsigned x, unsigned y) { return !ckd_sub(&x, x, y); } int add_s(int x, int y){ return !ckd_add(&x, x, y); } int sub_s(int x, int y) { return !ckd_sub(&x, x, y); } Now, I the difficulty you talk about goes deeper than high level language semantics. Math and predicate logic can't easily talk about a carry flag or an overflow flag. Math equivocates unsigned comparisons with signed comparisons: unsigned < means carry flag, signed < means sign flag != overflow flag. Thus, by coincidence, unsigned < can talk about carry, but < cannot talk about only overflow (without the sign flag). Furthermore, a theorem-proving language wants to prove that overflow cannot happen before attempting to calculate it. So, despite you clearly showing that carry and overflow have the same calculation cost, I don't know how to represent those predicates in a usual math language with equal symbol length or complexity.