Int.negSucc

Stream: lean4

[Zygimantas Straznickas]

Is Int supposed to be arbitrary precision, like Nat? There's some weirdness with Int.negSucc around Int64Max:

-- (9223372036854775807 == Int64Max)
#eval Int.negSucc 9223372036854775807 -- 0
#eval Int.negSucc 9223372036854775807 == 0 -- false
#eval Int.negSucc 9223372036854775807 == Int64Min -- false
#reduce Int.negSucc 9223372036854775807 == Int64Min -- true
#eval (Int.negSucc 9223372036854775807) + 1 == 1 -- true
#reduce (Int.negSucc 9223372036854775807) + 1 == 1 -- true

[Mario Carneiro]

Oh that's bad. Is it another proof of false?

[Mario Carneiro]

Not a proof of false, just a bad extern

[Zygimantas Straznickas]

Yup, I don’t think the kernel uses Int

[Mario Carneiro]

I suspect https://github.com/leanprover/lean4/blob/master/src/include/lean/lean.h#L1301-L1302 but that should also affect Nat.succ

[Mario Carneiro]

Where did you get Int64Min? I don't see it on the master branch

[Mario Carneiro]

I am also not replicating your result of the first #eval. I get various numbers nondeterministically like -84788720, -67524080, -72164848 which seems worse

[Julian Berman]

(I get seg fault on Lean (version 4.0.0-nightly-2021-03-06, commit be4cf605fde9, Release) )

[Mario Carneiro]

I suspect this is hitting C undefined behavior

[Mario Carneiro]

probably the negation here when given INT_MIN

[Zygimantas Straznickas]

Where did you get Int64Min? I don't see it on the master branch

Just my helper definitions:

def UInt32Max : Nat := UInt32.size - 1
def UInt64Max : Nat := UInt64.size - 1
def Int32Max : Int := (Int.ofNat ((UInt32.size / 2))) - 1
def Int32Min : Int := -1*(Int.ofNat ((UInt32.size / 2)))
def Int64Max : Int := (Int.ofNat ((UInt64.size / 2))) - 1
def Int64Min : Int := -1*(Int.ofNat ((UInt64.size / 2)))

One other weird thing: if I take https://github.com/leanprover/lean4/blob/master/src/include/lean/lean.h#L1509 (impl of Int.negSucc) and replace it with a Lean-defined function that just calls these three native functions, everything works

[Mario Carneiro]

I think I see the error. The code does this:

    lean_obj_res s  = lean_nat_succ(a);    lean_dec(a);
    lean_obj_res i  = lean_nat_to_int(s);  lean_dec(s);
    lean_obj_res r  = lean_int_neg(i);     lean_dec(i);

Here a is 2^63-1. The first step is lean_nat_succ:

    if (LEAN_LIKELY(lean_is_scalar(a)))
        return lean_usize_to_nat(lean_unbox(a) + 1);
    else
        ...

Since a is exactly the largest small nat, lean_unbox(a) + 1 does not overflow and produces 2^63. Since this is now too big for a nat, lean_usize_to_nat returns a new mpz with value 2^63.

The second step, lean_nat_to_int, does nothing because it's already an mpz.

The third step, lean_int_neg, calls lean_int_big_neg:

    return mpz_to_int(neg(mpz_value(a)));

neg is mpz negation and produces -2^63, assuming GMP is implemented correctly, so the last step is mpz_to_int:

    if (m < LEAN_MIN_SMALL_INT || m > LEAN_MAX_SMALL_INT)
        return mpz_to_int_core(m);
    else
        return lean_box(static_cast<unsigned>(m.get_int()));

I'm not 100% sure those inequalities are working correctly, because < is only overloaded for int, unsigned and unsigned long, so it might be casting them to unsigned longs or something, c++ integer promotion is weird. Assuming they work as advertised, we should go into the else branch, where we have more suspicious code: m.get_int() returns an int and is cast to an unsigned and promoted to a size_t, so if int and unsigned are 32 bit as is normal then this seems like it will hit UB (or at least overflow).

[Leonardo de Moura]

Pushed a fix for this bug
https://github.com/leanprover/lean4/commit/8afa96d6c89d7e34e372dda2d2b58abb1378cf8f