Primality proofs for primes related to EC crytography

Stream: CSLib

[Oliver Butterley]

Right now I would like a proof that 2^255 - 19 is prime and soon I suspect I need the same information for others similar primes. Two questions:

• Is CSLib going to be the correct place for this? I had in mind something like this collection of many ECC relevant primes together with the primality proofs.

• Did anyone already prove that 2^255 - 19 is prime in Lean? Or how far are we from this? I suspect this folder of @Bhavik Mehta gives most of the relevant arguments. Are there plans to upstream this to mathlib sometime?

[Bhavik Mehta]

I had indeed proved this number is prime. The most up to date version however will be in @Kenny Lau's repo, and although this example may not be already there, I expect it won't take long to appear!

[Oliver Butterley]

That's great! We'll keep a sorry in our code for the moment and then connect to your proof soon.

[Kenny Lau]

https://github.com/kckennylau/PrimeCert/blob/master/PrimeCert/PrimeList.lean#L84 @Oliver Butterley

[Oliver Butterley]

Thanks @Kenny Lau, that makes it very easy.

[Bas Spitters]

How does Lean currently compare to Rocq. https://github.com/thery/coqprime
I guess these benchmarks are some 8 years old, so it would be interesting to update them.
Also, what is the TCB for this proof in Lean? Does it use unverified integer computation in C++ ?

[Bhavik Mehta]

It uses only Lean's kernel, no native compute. This does use GMP for natural number computation, for values larger than 2^64, in particular for the operations listed here https://github.com/leanprover/lean4/blob/ae86c18ac19cee9bdf4e63cde2c11694e3217b70/src/kernel/type_checker.cpp#L613 (though in my version, not all these operations were used, and I expect similar for Kenny's upgraded version of mine). The benchmarks listed in the coqprime readme are specifically for Mersenne numbers; for which the Lucas-Lehmer test is more efficient, so a direct comparison wouldn't be entirely fair. This is, however, in mathlib, with some examples in mathlib's archive, although I think Kenny and I have optimised certain parts of this computation that the PrimeCert version might be faster than the mathlib version.

[Henrik Böving]

Does it use unverified integer computation in C++ ?

All kernel proofs that do reduction on closed Nat/Int terms use unverified integer computation in C++ in Lean. Do you mean to ask whether it makes use of native_decide?

I find these TCB comparisons between Rocq and Lean proofs a bit difficult btw. For example in Lean people will say, we have this native_decide thing that is outside of the kernel so you can opt into it. On the other hand we have the Rocq kernel which has iirc 2 evaluation engines that do an equivalent of native_decide built-in (albeit with less optimizations and, unlike Lean's native_decide, for open terms). So saying that something is done "with just the kernel" has completely different meaning for Rocq and for Lean.

[Bas Spitters]

Thanks. Yes, that's what I understood, that Lean depends on C++ integer computation.

Rocq has compute, vm_compute (https://dl.acm.org/doi/abs/10.1145/583852.581501, a verified VM) and native_compute (https://inria.hal.science/hal-00650940/file/full_throttle.pdf) a somewhat verified way of using extraction to ocaml. Work is under way, on using Rocq's new verified extraction to ocaml/malfunction (https://github.com/MetaRocq/rocq-verified-extraction).

Is there a paper describing native_decide?

[Henrik Böving]

native_decide is just Lean's normal compiler

[Bas Spitters]

Which is unverified, and is described in https://arxiv.org/abs/1908.05647 ?

[Bhavik Mehta]

I think section 3 of https://lean-lang.org/papers/lean4.pdf gives a small amount of description too

[Henrik Böving]

It is unverified yes, it will also likely never be verified. The algorithms from immutable beans counting have a formal proof in Marc Huisinga's Bachelor thesis but they amount only to the very last bits of the transformation pipeline. The main chunk of the transformation pipeline is just a normal functional compiler. That would make it quite difficult to publish a paper about given that there is not really anything new happening (in combination with the fact that time was tight when the largest chunk of the code was written in 2022/23). The description from the Lean 4 tool paper is, somewhat amusingly, so undetailed that it still holds true despite a full rewrite of about 2/3rds of the compiler.

[Bas Spitters]

Thanks @Bhavik Mehta. Yes, they point to the cool work on Perseus, which talks about a formalization, with which I believe they mean "mathematically precise" not in a proof assistant, but I may have overlooked something.
https://dl.acm.org/doi/pdf/10.1145/3453483.3454032
IIUC this approach does not work for coinductive types.

[Henrik Böving]

Bas Spitters said:

Thanks Bhavik Mehta. Yes, they point to the cool work on Perseus, which talks about a formalization, with which I believe they mean "mathematically precise" not in a proof assistant, but I may have overlooked something.
https://dl.acm.org/doi/pdf/10.1145/3453483.3454032
IIUC this approach does not work for coinductive types.

Perceus is an algorithm based on the immutable beans counting paper by de Moura and Ullrich that has a formalization in Marc's Bachelor thesis as I just said.

[Bas Spitters]

Thanks @Henrik Böving ! our messages crossed.

[Henrik Böving]

https://pp.ipd.kit.edu/uploads/publikationen/huisinga19bachelorarbeit.pdf here's the thesis for reference

[Bas Spitters]

@Bhavik Mehta Rocq-prime also has Pocklington. It should be easy to run some more extensive benchmarks, but at least here is a statement:

Proving the primality of a number of about 1200 decimal digits takes about 9 hours

However, that should be corrected for Moore's law, and it still uses Rocq's regular compute, as opposed to a more optimized one.

How long does it take to check a 1200 decimal digit number in Lean?
Unfortunately, the README does not say what the 1200 digit number was ...

[Alessandro D'Angelo]

Kenny Lau said:

https://github.com/kckennylau/PrimeCert/blob/master/PrimeCert/PrimeList.lean#L84 Oliver Butterley

Hi Kenny! I'm new here, but I'm working with Oliver on an issue related to this. I was wondering is the repo maintained? Would it make sense a PR to update it to mathlib 4.25.2? I'd be down to do that

[Oliver Butterley]

@Kenny Lau Some extra context: we are working a project verifying some ecc code in lean. For that we need the primality proof. It would be convenient to add your repo as a dependency for this. However we recently updated to the newer version of lean.

[Oliver Butterley]

Assuming that your intention is to keep the PrimeCert as a reference repo for these primality proofs, would it make sense to setup a system for auto tagging releases as lean updates?

[Bhavik Mehta]

I've added and (auto) tagged versions of the repo for 4.25.0, 4.25.1, 4.25.2. Hope this helps :)

[Oliver Butterley]

Thanks! That's perfect.