Large powers of `1` and `-1`

Stream: lean4

[Aaron Liu]

I was complaining to @Jovan Gerbscheid that there is no @[csimp] lemma for docs#Int.negOnePow, so this code overflows.

import Mathlib.Algebra.Ring.NegOnePow

-- stack overflow
#eval Int.negOnePow <| 10 ^ 2 ^ 10

Then I was confused, since Int.negOnePow would be evaluating (-1) ^ 10 ^ 2 ^ 10, which should presumably be some bignum computation that sees the base is -1 and tests the exponent for even or odd. It turns out docs#Int.pow is defined recursively instead of in terms of Nat.pow, so this also overflows.

-- stack overflow
#eval (1 : Int) ^ 10 ^ 2 ^ 10

and while I was testing it for Nat I discovered that this panics:

-- INTERNAL PANIC: Nat.pow exponent is too big
#eval 1 ^ 10 ^ 2 ^ 10

So

• should Int.pow be defined in terms of Nat.pow?
• should Nat.pow panic when the exponent is too big even when the base is 1 or 0?

[Eric Wieser]

In the past I thought it was strange that we limit b in a ^ b and not log a * b

[Jovan Gerbscheid]

@Eric Wieser, I believe you are talking about #4637. That was about safe exponentiation in the kernel and in whnf. The bound for the exponent is 256 by default and can be changed using set_option exponentiation.threshold).

What @Aaron Liu is complaining about is what happens in compiled code, where the c++ for Nat.powis this:

extern "C" LEAN_EXPORT lean_obj_res lean_nat_pow(b_lean_obj_arg a1, b_lean_obj_arg a2) {
    if (!lean_is_scalar(a2) || lean_unbox(a2) > UINT_MAX) {
        lean_internal_panic("Nat.pow exponent is too big");
    }
    if (lean_is_scalar(a1))
        return mpz_to_nat(mpz::of_size_t(lean_unbox(a1)).pow(lean_unbox(a2)));
    else
        return mpz_to_nat(mpz_value(a1).pow(lean_unbox(a2)));
}

So, the bound for the exponent is 4294967296.

[Eric Wieser]

I think the same argument for using some limit onlog a1 * a2 still applies, especially as log2 should be fast to compute on bignums