Way to turn off integer optimisations?

Stream: general

[Mr Proof]

In Lean 4, I'm told things like large integer multiplications are not written in Lean, but are "optimised" by using some un-verified big-integer library otherwise it would make Lean far too slow.

Ideally we would like Lean kernel to be written in Lean and self-verified. But I think that is not the case at the moment. And even if it was the hardware it is running on is not verified so at some level down the line we just have to go with trust. (In some universe every time a FLT proof is verified a random neutrino flies into the circuits and flips a bit - but I digress....).

As a compromise, is there some way to turn off the big-integer library optimisations, and so all large integer calculations are fully verified within Lean?

Are there other parts of Lean that have been optimised with unverified code? And do these have slower but verifiable alternatives? I assume lists and list-like structures have back end optimisations.

A good choice would be to use the fast optimisations for day-to-day working. But then to turn them off and use slower verifiable Lean code for a final proof check.

(On the alternative point of view are there more Lean objects that could be sped up with a faster unverified backend option for day-to-day work?)

[Robin Arnez]

Well, the only functions that are evaluated in optimized form in the kernel are:
docs#Nat.succ, docs#Nat.add, docs#Nat.sub, docs#Nat.mul, docs#Nat.pow, docs#Nat.gcd, docs#Nat.mod, docs#Nat.div, docs#Nat.beq, docs#Nat.ble, docs#Nat.land, docs#Nat.lor, docs#Nat.xor, docs#Nat.shiftLeft, docs#Nat.shiftRight.
Usually these rely on GMP and we're pretty sure that we can trust GMP; if you don't think so, you can use external type checkers.

[Alex Meiburg]

You can always use https://github.com/digama0/lean4lean/ , which has none of those optimizations you mentioned enabled. (no, it does)

[Robin Arnez]

That's not quite true, see https://github.com/digama0/lean4lean/blob/d74ab2e5bd37537807c157128a292ee7bb4736fb/Lean4Lean/TypeChecker.lean#L408-L432 which uses the same big-int optimizations

[Alex Meiburg]

Oh, by calling it back to the runtime itself? Shoot! Ok.

[Violeta Hernández]

Would it be fair to say that "GMP is correct" is in fact an axiom of Lean? Or to put it another way, if there was some flaw in the GMP implementation, would we be able to prove False without using native_decide?

[Henrik Böving]

You might be able to prove false to the builtin Lean kernel but since there can in principle exist arbitrary re-implementations of Lean that do not make use of GMP those kernels could still detect that fraud attempt (assuming their implementation doesn't happen to suffer from the same bug e.g. because someone copied GMP code into another library).

[Henrik Böving]

For example the nanoda re-implementation uses the num-bigint crate which is completely written in Rust so at least it has no direct code share with GMP.

[Mr Proof]

Robin Arnez said:

Well, the only functions that are evaluated in optimized form in the kernel are:
docs#Nat.succ, docs#Nat.add, docs#Nat.sub, docs#Nat.mul, docs#Nat.pow, docs#Nat.gcd, docs#Nat.mod, docs#Nat.div, docs#Nat.beq, docs#Nat.ble, docs#Nat.land, docs#Nat.lor, docs#Nat.xor, docs#Nat.shiftLeft, docs#Nat.shiftRight.
Usually these rely on GMP and we're pretty sure that we can trust GMP; if you don't think so, you can use external type checkers.

That surprised me that there would be no optimised alternatives for lists/arrays/tensor-arrays etc. (Is this true?) These could also be optimised on the GPU. And so make Lean a language for neural networks and graphics. (Fully backed up with slower verified alternatives). I think Agda and Indris have optimised lists. And indeed do most variants of LISP.

Here it says Arrays are optimised:

I fully trust GMP, I think you can't be a purist in these matters I suppose!

[Robin Arnez]

Just to clarify: array indexing is optimized at runtime (to make O(1) array indexing possible) but not in the kernel/type checker (where array indexing is O(n))

[Robin Arnez]

And if we take your idea of fast but not so reliable vs slow but reliable that's basically the difference between native_decide / docs#Lean.trustCompiler (fast because it can use the Lean compiler and runtime but quite simple to break) and regular decide (slow because it goes through the type checker / kernel but very reliable).

[Bhavik Mehta]

Robin Arnez said:

Well, the only functions that are evaluated in optimized form in the kernel are:
docs#Nat.succ, docs#Nat.add, docs#Nat.sub, docs#Nat.mul, docs#Nat.pow, docs#Nat.gcd, docs#Nat.mod, docs#Nat.div, docs#Nat.beq, docs#Nat.ble, docs#Nat.land, docs#Nat.lor, docs#Nat.xor, docs#Nat.shiftLeft, docs#Nat.shiftRight.
Usually these rely on GMP and we're pretty sure that we can trust GMP; if you don't think so, you can use external type checkers.

Most of these contain an explicit message in the docstring that they're optimised in the kernel, but Nat.div doesn't. Is there something I can check to generate/confirm the list?

[Aaron Liu]

docs#Lean.Meta.reduceNat?

[Aaron Liu]

has a list of elaborator-optimized functions

[Bhavik Mehta]

Hmm, is that the same as the kernel-optimized functions? That would surprise me

[Aaron Liu]

the kernel list seems to be here

[Aaron Liu]

they're in a different order but it's all the same functions

[Bhavik Mehta]

That's the one I wanted, thanks!

[Bhavik Mehta]

The earlier one isn't getting called for kernel reduction (in particular in my application), eg

def myFunc : Nat → Nat → Nat := Nat.add

set_option trace.Meta.isDefEq.whnf.reduceBinOp true

example : myFunc 2304920 109108 = 2414028 := by
  decide -- reduces in the elaborator, then kernel, so has a trace

example : myFunc 2304920 109108 = 2414028 := by
  decide +kernel -- reduces only in the kernel, so has no trace