nat.pow in core

Stream: general

[Yury G. Kudryashov]

I can't find nat.pow in https://github.com/leanprover-community/lean/tree/master/src/library/vm
Does it mean that nat.pow has no vm override and we can remove it from core?

[Bryan Gin-ge Chen]

Related: lean#128

[Yury G. Kudryashov]

In this discussion @Gabriel Ebner says that nat.pow has an efficient vm implementation. I can't find it.

[Bryan Gin-ge Chen]

Is it done by GMP? cf. https://github.com/leanprover-community/lean/blob/ec1613aef1eee72e601f192b16740629c6d49690/src/util/numerics/mpz.h

[Yury G. Kudryashov]

Where does C++ code register an override?

[Bryan Gin-ge Chen]

Maybe this function? I'm really just guessing though.

[Yury G. Kudryashov]

Do you see pow in this function? I don't. Let's wait for @Gabriel Ebner .

[Bryan Gin-ge Chen]

This is very fuzzy, but my working theory is that pow is overridden by a method for GMP's mpz type in the first file I linked. Somewhere in the second file, Lean nats are replaced by mpz in the VM.

[Bryan Gin-ge Chen]

But yes, let's see what Gabriel says.

[Yury G. Kudryashov]

Many other overrides are explicitly listed here

[Yury G. Kudryashov]

(probably the answer is "nat.pow is not here but should be")

[Mario Carneiro]

There are lots of other useful functions from gmp that could be exposed but aren't

[Bryan Gin-ge Chen]

Yeah, I think I was wrong. nat.pow doesn't seem to be overridden after all?

set_option trace.compiler.code_gen true
#eval 3*3
/-
[compiler.code_gen]  _main 0
0: scnstr #3
1: scnstr #3
2: cfun nat.mul -- I guess this means it's calling a C++ function
3: cfun nat.repr
4: ret
-/
#eval 3^3
/-
[compiler.code_gen]  _main 0
0: scnstr #3
1: scnstr #3
2: ginvoke nat.pow._main -- this is just using the Lean definition?
3: cfun nat.repr
4: ret
-/

[Mario Carneiro]

From https://gmplib.org/manual/Number-Theoretic-Functions.html#Number-Theoretic-Functions I see: gcd, lcm, legendre/jacobi/kronecker symbols, fibonacci and lucas numbers, modular inverses, probabilistic primes (dunno if this is useful without a proof of correctness)

[Gabriel Ebner]

Yury G. Kudryashov said:

In this discussion Gabriel Ebner says that nat.pow has an efficient vm implementation. I can't find it.

Ooops, no idea what I got that impression from. Indeed, I can confirm that there is no VM implementation of int.pow or nat.pow. It's a bit of an odd omission, there are like three different efficient implementations division: right shifts, division by two, a function that returns the pair (division by two, modulo 2).

[Mario Carneiro]

that was me

[Mario Carneiro]

Most of my work there was on the lean side, I think there is only basic support from the C++ side

[Mario Carneiro]

But I guess this means that nat.pow is implemented in unary wrt the exponent?

[Mario Carneiro]

Actually I think the support for bitwise stuff is not great, most importantly because bit0 is not a left shift

[Mario Carneiro]

Another nice GMP function I wish we had is divexact, which is a partial version of integer division that is only defined when the result is representable (i.e. the denominator divides the numerator)