Zulip Chat Archive

Stream: lean4

Topic: Int.negSucc


view this post on Zulip Zygimantas Straznickas (Mar 07 2021 at 19:20):

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

view this post on Zulip Mario Carneiro (Mar 07 2021 at 19:35):

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

view this post on Zulip Mario Carneiro (Mar 07 2021 at 19:37):

Not a proof of false, just a bad extern

view this post on Zulip Zygimantas Straznickas (Mar 07 2021 at 19:38):

Yup, I don’t think the kernel uses Int

view this post on Zulip Mario Carneiro (Mar 07 2021 at 19:42):

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

view this post on Zulip Mario Carneiro (Mar 07 2021 at 19:45):

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

view this post on Zulip Mario Carneiro (Mar 07 2021 at 19:48):

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

view this post on Zulip Julian Berman (Mar 07 2021 at 19:49):

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

view this post on Zulip Mario Carneiro (Mar 07 2021 at 19:50):

I suspect this is hitting C undefined behavior

view this post on Zulip Mario Carneiro (Mar 07 2021 at 19:51):

probably the negation here when given INT_MIN

view this post on Zulip Zygimantas Straznickas (Mar 07 2021 at 19:56):

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

view this post on Zulip Mario Carneiro (Mar 07 2021 at 20:17):

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).

view this post on Zulip Leonardo de Moura (Mar 07 2021 at 21:11):

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


Last updated: May 18 2021 at 22:15 UTC