Native high-performance arithmetic?

Stream: new members

[Mikhail Hogrefe]

Hi, I'm Mikhail! I'm new to Lean and very excited about what it can do.

I see that when it comes to natural and integer arithmetic, Lean offloads the work to GMP. This is a reasonable thing to do, and it's unlikely at this point that there are significant bugs in GMP... but wouldn't it be nice to use high-performance verified Lean code instead?

Sure, it would be a huge undertaking, but I'd be happy to work on it. I've spent the last few years porting a big chunk of GMP to Rust, so I'm fairly familiar with its code base. For "small" integers, say less than $2^{500}$, GMP generally uses naive algorithms, so just implementing those would be a good start.

My questions to the community are

1. Has something like this been proposed before?

2. Do you think this is a worthwhile thing to do? I know that the use of Coq-style numbers (num) is discouraged; what I'm imagining is a more elaborate version of that, where numbers are arrays of primitive unsigneds; so is there an argument against my idea that I'm unaware of? By the way, I'm not trying to replace ints when it comes to everyday proofs - I'm imaging something like a coercion to fast_int when it comes time to compute things.

3. Would it be appropriate to wait for Lean 4? I'd need to be able to prove things about machine integers, and I don't see a lot of support for that in Lean 3. Lean 4 at least has a placeholder page. In the meantime, I can make some fake machine integers to work with, that are just backed by nat. I'd need efficient arrays too.

[Johan Commelin]

@Mikhail Hogrefe Welcome! I'm not an export on these kind of things. But this sounds like a useful and interesting project!

[Johan Commelin]

I know that @Alex J. Best has some experience with high-performance arithmetic.

[Johan Commelin]

This certainly sounds like a project that is best done in Lean 4, because it is more performant, and also because we hope to transition from Lean 3 to Lean 4 in the next year or so.

[Greg Price]

I think Lean 4 would be a very natural environment to do that in. You may be interested in the discussion of extern here:
https://leanprover.github.io/lean4/doc/lean3changes.html#the-meta-keyword

[Greg Price]

The Lean 4 manual even has a paragraph that seems almost to call for someone to take on this very project:

The sharp-eyed reader will notice that GMP is part of the Lean kernel trusted code base. We believe this is not a problem because you can use external type checkers to double-check your developments, and we consider GMP very trustworthy. Existing external type checkers for Lean 3 (e.g., Trepplein and TC) can be easily adapted to Lean 4. If you are still concerned after checking your development with multiple different external checkers because they may all rely on buggy arbitrary-precision libraries, you can develop your own certified arbitrary-precision library and use it to implement your own type checker for Lean.

[Mikhail Hogrefe]

Thanks, Johan and Greg! Ok, I'll keep an eye on the development of Lean 4, and in the meantime do some experiments in Lean 3 to get a feel for what the implementation might look like.

[Daniel Fabian]

@Mikhail Hogrefe Do take a look at some of the lean 4 code for this. The programming side of lean 4 is different enough that it may be worthwhile to have a look. The whole interaction with the outside world and FFI do look different in Lean 4.