Fix signed safemath

[cag]

I also have a proof of correctness here:

---

Let +, -, * be the usual arithemetic operators on the integers, and / be integer division.

Let the integers in the range [-2^255, 2^255-1] be the space of int256s

Given int256s a and b, define a OP b overflows iff a OP b is not in int256s

Let ⊕, ⊖, ⊗, ⊘ be corresponding operators on int256s, where WLOG for all operators, a ⊕ b is equivalent to a + b (mod 2^256)

Note that WLOG for all operators, a + b == a ⊕ b iff a + b doesn't overflow.

---

• Assume int256s a, b

  • Assume b < 0

    • a + b < a
    • Assume a + b doesn't overflow
      • a ⊕ b == a + b < a
    • Assume a + b overflows
      • Either a + b < -2^255 or a + b > 2^255-1
      • a + b < a <= 2^255-1 means a + b < -2^255
      • -2^255 <= a < -2^255 - b <= 0 (due to int256 bounds for a and b)
      • -2^255 - 2^255 <= a + b < -2^255
      • 0 <= a + b + 2^256 < 2^255 is contained in int256
      • a ⊕ b == a + (b + 2^256) >= a + 2^255 >= a
    • a + b doesn't overflow iff a ⊕ b < a

  • Assume b >= 0

    • a + b >= a
    • Assume a + b doesn't overflow
      • a ⊕ b == a + b >= a
    • Assume a + b overflows
      • Either a + b < -2^255 or a + b > 2^255-1
      • a + b >= a >= -2^255 means a + b > 2^255-1
      • 2^255-1 >= a > 2^255-1 - b >= 0 (due to int256 bounds for a and b)
      • 2^255-1 + 2^255-1 >= a + b > 2^255-1
      • -2 >= a + b - 2^256 > -2^255 is contained in int256
      • a ⊕ b == a + (b - 2^256) <= a - 2^255 - 1 < a
    • a + b doesn't overflow iff a ⊕ b >= a

  • (b < 0 and a ⊕ b < a) or (b >= 0 and a ⊕ b >= a) implies a + b doesn't overflow

---

• Assume int256s a, b
  • a - b == a + (-b)
  • Assume b != -2^255
    • a ⊖ b == a ⊕ (-b)
    • (-b < 0 and a ⊕ -b < a) or (-b >= 0 and a ⊕ -b >= a) implies a - b doesn't overflow
    • (b > 0 and a ⊖ b < a) or (b <= 0 and a ⊖ b >= a) implies a - b doesn't overflow
  • Assume b == -2^255
    • b <= 0 (from assumption)
    • Assume a - b overflows
      • Either a - b < -2^255 or a - b > 2^255-1
      • -2^255 <= 0 <= a - b == a + 2^255, so a - b == a + 2^255 > 2^255-1
      • 2^255-1 < a - b < 2^255 + 2^255-1
      • -1 < a < 2^255-1
      • a ⊖ b == a - b - 2^256 == a - 2^255 < a
    • a - b overflows implies a ⊖ b < a
    • a ⊖ b >= a implies a - b doesn't overflow (via contrapositive)
    • (b > 0 and a ⊖ b < a) or (b <= 0 and a ⊖ b >= a) implies a - b doesn't overflow
  • (b > 0 and a ⊖ b < a) or (b <= 0 and a ⊖ b >= a) implies a - b doesn't overflow via case analysis

---

• For integers a and b where b != 0, abs(a / b) == abs(a) / abs(b)

• Assume int256s a, b where b != 0

  • abs(b) >= 1

  • Assume a != -2^255

    • a is in the range [-(2^255-1), 2^255-1]
    • abs(a) <= 2^255-1
    • abs(a / b) == abs(a) / abs(b) <= abs(a) / 1 == abs(a) <= 2^255-1
    • a / b is in the range [-(2^255-1), 2^255-1]
    • a / b doesn't overflow

  • Assume a == -2^255

    • Assume abs(b) > 1
      • abs(a / b) == abs(a) / abs(b) < abs(a) / 1 == abs(a) == -2^255
      • a / b is in the range [-(2^255-1), 2^255-1]
      • a / b doesn't overflow
    • Assume b == 1
      • a / b == -2^255 is an int256
      • a / b doesn't overflow
    • Assume b == -1
      • a / b == 2^255 is not an int256
      • a / b overflows

  • a / b doesn't overflow (a / b == a ⊘ b) iff a != -2^255 or b != -1

---

• Assume int256s a, b, (we want find necessary and sufficient conditions for when a * b doesn't overflow)

  • Assume a == 0

    • a * b == 0 doesn't overflow

  • Assume a != 0

    • a * b / a == b
    • Assume a * b doesn't overflow
      • a * b == a ⊗ b is an int256
      • a ⊗ b / a == b is an int256 (doesn't overflow)
      • a * b / a == a ⊗ b ⊘ a == b
    • Assume a ⊗ b ⊘ a == b
      • Assume a ⊗ b == -2^255, and a == -1 (⊘ overflows in a ⊗ b ⊘ a)
        • Assume a * b doesn't overflow
          • -1 ⊗ b == -1 * b == -2^255
          • b == 2^255
          • Contradiction: but b is an int256, therefore...
        • a * b overflows
        • a * b == -1 * b not an int256
        • b == -2^255 (this is the only int256 for which the above condition holds)
      • Assume ⊘ doesn't overflow in a ⊗ b ⊘ a
        • a ⊗ b ⊘ a == a ⊗ b / a == b
        • a ⊗ b == a * b
        • a * b == 0 doesn't overflow

  • a * b doesn't overflow (a * b == a ⊗ b) iff (a != -1 or b != -2^255) and (a == 0 or a ⊗ b ⊘ a == b)