# Zulip Chat Archive

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

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

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

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

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

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

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: Dec 20 2023 at 11:08 UTC