## Stream: general

### Topic: nat.pow in core

#### Yury G. Kudryashov (May 25 2020 at 05:49):

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 (May 25 2020 at 06:01):

Related: lean#128

#### Yury G. Kudryashov (May 25 2020 at 06:17):

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

#### Yury G. Kudryashov (May 25 2020 at 06:32):

Where does C++ code register an override?

#### Bryan Gin-ge Chen (May 25 2020 at 06:40):

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

#### Yury G. Kudryashov (May 25 2020 at 06:42):

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

#### Bryan Gin-ge Chen (May 25 2020 at 06:45):

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 (May 25 2020 at 06:46):

But yes, let's see what Gabriel says.

#### Yury G. Kudryashov (May 25 2020 at 06:47):

Many other overrides are explicitly listed here

#### Yury G. Kudryashov (May 25 2020 at 07:19):

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

#### Mario Carneiro (May 25 2020 at 07:20):

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

#### Bryan Gin-ge Chen (May 25 2020 at 07:23):

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 (May 25 2020 at 07:23):

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 (May 25 2020 at 07:36):

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

that was me

#### Mario Carneiro (May 25 2020 at 07:48):

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

#### Mario Carneiro (May 25 2020 at 07:48):

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

#### Mario Carneiro (May 25 2020 at 07:50):

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

#### Mario Carneiro (May 25 2020 at 07:54):

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)

Last updated: May 15 2021 at 00:39 UTC