# Zulip Chat Archive

## Stream: lean4

### Topic: Int.negSucc

#### 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
```

#### Mario Carneiro (Mar 07 2021 at 19:35):

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

#### Mario Carneiro (Mar 07 2021 at 19:37):

Not a proof of false, just a bad extern

#### Zygimantas Straznickas (Mar 07 2021 at 19:38):

Yup, I don’t think the kernel uses Int

#### 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`

#### Mario Carneiro (Mar 07 2021 at 19:45):

Where did you get `Int64Min`

? I don't see it on the master branch

#### 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

#### 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)`

)

#### Mario Carneiro (Mar 07 2021 at 19:50):

I suspect this is hitting C undefined behavior

#### Mario Carneiro (Mar 07 2021 at 19:51):

probably the negation here when given `INT_MIN`

#### 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

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

#### 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